Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
(* -*- mode: coq; mode: visual-line -*- *)
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
forall (A : Type) (B : ?O_reflector A -> Type),
(foralla : A, ?O_reflector (B (?to A a))) ->
forallz : ?O_reflector A, ?O_reflector (B z)
H: Funext U: HProp
forall (A : Type) (B : ?O_reflector A -> Type)
(f : foralla : A, ?O_reflector (B (?to A a)))
(a : A), ?O_indO A B f (?to A a) = f a
H: Funext U: HProp
forall (A : Type) (zz' : ?O_reflector A),
IsEquiv (?to (z = z'))
H: Funext U: HProp
Type -> Type
intros X; exact (U -> X).
H: Funext U: HProp
forallT : Type, T -> (funX : Type => U -> X) T
H: Funext U: HProp T: Type x: T
U -> T
exact (fun_ => x).
H: Funext U: HProp
forall (A : Type)
(B : (funX : Type => U -> X) A -> Type),
(foralla : A,
(funX : Type => U -> X)
(B
((fun (T : Type) (x : T) =>
(fun_ : U => x) : (funX : Type => U -> X) T)
A a))) ->
forallz : (funX : Type => U -> X) A,
(funX : Type => U -> X) (B z)
H: Funext U: HProp A: Type B: (U -> A) -> Type f: foralla : A, U -> B (fun_ : U => a) z: U -> A u: U
B z
H: Funext U: HProp A: Type B: (U -> A) -> Type f: foralla : A, U -> B (fun_ : U => a) z: U -> A u: U
(fun_ : U => z u) = z
H: Funext U: HProp A: Type B: (U -> A) -> Type f: foralla : A, U -> B (fun_ : U => a) z: U -> A u, u': U
z u = z u'
apply ap; apply path_ishprop.
H: Funext U: HProp
forall (A : Type)
(B : (funX : Type => U -> X) A -> Type)
(f : foralla : A,
(funX : Type => U -> X)
(B
((fun (T : Type) (x : T) =>
(fun_ : U => x)
:
(funX : Type => U -> X) T) A a)))
(a : A),
((fun (A0 : Type) (B0 : (U -> A0) -> Type)
(f0 : foralla0 : A0, U -> B0 (fun_ : U => a0))
(z : U -> A0) (u : U) =>
transport B0
(path_arrow (fun_ : U => z u) z
((funu' : U => ap z (path_ishprop u u'))
:
(fun_ : U => z u) == z)) (f0 (z u) u))
:
forall (A0 : Type)
(B0 : (funX : Type => U -> X) A0 -> Type),
(foralla0 : A0,
(funX : Type => U -> X)
(B0
((fun (T : Type) (x : T) =>
(fun_ : U => x) : (funX : Type => U -> X) T)
A0 a0))) ->
forallz : (funX : Type => U -> X) A0,
(funX : Type => U -> X) (B0 z)) A B f
((fun (T : Type) (x : T) =>
(fun_ : U => x) : (funX : Type => U -> X) T) A a) =
f a
H: Funext U: HProp A: Type B: (U -> A) -> Type f: foralla : A, U -> B (fun_ : U => a) a: A
(funu : U =>
transport B
(path_arrow (fun_ : U => a) (fun_ : U => a)
(funu' : U =>
ap (fun_ : U => a) (path_ishprop u u')))
(f a u)) = f a
H: Funext U: HProp A: Type B: (U -> A) -> Type f: foralla : A, U -> B (fun_ : U => a) a: A u: U
transport B
(path_arrow (fun_ : U => a) (fun_ : U => a)
(funu' : U =>
ap (fun_ : U => a) (path_ishprop u u')))
(f a u) = f a u
H: Funext U: HProp A: Type B: (U -> A) -> Type f: foralla : A, U -> B (fun_ : U => a) a: A u: U
transport B
(path_arrow (fun_ : U => a) (fun_ : U => a)
(funu' : U =>
ap (fun_ : U => a) (path_ishprop u u')))
(f a u) = transport B 1 (f a u)
H: Funext U: HProp A: Type B: (U -> A) -> Type f: foralla : A, U -> B (fun_ : U => a) a: A u: U
path_arrow (fun_ : U => a) (fun_ : U => a)
(funu' : U =>
ap (fun_ : U => a) (path_ishprop u u')) = 1
H: Funext U: HProp A: Type B: (U -> A) -> Type f: foralla : A, U -> B (fun_ : U => a) a: A u: U
path_arrow (fun_ : U => a) (fun_ : U => a)
(funu' : U =>
ap (fun_ : U => a) (path_ishprop u u')) =
path_arrow (fun_ : U => a) (fun_ : U => a) (ap10 1)
H: Funext U: HProp A: Type B: (U -> A) -> Type f: foralla : A, U -> B (fun_ : U => a) a: A u: U
path_arrow (fun_ : U => a) (fun_ : U => a) (ap10 1) =
1
H: Funext U: HProp A: Type B: (U -> A) -> Type f: foralla : A, U -> B (fun_ : U => a) a: A u: U
path_arrow (fun_ : U => a) (fun_ : U => a)
(funu' : U =>
ap (fun_ : U => a) (path_ishprop u u')) =
path_arrow (fun_ : U => a) (fun_ : U => a) (ap10 1)
H: Funext U: HProp A: Type B: (U -> A) -> Type f: foralla : A, U -> B (fun_ : U => a) a: A u: U
(funu' : U => ap (fun_ : U => a) (path_ishprop u u')) =
ap10 1
H: Funext U: HProp A: Type B: (U -> A) -> Type f: foralla : A, U -> B (fun_ : U => a) a: A u, u': U
ap (fun_ : U => a) (path_ishprop u u') = ap10 1 u'
apply ap_const.
H: Funext U: HProp A: Type B: (U -> A) -> Type f: foralla : A, U -> B (fun_ : U => a) a: A u: U
path_arrow (fun_ : U => a) (fun_ : U => a) (ap10 1) =
1
apply eta_path_arrow.
H: Funext U: HProp
forall (A : Type) (zz' : (funX : Type => U -> X) A),
IsEquiv
((fun (T : Type) (x : T) =>
(fun_ : U => x) : (funX : Type => U -> X) T)
(z = z'))
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A
IsEquiv
((fun (T : Type) (x : T) =>
(fun_ : U => x) : (funX : Type => U -> X) T)
(z = z'))
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A
(U -> z = z') -> z = z'
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A
(funx : z = z' =>
(fun_ : U => x) : (funX : Type => U -> X) (z = z'))
o ?g == idmap
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A
?g
o (funx : z = z' =>
(fun_ : U => x)
:
(funX : Type => U -> X) (z = z')) == idmap
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A
(U -> z = z') -> z = z'
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A f: U -> z = z' u: U
z u = z' u
exact (ap10 (f u) u).
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A
(funx : z = z' =>
(fun_ : U => x) : (funX : Type => U -> X) (z = z'))
o (funf : U -> z = z' =>
path_arrow z z'
((funu : U => ap10 (f u) u) : z == z')) == idmap
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A f: U -> z = z' u: U
path_arrow z z' (funu : U => ap10 (f u) u) = f u
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A f: U -> z = z' u: U
path_arrow z z' (funu : U => ap10 (f u) u) =
path_arrow z z' (ap10 (f u))
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A f: U -> z = z' u: U
path_arrow z z' (ap10 (f u)) = f u
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A f: U -> z = z' u: U
path_arrow z z' (funu : U => ap10 (f u) u) =
path_arrow z z' (ap10 (f u))
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A f: U -> z = z' u: U
(funu : U => ap10 (f u) u) = ap10 (f u)
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A f: U -> z = z' u, u': U
ap10 (f u') u' = ap10 (f u) u'
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A f: U -> z = z' u, u': U
u' = u
apply path_ishprop.
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A f: U -> z = z' u: U
path_arrow z z' (ap10 (f u)) = f u
apply eta_path_arrow.
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A
(funf : U -> z = z' =>
path_arrow z z'
((funu : U => ap10 (f u) u) : z == z'))
o (funx : z = z' =>
(fun_ : U => x)
:
(funX : Type => U -> X) (z = z')) == idmap
H: Funext U: HProp A: Type z, z': (funX : Type => U -> X) A p: z = z'
path_arrow z z' (funu : U => ap10 p u) = p
refine (eta_path_arrow _ _ _).Defined.(** ** The open modality is lex *)(** Note that unlike most other cases, we can prove this without univalence (though we do of course need funext). *)
H: Funext U: HProp
Lex (Op U)
H: Funext U: HProp
Lex (Op U)
H: Funext U: HProp
forallA : Type,
IsConnected (Op U) A ->
forallxy : A, IsConnected (Op U) (x = y)
H: Funext U: HProp A: Type Ac: IsConnected (Op U) A x, y: A
IsConnected (Op U) (x = y)
H: Funext U: HProp A: Type Ac: IsConnected (Op U) A x, y: A
U -> Contr (x = y)
H: Funext U: HProp A: Type Ac: IsConnected (Op U) A x, y: A u: U
Contr (x = y)
H: Funext U: HProp A: Type Ac: IsConnected (Op U) A x, y: A u: U i:= contr_inhabited_hprop U u: Contr U
Contr (x = y)
H: Funext U: HProp A: Type Ac: IsConnected (Op U) A x, y: A u: U i:= contr_inhabited_hprop U u: Contr U
Contr A
H: Funext U: HProp A: Type Ac: IsConnected (Op U) A x, y: A u: U i:= contr_inhabited_hprop U u: Contr U
Contr (U -> A)
exact Ac.Defined.(** ** The open modality is accessible. *)
H: Funext U: HProp
IsAccModality (Op U)
H: Funext U: HProp
IsAccModality (Op U)
H: Funext U: HProp
NullGenerators
H: Funext U: HProp
forallX : Type,
In (Op U) X <-> IsNull_Internal.IsNull ?acc_ngen X
H: Funext U: HProp
NullGenerators
H: Funext U: HProp
?ngen_indices -> Type
exact (unit_name U).
H: Funext U: HProp
forallX : Type,
In (Op U) X <->
IsNull_Internal.IsNull
{| ngen_indices := Unit; ngen_type := unit_name U |}
X
H: Funext U: HProp X: Type
In (Op U) X ->
IsNull_Internal.IsNull
{| ngen_indices := Unit; ngen_type := unit_name U |}
X
H: Funext U: HProp X: Type
IsNull_Internal.IsNull
{| ngen_indices := Unit; ngen_type := unit_name U |}
X -> In (Op U) X
H: Funext U: HProp X: Type
In (Op U) X ->
IsNull_Internal.IsNull
{| ngen_indices := Unit; ngen_type := unit_name U |}
X
H: Funext U: HProp X: Type X_inO: In (Op U) X u: lgen_indices
(null_to_local_generators
{|
ngen_indices := Unit;
ngen_type := unit_name U
|})
ooExtendableAlong
(null_to_local_generators
{|
ngen_indices := Unit; ngen_type := unit_name U
|} u)
(fun_ : lgen_codomain
(null_to_local_generators
{|
ngen_indices := Unit;
ngen_type := unit_name U
|}) u => X)
H: Funext U: HProp X: Type X_inO: In (Op U) X u: lgen_indices
(null_to_local_generators
{|
ngen_indices := Unit;
ngen_type := unit_name U
|})
IsEquiv
(fung : lgen_codomain
(null_to_local_generators
{|
ngen_indices := Unit;
ngen_type := unit_name U
|}) u -> X =>
g
oD null_to_local_generators
{|
ngen_indices := Unit;
ngen_type := unit_name U
|} u)
H: Funext U: HProp X: Type X_inO: In (Op U) X u: lgen_indices
(null_to_local_generators
{|
ngen_indices := Unit;
ngen_type := unit_name U
|})
IsEquiv
(funx : X =>
unit_name x
oD null_to_local_generators
{|
ngen_indices := Unit;
ngen_type := unit_name U
|} u)
apply X_inO.
H: Funext U: HProp X: Type
IsNull_Internal.IsNull
{| ngen_indices := Unit; ngen_type := unit_name U |}
X -> In (Op U) X
IsEquiv
(fun (h : Unit -> X) (x : U) => h (const_tt U x))
refine (isequiv_ooextendable (fun_ => X) (const_tt U) ext).Defined.(** Thus, arguably a better definition of [Op] would be as a nullification modality, as it would not require [Funext] and would have a judgmental computation rule. However, the above definition is also nice to know, as it doesn't use HITs. We name the other version [Op']. *)DefinitionOp' (U : HProp) : Modality
:= Nul (Build_NullGenerators Unit (fun_ => U)).