Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Universe.Require Import HSet.Require Import HIT.epi HIT.unique_choice.LocalOpen Scope path_scope.(** We prove that [epi + mono <-> IsEquiv] *)Sectioniso.Context `{Univalence}.VariablesXY : HSet.Variablef : X -> Y.
H: Univalence X, Y: HSet f: X -> Y injf: isinj f
forally : Y, atmost1P (funx : X => f x = y)
H: Univalence X, Y: HSet f: X -> Y injf: isinj f
forally : Y, atmost1P (funx : X => f x = y)
H: Univalence X, Y: HSet f: X -> Y injf: forallx0x1 : X, f x0 = f x1 -> x0 = x1
forall (y : Y) (x1x2 : X),
f x1 = y -> f x2 = y -> x1 = x2
H: Univalence X, Y: HSet f: X -> Y injf: forallx0x1 : X, f x0 = f x1 -> x0 = x1 y: Y x1, x2: X X0: f x1 = y X1: f x2 = y
x1 = x2
H: Univalence X, Y: HSet f: X -> Y injf: forallx0x1 : X, f x0 = f x1 -> x0 = x1 y: Y x1, x2: X X0: f x1 = y X1: f x2 = y
f x1 = f x2
H: Univalence X, Y: HSet f: X -> Y injf: forallx0x1 : X, f x0 = f x1 -> x0 = x1 x1, x2: X
f x1 = f x1
reflexivity.Defined.
H: Univalence X, Y: HSet f: X -> Y epif: isepi f monof: ismono f
IsEquiv f
H: Univalence X, Y: HSet f: X -> Y epif: isepi f monof: ismono f
IsEquiv f
H: Univalence X, Y: HSet f: X -> Y epif: isepi f monof: ismono f surjf: ReflectiveSubuniverse.IsConnMap
(Modality.modality_to_reflective_subuniverse
(Core.Tr (-1))) f
IsEquiv f
H: Univalence X, Y: HSet f: X -> Y epif: isepi f monof: ismono f surjf: ReflectiveSubuniverse.IsConnMap
(Modality.modality_to_reflective_subuniverse
(Core.Tr (-1))) f injf: isinj f
IsEquiv f
H: Univalence X, Y: HSet f: X -> Y epif: isepi f monof: ismono f surjf: ReflectiveSubuniverse.IsConnMap
(Modality.modality_to_reflective_subuniverse
(Core.Tr (-1))) f injf: isinj f H_unique_choice: {f0 : Y -> X &
forallx : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
(f0 x)}
IsEquiv f
H: Univalence X, Y: HSet f: X -> Y epif: isepi f monof: ismono f surjf: ReflectiveSubuniverse.IsConnMap
(Modality.modality_to_reflective_subuniverse
(Core.Tr (-1))) f injf: isinj f H_unique_choice: {f0 : Y -> X &
forallx : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
(f0 x)}
(funx : Y => f (H_unique_choice.1 x)) == idmap
H: Univalence X, Y: HSet f: X -> Y epif: isepi f monof: ismono f surjf: ReflectiveSubuniverse.IsConnMap
(Modality.modality_to_reflective_subuniverse
(Core.Tr (-1))) f injf: isinj f H_unique_choice: {f0 : Y -> X &
forallx : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
(f0 x)}
(funx : X => H_unique_choice.1 (f x)) == idmap
H: Univalence X, Y: HSet f: X -> Y epif: isepi f monof: ismono f surjf: ReflectiveSubuniverse.IsConnMap
(Modality.modality_to_reflective_subuniverse
(Core.Tr (-1))) f injf: isinj f H_unique_choice: {f0 : Y -> X &
forallx : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
(f0 x)}
(funx : Y => f (H_unique_choice.1 x)) == idmap
H: Univalence X, Y: HSet f: X -> Y epif: isepi f monof: ismono f surjf: ReflectiveSubuniverse.IsConnMap
(Modality.modality_to_reflective_subuniverse
(Core.Tr (-1))) f injf: isinj f H_unique_choice: {f0 : Y -> X &
forallx : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
(f0 x)} x: Y
f (H_unique_choice.1 x) = x
apply H_unique_choice.2.
H: Univalence X, Y: HSet f: X -> Y epif: isepi f monof: ismono f surjf: ReflectiveSubuniverse.IsConnMap
(Modality.modality_to_reflective_subuniverse
(Core.Tr (-1))) f injf: isinj f H_unique_choice: {f0 : Y -> X &
forallx : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
(f0 x)}
(funx : X => H_unique_choice.1 (f x)) == idmap
H: Univalence X, Y: HSet f: X -> Y epif: isepi f monof: ismono f surjf: ReflectiveSubuniverse.IsConnMap
(Modality.modality_to_reflective_subuniverse
(Core.Tr (-1))) f injf: isinj f H_unique_choice: {f0 : Y -> X &
forallx : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
(f0 x)} x: X
H_unique_choice.1 (f x) = x
H: Univalence X, Y: HSet f: X -> Y epif: isepi f monof: ismono f surjf: ReflectiveSubuniverse.IsConnMap
(Modality.modality_to_reflective_subuniverse
(Core.Tr (-1))) f injf: isinj f H_unique_choice: {f0 : Y -> X &
forallx : Y,
(fun (y : Y) (x0 : X) => f x0 = y) x
(f0 x)} x: X