{-# OPTIONS --cubical --safe --exact-split #-}

module Cubical.Structures.Set.Empty where

open import Cubical.Foundations.Everything
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty as 
import Cubical.Data.List as L

import Cubical.Structures.Free as F
open import Cubical.Structures.Sig
open import Cubical.Structures.Str public
open import Cubical.Structures.Tree
open import Cubical.Structures.Eq
open import Cubical.Structures.Arity

private
  variable
     ℓ' : Level
    A : Type 

empty-α :  (A : Type ) -> sig emptySig A -> A
empty-α _ (x , _) = ⊥.rec x

emptyHomDegen : (𝔜 : struct ℓ' emptySig) -> structHom < A , empty-α A > 𝔜  (A -> 𝔜 .car)
emptyHomDegen _ = Σ-contractSnd λ _ -> isContrΠ⊥

module EmptyDef = F.Definition emptySig emptyEqSig emptySEq

empty-sat :  (A : Type ) -> < A , empty-α A >  emptySEq
empty-sat _ eqn ρ = ⊥.rec eqn

treeEmpty≃  : Tree emptySig A  A
treeEmpty≃ = isoToEquiv (iso from leaf  _ -> refl) leaf∘from)
  where
  from : Tree emptySig A -> A
  from (leaf x) = x

  leaf∘from : retract from leaf
  leaf∘from (leaf x) = refl

treeDef :  { ℓ'} -> EmptyDef.Free  ℓ' 2
F.Definition.Free.F treeDef = Tree emptySig
F.Definition.Free.η treeDef = leaf
F.Definition.Free.α treeDef = empty-α (Tree emptySig _)
F.Definition.Free.sat treeDef = empty-sat (Tree emptySig _)
F.Definition.Free.isFree (treeDef { = }) {X = A} {𝔜 = 𝔜} H ϕ = lemma .snd
  where
  𝔗 : struct  emptySig
  𝔗 = < Tree emptySig A , empty-α (Tree emptySig A) >

  lemma : structHom 𝔗 𝔜  (A -> 𝔜 .car)
  lemma =
    structHom 𝔗 𝔜 ≃⟨ emptyHomDegen 𝔜 
    (𝔗 .car -> 𝔜 .car) ≃⟨ equiv→ treeEmpty≃ (idEquiv (𝔜 .car)) 
    (A -> 𝔜 .car) 
    
anyDef :  { ℓ'} -> EmptyDef.Free  ℓ' 2
F.Definition.Free.F anyDef A = A
F.Definition.Free.η anyDef a = a
F.Definition.Free.α anyDef = empty-α _
F.Definition.Free.sat anyDef = empty-sat _
F.Definition.Free.isFree anyDef {𝔜 = 𝔜} _ _ = emptyHomDegen 𝔜 .snd