{-# OPTIONS --cubical --type-in-type #-}

module _ where

open import Cubical.Foundations.Everything
open import Cubical.Foundations.Equiv
open import Cubical.Functions.Image
open import Cubical.HITs.PropositionalTruncation as P
open import Cubical.Data.Nat
open import Cubical.Data.FinData as F
open import Cubical.Data.List as L
open import Cubical.Data.List.FinData as F
open import Cubical.Data.Sigma
open import Cubical.Reflection.RecordEquiv
open import Cubical.HITs.SetQuotients as Q
open import Agda.Primitive

record Sig : Type₁ where
  field
    symbol : Type
    arity : symbol -> ℕ
open Sig public

module _ (σ : Sig) where
  sig : Type -> Type
  sig X = Σ (σ .symbol) \f -> Fin (σ .arity f) -> X

  sigF : {X Y : Type} -> (X -> Y) -> sig X -> sig Y
  sigF h (f , i) = f , h ∘ i

module _ (σ : Sig) where
  struct : Type₁
  struct = Σ Type (\X -> sig σ X -> X)

  structIsHom : (𝔛 𝔜 : struct) (h : 𝔛 .fst -> 𝔜 .fst) -> Type
  structIsHom (X , α) (Y , β) h =
    ((f , i) : sig σ X) -> β (f , h ∘ i) ≡ h (α (f , i))

  structHom : struct -> struct -> Type
  structHom 𝔛 𝔜 = Σ[ h ∈ (𝔛 .fst -> 𝔜 .fst) ] structIsHom 𝔛 𝔜 h

record EqSig : Type₁ where
  field
    name : Type
    free : name -> Type
open EqSig public

data Tree (σ : Sig) (V : Type) : Type where
  leaf : V -> Tree σ V
  node : sig σ (Tree σ V) -> Tree σ V

module _ {σ : Sig} (𝔛 : struct σ) where
  ext : {V : Type} -> (V -> 𝔛 .fst) -> Tree σ V -> 𝔛 .fst
  ext h (leaf v) = h v
  ext h (node (f , i)) = 𝔛 .snd (f , (ext h ∘ i))

  extHom : {V : Type} -> (V -> 𝔛 .fst) -> structHom σ (Tree σ V , node) 𝔛
  extHom h = ext h , \_ → refl

module _ (σ : Sig) (τ : EqSig) where
  eqs : Type
  eqs = (e : τ .name) -> Tree σ (τ .free e) × Tree σ (τ .free e)

module _ {σ : Sig} {τ : EqSig} where
  infix 30 _⊨_
  _⊨_ : struct σ -> eqs σ τ -> Type
  𝔛 ⊨ ε = (e : τ .name) (ρ : τ .free e -> 𝔛 .fst)
       -> ext 𝔛 ρ (ε e .fst) ≡ ext 𝔛 ρ (ε e .snd)

module Free1 (σ : Sig) (τ : EqSig) (ε : eqs σ τ) where

  congruence relation generated by equations
  data _≈_ {X : Type} : Tree σ X -> Tree σ X -> Type₁ where
    ≈-refl : ∀ t -> t ≈ t
    ≈-sym : ∀ t s -> t ≈ s -> s ≈ t
    ≈-trans : ∀ t s r -> t ≈ s -> s ≈ r -> t ≈ r
    ≈-cong : (f : σ .symbol) -> {t s : Fin (σ .arity f) -> Tree σ X}
          -> ((a : Fin (σ .arity f)) -> t a ≈ s a)
          -> node (f , t) ≈ node (f , s)
    ≈-eqs : (𝔜 : struct σ) (ϕ : 𝔜 ⊨ ε)
         -> (e : τ .name) (ρ : X -> 𝔜 .fst)
         -> ∀ t s -> ext 𝔜 ρ t ≡ ext 𝔜 ρ t
         -> t ≈ s

  Free : Type -> Type₁
  Free X = Tree σ X / _≈_

  test1 : {X : Type} (n : ℕ) -> (Fin n -> Free X) -> (Fin n -> Tree σ X)
  test1 zero i ()
  test1 (suc n) i zero = {!!} ??
  test1 (suc n) i (suc k) = test1 n (i ∘ weakenFin) k

  freeAlg : (X : Type) -> sig σ (Free X) -> Free X
  freeAlg X (f , i) = Q.[ node (f , {!!}) ] needs choice?

  freeStruct : (X : Type) -> struct σ
  freeStruct X = Free X , freeAlg X

module Free2 (σ : Sig) (τ : EqSig) (ε : eqs σ τ) where

  mutual
    data Free (X : Type) : Type where
      η : X -> Free X
      α : sig σ (Free X) -> Free X
      sat : (Free X , α) ⊨ ε

    ext 𝔜 (sharp ϕ h ∘ ρ) (ε₁ e .snd) !=
    sharp ϕ h (ext (Free X , α) ρ (ε₁ e .snd))

    sharp : {X : Type} {𝔜 : struct σ} (ϕ : 𝔜 ⊨ ε) (h : X -> 𝔜 .fst) -> Free X -> 𝔜 .fst
    sharp ϕ h (η x) = h x
    sharp {𝔜 = 𝔜} ϕ h (α (f , o)) = 𝔜 .snd (f , (sharp ϕ h ∘ o))
    sharp ϕ h (sat e ρ i) = ϕ e (sharp ϕ h ∘ ρ) {!i!}