f : A β B, P : A β U, Q : B β U, g : (a : A) β P(a) β Q(f(a)) β’ Ο(a, u) β‘ (f(a), ga), Ο : (Ξ£a : A P(a)) β (Ξ£b : B Q(b)), is-connectedn(ga) β is-connectedn(f) β is-connectedn(Ο).
Lemma
P, Q : A β U, f : (a : A) β (P(a) β Q(a)) β’ total(f) : Ξ£a : A P(a) β Ξ£a : A Q(a), is-connectedn(total(f)).
Lemma
f : A β B β’ is-connectedn(f), ||A||n β ||B||n.
Orthogonal factorisation
n-truncated
f : A β B β’ is-truncatedn(f) β‘ (b : B) β is-truncatedn(fibf(b)). is-truncated-2(f) = is-equivalence(f). is-truncatedn(A) = is-truncatedn(f : A β 1).
Lemma
n-image
f : A β B β’ imn(f) β‘ Ξ£b : b ||fibf(b)||n.
Lemma
f : A β B, f~ : A β imn(f) β’ is-connectedn(f~).
Lemma
H : h1 g1 βΌ h2 g2, b : B β’ is-connectedn(g1) Γ is-connectedn(g2) Γ is-truncatedn(h1) Γ is-truncatedn(h2) β E(H, b) : fibh1(b) β fibh2(b), E-(H, a) : E(H, h1(g1(a)))(g1(a), reflh1(g1(a))) = (g2(a), H(a)-1).
Theorem
f : A β B β’ factn(f) β‘ Ξ£X : U Ξ£g : A β X Ξ£h : X β B(h g βΌ f) Γ is-connectedn(g) is-truncatedn(h), is-truncated-2(factn(f)),(imn(f), f~, pr1, ΞΈ, Ο, Ο) : factn(f),
Theorem
e : A β B, m : C β D, Ο : (B β C) β Ξ£h : A β C Ξ£k : B β D(m h βΌ k e) β’ is-connectedn(e) Γ is-truncatedn(m) β is-equivalence(Ο).
Lemma
fibf(b) β fibg(h(b)).
Reflective subuniverse
P : U β (-1)-type, A : U β’ βA, Ξ·A : A β βA(βA β B) β (A β B), f β¦ f Ξ·A. UP β‘ {A : U | P(A)}.
Modality
β : U β U, Ξ·Aβ : A β βA, indβ : ((a : A) β β(B(Ξ·Aβ(a)))) β Ξ z : βA β(B(z)), indβ(f)(Ξ·Aβ(a)) = f(a), f : (a : A) β β(B(Ξ·Aβ(a))), z, z' : βA, Ξ·z = z'β : (z = z') β β(z = z').