{-# 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 ℓ ℓ' 
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 ℓ ℓ' 
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