Martin Escardo, 6th December 2018

\begin{code}

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

open import MLTT.Spartan

module Slice.Monad (𝓣 : Universe) where

open import UF.Base
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
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.IdentityViaSIP 𝓣

\end{code}

Constructions:

\begin{code}

𝓕̇ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓕 X β†’ 𝓕 Y
𝓕̇ f (P , Ο†) = P , f ∘ Ο†

_β™― : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ 𝓕 Y) β†’ (𝓕 X β†’ 𝓕 Y)
_β™― f (P , Ο† ) = (Ξ£ p κž‰ P , source (f (Ο† p))) ,
                (Ξ» Οƒ β†’ family (f (Ο† (pr₁ Οƒ))) (prβ‚‚ Οƒ))


ΞΌ : {X : 𝓀 Μ‡ } β†’ 𝓕 (𝓕 X) β†’ 𝓕 X
ΞΌ = id β™―

𝓕̇-id : {X : 𝓀 Μ‡ }
      β†’ 𝓕̇ id ＝ id
𝓕̇-id {𝓀} {X} = refl {𝓀 βŠ” (𝓣 ⁺)} {𝓕 X β†’ 𝓕 X}

𝓕̇-∘ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } (f : X β†’ Y) (g : Y β†’ Z)
     β†’ 𝓕̇ (g ∘ f) ＝ 𝓕̇ g ∘ 𝓕̇ f
𝓕̇-∘ f g = refl

Ξ·-natural : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
          β†’ Ξ· ∘ f ＝ 𝓕̇ f ∘ Ξ·
Ξ·-natural f = refl

Ξ·-natural∼ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
           β†’ Ξ· ∘ f ∼ 𝓕̇ f ∘ Ξ·
η-natural∼ f _ = refl

ΞΌ-natural∼ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
           β†’ 𝓕̇ f ∘ ΞΌ ∼ ΞΌ ∘ 𝓕̇ (𝓕̇ f)
μ-natural∼ f _ = refl

ΞΌ-natural : funext (𝓣 ⁺ βŠ” 𝓀) (𝓣 ⁺ βŠ” π“₯)
          β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
          β†’ 𝓕̇ f ∘ ΞΌ ＝ ΞΌ ∘ 𝓕̇ (𝓕̇ f)
μ-natural fe f = dfunext fe (μ-natural∼ f)


𝓕-unit-right⋍ : {X : 𝓀 Μ‡ } (l : 𝓕 X)
              β†’ ΞΌ (𝓕̇ Ξ· l) ⋍ l
𝓕-unit-right⋍ {𝓀} {X} (P , Ο†) = e , refl
 where
  e : P Γ— πŸ™ ≃ P
  e = πŸ™-rneutral

𝓕-unit-left⋍ : {X : 𝓀 Μ‡ } (l : 𝓕 X)
             β†’ ΞΌ (Ξ· l) ⋍ l
𝓕-unit-left⋍ (P , Ο†) = e , refl
 where
  e : πŸ™ Γ— P ≃ P
  e = πŸ™-lneutral

𝓕-unit-right∼ : is-univalent 𝓣 β†’ {X : 𝓀 Μ‡ }
              β†’ ΞΌ ∘ 𝓕̇ Ξ· ∼ id
𝓕-unit-right∼ {𝓀} ua {X} l = ⋍-gives-＝ ua (𝓕-unit-right⋍ {𝓀} {X} l)

𝓕-unit-left∼ : is-univalent 𝓣 β†’ {X : 𝓀 Μ‡ }
              β†’ ΞΌ ∘ Ξ· ∼ id
𝓕-unit-left∼ {𝓀} ua {X} l = ⋍-gives-＝ ua (𝓕-unit-left⋍ {𝓀} {X} l)

𝓕-assoc⋍ : {X : 𝓀 Μ‡ } (l : 𝓕 (𝓕 (𝓕 X))) β†’ ΞΌ (ΞΌ l) ⋍ ΞΌ (𝓕̇ ΞΌ l)
𝓕-assoc⋍ (P , Ο†) = Ξ£-assoc , refl

𝓕-assoc∼ : is-univalent 𝓣 β†’ {X : 𝓀 Μ‡ } β†’ ΞΌ ∘ ΞΌ ∼ ΞΌ ∘ 𝓕̇ ΞΌ
𝓕-assoc∼ {𝓀} ua {X} l = ⋍-gives-＝ ua (𝓕-assoc⋍ {𝓀} {X} l)

𝓕-Οƒ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X Γ— 𝓕 Y β†’ 𝓕 (X Γ— Y)
𝓕-Οƒ (x , m) = 𝓕̇ (Ξ» y β†’ (x , y)) m

𝓕-Ο„ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ 𝓕 X Γ— Y β†’ 𝓕 (X Γ— Y)
𝓕-Ο„ (l , y) = 𝓕̇ (Ξ» x β†’ (x , y)) l

𝓕-comm : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {l : 𝓕 X Γ— 𝓕 Y}
       β†’ ΞΌ (𝓕̇ 𝓕-Οƒ (𝓕-Ο„ l)) ⋍· ΞΌ (𝓕̇ 𝓕-Ο„ (𝓕-Οƒ l))
𝓕-comm = Γ—-comm , (Ξ» z β†’ refl)

𝓕-m : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ 𝓕 X Γ— 𝓕 Y β†’ 𝓕 (X Γ— Y)
𝓕-m (l , m) = ((Ξ» x β†’ curry 𝓕-Οƒ x m)β™―) l

Kleisli-Lawβ‚€ : {X : 𝓀 Μ‡ } (l : 𝓕 X) β†’ (Ξ· β™―) l ⋍ l
Kleisli-Lawβ‚€ (P , Ο†) = πŸ™-rneutral , refl

Kleisli-Law₁ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ 𝓕 Y) (x : X) β†’ (f β™―) (Ξ· x) ⋍ f x
Kleisli-Law₁ f x = πŸ™-lneutral , refl

Kleisli-Lawβ‚‚ : {X : π“₯ Μ‡ } {Y : 𝓦 Μ‡ } {Z : 𝓣 Μ‡ } (f : X β†’ 𝓕 Y) (g : Y β†’ 𝓕 Z) (l : 𝓕 X)
             β†’ (g β™― ∘ f β™―) l ⋍ ((g β™― ∘ f)β™―) l
Kleisli-Lawβ‚‚ f g l = Ξ£-assoc , refl

𝓕̇' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓕 X β†’ 𝓕 Y
𝓕̇' f = (Ξ· ∘ f)β™―

𝓕̇-agreement : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) (l : 𝓕 X)
             β†’ 𝓕̇' f l ⋍· 𝓕̇ f l
𝓕̇-agreement {𝓀} {π“₯} {X} {Y} f (P , Ο†) = πŸ™-rneutral , Ξ» _ β†’ refl

\end{code}