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 Spaces.Card.From HoTT.Sets Require Import Ordinals Powers.Close Scope trunc_scope.(** This file contains a construction of the Hartogs number. *)(** We begin with some results about changing the universe of a power set using propositional resizing. *)
H: PropResizing ua: Univalence C: Type p, p': C -> HProp
power_inj p = power_inj p' -> p = p'
H: PropResizing ua: Univalence C: Type p, p': C -> HProp
(funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a))) ->
p = p'
H: PropResizing ua: Univalence C: Type p, p': C -> HProp q: (funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a)))
p = p'
H: PropResizing ua: Univalence C: Type p, p': C -> HProp q: (funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a)))
p == p'
H: PropResizing ua: Univalence C: Type p, p': C -> HProp q: (funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a))) a: C
p a = p' a
H: PropResizing ua: Univalence C: Type p, p': C -> HProp q: (funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a))) a: C Ha: p a
p' a
H: PropResizing ua: Univalence C: Type p, p': C -> HProp q: (funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a))) a: C Ha: p' a
p a
H: PropResizing ua: Univalence C: Type p, p': C -> HProp q: (funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a))) a: C Ha: p a
p' a
H: PropResizing ua: Univalence C: Type p, p': C -> HProp q: (funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a))) a: C Ha: p a
smalltype (p' a)
H: PropResizing ua: Univalence C: Type p, p': C -> HProp q: (funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a))) a: C Ha: p a
(funa : C => Build_HProp (smalltype (p' a))) a
H: PropResizing ua: Univalence C: Type p, p': C -> HProp q: (funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a))) a: C Ha: p a
Build_HProp (smalltype (p a))
H: PropResizing ua: Univalence C: Type p, p': C -> HProp q: (funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a))) a: C Ha: p a
p a
exact Ha.
H: PropResizing ua: Univalence C: Type p, p': C -> HProp q: (funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a))) a: C Ha: p' a
p a
H: PropResizing ua: Univalence C: Type p, p': C -> HProp q: (funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a))) a: C Ha: p' a
smalltype (p a)
H: PropResizing ua: Univalence C: Type p, p': C -> HProp q: (funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a))) a: C Ha: p' a
(funa : C => Build_HProp (smalltype (p a))) a
H: PropResizing ua: Univalence C: Type p, p': C -> HProp q: (funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a))) a: C Ha: p' a
Build_HProp (smalltype (p' a))
H: PropResizing ua: Univalence C: Type p, p': C -> HProp q: (funa : C => Build_HProp (smalltype (p a))) =
(funa : C => Build_HProp (smalltype (p' a))) a: C Ha: p' a
p' a
exact Ha.Qed.(* TODO: Could factor this as something keeping the [HProp] universe the same, followed by [power_inj]. *)
H: PropResizing ua: Univalence C, B: Type f: C -> B
(C -> HProp) -> B -> HProp
H: PropResizing ua: Univalence C, B: Type f: C -> B
(C -> HProp) -> B -> HProp
H: PropResizing ua: Univalence C, B: Type f: C -> B p: C -> HProp b: B
HProp
exact (Build_HProp (smalltype (foralla, f a = b -> p a))).Defined.
H: PropResizing ua: Univalence C, B: Type f: C -> B
IsInjective f -> IsInjective (power_morph f)
H: PropResizing ua: Univalence C, B: Type f: C -> B
IsInjective f -> IsInjective (power_morph f)
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p'
p = p'
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p'
p == p'
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C
p a = p' a
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p a
p' a
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p' a
p a
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p a
p' a
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p a Hp: power_morph f p (f a)
p' a
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p a
power_morph f p (f a)
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p a Hp: power_morph f p (f a)
p' a
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p a Hp: power_morph f p' (f a)
p' a
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p a Hp: foralla0 : C, f a0 = f a -> p' a0
p' a
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p a Hp: foralla0 : C, f a0 = f a -> p' a0
f a = f a
reflexivity.
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p a
power_morph f p (f a)
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p a
foralla0 : C, f a0 = f a -> p a0
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p a
p a
exact Ha.
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p' a
p a
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p' a Hp: power_morph f p' (f a)
p a
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p' a
power_morph f p' (f a)
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p' a Hp: power_morph f p' (f a)
p a
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p' a Hp: power_morph f p (f a)
p a
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p' a Hp: foralla0 : C, f a0 = f a -> p a0
p a
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p' a Hp: foralla0 : C, f a0 = f a -> p a0
f a = f a
reflexivity.
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p' a
power_morph f p' (f a)
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p' a
foralla0 : C, f a0 = f a -> p' a0
H: PropResizing ua: Univalence C, B: Type f: C -> B Hf: IsInjective f p, p': C -> HProp q: power_morph f p = power_morph f p' a: C Ha: p' a
p' a
exact Ha.Qed.(** We'll also need this result. *)
H: PropResizing H0: Univalence B, C: Ordinal
B < C -> card B ≤ card C
H: PropResizing H0: Univalence B, C: Ordinal
B < C -> card B ≤ card C
H: PropResizing H0: Univalence B, C: Ordinal B_C: B < C
card B ≤ card C
H: PropResizing H0: Univalence B, C: Ordinal B_C: B < C
{i : Build_HSet B -> Build_HSet C & IsInjective i}
H: PropResizing H0: Univalence B, C: Ordinal B_C: B < C
{i : ordinal_carrier B -> ordinal_carrier C &
IsInjective i}
H: PropResizing H0: Univalence B, C: Ordinal B_C: B < C
{i
: ordinal_carrier ↓((H ◁ B) B_C) -> ordinal_carrier C
& IsInjective i}
H: PropResizing H0: Univalence B, C: Ordinal B_C: B < C
IsInjective out
H: PropResizing H0: Univalence B, C: Ordinal B_C: B < C
IsSimulation out
apply is_simulation_out.Qed.(** * Hartogs number *)SectionHartogs_Number.Declare Scope Hartogs.Open Scope Hartogs.
Identifier '𝒫' now a keyword
Local Coercionsubtype_as_type' {X} (Y : 𝒫 X) := { x : X & Y x }.UniverseA.Context {univalence : Univalence}
{prop_resizing : PropResizing}
{lem: ExcludedMiddle}
(A : HSet@{A}).(* The Hartogs number of [A] consists of all ordinals that embed into [A]. Note that this construction necessarily increases the universe level. *)
The command has indeed failed with message:
In environment
univalence : Univalence
prop_resizing : PropResizing
lem : ExcludedMiddle
A : HSet
The term "{B : Ordinal & card B ≤ card A}" has type
"Type@{max(Hartogs.1355,Hartogs.1356)}"
while it is expected to have type "Type@{A}"
(universe inconsistency: Cannot enforce Hartogs.1355
<= A because A < Hartogs.1355).
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet carrier:= {B : Ordinal &
Trunc (-1)
{i : ordinal_carrier B -> A &
IsInjective i}}: Type relation:= funBC : carrier => B.1 < C.1: carrier -> carrier -> Type B: Ordinal small_B: Trunc (-1)
{i : ordinal_carrier B -> A &
IsInjective i} C: Ordinal C_B: C < B
Trunc (-1)
{i : ordinal_carrier C -> A & IsInjective i}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet carrier:= {B : Ordinal &
Trunc (-1)
{i : ordinal_carrier B -> A &
IsInjective i}}: Type relation:= funBC : carrier => B.1 < C.1: carrier -> carrier -> Type B, C: Ordinal C_B: C < B
Trunc (-1)
{i : ordinal_carrier B -> A & IsInjective i} ->
Trunc (-1)
{i : ordinal_carrier C -> A & IsInjective i}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet carrier:= {B : Ordinal &
Trunc (-1)
{i : ordinal_carrier B -> A &
IsInjective i}}: Type relation:= funBC : carrier => B.1 < C.1: carrier -> carrier -> Type B, C: Ordinal C_B: C < B
{i : ordinal_carrier B -> A & IsInjective i} ->
Trunc (-1)
{i : ordinal_carrier C -> A & IsInjective i}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet carrier:= {B : Ordinal &
Trunc (-1)
{i : ordinal_carrier B -> A &
IsInjective i}}: Type relation:= funBC : carrier => B.1 < C.1: carrier -> carrier -> Type B, C: Ordinal C_B: C < B f: ordinal_carrier B -> A isinjective_f: IsInjective f
Trunc (-1)
{i : ordinal_carrier C -> A & IsInjective i}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet carrier:= {B : Ordinal &
Trunc (-1)
{i : ordinal_carrier B -> A &
IsInjective i}}: Type relation:= funBC : carrier => B.1 < C.1: carrier -> carrier -> Type B, C: Ordinal C_B: C < B f: ordinal_carrier B -> A isinjective_f: IsInjective f
{i : ordinal_carrier C -> A & IsInjective i}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet carrier:= {B : Ordinal &
Trunc (-1)
{i : ordinal_carrier B -> A &
IsInjective i}}: Type relation:= funBC : carrier => B.1 < C.1: carrier -> carrier -> Type B: Ordinal b: B f: ordinal_carrier B -> A isinjective_f: IsInjective f
{i : ordinal_carrier ↓b -> A & IsInjective i}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet carrier:= {B : Ordinal &
Trunc (-1)
{i : ordinal_carrier B -> A &
IsInjective i}}: Type relation:= funBC : carrier => B.1 < C.1: carrier -> carrier -> Type B: Ordinal b: B f: ordinal_carrier B -> A isinjective_f: IsInjective f
IsInjective
(funpat : {b0 : ordinal_carrier B &
smalltype (b0 < b)} => f pat.1)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet carrier:= {B : Ordinal &
Trunc (-1)
{i : ordinal_carrier B -> A &
IsInjective i}}: Type relation:= funBC : carrier => B.1 < C.1: carrier -> carrier -> Type B: Ordinal b: B f: ordinal_carrier B -> A isinjective_f: IsInjective f x: ordinal_carrier B x_b: smalltype (x < b) y: ordinal_carrier B y_b: smalltype (y < b) fx_fy: f x = f y
(x; x_b) = (y; y_b)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet carrier:= {B : Ordinal &
Trunc (-1)
{i : ordinal_carrier B -> A &
IsInjective i}}: Type relation:= funBC : carrier => B.1 < C.1: carrier -> carrier -> Type B: Ordinal b: B f: ordinal_carrier B -> A isinjective_f: IsInjective f x: ordinal_carrier B x_b: smalltype (x < b) y: ordinal_carrier B y_b: smalltype (y < b) fx_fy: f x = f y
x = y
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet carrier:= {B : Ordinal &
Trunc (-1)
{i : ordinal_carrier B -> A &
IsInjective i}}: Type relation:= funBC : carrier => B.1 < C.1: carrier -> carrier -> Type B: Ordinal b: B f: ordinal_carrier B -> A isinjective_f: IsInjective f x: ordinal_carrier B x_b: smalltype (x < b) y: ordinal_carrier B y_b: smalltype (y < b) fx_fy: f x = f y
f x = f y
exact fx_fy.Defined.Definitionproper_subtype_inclusion (UV : 𝒫 A)
:= (foralla, U a -> V a) /\ merely (existsa : A, V a /\ ~(U a)).Infix"⊊" := proper_subtype_inclusion (at level50) : Hartogs.Notation"(⊊)" := proper_subtype_inclusion : Hartogs.(* The Hartogs number of [A] embeds into the threefold power set of [A]. This preliminary injection also increases the universe level though. *)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B: Ordinal B_A: card B ≤ card A C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C))
(B; B_A) = (C; C_A)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B: Ordinal B_A: card B ≤ card A C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C))
B = C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C))
card B ≤ card A -> B = C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C))
{i : Build_HSet B -> Build_HSet A & IsInjective i} ->
B = C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f
B = C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f
Isomorphism B C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f
{X : (𝒫) ((𝒫) A) & Isomorphism (X; ϕ X) B}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) ((𝒫) A) iso: Isomorphism (X; ϕ X) B
Isomorphism B C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f
{X : (𝒫) ((𝒫) A) & Isomorphism (X; ϕ X) B}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f
forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
{X : (𝒫) ((𝒫) A) & Isomorphism (X; ϕ X) B}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f
forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type}
(b1; Hb1) = (b2; Hb2)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type}
forallx : ordinal_carrier B,
IsHProp
(foralla : A,
X a <->
{b' : ordinal_carrier B &
((b' < x) * (a = f b'))%type})
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type}
b1 = b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type}
forallx : ordinal_carrier B,
IsHProp
(foralla : A,
X a <->
{b' : ordinal_carrier B &
((b' < x) * (a = f b'))%type})
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b: ordinal_carrier B
IsHProp
(foralla : A,
X a <->
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type})
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b: ordinal_carrier B
foralla : A,
IsHProp
((funa0 : A =>
X a0 <->
{b' : ordinal_carrier B &
((b' < b) * (a0 = f b'))%type}) a)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b: ordinal_carrier B a: A
IsHProp
((funa : A =>
X a <->
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type}) a)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b: ordinal_carrier B a: A
IsHProp
(X a ->
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type})
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b: ordinal_carrier B a: A
IsHProp
({b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type} ->
X a)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b: ordinal_carrier B a: A
IsHProp
(X a ->
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type})
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b: ordinal_carrier B a: A
IsHProp
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b: ordinal_carrier B a: A
forallxy : ordinal_carrier B,
(x < b) * (a = f x) -> (y < b) * (a = f y) -> x = y
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b, b1', b2': ordinal_carrier B p: f b1' = f b2'
b1' = b2'
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b, b1', b2': ordinal_carrier B p: f b1' = f b2'
f b1' = f b2'
exact p.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type}
b1 = b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type}
forallc : ordinal_carrier B, c < b1 <-> c < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b': ordinal_carrier B
b' < b1 <-> b' < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b': ordinal_carrier B
b' < b1 -> b' < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b': ordinal_carrier B
b' < b2 -> b' < b1
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b': ordinal_carrier B
b' < b1 -> b' < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b': ordinal_carrier B b'_b1: b' < b1
b' < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B b': ordinal_carrier B Hb1: X (f b') <->
{b'0 : B & ((b'0 < b1) * (f b' = f b'0))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b'_b1: b' < b1
b' < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B b': ordinal_carrier B Hb1: {b'0 : B & ((b'0 < b1) * (f b' = f b'0))%type} ->
X (f b') b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b'_b1: b' < b1
b' < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B b': ordinal_carrier B Hb1: X (f b') b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b'_b1: b' < b1
b' < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B b': ordinal_carrier B b2: B Hb1: {b'0 : B & ((b'0 < b2) * (f b' = f b'0))%type} Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b'_b1: b' < b1
b' < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B b': ordinal_carrier B b2, proj1: B H2: proj1 < b2 H3: f b' = f proj1 Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b'_b1: b' < b1
b' < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B b': ordinal_carrier B b2, proj1: B H2: proj1 < b2 H3: b' = proj1 Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b'_b1: b' < b1
b' < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B b': ordinal_carrier B b2, proj1: B H2: proj1 < b2 H3: f b' = f proj1 Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b'_b1: b' < b1
IsInjective f
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B b': ordinal_carrier B b2, proj1: B H2: proj1 < b2 H3: b' = proj1 Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b'_b1: b' < b1
b' < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B b': ordinal_carrier B b2: B H2: b' < b2 Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b'_b1: b' < b1
b' < b2
exact H2.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b': ordinal_carrier B
b' < b2 -> b' < b1
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B Hb2: foralla : A,
X a <-> {b' : B & ((b' < b2) * (a = f b'))%type} b': ordinal_carrier B b'_b2: b' < b2
b' < b1
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B b': ordinal_carrier B Hb2: X (f b') <->
{b'0 : B & ((b'0 < b2) * (f b' = f b'0))%type} b'_b2: b' < b2
b' < b1
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B b': ordinal_carrier B Hb2: {b'0 : B & ((b'0 < b2) * (f b' = f b'0))%type} ->
X (f b') b'_b2: b' < b2
b' < b1
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B b': ordinal_carrier B Hb2: X (f b') b'_b2: b' < b2
b' < b1
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B b': ordinal_carrier B Hb2: {b'0 : B & ((b'0 < b1) * (f b' = f b'0))%type} b'_b2: b' < b2
b' < b1
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B b': ordinal_carrier B proj1: B H2: proj1 < b1 H3: f b' = f proj1 b'_b2: b' < b2
b' < b1
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B b': ordinal_carrier B proj1: B H2: proj1 < b1 H3: b' = proj1 b'_b2: b' < b2
b' < b1
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B b': ordinal_carrier B proj1: B H2: proj1 < b1 H3: f b' = f proj1 b'_b2: b' < b2
IsInjective f
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B b': ordinal_carrier B proj1: B H2: proj1 < b1 H3: b' = proj1 b'_b2: b' < b2
b' < b1
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) A b1: B Hb1: foralla : A,
X a <-> {b' : B & ((b' < b1) * (a = f b'))%type} b2: B b': ordinal_carrier B H2: b' < b1 b'_b2: b' < b2
b' < b1
exact H2.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
{X : (𝒫) ((𝒫) A) & Isomorphism (X; ϕ X) B}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
Isomorphism
(funX : (𝒫) A =>
Build_HProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}};
ϕ
(funX : (𝒫) A =>
Build_HProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}))
B
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
Isomorphism
(funX : (𝒫) A =>
Build_HProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}};
ϕ
(funX : (𝒫) A =>
Build_HProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}))
B
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
Isomorphism
({x : (𝒫) A &
Build_HProp
{b : B &
foralla : A,
x a <-> {b' : B & ((b' < b) * (a = f b'))%type}}};
ϕ
(funX : (𝒫) A =>
Build_HProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}))
B
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
{x : (𝒫) A &
Build_HProp
{b : B &
foralla : A,
x a <-> {b' : B & ((b' < b) * (a = f b'))%type}}} <~>
B.1
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
forall
(a : {x : (𝒫) A &
Build_HProp
{b : B &
foralla : A,
x a <-> {b' : B & ((b' < b) * (a = f b'))%type}}})
(a' : {x : (𝒫) A &
Build_HProp
{b : B &
foralla0 : A,
x a0 <->
{b' : B & ((b' < b) * (a0 = f b'))%type}}}),
ϕ
(funX : (𝒫) A =>
Build_HProp
{b : B &
foralla0 : A,
X a0 <-> {b' : B & ((b' < b) * (a0 = f b'))%type}})
a a' <-> B.2 (?f a) (?f a')
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
{x : (𝒫) A &
Build_HProp
{b : B &
foralla : A,
x a <-> {b' : B & ((b' < b) * (a = f b'))%type}}} <~>
B.1
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
{x : (𝒫) A &
Build_HProp
{b : B &
foralla : A,
x a <-> {b' : B & ((b' < b) * (a = f b'))%type}}} ->
B
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
B ->
{x : (𝒫) A &
Build_HProp
{b : B &
foralla : A,
x a <-> {b' : B & ((b' < b) * (a = f b'))%type}}}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
?f o ?g == idmap
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
?g o ?f == idmap
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
{x : (𝒫) A &
Build_HProp
{b : B &
foralla : A,
x a <-> {b' : B & ((b' < b) * (a = f b'))%type}}} ->
B
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X: (𝒫) A b: B
B
exact b.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
B ->
{x : (𝒫) A &
Build_HProp
{b : B &
foralla : A,
x a <-> {b' : B & ((b' < b) * (a = f b'))%type}}}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B
{x : (𝒫) A &
Build_HProp
{b : B &
foralla : A,
x a <-> {b' : B & ((b' < b) * (a = f b'))%type}}}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B a: Build_HSet A b': B
Lt B
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B a: Build_HSet A
IsHProp {b' : B & ((b' < b) * (a = f b'))%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B
Build_HProp
{b0 : B &
foralla : A,
Build_HProp {b' : B & ((b' < b) * (a = f b'))%type} <->
{b' : B & ((b' < b0) * (a = f b'))%type}}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B a: Build_HSet A
IsHProp {b' : B & ((b' < b) * (a = f b'))%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B
Build_HProp
{b0 : B &
foralla : A,
Build_HProp {b' : B & ((b' < b) * (a = f b'))%type} <->
{b' : B & ((b' < b0) * (a = f b'))%type}}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B a: Build_HSet A
IsHProp {b' : B & ((b' < b) * (a = f b'))%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B a: Build_HSet A
forallxy : {b' : B & ((b' < b) * (a = f b'))%type},
x = y
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B a: Build_HSet A b1: B b1_b: b1 < b p: a = f b1 b2: B b2_b: b2 < b q: a = f b2
(b1; (b1_b, p)) = (b2; (b2_b, q))
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B a: Build_HSet A b1: B b1_b: b1 < b p: a = f b1 b2: B b2_b: b2 < b q: a = f b2
b1 = b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B a: Build_HSet A b1: B b1_b: b1 < b p: a = f b1 b2: B b2_b: b2 < b q: a = f b2
f b1 = f b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B a: Build_HSet A b1: B b1_b: b1 < b b2: B b2_b: b2 < b
a = a
reflexivity.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B
Build_HProp
{b0 : B &
foralla : A,
Build_HProp {b' : B & ((b' < b) * (a = f b'))%type} <->
{b' : B & ((b' < b0) * (a = f b'))%type}}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B
foralla : A,
Build_HProp {b' : B & ((b' < b) * (a = f b'))%type} <->
{b' : B & ((b' < b) * (a = f b'))%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B b': A
Build_HProp
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type} <->
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} b: B b': A
{b'0 : ordinal_carrier B &
((b'0 < b) * (b' = f b'0))%type} <->
{b'0 : ordinal_carrier B &
((b'0 < b) * (b' = f b'0))%type}
reflexivity.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
(funX0 : {x : (𝒫) A &
Build_HProp
{b : B &
foralla : A,
x a <->
{b' : B & ((b' < b) * (a = f b'))%type}}} =>
(fun (X : (𝒫) A)
(proj2 : Build_HProp
{b : B &
foralla : A,
X a <->
{b' : B & ((b' < b) * (a = f b'))%type}})
=>
(fun (b : B)
(_ : foralla : A,
X a <->
{b' : B & ((b' < b) * (a = f b'))%type}) =>
b) proj2.1 proj2.2) X0.1 X0.2)
o (funb : B =>
(funa : Build_HSet A =>
Build_HProp
{b' : B & ((b' < b) * (a = f b'))%type}; b;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
((b'0 < b) * (b' = f b'0))%type}
:
Build_HProp
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type} <->
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type})) ==
idmap
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
idmap == idmap
reflexivity.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
(funb : B =>
(funa : Build_HSet A =>
Build_HProp {b' : B & ((b' < b) * (a = f b'))%type};
b;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
((b'0 < b) * (b' = f b'0))%type}
:
Build_HProp
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type} <->
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type}))
o (funX0 : {x : (𝒫) A &
Build_HProp
{b : B &
foralla : A,
x a <->
{b' : B & ((b' < b) * (a = f b'))%type}}}
=>
(fun (X : (𝒫) A)
(proj2 : Build_HProp
{b : B &
foralla : A,
X a <->
{b' : B &
((b' < b) * (a = f b'))%type}}) =>
(fun (b : B)
(_ : foralla : A,
X a <->
{b' : B & ((b' < b) * (a = f b'))%type})
=> b) proj2.1 proj2.2) X0.1 X0.2) == idmap
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
(funx : {x : (𝒫) A &
{b : ordinal_carrier B &
foralla : A,
x a <->
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type}}} =>
(funa : A =>
Build_HProp
{b' : ordinal_carrier B &
((b' < (x.2).1) * (a = f b'))%type}; (x.2).1;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
((b'0 < (x.2).1) * (b' = f b'0))%type})) == idmap
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X: (𝒫) A b: ordinal_carrier B Hb: foralla : A,
X a <->
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type}
(funa : A =>
Build_HProp
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type}; b;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
((b'0 < b) * (b' = f b'0))%type}) = (X; b; Hb)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X: (𝒫) A b: ordinal_carrier B Hb: foralla : A,
X a <->
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type}
(funa : A =>
Build_HProp
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type}; b;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
((b'0 < b) * (b' = f b'0))%type}).1 = (X; b; Hb).1
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X: (𝒫) A b: ordinal_carrier B Hb: foralla : A,
X a <->
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type}
(funa : A =>
Build_HProp
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type}) = X
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X: (𝒫) A b: ordinal_carrier B Hb: foralla : A,
X a <->
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type} a: A
Build_HProp
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type} = X a
apply path_iff_hprop; apply Hb.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
forall
(a : {x : (𝒫) A &
Build_HProp
{b : B &
foralla : A,
x a <-> {b' : B & ((b' < b) * (a = f b'))%type}}})
(a' : {x : (𝒫) A &
Build_HProp
{b : B &
foralla0 : A,
x a0 <->
{b' : B & ((b' < b) * (a0 = f b'))%type}}}),
ϕ
(funX : (𝒫) A =>
Build_HProp
{b : B &
foralla0 : A,
X a0 <-> {b' : B & ((b' < b) * (a0 = f b'))%type}})
a a' <->
B.2
(equiv_adjointify
(funX0 : {x : (𝒫) A &
Build_HProp
{b : B &
foralla0 : A,
x a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}}} =>
(fun (X : (𝒫) A)
(proj2 : Build_HProp
{b : B &
foralla0 : A,
X a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}})
=>
(fun (b : B)
(_ : foralla0 : A,
X a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}) => b)
proj2.1 proj2.2) X0.1 X0.2)
(funb : B =>
(funa0 : Build_HSet A =>
Build_HProp
{b' : B & ((b' < b) * (a0 = f b'))%type}; b;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
((b'0 < b) * (b' = f b'0))%type}
:
Build_HProp
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type} <->
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type}))
((funx0 : ordinal_carrier B => 1%path)
:
(funX0 : {x : (𝒫) A &
Build_HProp
{b : B &
foralla0 : A,
x a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}}} =>
(fun (X : (𝒫) A)
(proj2 : Build_HProp
{b : B &
foralla0 : A,
X a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}})
=>
(fun (b : B)
(_ : foralla0 : A,
X a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}) => b)
proj2.1 proj2.2) X0.1 X0.2)
o (funb : B =>
(funa0 : Build_HSet A =>
Build_HProp
{b' : B & ((b' < b) * (a0 = f b'))%type};
b;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
((b'0 < b) * (b' = f b'0))%type}
:
Build_HProp
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type} <->
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type})) ==
idmap)
(((funx : {x : (𝒫) A &
{b : ordinal_carrier B &
foralla0 : A,
x a0 <->
{b' : ordinal_carrier B &
((b' < b) * (a0 = f b'))%type}}} =>
(fun (X : (𝒫) A)
(proj2 : {b : ordinal_carrier B &
foralla0 : A,
X a0 <->
{b' : ordinal_carrier B &
((b' < b) * (a0 = f b'))%type}})
=>
(fun (b : ordinal_carrier B)
(Hb : foralla0 : A,
X a0 <->
{b' : ordinal_carrier B &
((b' < b) * (a0 = f b'))%type}) =>
path_sigma_hprop
(funa0 : A =>
Build_HProp
{b' : ordinal_carrier B &
((b' < b) * (a0 = f b'))%type}; b;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
((b'0 < b) * (b' = f b'0))%type})
(X; b; Hb)
(path_forall
(funa0 : A =>
Build_HProp
{b' : ordinal_carrier B &
(... * ...)%type}) X
((funa0 : A =>
path_iff_hprop (...) (...))
:
(fun ... => Build_HProp ...) == X)
:
(funa0 : A =>
Build_HProp
{b' : ordinal_carrier B &
(... * ...)%type}; b;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
(... * ...)%type}).1 = (X; b; Hb).1))
proj2.1 proj2.2) x.1 x.2)
:
(funx : {x : (𝒫) A &
{b : ordinal_carrier B &
foralla0 : A,
x a0 <->
{b' : ordinal_carrier B &
((b' < b) * (a0 = f b'))%type}}} =>
(funa0 : A =>
Build_HProp
{b' : ordinal_carrier B &
((b' < (x.2).1) * (a0 = f b'))%type};
(x.2).1;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
((b'0 < (x.2).1) * (b' = f b'0))%type})) ==
idmap)
:
(funb : B =>
(funa0 : Build_HSet A =>
Build_HProp
{b' : B & ((b' < b) * (a0 = f b'))%type}; b;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
((b'0 < b) * (b' = f b'0))%type}
:
Build_HProp
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type} <->
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type}))
o (funX0 : {x : (𝒫) A &
Build_HProp
{b : B &
foralla0 : A,
x a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}}} =>
(fun (X : (𝒫) A)
(proj2 : Build_HProp
{b : B &
foralla0 : A,
X a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}})
=>
(fun (b : B)
(_ : foralla0 : A,
X a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}) => b)
proj2.1 proj2.2) X0.1 X0.2) == idmap) a)
(equiv_adjointify
(funX0 : {x : (𝒫) A &
Build_HProp
{b : B &
foralla0 : A,
x a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}}} =>
(fun (X : (𝒫) A)
(proj2 : Build_HProp
{b : B &
foralla0 : A,
X a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}})
=>
(fun (b : B)
(_ : foralla0 : A,
X a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}) => b)
proj2.1 proj2.2) X0.1 X0.2)
(funb : B =>
(funa0 : Build_HSet A =>
Build_HProp
{b' : B & ((b' < b) * (a0 = f b'))%type}; b;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
((b'0 < b) * (b' = f b'0))%type}
:
Build_HProp
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type} <->
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type}))
((funx0 : ordinal_carrier B => 1%path)
:
(funX0 : {x : (𝒫) A &
Build_HProp
{b : B &
foralla0 : A,
x a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}}} =>
(fun (X : (𝒫) A)
(proj2 : Build_HProp
{b : B &
foralla0 : A,
X a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}})
=>
(fun (b : B)
(_ : foralla0 : A,
X a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}) => b)
proj2.1 proj2.2) X0.1 X0.2)
o (funb : B =>
(funa0 : Build_HSet A =>
Build_HProp
{b' : B & ((b' < b) * (a0 = f b'))%type};
b;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
((b'0 < b) * (b' = f b'0))%type}
:
Build_HProp
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type} <->
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type})) ==
idmap)
(((funx : {x : (𝒫) A &
{b : ordinal_carrier B &
foralla0 : A,
x a0 <->
{b' : ordinal_carrier B &
((b' < b) * (a0 = f b'))%type}}} =>
(fun (X : (𝒫) A)
(proj2 : {b : ordinal_carrier B &
foralla0 : A,
X a0 <->
{b' : ordinal_carrier B &
((b' < b) * (a0 = f b'))%type}})
=>
(fun (b : ordinal_carrier B)
(Hb : foralla0 : A,
X a0 <->
{b' : ordinal_carrier B &
((b' < b) * (a0 = f b'))%type}) =>
path_sigma_hprop
(funa0 : A =>
Build_HProp
{b' : ordinal_carrier B &
((b' < b) * (a0 = f b'))%type}; b;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
((b'0 < b) * (b' = f b'0))%type})
(X; b; Hb)
(path_forall
(funa0 : A =>
Build_HProp
{b' : ordinal_carrier B &
(... * ...)%type}) X
((funa0 : A =>
path_iff_hprop (...) (...))
:
(fun ... => Build_HProp ...) == X)
:
(funa0 : A =>
Build_HProp
{b' : ordinal_carrier B &
(... * ...)%type}; b;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
(... * ...)%type}).1 = (X; b; Hb).1))
proj2.1 proj2.2) x.1 x.2)
:
(funx : {x : (𝒫) A &
{b : ordinal_carrier B &
foralla0 : A,
x a0 <->
{b' : ordinal_carrier B &
((b' < b) * (a0 = f b'))%type}}} =>
(funa0 : A =>
Build_HProp
{b' : ordinal_carrier B &
((b' < (x.2).1) * (a0 = f b'))%type};
(x.2).1;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
((b'0 < (x.2).1) * (b' = f b'0))%type})) ==
idmap)
:
(funb : B =>
(funa0 : Build_HSet A =>
Build_HProp
{b' : B & ((b' < b) * (a0 = f b'))%type}; b;
funb' : A =>
iff_reflexive
{b'0 : ordinal_carrier B &
((b'0 < b) * (b' = f b'0))%type}
:
Build_HProp
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type} <->
{b'0 : B & ((b'0 < b) * (b' = f b'0))%type}))
o (funX0 : {x : (𝒫) A &
Build_HProp
{b : B &
foralla0 : A,
x a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}}} =>
(fun (X : (𝒫) A)
(proj2 : Build_HProp
{b : B &
foralla0 : A,
X a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}})
=>
(fun (b : B)
(_ : foralla0 : A,
X a0 <->
{b' : B &
((b' < b) * (a0 = f b'))%type}) => b)
proj2.1 proj2.2) X0.1 X0.2) == idmap) a')
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}}
forall
(a : {x : (𝒫) A &
{b : ordinal_carrier B &
foralla : A,
x a <->
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type}}})
(a' : {x : (𝒫) A &
{b : ordinal_carrier B &
foralla0 : A,
x a0 <->
{b' : ordinal_carrier B &
((b' < b) * (a0 = f b'))%type}}}),
ϕ
(funX : (𝒫) A =>
Build_HProp
{b : ordinal_carrier B &
foralla0 : A,
X a0 <->
{b' : ordinal_carrier B &
((b' < b) * (a0 = f b'))%type}}) a a' <->
(a.2).1 < (a'.2).1
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type}
ϕ
(funX : (𝒫) A =>
Build_HProp
{b : ordinal_carrier B &
foralla : A,
X a <->
{b' : ordinal_carrier B &
((b' < b) * (a = f b'))%type}}) (X1; b1; H'1)
(X2; b2; H'2) <-> b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type}
(foralla : A, (X1; b1; H'1).1 a -> (X2; b2; H'2).1 a) *
merely
{a : A &
((X2; b2; H'2).1 a * ~ (X1; b1; H'1).1 a)%type} <->
b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type}
(foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & (X2 a * ~ X1 a)%type} <-> b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type}
(foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & (X2 a * ~ X1 a)%type} -> b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type}
b1 < b2 ->
(foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & (X2 a * ~ X1 a)%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type}
(foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & (X2 a * ~ X1 a)%type} -> b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: ((foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & X2 a * ~ X1 a})%type
b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: ((foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & X2 a * ~ X1 a})%type
(b1 < b2) + hor (b1 = b2) (b2 < b1) -> b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: ((foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & X2 a * ~ X1 a})%type b1_b2: b1 < b2
b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: ((foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & X2 a * ~ X1 a})%type H4: hor (b1 = b2) (b2 < b1)
b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: ((foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & X2 a * ~ X1 a})%type b1_b2: b1 < b2
b1 < b2
exact b1_b2.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: ((foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & X2 a * ~ X1 a})%type H4: hor (b1 = b2) (b2 < b1)
b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: ((foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & X2 a * ~ X1 a})%type
hor (b1 = b2) (b2 < b1) -> b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: ((foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & X2 a * ~ X1 a})%type
(b1 = b2) + (b2 < b1) -> b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: ((foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & X2 a * ~ X1 a})%type b1_b2: b1 = b2
b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: ((foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & X2 a * ~ X1 a})%type b2_b1: b2 < b1
b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: ((foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & X2 a * ~ X1 a})%type b1_b2: b1 = b2
b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: ((foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & X2 a * ~ X1 a})%type b1_b2: b1 = b2
Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: Trunc (-1) {a : A & (X2 a * ~ X1 a)%type} b1_b2: b1 = b2
Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 = b2
Trunc (-1) {a : A & (X2 a * ~ X1 a)%type} -> Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 = b2
{a : A & (X2 a * ~ X1 a)%type} -> Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 = b2 a: A X2a: X2 a not_X1a: ~ X1 a
Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 = b2 a: A X2a: X2 a not_X1a: ~ X1 a
X1 a
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 = b2 a: A X2a: X2 a not_X1a: ~ X1 a
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 = b2 a: A X2a: X2 a not_X1a: ~ X1 a
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 = b2 a: A X2a: X2 a not_X1a: ~ X1 a
X2 a
exact X2a.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: ((foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & X2 a * ~ X1 a})%type b2_b1: b2 < b1
b1 < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: ((foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & X2 a * ~ X1 a})%type b2_b1: b2 < b1
Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} H3: Trunc (-1) {a : A & (X2 a * ~ X1 a)%type} b2_b1: b2 < b1
Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b2_b1: b2 < b1
Trunc (-1) {a : A & (X2 a * ~ X1 a)%type} -> Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b2_b1: b2 < b1
{a : A & (X2 a * ~ X1 a)%type} -> Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b2_b1: b2 < b1 a: A X2a: X2 a not_X1a: ~ X1 a
Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b2_b1: b2 < b1 a: A X2a: X2 a not_X1a: ~ X1 a
X1 a
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b2_b1: b2 < b1 a: A X2a: X2 a not_X1a: ~ X1 a
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b2_b1: b2 < b1 a: A X2a: {b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} not_X1a: ~ X1 a
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b2_b1: b2 < b1 a: A b': ordinal_carrier B b'_b2: b' < b2 a_fb': a = f b' not_X1a: ~ X1 a
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b2_b1: b2 < b1 a: A b': ordinal_carrier B b'_b2: b' < b2 a_fb': a = f b' not_X1a: ~ X1 a
((b' < b1) * (a = f b'))%type
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b2_b1: b2 < b1 a: A b': ordinal_carrier B b'_b2: b' < b2 a_fb': a = f b' not_X1a: ~ X1 a
b' < b1
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b2_b1: b2 < b1 a: A b': ordinal_carrier B b'_b2: b' < b2 a_fb': a = f b' not_X1a: ~ X1 a
a = f b'
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b2_b1: b2 < b1 a: A b': ordinal_carrier B b'_b2: b' < b2 a_fb': a = f b' not_X1a: ~ X1 a
b' < b1
transitivity b2; assumption.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b2_b1: b2 < b1 a: A b': ordinal_carrier B b'_b2: b' < b2 a_fb': a = f b' not_X1a: ~ X1 a
a = f b'
assumption.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type}
b1 < b2 ->
(foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & (X2 a * ~ X1 a)%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2
((foralla : A, X1 a -> X2 a) *
Trunc (-1) {a : A & X2 a * ~ X1 a})%type
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2
foralla : A, X1 a -> X2 a
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2
Trunc (-1) {a : A & (X2 a * ~ X1 a)%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2
foralla : A, X1 a -> X2 a
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 a: A X1a: X1 a
X2 a
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 a: A X1a: X1 a
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 a: A X1a: {b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type}
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 a: A b': ordinal_carrier B b'_b1: b' < b1 a_fb': a = f b'
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 a: A b': ordinal_carrier B b'_b1: b' < b1 a_fb': a = f b'
((b' < b2) * (a = f b'))%type
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 a: A b': ordinal_carrier B b'_b1: b' < b1 a_fb': a = f b'
b' < b2
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 a: A b': ordinal_carrier B b'_b1: b' < b1 a_fb': a = f b'
a = f b'
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 a: A b': ordinal_carrier B b'_b1: b' < b1 a_fb': a = f b'
b' < b2
transitivity b1; assumption.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 a: A b': ordinal_carrier B b'_b1: b' < b1 a_fb': a = f b'
a = f b'
assumption.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2
Trunc (-1) {a : A & (X2 a * ~ X1 a)%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2
{a : A & (X2 a * ~ X1 a)%type}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2
(X2 (f b1) * ~ X1 (f b1))%type
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2
X2 (f b1)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2
~ X1 (f b1)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2
X2 (f b1)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2
{b' : ordinal_carrier B &
((b' < b2) * (f b1 = f b'))%type}
existsb1; auto.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2
~ X1 (f b1)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 X1_fb1: X1 (f b1)
Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 X1_fb1: {b' : ordinal_carrier B &
((b' < b1) * (f b1 = f b'))%type}
Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 b': ordinal_carrier B b'_b1: b' < b1 fb1_fb': f b1 = f b'
Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 b': ordinal_carrier B b'_b1: b' < b1 fb1_fb': b1 = b'
Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 b'_b1: b1 < b1
Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 b'_b1: Empty
Empty
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 b'_b1: b1 < b1
Irreflexive lt
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f H2: forallX : (𝒫) A,
IsHProp
{b : B &
foralla : A,
X a <-> {b' : B & ((b' < b) * (a = f b'))%type}} X1: (𝒫) A b1: ordinal_carrier B H'1: foralla : A,
X1 a <->
{b' : ordinal_carrier B &
((b' < b1) * (a = f b'))%type} X2: (𝒫) A b2: ordinal_carrier B H'2: foralla : A,
X2 a <->
{b' : ordinal_carrier B &
((b' < b2) * (a = f b'))%type} b1_b2: b1 < b2 b'_b1: Empty
Empty
assumption.}
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) ((𝒫) A) iso: Isomorphism (X; ϕ X) B
Isomorphism B C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) ((𝒫) A) iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
Isomorphism B C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) ==
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f X: (𝒫) ((𝒫) A) iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
Isomorphism B C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: (funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) B)) X =
(funX : (𝒫) ((𝒫) A) =>
merely (Isomorphism (X; ϕ X) C)) X f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
Isomorphism B C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
Isomorphism B C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
Isomorphism B (X; ϕ X)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
Isomorphism (X; ϕ X) C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
Isomorphism B (X; ϕ X)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
Isomorphism (X; ϕ X) B
assumption.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
Isomorphism (X; ϕ X) C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X) X1: merely (Isomorphism (X : Type; ϕ X) C)
Isomorphism (X; ϕ X) C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
merely (Isomorphism (X; ϕ X) C)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X) X1: merely (Isomorphism (X : Type; ϕ X) C)
Isomorphism (X; ϕ X) C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
merely (Isomorphism (X : Type; ϕ X) C) ->
Isomorphism (X; ϕ X) C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
IsHProp (Isomorphism (X; ϕ X) C)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
Isomorphism (X; ϕ X) C -> Isomorphism (X; ϕ X) C
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
IsHProp (Isomorphism (X; ϕ X) C)
exact (ishprop_Isomorphism (Build_Ordinal X (ϕ X) _) C).
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
Isomorphism (X; ϕ X) C -> Isomorphism (X; ϕ X) C
auto.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
merely (Isomorphism (X; ϕ X) C)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
merely (Isomorphism (X; ϕ X) B)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet ϕ:= funX : (𝒫) ((𝒫) A) =>
(funx1x2 : X => (⊊) x1.1 x2.1) : Lt X: forallX : (𝒫) ((𝒫) A), Lt X B, C: Ordinal C_A: card C ≤ card A X: (𝒫) ((𝒫) A) H0: merely (Isomorphism (X; ϕ X) B) =
merely (Isomorphism (X; ϕ X) C) f: Build_HSet B -> Build_HSet A injective_f: IsInjective f iso: Isomorphism (X; ϕ X) B X0: IsOrdinal X (ϕ X)
Isomorphism (X; ϕ X) B
exact iso.Qed.(** Using hprop resizing, the threefold power set can be pushed to the same universe level as [A]. *)
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet X, Y: (𝒫) ((𝒫) ((𝒫) A)) H: power_morph (power_morph power_inj) X =
power_morph (power_morph power_inj) Y P, Q: (𝒫) ((𝒫) A)
power_morph power_inj P = power_morph power_inj Q ->
P = Q
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet X, Y: (𝒫) ((𝒫) ((𝒫) A)) H: power_morph (power_morph power_inj) X =
power_morph (power_morph power_inj) Y P, Q: (𝒫) ((𝒫) A) H': power_morph power_inj P = power_morph power_inj Q
IsInjective power_inj
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet X, Y: (𝒫) ((𝒫) ((𝒫) A)) H: power_morph (power_morph power_inj) X =
power_morph (power_morph power_inj) Y P, Q: (𝒫) ((𝒫) A) H': power_morph power_inj P = power_morph power_inj Q p, q: (𝒫) A
power_inj p = power_inj q -> p = q
apply injective_power_inj.Qed.(* We can therefore resize the Hartogs number of A to the same universe level as A. *)Definitionhartogs_number_carrier : Type@{A}
:= {X : 𝒫 (𝒫 (𝒫 A)) | smalltype (merely (existsa, uni_fix (hartogs_number'_injection.1 a) = X))}.
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet a, b: hartogs_number' H: uni_fix (hartogs_number'_injection.1 a) =
uni_fix (hartogs_number'_injection.1 b)
a = b
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet a, b: hartogs_number' H: uni_fix (hartogs_number'_injection.1 a) =
uni_fix (hartogs_number'_injection.1 b)
(uni_fix (hartogs_number'_injection.1 a) =
uni_fix (hartogs_number'_injection.1 b) ->
hartogs_number'_injection.1 a =
hartogs_number'_injection.1 b) -> a = b
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet a, b: hartogs_number' H: uni_fix (hartogs_number'_injection.1 a) =
uni_fix (hartogs_number'_injection.1 b) H': uni_fix (hartogs_number'_injection.1 a) =
uni_fix (hartogs_number'_injection.1 b) ->
hartogs_number'_injection.1 a =
hartogs_number'_injection.1 b
a = b
univalence: Univalence prop_resizing: PropResizing lem: ExcludedMiddle A: HSet a, b: hartogs_number' H: hartogs_number'_injection.1 a =
hartogs_number'_injection.1 b H': uni_fix (hartogs_number'_injection.1 a) =
uni_fix (hartogs_number'_injection.1 b) ->
hartogs_number'_injection.1 a =
hartogs_number'_injection.1 b
a = b
byapply hartogs_number'_injection.2.Qed.Definitionhartogs_number : Ordinal@{A _}
:= resize_ordinal hartogs_number' hartogs_number_carrier hartogs_equiv.(* This final definition by satisfies the expected cardinality properties. *)