Martin Escardo, Paulo Oliva, originally 2023, modified in 2024 for
relative monads on structured types.

\begin{code}

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

open import MLTT.Spartan hiding (J)

open import RelativeMonadOnStructuredTypes.OneSigmaStructure

module RelativeMonadOnStructuredTypes.J-transf
        {{ρ : πŸ™-Ξ£-structure}}
       where

open πŸ™-Ξ£-structure ρ

open import UF.FunExt
open import RelativeMonadOnStructuredTypes.Definition

𝕁-transf : Fun-Ext
         β†’ {β„“ : Universe β†’ Universe}
         β†’ Relative-Monad {β„“}
         β†’ π•Š 𝓦₀
         β†’ Relative-Monad {Ξ» 𝓀 β†’ β„“ 𝓦₀ βŠ” β„“ 𝓀 βŠ” 𝓀}
𝕁-transf {𝓦₀} fe {β„“} 𝕋 𝓑 =
 record
  { functor = JT
  ; Ξ· = Ξ·α΄Άα΅€
  ; ext = extα΄Άα΅€
  ; ext-Ξ· = extα΄Άα΅€-Ξ·
  ; unit = unitα΄Άα΅€
  ; assoc = assocα΄Άα΅€
  }
 where
  T : {𝓀 : Universe} β†’ π•Š 𝓀 β†’ β„“ 𝓀 Μ‡
  T = functor 𝕋

  JT : {𝓀 : Universe} β†’ π•Š 𝓀 β†’ β„“ 𝓦₀ βŠ” β„“ 𝓀 βŠ” 𝓀 Μ‡
  JT 𝓧 = (⟨ 𝓧 ⟩ β†’ T 𝓑) β†’ T 𝓧

  Ξ·α΄Άα΅€ : {𝓧 : π•Š 𝓀} β†’ ⟨ 𝓧 ⟩ β†’ JT 𝓧
  Ξ·α΄Άα΅€ x p = Ξ· 𝕋 x

  extα΄Άα΅€ : {𝓧 : π•Š 𝓀} {𝓨 : π•Š π“₯} β†’ (⟨ 𝓧 ⟩ β†’ JT 𝓨) β†’ JT 𝓧 β†’ JT 𝓨
  extα΄Άα΅€ f Ξ΅ p = ext 𝕋 (Ξ» x β†’ f x p) (Ξ΅ (Ξ» x β†’ ext 𝕋 p (f x p)))

  extα΄Άα΅€-Ξ· : {𝓧 : π•Š 𝓀} β†’ extα΄Άα΅€ (Ξ·α΄Άα΅€ {𝓀} {𝓧}) ∼ 𝑖𝑑 (JT 𝓧)
  extα΄Άα΅€-Ξ· Ξ΅ = dfunext fe (Ξ» p β†’
   ext 𝕋 (Ξ· 𝕋) (Ξ΅ (Ξ» x β†’ ext 𝕋 p (Ξ· 𝕋 x))) ＝⟨ ext-Ξ· 𝕋 _ ⟩
   Ξ΅ (Ξ» x β†’ ext 𝕋 p (Ξ· 𝕋 x))                ＝⟨ ap Ξ΅ (dfunext fe (unit 𝕋 _)) ⟩
   Ρ p                                       ∎)

  unitα΄Άα΅€ : {𝓧 : π•Š 𝓀} {𝓨 : π•Š π“₯} (f : ⟨ 𝓧 ⟩ β†’ JT 𝓨) (x : ⟨ 𝓧 ⟩)
         β†’ extα΄Άα΅€ {𝓀} {π“₯} {𝓧} {𝓨} f (Ξ·α΄Άα΅€ x) ＝ f x
  unitα΄Άα΅€ f x = dfunext fe (Ξ» p β†’ unit 𝕋 (Ξ» x β†’ f x p) x)

  assocα΄Άα΅€ : {𝓧 : π•Š 𝓀} {𝓨 : π•Š π“₯} {𝓩 : π•Š 𝓦} (g : ⟨ 𝓨 ⟩
          β†’ JT 𝓩) (f : ⟨ 𝓧 ⟩ β†’ JT 𝓨) (Ξ΅ : JT 𝓧)
          β†’ extα΄Άα΅€ (Ξ» x β†’ extα΄Άα΅€ g (f x)) Ξ΅ ＝ extα΄Άα΅€ g (extα΄Άα΅€ f Ξ΅)
  assocα΄Άα΅€ g f Ξ΅ = dfunext fe Ξ³
   where
    Ξ³ : βˆ€ p β†’ extα΄Άα΅€ (Ξ» x β†’ extα΄Άα΅€ g (f x)) Ξ΅ p ＝ extα΄Άα΅€ g (extα΄Άα΅€ f Ξ΅) p
    Ξ³ p =
     extα΄Άα΅€ (Ξ» x β†’ extα΄Άα΅€ g (f x)) Ξ΅ p                ＝⟨refl⟩
     𝕖 (Ξ» x β†’ 𝕖 π•˜ (𝕗 x)) (Ξ΅ (Ξ» x β†’ 𝕖 p (𝕖 π•˜ (𝕗 x)))) ＝⟨ assoc 𝕋 _ _ _ ⟩
     𝕖 π•˜ (𝕖 𝕗 (Ξ΅ (Ξ» x β†’ 𝕖 p (𝕖 π•˜ (𝕗 x)))))           ＝⟨ again-by-assoc ⟩
     𝕖 π•˜ (𝕖 𝕗 (Ξ΅ (Ξ» x β†’ 𝕖 (Ξ» y β†’ 𝕖 p (π•˜ y)) (𝕗 x)))) ＝⟨refl⟩
     extα΄Άα΅€ g (extα΄Άα΅€ f Ξ΅) p ∎
      where
       𝕖 = ext 𝕋
       π•˜ = Ξ» y β†’ g y p
       𝕗 = Ξ» x β†’ f x (Ξ» y β†’ 𝕖 p (π•˜ y))
       again-by-assoc = ap (Ξ» - β†’ 𝕖 π•˜ (𝕖 𝕗 (Ξ΅ -)))
                           (dfunext fe (Ξ» x β†’ (assoc 𝕋 _ _ _)⁻¹))

module relative-JT-definitions
        {β„“ : Universe β†’ Universe}
        (𝕋 : Relative-Monad {β„“})
        (𝓑 : π•Š 𝓦₀)
        (𝓐 : Relative-Algebra 𝕋 ⟨ 𝓑 ⟩)
        (fe : Fun-Ext)
       where

 open import MonadOnTypes.K

 open relative-T-definitions 𝕋
 open relative-Ξ±-definitions 𝕋 𝓑 𝓐
 open K-definitions ⟨ 𝓑 ⟩

 𝕁𝕋 : Relative-Monad
 𝕁𝕋 = 𝕁-transf fe 𝕋 𝓑

 JT : π•Š 𝓀 β†’ β„“ 𝓦₀ βŠ” β„“ 𝓀 βŠ” 𝓀 Μ‡
 JT = functor 𝕁𝕋

 KT : π•Š 𝓀 β†’ 𝓦₀ βŠ” β„“ 𝓦₀ βŠ” 𝓀 Μ‡
 KT 𝓧 = (⟨ 𝓧 ⟩ β†’ T 𝓑) β†’ ⟨ 𝓑 ⟩

 Ξ·α΄Άα΅€ : {𝓧 : π•Š 𝓀} β†’ ⟨ 𝓧 ⟩ β†’ JT 𝓧
 Ξ·α΄Άα΅€ = Ξ· 𝕁𝕋

 extα΄Άα΅€ : {𝓧 : π•Š 𝓀} {𝓨 : π•Š π“₯} β†’ (⟨ 𝓧 ⟩ β†’ JT 𝓨) β†’ JT 𝓧 β†’ JT 𝓨
 extα΄Άα΅€ = ext 𝕁𝕋

 mapα΄Άα΅€ : {𝓧 : π•Š 𝓀} {𝓨 : π•Š π“₯} β†’ (⟨ 𝓧 ⟩ β†’ ⟨ 𝓨 ⟩) β†’ JT 𝓧 β†’ JT 𝓨
 mapα΄Άα΅€ = map 𝕁𝕋

 _βŠ—α΄Άα΅€_ : {𝓧 : π•Š 𝓀} {𝓨 : ⟨ 𝓧 ⟩ β†’ π•Š π“₯}
       β†’ JT 𝓧
       β†’ ((x : ⟨ 𝓧 ⟩) β†’ JT (𝓨 x))
       β†’ JT (Ξ£β‚› x κž‰ 𝓧 , 𝓨 x)
 _βŠ—α΄Άα΅€_ = _βŠ—α΅£_ 𝕁𝕋

 overlineᴬ : {𝓧 : π•Š 𝓀} β†’ JT 𝓧 β†’ KT 𝓧
 overlineᴬ Ξ΅ = Ξ» p β†’ Ξ± (extα΅€ p (Ξ΅ p))

 -overlineᴬ : {𝓧 : π•Š 𝓀} β†’ JT 𝓧 β†’ K ⟨ 𝓧 ⟩
 -overlineᴬ Ξ΅ = Ξ» p β†’ Ξ± (extα΅€ (Ξ·α΅€ ∘ p) (Ξ΅ (Ξ·α΅€ ∘ p)))

 _attainsᴬ_ : {𝓧 : π•Š 𝓀} β†’ JT 𝓧 β†’ K ⟨ 𝓧 ⟩ β†’ 𝓦₀ βŠ” β„“ 𝓦₀ βŠ” 𝓀 Μ‡
 _attainsᴬ_ {𝓀} {𝓧} Ξ΅ Ο• = (p : ⟨ 𝓧 ⟩ β†’ T 𝓑) β†’ overlineᴬ Ξ΅ p ＝ Ο• (Ξ± ∘ p)

\end{code}