Martin Escardo 1st May 2020.

This is ported from the Midlands Graduate School 2019 lecture notes

 https://www.cs.bham.ac.uk/~mhe/HoTT-UF.in-Agda-Lecture-Notes/HoTT-UF-Agda.html
 https://github.com/martinescardo/HoTT-UF.Agda-Lecture-Notes

\begin{code}

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

module MGS.Basic-UF where

open import MGS.MLTT public

is-center : (X : 𝓀 Μ‡ ) β†’ X β†’ 𝓀 Μ‡
is-center X c = (x : X) β†’ c ＝ x

is-singleton : 𝓀 Μ‡ β†’ 𝓀 Μ‡
is-singleton X = Ξ£ c κž‰ X , is-center X c

πŸ™-is-singleton : is-singleton πŸ™
πŸ™-is-singleton = ⋆ , πŸ™-induction (Ξ» x β†’ ⋆ ＝ x) (refl ⋆)

center : (X : 𝓀 Μ‡ ) β†’ is-singleton X β†’ X
center X (c , Ο†) = c

centrality : (X : 𝓀 Μ‡ ) (i : is-singleton X) (x : X) β†’ center X i ＝ x
centrality X (c , Ο†) = Ο†

is-subsingleton : 𝓀 Μ‡ β†’ 𝓀 Μ‡
is-subsingleton X = (x y : X) β†’ x ＝ y

𝟘-is-subsingleton : is-subsingleton 𝟘
𝟘-is-subsingleton x y = !𝟘 (x ＝ y) x

singletons-are-subsingletons : (X : 𝓀 Μ‡ ) β†’ is-singleton X β†’ is-subsingleton X
singletons-are-subsingletons X (c , Ο†) x y = x ＝⟨ (Ο† x)⁻¹ ⟩
                                             c ＝⟨ Ο† y ⟩
                                             y ∎

πŸ™-is-subsingleton : is-subsingleton πŸ™
πŸ™-is-subsingleton = singletons-are-subsingletons πŸ™ πŸ™-is-singleton

pointed-subsingletons-are-singletons : (X : 𝓀 Μ‡ )
                                     β†’ X β†’ is-subsingleton X β†’ is-singleton X

pointed-subsingletons-are-singletons X x s = (x , s x)

singleton-iff-pointed-and-subsingleton : {X : 𝓀 Μ‡ }
                                       β†’ is-singleton X ↔ (X Γ— is-subsingleton X)

singleton-iff-pointed-and-subsingleton {𝓀} {X} = (a , b)
 where
  a : is-singleton X β†’ X Γ— is-subsingleton X
  a s = center X s , singletons-are-subsingletons X s

  b : X Γ— is-subsingleton X β†’ is-singleton X
  b (x , t) = pointed-subsingletons-are-singletons X x t

is-prop is-truth-value : 𝓀 Μ‡ β†’ 𝓀 Μ‡
is-prop        = is-subsingleton
is-truth-value = is-subsingleton

is-set : 𝓀 Μ‡ β†’ 𝓀 Μ‡
is-set X = (x y : X) β†’ is-subsingleton (x ＝ y)

EM EM' : βˆ€ 𝓀 β†’ 𝓀 ⁺ Μ‡
EM  𝓀 = (X : 𝓀 Μ‡ ) β†’ is-subsingleton X β†’ X + Β¬ X
EM' 𝓀 = (X : 𝓀 Μ‡ ) β†’ is-subsingleton X β†’ is-singleton X + is-empty X

EM-gives-EM' : EM 𝓀 β†’ EM' 𝓀
EM-gives-EM' em X s = Ξ³ (em X s)
 where
  Ξ³ : X + Β¬ X β†’ is-singleton X + is-empty X
  Ξ³ (inl x) = inl (pointed-subsingletons-are-singletons X x s)
  Ξ³ (inr x) = inr x

EM'-gives-EM : EM' 𝓀 β†’ EM 𝓀
EM'-gives-EM em' X s = Ξ³ (em' X s)
 where
  Ξ³ : is-singleton X + is-empty X β†’ X + Β¬ X
  Ξ³ (inl i) = inl (center X i)
  Ξ³ (inr x) = inr x

no-unicorns : Β¬ (Ξ£ X κž‰ 𝓀 Μ‡ , is-subsingleton X Γ— Β¬ (is-singleton X) Γ— Β¬ (is-empty X))
no-unicorns (X , i , f , g) = c
 where
  e : is-empty X
  e x = f (pointed-subsingletons-are-singletons X x i)

  c : 𝟘
  c = g e

module magmas where

 Magma : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
 Magma 𝓀 = Ξ£ X κž‰ 𝓀 Μ‡ , is-set X Γ— (X β†’ X β†’ X)

 ⟨_⟩ : Magma 𝓀 β†’ 𝓀 Μ‡
 ⟨ X , i , _·_ ⟩ = X

 magma-is-set : (M : Magma 𝓀) β†’ is-set ⟨ M ⟩
 magma-is-set (X , i , _Β·_) = i

 magma-operation : (M : Magma 𝓀) β†’ ⟨ M ⟩ β†’ ⟨ M ⟩ β†’ ⟨ M ⟩
 magma-operation (X , i , _Β·_) = _Β·_

 syntax magma-operation M x y = x ·⟨ M ⟩ y

 is-magma-hom : (M N : Magma 𝓀) β†’ (⟨ M ⟩ β†’ ⟨ N ⟩) β†’ 𝓀 Μ‡
 is-magma-hom M N f = (x y : ⟨ M ⟩) β†’ f (x ·⟨ M ⟩ y) ＝ f x ·⟨ N ⟩ f y

 id-is-magma-hom : (M : Magma 𝓀) β†’ is-magma-hom M M (𝑖𝑑 ⟨ M ⟩)
 id-is-magma-hom M = Ξ» (x y : ⟨ M ⟩) β†’ refl (x ·⟨ M ⟩ y)

 is-magma-iso : (M N : Magma 𝓀) β†’ (⟨ M ⟩ β†’ ⟨ N ⟩) β†’ 𝓀 Μ‡
 is-magma-iso M N f = is-magma-hom M N f
                    Γ— (Ξ£ g κž‰ (⟨ N ⟩ β†’ ⟨ M ⟩), is-magma-hom N M g
                                            Γ— (g ∘ f ∼ 𝑖𝑑 ⟨ M ⟩)
                                            Γ— (f ∘ g ∼ 𝑖𝑑 ⟨ N ⟩))

 id-is-magma-iso : (M : Magma 𝓀) β†’ is-magma-iso M M (𝑖𝑑 ⟨ M ⟩)
 id-is-magma-iso M = id-is-magma-hom M ,
                     𝑖𝑑 ⟨ M ⟩ ,
                     id-is-magma-hom M ,
                     refl ,
                     refl

 Idβ†’iso : {M N : Magma 𝓀} β†’ M ＝ N β†’ ⟨ M ⟩ β†’ ⟨ N ⟩
 Idβ†’iso p = transport ⟨_⟩ p

 Idβ†’iso-is-iso : {M N : Magma 𝓀} (p : M ＝ N) β†’ is-magma-iso M N (Idβ†’iso p)
 Id→iso-is-iso (refl M) = id-is-magma-iso M

 _β‰…β‚˜_ : Magma 𝓀 β†’ Magma 𝓀 β†’ 𝓀 Μ‡
 M β‰…β‚˜ N = Ξ£ f κž‰ (⟨ M ⟩ β†’ ⟨ N ⟩), is-magma-iso M N f

 magma-Idβ†’iso : {M N : Magma 𝓀} β†’ M ＝ N β†’ M β‰…β‚˜ N
 magma-Id→iso p = (Id→iso p , Id→iso-is-iso p)

 ∞-Magma : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
 ∞-Magma 𝓀 = Ξ£ X κž‰ 𝓀 Μ‡ , (X β†’ X β†’ X)

module monoids where

 left-neutral : {X : 𝓀 Μ‡ } β†’ X β†’ (X β†’ X β†’ X) β†’ 𝓀 Μ‡
 left-neutral e _Β·_ = βˆ€ x β†’ e Β· x ＝ x

 right-neutral : {X : 𝓀 Μ‡ } β†’ X β†’ (X β†’ X β†’ X) β†’ 𝓀 Μ‡
 right-neutral e _Β·_ = βˆ€ x β†’ x Β· e ＝ x

 associative : {X : 𝓀 Μ‡ } β†’ (X β†’ X β†’ X) β†’ 𝓀 Μ‡
 associative _Β·_ = βˆ€ x y z β†’ (x Β· y) Β· z ＝ x Β· (y Β· z)

 Monoid : (𝓀 : Universe) β†’ 𝓀 ⁺ Μ‡
 Monoid 𝓀 = Ξ£ X κž‰ 𝓀 Μ‡ , is-set X
                      Γ— (Ξ£ Β· κž‰ (X β†’ X β†’ X) , (Ξ£ e κž‰ X , (left-neutral e Β·)
                                                      Γ— (right-neutral e Β·)
                                                      Γ— (associative Β·)))

refl-left : {X : 𝓀 Μ‡ } {x y : X} {p : x ＝ y} β†’ refl x βˆ™ p ＝ p
refl-left {𝓀} {X} {x} {x} {refl x} = refl (refl x)

refl-right : {X : 𝓀 Μ‡ } {x y : X} {p : x ＝ y} β†’ p βˆ™ refl y ＝ p
refl-right {𝓀} {X} {x} {y} {p} = refl p

βˆ™assoc : {X : 𝓀 Μ‡ } {x y z t : X} (p : x ＝ y) (q : y ＝ z) (r : z ＝ t)
       β†’ (p βˆ™ q) βˆ™ r ＝ p βˆ™ (q βˆ™ r)

βˆ™assoc p q (refl z) = refl (p βˆ™ q)

⁻¹-leftβˆ™ : {X : 𝓀 Μ‡ } {x y : X} (p : x ＝ y)
         β†’ p ⁻¹ βˆ™ p ＝ refl y

⁻¹-leftβˆ™ (refl x) = refl (refl x)

⁻¹-rightβˆ™ : {X : 𝓀 Μ‡ } {x y : X} (p : x ＝ y)
          β†’ p βˆ™ p ⁻¹ ＝ refl x

⁻¹-rightβˆ™ (refl x) = refl (refl x)

⁻¹-involutive : {X : 𝓀 Μ‡ } {x y : X} (p : x ＝ y)
              β†’ (p ⁻¹)⁻¹ ＝ p

⁻¹-involutive (refl x) = refl (refl x)

ap-refl : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) (x : X)
        β†’ ap f (refl x) ＝ refl (f x)

ap-refl f x = refl (refl (f x))

ap-βˆ™ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) {x y z : X} (p : x ＝ y) (q : y ＝ z)
     β†’ ap f (p βˆ™ q) ＝ ap f p βˆ™ ap f q

ap-βˆ™ f p (refl y) = refl (ap f p)

ap⁻¹ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) {x y : X} (p : x ＝ y)
     β†’ (ap f p)⁻¹ ＝ ap f (p ⁻¹)

ap⁻¹ f (refl x) = refl (refl (f x))

ap-id : {X : 𝓀 Μ‡ } {x y : X} (p : x ＝ y)
      β†’ ap id p ＝ p

ap-id (refl x) = refl (refl x)

ap-∘ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ }
       (f : X β†’ Y) (g : Y β†’ Z) {x y : X} (p : x ＝ y)
     β†’ ap (g ∘ f) p ＝ (ap g ∘ ap f) p

ap-∘ f g (refl x) = refl (refl (g (f x)))

transportβˆ™ : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) {x y z : X} (p : x ＝ y) (q : y ＝ z)
           β†’ transport A (p βˆ™ q) ＝ transport A q ∘ transport A p

transportβˆ™ A p (refl y) = refl (transport A p)

Nat : {X : 𝓀 Μ‡ } β†’ (X β†’ π“₯ Μ‡ ) β†’ (X β†’ 𝓦 Μ‡ ) β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
Nat A B = (x : domain A) β†’ A x β†’ B x

Nats-are-natural : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ ) (Ο„ : Nat A B)
                 β†’ {x y : X} (p : x ＝ y)
                 β†’ Ο„ y ∘ transport A p ＝ transport B p ∘ Ο„ x

Nats-are-natural A B Ο„ (refl x) = refl (Ο„ x)

NatΞ£ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ } β†’ Nat A B β†’ Ξ£ A β†’ Ξ£ B
NatΞ£ Ο„ (x , a) = (x , Ο„ x a)

transport-ap : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (A : Y β†’ 𝓦 Μ‡ )
               (f : X β†’ Y) {x x' : X} (p : x ＝ x') (a : A (f x))
             β†’ transport (A ∘ f) p a ＝ transport A (ap f p) a

transport-ap A f (refl x) a = refl a

apd : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (f : (x : X) β†’ A x) {x y : X}
      (p : x ＝ y) β†’ transport A p (f x) ＝ f y

apd f (refl x) = refl (f x)

to-Ξ£-＝ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {Οƒ Ο„ : Ξ£ A}
       β†’ (Ξ£ p κž‰ pr₁ Οƒ ＝ pr₁ Ο„ , transport A p (prβ‚‚ Οƒ) ＝ prβ‚‚ Ο„)
       β†’ Οƒ ＝ Ο„

to-Σ-＝ (refl x , refl a) = refl (x , a)

from-Ξ£-＝ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {Οƒ Ο„ : Ξ£ A}
         β†’ Οƒ ＝ Ο„
         β†’ Ξ£ p κž‰ pr₁ Οƒ ＝ pr₁ Ο„ , transport A p (prβ‚‚ Οƒ) ＝ prβ‚‚ Ο„

from-Σ-＝ (refl (x , a)) = (refl x , refl a)

to-Ξ£-＝' : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {x : X} {a a' : A x}
        β†’ a ＝ a' β†’ Id (Ξ£ A) (x , a) (x , a')

to-Ξ£-＝' {𝓀} {π“₯} {X} {A} {x} = ap (Ξ» - β†’ (x , -))

transport-Γ— : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ )
                {x y : X} (p : x ＝ y) {c : A x Γ— B x}

            β†’ transport (Ξ» x β†’ A x Γ— B x) p c
            ＝ (transport A p (pr₁ c) , transport B p (prβ‚‚ c))

transport-Γ— A B (refl _) = refl _

transportd : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : (x : X) β†’ A x β†’ 𝓦 Μ‡ )
             {x : X}  (a : A x) {y : X} (p : x ＝ y)
           β†’ B x a β†’ B y (transport A p a)

transportd A B a (refl x) = id

transport-Ξ£ : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : (x : X) β†’ A x β†’ 𝓦 Μ‡ )
              {x : X} (y : X) (p : x ＝ y) (a : A x) {b : B x a}
            β†’ transport (Ξ» x β†’ Ξ£ y κž‰ A x , B x y) p (a , b)
            ＝ transport A p a , transportd A B a p b

transport-Ξ£ A B {x} x (refl x) a {b} = refl (a , b)

\end{code}