{-# OPTIONS --without-K --exact-split --safe --auto-inline #-} module HoTT where open import Universes public variable π€ π₯ π¦ π£ : Universe data π : π€β Μ where β : π π-induction : (A : π β π€βΜ ) β A β β (x : π) β A x π-induction A a β = a π-recursion : (B : π€βΜ ) β B β (π β B) π-recursion B b x = π-induction (Ξ» _ β B) b x !π' : (X : π€βΜ ) β X β π !π' X x = β !π : {X : π€βΜ } β X β π !π x = β data π : π€ββΜ where π-induction : (A : π β π€ Μ ) β (x : π) β A x π-induction A () π-recursion : (A : π€ Μ ) β π β A π-recursion A a = π-induction (Ξ» _ β A) a !π : (A : π€ Μ ) β π β A !π = π-recursion is-empty : π€ Μ β π€ Μ is-empty X = X β π Β¬ : π€ Μ β π€ Μ Β¬ X = X β π data β : π€β Μ where zero : β succ : β β β {-# BUILTIN NATURAL β #-} β-induction : (A : β β π€ Μ ) β A 0 β ((n : β) β A n β A (succ n)) β (n : β) β A n β-induction A aβ f = h where h : (n : β) β A n h 0 = aβ h (succ n) = f n (h n) β-recursion : (X : π€ Μ ) β X β (β β X β X) β β β X β-recursion X = β-induction (Ξ» _ β X) β-iteration : (X : π€ Μ ) β X β (X β X) β β β X β-iteration X x f = β-recursion X x (Ξ» _ x β f x) module Arithmetic where _+_ _Γ_ : β β β β β x + 0 = x x + succ y = succ (x + y) x Γ 0 = 0 x Γ succ y = x + x Γ y infixl 20 _+_ infixl 21 _Γ_ module Arithmetic' where _+_ _Γ_ : β β β β β x + y = h y where h : β β β h = β-iteration β x succ x Γ y = h y where h : β β β h = β-iteration β 0 (x +_) infixl 20 _+_ infixl 21 _Γ_ module β-order where _β€_ _β₯_ : β β β β π€β Μ 0 β€ y = π succ x β€ 0 = π succ x β€ succ y = x β€ y x β₯ y = y β€ x infix 10 _β€_ infix 10 _β₯_ data _+_ {π€ π₯} (X : π€ Μ ) (Y : π₯ Μ ) : π€ β π₯ Μ where inl : X β X + Y inr : Y β X + Y +-induction : {X : π€ Μ } {Y : π₯ Μ } (A : X + Y β π¦ Μ ) β ((x : X) β A (inl x)) β ((y : Y) β A (inr y)) β (z : X + Y) β A z +-induction A f g (inl x) = f x +-induction A f g (inr y) = g y +-recursion : {X : π€ Μ } {Y : π₯ Μ } {A : π¦ Μ } β (X β A) β (Y β A) β X + Y β A +-recursion {π€} {π₯} {π¦} {X} {Y} {A} = +-induction (Ξ» _ β A) π : π€β Μ π = π + π pattern β = inl β pattern β = inr β π-induction : (A : π β π€ Μ ) β A β β A β β (n : π) β A n π-induction A aβ aβ β = aβ π-induction A aβ aβ β = aβ π-induction' : (A : π β π€ Μ ) β A β β A β β (n : π) β A n π-induction' A aβ aβ = +-induction A (π-induction (Ξ» (x : π) β A (inl x)) aβ) (π-induction (Ξ» (y : π) β A (inr y)) aβ) record Ξ£ {π€ π₯} {X : π€ Μ } (Y : X β π₯ Μ ) : π€ β π₯ Μ where constructor _,_ field x : X y : Y x prβ : {X : π€ Μ } {Y : X β π₯ Μ } β Ξ£ Y β X prβ (x , y) = x prβ : {X : π€ Μ } {Y : X β π₯ Μ } β (z : Ξ£ Y) β Y (prβ z) prβ (x , y) = y -Ξ£ : {π€ π₯ : Universe} (X : π€ Μ ) (Y : X β π₯ Μ ) β π€ β π₯ Μ -Ξ£ X Y = Ξ£ Y syntax -Ξ£ X (Ξ» x β y) = Ξ£ x κ X , y Ξ£-induction : {X : π€ Μ } {Y : X β π₯ Μ } {A : Ξ£ Y β π¦ Μ } β ((x : X) (y : Y x) β A (x , y)) β ((x , y) : Ξ£ Y) β A (x , y) Ξ£-induction g (x , y) = g x y curry : {X : π€ Μ } {Y : X β π₯ Μ } {A : Ξ£ Y β π¦ Μ } β (((x , y) : Ξ£ Y) β A (x , y)) β ((x : X) (y : Y x) β A (x , y)) curry f x y = f (x , y) _Γ_ : π€ Μ β π₯ Μ β π€ β π₯ Μ X Γ Y = Ξ£ x κ X , Y Ξ : {X : π€ Μ } (A : X β π₯ Μ ) β π€ β π₯ Μ Ξ {π€} {π₯} {X} A = (x : X) β A x -Ξ : {π€ π₯ : Universe} (X : π€ Μ ) (Y : X β π₯ Μ ) β π€ β π₯ Μ -Ξ X Y = Ξ Y syntax -Ξ A (Ξ» x β b) = Ξ x κ A , b id : {X : π€ Μ } β X β X id x = x ππ : (X : π€ Μ ) β X β X ππ X = id _β_ : {X : π€ Μ } {Y : π₯ Μ } {Z : Y β π¦ Μ } β ((y : Y) β Z y) β (f : X β Y) β (x : X) β Z (f x) g β f = Ξ» x β g (f x) domain : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π€ Μ domain {π€} {π₯} {X} {Y} f = X codomain : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π₯ Μ codomain {π€} {π₯} {X} {Y} f = Y type-of : {X : π€ Μ } β X β π€ Μ type-of {π€} {X} x = X data Id {π€} (X : π€ Μ ) : X β X β π€ Μ where refl : (x : X) β Id X x x _β‘_ : {X : π€ Μ } β X β X β π€ Μ x β‘ y = Id _ x y π : (X : π€ Μ ) (A : (x y : X) β x β‘ y β π₯ Μ ) β ((x : X) β A x x (refl x)) β (x y : X) (p : x β‘ y) β A x y p π X A f x x (refl x) = f x β : {X : π€ Μ } (x : X) (B : (y : X) β x β‘ y β π₯ Μ ) β B x (refl x) β (y : X) (p : x β‘ y) β B y p β x B b x (refl x) = b π' : (X : π€ Μ ) (A : (x y : X) β x β‘ y β π₯ Μ ) β ((x : X) β A x x (refl x)) β (x y : X) (p : x β‘ y) β A x y p π' X A f x = β x (A x) (f x) πs-agreement : (X : π€ Μ ) (A : (x y : X) β x β‘ y β π₯ Μ ) (f : (x : X) β A x x (refl x)) (x y : X) (p : x β‘ y) β π X A f x y p β‘ π' X A f x y p πs-agreement X A f x x (refl x) = refl (f x) transport : {X : π€ Μ } (A : X β π₯ Μ ) {x y : X} β x β‘ y β A x β A y transport A (refl x) = ππ (A x) transportπ : {X : π€ Μ } (A : X β π₯ Μ ) {x y : X} β x β‘ y β A x β A y transportπ {π€} {π₯} {X} A {x} {y} = π X (Ξ» x y _ β A x β A y) (Ξ» x β ππ (A x)) x y nondep-β : {X : π€ Μ } (x : X) (A : X β π₯ Μ ) β A x β (y : X) β x β‘ y β A y nondep-β x A = β x (Ξ» y _ β A y) transportβ : {X : π€ Μ } (A : X β π₯ Μ ) {x y : X} β x β‘ y β A x β A y transportβ A {x} {y} p a = nondep-β x A a y p transports-agreement : {X : π€ Μ } (A : X β π₯ Μ ) {x y : X} (p : x β‘ y) β (transportβ A p β‘ transport A p) Γ (transportπ A p β‘ transport A p) transports-agreement A (refl x) = refl (transport A (refl x)) , refl (transport A (refl x)) lhs : {X : π€ Μ } {x y : X} β x β‘ y β X lhs {π€} {X} {x} {y} p = x rhs : {X : π€ Μ } {x y : X} β x β‘ y β X rhs {π€} {X} {x} {y} p = y _β_ : {X : π€ Μ } {x y z : X} β x β‘ y β y β‘ z β x β‘ z p β q = transport (lhs p β‘_) q p _β‘β¨_β©_ : {X : π€ Μ } (x : X) {y z : X} β x β‘ y β y β‘ z β x β‘ z x β‘β¨ p β© q = p β q _β : {X : π€ Μ } (x : X) β x β‘ x x β = refl x _β»ΒΉ : {X : π€ Μ } β {x y : X} β x β‘ y β y β‘ x p β»ΒΉ = transport (_β‘ lhs p) p (refl (lhs p)) _β'_ : {X : π€ Μ } {x y z : X} β x β‘ y β y β‘ z β x β‘ z p β' q = transport (_β‘ rhs q) (p β»ΒΉ) q βagreement : {X : π€ Μ } {x y z : X} (p : x β‘ y) (q : y β‘ z) β p β' q β‘ p β q βagreement (refl x) (refl x) = refl (refl x) rdnel : {X : π€ Μ } {x y : X} (p : x β‘ y) β p β refl y β‘ p rdnel p = refl p rdner : {X : π€ Μ } {y z : X} (q : y β‘ z) β refl y β' q β‘ q rdner q = refl q ap : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) {x x' : X} β x β‘ x' β f x β‘ f x' ap f {x} {x'} p = transport (Ξ» - β f x β‘ f -) p (refl (f x)) _βΌ_ : {X : π€ Μ } {A : X β π₯ Μ } β Ξ A β Ξ A β π€ β π₯ Μ f βΌ g = β x β f x β‘ g x ¬¬ ¬¬¬ : π€ Μ β π€ Μ Β¬Β¬ A = Β¬(Β¬ A) ¬¬¬ A = Β¬(¬¬ A) dni : (A : π€ Μ ) β A β ¬¬ A dni A a u = u a contrapositive : {A : π€ Μ } {B : π₯ Μ } β (A β B) β (Β¬ B β Β¬ A) contrapositive f v a = v (f a) tno : (A : π€ Μ ) β ¬¬¬ A β Β¬ A tno A = contrapositive (dni A) _β_ : π€ Μ β π₯ Μ β π€ β π₯ Μ X β Y = (X β Y) Γ (Y β X) lr-implication : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β (X β Y) lr-implication = prβ rl-implication : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β (Y β X) rl-implication = prβ absurdityΒ³-is-absurdity : {A : π€ Μ } β ¬¬¬ A β Β¬ A absurdityΒ³-is-absurdity {π€} {A} = firstly , secondly where firstly : ¬¬¬ A β Β¬ A firstly = contrapositive (dni A) secondly : Β¬ A β ¬¬¬ A secondly = dni (Β¬ A) _β’_ : {X : π€ Μ } β X β X β π€ Μ x β’ y = Β¬(x β‘ y) β’-sym : {X : π€ Μ } {x y : X} β x β’ y β y β’ x β’-sym {π€} {X} {x} {y} u = Ξ» (p : y β‘ x) β u (p β»ΒΉ) IdβFun : {X Y : π€ Μ } β X β‘ Y β X β Y IdβFun {π€} = transport (ππ (π€ Μ )) IdβFun' : {X Y : π€ Μ } β X β‘ Y β X β Y IdβFun' (refl X) = ππ X IdβFuns-agree : {X Y : π€ Μ } (p : X β‘ Y) β IdβFun p β‘ IdβFun' p IdβFuns-agree (refl X) = refl (ππ X) π-is-not-π : π β’ π π-is-not-π p = IdβFun p β β-is-not-β : β β’ β β-is-not-β p = π-is-not-π q where f : π β π€β Μ f β = π f β = π q : π β‘ π q = ap f p β-is-not-β[not-an-MLTT-proof] : Β¬(β β‘ β) β-is-not-β[not-an-MLTT-proof] () decidable : π€ Μ β π€ Μ decidable A = A + Β¬ A has-decidable-equality : π€ Μ β π€ Μ has-decidable-equality X = (x y : X) β decidable (x β‘ y) π-has-decidable-equality : has-decidable-equality π π-has-decidable-equality β β = inl (refl β) π-has-decidable-equality β β = inr (β’-sym β-is-not-β) π-has-decidable-equality β β = inr β-is-not-β π-has-decidable-equality β β = inl (refl β) not-zero-is-one : (n : π) β n β’ β β n β‘ β not-zero-is-one β f = !π (β β‘ β) (f (refl β)) not-zero-is-one β f = refl β inl-inr-disjoint-images : {X : π€ Μ } {Y : π₯ Μ } {x : X} {y : Y} β inl x β’ inr y inl-inr-disjoint-images {π€} {π₯} {X} {Y} p = π-is-not-π q where f : X + Y β π€β Μ f (inl x) = π f (inr y) = π q : π β‘ π q = ap f p right-fails-gives-left-holds : {P : π€ Μ } {Q : π₯ Μ } β P + Q β Β¬ Q β P right-fails-gives-left-holds (inl p) u = p right-fails-gives-left-holds (inr q) u = !π _ (u q) module twin-primes where open Arithmetic renaming (_Γ_ to _*_ ; _+_ to _β_) open β-order is-prime : β β π€β Μ is-prime n = (n β₯ 2) Γ ((x y : β) β x * y β‘ n β (x β‘ 1) + (x β‘ n)) twin-prime-conjecture : π€β Μ twin-prime-conjecture = (n : β) β Ξ£ p κ β , (p β₯ n) Γ is-prime p Γ is-prime (p β 2) positive-not-zero : (x : β) β succ x β’ 0 positive-not-zero x p = π-is-not-π (g p) where f : β β π€β Μ f 0 = π f (succ x) = π g : succ x β‘ 0 β π β‘ π g = ap f pred : β β β pred 0 = 0 pred (succ n) = n succ-lc : {x y : β} β succ x β‘ succ y β x β‘ y succ-lc = ap pred β-has-decidable-equality : has-decidable-equality β β-has-decidable-equality 0 0 = inl (refl 0) β-has-decidable-equality 0 (succ y) = inr (β’-sym (positive-not-zero y)) β-has-decidable-equality (succ x) 0 = inr (positive-not-zero x) β-has-decidable-equality (succ x) (succ y) = f (β-has-decidable-equality x y) where f : decidable (x β‘ y) β decidable (succ x β‘ succ y) f (inl p) = inl (ap succ p) f (inr k) = inr (Ξ» (s : succ x β‘ succ y) β k (succ-lc s)) module basic-arithmetic-and-order where open β-order public open Arithmetic renaming (_+_ to _β_) hiding (_Γ_) +-assoc : (x y z : β) β (x β y) β z β‘ x β (y β z) +-assoc x y 0 = (x β y) β 0 β‘β¨ refl _ β© x β (y β 0) β +-assoc x y (succ z) = (x β y) β succ z β‘β¨ refl _ β© succ ((x β y) β z) β‘β¨ ap succ IH β© succ (x β (y β z)) β‘β¨ refl _ β© x β (y β succ z) β where IH : (x β y) β z β‘ x β (y β z) IH = +-assoc x y z +-assoc' : (x y z : β) β (x β y) β z β‘ x β (y β z) +-assoc' x y zero = refl _ +-assoc' x y (succ z) = ap succ (+-assoc' x y z) +-base-on-first : (x : β) β 0 β x β‘ x +-base-on-first 0 = refl 0 +-base-on-first (succ x) = 0 β succ x β‘β¨ refl _ β© succ (0 β x) β‘β¨ ap succ IH β© succ x β where IH : 0 β x β‘ x IH = +-base-on-first x +-step-on-first : (x y : β) β succ x β y β‘ succ (x β y) +-step-on-first x zero = refl (succ x) +-step-on-first x (succ y) = succ x β succ y β‘β¨ refl _ β© succ (succ x β y) β‘β¨ ap succ IH β© succ (x β succ y) β where IH : succ x β y β‘ succ (x β y) IH = +-step-on-first x y +-comm : (x y : β) β x β y β‘ y β x +-comm 0 y = 0 β y β‘β¨ +-base-on-first y β© y β‘β¨ refl _ β© y β 0 β +-comm (succ x) y = succ x β y β‘β¨ +-step-on-first x y β© succ(x β y) β‘β¨ ap succ IH β© succ(y β x) β‘β¨ refl _ β© y β succ x β where IH : x β y β‘ y β x IH = +-comm x y +-lc : (x y z : β) β x β y β‘ x β z β y β‘ z +-lc 0 y z p = y β‘β¨ (+-base-on-first y)β»ΒΉ β© 0 β y β‘β¨ p β© 0 β z β‘β¨ +-base-on-first z β© z β +-lc (succ x) y z p = IH where q = succ (x β y) β‘β¨ (+-step-on-first x y)β»ΒΉ β© succ x β y β‘β¨ p β© succ x β z β‘β¨ +-step-on-first x z β© succ (x β z) β IH : y β‘ z IH = +-lc x y z (succ-lc q) _βΌ_ : β β β β π€β Μ x βΌ y = Ξ£ z κ β , x β z β‘ y β€-gives-βΌ : (x y : β) β x β€ y β x βΌ y β€-gives-βΌ 0 0 l = 0 , refl 0 β€-gives-βΌ 0 (succ y) l = succ y , +-base-on-first (succ y) β€-gives-βΌ (succ x) 0 l = !π (succ x βΌ zero) l β€-gives-βΌ (succ x) (succ y) l = Ξ³ where IH : x βΌ y IH = β€-gives-βΌ x y l z : β z = prβ IH p : x β z β‘ y p = prβ IH Ξ³ : succ x βΌ succ y Ξ³ = z , (succ x β z β‘β¨ +-step-on-first x z β© succ (x β z) β‘β¨ ap succ p β© succ y β) βΌ-gives-β€ : (x y : β) β x βΌ y β x β€ y βΌ-gives-β€ 0 0 (z , p) = β βΌ-gives-β€ 0 (succ y) (z , p) = β βΌ-gives-β€ (succ x) 0 (z , p) = positive-not-zero (x β z) q where q = succ (x β z) β‘β¨ (+-step-on-first x z)β»ΒΉ β© succ x β z β‘β¨ p β© zero β βΌ-gives-β€ (succ x) (succ y) (z , p) = IH where q = succ (x β z) β‘β¨ (+-step-on-first x z)β»ΒΉ β© succ x β z β‘β¨ p β© succ y β IH : x β€ y IH = βΌ-gives-β€ x y (z , succ-lc q) β€-refl : (n : β) β n β€ n β€-refl zero = β β€-refl (succ n) = β€-refl n β€-trans : (l m n : β) β l β€ m β m β€ n β l β€ n β€-trans zero m n p q = β β€-trans (succ l) zero n p q = !π (succ l β€ n) p β€-trans (succ l) (succ m) zero p q = q β€-trans (succ l) (succ m) (succ n) p q = β€-trans l m n p q β€-anti : (m n : β) β m β€ n β n β€ m β m β‘ n β€-anti zero zero p q = refl zero β€-anti zero (succ n) p q = !π (zero β‘ succ n) q β€-anti (succ m) zero p q = !π (succ m β‘ zero) p β€-anti (succ m) (succ n) p q = ap succ (β€-anti m n p q) β€-succ : (n : β) β n β€ succ n β€-succ zero = β β€-succ (succ n) = β€-succ n zero-minimal : (n : β) β zero β€ n zero-minimal n = β unique-minimal : (n : β) β n β€ zero β n β‘ zero unique-minimal zero p = refl zero unique-minimal (succ n) p = !π (succ n β‘ zero) p β€-split : (m n : β) β m β€ succ n β (m β€ n) + (m β‘ succ n) β€-split zero n l = inl l β€-split (succ m) zero l = inr (ap succ (unique-minimal m l)) β€-split (succ m) (succ n) l = +-recursion inl (inr β ap succ) (β€-split m n l) _<_ : β β β β π€β Μ x < y = succ x β€ y infix 10 _<_ not-<-gives-β₯ : (m n : β) β Β¬(n < m) β m β€ n not-<-gives-β₯ zero n u = zero-minimal n not-<-gives-β₯ (succ m) zero u = dni (zero < succ m) (zero-minimal m) u not-<-gives-β₯ (succ m) (succ n) u = not-<-gives-β₯ m n u bounded-β-next : (A : β β π€ Μ ) (k : β) β A k β ((n : β) β n < k β A n) β (n : β) β n < succ k β A n bounded-β-next A k a Ο n l = +-recursion f g s where s : (n < k) + (succ n β‘ succ k) s = β€-split (succ n) k l f : n < k β A n f = Ο n g : succ n β‘ succ k β A n g p = transport A ((succ-lc p)β»ΒΉ) a root : (β β β) β π€β Μ root f = Ξ£ n κ β , f n β‘ 0 _has-no-root<_ : (β β β) β β β π€β Μ f has-no-root< k = (n : β) β n < k β f n β’ 0 is-minimal-root : (β β β) β β β π€β Μ is-minimal-root f m = (f m β‘ 0) Γ (f has-no-root< m) at-most-one-minimal-root : (f : β β β) (m n : β) β is-minimal-root f m β is-minimal-root f n β m β‘ n at-most-one-minimal-root f m n (p , Ο) (q , Ο) = c m n a b where a : Β¬(m < n) a u = Ο m u p b : Β¬(n < m) b v = Ο n v q c : (m n : β) β Β¬(m < n) β Β¬(n < m) β m β‘ n c m n u v = β€-anti m n (not-<-gives-β₯ m n v) (not-<-gives-β₯ n m u) minimal-root : (β β β) β π€β Μ minimal-root f = Ξ£ m κ β , is-minimal-root f m minimal-root-is-root : β f β minimal-root f β root f minimal-root-is-root f (m , p , _) = m , p bounded-β-search : β k f β (minimal-root f) + (f has-no-root< k) bounded-β-search zero f = inr (Ξ» n β !π (f n β’ 0)) bounded-β-search (succ k) f = +-recursion Ο Ξ³ (bounded-β-search k f) where A : β β (β β β) β π€β Μ A k f = (minimal-root f) + (f has-no-root< k) Ο : minimal-root f β A (succ k) f Ο = inl Ξ³ : f has-no-root< k β A (succ k) f Ξ³ u = +-recursion Ξ³β Ξ³β (β-has-decidable-equality (f k) 0) where Ξ³β : f k β‘ 0 β A (succ k) f Ξ³β p = inl (k , p , u) Ξ³β : f k β’ 0 β A (succ k) f Ξ³β v = inr (bounded-β-next (Ξ» n β f n β’ 0) k v u) root-gives-minimal-root : β f β root f β minimal-root f root-gives-minimal-root f (n , p) = Ξ³ where g : Β¬(f has-no-root< (succ n)) g Ο = Ο n (β€-refl n) p Ξ³ : minimal-root f Ξ³ = right-fails-gives-left-holds (bounded-β-search (succ n) f) g is-singleton : π€ Μ β π€ Μ is-singleton X = Ξ£ c κ X , ((x : X) β c β‘ x) is-center : (X : π€ Μ ) β X β π€ Μ is-center X c = (x : X) β c β‘ x π-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-Ξ£-β‘-again : {X : π€ Μ } {A : X β π₯ Μ } {(x , a) (y , b) : Ξ£ A} β Ξ£ p κ x β‘ y , transport A p a β‘ b β (x , a) β‘ (y , b) to-Ξ£-β‘-again (refl x , refl a) = refl (x , a) from-Ξ£-β‘-again : {X : π€ Μ } {A : X β π₯ Μ } {(x , a) (y , b) : Ξ£ A} β (x , a) β‘ (y , b) β Ξ£ p κ x β‘ y , transport A p a β‘ b from-Ξ£-β‘-again (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) {(a , b) : A x Γ B x} β transport (Ξ» x β A x Γ B x) p (a , b) β‘ (transport A p a , transport B p b) transport-Γ A B (refl _) = refl _ transportd : {X : π€ Μ } (A : X β π₯ Μ ) (B : (x : X) β A x β π¦ Μ ) {x : 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 , b) (refl x) = id transport-Ξ£ : {X : π€ Μ } (A : X β π₯ Μ ) (B : (x : X) β A x β π¦ Μ ) {x : X} {y : X} (p : x β‘ y) {(a , b) : Ξ£ a κ A x , B x a} β transport (Ξ» - β Ξ£ (B -)) p (a , b) β‘ transport A p a , transportd A B (a , b) p b transport-Ξ£ A B (refl x) {a , b} = refl (a , b) _is-of-hlevel_ : π€ Μ β β β π€ Μ X is-of-hlevel 0 = is-singleton X X is-of-hlevel (succ n) = (x x' : X) β ((x β‘ x') is-of-hlevel n) wconstant : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π€ β π₯ Μ wconstant f = (x x' : domain f) β f x β‘ f x' wconstant-endomap : π€ Μ β π€ Μ wconstant-endomap X = Ξ£ f κ (X β X), wconstant f wcmap : (X : π€ Μ ) β wconstant-endomap X β (X β X) wcmap X (f , w) = f wcmap-constancy : (X : π€ Μ ) (c : wconstant-endomap X) β wconstant (wcmap X c) wcmap-constancy X (f , w) = w Hedberg : {X : π€ Μ } (x : X) β ((y : X) β wconstant-endomap (x β‘ y)) β (y : X) β is-subsingleton (x β‘ y) Hedberg {π€} {X} x c y p q = p β‘β¨ a y p β© (f x (refl x))β»ΒΉ β f y p β‘β¨ ap (Ξ» - β (f x (refl x))β»ΒΉ β -) (ΞΊ y p q) β© (f x (refl x))β»ΒΉ β f y q β‘β¨ (a y q)β»ΒΉ β© q β where f : (y : X) β x β‘ y β x β‘ y f y = wcmap (x β‘ y) (c y) ΞΊ : (y : X) (p q : x β‘ y) β f y p β‘ f y q ΞΊ y = wcmap-constancy (x β‘ y) (c y) a : (y : X) (p : x β‘ y) β p β‘ (f x (refl x))β»ΒΉ β f y p a x (refl x) = (β»ΒΉ-leftβ (f x (refl x)))β»ΒΉ wconstant-β‘-endomaps : π€ Μ β π€ Μ wconstant-β‘-endomaps X = (x y : X) β wconstant-endomap (x β‘ y) sets-have-wconstant-β‘-endomaps : (X : π€ Μ ) β is-set X β wconstant-β‘-endomaps X sets-have-wconstant-β‘-endomaps X s x y = (f , ΞΊ) where f : x β‘ y β x β‘ y f p = p ΞΊ : (p q : x β‘ y) β f p β‘ f q ΞΊ p q = s x y p q types-with-wconstant-β‘-endomaps-are-sets : (X : π€ Μ ) β wconstant-β‘-endomaps X β is-set X types-with-wconstant-β‘-endomaps-are-sets X c x = Hedberg x (Ξ» y β wcmap (x β‘ y) (c x y) , wcmap-constancy (x β‘ y) (c x y)) subsingletons-have-wconstant-β‘-endomaps : (X : π€ Μ ) β is-subsingleton X β wconstant-β‘-endomaps X subsingletons-have-wconstant-β‘-endomaps X s x y = (f , ΞΊ) where f : x β‘ y β x β‘ y f p = s x y ΞΊ : (p q : x β‘ y) β f p β‘ f q ΞΊ p q = refl (s x y) subsingletons-are-sets : (X : π€ Μ ) β is-subsingleton X β is-set X subsingletons-are-sets X s = types-with-wconstant-β‘-endomaps-are-sets X (subsingletons-have-wconstant-β‘-endomaps X s) singletons-are-sets : (X : π€ Μ ) β is-singleton X β is-set X singletons-are-sets X = subsingletons-are-sets X β singletons-are-subsingletons X π-is-set : is-set π π-is-set = subsingletons-are-sets π π-is-subsingleton π-is-set : is-set π π-is-set = subsingletons-are-sets π π-is-subsingleton subsingletons-are-of-hlevel-1 : (X : π€ Μ ) β is-subsingleton X β X is-of-hlevel 1 subsingletons-are-of-hlevel-1 X = g where g : ((x y : X) β x β‘ y) β (x y : X) β is-singleton (x β‘ y) g t x y = t x y , subsingletons-are-sets X t x y (t x y) types-of-hlevel-1-are-subsingletons : (X : π€ Μ ) β X is-of-hlevel 1 β is-subsingleton X types-of-hlevel-1-are-subsingletons X = f where f : ((x y : X) β is-singleton (x β‘ y)) β (x y : X) β x β‘ y f s x y = center (x β‘ y) (s x y) sets-are-of-hlevel-2 : (X : π€ Μ ) β is-set X β X is-of-hlevel 2 sets-are-of-hlevel-2 X = g where g : ((x y : X) β is-subsingleton (x β‘ y)) β (x y : X) β (x β‘ y) is-of-hlevel 1 g t x y = subsingletons-are-of-hlevel-1 (x β‘ y) (t x y) types-of-hlevel-2-are-sets : (X : π€ Μ ) β X is-of-hlevel 2 β is-set X types-of-hlevel-2-are-sets X = f where f : ((x y : X) β (x β‘ y) is-of-hlevel 1) β (x y : X) β is-subsingleton (x β‘ y) f s x y = types-of-hlevel-1-are-subsingletons (x β‘ y) (s x y) hlevel-upper : (X : π€ Μ ) (n : β) β X is-of-hlevel n β X is-of-hlevel (succ n) hlevel-upper X zero = Ξ³ where Ξ³ : is-singleton X β (x y : X) β is-singleton (x β‘ y) Ξ³ h x y = p , subsingletons-are-sets X k x y p where k : is-subsingleton X k = singletons-are-subsingletons X h p : x β‘ y p = k x y hlevel-upper X (succ n) = Ξ» h x y β hlevel-upper (x β‘ y) n (h x y) _has-minimal-hlevel_ : π€ Μ β β β π€ Μ X has-minimal-hlevel 0 = X is-of-hlevel 0 X has-minimal-hlevel (succ n) = (X is-of-hlevel (succ n)) Γ Β¬(X is-of-hlevel n) _has-minimal-hlevel-β : π€ Μ β π€ Μ X has-minimal-hlevel-β = (n : β) β Β¬(X is-of-hlevel n) pointed-types-have-wconstant-endomap : {X : π€ Μ } β X β wconstant-endomap X pointed-types-have-wconstant-endomap x = ((Ξ» y β x) , (Ξ» y y' β refl x)) empty-types-have-wconstant-endomap : {X : π€ Μ } β is-empty X β wconstant-endomap X empty-types-have-wconstant-endomap e = (id , (Ξ» x x' β !π (x β‘ x') (e x))) decidable-has-wconstant-endomap : {X : π€ Μ } β decidable X β wconstant-endomap X decidable-has-wconstant-endomap (inl x) = pointed-types-have-wconstant-endomap x decidable-has-wconstant-endomap (inr e) = empty-types-have-wconstant-endomap e hedberg-lemma : {X : π€ Μ } β has-decidable-equality X β wconstant-β‘-endomaps X hedberg-lemma {π€} {X} d x y = decidable-has-wconstant-endomap (d x y) hedberg : {X : π€ Μ } β has-decidable-equality X β is-set X hedberg {π€} {X} d = types-with-wconstant-β‘-endomaps-are-sets X (hedberg-lemma d) β-is-set : is-set β β-is-set = hedberg β-has-decidable-equality π-is-set : is-set π π-is-set = hedberg π-has-decidable-equality has-section : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π€ β π₯ Μ has-section r = Ξ£ s κ (codomain r β domain r), r β s βΌ id _β_ : π€ Μ β π₯ Μ β π€ β π₯ Μ X β Y = Ξ£ r κ (Y β X), has-section r retraction : {X : π€ Μ } {Y : π₯ Μ } β X β Y β Y β X retraction (r , s , Ξ·) = r section : {X : π€ Μ } {Y : π₯ Μ } β X β Y β X β Y section (r , s , Ξ·) = s retract-equation : {X : π€ Μ } {Y : π₯ Μ } (Ο : X β Y) β retraction Ο β section Ο βΌ ππ X retract-equation (r , s , Ξ·) = Ξ· retraction-has-section : {X : π€ Μ } {Y : π₯ Μ } (Ο : X β Y) β has-section (retraction Ο) retraction-has-section (r , h) = h id-β : (X : π€ Μ ) β X β X id-β X = ππ X , ππ X , refl _ββ_ : {X : π€ Μ } {Y : π₯ Μ } {Z : π¦ Μ } β X β Y β Y β Z β X β Z (r , s , Ξ·) ββ (r' , s' , Ξ·') = (r β r' , s' β s , Ξ·'') where Ξ·'' = Ξ» x β r (r' (s' (s x))) β‘β¨ ap r (Ξ·' (s x)) β© r (s x) β‘β¨ Ξ· x β© x β _ββ¨_β©_ : (X : π€ Μ ) {Y : π₯ Μ } {Z : π¦ Μ } β X β Y β Y β Z β X β Z X ββ¨ Ο β© Ο = Ο ββ Ο _β : (X : π€ Μ ) β X β X X β = id-β X Ξ£-retract : {X : π€ Μ } {A : X β π₯ Μ } {B : X β π¦ Μ } β ((x : X) β A x β B x) β Ξ£ A β Ξ£ B Ξ£-retract {π€} {π₯} {π¦} {X} {A} {B} Ο = NatΞ£ r , NatΞ£ s , Ξ·' where r : (x : X) β B x β A x r x = retraction (Ο x) s : (x : X) β A x β B x s x = section (Ο x) Ξ· : (x : X) (a : A x) β r x (s x a) β‘ a Ξ· x = retract-equation (Ο x) Ξ·' : (Ο : Ξ£ A) β NatΞ£ r (NatΞ£ s Ο) β‘ Ο Ξ·' (x , a) = x , r x (s x a) β‘β¨ to-Ξ£-β‘' (Ξ· x a) β© x , a β transport-is-retraction : {X : π€ Μ } (A : X β π₯ Μ ) {x y : X} (p : x β‘ y) β transport A p β transport A (p β»ΒΉ) βΌ ππ (A y) transport-is-retraction A (refl x) = refl transport-is-section : {X : π€ Μ } (A : X β π₯ Μ ) {x y : X} (p : x β‘ y) β transport A (p β»ΒΉ) β transport A p βΌ ππ (A x) transport-is-section A (refl x) = refl Ξ£-reindexing-retract : {X : π€ Μ } {Y : π₯ Μ } {A : X β π¦ Μ } (r : Y β X) β has-section r β (Ξ£ x κ X , A x) β (Ξ£ y κ Y , A (r y)) Ξ£-reindexing-retract {π€} {π₯} {π¦} {X} {Y} {A} r (s , Ξ·) = Ξ³ , Ο , Ξ³Ο where Ξ³ : Ξ£ (A β r) β Ξ£ A Ξ³ (y , a) = (r y , a) Ο : Ξ£ A β Ξ£ (A β r) Ο (x , a) = (s x , transport A ((Ξ· x)β»ΒΉ) a) Ξ³Ο : (Ο : Ξ£ A) β Ξ³ (Ο Ο) β‘ Ο Ξ³Ο (x , a) = p where p : (r (s x) , transport A ((Ξ· x)β»ΒΉ) a) β‘ (x , a) p = to-Ξ£-β‘ (Ξ· x , transport-is-retraction A (Ξ· x) a) singleton-type : {X : π€ Μ } β X β π€ Μ singleton-type {π€} {X} x = Ξ£ y κ X , y β‘ x singleton-type-center : {X : π€ Μ } (x : X) β singleton-type x singleton-type-center x = (x , refl x) singleton-type-centered : {X : π€ Μ } (x : X) (Ο : singleton-type x) β singleton-type-center x β‘ Ο singleton-type-centered x (x , refl x) = refl (x , refl x) singleton-types-are-singletons : (X : π€ Μ ) (x : X) β is-singleton (singleton-type x) singleton-types-are-singletons X x = singleton-type-center x , singleton-type-centered x retract-of-singleton : {X : π€ Μ } {Y : π₯ Μ } β Y β X β is-singleton X β is-singleton Y retract-of-singleton (r , s , Ξ·) (c , Ο) = r c , Ξ³ where Ξ³ = Ξ» y β r c β‘β¨ ap r (Ο (s y)) β© r (s y) β‘β¨ Ξ· y β© y β singleton-type' : {X : π€ Μ } β X β π€ Μ singleton-type' {π€} {X} x = Ξ£ y κ X , x β‘ y singleton-type'-center : {X : π€ Μ } (x : X) β singleton-type' x singleton-type'-center x = (x , refl x) singleton-type'-centered : {X : π€ Μ } (x : X) (Ο : singleton-type' x) β singleton-type'-center x β‘ Ο singleton-type'-centered x (x , refl x) = refl (x , refl x) singleton-types'-are-singletons : (X : π€ Μ ) (x : X) β is-singleton (singleton-type' x) singleton-types'-are-singletons X x = singleton-type'-center x , singleton-type'-centered x invertible : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π€ β π₯ Μ invertible f = Ξ£ g κ (codomain f β domain f) , (g β f βΌ id) Γ (f β g βΌ id) fiber : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β Y β π€ β π₯ Μ fiber f y = Ξ£ x κ domain f , f x β‘ y fiber-point : {X : π€ Μ } {Y : π₯ Μ } {f : X β Y} {y : Y} β fiber f y β X fiber-point (x , p) = x fiber-identification : {X : π€ Μ } {Y : π₯ Μ } {f : X β Y} {y : Y} β (w : fiber f y) β f (fiber-point w) β‘ y fiber-identification (x , p) = p is-equiv : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π€ β π₯ Μ is-equiv f = (y : codomain f) β is-singleton (fiber f y) inverse : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-equiv f β (Y β X) inverse f e y = fiber-point (center (fiber f y) (e y)) inverses-are-sections : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) (e : is-equiv f) β f β inverse f e βΌ id inverses-are-sections f e y = fiber-identification (center (fiber f y) (e y)) inverse-centrality : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) (e : is-equiv f) (y : Y) (t : fiber f y) β (inverse f e y , inverses-are-sections f e y) β‘ t inverse-centrality f e y = centrality (fiber f y) (e y) inverses-are-retractions : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) (e : is-equiv f) β inverse f e β f βΌ id inverses-are-retractions f e x = ap fiber-point p where p : inverse f e (f x) , inverses-are-sections f e (f x) β‘ x , refl (f x) p = inverse-centrality f e (f x) (x , (refl (f x))) equivs-are-invertible : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-equiv f β invertible f equivs-are-invertible f e = inverse f e , inverses-are-retractions f e , inverses-are-sections f e invertibles-are-equivs : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β invertible f β is-equiv f invertibles-are-equivs {π€} {π₯} {X} {Y} f (g , Ξ· , Ξ΅) yβ = iii where i : (y : Y) β (f (g y) β‘ yβ) β (y β‘ yβ) i y = r , s , transport-is-section (_β‘ yβ) (Ξ΅ y) where s : f (g y) β‘ yβ β y β‘ yβ s = transport (_β‘ yβ) (Ξ΅ y) r : y β‘ yβ β f (g y) β‘ yβ r = transport (_β‘ yβ) ((Ξ΅ y)β»ΒΉ) ii : fiber f yβ β singleton-type yβ ii = (Ξ£ x κ X , f x β‘ yβ) ββ¨ Ξ£-reindexing-retract g (f , Ξ·) β© (Ξ£ y κ Y , f (g y) β‘ yβ) ββ¨ Ξ£-retract i β© (Ξ£ y κ Y , y β‘ yβ) β iii : is-singleton (fiber f yβ) iii = retract-of-singleton ii (singleton-types-are-singletons Y yβ) inverses-are-equivs : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) (e : is-equiv f) β is-equiv (inverse f e) inverses-are-equivs f e = invertibles-are-equivs (inverse f e) (f , inverses-are-sections f e , inverses-are-retractions f e) inversion-involutive : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) (e : is-equiv f) β inverse (inverse f e) (inverses-are-equivs f e) β‘ f inversion-involutive f e = refl f id-invertible : (X : π€ Μ ) β invertible (ππ X) id-invertible X = ππ X , refl , refl β-invertible : {X : π€ Μ } {Y : π₯ Μ } {Z : π¦ Μ } {f : X β Y} {f' : Y β Z} β invertible f' β invertible f β invertible (f' β f) β-invertible {π€} {π₯} {π¦} {X} {Y} {Z} {f} {f'} (g' , gf' , fg') (g , gf , fg) = g β g' , Ξ· , Ξ΅ where Ξ· = Ξ» x β g (g' (f' (f x))) β‘β¨ ap g (gf' (f x)) β© g (f x) β‘β¨ gf x β© x β Ξ΅ = Ξ» z β f' (f (g (g' z))) β‘β¨ ap f' (fg (g' z)) β© f' (g' z) β‘β¨ fg' z β© z β id-is-equiv : (X : π€ Μ ) β is-equiv (ππ X) id-is-equiv = singleton-types-are-singletons β-is-equiv : {X : π€ Μ } {Y : π₯ Μ } {Z : π¦ Μ } {f : X β Y} {g : Y β Z} β is-equiv g β is-equiv f β is-equiv (g β f) β-is-equiv {π€} {π₯} {π¦} {X} {Y} {Z} {f} {g} i j = Ξ³ where abstract Ξ³ : is-equiv (g β f) Ξ³ = invertibles-are-equivs (g β f) (β-invertible (equivs-are-invertible g i) (equivs-are-invertible f j)) inverse-of-β : {X : π€ Μ } {Y : π₯ Μ } {Z : π¦ Μ } (f : X β Y) (g : Y β Z) (i : is-equiv f) (j : is-equiv g) β inverse f i β inverse g j βΌ inverse (g β f) (β-is-equiv j i) inverse-of-β f g i j z = f' (g' z) β‘β¨ (ap (f' β g') (s z))β»ΒΉ β© f' (g' (g (f (h z)))) β‘β¨ ap f' (inverses-are-retractions g j (f (h z))) β© f' (f (h z)) β‘β¨ inverses-are-retractions f i (h z) β© h z β where f' = inverse f i g' = inverse g j h = inverse (g β f) (β-is-equiv j i) s : g β f β h βΌ id s = inverses-are-sections (g β f) (β-is-equiv j i) _β_ : π€ Μ β π₯ Μ β π€ β π₯ Μ X β Y = Ξ£ f κ (X β Y), is-equiv f Eqβfun β_β : {X : π€ Μ } {Y : π₯ Μ } β X β Y β X β Y Eqβfun (f , i) = f β_β = Eqβfun Eqβfun-is-equiv ββ-is-equiv : {X : π€ Μ } {Y : π₯ Μ } (e : X β Y) β is-equiv (β e β) Eqβfun-is-equiv (f , i) = i ββ-is-equiv = Eqβfun-is-equiv invertibility-gives-β : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β invertible f β X β Y invertibility-gives-β f i = f , invertibles-are-equivs f i Ξ£-induction-β : {X : π€ Μ } {Y : X β π₯ Μ } {A : Ξ£ Y β π¦ Μ } β ((x : X) (y : Y x) β A (x , y)) β ((z : Ξ£ Y) β A z) Ξ£-induction-β = invertibility-gives-β Ξ£-induction (curry , refl , refl) Ξ£-flip : {X : π€ Μ } {Y : π₯ Μ } {A : X β Y β π¦ Μ } β (Ξ£ x κ X , Ξ£ y κ Y , A x y) β (Ξ£ y κ Y , Ξ£ x κ X , A x y) Ξ£-flip = invertibility-gives-β (Ξ» (x , y , p) β (y , x , p)) ((Ξ» (y , x , p) β (x , y , p)) , refl , refl) Γ-comm : {X : π€ Μ } {Y : π₯ Μ } β (X Γ Y) β (Y Γ X) Γ-comm = invertibility-gives-β (Ξ» (x , y) β (y , x)) ((Ξ» (y , x) β (x , y)) , refl , refl) id-β : (X : π€ Μ ) β X β X id-β X = ππ X , id-is-equiv X _β_ : {X : π€ Μ } {Y : π₯ Μ } {Z : π¦ Μ } β X β Y β Y β Z β X β Z (f , d) β (f' , e) = f' β f , β-is-equiv e d β-sym : {X : π€ Μ } {Y : π₯ Μ } β X β Y β Y β X β-sym (f , e) = inverse f e , inverses-are-equivs f e _ββ¨_β©_ : (X : π€ Μ ) {Y : π₯ Μ } {Z : π¦ Μ } β X β Y β Y β Z β X β Z _ ββ¨ d β© e = d β e _β : (X : π€ Μ ) β X β X _β = id-β transport-is-equiv : {X : π€ Μ } (A : X β π₯ Μ ) {x y : X} (p : x β‘ y) β is-equiv (transport A p) transport-is-equiv A (refl x) = id-is-equiv (A x) Ξ£-β‘-β : {X : π€ Μ } {A : X β π₯ Μ } (Ο Ο : Ξ£ A) β (Ο β‘ Ο) β (Ξ£ p κ prβ Ο β‘ prβ Ο , transport A p (prβ Ο) β‘ prβ Ο) Ξ£-β‘-β {π€} {π₯} {X} {A} Ο Ο = invertibility-gives-β from-Ξ£-β‘ (to-Ξ£-β‘ , Ξ· , Ξ΅) where Ξ· : (q : Ο β‘ Ο) β to-Ξ£-β‘ (from-Ξ£-β‘ q) β‘ q Ξ· (refl Ο) = refl (refl Ο) Ξ΅ : (w : Ξ£ p κ prβ Ο β‘ prβ Ο , transport A p (prβ Ο) β‘ prβ Ο) β from-Ξ£-β‘ (to-Ξ£-β‘ w) β‘ w Ξ΅ (refl p , refl q) = refl (refl p , refl q) to-Γ-β‘ : {X : π€ Μ } {Y : π₯ Μ } {z t : X Γ Y} β (prβ z β‘ prβ t) Γ (prβ z β‘ prβ t) β z β‘ t to-Γ-β‘ (refl x , refl y) = refl (x , y) from-Γ-β‘ : {X : π€ Μ } {Y : π₯ Μ } {z t : X Γ Y} β z β‘ t β (prβ z β‘ prβ t) Γ (prβ z β‘ prβ t) from-Γ-β‘ {π€} {π₯} {X} {Y} (refl (x , y)) = (refl x , refl y) Γ-β‘-β : {X : π€ Μ } {Y : π₯ Μ } (z t : X Γ Y) β (z β‘ t) β (prβ z β‘ prβ t) Γ (prβ z β‘ prβ t) Γ-β‘-β {π€} {π₯} {X} {Y} z t = invertibility-gives-β from-Γ-β‘ (to-Γ-β‘ , Ξ· , Ξ΅) where Ξ· : (p : z β‘ t) β to-Γ-β‘ (from-Γ-β‘ p) β‘ p Ξ· (refl z) = refl (refl z) Ξ΅ : (q : (prβ z β‘ prβ t) Γ (prβ z β‘ prβ t)) β from-Γ-β‘ (to-Γ-β‘ q) β‘ q Ξ΅ (refl x , refl y) = refl (refl x , refl y) ap-prβ-to-Γ-β‘ : {X : π€ Μ } {Y : π₯ Μ } {z t : X Γ Y} β (pβ : prβ z β‘ prβ t) β (pβ : prβ z β‘ prβ t) β ap prβ (to-Γ-β‘ (pβ , pβ)) β‘ pβ ap-prβ-to-Γ-β‘ (refl x) (refl y) = refl (refl x) ap-prβ-to-Γ-β‘ : {X : π€ Μ } {Y : π₯ Μ } {z t : X Γ Y} β (pβ : prβ z β‘ prβ t) β (pβ : prβ z β‘ prβ t) β ap prβ (to-Γ-β‘ (pβ , pβ)) β‘ pβ ap-prβ-to-Γ-β‘ (refl x) (refl y) = refl (refl y) Ξ£-cong : {X : π€ Μ } {A : X β π₯ Μ } {B : X β π¦ Μ } β ((x : X) β A x β B x) β Ξ£ A β Ξ£ B Ξ£-cong {π€} {π₯} {π¦} {X} {A} {B} Ο = invertibility-gives-β (NatΞ£ f) (NatΞ£ g , NatΞ£-Ξ· , NatΞ£-Ξ΅) where f : (x : X) β A x β B x f x = β Ο x β g : (x : X) β B x β A x g x = inverse (f x) (ββ-is-equiv (Ο x)) Ξ· : (x : X) (a : A x) β g x (f x a) β‘ a Ξ· x = inverses-are-retractions (f x) (ββ-is-equiv (Ο x)) Ξ΅ : (x : X) (b : B x) β f x (g x b) β‘ b Ξ΅ x = inverses-are-sections (f x) (ββ-is-equiv (Ο x)) NatΞ£-Ξ· : (w : Ξ£ A) β NatΞ£ g (NatΞ£ f w) β‘ w NatΞ£-Ξ· (x , a) = x , g x (f x a) β‘β¨ to-Ξ£-β‘' (Ξ· x a) β© x , a β NatΞ£-Ξ΅ : (t : Ξ£ B) β NatΞ£ f (NatΞ£ g t) β‘ t NatΞ£-Ξ΅ (x , b) = x , f x (g x b) β‘β¨ to-Ξ£-β‘' (Ξ΅ x b) β© x , b β β-gives-β : {X : π€ Μ } {Y : π₯ Μ } β X β Y β X β Y β-gives-β (f , e) = (inverse f e , f , inverses-are-retractions f e) β-gives-β· : {X : π€ Μ } {Y : π₯ Μ } β X β Y β Y β X β-gives-β· (f , e) = (f , inverse f e , inverses-are-sections f e) equiv-to-singleton : {X : π€ Μ } {Y : π₯ Μ } β X β Y β is-singleton Y β is-singleton X equiv-to-singleton e = retract-of-singleton (β-gives-β e) IdβEq : (X Y : π€ Μ ) β X β‘ Y β X β Y IdβEq X X (refl X) = id-β X is-univalent : (π€ : Universe) β π€ βΊ Μ is-univalent π€ = (X Y : π€ Μ ) β is-equiv (IdβEq X Y) univalence-β : is-univalent π€ β (X Y : π€ Μ ) β (X β‘ Y) β (X β Y) univalence-β ua X Y = IdβEq X Y , ua X Y EqβId : is-univalent π€ β (X Y : π€ Μ ) β X β Y β X β‘ Y EqβId ua X Y = inverse (IdβEq X Y) (ua X Y) Idβfun : {X Y : π€ Μ } β X β‘ Y β X β Y Idβfun {π€} {X} {Y} p = β IdβEq X Y p β Idβfuns-agree : {X Y : π€ Μ } (p : X β‘ Y) β Idβfun p β‘ IdβFun p Idβfuns-agree (refl X) = refl (ππ X) swapβ : π β π swapβ β = β swapβ β = β swapβ-involutive : (n : π) β swapβ (swapβ n) β‘ n swapβ-involutive β = refl β swapβ-involutive β = refl β swapβ-is-equiv : is-equiv swapβ swapβ-is-equiv = invertibles-are-equivs swapβ (swapβ , swapβ-involutive , swapβ-involutive) module example-of-a-nonset (ua : is-univalent π€β) where eβ eβ : π β π eβ = id-β π eβ = swapβ , swapβ-is-equiv eβ-is-not-eβ : eβ β’ eβ eβ-is-not-eβ p = β-is-not-β r where q : id β‘ swapβ q = ap β_β p r : β β‘ β r = ap (Ξ» - β - β) q pβ pβ : π β‘ π pβ = EqβId ua π π eβ pβ = EqβId ua π π eβ pβ-is-not-pβ : pβ β’ pβ pβ-is-not-pβ q = eβ-is-not-eβ r where r = eβ β‘β¨ (inverses-are-sections (IdβEq π π) (ua π π) eβ)β»ΒΉ β© IdβEq π π pβ β‘β¨ ap (IdβEq π π) q β© IdβEq π π pβ β‘β¨ inverses-are-sections (IdβEq π π) (ua π π) eβ β© eβ β π€β-is-not-a-set : Β¬(is-set (π€β Μ )) π€β-is-not-a-set s = pβ-is-not-pβ q where q : pβ β‘ pβ q = s π π pβ pβ subsingleton-criterion : {X : π€ Μ } β (X β is-singleton X) β is-subsingleton X subsingleton-criterion' : {X : π€ Μ } β (X β is-subsingleton X) β is-subsingleton X retract-of-subsingleton : {X : π€ Μ } {Y : π₯ Μ } β Y β X β is-subsingleton X β is-subsingleton Y left-cancellable : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π€ β π₯ Μ left-cancellable f = {x x' : domain f} β f x β‘ f x' β x β‘ x' lc-maps-reflect-subsingletons : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β left-cancellable f β is-subsingleton Y β is-subsingleton X has-retraction : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π€ β π₯ Μ has-retraction s = Ξ£ r κ (codomain s β domain s), r β s βΌ id sections-are-lc : {X : π€ Μ } {A : π₯ Μ } (s : X β A) β has-retraction s β left-cancellable s equivs-have-retractions : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-equiv f β has-retraction f equivs-have-sections : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-equiv f β has-section f equivs-are-lc : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-equiv f β left-cancellable f equiv-to-subsingleton : {X : π€ Μ } {Y : π₯ Μ } β X β Y β is-subsingleton Y β is-subsingleton X comp-inverses : {X : π€ Μ } {Y : π₯ Μ } {Z : π¦ Μ } (f : X β Y) (g : Y β Z) (i : is-equiv f) (j : is-equiv g) (f' : Y β X) (g' : Z β Y) β f' βΌ inverse f i β g' βΌ inverse g j β f' β g' βΌ inverse (g β f) (β-is-equiv j i) equiv-to-set : {X : π€ Μ } {Y : π₯ Μ } β X β Y β is-set Y β is-set X sections-closed-under-βΌ : {X : π€ Μ } {Y : π₯ Μ } (f g : X β Y) β has-retraction f β g βΌ f β has-retraction g retractions-closed-under-βΌ : {X : π€ Μ } {Y : π₯ Μ } (f g : X β Y) β has-section f β g βΌ f β has-section g is-joyal-equiv : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π€ β π₯ Μ is-joyal-equiv f = has-section f Γ has-retraction f one-inverse : (X : π€ Μ ) (Y : π₯ Μ ) (f : X β Y) (r s : Y β X) β (r β f βΌ id) β (f β s βΌ id) β r βΌ s joyal-equivs-are-invertible : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-joyal-equiv f β invertible f joyal-equivs-are-equivs : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-joyal-equiv f β is-equiv f invertibles-are-joyal-equivs : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β invertible f β is-joyal-equiv f equivs-are-joyal-equivs : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-equiv f β is-joyal-equiv f equivs-closed-under-βΌ : {X : π€ Μ } {Y : π₯ Μ } {f g : X β Y} β is-equiv f β g βΌ f β is-equiv g equiv-to-singleton' : {X : π€ Μ } {Y : π₯ Μ } β X β Y β is-singleton X β is-singleton Y subtypes-of-sets-are-sets : {X : π€ Μ } {Y : π₯ Μ } (m : X β Y) β left-cancellable m β is-set Y β is-set X prβ-lc : {X : π€ Μ } {A : X β π₯ Μ } β ((x : X) β is-subsingleton (A x)) β left-cancellable (Ξ» (t : Ξ£ A) β prβ t) subsets-of-sets-are-sets : (X : π€ Μ ) (A : X β π₯ Μ ) β is-set X β ((x : X) β is-subsingleton (A x)) β is-set (Ξ£ x κ X , A x) to-subtype-β‘ : {X : π¦ Μ } {A : X β π₯ Μ } {x y : X} {a : A x} {b : A y} β ((x : X) β is-subsingleton (A x)) β x β‘ y β (x , a) β‘ (y , b) prβ-is-equiv : {X : π€ Μ } {A : X β π₯ Μ } β ((x : X) β is-singleton (A x)) β is-equiv (Ξ» (t : Ξ£ A) β prβ t) prβ-β : {X : π€ Μ } {A : X β π₯ Μ } β ((x : X) β is-singleton (A x)) β Ξ£ A β X prβ-β i = prβ , prβ-is-equiv i Ξ Ξ£-distr-β : {X : π€ Μ } {A : X β π₯ Μ } {P : (x : X) β A x β π¦ Μ } β (Ξ x κ X , Ξ£ a κ A x , P x a) β (Ξ£ f κ Ξ A , Ξ x κ X , P x (f x)) Ξ£-assoc : {X : π€ Μ } {Y : X β π₯ Μ } {Z : Ξ£ Y β π¦ Μ } β Ξ£ Z β (Ξ£ x κ X , Ξ£ y κ Y x , Z (x , y)) β»ΒΉ-β : {X : π€ Μ } (x y : X) β (x β‘ y) β (y β‘ x) singleton-types-β : {X : π€ Μ } (x : X) β singleton-type' x β singleton-type x singletons-β : {X : π€ Μ } {Y : π₯ Μ } β is-singleton X β is-singleton Y β X β Y maps-of-singletons-are-equivs : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-singleton X β is-singleton Y β is-equiv f logically-equivalent-subsingletons-are-equivalent : (X : π€ Μ ) (Y : π₯ Μ ) β is-subsingleton X β is-subsingleton Y β X β Y β X β Y singletons-are-equivalent : (X : π€ Μ ) (Y : π₯ Μ ) β is-singleton X β is-singleton Y β X β Y NatΞ£-fiber-equiv : {X : π€ Μ } (A : X β π₯ Μ ) (B : X β π¦ Μ ) (Ο : Nat A B) (x : X) (b : B x) β fiber (Ο x) b β fiber (NatΞ£ Ο) (x , b) NatΞ£-equiv-gives-fiberwise-equiv : {X : π€ Μ } {A : X β π₯ Μ } {B : X β π¦ Μ } (Ο : Nat A B) β is-equiv (NatΞ£ Ο) β ((x : X) β is-equiv (Ο x)) Ξ£-is-subsingleton : {X : π€ Μ } {A : X β π₯ Μ } β is-subsingleton X β ((x : X) β is-subsingleton (A x)) β is-subsingleton (Ξ£ A) Γ-is-singleton : {X : π€ Μ } {Y : π₯ Μ } β is-singleton X β is-singleton Y β is-singleton (X Γ Y) Γ-is-subsingleton : {X : π€ Μ } {Y : π₯ Μ } β is-subsingleton X β is-subsingleton Y β is-subsingleton (X Γ Y) Γ-is-subsingleton' : {X : π€ Μ } {Y : π₯ Μ } β ((Y β is-subsingleton X) Γ (X β is-subsingleton Y)) β is-subsingleton (X Γ Y) Γ-is-subsingleton'-back : {X : π€ Μ } {Y : π₯ Μ } β is-subsingleton (X Γ Y) β (Y β is-subsingleton X) Γ (X β is-subsingleton Y) apβ : {X : π€ Μ } {Y : π₯ Μ } {Z : π¦ Μ } (f : X β Y β Z) {x x' : X} {y y' : Y} β x β‘ x' β y β‘ y' β f x y β‘ f x' y' subsingleton-criterion = sol where sol : {X : π€ Μ } β (X β is-singleton X) β is-subsingleton X sol f x = singletons-are-subsingletons (domain f) (f x) x subsingleton-criterion' = sol where sol : {X : π€ Μ } β (X β is-subsingleton X) β is-subsingleton X sol f x y = f x x y retract-of-subsingleton = sol where sol : {X : π€ Μ } {Y : π₯ Μ } β Y β X β is-subsingleton X β is-subsingleton Y sol (r , s , Ξ·) i = subsingleton-criterion (Ξ» x β retract-of-singleton (r , s , Ξ·) (pointed-subsingletons-are-singletons (codomain s) (s x) i)) lc-maps-reflect-subsingletons = sol where sol : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β left-cancellable f β is-subsingleton Y β is-subsingleton X sol f l s x x' = l (s (f x) (f x')) sections-are-lc = sol where sol : {X : π€ Μ } {A : π₯ Μ } (s : X β A) β has-retraction s β left-cancellable s sol s (r , Ξ΅) {x} {y} p = x β‘β¨ (Ξ΅ x)β»ΒΉ β© r (s x) β‘β¨ ap r p β© r (s y) β‘β¨ Ξ΅ y β© y β equivs-have-retractions = sol where sol : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-equiv f β has-retraction f sol f e = (inverse f e , inverses-are-retractions f e) equivs-have-sections = sol where sol : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-equiv f β has-section f sol f e = (inverse f e , inverses-are-sections f e) equivs-are-lc = sol where sol : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-equiv f β left-cancellable f sol f e = sections-are-lc f (equivs-have-retractions f e) equiv-to-subsingleton = sol where sol : {X : π€ Μ } {Y : π₯ Μ } β X β Y β is-subsingleton Y β is-subsingleton X sol (f , i) = lc-maps-reflect-subsingletons f (equivs-are-lc f i) comp-inverses = sol where sol : {X : π€ Μ } {Y : π₯ Μ } {Z : π¦ Μ } (f : X β Y) (g : Y β Z) (i : is-equiv f) (j : is-equiv g) (f' : Y β X) (g' : Z β Y) β f' βΌ inverse f i β g' βΌ inverse g j β f' β g' βΌ inverse (g β f) (β-is-equiv j i) sol f g i j f' g' h k z = f' (g' z) β‘β¨ h (g' z) β© inverse f i (g' z) β‘β¨ ap (inverse f i) (k z) β© inverse f i (inverse g j z) β‘β¨ inverse-of-β f g i j z β© inverse (g β f) (β-is-equiv j i) z β equiv-to-set = sol where sol : {X : π€ Μ } {Y : π₯ Μ } β X β Y β is-set Y β is-set X sol e = subtypes-of-sets-are-sets β e β (equivs-are-lc β e β (ββ-is-equiv e)) sections-closed-under-βΌ = sol where sol : {X : π€ Μ } {Y : π₯ Μ } (f g : X β Y) β has-retraction f β g βΌ f β has-retraction g sol f g (r , rf) h = (r , Ξ» x β r (g x) β‘β¨ ap r (h x) β© r (f x) β‘β¨ rf x β© x β) retractions-closed-under-βΌ = sol where sol : {X : π€ Μ } {Y : π₯ Μ } (f g : X β Y) β has-section f β g βΌ f β has-section g sol f g (s , fs) h = (s , Ξ» y β g (s y) β‘β¨ h (s y) β© f (s y) β‘β¨ fs y β© y β) one-inverse = sol where sol : (X : π€ Μ ) (Y : π₯ Μ ) (f : X β Y) (r s : Y β X) β (r β f βΌ id) β (f β s βΌ id) β r βΌ s sol X Y f r s h k y = r y β‘β¨ ap r ((k y)β»ΒΉ) β© r (f (s y)) β‘β¨ h (s y) β© s y β joyal-equivs-are-invertible = sol where sol : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-joyal-equiv f β invertible f sol f ((s , Ξ΅) , (r , Ξ·)) = (s , sf , Ξ΅) where sf = Ξ» (x : domain f) β s(f x) β‘β¨ (Ξ· (s (f x)))β»ΒΉ β© r(f(s(f x))) β‘β¨ ap r (Ξ΅ (f x)) β© r(f x) β‘β¨ Ξ· x β© x β joyal-equivs-are-equivs = sol where sol : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-joyal-equiv f β is-equiv f sol f j = invertibles-are-equivs f (joyal-equivs-are-invertible f j) invertibles-are-joyal-equivs = sol where sol : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β invertible f β is-joyal-equiv f sol f (g , Ξ· , Ξ΅) = ((g , Ξ΅) , (g , Ξ·)) equivs-are-joyal-equivs = sol where sol : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-equiv f β is-joyal-equiv f sol f e = invertibles-are-joyal-equivs f (equivs-are-invertible f e) equivs-closed-under-βΌ = sol where sol : {X : π€ Μ } {Y : π₯ Μ } {f g : X β Y} β is-equiv f β g βΌ f β is-equiv g sol {π€} {π₯} {X} {Y} {f} {g} e h = joyal-equivs-are-equivs g (retractions-closed-under-βΌ f g (equivs-have-sections f e) h , sections-closed-under-βΌ f g (equivs-have-retractions f e) h) equiv-to-singleton' = sol where sol : {X : π€ Μ } {Y : π₯ Μ } β X β Y β is-singleton X β is-singleton Y sol e = retract-of-singleton (β-gives-β· e) subtypes-of-sets-are-sets = sol where sol : {X : π€ Μ } {Y : π₯ Μ } (m : X β Y) β left-cancellable m β is-set Y β is-set X sol {π€} {π₯} {X} m i h = types-with-wconstant-β‘-endomaps-are-sets X c where f : (x x' : X) β x β‘ x' β x β‘ x' f x x' r = i (ap m r) ΞΊ : (x x' : X) (r s : x β‘ x') β f x x' r β‘ f x x' s ΞΊ x x' r s = ap i (h (m x) (m x') (ap m r) (ap m s)) c : wconstant-β‘-endomaps X c x x' = f x x' , ΞΊ x x' prβ-lc = sol where sol : {X : π€ Μ } {A : X β π₯ Μ } β ((x : X) β is-subsingleton (A x)) β left-cancellable (Ξ» (t : Ξ£ A) β prβ t) sol i p = to-Ξ£-β‘ (p , i _ _ _) subsets-of-sets-are-sets = sol where sol : (X : π€ Μ ) (A : X β π₯ Μ ) β is-set X β ((x : X) β is-subsingleton (A x)) β is-set (Ξ£ x κ X , A x) sol X A h p = subtypes-of-sets-are-sets prβ (prβ-lc p) h to-subtype-β‘ = sol where sol : {X : π€ Μ } {A : X β π₯ Μ } {x y : X} {a : A x} {b : A y} β ((x : X) β is-subsingleton (A x)) β x β‘ y β (x , a) β‘ (y , b) sol {π€} {π₯} {X} {A} {x} {y} {a} {b} s p = to-Ξ£-β‘ (p , s y (transport A p a) b) prβ-is-equiv = sol where sol : {X : π€ Μ } {A : X β π₯ Μ } β ((x : X) β is-singleton (A x)) β is-equiv (Ξ» (t : Ξ£ A) β prβ t) sol {π€} {π₯} {X} {A} s = invertibles-are-equivs prβ (g , Ξ· , Ξ΅) where g : X β Ξ£ A g x = x , prβ(s x) Ξ΅ : (x : X) β prβ (g x) β‘ x Ξ΅ x = refl (prβ (g x)) Ξ· : (Ο : Ξ£ A) β g (prβ Ο) β‘ Ο Ξ· (x , a) = to-subtype-β‘ (Ξ» x β singletons-are-subsingletons (A x) (s x)) (Ξ΅ x) Ξ Ξ£-distr-β = sol where sol : {X : π€ Μ } {A : X β π₯ Μ } {P : (x : X) β A x β π¦ Μ } β (Ξ x κ X , Ξ£ a κ A x , P x a) β (Ξ£ f κ Ξ A , Ξ x κ X , P x (f x)) sol {π€} {π₯} {π¦} {X} {A} {P} = invertibility-gives-β Ο (Ξ³ , Ξ· , Ξ΅) where Ο : (Ξ x κ X , Ξ£ a κ A x , P x a) β Ξ£ f κ Ξ A , Ξ x κ X , P x (f x) Ο g = ((Ξ» x β prβ (g x)) , Ξ» x β prβ (g x)) Ξ³ : (Ξ£ f κ Ξ A , Ξ x κ X , P x (f x)) β Ξ x κ X , Ξ£ a κ A x , P x a Ξ³ (f , Ο) x = f x , Ο x Ξ· : Ξ³ β Ο βΌ id Ξ· = refl Ξ΅ : Ο β Ξ³ βΌ id Ξ΅ = refl Ξ£-assoc = sol where sol : {X : π€ Μ } {Y : X β π₯ Μ } {Z : Ξ£ Y β π¦ Μ } β Ξ£ Z β (Ξ£ x κ X , Ξ£ y κ Y x , Z (x , y)) sol {π€} {π₯} {π¦} {X} {Y} {Z} = invertibility-gives-β f (g , refl , refl) where f : Ξ£ Z β Ξ£ x κ X , Ξ£ y κ Y x , Z (x , y) f ((x , y) , z) = (x , (y , z)) g : (Ξ£ x κ X , Ξ£ y κ Y x , Z (x , y)) β Ξ£ Z g (x , (y , z)) = ((x , y) , z) β»ΒΉ-is-equiv : {X : π€ Μ } (x y : X) β is-equiv (Ξ» (p : x β‘ y) β p β»ΒΉ) β»ΒΉ-is-equiv x y = invertibles-are-equivs _β»ΒΉ (_β»ΒΉ , β»ΒΉ-involutive , β»ΒΉ-involutive) β»ΒΉ-β = sol where sol : {X : π€ Μ } (x y : X) β (x β‘ y) β (y β‘ x) sol x y = (_β»ΒΉ , β»ΒΉ-is-equiv x y) singleton-types-β = sol where sol : {X : π€ Μ } (x : X) β singleton-type' x β singleton-type x sol x = Ξ£-cong (Ξ» y β β»ΒΉ-β x y) singletons-β = sol where sol : {X : π€ Μ } {Y : π₯ Μ } β is-singleton X β is-singleton Y β X β Y sol {π€} {π₯} {X} {Y} i j = invertibility-gives-β f (g , Ξ· , Ξ΅) where f : X β Y f x = center Y j g : Y β X g y = center X i Ξ· : (x : X) β g (f x) β‘ x Ξ· = centrality X i Ξ΅ : (y : Y) β f (g y) β‘ y Ξ΅ = centrality Y j maps-of-singletons-are-equivs = sol where sol : {X : π€ Μ } {Y : π₯ Μ } (f : X β Y) β is-singleton X β is-singleton Y β is-equiv f sol {π€} {π₯} {X} {Y} f i j = invertibles-are-equivs f (g , Ξ· , Ξ΅) where g : Y β X g y = center X i Ξ· : (x : X) β g (f x) β‘ x Ξ· = centrality X i Ξ΅ : (y : Y) β f (g y) β‘ y Ξ΅ y = singletons-are-subsingletons Y j (f (g y)) y logically-equivalent-subsingletons-are-equivalent = sol where sol : (X : π€ Μ ) (Y : π₯ Μ ) β is-subsingleton X β is-subsingleton Y β X β Y β X β Y sol X Y i j (f , g) = invertibility-gives-β f (g , (Ξ» x β i (g (f x)) x) , (Ξ» y β j (f (g y)) y)) singletons-are-equivalent = sol where sol : (X : π€ Μ ) (Y : π₯ Μ ) β is-singleton X β is-singleton Y β X β Y sol X Y i j = invertibility-gives-β (Ξ» _ β center Y j) ((Ξ» _ β center X i) , centrality X i , centrality Y j) NatΞ£-fiber-equiv = sol where sol : {X : π€ Μ } (A : X β π₯ Μ ) (B : X β π¦ Μ ) (Ο : Nat A B) (x : X) (b : B x) β fiber (Ο x) b β fiber (NatΞ£ Ο) (x , b) sol A B Ο x b = invertibility-gives-β f (g , Ξ΅ , Ξ·) where f : fiber (Ο x) b β fiber (NatΞ£ Ο) (x , b) f (a , refl _) = ((x , a) , refl (x , Ο x a)) g : fiber (NatΞ£ Ο) (x , b) β fiber (Ο x) b g ((x , a) , refl _) = (a , refl (Ο x a)) Ξ΅ : (w : fiber (Ο x) b) β g (f w) β‘ w Ξ΅ (a , refl _) = refl (a , refl (Ο x a)) Ξ· : (t : fiber (NatΞ£ Ο) (x , b)) β f (g t) β‘ t Ξ· ((x , a) , refl _) = refl ((x , a) , refl (NatΞ£ Ο (x , a))) NatΞ£-equiv-gives-fiberwise-equiv = sol where sol : {X : π€ Μ } {A : X β π₯ Μ } {B : X β π¦ Μ } (Ο : Nat A B) β is-equiv (NatΞ£ Ο) β ((x : X) β is-equiv (Ο x)) sol {π€} {π₯} {π¦} {X} {A} {B} Ο e x b = Ξ³ where d : fiber (Ο x) b β fiber (NatΞ£ Ο) (x , b) d = NatΞ£-fiber-equiv A B Ο x b s : is-singleton (fiber (NatΞ£ Ο) (x , b)) s = e (x , b) Ξ³ : is-singleton (fiber (Ο x) b) Ξ³ = equiv-to-singleton d s Ξ£-is-subsingleton = sol where sol : {X : π€ Μ } {A : X β π₯ Μ } β is-subsingleton X β ((x : X) β is-subsingleton (A x)) β is-subsingleton (Ξ£ A) sol i j (x , _) (y , _) = to-subtype-β‘ j (i x y) Γ-is-singleton = sol where sol : {X : π€ Μ } {Y : π₯ Μ } β is-singleton X β is-singleton Y β is-singleton (X Γ Y) sol (x , Ο) (y , Ξ³) = (x , y) , Ξ΄ where Ξ΄ : β z β (x , y) β‘ z Ξ΄ (x' , y' ) = to-Γ-β‘ (Ο x' , Ξ³ y') Γ-is-subsingleton = sol where sol : {X : π€ Μ } {Y : π₯ Μ } β is-subsingleton X β is-subsingleton Y β is-subsingleton (X Γ Y) sol i j = Ξ£-is-subsingleton i (Ξ» _ β j) Γ-is-subsingleton' = sol where sol : {X : π€ Μ } {Y : π₯ Μ } β ((Y β is-subsingleton X) Γ (X β is-subsingleton Y)) β is-subsingleton (X Γ Y) sol {π€} {π₯} {X} {Y} (i , j) = k where k : is-subsingleton (X Γ Y) k (x , y) (x' , y') = to-Γ-β‘ (i y x x' , j x y y') Γ-is-subsingleton'-back = sol where sol : {X : π€ Μ } {Y : π₯ Μ } β is-subsingleton (X Γ Y) β (Y β is-subsingleton X) Γ (X β is-subsingleton Y) sol {π€} {π₯} {X} {Y} k = i , j where i : Y β is-subsingleton X i y x x' = ap prβ (k (x , y) (x' , y)) j : X β is-subsingleton Y j x y y' = ap prβ (k (x , y) (x , y')) apβ = sol where sol : {X : π€ Μ } {Y : π₯ Μ } {Z : π¦ Μ } (f : X β Y β Z) {x x' : X} {y y' : Y} β x β‘ x' β y β‘ y' β f x y β‘ f x' y' sol f (refl x) (refl y) = refl (f x y) equiv-singleton-lemma : {X : π€ Μ } {A : X β π₯ Μ } (x : X) (f : (y : X) β x β‘ y β A y) β ((y : X) β is-equiv (f y)) β is-singleton (Ξ£ A) equiv-singleton-lemma {π€} {π₯} {X} {A} x f i = Ξ³ where abstract e : (y : X) β (x β‘ y) β A y e y = (f y , i y) d : singleton-type' x β Ξ£ A d = Ξ£-cong e Ξ³ : is-singleton (Ξ£ A) Ξ³ = equiv-to-singleton (β-sym d) (singleton-types'-are-singletons X x) singleton-equiv-lemma : {X : π€ Μ } {A : X β π₯ Μ } (x : X) (f : (y : X) β x β‘ y β A y) β is-singleton (Ξ£ A) β (y : X) β is-equiv (f y) singleton-equiv-lemma {π€} {π₯} {X} {A} x f i = Ξ³ where abstract g : singleton-type' x β Ξ£ A g = NatΞ£ f e : is-equiv g e = maps-of-singletons-are-equivs g (singleton-types'-are-singletons X x) i Ξ³ : (y : X) β is-equiv (f y) Ξ³ = NatΞ£-equiv-gives-fiberwise-equiv f e univalenceβ : is-univalent π€ β (X : π€ Μ ) β is-singleton (Ξ£ Y κ π€ Μ , X β Y) univalenceβ ua X = equiv-singleton-lemma X (IdβEq X) (ua X) βunivalence : ((X : π€ Μ ) β is-singleton (Ξ£ Y κ π€ Μ , X β Y)) β is-univalent π€ βunivalence i X = singleton-equiv-lemma X (IdβEq X) (i X) univalenceβ : is-univalent π€ β (X : π€ Μ ) β is-subsingleton (Ξ£ Y κ π€ Μ , X β Y) univalenceβ ua X = singletons-are-subsingletons (Ξ£ (X β_)) (univalenceβ ua X) βunivalence : ((X : π€ Μ ) β is-subsingleton (Ξ£ Y κ π€ Μ , X β Y)) β is-univalent π€ βunivalence i = βunivalence (Ξ» X β pointed-subsingletons-are-singletons (Ξ£ (X β_)) (X , id-β X) (i X)) πΎ-β : is-univalent π€ β (X : π€ Μ ) (A : (Ξ£ Y κ π€ Μ , X β Y) β π₯ Μ ) β A (X , id-β X) β (Y : π€ Μ ) (e : X β Y) β A (Y , e) πΎ-β {π€} ua X A a Y e = transport A p a where t : Ξ£ Y κ π€ Μ , X β Y t = (X , id-β X) p : t β‘ (Y , e) p = univalenceβ {π€} ua X t (Y , e) πΎ-β-equation : (ua : is-univalent π€) β (X : π€ Μ ) (A : (Ξ£ Y κ π€ Μ , X β Y) β π₯ Μ ) (a : A (X , id-β X)) β πΎ-β ua X A a X (id-β X) β‘ a πΎ-β-equation {π€} {π₯} ua X A a = πΎ-β ua X A a X (id-β X) β‘β¨ refl _ β© transport A p a β‘β¨ ap (Ξ» - β transport A - a) q β© transport A (refl t) a β‘β¨ refl _ β© a β where t : Ξ£ Y κ π€ Μ , X β Y t = (X , id-β X) p : t β‘ t p = univalenceβ {π€} ua X t t q : p β‘ refl t q = subsingletons-are-sets (Ξ£ Y κ π€ Μ , X β Y) (univalenceβ {π€} ua X) t t p (refl t) β-β : is-univalent π€ β (X : π€ Μ ) (A : (Y : π€ Μ ) β X β Y β π₯ Μ ) β A X (id-β X) β (Y : π€ Μ ) (e : X β Y) β A Y e β-β ua X A = πΎ-β ua X (Ξ£-induction A) β-β-equation : (ua : is-univalent π€) β (X : π€ Μ ) (A : (Y : π€ Μ ) β X β Y β π₯ Μ ) (a : A X (id-β X)) β β-β ua X A a X (