Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
From HoTT Require Import Universes.Smallness.From HoTT Require Import Colimits.Quotient.From HoTT Require Import HSet.LocalClose Scope trunc_scope.LocalOpen Scope hprop_scope.(** This file contains a definition of ordinals and some fundamental results, roughly following the presentation in the HoTT book. *)(** * Well-foundedness *)InductiveAccessible {A} (R : Lt A) (a : A) :=
acc : (forallb, b < a -> Accessible R b) -> Accessible R a.
H: Funext A: Type R: Lt A a: A
IsHProp (Accessible R a)
H: Funext A: Type R: Lt A a: A
IsHProp (Accessible R a)
H: Funext A: Type R: Lt A a: A
forallxy : Accessible R a, x = y
H: Funext A: Type R: Lt A a: A acc1: Accessible R a
forally : Accessible R a, acc1 = y
H: Funext A: Type R: Lt A a: A acc1': forallb : A, b < a -> Accessible R b IH: forall (b : A) (l : b < a)
(y : Accessible R b), acc1' b l = y
forally : Accessible R a, acc R a acc1' = y
H: Funext A: Type R: Lt A a: A acc1': forallb : A, b < a -> Accessible R b IH: forall (b : A) (l : b < a)
(y : Accessible R b), acc1' b l = y acc2': forallb : A, b < a -> Accessible R b
acc R a acc1' = acc R a acc2'
H: Funext A: Type R: Lt A a: A acc1': forallb : A, b < a -> Accessible R b IH: forall (b : A) (l : b < a)
(y : Accessible R b), acc1' b l = y acc2': forallb : A, b < a -> Accessible R b
acc1' = acc2'
H: Funext A: Type R: Lt A a: A acc1': forallb : A, b < a -> Accessible R b IH: forall (b : A) (l : b < a)
(y : Accessible R b), acc1' b l = y acc2': forallb : A, b < a -> Accessible R b b: A
acc1' b = acc2' b
H: Funext A: Type R: Lt A a: A acc1': forallb : A, b < a -> Accessible R b IH: forall (b : A) (l : b < a)
(y : Accessible R b), acc1' b l = y acc2': forallb : A, b < a -> Accessible R b b: A Hb: b < a
acc1' b Hb = acc2' b Hb
apply IH.Qed.ClassWellFounded {A} (R : Relation A) :=
well_foundedness : foralla : A, Accessible R a.
H: Funext A: Type R: Relation A
IsHProp (WellFounded R)
H: Funext A: Type R: Relation A
IsHProp (WellFounded R)
H: Funext A: Type R: Relation A H1, H2: WellFounded R
H1 = H2
H: Funext A: Type R: Relation A H1, H2: WellFounded R a: A
H1 a = H2 a
apply path_ishprop.Qed.(** * Extensionality *)ClassExtensional {A} (R : Lt A) :=
extensionality : forallab : A, (forallc : A, c < a <-> c < b) -> a = b.
H: Funext A: Type IsHSet0: IsHSet A R: Relation A
IsHProp (Extensional R)
H: Funext A: Type IsHSet0: IsHSet A R: Relation A
IsHProp (Extensional R)
H: Funext A: Type IsHSet0: IsHSet A R: Relation A
IsHProp
(forallab : A,
(forallc : A, c < a <-> c < b) -> a = b)
exact _.Qed.(** * Ordinals *)ClassIsOrdinal@{carrier relation} (A : Type@{carrier}) (R : Relation@{carrier relation} A) := {
ordinal_is_hset :: IsHSet A ;
ordinal_relation_is_mere :: is_mere_relation A R ;
ordinal_extensionality :: Extensional R ;
ordinal_well_foundedness :: WellFounded R ;
ordinal_transitivity :: Transitive R ;
}.
H: Funext A: Type R: Relation A
IsHProp (IsOrdinal A R)
H: Funext A: Type R: Relation A
IsHProp (IsOrdinal A R)
H: Funext A: Type R: Relation A
?A <~> IsOrdinal A R
H: Funext A: Type R: Relation A
IsHProp ?A
H: Funext A: Type R: Relation A
?A <~> IsOrdinal A R
issig.
H: Funext A: Type R: Relation A
IsHProp
{_ : IsHSet A &
{_ : is_mere_relation A R &
{_ : Extensional R &
{_ : WellFounded R & Transitive R}}}}
H: Funext A: Type R: Relation A
IsHProp
{_ : IsHSet A &
{_ : is_mere_relation A R &
{_ : Extensional R &
{_ : WellFounded R &
forallxyz : A, R x y -> R y z -> R x z}}}}
A: Type R: Relation A is_ordinal: IsOrdinal A R a: A H: R a a
Empty
A: Type R: Relation A is_ordinal: IsOrdinal A R a: A H: R a a IH: forallb : A, b < a -> R b b -> Empty
Empty
apply (IH a); assumption.Qed.DefinitionTypeWithRelation
:= { A : Type & Relation A }.Coercionordinal_as_type_with_relation (A : Ordinal) : TypeWithRelation
:= (A : Type; (<)).(** * Paths in Ordinal *)
Ordinal <~>
{A : Type & {R : Relation A & IsOrdinal A R}}
{A : Type & {R : Relation A & IsOrdinal A R}} <~>
{R : {A : Type & Relation A} & IsOrdinal R.1 R.2}
Ordinal <~>
{A : Type & {R : Relation A & IsOrdinal A R}}
{A : Type & {R : Relation A & IsOrdinal A R}} <~>
Ordinal
issig.
{A : Type & {R : Relation A & IsOrdinal A R}} <~>
{R : {A : Type & Relation A} & IsOrdinal R.1 R.2}
apply equiv_sigma_assoc'.Defined.DefinitionIsomorphism : TypeWithRelation -> TypeWithRelation -> Type
:= fun '(A; R__A) '(B; R__B) =>
{ f : A <~> B & forallaa', R__A a a' <-> R__B (f a) (f a') }.
Reflexive Isomorphism
Reflexive Isomorphism
A: TypeWithRelation
Isomorphism A A
A: TypeWithRelation
forallaa' : A.1,
A.2 a a' <-> A.2 (1%equiv a) (1%equiv a')
A: TypeWithRelation
forallaa' : A.1, A.2 a a' <-> A.2 a a'
A: TypeWithRelation a, a': A.1
A.2 a a' <-> A.2 a a'
reflexivity.Qed.
forallAB : TypeWithRelation,
Isomorphism A B -> Isomorphism B A
forallAB : TypeWithRelation,
Isomorphism A B -> Isomorphism B A
A: Type R__A: Relation A B: Type R__B: Relation B f: A <~> B H: forallaa' : A, R__A a a' <-> R__B (f a) (f a')
Isomorphism (B; R__B) (A; R__A)
A: Type R__A: Relation A B: Type R__B: Relation B f: A <~> B H: forallaa' : A, R__A a a' <-> R__B (f a) (f a')
forallaa' : B,
R__B a a' <-> R__A (f^-1%equiv a) (f^-1%equiv a')
A: Type R__A: Relation A B: Type R__B: Relation B f: A <~> B H: forallaa' : A, R__A a a' <-> R__B (f a) (f a') b, b': B
R__B b b' <-> R__A (f^-1%equiv b) (f^-1%equiv b')
A: Type R__A: Relation A B: Type R__B: Relation B f: A <~> B H: forallaa' : A, R__A a a' <-> R__B (f a) (f a') b, b': B
R__B b b' <-> R__A (f^-1 b) (f^-1 b')
A: Type R__A: Relation A B: Type R__B: Relation B f: A <~> B H: forallaa' : A, R__A a a' <-> R__B (f a) (f a') b, b': B
A: Type R__A: Relation A B: Type R__B: Relation B f: A <~> B H: forallaa' : A, R__A a a' <-> R__B (f a) (f a') b, b': B a:= f^-1 b: A
R__B (f a) b' <-> R__A (f^-1 (f a)) (f^-1 b')
A: Type R__A: Relation A B: Type R__B: Relation B f: A <~> B H: forallaa' : A, R__A a a' <-> R__B (f a) (f a') b, b': B a:= f^-1 b: A
R__B (f a) b' <-> R__A a (f^-1 b')
A: Type R__A: Relation A B: Type R__B: Relation B f: A <~> B H: forallaa' : A, R__A a a' <-> R__B (f a) (f a') b, b': B a:= f^-1 b: A
R__B (f a) (f (f^-1 b')) <->
R__A a (f^-1 (f (f^-1 b')))
A: Type R__A: Relation A B: Type R__B: Relation B f: A <~> B H: forallaa' : A, R__A a a' <-> R__B (f a) (f a') b, b': B a:= f^-1 b: A a':= f^-1 b': A
R__B (f a) (f a') <-> R__A a (f^-1 (f a'))
A: Type R__A: Relation A B: Type R__B: Relation B f: A <~> B H: forallaa' : A, R__A a a' <-> R__B (f a) (f a') b, b': B a:= f^-1 b: A a':= f^-1 b': A
R__B (f a) (f a') <-> R__A a a'
(* We don't apply the symmetry tactic because that would introduce bad universe constraints *)split; apply H.Defined.(** We state this first without using [Transitive] to allow more general universe variables. *)
forallABC : TypeWithRelation,
Isomorphism A B -> Isomorphism B C -> Isomorphism A C
forallABC : TypeWithRelation,
Isomorphism A B -> Isomorphism B C -> Isomorphism A C
A: Type R__A: Relation A B: Type R__B: Relation B C: Type R__C: Relation C
A: Type R__A: Relation A B: Type R__B: Relation B C: Type R__C: Relation C f: A <~> B Hf: forallaa' : A, R__A a a' <-> R__B (f a) (f a') g: B <~> C Hg: forallaa' : B, R__B a a' <-> R__C (g a) (g a')
Isomorphism (A; R__A) (C; R__C)
A: Type R__A: Relation A B: Type R__B: Relation B C: Type R__C: Relation C f: A <~> B Hf: forallaa' : A, R__A a a' <-> R__B (f a) (f a') g: B <~> C Hg: forallaa' : B, R__B a a' <-> R__C (g a) (g a')
forallaa' : A,
R__A a a' <-> R__C ((g oE f) a) ((g oE f) a')
A: Type R__A: Relation A B: Type R__B: Relation B C: Type R__C: Relation C f: A <~> B Hf: forallaa' : A, R__A a a' <-> R__B (f a) (f a') g: B <~> C Hg: forallaa' : B, R__B a a' <-> R__C (g a) (g a') a, a': A
R__A a a' <-> R__C ((g oE f) a) ((g oE f) a')
A: Type R__A: Relation A B: Type R__B: Relation B C: Type R__C: Relation C f: A <~> B Hf: forallaa' : A, R__A a a' <-> R__B (f a) (f a') g: B <~> C Hg: forallaa' : B, R__B a a' <-> R__C (g a) (g a') a, a': A
R__A a a' -> R__C ((g oE f) a) ((g oE f) a')
A: Type R__A: Relation A B: Type R__B: Relation B C: Type R__C: Relation C f: A <~> B Hf: forallaa' : A, R__A a a' <-> R__B (f a) (f a') g: B <~> C Hg: forallaa' : B, R__B a a' <-> R__C (g a) (g a') a, a': A
R__C ((g oE f) a) ((g oE f) a') -> R__A a a'
A: Type R__A: Relation A B: Type R__B: Relation B C: Type R__C: Relation C f: A <~> B Hf: forallaa' : A, R__A a a' <-> R__B (f a) (f a') g: B <~> C Hg: forallaa' : B, R__B a a' <-> R__C (g a) (g a') a, a': A
R__A a a' -> R__C ((g oE f) a) ((g oE f) a')
A: Type R__A: Relation A B: Type R__B: Relation B C: Type R__C: Relation C f: A <~> B Hf: forallaa' : A, R__A a a' <-> R__B (f a) (f a') g: B <~> C Hg: forallaa' : B, R__B a a' <-> R__C (g a) (g a') a, a': A a_a': R__A a a'
R__C ((g oE f) a) ((g oE f) a')
A: Type R__A: Relation A B: Type R__B: Relation B C: Type R__C: Relation C f: A <~> B Hf: forallaa' : A, R__A a a' <-> R__B (f a) (f a') g: B <~> C Hg: forallaa' : B, R__B a a' <-> R__C (g a) (g a') a, a': A a_a': R__A a a'
R__B (f a) (f a')
A: Type R__A: Relation A B: Type R__B: Relation B C: Type R__C: Relation C f: A <~> B Hf: forallaa' : A, R__A a a' <-> R__B (f a) (f a') g: B <~> C Hg: forallaa' : B, R__B a a' <-> R__C (g a) (g a') a, a': A a_a': R__A a a'
R__A a a'
exact a_a'.
A: Type R__A: Relation A B: Type R__B: Relation B C: Type R__C: Relation C f: A <~> B Hf: forallaa' : A, R__A a a' <-> R__B (f a) (f a') g: B <~> C Hg: forallaa' : B, R__B a a' <-> R__C (g a) (g a') a, a': A
R__C ((g oE f) a) ((g oE f) a') -> R__A a a'
A: Type R__A: Relation A B: Type R__B: Relation B C: Type R__C: Relation C f: A <~> B Hf: forallaa' : A, R__A a a' <-> R__B (f a) (f a') g: B <~> C Hg: forallaa' : B, R__B a a' <-> R__C (g a) (g a') a, a': A gfa_gfa': R__C ((g oE f) a) ((g oE f) a')
R__A a a'
A: Type R__A: Relation A B: Type R__B: Relation B C: Type R__C: Relation C f: A <~> B Hf: forallaa' : A, R__A a a' <-> R__B (f a) (f a') g: B <~> C Hg: forallaa' : B, R__B a a' <-> R__C (g a) (g a') a, a': A gfa_gfa': R__C ((g oE f) a) ((g oE f) a')
R__B (f a) (f a')
A: Type R__A: Relation A B: Type R__B: Relation B C: Type R__C: Relation C f: A <~> B Hf: forallaa' : A, R__A a a' <-> R__B (f a) (f a') g: B <~> C Hg: forallaa' : B, R__B a a' <-> R__C (g a) (g a') a, a': A gfa_gfa': R__C ((g oE f) a) ((g oE f) a')
(A; lt) = (B; lt) <~>
{f : A.1 <~> B.1 &
forallaa' : A.1, A.2 a a' <-> B.2 (f a) (f a')}
H: Univalence A, B: Ordinal
(A; lt) = (B; lt) <~>
{p : A = B & transport Relation p lt = lt}
H: Univalence A, B: Ordinal
{p : A = B & transport Relation p lt = lt} <~>
{f : A.1 <~> B.1 &
forallaa' : A.1, A.2 a a' <-> B.2 (f a) (f a')}
H: Univalence A, B: Ordinal
(A; lt) = (B; lt) <~>
{p : A = B & transport Relation p lt = lt}
H: Univalence A, B: Ordinal
{p : A = B & transport Relation p lt = lt} <~>
(A; lt) = (B; lt)
exact (equiv_path_sigma Relation
(exist Relation A (<))
(exist Relation B (<))).
H: Univalence A, B: Ordinal
{p : A = B & transport Relation p lt = lt} <~>
{f : A.1 <~> B.1 &
forallaa' : A.1, A.2 a a' <-> B.2 (f a) (f a')}
H: Univalence A, B: Ordinal
A = B <~> (A.1 <~> B.1)
H: Univalence A, B: Ordinal
foralla : A = B,
(funp : A = B => transport Relation p lt = lt) a <~>
(funf : A.1 <~> B.1 =>
foralla0a' : A.1, A.2 a0 a' <-> B.2 (f a0) (f a'))
(?f a)
H: Univalence A, B: Ordinal
A = B <~> (A.1 <~> B.1)
exact (equiv_equiv_path A B).
H: Univalence A, B: Ordinal
foralla : A = B,
(funp : A = B => transport Relation p lt = lt) a <~>
(funf : A.1 <~> B.1 =>
foralla0a' : A.1, A.2 a0 a' <-> B.2 (f a0) (f a'))
(equiv_equiv_path A B a)
H: Univalence A, B: Ordinal
foralla : ordinal_carrier A = ordinal_carrier B,
transport Relation a lt = lt <~>
(foralla0a' : ordinal_carrier A,
a0 < a' <->
transport idmap a a0 < transport idmap a a')
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
transport Relation p lt = lt <~>
(forallaa' : ordinal_carrier A,
a < a' <-> transport idmap p a < transport idmap p a')
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
IsHProp (transport Relation p lt = lt)
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
IsHProp
(forallaa' : ordinal_carrier A,
a < a' <->
transport idmap p a < transport idmap p a')
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
transport Relation p lt = lt ->
forallaa' : ordinal_carrier A,
a < a' <-> transport idmap p a < transport idmap p a'
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
(forallaa' : ordinal_carrier A,
a < a' <-> transport idmap p a < transport idmap p a') ->
transport Relation p lt = lt
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
IsHProp (transport Relation p lt = lt)
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
(forallbb' : B,
transport Relation p lt b b' = (b < b')) <~>
transport Relation p lt = lt
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
IsHProp
(forallbb' : B,
transport Relation p lt b b' = (b < b'))
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
(forallbb' : B,
transport Relation p lt b b' = (b < b')) <~>
transport Relation p lt = lt
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
(forallbb' : B,
transport Relation p lt b b' = (b < b')) <~>
(forallb : B, transport Relation p lt b = lt b)
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
(forallb : B, transport Relation p lt b = lt b) <~>
transport Relation p lt = lt
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
(forallbb' : B,
transport Relation p lt b b' = (b < b')) <~>
(forallb : B, transport Relation p lt b = lt b)
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B b: B
(forallb' : B,
transport Relation p lt b b' = (b < b')) <~>
transport Relation p lt b = lt b
apply equiv_path_arrow.
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
(forallb : B, transport Relation p lt b = lt b) <~>
transport Relation p lt = lt
apply equiv_path_arrow.
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
IsHProp
(forallbb' : B,
transport Relation p lt b b' = (b < b'))
exact _.
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
IsHProp
(forallaa' : ordinal_carrier A,
a < a' <->
transport idmap p a < transport idmap p a')
exact _.
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
transport Relation p lt = lt ->
forallaa' : ordinal_carrier A,
a < a' <-> transport idmap p a < transport idmap p a'
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B a, a': ordinal_carrier A
a < a' <->
transport Relation p lt (transport idmap p a)
(transport idmap p a')
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B a, a': ordinal_carrier A
a < a' <->
transport (funx : Type => x -> Type) p
(lt (transport idmap p^ (transport idmap p a)))
(transport idmap p a')
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B a, a': ordinal_carrier A
a < a' <->
transport idmap p^ (transport idmap p a) <
transport idmap p^ (transport idmap p a')
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B a, a': ordinal_carrier A
a < a' <-> a < a'
reflexivity.
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B
(forallaa' : ordinal_carrier A,
a < a' <-> transport idmap p a < transport idmap p a') ->
transport Relation p lt = lt
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B H0: forallaa' : ordinal_carrier A,
a < a' <->
transport idmap p a < transport idmap p a'
transport Relation p lt = lt
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B H0: forallaa' : ordinal_carrier A,
a < a' <->
transport idmap p a < transport idmap p a' b: ordinal_carrier B
transport Relation p lt b = lt b
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B H0: forallaa' : ordinal_carrier A,
a < a' <->
transport idmap p a < transport idmap p a' b, b': ordinal_carrier B
transport Relation p lt b b' = (b < b')
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B H0: forallaa' : ordinal_carrier A,
a < a' <->
transport idmap p a < transport idmap p a' b, b': ordinal_carrier B
transport (funx : Type => x -> Type) p
(lt (transport idmap p^ b)) b' = (b < b')
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B H0: forallaa' : ordinal_carrier A,
a < a' <->
transport idmap p a < transport idmap p a' b, b': ordinal_carrier B
(transport idmap p^ b < transport idmap p^ b') =
(b < b')
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B H0: forallaa' : ordinal_carrier A,
a < a' <->
transport idmap p a < transport idmap p a' b, b': ordinal_carrier B
transport idmap p^ b < transport idmap p^ b' <->
b < b'
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B b, b': ordinal_carrier B H0: transport idmap p^ b < transport idmap p^ b' <->
transport idmap p (transport idmap p^ b) <
transport idmap p (transport idmap p^ b')
transport idmap p^ b < transport idmap p^ b' <->
b < b'
H: Univalence A, B: Ordinal p: ordinal_carrier A = ordinal_carrier B b, b': ordinal_carrier B H0: transport idmap p^ b < transport idmap p^ b' <->
b < b'
transport idmap p^ b < transport idmap p^ b' <->
b < b'
exact H0.Qed.
H: Univalence A, B: Ordinal
forallf : A <~> B,
(forallaa' : A, a < a' <-> f a < f a') -> A = B
H: Univalence A, B: Ordinal
forallf : A <~> B,
(forallaa' : A, a < a' <-> f a < f a') -> A = B
H: Univalence A, B: Ordinal f: A <~> B H0: forallaa' : A, a < a' <-> f a < f a'
A = B
H: Univalence A, B: Ordinal f: A <~> B H0: forallaa' : A, a < a' <-> f a < f a'
Isomorphism A B
H: Univalence A, B: Ordinal f: A <~> B H0: forallaa' : A, a < a' <-> f a < f a'
forallaa' : A.1, A.2 a a' <-> B.2 (f a) (f a')
exact H0.Qed.
H: ExcludedMiddle A: Ordinal a, b: A
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a, b: A
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A
forallb : A, a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b
forallb : A, a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type}
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type}
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type}
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a
merely {b' : A & ((b' < b) * (a = b' \/ a < b'))%type} ->
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} ->
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a b': A b'_b: b' < b Hb': a = b' \/ a < b'
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a b': A b'_b: b' < b
a = b' \/ a < b' -> a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a b': A b'_b: b' < b
(a = b') + (a < b') -> a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a b': A b'_b: b' < b a_b': a = b'
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A,
b < a ->
forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A,
b0 < b -> a < b0 \/ a = b0 \/ b0 < a b': A b'_b: b' < b b'_a: a < b'
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a b': A b'_b: b' < b a_b': a = b'
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a b': A b'_b: b' < b a_b': a = b'
((a < b) + (a = b \/ b < a))%type
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a b': A b'_b: b' < b a_b': a = b'
a < b
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a b': A b'_b: b' < b a_b': a = b'
b' < b
exact b'_b.
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a b': A b'_b: b' < b b'_a: a < b'
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a b': A b'_b: b' < b b'_a: a < b'
((a < b) + (a = b \/ b < a))%type
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a b': A b'_b: b' < b b'_a: a < b'
a < b
transitivity b'; assumption.
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type}
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type}
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type}
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type}
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type}
merely {a' : A & ((a' < a) * (a' = b \/ b < a'))%type} ->
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type}
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} ->
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a Ha': a' = b \/ b < a'
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a
a' = b \/ b < a' -> a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a
(a' = b) + (b < a') -> a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a a'_b: a' = b
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A,
b < a ->
forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A,
b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a b_a': b < a'
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a a'_b: a' = b
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a a'_b: a' = b
((a < b) + (a = b \/ b < a))%type
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a a'_b: a' = b
a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a a'_b: a' = b
((a = b) + (b < a))%type
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a a'_b: a' = b
b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a a'_b: a' = b
a' < a
exact a'_a.
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a b_a': b < a'
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a b_a': b < a'
((a < b) + (a = b \/ b < a))%type
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a b_a': b < a'
a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a b_a': b < a'
((a = b) + (b < a))%type
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} a': A a'_a: a' < a b_a': b < a'
b < a
transitivity a'; assumption.
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type}
a < b \/ a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type}
((a < b) + (a = b \/ b < a))%type
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type}
a = b \/ b < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type}
((a = b) + (b < a))%type
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type}
a = b
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type}
forallc : A, c < a <-> c < b
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A
c < a <-> c < b
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A
c < a -> c < b
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A
c < b -> c < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A
c < a -> c < b
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a
c < b
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a
~~ (c < b)
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a not_c_b: ~ (c < b)
Empty
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a not_c_b: ~ (c < b)
merely {a' : A & ((a' < a) * (a' = b \/ b < a'))%type}
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a not_c_b: ~ (c < b)
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type}
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a not_c_b: ~ (c < b)
((c < a) * (c = b \/ b < c))%type
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a not_c_b: ~ (c < b)
c < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A,
b < a ->
forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A,
b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a not_c_b: ~ (c < b)
c = b \/ b < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a not_c_b: ~ (c < b)
c < a
exact c_a.
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a not_c_b: ~ (c < b)
c = b \/ b < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a not_c_b: ~ (c < b)
(c < b) + (c = b \/ b < c) -> c = b \/ b < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a not_c_b: ~ (c < b) c_b: c < b
c = b \/ b < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A,
b < a ->
forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A,
b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a not_c_b: ~ (c < b) H3: c = b \/ b < c
c = b \/ b < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a not_c_b: ~ (c < b) c_b: c < b
c = b \/ b < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a not_c_b: ~ (c < b) c_b: c < b
Empty
exact (not_c_b c_b).
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_a: c < a not_c_b: ~ (c < b) H3: c = b \/ b < c
c = b \/ b < c
exact H3.
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A
c < b -> c < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b
c < a
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b
~~ (c < a)
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a)
Empty
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a)
merely {b' : A & ((b' < b) * (a = b' \/ a < b'))%type}
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a)
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type}
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a)
((c < b) * (a = c \/ a < c))%type
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a)
c < b
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A,
b < a ->
forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A,
b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a)
a = c \/ a < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a)
c < b
exact c_b.
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a)
a = c \/ a < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a)
(a < c) + (a = c \/ c < a) -> a = c \/ a < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) a_c: a < c
a = c \/ a < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A,
b < a ->
forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A,
b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) H3: a = c \/ c < a
a = c \/ a < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) a_c: a < c
a = c \/ a < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) a_c: a < c
((a = c) + (a < c))%type
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) a_c: a < c
a < c
exact a_c.
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) H3: a = c \/ c < a
a = c \/ a < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) H3: a = c \/ c < a
(a = c) + (c < a) -> a = c \/ a < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) H3: a = c \/ c < a a_c: a = c
a = c \/ a < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A,
b < a ->
forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A,
b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) H3: a = c \/ c < a c_a: c < a
a = c \/ a < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) H3: a = c \/ c < a a_c: a = c
a = c \/ a < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) H3: a = c \/ c < a a_c: a = c
((a = c) + (a < c))%type
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) H3: a = c \/ c < a a_c: a = c
a = c
exact a_c.
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) H3: a = c \/ c < a c_a: c < a
a = c \/ a < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) H3: a = c \/ c < a c_a: c < a
((a = c) + (a < c))%type
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) H3: a = c \/ c < a c_a: c < a
a < c
H: ExcludedMiddle A: Ordinal a: A IHa: forallb : A, b < a -> forallb0 : A, b < b0 \/ b = b0 \/ b0 < b b: A IHb: forallb0 : A, b0 < b -> a < b0 \/ a = b0 \/ b0 < a H1: ~
merely
{b' : A & ((b' < b) * (a = b' \/ a < b'))%type} H2: ~
merely
{a' : A & ((a' < a) * (a' = b \/ b < a'))%type} c: A c_b: c < b not_c_a: ~ (c < a) H3: a = c \/ c < a c_a: c < a
Empty
exact (not_c_a c_a).Qed.
lem: ExcludedMiddle A: Ordinal P: A -> HProp
merely {a : A & P a} ->
merely
{a : A &
(P a * (forallb : A, P b -> a < b \/ a = b))%type}
lem: ExcludedMiddle A: Ordinal P: A -> HProp
merely {a : A & P a} ->
merely
{a : A &
(P a * (forallb : A, P b -> a < b \/ a = b))%type}
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a}
merely
{a : A &
(P a * (forallb : A, P b -> a < b \/ a = b))%type}
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a}
{a : A & P a} ->
merely
{a : A &
(P a * (forallb : A, P b -> a < b \/ a = b))%type}
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a
merely
{a : A &
(P a * (forallb : A, P b -> a < b \/ a = b))%type}
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type}
merely
{a : A &
(P a * (forallb : A, P b -> a < b \/ a = b))%type}
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: merely {b : A & (P b * (b < a))%type}
merely
{a : A &
(P a * (forallb : A, P b -> a < b \/ a = b))%type}
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type}
merely
{a : A &
(P a * (forallb : A, P b -> a < b \/ a = b))%type}
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: merely {b : A & (P b * (b < a))%type}
merely
{a : A &
(P a * (forallb : A, P b -> a < b \/ a = b))%type}
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: merely {b : A & (P b * (b < a))%type}
{b : A & (P b * (b < a))%type} ->
merely
{a : A &
(P a * (forallb : A, P b -> a < b \/ a = b))%type}
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: merely {b : A & (P b * (b < a))%type} b: A Hb: (P b * (b < a))%type
merely
{a : A &
(P a * (forallb : A, P b -> a < b \/ a = b))%type}
apply (IH b); apply Hb.
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type}
merely
{a : A &
(P a * (forallb : A, P b -> a < b \/ a = b))%type}
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type}
{a : A &
(P a * (forallb : A, P b -> a < b \/ a = b))%type}
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type}
(P a * (forallb : A, P b -> a < b \/ a = b))%type
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type}
forallb : A, P b -> a < b \/ a = b
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b
a < b \/ a = b
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b
a < b \/ a = b \/ b < a -> a < b \/ a = b
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b H1: a < b \/ a = b \/ b < a
a < b \/ a = b
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b H1: a < b \/ a = b \/ b < a
(a < b) + (a = b \/ b < a) -> a < b \/ a = b
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b H1: a < b \/ a = b \/ b < a H2: a < b
a < b \/ a = b
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b H1: a < b \/ a = b \/ b < a H2: a = b \/ b < a
a < b \/ a = b
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b H1: a < b \/ a = b \/ b < a H2: a < b
a < b \/ a = b
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b H1: a < b \/ a = b \/ b < a H2: a < b
((a < b) + (a = b))%type
byleft.
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b H1: a < b \/ a = b \/ b < a H2: a = b \/ b < a
a < b \/ a = b
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b H1: a < b \/ a = b \/ b < a H2: a = b \/ b < a
(a = b) + (b < a) -> a < b \/ a = b
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b H1: a < b \/ a = b \/ b < a H2: a = b \/ b < a H3: a = b
a < b \/ a = b
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b H1: a < b \/ a = b \/ b < a H2: a = b \/ b < a H3: b < a
a < b \/ a = b
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b H1: a < b \/ a = b \/ b < a H2: a = b \/ b < a H3: a = b
a < b \/ a = b
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b H1: a < b \/ a = b \/ b < a H2: a = b \/ b < a H3: a = b
((a < b) + (a = b))%type
byright.
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b H1: a < b \/ a = b \/ b < a H2: a = b \/ b < a H3: b < a
a < b \/ a = b
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b H1: a < b \/ a = b \/ b < a H2: a = b \/ b < a H3: b < a
{b : A & (P b * (b < a))%type}
lem: ExcludedMiddle A: Ordinal P: A -> HProp H': merely {a : A & P a} a: A Ha: P a IH: forallb : A,
b < a ->
P b ->
merely
{a : A &
(P a *
(forallb0 : A, P b0 -> a < b0 \/ a = b0))%type} H: ~ merely {b : A & (P b * (b < a))%type} b: A Hb: P b H1: a < b \/ a = b \/ b < a H2: a = b \/ b < a H3: b < a
(P b * (b < a))%type
bysplit.Qed.(** * Simulations *)(** We define the notion of simulations between arbitrary relations. For simplicity, most lemmas about simulations are formulated for ordinals only, even if they do not need all properties of ordinals. The only exception is [isordinal_simulation] which can be used to prove that a relation is an ordinal. *)ClassIsSimulation {AB : Type} {R__A : Lt A} {R__B : Lt B} (f : A -> B) :=
{ simulation_is_hom {a a'}
: a < a' -> f a < f a'
; simulation_is_merely_minimal {a b}
: b < f a -> hexists (funa' => a' < a /\ f a' = b)
}.Arguments simulation_is_hom {_ _ _ _} _ {_ _ _}.
H: Funext A, B: Ordinal f: A -> B
IsHProp (IsSimulation f)
H: Funext A, B: Ordinal f: A -> B
IsHProp (IsSimulation f)
H: Funext A, B: Ordinal f: A -> B
?A <~> IsSimulation f
H: Funext A, B: Ordinal f: A -> B
IsHProp ?A
H: Funext A, B: Ordinal f: A -> B
?A <~> IsSimulation f
issig.
H: Funext A, B: Ordinal f: A -> B
IsHProp
{_ : forallaa' : A, a < a' -> f a < f a' &
forall (a : A) (b : B),
b < f a ->
hexists (funa' : A => ((a' < a) * (f a' = b))%type)}
exact _.Qed.
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f
IsInjective f
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f
IsInjective f
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
forally : A, f a = f y -> a = y
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y
forally : A, f a = f y -> a = y
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y b: A
f a = f b -> a = b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b -> a = b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b -> a = b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y
f a = f b -> a = b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b
a = b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A
c < a <-> c < b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A
c < a -> c < b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A
c < b -> c < a
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A
c < a -> c < b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_a: c < a
c < b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_a: c < a fc_fa: f c < f a
c < b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_a: c < a fc_fa: f c < f a fc_fb: f c < f b
c < b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_a: c < a fc_fa: f c < f a fc_fb: f c < f b H1: hexists
(func' : A => ((c' < b) * (f c' = f c))%type)
c < b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_a: c < a fc_fa: f c < f a fc_fb: f c < f b H1: hexists
(func' : A => ((c' < b) * (f c' = f c))%type)
{c' : A & ((c' < b) * (f c' = f c))%type} -> c < b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_a: c < a fc_fa: f c < f a fc_fb: f c < f b H1: hexists
(func' : A => ((c' < b) * (f c' = f c))%type) c': A c'_b: c' < b fc'_fc: f c' = f c
c < b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_a: c < a fc_fa: f c < f a fc_fb: f c < f b H1: hexists
(func' : A => ((c' < b) * (f c' = f c))%type) c': A c'_b: c' < b fc'_fc: f c' = f c
c = c'
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c': A H1: hexists
(func'0 : A =>
((c'0 < b) * (f c'0 = f c'))%type) fc_fb: f c' < f b fc_fa: f c' < f a c_a: c' < a c'_b: c' < b fc'_fc: f c' = f c'
c' < b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_a: c < a fc_fa: f c < f a fc_fb: f c < f b H1: hexists
(func' : A => ((c' < b) * (f c' = f c))%type) c': A c'_b: c' < b fc'_fc: f c' = f c
c = c'
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_a: c < a fc_fa: f c < f a fc_fb: f c < f b H1: hexists
(func' : A => ((c' < b) * (f c' = f c))%type) c': A c'_b: c' < b fc'_fc: f c' = f c
c < a
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_a: c < a fc_fa: f c < f a fc_fb: f c < f b H1: hexists
(func' : A => ((c' < b) * (f c' = f c))%type) c': A c'_b: c' < b fc'_fc: f c' = f c
f c = f c'
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_a: c < a fc_fa: f c < f a fc_fb: f c < f b H1: hexists
(func' : A => ((c' < b) * (f c' = f c))%type) c': A c'_b: c' < b fc'_fc: f c' = f c
c < a
exact c_a.
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_a: c < a fc_fa: f c < f a fc_fb: f c < f b H1: hexists
(func' : A => ((c' < b) * (f c' = f c))%type) c': A c'_b: c' < b fc'_fc: f c' = f c
f c = f c'
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_a: c < a fc_fa: f c < f a fc_fb: f c < f b H1: hexists
(func' : A => ((c' < b) * (f c' = f c))%type) c': A c'_b: c' < b fc'_fc: f c' = f c
f c' = f c
exact fc'_fc.
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c': A H1: hexists
(func'0 : A =>
((c'0 < b) * (f c'0 = f c'))%type) fc_fb: f c' < f b fc_fa: f c' < f a c_a: c' < a c'_b: c' < b fc'_fc: f c' = f c'
c' < b
exact c'_b.
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A
c < b -> c < a
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b
c < a
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b fc_fb: f c < f b
c < a
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b fc_fb: f c < f b fc_fa: f c < f a
c < a
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b fc_fb: f c < f b fc_fa: f c < f a H1: hexists
(func' : A => ((c' < a) * (f c' = f c))%type)
c < a
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b fc_fb: f c < f b fc_fa: f c < f a H1: hexists
(func' : A => ((c' < a) * (f c' = f c))%type)
{c' : A & ((c' < a) * (f c' = f c))%type} -> c < a
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b fc_fb: f c < f b fc_fa: f c < f a H1: hexists
(func' : A => ((c' < a) * (f c' = f c))%type) c': A c'_a: c' < a fc'_fc: f c' = f c
c < a
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b fc_fb: f c < f b fc_fa: f c < f a H1: hexists
(func' : A => ((c' < a) * (f c' = f c))%type) c': A c'_a: c' < a fc'_fc: f c' = f c
c' = c
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c': A H1: hexists
(func'0 : A =>
((c'0 < a) * (f c'0 = f c'))%type) fc_fa: f c' < f a fc_fb: f c' < f b c_b: c' < b c'_a: c' < a fc'_fc: f c' = f c'
c' < a
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b fc_fb: f c < f b fc_fa: f c < f a H1: hexists
(func' : A => ((c' < a) * (f c' = f c))%type) c': A c'_a: c' < a fc'_fc: f c' = f c
c' = c
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b fc_fb: f c < f b fc_fa: f c < f a H1: hexists
(func' : A => ((c' < a) * (f c' = f c))%type) c': A c'_a: c' < a fc'_fc: f c' = f c
c < b
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b fc_fb: f c < f b fc_fa: f c < f a H1: hexists
(func' : A => ((c' < a) * (f c' = f c))%type) c': A c'_a: c' < a fc'_fc: f c' = f c
forallb : A,
b < c' -> forally : A, f b = f y -> b = y
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b fc_fb: f c < f b fc_fa: f c < f a H1: hexists
(func' : A => ((c' < a) * (f c' = f c))%type) c': A c'_a: c' < a fc'_fc: f c' = f c
f c' = f c
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b fc_fb: f c < f b fc_fa: f c < f a H1: hexists
(func' : A => ((c' < a) * (f c' = f c))%type) c': A c'_a: c' < a fc'_fc: f c' = f c
c < b
exact c_b.
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b fc_fb: f c < f b fc_fa: f c < f a H1: hexists
(func' : A => ((c' < a) * (f c' = f c))%type) c': A c'_a: c' < a fc'_fc: f c' = f c
forallb : A,
b < c' -> forally : A, f b = f y -> b = y
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b fc_fb: f c < f b fc_fa: f c < f a H1: hexists
(func' : A => ((c' < a) * (f c' = f c))%type) c': A c'_a: c' < a fc'_fc: f c' = f c a': A a'_c': a' < c'
forally : A, f a' = f y -> a' = y
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b fc_fb: f c < f b fc_fa: f c < f a H1: hexists
(func' : A => ((c' < a) * (f c' = f c))%type) c': A c'_a: c' < a fc'_fc: f c' = f c a': A a'_c': a' < c'
a' < a
exact (transitivity a'_c' c'_a).
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c: A c_b: c < b fc_fb: f c < f b fc_fa: f c < f a H1: hexists
(func' : A => ((c' < a) * (f c' = f c))%type) c': A c'_a: c' < a fc'_fc: f c' = f c
f c' = f c
exact fc'_fc.
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f b: A IHb: forallb0 : A,
b0 < b ->
foralla : A,
(forallb : A,
b < a -> forally : A, f b = f y -> b = y) ->
f a = f b0 -> a = b0 a: A IHa: forallb : A,
b < a -> forally : A, f b = f y -> b = y fa_fb: f a = f b c': A H1: hexists
(func'0 : A =>
((c'0 < a) * (f c'0 = f c'))%type) fc_fa: f c' < f a fc_fb: f c' < f b c_b: c' < b c'_a: c' < a fc'_fc: f c' = f c'
c' < a
exact c'_a.Qed.
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f
forall (a : A) (b : B),
b < f a -> {a' : A & ((a' < a) * (f a' = b))%type}
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f
forall (a : A) (b : B),
b < f a -> {a' : A & ((a' < a) * (f a' = b))%type}
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A b: B H1: b < f a
{a' : A & ((a' < a) * (f a' = b))%type}
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A b: B H1: b < f a
IsHProp {a' : A & ((a' < a) * (f a' = b))%type}
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A b: B H1: b < f a
{a' : A & ((a' < a) * (f a' = b))%type} ->
{a' : A & ((a' < a) * (f a' = b))%type}
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A b: B H1: b < f a
IsHProp {a' : A & ((a' < a) * (f a' = b))%type}
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A b: B H1: b < f a
forallxy : {a' : A & ((a' < a) * (f a' = b))%type},
x = y
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a, a2: A H1: f a2 < f a a1: A fst: a1 < a p: f a1 = f a2 fst0: a2 < a
(a1; (fst, p)) = (a2; (fst0, 1%path))
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a, a2: A H1: f a2 < f a a1: A fst: a1 < a p: f a1 = f a2 fst0: a2 < a
a1 = a2
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a, a2: A H1: f a2 < f a a1: A fst: a1 < a p: f a1 = f a2 fst0: a2 < a
f a1 = f a2
exact p.
A: Type R: Lt A H: IsOrdinal A R B: Type Q: Lt B H0: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A b: B H1: b < f a
{a' : A & ((a' < a) * (f a' = b))%type} ->
{a' : A & ((a' < a) * (f a' = b))%type}
exact idmap.Qed.
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g
f = g
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g
f = g
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A
f a = g a
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A IH: forallb : A, b < a -> f b = g b
f a = g a
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A IH: forallb : A, b < a -> f b = g b
forallc : B, c < f a <-> c < g a
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A IH: forallb : A, b < a -> f b = g b b: B
b < f a <-> b < g a
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A IH: forallb : A, b < a -> f b = g b b: B
b < f a -> b < g a
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A IH: forallb : A, b < a -> f b = g b b: B
b < g a -> b < f a
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A IH: forallb : A, b < a -> f b = g b b: B
b < f a -> b < g a
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A IH: forallb : A, b < a -> f b = g b b: B b_fa: b < f a
b < g a
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A IH: forallb : A, b < a -> f b = g b a': A b_fa: f a' < f a a'_a: a' < a
f a' < g a
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A IH: forallb : A, b < a -> f b = g b a': A b_fa: f a' < f a a'_a: a' < a
g a' < g a
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A IH: forallb : A, b < a -> f b = g b a': A b_fa: f a' < f a a'_a: a' < a
a' < a
exact a'_a.
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A IH: forallb : A, b < a -> f b = g b b: B
b < g a -> b < f a
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A IH: forallb : A, b < a -> f b = g b b: B b_ga: b < g a
b < f a
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A IH: forallb : A, b < a -> f b = g b a': A b_ga: g a' < g a a'_a: a' < a
g a' < f a
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A IH: forallb : A, b < a -> f b = g b a': A b_ga: g a' < g a a'_a: a' < a
f a' < f a
H: Funext A, B: Ordinal f: A -> B is_simulation_f: IsSimulation f g: A -> B is_simulation_g: IsSimulation g a: A IH: forallb : A, b < a -> f b = g b a': A b_ga: g a' < g a a'_a: a' < a
a' < a
exact a'_a.Qed.
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B)
IsSimulation f.1
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B)
IsSimulation f.1
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B)
forallaa' : A, a < a' -> f.1 a < f.1 a'
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B)
forall (a : A) (b : B),
b < f.1 a ->
hexists (funa' : A => ((a' < a) * (f.1 a' = b))%type)
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B)
forallaa' : A, a < a' -> f.1 a < f.1 a'
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B) a, a': A a_a': a < a'
f.1 a < f.1 a'
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B) a, a': A a_a': a < a'
R__A a a'
exact a_a'.
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B)
forall (a : A) (b : B),
b < f.1 a ->
hexists (funa' : A => ((a' < a) * (f.1 a' = b))%type)
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B) a: A b: B b_fa: b < f.1 a
hexists (funa' : A => ((a' < a) * (f.1 a' = b))%type)
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B) a: A b: B b_fa: b < f.1 a
{a' : A & ((a' < a) * (f.1 a' = b))%type}
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B) a: A b: B b_fa: b < f.1 a
(((f.1)^-1 b < a) * (f.1 ((f.1)^-1 b) = b))%type
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B) a: A b: B b_fa: b < f.1 a
(f.1)^-1 b < a
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B) a: A b: B b_fa: b < f.1 a
f.1 ((f.1)^-1 b) = b
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B) a: A b: B b_fa: b < f.1 a
(f.1)^-1 b < a
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B) a: A b: B b_fa: b < f.1 a
R__B (f.1 ((f.1)^-1 b)) (f.1 a)
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B) a: A b: B b_fa: b < f.1 a
R__B b (f.1 a)
exact b_fa.
A: Type R__A: Lt A B: Type R__B: Lt B f: Isomorphism (A; R__A) (B; R__B) a: A b: B b_fa: b < f.1 a
f.1 ((f.1)^-1 b) = b
apply eisretr.Qed.
H: Funext A, B: Ordinal
IsHProp (Isomorphism A B)
H: Funext A, B: Ordinal
IsHProp (Isomorphism A B)
H: Funext A, B: Ordinal f, g: Isomorphism A B
f = g
H: Funext A, B: Ordinal f, g: Isomorphism A B
f.1 = g.1
H: Funext A, B: Ordinal f, g: Isomorphism A B
f.1 = g.1
apply path_simulation; exact _.Qed.
H: Univalence
IsHSet Ordinal
H: Univalence
IsHSet Ordinal
H: Univalence
is_mere_relation Ordinal paths
H: Univalence A, B: Ordinal
IsHProp (A = B)
H: Univalence A, B: Ordinal
Isomorphism A B <~> A = B
H: Univalence A, B: Ordinal
IsHProp (Isomorphism A B)
H: Univalence A, B: Ordinal
Isomorphism A B <~> A = B
apply equiv_path_Ordinal.
H: Univalence A, B: Ordinal
IsHProp (Isomorphism A B)
exact _.Qed.
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f
IsOrdinal A R
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f
IsOrdinal A R
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f
IsHSet A
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f
is_mere_relation A R
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f
Extensional R
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f
WellFounded R
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f
Transitive R
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f
IsHSet A
exact _.
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f
is_mere_relation A R
exact _.
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f
Extensional R
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a'
a = a'
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a'
f a = f a'
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a'
forallc : B, c < f a <-> c < f a'
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a' b: B
b < f a <-> b < f a'
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a' b: B
b < f a -> b < f a'
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a' b: B
b < f a' -> b < f a
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a' b: B
b < f a -> b < f a'
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a' b: B b_fa: b < f a
b < f a'
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a' b: B b_fa: b < f a
{a' : A & ((a' < a) * (f a' = b))%type} -> b < f a'
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a' a0: A b_fa: f a0 < f a a0_a: a0 < a
f a0 < f a'
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a' a0: A b_fa: f a0 < f a a0_a: a0 < a
a0 < a'
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a' a0: A b_fa: f a0 < f a a0_a: a0 < a
a0 < a
exact a0_a.
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a' b: B
b < f a' -> b < f a
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a' b: B b_fa': b < f a'
b < f a
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a' b: B b_fa': b < f a'
{a'0 : A & ((a'0 < a') * (f a'0 = b))%type} -> b < f a
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a' a0: A b_fa': f a0 < f a' a0_a': a0 < a'
f a0 < f a
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a' a0: A b_fa': f a0 < f a' a0_a': a0 < a'
a0 < a
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, a': A H1: forallc : A, c < a <-> c < a' a0: A b_fa': f a0 < f a' a0_a': a0 < a'
a0 < a'
exact a0_a'.
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f
WellFounded R
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a: A
Accessible R a
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a: A b: B fa_b: f a = b
Accessible R a
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f b: B
foralla : A, f a = b -> Accessible R a
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f b: B IH: forallb0 : B,
b0 < b ->
foralla : A, f a = b0 -> Accessible R a
foralla : A, f a = b -> Accessible R a
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a: A IH: forallb : B,
b < f a ->
foralla : A, f a = b -> Accessible R a
Accessible R a
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a: A IH: forallb : B,
b < f a ->
foralla : A, f a = b -> Accessible R a a': A a'_a: a' < a
Accessible R a'
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a: A IH: forallb : B,
b < f a ->
foralla : A, f a = b -> Accessible R a a': A a'_a: a' < a
f a' < f a
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a: A IH: forallb : B,
b < f a ->
foralla : A, f a = b -> Accessible R a a': A a'_a: a' < a
f a' = f a'
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a: A IH: forallb : B,
b < f a ->
foralla : A, f a = b -> Accessible R a a': A a'_a: a' < a
f a' < f a
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a: A IH: forallb : B,
b < f a ->
foralla : A, f a = b -> Accessible R a a': A a'_a: a' < a
a' < a
exact a'_a.
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a: A IH: forallb : B,
b < f a ->
foralla : A, f a = b -> Accessible R a a': A a'_a: a' < a
f a' = f a'
reflexivity.
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f
Transitive R
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, b, c: A a_b: R a b b_c: R b c
R a c
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, b, c: A a_b: R a b b_c: R b c
f a < f c
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, b, c: A a_b: R a b b_c: R b c fa_fc: f a < f c
R a c
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, b, c: A a_b: R a b b_c: R b c
f a < f c
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, b, c: A a_b: R a b b_c: R b c
f a < f b
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, b, c: A a_b: R a b b_c: R b c
f b < f c
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, b, c: A a_b: R a b b_c: R b c
f a < f b
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, b, c: A a_b: R a b b_c: R b c
a < b
exact a_b.
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, b, c: A a_b: R a b b_c: R b c
f b < f c
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, b, c: A a_b: R a b b_c: R b c
b < c
exact b_c.
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, b, c: A a_b: R a b b_c: R b c fa_fc: f a < f c
R a c
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, b, c: A a_b: R a b b_c: R b c fa_fc: f a < f c
{a' : A & ((a' < c) * (f a' = f a))%type} -> R a c
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, b, c: A a_b: R a b b_c: R b c fa_fc: f a < f c a': A a'_c: a' < c fa'_fa: f a' = f a
R a c
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, b, c: A a_b: R a b b_c: R b c fa_fc: f a < f c a': A a'_c: a' < c fa'_fa: a' = a
R a c
A: Type IsHSet0: IsHSet A R: Lt A mere: is_mere_relation A R B: Type Q: Lt B H: IsOrdinal B Q f: A -> B H0: IsInjective f is_simulation: IsSimulation f a, b, c: A a_b: R a b b_c: R b c fa_fc: f a < f c a'_c: a < c
R a c
exact a'_c.Qed.(** * Initial segments *)
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R a: A
Ordinal
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R a: A
Ordinal
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R a: A
IsOrdinal {b : A & smalltype (b < a)} lt
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R a: A
is_mere_relation {b : A & smalltype (b < a)} lt
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R a: A
Lt A
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R a: A
IsOrdinal A ?Q
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R a: A
IsSimulation pr1
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R a: A
is_mere_relation {b : A & smalltype (b < a)} lt
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R a: A
forallxy : {b : A & smalltype (R b a)},
IsHProp (R x.1 y.1)
exact _.
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R a: A
Lt A
exact _.
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R a: A
IsOrdinal A R
exact _.
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R a: A
IsSimulation pr1
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R a: A
foralla0a' : {b : A & smalltype (b < a)},
a0 < a' -> a0.1 < a'.1
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R a: A
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
(↓a).1 <~> (↓(f a)).1
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
↓a -> ↓(f a)
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
↓(f a) -> ↓a
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
?f o ?g == idmap
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
?g o ?f == idmap
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
↓a -> ↓(f a)
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: ↓a
↓(f a)
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: ↓a
smalltype (f x.1 < f a)
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: ↓a
f x.1 < f a
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: ↓a
x.1 < a
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: ↓a
smalltype (x.1 < a)
exact x.2.
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
↓(f a) -> ↓a
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: ↓(f a)
↓a
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: ↓(f a)
x.1 < f a
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: ↓(f a) x_fa: x.1 < f a
↓a
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: ↓(f a)
x.1 < f a
exact ((equiv_smalltype _) x.2).
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: ↓(f a) x_fa: x.1 < f a
↓a
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: ↓(f a) x_fa: x.1 < f a a': A a'_a: a' < a
↓a
exact (a'; (equiv_smalltype _)^-1 a'_a).
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
(funx : ↓a =>
(f x.1;
(equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(letX := equiv_fun (equiv_smalltype (x.1 < a))
in
X x.2))))
o (funx : ↓(f a) =>
letx_fa := equiv_smalltype (x.1 < f a) x.2inlets := simulation_is_minimal f x_fa in
(fun (a' : A) (proj2 : (a' < a) * (f a' = x.1)) =>
(fun (a'_a : a' < a) (_ : f a' = x.1) =>
(a'; (equiv_smalltype (a' < a))^-1 a'_a))
(fst proj2) (snd proj2)) s.1 s.2) == idmap
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
(funx : {b : B & smalltype (b < f a)} =>
(f
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1;
(equiv_smalltype
(f
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype
((simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1 < a)
((equiv_smalltype
((simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1 <
a))^-1
(fst
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).2)))))) ==
idmap
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : B & smalltype (b < f a)}
(f
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1;
(equiv_smalltype
(f
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype
((simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1 < a)
((equiv_smalltype
((simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1 <
a))^-1
(fst
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).2))))) =
x
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : B & smalltype (b < f a)}
f
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1 = x.1
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : B & smalltype (b < f a)}
x.1 < f a
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : B & smalltype (b < f a)} x_fa:= ?Goal: x.1 < f a
f
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1 = x.1
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : B & smalltype (b < f a)}
x.1 < f a
exact (equiv_smalltype _ x.2).
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : B & smalltype (b < f a)} x_fa:= equiv_smalltype (x.1 < f a) x.2: x.1 < f a
f
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1 = x.1
exact (snd (simulation_is_minimal f x_fa).2).
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
(funx : ↓(f a) =>
letx_fa := equiv_smalltype (x.1 < f a) x.2inlets := simulation_is_minimal f x_fa in
(fun (a' : A) (proj2 : (a' < a) * (f a' = x.1)) =>
(fun (a'_a : a' < a) (_ : f a' = x.1) =>
(a'; (equiv_smalltype (a' < a))^-1 a'_a))
(fst proj2) (snd proj2)) s.1 s.2)
o (funx : ↓a =>
(f x.1;
(equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(letX :=
equiv_fun (equiv_smalltype (x.1 < a)) in
X x.2)))) == idmap
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
(funx : {b : A & smalltype (b < a)} =>
((simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).1;
(equiv_smalltype
((simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).1 <
a))^-1
(fst
(simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).2))) ==
idmap
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : A & smalltype (b < a)}
((simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).1;
(equiv_smalltype
((simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).1 <
a))^-1
(fst
(simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).2)) =
x
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : A & smalltype (b < a)}
(simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).1 =
x.1
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : A & smalltype (b < a)}
x.1 < a
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : A & smalltype (b < a)} x_a:= ?Goal: x.1 < a
(simulation_is_minimal f
(equiv_smalltype
(f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).1 =
x.1
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : A & smalltype (b < a)}
x.1 < a
exact (equiv_smalltype _ x.2).
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : A & smalltype (b < a)} x_a:= equiv_smalltype (x.1 < a) x.2: x.1 < a
(simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).1 =
x.1
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : A & smalltype (b < a)} x_a:= equiv_smalltype (x.1 < a) x.2: x.1 < a
f
(simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).1 =
f x.1
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : A & smalltype (b < a)} x_a:= equiv_smalltype (x.1 < a) x.2: x.1 < a
f
(simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).1 =
f x.1
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : A & smalltype (b < a)} x_a:= equiv_smalltype (x.1 < a) x.2: x.1 < a
f
(simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).1 =
f x.1
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : A & smalltype (b < a)} x_a:= equiv_smalltype (x.1 < a) x.2: x.1 < a
f
(simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).1 =
f x.1
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A x: {b : A & smalltype (b < a)} x_a:= equiv_smalltype (x.1 < a) x.2: x.1 < a
f
(simulation_is_minimal f
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))).1 = f x.1
exact (snd (simulation_is_minimal f (simulation_is_hom f x_a)).2).
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
(funf0 : (↓a).1 <~> (↓(f a)).1 =>
foralla0a' : (↓a).1,
(↓a).2 a0 a' <-> (↓(f a)).2 (f0 a0) (f0 a'))
(equiv_adjointify
(funx : ↓a =>
(f x.1;
(equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(letX :=
equiv_fun (equiv_smalltype (x.1 < a)) in
X x.2))))
(funx : ↓(f a) =>
letx_fa := equiv_smalltype (x.1 < f a) x.2inlets := simulation_is_minimal f x_fa in
(fun (a' : A) (proj2 : (a' < a) * (f a' = x.1))
=>
(fun (a'_a : a' < a) (_ : f a' = x.1) =>
(a'; (equiv_smalltype (a' < a))^-1 a'_a))
(fst proj2) (snd proj2)) s.1 s.2)
(((funx : {b : B & smalltype (b < f a)} =>
path_sigma_hprop
(f
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1;
(equiv_smalltype
(f
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1 <
f a))^-1
(simulation_is_hom f
(equiv_smalltype
((simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1 <
a)
((equiv_smalltype
((simulation_is_minimal f
(equiv_smalltype (...) x.2)).1 <
a))^-1
(fst
(simulation_is_minimal f
(equiv_smalltype
(x.1 < f a) x.2)).2)))))
x
((let__transparent_assert_hypothesis :=
equiv_smalltype (x.1 < f a) x.2in
snd
(simulation_is_minimal f
__transparent_assert_hypothesis).2)
:
(f
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1;
(equiv_smalltype
(f
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1 <
f a))^-1
(simulation_is_hom f
(equiv_smalltype
((simulation_is_minimal f
(equiv_smalltype (x.1 < ...)
x.2)).1 < a)
((equiv_smalltype
((simulation_is_minimal f ...).1 <
a))^-1
(fst
(simulation_is_minimal f
(equiv_smalltype ... x.2)).2))))).1 =
x.1))
:
(funx : {b : B & smalltype (b < f a)} =>
(f
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1;
(equiv_smalltype
(f
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1 <
f a))^-1
(simulation_is_hom f
(equiv_smalltype
((simulation_is_minimal f
(equiv_smalltype (x.1 < f a) x.2)).1 <
a)
((equiv_smalltype
((simulation_is_minimal f
(equiv_smalltype (...) x.2)).1 <
a))^-1
(fst
(simulation_is_minimal f
(equiv_smalltype (x.1 < f a)
x.2)).2)))))) == idmap)
:
(funx : ↓a =>
(f x.1;
(equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(letX :=
equiv_fun (equiv_smalltype (x.1 < a))
in
X x.2))))
o (funx : ↓(f a) =>
letx_fa := equiv_smalltype (x.1 < f a) x.2inlets := simulation_is_minimal f x_fa in
(fun (a' : A)
(proj2 : (a' < a) * (f a' = x.1)) =>
(fun (a'_a : a' < a) (_ : f a' = x.1) =>
(a'; (equiv_smalltype (a' < a))^-1 a'_a))
(fst proj2) (snd proj2)) s.1 s.2) == idmap)
(((funx : {b : A & smalltype (b < a)} =>
path_sigma_hprop
((simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).1;
(equiv_smalltype
((simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (...) x.2))))).1 <
a))^-1
(fst
(simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a)
x.2))))).2)) x
((let__transparent_assert_hypothesis :=
equiv_smalltype (x.1 < a) x.2in
injective f
(simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a)
x.2))))).1 x.1
(((internal_paths_rew_r
(funl : ... < ... =>
f (...).1 = f x.1)
(snd
(simulation_is_minimal f (...)).2)
(eisretr (equiv_smalltype (...))
(simulation_is_hom f (...)))
:
f
(simulation_is_minimal f
(equiv_smalltype ... ...)).1 =
f x.1)
:
f
(simulation_is_minimal f
(equiv_smalltype (... < ...)
(...^-1 ...))).1 = f x.1)
:
f
(simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype ...)^-1
(simulation_is_hom f ...)))).1 =
f x.1))
:
((simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).1;
(equiv_smalltype
((simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype ...)^-1
(simulation_is_hom f ...)))).1 <
a))^-1
(fst
(simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (... < ...))^-1
(simulation_is_hom f
(equiv_smalltype ... x.2))))).2)).1 =
x.1))
:
(funx : {b : A & smalltype (b < a)} =>
((simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a) x.2))))).1;
(equiv_smalltype
((simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (...) x.2))))).1 <
a))^-1
(fst
(simulation_is_minimal f
(equiv_smalltype (f x.1 < f a)
((equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(equiv_smalltype (x.1 < a)
x.2))))).2))) == idmap)
:
(funx : ↓(f a) =>
letx_fa := equiv_smalltype (x.1 < f a) x.2inlets := simulation_is_minimal f x_fa in
(fun (a' : A) (proj2 : (a' < a) * (f a' = x.1))
=>
(fun (a'_a : a' < a) (_ : f a' = x.1) =>
(a'; (equiv_smalltype (a' < a))^-1 a'_a))
(fst proj2) (snd proj2)) s.1 s.2)
o (funx : ↓a =>
(f x.1;
(equiv_smalltype (f x.1 < f a))^-1
(simulation_is_hom f
(letX :=
equiv_fun (equiv_smalltype (x.1 < a))
in
X x.2)))) == idmap))
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
foralla0a' : {b : A & smalltype (b < a)},
a0.1 < a'.1 <-> f a0.1 < f a'.1
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a, x: A x_a: smalltype (x < a) y: A y_a: smalltype (y < a)
x < y <-> f x < f y
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a, x: A x_a: smalltype (x < a) y: A y_a: smalltype (y < a)
x < y -> f x < f y
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a, x: A x_a: smalltype (x < a) y: A y_a: smalltype (y < a)
f x < f y -> x < y
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a, x: A x_a: smalltype (x < a) y: A y_a: smalltype (y < a)
x < y -> f x < f y
exact (simulation_is_hom f).
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a, x: A x_a: smalltype (x < a) y: A y_a: smalltype (y < a)
f x < f y -> x < y
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a, x: A x_a: smalltype (x < a) y: A y_a: smalltype (y < a) fx_fy: f x < f y
x < y
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a, x: A x_a: smalltype (x < a) y: A y_a: smalltype (y < a) fx_fy: f x < f y a': A a'_y: a' < y p: f a' = f x
x < y
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a, x: A x_a: smalltype (x < a) y: A y_a: smalltype (y < a) fx_fy: f x < f y a': A a'_y: a' < y p: a' = x
x < y
H: PropResizing A: Type R: Lt A H0: IsOrdinal A R B: Type Q: Lt B H1: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a, x: A x_a: smalltype (x < a) y: A y_a: smalltype (y < a) fx_fy: f x < f y a'_y: x < y
x < y
exact a'_y.Qed.
H: Univalence H0: PropResizing A: Type R: Lt A H1: IsOrdinal A R B: Type Q: Lt B H2: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
↓(f a) = ↓a
H: Univalence H0: PropResizing A: Type R: Lt A H1: IsOrdinal A R B: Type Q: Lt B H2: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
↓(f a) = ↓a
H: Univalence H0: PropResizing A: Type R: Lt A H1: IsOrdinal A R B: Type Q: Lt B H2: IsOrdinal B Q f: A -> B is_simulation: IsSimulation f a: A
Isomorphism ↓(f a) ↓a
apply (equiv_initial_segment_simulation f).Qed.(** * `Ordinal` is an ordinal *)Instancelt_Ordinal@{carrier relation +} `{PropResizing}
: Lt Ordinal@{carrier relation}
:= funAB => existsb : B, A = ↓b.
exact p.Qed.Definitionbound `{PropResizing}
{A B : Ordinal} (H : A < B)
: B
:= H.1.(* We use this notation to hide the proof of A < B that `bound` takes as an argument *)Notation"A ◁ B" := (@bound A B _) (at level70) : Ordinals.Definitionbound_property `{PropResizing}
{A B : Ordinal} (H : A < B)
: A = ↓(bound H)
:= H.2.
H: PropResizing H0: Univalence A: Ordinal a, b: A
a < b <-> ↓a < ↓b
H: PropResizing H0: Univalence A: Ordinal a, b: A
a < b <-> ↓a < ↓b
H: PropResizing H0: Univalence A: Ordinal a, b: A
a < b -> ↓a < ↓b
H: PropResizing H0: Univalence A: Ordinal a, b: A
↓a < ↓b -> a < b
H: PropResizing H0: Univalence A: Ordinal a, b: A
a < b -> ↓a < ↓b
H: PropResizing H0: Univalence A: Ordinal a, b: A a_b: a < b
↓a < ↓b
H: PropResizing H0: Univalence A: Ordinal a, b: A a_b: a < b
↓a = ↓(in_ a a_b)
exact (path_initial_segment_simulation out (in_ a a_b)).
H: PropResizing H0: Univalence A: Ordinal a, b: A
↓a < ↓b -> a < b
H: PropResizing H0: Univalence A: Ordinal a, b: A a_b: ↓a < ↓b
a < b
H: PropResizing H0: Univalence A: Ordinal a, b: A a_b: ↓a < ↓b
a = out ((H ◁ ↓a) a_b)
H: PropResizing H0: Univalence A: Ordinal a, b: A a_b: ↓a < ↓b
out ((H ◁ ↓a) a_b) < b
H: PropResizing H0: Univalence A: Ordinal a, b: A a_b: ↓a < ↓b
a = out ((H ◁ ↓a) a_b)
H: PropResizing H0: Univalence A: Ordinal a, b: A a_b: ↓a < ↓b
↓a = ↓(out ((H ◁ ↓a) a_b))
H: PropResizing H0: Univalence A: Ordinal a, b: A a_b: ↓a < ↓b
↓a = ↓((H ◁ ↓a) a_b)
apply bound_property.
H: PropResizing H0: Univalence A: Ordinal a, b: A a_b: ↓a < ↓b
out ((H ◁ ↓a) a_b) < b
apply initial_segment_property.Qed.
H: PropResizing H0: Univalence
IsOrdinal Ordinal lt
H: PropResizing H0: Univalence
IsOrdinal Ordinal lt
H: PropResizing H0: Univalence
IsHSet Ordinal
H: PropResizing H0: Univalence
is_mere_relation Ordinal lt
H: PropResizing H0: Univalence
Extensional lt
H: PropResizing H0: Univalence
WellFounded lt
H: PropResizing H0: Univalence
Transitive lt
H: PropResizing H0: Univalence
IsHSet Ordinal
exact _.
H: PropResizing H0: Univalence
is_mere_relation Ordinal lt
exact is_mere_relation_lt_on_Ordinal.
H: PropResizing H0: Univalence
Extensional lt
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
A = B
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
A <~> B
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
forallaa' : A, a < a' <-> ?f a < ?f a'
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
A <~> B
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
A -> B
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
B -> A
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
?f o ?g == idmap
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
?g o ?f == idmap
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
A -> B
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
foralla : A, ↓a < B
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B lt_B: foralla : A, ↓a < B
A -> B
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
foralla : A, ↓a < B
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B a: A
↓a < B
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B a: A
↓a < A
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B a: A
↓a = ↓a
reflexivity.
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B lt_B: foralla : A, ↓a < B
A -> B
exact (funa => bound (lt_B a)).
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
B -> A
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
forallb : B, ↓b < A
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B lt_A: forallb : B, ↓b < A
B -> A
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
forallb : B, ↓b < A
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B b: B
↓b < A
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B b: B
↓b < B
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B b: B
↓b = ↓b
reflexivity.
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B lt_A: forallb : B, ↓b < A
B -> A
exact (funb => bound (lt_A b)).
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
(letlt_B :=
funa : A =>
letX := func : Ordinal => fst (H1 c) in
X ↓a (a; 1%path) infuna : A => (H ◁ ↓a) (lt_B a))
o (letlt_A :=
funb : B =>
letX := func : Ordinal => snd (H1 c) in
X ↓b (b; 1%path) infunb : B => (H ◁ ↓b) (lt_A b)) == idmap
H: PropResizing H0: Univalence A, B: Ordinal H1: forallc : Ordinal, c < A <-> c < B
(funX : ↓B =>
(fun (C : Ordinal) (HC : smalltype (C < B)) =>
letX0 :=
fun (X0 : Type) (IsSmall : IsSmall X0) =>
equiv_fun (equiv_smalltype X0) inletHC0 :=
X0 (C < B)
(issmall_hprop (C < B)
(ordinal_relation_is_mere C B)) HC in
(H ◁ C) HC0) X.1 X.2)
o (funb : B =>
(↓b;
letX :=
fun (X : Type) (IsSmall : IsSmall X) =>
equiv_isequiv (equiv_smalltype X) inletX0 :=
fun (X0 : Type) (IsSmall : IsSmall X0) =>
(equiv_smalltype X0)^-1in
X0 (↓b < B)
(issmall_hprop (↓b < B)
(ordinal_relation_is_mere ↓b B)) (b; 1%path))) ==
idmap
H: PropResizing H0: Univalence B: Ordinal
(funx : ordinal_carrier B =>
(H ◁ ↓x)
(equiv_smalltype (↓x < B)
((equiv_smalltype (↓x < B))^-1 (x; 1%path)))) ==
idmap
H: PropResizing H0: Univalence B: Ordinal x: ordinal_carrier B
(H ◁ ↓x)
(equiv_smalltype (↓x < B)
((equiv_smalltype (↓x < B))^-1 (x; 1%path))) = x
H: PropResizing H0: Univalence B: Ordinal x: ordinal_carrier B
(H ◁ ↓x) (x; 1%path) = x
reflexivity.
H: PropResizing H0: Univalence B: Ordinal
(funf : B.1 <~> (↓B).1 =>
forallaa' : B.1, B.2 a a' <-> (↓B).2 (f a) (f a'))
(equiv_adjointify
(funb : B =>
(↓b;
letX :=
fun (X : Type) (IsSmall : IsSmall X) =>
equiv_isequiv (equiv_smalltype X) inletX0 :=
fun (X0 : Type) (IsSmall : IsSmall X0) =>
(equiv_smalltype X0)^-1in
X0 (↓b < B)
(issmall_hprop (↓b < B)
(ordinal_relation_is_mere ↓b B))
(b; 1%path)))
(funX : ↓B =>
(fun (C : Ordinal) (HC : smalltype (C < B)) =>
letX0 :=
fun (X0 : Type) (IsSmall : IsSmall X0) =>
equiv_fun (equiv_smalltype X0) inletHC0 :=
X0 (C < B)
(issmall_hprop (C < B)
(ordinal_relation_is_mere C B)) HC in
(H ◁ C) HC0) X.1 X.2)
(((funx : {b : Ordinal & smalltype (b < B)} =>
(fun (C : Ordinal) (HC : smalltype (C < B)) =>
path_sigma_hprop
(↓((H ◁ C) (equiv_smalltype (C < B) HC));
(equiv_smalltype
(↓((H ◁ C) (equiv_smalltype (C < B) HC)) <
B))^-1
((H ◁ C) (equiv_smalltype (C < B) HC);
1%path)) (C; HC)
((bound_property
(equiv_smalltype (C < B) HC))^
:
(↓((H ◁ C) (equiv_smalltype (C < B) HC));
(equiv_smalltype
(↓((H ◁ C) (equiv_smalltype (...) HC)) <
B))^-1
((H ◁ C) (equiv_smalltype (C < B) HC);
1%path)).1 = (C; HC).1)) x.1 x.2)
:
(funx : {b : Ordinal & smalltype (b < B)} =>
(↓((H ◁ x.1) (equiv_smalltype (x.1 < B) x.2));
(equiv_smalltype
(↓((H ◁ x.1)
(equiv_smalltype (x.1 < B) x.2)) < B))^-1
((H ◁ x.1) (equiv_smalltype (x.1 < B) x.2);
1%path))) == idmap)
:
(funb : B =>
(↓b;
letX :=
fun (X : Type) (IsSmall : IsSmall X) =>
equiv_isequiv (equiv_smalltype X) inletX0 :=
fun (X0 : Type) (IsSmall : IsSmall X0) =>
(equiv_smalltype X0)^-1in
X0 (↓b < B)
(issmall_hprop (↓b < B)
(ordinal_relation_is_mere ↓b B))
(b; 1%path)))
o (funX : ↓B =>
(fun (C : Ordinal) (HC : smalltype (C < B))
=>
letX0 :=
fun (X0 : Type) (IsSmall : IsSmall X0) =>
equiv_fun (equiv_smalltype X0) inletHC0 :=
X0 (C < B)
(issmall_hprop (C < B)
(ordinal_relation_is_mere C B)) HC in
(H ◁ C) HC0) X.1 X.2) == idmap)
(((funx : ordinal_carrier B =>
internal_paths_rew_r
(funl : ↓x < B => (H ◁ ↓x) l = x) 1%path
(eisretr (equiv_smalltype (↓x < B))
(x; 1%path)))
:
(funx : ordinal_carrier B =>
(H ◁ ↓x)
(equiv_smalltype (↓x < B)
((equiv_smalltype (↓x < B))^-1
(x; 1%path)))) == idmap)
:
(funX : ↓B =>
(fun (C : Ordinal) (HC : smalltype (C < B)) =>
letX0 :=
fun (X0 : Type) (IsSmall : IsSmall X0) =>
equiv_fun (equiv_smalltype X0) inletHC0 :=
X0 (C < B)
(issmall_hprop (C < B)
(ordinal_relation_is_mere C B)) HC in
(H ◁ C) HC0) X.1 X.2)
o (funb : B =>
(↓b;
letX :=
fun (X : Type) (IsSmall : IsSmall X) =>
equiv_isequiv (equiv_smalltype X) inletX0 :=
fun (X0 : Type) (IsSmall : IsSmall X0) =>
(equiv_smalltype X0)^-1in
X0 (↓b < B)
(issmall_hprop (↓b < B)
(ordinal_relation_is_mere ↓b B))
(b; 1%path))) == idmap))
H: PropResizing H0: Univalence B: Ordinal
forallaa' : ordinal_carrier B, a < a' <-> ↓a < ↓a'
H: PropResizing H0: Univalence B: Ordinal b, b': ordinal_carrier B
b < b' <-> ↓b < ↓b'
apply isembedding_initial_segment.Qed.(** But an ordinal isn't isomorphic to any initial segment of itself. *)
H: PropResizing H0: Univalence O: Ordinal a: O
Isomorphism O ↓a -> Empty
H: PropResizing H0: Univalence O: Ordinal a: O
Isomorphism O ↓a -> Empty
H: PropResizing H0: Univalence O: Ordinal a: O p: O = ↓a
Empty
H: PropResizing H0: Univalence O: Ordinal a: O p: O = ↓a
O < O
H: PropResizing H0: Univalence O: Ordinal a: O p: O = ↓a
O = ↓a
exact p.Qed.(** * Ordinal successor *)
A: Ordinal
Ordinal
A: Ordinal
Ordinal
A: Ordinal carrier:= (A + Unit)%type: Type
Ordinal
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type
Ordinal
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type
IsOrdinal carrier lt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type
IsHSet carrier
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type
is_mere_relation carrier lt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type
Extensional lt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type
WellFounded lt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type
Transitive lt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type
IsHSet carrier
exact _.
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type
is_mere_relation carrier lt
intros [x | ?] [y | ?]; cbn; exact _.
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type
Extensional lt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type x, y: A H: forallc : carrier, c < inl x <-> c < inl y
inl x = inl y
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type x: A H: forallc : carrier, c < inl x <-> c < inr tt
inl x = inr tt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type y: A H: forallc : carrier, c < inr tt <-> c < inl y
inr tt = inl y
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type H: forallc : carrier, c < inr tt <-> c < inr tt
inr tt = inr tt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type x, y: A H: forallc : carrier, c < inl x <-> c < inl y
inl x = inl y
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type x, y: A H: forallc : carrier, c < inl x <-> c < inl y
x = y
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type x, y: A H: forallc : carrier, c < inl x <-> c < inl y
forallc : A, c < x <-> c < y
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type x, y: A H: forallc : carrier, c < inl x <-> c < inl y z: A
z < x <-> z < y
exact (H (inl z)).
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type x: A H: forallc : carrier, c < inl x <-> c < inr tt
inl x = inr tt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type x: A H: forallc : carrier, c < inl x <-> c < inr tt H0: relation (inl x) (inl x)
inl x = inr tt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type x: A H: forallc : carrier, c < inl x <-> c < inr tt
relation (inl x) (inl x)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type x: A H: forallc : carrier, c < inl x <-> c < inr tt H0: relation (inl x) (inl x)
inl x = inr tt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type x: A H: forallc : carrier, c < inl x <-> c < inr tt H0: x < x
inl x = inr tt
destruct (irreflexivity _ _ H0).
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type x: A H: forallc : carrier, c < inl x <-> c < inr tt
relation (inl x) (inl x)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type x: A H: forallc : carrier, c < inl x <-> c < inr tt
inl x < inr tt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type x: A H: forallc : carrier, c < inl x <-> c < inr tt
Unit
exact tt.
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type y: A H: forallc : carrier, c < inr tt <-> c < inl y
inr tt = inl y
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type y: A H: forallc : carrier, c < inr tt <-> c < inl y H0: relation (inl y) (inl y)
inr tt = inl y
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type y: A H: forallc : carrier, c < inr tt <-> c < inl y
relation (inl y) (inl y)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type y: A H: forallc : carrier, c < inr tt <-> c < inl y H0: relation (inl y) (inl y)
inr tt = inl y
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type y: A H: forallc : carrier, c < inr tt <-> c < inl y H0: y < y
inr tt = inl y
destruct (irreflexivity _ _ H0).
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type y: A H: forallc : carrier, c < inr tt <-> c < inl y
relation (inl y) (inl y)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type y: A H: forallc : carrier, c < inr tt <-> c < inl y
inl y < inr tt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type y: A H: forallc : carrier, c < inr tt <-> c < inl y
Unit
exact tt.
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type H: forallc : carrier, c < inr tt <-> c < inr tt
inr tt = inr tt
reflexivity.
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type
WellFounded lt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type
foralla : A, Accessible relation (inl a)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type H: foralla : A, Accessible relation (inl a)
WellFounded lt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type
foralla : A, Accessible relation (inl a)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type a: A
Accessible relation (inl a)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type a: A IH: forallb : A,
b < a -> Accessible relation (inl b)
Accessible relation (inl a)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type a: A IH: forallb : A,
b < a -> Accessible relation (inl b) b: A H: b < a
Accessible relation (inl b)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type a: A IH: forallb : A,
b < a -> Accessible relation (inl b) H: Empty
Accessible relation (inr tt)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type a: A IH: forallb : A,
b < a -> Accessible relation (inl b) b: A H: b < a
Accessible relation (inl b)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type a: A IH: forallb : A,
b < a -> Accessible relation (inl b) b: A H: b < a
b < a
exact H.
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type a: A IH: forallb : A,
b < a -> Accessible relation (inl b) H: Empty
Accessible relation (inr tt)
destruct H.
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type H: foralla : A, Accessible relation (inl a)
WellFounded lt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type H: foralla : A, Accessible relation (inl a) x: A
Accessible lt (inl x)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type H: foralla : A, Accessible relation (inl a)
Accessible lt (inr tt)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type H: foralla : A, Accessible relation (inl a) x: A
Accessible lt (inl x)
apply H.
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type H: foralla : A, Accessible relation (inl a)
Accessible lt (inr tt)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type H: foralla : A, Accessible relation (inl a) b: A H0: Unit
Accessible lt (inl b)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type H: foralla : A, Accessible relation (inl a) H0: Empty
Accessible lt (inr tt)
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type H: foralla : A, Accessible relation (inl a) b: A H0: Unit
Accessible lt (inl b)
apply H.
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type H: foralla : A, Accessible relation (inl a) H0: Empty
Accessible lt (inr tt)
destruct H0.
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type
Transitive lt
A: Ordinal carrier:= (A + Unit)%type: Type relation:= funxy : carrier =>
match x with
| inl x0 =>
match y with
| inl y0 => x0 < y0
| inr _ => Unit
end
| inr _ =>
match y with
| inl _ | _ => Empty
endend: carrier -> carrier -> Type x, z: A
Unit -> Empty -> x < z
intros _ [].Defined.
H: PropResizing H0: Univalence A: Ordinal
A < successor A
H: PropResizing H0: Univalence A: Ordinal
A < successor A
H: PropResizing H0: Univalence A: Ordinal
A = ↓(inr tt)
H: PropResizing H0: Univalence A: Ordinal
A <~> ↓(inr tt)
H: PropResizing H0: Univalence A: Ordinal
forallaa' : A, a < a' <-> ?f a < ?f a'
H: PropResizing H0: Univalence A: Ordinal
A <~> ↓(inr tt)
H: PropResizing H0: Univalence A: Ordinal
A -> ↓(inr tt)
H: PropResizing H0: Univalence A: Ordinal
↓(inr tt) -> A
H: PropResizing H0: Univalence A: Ordinal
?f o ?g == idmap
H: PropResizing H0: Univalence A: Ordinal
?g o ?f == idmap
H: PropResizing H0: Univalence A: Ordinal
A -> ↓(inr tt)
H: PropResizing H0: Univalence A: Ordinal a: A
↓(inr tt)
H: PropResizing H0: Univalence A: Ordinal a: A
successor A
H: PropResizing H0: Univalence A: Ordinal a: A
?x < inr tt
H: PropResizing H0: Univalence A: Ordinal a: A
successor A
exact (inl a).
H: PropResizing H0: Univalence A: Ordinal a: A
inl a < inr tt
exact tt.
H: PropResizing H0: Univalence A: Ordinal
↓(inr tt) -> A
H: PropResizing H0: Univalence A: Ordinal a: ordinal_carrier A Ha: smalltype Unit
(funa : A => in_ (inl a) tt)
o (funX : ↓(inr tt) =>
(funproj1 : successor A =>
match
proj1 as s return (smalltype (s < inr tt) -> A)
with
| inl t =>
(fun (a : A) (_ : smalltype (inl a < inr tt))
=> a : A) t
| inr u =>
(funu0 : Unit =>
match
u0 as u1
return (smalltype (inr u1 < inr tt) -> A)
with
| tt =>
funHa : smalltype (inr tt < inr tt) =>
(letX0 :=
fun (X0 : Type) (IsSmall : IsSmall X0)
=> equiv_fun (equiv_smalltype X0) inletHa0 :=
X0 Empty
(issmall_hprop Empty
(istrunc_S Empty (... => ...)))
Ha inmatch
Ha0 return (ordinal_carrier A)
withend)
:
A
end) u
end) X.1 X.2) == idmap
H: PropResizing H0: Univalence A: Ordinal a: A Ha: smalltype (inl a < inr tt)
in_
(inl
(letX :=
fun (X : Type) (IsSmall : IsSmall X) =>
equiv_fun (equiv_smalltype X) inletHa :=
X Empty
(issmall_hprop Empty
(istrunc_S Empty
(funxy : Empty =>
match
x as e
return
(forally0 : Empty,
Contr (e = y0))
withend y))) Ha inmatch Ha return (ordinal_carrier A) withend)) tt = (inr tt; Ha)
destruct (equiv_smalltype _ Ha).
H: PropResizing H0: Univalence A: Ordinal
(funX : ↓(inr tt) =>
(funproj1 : successor A =>
match
proj1 as s return (smalltype (s < inr tt) -> A)
with
| inl t =>
(fun (a : A) (_ : smalltype (inl a < inr tt)) =>
a : A) t
| inr u =>
(funu0 : Unit =>
match
u0 as u1
return (smalltype (inr u1 < inr tt) -> A)
with
| tt =>
funHa : smalltype (inr tt < inr tt) =>
(letX0 :=
fun (X0 : Type) (IsSmall : IsSmall X0)
=> equiv_fun (equiv_smalltype X0) inletHa0 :=
X0 Empty
(issmall_hprop Empty
(istrunc_S Empty (... => ...))) Ha
inmatch Ha0 return (ordinal_carrier A) withend)
:
A
end) u
end) X.1 X.2) o (funa : A => in_ (inl a) tt) ==
idmap
H: PropResizing H0: Univalence A: Ordinal a: A
match
(in_ (inl a) tt).1as s
return (smalltype (s < inr tt) -> A)
with
| inl t => fun_ : smalltype (inl t < inr tt) => t
| inr u =>
match
u as u0
return (smalltype (inr u0 < inr tt) -> A)
with
| tt =>
funHa : smalltype (inr tt < inr tt) =>
letX :=
fun (X : Type) (IsSmall : IsSmall X) =>
equiv_fun (equiv_smalltype X) inletHa0 :=
X Empty
(issmall_hprop Empty
(istrunc_S Empty
(funxy : Empty =>
match
x as e
return
(forally0 : Empty,
Contr (e = y0))
withend y))) Ha inmatch Ha0 return (ordinal_carrier A) withendendend (in_ (inl a) tt).2 = a
reflexivity.
H: PropResizing H0: Univalence A: Ordinal
forallaa' : A,
a < a' <->
equiv_adjointify (funa0 : A => in_ (inl a0) tt)
(funX : ↓(inr tt) =>
(funproj1 : successor A =>
match
proj1 as s return (smalltype (s < inr tt) -> A)
with
| inl t =>
(fun (a0 : A)
(_ : smalltype (inl a0 < inr tt)) => a0 : A)
t
| inr u =>
(funu0 : Unit =>
match
u0 as u1
return (smalltype (inr u1 < inr tt) -> A)
with
| tt =>
funHa : smalltype (inr tt < inr tt) =>
(letX0 :=
fun (X0 : Type) (IsSmall : IsSmall X0)
=> equiv_fun (equiv_smalltype X0) inletHa0 :=
X0 Empty
(issmall_hprop Empty
(istrunc_S Empty ...)) Ha inmatch
Ha0 return (ordinal_carrier A)
withend)
:
A
end) u
end) X.1 X.2)
((funx : ↓(inr tt) =>
(funproj1 : successor A =>
match
proj1 as s
return
(forallproj2 : smalltype (s < inr tt),
in_
(inl
(match s as s0 return ... with
| inl t => fun ... => t
| inr u =>
match ... with
| ... ...
endend proj2)) tt = (s; proj2))
with
| inl t =>
(fun (a0 : A)
(Ha : smalltype (inl a0 < inr tt)) =>
(ap11 1
(letX := istrunc_smalltype Unit (-1) in
path_ishprop
((equiv_smalltype Unit)^-1 tt) Ha)
:
(inl a0;
(equiv_smalltype (inl a0 < inr tt))^-1 tt) =
(inl a0; Ha))
:
in_ (inl a0) tt = (inl a0; Ha)) t
| inr u =>
(funu0 : Unit =>
match
u0 as u1
return
(forallproj2 : smalltype (inr u1 < inr tt),
in_ (inl (...)) tt = (inr u1; proj2))
with
| tt =>
funHa : smalltype (inr tt < inr tt) =>
letl :=
equiv_smalltype (inr tt < inr tt) Ha
inmatch
l return (in_ ... tt = (...; Ha))
withendend) u
end) x.1 x.2)
:
(funa0 : A => in_ (inl a0) tt)
o (funX : ↓(inr tt) =>
(funproj1 : successor A =>
match
proj1 as s
return (smalltype (s < inr tt) -> A)
with
| inl t =>
(fun (a0 : A)
(_ : smalltype (inl a0 < inr tt)) =>
a0 : A) t
| inr u =>
(funu0 : Unit =>
match
u0 as u1
return (smalltype (... < ...) -> A)
with
| tt =>
funHa : smalltype (inr tt < inr tt)
=>
(letX0 :=
fun ... ... => equiv_fun ... inletHa0 := X0 Empty ... Ha inmatch ... withend)
:
A
end) u
end) X.1 X.2) == idmap)
((funa0 : A => 1%path)
:
(funX : ↓(inr tt) =>
(funproj1 : successor A =>
match
proj1 as s return (smalltype (s < inr tt) -> A)
with
| inl t =>
(fun (a0 : A)
(_ : smalltype (inl a0 < inr tt)) =>
a0 : A) t
| inr u =>
(funu0 : Unit =>
match
u0 as u1
return (smalltype (... < ...) -> A)
with
| tt =>
funHa : smalltype (inr tt < inr tt) =>
(letX0 := fun ... ... => equiv_fun ...
inletHa0 := X0 Empty ... Ha inmatch ... withend)
:
A
end) u
end) X.1 X.2) o (funa0 : A => in_ (inl a0) tt) ==
idmap) a <
equiv_adjointify (funa0 : A => in_ (inl a0) tt)
(funX : ↓(inr tt) =>
(funproj1 : successor A =>
match
proj1 as s return (smalltype (s < inr tt) -> A)
with
| inl t =>
(fun (a0 : A)
(_ : smalltype (inl a0 < inr tt)) => a0 : A)
t
| inr u =>
(funu0 : Unit =>
match
u0 as u1
return (smalltype (inr u1 < inr tt) -> A)
with
| tt =>
funHa : smalltype (inr tt < inr tt) =>
(letX0 :=
fun (X0 : Type) (IsSmall : IsSmall X0)
=> equiv_fun (equiv_smalltype X0) inletHa0 :=
X0 Empty
(issmall_hprop Empty
(istrunc_S Empty ...)) Ha inmatch
Ha0 return (ordinal_carrier A)
withend)
:
A
end) u
end) X.1 X.2)
((funx : ↓(inr tt) =>
(funproj1 : successor A =>
match
proj1 as s
return
(forallproj2 : smalltype (s < inr tt),
in_
(inl
(match s as s0 return ... with
| inl t => fun ... => t
| inr u =>
match ... with
| ... ...
endend proj2)) tt = (s; proj2))
with
| inl t =>
(fun (a0 : A)
(Ha : smalltype (inl a0 < inr tt)) =>
(ap11 1
(letX := istrunc_smalltype Unit (-1) in
path_ishprop
((equiv_smalltype Unit)^-1 tt) Ha)
:
(inl a0;
(equiv_smalltype (inl a0 < inr tt))^-1 tt) =
(inl a0; Ha))
:
in_ (inl a0) tt = (inl a0; Ha)) t
| inr u =>
(funu0 : Unit =>
match
u0 as u1
return
(forallproj2 : smalltype (inr u1 < inr tt),
in_ (inl (...)) tt = (inr u1; proj2))
with
| tt =>
funHa : smalltype (inr tt < inr tt) =>
letl :=
equiv_smalltype (inr tt < inr tt) Ha
inmatch
l return (in_ ... tt = (...; Ha))
withendend) u
end) x.1 x.2)
:
(funa0 : A => in_ (inl a0) tt)
o (funX : ↓(inr tt) =>
(funproj1 : successor A =>
match
proj1 as s
return (smalltype (s < inr tt) -> A)
with
| inl t =>
(fun (a0 : A)
(_ : smalltype (inl a0 < inr tt)) =>
a0 : A) t
| inr u =>
(funu0 : Unit =>
match
u0 as u1
return (smalltype (... < ...) -> A)
with
| tt =>
funHa : smalltype (inr tt < inr tt)
=>
(letX0 :=
fun ... ... => equiv_fun ... inletHa0 := X0 Empty ... Ha inmatch ... withend)
:
A
end) u
end) X.1 X.2) == idmap)
((funa0 : A => 1%path)
:
(funX : ↓(inr tt) =>
(funproj1 : successor A =>
match
proj1 as s return (smalltype (s < inr tt) -> A)
with
| inl t =>
(fun (a0 : A)
(_ : smalltype (inl a0 < inr tt)) =>
a0 : A) t
| inr u =>
(funu0 : Unit =>
match
u0 as u1
return (smalltype (... < ...) -> A)
with
| tt =>
funHa : smalltype (inr tt < inr tt) =>
(letX0 := fun ... ... => equiv_fun ...
inletHa0 := X0 Empty ... Ha inmatch ... withend)
:
A
end) u
end) X.1 X.2) o (funa0 : A => in_ (inl a0) tt) ==
idmap) a'
H: PropResizing H0: Univalence A: Ordinal
forallaa' : ordinal_carrier A, a < a' <-> a < a'
H: PropResizing H0: Univalence A: Ordinal a, a': ordinal_carrier A
a < a' <-> a < a'
reflexivity.Qed.(** * Ordinal limit *)SectionImage.Universes i j.(** In the following, there are no constraints between [i] and [j]. *)Context `{PropResizing} `{Funext} {A : Type@{i}} {B : HSet@{j}} (f : A -> B).Local Definitionqkfs := quotient_kernel_factor_small f.Local Definitionimage : Type@{i} := qkfs.1.Local Definitionfactor1 : A -> image := qkfs.2.1.Local Definitionfactor2 : image -> B := qkfs.2.2.1.Local Definitionisinjective_factor2 : IsInjective factor2
:= isinj_embedding _ (snd (fst qkfs.2.2.2)).Local Definitionimage_ind_prop (P : image -> Type@{k}) `{forallx, IsHProp (P x)}
(step : foralla : A, P (factor1 a))
: forallx : image, P x
:= Quotient_ind_hprop _ P step.(** [factor2 o factor1 == f] is definitional, so we don't state that. *)EndImage.
H: Univalence H0: PropResizing X: Type F: X -> Ordinal
Ordinal
H: Univalence H0: PropResizing X: Type F: X -> Ordinal
Ordinal
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal
Ordinal
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type
Ordinal
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
Ordinal
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
IsOrdinal carrier lt
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
IsHSet (image f)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
is_mere_relation (image f) lt
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
Lt (default_TruncType 0 Ordinal ishset_Ordinal)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
IsInjective (factor2 f)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
IsSimulation (factor2 f)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
IsInjective (factor2 f)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
IsSimulation (factor2 f)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
IsInjective (factor2 f)
apply isinjective_factor2.
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
IsSimulation (factor2 f)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
forallaa' : image f,
a < a' -> factor2 f a < factor2 f a'
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
forall (a : image f)
(b : default_TruncType 0 Ordinal ishset_Ordinal),
b < factor2 f a ->
hexists
(funa' : image f =>
((a' < a) * (factor2 f a' = b))%type)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
forallaa' : image f,
a < a' -> factor2 f a < factor2 f a'
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type x, x': image f x_x': x < x'
factor2 f x < factor2 f x'
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type x, x': image f x_x': x < x'
lt_Ordinal (factor2 f x) (factor2 f x')
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type x, x': image f x_x': factor2 f x < factor2 f x'
lt_Ordinal (factor2 f x) (factor2 f x')
exact x_x'.
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
forall (a : image f)
(b : default_TruncType 0 Ordinal ishset_Ordinal),
b < factor2 f a ->
hexists
(funa' : image f =>
((a' < a) * (factor2 f a' = b))%type)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
forallx : image f,
IsHProp
(forallb : default_TruncType 0 Ordinal ishset_Ordinal,
b < factor2 f x ->
hexists
(funa' : image f =>
((a' < x) * (factor2 f a' = b))%type))
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
forall (a : {i : X & F i})
(b : default_TruncType 0 Ordinal ishset_Ordinal),
b < factor2 f (factor1 f a) ->
hexists
(funa' : image f =>
((a' < factor1 f a) * (factor2 f a' = b))%type)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type
forall (a : {i : X & F i})
(b : default_TruncType 0 Ordinal ishset_Ordinal),
b < factor2 f (factor1 f a) ->
hexists
(funa' : image f =>
((a' < factor1 f a) * (factor2 f a' = b))%type)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i}
forallb : default_TruncType 0 Ordinal ishset_Ordinal,
b < factor2 f (factor1 f a) ->
hexists
(funa' : image f =>
((a' < factor1 f a) * (factor2 f a' = b))%type)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i}
forallb : default_TruncType 0 Ordinal ishset_Ordinal,
b < factor2 f (factor1 f a) ->
hexists
(funa' : image f =>
((a' < factor1 f a) * (factor2 f a' = b))%type)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
hexists
(funa' : image f =>
((a' < factor1 f a) * (factor2 f a' = B))%type)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
{a' : image f &
((a' < factor1 f a) * (factor2 f a' = B))%type}
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
((factor1 f (a.1; out ((H0 ◁ B) B_fa)) < factor1 f a) *
(factor2 f (factor1 f (a.1; out ((H0 ◁ B) B_fa))) = B))%type
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
(smalltype
(factor2 f (factor1 f (a.1; out ((H0 ◁ B) B_fa))) <
factor2 f (factor1 f a)) *
(factor2 f (factor1 f (a.1; out ((H0 ◁ B) B_fa))) = B))%type
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
(smalltype (f (a.1; out ((H0 ◁ B) B_fa)) < f a) *
(f (a.1; out ((H0 ◁ B) B_fa)) = B))%type
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
(smalltype (↓(a.1; out ((H0 ◁ B) B_fa)).2 < ↓a.2) *
(↓(a.1; out ((H0 ◁ B) B_fa)).2 = B))%type
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
↓(out ((H0 ◁ B) B_fa)) = B
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
(smalltype (B < ↓a.2) * (B = B))%type
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
↓(out ((H0 ◁ B) B_fa)) = B
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
↓((H0 ◁ B) B_fa) = B
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
B = ↓((H0 ◁ B) B_fa)
apply bound_property.
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
(smalltype (B < ↓a.2) * (B = B))%type
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
smalltype (B < ↓a.2)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
B = B
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
smalltype (B < ↓a.2)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
B < ↓a.2
exact B_fa.
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal carrier:= image f : Type: Type relation:= funAB : carrier =>
smalltype (factor2 f A < factor2 f B) : Type: carrier -> carrier -> Type a: {i : X & F i} B: default_TruncType 0 Ordinal ishset_Ordinal B_fa: B < factor2 f (factor1 f a)
B = B
reflexivity.Defined.Instancele_on_Ordinal : Le Ordinal :=
funAB => existsf : A -> B, IsSimulation f.
H: Univalence H0: PropResizing X: Type F: X -> Ordinal
forallx : X, F x ≤ limit F
H: Univalence H0: PropResizing X: Type F: X -> Ordinal
forallx : X, F x ≤ limit F
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal
forallx : X, F x ≤ limit F
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X
F x ≤ limit F
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X
{f : F x -> limit F & IsSimulation f}
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X
IsSimulation (funu : F x => factor1 f (x; u))
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X
forallaa' : F x,
a < a' -> factor1 f (x; a) < factor1 f (x; a')
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X
forall (a : F x) (b : limit F),
b < factor1 f (x; a) ->
hexists
(funa' : F x =>
((a' < a) * (factor1 f (x; a') = b))%type)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X
forallaa' : F x,
a < a' -> factor1 f (x; a) < factor1 f (x; a')
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u, v: F x u_v: u < v
factor1 f (x; u) < factor1 f (x; v)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u, v: F x u_v: u < v
smalltype (f (x; u) < f (x; v))
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u, v: F x u_v: u < v
f (x; u) < f (x; v)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u, v: F x u_v: u < v
(x; u).2 < (x; v).2
exact u_v.
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X
forall (a : F x) (b : limit F),
b < factor1 f (x; a) ->
hexists
(funa' : F x =>
((a' < a) * (factor1 f (x; a') = b))%type)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x
forallb : limit F,
b < factor1 f (x; u) ->
hexists
(funa' : F x =>
((a' < u) * (factor1 f (x; a') = b))%type)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x
forallx0 : image f,
IsHProp
(x0 < factor1 f (x; u) ->
hexists
(funa' : F x =>
((a' < u) * (factor1 f (x; a') = x0))%type))
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x
foralla : {i : X & F i},
factor1 f a < factor1 f (x; u) ->
hexists
(funa' : F x =>
((a' < u) * (factor1 f (x; a') = factor1 f a))%type)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x
foralla : {i : X & F i},
factor1 f a < factor1 f (x; u) ->
hexists
(funa' : F x =>
((a' < u) * (factor1 f (x; a') = factor1 f a))%type)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x a: {i : X & F i} a_u: factor1 f a < factor1 f (x; u)
hexists
(funa' : F x =>
((a' < u) * (factor1 f (x; a') = factor1 f a))%type)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x a: {i : X & F i} a_u: smalltype (f a < f (x; u))
hexists
(funa' : F x =>
((a' < u) * (factor1 f (x; a') = factor1 f a))%type)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x a: {i : X & F i} a_u: f a < f (x; u)
hexists
(funa' : F x =>
((a' < u) * (factor1 f (x; a') = factor1 f a))%type)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x a: {i : X & F i} a_u: f a < f (x; u)
{a' : F x &
((a' < u) * (factor1 f (x; a') = factor1 f a))%type}
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x a: {i : X & F i} a_u: f a < f (x; u)
((out ((H0 ◁ f a) a_u) < u) *
(factor1 f (x; out ((H0 ◁ f a) a_u)) = factor1 f a))%type
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x a: {i : X & F i} a_u: f a < f (x; u)
out ((H0 ◁ f a) a_u) < u
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x a: {i : X & F i} a_u: f a < f (x; u)
factor1 f (x; out ((H0 ◁ f a) a_u)) = factor1 f a
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x a: {i : X & F i} a_u: f a < f (x; u)
out ((H0 ◁ f a) a_u) < u
apply initial_segment_property.
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x a: {i : X & F i} a_u: f a < f (x; u)
factor1 f (x; out ((H0 ◁ f a) a_u)) = factor1 f a
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x a: {i : X & F i} a_u: f a < f (x; u)
factor2 f (factor1 f (x; out ((H0 ◁ f a) a_u))) =
factor2 f (factor1 f a)
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x a: {i : X & F i} a_u: f a < f (x; u)
f (x; out ((H0 ◁ f a) a_u)) = f a
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x a: {i : X & F i} a_u: f a < f (x; u)
↓(x; out ((H0 ◁ ↓a.2) a_u)).2 = ↓a.2
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x a: {i : X & F i} a_u: f a < f (x; u)
↓((H0 ◁ ↓a.2) a_u) = ↓a.2
H: Univalence H0: PropResizing X: Type F: X -> Ordinal f:= funx : {i : X & F i} => ↓x.2: {i : X & F i} -> Ordinal x: X u: F x a: {i : X & F i} a_u: f a < f (x; u)
↓a.2 = ↓((H0 ◁ ↓a.2) a_u)
apply bound_property.Qed.(** Any type equivalent to an ordinal is an ordinal, and we can change the universe that the relation takes values in. *)(* TODO: Should factor this into two results: (1) Anything equivalent to an ordinal is an ordinal (with the relation landing in the same universe for both). (2) Under PropResizing, the universe that the relation takes values in can be changed. *)
H: PropResizing B: Ordinal C: Type g: C <~> B
Ordinal
H: PropResizing B: Ordinal C: Type g: C <~> B
Ordinal
H: PropResizing B: Ordinal C: Type g: C <~> B
IsOrdinal C lt
H: PropResizing B: Ordinal C: Type g: C <~> B
IsHSet C
H: PropResizing B: Ordinal C: Type g: C <~> B
IsSimulation g
H: PropResizing B: Ordinal C: Type g: C <~> B
IsHSet C
exact (istrunc_equiv_istrunc B (equiv_inverse g)).
H: PropResizing B: Ordinal C: Type g: C <~> B
IsSimulation g
H: PropResizing B: Ordinal C: Type g: C <~> B
forallaa' : C, a < a' -> g a < g a'
H: PropResizing B: Ordinal C: Type g: C <~> B
forall (a : C) (b : B),
b < g a ->
hexists (funa' : C => ((a' < a) * (g a' = b))%type)
H: PropResizing B: Ordinal C: Type g: C <~> B
forallaa' : C, a < a' -> g a < g a'
H: PropResizing B: Ordinal C: Type g: C <~> B a, a': C a_a': a < a'
g a < g a'
H: PropResizing B: Ordinal C: Type g: C <~> B a, a': C a_a': a < a'
smalltype (g a < g a')
exact a_a'.
H: PropResizing B: Ordinal C: Type g: C <~> B
forall (a : C) (b : B),
b < g a ->
hexists (funa' : C => ((a' < a) * (g a' = b))%type)
H: PropResizing B: Ordinal C: Type g: C <~> B a: C b: B b_fa: b < g a
hexists (funa' : C => ((a' < a) * (g a' = b))%type)
H: PropResizing B: Ordinal C: Type g: C <~> B a: C b: B b_fa: b < g a
{a' : C & ((a' < a) * (g a' = b))%type}
H: PropResizing B: Ordinal C: Type g: C <~> B a: C b: B b_fa: b < g a
((g^-1 b < a) * (g (g^-1 b) = b))%type
H: PropResizing B: Ordinal C: Type g: C <~> B a: C b: B b_fa: b < g a
g^-1 b < a
H: PropResizing B: Ordinal C: Type g: C <~> B a: C b: B b_fa: b < g a
g (g^-1 b) = b
H: PropResizing B: Ordinal C: Type g: C <~> B a: C b: B b_fa: b < g a
g^-1 b < a
H: PropResizing B: Ordinal C: Type g: C <~> B a: C b: B b_fa: b < g a
g (g^-1 b) < g a
H: PropResizing B: Ordinal C: Type g: C <~> B a: C b: B b_fa: b < g a
b < g a
exact b_fa.
H: PropResizing B: Ordinal C: Type g: C <~> B a: C b: B b_fa: b < g a
g (g^-1 b) = b
apply eisretr.Defined.
H: PropResizing B: Ordinal C: Type g: C <~> B
Isomorphism (resize_ordinal B C g) B
H: PropResizing B: Ordinal C: Type g: C <~> B
Isomorphism (resize_ordinal B C g) B
H: PropResizing B: Ordinal C: Type g: C <~> B
forallaa' : (resize_ordinal B C g).1,
(resize_ordinal B C g).2 a a' <-> B.2 (g a) (g a')
H: PropResizing B: Ordinal C: Type g: C <~> B a, a': (resize_ordinal B C g).1
(resize_ordinal B C g).2 a a' <-> B.2 (g a) (g a')
H: PropResizing B: Ordinal C: Type g: C <~> B a, a': (resize_ordinal B C g).1