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

module Cubical.Structures.Set.CMon.SList.Head where

open import Cubical.Foundations.Everything
open import Cubical.Data.Sigma
open import Cubical.Data.Maybe
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty as 
open import Cubical.Induction.WellFounded
import Cubical.Data.List as L
open import Cubical.Functions.Logic as L
open import Cubical.HITs.PropositionalTruncation as P
open import Cubical.Data.Sum as 
open import Cubical.Relation.Nullary as R
open import Cubical.Relation.Binary.Order

open import Cubical.Structures.Prelude
import Cubical.Structures.Set.Mon.Desc as M
import Cubical.Structures.Set.CMon.Desc as M
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
open import Cubical.Structures.Set.Mon.List hiding (module Head)

open import Cubical.Structures.Set.CMon.SList.Base as SList

private
  variable
     : Level
    A : Type 

module Head {} {A : Type } (isSetA : isSet A) (_≤_ : A -> A -> Type ) (tosetA : IsToset _≤_) where

  open Toset.Toset-⋀ isSetA _≤_ tosetA

  _⊕_ : Maybe A -> Maybe A -> Maybe A
  nothing  b = b
  just a  nothing = just a
  just a  just b = just (a  b)

  ⊕-unitl :  x -> nothing  x  x
  ⊕-unitl x = refl

  ⊕-unitr :  x -> x  nothing  x
  ⊕-unitr nothing = refl
  ⊕-unitr (just x) = refl

  ⊕-assocr :  x y z -> (x  y)  z  x  (y  z)
  ⊕-assocr nothing y z = refl
  ⊕-assocr (just x) nothing z = refl
  ⊕-assocr (just x) (just y) nothing = refl
  ⊕-assocr (just x) (just y) (just z) = congS just (⋀-assocr x y z)

  ⊕-comm :  x y -> x  y  y  x
  ⊕-comm nothing y = sym (⊕-unitr y)
  ⊕-comm (just x) nothing = refl
  ⊕-comm (just x) (just y) = congS just (⋀-comm x y)

  Maybe-MonStr : M.MonStruct
  car Maybe-MonStr = Maybe A
  alg Maybe-MonStr (M.`e , _) = nothing
  alg Maybe-MonStr (M.`⊕ , i) = i fzero  i fone

  Maybe-MonStr-MonSEq : Maybe-MonStr  M.MonSEq
  Maybe-MonStr-MonSEq M.`unitl ρ = ⊕-unitl (ρ fzero)
  Maybe-MonStr-MonSEq M.`unitr ρ = ⊕-unitr (ρ fzero)
  Maybe-MonStr-MonSEq M.`assocr ρ = ⊕-assocr (ρ fzero) (ρ fone) (ρ ftwo)

  Maybe-MonStr-CMonSEq : Maybe-MonStr  M.CMonSEq
  Maybe-MonStr-CMonSEq (M.`mon eqn) ρ = Maybe-MonStr-MonSEq eqn ρ
  Maybe-MonStr-CMonSEq M.`comm ρ = ⊕-comm (ρ fzero) (ρ fone)

  open SList.Free {A = A} (isOfHLevelMaybe 0 isSetA) Maybe-MonStr-CMonSEq

  head : SList A -> Maybe A
  head = just 

  head-[] : head []  nothing
  head-[] = refl

  head-[x] :  x -> head [ x ]  just x
  head-[x] _ = refl

  head-[x,y] :  x y -> head (x  y  [])  just (x  y)
  head-[x,y] _ _ = refl