module Spice where

------------------------------------------------------------------------------
-- We'll be using the Cubical Agda standard Library:

open import Cubical.Foundations.Prelude
  renaming ( congS to ap
           ; cong to apd
           ; congP to apP
           ; subst to tpt
           )
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Relation.Binary.Order.Toset
import Cubical.HITs.PropositionalTruncation as PTrunc
import Cubical.Functions.Logic as L
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
import Cubical.Data.Nat.Order as Nat
open import Cubical.Data.Unit renaming (Unit to πŸ™ ; tt to ⋆)
open import Cubical.Data.Empty hiding (rec)
open import Cubical.Data.Sum hiding (rec)
import Cubical.Data.Sum as ⊎ using (rec)

variable
  β„“ β„“' β„“'' : Level
  A B C : Type β„“

------------------------------------------------------------------------------

------------------------------------------------------------------------------
-- Spicy Lists
------------------------------------------------------------------------------

module SLists where

  infixr 10 _∷_

  data SList {β„“} (A : Type β„“) : Type β„“ where
    []  : SList A
    _∷_ : A β†’ SList A β†’ SList A
    swap : (x y : A) (xs : SList A) β†’ x ∷ y ∷ xs ≑ y ∷ x ∷ xs
    trunc : isSet (SList A)

  {- eliminators -}
  module SListElim where
    module _ (P : SList A β†’ Type β„“')
         ([]* : P [])
         (_∷*_ : (x : A) {xs : SList A} β†’ P xs β†’ P (x ∷ xs))
         (swap* : (x y : A) {xs : SList A} (p : P xs) β†’ PathP (Ξ» i β†’ P (swap x y xs i)) (x ∷* (y ∷* p)) (y ∷* (x ∷* p)))
         (trunc* : (xs : SList A) β†’ isSet (P xs)) where

      ind : (xs : SList A) β†’ P xs
      ind [] = []*
      ind (x ∷ xs) = x ∷* ind xs
      ind (swap x y xs i) = swap* x y (ind xs) i
      ind (trunc x y p q i j) =
             isSet→SquareP (λ i j → trunc* (trunc x y p q i j)) (apd ind p) (apd ind q) refl refl i j

    module _ {A : Type β„“} (P : SList A β†’ Type β„“')
         ([]* : P [])
         (_∷*_ : (x : A) {xs : SList A} β†’ P xs β†’ P (x ∷ xs))
         (trunc* : (xs : SList A) β†’ isProp (P xs)) where

      private
        swap* : (x y : A) {xs : SList A} (p : P xs) β†’ PathP (Ξ» i β†’ P (swap x y xs i)) (x ∷* (y ∷* p)) (y ∷* (x ∷* p))
        swap* x y {xs} p = isPropβ†’PathP (Ξ» i β†’ trunc* (swap x y xs i)) (x ∷* (y ∷* p)) (y ∷* (x ∷* p))

      indProp : (xs : SList A) β†’ P xs
      indProp = ind P []* _∷*_ swap* (Ξ» xs β†’ isPropβ†’isSet (trunc* xs))

    module _ {A : Type β„“} (P : Type β„“')
         ([]* : P)
         (_∷*_ : A β†’ P β†’ P)
         (swap* : (x y : A) β†’ (p : P) β†’ Path P (x ∷* (y ∷* p)) (y ∷* (x ∷* p)))
         (trunc* : isSet P) where

      rec : SList A β†’ P
      rec = ind (Ξ» _ β†’ P) []* (Ξ» x {xs} β†’ x ∷*_) (Ξ» x y {xs} β†’ swap* x y) (Ξ» _ β†’ trunc*)






  {- permutations -}
  as : SList β„•
  as = 1 ∷ 2 ∷ 3 ∷ []

  bs : SList β„•
  bs = 3 ∷ 2 ∷ 1 ∷ []

  p : as ≑ bs
  p = swap 1 2 _ βˆ™ ap (2 ∷_) (swap 1 3 _) βˆ™ swap 2 3 _

  q : as ≑ bs
  q = ap (1 ∷_) (swap 2 3 _) βˆ™ swap 1 3 _ βˆ™ ap (3 ∷_) (swap 1 2 _)

  _ : p ≑ q
  _ = trunc as bs p q

  -- head : βˆ€ {a} {A : Type a} β†’ SList A β†’ πŸ™ ⊎ A
  -- head [] = inl ⋆
  -- head (x ∷ xs) = inr x
  -- head (swap x y xs i) = inr {!!}
  -- head (trunc x xs p q i j) = {!!}











module Monoid where

  open import Cubical.Data.List

  pattern [_∢_]       a b         = a ∷ b ∷ []
  pattern [_∢_∢_]     a b c       = a ∷ b ∷ c ∷ []
  pattern [_∢_∢_∢_]   a b c d     = a ∷ b ∷ c ∷ d ∷ []
  pattern [_∢_∢_∢_∢_] a b c d e   = a ∷ b ∷ c ∷ d ∷ e ∷ []

  record Mon {a} (A : Type a) : Type a where
    infixr 10 _βŠ•_
    field
      e : A
      _βŠ•_ : A β†’ A β†’ A
      unitl : βˆ€ x β†’ e βŠ• x ≑ x
      unitr : βˆ€ x β†’ x βŠ• e ≑ x
      assocr : βˆ€ x y z β†’ (x βŠ• y) βŠ• z ≑ x βŠ• (y βŠ• z)
  open Mon

  record MonHom {a b} {A : Type a} {B : Type b} (M : Mon A) (N : Mon B) : Type (β„“-max a b) where
    private
      module M = Mon M
      module N = Mon N
    field
      Ο• : A β†’ B
      preserves-e : Ο• M.e ≑ N.e
      preserves-βŠ• : βˆ€ x y β†’ Ο• (x M.βŠ• y) ≑ Ο• x N.βŠ• Ο• y
  open MonHom

  ListMon : βˆ€ {a} {A : Type a} β†’ Mon (List A)
  ListMon .e = []
  ListMon ._βŠ•_ = _++_
  ListMon .unitl xs = refl
  ListMon .unitr = ++-unit-r
  ListMon .assocr = ++-assoc

  Ξ· : βˆ€ {a} {A : Type a} β†’ A β†’ List A
  Ξ· a = [ a ]

  module _ {a m} {A : Type a} {M : Type m} (M* : Mon M) where
    private
      module M = Mon M*
      eval : (A β†’ M) β†’ List A β†’ M
      eval f [] = M.e
      eval f (x ∷ xs) = f x M.βŠ• eval f xs

    [_]_β™― = eval

    module _ (h* : MonHom ListMon M*) (f : A β†’ M) where
      private
        module h = MonHom h*
        eval-uniq : h.Ο• ∘ Ξ· ≑ f β†’ βˆ€ xs β†’ h.Ο• xs ≑ eval f xs
        eval-uniq p [] =
          h.preserves-e
        eval-uniq p (x ∷ xs) =
            h.preserves-βŠ• [ x ] xs
          βˆ™ ap (M._βŠ• h.Ο• xs) (funExt⁻ p x)
          βˆ™ ap (f x M.βŠ•_) (eval-uniq p xs)

      [_]_β™―-uniq = eval-uniq

  πŸ™+⟨_⟩-Mon : βˆ€ {a} (A : Type a) β†’ Mon (πŸ™ ⊎ A)
  πŸ™+⟨ A ⟩-Mon .e = inl ⋆
  πŸ™+⟨ A ⟩-Mon ._βŠ•_ (inl ⋆) y = y
  πŸ™+⟨ A ⟩-Mon ._βŠ•_ (inr x) y = inr x
  πŸ™+⟨ A ⟩-Mon .unitl x = refl
  πŸ™+⟨ A ⟩-Mon .unitr (inl ⋆) = refl
  πŸ™+⟨ A ⟩-Mon .unitr (inr x) = refl
  πŸ™+⟨ A ⟩-Mon .assocr (inl ⋆) y z = refl
  πŸ™+⟨ A ⟩-Mon .assocr (inr x) (inl ⋆) z = refl
  πŸ™+⟨ A ⟩-Mon .assocr (inr x) (inr y) z = refl

  head : βˆ€ {a} {A : Type a} β†’ List A β†’ πŸ™ ⊎ A
  head {A = A} = [ πŸ™+⟨ A ⟩-Mon ] inr β™―

  _ : head {A = β„•} [] ≑ inl ⋆
  _ = refl

  _ : head {A = β„•} [ 2 ∢ 1 ∢ 3 ] ≑ inr 2
  _ = refl











module CMonoid where

  open SLists

  pattern [_]         a           = a ∷ []
  pattern [_∢_]       a b         = a ∷ b ∷ []
  pattern [_∢_∢_]     a b c       = a ∷ b ∷ c ∷ []
  pattern [_∢_∢_∢_]   a b c d     = a ∷ b ∷ c ∷ d ∷ []
  pattern [_∢_∢_∢_∢_] a b c d e   = a ∷ b ∷ c ∷ d ∷ e ∷ []

  module _ {β„“} {A : Type β„“} where

    infixr 5 _++_

    _++_ : SList A β†’ SList A β†’ SList A
    _++_ = SListElim.rec (SList A β†’ SList A)
      (Ξ» ys β†’ ys)
      (Ξ» x h ys β†’ x ∷ h ys)
      (Ξ» x y h i β†’ Ξ» ys β†’ swap x y (h ys) i)
      (isSet→ trunc)






    ++-unit-r : (xs : SList A) β†’ xs ++ [] ≑ xs
    ++-unit-r = SListElim.indProp (Ξ» xs β†’ xs ++ [] ≑ xs)
      refl
      (Ξ» x {xs} h i β†’ x ∷ h i)
      (Ξ» xs β†’ trunc (xs ++ []) xs)

    ++-assoc : (xs ys zs : SList A) β†’ (xs ++ ys) ++ zs ≑ xs ++ ys ++ zs
    ++-assoc = SListElim.indProp (Ξ» xs β†’ (ys zs : SList A) β†’ (xs ++ ys) ++ zs ≑ xs ++ ys ++ zs)
      (Ξ» ys zs β†’ refl)
      (Ξ» x {xs} h ys zs i β†’ x ∷ h ys zs i)
      (Ξ» xs β†’ isPropΞ 2 Ξ» x y β†’ trunc ((xs ++ x) ++ y) (xs ++ x ++ y))

    ∷-comm : (x : A) (xs : SList A) β†’ x ∷ xs ≑ xs ++ [ x ]
    ∷-comm x = SListElim.indProp (Ξ» xs β†’ x ∷ xs ≑ xs ++ [ x ])
      refl
      (Ξ» y {xs} h β†’ swap x y xs βˆ™ ap (y ∷_) h)
      (Ξ» xs β†’ trunc (x ∷ xs) (xs ++ [ x ]))

    ++-comm : (xs ys : SList A) β†’ xs ++ ys ≑ ys ++ xs
    ++-comm = SListElim.indProp (Ξ» xs β†’ (ys : SList A) β†’ xs ++ ys ≑ ys ++ xs)
      (Ξ» ys β†’ sym (++-unit-r ys))
      (Ξ» x {xs} h ys i β†’
        hcomp (Ξ» j β†’ Ξ» { (i = i0) β†’ x ∷ h ys (~ j)
                       ; (i = i1) β†’ ++-assoc ys [ x ] xs j })
              (∷-comm x ys i ++ xs))
      (Ξ» xs β†’ isPropΞ  (Ξ» ys β†’ trunc (xs ++ ys) (ys ++ xs)))









  record CMon {a} (A : Type a) : Type a where
    infixr 10 _βŠ•_
    field
      e : A
      _βŠ•_ : A β†’ A β†’ A
      unitl : βˆ€ x β†’ e βŠ• x ≑ x
      assocr : βˆ€ x y z β†’ (x βŠ• y) βŠ• z ≑ x βŠ• (y βŠ• z)
      comm : βˆ€ x y β†’ x βŠ• y ≑ y βŠ• x
      hLevel : isSet A
  open CMon

  record CMonHom {a b} {A : Type a} {B : Type b} (M : CMon A) (N : CMon B) : Type (β„“-max a b) where
    private
      module M = CMon M
      module N = CMon N
    field
      Ο• : A β†’ B
      preserves-e : Ο• M.e ≑ N.e
      preserves-βŠ• : βˆ€ x y β†’ Ο• (x M.βŠ• y) ≑ Ο• x N.βŠ• Ο• y
  open CMonHom

  SListCMon : βˆ€ {a} {A : Type a} β†’ CMon (SList A)
  SListCMon .e = []
  SListCMon ._βŠ•_ = _++_
  SListCMon .unitl xs = refl
  SListCMon .assocr = ++-assoc
  SListCMon .comm = ++-comm
  SListCMon .hLevel = trunc



  Ξ· : βˆ€ {a} {A : Type a} β†’ A β†’ SList A
  Ξ· a = [ a ]



  hPropCMon : βˆ€ {β„“} β†’ CMon (hProp β„“)
  hPropCMon .e = (βŠ₯* , isPropβŠ₯*)
  hPropCMon ._βŠ•_ = L._βŠ”_
  hPropCMon .unitl x =
    L.β‡’βˆΆ PTrunc.rec (x .snd) (Ξ» { (inr x) β†’ x ; (inl ()) })
      β‡βˆΆ Ξ» x β†’ PTrunc.∣ (inr x) βˆ£β‚
  hPropCMon .assocr = Ξ» x y z β†’ (sym (L.βŠ”-assoc x y z))
  hPropCMon .comm = L.βŠ”-comm
  hPropCMon .hLevel = isSetHProp





  module _ {a m} {A : Type a} {M : Type m} (M* : CMon M) where
    private
      module M = CMon M*
      eval : (A β†’ M) β†’ SList A β†’ M
      eval f = SListElim.rec M
        M.e
        (Ξ» a h β†’ f a M.βŠ• h)
        (Ξ» x y h β†’ sym (M.assocr (f x) (f y) h) βˆ™βˆ™ ap (M._βŠ• h) (M.comm (f x) (f y)) βˆ™βˆ™ M.assocr (f y) (f x) h)
        M.hLevel

    [_]_β™― = eval

    eval-cons : βˆ€ x xs β†’ {f : A β†’ M} β†’ eval f (x ∷ xs) ≑ f x M.βŠ• eval f xs
    eval-cons x xs = refl

    module _ (h* : CMonHom SListCMon M*) (f : A β†’ M) where
      private
        module h = CMonHom h*
        eval-uniq : h.Ο• ∘ Ξ· ≑ f β†’ βˆ€ xs β†’ h.Ο• xs ≑ eval f xs
        eval-uniq p = SListElim.indProp (Ξ» xs β†’ h.Ο• xs ≑ eval f xs)
          h.preserves-e
          (Ξ» x {xs} H β†’ h.preserves-βŠ• [ x ] xs βˆ™ ap (M._βŠ• h.Ο• xs) (funExt⁻ p x) βˆ™ ap (f x M.βŠ•_) H)
          (Ξ» xs β†’ M.hLevel (h.Ο• xs) (eval f xs))

      [_]_β™―-uniq = eval-uniq




  module SymHead (T@(A , A*) : Toset β„“ β„“') where
    private
      _≀_ = TosetStr._≀_ A*
      isPropValued = TosetStr.is-prop-valued A*
      antisym = TosetStr.is-antisym A*
      trans = TosetStr.is-trans A*
      totality = TosetStr.is-total A*
      reflexivity = TosetStr.is-refl A*
      isSetA = TosetStr.is-set A*

    infixr 20 _βŠ“_
    βŠ“-min : (a b : A) β†’ (a ≀ b) ⊎ (b ≀ a) β†’ A
    βŠ“-min a b = ⊎.rec (Ξ» p β†’ a) (Ξ» q β†’ b)

    βŠ“-2Const : (a b : A) β†’ 2-Constant (βŠ“-min a b)
    βŠ“-2Const a b =
      ⊎.elim (Ξ» a≀b -> ⊎.elim (Ξ» _ -> refl) (Ξ» b≀a -> antisym a b a≀b b≀a))
             (Ξ» b≀a -> ⊎.elim (Ξ» a≀b -> antisym b a b≀a a≀b) (Ξ» _ -> refl))

    _βŠ“_ : A β†’ A β†’ A
    _βŠ“_ a b =
      PTrunc.rec→Set (IsToset.is-set (TosetStr.isToset A*))
      (βŠ“-min a b) (βŠ“-2Const a b) (totality a b)

    βŠ“-a≀b : (a b : A) β†’ (a ≀ b) β†’ (a βŠ“ b) ≑ a
    βŠ“-a≀b a b p = PTrunc.SetElim.helper
      isSetA
      (βŠ“-min a b)
      (βŠ“-2Const a b)
      (totality a b)
      PTrunc.∣ (inl p) βˆ£β‚

    βŠ“-b≀a : (a b : A) β†’ (b ≀ a) β†’ (a βŠ“ b) ≑ b
    βŠ“-b≀a a b q = PTrunc.SetElim.helper
      isSetA
      (βŠ“-min a b)
      (βŠ“-2Const a b)
      (totality a b)
      PTrunc.∣ inr q βˆ£β‚

    βŠ“-meet : (a b : A) β†’ (a βŠ“ b) ≀ a Γ— (a βŠ“ b) ≀ b
    βŠ“-meet a b =
      ( PTrunc.rec (isPropValued (a βŠ“ b) a)
      (⊎.rec (Ξ» p β†’ tpt (_≀ a) (sym (βŠ“-a≀b a b p)) (reflexivity a))
              Ξ» q β†’ tpt (_≀ a) (sym (βŠ“-b≀a a b q)) q)
             (totality a b)
      , PTrunc.rec (isPropValued (a βŠ“ b) b)
      (⊎.rec (Ξ» p β†’ tpt (_≀ b) (sym (βŠ“-a≀b a b p)) p)
              Ξ» q β†’ tpt (_≀ b) (sym (βŠ“-b≀a a b q)) (reflexivity b))
             (totality a b))

    βŠ“-univ₁ : (a b x : A) β†’ x ≀ (a βŠ“ b) β†’ (x ≀ a) Γ— (x ≀ b)
    βŠ“-univ₁ a b x p =
      ( trans x (a βŠ“ b) a p (βŠ“-meet a b .fst)
      , trans x (a βŠ“ b) b p (βŠ“-meet a b .snd))

    βŠ“-univβ‚‚ : (a b x : A) β†’ (x ≀ a) Γ— (x ≀ b) β†’ x ≀ (a βŠ“ b)
    βŠ“-univβ‚‚ a b x (p , q) =
      PTrunc.rec (isPropValued x (a βŠ“ b))
      (⊎.rec (Ξ» r β†’ tpt (x ≀_) (sym (βŠ“-a≀b a b r)) p)
             (Ξ» s β†’ tpt (x ≀_) (sym (βŠ“-b≀a a b s)) q))
      (totality a b)

    βŠ“-univ : (a b x : A) β†’ (x ≀ (a βŠ“ b)) ≃ ((x ≀ a) Γ— (x ≀ b))
    βŠ“-univ a b x =
      propBiimplβ†’Equiv (isPropValued x (a βŠ“ b))
      (isPropΓ— (isPropValued x a) (isPropValued x b))
      (βŠ“-univ₁ a b x) (βŠ“-univβ‚‚ a b x)

    γ‚ˆβ‰‘ : (a b : A) β†’ ((x : A) β†’ x ≀ a ≃ x ≀ b) β†’ a ≑ b
    γ‚ˆβ‰‘ a b f = antisym a b (f a .fst (reflexivity a)) (invEq (f b) (reflexivity b))

    βŠ“-assoc : (a b c : A) β†’ (a βŠ“ b) βŠ“ c ≑ a βŠ“ (b βŠ“ c)
    βŠ“-assoc a b c =
      γ‚ˆβ‰‘ ((a βŠ“ b) βŠ“ c) (a βŠ“ b βŠ“ c)
        Ξ» x β†’ compEquiv (βŠ“-univ (a βŠ“ b) c x)
          (compEquiv (Ξ£-cong-equiv (βŠ“-univ a b x) (Ξ» _ β†’ idEquiv (x ≀ c)))
            (compEquiv Ξ£-assoc-≃ (compEquiv (Ξ£-cong-equiv (idEquiv (x ≀ a))
              (Ξ» _ β†’ invEquiv (βŠ“-univ b c x))) (invEquiv (βŠ“-univ a (b βŠ“ c) x)))))

    βŠ“-comm : (a b : A) β†’ a βŠ“ b ≑ b βŠ“ a
    βŠ“-comm a b = γ‚ˆβ‰‘ (a βŠ“ b) (b βŠ“ a)
      Ξ» x β†’ compEquiv (βŠ“-univ a b x) (compEquiv Ξ£-swap-≃ (invEquiv (βŠ“-univ b a x)))





    infixr 20 _βŠ—_
    _βŠ—_ : πŸ™ ⊎ A β†’ πŸ™ ⊎ A β†’ πŸ™ ⊎ A
    inl ⋆ βŠ— b = b
    inr x βŠ— inl ⋆ = inr x
    inr x βŠ— inr y = inr (x βŠ“ y)

    βŠ—-unitl : (x : πŸ™ ⊎ A) β†’ x ≑ x
    βŠ—-unitl (inl ⋆) = refl
    βŠ—-unitl (inr x) = refl

    βŠ—-assoc : (a b c : πŸ™ ⊎ A) β†’ (a βŠ— b) βŠ— c ≑ a βŠ— (b βŠ— c)
    βŠ—-assoc (inl ⋆) b c = refl
    βŠ—-assoc (inr a) (inl ⋆) c = refl
    βŠ—-assoc (inr a) (inr b) (inl ⋆) = refl
    βŠ—-assoc (inr a) (inr b) (inr c) = ap inr (βŠ“-assoc a b c)

    βŠ—-comm : (a b : πŸ™ ⊎ A) β†’ a βŠ— b ≑ b βŠ— a
    βŠ—-comm (inl ⋆) (inl ⋆) = refl
    βŠ—-comm (inl ⋆) (inr b) = refl
    βŠ—-comm (inr a) (inl ⋆) = refl
    βŠ—-comm (inr a) (inr b) = ap inr (βŠ“-comm a b)






    MaybeCMon : CMon (πŸ™ ⊎ A)
    MaybeCMon .e = inl ⋆
    MaybeCMon ._βŠ•_ = _βŠ—_
    MaybeCMon .unitl = Ξ» _ β†’ refl
    MaybeCMon .assocr = βŠ—-assoc
    MaybeCMon .comm = βŠ—-comm
    MaybeCMon .hLevel = isSet⊎ isSetUnit (IsToset.is-set (TosetStr.isToset A*))





    head : SList A β†’ πŸ™ ⊎ A
    head = [ MaybeCMon ] inr β™―

  β„•* : IsToset {β„“ = β„“-zero} {β„“' = β„“-zero} {A = β„•} Nat._≀_
  β„•* .IsToset.is-set = isSetβ„•
  β„•* .IsToset.is-prop-valued a b = Nat.isProp≀
  β„•* .IsToset.is-refl a = Nat.≀-refl
  β„•* .IsToset.is-trans a b c = Nat.≀-trans
  β„•* .IsToset.is-antisym a b = Nat.≀-antisym
  β„•* .IsToset.is-total a b with (Nat._β‰Ÿ_ a b)
  ... | Nat.lt x = PTrunc.∣ (inl (Nat.<-weaken x)) βˆ£β‚
  ... | Nat.eq x = PTrunc.∣ (inl (tpt (Ξ» y β†’ (y Nat.≀ b)) (sym x) Nat.≀-refl)) βˆ£β‚
  ... | Nat.gt x = PTrunc.∣ (inr (Nat.<-weaken x)) βˆ£β‚


  open SymHead (β„• , (tosetstr Nat._≀_ β„•*))

  _ : head [] ≑ inl ⋆
  _ = refl

  _ : head [ 4 ∢ 6 ∢ 9 ∢ 6 ∢ 7 ] ≑ inr 4
  _ = refl