Martin Escardo, January 2018, May 2020
Jonathan Sterling, June 2023

\begin{code}

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

open import Dominance.Definition
open import MLTT.Spartan
open import UF.Base
open import UF.SIP
open import UF.Univalence
open import UF.FunExt
open import UF.Equiv-FunExt
open import UF.Equiv hiding (_β_; β-refl)
open import UF.EquivalenceExamples
open import UF.UA-FunExt
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import W.Type

import UF.PairFun as PairFun

module
Dominance.Lifting
{π£ π : Universe}
(π£-ua : is-univalent π£)
(d : π£ Μ β π Μ)
(isd : is-dominance d)
where

D : Dominance
D = (d , isd)

module _ {π₯} where
L : (X : π₯ Μ) β π£ βΊ β π β π₯ Μ
L X = Ξ£ P κ π£ Μ , (P β X) Γ d P

is-defined : {X : π₯ Μ} β L X β π£ Μ
is-defined (P , (Ο , dP)) = P

_β = is-defined

β-is-dominant : {X : π₯ Μ} β (xΜ : L X) β is-dominant D (xΜ β)
β-is-dominant (P , (Ο , dP)) = dP

value : {X : π₯ Μ} β (xΜ : L X) β xΜ β β X
value (P , (Ο , dP)) = Ο

module _ {π₯ : _} {X : π₯ Μ} where
open sip

fam-str : (P : π£ Μ) β π£ β π₯ Μ
fam-str P = P β X

fam-sns-data : SNS fam-str (π£ β π₯)
fam-sns-data = ΞΉ , Ο , ΞΈ
where
ΞΉ : (u v : Ξ£ fam-str) β β¨ u β© β β¨ v β© β π£ β π₯ Μ
ΞΉ (P , u) (Q , v) (f , _) = u οΌ v β f

Ο : (u : Ξ£ fam-str) β ΞΉ u u (β-refl β¨ u β©)
Ο _ = refl

h : {P : π£ Μ} {u v : fam-str P} β canonical-map ΞΉ Ο u v βΌ -id (u οΌ v)
h refl = refl

ΞΈ : {P : π£ Μ} (u v : fam-str P) β is-equiv (canonical-map ΞΉ Ο u v)
ΞΈ u v = equiv-closed-under-βΌ _ _ (id-is-equiv (u οΌ v)) h

fam-β : (u v : Ξ£ fam-str) β π£ β π₯ Μ
fam-β (P , u) (Q , v) =
Ξ£ f κ (P β Q) , is-equiv f Γ (u οΌ v β f)

characterization-of-fam-οΌ : (u v : Ξ£ fam-str) β (u οΌ v) β fam-β u v
characterization-of-fam-οΌ = characterization-of-οΌ π£-ua fam-sns-data

_β_ : L X β L X β π£ β π₯ Μ
(P , u , dP) β (Q , v , dQ) =
Ξ£ f κ P β Q , u βΌ v β prβ f

β-refl : (u : L X) β u β u
β-refl u = (id , id) , Ξ» _ β refl

module _ (π£π₯-fe : funext π£ π₯) where
οΌ-to-β : (u v : L X) β (u οΌ v) β (u β v)
οΌ-to-β u v =
(u οΌ v)
fam-β (u β , value u) (v β , value v)
(Ξ£ f κ (u β β v β) , (v β β u β) Γ value u βΌ value v β f)
u β v β

where
open sip-with-axioms

uβ-is-prop = dominant-types-are-props D (u β) (β-is-dominant u)
vβ-is-prop = dominant-types-are-props D (v β) (β-is-dominant v)
π£-fe = univalence-gives-funext π£-ua

step1 =
characterization-of-οΌ-with-axioms π£-ua
fam-sns-data
(Ξ» P u β d P)
(Ξ» P _ β being-dominant-is-prop D P)

step2 =
PairFun.pair-fun-equiv
(β-refl (u β β v β))
(Ξ» f β
PairFun.pair-fun-equiv
(logically-equivalent-props-are-equivalent
(being-equiv-is-prop' π£-fe π£-fe π£-fe π£-fe f)
(Ξ -is-prop π£-fe (Ξ» _ β uβ-is-prop))
(inverse f)
(logically-equivalent-props-give-is-equiv
uβ-is-prop
vβ-is-prop
f))
(Ξ» _ β β-funext π£π₯-fe (value u) (value v β f)))

οΌ-to-β-refl : (u : L X) β eqtofun (οΌ-to-β u u) refl οΌ β-refl u
οΌ-to-β-refl _ = refl

L-ext : {u v : L X} β u β v β u οΌ v
L-ext = back-eqtofun (οΌ-to-β _ _)

Ξ· : {π₯ : _} {X : π₯ Μ} β X β L X
Ξ· x = π , (Ξ» _ β x) , π-is-dominant D

_β_ : {π₯ π¦ : _} β π₯ Μ β π¦ Μ β π£ βΊ β π β π₯ β π¦ Μ
X β Y = X β L Y

module _ {π₯ π¦ : _} {X : π₯ Μ} {Y : π¦ Μ} where
extension : (X β Y) β (L X β L Y)
extension f (P , (Ο , dP)) = (Q , (Ξ³ , dQ))
where
Q : π£ Μ
Q = Ξ£ p κ P , f (Ο p) β

dQ : is-dominant D Q
dQ = dominant-closed-under-Ξ£ D P (_β β f β Ο) dP (β-is-dominant β f β Ο)

Ξ³ : Q β Y
Ξ³ (p , def) = value (f (Ο p)) def

_β― : (X β Y) β (L X β L Y)
f β― = extension f

_<<<_
: {π₯ π¦ π£ : _} {X : π₯ Μ} {Y : π¦ Μ} {Z : π£ Μ}
β (Y β Z) β (X β Y) β (X β Z)
g <<< f = g β― β f

ΞΌ : {π₯ : _} {X : π₯ Μ} β L (L X) β L X
ΞΌ = extension id

module _ {π₯} {X : π₯ Μ} (π£π₯-fe : funext π£ π₯) where
kleisli-lawβ : extension (Ξ· {π₯} {X}) βΌ id
kleisli-lawβ u =
L-ext π£π₯-fe (Ξ± , Ξ» _ β refl)
where
Ξ± : u β Γ π β u β
Ξ± = prβ , (_, β)

module _ {π₯ π¦} {X : π₯ Μ} {Y : π¦ Μ} (π£π¦-fe : funext π£ π¦) where
kleisli-lawβ : (f : X β Y) β extension f β Ξ· βΌ f
kleisli-lawβ f u =
L-ext π£π¦-fe (Ξ± , Ξ» _ β refl)
where
Ξ± : π Γ f u β β f u β
Ξ± = prβ , (β ,_)

module _ {π₯ π¦ π§} {X : π₯ Μ} {Y : π¦ Μ} {Z : π§ Μ} (π£π§-fe : funext π£ π§) where
kleisli-lawβ : (f : X β Y) (g : Y β Z) β (g β― β f)β― βΌ g β― β f β―
kleisli-lawβ f g x =
L-ext π£π§-fe (Ξ± , Ξ» _ β refl)
where
Ξ± : (((g β―) β f) β―) x β β ((g β―) β (f β―)) x β
prβ Ξ± (p , q , r) = (p , q) , r
prβ Ξ± ((p , q) , r) = p , q , r

\end{code}

TODO: state and prove the naturality of all the monad components, define both
algebras for the endofunctor and for the monad, recall the results of Joyal and
Moerdijk on monads and algebras with successor, etc.

We can define carrier of the initial lift algebra using a W-type.

\begin{code}

module Initial-Lift-Algebra where
Ο : π£ βΊ β π Μ
Ο = W (dominant-prop D) prβ

\end{code}