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)
     β‰ƒβŸ¨ 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.

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}