module Experiments.FreeByTree where
-- -- constructions of a free structure on a signature and equations
-- -- TODO: generalise the universe levels!!
-- -- using a HIT
-- module Construction {f a e n : Level} (σ : Sig f a) (τ : EqSig e n) (ε : seq σ τ) where
--
--   data Free (X : Type n) : Type (ℓ-suc (ℓ-max f (ℓ-max a (ℓ-max e n)))) where
--       η : X -> Free X
--       α : sig σ (Free X) -> Free X
--       sat : mkStruct (Free X) α ⊨ ε

--  freeStruct : (X : Type) -> struct σ
--  car (freeStruct X) = Free X
--  alg (freeStruct _) = α
--
--  module _ (X : Type) (𝔜 : struct σ) (ϕ : 𝔜 ⊨ ε) where

    -- private
    --   Y = 𝔜 .fst
    --   β = 𝔜 .snd

    -- ext : (h : X -> Y) -> Free X -> Y
    -- ext h (η x) = h x
    -- ext h (α (f , o)) = β (f , (ext h ∘ o))
    -- ext h (sat e ρ i) = ϕ e (ext h ∘ ρ) {!i!}

    -- module _  where
    --   postulate
    --     Fr : Type (ℓ-max (ℓ-max f a) n)
    --     Fα : sig σ Fr -> Fr
    --     Fs : sat σ τ ε (Fr , Fα)

    --   module _ (Y : Type (ℓ-max (ℓ-max f a) n)) (α : sig σ Y -> Y) where
    --     postulate
    --       Frec : sat σ τ ε (Y , α) -> Fr -> Y
    --       Fhom : (p : sat σ τ ε (Y , α)) -> walgIsH σ (Fr , Fα) (Y , α) (Frec p)
    --       Feta : (p : sat σ τ ε (Y , α)) (h : Fr -> Y) -> walgIsH σ (Fr , Fα) (Y , α) h -> Frec p ≡ h

-- -- using a quotient
-- module Construction2 (σ : Sig ℓ-zero ℓ-zero) (τ : EqSig ℓ-zero ℓ-zero) (ε : seq σ τ) where
--
--   -- congruence relation generated by equations
--   data _≈_ {X : Type} : Tree σ X -> Tree σ X -> Type (ℓ-suc ℓ-zero) 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 : σ .arity f -> Tree σ X}
--           -> ((a : σ .arity f) -> t a ≈ s a)
--           -> node (f , t) ≈ node (f , s)
--     ≈-eqs : (𝔜 : struct {ℓ-zero} {ℓ-zero} {ℓ-zero} σ) (ϕ : 𝔜 ⊨ ε)
--          -> (e : τ .name) (ρ : X -> 𝔜 .car)
--          -> ∀ t s -> sharp σ {𝔜 = 𝔜} ρ t ≡ sharp σ {𝔜 = 𝔜} ρ s
--          -> t ≈ s
--
--   Free : Type -> Type₁
--   Free X = Tree σ X / _≈_
--
--   -- 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 _ (X : Type) (𝔜 : struct σ) (ϕ : 𝔜 ⊨ ε) where
--
--   --   private
--   --     Y = 𝔜 .fst
--   --     β = 𝔜 .snd