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)β»ΒΉ β©
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 ,
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}