Martin Escardo 31 Jan 2019

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan

module Slice.Algebras
        (𝓣 : Universe)
       where

open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Univalence
open import UF.UA-FunExt

open import Slice.Construction 𝓣
open import Slice.Monad 𝓣

double-𝓕-charac : (X : 𝓀 Μ‡ )
                β†’ 𝓕 (𝓕 X) ≃ (Ξ£ I κž‰ 𝓣 Μ‡ , (Ξ£ J κž‰ (I β†’ 𝓣 Μ‡ ), ((i : I) β†’ J i β†’ X)))
double-𝓕-charac X = Ξ£-cong (Ξ³ X)
 where
  Ξ³ : (X : 𝓀 Μ‡ ) (I : 𝓣 Μ‡ ) β†’ (I β†’ 𝓕 X) ≃ (Ξ£ J κž‰ (I β†’ 𝓣 Μ‡ ), ((i : I) β†’ J i β†’ X))
  Ξ³ X I = (I β†’ Ξ£ J κž‰ 𝓣 Μ‡ , (J β†’ X))               β‰ƒβŸ¨ Ξ Ξ£-distr-≃ ⟩
          (Ξ£ J κž‰ (I β†’ 𝓣 Μ‡ ), ((i : I) β†’ J i β†’ X)) β– 

𝓕-algebra : 𝓀 Μ‡ β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
𝓕-algebra X = Ξ£ s κž‰ (𝓕 X β†’ X), (s ∘ Ξ· ∼ id) Γ— (s ∘ ΞΌ ∼ s ∘ 𝓕̇ s)

free-𝓕-algebra : is-univalent 𝓣 β†’ (X : 𝓀 Μ‡ ) β†’ 𝓕-algebra (𝓕 X)
free-𝓕-algebra ua X = ΞΌ , 𝓕-unit-left∼ ua , 𝓕-assoc∼ ua

joinop : 𝓀 Μ‡ β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
joinop X = {I : 𝓣 Μ‡ } β†’ (I β†’ X) β†’ X

𝓕-alg-Lawβ‚€ : {X : 𝓀 Μ‡ } β†’ joinop X β†’ 𝓀 Μ‡
𝓕-alg-Lawβ‚€ {𝓀} {X} ∐ = (x : X) β†’ ∐ (Ξ» (i : πŸ™) β†’ x) ＝ x

𝓕-alg-Law₁ : {X : 𝓀 Μ‡ } β†’ joinop X β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
𝓕-alg-Law₁ {𝓀} {X} ∐ = (I : 𝓣 Μ‡ ) (J : I β†’ 𝓣 Μ‡ ) (f : Ξ£ J β†’ X)
                     β†’ ∐ f ＝ ∐ (Ξ» i β†’ ∐ (Ξ» j β†’ f (i , j)))

𝓕-alg : 𝓀 Μ‡ β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
𝓕-alg X = Ξ£ ∐ κž‰ joinop X , 𝓕-alg-Lawβ‚€ ∐ Γ— 𝓕-alg-Law₁ ∐

⋁ : {X : 𝓀 Μ‡ } β†’ (𝓕 X β†’ X) β†’ joinop X
⋁ s {I} f = s (I , f)

βˆΜ‡ : {X : 𝓀 Μ‡ } β†’ 𝓕-algebra X β†’ joinop X
βˆΜ‡ (s , _) = ⋁ s

∐ : {X : 𝓀 Μ‡ } β†’ 𝓕-alg X β†’ joinop X
∐ (∐ , κ , ι) = ∐

lawβ‚€ : {X : 𝓀 Μ‡ } (a : 𝓕-alg X) β†’ 𝓕-alg-Lawβ‚€ (∐ a)
lawβ‚€ (∐ , ΞΊ , ΞΉ) = ΞΊ

law₁ : {X : 𝓀 Μ‡ } (a : 𝓕-alg X) β†’ 𝓕-alg-Law₁ (∐ a)
law₁ (∐ , ΞΊ , ΞΉ) = ΞΉ

𝓕-morphism-charac : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                    (s : 𝓕 X β†’ X) (t : 𝓕 Y β†’ Y)
                    (h : X β†’ Y)

                  β†’ (h ∘ s ∼ t ∘ 𝓕̇ h)
                  ≃ ({I : 𝓣 Μ‡ } (f : I β†’ X) β†’ h (⋁ s f) ＝ ⋁ t (h ∘ f))
𝓕-morphism-charac s t h = qinveq (Ξ» H {I} f β†’ H (I , f))
                                 ((Ξ» {Ο€ (I , f) β†’ Ο€ {I} f}) ,
                                  (Ξ» _ β†’ refl) ,
                                  (Ξ» _ β†’ refl))


𝓕-algebra-gives-alg : {X : 𝓀 Μ‡ } β†’ 𝓕-algebra X β†’ 𝓕-alg X
𝓕-algebra-gives-alg (s , unit , assoc) =
                    ⋁ s ,
                    unit ,
                    (Ξ» I J f β†’ assoc (I , (Ξ» i β†’ J i , (Ξ» j β†’ f (i , j)))))

𝓕-alg-gives-algebra : {X : 𝓀 Μ‡ } β†’ 𝓕-alg X β†’ 𝓕-algebra X
𝓕-alg-gives-algebra {𝓀} {X} (∐ , unit , ΞΉ) = s , unit , assoc
 where
  s : 𝓕 X β†’ X
  s (I , f) = ∐ f
  assoc : s ∘ ΞΌ ∼ s ∘ 𝓕̇ s
  assoc (I , g) = ΞΉ I (pr₁ ∘ g) Ξ» { (i , j) β†’ prβ‚‚ (g i) j}

𝓕-alg-charac : {X : 𝓀 Μ‡ } β†’ 𝓕-algebra X ≃ 𝓕-alg X
𝓕-alg-charac = qinveq 𝓕-algebra-gives-alg (𝓕-alg-gives-algebra , ((Ξ» _ β†’ refl) , (Ξ» _ β†’ refl)))

Ξ -is-alg : funext 𝓀 π“₯
         β†’ {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
         β†’ ((x : X) β†’ 𝓕-alg (A x))
         β†’ 𝓕-alg (Ξ  A)
Ξ -is-alg {𝓀} {π“₯} fe {X} A Ξ± = ∐· , lβ‚€ , l₁
 where
  ∐· : {I : 𝓣 Μ‡ } β†’ (I β†’ Ξ  A) β†’ Ξ  A
  ∐· f x = ∐ (Ξ± x) (Ξ» i β†’ f i x)
  lβ‚€ : (Ο† : Ξ  A) β†’ ∐· (Ξ» i β†’ Ο†) ＝ Ο†
  lβ‚€ Ο† = dfunext fe (Ξ» x β†’ lawβ‚€ (Ξ± x) (Ο† x))
  l₁ : (I : 𝓣 Μ‡ ) (J : I β†’ 𝓣 Μ‡ ) (f : Ξ£ J β†’ Ξ  A)
    β†’ ∐· f ＝ ∐· (Ξ» i β†’ ∐· (Ξ» j β†’ f (i , j)))
  l₁ I J f = dfunext fe (Ξ» x β†’ law₁ (Ξ± x) I J (Ξ» Οƒ β†’ f Οƒ x))

universe-is-algebra-Ξ£ : is-univalent 𝓣 β†’ 𝓕-alg (𝓣 Μ‡ )
universe-is-algebra-Ξ£ ua = sum , k , ΞΉ
 where
  sum : {I : 𝓣 Μ‡ } β†’ (I β†’ 𝓣 Μ‡ ) β†’ 𝓣 Μ‡
  sum = Ξ£
  k : (X : 𝓣 Μ‡ ) β†’ Ξ£ (Ξ» i β†’ X) ＝ X
  k X = eqtoid ua (πŸ™ Γ— X) X πŸ™-lneutral
  ΞΉ : (I : 𝓣 Μ‡ ) (J : I β†’ 𝓣 Μ‡ ) (f : Ξ£ J β†’ 𝓣 Μ‡ )
    β†’ Ξ£ f ＝ Ξ£ (Ξ» i β†’ Ξ£ (Ξ» j β†’ f (i , j)))
  ΞΉ I J f = eqtoid ua _ _ Ξ£-assoc

universe-is-algebra-Ξ  : is-univalent 𝓣 β†’ 𝓕-alg (𝓣 Μ‡ )
universe-is-algebra-Ξ  ua = prod , k , ΞΉ
 where
  fe : funext 𝓣 𝓣
  fe = univalence-gives-funext ua
  prod : {I : 𝓣 Μ‡ } β†’ (I β†’ 𝓣 Μ‡ ) β†’ 𝓣 Μ‡
  prod = Ξ 
  k : (X : 𝓣 Μ‡ ) β†’ Ξ  (Ξ» i β†’ X) ＝ X
  k X = eqtoid ua (πŸ™ β†’ X) X (≃-sym (πŸ™β†’ (univalence-gives-funext ua)))
  ΞΉ : (I : 𝓣 Μ‡ ) (J : I β†’ 𝓣 Μ‡ ) (f : Ξ£ J β†’ 𝓣 Μ‡ )
    β†’ Ξ  f ＝ Ξ  (Ξ» i β†’ Ξ  (Ξ» j β†’ f (i , j)))
  ΞΉ I J f = eqtoid ua _ _ (curry-uncurry' fe fe)

\end{code}