Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
issig.Defined.(** Note that the sigma over cardinalities is not truncated. Nevertheless, because canonical finite sets of different cardinalities are not isomorphic, being finite is still an hprop. (Thus, we could have truncated the sigma and gotten an equivalent definition, but it would be less convenient to reason about.) *)
X: Type
IsHProp (Finite X)
X: Type
IsHProp (Finite X)
X: Type
IsHProp {n : nat & merely (X <~> Fin n)}
X: Type n, m: nat Hn: merely (X <~> Fin n) Hm: merely (X <~> Fin m)
n = m
X: Type n, m: nat Hm: X <~> Fin m Hn: X <~> Fin n
n = m
exact (nat_eq_fin_equiv n m (Hm oE Hn^-1)).Defined.(** ** Preservation of finiteness by equivalences *)
X, Y: Type e: X -> Y H: IsEquiv e
Finite X -> Finite Y
X, Y: Type e: X -> Y H: IsEquiv e
Finite X -> Finite Y
X, Y: Type e: X -> Y H: IsEquiv e X0: Finite X
Finite Y
X, Y: Type e: X -> Y H: IsEquiv e X0: Finite X
merely (Y <~> Fin (fcard X))
X, Y: Type e: X -> Y H: IsEquiv e X0: Finite X f: X <~> Fin (fcard X)
merely (Y <~> Fin (fcard X))
X, Y: Type e: X -> Y H: IsEquiv e X0: Finite X f: X <~> Fin (fcard X)
Y <~> Fin (fcard X)
exact (equiv_compose f e^-1).Defined.Definitionfinite_equiv'X {Y} (e : X <~> Y)
: Finite X -> Finite Y
:= finite_equiv X e.
X, Y: Type e: X -> Y H: IsEquiv e H0: Finite X H1: Finite Y
fcard X = fcard Y
X, Y: Type e: X -> Y H: IsEquiv e H0: Finite X H1: Finite Y
fcard X = fcard Y
X, Y: Type e: X -> Y H: IsEquiv e H0: Finite X H1: Finite Y
fcard X = fcard Y
X, Y: Type e: X -> Y H: IsEquiv e H0: Finite X H1: Finite Y
fcard Y = fcard Y
X, Y: Type e: X -> Y H: IsEquiv e H0: Finite X H1: Finite Y
fcard X = fcard Y
reflexivity.
X, Y: Type e: X -> Y H: IsEquiv e H0: Finite X H1: Finite Y
fcard Y = fcard Y
exact (ap (@fcard Y) (path_ishprop _ _)).Defined.Definitionfcard_equiv' {XY} (e : X <~> Y)
`{Finite X} `{Finite Y}
: fcard X = fcard Y
:= fcard_equiv e.(** ** Simple examples of finite sets *)(** Canonical finite sets are finite *)Instancefinite_finn : Finite (Fin n)
:= Build_Finite _ n (tr (equiv_idmap _)).(** This includes the empty set. *)Instancefinite_empty : Finite Empty
:= finite_fin 0.(** The unit type is finite, since it's equivalent to [Fin 1]. *)
Finite Unit
Finite Unit
Empty + Unit <~> Unit
apply sum_empty_l.Defined.(** Thus, any contractible type is finite. *)Instancefinite_contrX `{Contr X} : Finite X
:= finite_equiv Unit equiv_contr_unit^-1 _.(** Any decidable hprop is finite, since it must be equivalent to [Empty] or [Unit]. *)
X: Type IsHProp0: IsHProp X H: Decidable X
Finite X
X: Type IsHProp0: IsHProp X H: Decidable X
Finite X
X: Type IsHProp0: IsHProp X H: Decidable X x: X
Finite X
X: Type IsHProp0: IsHProp X H: Decidable X nx: ~ X
Finite X
X: Type IsHProp0: IsHProp X H: Decidable X x: X
Finite X
X: Type IsHProp0: IsHProp X H: Decidable X x: X X0: Contr X
Finite X
exact _.
X: Type IsHProp0: IsHProp X H: Decidable X nx: ~ X
Finite X
refine (finite_equiv Empty nx^-1 _).Defined.#[export]
Hint Immediate finite_decidable_hprop : typeclass_instances.(** It follows that the propositional truncation of any finite set is finite. *)
X: Type fX: Finite X
Finite (merely X)
X: Type fX: Finite X
Finite (merely X)
(** As in decidable_finite_hprop, we case on cardinality first to avoid needing funext. *)
X: Type e: merely (X <~> Fin 0)
Decidable (merely X)
X: Type n: nat e: merely (X <~> Fin n.+1)
Decidable (merely X)
X: Type e: merely (X <~> Fin 0)
Decidable (merely X)
X: Type e: merely (X <~> Fin 0)
~ merely X
intros x; strip_truncations; exact (e x).
X: Type n: nat e: merely (X <~> Fin n.+1)
Decidable (merely X)
X: Type n: nat e: merely (X <~> Fin n.+1)
merely X
strip_truncations; exact (tr (e^-1 (inr tt))).Defined.(** Finite sets are closed under path-spaces. *)
X: Type H: Finite X x, y: X
Finite (x = y)
X: Type H: Finite X x, y: X
Finite (x = y)
(** If we assume [Funext], then typeclass inference produces this automatically, since [X] has decidable equality and (hence) is a set, so [x=y] is a decidable hprop. But we can also deduce it without funext, since [Finite] is an hprop even without funext. *)
X: Type H: Finite X x, y: X e: merely (X <~> Fin (fcard X))
Finite (x = y)
X: Type H: Finite X x, y: X e: X <~> Fin (fcard X)
Finite (x = y)
X: Type H: Finite X x, y: X e: X <~> Fin (fcard X)
Finite (e x = e y)
apply finite_decidable_hprop; exact _.Defined.(** Finite sets are also closed under successors. *)
X: Type H: Finite X
Finite (X + Unit)
X: Type H: Finite X
Finite (X + Unit)
X: Type H: Finite X
merely (X + Unit <~> Fin (fcard X).+1)
X: Type H: Finite X X0: merely (X <~> Fin (fcard X))
H: Funext X: Type H0: Finite X e: merely (X <~> Fin (fcard X))
DecidablePaths X
H: Funext X: Type H0: Finite X e: X <~> Fin (fcard X)
DecidablePaths X
exact (decidablepaths_equiv _ e^-1 _).Defined.(** However, contrary to what you might expect, we cannot assert that "every finite set is decidable"! That would be claiming a *uniform* way to select an element from every nonempty finite set, which contradicts univalence. *)(** One thing we can prove is that any finite hprop is decidable. *)
X: Type IsHProp0: IsHProp X fX: Finite X
Decidable X
X: Type IsHProp0: IsHProp X fX: Finite X
Decidable X
(** To avoid having to use [Funext], we case on the cardinality of [X] before stripping the truncation from its equivalence to [Fin n]; if we did things in the other order then we'd have to know that [Decidable X] is an hprop, which requires funext. *)
X: Type IsHProp0: IsHProp X e: merely (X <~> Fin 0)
Decidable X
X: Type IsHProp0: IsHProp X n: nat e: merely (X <~> Fin n.+1)
Decidable X
X: Type IsHProp0: IsHProp X e: merely (X <~> Fin 0)
Decidable X
X: Type IsHProp0: IsHProp X e: merely (X <~> Fin 0) x: X
Empty
strip_truncations; exact (e x).
X: Type IsHProp0: IsHProp X n: nat e: merely (X <~> Fin n.+1)
Decidable X
X: Type IsHProp0: IsHProp X n: nat e: merely (X <~> Fin n.+1)
X
strip_truncations; exact (e^-1 (inr tt)).Defined.(** It follows that if [X] is finite, then its propositional truncation is decidable. *)
X: Type fX: Finite X
Decidable (merely X)
X: Type fX: Finite X
Decidable (merely X)
exact _.Defined.(** From this, it follows that any finite set is *merely* decidable. *)
X: Type H: Finite X
merely (Decidable X)
X: Type H: Finite X
merely (Decidable X)
apply O_decidable; exact _.Defined.(** ** Induction over finite sets *)(** Most concrete applications of this don't actually require univalence, but the general version does. For this reason the general statement is less useful (and less used in the sequel) than it might be. *)
H: Univalence P: forallX : Type, Finite X -> Type H0: forall (X : Type) (fX : Finite X),
IsHProp (P X fX) f0: P Empty finite_empty fs: forall (X : Type) (fX : Finite X),
P X fX -> P (X + Unit)%type (finite_succ X) X: Type H1: Finite X
P X H1
H: Univalence P: forallX : Type, Finite X -> Type H0: forall (X : Type) (fX : Finite X),
IsHProp (P X fX) f0: P Empty finite_empty fs: forall (X : Type) (fX : Finite X),
P X fX -> P (X + Unit)%type (finite_succ X) X: Type H1: Finite X
P X H1
H: Univalence P: forallX : Type, Finite X -> Type H0: forall (X : Type) (fX : Finite X),
IsHProp (P X fX) f0: P Empty finite_empty fs: forall (X : Type) (fX : Finite X),
P X fX -> P (X + Unit)%type (finite_succ X) X: Type H1: Finite X e: merely (X <~> Fin (fcard X))
P X H1
H: Univalence P: forallX : Type, Finite X -> Type H0: forall (X : Type) (fX : Finite X),
IsHProp (P X fX) f0: P Empty finite_empty fs: forall (X : Type) (fX : Finite X),
P X fX -> P (X + Unit)%type (finite_succ X) X: Type H1: Finite X e: X <~> Fin (fcard X)
P X H1
H: Univalence P: forallX : Type, Finite X -> Type H0: forall (X : Type) (fX : Finite X),
IsHProp (P X fX) f0: P Empty finite_empty fs: forall (X : Type) (fX : Finite X),
P X fX -> P (X + Unit)%type (finite_succ X) X: Type H1: Finite X e: X <~> Fin (fcard X) p: P (Fin (fcard X)) (finite_fin (fcard X)) ->
P X
(transport Finite (path_universe e^-1)
(finite_fin (fcard X)))
P X H1
H: Univalence P: forallX : Type, Finite X -> Type H0: forall (X : Type) (fX : Finite X),
IsHProp (P X fX) f0: P Empty finite_empty fs: forall (X : Type) (fX : Finite X),
P X fX -> P (X + Unit)%type (finite_succ X) X: Type H1: Finite X e: X <~> Fin (fcard X) p: P (Fin (fcard X)) (finite_fin (fcard X)) ->
P X
(transport Finite (path_universe e^-1)
(finite_fin (fcard X)))
P (Fin (fcard X)) (finite_fin (fcard X))
H: Univalence P: forallX : Type, Finite X -> Type H0: forall (X : Type) (fX : Finite X),
IsHProp (P X fX) f0: P Empty finite_empty fs: forall (X : Type) (fX : Finite X),
P X fX -> P (X + Unit)%type (finite_succ X) X: Type H1: Finite X e: X <~> Fin (fcard X) p: P (Fin (fcard X)) (finite_fin (fcard X)) ->
P X
(transport Finite (path_universe e^-1)
(finite_fin (fcard X))) n: nat
P (Fin n) (finite_fin n)
H: Univalence P: forallX : Type, Finite X -> Type H0: forall (X : Type) (fX : Finite X),
IsHProp (P X fX) f0: P Empty finite_empty fs: forall (X : Type) (fX : Finite X),
P X fX -> P (X + Unit)%type (finite_succ X) X: Type H1: Finite X e: X <~> Fin (fcard X) p: P (Fin (fcard X)) (finite_fin (fcard X)) ->
P X
(transport Finite (path_universe e^-1)
(finite_fin (fcard X)))
P (Fin 0) (finite_fin 0)
H: Univalence P: forallX : Type, Finite X -> Type H0: forall (X : Type) (fX : Finite X),
IsHProp (P X fX) f0: P Empty finite_empty fs: forall (X : Type) (fX : Finite X),
P X fX -> P (X + Unit)%type (finite_succ X) X: Type H1: Finite X e: X <~> Fin (fcard X) p: P (Fin (fcard X)) (finite_fin (fcard X)) ->
P X
(transport Finite (path_universe e^-1)
(finite_fin (fcard X))) n: nat IH: P (Fin n) (finite_fin n)
P (Fin n.+1) (finite_fin n.+1)
H: Univalence P: forallX : Type, Finite X -> Type H0: forall (X : Type) (fX : Finite X),
IsHProp (P X fX) f0: P Empty finite_empty fs: forall (X : Type) (fX : Finite X),
P X fX -> P (X + Unit)%type (finite_succ X) X: Type H1: Finite X e: X <~> Fin (fcard X) p: P (Fin (fcard X)) (finite_fin (fcard X)) ->
P X
(transport Finite (path_universe e^-1)
(finite_fin (fcard X)))
P (Fin 0) (finite_fin 0)
exact f0.
H: Univalence P: forallX : Type, Finite X -> Type H0: forall (X : Type) (fX : Finite X),
IsHProp (P X fX) f0: P Empty finite_empty fs: forall (X : Type) (fX : Finite X),
P X fX -> P (X + Unit)%type (finite_succ X) X: Type H1: Finite X e: X <~> Fin (fcard X) p: P (Fin (fcard X)) (finite_fin (fcard X)) ->
P X
(transport Finite (path_universe e^-1)
(finite_fin (fcard X))) n: nat IH: P (Fin n) (finite_fin n)
P (Fin n.+1) (finite_fin n.+1)
exact (transport (P (Fin n.+1)) (path_ishprop _ _) (fs _ _ IH)).Defined.(** ** The finite axiom of choice, and projectivity *)
X: Type H: Finite X
HasChoice X
X: Type H: Finite X
HasChoice X
X: Type H: Finite X P: X -> Type f: forallx : X, merely (P x)
merely (forallx : X, P x)
X: Type H: Finite X P: X -> Type f: forallx : X, merely (P x) e: merely (X <~> Fin (fcard X))
merely (forallx : X, P x)
X: Type H: Finite X P: X -> Type f: forallx : X, merely (P x) e: X <~> Fin (fcard X)
merely (forallx : X, P x)
X: Type H: Finite X P: X -> Type f: forallx : X, merely (P x) e: X <~> Fin (fcard X) P':= P o e^-1: Fin (fcard X) -> Type
merely (forallx : X, P x)
X: Type H: Finite X P: X -> Type f: forallx : X, merely (P x) e: X <~> Fin (fcard X) P':= P o e^-1: Fin (fcard X) -> Type f': forallx : Fin (fcard X), merely (P' x)
merely (forallx : X, P x)
X: Type H: Finite X P: X -> Type f: forallx : X, merely (P x) e: X <~> Fin (fcard X) P':= P o e^-1: Fin (fcard X) -> Type f': forallx : Fin (fcard X), merely (P' x)
(forallx : Fin (fcard X), P' x) -> forallx : X, P x
X: Type H: Finite X P: X -> Type f: forallx : X, merely (P x) e: X <~> Fin (fcard X) P':= P o e^-1: Fin (fcard X) -> Type f': forallx : Fin (fcard X), merely (P' x)
Tr (-1) (forallx : Fin (fcard X), P' x)
X: Type H: Finite X P: X -> Type f: forallx : X, merely (P x) e: X <~> Fin (fcard X) P':= P o e^-1: Fin (fcard X) -> Type f': forallx : Fin (fcard X), merely (P' x)
(forallx : Fin (fcard X), P' x) -> forallx : X, P x
intros g x; exact (eissect e x # g (e x)).
X: Type H: Finite X P: X -> Type f: forallx : X, merely (P x) e: X <~> Fin (fcard X) P':= P o e^-1: Fin (fcard X) -> Type f': forallx : Fin (fcard X), merely (P' x)
Tr (-1) (forallx : Fin (fcard X), P' x)
X: Type H: Finite X P': Fin (fcard X) -> Type f': forallx : Fin (fcard X), merely (P' x)
Tr (-1) (forallx : Fin (fcard X), P' x)
X: Type H: Finite X n: nat P: Fin n -> Type f: forallx : Fin n, merely (P x)
Tr (-1) (forallx : Fin n, P x)
X: Type H: Finite X P: Fin 0 -> Type f: forallx : Fin 0, merely (P x)
Tr (-1) (forallx : Fin 0, P x)
X: Type H: Finite X n: nat P: Fin n.+1 -> Type f: forallx : Fin n.+1, merely (P x) IH: forallP : Fin n -> Type,
(forallx : Fin n, merely (P x)) ->
Tr (-1) (forallx : Fin n, P x)
Tr (-1) (forallx : Fin n.+1, P x)
X: Type H: Finite X P: Fin 0 -> Type f: forallx : Fin 0, merely (P x)
Tr (-1) (forallx : Fin 0, P x)
exact (tr (Empty_ind P)).
X: Type H: Finite X n: nat P: Fin n.+1 -> Type f: forallx : Fin n.+1, merely (P x) IH: forallP : Fin n -> Type,
(forallx : Fin n, merely (P x)) ->
Tr (-1) (forallx : Fin n, P x)
Tr (-1) (forallx : Fin n.+1, P x)
X: Type H: Finite X n: nat P: Fin n.+1 -> Type f: forallx : Fin n.+1, merely (P x) IH: Tr (-1) (forallx : Fin n, (P o inl) x)
Tr (-1) (forallx : Fin n.+1, P x)
X: Type H: Finite X n: nat P: Fin n.+1 -> Type f: forallx : Fin n.+1, merely (P x) IH: Tr (-1) (forallx : Fin n, (P o inl) x) e: merely (P (inr tt))
Tr (-1) (forallx : Fin n.+1, P x)
X: Type H: Finite X n: nat P: Fin n.+1 -> Type f: forallx : Fin n.+1, merely (P x) e: P (inr tt) IH: forallx : Fin n, P (inl x)
Tr (-1) (forallx : Fin n.+1, P x)
exact (tr (sum_ind P IH (Unit_ind e))).Defined.
n: nat
IsProjective (Fin n)
n: nat
IsProjective (Fin n)
n: nat
HasChoice (Fin n)
exact finite_choice.Defined.(** ** Constructions on finite sets *)(** Finite sets are closed under sums, products, function spaces, and equivalence spaces. There are multiple choices we could make regarding how to prove these facts. Since we know what the cardinalities ought to be in all cases (since we know how to add, multiply, exponentiate, and take factorials of natural numbers), we could specify those off the bat, and then reduce to the case of canonical finite sets. However, it's more amusing to instead prove finiteness of these constructions by "finite-set induction", and then *deduce* that their cardinalities are given by the corresponding operations on natural numbers (because they satisfy the same recurrences). *)(** *** Binary sums *)
X, Y: Type H: Finite X H0: Finite Y
Finite (X + Y)
X, Y: Type H: Finite X H0: Finite Y
Finite (X + Y)
X, Y: Type H: Finite X H0: Finite Y e: merely (Y <~> Fin (fcard Y))
Finite (X + Y)
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y)
Finite (X + Y)
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y)
Finite (X + Fin (fcard Y))
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y) n: nat
Finite (X + Fin n)
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y)
Finite (X + Fin 0)
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y) n: nat IH: Finite (X + Fin n)
Finite (X + Fin n.+1)
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y)
Finite (X + Fin 0)
exact (finite_equiv _ (sum_empty_r X)^-1 _).
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y) n: nat IH: Finite (X + Fin n)
Finite (X + Fin n.+1)
exact (finite_equiv _ (equiv_sum_assoc X _ Unit) _).Defined.(** Note that the cardinality function [fcard] actually computes. The same will be true of all the other proofs in this section, though we don't always verify it. *)
fcard (Fin 3 + Fin 4) = 7
reflexivity.Abort.
X, Y: Type H: Finite X H0: Finite Y
fcard (X + Y) = fcard X + fcard Y
X, Y: Type H: Finite X H0: Finite Y
fcard (X + Y) = fcard X + fcard Y
X, Y: Type H: Finite X H0: Finite Y
fcard (X + Y) = fcard Y + fcard X
X, Y: Type H: Finite X H0: Finite Y e: merely (Y <~> Fin (fcard Y))
fcard (X + Y) = fcard Y + fcard X
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y)
fcard (X + Y) = fcard Y + fcard X
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y)
fcard (X + Fin (fcard Y)) = fcard Y + fcard X
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y)
fcard (X + Fin (fcard Y)) =
fcard (Fin (fcard Y)) + fcard X
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y) n: nat
fcard (X + Fin n) = fcard (Fin n) + fcard X
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y)
fcard (X + Fin 0) = fcard (Fin 0) + fcard X
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y) n: nat IH: fcard (X + Fin n) = fcard (Fin n) + fcard X
fcard (X + Fin n.+1) = fcard (Fin n.+1) + fcard X
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y)
fcard (X + Fin 0) = fcard (Fin 0) + fcard X
exact (fcard_equiv (sum_empty_r X)^-1).
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y) n: nat IH: fcard (X + Fin n) = fcard (Fin n) + fcard X
fcard (X + Fin n.+1) = fcard (Fin n.+1) + fcard X
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y) n: nat IH: fcard (X + Fin n) = fcard (Fin n) + fcard X
fcard
(X +
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n + Unit) = fcard (Fin n.+1) + fcard X
exact (ap S IH).Defined.(** *** Binary products *)
X, Y: Type H: Finite X H0: Finite Y
Finite (X * Y)
X, Y: Type H: Finite X H0: Finite Y
Finite (X * Y)
X, Y: Type H: Finite X H0: Finite Y e: merely (Y <~> Fin (fcard Y))
Finite (X * Y)
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y)
Finite (X * Y)
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y)
Finite (X * Fin (fcard Y))
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y) n: nat
Finite (X * Fin n)
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y)
Finite (X * Fin 0)
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y) n: nat IH: Finite (X * Fin n)
Finite (X * Fin n.+1)
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y)
Finite (X * Fin 0)
refine (finite_equiv _ (prod_empty_r X)^-1 _).
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y) n: nat IH: Finite (X * Fin n)
Finite (X * Fin n.+1)
X, Y: Type H: Finite X H0: Finite Y e: Y <~> Fin (fcard Y) n: nat IH: Finite (X * Fin n)
X, Y: Type H: Finite X H0: Finite Y e: X <~> Fin (fcard X) n: nat
fcard (Fin n * Y) = fcard (Fin n) * fcard Y
X, Y: Type H: Finite X H0: Finite Y e: X <~> Fin (fcard X)
fcard (Fin 0 * Y) = fcard (Fin 0) * fcard Y
X, Y: Type H: Finite X H0: Finite Y e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n * Y) = fcard (Fin n) * fcard Y
fcard (Fin n.+1 * Y) = fcard (Fin n.+1) * fcard Y
X, Y: Type H: Finite X H0: Finite Y e: X <~> Fin (fcard X)
fcard (Fin 0 * Y) = fcard (Fin 0) * fcard Y
refine (fcard_equiv (prod_empty_l Y)).
X, Y: Type H: Finite X H0: Finite Y e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n * Y) = fcard (Fin n) * fcard Y
fcard (Fin n.+1 * Y) = fcard (Fin n.+1) * fcard Y
X, Y: Type H: Finite X H0: Finite Y e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n * Y) = fcard (Fin n) * fcard Y
fcard (Fin n * Y + Unit * Y) =
fcard (Fin n.+1) * fcard Y
X, Y: Type H: Finite X H0: Finite Y e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n * Y) = fcard (Fin n) * fcard Y
fcard (Fin n * Y) + fcard (Unit * Y) =
fcard (Fin n.+1) * fcard Y
X, Y: Type H: Finite X H0: Finite Y e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n * Y) = fcard (Fin n) * fcard Y
fcard (Fin n * Y) + fcard (Unit * Y) =
fcard Y + n * fcard Y
X, Y: Type H: Finite X H0: Finite Y e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n * Y) = fcard (Fin n) * fcard Y
fcard (Fin n * Y) + fcard (Unit * Y) =
n * fcard Y + fcard Y
X, Y: Type H: Finite X H0: Finite Y e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n * Y) = fcard (Fin n) * fcard Y
fcard (Fin n * Y) = n * fcard Y
X, Y: Type H: Finite X H0: Finite Y e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n * Y) = fcard (Fin n) * fcard Y
fcard (Unit * Y) = fcard Y
X, Y: Type H: Finite X H0: Finite Y e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n * Y) = fcard (Fin n) * fcard Y
fcard (Fin n * Y) = n * fcard Y
exact IH.
X, Y: Type H: Finite X H0: Finite Y e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n * Y) = fcard (Fin n) * fcard Y
fcard (Unit * Y) = fcard Y
apply fcard_equiv', prod_unit_l.Defined.(** *** Function types *)(** Finite sets are closed under function types, and even dependent function types. *)
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x)
Finite (forallx : X, Y x)
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x)
Finite (forallx : X, Y x)
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) e: merely (X <~> Fin (fcard X))
Finite (forallx : X, Y x)
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) e: X <~> Fin (fcard X)
Finite (forallx : X, Y x)
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) e: X <~> Fin (fcard X)
forallb : X,
(funx : Fin (fcard X) => Y (e^-1 x)) (e b) <~> Y b
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) e: X <~> Fin (fcard X)
Finite
(foralla : Fin (fcard X),
(funx : Fin (fcard X) => Y (e^-1 x)) a)
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) e: X <~> Fin (fcard X)
forallb : X,
(funx : Fin (fcard X) => Y (e^-1 x)) (e b) <~> Y b
intros x; refine (equiv_transport _ (eissect e x)).
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) e: X <~> Fin (fcard X)
Finite
(foralla : Fin (fcard X),
(funx : Fin (fcard X) => Y (e^-1 x)) a)
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) e: X <~> Fin (fcard X) Y':= Y o e^-1: Fin (fcard X) -> Type
Finite (forallx : Fin (fcard X), Y' x)
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) Y': Fin (fcard X) -> Type X0: forallx : Fin (fcard X), Finite (Y' x)
Finite (forallx : Fin (fcard X), Y' x)
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) n: nat Y': Fin n -> Type X0: forallx : Fin n, Finite (Y' x)
Finite (forallx : Fin n, Y' x)
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) Y': Fin 0 -> Type X0: forallx : Fin 0, Finite (Y' x)
Finite (forallx : Fin 0, Y' x)
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) n: nat Y': Fin n.+1 -> Type X0: forallx : Fin n.+1, Finite (Y' x) IH: forallY' : Fin n -> Type,
(forallx : Fin n, Finite (Y' x)) ->
Finite (forallx : Fin n, Y' x)
Finite (forallx : Fin n.+1, Y' x)
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) Y': Fin 0 -> Type X0: forallx : Fin 0, Finite (Y' x)
Finite (forallx : Fin 0, Y' x)
exact _.
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) n: nat Y': Fin n.+1 -> Type X0: forallx : Fin n.+1, Finite (Y' x) IH: forallY' : Fin n -> Type,
(forallx : Fin n, Finite (Y' x)) ->
Finite (forallx : Fin n, Y' x)
Finite (forallx : Fin n.+1, Y' x)
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) n: nat Y': Fin n.+1 -> Type X0: forallx : Fin n.+1, Finite (Y' x) IH: forallY' : Fin n -> Type,
(forallx : Fin n, Finite (Y' x)) ->
Finite (forallx : Fin n, Y' x)
Finite
((foralla : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n, Y' (inl a)) *
(forallb : Unit, Y' (inr b)))
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) n: nat Y': Fin n.+1 -> Type X0: forallx : Fin n.+1, Finite (Y' x) IH: forallY' : Fin n -> Type,
(forallx : Fin n, Finite (Y' x)) ->
Finite (forallx : Fin n, Y' x)
Finite
(foralla : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n, Y' (inl a))
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) n: nat Y': Fin n.+1 -> Type X0: forallx : Fin n.+1, Finite (Y' x) IH: forallY' : Fin n -> Type,
(forallx : Fin n, Finite (Y' x)) ->
Finite (forallx : Fin n, Y' x)
Finite (forallb : Unit, Y' (inr b))
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) n: nat Y': Fin n.+1 -> Type X0: forallx : Fin n.+1, Finite (Y' x) IH: forallY' : Fin n -> Type,
(forallx : Fin n, Finite (Y' x)) ->
Finite (forallx : Fin n, Y' x)
Finite
(foralla : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n, Y' (inl a))
apply IH; exact _.
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) n: nat Y': Fin n.+1 -> Type X0: forallx : Fin n.+1, Finite (Y' x) IH: forallY' : Fin n -> Type,
(forallx : Fin n, Finite (Y' x)) ->
Finite (forallx : Fin n, Y' x)
Finite (forallb : Unit, Y' (inr b))
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) n: nat Y': Fin n.+1 -> Type X0: forallx : Fin n.+1, Finite (Y' x) IH: forallY' : Fin n -> Type,
(forallx : Fin n, Finite (Y' x)) ->
Finite (forallx : Fin n, Y' x)
IsEquiv (Unit_ind (A:=funu : Unit => Y' (inr u)))
refine (isequiv_unit_ind (Y' o inr)).Defined.#[local] Hint Extern4 => progress (cbv beta iota) : typeclass_instances.
H: Funext X: Type H0: Finite X e: X <~> Fin (fcard X) n: nat
fcard (Fin n <~> Fin n) = factorial n
H: Funext X: Type H0: Finite X e: X <~> Fin (fcard X)
fcard (Fin 0 <~> Fin 0) = factorial 0
H: Funext X: Type H0: Finite X e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n <~> Fin n) = factorial n
fcard (Fin n.+1 <~> Fin n.+1) = factorial n.+1
H: Funext X: Type H0: Finite X e: X <~> Fin (fcard X)
fcard (Fin 0 <~> Fin 0) = factorial 0
reflexivity.
H: Funext X: Type H0: Finite X e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n <~> Fin n) = factorial n
fcard (Fin n.+1 <~> Fin n.+1) = factorial n.+1
H: Funext X: Type H0: Finite X e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n <~> Fin n) = factorial n
fcard (Fin n.+1 * (Fin n <~> Fin n)) = factorial n.+1
H: Funext X: Type H0: Finite X e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n <~> Fin n) = factorial n
fcard (Fin n.+1) * fcard (Fin n <~> Fin n) =
factorial n.+1
H: Funext X: Type H0: Finite X e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n <~> Fin n) = factorial n
fcard (Fin n.+1) = n.+1
H: Funext X: Type H0: Finite X e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n <~> Fin n) = factorial n
fcard (Fin n <~> Fin n) =
(fix factorial (n : nat) : nat :=
match n with
| 0 => 1
| n0.+1 => n0.+1 * factorial n0
end) n
H: Funext X: Type H0: Finite X e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n <~> Fin n) = factorial n
fcard (Fin n.+1) = n.+1
reflexivity.
H: Funext X: Type H0: Finite X e: X <~> Fin (fcard X) n: nat IH: fcard (Fin n <~> Fin n) = factorial n
fcard (Fin n <~> Fin n) =
(fix factorial (n : nat) : nat :=
match n with
| 0 => 1
| n0.+1 => n0.+1 * factorial n0
end) n
assumption.Defined.(** [fcard] still computes: *)
forallfs : Funext, fcard (Fin 4 <~> Fin 4) = 24
reflexivity.Abort.(** ** Finite sums of natural numbers *)(** Perhaps slightly less obviously, finite sets are also closed under sigmas. *)
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x)
Finite {x : X & Y x}
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x)
Finite {x : X & Y x}
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) e: merely (X <~> Fin (fcard X))
Finite {x : X & Y x}
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) e: X <~> Fin (fcard X)
Finite {x : X & Y x}
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) e: X <~> Fin (fcard X)
Finite {x : Fin (fcard X) & Y (e^-1 x)}
(** Unfortunately, because [compose] is currently beta-expanded, [set (Y' := Y o e^-1)] doesn't change the goal. *)
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) e: X <~> Fin (fcard X) Y':= funx : Fin (fcard X) => Y (e^-1 x): Fin (fcard X) -> Type
Finite {x : _ & Y' x}
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) Y': Fin (fcard X) -> Type X0: forallx : Fin (fcard X), Finite (Y' x)
Finite {x : _ & Y' x}
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) n: nat Y': Fin n -> Type X0: forallx : Fin n, Finite (Y' x)
Finite {x : _ & Y' x}
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) Y': Fin 0 -> Type X0: forallx : Fin 0, Finite (Y' x)
Finite {x : _ & Y' x}
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) n: nat Y': Fin n.+1 -> Type X0: forallx : Fin n.+1, Finite (Y' x) IH: forallY' : Fin n -> Type,
(forallx : Fin n, Finite (Y' x)) ->
Finite {x : _ & Y' x}
Finite {x : _ & Y' x}
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) Y': Fin 0 -> Type X0: forallx : Fin 0, Finite (Y' x)
Finite {x : _ & Y' x}
exact (finite_equiv Empty pr1^-1 _).
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) n: nat Y': Fin n.+1 -> Type X0: forallx : Fin n.+1, Finite (Y' x) IH: forallY' : Fin n -> Type,
(forallx : Fin n, Finite (Y' x)) ->
Finite {x : _ & Y' x}
Finite {x : _ & Y' x}
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) n: nat Y': Fin n.+1 -> Type X0: forallx : Fin n.+1, Finite (Y' x) IH: forallY' : Fin n -> Type,
(forallx : Fin n, Finite (Y' x)) ->
Finite {x : _ & Y' x}
Finite
({a : Fin n & Y' (inl a)} + {b : Unit & Y' (inr b)})
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) n: nat Y': Fin n.+1 -> Type X0: forallx : Fin n.+1, Finite (Y' x) IH: forallY' : Fin n -> Type,
(forallx : Fin n, Finite (Y' x)) ->
Finite {x : _ & Y' x}
Finite {a : Fin n & Y' (inl a)}
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) n: nat Y': Fin n.+1 -> Type X0: forallx : Fin n.+1, Finite (Y' x) IH: forallY' : Fin n -> Type,
(forallx : Fin n, Finite (Y' x)) ->
Finite {x : _ & Y' x}
Finite {b : Unit & Y' (inr b)}
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) n: nat Y': Fin n.+1 -> Type X0: forallx : Fin n.+1, Finite (Y' x) IH: forallY' : Fin n -> Type,
(forallx : Fin n, Finite (Y' x)) ->
Finite {x : _ & Y' x}
Finite {a : Fin n & Y' (inl a)}
apply IH; exact _.
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) n: nat Y': Fin n.+1 -> Type X0: forallx : Fin n.+1, Finite (Y' x) IH: forallY' : Fin n -> Type,
(forallx : Fin n, Finite (Y' x)) ->
Finite {x : _ & Y' x}
Finite {b : Unit & Y' (inr b)}
exact (finite_equiv _ (equiv_contr_sigma _)^-1 _).Defined.(** Amusingly, this automatically gives us a way to add up a family of natural numbers indexed by any finite set. (We could of course also define such an operation directly, probably using [merely_ind_hset].) *)Definitionfinadd {X} `{Finite X} (f : X -> nat) : nat
:= fcard { x:X & Fin (f x) }.
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x)
fcard {x : X & Y x} =
finadd (funx : X => fcard (Y x))
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x)
fcard {x : X & Y x} =
finadd (funx : X => fcard (Y x))
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) f:= funx : X => fcard (Y x): X -> nat
fcard {x : X & Y x} = finadd f
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) f:= funx : X => fcard (Y x): X -> nat g:= funx : X =>
merely_equiv_fin (Y x) : merely (Y x <~> Fin (f x)): forallx : X, merely (Y x <~> Fin (f x))
fcard {x : X & Y x} = finadd f
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) f:= funx : X => fcard (Y x): X -> nat g: merely (forallx : X, Y x <~> Fin (f x))
fcard {x : X & Y x} = finadd f
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) f:= funx : X => fcard (Y x): X -> nat g: forallx : X, Y x <~> Fin (f x)
fcard {x : X & Y x} = finadd f
X: Type Y: X -> Type H: Finite X H0: forallx : X, Finite (Y x) f:= funx : X => fcard (Y x): X -> nat g: forallx : X, Y x <~> Fin (f x)
fcard {x : X & Y x} =
fcard {x : X & (funx0 : X => Fin (f x0)) x}
exact (fcard_equiv' (equiv_functor_sigma_id g)).Defined.(** The sum of a finite constant family is the product by its cardinality. *)
X: Type H: Finite X n: nat
finadd (fun_ : X => n) = fcard X * n
X: Type H: Finite X n: nat
finadd (fun_ : X => n) = fcard X * n
X: Type H: Finite X n: nat
finadd (fun_ : X => n) = fcard (X * Fin n)
X: Type H: Finite X n: nat
fcard (X * Fin n) = fcard X * n
X: Type H: Finite X n: nat
finadd (fun_ : X => n) = fcard (X * Fin n)
exact (fcard_equiv' (equiv_sigma_prod0 X (Fin n))).
X: Type H: Finite X n: nat
fcard (X * Fin n) = fcard X * n
exact (fcard_prod X (Fin n)).Defined.(** Closure under sigmas and paths also implies closure under hfibers. *)
X, Y: Type f: X -> Y y: Y H: Finite X H0: Finite Y
Finite (hfiber f y)
X, Y: Type f: X -> Y y: Y H: Finite X H0: Finite Y
Finite (hfiber f y)
exact _.Defined.(** Therefore, the cardinality of the domain of a map between finite sets is the sum of the cardinalities of its hfibers. *)
X, Y: Type f: X -> Y H: Finite X H0: Finite Y
fcard X =
finadd
(funy : Y =>
fcard {x : X & (funx0 : X => f x0 = y) x})
X, Y: Type f: X -> Y H: Finite X H0: Finite Y
fcard X =
finadd
(funy : Y =>
fcard {x : X & (funx0 : X => f x0 = y) x})
X, Y: Type f: X -> Y H: Finite X H0: Finite Y
fcard X = fcard {x : Y & hfiber f x}
exact (fcard_equiv' (equiv_fibration_replacement f)).Defined.(** In particular, the image of a map between finite sets is finite. *)
X, Y: Type H: Finite X H0: Finite Y f: X -> Y
Finite (himage f)
X, Y: Type H: Finite X H0: Finite Y f: X -> Y
Finite (himage f)
exact _.Defined.(** ** Finite products of natural numbers *)(** Similarly, closure of finite sets under [forall] automatically gives us a way to multiply a family of natural numbers indexed by any finite set. Of course, if we defined this explicitly, it wouldn't need funext. *)Definitionfinmult `{Funext} {X} `{Finite X} (f : X -> nat) : nat
:= fcard (forallx:X, Fin (f x)).
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x)
fcard (forallx : X, Y x) =
finmult (funx : X => fcard (Y x))
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x)
fcard (forallx : X, Y x) =
finmult (funx : X => fcard (Y x))
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) f:= funx : X => fcard (Y x): X -> nat
fcard (forallx : X, Y x) = finmult f
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) f:= funx : X => fcard (Y x): X -> nat g:= funx : X =>
merely_equiv_fin (Y x) : merely (Y x <~> Fin (f x)): forallx : X, merely (Y x <~> Fin (f x))
fcard (forallx : X, Y x) = finmult f
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) f:= funx : X => fcard (Y x): X -> nat g: merely (forallx : X, Y x <~> Fin (f x))
fcard (forallx : X, Y x) = finmult f
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) f:= funx : X => fcard (Y x): X -> nat g: forallx : X, Y x <~> Fin (f x)
fcard (forallx : X, Y x) = finmult f
H: Funext X: Type Y: X -> Type H0: Finite X H1: forallx : X, Finite (Y x) f:= funx : X => fcard (Y x): X -> nat g: forallx : X, Y x <~> Fin (f x)
fcard (forallx : X, Y x) =
fcard (forallx : X, (funx0 : X => Fin (f x0)) x)
exact (fcard_equiv' (equiv_functor_forall' (equiv_idmap X) g)).Defined.(** The product of a finite constant family is the exponential by its cardinality. *)
H: Funext X: Type H0: Finite X n: nat
finmult (fun_ : X => n) = nat_pow n (fcard X)
H: Funext X: Type H0: Finite X n: nat
finmult (fun_ : X => n) = nat_pow n (fcard X)
exact (fcard_arrow X (Fin n)).Defined.(** ** Finite subsets *)(** Closure under sigmas implies that a detachable subset of a finite set is finite. *)
X: Type H: Finite X P: X -> Type H0: forallx : X, IsHProp (P x) H1: forallx : X, Decidable (P x)
Finite {x : X & P x}
X: Type H: Finite X P: X -> Type H0: forallx : X, IsHProp (P x) H1: forallx : X, Decidable (P x)
Finite {x : X & P x}
exact _.Defined.(** Conversely, if a subset of a finite set is finite, then it is detachable. We show first that an embedding between finite subsets has detachable image. *)
X, Y: Type H: Finite X H0: Finite Y f: X -> Y IsEmbedding0: IsEmbedding f
forally : Y, Decidable (hfiber f y)
X, Y: Type H: Finite X H0: Finite Y f: X -> Y IsEmbedding0: IsEmbedding f
forally : Y, Decidable (hfiber f y)
X, Y: Type H: Finite X H0: Finite Y f: X -> Y IsEmbedding0: IsEmbedding f y: Y
Decidable (hfiber f y)
X, Y: Type H: Finite X H0: Finite Y f: X -> Y IsEmbedding0: IsEmbedding f y: Y ff: Finite (hfiber f y)
Decidable (hfiber f y)
X, Y: Type H: Finite X H0: Finite Y f: X -> Y IsEmbedding0: IsEmbedding f y: Y e: merely (hfiber f y <~> Fin 0)
Decidable (hfiber f y)
X, Y: Type H: Finite X H0: Finite Y f: X -> Y IsEmbedding0: IsEmbedding f y: Y n: nat e: merely (hfiber f y <~> Fin n.+1)
Decidable (hfiber f y)
X, Y: Type H: Finite X H0: Finite Y f: X -> Y IsEmbedding0: IsEmbedding f y: Y e: merely (hfiber f y <~> Fin 0)
Decidable (hfiber f y)
right; intros u; strip_truncations; exact (e u).
X, Y: Type H: Finite X H0: Finite Y f: X -> Y IsEmbedding0: IsEmbedding f y: Y n: nat e: merely (hfiber f y <~> Fin n.+1)
X: Type H: Finite X P: X -> Type H0: forallx : X, IsHProp (P x) Pf: Finite {x : X & P x}
forallx : X, Decidable (P x)
X: Type H: Finite X P: X -> Type H0: forallx : X, IsHProp (P x) Pf: Finite {x : X & P x}
forallx : X, Decidable (P x)
X: Type H: Finite X P: X -> Type H0: forallx : X, IsHProp (P x) Pf: Finite {x : X & P x} x: X
Decidable (P x)
X: Type H: Finite X P: X -> Type H0: forallx : X, IsHProp (P x) Pf: Finite {x : X & P x} x: X
Decidable (hfiber pr1 x)
X: Type H: Finite X P: X -> Type H0: forallx : X, IsHProp (P x) Pf: Finite {x : X & P x} x: X
Finite {x : _ & P x}
X: Type H: Finite X P: X -> Type H0: forallx : X, IsHProp (P x) Pf: Finite {x : X & P x} x: X
Finite X
X: Type H: Finite X P: X -> Type H0: forallx : X, IsHProp (P x) Pf: Finite {x : X & P x} x: X
IsEmbedding pr1
X: Type H: Finite X P: X -> Type H0: forallx : X, IsHProp (P x) Pf: Finite {x : X & P x} x: X
IsEmbedding pr1
exact (mapinO_pr1 (Tr (-1))). (** Why doesn't Coq find this? *)Defined.(** ** Quotients *)(** The quotient of a finite set by a detachable equivalence relation is finite. *)SectionDecidableQuotients.Context `{Univalence} {X} `{Finite X}
(R : Relation X) `{is_mere_relation X R}
`{Reflexive _ R} `{Transitive _ R} `{Symmetric _ R}
{Rd : forallxy, Decidable (R x y)}.
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y)
Finite (Quotient R)
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y)
Finite (Quotient R)
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) e: merely (X <~> Fin (fcard X))
Finite (Quotient R)
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) e: X <~> Fin (fcard X)
Finite (Quotient R)
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) e: X <~> Fin (fcard X) R':= funxy : Fin (fcard X) => R (e^-1 x) (e^-1 y): Fin (fcard X) -> Fin (fcard X) -> Type
Finite (Quotient R)
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) e: X <~> Fin (fcard X) R':= funxy : Fin (fcard X) => R (e^-1 x) (e^-1 y): Fin (fcard X) -> Fin (fcard X) -> Type X0: is_mere_relation (Fin (fcard X)) R'
Finite (Quotient R)
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) e: X <~> Fin (fcard X) R':= funxy : Fin (fcard X) => R (e^-1 x) (e^-1 y): Fin (fcard X) -> Fin (fcard X) -> Type X0: is_mere_relation (Fin (fcard X)) R' X1: Reflexive R'
Finite (Quotient R)
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) e: X <~> Fin (fcard X) R':= funxy : Fin (fcard X) => R (e^-1 x) (e^-1 y): Fin (fcard X) -> Fin (fcard X) -> Type X0: is_mere_relation (Fin (fcard X)) R' X1: Reflexive R' X2: Symmetric R'
Finite (Quotient R)
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) e: X <~> Fin (fcard X) R':= funxy : Fin (fcard X) => R (e^-1 x) (e^-1 y): Fin (fcard X) -> Fin (fcard X) -> Type X0: is_mere_relation (Fin (fcard X)) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R'
Finite (Quotient R)
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) e: X <~> Fin (fcard X) R':= funxy : Fin (fcard X) => R (e^-1 x) (e^-1 y): Fin (fcard X) -> Fin (fcard X) -> Type X0: is_mere_relation (Fin (fcard X)) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin (fcard X), Decidable (R' x y)
Finite (Quotient R)
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) e: X <~> Fin (fcard X) R':= funxy : Fin (fcard X) => R (e^-1 x) (e^-1 y): Fin (fcard X) -> Fin (fcard X) -> Type X0: is_mere_relation (Fin (fcard X)) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin (fcard X), Decidable (R' x y)
forallab : Fin (fcard X),
R' a b <-> R (e^-1 a) (e^-1 b)
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) e: X <~> Fin (fcard X) R':= funxy : Fin (fcard X) => R (e^-1 x) (e^-1 y): Fin (fcard X) -> Fin (fcard X) -> Type X0: is_mere_relation (Fin (fcard X)) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin (fcard X), Decidable (R' x y)
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) e: X <~> Fin (fcard X) R':= funxy : Fin (fcard X) => R (e^-1 x) (e^-1 y): Fin (fcard X) -> Fin (fcard X) -> Type X0: is_mere_relation (Fin (fcard X)) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin (fcard X), Decidable (R' x y)
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) R': Fin (fcard X) -> Fin (fcard X) -> Type X0: is_mere_relation (Fin (fcard X)) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin (fcard X), Decidable (R' x y)
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) R': Fin 0 -> Fin 0 -> Type X0: is_mere_relation (Fin 0) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin 0, Decidable (R' x y)
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y)
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) R': Fin 0 -> Fin 0 -> Type X0: is_mere_relation (Fin 0) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin 0, Decidable (R' x y)
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) R': Fin 0 -> Fin 0 -> Type X0: is_mere_relation (Fin 0) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin 0, Decidable (R' x y)
Quotient R' -> Empty
exact (Quotient_rec R' _ Empty_rec (funx__ => match x withend)).
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y)
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y) R'':= funxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n =>
R' (inl x) (inl y): (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n ->
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n -> Type
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y) R'':= funxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n =>
R' (inl x) (inl y): (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n ->
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n -> Type X4: is_mere_relation
((fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n) R''
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y) R'':= funxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n =>
R' (inl x) (inl y): (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n ->
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n -> Type X4: is_mere_relation
((fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n) R'' X5: Reflexive R''
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y) R'':= funxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n =>
R' (inl x) (inl y): (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n ->
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n -> Type X4: is_mere_relation
((fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n) R'' X5: Reflexive R'' X6: Symmetric R''
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y) R'':= funxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n =>
R' (inl x) (inl y): (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n ->
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n -> Type X4: is_mere_relation
((fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n) R'' X5: Reflexive R'' X6: Symmetric R'' X7: Transitive R''
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y) R'':= funxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n =>
R' (inl x) (inl y): (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n ->
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n -> Type X4: is_mere_relation
((fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n) R'' X5: Reflexive R'' X6: Symmetric R'' X7: Transitive R'' X8: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n, Decidable (R'' x y)
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y) R'':= funxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n =>
R' (inl x) (inl y): (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n ->
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n -> Type X4: is_mere_relation
((fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n) R'' X5: Reflexive R'' X6: Symmetric R'' X7: Transitive R'' X8: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n, Decidable (R'' x y) inlresp: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n,
R'' x y -> R' (inl x) (inl y)
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y) R'':= funxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n =>
R' (inl x) (inl y): (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n ->
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n -> Type X4: is_mere_relation
((fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n) R'' X5: Reflexive R'' X6: Symmetric R'' X7: Transitive R'' X8: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n, Decidable (R'' x y) inlresp: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n,
R'' x y -> R' (inl x) (inl y) p: merely {x : Fin n & R' (inl x) (inr tt)}
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y) R'':= funxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n =>
R' (inl x) (inl y): (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n ->
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n -> Type X4: is_mere_relation
((fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n) R'' X5: Reflexive R'' X6: Symmetric R'' X7: Transitive R'' X8: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n, Decidable (R'' x y) inlresp: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n,
R'' x y -> R' (inl x) (inl y) np: ~ merely {x : Fin n & R' (inl x) (inr tt)}
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y) R'':= funxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n =>
R' (inl x) (inl y): (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n ->
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n -> Type X4: is_mere_relation
((fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n) R'' X5: Reflexive R'' X6: Symmetric R'' X7: Transitive R'' X8: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n, Decidable (R'' x y) inlresp: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n,
R'' x y -> R' (inl x) (inl y) p: merely {x : Fin n & R' (inl x) (inr tt)}
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y) R'':= funxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n =>
R' (inl x) (inl y): (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n ->
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n -> Type X4: is_mere_relation
((fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n) R'' X5: Reflexive R'' X6: Symmetric R'' X7: Transitive R'' X8: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n, Decidable (R'' x y) inlresp: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n,
R'' x y -> R' (inl x) (inl y) p: {x : Fin n & R' (inl x) (inr tt)}
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y) R'':= funxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n =>
R' (inl x) (inl y): (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n ->
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n -> Type X4: is_mere_relation
((fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n) R'' X5: Reflexive R'' X6: Symmetric R'' X7: Transitive R'' X8: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n, Decidable (R'' x y) inlresp: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n,
R'' x y -> R' (inl x) (inl y) x: Fin n r: R' (inl x) (inr tt)
Finite (Quotient R')
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y) R'':= funxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n =>
R' (inl x) (inl y): (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n ->
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n -> Type X4: is_mere_relation
((fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n) R'' X5: Reflexive R'' X6: Symmetric R'' X7: Transitive R'' X8: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n, Decidable (R'' x y) inlresp: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n,
R'' x y -> R' (inl x) (inl y) x: Fin n r: R' (inl x) (inr tt)
Quotient R'' <~> Quotient R'
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y) R'':= funxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n =>
R' (inl x) (inl y): (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n ->
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n -> Type X4: is_mere_relation
((fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n) R'' X5: Reflexive R'' X6: Symmetric R'' X7: Transitive R'' X8: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n, Decidable (R'' x y) inlresp: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n,
R'' x y -> R' (inl x) (inl y) x: Fin n r: R' (inl x) (inr tt)
IsEquiv (Quotient_functor R'' R' inl inlresp)
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) n: nat IH: forallR' : Fin n -> Fin n -> Type,
is_mere_relation (Fin n) R' ->
Reflexive R' ->
Symmetric R' ->
Transitive R' ->
(forallxy : Fin n, Decidable (R' x y)) ->
Finite (Quotient R') R': Fin n.+1 -> Fin n.+1 -> Type X0: is_mere_relation (Fin n.+1) R' X1: Reflexive R' X2: Symmetric R' X3: Transitive R' R'd: forallxy : Fin n.+1, Decidable (R' x y) R'':= funxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n =>
R' (inl x) (inl y): (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n ->
(fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n -> Type X4: is_mere_relation
((fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n) R'' X5: Reflexive R'' X6: Symmetric R'' X7: Transitive R'' X8: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n, Decidable (R'' x y) inlresp: forallxy : (fix Fin (n : nat) : Type0 :=
match n with
| 0 => Empty
| n0.+1 => (Fin n0 + Unit)%type
end) n,
R'' x y -> R' (inl x) (inl y) x: Fin n r: R' (inl x) (inr tt)
intros; reflexivity.}Defined.(** Therefore, the cardinality of [X] is the sum of the cardinalities of its equivalence classes. *)
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y)
fcard X =
finadd
(funz : Quotient R =>
fcard
{x : X &
(funx0 : X => trunctype_type (in_class R z x0))
x})
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y)
fcard X =
finadd
(funz : Quotient R =>
fcard
{x : X &
(funx0 : X => trunctype_type (in_class R z x0))
x})
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y)
finadd
(funy : Quotient R =>
fcard {x : X & (funx0 : X => class_of R x0 = y) x}) =
finadd
(funz : Quotient R =>
fcard
{x : X &
(funx0 : X => trunctype_type (in_class R z x0))
x})
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y)
forallz : Quotient R,
fcard {x : X & (funx0 : X => class_of R x0 = z) x} =
fcard
{x : X &
(funx0 : X => trunctype_type (in_class R z x0)) x}
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) x: X
fcard
{x0 : X &
(funx1 : X => class_of R x1 = class_of R x) x0} =
fcard {x0 : X & (funx1 : X => R x x1) x0}
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) x: X
{x0 : X & class_of R x0 = class_of R x} <~>
{x0 : X & R x x0}
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) x, y: X
class_of R y = class_of R x <~> R x y
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) x, y: X
R x y <~> class_of R y = class_of R x
H: Univalence X: Type H0: Finite X R: Relation X is_mere_relation0: is_mere_relation X R H1: Reflexive R H2: Transitive R H3: Symmetric R Rd: forallxy : X, Decidable (R x y) x, y: X
R x y <~> R y x
apply equiv_iff_hprop; applysymmetry.Defined.EndDecidableQuotients.(** ** Injections *)(** An injection between finite sets induces an inequality between their cardinalities. *)
X, Y: Type fX: Finite X fY: Finite Y f: X -> Y i: IsEmbedding f
fcard X <= fcard Y
X, Y: Type fX: Finite X fY: Finite Y f: X -> Y i: IsEmbedding f
fcard X <= fcard Y
X, Y: Type fX: Finite X fY: Finite Y f: X -> Y i: IsEmbedding f X0: MapIn (Tr (-1)) f
fcard X <= fcard Y
X, Y: Type fX: Finite X fY: Finite Y f: X -> Y X0: MapIn (Tr (-1)) f
fcard X <= fcard Y
X, Y: Type n: nat e: merely (X <~> Fin n) fY: Finite Y f: X -> Y X0: MapIn (Tr (-1)) f
n <= fcard Y
X, Y: Type n: nat e: merely (X <~> Fin n) m: nat e': merely (Y <~> Fin m) f: X -> Y X0: MapIn (Tr (-1)) f
n <= m
X, Y: Type n, m: nat f: X -> Y X0: MapIn (Tr (-1)) f e': Y <~> Fin m e: X <~> Fin n
n <= m
X, Y: Type n, m: nat f: X -> Y X0: MapIn (Tr (-1)) f e': Y <~> Fin m e: X <~> Fin n g:= e' o f o e^-1: Fin n -> Fin m
n <= m
X, Y: Type n, m: nat f: X -> Y X0: MapIn (Tr (-1)) f e': Y <~> Fin m e: X <~> Fin n g:= e' o f o e^-1: Fin n -> Fin m X1: MapIn (Tr (-1)) g
n <= m
X, Y: Type n, m: nat f: X -> Y X0: MapIn (Tr (-1)) f e': Y <~> Fin m e: X <~> Fin n g: Fin n -> Fin m X1: MapIn (Tr (-1)) g
n <= m
X, Y: Type n, m: nat f: X -> Y X0: MapIn (Tr (-1)) f g: Fin n -> Fin m X1: MapIn (Tr (-1)) g
n <= m
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f
forall (m : nat) (g : Fin n -> Fin m),
MapIn (Tr (-1)) g -> n <= m
X, Y: Type f: X -> Y X0: MapIn (Tr (-1)) f
forall (m : nat) (g : Fin 0 -> Fin m),
MapIn (Tr (-1)) g -> 0 <= m
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m
forall (m : nat) (g : Fin n.+1 -> Fin m),
MapIn (Tr (-1)) g -> n.+1 <= m
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m
forall (m : nat) (g : Fin n.+1 -> Fin m),
MapIn (Tr (-1)) g -> n.+1 <= m
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m X1: MapIn (Tr (-1)) g
n.+1 <= m
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m X1: MapIn (Tr (-1)) g i: IsInjective g
n.+1 <= m
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m g: Fin n.+1 -> Fin 0 X1: MapIn (Tr (-1)) g i: IsInjective g
n.+1 <= 0
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g
n.+1 <= m.+1
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m g: Fin n.+1 -> Fin 0 X1: MapIn (Tr (-1)) g i: IsInjective g
n.+1 <= 0
elim (g (inr tt)).
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g
n.+1 <= m.+1
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1
n.+1 <= m.+1
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h
n.+1 <= m.+1
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h
foralla : Fin n, is_inl (h (inl a))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h Ha: foralla : Fin n, is_inl (h (inl a))
n.+1 <= m.+1
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h
foralla : Fin n, is_inl (h (inl a))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n
is_inl (h (inl a))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n b: Fin m.+1 p: g (inl a) = b
is_inl (h (inl a))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n b: Fin m p: g (inl a) = inl b
is_inl (h (inl a))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n p: g (inl a) = inr tt
is_inl (h (inl a))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n b: Fin m p: g (inl a) = inl b
is_inl (h (inl a))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n b: Fin m p: g (inl a) = inl b
g (inl a) <> g (inr tt)
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n b: Fin m p: g (inl a) = inl b q: g (inl a) <> g (inr tt)
is_inl (h (inl a))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n b: Fin m p: g (inl a) = inl b
g (inl a) <> g (inr tt)
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n b: Fin m p: g (inl a) = inl b r: g (inl a) = g (inr tt)
Empty
exact (inl_ne_inr _ _ (i _ _ r)).
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n b: Fin m p: g (inl a) = inl b q: g (inl a) <> g (inr tt)
is_inl (h (inl a))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n b: Fin m p: g (inl a) = inl b q: g (inr tt) <> inl b
is_inl (h (inl a))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n b: Fin m p: g (inl a) = inl b q: g (inr tt) <> inl b
h (inl a) = inl b
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n b: Fin m p: g (inl a) = inl b q: g (inr tt) <> inl b r: h (inl a) = inl b
is_inl (h (inl a))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n b: Fin m p: g (inl a) = inl b q: g (inr tt) <> inl b
h (inl a) = inl b
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n b: Fin m p: g (inl a) = inl b q: g (inr tt) <> inl b
fin_transpose_last_with m (g (inr tt)) (inl b) =
g (inl a)
exact (fin_transpose_last_with_rest m (g (inr tt)) b q @ p^).
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n b: Fin m p: g (inl a) = inl b q: g (inr tt) <> inl b r: h (inl a) = inl b
is_inl (h (inl a))
rewrite r; exact tt.
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n p: g (inl a) = inr tt
is_inl (h (inl a))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n p: g (inl a) = inr tt
h (inl a) = g (inr tt)
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n p: g (inl a) = inr tt q: h (inl a) = g (inr tt)
is_inl (h (inl a))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n p: g (inl a) = inr tt
h (inl a) = g (inr tt)
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n p: g (inl a) = inr tt
fin_transpose_last_with m (g (inr tt)) (g (inr tt)) =
g (inl a)
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n p: g (inl a) = inr tt q: h (inl a) = g (inr tt)
is_inl (h (inl a))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n p: g (inl a) = inr tt q: h (inl a) = g (inr tt)
is_inl (g (inr tt))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n p: g (inl a) = inr tt q: h (inl a) = g (inr tt) r: is_inr (g (inr tt))
is_inl (g (inr tt))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n p: g (inl a) = inr tt q: h (inl a) = g (inr tt) r: is_inr (g (inr tt)) s: inr (un_inr (g (inr tt)) r) = g (inr tt)
is_inl (g (inr tt))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h a: Fin n p: g (inl a) = inr tt q: h (inl a) = g (inr tt) r: is_inr (g (inr tt)) s: inr tt = g (inr tt)
is_inl (g (inr tt))
elim (inl_ne_inr _ _ (i _ _ (p @ s))).
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h Ha: foralla : Fin n, is_inl (h (inl a))
n.+1 <= m.+1
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h Ha: foralla : Fin n, is_inl (h (inl a))
forallb : Unit, is_inr (h (inr b))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h Ha: foralla : Fin n, is_inl (h (inl a)) Hb: forallb : Unit, is_inr (h (inr b))
n.+1 <= m.+1
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h Ha: foralla : Fin n, is_inl (h (inl a))
forallb : Unit, is_inr (h (inr b))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h Ha: foralla : Fin n, is_inl (h (inl a))
is_inr (h (inr tt))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h Ha: foralla : Fin n, is_inl (h (inl a))
h (inr tt) = inr tt
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h Ha: foralla : Fin n, is_inl (h (inl a)) q: h (inr tt) = inr tt
is_inr (h (inr tt))
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h Ha: foralla : Fin n, is_inl (h (inl a))
h (inr tt) = inr tt
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h Ha: foralla : Fin n, is_inl (h (inl a))
fin_transpose_last_with m (g (inr tt)) (inr tt) =
g (inr tt)
apply fin_transpose_last_with_last.
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h Ha: foralla : Fin n, is_inl (h (inl a)) q: h (inr tt) = inr tt
is_inr (h (inr tt))
rewrite q; exact tt.
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h Ha: foralla : Fin n, is_inl (h (inl a)) Hb: forallb : Unit, is_inr (h (inr b))
n.+1 <= m.+1
X, Y: Type n: nat f: X -> Y X0: MapIn (Tr (-1)) f IHn: forall (m : nat) (g : Fin n -> Fin m), MapIn (Tr (-1)) g -> n <= m m: nat g: Fin n.+1 -> Fin m.+1 X1: MapIn (Tr (-1)) g i: IsInjective g h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1 X2: MapIn (Tr (-1)) h Ha: foralla : Fin n, is_inl (h (inl a)) Hb: forallb : Unit, is_inr (h (inr b))
n <= m
exact (IHn m (unfunctor_sum_l h Ha)
(mapinO_unfunctor_sum_l (Tr (-1)) h Ha Hb)).Qed.(** ** Surjections *)(** A surjection between finite sets induces an inequality between their cardinalities. *)
X, Y: Type fX: Finite X fY: Finite Y f: X -> Y i: IsConnMap (Tr (-1)) f
fcard X >= fcard Y
X, Y: Type fX: Finite X fY: Finite Y f: X -> Y i: IsConnMap (Tr (-1)) f
fcard X >= fcard Y
X, Y: Type n: nat e: merely (X <~> Fin n) m: nat e': merely (Y <~> Fin m) f: X -> Y i: IsConnMap (Tr (-1)) f
n >= m
X, Y: Type n: nat e: merely (X <~> Fin n) m: nat e': merely (Y <~> Fin m) f: X -> Y i: IsConnMap (Tr (-1)) f k: IsProjective (Fin m)
n >= m
X, Y: Type n, m: nat f: X -> Y i: IsConnMap (Tr (-1)) f k: IsProjective (Fin m) e': Y <~> Fin m e: X <~> Fin n
n >= m
X, Y: Type n, m: nat f: X -> Y i: IsConnMap (Tr (-1)) f k: IsProjective (Fin m) e': Y <~> Fin m e: X <~> Fin n g:= e' o f o e^-1: Fin n -> Fin m
n >= m
X, Y: Type n, m: nat f: X -> Y i: IsConnMap (Tr (-1)) f k: IsProjective (Fin m) e': Y <~> Fin m e: X <~> Fin n g:= e' o f o e^-1: Fin n -> Fin m k': IsConnMap (Tr (-1)) g
n >= m
X, Y: Type n, m: nat k: IsProjective (Fin m) e': Y <~> Fin m e: X <~> Fin n g: Fin n -> Fin m k': IsConnMap (Tr (-1)) g
n >= m
X, Y: Type n, m: nat k: IsProjective (Fin m) e': Y <~> Fin m e: X <~> Fin n g: Fin n -> Fin m k': IsConnMap (Tr (-1)) g j: merely {s : Fin m -> Fin n & g o s == idmap}
n >= m
X, Y: Type n, m: nat k: IsProjective (Fin m) e': Y <~> Fin m e: X <~> Fin n g: Fin n -> Fin m k': IsConnMap (Tr (-1)) g j: {s : Fin m -> Fin n &
(funx : Fin m => g (s x)) == idmap}
n >= m
X, Y: Type n, m: nat k: IsProjective (Fin m) e': Y <~> Fin m e: X <~> Fin n g: Fin n -> Fin m k': IsConnMap (Tr (-1)) g s: Fin m -> Fin n is_section: (funx : Fin m => g (s x)) == idmap
n >= m
X, Y: Type n, m: nat k: IsProjective (Fin m) e': Y <~> Fin m e: X <~> Fin n g: Fin n -> Fin m k': IsConnMap (Tr (-1)) g s: Fin m -> Fin n is_section: (funx : Fin m => g (s x)) == idmap
fcard (Fin n) >= m
X, Y: Type n, m: nat k: IsProjective (Fin m) e': Y <~> Fin m e: X <~> Fin n g: Fin n -> Fin m k': IsConnMap (Tr (-1)) g s: Fin m -> Fin n is_section: (funx : Fin m => g (s x)) == idmap
fcard (Fin n) >= fcard (Fin m)
X, Y: Type n, m: nat k: IsProjective (Fin m) e': Y <~> Fin m e: X <~> Fin n g: Fin n -> Fin m k': IsConnMap (Tr (-1)) g s: Fin m -> Fin n is_section: (funx : Fin m => g (s x)) == idmap
IsEmbedding s
apply isembedding_isinj_hset, (isinj_section is_section).Defined.(** ** Enumerations *)(** A function from [nat] to a finite set must repeat itself eventually. *)SectionEnumeration.Context `{Funext} {X} `{Finite@{_ Set _} X} (e : nat -> X).Leter (n : nat) : Fin n -> X
:= funk => e (nat_fin n k).
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat
(IsEmbedding (er n) +
{n : nat & {k : nat & e n = e (n + k).+1}})%type
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat
(IsEmbedding (er n) +
{n : nat & {k : nat & e n = e (n + k).+1}})%type
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X
(IsEmbedding (er 0) +
{n : nat & {k : nat & e n = e (n + k).+1}})%type
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n)
(IsEmbedding (er n.+1) +
{n : nat & {k : nat & e n = e (n + k).+1}})%type
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: {n : nat & {k : nat & e n = e (n + k).+1}}
(IsEmbedding (er n.+1) +
{n : nat & {k : nat & e n = e (n + k).+1}})%type
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X
(IsEmbedding (er 0) +
{n : nat & {k : nat & e n = e (n + k).+1}})%type
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X
IsEmbedding (er 0)
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X x: X
IsHProp (hfiber (er 0) x)
apply hprop_inhabited_contr; intros [[] _].
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n)
(IsEmbedding (er n.+1) +
{n : nat & {k : nat & e n = e (n + k).+1}})%type
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) k: Fin n p: er n k = er n.+1 (inr tt)
(IsEmbedding (er n.+1) +
{n : nat & {k : nat & e n = e (n + k).+1}})%type
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt))
(IsEmbedding (er n.+1) +
{n : nat & {k : nat & e n = e (n + k).+1}})%type
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) k: Fin n p: er n k = er n.+1 (inr tt)
(IsEmbedding (er n.+1) +
{n : nat & {k : nat & e n = e (n + k).+1}})%type
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) k: Fin n p: er n k = er n.+1 (inr tt)
{n : nat & {k : nat & e n = e (n + k).+1}}
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) k: Fin n p: er n k = er n.+1 (inr tt)
{k0 : nat & e (nat_fin n k) = e (nat_fin n k + k0).+1}
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) k: Fin n p: er n k = er n.+1 (inr tt)
e (nat_fin n k) =
e (nat_fin n k + nat_fin_compl n k).+1
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) k: Fin n p: er n k = er n.+1 (inr tt)
e (nat_fin n k) = e n
exact p.
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt))
(IsEmbedding (er n.+1) +
{n : nat & {k : nat & e n = e (n + k).+1}})%type
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt))
IsEmbedding (er n.+1)
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X
IsHProp (hfiber (er n.+1) x)
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X
forallx0y : hfiber (er n.+1) x, x0 = y
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X k, l: hfiber (er n.+1) x
k = l
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X k, l: hfiber (er n.+1) x
k.1 = l.1
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X k: Fin n p: er n.+1 (inl k) = x l: Fin n q: er n.+1 (inl l) = x
inl k = inl l
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X k: Fin n p: er n.+1 (inl k) = x q: er n.+1 (inr tt) = x
inl k = inr tt
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X p: er n.+1 (inr tt) = x l: Fin n q: er n.+1 (inl l) = x
inr tt = inl l
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X p, q: er n.+1 (inr tt) = x
inr tt = inr tt
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X k: Fin n p: er n.+1 (inl k) = x l: Fin n q: er n.+1 (inl l) = x
inl k = inl l
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsInjective (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X k: Fin n p: er n.+1 (inl k) = x l: Fin n q: er n.+1 (inl l) = x
inl k = inl l
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsInjective (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X k: Fin n p: er n.+1 (inl k) = x l: Fin n q: er n.+1 (inl l) = x
k = l
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsInjective (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X k: Fin n p: er n.+1 (inl k) = x l: Fin n q: er n.+1 (inl l) = x
er n k = er n l
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsInjective (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X k: Fin n p: e (nat_fin n.+1 (inl k)) = x l: Fin n q: e (nat_fin n.+1 (inl l)) = x
er n k = er n l
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsInjective (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X k: Fin n p: e (nat_fin n k) = x l: Fin n q: e (nat_fin n l) = x
er n k = er n l
exact (p @ q^).
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X k: Fin n p: er n.+1 (inl k) = x q: er n.+1 (inr tt) = x
inl k = inr tt
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X k: Fin n p: er n.+1 (inl k) = x q: er n.+1 (inr tt) = x
hfiber (er n) (er n.+1 (inr tt))
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X k: Fin n p: er n.+1 (inl k) = x q: er n.+1 (inr tt) = x
er n k = er n.+1 (inr tt)
exact (p @ q^).
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X p: er n.+1 (inr tt) = x l: Fin n q: er n.+1 (inl l) = x
inr tt = inl l
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X p: er n.+1 (inr tt) = x l: Fin n q: er n.+1 (inl l) = x
hfiber (er n) (er n.+1 (inr tt))
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X p: er n.+1 (inr tt) = x l: Fin n q: er n.+1 (inl l) = x
er n l = er n.+1 (inr tt)
exact (q @ p^).
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: IsEmbedding (er n) ne: ~ hfiber (er n) (er n.+1 (inr tt)) x: X p, q: er n.+1 (inr tt) = x
inr tt = inr tt
reflexivity.
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X n: nat IH: {n : nat & {k : nat & e n = e (n + k).+1}}
(IsEmbedding (er n.+1) +
{n : nat & {k : nat & e n = e (n + k).+1}})%type
right; exact IH.Defined.
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X
{n : nat & {k : nat & e n = e (n + k).+1}}
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X
{n : nat & {k : nat & e n = e (n + k).+1}}
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X p: IsEmbedding (er (fcard X).+1)
{n : nat & {k : nat & e n = e (n + k).+1}}
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X s: {n : nat & {k : nat & e n = e (n + k).+1}}
{n : nat & {k : nat & e n = e (n + k).+1}}
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X p: IsEmbedding (er (fcard X).+1)
{n : nat & {k : nat & e n = e (n + k).+1}}
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X p: IsEmbedding (er (fcard X).+1) q: (fcard X).+1 <= fcard X
{n : nat & {k : nat & e n = e (n + k).+1}}
elim (lt_irrefl _ q).
H: Funext X: Type H0: Finite X e: nat -> X er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): foralln : nat, Fin n -> X s: {n : nat & {k : nat & e n = e (n + k).+1}}