Agda UALib β

MartΓ­n EscardΓ³ 1st May 2020.

This is ported from the Midlands Graduate School 2019 lecture notes, which are available online from the following links.

html lecture notes

Source code repository

```
{-# OPTIONS --without-K --exact-split --safe #-}

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

data Color : π€β Μ  where
Black White : Color

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) ((a' , b) : Ξ£ a κ A x , B x a) {y : X} (p : x β‘ y)
β B x a' β B y (transport A p a')

transportd A B a Ο (refl y) = id

transport-Ξ£ : {X : π€ Μ } (A : X β π₯ Μ ) (B : (x : X) β A x β π¦ Μ )
{x : X} (y : X) (p : x β‘ y) (a : A x) {(a' , b) : Ξ£ a κ A x , B x a}

β transport (Ξ» x β Ξ£ y κ A x , B x y) p (a' , b)
β‘ transport A p a' , transportd A B a (a' , b) p b

transport-Ξ£ A B {x} x (refl x) a {Ο} = refl Ο

```