Finite Types
Table of Contents
- 1. Finite types
- 1.1. Packages imports
- 1.2. Definition
- 1.3. Properties
- 1.3.1. A type that has a count is finite
- 1.3.2. Unit and Empty are finite
- 1.3.3. Fin is finite
- 1.3.4. Closure under equivalence
- 1.3.5. Decidable
- 1.3.6. A finite type is either inhabited or empty
- 1.3.7. A finite type has decidable propositional truncation
- 1.3.8. A finite type has finite propositional truncation
- 1.3.9. Contractible type is finite
- 1.4. Cardinality
- 1.5. One element is contractible
- 1.6. Some immediate consequences
- 1.7. Cardinal of Bool * Bool
- 1.8. Closure under Π-types
- 1.9. A finite type is a set
- 1.10. A finite type has decidable equality
- 1.11. Finite choice
- 1.12. Extracting count from finiteness
- 1.13. Another "finite" choice
- 1.14. Closure under Σ-types
- 1.15. Surjective map codomain is finite iff it has decidable equality
- 1.16. It is decidable to know whether a finite type is contractible or not
- 1.17. The number of equivalences between finite types are finite
1 Finite types
module Lib.IsFinite where
Finite types are types that can be counted. However, when defining finite types, we do not especially care about the counting, we only care about the fact that it can be counted, which translates in the definition by using propositional truncation. However, this definition is not practical as it does not give the number of elements. Hence, we also show that finite types are logically equivalent to types with cardinalities.
1.1 Packages imports
The imported packages can be accessed via the following links:
- Lib/Counting
- Lib/GlobalChoice
- Lib/PropTrunc
- Lib/Image
- Lib/Sorry
- Lib/Prop/Coprod
- Lib/Prop/Decidability
- Lib/Prop/Empty
- Lib/Prop/Nat
import Lib.Counting import Lib.GlobalChoice import Lib.PropTrunc import Lib.Image import Lib.Sorry import Lib.Prop.Coprod import Lib.Prop.Decidability import Lib.Prop.Empty import Lib.Prop.Nat
1.2 Definition
Definition using propositional truncation.
is-finite (X : U) : U = Prop-trunc ( count X)
Some shortcuts.
is-finite/is-prop (X : U) : is-prop (is-finite X) = Prop-trunc/is-prop ( count X) is-finite/Prop (X : U) : UU-Prop = ( is-finite X, is-finite/is-prop X)
1.3 Properties
1.3.1 A type that has a count is finite
count/is-finite (X : U) (c : count X) : is-finite X = Prop-trunc/unit c
1.3.2 Unit and Empty are finite
Unit/is-finite : is-finite Unit = count/is-finite Unit ( count/Unit) Empty/is-finite : is-finite Empty = count/is-finite Empty ( count/zero-count)
1.3.3 Fin is finite
Fin/is-finite (k : Nat) : is-finite (Fin k) = count/is-finite ( Fin k) ( count/fin-count k)
1.3.4 Closure under equivalence
Of course, if Equiv X Y and one of them is finite, the other one is also finite.
is-finite/closed-Equiv (A B : U) (e : Equiv A B) (is-finite-B : is-finite B) : is-finite A = Prop-trunc/map ( count B) ( count A) ( count/closed-equiv A B e) is-finite-B is-finite/closed-Equiv' (A B : U) (e : Equiv A B) (is-finite-A : is-finite A) : is-finite B = is-finite/closed-Equiv B A (Equiv/sym A B e) is-finite-A
1.3.5 Decidable
A proposition is finite iff it is decidable.
is-finite/is-decidable (X : U) (is-prop-X : is-prop X) (is-finite-X : is-finite X) : is-decidable X = rec-Prop-trunc ( count X) ( is-decidable/Prop X is-prop-X) ( λc. count/countable-is-decidable X c) is-finite-X is-decidable/is-finite (X : U) (is-prop-X : is-prop X) (is-decidable-X : is-decidable X) : is-finite X = Prop-trunc/unit ( count/is-decidable-is-countable X is-prop-X is-decidable-X)
1.3.6 A finite type is either inhabited or empty
is-finite/is-inhabited-or-empty' (A : U) : (k : Nat) → (e : Equiv (Fin k) A) → Coprod (Prop-trunc A) (is-empty A) = split zero → λe. inr (Equiv/inv-map (Fin zero) A e) suc k → λe. inl (Prop-trunc/unit (Equiv/map (Fin (suc k)) A e (zero-Fin k))) is-finite/is-inhabited-or-empty (A : U) : is-finite A → Coprod (Prop-trunc A) (is-empty A) = rec-Prop-trunc ( count A) ( Coprod/Prop ( Prop-trunc/Prop A) ( Prop/Pi A (λ_. Empty/Prop)) ( rec-Prop-trunc A ( Prop/Pi (is-empty A) (λ_. Empty/Prop)) ( λa h. h a))) ( λc. is-finite/is-inhabited-or-empty' A ( number-of-elements A c) ( count/Equiv A c))
1.3.7 A finite type has decidable propositional truncation
is-finite/is-decidable-Prop-trunc' (A : U) : Coprod (Prop-trunc A) (is-empty A) → is-decidable (Prop-trunc A) = split inl x → inl x inr na → inr ( rec-Prop-trunc A ( Empty/Prop) ( λa. na a)) is-finite/is-decidable-Prop-trunc (A : U) (is-finite-A : is-finite A) : is-decidable (Prop-trunc A) = is-finite/is-decidable-Prop-trunc' A ( is-finite/is-inhabited-or-empty A is-finite-A)
1.3.8 A finite type has finite propositional truncation
is-finite/is-finite-Prop-trunc (A : U) (is-finite-A : is-finite A) : is-finite (Prop-trunc A) = Prop-trunc/unit ( count/is-decidable-is-countable ( Prop-trunc A) ( Prop-trunc/is-prop A) ( is-finite/is-decidable-Prop-trunc A is-finite-A))
1.3.9 Contractible type is finite
is-contr/is-finite (X : U) (H : is-contr X) : is-finite X = count/is-finite X ( count/contr-count X H)
1.4 Cardinality
We define the notion of having a cardinality and its equivalence to the notion of is-finite.
has-cardinality (X : U) : U = Σ Nat ( λk. mere-equiv (Fin k) X)
Of course, has-cardinality is a proposition.
has-cardinality/is-prop/sg (X : U) (k : Nat) (h : mere-equiv (Fin k) X) (k' : Nat) (h' : mere-equiv (Fin k') X) : Path (has-cardinality X) (k, h) (k', h') = SgPath-prop Nat ( λn. mere-equiv (Fin n) X) ( λn. mere-equiv/is-prop (Fin n) X) ( k, h) ( k', h') ( rec-Prop-trunc ( Equiv (Fin k) X) ( Nat/eq/Prop k k') ( λe. rec-Prop-trunc ( Equiv (Fin k') X) ( Nat/eq/Prop k k') ( λe'. Fin/is-inj k k' ( Equiv/trans ( Fin k) X ( Fin k') e ( Equiv/sym (Fin k') X e'))) h') h) has-cardinality/is-prop (X : U) : is-prop (has-cardinality X) = λh h'. has-cardinality/is-prop/sg X h.1 h.2 h'.1 h'.2 has-cardinality/Prop (X : U) : UU-Prop = ( has-cardinality X, has-cardinality/is-prop X)
Thus, there is an equivalence between having a cardinality and being finite.
is-finite/has-cardinality (X : U) : is-finite X → has-cardinality X = rec-Prop-trunc ( count X) ( has-cardinality/Prop X) ( λc. ( number-of-elements X c, Prop-trunc/unit (count/Equiv X c))) has-cardinality/is-finite' (X : U) (k : Nat) (e : mere-equiv (Fin k) X) : is-finite X = rec-Prop-trunc ( Equiv (Fin k) X) ( is-finite/Prop X) ( λe'. Prop-trunc/unit (k, e')) e has-cardinality/is-finite (X : U) : has-cardinality X → is-finite X = λt. has-cardinality/is-finite' X t.1 t.2
Some shortcuts.
has-cardinality/card (X : U) (h : has-cardinality X) : Nat = h.1 has-cardinality/Equiv (X : U) (h : has-cardinality X) : mere-equiv (Fin (has-cardinality/card X h)) X = h.2 card (X : U) (i : is-finite X) : Nat = has-cardinality/card X ( is-finite/has-cardinality X i)
1.5 One element is contractible
lock has-cardinality/is-prop is-finite/one-element-is-contr (A : U) (is-finite-A : is-finite A) (p : Path Nat one-Nat (card A is-finite-A)) : is-contr A = rec-Prop-trunc ( Equiv (Fin (card A is-finite-A)) A) ( ( is-contr A, is-contr/is-prop A)) ( λe. count/one-element-is-contr A (card A is-finite-A, e) p) ( is-finite/has-cardinality A is-finite-A).2 unlock has-cardinality/is-prop
1.6 Some immediate consequences
X and Y are finite iff their coproduct is finite.
is-finite/closed-Coprod (A B : U) (is-finite-A : is-finite A) (is-finite-B : is-finite B) : is-finite (Coprod A B) = rec-Prop-trunc ( count A) ( is-finite/Prop (Coprod A B)) ( λc. rec-Prop-trunc ( count B) ( is-finite/Prop (Coprod A B)) ( λc'. Prop-trunc/unit (count/closed-Coprod A B c c')) is-finite-B) is-finite-A is-finite/closed-Coprod-left (A B : U) (is-finite-copr : is-finite (Coprod A B)) : is-finite A = rec-Prop-trunc ( count (Coprod A B)) ( is-finite/Prop A) ( λc. Prop-trunc/unit (count/closed-Coprod-left A B c)) is-finite-copr is-finite/closed-Coprod-right (A B : U) (is-finite-copr : is-finite (Coprod A B)) : is-finite B = rec-Prop-trunc ( count (Coprod A B)) ( is-finite/Prop B) ( λc. Prop-trunc/unit (count/closed-Coprod-right A B c)) is-finite-copr
If X and Y are finite, then X * Y is also finite.
is-finite/closed-Prod (A B : U) (is-finite-A : is-finite A) (is-finite-B : is-finite B) : is-finite (A * B) = rec-Prop-trunc ( count A) ( is-finite/Prop (A * B)) ( λc. rec-Prop-trunc ( count B) ( is-finite/Prop (A * B)) ( λc'. Prop-trunc/unit (count/closed-Prod A B c c')) is-finite-B) is-finite-A
1.7 Cardinal of Bool * Bool
Bool : U = Coprod Unit Unit true : Bool = inl star false : Bool = inr star Bool/is-finite : is-finite Bool = is-finite/closed-Coprod Unit Unit Unit/is-finite Unit/is-finite BoolBool/card : Nat = card ( Bool * Bool) ( is-finite/closed-Prod Bool Bool Bool/is-finite Bool/is-finite)
1.8 Closure under Π-types
In this section, we show that if B is a family of finite types over a finite type A, then the product Πx: AB(x) is also finite.
1.8.1 Finite family over Fin k
First, we start by showing that if B is a finite family over Fin k, then Πx: Fin kB(x) is also finite. This proof is by induction on k.
The case k = 0 is trivial: a family over the empty type is contractible thus it has a count and it is finite.
The case k > 0 is done using the dependent universal property of coproduct. By induction hypothesis, Πx: Fin kB(x) is finite and by hypothesis, B(inr star) is also finite. Finally, a product of finite things is finite.
is-finite/pi' : (k : Nat) → (B : Fin k → U) → ((x : Fin k) → is-finite (B x)) → is-finite ((x : Fin k) → B x) = split zero → λB _. count/is-finite ( (x : Fin zero) → B x) ( count/contr-count ( (x : Fin zero) → B x) ( Empty/universal-dependent-property ( Fin zero) B ( Equiv/refl (Fin zero)))) suc k → λB is-fin-B. is-finite/closed-Equiv ( (x : Fin (suc k)) → B x) ( ((x : Fin k) → B (inl x)) * (B (inr star))) ( Equiv/trans ( (x : Fin (suc k)) → B x) ( ((x : Fin k) → B (inl x)) * ((u : Unit) → B (inr u))) ( ((x : Fin k) → B (inl x)) * (B (inr star))) ( Coprod/dependent-universal-property ( Fin k) Unit B) ( Equiv/prod' ( (x : Fin k) → B (inl x)) ( (u : Unit) → B (inr u)) ( B (inr star)) ( Equiv/pi-Unit ( λu. B (inr u))))) ( is-finite/closed-Prod ( (x : Fin k) → B (inl x)) ( B (inr star)) ( is-finite/pi' k ( λx. B (inl x)) ( λx. is-fin-B (inl x))) ( is-fin-B (inr star)))
1.8.2 Finite family over finite type
Let A be a finite type. As is-finite is a proposition, by the induction principle of the propositional truncation, we assume that we have a count of A; that is, an equivalence from Fin k to A for some k. Then, as is-finite is closed under equivalence, for any finite family B over a finite type A, Πx: AB(x) is also finite.
is-finite/Pi (A : U) (B : A → U) (is-finite-A : is-finite A) (is-finite-B : (x : A) → is-finite (B x)) : is-finite ((x : A) → B x) = rec-Prop-trunc ( count A) ( is-finite/Prop ((x : A) → B x)) ( λc. is-finite/closed-Equiv ( (x : A) → B x) ( (x : Fin (number-of-elements A c)) → B (Equiv/map (Fin (number-of-elements A c)) A (count/Equiv A c) x)) ( Equiv/dependent ( Fin (number-of-elements A c)) A B ( count/Equiv A c)) ( is-finite/pi' ( number-of-elements A c) ( λx. B (Equiv/map (Fin (number-of-elements A c)) A (count/Equiv A c) x)) ( λx. is-finite-B (Equiv/map (Fin (number-of-elements A c)) A (count/Equiv A c) x)))) is-finite-A
1.9 A finite type is a set
is-finite/is-set (A : U) : is-finite A → is-set A = rec-Prop-trunc ( count A) ( is-set/Prop A) ( λc. count/is-set A c)
1.10 A finite type has decidable equality
If a type is finite, then it is a set. In particular, has-decidable-equality is a proposition on this type, so it follows by the recursion principle of propositional truncation that a finite type has decidable equality.
is-finite/has-decidable-equality (A : U) (is-finite-A : is-finite A) : has-decidable-equality A = rec-Prop-trunc ( count A) ( has-decidable-equality/Prop A ( is-finite/is-set A is-finite-A)) ( count/has-decidable-eq A) is-finite-A
1.11 Finite choice
There is a finite choice map (Πx: A||B x||) → ||Πx: AB(x)|| for any finite type A and family over this finite type B.
Fin/choice : (k : Nat) (B : Fin k → U) (H : (x : Fin k) → Prop-trunc (B x)) → Prop-trunc ((x : Fin k) → B x) = split zero → λB _. Prop-trunc/unit ( center ((x : Fin zero) → B x) ( Empty/universal-dependent-property ( Fin zero) B ( Equiv/refl (Fin zero)))) suc k → λB. Equiv/map ( (x : Fin (suc k)) → Prop-trunc (B x)) ( Prop-trunc ((x : Fin (suc k)) → B x)) ( Equiv/comp five-Nat ( (x : Fin (suc k)) → Prop-trunc (B x)) ( ((x : Fin k) → Prop-trunc (B (inl x))) * ((x : Unit) → Prop-trunc (B (inr x)))) ( Coprod/dependent-universal-property ( Fin k) Unit (λx. Prop-trunc (B x))) ( ((x : Fin k) → Prop-trunc (B (inl x))) * (Prop-trunc (B (inr star)))) ( Equiv/prod' ( (x : Fin k) → Prop-trunc (B (inl x))) ( (x : Unit) → Prop-trunc (B (inr x))) ( Prop-trunc (B (inr star))) ( Equiv/pi-Unit ( λx. Prop-trunc (B (inr x))))) ( (Prop-trunc ((x : Fin k) → B (inl x))) * (Prop-trunc (B (inr star)))) ( Equiv/prod ( (x : Fin k) → Prop-trunc (B (inl x))) ( Prop-trunc ((x : Fin k) → B (inl x))) ( Prop-trunc (B (inr star))) ( Prop/Equiv ( Prop/Pi (Fin k) (λx. Prop-trunc/Prop (B (inl x)))) ( Prop-trunc/Prop ((x : Fin k) → B (inl x))) ( Fin/choice k (λx. B (inl x))) ( Prop-trunc/Pi/map-out ( Fin k) ( λx. B (inl x))))) ( Prop-trunc (((x : Fin k) → B (inl x)) * (B (inr star)))) ( Prop-trunc/closed-Prod ( (x : Fin k) → B (inl x)) ( B (inr star))) ( Prop-trunc (((x : Fin k) → B (inl x)) * ((x : Unit) → B (inr x)))) ( Equiv/Prop-trunc (((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)))))) ( Prop-trunc ((x : Fin (suc k)) → B x)) ( Equiv/Prop-trunc ( ((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)))) is-finite/choice (A : U) (B : A → U) (is-finite-A : is-finite A) (H : (x : A) → Prop-trunc (B x)) : Prop-trunc ((x : A) → B x) = rec-Prop-trunc ( count A) ( Prop-trunc/Prop ( (x : A) → B x)) ( λc. let k : Nat = number-of-elements A c f : Fin k → A = Equiv/map (Fin k) A (count/Equiv A c) g : A → Fin k = Equiv/inv-map (Fin k) A (count/Equiv A c) in rec-Prop-trunc ( (x : (Fin k)) → B (f x)) ( Prop-trunc/Prop ((x : A) → B x)) ( λh. Prop-trunc/unit ( λx. tr A (f (g x)) x (Equiv/inv-right-htpy (Fin k) A (count/Equiv A c) x) B (h (g x)))) ( Fin/choice k ( λx. B (f x)) ( λx. H (f x)))) is-finite-A
1.12 Extracting count from finiteness
Under some conditions, counting can be extracted from finiteness.
is-finite/count (A : U) (B : A → U) (Heq : has-decidable-equality A) (c : count (Σ A B)) (H : (x : A) → is-finite (B x)) (f : (x : A) → Prop-trunc (B x)) (a : A) : count (B a) = let is-inj-fib-incl : (z z' : B a) → Path (Σ A B) (a, z) (a, z') → Path (B a) z z' = is-set-is-inj-fib A B a (hedberg A Heq) is-prop-fib : (t : Σ A B) → is-prop (Σ (B a) (λz. Path (Σ A B) t (a, z))) = λt u v. SgPath-prop ( B a) ( λz. Path (Σ A B) t (a, z)) ( λz. count/is-set (Σ A B) c t (a, z)) u v ( is-inj-fib-incl u.1 v.1 ( comp (Σ A B) (a, u.1) t ( inv (Σ A B) t (a, u.1) u.2) (a, v.1) v.2)) in count/closed-equiv ( B a) ( Σ (Σ A B) (Fib (B a) (Σ A B) (fiber-inclusion A B a))) ( Equiv/total-fib (B a) (Σ A B) (fiber-inclusion A B a)) ( count/closed-Sg ( Σ A B) ( Fib (B a) (Σ A B) (fiber-inclusion A B a)) c ( λt. count/closed-equiv ( Σ (B a) (λz. Path (Σ A B) t (a, z))) ( Path A t.1 a) ( Equiv/Path-tot A B a t.1 t.2) ( count/is-decidable-is-countable ( Path A t.1 a) ( hedberg A Heq t.1 a) ( Heq t.1 a))))
1.13 Another "finite" choice
There is another case where we can make such a choice.
lock is-finite/count count-choice (A : U) (B : A → U) (Heq : has-decidable-equality A) (k : Nat) (e : Equiv (Fin k) (Σ A B)) (is-finite-B : (x : A) → is-finite (B x)) (H : (x : A) → Prop-trunc (B x)) : (x : A) → B x = λx. let t : count (B x) = is-finite/count A B Heq (k, e) is-finite-B H x in count/global-choice ( B x) t.1 t.2 ( H x) unlock is-finite/count finite-choice (A : U) (B : A → U) (Heq : has-decidable-equality A) (is-finite-AB : is-finite (Σ A B)) (is-finite-B : (x : A) → is-finite (B x)) (H : (x : A) → Prop-trunc (B x)) : Prop-trunc ((x : A) → B x) = rec-Prop-trunc ( count (Σ A B)) ( Prop-trunc/Prop ((x : A) → B x)) ( λc. Prop-trunc/unit (count-choice A B Heq c.1 c.2 is-finite-B H)) ( is-finite-AB)
1.14 Closure under Σ-types
Given a finite type A and a family of finite types B over A, Σ A B is also finite.
is-finite/closed-Σ (A : U) (B : A → U) (is-finite-A : is-finite A) (H : (x : A) → is-finite (B x)) : is-finite (Σ A B) = rec-Prop-trunc ( count A) ( is-finite/Prop ( Σ A B)) ( λc. rec-Prop-trunc ( (x : A) → count (B x)) ( is-finite/Prop ( Σ A B)) ( λH'. Prop-trunc/unit (count/closed-Σ A B c H')) ( is-finite/choice A (λx. count (B x)) is-finite-A H)) is-finite-A
The following is shown for testing purposes, when a counting can directly be extracted from B x.
is-finite/closed-Sg' (A : U) (B : A → U) (is-finite-A : is-finite A) (H : (x : A) → count (B x)) : is-finite (Σ A B) = rec-Prop-trunc ( count A) ( is-finite/Prop ( Σ A B)) ( λc. Prop-trunc/unit (count/closed-Σ A B c H)) ( is-finite-A)
Moreover, if B(x) is finite forall x : A and if Σ A B is finite and the type family B has a section, then it follows that A is finite. We start by defining a function such that A is equivalent to its fibrations.
is-finite-Sg/is-finite-base/map (A : U) (B : A → U) (f : (x : A) → B x) (x : A) : Σ A B = (x, f x)
The type of fibrations of this map is equivalent to the equality on (B x): fibg(t) ≅ Σx: AΣt.1 = x t.2 = f(x) ≅ ΣΣ A (λx. t.1 = x) t.2 = f(x)
is-finite-Sg/is-finite-base/Equiv' (A : U) (B : A → U) (f : (x : A) → B x) (t : Σ A B) : Equiv (Fib A (Σ A B) (is-finite-Sg/is-finite-base/map A B f) t) (Σ (Σ A (λx. Path A t.1 x)) (λu. Path (B u.1) (tr A t.1 u.1 u.2 B t.2) (f u.1))) = let C : (x : A) → Path A t.1 x → U = λx p. Path (B x) (tr A t.1 x p B t.2) (f x) in Equiv/trans ( Fib A (Σ A B) (is-finite-Sg/is-finite-base/map A B f) t) ( Σ A (λx. Σ (Path A t.1 x) (C x))) ( Σ (Σ A (λx. Path A t.1 x)) (λu. C u.1 u.2)) ( Equiv/Sg-fam A ( λx. Path (Σ A B) t (x, f x)) ( λx. Σ (Path A t.1 x) (λp. Path (B x) (tr A t.1 x p B t.2) (f x))) ( λx. PathSg/Equiv A B t (x, f x))) ( Equiv/associative-Σ A ( λx. Path A t.1 x) C)
In particular, as Σx: At.1 = x is contractible, we can further this equivalence.
is-finite-Sg/is-finite-base/Equiv (A : U) (B : A → U) (f : (x : A) → B x) (t : Σ A B) : let c : Σ A (λx. Path A t.1 x) = (is-contr/Sg-path-is-contr A t.1).1 in Equiv (Fib A (Σ A B) (is-finite-Sg/is-finite-base/map A B f) t) (Path (B c.1) (tr A t.1 c.1 c.2 B t.2) (f c.1)) = let C : (x : A) → Path A t.1 x → U = λx p. (Path (B x) (tr A t.1 x p B t.2) (f x)) c : Σ A (λx. Path A t.1 x) = (is-contr/Sg-path-is-contr A t.1).1 in Equiv/trans ( Fib A (Σ A B) (is-finite-Sg/is-finite-base/map A B f) t) ( Σ (Σ A (λx. Path A t.1 x)) (λu. C u.1 u.2)) ( Path (B c.1) (tr A t.1 c.1 c.2 B t.2) (f c.1)) ( is-finite-Sg/is-finite-base/Equiv' A B f t) ( Equiv/is-contr-total-space' ( Σ A (λx. Path A t.1 x)) ( λu. C u.1 u.2) ( is-contr/Sg-path-is-contr A t.1) c)
As A is equivalent to the sum of fibrations of the map, and forall x, (B x) is finite (hence it has a propositional, decidable equality) then A is finite.
is-finite-Sg/is-finite-base (A : U) (B : A → U) (f : (x : A) → B x) (H : (x : A) → is-finite (B x)) (H' : is-finite (Σ A B)) : is-finite A = is-finite/closed-Equiv A ( Σ (Σ A B) (Fib A (Σ A B) (is-finite-Sg/is-finite-base/map A B f))) ( Equiv/total-fib A ( Σ A B) ( is-finite-Sg/is-finite-base/map A B f)) ( is-finite/closed-Sg ( Σ A B) ( Fib A (Σ A B) (is-finite-Sg/is-finite-base/map A B f)) H' ( λt. let c : Σ A (λx. Path A t.1 x) = (is-contr/Sg-path-is-contr A t.1).1 in is-finite/closed-Equiv ( Fib A (Σ A B) (is-finite-Sg/is-finite-base/map A B f) t) ( Path (B c.1) (tr A t.1 c.1 c.2 B t.2) (f c.1)) ( is-finite-Sg/is-finite-base/Equiv A B f t) ( is-decidable/is-finite ( Path (B c.1) (tr A t.1 c.1 c.2 B t.2) (f c.1)) ( is-finite/is-set ( B c.1) ( H c.1) ( tr A t.1 c.1 c.2 B t.2) ( f c.1)) ( is-finite/has-decidable-equality ( B c.1) ( H c.1) ( tr A t.1 c.1 c.2 B t.2) ( f c.1)))))
1.15 Surjective map codomain is finite iff it has decidable equality
We show that if f : A → B is a surjective map and A is finite, then B is finite iff it has decidable equality. In fact, the forward direction is immediate from is-finite/has-decidable-equality. We show the converse by induction on the number of elements. First, we set A to be Fin k and we show that B has a count. The base case is trivial, ∅ ≅ B.
has-decidable-equality/is-finite/base/map (B : U) (f : Empty → B) (H : is-surj Empty B f) : B → Empty = λb. rec-Prop-trunc ( Fib Empty B f b) ( Empty/Prop) ( λt. t.1) ( H b) has-decidable-equality/is-finite/base/right-htpy (B : U) (f : Empty → B) (H : is-surj Empty B f) (x : Empty) : Path Empty (has-decidable-equality/is-finite/base/map B f H (f x)) x = ex-falso ( Path Empty (has-decidable-equality/is-finite/base/map B f H (f x)) x) x has-decidable-equality/is-finite/base/left-htpy (B : U) (f : Empty → B) (H : is-surj Empty B f) (b : B) : Path B (f (has-decidable-equality/is-finite/base/map B f H b)) b = ex-falso ( Path B (f (has-decidable-equality/is-finite/base/map B f H b)) b) ( rec-Prop-trunc ( Fib Empty B f b) ( Empty/Prop) ( λt. t.1) ( H b)) has-decidable-equality/is-finite/base (B : U) (f : Empty → B) (H : is-surj Empty B f) : count B = ( zero, has-inverse/Equiv Empty B f ( has-decidable-equality/is-finite/base/map B f H, ( has-decidable-equality/is-finite/base/left-htpy B f H, has-decidable-equality/is-finite/base/right-htpy B f H)))
The inductive case is more involved. First, as B's equality is decidable, we can decide for any y : B whether there exists an x : Fin k such that y = f(x) or if no x : Fin k are such that y = f(x).
1.15.1 Decidability
has-decidable-equality/is-finite/decide/s'' (B : U) (y : B) (k : Nat) (f : Fin (suc k) → B) (p : neg (Path B y (f (inr star)))) (h : (x : Fin k) → neg (Path B y (f (inl x)))) : (x : Fin (suc k)) → neg (Path B y (f x)) = split inl x → h x inr s → ind-Unit ( λx. neg (Path B y (f (inr x)))) p s has-decidable-equality/is-finite/decide/s' (B : U) (y : B) (k : Nat) (f : Fin (suc k) → B) (p : neg (Path B y (f (inr star)))) : Coprod (Σ (Fin k) (λx. Path B y (f (inl x)))) ((x : Fin k) → neg (Path B y (f (inl x)))) → Coprod (Σ (Fin (suc k)) (λx. Path B y (f x))) ((x : Fin (suc k)) → neg (Path B y (f x))) = split inl t → inl (inl t.1, t.2) inr h → inr (has-decidable-equality/is-finite/decide/s'' B y k f p h) has-decidable-equality/is-finite/decide/s (B : U) (y : B) (k : Nat) (f : Fin (suc k) → B) (u : Coprod (Σ (Fin k) (λx. Path B y (f (inl x)))) ((x : Fin k) → neg (Path B y (f (inl x))))) : Coprod (Path B y (f (inr star))) (neg (Path B y (f (inr star)))) → Coprod (Σ (Fin (suc k)) (λx. Path B y (f x))) ((x : Fin (suc k)) → neg (Path B y (f x))) = split inl p → inl (inr star, p) inr p → has-decidable-equality/is-finite/decide/s' B y k f p u has-decidable-equality/is-finite/decide'/z' (B : U) (y : B) (f : Fin (suc (suc zero)) → B) (np : neg (Path B y (f (inl (inr star))))) : (x : Fin (suc zero)) → neg (Path B y (f (inl x))) = split inl x → λ_. x inr s → ind-Unit ( λx. neg (Path B y (f (inl (inr x))))) np s has-decidable-equality/is-finite/decide'/z (B : U) (y : B) (f : Fin (suc (suc zero)) → B) : Coprod (Path B y (f (inl (inr star)))) (neg (Path B y (f (inl (inr star))))) → Coprod (Σ (Fin (suc zero)) (λx. Path B y (f (inl x)))) ((x : Fin (suc zero)) → neg (Path B y (f (inl x)))) = split inl p → inl (inr star, p) inr np → inr (has-decidable-equality/is-finite/decide'/z' B y f np) has-decidable-equality/is-finite/decide' (B : U) (y : B) (Heq : has-decidable-equality B) : (k : Nat) → (f : Fin (suc (suc k)) → B) → Coprod (Σ (Fin (suc k)) (λx. Path B y (f (inl x)))) ((x : Fin (suc k)) → neg (Path B y (f (inl x)))) = split zero → λf. has-decidable-equality/is-finite/decide'/z B y f (Heq y (f (inl (inr star)))) suc k → λf. has-decidable-equality/is-finite/decide/s B y (suc k) (λx. f (inl x)) ( has-decidable-equality/is-finite/decide' B y Heq k (λx. f (inl x))) ( Heq y (f (inl (inr star)))) has-decidable-equality/is-finite/decide (B : U) (y : B) (Heq : has-decidable-equality B) : (k : Nat) → (f : Fin (suc k) → B) → Coprod (Σ (Fin k) (λx. Path B y (f (inl x)))) ((x : Fin k) → neg (Path B y (f (inl x)))) = split zero → λ_. inr (λx _. x) suc k → has-decidable-equality/is-finite/decide' B y Heq k
1.15.2 Inductive case
Now, there are two cases for the inductive case. If we can find an x : Fin k such that (f (inr star)) = (f (inl x)), then we can directly conclude by induction hypothesis: the function is still surjective while removing the last element. Otherwise, we need to build a subtype X such that B ≅ X + 1 such that, morally, we put in X all the elements of B that are not f (inr star). Such an X can be built as follows: consider P the subtype of B defined as: P(y) :≡ y ≠ f(inr *). Thus, let X :≡ Σy: B P(y).
has-decidable-equality/is-finite/subtype (k : Nat) (B : U) (f : Fin (suc k) → B) : U = Σ B (λy. neg (Path B y (f (inr star))))
Let us build a back-and-forth map between B and X + 1.
1.15.3 Maps
has-decidable-equality/is-finite/map' (k : Nat) (B : U) (f : Fin (suc k) → B) (y : B) : Coprod (Path B y (f (inr star))) (neg (Path B y (f (inr star)))) → Maybe (has-decidable-equality/is-finite/subtype k B f) = split inl _ → inr star inr np → inl (y, np) has-decidable-equality/is-finite/map (k : Nat) (B : U) (f : Fin (suc k) → B) (H : has-decidable-equality B) (y : B) : Maybe (has-decidable-equality/is-finite/subtype k B f) = has-decidable-equality/is-finite/map' k B f y ( H y (f (inr star))) has-decidable-equality/is-finite/inv-map (k : Nat) (B : U) (f : Fin (suc k) → B) (H : has-decidable-equality B) : Maybe (has-decidable-equality/is-finite/subtype k B f) → B = split inl t → t.1 inr _ → f (inr star)
1.15.4 Right homotopy
We show that the inverse map is a right inverse of the map.
lock Coprod/Eq/map has-decidable-equality/is-finite/right-htpy/inl (k : Nat) (B : U) (f : Fin (suc k) → B) (H : has-decidable-equality B) (t : has-decidable-equality/is-finite/subtype k B f) : (u : Coprod (Path B t.1 (f (inr star))) (neg (Path B t.1 (f (inr star))))) → Path (Coprod (Path B t.1 (f (inr star))) (neg (Path B t.1 (f (inr star))))) (H t.1 (f (inr star))) u → Path (Maybe (has-decidable-equality/is-finite/subtype k B f)) (has-decidable-equality/is-finite/map k B f H t.1) (inl t) = split inl p → λ_. ex-falso ( Path ( Maybe (has-decidable-equality/is-finite/subtype k B f)) ( has-decidable-equality/is-finite/map k B f H t.1) ( inl t)) ( t.2 p) inr np → λp. comp ( Maybe (has-decidable-equality/is-finite/subtype k B f)) ( has-decidable-equality/is-finite/map k B f H t.1) ( has-decidable-equality/is-finite/map' k B f t.1 (inr np)) ( ap ( Coprod (Path B t.1 (f (inr star))) (neg (Path B t.1 (f (inr star))))) ( Maybe (has-decidable-equality/is-finite/subtype k B f)) ( has-decidable-equality/is-finite/map' k B f t.1) ( H t.1 (f (inr star))) (inr np) p) ( inl t) ( Coprod/Eq/map ( has-decidable-equality/is-finite/subtype k B f) Unit ( inl (t.1, np)) ( inl t) ( SgPath-prop B ( λy. neg (Path B y (f (inr star)))) ( λy. Pi/is-prop ( Path B y (f (inr star))) ( λ_. Empty/Prop)) ( t.1, np) t ( refl B t.1))) has-decidable-equality/is-finite/right-htpy/inr (k : Nat) (B : U) (f : Fin (suc k) → B) (H : has-decidable-equality B) : (u : Coprod (Path B (f (inr star)) (f (inr star))) (neg (Path B (f (inr star)) (f (inr star))))) → Path (Coprod (Path B (f (inr star)) (f (inr star))) (neg (Path B (f (inr star)) (f (inr star))))) (H (f (inr star)) (f (inr star))) u → Path (Maybe (has-decidable-equality/is-finite/subtype k B f)) (has-decidable-equality/is-finite/map k B f H (f (inr star))) (inr star) = split inl p → λq. ap ( Coprod (Path B (f (inr star)) (f (inr star))) (neg (Path B (f (inr star)) (f (inr star))))) ( Maybe (has-decidable-equality/is-finite/subtype k B f)) ( has-decidable-equality/is-finite/map' k B f (f (inr star))) ( H (f (inr star)) (f (inr star))) ( inl p) q inr np → λ_. ex-falso ( Path ( Maybe (has-decidable-equality/is-finite/subtype k B f)) ( has-decidable-equality/is-finite/map k B f H (f (inr star))) ( inr star)) ( np (refl B (f (inr star)))) has-decidable-equality/is-finite/right-htpy (k : Nat) (B : U) (f : Fin (suc k) → B) (H : has-decidable-equality B) : (u : Maybe (has-decidable-equality/is-finite/subtype k B f)) → Path (Maybe (has-decidable-equality/is-finite/subtype k B f)) (has-decidable-equality/is-finite/map k B f H (has-decidable-equality/is-finite/inv-map k B f H u)) u = split inl t → has-decidable-equality/is-finite/right-htpy/inl k B f H t ( H t.1 (f (inr star))) ( refl (Coprod (Path B t.1 (f (inr star))) (neg (Path B t.1 (f (inr star))))) (H t.1 (f (inr star)))) inr s → ind-Unit ( λx. Path (Maybe (has-decidable-equality/is-finite/subtype k B f)) (has-decidable-equality/is-finite/map k B f H (f (inr star))) (inr x)) ( has-decidable-equality/is-finite/right-htpy/inr k B f H ( H (f (inr star)) (f (inr star))) ( refl ( Coprod (Path B (f (inr star)) (f (inr star))) (neg (Path B (f (inr star)) (f (inr star))))) ( H (f (inr star)) (f (inr star))))) s
1.15.5 Left homotopy
We show that the inverse map is a left inverse to the map.
has-decidable-equality/is-finite/left-htpy' (k : Nat) (B : U) (f : Fin (suc k) → B) (H : has-decidable-equality B) (y : B) : (u : Coprod (Path B y (f (inr star))) (neg (Path B y (f (inr star))))) → Path (Coprod (Path B y (f (inr star))) (neg (Path B y (f (inr star))))) (H y (f (inr star))) u → Path B (has-decidable-equality/is-finite/inv-map k B f H (has-decidable-equality/is-finite/map k B f H y)) y = split inl p → λq. comp B ( has-decidable-equality/is-finite/inv-map k B f H ( has-decidable-equality/is-finite/map k B f H y)) ( has-decidable-equality/is-finite/inv-map k B f H ( has-decidable-equality/is-finite/map' k B f y (inl p))) ( ap ( Coprod (Path B y (f (inr star))) (neg (Path B y (f (inr star))))) B ( λu. has-decidable-equality/is-finite/inv-map k B f H ( has-decidable-equality/is-finite/map' k B f y u)) ( H y (f (inr star))) ( inl p) q) y (inv B y (f (inr star)) p) inr np → λq. ap ( Coprod (Path B y (f (inr star))) (neg (Path B y (f (inr star))))) B ( λu. has-decidable-equality/is-finite/inv-map k B f H ( has-decidable-equality/is-finite/map' k B f y u)) ( H y (f (inr star))) ( inr np) q has-decidable-equality/is-finite/left-htpy (k : Nat) (B : U) (f : Fin (suc k) → B) (H : has-decidable-equality B) (y : B) : Path B (has-decidable-equality/is-finite/inv-map k B f H (has-decidable-equality/is-finite/map k B f H y)) y = has-decidable-equality/is-finite/left-htpy' k B f H y ( H y (f (inr star))) ( refl ( Coprod (Path B y (f (inr star))) (neg (Path B y (f (inr star))))) ( H y (f (inr star))))
1.15.6 Equivalence
Thus, there is an equivalence between B and X + 1.
has-decidable-equality/is-finite/Equiv (k : Nat) (B : U) (f : Fin (suc k) → B) (H : has-decidable-equality B) : Equiv B (Maybe (has-decidable-equality/is-finite/subtype k B f)) = has-inverse/Equiv B ( Maybe (has-decidable-equality/is-finite/subtype k B f)) ( has-decidable-equality/is-finite/map k B f H) ( has-decidable-equality/is-finite/inv-map k B f H, ( has-decidable-equality/is-finite/right-htpy k B f H, has-decidable-equality/is-finite/left-htpy k B f H))
1.15.7 Decidable equality
Of course, if B has a decidable equality, X also has a decidable equality as the equality between two elements of X is equivalent to the equality between two elements of B.
has-decidable-equality/is-finite/subtype-has-dec-eq' (k : Nat) (B : U) (f : Fin (suc k) → B) (H : has-decidable-equality B) (t u : has-decidable-equality/is-finite/subtype k B f) : Coprod (Path B t.1 u.1) (neg (Path B t.1 u.1)) → Coprod (Path (has-decidable-equality/is-finite/subtype k B f) t u) (neg (Path (has-decidable-equality/is-finite/subtype k B f) t u)) = split inl p → inl ( SgPath-prop B ( λy. neg (Path B y (f (inr star)))) ( λy. Pi/is-prop ( Path B y (f (inr star))) ( λ_. Empty/Prop)) t u p) inr np → inr (λp. np (Sg-path/left B (λy. neg (Path B y (f (inr star)))) t u p)) has-decidable-equality/is-finite/subtype-has-dec-eq (k : Nat) (B : U) (f : Fin (suc k) → B) (H : has-decidable-equality B) : has-decidable-equality (has-decidable-equality/is-finite/subtype k B f) = λt u. has-decidable-equality/is-finite/subtype-has-dec-eq' k B f H t u ( H t.1 u.1)
1.15.8 Result
It is now time to prove the result. First, we write the formalization of the inductive case.
has-decidable-equality/is-finite/is-surj'' (k : Nat) (B : U) (f : Fin (suc k) → B) (y : B) (np : neg (Path B y (f (inr star)))) : (x : Fin (suc k)) → Path B y (f x) → Fib (Fin k) B (λx'. f (inl x')) y = split inr s → ind-Unit ( λx. Path B y (f (inr x)) → ( Fib (Fin k) B (λx'. f (inl x')) y)) ( λq. ex-falso ( Fib (Fin k) B (λx. f (inl x)) y) ( np q)) s inl x → λp. (x, p) has-decidable-equality/is-finite/is-surj' (k : Nat) (B : U) (f : Fin (suc k) → B) (is-surj-f : is-surj (Fin (suc k)) B f) (y : B) (x : Fin k) (p : Path B (f (inr star)) (f (inl x))) : Coprod (Path B y (f (inr star))) (neg (Path B y (f (inr star)))) → Prop-trunc (Fib (Fin k) B (λx'. f (inl x')) y) = split inl q → Prop-trunc/unit (x, comp B y (f (inr star)) q (f (inl x)) p) inr np → rec-Prop-trunc ( Fib (Fin (suc k)) B f y) ( Prop-trunc/Prop (Fib (Fin k) B (λx'. f (inl x')) y)) ( λt. Prop-trunc/unit ( has-decidable-equality/is-finite/is-surj'' k B f y np t.1 t.2)) ( is-surj-f y) has-decidable-equality/is-finite/is-surj (k : Nat) (B : U) (H : has-decidable-equality B) (f : Fin (suc k) → B) (is-surj-f : is-surj (Fin (suc k)) B f) (x : Fin k) (p : Path B (f (inr star)) (f (inl x))) : is-surj (Fin k) B (λx'. f (inl x')) = λy. has-decidable-equality/is-finite/is-surj' k B f is-surj-f y x p (H y (f (inr star))) has-decidable-equality/is-finite/ind-map (k : Nat) (B : U) (f : Fin (suc k) → B) (h : (x : Fin k) → neg (Path B (f (inr star)) (f (inl x)))) (x : Fin k) : has-decidable-equality/is-finite/subtype k B f = (f (inl x), (λp. h x (inv B (f (inl x)) (f (inr star)) p))) has-decidable-equality/is-finite/is-surj/o (k : Nat) (B : U) (f : Fin (suc k) → B) (y : B) (np : neg (Path B y (f (inr star)))) (h : (x : Fin k) → neg (Path B (f (inr star)) (f (inl x)))) : (x : Fin (suc k)) → Path B y (f x) → Fib (Fin k) (has-decidable-equality/is-finite/subtype k B f) (has-decidable-equality/is-finite/ind-map k B f h) (y, np) = split inr s → ind-Unit ( λx. Path B y (f (inr x)) → Fib (Fin k) (has-decidable-equality/is-finite/subtype k B f) (has-decidable-equality/is-finite/ind-map k B f h) (y, np)) ( λq. ex-falso ( Fib (Fin k) (has-decidable-equality/is-finite/subtype k B f) (has-decidable-equality/is-finite/ind-map k B f h) (y, np)) ( np q)) s inl x → λq. ( x, SgPath-prop B ( λz. neg (Path B z (f (inr star)))) ( λz. Pi/is-prop ( Path B z (f (inr star))) ( λ_. Empty/Prop)) ( y, np) ( has-decidable-equality/is-finite/ind-map k B f h x) q) has-decidable-equality/is-finite' (k : Nat) (B : U) (H : has-decidable-equality B) (f : Fin (suc k) → B) (is-surj-f : is-surj (Fin (suc k)) B f) (IH : (B' : U) (H' : has-decidable-equality B') (f' : Fin k → B') → is-surj (Fin k) B' f' → is-finite B') : Coprod (Σ (Fin k) (λx. Path B (f (inr star)) (f (inl x)))) ((x : Fin k) → neg (Path B (f (inr star)) (f (inl x)))) → is-finite B = split inl t → IH B H (λx. f (inl x)) ( has-decidable-equality/is-finite/is-surj k B H f is-surj-f t.1 t.2) inr h → let g : Fin k → has-decidable-equality/is-finite/subtype k B f = has-decidable-equality/is-finite/ind-map k B f h in is-finite/closed-Equiv B ( Maybe (has-decidable-equality/is-finite/subtype k B f)) ( has-decidable-equality/is-finite/Equiv k B f H) ( is-finite/closed-Coprod ( has-decidable-equality/is-finite/subtype k B f) Unit ( IH ( has-decidable-equality/is-finite/subtype k B f) ( has-decidable-equality/is-finite/subtype-has-dec-eq k B f H) g ( λt. rec-Prop-trunc ( Fib (Fin (suc k)) B f t.1) ( Prop-trunc/Prop ( Fib (Fin k) (has-decidable-equality/is-finite/subtype k B f) g t)) ( λu. Prop-trunc/unit ( has-decidable-equality/is-finite/is-surj/o k B f t.1 t.2 h u.1 u.2)) ( is-surj-f t.1))) ( Unit/is-finite))
Then, we can prove the result for Fin k.
has-decidable-equality/Fin-is-finite : (k : Nat) (B : U) (H : has-decidable-equality B) (f : Fin k → B) (is-surj-f : is-surj (Fin k) B f) → is-finite B = split zero → λB H f is-surj-f. count/is-finite B (has-decidable-equality/is-finite/base B f is-surj-f) suc k → λB H f is-surj-f. has-decidable-equality/is-finite' k B H f is-surj-f ( has-decidable-equality/Fin-is-finite k) ( has-decidable-equality/is-finite/decide B (f (inr star)) H k f)
As we prove a property, it holds for any finite type.
has-decidable-equality/is-finite-codomain (A B : U) (is-finite-A : is-finite A) (H : has-decidable-equality B) (f : A → B) (is-surj-f : is-surj A B f) : is-finite B = rec-Prop-trunc ( count A) ( is-finite/Prop B) ( λc. let k : Nat = number-of-elements A c e : Equiv (Fin k) A = count/Equiv A c g : Fin k → B = λx. f (Equiv/map (Fin k) A e x) in has-decidable-equality/Fin-is-finite c.1 B H g ( λy. rec-Prop-trunc ( Fib A B f y) ( Prop-trunc/Prop (Fib (Fin k) B g y)) ( λt. Prop-trunc/unit ( ( Equiv/inv-map (Fin k) A e t.1), ( comp B y (f t.1) t.2 ( f (Equiv/map (Fin k) A e (Equiv/inv-map (Fin k) A e t.1))) ( ap A B f t.1 (Equiv/map (Fin k) A e (Equiv/inv-map (Fin k) A e t.1)) ( inv A (Equiv/map (Fin k) A e (Equiv/inv-map (Fin k) A e t.1)) t.1 (Equiv/inv-right-htpy (Fin k) A e t.1)))))) ( is-surj-f y))) ( is-finite-A)
1.15.9 Unlock
unlock Coprod/Eq/map
1.15.10 Another proof
The above proof is a bit complex and does not compute well. We try to give another proof of that fact here.
is-surjective/is-finite-codomain (A B : U) (H : is-finite A) (Heq : has-decidable-equality B) (f : A → B) (H' : is-surj A B f) : is-finite B = let is-finite-F : (y : B) → is-finite (Fib A B f y) = ( λy. is-finite/closed-Σ A ( λx. Path B y (f x)) H ( λx. is-decidable/is-finite ( Path B y (f x)) ( hedberg B Heq y (f x)) ( Heq y (f x)))) is-finite-BF : is-finite (Σ B (Fib A B f)) = ( is-finite/closed-Equiv ( Σ B (Fib A B f)) A ( equiv-total-fib/Equiv A B f) H) in rec-Prop-trunc ( (y : B) → Fib A B f y) ( is-finite/Prop B) ( λh. is-finite-Sg/is-finite-base B ( Fib A B f) h ( is-finite-F) ( is-finite-BF)) ( finite-choice B ( Fib A B f) Heq ( is-finite-BF) ( is-finite-F) ( H'))
1.16 It is decidable to know whether a finite type is contractible or not
is-contr/is-finite-is-decidable/neg-Path (A : U) (a : A) (k : Nat) (e : Equiv (Fin (suc (suc k))) A) (h : (x : A) → Path A a x) : Coprod (Path (Fin (suc (suc k))) (inr star) (Equiv/inv-map (Fin (suc (suc k))) A e a)) (neg (Path (Fin (suc (suc k))) (inr star) (Equiv/inv-map (Fin (suc (suc k))) A e a))) → Σ A (λx. neg (Path A a x)) = split inl p → let x : A = Equiv/map (Fin (suc (suc k))) A e (inl (inr star)) in ( x, λq. Fin/is-path-is-Eq (suc (suc k)) ( inr star) ( inl (inr star)) ( comp-n ( Fin (suc (suc k))) three-Nat ( inr star) ( Equiv/inv-map (Fin (suc (suc k))) A e a) p ( Equiv/inv-map (Fin (suc (suc k))) A e x) ( ap A (Fin (suc (suc k))) (Equiv/inv-map (Fin (suc (suc k))) A e) a x q) ( inl (inr star)) ( Equiv/inv-left-htpy (Fin (suc (suc k))) A e (inl (inr star))))) inr f → let x : A = Equiv/map (Fin (suc (suc k))) A e (inr star) in ( x, λq. f (comp ( Fin (suc (suc k))) (inr star) ( Equiv/inv-map (Fin (suc (suc k))) A e x) ( inv ( Fin (suc (suc k))) ( Equiv/inv-map (Fin (suc (suc k))) A e x) ( inr star) ( Equiv/inv-left-htpy (Fin (suc (suc k))) A e (inr star))) ( Equiv/inv-map (Fin (suc (suc k))) A e a) ( ap A (Fin (suc (suc k))) (Equiv/inv-map (Fin (suc (suc k))) A e) x a ( inv A a x q)))) is-contr/is-finite-is-decidable/s (A : U) : (k : Nat) → Equiv (Fin (suc k)) A → is-decidable (is-contr A) = split zero → λe. inl (is-contr/is-contr-equiv' (Fin one-Nat) A e (Fin/fin-one-is-contr)) suc k → λe. inr (λt. let u : Σ A (λx. neg (Path A t.1 x)) = ( is-contr/is-finite-is-decidable/neg-Path A t.1 k e t.2 ( Fin/decidable-eq ( suc (suc k)) ( inr star) ( Equiv/inv-map (Fin (suc (suc k))) A e t.1))) in u.2 (t.2 u.1)) is-contr/is-finite-is-decidable' (A : U) : (k : Nat) → Equiv (Fin k) A → is-decidable (is-contr A) = split zero → λe. inr (λt. Equiv/inv-map (Fin zero) A e t.1) suc k → is-contr/is-finite-is-decidable/s A k is-contr/is-finite-is-decidable (A : U) : is-finite A → is-decidable (is-contr A) = rec-Prop-trunc ( count A) ( is-decidable/Prop ( is-contr A) ( is-contr/is-prop A)) ( λc. is-contr/is-finite-is-decidable' A (number-of-elements A c) (count/Equiv A c))
1.17 The number of equivalences between finite types are finite
Indeed, being contractible is a proposition. Moreover, the fibration is finite as it has a counting. As we prove a proposition, we can get a counting for A, and B is a set that has decidable equality, hence the equality type of B has a counting.
is-finite/is-finite-Equiv (A B : U) (HA : is-finite A) (HB : is-finite B) : is-finite (Equiv A B) = rec-Prop-trunc ( count A) ( is-finite/Prop (Equiv A B)) ( λcA. rec-Prop-trunc ( count B) ( is-finite/Prop (Equiv A B)) ( λcB. is-finite/closed-Sg ( A → B) ( is-equiv A B) ( is-finite/Pi A ( λ_. B) HA ( λ_. HB)) ( λf. is-finite/Pi B ( λy. is-contr (Fib A B f y)) HB ( λy. is-decidable/is-finite ( is-contr (Fib A B f y)) ( is-contr/is-prop (Fib A B f y)) ( is-contr/is-finite-is-decidable ( Fib A B f y) ( count/is-finite ( Fib A B f y) ( count/closed-Σ A ( λx. Path B y (f x)) cA ( λx. count/is-decidable-is-countable ( Path B y (f x)) ( count/is-set B cB y (f x)) ( count/has-decidable-eq B cB y (f x))))))))) HB) HA