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.Paths Types.Sigma Types.Forall.Declare Scope dpath_scope.Delimit Scope dpath_scope with dpath.LocalOpen Scope dpath_scope.DefinitionDPath {A} (P : A -> Type) {a0a1} (p : a0 = a1)
(b0 : P a0) (b1 : P a1) : Type
:= transport P p b0 = b1.(** This allows DPaths to collapse to paths under cbn *)Arguments DPath _ / _ _ _ : simpl nomatch.Global Instanceistrunc_dp {A : Type} {P : A -> Type} {n : trunc_index}
{a0a1} {p : a0 = a1} {b0 : P a0} {b1 : P a1} `{IsTrunc n.+1 (P a0)}
`{IsTrunc n.+1 (P a1)} : IsTrunc n (DPath P p b0 b1) := _.
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1: P a1 IsHProp0: IsHProp (P a0) IsHProp1: IsHProp (P a1)
DPath P p b0 b1
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1: P a1 IsHProp0: IsHProp (P a0) IsHProp1: IsHProp (P a1)
DPath P p b0 b1
apply path_ishprop.Defined.(** We have reflexivity for DPaths, this helps coq guess later *)Definitiondp_id {A} {P : A -> Type} {a : A} {x : P a} : DPath P 1 x x := 1%path.(** Although [1%dpath] is definitionally [1%path], when [1%path] is used where a dependent path is expected, Coq sometimes has trouble interpreting this. So we make a custom notation for [1] in [dpath_scope]. *)Notation"1" := dp_id : dpath_scope.(** DPath induction *)
A: Type P: A -> Type P0: forall (a0a1 : A) (p : a0 = a1) (b0 : P a0)
(b1 : P a1), DPath P p b0 b1 -> Type
(forall (x : A) (y : P x), P0 x x 1%path y y 1) ->
forall (a0a1 : A) (p : a0 = a1) (b0 : P a0)
(b1 : P a1) (d : DPath P p b0 b1), P0 a0 a1 p b0 b1 d
A: Type P: A -> Type P0: forall (a0a1 : A) (p : a0 = a1) (b0 : P a0)
(b1 : P a1), DPath P p b0 b1 -> Type
(forall (x : A) (y : P x), P0 x x 1%path y y 1) ->
forall (a0a1 : A) (p : a0 = a1) (b0 : P a0)
(b1 : P a1) (d : DPath P p b0 b1), P0 a0 a1 p b0 b1 d
intros X a0 a1 [] b0 b1 []; apply X.Defined.(** A DPath over a constant family is just a path *)
A, C: Type a0, a1: A p: a0 = a1 x, y: C
x = y <~> DPath (fun_ : A => C) p x y
A, C: Type a0, a1: A p: a0 = a1 x, y: C
x = y <~> DPath (fun_ : A => C) p x y
bydestruct p.Defined.Notationdp_const := equiv_dp_const.(** dp_apD of a non-dependent map is just a constant DPath *)
A, B: Type f: A -> B a0, a1: A p: a0 = a1
apD f p = dp_const (ap f p)
A, B: Type f: A -> B a0, a1: A p: a0 = a1
apD f p = dp_const (ap f p)
bydestruct p.Defined.(** An alternate version useful for proving recursion computation rules from induction ones *)
A, B: Type f: A -> B a0, a1: A p: a0 = a1
dp_const^-1 (apD f p) = ap f p
A, B: Type f: A -> B a0, a1: A p: a0 = a1
dp_const^-1 (apD f p) = ap f p
A, B: Type f: A -> B a0, a1: A p: a0 = a1
apD f p = dp_const (ap f p)
apply dp_apD_const.Defined.(** Concatenation of dependent paths *)
A: Type P: A -> Type a0, a1, a2: A p: a0 = a1 q: a1 = a2 b0: P a0 b1: P a1 b2: P a2
DPath P p b0 b1 ->
DPath P q b1 b2 -> DPath P (p @ q) b0 b2
A: Type P: A -> Type a0, a1, a2: A p: a0 = a1 q: a1 = a2 b0: P a0 b1: P a1 b2: P a2
DPath P p b0 b1 ->
DPath P q b1 b2 -> DPath P (p @ q) b0 b2
A: Type P: A -> Type a0: A b0, b1, b2: P a0
DPath P 1 b0 b1 ->
DPath P 1 b1 b2 -> DPath P (1 @ 1) b0 b2
exact concat.Defined.Notation"x '@Dp' y" := (dp_concat x y) : dpath_scope.(** Concatenation of dependent paths with non-dependent paths *)
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1, b2: P a1
DPath P p b0 b1 -> b1 = b2 -> DPath P p b0 b2
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1, b2: P a1
bydestruct p.Defined.SectionDGroupoid.Context {A} {P : A -> Type} {a0a1} {p : a0 = a1}
{b0 : P a0} {b1 : P a1} {dp : DPath P p b0 b1}.
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1: P a1 dp: DPath P p b0 b1
DPath (funt : a0 = a1 => DPath P t b0 b1)
(concat_p1 p) (dp @Dp 1) dp
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1: P a1 dp: DPath P p b0 b1
DPath (funt : a0 = a1 => DPath P t b0 b1)
(concat_p1 p) (dp @Dp 1) dp
A: Type P: A -> Type a0: A p: a0 = a0 b0, b1: P a0 dp: DPath P 1 b0 b1
DPath (funt : a0 = a0 => DPath P t b0 b1)
(concat_p1 1) (dp @Dp 1) dp
apply concat_p1.Defined.
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1: P a1 dp: DPath P p b0 b1
DPath (funt : a0 = a1 => DPath P t b0 b1)
(concat_1p p) (1 @Dp dp) dp
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1: P a1 dp: DPath P p b0 b1
DPath (funt : a0 = a1 => DPath P t b0 b1)
(concat_1p p) (1 @Dp dp) dp
A: Type P: A -> Type a0: A p: a0 = a0 b0, b1: P a0 dp: DPath P 1 b0 b1
DPath (funt : a0 = a0 => DPath P t b0 b1)
(concat_1p 1) (1 @Dp dp) dp
apply concat_1p.Defined.
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1: P a1 dp: DPath P p b0 b1
DPath (funt : a1 = a1 => DPath P t b1 b1)
(concat_Vp p) (dp ^D @Dp dp) 1
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1: P a1 dp: DPath P p b0 b1
DPath (funt : a1 = a1 => DPath P t b1 b1)
(concat_Vp p) (dp ^D @Dp dp) 1
A: Type P: A -> Type a0: A p: a0 = a0 b0, b1: P a0 dp: DPath P 1 b0 b1
DPath (funt : a0 = a0 => DPath P t b1 b1)
(concat_Vp 1) (dp ^D @Dp dp) 1
apply concat_Vp.Defined.
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1: P a1 dp: DPath P p b0 b1
DPath (funt : a0 = a0 => DPath P t b0 b0)
(concat_pV p) (dp @Dp dp ^D) 1
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1: P a1 dp: DPath P p b0 b1
DPath (funt : a0 = a0 => DPath P t b0 b0)
(concat_pV p) (dp @Dp dp ^D) 1
A: Type P: A -> Type a0: A p: a0 = a0 b0, b1: P a0 dp: DPath P 1 b0 b1
DPath (funt : a0 = a0 => DPath P t b0 b0)
(concat_pV 1) (dp @Dp dp ^D) 1
apply concat_pV.Defined.SectionConcat.Context {a2a3} {q : a1 = a2} {r : a2 = a3}
{b2 : P a2} {b3 : P a3}
(dq : DPath P q b1 b2) (dr : DPath P r b2 b3).
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1: P a1 dp: DPath P p b0 b1 a2, a3: A q: a1 = a2 r: a2 = a3 b2: P a2 b3: P a3 dq: DPath P q b1 b2 dr: DPath P r b2 b3
DPath (funt : a0 = a3 => DPath P t b0 b3)
(concat_pp_p p q r) ((dp @Dp dq) @Dp dr)
(dp @Dp (dq @Dp dr))
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1: P a1 dp: DPath P p b0 b1 a2, a3: A q: a1 = a2 r: a2 = a3 b2: P a2 b3: P a3 dq: DPath P q b1 b2 dr: DPath P r b2 b3
DPath (funt : a0 = a3 => DPath P t b0 b3)
(concat_pp_p p q r) ((dp @Dp dq) @Dp dr)
(dp @Dp (dq @Dp dr))
A: Type P: A -> Type a0: A p: a0 = a0 b0, b1: P a0 dp: DPath P 1 b0 b1 q, r: a0 = a0 b2, b3: P a0 dq: DPath P 1 b1 b2 dr: DPath P 1 b2 b3
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1: P a1 dp: DPath P p b0 b1 a2, a3: A q: a1 = a2 r: a2 = a3 b2: P a2 b3: P a3 dq: DPath P q b1 b2 dr: DPath P r b2 b3
DPath (funt : a0 = a3 => DPath P t b0 b3)
(concat_p_pp p q r) (dp @Dp (dq @Dp dr))
((dp @Dp dq) @Dp dr)
A: Type P: A -> Type a0, a1: A p: a0 = a1 b0: P a0 b1: P a1 dp: DPath P p b0 b1 a2, a3: A q: a1 = a2 r: a2 = a3 b2: P a2 b3: P a3 dq: DPath P q b1 b2 dr: DPath P r b2 b3
DPath (funt : a0 = a3 => DPath P t b0 b3)
(concat_p_pp p q r) (dp @Dp (dq @Dp dr))
((dp @Dp dq) @Dp dr)
A: Type P: A -> Type a0: A p: a0 = a0 b0, b1: P a0 dp: DPath P 1 b0 b1 q, r: a0 = a0 b2, b3: P a0 dq: DPath P 1 b1 b2 dr: DPath P 1 b2 b3
apply concat_p_pp.Defined.EndConcat.EndDGroupoid.(** Dependent paths over paths *)(** These can be found under names such as dp_paths_l akin to transport_paths_l *)
A: Type x1, x2, y: A p: x1 = x2 q: x1 = y r: x2 = y
p^ @ q = r <~> DPath (funx : A => x = y) p q r
A: Type x1, x2, y: A p: x1 = x2 q: x1 = y r: x2 = y
A, B: Type f: A -> B P: B -> Type x, y: A p: x = y q: f x = f y r: ap f p = q u: P (f x) v: P (f y)
DPath (funx : A => P (f x)) p u v <~> DPath P q u v
A, B: Type f: A -> B P: B -> Type x, y: A p: x = y q: f x = f y r: ap f p = q u: P (f x) v: P (f y)
DPath (funx : A => P (f x)) p u v <~> DPath P q u v
bydestruct r, p.Defined.Notationdp_compose' := equiv_dp_compose'.Definitionequiv_dp_compose {AB} (f : A -> B) (P : B -> Type) {xy : A}
(p : x = y) {u : P (f x)} {v : P (f y)}
: DPath (funx => P (f x)) p u v <~> DPath P (ap f p) u v
:= dp_compose' f P (idpath (ap f p)).Notationdp_compose := equiv_dp_compose.
A, B: Type f: A -> B P: B -> Type x, y: A p: x = y q: f x = f y r: ap f p = q g: forallb : B, P b
apD (g o f) p = (dp_compose' f P r)^-1 (apD g q)
A, B: Type f: A -> B P: B -> Type x, y: A p: x = y q: f x = f y r: ap f p = q g: forallb : B, P b
apD (g o f) p = (dp_compose' f P r)^-1 (apD g q)
bydestruct r, p.Defined.Definitiondp_apD_compose {AB : Type} (f : A -> B) (P : B -> Type)
{xy : A} (p : x = y) (g : forallb:B, P b)
: apD (g o f) p = (dp_compose f P p)^-1 (apD g (ap f p))
:= dp_apD_compose' f P (idpath (ap f p)) g.(** Type constructors *)(** Many of these lemmas exist already for transports but we prove them for DPaths anyway. If we change the definition of DPath to the transport, then these will no longer be needed. It is however, far more readable to keep such lemmas seperate, since it is difficult to otherwise search for a DPath lemma if they are all written using transports. *)(** A version of [equiv_path_sigma] for [DPath]s *)Definitionequiv_path_sigma_dp {AP} {xx' : A} {y : P x} {y' : P x'}
: {p : x = x' & DPath P p y y'} <~> (x; y) = (x'; y')
:= equiv_path_sigma P (x; y) (x'; y').Notationpath_sigma_dp := equiv_path_sigma_dp.
A: Type P: A -> Type x, x': A y: P x y': P x' p: x = x' q: DPath P p y y'
ap pr1 (path_sigma_dp (p; q)) = p
A: Type P: A -> Type x, x': A y: P x y': P x' p: x = x' q: DPath P p y y'
ap pr1 (path_sigma_dp (p; q)) = p
apply ap_pr1_path_sigma.Defined.(* DPath over a forall *)
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1, a2: A p: a1 = a2 f: forallx : B a1, C (a1; x) g: forallx : B a2, C (a2; x)
(forall (x : B a1) (y : B a2) (q : DPath B p x y),
DPath C (path_sigma_dp (p; q)) (f x) (g y)) <~>
DPath (funa : A => forallx : B a, C (a; x)) p f g
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1, a2: A p: a1 = a2 f: forallx : B a1, C (a1; x) g: forallx : B a2, C (a2; x)
(forall (x : B a1) (y : B a2) (q : DPath B p x y),
DPath C (path_sigma_dp (p; q)) (f x) (g y)) <~>
DPath (funa : A => forallx : B a, C (a; x)) p f g
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1, a2: A p: a1 = a2 f: forallx : B a1, C (a1; x) g: forallx : B a2, C (a2; x)
DPath (funa : A => forallx : B a, C (a; x)) p f g <~>
(forall (x : B a1) (y : B a2) (q : DPath B p x y),
DPath C (path_sigma_dp (p; q)) (f x) (g y))
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1: A f, g: forallx : B a1, C (a1; x)
f = g <~>
(forall (xy : B a1) (q : x = y),
transport C
(path_sigma_uncurried B (a1; x) (a1; y) (1%path; q))
(f x) = g y)
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1: A f, g: forallx : B a1, C (a1; x)
f == g <~>
(forall (xy : B a1) (q : x = y),
transport C
(path_sigma_uncurried B (a1; x) (a1; y) (1%path; q))
(f x) = g y)
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1: A f, g: forallx : B a1, C (a1; x)
foralla : B a1,
f a = g a <~>
(forall (y : B a1) (q : a = y),
transport C
(path_sigma_uncurried B (a1; a) (a1; y) (1%path; q))
(f a) = g y)
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1: A f, g: forallx : B a1, C (a1; x) a: B a1
f a = g a <~>
(forall (y : B a1) (q : a = y),
transport C
(path_sigma_uncurried B (a1; a) (a1; y) (1%path; q))
(f a) = g y)
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1: A f, g: forallx : B a1, C (a1; x) a: B a1
f a = g a ->
forall (y : B a1) (q : a = y),
transport C
(path_sigma_uncurried B (a1; a) (a1; y) (1%path; q))
(f a) = g y
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1: A f, g: forallx : B a1, C (a1; x) a: B a1
(forall (y : B a1) (q : a = y),
transport C
(path_sigma_uncurried B (a1; a) (a1; y) (1%path; q))
(f a) = g y) -> f a = g a
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1: A f, g: forallx : B a1, C (a1; x) a: B a1
?f o ?g == idmap
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1: A f, g: forallx : B a1, C (a1; x) a: B a1
?g o ?f == idmap
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1: A f, g: forallx : B a1, C (a1; x) a: B a1
f a = g a ->
forall (y : B a1) (q : a = y),
transport C
(path_sigma_uncurried B (a1; a) (a1; y) (1%path; q))
(f a) = g y
byintros ? ? [].
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1: A f, g: forallx : B a1, C (a1; x) a: B a1
(forall (y : B a1) (q : a = y),
transport C
(path_sigma_uncurried B (a1; a) (a1; y) (1%path; q))
(f a) = g y) -> f a = g a
intro F; exact (F a 1).
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1: A f, g: forallx : B a1, C (a1; x) a: B a1
(fun (X : f a = g a) (y : B a1) (q : a = y) =>
match
q as p in (_ = b)
return
(transport C
(path_sigma_uncurried B (a1; a) (a1; b)
(1%path; p)) (f a) = g b)
with
| 1%path => X
end)
o (funF : forall (y : B a1) (q : a = y),
transport C
(path_sigma_uncurried B (a1; a) (a1; y)
(1%path; q)) (f a) = g y => F a 1) ==
idmap
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1: A f, g: forallx : B a1, C (a1; x) a: B a1 x: forall (y : B a1) (q : a = y),
transport C
(path_sigma_uncurried B (a1; a) (a1; y)
(1%path; q)) (f a) = g y x0: B a1
(funq : a = x0 =>
match
q as p in (_ = b)
return
(transport C
(path_sigma_uncurried B (a1; a) (a1; b)
(1%path; p)) (f a) = g b)
with
| 1%path => x a 1end) == x x0
byintros [].
H: Funext A: Type B: A -> Type C: {x : _ & B x} -> Type a1: A f, g: forallx : B a1, C (a1; x) a: B a1
(funF : forall (y : B a1) (q : a = y),
transport C
(path_sigma_uncurried B (a1; a) (a1; y)
(1%path; q)) (f a) = g y => F a 1)
o (fun (X : f a = g a) (y : B a1) (q : a = y) =>
match
q as p in (_ = b)
return
(transport C
(path_sigma_uncurried B (a1; a) (a1; b)
(1%path; p)) (f a) = g b)
with
| 1%path => X
end) == idmap
byintro.Defined.Notationdp_forall := equiv_dp_forall.(* DPath over an arrow *)
H: Funext A: Type B, C: A -> Type a1, a2: A p: a1 = a2 f: B a1 -> C a1 g: B a2 -> C a2
(forallx : B a1,
DPath C p (f x) (g (transport B p x))) <~>
DPath (funx : A => B x -> C x) p f g
H: Funext A: Type B, C: A -> Type a1, a2: A p: a1 = a2 f: B a1 -> C a1 g: B a2 -> C a2
(forallx : B a1,
DPath C p (f x) (g (transport B p x))) <~>
DPath (funx : A => B x -> C x) p f g
H: Funext A: Type B, C: A -> Type a1: A f, g: B a1 -> C a1
(forallx : B a1,
DPath C 1 (f x) (g (transport B 1 x))) <~>
DPath (funx : A => B x -> C x) 1 f g
apply equiv_path_forall.Defined.Notationdp_arrow := equiv_dp_arrow.(* Restricted version allowing us to pull the domain of a forall out *)
H: Funext D, A: Type B: D -> A -> Type t1, t2: D d: t1 = t2 f: forallx : A, B t1 x g: forallx : A, B t2 x
(forallx : A,
DPath (funt : D => B t x) d (f x) (g x)) <~>
DPath (funt : D => forallx : A, B t x) d f g
H: Funext D, A: Type B: D -> A -> Type t1, t2: D d: t1 = t2 f: forallx : A, B t1 x g: forallx : A, B t2 x
(forallx : A,
DPath (funt : D => B t x) d (f x) (g x)) <~>
DPath (funt : D => forallx : A, B t x) d f g
H: Funext D, A: Type B: D -> A -> Type t1: D f, g: forallx : A, B t1 x
(forallx : A,
DPath (funt : D => B t x) 1 (f x) (g x)) <~>
DPath (funt : D => forallx : A, B t x) 1 f g