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

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)
    β‰ƒβŸ¨ step1 u v ⟩
   fam-β‰… (u ↓ , value u) (v ↓ , value v)
    β‰ƒβŸ¨ step2 ⟩
   (Ξ£ f κž‰ (u ↓ β†’ v ↓) , (v ↓ β†’ u ↓) Γ— value u ∼ value v ∘ f)
    β‰ƒβŸ¨ ≃-sym Ξ£-assoc ⟩
   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)
         (logical-equivs-of-props-are-equivs
          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.