Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.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.
(* -*- mode: coq; mode: visual-line -*- *)
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import HFiber. Require Import Factorization. Require Import Truncations. Require Import Colimits.Quotient. Require Import Projective. Require Import Fin. Local Open Scope path_scope. Local Open Scope nat_scope. (** ** Definition of general finite sets *) Class Finite (X : Type) := { fcard : nat ; merely_equiv_fin : merely (X <~> Fin fcard) }. Arguments fcard X {_}. Arguments merely_equiv_fin X {_}.
X: Type

{n : nat & merely (X <~> Fin n)} <~> Finite X
X: Type

{n : nat & merely (X <~> Fin n)} <~> Finite X
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
refine (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. Definition finite_equiv' X {Y} (e : X <~> Y) : Finite X -> Finite Y := finite_equiv X e.
X, Y: Type

X <~> Y -> Finite X <~> Finite Y
X, Y: Type

X <~> Y -> Finite X <~> Finite Y
intros ?; apply equiv_iff_hprop; apply finite_equiv'; [ assumption | symmetry; assumption ]. Defined.
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. Definition fcard_equiv' {X Y} (e : X <~> Y) `{Finite X} `{Finite Y} : fcard X = fcard Y := fcard_equiv e. (** ** Simple examples of finite sets *) (** Canonical finite sets are finite *) Global Instance finite_fin n : Finite (Fin n) := Build_Finite _ n (tr (equiv_idmap _)). (** This includes the empty set. *) Global Instance finite_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. *) Global Instance finite_contr X `{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))

merely (X + Unit <~> Fin (fcard X).+1)
X: Type
H: Finite X
X0: X <~> Fin (fcard X)

X + Unit <~> Fin (fcard X).+1
refine (_ +E 1); assumption. Defined. Definition fcard_succ X `{Finite X} : fcard (X + Unit) = (fcard X).+1 := 1. (** ** Decidability *) (** Like canonical finite sets, finite sets have decidable equality. *)
H: Funext
X: Type
H0: Finite X

DecidablePaths X
H: Funext
X: Type
H0: Finite X

DecidablePaths 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
refine (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: forall X : 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: forall X : 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: forall X : 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: forall X : 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: forall X : 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: forall X : 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: forall X : 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: forall X : 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: forall X : 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: forall X : 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: forall X : 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)
refine (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: forall x : X, merely (P x)

merely (forall x : X, P x)
X: Type
H: Finite X
P: X -> Type
f: forall x : X, merely (P x)
e: merely (X <~> Fin (fcard X))

merely (forall x : X, P x)
X: Type
H: Finite X
P: X -> Type
f: forall x : X, merely (P x)
e: X <~> Fin (fcard X)

merely (forall x : X, P x)
X: Type
H: Finite X
P: X -> Type
f: forall x : X, merely (P x)
e: X <~> Fin (fcard X)
P':= P o e^-1: Fin (fcard X) -> Type

merely (forall x : X, P x)
X: Type
H: Finite X
P: X -> Type
f: forall x : X, merely (P x)
e: X <~> Fin (fcard X)
P':= P o e^-1: Fin (fcard X) -> Type
f': forall x : Fin (fcard X), merely (P' x)

merely (forall x : X, P x)
X: Type
H: Finite X
P: X -> Type
f: forall x : X, merely (P x)
e: X <~> Fin (fcard X)
P':= P o e^-1: Fin (fcard X) -> Type
f': forall x : Fin (fcard X), merely (P' x)

(forall x : Fin (fcard X), P' x) -> forall x : X, P x
X: Type
H: Finite X
P: X -> Type
f: forall x : X, merely (P x)
e: X <~> Fin (fcard X)
P':= P o e^-1: Fin (fcard X) -> Type
f': forall x : Fin (fcard X), merely (P' x)
Tr (-1) (forall x : Fin (fcard X), P' x)
X: Type
H: Finite X
P: X -> Type
f: forall x : X, merely (P x)
e: X <~> Fin (fcard X)
P':= P o e^-1: Fin (fcard X) -> Type
f': forall x : Fin (fcard X), merely (P' x)

(forall x : Fin (fcard X), P' x) -> forall x : X, P x
intros g x; exact (eissect e x # g (e x)).
X: Type
H: Finite X
P: X -> Type
f: forall x : X, merely (P x)
e: X <~> Fin (fcard X)
P':= P o e^-1: Fin (fcard X) -> Type
f': forall x : Fin (fcard X), merely (P' x)

Tr (-1) (forall x : Fin (fcard X), P' x)
X: Type
H: Finite X
P': Fin (fcard X) -> Type
f': forall x : Fin (fcard X), merely (P' x)

Tr (-1) (forall x : Fin (fcard X), P' x)
X: Type
H: Finite X
n: nat
P: Fin n -> Type
f: forall x : Fin n, merely (P x)

Tr (-1) (forall x : Fin n, P x)
X: Type
H: Finite X
P: Fin 0 -> Type
f: forall x : Fin 0, merely (P x)

Tr (-1) (forall x : Fin 0, P x)
X: Type
H: Finite X
n: nat
P: Fin n.+1 -> Type
f: forall x : Fin n.+1, merely (P x)
IH: forall P : Fin n -> Type, (forall x : Fin n, merely (P x)) -> Tr (-1) (forall x : Fin n, P x)
Tr (-1) (forall x : Fin n.+1, P x)
X: Type
H: Finite X
P: Fin 0 -> Type
f: forall x : Fin 0, merely (P x)

Tr (-1) (forall x : Fin 0, P x)
exact (tr (Empty_ind P)).
X: Type
H: Finite X
n: nat
P: Fin n.+1 -> Type
f: forall x : Fin n.+1, merely (P x)
IH: forall P : Fin n -> Type, (forall x : Fin n, merely (P x)) -> Tr (-1) (forall x : Fin n, P x)

Tr (-1) (forall x : Fin n.+1, P x)
X: Type
H: Finite X
n: nat
P: Fin n.+1 -> Type
f: forall x : Fin n.+1, merely (P x)
IH: Tr (-1) (forall x : Fin n, (P o inl) x)

Tr (-1) (forall x : Fin n.+1, P x)
X: Type
H: Finite X
n: nat
P: Fin n.+1 -> Type
f: forall x : Fin n.+1, merely (P x)
IH: Tr (-1) (forall x : Fin n, (P o inl) x)
e: merely (P (inr tt))

Tr (-1) (forall x : Fin n.+1, P x)
X: Type
H: Finite X
n: nat
P: Fin n.+1 -> Type
f: forall x : Fin n.+1, merely (P x)
e: P (inr tt)
IH: forall x : Fin n, P (inl x)

Tr (-1) (forall x : 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)
rapply 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)
refine (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)
refine (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
refine (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)

Finite (X * Unit)
refine (finite_equiv _ (prod_unit_r X)^-1 _). Defined.
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
e: merely (X <~> Fin (fcard X))

fcard (X * Y) = fcard X * fcard Y
X, Y: Type
H: Finite X
H0: Finite Y
e: X <~> Fin (fcard X)

fcard (X * Y) = fcard X * fcard Y
X, Y: Type
H: Finite X
H0: Finite Y
e: X <~> Fin (fcard X)

fcard (Fin (fcard X) * Y) = fcard X * fcard Y
X, Y: Type
H: Finite X
H0: Finite Y
e: X <~> Fin (fcard X)

fcard (Fin (fcard X) * Y) = fcard (Fin (fcard X)) * fcard Y
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
apply 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: forall x : X, Finite (Y x)

Finite (forall x : X, Y x)
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)

Finite (forall x : X, Y x)
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
e: merely (X <~> Fin (fcard X))

Finite (forall x : X, Y x)
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
e: X <~> Fin (fcard X)

Finite (forall x : X, Y x)
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
e: X <~> Fin (fcard X)

forall b : X, (fun x : Fin (fcard X) => Y (e^-1 x)) (e b) <~> Y b
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
e: X <~> Fin (fcard X)
Finite (forall a : Fin (fcard X), (fun x : Fin (fcard X) => Y (e^-1 x)) a)
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
e: X <~> Fin (fcard X)

forall b : X, (fun x : 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: forall x : X, Finite (Y x)
e: X <~> Fin (fcard X)

Finite (forall a : Fin (fcard X), (fun x : Fin (fcard X) => Y (e^-1 x)) a)
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
e: X <~> Fin (fcard X)
Y':= Y o e^-1: Fin (fcard X) -> Type

Finite (forall x : Fin (fcard X), Y' x)
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
Y': Fin (fcard X) -> Type
X0: forall x : Fin (fcard X), Finite (Y' x)

Finite (forall x : Fin (fcard X), Y' x)
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
n: nat
Y': Fin n -> Type
X0: forall x : Fin n, Finite (Y' x)

Finite (forall x : Fin n, Y' x)
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
Y': Fin 0 -> Type
X0: forall x : Fin 0, Finite (Y' x)

Finite (forall x : Fin 0, Y' x)
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
n: nat
Y': Fin n.+1 -> Type
X0: forall x : Fin n.+1, Finite (Y' x)
IH: forall Y' : Fin n -> Type, (forall x : Fin n, Finite (Y' x)) -> Finite (forall x : Fin n, Y' x)
Finite (forall x : Fin n.+1, Y' x)
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
Y': Fin 0 -> Type
X0: forall x : Fin 0, Finite (Y' x)

Finite (forall x : Fin 0, Y' x)
exact _.
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
n: nat
Y': Fin n.+1 -> Type
X0: forall x : Fin n.+1, Finite (Y' x)
IH: forall Y' : Fin n -> Type, (forall x : Fin n, Finite (Y' x)) -> Finite (forall x : Fin n, Y' x)

Finite (forall x : Fin n.+1, Y' x)
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
n: nat
Y': Fin n.+1 -> Type
X0: forall x : Fin n.+1, Finite (Y' x)
IH: forall Y' : Fin n -> Type, (forall x : Fin n, Finite (Y' x)) -> Finite (forall x : Fin n, Y' x)

Finite ((forall a : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Y' (inl a)) * (forall b : Unit, Y' (inr b)))
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
n: nat
Y': Fin n.+1 -> Type
X0: forall x : Fin n.+1, Finite (Y' x)
IH: forall Y' : Fin n -> Type, (forall x : Fin n, Finite (Y' x)) -> Finite (forall x : Fin n, Y' x)

Finite (forall a : (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: forall x : X, Finite (Y x)
n: nat
Y': Fin n.+1 -> Type
X0: forall x : Fin n.+1, Finite (Y' x)
IH: forall Y' : Fin n -> Type, (forall x : Fin n, Finite (Y' x)) -> Finite (forall x : Fin n, Y' x)
Finite (forall b : Unit, Y' (inr b))
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
n: nat
Y': Fin n.+1 -> Type
X0: forall x : Fin n.+1, Finite (Y' x)
IH: forall Y' : Fin n -> Type, (forall x : Fin n, Finite (Y' x)) -> Finite (forall x : Fin n, Y' x)

Finite (forall a : (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: forall x : X, Finite (Y x)
n: nat
Y': Fin n.+1 -> Type
X0: forall x : Fin n.+1, Finite (Y' x)
IH: forall Y' : Fin n -> Type, (forall x : Fin n, Finite (Y' x)) -> Finite (forall x : Fin n, Y' x)

Finite (forall b : Unit, Y' (inr b))
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
n: nat
Y': Fin n.+1 -> Type
X0: forall x : Fin n.+1, Finite (Y' x)
IH: forall Y' : Fin n -> Type, (forall x : Fin n, Finite (Y' x)) -> Finite (forall x : Fin n, Y' x)

IsEquiv (Unit_ind (A:=fun u : Unit => Y' (inr u)))
refine (isequiv_unit_ind (Y' o inr)). Defined. #[local] Hint Extern 4 => progress (cbv beta iota) : typeclass_instances.
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y

fcard (forall x : X, (fun _ : X => Y) x) = nat_exp (fcard Y) (fcard X)
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y

fcard (forall x : X, (fun _ : X => Y) x) = nat_exp (fcard Y) (fcard X)
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y
e: merely (X <~> Fin (fcard X))

fcard (forall x : X, (fun _ : X => Y) x) = nat_exp (fcard Y) (fcard X)
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y
e: X <~> Fin (fcard X)

fcard (forall x : X, (fun _ : X => Y) x) = nat_exp (fcard Y) (fcard X)
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y
e: X <~> Fin (fcard X)

fcard (forall x : Fin (fcard X), (fun _ : Fin (fcard X) => Y) x) = nat_exp (fcard Y) (fcard X)
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y
e: X <~> Fin (fcard X)

fcard (forall x : Fin (fcard X), (fun _ : Fin (fcard X) => Y) x) = nat_exp (fcard Y) (fcard X)
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y
e: X <~> Fin (fcard X)
n: nat

fcard (forall x : Fin n, (fun _ : Fin n => Y) x) = nat_exp (fcard Y) n
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y
e: X <~> Fin (fcard X)

fcard (forall x : Fin 0, (fun _ : Fin 0 => Y) x) = nat_exp (fcard Y) 0
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y
e: X <~> Fin (fcard X)
n: nat
IH: fcard (forall x : Fin n, (fun _ : Fin n => Y) x) = nat_exp (fcard Y) n
fcard (forall x : Fin n.+1, (fun _ : Fin n.+1 => Y) x) = nat_exp (fcard Y) n.+1
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y
e: X <~> Fin (fcard X)

fcard (forall x : Fin 0, (fun _ : Fin 0 => Y) x) = nat_exp (fcard Y) 0
reflexivity.
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y
e: X <~> Fin (fcard X)
n: nat
IH: fcard (forall x : Fin n, (fun _ : Fin n => Y) x) = nat_exp (fcard Y) n

fcard (forall x : Fin n.+1, (fun _ : Fin n.+1 => Y) x) = nat_exp (fcard Y) n.+1
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y
e: X <~> Fin (fcard X)
n: nat
IH: fcard (forall x : Fin n, (fun _ : Fin n => Y) x) = nat_exp (fcard Y) n

fcard (((fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n -> Y) * (Unit -> Y)) = nat_exp (fcard Y) n.+1
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y
e: X <~> Fin (fcard X)
n: nat
IH: fcard (forall x : Fin n, (fun _ : Fin n => Y) x) = nat_exp (fcard Y) n

fcard (forall x : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, (fun _ : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n => Y) x) * fcard (forall x : Unit, unit_name Y x) = nat_exp (fcard Y) n.+1
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y
e: X <~> Fin (fcard X)
n: nat
IH: fcard (forall x : Fin n, (fun _ : Fin n => Y) x) = nat_exp (fcard Y) n

fcard (forall x : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, (fun _ : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n => Y) x) = (fix nat_exp (n m : nat) {struct m} : nat := match m with | 0 => 1 | m0.+1 => nat_exp n m0 * n end) (fcard Y) n
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y
e: X <~> Fin (fcard X)
n: nat
IH: fcard (forall x : Fin n, (fun _ : Fin n => Y) x) = nat_exp (fcard Y) n
fcard (forall x : Unit, unit_name Y x) = fcard Y
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y
e: X <~> Fin (fcard X)
n: nat
IH: fcard (forall x : Fin n, (fun _ : Fin n => Y) x) = nat_exp (fcard Y) n

fcard (forall x : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, (fun _ : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n => Y) x) = (fix nat_exp (n m : nat) {struct m} : nat := match m with | 0 => 1 | m0.+1 => nat_exp n m0 * n end) (fcard Y) n
assumption.
H: Funext
X, Y: Type
H0: Finite X
H1: Finite Y
e: X <~> Fin (fcard X)
n: nat
IH: fcard (forall x : Fin n, (fun _ : Fin n => Y) x) = nat_exp (fcard Y) n

fcard (forall x : Unit, unit_name Y x) = fcard Y
refine (fcard_equiv (@Unit_ind (fun (_:Unit) => Y))^-1). Defined. (** [fcard] still computes, despite the funext: *)

forall fs : Funext, fcard (forall x : Fin 3, (fun _ : Fin 3 => Fin 4) x) = 64
reflexivity. Abort. (** *** Automorphism types (i.e. symmetric groups) *)
H: Funext
X: Type
H0: Finite X

Finite (X <~> X)
H: Funext
X: Type
H0: Finite X

Finite (X <~> X)
H: Funext
X: Type
H0: Finite X
e: merely (X <~> Fin (fcard X))

Finite (X <~> X)
H: Funext
X: Type
H0: Finite X
e: X <~> Fin (fcard X)

Finite (X <~> X)
H: Funext
X: Type
H0: Finite X
e: X <~> Fin (fcard X)

Finite (Fin (fcard X) <~> Fin (fcard X))
H: Funext
X: Type
H0: Finite X
e: X <~> Fin (fcard X)
n: nat

Finite (Fin n <~> Fin n)
H: Funext
X: Type
H0: Finite X
e: X <~> Fin (fcard X)

Finite (Fin 0 <~> Fin 0)
H: Funext
X: Type
H0: Finite X
e: X <~> Fin (fcard X)
n: nat
IH: Finite (Fin n <~> Fin n)
Finite (Fin n.+1 <~> Fin n.+1)
H: Funext
X: Type
H0: Finite X
e: X <~> Fin (fcard X)

Finite (Fin 0 <~> Fin 0)
exact _.
H: Funext
X: Type
H0: Finite X
e: X <~> Fin (fcard X)
n: nat
IH: Finite (Fin n <~> Fin n)

Finite (Fin n.+1 <~> Fin n.+1)
refine (finite_equiv _ (equiv_fin_equiv n n) _). Defined.
H: Funext
X: Type
H0: Finite X

fcard (X <~> X) = factorial (fcard X)
H: Funext
X: Type
H0: Finite X

fcard (X <~> X) = factorial (fcard X)
H: Funext
X: Type
H0: Finite X
e: merely (X <~> Fin (fcard X))

fcard (X <~> X) = factorial (fcard X)
H: Funext
X: Type
H0: Finite X
e: X <~> Fin (fcard X)

fcard (X <~> X) = factorial (fcard X)
H: Funext
X: Type
H0: Finite X
e: X <~> Fin (fcard X)

fcard (Fin (fcard X) <~> Fin (fcard X)) = factorial (fcard X)
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: *)

forall fs : 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: forall x : X, Finite (Y x)

Finite {x : X & Y x}
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)

Finite {x : X & Y x}
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)
e: merely (X <~> Fin (fcard X))

Finite {x : X & Y x}
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)
e: X <~> Fin (fcard X)

Finite {x : X & Y x}
X: Type
Y: X -> Type
H: Finite X
H0: forall x : 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: forall x : X, Finite (Y x)
e: X <~> Fin (fcard X)
Y':= fun x : Fin (fcard X) => Y (e^-1 x): Fin (fcard X) -> Type

Finite {x : _ & Y' x}
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)
Y': Fin (fcard X) -> Type
X0: forall x : Fin (fcard X), Finite (Y' x)

Finite {x : _ & Y' x}
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)
n: nat
Y': Fin n -> Type
X0: forall x : Fin n, Finite (Y' x)

Finite {x : _ & Y' x}
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)
Y': Fin 0 -> Type
X0: forall x : Fin 0, Finite (Y' x)

Finite {x : _ & Y' x}
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)
n: nat
Y': Fin n.+1 -> Type
X0: forall x : Fin n.+1, Finite (Y' x)
IH: forall Y' : Fin n -> Type, (forall x : Fin n, Finite (Y' x)) -> Finite {x : _ & Y' x}
Finite {x : _ & Y' x}
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)
Y': Fin 0 -> Type
X0: forall x : Fin 0, Finite (Y' x)

Finite {x : _ & Y' x}
refine (finite_equiv Empty pr1^-1 _).
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)
n: nat
Y': Fin n.+1 -> Type
X0: forall x : Fin n.+1, Finite (Y' x)
IH: forall Y' : Fin n -> Type, (forall x : Fin n, Finite (Y' x)) -> Finite {x : _ & Y' x}

Finite {x : _ & Y' x}
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)
n: nat
Y': Fin n.+1 -> Type
X0: forall x : Fin n.+1, Finite (Y' x)
IH: forall Y' : Fin n -> Type, (forall x : 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: forall x : X, Finite (Y x)
n: nat
Y': Fin n.+1 -> Type
X0: forall x : Fin n.+1, Finite (Y' x)
IH: forall Y' : Fin n -> Type, (forall x : 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: forall x : X, Finite (Y x)
n: nat
Y': Fin n.+1 -> Type
X0: forall x : Fin n.+1, Finite (Y' x)
IH: forall Y' : Fin n -> Type, (forall x : Fin n, Finite (Y' x)) -> Finite {x : _ & Y' x}
Finite {b : Unit & Y' (inr b)}
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)
n: nat
Y': Fin n.+1 -> Type
X0: forall x : Fin n.+1, Finite (Y' x)
IH: forall Y' : Fin n -> Type, (forall x : 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: forall x : X, Finite (Y x)
n: nat
Y': Fin n.+1 -> Type
X0: forall x : Fin n.+1, Finite (Y' x)
IH: forall Y' : Fin n -> Type, (forall x : Fin n, Finite (Y' x)) -> Finite {x : _ & Y' x}

Finite {b : Unit & Y' (inr b)}
refine (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].) *) Definition finadd {X} `{Finite X} (f : X -> nat) : nat := fcard { x:X & Fin (f x) }.
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)

fcard {x : X & Y x} = finadd (fun x : X => fcard (Y x))
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)

fcard {x : X & Y x} = finadd (fun x : X => fcard (Y x))
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)
f:= fun x : X => fcard (Y x): X -> nat

fcard {x : X & Y x} = finadd f
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)
f:= fun x : X => fcard (Y x): X -> nat
g:= fun x : X => merely_equiv_fin (Y x) : merely (Y x <~> Fin (f x)): forall x : X, merely (Y x <~> Fin (f x))

fcard {x : X & Y x} = finadd f
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)
f:= fun x : X => fcard (Y x): X -> nat
g: merely (forall x : X, Y x <~> Fin (f x))

fcard {x : X & Y x} = finadd f
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)
f:= fun x : X => fcard (Y x): X -> nat
g: forall x : X, Y x <~> Fin (f x)

fcard {x : X & Y x} = finadd f
X: Type
Y: X -> Type
H: Finite X
H0: forall x : X, Finite (Y x)
f:= fun x : X => fcard (Y x): X -> nat
g: forall x : X, Y x <~> Fin (f x)

fcard {x : X & Y x} = fcard {x : X & (fun x0 : X => Fin (f x0)) x}
refine (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 (fun y : Y => fcard {x : X & (fun x0 : X => f x0 = y) x})
X, Y: Type
f: X -> Y
H: Finite X
H0: Finite Y

fcard X = finadd (fun y : Y => fcard {x : X & (fun x0 : 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}
refine (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. *) Definition finmult `{Funext} {X} `{Finite X} (f : X -> nat) : nat := fcard (forall x:X, Fin (f x)).
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)

fcard (forall x : X, Y x) = finmult (fun x : X => fcard (Y x))
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)

fcard (forall x : X, Y x) = finmult (fun x : X => fcard (Y x))
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
f:= fun x : X => fcard (Y x): X -> nat

fcard (forall x : X, Y x) = finmult f
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
f:= fun x : X => fcard (Y x): X -> nat
g:= fun x : X => merely_equiv_fin (Y x) : merely (Y x <~> Fin (f x)): forall x : X, merely (Y x <~> Fin (f x))

fcard (forall x : X, Y x) = finmult f
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
f:= fun x : X => fcard (Y x): X -> nat
g: merely (forall x : X, Y x <~> Fin (f x))

fcard (forall x : X, Y x) = finmult f
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
f:= fun x : X => fcard (Y x): X -> nat
g: forall x : X, Y x <~> Fin (f x)

fcard (forall x : X, Y x) = finmult f
H: Funext
X: Type
Y: X -> Type
H0: Finite X
H1: forall x : X, Finite (Y x)
f:= fun x : X => fcard (Y x): X -> nat
g: forall x : X, Y x <~> Fin (f x)

fcard (forall x : X, Y x) = fcard (forall x : X, (fun x0 : X => Fin (f x0)) x)
refine (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_exp n (fcard X)
H: Funext
X: Type
H0: Finite X
n: nat

finmult (fun _ : X => n) = nat_exp n (fcard X)
refine (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: forall x : X, IsHProp (P x)
H1: forall x : X, Decidable (P x)

Finite {x : X & P x}
X: Type
H: Finite X
P: X -> Type
H0: forall x : X, IsHProp (P x)
H1: forall x : 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

forall y : Y, Decidable (hfiber f y)
X, Y: Type
H: Finite X
H0: Finite Y
f: X -> Y
IsEmbedding0: IsEmbedding f

forall y : 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)

Decidable (hfiber f y)
left; strip_truncations; exact (e^-1 (inr tt)). Defined.
X: Type
H: Finite X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Pf: Finite {x : X & P x}

forall x : X, Decidable (P x)
X: Type
H: Finite X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Pf: Finite {x : X & P x}

forall x : X, Decidable (P x)
X: Type
H: Finite X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Pf: Finite {x : X & P x}
x: X

Decidable (P x)
X: Type
H: Finite X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Pf: Finite {x : X & P x}
x: X

Decidable (hfiber pr1 x)
(* The try clause below is only needed for Coq <= 8.11 *)
X: Type
H: Finite X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Pf: Finite {x : X & P x}
x: X

IsEmbedding pr1
X: Type
H: Finite X
P: X -> Type
H0: forall x : X, IsHProp (P x)
Pf: Finite {x : X & P x}
x: X

IsEmbedding pr1
apply (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. *) Section DecidableQuotients. Context `{Univalence} {X} `{Finite X} (R : Relation X) `{is_mere_relation X R} `{Reflexive _ R} `{Transitive _ R} `{Symmetric _ R} {Rd : forall x y, 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: forall x y : 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: forall x y : 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: forall x y : 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: forall x y : 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: forall x y : X, Decidable (R x y)
e: X <~> Fin (fcard X)
R':= fun x y : 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: forall x y : X, Decidable (R x y)
e: X <~> Fin (fcard X)
R':= fun x y : 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: forall x y : X, Decidable (R x y)
e: X <~> Fin (fcard X)
R':= fun x y : 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: forall x y : X, Decidable (R x y)
e: X <~> Fin (fcard X)
R':= fun x y : 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: forall x y : X, Decidable (R x y)
e: X <~> Fin (fcard X)
R':= fun x y : 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: forall x y : X, Decidable (R x y)
e: X <~> Fin (fcard X)
R':= fun x y : 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: forall x y : 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: forall x y : X, Decidable (R x y)
e: X <~> Fin (fcard X)
R':= fun x y : 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: forall x y : Fin (fcard X), Decidable (R' x y)

forall x y : Fin (fcard X), R' x y <-> R (e^-1 x) (e^-1 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: forall x y : X, Decidable (R x y)
e: X <~> Fin (fcard X)
R':= fun x y : 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: forall x y : 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: forall x y : X, Decidable (R x y)
e: X <~> Fin (fcard X)
R':= fun x y : 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: forall x y : 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: forall x y : 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: forall x y : 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: forall x y : 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: forall x y : 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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : 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: forall x y : 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: forall x y : 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: forall x y : 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: forall x y : Fin 0, Decidable (R' x y)

Quotient R' -> Empty
refine (Quotient_rec R' _ Empty_rec (fun x _ _ => match x with end)).
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : 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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)

IsConnMap (Tr (-1)) (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)
IsEmbedding (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)

IsConnMap (Tr (-1)) (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)

forall b : Quotient R', merely (hfiber (Quotient_functor R'' R' inl inlresp) 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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)

forall x : Fin n.+1, merely (hfiber (Quotient_functor R'' R' inl inlresp) (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)
y: Fin n

hfiber (Quotient_functor R'' R' inl inlresp) (class_of R' (inl 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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)
hfiber (Quotient_functor R'' R' inl inlresp) (class_of R' (inr tt))
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)
y: Fin n

hfiber (Quotient_functor R'' R' inl inlresp) (class_of R' (inl y))
exists (class_of R'' y); reflexivity.
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)

hfiber (Quotient_functor R'' R' inl inlresp) (class_of R' (inr tt))
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)

class_of R' (inl x) = class_of R' (inr tt)
apply qglue, 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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)

IsEmbedding (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)
u: Quotient R''

forall x1 : Quotient R'', Quotient_functor R'' R' inl inlresp u = Quotient_functor R'' R' inl inlresp x1 -> u = x1
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)
u: Quotient R''
v: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n

Quotient_functor R'' R' inl inlresp u = Quotient_functor R'' R' inl inlresp (class_of R'' v) -> u = class_of R'' v
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)
v, u: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n

Quotient_functor R'' R' inl inlresp (class_of R'' u) = Quotient_functor R'' R' inl inlresp (class_of R'' v) -> class_of R'' u = class_of R'' v
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)
v, u: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n
q: class_of R' (inl u) = class_of R' (inl v)

class_of R'' u = class_of R'' v
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)
v, u: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n
q: class_of R' (inl u) = class_of R' (inl v)

R' (inl u) (inl v)
exact (related_quotient_paths R' (inl u) (inl v) q).
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}

Quotient R'' + Unit <~> 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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}

IsEquiv (sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))))
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}

IsConnMap (Tr (-1)) (sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))))
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
IsEmbedding (sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))))
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}

IsConnMap (Tr (-1)) (sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))))
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}

forall b : Quotient R', merely (hfiber (sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt)))) 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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}

forall x : Fin n.+1, merely (hfiber (sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt)))) (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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
y: Fin n

hfiber (sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt)))) (class_of R' (inl 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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
hfiber (sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt)))) (class_of R' (inr tt))
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
y: Fin n

hfiber (sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt)))) (class_of R' (inl y))
exists (inl (class_of R'' y)); reflexivity.
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}

hfiber (sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt)))) (class_of R' (inr tt))
exists (inr tt); reflexivity.
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}

IsEmbedding (sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))))
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
u: (Quotient R'' + Unit)%type

forall x1 : Quotient R'' + Unit, sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) u = sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) x1 -> u = x1
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
u: (Quotient R'' + Unit)%type

forall a : Quotient R'', sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) u = sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) (inl a) -> u = inl a
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
u: (Quotient R'' + Unit)%type
forall b : Unit, sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) u = sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) (inr b) -> u = inr 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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
u: (Quotient R'' + Unit)%type

forall a : Quotient R'', sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) u = sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) (inl a) -> u = inl a
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
u: (Quotient R'' + Unit)%type
v: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n

sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) u = sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) (inl (class_of R'' v)) -> u = inl (class_of R'' v)
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
v: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n

forall a : Quotient R'', sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) (inl a) = sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) (inl (class_of R'' v)) -> inl a = inl (class_of R'' v)
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
v: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n
forall b : Unit, sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) (inr b) = sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) (inl (class_of R'' v)) -> inr b = inl (class_of R'' v)
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
v: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n

forall a : Quotient R'', sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) (inl a) = sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) (inl (class_of R'' v)) -> inl a = inl (class_of R'' v)
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
v, u: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n

sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) (inl (class_of R'' u)) = sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) (inl (class_of R'' v)) -> inl (class_of R'' u) = inl (class_of R'' v)
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
v, u: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n
q: class_of R' (inl u) = class_of R' (inl v)

inl (class_of R'' u) = inl (class_of R'' v)
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
v, u: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n
q: class_of R' (inl u) = class_of R' (inl v)

R' (inl u) (inl v)
exact (related_quotient_paths R' (inl u) (inl v) q).
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
v: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n

forall b : Unit, sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) (inr b) = sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) (inl (class_of R'' v)) -> inr b = inl (class_of R'' v)
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
v: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n

class_of R' (inr tt) = class_of R' (inl v) -> inr tt = inl (class_of R'' v)
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
v: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n
q: class_of R' (inr tt) = class_of R' (inl v)

inr tt = inl (class_of R'' v)
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
v: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n
q: R' (inr tt) (inl v)

inr tt = inl (class_of R'' v)
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
v: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n
q: R' (inl v) (inr tt)

inr tt = inl (class_of R'' v)
elim (np (tr (v ; q))).
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
u: (Quotient R'' + Unit)%type

forall b : Unit, sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) u = sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) (inr b) -> u = inr 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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
u: (Quotient R'' + Unit)%type

sum_ind (fun _ : Quotient R'' + Unit => Quotient R') (Quotient_functor R'' R' inl inlresp) (unit_name (class_of R' (inr tt))) u = class_of R' (inr tt) -> u = inr tt
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
u: Quotient R''

Quotient_functor R'' R' inl inlresp u = class_of R' (inr tt) -> inl u = inr tt
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
class_of R' (inr tt) = class_of R' (inr tt) -> inr tt = inr tt
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
u: Quotient R''

Quotient_functor R'' R' inl inlresp u = class_of R' (inr tt) -> inl u = inr tt
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
u: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n

class_of R' (inl u) = class_of R' (inr tt) -> inl (class_of R'' u) = inr tt
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
u: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n
q: class_of R' (inl u) = class_of R' (inr tt)

inl (class_of R'' u) = inr tt
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}
u: (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n
q: R' (inl u) (inr tt)

inl (class_of R'' u) = inr tt
elim (np (tr (u;q))).
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: forall x y : X, Decidable (R x y)
n: nat
IH: forall R' : Fin n -> Fin n -> Type, is_mere_relation (Fin n) R' -> Reflexive R' -> Symmetric R' -> Transitive R' -> (forall x y : 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: forall x y : Fin n.+1, Decidable (R' x y)
R'':= fun x y : (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: forall x y : (fix Fin (n : nat) : Type0 := match n with | 0 => Empty | n0.+1 => (Fin n0 + Unit)%type end) n, Decidable (R'' x y)
inlresp: forall x y : (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)}

class_of R' (inr tt) = class_of R' (inr tt) -> inr tt = 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: forall x y : X, Decidable (R x y)

fcard X = finadd (fun z : Quotient R => fcard {x : X & (fun x0 : 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: forall x y : X, Decidable (R x y)

fcard X = finadd (fun z : Quotient R => fcard {x : X & (fun x0 : 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: forall x y : X, Decidable (R x y)

finadd (fun y : Quotient R => fcard {x : X & (fun x0 : X => class_of R x0 = y) x}) = finadd (fun z : Quotient R => fcard {x : X & (fun x0 : 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: forall x y : X, Decidable (R x y)

forall z : Quotient R, fcard {x : X & (fun x0 : X => class_of R x0 = z) x} = fcard {x : X & (fun x0 : 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: forall x y : X, Decidable (R x y)
x: X

fcard {x0 : X & (fun x1 : X => class_of R x1 = class_of R x) x0} = fcard {x0 : X & (fun x1 : 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: forall x y : 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: forall x y : 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: forall x y : 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: forall x y : X, Decidable (R x y)
x, y: X

R x y <~> R y x
apply equiv_iff_hprop; apply symmetry. Defined. End DecidableQuotients. (** ** 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj g
h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1
X2: MapIn (Tr (-1)) h

forall 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: isinj 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: forall a : 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: isinj g
h:= (fin_transpose_last_with m (g (inr tt)))^-1 o g: Fin n.+1 -> Fin m.+1
X2: MapIn (Tr (-1)) h

forall 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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)
refine (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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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)
refine (_ @ p^); apply fin_transpose_last_with_with.
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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: isinj 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: forall a : 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: isinj 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: forall a : Fin n, is_inl (h (inl a))

forall b : 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: isinj 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: forall a : Fin n, is_inl (h (inl a))
Hb: forall b : 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: isinj 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: forall a : Fin n, is_inl (h (inl a))

forall b : 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: isinj 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: forall a : 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: isinj 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: forall a : 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: isinj 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: forall a : 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: isinj 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: forall a : 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: isinj 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: forall a : 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: isinj 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: forall a : 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: isinj 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: forall a : Fin n, is_inl (h (inl a))
Hb: forall b : 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: isinj 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: forall a : Fin n, is_inl (h (inl a))
Hb: forall b : 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 & (fun x : 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: (fun x : 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: (fun x : 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: (fun x : 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: (fun x : 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. *) Section Enumeration. Context `{Funext} {X} `{Finite@{_ Set _} X} (e : nat -> X). Let er (n : nat) : Fin n -> X := fun k => 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : nat, Fin n -> X
n: nat
IH: IsEmbedding (er n)
ne: ~ hfiber (er n) (er n.+1 (inr tt))
x: X

forall x0 y : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : nat, Fin n -> X
n: nat
IH: isinj (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): forall n : nat, Fin n -> X
n: nat
IH: isinj (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): forall n : nat, Fin n -> X
n: nat
IH: isinj (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): forall n : nat, Fin n -> X
n: nat
IH: isinj (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): forall n : nat, Fin n -> X
n: nat
IH: isinj (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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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): forall n : 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 (not_lt_n_n _ q).
H: Funext
X: Type
H0: Finite X
e: nat -> X
er:= fun (n : nat) (k : Fin n) => e (nat_fin n k): forall n : 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}}
assumption. Defined. End Enumeration.