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.
{-# 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)β»ΒΉ β© 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 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 Ο