Homotopy Finiteness
Table of Contents
- 1. Homotopy Finiteness
- 1.1. Packages imports
- 1.2. Homotopy finite
- 1.3.
is-htpy-finiteis a proposition - 1.4. Empty is πn finite
- 1.5. Any contractible type is πn finite (in particular, Unit is πn finite)
- 1.6. Homotopy finiteness is closed downwards
- 1.7. Closure under equivalence
- 1.8. Closure under coproduct
- 1.9. Finite type is πn finite
- 1.10. Equivalence of set-truncated function type
- 1.11. Closure under Π-types
- 1.12. Closure under Σ-types, base case
- 1.13. Closure under Σ-types
- 1.14. Unlock
1 Homotopy Finiteness
module HomotopyFiniteness where
This file is a formalization of the proof presented by Rijke in his CIRM talk about the finiteness of structures up to isomorphism.
1.1 Packages imports
The imported packages can be accessed via the following links:
import Lib.IsFinite import Lib.SetTrunc
1.2 Homotopy finite
A type A is said nth-homotopy finite if it has finitely many connected components and all its homotopy groups πi(A, x) are finite, for every i ≤ n and x : A.
is-htpy-finite : Nat → U → U = split zero → λA. is-finite (Set-trunc A) suc k → λA. is-finite (Set-trunc A) * ( (x y : A) → is-htpy-finite k (Path A x y))
1.3 is-htpy-finite is a proposition
As propositions are closed under products, we can show by induction that is-htpy-finite n is a proposition.
is-htpy-finite/is-prop : (k : Nat) → (A : U) → is-prop (is-htpy-finite k A) = split zero → λA. is-finite/is-prop (Set-trunc A) suc k → λA. is-prop/prod ( is-finite (Set-trunc A)) ( (x y : A) → is-htpy-finite k (Path A x y)) ( is-finite/is-prop (Set-trunc A)) ( is-prop/pi-2 A ( λ_. A) ( λx y. is-htpy-finite k (Path A x y)) ( λx y. is-htpy-finite/is-prop k (Path A x y))) is-htpy-finite/Prop (k : Nat) (A : U) : UU-Prop = ( is-htpy-finite k A, is-htpy-finite/is-prop k A)
1.4 Empty is πn finite
The empty type is πn finite.
Empty/is-htpy-finite : (n : Nat) → is-htpy-finite n Empty = split zero → is-finite/closed-Equiv' Empty ( Set-trunc Empty) ( Set/Equiv-Set-trunc ( Prop/Set (Empty/Prop))) ( Empty/is-finite) suc n → ( Empty/is-htpy-finite zero, λx y. ex-falso (is-htpy-finite n (Path Empty x y)) x)
1.5 Any contractible type is πn finite (in particular, Unit is πn finite)
is-contr/is-htpy-finite : (n : Nat) → (X : U) → is-contr X → is-htpy-finite n X = split zero → λX H. is-contr/is-finite ( Set-trunc X) ( Set-trunc/closed-contr X H) suc n → λX H. ( is-contr/is-htpy-finite zero X H, λx y. is-contr/is-htpy-finite n ( Path X x y) ( is-contr/closed-upwards X H x y)) Unit/is-htpy-finite (n : Nat) : is-htpy-finite n Unit = is-contr/is-htpy-finite n Unit ( Unit/is-contr)
1.6 Homotopy finiteness is closed downwards
If a type A is πn-finite, then its set truncation is finite.
is-htpy-finite/is-finite-Set-trunc (A : U) : (n : Nat) → is-htpy-finite n A → is-finite (Set-trunc A) = split zero → id (is-finite (Set-trunc A)) suc n → λH. H.1
If is-πn+1-finite A, then is-πn-finite A.
is-htpy-finite/pred : (n : Nat) → (A : U) → is-htpy-finite (suc n) A → is-htpy-finite n A = split zero → λA H. H.1 suc n → λA H. ( H.1, λx y. is-htpy-finite/pred n ( Path A x y) (H.2 x y))
If a type A is πn+1 finite, then it is π1 finite.
is-htpy-finite/is-htpy-one-finite (A : U) : (n : Nat) → is-htpy-finite (suc n) A → is-htpy-finite one-Nat A = split zero → id (is-htpy-finite one-Nat A) suc n → λHA. is-htpy-finite/is-htpy-one-finite A n ( is-htpy-finite/pred (suc n) A HA)
1.7 Closure under equivalence
If A and B are equivalent, then whenever one of them is πn finite, the other one is also πn finite.
is-htpy-finite/closed-Equiv/aux : (n : Nat) → (A B : U) → Equiv A B → is-htpy-finite n B → is-htpy-finite n A = split zero → λA B e. is-finite/closed-Equiv ( Set-trunc A) ( Set-trunc B) ( Set-trunc/Equiv A B e) suc n → λA B e is-htpy-finite-B. ( is-finite/closed-Equiv ( Set-trunc A) ( Set-trunc B) ( Set-trunc/Equiv A B e) ( is-htpy-finite-B.1), λx y. is-htpy-finite/closed-Equiv/aux n ( Path A x y) ( Path B (Equiv/map A B e x) (Equiv/map A B e y)) ( Equiv/Equiv-id A B e x y) ( is-htpy-finite-B.2 ( Equiv/map A B e x) ( Equiv/map A B e y))) is-htpy-finite/closed-Equiv (A B : U) (e : Equiv A B) (n : Nat) (is-htpy-finite-B : is-htpy-finite n B) : is-htpy-finite n A = is-htpy-finite/closed-Equiv/aux n A B e is-htpy-finite-B is-htpy-finite/closed-Equiv' (A B : U) (e : Equiv A B) (n : Nat) (is-htpy-finite-A : is-htpy-finite n A) : is-htpy-finite n B = is-htpy-finite/closed-Equiv B A (Equiv/sym A B e) n is-htpy-finite-A
1.8 Closure under coproduct
If A and B are both πn finite, then the coproduct A + B is also πn finite.
is-htpy-finite/closed-Coprod/inl (A B : U) (n : Nat) (is-htpy-finite-A : is-htpy-finite (suc n) A) (is-htpy-finite-B : is-htpy-finite (suc n) B) (x : A) : (v : Coprod A B) → is-htpy-finite n (Path (Coprod A B) (inl x) v) = split inl a → is-htpy-finite/closed-Equiv ( Path (Coprod A B) (inl x) (inl a)) ( Path A x a) ( Coprod/Eq/Equiv A B (inl x) (inl a)) n ( is-htpy-finite-A.2 x a) inr y → is-htpy-finite/closed-Equiv ( Path (Coprod A B) (inl x) (inr y)) ( Empty) ( Coprod/Eq/Equiv A B (inl x) (inr y)) n ( Empty/is-htpy-finite n) is-htpy-finite/closed-Coprod/inr (A B : U) (n : Nat) (is-htpy-finite-A : is-htpy-finite (suc n) A) (is-htpy-finite-B : is-htpy-finite (suc n) B) (y : B) : (v : Coprod A B) → is-htpy-finite n (Path (Coprod A B) (inr y) v) = split inl a → is-htpy-finite/closed-Equiv ( Path (Coprod A B) (inr y) (inl a)) ( Empty) ( Coprod/Eq/Equiv A B (inr y) (inl a)) n ( Empty/is-htpy-finite n) inr b → is-htpy-finite/closed-Equiv ( Path (Coprod A B) (inr y) (inr b)) ( Path B y b) ( Coprod/Eq/Equiv A B (inr y) (inr b)) n ( is-htpy-finite-B.2 y b) is-htpy-finite/closed-Coprod' (A B : U) (n : Nat) (is-htpy-finite-A : is-htpy-finite (suc n) A) (is-htpy-finite-B : is-htpy-finite (suc n) B) : (u : Coprod A B) (v : Coprod A B) → is-htpy-finite n (Path (Coprod A B) u v) = split inl x → is-htpy-finite/closed-Coprod/inl A B n is-htpy-finite-A is-htpy-finite-B x inr y → is-htpy-finite/closed-Coprod/inr A B n is-htpy-finite-A is-htpy-finite-B y is-htpy-finite/closed-Coprod : (n : Nat) → (A B : U) (is-htpy-finite-A : is-htpy-finite n A) (is-htpy-finite-B : is-htpy-finite n B) → is-htpy-finite n (Coprod A B) = split zero → λA B HA HB. is-finite/closed-Equiv ( Set-trunc (Coprod A B)) ( Coprod (Set-trunc A) (Set-trunc B)) ( Set-trunc/closed-Coprod' A B) ( is-finite/closed-Coprod ( Set-trunc A) ( Set-trunc B) ( HA) ( HB)) suc n → λA B HA HB. ( is-htpy-finite/closed-Coprod zero A B ( is-htpy-finite/is-finite-Set-trunc A (suc n) HA) ( is-htpy-finite/is-finite-Set-trunc B (suc n) HB), is-htpy-finite/closed-Coprod' A B n HA HB)
On the other hand, if A + B is πn finite, then A and B are also πn finite.
is-htpy-finite/Coprod/left (A B : U) : (n : Nat) (is-htpy-finite-copr : is-htpy-finite n (Coprod A B)) → is-htpy-finite n A = split zero → λH. is-finite/closed-Coprod-left ( Set-trunc A) ( Set-trunc B) ( is-finite/closed-Equiv ( Coprod (Set-trunc A) (Set-trunc B)) ( Set-trunc (Coprod A B)) ( Set-trunc/closed-Coprod A B) ( H)) suc n → λH. ( is-htpy-finite/Coprod/left A B zero ( is-htpy-finite/is-finite-Set-trunc ( Coprod A B) ( suc n) H), λx y. is-htpy-finite/closed-Equiv ( Path A x y) ( Path (Coprod A B) (inl x) (inl y)) ( Coprod/Eq/Equiv' A B (inl x) (inl y)) n ( H.2 (inl x) (inl y))) is-htpy-finite/Coprod/right (A B : U) : (n : Nat) (is-htpy-finite-copr : is-htpy-finite n (Coprod A B)) → is-htpy-finite n B = split zero → λH. is-finite/closed-Coprod-right ( Set-trunc A) ( Set-trunc B) ( is-finite/closed-Equiv ( Coprod (Set-trunc A) (Set-trunc B)) ( Set-trunc (Coprod A B)) ( Set-trunc/closed-Coprod A B) ( H)) suc n → λH. ( is-htpy-finite/Coprod/right A B zero ( is-htpy-finite/is-finite-Set-trunc ( Coprod A B) ( suc n) H), λx y. is-htpy-finite/closed-Equiv ( Path B x y) ( Path (Coprod A B) (inr x) (inr y)) ( Coprod/Eq/Equiv' A B (inr x) (inr y)) n ( H.2 (inr x) (inr y)))
1.9 Finite type is πn finite
First, we show that Fin k is πn finite for all k, n.
Fin/is-htpy-finite (n : Nat) : (k : Nat) → is-htpy-finite n (Fin k) = split zero → Empty/is-htpy-finite n suc k → is-htpy-finite/closed-Coprod n ( Fin k) Unit ( Fin/is-htpy-finite n k) ( Unit/is-htpy-finite n)
That is, everything that has a count is πn finite for all n.
count/is-htpy-finite (X : U) (H : count X) (n : Nat) : is-htpy-finite n X = let k : Nat = number-of-elements X H e : Equiv (Fin k) X = count/Equiv X H in is-htpy-finite/closed-Equiv' ( Fin k) X e n ( Fin/is-htpy-finite n k)
As being πn finite is a proposition, it generalizes if X is finite.
is-finite/is-htpy-finite (X : U) (H : is-finite X) (n : Nat) : is-htpy-finite n X = rec-Prop-trunc ( count X) ( is-htpy-finite/Prop n X) ( λc. count/is-htpy-finite X c n) H
1.10 Equivalence of set-truncated function type
We show that if A is finite, then there is an equivalence between Πx: A||B x||0 and ||Πx: A B x||0. First, we show this result for A = Fin k by induction on k.
- if k = 0, then both types are contractible. By the 3-for-2 property of contractibility, they are equivalent.
- if k > 0, there is the following chain of equivalences: Πx: Fin (k + 1)||B x||0 ≅ Πx: Fin k||B (inl x)||0 × ||B (inr star)||0 ≅ ||Πx: Fin k B (inl x)||0 × ||B (inr star)||0 ≅ ||Πx: Fin (k + 1)B x||0
Fin/Equiv-Pi-Set-trunc : (k : Nat) → (B : Fin k → U) → Equiv ((x : Fin k) → Set-trunc (B x)) (Set-trunc ((x : Fin k) → B x)) = split zero → λB. is-contr/Equiv ( (x : Fin zero) → Set-trunc (B x)) ( Set-trunc ((x : Fin zero) → B x)) ( Empty/universal-dependent-property ( Fin zero) ( λx. Set-trunc (B x)) ( Equiv/refl (Fin zero))) ( Set-trunc/closed-contr ( (x : Fin zero) → B x) ( Empty/universal-dependent-property ( Fin zero) B ( Equiv/refl (Fin zero)))) suc k → λB. Equiv/comp five-Nat ( (x : Fin (suc k)) → Set-trunc (B x)) ( ((x : Fin k) → Set-trunc (B (inl x))) * ((x : Unit) → Set-trunc (B (inr x)))) ( Coprod/dependent-universal-property ( Fin k) Unit (λx. Set-trunc (B x))) ( ((x : Fin k) → Set-trunc (B (inl x))) * (Set-trunc (B (inr star)))) ( Equiv/prod' ( (x : Fin k) → Set-trunc (B (inl x))) ( (x : Unit) → Set-trunc (B (inr x))) ( Set-trunc (B (inr star))) ( Equiv/pi-Unit ( λx. Set-trunc (B (inr x))))) ( (Set-trunc ((x : Fin k) → B (inl x))) * (Set-trunc (B (inr star)))) ( Equiv/prod ( (x : Fin k) → Set-trunc (B (inl x))) ( Set-trunc ((x : Fin k) → B (inl x))) ( Set-trunc (B (inr star))) ( Fin/Equiv-Pi-Set-trunc k ( λx. B (inl x)))) ( Set-trunc (((x : Fin k) → B (inl x)) * (B (inr star)))) ( Set-trunc/closed-Prod ( (x : Fin k) → B (inl x)) ( B (inr star))) ( Set-trunc (((x : Fin k) → B (inl x)) * ((x : Unit) → B (inr x)))) ( Set-trunc/Equiv ( ((x : Fin k) → B (inl x)) * (B (inr star))) ( ((x : Fin k) → B (inl x)) * ((x : Unit) → B (inr x))) ( Equiv/prod' ( (x : Fin k) → B (inl x)) ( B (inr star)) ( (x : Unit) → B (inr x)) ( Equiv/sym ( (x : Unit) → B (inr x)) ( B (inr star)) ( Equiv/pi-Unit (λx. B (inr x)))))) ( Set-trunc ((x : Fin (suc k)) → B x)) ( Set-trunc/Equiv ( ((x : Fin k) → B (inl x)) * ((x : Unit) → B (inr x))) ( (x : Fin (suc k)) → B x) ( Equiv/sym ( (x : Fin (suc k)) → B x) ( ((x : Fin k) → B (inl x)) * ((x : Unit) → B (inr x))) ( Coprod/dependent-universal-property ( Fin k) Unit B)))
This result cannot be directly generalized for a finite type (as Equiv is not a proposition). It can be, however, generalized for any type that has a counting.
Path/Pi (A : U) (B : A → U) (f : A → A) (H : (x : A) → Path A (f x) x) : Path U ((x : A) → B (f x)) ((x : A) → B x) = λi. (x : A) → B (H x i) count/Equiv-Pi-Set-trunc (A : U) (B : A → U) (c : count A) : Equiv ((x : A) → Set-trunc (B x)) (Set-trunc ((x : A) → B x)) = let k : Nat = number-of-elements A c e : Equiv (Fin k) A = count/Equiv A c f : (Fin k) → A = Equiv/map (Fin k) A e g : A → (Fin k) = Equiv/inv-map (Fin k) A e in Equiv/comp three-Nat ( (x : A) → Set-trunc (B x)) ( (x : Fin k) → Set-trunc (B (f x))) ( Equiv/dependent ( Fin k) A ( λx. Set-trunc (B x)) e) ( Set-trunc ((x : Fin k) → B (f x))) ( Fin/Equiv-Pi-Set-trunc k ( λx. B (f x))) ( Set-trunc ((x : A) → B (f (g x)))) ( Set-trunc/Equiv ( (x : Fin k) → B (f x)) ( (x : A) → B (f (g x))) ( Equiv/dependent A ( Fin k) ( λx. B (f x)) ( Equiv/sym ( Fin k) A e))) ( Set-trunc ((x : A) → B x)) ( Set-trunc/Equiv ( (x : A) → B (f (g x))) ( (x : A) → B x) ( path-to-equiv ( (x : A) → B (f (g x))) ( (x : A) → B x) ( Path/Pi A B (λx. f (g x)) (Equiv/inv-right-htpy (Fin k) A e))))
1.11 Closure under Π-types
In this section, we show that if B is a family of πn finite types over a finite type A, then the product Πx: AB(x) is also πn-finite.
We proceed by induction over n.
- If
nis zero, then by is-finite/Π, is-finite (Πx: A||B x||0). Moreover, Πx: A||B x||0 is equivalent to ||Πx: AB(x)||0 and as is-finite is closed by equivalences, the result follows. - If
n > 0, then it suffices to show that f ∼ g is πn finite by function extensionality and πn-finiteness closure under equivalence. It then suffices to use the induction hypothesis.
is-htpy-finite/closed-Pi : (n : Nat) → (A : U) → (B : A → U) → is-finite A → ((x : A) → is-htpy-finite n (B x)) → is-htpy-finite n ((x : A) → B x) = split zero → λA B HA HB. (rec-Prop-trunc ( count A) ( is-finite/Prop (Set-trunc ((x : A) → B x))) ( λc. is-finite/closed-Equiv' ( (x : A) → Set-trunc (B x)) ( Set-trunc ((x : A) → B x)) ( count/Equiv-Pi-Set-trunc A B c) ( is-finite/Pi A ( λx. Set-trunc (B x)) HA HB)) HA) suc n → λA B HA HB. let IH : is-htpy-finite n ((x : A) → B x) = is-htpy-finite/closed-Pi n A B HA (λx. is-htpy-finite/pred n (B x) (HB x)) in ( is-htpy-finite/is-finite-Set-trunc ((x : A) → B x) n IH, λf g. is-htpy-finite/closed-Equiv ( Path ((x : A) → B x) f g) ( Htpy A B f g) ( htpy-eq/Equiv A B f g) n ( is-htpy-finite/closed-Pi n A ( λx. Path (B x) (f x) (g x)) HA ( λx. (HB x).2 (f x) (g x))))
1.12 Closure under Σ-types, base case
In this section, we show that if B is a family of π0-finite types over a connected, π1-finite type A, then Σx: AB(x) is also π0-finite, i.e., that || Σx: AB(x) ||0 is finite.
1.12.1 Preliminaries
As A is connected, and we show a property, we assume that a : A. Then, the fiber inclusion function (recall that it is defined as λb. (a, b) for b : B(a)) is surjective. As set truncation preserves surjectivity, || Σx: A B(x) ||0 is finite whenever it has decidable equality.
is-htpy-finite/closed-Sg/base' (A : U) (B : A → U) (H : is-conn A) (is-htpy-finite-A : is-htpy-finite one-Nat A) (is-htpy-finite-B : (x : A) → is-htpy-finite zero (B x)) (has-dec-eq-Σ : has-decidable-equality (Set-trunc (Σ A B))) : is-htpy-finite zero (Σ A B) = rec-Prop-trunc A ( is-htpy-finite/Prop zero (Σ A B)) ( λa. has-decidable-equality/is-finite-codomain ( Set-trunc (B a)) ( Set-trunc (Σ A B)) ( is-htpy-finite-B a) ( has-dec-eq-Sg) ( Set-trunc-map ( B a) ( Σ A B) ( fiber-inclusion A B a)) ( Set-trunc-map/is-surj ( B a) ( Σ A B) ( fiber-inclusion A B a) ( is-connected/fiber-inclusion-is-surj A B H a))) ( is-conn/is-inhabited A H)
We thus focus on showing, under the same hypotheses, that || Σx: AB(x) ||0 has decidable equality. In fact, recall that decidability is closed under equivalence. Thus, let |(x, y)|0 and |(x', y')|0 of type || Σx: AB(x) ||0. We have the following equivalences:
- |(x, y)|0 = |(x', y')|0 ≅ || (x, y) = (x', y') ||
as A is connected, let a : A. Moreover, still by connectivity, |a|0 = |x|0 and |a|0 = |x'|0, that is, we have two mere equalities || a = x || and || a = x' ||. Hence, || (x, y) = (x', y') || ≅ || (a, y) = (a, y') ||.
is-htpy-finite/closed-Sg/dec-mere-eq' (A : U) (B : A → U) (is-conn-A : is-conn A) (a : A) (h : (y y' : B a) → is-decidable (mere-eq (Σ A B) (a, y) (a, y'))) (y : B a) (x' : A) (y' : B x') : is-decidable (mere-eq (Σ A B) (a, y) (x', y')) = rec-Prop-trunc ( Path A a x') ( is-decidable/Prop ( mere-eq (Σ A B) (a, y) (x', y')) ( Prop-trunc/is-prop (Path (Σ A B) (a, y) (x', y')))) ( λp. J A a ( λz _. (b : B z) → is-decidable (mere-eq (Σ A B) (a, y) (z, b))) ( h y) x' p y') ( Set-trunc/is-effective/map A a x' ( is-contr/all-elements-equal ( Set-trunc A) ( is-conn-A) ( Set-trunc/unit a) ( Set-trunc/unit x'))) is-htpy-finite/closed-Sg/dec-mere-eq (A : U) (B : A → U) (is-conn-A : is-conn A) (a : A) (h : (y y' : B a) → is-decidable (mere-eq (Σ A B) (a, y) (a, y'))) (x : A) (y : B x) (x' : A) (y' : B x') : is-decidable (mere-eq (Σ A B) (x, y) (x', y')) = rec-Prop-trunc ( Path A a x) ( is-decidable/Prop ( mere-eq (Σ A B) (x, y) (x', y')) ( Prop-trunc/is-prop (Path (Σ A B) (x, y) (x', y')))) ( λp. J A a ( λz _. (b : B z) → is-decidable (mere-eq (Σ A B) (z, b) (x', y'))) ( λb. is-htpy-finite/closed-Sg/dec-mere-eq' A B is-conn-A a h b x' y') x p y) ( Set-trunc/is-effective/map A a x ( is-contr/all-elements-equal ( Set-trunc A) ( is-conn-A) ( Set-trunc/unit a) ( Set-trunc/unit x))) is-htpy-finite/closed-Sg/dec-mere-eq-dec-eq' (A : U) (B : A → U) (is-conn-A : is-conn A) (a : A) (h : (y y' : B a) → is-decidable (mere-eq (Σ A B) (a, y) (a, y'))) (x : A) (y : B x) (x' : A) (y' : B x') : is-decidable (Path (Set-trunc (Σ A B)) (Set-trunc/unit (x, y)) (Set-trunc/unit (x', y'))) = is-decidable/closed-Equiv ( Path (Set-trunc (Σ A B)) (Set-trunc/unit (x, y)) (Set-trunc/unit (x', y'))) ( mere-eq (Σ A B) (x, y) (x', y')) ( Set-trunc/is-effective (Σ A B) (x, y) (x', y')) ( is-htpy-finite/closed-Sg/dec-mere-eq A B is-conn-A a h x y x' y') is-htpy-finite/closed-Sg/dec-mere-eq-dec-eq (A : U) (B : A → U) (is-conn-A : is-conn A) (a : A) (h : (y y' : B a) → is-decidable (mere-eq (Σ A B) (a, y) (a, y'))) (t u : Set-trunc (Σ A B)) : is-decidable (Path (Set-trunc (Σ A B)) t u) = ind-Set-trunc/Prop ( Σ A B) ( λt'. is-decidable/Prop ( Path (Set-trunc (Σ A B)) t' u) ( Set-trunc/is-set (Σ A B) t' u)) ( λt'. ind-Set-trunc/Prop ( Σ A B) ( λu'. is-decidable/Prop ( Path (Set-trunc (Σ A B)) (Set-trunc/unit t') u') ( Set-trunc/is-set (Σ A B) (Set-trunc/unit t') u')) ( λu'. is-htpy-finite/closed-Sg/dec-mere-eq-dec-eq' A B is-conn-A a h t'.1 t'.2 u'.1 u'.2) u) t
Thus, it suffices to show that || (a, y) = (a, y') || is decidable. But again, we have that || (a, y) = (a, y') || ≅ || Σp: a = a ||trB(p, y) = y'|| ||. The right-hand side of the underlying type is decidable by assumption (by π0 finiteness of (B a)), but not the left-hand side. But as || trB(p, y) = y' || is a proposition, by the induction principle of the set truncation, we get a corresponding type taking || a = a ||0 as parameter. We can then show that both things are finite, and thus that || Σp: a = a ||trB(p, y) = y'|| || is finite; that is, it is decidable.
1.12.2 Definition of the type
We start by defining the goal type by the induction principle of set truncation.
is-htpy-finite/closed-Sg/type (A : U) (B : A → U) (a : A) (y y' : B a) : Set-trunc (Path A a a) → UU-Prop = rec-Set-trunc ( Path A a a) ( UU-Prop/Set) ( λp. mere-eq/Prop (B a) (tr A a a p B y) y')
1.12.3 Equivalence
We continue by showing the equivalence between || (a, y) = (a, y') || and || Σp: || a = a ||0 P(p) ||. As these two types are propositions, we only need a back-and-forth map between them. The forward map is immediate by the computation rule of the induction principle of set truncation.
lock Prop-trunc/is-prop UU-Prop/is-set is-htpy-finite/closed-Sg/Equiv/map (A : U) (B : A → U) (a : A) (y y' : B a) : (p : Prop-trunc (Path (Σ A B) (a, y) (a, y'))) → (Prop-trunc (Σ (Set-trunc (Path A a a)) (λq. Prop/type (is-htpy-finite/closed-Sg/type A B a y y' q)))) = rec-Prop-trunc ( Path (Σ A B) (a, y) (a, y')) ( Prop-trunc/Prop (Σ (Set-trunc (Path A a a)) (λq. Prop/type (is-htpy-finite/closed-Sg/type A B a y y' q)))) ( λp. let t : SgPathO A B (a, y) (a, y') = PathSg→SgPathO A B (a, y) (a, y') p in Prop-trunc/unit ( Set-trunc/unit t.1, Prop-trunc/unit t.2))
The backward map is also straightforward as we prove a property; that is, we can get a path in A.
is-htpy-finite/closed-Sg/Equiv/inv-map (A : U) (B : A → U) (a : A) (y y' : B a) : (Prop-trunc (Σ (Set-trunc (Path A a a)) (λq. Prop/type (is-htpy-finite/closed-Sg/type A B a y y' q)))) → Prop-trunc (Path (Σ A B) (a, y) (a, y')) = rec-Prop-trunc ( Σ (Set-trunc (Path A a a)) (λq. Prop/type (is-htpy-finite/closed-Sg/type A B a y y' q))) ( Prop-trunc/Prop (Path (Σ A B) (a, y) (a, y'))) ( λt. ind-Set-trunc/Prop ( Path A a a) ( λp. Prop/Pi ( Prop/type (is-htpy-finite/closed-Sg/type A B a y y' p)) ( λ_. Prop-trunc/Prop (Path (Σ A B) (a, y) (a, y')))) ( λp. rec-Prop-trunc ( Path (B a) (tr A a a p B y) y') ( Prop-trunc/Prop (Path (Σ A B) (a, y) (a, y'))) ( λq'. Prop-trunc/unit ( SgPathO→PathΣ A B ( a, y) ( a, y') ( p, q')))) t.1 t.2)
And we have the equivalence:
is-htpy-finite/closed-Sg/Equiv (A : U) (B : A → U) (a : A) (y y' : B a) : Equiv (Prop-trunc (Path (Σ A B) (a, y) (a, y'))) (Prop-trunc (Σ (Set-trunc (Path A a a)) (λq. Prop/type (is-htpy-finite/closed-Sg/type A B a y y' q)))) = Prop/Equiv ( Prop-trunc/Prop (Path (Σ A B) (a, y) (a, y'))) ( Prop-trunc/Prop (Σ (Set-trunc (Path A a a)) (λq. Prop/type (is-htpy-finite/closed-Sg/type A B a y y' q)))) ( is-htpy-finite/closed-Sg/Equiv/map A B a y y') ( is-htpy-finite/closed-Sg/Equiv/inv-map A B a y y')
1.12.4 Decidable equality of || Σx : AB(x) ||0
We start by showing that || Σw : || a = a ||0P(w) || is decidable. To show this, it suffices to show that the type underlying the propositional truncation is finite. It is the case as, by hypothesis, A is π1 finite and || trB(p, y) = y' || ≅ |trB(p, y)|0 = |y'|0 which is decidable as || B(a) ||0 is finite.
is-htpy-finite/closed-Sg/subtype-decidable (A : U) (B : A → U) (is-finite-A : is-htpy-finite one-Nat A) (is-finite-B : (x : A) → is-htpy-finite zero (B x)) (a : A) (y y' : B a) : is-decidable (Prop-trunc (Σ (Set-trunc (Path A a a)) (λq. Prop/type (is-htpy-finite/closed-Sg/type A B a y y' q)))) = is-finite/is-decidable-Prop-trunc ( Σ (Set-trunc (Path A a a)) (λq. Prop/type (is-htpy-finite/closed-Sg/type A B a y y' q))) ( is-finite/closed-Sg ( Set-trunc (Path A a a)) ( λq. Prop/type (is-htpy-finite/closed-Sg/type A B a y y' q)) ( is-finite-A.2 a a) ( ind-Set-trunc/Prop ( Path A a a) ( λq. is-finite/Prop (Prop/type (is-htpy-finite/closed-Sg/type A B a y y' q))) ( λw. is-finite/closed-Equiv ( Prop-trunc (Path (B a) (tr A a a w B y) y')) ( Path (Set-trunc (B a)) (Set-trunc/unit (tr A a a w B y)) (Set-trunc/unit y')) ( Set-trunc/is-effective' (B a) (tr A a a w B y) y') ( is-decidable/is-finite ( Path (Set-trunc (B a)) (Set-trunc/unit (tr A a a w B y)) (Set-trunc/unit y')) ( Set-trunc/is-set (B a) (Set-trunc/unit (tr A a a w B y)) (Set-trunc/unit y')) ( is-finite/has-decidable-equality ( Set-trunc (B a)) ( is-finite-B a) ( Set-trunc/unit (tr A a a w B y)) ( Set-trunc/unit y'))))))
Hence, under the same hypotheses, || (a, y) = (a, y') || is also decidable.
is-htpy-finite/closed-Sg/mere-eq-decidable (A : U) (B : A → U) (is-finite-A : is-htpy-finite one-Nat A) (is-finite-B : (x : A) → is-htpy-finite zero (B x)) (a : A) (y y' : B a) : is-decidable (mere-eq (Σ A B) (a, y) (a, y')) = is-decidable/closed-Equiv ( mere-eq (Σ A B) (a, y) (a, y')) ( Prop-trunc (Σ (Set-trunc (Path A a a)) (λq. Prop/type (is-htpy-finite/closed-Sg/type A B a y y' q)))) ( is-htpy-finite/closed-Sg/Equiv A B a y y') ( is-htpy-finite/closed-Sg/subtype-decidable A B is-finite-A is-finite-B a y y')
Adding the connectedness hypothesis, we show that || Σx: AB(x) ||0 has a decidable equality.
is-htpy-finite/closed-Sg/has-decidable-equality (A : U) (B : A → U) (is-finite-A : is-htpy-finite one-Nat A) (is-conn-A : is-conn A) (is-finite-B : (x : A) → is-htpy-finite zero (B x)) (t u : Set-trunc (Σ A B)) : is-decidable (Path (Set-trunc (Σ A B)) t u) = rec-Prop-trunc A ( is-decidable/Prop ( Path (Set-trunc (Σ A B)) t u) ( Set/is-set (Set-trunc/Set (Σ A B)) t u)) ( λa. is-htpy-finite/closed-Sg/dec-mere-eq-dec-eq A B is-conn-A a ( is-htpy-finite/closed-Sg/mere-eq-decidable A B is-finite-A is-finite-B a) t u) ( is-conn/is-inhabited A is-conn-A)
1.12.5 Closed under Σ-types (base case)
Finally, we show the base case of the homotopy finite being closed under Σ-types.
is-htpy-finite/closed-Sg/base (A : U) (B : A → U) (H : is-conn A) (is-htpy-finite-A : is-htpy-finite one-Nat A) (is-htpy-finite-B : (x : A) → is-htpy-finite zero (B x)) : is-htpy-finite zero (Σ A B) = is-htpy-finite/closed-Sg/base' A B H is-htpy-finite-A is-htpy-finite-B ( is-htpy-finite/closed-Sg/has-decidable-equality A B is-htpy-finite-A H is-htpy-finite-B)
1.13 Closure under Σ-types
In this section, we generalize the previous result and forget the connectedness assumption. To do so, we do a double induction; on n, and then on the number of connected components.
As the finiteness hypothesis resides in the set truncation of A, we have a map f : Fin (k + 1) → A (see Lib/SetTrunc.org). We start by showing that A is equivalent to the coproduct of im (f ˆ inl) and im (f ˆ inr). We prove a more general version of this lemma, using whatever types. First, we exhibit the back-and-forth maps.
1.13.1 Maps and right homotopy
codomain-is-coproduct/map (A1 A2 B : U) (f : Coprod A1 A2 → B) : Coprod (im A1 B (λx. f (inl x))) (im A2 B (λy. f (inr y))) → B = split inl t → t.1 inr t → t.1 codomain-is-coproduct/inv-map' (A1 A2 B : U) (f : Coprod A1 A2 → B) (e : Equiv (Coprod A1 A2) (Set-trunc B)) (H : Htpy' (Coprod A1 A2) (Set-trunc B) (λx. Set-trunc/unit (f x)) (Equiv/map (Coprod A1 A2) (Set-trunc B) e)) (y : B) : (x : Coprod A1 A2) → Path (Coprod A1 A2) (Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit y)) x → Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy'. f (inr y'))) = split inl x → λp. inl ( y, Prop-trunc/closed-Sg/map A1 ( λz. Path B y (f (inl z))) ( Prop-trunc/unit ( x, Set-trunc/is-effective/map B y ( f (inl x)) ( comp-n ( Set-trunc B) three-Nat ( Set-trunc/unit y) ( Equiv/map (Coprod A1 A2) (Set-trunc B) e ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit y))) ( inv ( Set-trunc B) ( Equiv/map (Coprod A1 A2) (Set-trunc B) e ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit y))) ( Set-trunc/unit y) ( Equiv/inv-right-htpy ( Coprod A1 A2) ( Set-trunc B) e ( Set-trunc/unit y))) ( Equiv/map (Coprod A1 A2) (Set-trunc B) e (inl x)) ( ap ( Coprod A1 A2) (Set-trunc B) (Equiv/map (Coprod A1 A2) (Set-trunc B) e) ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit y)) (inl x) p) ( Set-trunc/unit (f (inl x))) ( inv ( Set-trunc B) ( Set-trunc/unit (f (inl x))) ( Equiv/map (Coprod A1 A2) (Set-trunc B) e (inl x)) ( H (inl x))))))) inr x → λp. inr ( y, Prop-trunc/closed-Sg/map A2 ( λz. Path B y (f (inr z))) ( Prop-trunc/unit ( x, Set-trunc/is-effective/map B y ( f (inr x)) ( comp-n ( Set-trunc B) three-Nat ( Set-trunc/unit y) ( Equiv/map (Coprod A1 A2) (Set-trunc B) e ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit y))) ( inv ( Set-trunc B) ( Equiv/map (Coprod A1 A2) (Set-trunc B) e ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit y))) ( Set-trunc/unit y) ( Equiv/inv-right-htpy ( Coprod A1 A2) ( Set-trunc B) e ( Set-trunc/unit y))) ( Equiv/map (Coprod A1 A2) (Set-trunc B) e (inr x)) ( ap ( Coprod A1 A2) (Set-trunc B) (Equiv/map (Coprod A1 A2) (Set-trunc B) e) ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit y)) (inr x) p) ( Set-trunc/unit (f (inr x))) ( inv ( Set-trunc B) ( Set-trunc/unit (f (inr x))) ( Equiv/map (Coprod A1 A2) (Set-trunc B) e (inr x)) ( H (inr x))))))) codomain-is-coproduct/inv-map (A1 A2 B : U) (f : Coprod A1 A2 → B) (e : Equiv (Coprod A1 A2) (Set-trunc B)) (H : Htpy' (Coprod A1 A2) (Set-trunc B) (λx. Set-trunc/unit (f x)) (Equiv/map (Coprod A1 A2) (Set-trunc B) e)) (y : B) : Coprod (im A1 B (λx. f (inl x))) (im A2 B (λy'. f (inr y'))) = codomain-is-coproduct/inv-map' A1 A2 B f e H y ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit y)) ( refl ( Coprod A1 A2) ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit y)))
As the second element of images are propositions, the homotopies are (should be) trivial.
codomain-is-coproduct/right-htpy' (A1 A2 B : U) (f : Coprod A1 A2 → B) (e : Equiv (Coprod A1 A2) (Set-trunc B)) (H : Htpy' (Coprod A1 A2) (Set-trunc B) (λx. Set-trunc/unit (f x)) (Equiv/map (Coprod A1 A2) (Set-trunc B) e)) (y : B) : (x : Coprod A1 A2) → (p : Path (Coprod A1 A2) (Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit y)) x) → Path B (codomain-is-coproduct/map A1 A2 B f ( codomain-is-coproduct/inv-map' A1 A2 B f e H y x p)) y = split inl _ → λ_. refl B y inr _ → λ_. refl B y codomain-is-coproduct/right-htpy (A1 A2 B : U) (f : Coprod A1 A2 → B) (e : Equiv (Coprod A1 A2) (Set-trunc B)) (H : Htpy' (Coprod A1 A2) (Set-trunc B) (λx. Set-trunc/unit (f x)) (Equiv/map (Coprod A1 A2) (Set-trunc B) e)) (y : B) : Path B (codomain-is-coproduct/map A1 A2 B f (codomain-is-coproduct/inv-map A1 A2 B f e H y)) y = codomain-is-coproduct/right-htpy' A1 A2 B f e H y ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit y)) ( refl ( Coprod A1 A2) ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit y)))
1.13.2 Left homotopy
The left homotopy is very bothersome but nothing of note happens inside.
lock Set-trunc/is-effective/map codomain-is-coproduct/left-htpy/inl' (A1 A2 B : U) (f : Coprod A1 A2 → B) (e : Equiv (Coprod A1 A2) (Set-trunc B)) (H : Htpy' (Coprod A1 A2) (Set-trunc B) (λx. Set-trunc/unit (f x)) (Equiv/map (Coprod A1 A2) (Set-trunc B) e)) (t : im A1 B (λx. f (inl x))) (a : A1) (p : Path (Coprod A1 A2) (Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1)) (inl a)) : (u : Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy. f (inr y)))) → Path (Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy. f (inr y)))) u (codomain-is-coproduct/inv-map' A1 A2 B f e H t.1 (inl a) p) → Path (Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy. f (inr y)))) u (inl t) = split inl u → λq. Coprod/Eq/map ( im A1 B (λx. f (inl x))) ( im A2 B (λy. f (inr y))) ( inl u) ( inl t) ( SgPath-prop B ( λz. Prop-trunc (Fib A1 B (λx. f (inl x)) z)) ( λz. Prop-trunc/is-prop (Fib A1 B (λx. f (inl x)) z)) u t ( λi. (( Coprod/Eq/eq-map ( im A1 B (λx. f (inl x))) ( im A2 B (λy. f (inr y))) ( inl u) ( codomain-is-coproduct/inv-map' A1 A2 B f e H t.1 (inl a) p) q) i).1)) inr v → λq. ex-falso ( Path (Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy. f (inr y)))) (inr v) (inl t)) ( Coprod/Eq/eq-map ( im A1 B (λx. f (inl x))) ( im A2 B (λy. f (inr y))) ( inr v) ( codomain-is-coproduct/inv-map' A1 A2 B f e H t.1 (inl a) p) q) codomain-is-coproduct/left-htpy/inl (A1 A2 B : U) (f : Coprod A1 A2 → B) (e : Equiv (Coprod A1 A2) (Set-trunc B)) (H : Htpy' (Coprod A1 A2) (Set-trunc B) (λx. Set-trunc/unit (f x)) (Equiv/map (Coprod A1 A2) (Set-trunc B) e)) (t : im A1 B (λx. f (inl x))) : (x : Coprod A1 A2) → (p : Path (Coprod A1 A2) (Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1)) x) → Path (Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy. f (inr y)))) (codomain-is-coproduct/inv-map' A1 A2 B f e H t.1 x p) (inl t) = split inl u → λp. codomain-is-coproduct/left-htpy/inl' A1 A2 B f e H t u p ( codomain-is-coproduct/inv-map' A1 A2 B f e H t.1 (inl u) p) ( refl ( Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy. f (inr y)))) ( codomain-is-coproduct/inv-map' A1 A2 B f e H t.1 (inl u) p)) inr u → λp. ex-falso ( Path (Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy. f (inr y)))) (codomain-is-coproduct/inv-map' A1 A2 B f e H t.1 (inr u) p) (inl t)) ( rec-Prop-trunc ( Fib A1 B (λx. f (inl x)) t.1) ( Empty/Prop) ( λw. let x : A1 = w.1 q : Path B t.1 (f (inl x)) = w.2 in Coprod/Eq/eq-map A1 A2 ( inr u) ( inl x) ( map-Equiv/is-injective ( Coprod A1 A2) (Set-trunc B) e ( inr u) ( inl x) ( comp-n (Set-trunc B) four-Nat ( Equiv/map (Coprod A1 A2) (Set-trunc B) e (inr u)) ( Equiv/map (Coprod A1 A2) (Set-trunc B) e ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1))) ( ap (Coprod A1 A2) (Set-trunc B) (Equiv/map (Coprod A1 A2) (Set-trunc B) e) (inr u) (Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1)) (inv (Coprod A1 A2) (Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1)) (inr u) p)) ( Set-trunc/unit t.1) ( Equiv/inv-right-htpy (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1)) ( Set-trunc/unit (f (inl x))) ( ap B (Set-trunc B) (λz. Set-trunc/unit z) t.1 (f (inl x)) q) ( Equiv/map (Coprod A1 A2) (Set-trunc B) e (inl x)) ( H (inl x))))) ( t.2))
The other side is a copy/paste:
codomain-is-coproduct/left-htpy/inr' (A1 A2 B : U) (f : Coprod A1 A2 → B) (e : Equiv (Coprod A1 A2) (Set-trunc B)) (H : Htpy' (Coprod A1 A2) (Set-trunc B) (λx. Set-trunc/unit (f x)) (Equiv/map (Coprod A1 A2) (Set-trunc B) e)) (t : im A2 B (λy. f (inr y))) (a : A2) (p : Path (Coprod A1 A2) (Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1)) (inr a)) : (u : Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy. f (inr y)))) → Path (Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy. f (inr y)))) u (codomain-is-coproduct/inv-map' A1 A2 B f e H t.1 (inr a) p) → Path (Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy. f (inr y)))) u (inr t) = split inl v → λq. ex-falso ( Path (Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy. f (inr y)))) (inl v) (inr t)) ( Coprod/Eq/eq-map ( im A1 B (λx. f (inl x))) ( im A2 B (λy. f (inr y))) ( inl v) ( codomain-is-coproduct/inv-map' A1 A2 B f e H t.1 (inr a) p) q) inr u → λq. Coprod/Eq/map ( im A1 B (λx. f (inl x))) ( im A2 B (λy. f (inr y))) ( inr u) ( inr t) ( SgPath-prop B ( λz. Prop-trunc (Fib A2 B (λy. f (inr y)) z)) ( λz. Prop-trunc/is-prop (Fib A2 B (λy. f (inr y)) z)) u t ( λi. (( Coprod/Eq/eq-map ( im A1 B (λx. f (inl x))) ( im A2 B (λy. f (inr y))) ( inr u) ( codomain-is-coproduct/inv-map' A1 A2 B f e H t.1 (inr a) p) q) i).1)) codomain-is-coproduct/left-htpy/inr (A1 A2 B : U) (f : Coprod A1 A2 → B) (e : Equiv (Coprod A1 A2) (Set-trunc B)) (H : Htpy' (Coprod A1 A2) (Set-trunc B) (λx. Set-trunc/unit (f x)) (Equiv/map (Coprod A1 A2) (Set-trunc B) e)) (t : im A2 B (λy. f (inr y))) : (x : Coprod A1 A2) → (p : Path (Coprod A1 A2) (Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1)) x) → Path (Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy. f (inr y)))) (codomain-is-coproduct/inv-map' A1 A2 B f e H t.1 x p) (inr t) = split inl u → λp. ex-falso ( Path (Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy. f (inr y)))) (codomain-is-coproduct/inv-map' A1 A2 B f e H t.1 (inl u) p) (inr t)) ( rec-Prop-trunc ( Fib A2 B (λy. f (inr y)) t.1) ( Empty/Prop) ( λw. let y : A2 = w.1 q : Path B t.1 (f (inr y)) = w.2 in Coprod/Eq/eq-map A1 A2 ( inl u) ( inr y) ( map-Equiv/is-injective ( Coprod A1 A2) (Set-trunc B) e ( inl u) ( inr y) ( comp-n (Set-trunc B) four-Nat ( Equiv/map (Coprod A1 A2) (Set-trunc B) e (inl u)) ( Equiv/map (Coprod A1 A2) (Set-trunc B) e ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1))) ( ap (Coprod A1 A2) (Set-trunc B) (Equiv/map (Coprod A1 A2) (Set-trunc B) e) (inl u) (Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1)) (inv (Coprod A1 A2) (Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1)) (inl u) p)) ( Set-trunc/unit t.1) ( Equiv/inv-right-htpy (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1)) ( Set-trunc/unit (f (inr y))) ( ap B (Set-trunc B) (λz. Set-trunc/unit z) t.1 (f (inr y)) q) ( Equiv/map (Coprod A1 A2) (Set-trunc B) e (inr y)) ( H (inr y))))) ( t.2)) inr u → λp. codomain-is-coproduct/left-htpy/inr' A1 A2 B f e H t u p ( codomain-is-coproduct/inv-map' A1 A2 B f e H t.1 (inr u) p) ( refl ( Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy. f (inr y)))) ( codomain-is-coproduct/inv-map' A1 A2 B f e H t.1 (inr u) p))
We can finally state the left homotopy:
codomain-is-coproduct/left-htpy (A1 A2 B : U) (f : Coprod A1 A2 → B) (e : Equiv (Coprod A1 A2) (Set-trunc B)) (H : Htpy' (Coprod A1 A2) (Set-trunc B) (λx. Set-trunc/unit (f x)) (Equiv/map (Coprod A1 A2) (Set-trunc B) e)) : (x : Coprod (im A1 B (λx. f (inl x))) (im A2 B (λy. f (inr y)))) → Path (Coprod (im A1 B (λx'. f (inl x'))) (im A2 B (λy. f (inr y)))) (codomain-is-coproduct/inv-map A1 A2 B f e H (codomain-is-coproduct/map A1 A2 B f x)) x = split inl t → codomain-is-coproduct/left-htpy/inl A1 A2 B f e H t ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1)) ( refl ( Coprod A1 A2) ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1))) inr t → codomain-is-coproduct/left-htpy/inr A1 A2 B f e H t ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1)) ( refl ( Coprod A1 A2) ( Equiv/inv-map (Coprod A1 A2) (Set-trunc B) e (Set-trunc/unit t.1)))
1.13.3 Equivalence
Thus, B is equivalent to the coproduct of the images.
codomain-is-coproduct (A1 A2 B : U) (f : Coprod A1 A2 → B) (e : Equiv (Coprod A1 A2) (Set-trunc B)) (H : Htpy' (Coprod A1 A2) (Set-trunc B) (λx. Set-trunc/unit (f x)) (Equiv/map (Coprod A1 A2) (Set-trunc B) e)) : Equiv (Coprod (im A1 B (λx. f (inl x))) (im A2 B (λy. f (inr y)))) B = has-inverse/Equiv ( Coprod (im A1 B (λx. f (inl x))) (im A2 B (λy. f (inr y)))) B ( codomain-is-coproduct/map A1 A2 B f) ( codomain-is-coproduct/inv-map A1 A2 B f e H, ( codomain-is-coproduct/right-htpy A1 A2 B f e H, codomain-is-coproduct/left-htpy A1 A2 B f e H))
1.13.4 Another equivalence
We can also show that the set truncation of im (f ˆ inl) is equivalent to A1 in this case.
im-Set-trunc/map (A1 A2 B : U) (f : Coprod A1 A2 → B) : A1 → Set-trunc (im A1 B (λx. f (inl x))) = λa. Set-trunc/unit ( im/q A1 B (λx. f (inl x)) a)
Indeed, this function is both surjective;
im-Set-trunc-map/is-surj (A1 A2 B : U) (f : Coprod A1 A2 → B) : is-surj A1 (Set-trunc (im A1 B (λx. f (inl x)))) (im-Set-trunc/map A1 A2 B f) = is-surj/comp A1 ( im A1 B (λx. f (inl x))) ( Set-trunc (im A1 B (λx. f (inl x)))) ( λx. Set-trunc/unit x) ( Set-trunc/is-surjective ( im A1 B (λx. f (inl x)))) ( im/q A1 B (λx. f (inl x))) ( im/q/is-surj A1 B (λx. f (inl x)))
and injective.
im-Set-trunc-map/is-inj (A1 A2 B : U) (f : Coprod A1 A2 → B) (e : Equiv (Coprod A1 A2) (Set-trunc B)) (is-set-A1 : is-set A1) (H : Htpy' (Coprod A1 A2) (Set-trunc B) (λx. Set-trunc/unit (f x)) (Equiv/map (Coprod A1 A2) (Set-trunc B) e)) (x y : A1) (p : Path (Set-trunc (im A1 B (λz. f (inl z)))) (im-Set-trunc/map A1 A2 B f x) (im-Set-trunc/map A1 A2 B f y)) : Path A1 x y = rec-Prop-trunc ( Path (im A1 B (λz. f (inl z))) (im/q A1 B (λz. f (inl z)) x) (im/q A1 B (λz. f (inl z)) y)) ( Set/eq/Prop ( A1, is-set-A1) x y) ( λq. Coprod/inl-inj A1 A2 x y ( map-Equiv/is-injective ( Coprod A1 A2) ( Set-trunc B) e ( inl x) ( inl y) ( comp-n ( Set-trunc B) three-Nat ( Equiv/map (Coprod A1 A2) (Set-trunc B) e (inl x)) ( Set-trunc/unit (f (inl x))) ( inv ( Set-trunc B) ( Set-trunc/unit (f (inl x))) ( Equiv/map (Coprod A1 A2) (Set-trunc B) e (inl x)) ( H (inl x))) ( Set-trunc/unit (f (inl y))) ( ap B (Set-trunc B) (λz. Set-trunc/unit z) (f (inl x)) (f (inl y)) (λi. (q i).1)) ( Equiv/map (Coprod A1 A2) (Set-trunc B) e (inl y)) ( H (inl y))))) ( Set-trunc/is-effective/map ( im A1 B (λz. f (inl z))) ( im/q A1 B (λz. f (inl z)) x) ( im/q A1 B (λz. f (inl z)) y) p)
Hence, it is an equivalence.
im-Set-trunc/is-equiv-map (A1 A2 B : U) (f : Coprod A1 A2 → B) (e : Equiv (Coprod A1 A2) (Set-trunc B)) (is-set-A1 : is-set A1) (H : Htpy' (Coprod A1 A2) (Set-trunc B) (λx. Set-trunc/unit (f x)) (Equiv/map (Coprod A1 A2) (Set-trunc B) e)) : is-equiv A1 (Set-trunc (im A1 B (λx. f (inl x)))) (im-Set-trunc/map A1 A2 B f) = is-inj-is-surj/is-equiv A1 ( Set-trunc (im A1 B (λx. f (inl x)))) ( Set-trunc/is-set ( im A1 B (λx. f (inl x)))) ( im-Set-trunc/map A1 A2 B f) ( im-Set-trunc-map/is-surj A1 A2 B f) ( im-Set-trunc-map/is-inj A1 A2 B f e is-set-A1 H)
That is, we have an equivalence between A1 and the set truncation of the image of f ˆ inl.
im-Set-trunc/Equiv (A1 A2 B : U) (f : Coprod A1 A2 → B) (e : Equiv (Coprod A1 A2) (Set-trunc B)) (is-set-A1 : is-set A1) (H : Htpy' (Coprod A1 A2) (Set-trunc B) (λx. Set-trunc/unit (f x)) (Equiv/map (Coprod A1 A2) (Set-trunc B) e)) : Equiv A1 (Set-trunc (im A1 B (λx. f (inl x)))) = ( im-Set-trunc/map A1 A2 B f, im-Set-trunc/is-equiv-map A1 A2 B f e is-set-A1 H)
1.13.5 im Unit A f is connected
The last component needed for the proof is to show that im Unit A f is connected.
im-Unit/is-conn (A : U) (f : Unit → A) : is-conn (im Unit A f) = is-prop/is-proof-irrelevant ( Set-trunc (im Unit A f)) ( λt u. ind-Set-trunc/Prop ( im Unit A f) ( λv. Set-trunc/eq/Prop ( im Unit A f) v u) ( λv. ind-Set-trunc/Prop ( im Unit A f) ( λw. Set-trunc/eq/Prop ( im Unit A f) ( Set-trunc/unit v) w) ( λw. rec-Prop-trunc ( Fib Unit A f v.1) ( Set-trunc/eq/Prop ( im Unit A f) ( Set-trunc/unit v) ( Set-trunc/unit w)) ( λx. rec-Prop-trunc ( Fib Unit A f w.1) ( Set-trunc/eq/Prop ( im Unit A f) ( Set-trunc/unit v) ( Set-trunc/unit w)) ( λy. ap (im Unit A f) (Set-trunc (im Unit A f)) (λk. Set-trunc/unit k) v w ( SgPath-prop A ( λz. Prop-trunc (Fib Unit A f z)) ( λz. Prop-trunc/is-prop (Fib Unit A f z)) v w ( comp-n A three-Nat v.1 ( f x.1) x.2 ( f y.1) ( ap Unit A f x.1 y.1 ( is-contr/all-elements-equal Unit ( Unit/is-contr) x.1 y.1)) w.1 ( inv A w.1 (f y.1) y.2)))) w.2) v.2) u) t) ( Set-trunc/unit (im/q Unit A f star))
1.13.6 Closure under Σ-types
We start to show the inductive case of the base case of the induction, i.e., A is π1-finite and has at least one connected component, and B(x) is π0-finite forall x.
is-htpy-finite/closed-Sg/z : (k : Nat) → (A : U) (B : A → U) (is-htpy-finite-A : is-htpy-finite one-Nat A) (is-htpy-finite-B : (x : A) → is-htpy-finite zero (B x)) → (e : Equiv (Fin k) (Set-trunc A)) → is-htpy-finite zero (Σ A B) = split zero → λA B _ _ e. let e' : Equiv Empty A = Equiv/sym A Empty ( Empty/equiv A ( is-empty-Set-trunc/is-empty A ( Equiv/inv-map Empty (Set-trunc A) e))) f : Empty → A = Equiv/map Empty A e' in is-htpy-finite/closed-Equiv ( Σ A B) Empty ( Equiv/trans ( Σ A B) ( Σ (Fin zero) (λx. B (f x))) ( Empty) ( Sg/equiv-base' Empty A B e') ( Equiv/Equiv-Sg-empty (λx. B (f x)))) ( zero) ( Empty/is-htpy-finite zero) suc k → λA B is-htpy-finite-A is-htpy-finite-B e. rec-Prop-trunc ( Σ (Fin (suc k) → A) (λf. Htpy' (Fin (suc k)) (Set-trunc A) (λz. Set-trunc/unit (f z)) (Equiv/map (Fin (suc k)) (Set-trunc A) e))) ( is-htpy-finite/Prop zero (Σ A B)) ( λF. let f : (Fin (suc k) → A) = F.1 H : Htpy' (Fin (suc k)) (Set-trunc A) (λz. Set-trunc/unit (f z)) (Equiv/map (Fin (suc k)) (Set-trunc A) e) = F.2 e' : Equiv (Coprod (im (Fin k) A (λx. f (inl x))) (im Unit A (λx. f (inr x)))) A = codomain-is-coproduct (Fin k) Unit A f e H in is-htpy-finite/closed-Equiv ( Σ A B) ( Coprod ( Σ (im (Fin k) A (λx. f (inl x))) (λt. B (t.1))) ( Σ (im Unit A (λx. f (inr x))) (λt. B (t.1)))) ( Equiv/trans ( Σ A B) ( Σ (Coprod (im (Fin k) A (λx. f (inl x))) (im Unit A (λx. f (inr x)))) (λu. B (Equiv/map (Coprod (im (Fin k) A (λx. f (inl x))) (im Unit A (λx. f (inr x)))) A e' u))) ( Coprod ( Σ (im (Fin k) A (λx. f (inl x))) (λt. B (t.1))) ( Σ (im Unit A (λx. f (inr x))) (λt. B (t.1)))) ( Sg/equiv-base' ( Coprod (im (Fin k) A (λx. f (inl x))) (im Unit A (λx. f (inr x)))) A B e') ( Equiv/Sg-distr-over-coprod ( im (Fin k) A (λx. f (inl x))) ( im Unit A (λx. f (inr x))) ( λu. B (Equiv/map (Coprod (im (Fin k) A (λx. f (inl x))) (im Unit A (λx. f (inr x)))) A e' u)))) zero ( is-htpy-finite/closed-Coprod zero ( Σ (im (Fin k) A (λx. f (inl x))) (λt. B (t.1))) ( Σ (im Unit A (λx. f (inr x))) (λt. B (t.1))) ( is-htpy-finite/closed-Sg/z k ( im (Fin k) A (λx. f (inl x))) ( λt. B (t.1)) ( is-htpy-finite/Coprod/left ( im (Fin k) A (λx. f (inl x))) ( im Unit A (λx. f (inr x))) one-Nat ( is-htpy-finite/closed-Equiv ( Coprod (im (Fin k) A (λx. f (inl x))) (im Unit A (λx. f (inr x)))) A e' one-Nat ( is-htpy-finite-A))) ( λt. is-htpy-finite-B t.1) ( im-Set-trunc/Equiv ( Fin k) Unit A f e ( count/is-set (Fin k) (count/fin-count k)) H)) ( is-htpy-finite/closed-Sg/base ( im Unit A (λx. f (inr x))) ( λt. B t.1) ( im-Unit/is-conn A (λx. f (inr x))) ( is-htpy-finite/Coprod/right ( im (Fin k) A (λx. f (inl x))) ( im Unit A (λx. f (inr x))) one-Nat ( is-htpy-finite/closed-Equiv ( Coprod (im (Fin k) A (λx. f (inl x))) (im Unit A (λx. f (inr x)))) A e' one-Nat ( is-htpy-finite-A))) ( λt. is-htpy-finite-B t.1)))) ( is-finite-Set-trunc/has-Equiv-map A (suc k) e)
And we can conclude the inductive case by remarking that for t, u : Σ A B, t = u is equivalent to Σp: t.1 = u.1(trB(p, t.2) = u.2).
is-htpy-finite/closed-Sg' : (n : Nat) (A : U) (B : A → U) (is-htpy-finite-A : is-htpy-finite (suc n) A) (is-htpy-finite-B : (x : A) → is-htpy-finite n (B x)) → is-htpy-finite n (Σ A B) = split zero → λA B is-htpy-finite-A is-htpy-finite-B. rec-Prop-trunc ( count (Set-trunc A)) ( is-htpy-finite/Prop zero (Σ A B)) ( λc. is-htpy-finite/closed-Sg/z c.1 A B is-htpy-finite-A is-htpy-finite-B c.2) ( is-htpy-finite-A.1) suc n → λA B is-htpy-finite-A is-htpy-finite-B. ( is-htpy-finite/closed-Sg' zero A B ( is-htpy-finite/is-htpy-one-finite A (suc n) is-htpy-finite-A) ( λx. is-htpy-finite/is-finite-Set-trunc ( B x) ( suc n) ( is-htpy-finite-B x)), λt u. is-htpy-finite/closed-Equiv ( Path (Σ A B) t u) ( SgPathO A B t u) ( PathSg/Equiv A B t u) n ( is-htpy-finite/closed-Sg' n ( Path A t.1 u.1) ( λp. Path (B u.1) (tr A t.1 u.1 p B t.2) u.2) ( is-htpy-finite-A.2 t.1 u.1) ( λp. (is-htpy-finite-B u.1).2 (tr A t.1 u.1 p B t.2) u.2)))
We rearrange the arguments to make it easier to call.
is-htpy-finite/closed-Σ (A : U) (B : A → U) (n : Nat) (is-htpy-finite-A : is-htpy-finite (suc n) A) (is-htpy-finite-B : (x : A) → is-htpy-finite n (B x)) : is-htpy-finite n (Σ A B) = is-htpy-finite/closed-Sg' n A B is-htpy-finite-A is-htpy-finite-B
1.14 Unlock
unlock Prop-trunc/is-prop UU-Prop/is-set Set-trunc/is-effective/map