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.
(** * Sequential colimits *)(** We present a proof of the conjecture that sequential colimits in HoTT appropriately commute with Σ-types. As a corollary, we characterize the path space of a sequential colimit as a sequential colimit of path spaces. For the written account of these results see https://www.cs.cornell.edu/~ks858/papers/sequential_colimits_homotopy.pdf. *)
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.Require Import Diagrams.Diagram.Require Import Diagrams.Sequence.Require Import Diagrams.Cocone.Require Import Colimits.Colimit.Require Import Spaces.Nat.Core.Require Import Homotopy.IdentitySystems.LocalOpen Scope nat_scope.LocalOpen Scope path_scope.(** [coe] is [transport idmap : (A = B) -> (A -> B)], but is described as the underlying map of an equivalence so that Coq knows that it is an equivalence. *)Notationcoe := (funp => equiv_fun (equiv_path _ _ p)).Notation"a ^+" := (@arr sequence_graph _ _ _ 1 a).(** Mapping spaces into hprops from colimits of sequences can be characterized. *)
H: Funext A: Sequence P: Type IsHProp0: IsHProp P
(Colimit A -> P) <~>
(foralln : Graph.graph0 sequence_graph, A n -> P)
H: Funext A: Sequence P: Type IsHProp0: IsHProp P
(Colimit A -> P) <~>
(foralln : Graph.graph0 sequence_graph, A n -> P)
H: Funext A: Sequence P: Type IsHProp0: IsHProp P
(foralln : Graph.graph0 sequence_graph, A n -> P) <~>
(Colimit A -> P)
H: Funext A: Sequence P: Type IsHProp0: IsHProp P
(foralln : Graph.graph0 sequence_graph, A n -> P) <~>
Cocone A P
H: Funext A: Sequence P: Type IsHProp0: IsHProp P
(foralln : Graph.graph0 sequence_graph, A n -> P) <~>
{H : foralli : Graph.graph0 sequence_graph, A i -> P
&
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
(funx : A i => H j ((A _f g) x)) == H i}
H: Funext A: Sequence P: Type IsHProp0: IsHProp P
{H : foralli : Graph.graph0 sequence_graph, A i -> P
&
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
(funx : A i => H j ((A _f g) x)) == H i} <~>
(foralln : Graph.graph0 sequence_graph, A n -> P)
H: Funext A: Sequence P: Type IsHProp0: IsHProp P
{H : foralli : Graph.graph0 sequence_graph, A i -> P
&
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
(funx : A i => H j ((A _f g) x)) == H i} ->
foralln : Graph.graph0 sequence_graph, A n -> P
H: Funext A: Sequence P: Type IsHProp0: IsHProp P
IsEquiv ?equiv_fun
H: Funext A: Sequence P: Type IsHProp0: IsHProp P
IsEquiv pr1
exact _.Defined.(** If a sequential colimit has maps homotopic to a constant map then the colimit is contractible. *)
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1
Contr (Colimit A)
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1
Contr (Colimit A)
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1
Sequence
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= ?Goal: Sequence
Contr (Colimit A)
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1
Sequence
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1
nat -> Type
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1
foralln : nat, ?X n -> ?X n.+1
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1
foralln : nat, A n -> A n.+1
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 n: nat
A n -> A n.+1
exact (const (a n.+1)).
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
Contr (Colimit A)
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
?Goal <~> Colimit A
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
Contr ?Goal
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
?Goal0 ~d~ A
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
Contr (Colimit ?Goal0)
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
B 0 <~> A 0
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
forall (n : Graph.graph0 sequence_graph)
(e : B n <~> A n),
{e' : B n.+1 <~> A n.+1 &
(funx : B n => (e x) ^+) == (funx : B n => e' x ^+)}
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
Contr (Colimit B)
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
forall (n : Graph.graph0 sequence_graph)
(e : B n <~> A n),
{e' : B n.+1 <~> A n.+1 &
(funx : B n => (e x) ^+) == (funx : B n => e' x ^+)}
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
Contr (Colimit B)
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
forall (n : Graph.graph0 sequence_graph)
(e : B n <~> A n),
{e' : B n.+1 <~> A n.+1 &
(funx : B n => (e x) ^+) == (funx : B n => e' x ^+)}
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence n: Graph.graph0 sequence_graph e: B n <~> A n
{e' : B n.+1 <~> A n.+1 &
(funx : B n => (e x) ^+) == (funx : B n => e' x ^+)}
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence n: Graph.graph0 sequence_graph e: B n <~> A n
(funx : B n => (e x) ^+) ==
(funx : B n => 1%equiv x ^+)
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence n: Graph.graph0 sequence_graph e: B n <~> A n x: B n
(e x) ^+ = 1%equiv x ^+
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence n: Graph.graph0 sequence_graph e: B n <~> A n x: B n
1%equiv x ^+ = (e x) ^+
exact (H _ (e x)).
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
Contr (Colimit B)
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
Colimit B
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
forally : Colimit B, ?center = y
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
forally : Colimit B, colim 1 (a 1) = y
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
forall (i : Graph.graph0 sequence_graph) (x : B i),
colim 1 (a 1) = colim i x
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j)
(x : B i),
transport (paths (colim 1 (a 1)))
(colimp i j g x) (?q j ((B _f g) x)) =
?q i x
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
forall (i : Graph.graph0 sequence_graph) (x : B i),
colim 1 (a 1) = colim i x
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence i: Graph.graph0 sequence_graph x: B i
colim 1 (a 1) = colim i x
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence x: B 0
colim 1 (a 1) = colim 0 x
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence i: nat x: B i.+1 IHi: forallx : B i, colim 1 (a 1) = colim i x
colim 1 (a 1) = colim i.+1 x
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence i: nat x: B i.+1 IHi: forallx : B i, colim 1 (a 1) = colim i x
colim 1 (a 1) = colim i.+1 x
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence i: nat x: B i.+1 IHi: forallx : B i, colim 1 (a 1) = colim i x
colim i (a i) = colim i.+1 x
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence i: nat x: B i.+1 IHi: forallx : B i, colim 1 (a 1) = colim i x
colim i.+1 (a i) ^+ = colim i.+1 x
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence i: nat x: B i.+1 IHi: forallx : B i, colim 1 (a 1) = colim i x
colim i.+2 (a i.+1) ^+ = colim i.+1 x
exact (colimp (D:=B) _ _ idpath x).
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j) (x : B i),
transport (paths (colim 1 (a 1))) (colimp i j g x)
((fun (i0 : Graph.graph0 sequence_graph) (x0 : B i0)
=>
nat_rect
(funi1 : nat =>
forallx1 : B i1, colim 1 (a 1) = colim i1 x1)
(funx1 : B 0 => colimp 011 x1)
(fun (i1 : nat)
(IHi : forallx1 : B i1,
colim 1 (a 1) = colim i1 x1)
(x1 : B i1.+1) =>
IHi (a i1) @
((colimp i1 i1.+11 (a i1))^ @
((colimp i1.+1 i1.+21 (a i1.+1))^ @
colimp i1.+1 i1.+21 x1))) i0 x0) j
((B _f g) x)) =
(fun (i0 : Graph.graph0 sequence_graph) (x0 : B i0) =>
nat_rect
(funi1 : nat =>
forallx1 : B i1, colim 1 (a 1) = colim i1 x1)
(funx1 : B 0 => colimp 011 x1)
(fun (i1 : nat)
(IHi : forallx1 : B i1,
colim 1 (a 1) = colim i1 x1)
(x1 : B i1.+1) =>
IHi (a i1) @
((colimp i1 i1.+11 (a i1))^ @
((colimp i1.+1 i1.+21 (a i1.+1))^ @
colimp i1.+1 i1.+21 x1))) i0 x0) i x
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence n, m: Graph.graph0 sequence_graph x: B n
transport (paths (colim 1 (a 1))) (colimp n n.+11 x)
(nat_rect
(funi : nat =>
forallx : B i, colim 1 (a 1) = colim i x)
(funx : B 0 => colimp 011 x)
(fun (i : nat)
(IHi : forallx : B i,
colim 1 (a 1) = colim i x) (x : B i.+1)
=>
IHi (a i) @
((colimp i i.+11 (a i))^ @
((colimp i.+1 i.+21 (a i.+1))^ @
colimp i.+1 i.+21 x))) n.+1 x ^+) =
nat_rect
(funi : nat =>
forallx : B i, colim 1 (a 1) = colim i x)
(funx : B 0 => colimp 011 x)
(fun (i : nat)
(IHi : forallx : B i, colim 1 (a 1) = colim i x)
(x : B i.+1) =>
IHi (a i) @
((colimp i i.+11 (a i))^ @
((colimp i.+1 i.+21 (a i.+1))^ @
colimp i.+1 i.+21 x))) n x
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence n, m: Graph.graph0 sequence_graph x: B n
((ap (fun_ : Colimit B => colim 1 (a 1))
(colimp n n.+11 x))^ @
nat_rect
(funi : nat =>
forallx : B i, colim 1 (a 1) = colim i x)
(funx : B 0 => colimp 011 x)
(fun (i : nat)
(IHi : forallx : B i, colim 1 (a 1) = colim i x)
(x : B i.+1) =>
IHi (a i) @
((colimp i i.+11 (a i))^ @
((colimp i.+1 i.+21 (a i.+1))^ @
colimp i.+1 i.+21 x))) n.+1 x ^+) @
ap idmap (colimp n n.+11 x) =
nat_rect
(funi : nat =>
forallx : B i, colim 1 (a 1) = colim i x)
(funx : B 0 => colimp 011 x)
(fun (i : nat)
(IHi : forallx : B i, colim 1 (a 1) = colim i x)
(x : B i.+1) =>
IHi (a i) @
((colimp i i.+11 (a i))^ @
((colimp i.+1 i.+21 (a i.+1))^ @
colimp i.+1 i.+21 x))) n x
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence n, m: Graph.graph0 sequence_graph x: B n
(1^ @
nat_rect
(funi : nat =>
forallx : B i, colim 1 (a 1) = colim i x)
(funx : B 0 => colimp 011 x)
(fun (i : nat)
(IHi : forallx : B i, colim 1 (a 1) = colim i x)
(x : B i.+1) =>
IHi (a i) @
((colimp i i.+11 (a i))^ @
((colimp i.+1 i.+21 (a i.+1))^ @
colimp i.+1 i.+21 x))) n.+1 x ^+) @
ap idmap (colimp n n.+11 x) =
nat_rect
(funi : nat =>
forallx : B i, colim 1 (a 1) = colim i x)
(funx : B 0 => colimp 011 x)
(fun (i : nat)
(IHi : forallx : B i, colim 1 (a 1) = colim i x)
(x : B i.+1) =>
IHi (a i) @
((colimp i i.+11 (a i))^ @
((colimp i.+1 i.+21 (a i.+1))^ @
colimp i.+1 i.+21 x))) n x
funext: Funext A: Sequence a: foralln : Graph.graph0 sequence_graph, A n H: foralln : nat, const (a n.+1) == A _f 1 B:= Build_Sequence A (funn : nat => const (a n.+1)): Sequence n, m: Graph.graph0 sequence_graph x: B n
(1^ @
nat_rect
(funi : nat =>
forallx : B i, colim 1 (a 1) = colim i x)
(funx : B 0 => colimp 011 x)
(fun (i : nat)
(IHi : forallx : B i, colim 1 (a 1) = colim i x)
(x : B i.+1) =>
IHi (a i) @
((colimp i i.+11 (a i))^ @
((colimp i.+1 i.+21 (a i.+1))^ @
colimp i.+1 i.+21 x))) n.+1 x ^+) @
colimp n n.+11 x =
nat_rect
(funi : nat =>
forallx : B i, colim 1 (a 1) = colim i x)
(funx : B 0 => colimp 011 x)
(fun (i : nat)
(IHi : forallx : B i, colim 1 (a 1) = colim i x)
(x : B i.+1) =>
IHi (a i) @
((colimp i i.+11 (a i))^ @
((colimp i.+1 i.+21 (a i.+1))^ @
colimp i.+1 i.+21 x))) n x
destruct n; simpl; hott_simpl.Qed.
A: Sequence a: A 0 k: Graph.graph0 sequence_graph
A k
A: Sequence a: A 0 k: Graph.graph0 sequence_graph
A k
A: Sequence a: A 0
A 0
A: Sequence a: A 0 k: nat q: A k
A k.+1
A: Sequence a: A 0
A 0
exact a.
A: Sequence a: A 0 k: nat q: A k
A k.+1
exact q^+.Defined.Notation"a ^+ k" := (seq_shift_from_zero_by a k).(** Shiftings; described in the paragraph after Lemma 3.7. *)
A: Sequence x: {x : _ & A x}
{x : _ & A x}
A: Sequence x: {x : _ & A x}
{x : _ & A x}
destruct x as [n a]; exact (n.+1; a^+).Defined.
A: Sequence x: {x : _ & A x} k: nat
{x : _ & A x}
A: Sequence x: {x : _ & A x} k: nat
{x : _ & A x}
A: Sequence x: {x : _ & A x}
{x : _ & A x}
A: Sequence x: {x : _ & A x} k: nat y: {x : _ & A x}
{x : _ & A x}
A: Sequence x: {x : _ & A x}
{x : _ & A x}
exact x.
A: Sequence x: {x : _ & A x} k: nat y: {x : _ & A x}
A: Sequence x: {x : _ & A x} k: nat q: (x ^++) ^++ k = x ^++ (k.+1)
(x ^++) ^++ (k.+1) = x ^++ (k.+2)
A: Sequence x: {x : _ & A x}
(x ^++) ^++ 0 = x ^++ 1
reflexivity.
A: Sequence x: {x : _ & A x} k: nat q: (x ^++) ^++ k = x ^++ (k.+1)
(x ^++) ^++ (k.+1) = x ^++ (k.+2)
exact (ap seq_pair_shift q).Defined.
A: Sequence a: A 0 k: nat
(0; a) ^++ k = (k; a ^+ k)
A: Sequence a: A 0 k: nat
(0; a) ^++ k = (k; a ^+ k)
A: Sequence a: A 0
(0; a) ^++ 0 = (0; a ^+ 0)
A: Sequence a: A 0 k: nat q: (0; a) ^++ k = (k; a ^+ k)
(0; a) ^++ (k.+1) = (k.+1; a ^+ (k.+1))
A: Sequence a: A 0
(0; a) ^++ 0 = (0; a ^+ 0)
reflexivity.
A: Sequence a: A 0 k: nat q: (0; a) ^++ k = (k; a ^+ k)
(0; a) ^++ (k.+1) = (k.+1; a ^+ (k.+1))
exact (ap seq_pair_shift q).Defined.Notationinj A := (@colim sequence_graph A).Notationglue A := (funn => @colimp sequence_graph A n n.+11).(** The uniqueness principle for sequential colimits; Lemma 3.3. *)
A: Sequence E: Type F, G: Colimit A -> E h: foralln : Graph.graph0 sequence_graph,
F o inj A n == G o inj A n H: forall (n : Graph.graph0 sequence_graph)
(a : A n),
ap F (glue A n a) @ h n a =
h n.+1 a ^+ @ ap G (glue A n a)
F == G
A: Sequence E: Type F, G: Colimit A -> E h: foralln : Graph.graph0 sequence_graph,
F o inj A n == G o inj A n H: forall (n : Graph.graph0 sequence_graph)
(a : A n),
ap F (glue A n a) @ h n a =
h n.+1 a ^+ @ ap G (glue A n a)
F == G
A: Sequence E: Type F, G: Colimit A -> E h: foralln : Graph.graph0 sequence_graph,
F o inj A n == G o inj A n H: forall (n : Graph.graph0 sequence_graph)
(a : A n),
ap F (glue A n a) @ h n a =
h n.+1 a ^+ @ ap G (glue A n a) n: Graph.graph0 sequence_graph a: A n
transport (funw : Colimit A => F w = G w)
(colimp n n.+11 a) (h n.+1 a ^+) = h n a
A: Sequence E: Type F, G: Colimit A -> E h: foralln : Graph.graph0 sequence_graph,
F o inj A n == G o inj A n H: forall (n : Graph.graph0 sequence_graph)
(a : A n),
ap F (glue A n a) @ h n a =
h n.+1 a ^+ @ ap G (glue A n a) n: Graph.graph0 sequence_graph a: A n
forallp : F (inj A n.+1 a ^+) = G (inj A n.+1 a ^+),
ap F 1 @ p = h n.+1 a ^+ @ ap G 1 ->
transport (funw : Colimit A => F w = G w) 1
(h n.+1 a ^+) = p
intros p q; srefine ((concat_p1 _)^ @ _); srefine (_ @ (concat_1p _)); exact q^.Defined.(** The successor sequence from Lemma 3.6. *)Definitionsucc_seq (A : Sequence) : Sequence
:= Build_Sequence (funk => A k.+1) (funka => a^+).(** The shifted sequence from Lemma 3.7. *)Definitionshift_seq (A : Sequence) n : Sequence
:= Build_Sequence (funk => A (k+n)%nat) (funka => a^+).(** The canonical equivalence between the colimit of the successor sequence and the colimit of the original sequence; Lemma 3.6. *)
A: Sequence
Colimit (succ_seq A) -> Colimit A
A: Sequence
Colimit (succ_seq A) -> Colimit A
A: Sequence
foralli : Graph.graph0 sequence_graph,
succ_seq A i -> Colimit A
A: Sequence
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
?legs j o (succ_seq A) _f g == ?legs i
A: Sequence
foralli : Graph.graph0 sequence_graph,
succ_seq A i -> Colimit A
exact (funna => inj _ n.+1 a).
A: Sequence
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
(fun (n : Graph.graph0 sequence_graph)
(a : succ_seq A n) => inj A n.+1 a) j
o (succ_seq A) _f g ==
(fun (n : Graph.graph0 sequence_graph)
(a : succ_seq A n) => inj A n.+1 a) i
intros n m p; destruct p; exact (glue A n.+1).Defined.
A: Sequence n: Graph.graph0 sequence_graph a: succ_seq A n
ap (colim_succ_seq_to_colim_seq A)
(glue (succ_seq A) n a) = glue A n.+1 a
A: Sequence n: Graph.graph0 sequence_graph a: succ_seq A n
ap (colim_succ_seq_to_colim_seq A)
(glue (succ_seq A) n a) = glue A n.+1 a
srapply Colimit_rec_beta_colimp.Defined.
A: Sequence n: Graph.graph0 sequence_graph a1, a2: succ_seq A n p: a1 = a2
ap (colim_succ_seq_to_colim_seq A)
(ap (inj (succ_seq A) n) p) = ap (inj A n.+1) p
A: Sequence n: Graph.graph0 sequence_graph a1, a2: succ_seq A n p: a1 = a2
ap (colim_succ_seq_to_colim_seq A)
(ap (inj (succ_seq A) n) p) = ap (inj A n.+1) p
destruct p; reflexivity.Defined.
A: Sequence
IsEquiv (colim_succ_seq_to_colim_seq A)
A: Sequence
IsEquiv (colim_succ_seq_to_colim_seq A)
A: Sequence
Colimit A -> Colimit (succ_seq A)
A: Sequence
colim_succ_seq_to_colim_seq A o ?g == idmap
A: Sequence
?g o colim_succ_seq_to_colim_seq A == idmap
A: Sequence
Colimit A -> Colimit (succ_seq A)
A: Sequence
foralli : Graph.graph0 sequence_graph,
A i -> Colimit (succ_seq A)
A: Sequence
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
?legs j o A _f g == ?legs i
A: Sequence
foralli : Graph.graph0 sequence_graph,
A i -> Colimit (succ_seq A)
exact (funna => inj (succ_seq A) n a^+).
A: Sequence
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
(fun (n : Graph.graph0 sequence_graph) (a : A n) =>
inj (succ_seq A) n a ^+) j o A _f g ==
(fun (n : Graph.graph0 sequence_graph) (a : A n) =>
inj (succ_seq A) n a ^+) i
intros n m p a; destruct p; exact (glue (succ_seq A) n a^+).
A: Sequence
colim_succ_seq_to_colim_seq A
o Colimit_rec (Colimit (succ_seq A))
{|
legs :=
fun (n : Graph.graph0 sequence_graph)
(a : A n) => inj (succ_seq A) n a ^+;
legs_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m) =>
(funa : A n =>
match
p as p0 in (_ = n0)
return
(inj (succ_seq A) n0 ((A _f p0) a) ^+ =
inj (succ_seq A) n a ^+)
with
| 1 => glue (succ_seq A) n a ^+
end)
:
(fun (n0 : Graph.graph0 sequence_graph)
(a : A n0) => inj (succ_seq A) n0 a ^+) m
o A _f p ==
(fun (n0 : Graph.graph0 sequence_graph)
(a : A n0) => inj (succ_seq A) n0 a ^+) n
|} == idmap
A: Sequence
foralln : Graph.graph0 sequence_graph,
(funx : Colimit A =>
colim_succ_seq_to_colim_seq A
(Colimit_rec (Colimit (succ_seq A))
{|
legs :=
fun (n0 : Graph.graph0 sequence_graph)
(a : A n0) => inj (succ_seq A) n0 a ^+;
legs_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m) =>
(funa : A n0 =>
match
p as p0 in (_ = n1)
return
(inj (succ_seq A) n1 ((A _f p0) a) ^+ =
inj (succ_seq A) n0 a ^+)
with
| 1 => glue (succ_seq A) n0 a ^+
end)
:
(fun (n1 : Graph.graph0 sequence_graph)
(a : A n1) => inj (succ_seq A) n1 a ^+) m
o A _f p ==
(fun (n1 : Graph.graph0 sequence_graph)
(a : A n1) => inj (succ_seq A) n1 a ^+)
n0
|} x)) o inj A n == idmap o inj A n
A: Sequence
forall (n : Graph.graph0 sequence_graph) (a : A n),
ap
(funx : Colimit A =>
colim_succ_seq_to_colim_seq A
(Colimit_rec (Colimit (succ_seq A))
{|
legs :=
fun (n0 : Graph.graph0 sequence_graph)
(a0 : A n0) => inj (succ_seq A) n0 a0 ^+;
legs_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m)
=>
(funa0 : A n0 =>
match
p as p0 in (_ = n1)
return
(inj (succ_seq A) n1 ((...) a0) ^+ =
inj (succ_seq A) n0 a0 ^+)
with
| 1 => glue (succ_seq A) n0 a0 ^+
end)
:
(fun (n1 : Graph.graph0 sequence_graph)
(a0 : A n1) =>
inj (succ_seq A) n1 a0 ^+) m o A _f p ==
(fun (n1 : Graph.graph0 sequence_graph)
(a0 : A n1) =>
inj (succ_seq A) n1 a0 ^+) n0
|} x)) (glue A n a) @ ?h n a =
?h n.+1 a ^+ @ ap idmap (glue A n a)
A: Sequence
foralln : Graph.graph0 sequence_graph,
(funx : Colimit A =>
colim_succ_seq_to_colim_seq A
(Colimit_rec (Colimit (succ_seq A))
{|
legs :=
fun (n0 : Graph.graph0 sequence_graph)
(a : A n0) => inj (succ_seq A) n0 a ^+;
legs_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m) =>
(funa : A n0 =>
match
p as p0 in (_ = n1)
return
(inj (succ_seq A) n1 ((A _f p0) a) ^+ =
inj (succ_seq A) n0 a ^+)
with
| 1 => glue (succ_seq A) n0 a ^+
end)
:
(fun (n1 : Graph.graph0 sequence_graph)
(a : A n1) => inj (succ_seq A) n1 a ^+) m
o A _f p ==
(fun (n1 : Graph.graph0 sequence_graph)
(a : A n1) => inj (succ_seq A) n1 a ^+)
n0
|} x)) o inj A n == idmap o inj A n
exact (funna => glue _ n a).
A: Sequence
forall (n : Graph.graph0 sequence_graph) (a : A n),
ap
(funx : Colimit A =>
colim_succ_seq_to_colim_seq A
(Colimit_rec (Colimit (succ_seq A))
{|
legs :=
fun (n0 : Graph.graph0 sequence_graph)
(a0 : A n0) => inj (succ_seq A) n0 a0 ^+;
legs_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m)
=>
(funa0 : A n0 =>
match
p as p0 in (_ = n1)
return
(inj (succ_seq A) n1 ((...) a0) ^+ =
inj (succ_seq A) n0 a0 ^+)
with
| 1 => glue (succ_seq A) n0 a0 ^+
end)
:
(fun (n1 : Graph.graph0 sequence_graph)
(a0 : A n1) =>
inj (succ_seq A) n1 a0 ^+) m o A _f p ==
(fun (n1 : Graph.graph0 sequence_graph)
(a0 : A n1) =>
inj (succ_seq A) n1 a0 ^+) n0
|} x)) (glue A n a) @
(fun (n0 : Graph.graph0 sequence_graph) (a0 : A n0) =>
glue A n0 a0) n a =
(fun (n0 : Graph.graph0 sequence_graph) (a0 : A n0) =>
glue A n0 a0) n.+1 a ^+ @ ap idmap (glue A n a)
A: Sequence n: Graph.graph0 sequence_graph a: A n
ap (colim_succ_seq_to_colim_seq A)
(legs_comm
{|
legs :=
fun (n : Graph.graph0 sequence_graph)
(a : A n) => inj (succ_seq A) n a ^+;
legs_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m)
(a : A n) =>
match
p as p0 in (_ = n0)
return
(inj (succ_seq A) n0 ((A _f p0) a) ^+ =
inj (succ_seq A) n a ^+)
with
| 1 => colimp n n.+11 a ^+
end
|} n n.+11 a) @ colimp n n.+11 a =
colimp n.+1 n.+21 a ^+ @ colimp n n.+11 a
Colimit_rec (Colimit (succ_seq A))
{|
legs :=
fun (n : Graph.graph0 sequence_graph) (a : A n)
=> inj (succ_seq A) n a ^+;
legs_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m) =>
(funa : A n =>
match
p as p0 in (_ = n0)
return
(inj (succ_seq A) n0 ((A _f p0) a) ^+ =
inj (succ_seq A) n a ^+)
with
| 1 => glue (succ_seq A) n a ^+
end)
:
(fun (n0 : Graph.graph0 sequence_graph)
(a : A n0) => inj (succ_seq A) n0 a ^+) m
o A _f p ==
(fun (n0 : Graph.graph0 sequence_graph)
(a : A n0) => inj (succ_seq A) n0 a ^+) n
|} o colim_succ_seq_to_colim_seq A == idmap
A: Sequence
foralln : Graph.graph0 sequence_graph,
(funx : Colimit (succ_seq A) =>
Colimit_rec (Colimit (succ_seq A))
{|
legs :=
fun (n0 : Graph.graph0 sequence_graph)
(a : A n0) => inj (succ_seq A) n0 a ^+;
legs_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m) =>
(funa : A n0 =>
match
p as p0 in (_ = n1)
return
(inj (succ_seq A) n1 ((A _f p0) a) ^+ =
inj (succ_seq A) n0 a ^+)
with
| 1 => glue (succ_seq A) n0 a ^+
end)
:
(fun (n1 : Graph.graph0 sequence_graph)
(a : A n1) => inj (succ_seq A) n1 a ^+) m
o A _f p ==
(fun (n1 : Graph.graph0 sequence_graph)
(a : A n1) => inj (succ_seq A) n1 a ^+) n0
|} (colim_succ_seq_to_colim_seq A x))
o inj (succ_seq A) n == idmap o inj (succ_seq A) n
A: Sequence
forall (n : Graph.graph0 sequence_graph)
(a : succ_seq A n),
ap
(funx : Colimit (succ_seq A) =>
Colimit_rec (Colimit (succ_seq A))
{|
legs :=
fun (n0 : Graph.graph0 sequence_graph)
(a0 : A n0) => inj (succ_seq A) n0 a0 ^+;
legs_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m) =>
(funa0 : A n0 =>
match
p as p0 in (_ = n1)
return
(inj (succ_seq A) n1 ((A _f p0) a0) ^+ =
inj (succ_seq A) n0 a0 ^+)
with
| 1 => glue (succ_seq A) n0 a0 ^+
end)
:
(fun (n1 : Graph.graph0 sequence_graph)
(a0 : A n1) => inj (succ_seq A) n1 a0 ^+)
m o A _f p ==
(fun (n1 : Graph.graph0 sequence_graph)
(a0 : A n1) => inj (succ_seq A) n1 a0 ^+)
n0
|} (colim_succ_seq_to_colim_seq A x))
(glue (succ_seq A) n a) @ ?h n a =
?h n.+1 a ^+ @ ap idmap (glue (succ_seq A) n a)
A: Sequence
foralln : Graph.graph0 sequence_graph,
(funx : Colimit (succ_seq A) =>
Colimit_rec (Colimit (succ_seq A))
{|
legs :=
fun (n0 : Graph.graph0 sequence_graph)
(a : A n0) => inj (succ_seq A) n0 a ^+;
legs_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m) =>
(funa : A n0 =>
match
p as p0 in (_ = n1)
return
(inj (succ_seq A) n1 ((A _f p0) a) ^+ =
inj (succ_seq A) n0 a ^+)
with
| 1 => glue (succ_seq A) n0 a ^+
end)
:
(fun (n1 : Graph.graph0 sequence_graph)
(a : A n1) => inj (succ_seq A) n1 a ^+) m
o A _f p ==
(fun (n1 : Graph.graph0 sequence_graph)
(a : A n1) => inj (succ_seq A) n1 a ^+) n0
|} (colim_succ_seq_to_colim_seq A x))
o inj (succ_seq A) n == idmap o inj (succ_seq A) n
exact (funna => glue _ n a).
A: Sequence
forall (n : Graph.graph0 sequence_graph)
(a : succ_seq A n),
ap
(funx : Colimit (succ_seq A) =>
Colimit_rec (Colimit (succ_seq A))
{|
legs :=
fun (n0 : Graph.graph0 sequence_graph)
(a0 : A n0) => inj (succ_seq A) n0 a0 ^+;
legs_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m) =>
(funa0 : A n0 =>
match
p as p0 in (_ = n1)
return
(inj (succ_seq A) n1 ((A _f p0) a0) ^+ =
inj (succ_seq A) n0 a0 ^+)
with
| 1 => glue (succ_seq A) n0 a0 ^+
end)
:
(fun (n1 : Graph.graph0 sequence_graph)
(a0 : A n1) => inj (succ_seq A) n1 a0 ^+)
m o A _f p ==
(fun (n1 : Graph.graph0 sequence_graph)
(a0 : A n1) => inj (succ_seq A) n1 a0 ^+)
n0
|} (colim_succ_seq_to_colim_seq A x))
(glue (succ_seq A) n a) @
(fun (n0 : Graph.graph0 sequence_graph)
(a0 : succ_seq A n0) => glue (succ_seq A) n0 a0) n
a =
(fun (n0 : Graph.graph0 sequence_graph)
(a0 : succ_seq A n0) => glue (succ_seq A) n0 a0)
n.+1 a ^+ @ ap idmap (glue (succ_seq A) n a)
A: Sequence n: Graph.graph0 sequence_graph a: succ_seq A n
ap
(Colimit_rec (Colimit (succ_seq A))
{|
legs :=
fun (n : Graph.graph0 sequence_graph)
(a : A n) => inj (succ_seq A) n a ^+;
legs_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m)
(a : A n) =>
match
p as p0 in (_ = n0)
return
(inj (succ_seq A) n0 ((A _f p0) a) ^+ =
inj (succ_seq A) n a ^+)
with
| 1 => colimp n n.+11 a ^+
end
|})
(legs_comm
{|
legs :=
fun (n : Graph.graph0 sequence_graph)
(a : succ_seq A n) => inj A n.+1 a;
legs_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m) =>
match
p as p0 in (_ = n0)
return
((funx : succ_seq A n =>
inj A n0.+1 (((succ_seq A) _f p0) x)) ==
(funa : succ_seq A n => inj A n.+1 a))
with
| 1 => colimp n.+1 n.+21end
|} n n.+11 a) @ colimp n n.+11 a =
colimp n.+1 n.+21 a ^+ @ colimp n n.+11 a
rewrite (@Colimit_rec_beta_colimp _ A _ _ _ _ 1); reflexivity.Defined.Definitionequiv_colim_succ_seq_to_colim_seqA : Colimit (succ_seq A) <~> Colimit A
:= Build_Equiv _ _ (colim_succ_seq_to_colim_seq A) _.(** The canonical equivalence between the colimit of the shifted sequence and the colimit of the original sequence; Lemma 3.6. *)
A: Sequence n: nat
Colimit (shift_seq A n) -> Colimit A
A: Sequence n: nat
Colimit (shift_seq A n) -> Colimit A
A: Sequence n: nat
foralli : Graph.graph0 sequence_graph,
shift_seq A n i -> Colimit A
A: Sequence n: nat
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
?legs j o (shift_seq A n) _f g == ?legs i
A: Sequence n: nat
foralli : Graph.graph0 sequence_graph,
shift_seq A n i -> Colimit A
exact (funka => inj A (k+n)%nat a).
A: Sequence n: nat
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
(fun (k : Graph.graph0 sequence_graph)
(a : shift_seq A n k) => inj A (k + n) a) j
o (shift_seq A n) _f g ==
(fun (k : Graph.graph0 sequence_graph)
(a : shift_seq A n k) => inj A (k + n) a) i
intros k l p; destruct p; exact (glue A (k+n)%nat).Defined.
A: Sequence n: nat k: Graph.graph0 sequence_graph a: shift_seq A n k
ap (colim_shift_seq_to_colim_seq A n)
(glue (shift_seq A n) k a) = glue A (k + n) a
A: Sequence n: nat k: Graph.graph0 sequence_graph a: shift_seq A n k
ap (colim_shift_seq_to_colim_seq A n)
(glue (shift_seq A n) k a) = glue A (k + n) a
srapply Colimit_rec_beta_colimp.Defined.
A: Sequence n: nat k: Graph.graph0 sequence_graph a1, a2: shift_seq A n k p: a1 = a2
ap (colim_shift_seq_to_colim_seq A n)
(ap (inj (shift_seq A n) k) p) =
ap (inj A (k + n)) p
A: Sequence n: nat k: Graph.graph0 sequence_graph a1, a2: shift_seq A n k p: a1 = a2
ap (colim_shift_seq_to_colim_seq A n)
(ap (inj (shift_seq A n) k) p) =
ap (inj A (k + n)) p
destruct p; reflexivity.Defined.
X: Type Y: X -> Type Z: Type x1, x2: X y: Y x2 I: forallx : X, Y x -> Z p: x2 = x1
I x2 y = I x1 (coe (ap Y p) y)
X: Type Y: X -> Type Z: Type x1, x2: X y: Y x2 I: forallx : X, Y x -> Z p: x2 = x1
I x2 y = I x1 (coe (ap Y p) y)
destruct p; reflexivity.Defined.
X: Type Y: X -> Type x1, x2: X y: Y x1 F: X -> X G: forallx : X, Y x -> Y (F x) p: x1 = x2
G x2 (coe (ap Y p) y) = coe (ap Y (ap F p)) (G x1 y)
X: Type Y: X -> Type x1, x2: X y: Y x1 F: X -> X G: forallx : X, Y x -> Y (F x) p: x1 = x2
G x2 (coe (ap Y p) y) = coe (ap Y (ap F p)) (G x1 y)
destruct p; reflexivity.Defined.
X: Type Y: X -> Type Z: Type x1, x2: X y: Y x2 F: X -> X G: forallx : X, Y x -> Y (F x) I: forallx : X, Y x -> Z p: x2 = x1 Q: forall (x : X) (y : Y x), I (F x) (G x y) = I x y
Q x2 y @ J p =
J (ap F p) @
(ap (I (F x1)) (K F G p)^ @ Q x1 (coe (ap Y p) y))
X: Type Y: X -> Type Z: Type x1, x2: X y: Y x2 F: X -> X G: forallx : X, Y x -> Y (F x) I: forallx : X, Y x -> Z p: x2 = x1 Q: forall (x : X) (y : Y x), I (F x) (G x y) = I x y
Q x2 y @ J p =
J (ap F p) @
(ap (I (F x1)) (K F G p)^ @ Q x1 (coe (ap Y p) y))
X: Type Y: X -> Type Z: Type x2: X y: Y x2 F: X -> X G: forallx : X, Y x -> Y (F x) I: forallx : X, Y x -> Z Q: forall (x : X) (y : Y x), I (F x) (G x y) = I x y
Q x2 y @ 1 = 1 @ (1 @ Q x2 y)
X: Type Y: X -> Type Z: Type x2: X y: Y x2 F: X -> X G: forallx : X, Y x -> Y (F x) I: forallx : X, Y x -> Z Q: forall (x : X) (y : Y x), I (F x) (G x y) = I x y
foralli : Graph.graph0 sequence_graph,
shift_seq A 0 i -> A i
H: Funext A: Sequence
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j)
(x : shift_seq A 0 i),
(A _f g) (?DiagramMap_obj i x) =
?DiagramMap_obj j (((shift_seq A 0) _f g) x)
H: Funext A: Sequence
foralli : Graph.graph0 sequence_graph,
shift_seq A 0 i -> A i
exact (funk => coe (ap A (nat_add_zero_r k))).
H: Funext A: Sequence
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j)
(x : shift_seq A 0 i),
(A _f g)
((funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_zero_r k))) i x) =
(funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_zero_r k))) j
(((shift_seq A 0) _f g) x)
H: Funext A: Sequence k: Graph.graph0 sequence_graph a: shift_seq A 0 k
(equiv_path (A (k + 0)) (A k)
(ap A (nat_add_zero_r k)) a) ^+ =
equiv_path (A (k.+1 + 0)) (A k.+1)
(ap A (nat_add_zero_r k.+1)) a ^+
exact (K S (funna => a^+) _).
H: Funext A: Sequence
foralli : Graph.graph0 sequence_graph,
IsEquiv
({|
DiagramMap_obj :=
funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_zero_r k));
DiagramMap_comm :=
fun (kl : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k l)
(a : shift_seq A 0 k) =>
match
p as p0 in (_ = n)
return
((A _f p0)
(equiv_path (A (k + 0)) (A k)
(ap A (nat_add_zero_r k)) a) =
equiv_path (A (n + 0)) (A n)
(ap A (nat_add_zero_r n))
(((shift_seq A 0) _f p0) a))
with
| 1 =>
K S (fun (n : nat) (a0 : A n) => a0 ^+)
(nat_add_zero_r k)
end
|} i)
exact _.
H: Funext A: Sequence
equiv_functor_colimit
{|
diag_equiv_map :=
{|
DiagramMap_obj :=
funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_zero_r k));
DiagramMap_comm :=
fun (kl : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k l)
(a : shift_seq A 0 k) =>
match
p as p0 in (_ = n)
return
((A _f p0)
(equiv_path (A (k + 0)) (A k)
(ap A (nat_add_zero_r k)) a) =
equiv_path (A (n + 0)) (A n)
(ap A (nat_add_zero_r n))
(((shift_seq A 0) _f p0) a))
with
| 1 =>
K S (fun (n : nat) (a0 : A n) => a0 ^+)
(nat_add_zero_r k)
end
|};
diag_equiv_isequiv :=
funi : Graph.graph0 sequence_graph =>
equiv_isequiv
(equiv_path (A (i + 0)) (A i)
(ap A (nat_add_zero_r i)))
|} (iscolimit_colimit (shift_seq A 0))
(iscolimit_colimit A) ==
colim_shift_seq_to_colim_seq A 0
H: Funext A: Sequence
foralln : Graph.graph0 sequence_graph,
colim_shift_seq_to_colim_seq A 0
o inj (shift_seq A 0) n ==
equiv_functor_colimit
{|
diag_equiv_map :=
{|
DiagramMap_obj :=
funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_zero_r k));
DiagramMap_comm :=
fun (kl : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k l)
(a : shift_seq A 0 k) =>
match
p as p0 in (_ = n0)
return
((A _f p0)
(equiv_path (A (k + 0)) (A k)
(ap A (nat_add_zero_r k)) a) =
equiv_path (A (n0 + 0)) (A n0)
(ap A (nat_add_zero_r n0))
(((shift_seq A 0) _f p0) a))
with
| 1 =>
K S
(fun (n0 : nat) (a0 : A n0) => a0 ^+)
(nat_add_zero_r k)
end
|};
diag_equiv_isequiv :=
funi : Graph.graph0 sequence_graph =>
equiv_isequiv
(equiv_path (A (i + 0)) (A i)
(ap A (nat_add_zero_r i)))
|} (iscolimit_colimit (shift_seq A 0))
(iscolimit_colimit A) o inj (shift_seq A 0) n
H: Funext A: Sequence
forall (n : Graph.graph0 sequence_graph)
(a : shift_seq A 0 n),
ap (colim_shift_seq_to_colim_seq A 0)
(glue (shift_seq A 0) n a) @ ?h0 n a =
?h0 n.+1 a ^+ @
ap
(equiv_functor_colimit
{|
diag_equiv_map :=
{|
DiagramMap_obj :=
funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_zero_r k));
DiagramMap_comm :=
fun (kl : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k l)
(a0 : shift_seq A 0 k) =>
match
p as p0 in (_ = n0)
return
((A _f p0)
(equiv_path (A (k + 0)) (A k)
(ap A (nat_add_zero_r k)) a0) =
equiv_path (A (n0 + 0)) (A n0)
(ap A (nat_add_zero_r n0))
(((shift_seq A 0) _f p0) a0))
with
| 1 =>
K S
(fun (n0 : nat) (a1 : A n0) =>
a1 ^+) (nat_add_zero_r k)
end
|};
diag_equiv_isequiv :=
funi : Graph.graph0 sequence_graph =>
equiv_isequiv
(equiv_path (A (i + 0)) (A i)
(ap A (nat_add_zero_r i)))
|} (iscolimit_colimit (shift_seq A 0))
(iscolimit_colimit A)) (glue (shift_seq A 0) n a)
H: Funext A: Sequence
foralln : Graph.graph0 sequence_graph,
colim_shift_seq_to_colim_seq A 0
o inj (shift_seq A 0) n ==
equiv_functor_colimit
{|
diag_equiv_map :=
{|
DiagramMap_obj :=
funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_zero_r k));
DiagramMap_comm :=
fun (kl : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k l)
(a : shift_seq A 0 k) =>
match
p as p0 in (_ = n0)
return
((A _f p0)
(equiv_path (A (k + 0)) (A k)
(ap A (nat_add_zero_r k)) a) =
equiv_path (A (n0 + 0)) (A n0)
(ap A (nat_add_zero_r n0))
(((shift_seq A 0) _f p0) a))
with
| 1 =>
K S
(fun (n0 : nat) (a0 : A n0) => a0 ^+)
(nat_add_zero_r k)
end
|};
diag_equiv_isequiv :=
funi : Graph.graph0 sequence_graph =>
equiv_isequiv
(equiv_path (A (i + 0)) (A i)
(ap A (nat_add_zero_r i)))
|} (iscolimit_colimit (shift_seq A 0))
(iscolimit_colimit A) o inj (shift_seq A 0) n
intros k a; exact (J (nat_add_zero_r k)).
H: Funext A: Sequence
forall (n : Graph.graph0 sequence_graph)
(a : shift_seq A 0 n),
ap (colim_shift_seq_to_colim_seq A 0)
(glue (shift_seq A 0) n a) @
(funk : Graph.graph0 sequence_graph =>
(funa0 : shift_seq A 0 k => J (nat_add_zero_r k))
:
colim_shift_seq_to_colim_seq A 0
o inj (shift_seq A 0) k ==
equiv_functor_colimit
{|
diag_equiv_map :=
{|
DiagramMap_obj :=
funk0 : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_zero_r k0));
DiagramMap_comm :=
fun (k0l : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k0 l)
(a0 : shift_seq A 0 k0) =>
match
p as p0 in (_ = n0)
return
((A _f p0)
(equiv_path (...) (...) (...) a0) =
equiv_path (A (...)) (A n0)
(ap A (...)) ((...) a0))
with
| 1 =>
K S
(fun (n0 : nat) (a1 : A n0) => a1 ^+)
(nat_add_zero_r k0)
end
|};
diag_equiv_isequiv :=
funi : Graph.graph0 sequence_graph =>
equiv_isequiv
(equiv_path (A (i + 0)) (A i)
(ap A (nat_add_zero_r i)))
|} (iscolimit_colimit (shift_seq A 0))
(iscolimit_colimit A) o inj (shift_seq A 0) k) n a =
(funk : Graph.graph0 sequence_graph =>
(funa0 : shift_seq A 0 k => J (nat_add_zero_r k))
:
colim_shift_seq_to_colim_seq A 0
o inj (shift_seq A 0) k ==
equiv_functor_colimit
{|
diag_equiv_map :=
{|
DiagramMap_obj :=
funk0 : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_zero_r k0));
DiagramMap_comm :=
fun (k0l : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k0 l)
(a0 : shift_seq A 0 k0) =>
match
p as p0 in (_ = n0)
return
((A _f p0)
(equiv_path (...) (...) (...) a0) =
equiv_path (A (...)) (A n0)
(ap A (...)) ((...) a0))
with
| 1 =>
K S
(fun (n0 : nat) (a1 : A n0) => a1 ^+)
(nat_add_zero_r k0)
end
|};
diag_equiv_isequiv :=
funi : Graph.graph0 sequence_graph =>
equiv_isequiv
(equiv_path (A (i + 0)) (A i)
(ap A (nat_add_zero_r i)))
|} (iscolimit_colimit (shift_seq A 0))
(iscolimit_colimit A) o inj (shift_seq A 0) k) n.+1
a ^+ @
ap
(equiv_functor_colimit
{|
diag_equiv_map :=
{|
DiagramMap_obj :=
funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_zero_r k));
DiagramMap_comm :=
fun (kl : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k l)
(a0 : shift_seq A 0 k) =>
match
p as p0 in (_ = n0)
return
((A _f p0)
(equiv_path (A (k + 0)) (A k)
(ap A (nat_add_zero_r k)) a0) =
equiv_path (A (n0 + 0)) (A n0)
(ap A (nat_add_zero_r n0))
(((shift_seq A 0) _f p0) a0))
with
| 1 =>
K S
(fun (n0 : nat) (a1 : A n0) =>
a1 ^+) (nat_add_zero_r k)
end
|};
diag_equiv_isequiv :=
funi : Graph.graph0 sequence_graph =>
equiv_isequiv
(equiv_path (A (i + 0)) (A i)
(ap A (nat_add_zero_r i)))
|} (iscolimit_colimit (shift_seq A 0))
(iscolimit_colimit A)) (glue (shift_seq A 0) n a)
intros k a; rewrite !Colimit_rec_beta_colimp; exact (L (glue A)).
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j)
(x : shift_seq A n.+1 i),
((succ_seq (shift_seq A n)) _f g)
((funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_succ_r k n))) i x) =
(funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_succ_r k n))) j
(((shift_seq A n.+1) _f g) x)
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j)
(x : shift_seq A n.+1 i),
((succ_seq (shift_seq A n)) _f g)
((funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_succ_r k n))) i x) =
(funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_succ_r k n))) j
(((shift_seq A n.+1) _f g) x)
intros k l p a; destruct p; rapply (K S (funna => a^+) (nat_add_succ_r k n)).}
foralli : Graph.graph0 sequence_graph,
IsEquiv
({|
DiagramMap_obj :=
funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_succ_r k n));
DiagramMap_comm :=
fun (kl : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k l)
(a : shift_seq A n.+1 k) =>
match
p as p0 in (_ = n0)
return
(((succ_seq (shift_seq A n)) _f p0)
(equiv_path (A (k + n.+1))
(A (k + n).+1)
(ap A (nat_add_succ_r k n)) a) =
equiv_path (A (n0 + n.+1)) (A (n0 + n).+1)
(ap A (nat_add_succ_r n0 n))
(((shift_seq A n.+1) _f p0) a))
with
| 1 =>
K S (fun (n : nat) (a0 : A n) => a0 ^+)
(nat_add_succ_r k n)
end
|} i)
(fun (xyz : Type) (f : x <~> y) (g : y <~> z) =>
equiv_compose g f) (Colimit (shift_seq A n.+1))
(Colimit (succ_seq (shift_seq A n))) (Colimit A)
(equiv_functor_colimit
{|
diag_equiv_map :=
{|
DiagramMap_obj :=
funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_succ_r k n));
DiagramMap_comm :=
fun (kl : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k l)
(a : shift_seq A n.+1 k) =>
match
p as p0 in (_ = n0)
return
(((succ_seq (shift_seq A n)) _f p0)
(equiv_path (A (k + n.+1))
(A (k + n).+1)
(ap A (nat_add_succ_r k n)) a) =
equiv_path (A (n0 + n.+1))
(A (n0 + n).+1)
(ap A (nat_add_succ_r n0 n))
(((shift_seq A n.+1) _f p0) a))
with
| 1 =>
K S
(fun (n : nat) (a0 : A n) => a0 ^+)
(nat_add_succ_r k n)
end
|};
diag_equiv_isequiv :=
funi : Graph.graph0 sequence_graph =>
equiv_isequiv
(equiv_path (A (i + n.+1)) (A (i + n).+1)
(ap A (nat_add_succ_r i n)))
|} (iscolimit_colimit (shift_seq A n.+1))
(iscolimit_colimit (succ_seq (shift_seq A n))))
(transitivity
(equiv_colim_succ_seq_to_colim_seq
(shift_seq A n))
{|
equiv_fun := colim_shift_seq_to_colim_seq A n;
equiv_isequiv := e
|}) == colim_shift_seq_to_colim_seq A n.+1
foralln0 : Graph.graph0 sequence_graph,
colim_shift_seq_to_colim_seq A n.+1
o inj (shift_seq A n.+1) n0 ==
(fun (xyz : Type) (f : x <~> y) (g : y <~> z) =>
equiv_compose g f) (Colimit (shift_seq A n.+1))
(Colimit (succ_seq (shift_seq A n))) (Colimit A)
(equiv_functor_colimit
{|
diag_equiv_map :=
{|
DiagramMap_obj :=
funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_succ_r k n));
DiagramMap_comm :=
fun (kl : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k l)
(a : shift_seq A n.+1 k) =>
match
p as p0 in (_ = n1)
return
(((succ_seq (shift_seq A n)) _f p0)
(equiv_path (A (k + n.+1))
(A (k + n).+1)
(ap A (nat_add_succ_r k n)) a) =
equiv_path (A (n1 + n.+1))
(A (n1 + n).+1)
(ap A (nat_add_succ_r n1 n))
(((shift_seq A n.+1) _f p0) a))
with
| 1 =>
K S
(fun (n : nat) (a0 : A n) => a0 ^+)
(nat_add_succ_r k n)
end
|};
diag_equiv_isequiv :=
funi : Graph.graph0 sequence_graph =>
equiv_isequiv
(equiv_path (A (i + n.+1)) (A (i + n).+1)
(ap A (nat_add_succ_r i n)))
|} (iscolimit_colimit (shift_seq A n.+1))
(iscolimit_colimit (succ_seq (shift_seq A n))))
(transitivity
(equiv_colim_succ_seq_to_colim_seq
(shift_seq A n))
{|
equiv_fun := colim_shift_seq_to_colim_seq A n;
equiv_isequiv := e
|}) o inj (shift_seq A n.+1) n0
forall (n0 : Graph.graph0 sequence_graph)
(a : shift_seq A n.+1 n0),
ap (colim_shift_seq_to_colim_seq A n.+1)
(glue (shift_seq A n.+1) n0 a) @ ?h n0 a =
?h n0.+1 a ^+ @
ap
((fun (xyz : Type) (f : x <~> y) (g : y <~> z) =>
equiv_compose g f) (Colimit (shift_seq A n.+1))
(Colimit (succ_seq (shift_seq A n))) (Colimit A)
(equiv_functor_colimit
{|
diag_equiv_map :=
{|
DiagramMap_obj :=
funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_succ_r k n));
DiagramMap_comm :=
fun
(kl : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k l)
(a0 : shift_seq A n.+1 k) =>
match
p as p0 in (_ = n1)
return
(((succ_seq (...)) _f p0)
(equiv_path (A (...))
(A (...).+1) (ap A (...)) a0) =
equiv_path (A (n1 + n.+1))
(A (n1 + n).+1)
(ap A (nat_add_succ_r n1 n))
(((...) _f p0) a0))
with
| 1 =>
K S
(fun (n : nat) (a1 : A n) =>
a1 ^+) (nat_add_succ_r k n)
end
|};
diag_equiv_isequiv :=
funi : Graph.graph0 sequence_graph =>
equiv_isequiv
(equiv_path (A (i + n.+1))
(A (i + n).+1)
(ap A (nat_add_succ_r i n)))
|} (iscolimit_colimit (shift_seq A n.+1))
(iscolimit_colimit (succ_seq (shift_seq A n))))
(transitivity
(equiv_colim_succ_seq_to_colim_seq
(shift_seq A n))
{|
equiv_fun :=
colim_shift_seq_to_colim_seq A n;
equiv_isequiv := e
|})) (glue (shift_seq A n.+1) n0 a)
foralln0 : Graph.graph0 sequence_graph,
colim_shift_seq_to_colim_seq A n.+1
o inj (shift_seq A n.+1) n0 ==
(fun (xyz : Type) (f : x <~> y) (g : y <~> z) =>
equiv_compose g f) (Colimit (shift_seq A n.+1))
(Colimit (succ_seq (shift_seq A n))) (Colimit A)
(equiv_functor_colimit
{|
diag_equiv_map :=
{|
DiagramMap_obj :=
funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_succ_r k n));
DiagramMap_comm :=
fun (kl : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k l)
(a : shift_seq A n.+1 k) =>
match
p as p0 in (_ = n1)
return
(((succ_seq (shift_seq A n)) _f p0)
(equiv_path (A (k + n.+1))
(A (k + n).+1)
(ap A (nat_add_succ_r k n)) a) =
equiv_path (A (n1 + n.+1))
(A (n1 + n).+1)
(ap A (nat_add_succ_r n1 n))
(((shift_seq A n.+1) _f p0) a))
with
| 1 =>
K S
(fun (n : nat) (a0 : A n) => a0 ^+)
(nat_add_succ_r k n)
end
|};
diag_equiv_isequiv :=
funi : Graph.graph0 sequence_graph =>
equiv_isequiv
(equiv_path (A (i + n.+1)) (A (i + n).+1)
(ap A (nat_add_succ_r i n)))
|} (iscolimit_colimit (shift_seq A n.+1))
(iscolimit_colimit (succ_seq (shift_seq A n))))
(transitivity
(equiv_colim_succ_seq_to_colim_seq
(shift_seq A n))
{|
equiv_fun := colim_shift_seq_to_colim_seq A n;
equiv_isequiv := e
|}) o inj (shift_seq A n.+1) n0
forall (n0 : Graph.graph0 sequence_graph)
(a : shift_seq A n.+1 n0),
ap (colim_shift_seq_to_colim_seq A n.+1)
(glue (shift_seq A n.+1) n0 a) @
(funk : Graph.graph0 sequence_graph =>
(funa0 : shift_seq A n.+1 k =>
J (nat_add_succ_r k n))
:
colim_shift_seq_to_colim_seq A n.+1
o inj (shift_seq A n.+1) k ==
(fun (xyz : Type) (f : x <~> y) (g : y <~> z) =>
equiv_compose g f) (Colimit (shift_seq A n.+1))
(Colimit (succ_seq (shift_seq A n))) (Colimit A)
(equiv_functor_colimit
{|
diag_equiv_map :=
{|
DiagramMap_obj :=
funk0 : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_succ_r k0 n));
DiagramMap_comm :=
fun (k0l : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k0 l)
(a0 : shift_seq A n.+1 k0) =>
match
p as p0 in (_ = n1)
return
((...) (...) =
equiv_path (...) (...) (...) (...))
with
| 1 =>
K S
(fun (n : nat) (a1 : A n) => a1 ^+)
(nat_add_succ_r k0 n)
end
|};
diag_equiv_isequiv :=
funi : Graph.graph0 sequence_graph =>
equiv_isequiv
(equiv_path (A (i + n.+1)) (A (i + n).+1)
(ap A (nat_add_succ_r i n)))
|} (iscolimit_colimit (shift_seq A n.+1))
(iscolimit_colimit (succ_seq (shift_seq A n))))
(transitivity
(equiv_colim_succ_seq_to_colim_seq
(shift_seq A n))
{|
equiv_fun := colim_shift_seq_to_colim_seq A n;
equiv_isequiv := e
|}) o inj (shift_seq A n.+1) k) n0 a =
(funk : Graph.graph0 sequence_graph =>
(funa0 : shift_seq A n.+1 k =>
J (nat_add_succ_r k n))
:
colim_shift_seq_to_colim_seq A n.+1
o inj (shift_seq A n.+1) k ==
(fun (xyz : Type) (f : x <~> y) (g : y <~> z) =>
equiv_compose g f) (Colimit (shift_seq A n.+1))
(Colimit (succ_seq (shift_seq A n))) (Colimit A)
(equiv_functor_colimit
{|
diag_equiv_map :=
{|
DiagramMap_obj :=
funk0 : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_succ_r k0 n));
DiagramMap_comm :=
fun (k0l : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k0 l)
(a0 : shift_seq A n.+1 k0) =>
match
p as p0 in (_ = n1)
return
((...) (...) =
equiv_path (...) (...) (...) (...))
with
| 1 =>
K S
(fun (n : nat) (a1 : A n) => a1 ^+)
(nat_add_succ_r k0 n)
end
|};
diag_equiv_isequiv :=
funi : Graph.graph0 sequence_graph =>
equiv_isequiv
(equiv_path (A (i + n.+1)) (A (i + n).+1)
(ap A (nat_add_succ_r i n)))
|} (iscolimit_colimit (shift_seq A n.+1))
(iscolimit_colimit (succ_seq (shift_seq A n))))
(transitivity
(equiv_colim_succ_seq_to_colim_seq
(shift_seq A n))
{|
equiv_fun := colim_shift_seq_to_colim_seq A n;
equiv_isequiv := e
|}) o inj (shift_seq A n.+1) k) n0.+1 a ^+ @
ap
((fun (xyz : Type) (f : x <~> y) (g : y <~> z) =>
equiv_compose g f) (Colimit (shift_seq A n.+1))
(Colimit (succ_seq (shift_seq A n))) (Colimit A)
(equiv_functor_colimit
{|
diag_equiv_map :=
{|
DiagramMap_obj :=
funk : Graph.graph0 sequence_graph =>
coe (ap A (nat_add_succ_r k n));
DiagramMap_comm :=
fun
(kl : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph k l)
(a0 : shift_seq A n.+1 k) =>
match
p as p0 in (_ = n1)
return
(((succ_seq (...)) _f p0)
(equiv_path (A (...))
(A (...).+1) (ap A (...)) a0) =
equiv_path (A (n1 + n.+1))
(A (n1 + n).+1)
(ap A (nat_add_succ_r n1 n))
(((...) _f p0) a0))
with
| 1 =>
K S
(fun (n : nat) (a1 : A n) =>
a1 ^+) (nat_add_succ_r k n)
end
|};
diag_equiv_isequiv :=
funi : Graph.graph0 sequence_graph =>
equiv_isequiv
(equiv_path (A (i + n.+1))
(A (i + n).+1)
(ap A (nat_add_succ_r i n)))
|} (iscolimit_colimit (shift_seq A n.+1))
(iscolimit_colimit (succ_seq (shift_seq A n))))
(transitivity
(equiv_colim_succ_seq_to_colim_seq
(shift_seq A n))
{|
equiv_fun :=
colim_shift_seq_to_colim_seq A n;
equiv_isequiv := e
|})) (glue (shift_seq A n.+1) n0 a)
H: Funext A: Sequence n: nat e: IsEquiv (colim_shift_seq_to_colim_seq A n) k: Graph.graph0 sequence_graph a: shift_seq A n.+1 k
colimp (k + n.+1) (k + n.+1).+11 a @
J (nat_add_succ_r k n) =
J (ap S (nat_add_succ_r k n)) @
ap
(funx : Colimit (shift_seq A n.+1) =>
colim_shift_seq_to_colim_seq A n
(colim_succ_seq_to_colim_seq (shift_seq A n)
(functor_colimit
{|
DiagramMap_obj :=
funk : nat =>
transport idmap
(ap A (nat_add_succ_r k n));
DiagramMap_comm :=
fun (kl : nat) (p : k.+1 = l)
(a : A (k + n.+1)) =>
match
p as p0 in (_ = n0)
return
(match
p0 in (_ = n1)
return (... -> ...)
with
| 1 => funa0 : A ....+1 => a0 ^+
end
(transport idmap
(ap A (nat_add_succ_r k n)) a) =
transport idmap
(ap A (nat_add_succ_r n0 n))
(match p0 in ... return ... with
| 1 => fun ... => a0 ^+
end a))
with
| 1 =>
K S
(fun (n : nat) (a0 : A n) =>
a0 ^+) (nat_add_succ_r k n)
end
|} (iscolimit_colimit (shift_seq A n.+1))
(iscolimit_colimit
(succ_seq (shift_seq A n))) x)))
(colimp k k.+11 a)
H: Funext A: Sequence n: nat e: IsEquiv (colim_shift_seq_to_colim_seq A n) k: Graph.graph0 sequence_graph a: shift_seq A n.+1 k
colimp (k + n.+1) (k + n.+1).+11 a @
J (nat_add_succ_r k n) =
J (ap S (nat_add_succ_r k n)) @
(ap (colim_shift_seq_to_colim_seq A n)
(ap (colim_succ_seq_to_colim_seq (shift_seq A n))
(ap
(iscolimit_colimit (succ_seq (shift_seq A n))
k.+1)
(DiagramMap_comm
{|
DiagramMap_obj :=
funk : nat =>
transport idmap
(ap A (nat_add_succ_r k n));
DiagramMap_comm :=
fun (kl : nat) (p : k.+1 = l)
(a : A (k + n.+1)) =>
match
p as p0 in (_ = n0)
return
(match
p0 in (...) return (...)
with
| 1 => funa0 : ... => a0 ^+
end
(transport idmap (ap A (...)) a) =
transport idmap
(ap A (nat_add_succ_r n0 n))
(match ... ... with
| ... => ... => ...
end a))
with
| 1 =>
K S
(fun (n : nat) (a0 : A n) =>
a0 ^+) (nat_add_succ_r k n)
end
|} 1 a)^)) @
ap (colim_shift_seq_to_colim_seq A n)
(ap (colim_succ_seq_to_colim_seq (shift_seq A n))
(legs_comm
(iscolimit_colimit (succ_seq (shift_seq A n)))
k k.+11
({|
DiagramMap_obj :=
funk : nat =>
transport idmap
(ap A (nat_add_succ_r k n));
DiagramMap_comm :=
fun (kl : nat) (p : k.+1 = l)
(a : A (k + n.+1)) =>
match
p as p0 in (_ = n0)
return
(match p0 in (...) return (...) with
| 1 => funa0 : ... => a0 ^+
end
(transport idmap (ap A (...)) a) =
transport idmap
(ap A (nat_add_succ_r n0 n))
(match ... ... with
| ... => ... => ...
end a))
with
| 1 =>
K S
(fun (n : nat) (a0 : A n) => a0 ^+)
(nat_add_succ_r k n)
end
|} k a))))
H: Funext A: Sequence n: nat e: IsEquiv (colim_shift_seq_to_colim_seq A n) k: Graph.graph0 sequence_graph a: shift_seq A n.+1 k
colimp (k + n.+1) (k + n.+1).+11 a @
J (nat_add_succ_r k n) =
J (ap S (nat_add_succ_r k n)) @
(ap (inj A (k.+2 + n))
(DiagramMap_comm
{|
DiagramMap_obj :=
funk : nat =>
transport idmap (ap A (nat_add_succ_r k n));
DiagramMap_comm :=
fun (kl : nat) (p : k.+1 = l)
(a : A (k + n.+1)) =>
match
p as p0 in (_ = n0)
return
(match
p0 in (_ = n1)
return
(A (k + n).+1 -> A (n1 + n).+1)
with
| 1 => funa0 : A (k + n).+1 => a0 ^+
end
(transport idmap
(ap A (nat_add_succ_r k n)) a) =
transport idmap
(ap A (nat_add_succ_r n0 n))
(match
p0 in (_ = n1)
return (A ... -> A ...)
with
| 1 => funa0 : A (...) => a0 ^+
end a))
with
| 1 =>
K S (fun (n : nat) (a0 : A n) => a0 ^+)
(nat_add_succ_r k n)
end
|} 1 a)^ @
ap (colim_shift_seq_to_colim_seq A n)
(ap (colim_succ_seq_to_colim_seq (shift_seq A n))
(legs_comm
(iscolimit_colimit (succ_seq (shift_seq A n)))
k k.+11
({|
DiagramMap_obj :=
funk : nat =>
transport idmap
(ap A (nat_add_succ_r k n));
DiagramMap_comm :=
fun (kl : nat) (p : k.+1 = l)
(a : A (k + n.+1)) =>
match
p as p0 in (_ = n0)
return
(match p0 in (...) return (...) with
| 1 => funa0 : ... => a0 ^+
end
(transport idmap (ap A (...)) a) =
transport idmap
(ap A (nat_add_succ_r n0 n))
(match ... ... with
| ... => ... => ...
end a))
with
| 1 =>
K S
(fun (n : nat) (a0 : A n) => a0 ^+)
(nat_add_succ_r k n)
end
|} k a))))
H: Funext A: Sequence n: nat e: IsEquiv (colim_shift_seq_to_colim_seq A n) k: Graph.graph0 sequence_graph a: shift_seq A n.+1 k
colimp (k + n.+1) (k + n.+1).+11 a @
J (nat_add_succ_r k n) =
J (ap S (nat_add_succ_r k n)) @
(ap (inj A (k.+2 + n))
(DiagramMap_comm
{|
DiagramMap_obj :=
funk : nat =>
transport idmap (ap A (nat_add_succ_r k n));
DiagramMap_comm :=
fun (kl : nat) (p : k.+1 = l)
(a : A (k + n.+1)) =>
match
p as p0 in (_ = n0)
return
(match
p0 in (_ = n1)
return
(A (k + n).+1 -> A (n1 + n).+1)
with
| 1 => funa0 : A (k + n).+1 => a0 ^+
end
(transport idmap
(ap A (nat_add_succ_r k n)) a) =
transport idmap
(ap A (nat_add_succ_r n0 n))
(match
p0 in (_ = n1)
return (A ... -> A ...)
with
| 1 => funa0 : A (...) => a0 ^+
end a))
with
| 1 =>
K S (fun (n : nat) (a0 : A n) => a0 ^+)
(nat_add_succ_r k n)
end
|} 1 a)^ @
ap (colim_shift_seq_to_colim_seq A n)
(colimp k.+1 k.+21
({|
DiagramMap_obj :=
funk : nat =>
transport idmap (ap A (nat_add_succ_r k n));
DiagramMap_comm :=
fun (kl : nat) (p : k.+1 = l)
(a : A (k + n.+1)) =>
match
p as p0 in (_ = n0)
return
(match
p0 in (_ = n1)
return (A ....+1 -> A ....+1)
with
| 1 => funa0 : A (...).+1 => a0 ^+
end
(transport idmap
(ap A (nat_add_succ_r k n)) a) =
transport idmap
(ap A (nat_add_succ_r n0 n))
(match p0 in (...) return (...) with
| 1 => funa0 : ... => a0 ^+
end a))
with
| 1 =>
K S (fun (n : nat) (a0 : A n) => a0 ^+)
(nat_add_succ_r k n)
end
|} k a)))
rewrite colim_shift_seq_to_colim_seq_beta_glue; exact (L (glue A)).Defined.Definitionequiv_colim_shift_seq_to_colim_seq `{Funext} A n
: Colimit (shift_seq A n) <~> Colimit A
:= Build_Equiv _ _ (colim_shift_seq_to_colim_seq A n) _.(** Corollary 7.7.1 for k := -2; implies Lemma 7.2. *)
H: Funext A: Sequence
(forallk : Graph.graph0 sequence_graph, Contr (A k)) ->
Contr (Colimit A)
H: Funext A: Sequence
(forallk : Graph.graph0 sequence_graph, Contr (A k)) ->
Contr (Colimit A)
forall (n : Graph.graph0 sequence_graph)
(a : unit_seq n),
ap idmap (glue unit_seq n a) @ ?h n a =
?h n.+1 a ^+ @
ap (fun_ : Colimit unit_seq => inj unit_seq 0 tt)
(glue unit_seq n a)
forall (n : Graph.graph0 sequence_graph)
(a : unit_seq n),
ap idmap (glue unit_seq n a) @
(funn0 : Graph.graph0 sequence_graph =>
(funa0 : unit_seq n0 =>
match
a0 as u
return (inj unit_seq n0 u = inj unit_seq 0 tt)
with
| tt =>
nat_rect
(funn1 : nat =>
inj unit_seq n1 tt = inj unit_seq 0 tt) 1
(fun (n1 : nat)
(r : inj unit_seq n1 tt = inj unit_seq 0 tt)
=> glue unit_seq n1 tt @ r) n0
end)
:
idmap o inj unit_seq n0 ==
(fun_ : Colimit unit_seq => inj unit_seq 0 tt)
o inj unit_seq n0) n a =
(funn0 : Graph.graph0 sequence_graph =>
(funa0 : unit_seq n0 =>
match
a0 as u
return (inj unit_seq n0 u = inj unit_seq 0 tt)
with
| tt =>
nat_rect
(funn1 : nat =>
inj unit_seq n1 tt = inj unit_seq 0 tt) 1
(fun (n1 : nat)
(r : inj unit_seq n1 tt = inj unit_seq 0 tt)
=> glue unit_seq n1 tt @ r) n0
end)
:
idmap o inj unit_seq n0 ==
(fun_ : Colimit unit_seq => inj unit_seq 0 tt)
o inj unit_seq n0) n.+1 a ^+ @
ap (fun_ : Colimit unit_seq => inj unit_seq 0 tt)
(glue unit_seq n a)
intro n; destruct a; rewrite ap_idmap, ap_const, concat_p1; reflexivity.Defined.(** Fibered sequences; Section 4. *)RecordFibSequence (A : Sequence) := {
fibSequence : sig A -> Type;
fibSequenceArr x : fibSequence x -> fibSequence x^++
}.CoercionfibSequence : FibSequence >-> Funclass.Arguments fibSequence {A}.Arguments fibSequenceArr {A}.Notation"b ^+f" := (fibSequenceArr _ _ b).(** The Sigma of a fibered type sequence; Definition 4.3. *)
A: Sequence B: FibSequence A
Sequence
A: Sequence B: FibSequence A
Sequence
A: Sequence B: FibSequence A
nat -> Type
A: Sequence B: FibSequence A
foralln : nat, ?X n -> ?X n.+1
A: Sequence B: FibSequence A
nat -> Type
exact (funn => {a : A n & B (n;a)}).
A: Sequence B: FibSequence A
foralln : nat,
(funn0 : nat => {a : A n0 & B (n0; a)}) n ->
(funn0 : nat => {a : A n0 & B (n0; a)}) n.+1
intros n [a b]; exact (a^+; b^+f).Defined.(** The canonical projection from the sequential colimit of Sigmas to the sequential colimit of the first component; Definition 4.3. *)
A: Sequence B: FibSequence A
Colimit (sig_seq B) -> Colimit A
A: Sequence B: FibSequence A
Colimit (sig_seq B) -> Colimit A
A: Sequence B: FibSequence A
foralli : Graph.graph0 sequence_graph,
sig_seq B i -> Colimit A
A: Sequence B: FibSequence A
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
?legs j o (sig_seq B) _f g == ?legs i
A: Sequence B: FibSequence A
foralli : Graph.graph0 sequence_graph,
sig_seq B i -> Colimit A
intros n [a _]; exact (inj _ n a).
A: Sequence B: FibSequence A
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
(fun (n : Graph.graph0 sequence_graph)
(X : sig_seq B n) =>
(fun (a : A n) (_ : B (n; a)) => inj A n a) X.1 X.2)
j o (sig_seq B) _f g ==
(fun (n : Graph.graph0 sequence_graph)
(X : sig_seq B n) =>
(fun (a : A n) (_ : B (n; a)) => inj A n a) X.1 X.2)
i
intros n m p [a b]; destruct p; exact (glue _ n a).Defined.(** Given a sequence fibered over [A], each point [x : sig A] induces a new type sequence; Section 4. *)
A: Sequence B: FibSequence A x: {x : _ & A x}
Sequence
A: Sequence B: FibSequence A x: {x : _ & A x}
Sequence
A: Sequence B: FibSequence A
{x : _ & A x} -> Type
A: Sequence B: FibSequence A k: nat h: {x : _ & A x} -> Type
A: Sequence B: FibSequence A k: nat h: {x : _ & A x} -> Type
{x : _ & A x} -> Type
exact (funx => h x^++).
A: Sequence B: FibSequence A
forallx : {x : _ & A x},
nat_rect (fun_ : nat => {x : _ & A x} -> Type)
(funx0 : {x : _ & A x} => B x0)
(fun (_ : nat) (h : {x : _ & A x} -> Type)
(x0 : {x : _ & A x}) => h x0 ^++) 0 x ->
nat_rect (fun_ : nat => {x : _ & A x} -> Type)
(funx0 : {x : _ & A x} => B x0)
(fun (_ : nat) (h : {x : _ & A x} -> Type)
(x0 : {x : _ & A x}) => h x0 ^++) 1 x
exact (funxb => b^+f).
A: Sequence B: FibSequence A k: nat h: forallx : {x : _ & A x},
nat_rect (fun_ : nat => {x : _ & A x} -> Type)
(funx0 : {x : _ & A x} => B x0)
(fun (_ : nat) (h : {x : _ & A x} -> Type)
(x0 : {x : _ & A x}) => h x0 ^++) k x ->
nat_rect (fun_ : nat => {x : _ & A x} -> Type)
(funx0 : {x : _ & A x} => B x0)
(fun (_ : nat) (h : {x : _ & A x} -> Type)
(x0 : {x : _ & A x}) => h x0 ^++) k.+1 x
forallx : {x : _ & A x},
nat_rect (fun_ : nat => {x : _ & A x} -> Type)
(funx0 : {x : _ & A x} => B x0)
(fun (_ : nat) (h : {x : _ & A x} -> Type)
(x0 : {x : _ & A x}) => h x0 ^++) k.+1 x ->
nat_rect (fun_ : nat => {x : _ & A x} -> Type)
(funx0 : {x : _ & A x} => B x0)
(fun (_ : nat) (h : {x : _ & A x} -> Type)
(x0 : {x : _ & A x}) => h x0 ^++) k.+2 x
exact (funx => h x^++).Defined.(** The induced sequence can be equivalently described by using shifting; Lemma 7.1. *)Definitionfib_seq_to_seq' {A} (B : FibSequence A) (x : sig A) : Sequence
:= Build_Sequence (funk => B x^++k) (funkb => b^+f).
A: Sequence B: FibSequence A x: {x : _ & A x}
fib_seq_to_seq B x ~d~ fib_seq_to_seq' B x
A: Sequence B: FibSequence A x: {x : _ & A x}
fib_seq_to_seq B x ~d~ fib_seq_to_seq' B x
A: Sequence B: FibSequence A x: {x : _ & A x}
DiagramMap (fib_seq_to_seq B x) (fib_seq_to_seq' B x)
DiagramMap (fib_seq_to_seq B x) (fib_seq_to_seq' B x)
A: Sequence B: FibSequence A x: {x : _ & A x}
foralli : Graph.graph0 sequence_graph,
fib_seq_to_seq B x i -> fib_seq_to_seq' B x i
A: Sequence B: FibSequence A x: {x : _ & A x}
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j)
(x0 : fib_seq_to_seq B x i),
((fib_seq_to_seq' B x) _f g) (?DiagramMap_obj i x0) =
?DiagramMap_obj j (((fib_seq_to_seq B x) _f g) x0)
A: Sequence B: FibSequence A x: {x : _ & A x}
foralli : Graph.graph0 sequence_graph,
fib_seq_to_seq B x i -> fib_seq_to_seq' B x i
A: Sequence B: FibSequence A
forallx : {x : _ & A x},
fib_seq_to_seq B x 0 -> fib_seq_to_seq' B x 0
A: Sequence B: FibSequence A n: nat e: forallx : {x : _ & A x},
fib_seq_to_seq B x n -> fib_seq_to_seq' B x n
forallx : {x : _ & A x},
fib_seq_to_seq B x n.+1 -> fib_seq_to_seq' B x n.+1
A: Sequence B: FibSequence A
forallx : {x : _ & A x},
fib_seq_to_seq B x 0 -> fib_seq_to_seq' B x 0
exact (fun_ => idmap).
A: Sequence B: FibSequence A n: nat e: forallx : {x : _ & A x},
fib_seq_to_seq B x n -> fib_seq_to_seq' B x n
forallx : {x : _ & A x},
fib_seq_to_seq B x n.+1 -> fib_seq_to_seq' B x n.+1
exact (funx => coe (ap B (seq_pair_shift_assoc x n)) o e x^++).
A: Sequence B: FibSequence A x: {x : _ & A x}
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j)
(x0 : fib_seq_to_seq B x i),
((fib_seq_to_seq' B x) _f g)
((funn : Graph.graph0 sequence_graph =>
nat_rect
(funn0 : nat =>
forallx : {x : _ & A x},
fib_seq_to_seq B x n0 -> fib_seq_to_seq' B x n0)
(funx : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx : {x : _ & A x},
fib_seq_to_seq B x n0 ->
fib_seq_to_seq' B x n0)
(x : {x : _ & A x}) =>
coe (ap B (seq_pair_shift_assoc x n0))
o e x ^++) n x) i x0) =
(funn : Graph.graph0 sequence_graph =>
nat_rect
(funn0 : nat =>
forallx : {x : _ & A x},
fib_seq_to_seq B x n0 -> fib_seq_to_seq' B x n0)
(funx : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx : {x : _ & A x},
fib_seq_to_seq B x n0 ->
fib_seq_to_seq' B x n0) (x : {x : _ & A x})
=>
coe (ap B (seq_pair_shift_assoc x n0)) o e x ^++)
n x) j (((fib_seq_to_seq B x) _f g) x0)
A: Sequence B: FibSequence A
forall (x : {x : _ & A x})
(x0 : fib_seq_to_seq B x 0),
(nat_rect
(funn : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n -> fib_seq_to_seq' B x1 n)
(funx1 : {x : _ & A x} => idmap)
(fun (n : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n ->
fib_seq_to_seq' B x1 n)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n) =>
equiv_path (B (x1 ^++) ^++ n) (B x1 ^++ (n.+1))
(ap B (seq_pair_shift_assoc x1 n)) (e x1 ^++ x2))
0 x x0) ^+ =
nat_rect
(funn : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n -> fib_seq_to_seq' B x1 n)
(funx1 : {x : _ & A x} => idmap)
(fun (n : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n ->
fib_seq_to_seq' B x1 n) (x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n) =>
equiv_path (B (x1 ^++) ^++ n) (B x1 ^++ (n.+1))
(ap B (seq_pair_shift_assoc x1 n)) (e x1 ^++ x2))
1 x x0 ^+
A: Sequence B: FibSequence A n: nat p: forall (x : {x : _ & A x})
(x0 : fib_seq_to_seq B x n),
(nat_rect
(funn : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n ->
fib_seq_to_seq' B x1 n)
(funx1 : {x : _ & A x} => idmap)
(fun (n : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n ->
fib_seq_to_seq' B x1 n)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n) =>
equiv_path (B (x1 ^++) ^++ n)
(B x1 ^++ (n.+1))
(ap B (seq_pair_shift_assoc x1 n))
(e x1 ^++ x2)) n x x0) ^+ =
nat_rect
(funn : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n -> fib_seq_to_seq' B x1 n)
(funx1 : {x : _ & A x} => idmap)
(fun (n : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n ->
fib_seq_to_seq' B x1 n)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n) =>
equiv_path (B (x1 ^++) ^++ n) (B x1 ^++ (n.+1))
(ap B (seq_pair_shift_assoc x1 n))
(e x1 ^++ x2)) n.+1 x x0 ^+
forall (x : {x : _ & A x})
(x0 : fib_seq_to_seq B x n.+1),
(nat_rect
(funn : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n -> fib_seq_to_seq' B x1 n)
(funx1 : {x : _ & A x} => idmap)
(fun (n : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n ->
fib_seq_to_seq' B x1 n)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n) =>
equiv_path (B (x1 ^++) ^++ n) (B x1 ^++ (n.+1))
(ap B (seq_pair_shift_assoc x1 n)) (e x1 ^++ x2))
n.+1 x x0) ^+ =
nat_rect
(funn : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n -> fib_seq_to_seq' B x1 n)
(funx1 : {x : _ & A x} => idmap)
(fun (n : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n ->
fib_seq_to_seq' B x1 n) (x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n) =>
equiv_path (B (x1 ^++) ^++ n) (B x1 ^++ (n.+1))
(ap B (seq_pair_shift_assoc x1 n)) (e x1 ^++ x2))
n.+2 x x0 ^+
A: Sequence B: FibSequence A
forall (x : {x : _ & A x})
(x0 : fib_seq_to_seq B x 0),
(nat_rect
(funn : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n -> fib_seq_to_seq' B x1 n)
(funx1 : {x : _ & A x} => idmap)
(fun (n : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n ->
fib_seq_to_seq' B x1 n)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n) =>
equiv_path (B (x1 ^++) ^++ n) (B x1 ^++ (n.+1))
(ap B (seq_pair_shift_assoc x1 n)) (e x1 ^++ x2))
0 x x0) ^+ =
nat_rect
(funn : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n -> fib_seq_to_seq' B x1 n)
(funx1 : {x : _ & A x} => idmap)
(fun (n : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n ->
fib_seq_to_seq' B x1 n) (x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n) =>
equiv_path (B (x1 ^++) ^++ n) (B x1 ^++ (n.+1))
(ap B (seq_pair_shift_assoc x1 n)) (e x1 ^++ x2))
1 x x0 ^+
exact (fun__ => idpath).
A: Sequence B: FibSequence A n: nat p: forall (x : {x : _ & A x})
(x0 : fib_seq_to_seq B x n),
(nat_rect
(funn : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n ->
fib_seq_to_seq' B x1 n)
(funx1 : {x : _ & A x} => idmap)
(fun (n : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n ->
fib_seq_to_seq' B x1 n)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n) =>
equiv_path (B (x1 ^++) ^++ n)
(B x1 ^++ (n.+1))
(ap B (seq_pair_shift_assoc x1 n))
(e x1 ^++ x2)) n x x0) ^+ =
nat_rect
(funn : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n -> fib_seq_to_seq' B x1 n)
(funx1 : {x : _ & A x} => idmap)
(fun (n : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n ->
fib_seq_to_seq' B x1 n)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n) =>
equiv_path (B (x1 ^++) ^++ n) (B x1 ^++ (n.+1))
(ap B (seq_pair_shift_assoc x1 n))
(e x1 ^++ x2)) n.+1 x x0 ^+
forall (x : {x : _ & A x})
(x0 : fib_seq_to_seq B x n.+1),
(nat_rect
(funn : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n -> fib_seq_to_seq' B x1 n)
(funx1 : {x : _ & A x} => idmap)
(fun (n : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n ->
fib_seq_to_seq' B x1 n)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n) =>
equiv_path (B (x1 ^++) ^++ n) (B x1 ^++ (n.+1))
(ap B (seq_pair_shift_assoc x1 n)) (e x1 ^++ x2))
n.+1 x x0) ^+ =
nat_rect
(funn : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n -> fib_seq_to_seq' B x1 n)
(funx1 : {x : _ & A x} => idmap)
(fun (n : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n ->
fib_seq_to_seq' B x1 n) (x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n) =>
equiv_path (B (x1 ^++) ^++ n) (B x1 ^++ (n.+1))
(ap B (seq_pair_shift_assoc x1 n)) (e x1 ^++ x2))
n.+2 x x0 ^+
exact (funxb => K _ _ _ @ (ap _ (p (x^++) b))).
A: Sequence B: FibSequence A x: {x : _ & A x}
foralli : Graph.graph0 sequence_graph,
IsEquiv
({|
DiagramMap_obj :=
funn : Graph.graph0 sequence_graph =>
nat_rect
(funn0 : nat =>
forallx : {x : _ & A x},
fib_seq_to_seq B x n0 ->
fib_seq_to_seq' B x n0)
(funx : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx : {x : _ & A x},
fib_seq_to_seq B x n0 ->
fib_seq_to_seq' B x n0)
(x : {x : _ & A x}) =>
coe (ap B (seq_pair_shift_assoc x n0))
o e x ^++) n x;
DiagramMap_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m) =>
match
p as p0 in (_ = n0)
return
(forallx0 : fib_seq_to_seq B x n,
((fib_seq_to_seq' B x) _f p0)
(nat_rect
(funn1 : nat =>
forallx : {x : _ & A x},
fib_seq_to_seq B x n1 ->
fib_seq_to_seq' B x n1)
(funx : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx : {x : _ & A x},
fib_seq_to_seq B x n1 ->
fib_seq_to_seq' B x n1)
(x : {x : _ & A x})
(x1 : fib_seq_to_seq B x ^++ n1)
=>
equiv_path (B (x ^++) ^++ n1)
(B x ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x n1))
(e x ^++ x1)) n x x0) =
nat_rect
(funn1 : nat =>
forallx : {x : _ & A x},
fib_seq_to_seq B x n1 ->
fib_seq_to_seq' B x n1)
(funx : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx : {x : _ & A x},
fib_seq_to_seq B x n1 ->
fib_seq_to_seq' B x n1)
(x : {x : _ & A x})
(x1 : fib_seq_to_seq B x ^++ n1) =>
equiv_path (B (x ^++) ^++ n1)
(B x ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x n1))
(e x ^++ x1)) n0 x
(((fib_seq_to_seq B x) _f p0) x0))
with
| 1 =>
nat_rect
(funn0 : nat =>
forall (x : {x : _ & A x})
(x0 : fib_seq_to_seq B x n0),
(nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n1)
=>
equiv_path (B (x1 ^++) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x1 n1))
(e x1 ^++ x2)) n0 x x0) ^+ =
nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n1)
=>
equiv_path (B (x1 ^++) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x1 n1))
(e x1 ^++ x2)) n0.+1 x x0 ^+)
(fun (x : {x : _ & A x})
(x0 : fib_seq_to_seq B x 0) => 1)
(fun (n0 : nat)
(p0 : forall (x : {x : _ & A x})
(x0 : fib_seq_to_seq B x n0),
(nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} =>
idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & ...},
fib_seq_to_seq B x1
n1 ->
fib_seq_to_seq' B x1
n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B
x1 ^++ n1) =>
equiv_path (B (...) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc
x1 n1))
(e x1 ^++ x2)) n0 x x0) ^+ =
nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} =>
idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1
n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B
x1 ^++ n1) =>
equiv_path
(B (x1 ^++) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc x1
n1)) (e x1 ^++ x2))
n0.+1 x x0 ^+)
(x : {x : _ & A x})
(b : fib_seq_to_seq B x n0.+1) =>
K seq_pair_shift (fibSequenceArr B)
(seq_pair_shift_assoc x n0) @
ap
(equiv_path (B ((x ^++) ^++ n0) ^++)
(B
(((fix F ... : ... :=
...
...
...
end) n0) ^++) ^++)
(ap B
(ap seq_pair_shift
(seq_pair_shift_assoc x n0))))
(p0 x ^++ b)) n x
end
|} i)
A: Sequence B: FibSequence A
forallx : {x : _ & A x},
IsEquiv
({|
DiagramMap_obj :=
funn : Graph.graph0 sequence_graph =>
nat_rect
(funn0 : nat =>
forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n0 ->
fib_seq_to_seq' B x0 n0)
(funx0 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n0 ->
fib_seq_to_seq' B x0 n0)
(x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 ^++ n0) =>
equiv_path (B (x0 ^++) ^++ n0)
(B x0 ^++ (n0.+1))
(ap B (seq_pair_shift_assoc x0 n0))
(e x0 ^++ x1)) n x;
DiagramMap_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m) =>
match
p as p0 in (_ = n0)
return
(forallx0 : fib_seq_to_seq B x n,
((fib_seq_to_seq' B x) _f p0)
(nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n1)
=>
equiv_path (B (x1 ^++) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x1 n1))
(e x1 ^++ x2)) n x x0) =
nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n1) =>
equiv_path (B (x1 ^++) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x1 n1))
(e x1 ^++ x2)) n0 x
(((fib_seq_to_seq B x) _f p0) x0))
with
| 1 =>
nat_rect
(funn0 : nat =>
forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n0),
(nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n1)
=>
equiv_path (B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x2 n1))
(e x2 ^++ x3)) n0 x0 x1) ^+ =
nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n1)
=>
equiv_path (B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x2 n1))
(e x2 ^++ x3)) n0.+1 x0 x1 ^+)
(fun (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 0) => 1)
(fun (n0 : nat)
(p0 : forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n0),
(nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} =>
idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & ...},
fib_seq_to_seq B x2
n1 ->
fib_seq_to_seq' B x2
n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B
x2 ^++ n1) =>
equiv_path (B (...) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc
x2 n1))
(e x2 ^++ x3)) n0 x0 x1)
^+ =
nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} =>
idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2
n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B
x2 ^++ n1) =>
equiv_path
(B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc x2
n1)) (e x2 ^++ x3))
n0.+1 x0 x1 ^+)
(x0 : {x : _ & A x})
(b : fib_seq_to_seq B x0 n0.+1) =>
K seq_pair_shift (fibSequenceArr B)
(seq_pair_shift_assoc x0 n0) @
ap
(equiv_path (B ((x0 ^++) ^++ n0) ^++)
(B
((nat_iter n0 seq_pair_shift x0)
^++) ^++)
(ap B
(ap seq_pair_shift
(seq_pair_shift_assoc x0 n0))))
(p0 x0 ^++ b)) n x
end
|} 0)
A: Sequence B: FibSequence A n: nat e: forallx : {x : _ & A x},
IsEquiv
({|
DiagramMap_obj :=
funn : Graph.graph0 sequence_graph =>
nat_rect
(funn0 : nat =>
forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n0 ->
fib_seq_to_seq' B x0 n0)
(funx0 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n0 ->
fib_seq_to_seq' B x0 n0)
(x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 ^++ n0) =>
equiv_path (B (x0 ^++) ^++ n0)
(B x0 ^++ (n0.+1))
(ap B (seq_pair_shift_assoc x0 n0))
(e x0 ^++ x1)) n x;
DiagramMap_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m) =>
match
p as p0 in (_ = n0)
return
(forallx0 : fib_seq_to_seq B x n,
((fib_seq_to_seq' B x) _f p0)
(nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++
n1) =>
equiv_path (B (x1 ^++) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc x1 n1))
(e x1 ^++ x2)) n x x0) =
nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n1)
=>
equiv_path (B (x1 ^++) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc x1 n1))
(e x1 ^++ x2)) n0 x
(((fib_seq_to_seq B x) _f p0) x0))
with
| 1 =>
nat_rect
(funn0 : nat =>
forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n0),
(nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++
n1) =>
equiv_path (B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc x2 n1))
(e x2 ^++ x3)) n0 x0 x1) ^+ =
nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++
n1) =>
equiv_path (B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc x2 n1))
(e x2 ^++ x3)) n0.+1 x0 x1 ^+)
(fun (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 0) => 1)
(fun (n0 : nat)
(p0 : forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n0),
(nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x}
=> idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ &
...},
fib_seq_to_seq B
x2 n1 ->
fib_seq_to_seq' B
x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B
x2 ^++ n1) =>
equiv_path
(B (...) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc
x2 n1))
(e x2 ^++ x3)) n0 x0
x1) ^+ =
nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} =>
idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B
x2 n1 ->
fib_seq_to_seq' B
x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B
x2 ^++ n1) =>
equiv_path
(B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc
x2 n1))
(e x2 ^++ x3)) n0.+1 x0
x1 ^+)
(x0 : {x : _ & A x})
(b : fib_seq_to_seq B x0 n0.+1) =>
K seq_pair_shift (fibSequenceArr B)
(seq_pair_shift_assoc x0 n0) @
ap
(equiv_path
(B ((x0 ^++) ^++ n0) ^++)
(B
((nat_iter n0 seq_pair_shift
x0) ^++) ^++)
(ap B
(ap seq_pair_shift
(seq_pair_shift_assoc x0
n0)))) (p0 x0 ^++ b))
n x
end
|} n)
forallx : {x : _ & A x},
IsEquiv
({|
DiagramMap_obj :=
funn : Graph.graph0 sequence_graph =>
nat_rect
(funn0 : nat =>
forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n0 ->
fib_seq_to_seq' B x0 n0)
(funx0 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n0 ->
fib_seq_to_seq' B x0 n0)
(x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 ^++ n0) =>
equiv_path (B (x0 ^++) ^++ n0)
(B x0 ^++ (n0.+1))
(ap B (seq_pair_shift_assoc x0 n0))
(e x0 ^++ x1)) n x;
DiagramMap_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m) =>
match
p as p0 in (_ = n0)
return
(forallx0 : fib_seq_to_seq B x n,
((fib_seq_to_seq' B x) _f p0)
(nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n1)
=>
equiv_path (B (x1 ^++) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x1 n1))
(e x1 ^++ x2)) n x x0) =
nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n1) =>
equiv_path (B (x1 ^++) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x1 n1))
(e x1 ^++ x2)) n0 x
(((fib_seq_to_seq B x) _f p0) x0))
with
| 1 =>
nat_rect
(funn0 : nat =>
forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n0),
(nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n1)
=>
equiv_path (B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x2 n1))
(e x2 ^++ x3)) n0 x0 x1) ^+ =
nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n1)
=>
equiv_path (B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x2 n1))
(e x2 ^++ x3)) n0.+1 x0 x1 ^+)
(fun (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 0) => 1)
(fun (n0 : nat)
(p0 : forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n0),
(nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} =>
idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & ...},
fib_seq_to_seq B x2
n1 ->
fib_seq_to_seq' B x2
n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B
x2 ^++ n1) =>
equiv_path (B (...) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc
x2 n1))
(e x2 ^++ x3)) n0 x0 x1)
^+ =
nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} =>
idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2
n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B
x2 ^++ n1) =>
equiv_path
(B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc x2
n1)) (e x2 ^++ x3))
n0.+1 x0 x1 ^+)
(x0 : {x : _ & A x})
(b : fib_seq_to_seq B x0 n0.+1) =>
K seq_pair_shift (fibSequenceArr B)
(seq_pair_shift_assoc x0 n0) @
ap
(equiv_path (B ((x0 ^++) ^++ n0) ^++)
(B
((nat_iter n0 seq_pair_shift x0)
^++) ^++)
(ap B
(ap seq_pair_shift
(seq_pair_shift_assoc x0 n0))))
(p0 x0 ^++ b)) n x
end
|} n.+1)
A: Sequence B: FibSequence A
forallx : {x : _ & A x},
IsEquiv
({|
DiagramMap_obj :=
funn : Graph.graph0 sequence_graph =>
nat_rect
(funn0 : nat =>
forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n0 ->
fib_seq_to_seq' B x0 n0)
(funx0 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n0 ->
fib_seq_to_seq' B x0 n0)
(x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 ^++ n0) =>
equiv_path (B (x0 ^++) ^++ n0)
(B x0 ^++ (n0.+1))
(ap B (seq_pair_shift_assoc x0 n0))
(e x0 ^++ x1)) n x;
DiagramMap_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m) =>
match
p as p0 in (_ = n0)
return
(forallx0 : fib_seq_to_seq B x n,
((fib_seq_to_seq' B x) _f p0)
(nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n1)
=>
equiv_path (B (x1 ^++) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x1 n1))
(e x1 ^++ x2)) n x x0) =
nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n1) =>
equiv_path (B (x1 ^++) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x1 n1))
(e x1 ^++ x2)) n0 x
(((fib_seq_to_seq B x) _f p0) x0))
with
| 1 =>
nat_rect
(funn0 : nat =>
forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n0),
(nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n1)
=>
equiv_path (B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x2 n1))
(e x2 ^++ x3)) n0 x0 x1) ^+ =
nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n1)
=>
equiv_path (B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x2 n1))
(e x2 ^++ x3)) n0.+1 x0 x1 ^+)
(fun (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 0) => 1)
(fun (n0 : nat)
(p0 : forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n0),
(nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} =>
idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & ...},
fib_seq_to_seq B x2
n1 ->
fib_seq_to_seq' B x2
n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B
x2 ^++ n1) =>
equiv_path (B (...) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc
x2 n1))
(e x2 ^++ x3)) n0 x0 x1)
^+ =
nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} =>
idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2
n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B
x2 ^++ n1) =>
equiv_path
(B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc x2
n1)) (e x2 ^++ x3))
n0.+1 x0 x1 ^+)
(x0 : {x : _ & A x})
(b : fib_seq_to_seq B x0 n0.+1) =>
K seq_pair_shift (fibSequenceArr B)
(seq_pair_shift_assoc x0 n0) @
ap
(equiv_path (B ((x0 ^++) ^++ n0) ^++)
(B
((nat_iter n0 seq_pair_shift x0)
^++) ^++)
(ap B
(ap seq_pair_shift
(seq_pair_shift_assoc x0 n0))))
(p0 x0 ^++ b)) n x
end
|} 0)
exact (fun_ => isequiv_idmap _).
A: Sequence B: FibSequence A n: nat e: forallx : {x : _ & A x},
IsEquiv
({|
DiagramMap_obj :=
funn : Graph.graph0 sequence_graph =>
nat_rect
(funn0 : nat =>
forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n0 ->
fib_seq_to_seq' B x0 n0)
(funx0 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n0 ->
fib_seq_to_seq' B x0 n0)
(x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 ^++ n0) =>
equiv_path (B (x0 ^++) ^++ n0)
(B x0 ^++ (n0.+1))
(ap B (seq_pair_shift_assoc x0 n0))
(e x0 ^++ x1)) n x;
DiagramMap_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m) =>
match
p as p0 in (_ = n0)
return
(forallx0 : fib_seq_to_seq B x n,
((fib_seq_to_seq' B x) _f p0)
(nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++
n1) =>
equiv_path (B (x1 ^++) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc x1 n1))
(e x1 ^++ x2)) n x x0) =
nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n1)
=>
equiv_path (B (x1 ^++) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc x1 n1))
(e x1 ^++ x2)) n0 x
(((fib_seq_to_seq B x) _f p0) x0))
with
| 1 =>
nat_rect
(funn0 : nat =>
forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n0),
(nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++
n1) =>
equiv_path (B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc x2 n1))
(e x2 ^++ x3)) n0 x0 x1) ^+ =
nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++
n1) =>
equiv_path (B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc x2 n1))
(e x2 ^++ x3)) n0.+1 x0 x1 ^+)
(fun (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 0) => 1)
(fun (n0 : nat)
(p0 : forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n0),
(nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x}
=> idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ &
...},
fib_seq_to_seq B
x2 n1 ->
fib_seq_to_seq' B
x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B
x2 ^++ n1) =>
equiv_path
(B (...) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc
x2 n1))
(e x2 ^++ x3)) n0 x0
x1) ^+ =
nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} =>
idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B
x2 n1 ->
fib_seq_to_seq' B
x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B
x2 ^++ n1) =>
equiv_path
(B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc
x2 n1))
(e x2 ^++ x3)) n0.+1 x0
x1 ^+)
(x0 : {x : _ & A x})
(b : fib_seq_to_seq B x0 n0.+1) =>
K seq_pair_shift (fibSequenceArr B)
(seq_pair_shift_assoc x0 n0) @
ap
(equiv_path
(B ((x0 ^++) ^++ n0) ^++)
(B
((nat_iter n0 seq_pair_shift
x0) ^++) ^++)
(ap B
(ap seq_pair_shift
(seq_pair_shift_assoc x0
n0)))) (p0 x0 ^++ b))
n x
end
|} n)
forallx : {x : _ & A x},
IsEquiv
({|
DiagramMap_obj :=
funn : Graph.graph0 sequence_graph =>
nat_rect
(funn0 : nat =>
forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n0 ->
fib_seq_to_seq' B x0 n0)
(funx0 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n0 ->
fib_seq_to_seq' B x0 n0)
(x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 ^++ n0) =>
equiv_path (B (x0 ^++) ^++ n0)
(B x0 ^++ (n0.+1))
(ap B (seq_pair_shift_assoc x0 n0))
(e x0 ^++ x1)) n x;
DiagramMap_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m) =>
match
p as p0 in (_ = n0)
return
(forallx0 : fib_seq_to_seq B x n,
((fib_seq_to_seq' B x) _f p0)
(nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n1)
=>
equiv_path (B (x1 ^++) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x1 n1))
(e x1 ^++ x2)) n x x0) =
nat_rect
(funn1 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(funx1 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n1 ->
fib_seq_to_seq' B x1 n1)
(x1 : {x : _ & A x})
(x2 : fib_seq_to_seq B x1 ^++ n1) =>
equiv_path (B (x1 ^++) ^++ n1)
(B x1 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x1 n1))
(e x1 ^++ x2)) n0 x
(((fib_seq_to_seq B x) _f p0) x0))
with
| 1 =>
nat_rect
(funn0 : nat =>
forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n0),
(nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n1)
=>
equiv_path (B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x2 n1))
(e x2 ^++ x3)) n0 x0 x1) ^+ =
nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n1)
=>
equiv_path (B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x2 n1))
(e x2 ^++ x3)) n0.+1 x0 x1 ^+)
(fun (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 0) => 1)
(fun (n0 : nat)
(p0 : forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n0),
(nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} =>
idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & ...},
fib_seq_to_seq B x2
n1 ->
fib_seq_to_seq' B x2
n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B
x2 ^++ n1) =>
equiv_path (B (...) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc
x2 n1))
(e x2 ^++ x3)) n0 x0 x1)
^+ =
nat_rect
(funn1 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2 n1)
(funx2 : {x : _ & A x} =>
idmap)
(fun (n1 : nat)
(e : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n1 ->
fib_seq_to_seq' B x2
n1)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B
x2 ^++ n1) =>
equiv_path
(B (x2 ^++) ^++ n1)
(B x2 ^++ (n1.+1))
(ap B
(seq_pair_shift_assoc x2
n1)) (e x2 ^++ x3))
n0.+1 x0 x1 ^+)
(x0 : {x : _ & A x})
(b : fib_seq_to_seq B x0 n0.+1) =>
K seq_pair_shift (fibSequenceArr B)
(seq_pair_shift_assoc x0 n0) @
ap
(equiv_path (B ((x0 ^++) ^++ n0) ^++)
(B
((nat_iter n0 seq_pair_shift x0)
^++) ^++)
(ap B
(ap seq_pair_shift
(seq_pair_shift_assoc x0 n0))))
(p0 x0 ^++ b)) n x
end
|} n.+1)
intro x; rapply isequiv_compose.Defined.(** A fibered type sequence defines a type family; Section 4. *)
H: Univalence A: Sequence B: FibSequence A
Colimit A -> Type
H: Univalence A: Sequence B: FibSequence A
Colimit A -> Type
H: Univalence A: Sequence B: FibSequence A
foralli : Graph.graph0 sequence_graph, A i -> Type
H: Univalence A: Sequence B: FibSequence A
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
?legs j o A _f g == ?legs i
H: Univalence A: Sequence B: FibSequence A
foralli : Graph.graph0 sequence_graph, A i -> Type
exact (funna => Colimit (fib_seq_to_seq B (n;a))).
H: Univalence A: Sequence B: FibSequence A
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
(fun (n : Graph.graph0 sequence_graph) (a : A n) =>
Colimit (fib_seq_to_seq B (n; a))) j o A _f g ==
(fun (n : Graph.graph0 sequence_graph) (a : A n) =>
Colimit (fib_seq_to_seq B (n; a))) i
H: Univalence A: Sequence B: FibSequence A n: Graph.graph0 sequence_graph a: A n
Colimit (fib_seq_to_seq B (n.+1; a ^+)) <~>
Colimit (fib_seq_to_seq B (n; a))
exact (equiv_colim_succ_seq_to_colim_seq (fib_seq_to_seq B (n;a))).Defined.
H: Univalence A: Diagram sequence_graph B: FibSequence A n: Graph.graph0 sequence_graph a: A n
coe (ap (fib_seq_to_type_fam B) (glue A n a)) =
colim_succ_seq_to_colim_seq (fib_seq_to_seq B (n; a))
H: Univalence A: Diagram sequence_graph B: FibSequence A n: Graph.graph0 sequence_graph a: A n
coe (ap (fib_seq_to_type_fam B) (glue A n a)) =
colim_succ_seq_to_colim_seq (fib_seq_to_seq B (n; a))
H: Univalence A: Diagram sequence_graph B: FibSequence A n: Graph.graph0 sequence_graph a: A n
coe
(legs_comm
{|
legs :=
fun (n : Graph.graph0 sequence_graph)
(a : A n) =>
Colimit (fib_seq_to_seq B (n; a));
legs_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m) =>
(funa : A n =>
match
p as p0 in (_ = n0)
return
(Colimit
(fib_seq_to_seq B (n0; (A _f p0) a)) =
Colimit (fib_seq_to_seq B (n; a)))
with
| 1 =>
path_universe_uncurried
(equiv_colim_succ_seq_to_colim_seq
(fib_seq_to_seq B (n; a)))
end)
:
(fun (n0 : Graph.graph0 sequence_graph)
(a : A n0) =>
Colimit (fib_seq_to_seq B (n0; a))) m
o A _f p ==
(fun (n0 : Graph.graph0 sequence_graph)
(a : A n0) =>
Colimit (fib_seq_to_seq B (n0; a))) n
|} n n.+11 a) =
colim_succ_seq_to_colim_seq (fib_seq_to_seq B (n; a))
X: Type Y: X -> Type x1, x2: X F: Y x1 -> Y x2 p: x1 = x2 psi: coe (ap Y p) = F y: Y x1
(x1; y) = (x2; F y)
X: Type Y: X -> Type x1, x2: X F: Y x1 -> Y x2 p: x1 = x2 psi: coe (ap Y p) = F y: Y x1
(x1; y) = (x2; F y)
destruct p; destruct psi; reflexivity.Defined.
X: Type Y: X -> Type x1, x2: X F: Y x1 -> Y x2 p: x1 = x2 psi: coe (ap Y p) = F y: Y x1
ap pr1 (Delta p psi y) = p
X: Type Y: X -> Type x1, x2: X F: Y x1 -> Y x2 p: x1 = x2 psi: coe (ap Y p) = F y: Y x1
ap pr1 (Delta p psi y) = p
destruct p; destruct psi; reflexivity.Defined.(** The canonical map from the sequential colimit of Sigmas to the Sigma of sequential colimits; Definition 5.1. *)
H: Univalence A: Sequence B: FibSequence A
Colimit (sig_seq B) ->
{x : _ & fib_seq_to_type_fam B x}
H: Univalence A: Sequence B: FibSequence A
Colimit (sig_seq B) ->
{x : _ & fib_seq_to_type_fam B x}
H: Univalence A: Sequence B: FibSequence A
foralli : Graph.graph0 sequence_graph,
sig_seq B i -> {x : _ & fib_seq_to_type_fam B x}
H: Univalence A: Sequence B: FibSequence A
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
?legs j o (sig_seq B) _f g == ?legs i
H: Univalence A: Sequence B: FibSequence A
foralli : Graph.graph0 sequence_graph,
sig_seq B i -> {x : _ & fib_seq_to_type_fam B x}
intros n [a b]; exact (inj A n a; inj (fib_seq_to_seq _ _) 0 b).
H: Univalence A: Sequence B: FibSequence A
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
(fun (n : Graph.graph0 sequence_graph)
(X : sig_seq B n) =>
(fun (a : A n) (b : B (n; a)) =>
(inj A n a; inj (fib_seq_to_seq B (n; a)) 0 b)) X.1
X.2) j o (sig_seq B) _f g ==
(fun (n : Graph.graph0 sequence_graph)
(X : sig_seq B n) =>
(fun (a : A n) (b : B (n; a)) =>
(inj A n a; inj (fib_seq_to_seq B (n; a)) 0 b)) X.1
X.2) i
H: Univalence A: Sequence B: FibSequence A n: Graph.graph0 sequence_graph a: A n b: B (n; a)
(inj A n.+1 ((a; b) ^+).1;
inj (fib_seq_to_seq B (n.+1; ((a; b) ^+).1)) 0
((a; b) ^+).2) =
(inj A n a; inj (fib_seq_to_seq B (n; a)) 1 b ^+)
srapply (Delta _ (fib_seq_to_type_fam_beta_glue B n a)).Defined.
H: Univalence A: Diagram sequence_graph B: FibSequence A n: Graph.graph0 sequence_graph a: A n b: (funa : A n => B (n; a)) a
ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)) =
Delta (colimp n n.+11 a)
(fib_seq_to_type_fam_beta_glue B n a)
(inj
(fib_seq_to_seq B
((n.+1; a ^+).1; (n.+1; a ^+).2)) 0 b ^+) @
ap (exist (fib_seq_to_type_fam B) (inj A n a))
(glue (fib_seq_to_seq B (n; a)) 0 b)
H: Univalence A: Diagram sequence_graph B: FibSequence A n: Graph.graph0 sequence_graph a: A n b: (funa : A n => B (n; a)) a
ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)) =
Delta (colimp n n.+11 a)
(fib_seq_to_type_fam_beta_glue B n a)
(inj
(fib_seq_to_seq B
((n.+1; a ^+).1; (n.+1; a ^+).2)) 0 b ^+) @
ap (exist (fib_seq_to_type_fam B) (inj A n a))
(glue (fib_seq_to_seq B (n; a)) 0 b)
srapply Colimit_rec_beta_colimp.Defined.(** An alternative induction principle for the sum of colimits; Lemma 5.2 and Section 6. *)SectionSeqColimitSumInd.Context `{Univalence} {A} (B : FibSequence A).Context (E : sig (fib_seq_to_type_fam B) -> Type).Context (e : forallnab, E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n (a;b)))).Context (t : forallnab, ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n (a;b))
# e n.+1 (a^+) (b^+f) = e n a b).(** The point-point case of the nested induction; corresponds to "h" in the paper. *)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b k: Graph.graph0 sequence_graph
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B ((n; a).1; (n; a).2) k),
E
(inj A n a;
inj (fib_seq_to_seq B ((n; a).1; (n; a).2)) k b)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b k: Graph.graph0 sequence_graph
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B ((n; a).1; (n; a).2) k),
E
(inj A n a;
inj (fib_seq_to_seq B ((n; a).1; (n; a).2)) k b)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B (n; a) 0),
E (inj A n a; inj (fib_seq_to_seq B (n; a)) 0 b)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b k: nat h: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B (n; a) k),
E (inj A n a; inj (fib_seq_to_seq B (n; a)) k b)
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B (n; a) k.+1),
E (inj A n a; inj (fib_seq_to_seq B (n; a)) k.+1 b)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B (n; a) 0),
E (inj A n a; inj (fib_seq_to_seq B (n; a)) 0 b)
exact e.
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b k: nat h: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B (n; a) k),
E (inj A n a; inj (fib_seq_to_seq B (n; a)) k b)
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B (n; a) k.+1),
E (inj A n a; inj (fib_seq_to_seq B (n; a)) k.+1 b)
intros n a b; exact (Delta _ (fib_seq_to_type_fam_beta_glue B n a) _ # h n.+1 (a^+) b).Defined.(** The path-point case of the nested induction is just reflexivity; corresponds to "mu" in the paper. *)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type x: X y1, y2: Y x z: {x : _ & Y x} p: y1 = y2 q1: z = (x; y1) q2: z = (x; y2) theta: q2 = q1 @ ap (exist Y x) p
transport (Z o exist Y x) p o transport Z q1 ==
transport Z q2
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type x: X y1, y2: Y x z: {x : _ & Y x} p: y1 = y2 q1: z = (x; y1) q2: z = (x; y2) theta: q2 = q1 @ ap (exist Y x) p
transport (Z o exist Y x) p o transport Z q1 ==
transport Z q2
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type x: X y1: Y x z: {x : _ & Y x}
(funx0 : Z z => transport Z 1 x0) ==
transport Z (1 @ 1)
reflexivity.Defined.
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type x1, x2: X y1, y2: Y x1 F: Y x1 -> Y x2 p: x1 = x2 q: y1 = y2 psi: coe (ap Y p) = F r: F y1 = F y2 theta: ap F q = r
transport (Z o exist Y x2) r
o transport Z (Delta p psi y1) ==
transport Z (Delta p psi y2)
o transport (Z o exist Y x1) q
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type x1, x2: X y1, y2: Y x1 F: Y x1 -> Y x2 p: x1 = x2 q: y1 = y2 psi: coe (ap Y p) = F r: F y1 = F y2 theta: ap F q = r
transport (Z o exist Y x2) r
o transport Z (Delta p psi y1) ==
transport Z (Delta p psi y2)
o transport (Z o exist Y x1) q
destruct theta; destruct q; reflexivity.Defined.(** The point-path case of the nested induction; corresponds to "H" in the paper. *)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b k: Graph.graph0 sequence_graph
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B ((n; a).1; (n; a).2) k),
transport
(E o exist (fib_seq_to_type_fam B) (inj A n a))
(glue (fib_seq_to_seq B ((n; a).1; (n; a).2)) k b)
(Q k.+1 n a b ^+) = Q k n a b
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b k: Graph.graph0 sequence_graph
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B ((n; a).1; (n; a).2) k),
transport
(E o exist (fib_seq_to_type_fam B) (inj A n a))
(glue (fib_seq_to_seq B ((n; a).1; (n; a).2)) k b)
(Q k.+1 n a b ^+) = Q k n a b
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B (n; a) 0),
transport
(funx : fib_seq_to_type_fam B (inj A n a) =>
E (inj A n a; x)) (colimp 011 b) (Q 1 n a b ^+) =
Q 0 n a b
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b k: nat h: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B (n; a) k),
transport
(funx : fib_seq_to_type_fam B (inj A n a) =>
E (inj A n a; x)) (colimp k k.+11 b)
(Q k.+1 n a b ^+) = Q k n a b
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B (n; a) k.+1),
transport
(funx : fib_seq_to_type_fam B (inj A n a) =>
E (inj A n a; x)) (colimp k.+1 k.+21 b)
(Q k.+2 n a b ^+) = Q k.+1 n a b
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B (n; a) 0),
transport
(funx : fib_seq_to_type_fam B (inj A n a) =>
E (inj A n a; x)) (colimp 011 b) (Q 1 n a b ^+) =
Q 0 n a b
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n b: fib_seq_to_seq B (n; a) 0
transport
(funx : fib_seq_to_type_fam B (inj A n a) =>
E (inj A n a; x)) (colimp 011 b) (Q 1 n a b ^+) =
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b))) (e n.+1 a ^+ b ^+f)
srapply (Eta (seq_colim_sum_to_sum_seq_colim_beta_glue B n a b)).
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b k: nat h: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B (n; a) k),
transport
(funx : fib_seq_to_type_fam B (inj A n a) =>
E (inj A n a; x)) (colimp k k.+11 b)
(Q k.+1 n a b ^+) = Q k n a b
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B (n; a) k.+1),
transport
(funx : fib_seq_to_type_fam B (inj A n a) =>
E (inj A n a; x)) (colimp k.+1 k.+21 b)
(Q k.+2 n a b ^+) = Q k.+1 n a b
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b k: nat h: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : fib_seq_to_seq B (n; a) k),
transport
(funx : fib_seq_to_type_fam B (inj A n a) =>
E (inj A n a; x)) (colimp k k.+11 b)
(Q k.+1 n a b ^+) = Q k n a b n: Graph.graph0 sequence_graph a: A n b: fib_seq_to_seq B (n; a) k.+1
transport
(funx : fib_seq_to_type_fam B (inj A n a) =>
E (inj A n a; x)) (colimp k.+1 k.+21 b)
(Q k.+2 n a b ^+) =
transport E
(Delta (colimp n n.+11 a)
(fib_seq_to_type_fam_beta_glue B n a)
(inj (fib_seq_to_seq B (n.+1; a ^+)) k b))
(transport
(funx : fib_seq_to_type_fam B (inj A n.+1 a ^+)
=> E (inj A n.+1 a ^+; x)) (colimp k k.+11 b)
(Q k.+1 n.+1 a ^+ b ^+))
srapply (Epsilon (glue A n a) (colim_succ_seq_to_colim_seq_beta_glue _ _ _)).Defined.(** The point case of the nested induction; corresponds to "g" in the paper. *)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n
forallx : fib_seq_to_type_fam B (inj A n a),
E (inj A n a; x)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n
forallx : fib_seq_to_type_fam B (inj A n a),
E (inj A n a; x)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n
forall (i : Graph.graph0 sequence_graph)
(x : fib_seq_to_seq B ((n; a).1; (n; a).2) i),
(funw : Colimit (fib_seq_to_seq B ((n; a).1; (n; a).2))
=> E (inj A n a; w))
(inj (fib_seq_to_seq B ((n; a).1; (n; a).2)) i x)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j)
(x : fib_seq_to_seq B ((n; a).1; (n; a).2) i),
transport
(funw : Colimit
(fib_seq_to_seq B ((n; a).1; (n; a).2)) =>
E (inj A n a; w)) (colimp i j g x)
(?q j
(((fib_seq_to_seq B ((n; a).1; (n; a).2)) _f g) x)) =
?q i x
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n
forall (i : Graph.graph0 sequence_graph)
(x : fib_seq_to_seq B ((n; a).1; (n; a).2) i),
(funw : Colimit (fib_seq_to_seq B ((n; a).1; (n; a).2))
=> E (inj A n a; w))
(inj (fib_seq_to_seq B ((n; a).1; (n; a).2)) i x)
exact (funk => Q k n a).
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j)
(x : fib_seq_to_seq B ((n; a).1; (n; a).2) i),
transport
(funw : Colimit
(fib_seq_to_seq B ((n; a).1; (n; a).2)) =>
E (inj A n a; w)) (colimp i j g x)
((funk : Graph.graph0 sequence_graph => Q k n a) j
(((fib_seq_to_seq B ((n; a).1; (n; a).2)) _f g) x)) =
(funk : Graph.graph0 sequence_graph => Q k n a) i x
intros k l p; destruct p; exact (R k n a).Defined.
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n b: fib_seq_to_seq B ((n; a).1; (n; a).2) 0
apD (F n a)
(glue (fib_seq_to_seq B ((n; a).1; (n; a).2)) 0 b) =
R 0 n a b
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n b: fib_seq_to_seq B ((n; a).1; (n; a).2) 0
apD (F n a)
(glue (fib_seq_to_seq B ((n; a).1; (n; a).2)) 0 b) =
R 0 n a b
srapply Colimit_ind_beta_colimp.Defined.
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type x1, x2: X y1, y2: Y x1 F: Y x1 -> Y x2 p: x1 = x2 q: y1 = y2 psi: coe (ap Y p) = F G1: forally : Y x1, Z (x1; y) G2: forally : Y x2, Z (x2; y) r: F y1 = F y2 theta: ap F q = r
forall
(u1 : G2 (F y1) = transport Z (Delta p psi y1) (G1 y1))
(u2 : G2 (F y2) = transport Z (Delta p psi y2) (G1 y2)),
apD G2 r @ u2 =
(ap (transport (funx : Y x2 => Z (x2; x)) r) u1 @
Epsilon p theta (G1 y1)) @
ap (transport Z (Delta p psi y2)) (apD G1 q) ->
transport
(funy : Y x1 =>
G2 (F y) = transport Z (Delta p psi y) (G1 y)) q u1 =
u2
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type x1, x2: X y1, y2: Y x1 F: Y x1 -> Y x2 p: x1 = x2 q: y1 = y2 psi: coe (ap Y p) = F G1: forally : Y x1, Z (x1; y) G2: forally : Y x2, Z (x2; y) r: F y1 = F y2 theta: ap F q = r
forall
(u1 : G2 (F y1) = transport Z (Delta p psi y1) (G1 y1))
(u2 : G2 (F y2) = transport Z (Delta p psi y2) (G1 y2)),
apD G2 r @ u2 =
(ap (transport (funx : Y x2 => Z (x2; x)) r) u1 @
Epsilon p theta (G1 y1)) @
ap (transport Z (Delta p psi y2)) (apD G1 q) ->
transport
(funy : Y x1 =>
G2 (F y) = transport Z (Delta p psi y) (G1 y)) q u1 =
u2
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type x1, x2: X y1: Y x1 F: Y x1 -> Y x2 p: x1 = x2 psi: coe (ap Y p) = F G1: forally : Y x1, Z (x1; y) G2: forally : Y x2, Z (x2; y) u1, u2: G2 (F y1) = transport Z (Delta p psi y1) (G1 y1)
apD G2 (ap F 1) @ u2 = u1 ->
transport
(funy : Y x1 =>
G2 (F y) = transport Z (Delta p psi y) (G1 y)) 1 u1 =
u2
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type x1, x2: X y1: Y x1 F: Y x1 -> Y x2 p: x1 = x2 psi: coe (ap Y p) = F G1: forally : Y x1, Z (x1; y) G2: forally : Y x2, Z (x2; y) u1, u2: G2 (F y1) = transport Z (Delta p psi y1) (G1 y1)
1 @ u2 = u1 -> u1 = u2
intro s; destruct s; exact (concat_1p _).Defined.(** The path case of the nested induction; corresponds to "omega" in the paper. *)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n
forally : fib_seq_to_type_fam B (inj A n.+1 a ^+),
F n a
(colim_succ_seq_to_colim_seq
(fib_seq_to_seq B (n; a)) y) =
transport E
(Delta (colimp n n.+11 a)
(fib_seq_to_type_fam_beta_glue B n a) y)
(F n.+1 a ^+ y)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n
forally : fib_seq_to_type_fam B (inj A n.+1 a ^+),
F n a
(colim_succ_seq_to_colim_seq
(fib_seq_to_seq B (n; a)) y) =
transport E
(Delta (colimp n n.+11 a)
(fib_seq_to_type_fam_beta_glue B n a) y)
(F n.+1 a ^+ y)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n
forall (i : Graph.graph0 sequence_graph)
(x : fib_seq_to_seq B ((n.+1; a ^+).1; (n.+1; a ^+).2)
i),
(funw : Colimit
(fib_seq_to_seq B
((n.+1; a ^+).1; (n.+1; a ^+).2)) =>
F n a
(colim_succ_seq_to_colim_seq
(fib_seq_to_seq B (n; a)) w) =
transport E
(Delta (colimp n n.+11 a)
(fib_seq_to_type_fam_beta_glue B n a) w)
(F n.+1 a ^+ w))
(inj
(fib_seq_to_seq B
((n.+1; a ^+).1; (n.+1; a ^+).2)) i x)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j)
(x : fib_seq_to_seq B ((n.+1; a ^+).1; (n.+1; a ^+).2)
i),
transport
(funw : Colimit
(fib_seq_to_seq B
((n.+1; a ^+).1; (n.+1; a ^+).2)) =>
F n a
(colim_succ_seq_to_colim_seq
(fib_seq_to_seq B (n; a)) w) =
transport E
(Delta (colimp n n.+11 a)
(fib_seq_to_type_fam_beta_glue B n a) w)
(F n.+1 a ^+ w)) (colimp i j g x)
(?q j
(((fib_seq_to_seq B
((n.+1; a ^+).1; (n.+1; a ^+).2)) _f g) x)) =
?q i x
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n
forall (i : Graph.graph0 sequence_graph)
(x : fib_seq_to_seq B ((n.+1; a ^+).1; (n.+1; a ^+).2)
i),
(funw : Colimit
(fib_seq_to_seq B
((n.+1; a ^+).1; (n.+1; a ^+).2)) =>
F n a
(colim_succ_seq_to_colim_seq
(fib_seq_to_seq B (n; a)) w) =
transport E
(Delta (colimp n n.+11 a)
(fib_seq_to_type_fam_beta_glue B n a) w)
(F n.+1 a ^+ w))
(inj
(fib_seq_to_seq B
((n.+1; a ^+).1; (n.+1; a ^+).2)) i x)
exact (funkb => idpath).
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j)
(x : fib_seq_to_seq B ((n.+1; a ^+).1; (n.+1; a ^+).2)
i),
transport
(funw : Colimit
(fib_seq_to_seq B
((n.+1; a ^+).1; (n.+1; a ^+).2)) =>
F n a
(colim_succ_seq_to_colim_seq
(fib_seq_to_seq B (n; a)) w) =
transport E
(Delta (colimp n n.+11 a)
(fib_seq_to_type_fam_beta_glue B n a) w)
(F n.+1 a ^+ w)) (colimp i j g x)
((fun (k : Graph.graph0 sequence_graph)
(b : fib_seq_to_seq B
((n.+1; a ^+).1; (n.+1; a ^+).2) k) => 1)
j
(((fib_seq_to_seq B
((n.+1; a ^+).1; (n.+1; a ^+).2)) _f g) x)) =
(fun (k : Graph.graph0 sequence_graph)
(b : fib_seq_to_seq B
((n.+1; a ^+).1; (n.+1; a ^+).2) k) => 1) i
x
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n k: Graph.graph0 sequence_graph b: fib_seq_to_seq B ((n.+1; a ^+).1; (n.+1; a ^+).2)
k
transport
(funw : Colimit (fib_seq_to_seq B (n.+1; a ^+)) =>
F n a
(colim_succ_seq_to_colim_seq
(fib_seq_to_seq B (n; a)) w) =
transport E
(Delta (colimp n n.+11 a)
(fib_seq_to_type_fam_beta_glue B n a) w)
(F n.+1 a ^+ w)) (colimp k k.+11 b) 1 = 1
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n k: Graph.graph0 sequence_graph b: fib_seq_to_seq B ((n.+1; a ^+).1; (n.+1; a ^+).2)
k
apD (F n a) (colimp k.+1 k.+21 b) @ 1 =
(ap
(transport
(funx : fib_seq_to_type_fam B (inj A n a) =>
E (inj A n a; x)) (colimp k.+1 k.+21 b)) 1 @
Epsilon (glue A n a)
(colim_succ_seq_to_colim_seq_beta_glue
(fib_seq_to_seq B (n; a)) k b)
(F n.+1 a ^+
(inj (succ_seq (fib_seq_to_seq B (n; a))) k.+1
b ^+))) @
ap
(transport E
(Delta (glue A n a)
(fib_seq_to_type_fam_beta_glue B n a)
(inj (succ_seq (fib_seq_to_seq B (n; a))) k b)))
(apD (F n.+1 a ^+) (colimp k k.+11 b))
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n k: Graph.graph0 sequence_graph b: fib_seq_to_seq B ((n.+1; a ^+).1; (n.+1; a ^+).2)
k
R k.+1 n a b @ 1 =
(ap
(transport
(funx : fib_seq_to_type_fam B (inj A n a) =>
E (inj A n a; x)) (colimp k.+1 k.+21 b)) 1 @
Epsilon (colimp n n.+11 a)
(colim_succ_seq_to_colim_seq_beta_glue
(fib_seq_to_seq B (n; a)) k b)
(F n.+1 a ^+
(inj (succ_seq (fib_seq_to_seq B (n; a))) k.+1
b ^+))) @
ap
(transport E
(Delta (colimp n n.+11 a)
(fib_seq_to_type_fam_beta_glue B n a)
(inj (succ_seq (fib_seq_to_seq B (n; a))) k b)))
(apD (F n.+1 a ^+) (colimp k k.+11 b))
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n k: Graph.graph0 sequence_graph b: fib_seq_to_seq B ((n.+1; a ^+).1; (n.+1; a ^+).2)
k
R k.+1 n a b @ 1 =
(ap
(transport
(funx : fib_seq_to_type_fam B (inj A n a) =>
E (inj A n a; x)) (colimp k.+1 k.+21 b)) 1 @
Epsilon (colimp n n.+11 a)
(colim_succ_seq_to_colim_seq_beta_glue
(fib_seq_to_seq B (n; a)) k b)
(F n.+1 a ^+
(inj (succ_seq (fib_seq_to_seq B (n; a))) k.+1
b ^+))) @
ap
(transport E
(Delta (colimp n n.+11 a)
(fib_seq_to_type_fam_beta_glue B n a)
(inj (succ_seq (fib_seq_to_seq B (n; a))) k b)))
(R k n.+1 a ^+ b)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type x1, x2: X p: x1 = x2 F: Y x1 -> Y x2 psi: coe (ap Y p) = F G1: forally : Y x1, Z (x1; y) G2: forally : Y x2, Z (x2; y)
transport (funx : X => forally : Y x, Z (x; y)) p G1 =
G2 <~>
(forally : Y x1,
G2 (F y) = transport Z (Delta p psi y) (G1 y))
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type x1, x2: X p: x1 = x2 F: Y x1 -> Y x2 psi: coe (ap Y p) = F G1: forally : Y x1, Z (x1; y) G2: forally : Y x2, Z (x2; y)
transport (funx : X => forally : Y x, Z (x; y)) p G1 =
G2 <~>
(forally : Y x1,
G2 (F y) = transport Z (Delta p psi y) (G1 y))
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type x1: X G1, G2: forally : Y x1, Z (x1; y)
transport (funx : X => forally : Y x, Z (x; y)) 1 G1 =
G2 <~>
(forally : Y x1,
G2 (equiv_path (Y x1) (Y x1) (ap Y 1) y) =
transport Z (Delta 11 y) (G1 y))
exact (transitivity (equiv_path_inverse _ _) (equiv_apD10 _ _ _)).Defined.(** The alternative induction rule in curried form; corresponds to curried "G" in the paper. *)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b
forall (x : Colimit A) (y : fib_seq_to_type_fam B x),
E (x; y)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b
forall (x : Colimit A) (y : fib_seq_to_type_fam B x),
E (x; y)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n
transport
(funw : Colimit A =>
forally : fib_seq_to_type_fam B w, E (w; y))
(colimp n n.+11 a) (F n.+1 a ^+) = F n a
exact ((I (fib_seq_to_type_fam_beta_glue B n a))^-1 (G n a)).Defined.(** The computation rule for the alternative induction rule in curried form. *)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n
I (fib_seq_to_type_fam_beta_glue B n a)
(apD seq_colim_sum_ind_cur (glue A n a)) = G n a
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n
I (fib_seq_to_type_fam_beta_glue B n a)
(apD seq_colim_sum_ind_cur (glue A n a)) = G n a
apply moveR_equiv_M; srapply Colimit_ind_beta_colimp.Defined.(** The alternative induction rule; corresponds to "G" in the paper. *)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b
forallx : {x : _ & fib_seq_to_type_fam B x}, E x
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type G: forallx0 : {x : _ & Y x}, Z x0 x: X y1, y2: Y x z: {x : _ & Y x} p: y1 = y2 q1: z = (x; y1) q2: z = (x; y2) theta: q2 = q1 @ ap (exist Y x) p
apD (G o exist Y x) p =
(ap (transport (Z o exist Y x) p) (apD G q1)^ @
Eta theta (G z)) @ apD G q2
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type G: forallx0 : {x : _ & Y x}, Z x0 x: X y1, y2: Y x z: {x : _ & Y x} p: y1 = y2 q1: z = (x; y1) q2: z = (x; y2) theta: q2 = q1 @ ap (exist Y x) p
apD (G o exist Y x) p =
(ap (transport (Z o exist Y x) p) (apD G q1)^ @
Eta theta (G z)) @ apD G q2
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type G: forallx0 : {x : _ & Y x}, Z x0 x: X y1, y2: Y x z: {x : _ & Y x} p: y1 = y2 q1: z = (x; y1) q2: z = (x; y2)
forallx0 : q1 @ ap (exist Y x) p = q2,
(funy : q2 = q1 @ ap (exist Y x) p =>
apD (G o exist Y x) p =
(ap (transport (Z o exist Y x) p) (apD G q1)^ @
Eta y (G z)) @ apD G q2)
(equiv_path_inverse (q1 @ ap (exist Y x) p) q2 x0)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type G: forallx0 : {x : _ & Y x}, Z x0 x: X y1, y2: Y x z: {x : _ & Y x} p: y1 = y2 q1: z = (x; y1)
apD (funx0 : Y x => G (x; x0)) p =
(ap (transport (funx0 : Y x => Z (x; x0)) p)
(apD G q1)^ @
Eta
(equiv_path_inverse (q1 @ ap (exist Y x) p)
(q1 @ ap (exist Y x) p) 1) (G z)) @
apD G (q1 @ ap (exist Y x) p)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type G: forallx0 : {x : _ & Y x}, Z x0 x: X y1, y2: Y x p: y1 = y2
apD (funx0 : Y x => G (x; x0)) p =
(ap (transport (funx0 : Y x => Z (x; x0)) p)
(apD G (equiv_path_inverse (x; y1) (x; y1) 1))^ @
Eta
(equiv_path_inverse
(equiv_path_inverse (x; y1) (x; y1) 1 @
ap (exist Y x) p)
(equiv_path_inverse (x; y1) (x; y1) 1 @
ap (exist Y x) p) 1) (G (x; y1))) @
apD G
(equiv_path_inverse (x; y1) (x; y1) 1 @
ap (exist Y x) p)
destruct p; reflexivity.Defined.
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type x1, x2: X p: x1 = x2 F: Y x1 -> Y x2 G: forallz : {x : _ & Y x}, Z z psi: coe (ap Y p) = F q: forally : Y x1,
(funy0 : Y x2 => G (x2; y0)) (F y) =
transport Z (Delta p psi y)
((funy0 : Y x1 => G (x1; y0)) y) theta: I psi
(apD (fun (x : X) (y : Y x) => G (x; y)) p) =
q y: Y x1
apD G (Delta p psi y) = (q y)^
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b X: Type Y: X -> Type Z: {x : _ & Y x} -> Type x1, x2: X p: x1 = x2 F: Y x1 -> Y x2 G: forallz : {x : _ & Y x}, Z z psi: coe (ap Y p) = F q: forally : Y x1,
(funy0 : Y x2 => G (x2; y0)) (F y) =
transport Z (Delta p psi y)
((funy0 : Y x1 => G (x1; y0)) y) theta: I psi
(apD (fun (x : X) (y : Y x) => G (x; y)) p) =
q y: Y x1
apD G (Delta p psi y) = (q y)^
destruct p; destruct psi; destruct theta; reflexivity.Defined.(** The computation rule for the alternative induction rule. *)
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : B (n; a)),
apD seq_colim_sum_ind
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b))) = t n a b
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : B (n; a)),
apD seq_colim_sum_ind
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b))) = t n a b
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n b: B (n; a) h:= F_beta_glue n a b: apD (F n a)
(glue (fib_seq_to_seq B ((n; a).1; (n; a).2)) 0
b) = R 0 n a b
apD seq_colim_sum_ind
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b))) = t n a b
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n b: B (n; a) h: (ap
(transport
(funx0 : fib_seq_to_type_fam B (inj A n a)
=> E (inj A n a; x0)) (colimp 011 b))
(apD seq_colim_sum_ind
(Delta (colimp n n.+11 a)
(fib_seq_to_type_fam_beta_glue B n a)
(inj (fib_seq_to_seq B (n.+1; a ^+)) 0
b ^+)))^ @
Eta
(seq_colim_sum_to_sum_seq_colim_beta_glue B n a
b)
(seq_colim_sum_ind
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n.+1 (a; b) ^+)))) @
apD seq_colim_sum_ind
(ap (seq_colim_sum_to_sum_seq_colim B)
(colimp n n.+11 (a; b))) = R 0 n a b
apD seq_colim_sum_ind
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b))) = t n a b
H: Univalence A: Sequence B: FibSequence A E: {x : _ & fib_seq_to_type_fam B x} -> Type e: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
E
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n (a; b))) t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(e n.+1 a ^+ b ^+f) = e n a b n: Graph.graph0 sequence_graph a: A n b: B (n; a) h: (ap
(transport
(funx0 : fib_seq_to_type_fam B (inj A n a)
=> E (inj A n a; x0)) (colimp 011 b))
((G n a
(inj (fib_seq_to_seq B (n.+1; a ^+)) 0 b ^+))^)^ @
Eta
(seq_colim_sum_to_sum_seq_colim_beta_glue B n a
b)
(seq_colim_sum_ind
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n.+1 (a; b) ^+)))) @
apD seq_colim_sum_ind
(ap (seq_colim_sum_to_sum_seq_colim B)
(colimp n n.+11 (a; b))) = R 0 n a b
apD seq_colim_sum_ind
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b))) = t n a b
rewrite concat_1p in h; exact (cancelL _ _ _ h).Defined.EndSeqColimitSumInd.(** An alternative recursion principle for the sum of colimits; Lemma 5.3. *)SectionSeqColimitSumRec.Context `{Univalence} {A} (B : FibSequence A).ContextE (e : forallna, B (n;a) -> E).Context (t : forallna (b : B (n;a)), e n.+1 (a^+) (b^+f) = e n a b).
H: Univalence A: Sequence B: FibSequence A E: Type e: forall (n : Graph.graph0 sequence_graph)
(a : A n), B (n; a) -> E t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : B (n; a)), e n.+1 a ^+ b ^+f = e n a b
{x : _ & fib_seq_to_type_fam B x} -> E
H: Univalence A: Sequence B: FibSequence A E: Type e: forall (n : Graph.graph0 sequence_graph)
(a : A n), B (n; a) -> E t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : B (n; a)), e n.+1 a ^+ b ^+f = e n a b
{x : _ & fib_seq_to_type_fam B x} -> E
exact (seq_colim_sum_ind B _ e (funnab => transport_const _ _ @ t n a b)).Defined.
H: Univalence A: Sequence B: FibSequence A E: Type e: forall (n : Graph.graph0 sequence_graph)
(a : A n), B (n; a) -> E t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : B (n; a)), e n.+1 a ^+ b ^+f = e n a b
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
ap seq_colim_sum_rec
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b))) = t n a b
H: Univalence A: Sequence B: FibSequence A E: Type e: forall (n : Graph.graph0 sequence_graph)
(a : A n), B (n; a) -> E t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : B (n; a)), e n.+1 a ^+ b ^+f = e n a b
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a),
ap seq_colim_sum_rec
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b))) = t n a b
H: Univalence A: Sequence B: FibSequence A E: Type e: forall (n : Graph.graph0 sequence_graph)
(a : A n), B (n; a) -> E t: forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : B (n; a)), e n.+1 a ^+ b ^+f = e n a b n: Graph.graph0 sequence_graph a: A n b: (funa : A n => B (n; a)) a
apD seq_colim_sum_rec
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b))) =
transport_const
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
(seq_colim_sum_rec
(seq_colim_sum_to_sum_seq_colim B
(inj (sig_seq B) n.+1 (a; b) ^+))) @ t n a b
H: Univalence A: Sequence B: FibSequence A E: Type F, G: {x : _ & fib_seq_to_type_fam B x} -> E
F o seq_colim_sum_to_sum_seq_colim B ==
G o seq_colim_sum_to_sum_seq_colim B -> F == G
H: Univalence A: Sequence B: FibSequence A E: Type F, G: {x : _ & fib_seq_to_type_fam B x} -> E
F o seq_colim_sum_to_sum_seq_colim B ==
G o seq_colim_sum_to_sum_seq_colim B -> F == G
H: Univalence A: Sequence B: FibSequence A E: Type F, G: {x : _ & fib_seq_to_type_fam B x} -> E h: F o seq_colim_sum_to_sum_seq_colim B ==
G o seq_colim_sum_to_sum_seq_colim B n: Graph.graph0 sequence_graph a: A n b: (funa : A n => B (n; a)) a
transport
(funx : {x : _ & fib_seq_to_type_fam B x} =>
F x = G x)
(ap (seq_colim_sum_to_sum_seq_colim B)
(glue (sig_seq B) n (a; b)))
((fun (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a) =>
h (inj (sig_seq B) n (a; b))) n.+1 a ^+ b ^+f) =
(fun (n : Graph.graph0 sequence_graph) (a : A n)
(b : (funa0 : A n => B (n; a0)) a) =>
h (inj (sig_seq B) n (a; b))) n a b
srapply ((transport_compose _ _ _ _)^ @ _); exact (apD h (glue (sig_seq B) n (a;b))).Defined.(** The canonical map from the sequential colimit of Sigmas to the Sigma of sequential colimits is an equivalence; Theorem 5.1. *)
H: Univalence A: Sequence B: FibSequence A
IsEquiv (seq_colim_sum_to_sum_seq_colim B)
H: Univalence A: Sequence B: FibSequence A
IsEquiv (seq_colim_sum_to_sum_seq_colim B)
H: Univalence A: Sequence B: FibSequence A
{G
: {x : _ & fib_seq_to_type_fam B x} ->
GraphQuotient.GraphQuotient.GraphQuotient
(funab : {x : _ & sig_seq B x} =>
{x
: {x : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x.1 j}} &
((x.1 = a) *
(((x.2).1; ((sig_seq B) _f (x.2).2) (x.1).2) = b))%type})
&
(funx : Colimit (sig_seq B) =>
G (seq_colim_sum_to_sum_seq_colim B x)) == idmap}
H: Univalence A: Sequence B: FibSequence A L: {G
: {x : _ & fib_seq_to_type_fam B x} ->
GraphQuotient.GraphQuotient.GraphQuotient
(funab : {x : _ & sig_seq B x} =>
{x
: {x : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x.1 j}} &
(((funt : {x0 : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x0.1 j}}
=> t.1) x = a) *
((funt : {x0 : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x0.1 j}}
=>
((t.2).1;
((sig_seq B) _f (t.2).2) (t.1).2)) x = b))%type})
& G o seq_colim_sum_to_sum_seq_colim B == idmap}
IsEquiv (seq_colim_sum_to_sum_seq_colim B)
H: Univalence A: Sequence B: FibSequence A
{G
: {x : _ & fib_seq_to_type_fam B x} ->
GraphQuotient.GraphQuotient.GraphQuotient
(funab : {x : _ & sig_seq B x} =>
{x
: {x : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x.1 j}} &
((x.1 = a) *
(((x.2).1; ((sig_seq B) _f (x.2).2) (x.1).2) = b))%type})
&
(funx : Colimit (sig_seq B) =>
G (seq_colim_sum_to_sum_seq_colim B x)) == idmap}
forall (n : Graph.graph0 sequence_graph) (a : A n),
B (n; a) ->
GraphQuotient.GraphQuotient.GraphQuotient
(funa0b : {x : _ & sig_seq B x} =>
{x
: {x : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x.1 j}} &
((x.1 = a0) *
(((x.2).1; ((sig_seq B) _f (x.2).2) (x.1).2) = b))%type})
H: Univalence A: Sequence B: FibSequence A
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : B (n; a)), ?e n.+1 a ^+ b ^+f = ?e n a b
H: Univalence A: Sequence B: FibSequence A
forall (n : Graph.graph0 sequence_graph) (a : A n),
B (n; a) ->
GraphQuotient.GraphQuotient.GraphQuotient
(funa0b : {x : _ & sig_seq B x} =>
{x
: {x : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x.1 j}} &
((x.1 = a0) *
(((x.2).1; ((sig_seq B) _f (x.2).2) (x.1).2) = b))%type})
exact (funnab => inj (sig_seq B) n (a;b)).
H: Univalence A: Sequence B: FibSequence A
forall (n : Graph.graph0 sequence_graph) (a : A n)
(b : B (n; a)),
(fun (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : B (n0; a0)) => inj (sig_seq B) n0 (a0; b0))
n.+1 a ^+ b ^+f =
(fun (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : B (n0; a0)) => inj (sig_seq B) n0 (a0; b0)) n
a b
exact (funnab => glue (sig_seq B) n (a;b)).
H: Univalence A: Sequence B: FibSequence A
(funG : {x : _ & fib_seq_to_type_fam B x} ->
GraphQuotient.GraphQuotient.GraphQuotient
(funab : {x : _ & sig_seq B x} =>
{x
: {x : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x.1 j}} &
((x.1 = a) *
(((x.2).1;
((sig_seq B) _f (x.2).2) (x.1).2) = b))%type})
=>
(funx : Colimit (sig_seq B) =>
G (seq_colim_sum_to_sum_seq_colim B x)) == idmap)
(seq_colim_sum_rec B
(GraphQuotient.GraphQuotient.GraphQuotient
(funab : {x : _ & sig_seq B x} =>
{x
: {x : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x.1 j}} &
((x.1 = a) *
(((x.2).1; ((sig_seq B) _f (x.2).2) (x.1).2) =
b))%type}))
(fun (n : Graph.graph0 sequence_graph) (a : A n)
(b : B (n; a)) => inj (sig_seq B) n (a; b))
(fun (n : Graph.graph0 sequence_graph) (a : A n)
(b : B (n; a)) => glue (sig_seq B) n (a; b)))
H: Univalence A: Sequence B: FibSequence A
foralln : Graph.graph0 sequence_graph,
(funx : Colimit (sig_seq B) =>
seq_colim_sum_rec B
(GraphQuotient.GraphQuotient.GraphQuotient
(funab : {x : _ & sig_seq B x} =>
{x0
: {x0 : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x0.1 j}} &
((x0.1 = a) *
(((x0.2).1;
((sig_seq B) _f (x0.2).2) (x0.1).2) = b))%type}))
(fun (n0 : Graph.graph0 sequence_graph) (a : A n0)
(b : B (n0; a)) => inj (sig_seq B) n0 (a; b))
(fun (n0 : Graph.graph0 sequence_graph) (a : A n0)
(b : B (n0; a)) => glue (sig_seq B) n0 (a; b))
(seq_colim_sum_to_sum_seq_colim B x))
o inj (sig_seq B) n == idmap o inj (sig_seq B) n
H: Univalence A: Sequence B: FibSequence A
forall (n : Graph.graph0 sequence_graph)
(a : sig_seq B n),
ap
(funx : Colimit (sig_seq B) =>
seq_colim_sum_rec B
(GraphQuotient.GraphQuotient.GraphQuotient
(funa0b : {x : _ & sig_seq B x} =>
{x0
: {x0 : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x0.1 j}} &
((x0.1 = a0) *
(((x0.2).1;
((sig_seq B) _f (x0.2).2) (x0.1).2) = b))%type}))
(fun (n0 : Graph.graph0 sequence_graph)
(a0 : A n0) (b : B (n0; a0)) =>
inj (sig_seq B) n0 (a0; b))
(fun (n0 : Graph.graph0 sequence_graph)
(a0 : A n0) (b : B (n0; a0)) =>
glue (sig_seq B) n0 (a0; b))
(seq_colim_sum_to_sum_seq_colim B x))
(glue (sig_seq B) n a) @ ?h n a =
?h n.+1 a ^+ @ ap idmap (glue (sig_seq B) n a)
H: Univalence A: Sequence B: FibSequence A
foralln : Graph.graph0 sequence_graph,
(funx : Colimit (sig_seq B) =>
seq_colim_sum_rec B
(GraphQuotient.GraphQuotient.GraphQuotient
(funab : {x : _ & sig_seq B x} =>
{x0
: {x0 : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x0.1 j}} &
((x0.1 = a) *
(((x0.2).1;
((sig_seq B) _f (x0.2).2) (x0.1).2) = b))%type}))
(fun (n0 : Graph.graph0 sequence_graph) (a : A n0)
(b : B (n0; a)) => inj (sig_seq B) n0 (a; b))
(fun (n0 : Graph.graph0 sequence_graph) (a : A n0)
(b : B (n0; a)) => glue (sig_seq B) n0 (a; b))
(seq_colim_sum_to_sum_seq_colim B x))
o inj (sig_seq B) n == idmap o inj (sig_seq B) n
exact (funna => idpath).
H: Univalence A: Sequence B: FibSequence A
forall (n : Graph.graph0 sequence_graph)
(a : sig_seq B n),
ap
(funx : Colimit (sig_seq B) =>
seq_colim_sum_rec B
(GraphQuotient.GraphQuotient.GraphQuotient
(funa0b : {x : _ & sig_seq B x} =>
{x0
: {x0 : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x0.1 j}} &
((x0.1 = a0) *
(((x0.2).1;
((sig_seq B) _f (x0.2).2) (x0.1).2) = b))%type}))
(fun (n0 : Graph.graph0 sequence_graph)
(a0 : A n0) (b : B (n0; a0)) =>
inj (sig_seq B) n0 (a0; b))
(fun (n0 : Graph.graph0 sequence_graph)
(a0 : A n0) (b : B (n0; a0)) =>
glue (sig_seq B) n0 (a0; b))
(seq_colim_sum_to_sum_seq_colim B x))
(glue (sig_seq B) n a) @
(fun (n0 : Graph.graph0 sequence_graph)
(a0 : sig_seq B n0) => 1) n a =
(fun (n0 : Graph.graph0 sequence_graph)
(a0 : sig_seq B n0) => 1) n.+1 a ^+ @
ap idmap (glue (sig_seq B) n a)
H: Univalence A: Sequence B: FibSequence A n: Graph.graph0 sequence_graph a: sig_seq B n
ap
(seq_colim_sum_rec B
(GraphQuotient.GraphQuotient.GraphQuotient
(funab : {x : _ & sig_seq B x} =>
{x
: {x : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x.1 j}} &
((x.1 = a) *
(((x.2).1; ((sig_seq B) _f (x.2).2) (x.1).2) =
b))%type}))
(fun (n : Graph.graph0 sequence_graph) (a : A n)
(b : B (n; a)) => inj (sig_seq B) n (a; b))
(fun (n : Graph.graph0 sequence_graph) (a : A n)
(b : B (n; a)) => colimp n n.+11 (a; b)))
(ap (seq_colim_sum_to_sum_seq_colim B)
(colimp n n.+11 a)) = colimp n n.+11 a
rewrite seq_colim_sum_rec_beta_glue; reflexivity.
H: Univalence A: Sequence B: FibSequence A L: {G
: {x : _ & fib_seq_to_type_fam B x} ->
GraphQuotient.GraphQuotient.GraphQuotient
(funab : {x : _ & sig_seq B x} =>
{x
: {x : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x.1 j}} &
(((funt : {x0 : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x0.1 j}}
=> t.1) x = a) *
((funt : {x0 : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x0.1 j}}
=>
((t.2).1;
((sig_seq B) _f (t.2).2) (t.1).2)) x = b))%type})
& G o seq_colim_sum_to_sum_seq_colim B == idmap}
IsEquiv (seq_colim_sum_to_sum_seq_colim B)
H: Univalence A: Sequence B: FibSequence A L: {G
: {x : _ & fib_seq_to_type_fam B x} ->
GraphQuotient.GraphQuotient.GraphQuotient
(funab : {x : _ & sig_seq B x} =>
{x
: {x : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x.1 j}} &
(((funt : {x0 : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x0.1 j}}
=> t.1) x = a) *
((funt : {x0 : {x : _ & sig_seq B x} &
{j : Graph.graph0 sequence_graph &
Graph.graph1 sequence_graph x0.1 j}}
=>
((t.2).1;
((sig_seq B) _f (t.2).2) (t.1).2)) x = b))%type})
& G o seq_colim_sum_to_sum_seq_colim B == idmap}
(funx : {x : _ & fib_seq_to_type_fam B x} =>
seq_colim_sum_to_sum_seq_colim B (L.1 x))
o seq_colim_sum_to_sum_seq_colim B ==
idmap o seq_colim_sum_to_sum_seq_colim B
intro x; rewrite L.2; reflexivity.Defined.Definitionequiv_seq_colim_sum_to_sum_seq_colim `{Univalence} {A} (B : FibSequence A)
: Colimit (sig_seq B) <~> sig (fib_seq_to_type_fam B)
:= Build_Equiv _ _ _ (isequiv_seq_colim_sum_to_sum_seq_colim B).(** The canonical map from the sequential colimit of Sigmas to the Sigma of sequential colimits commutes with the first projection; Theorem 5.1. *)
H: Univalence A: Sequence B: FibSequence A
pr1 o seq_colim_sum_to_sum_seq_colim B ==
seq_colim_sum_to_seq_colim_fst B
H: Univalence A: Sequence B: FibSequence A
pr1 o seq_colim_sum_to_sum_seq_colim B ==
seq_colim_sum_to_seq_colim_fst B
H: Univalence A: Sequence B: FibSequence A
foralln : Graph.graph0 sequence_graph,
(funx : Colimit (sig_seq B) =>
(seq_colim_sum_to_sum_seq_colim B x).1)
o inj (sig_seq B) n ==
seq_colim_sum_to_seq_colim_fst B o inj (sig_seq B) n
H: Univalence A: Sequence B: FibSequence A
forall (n : Graph.graph0 sequence_graph)
(a : sig_seq B n),
ap
(funx : Colimit (sig_seq B) =>
(seq_colim_sum_to_sum_seq_colim B x).1)
(glue (sig_seq B) n a) @ ?h n a =
?h n.+1 a ^+ @
ap (seq_colim_sum_to_seq_colim_fst B)
(glue (sig_seq B) n a)
H: Univalence A: Sequence B: FibSequence A
foralln : Graph.graph0 sequence_graph,
(funx : Colimit (sig_seq B) =>
(seq_colim_sum_to_sum_seq_colim B x).1)
o inj (sig_seq B) n ==
seq_colim_sum_to_seq_colim_fst B o inj (sig_seq B) n
exact (funna => idpath).
H: Univalence A: Sequence B: FibSequence A
forall (n : Graph.graph0 sequence_graph)
(a : sig_seq B n),
ap
(funx : Colimit (sig_seq B) =>
(seq_colim_sum_to_sum_seq_colim B x).1)
(glue (sig_seq B) n a) @
(fun (n0 : Graph.graph0 sequence_graph)
(a0 : sig_seq B n0) => 1) n a =
(fun (n0 : Graph.graph0 sequence_graph)
(a0 : sig_seq B n0) => 1) n.+1 a ^+ @
ap (seq_colim_sum_to_seq_colim_fst B)
(glue (sig_seq B) n a)
H: Univalence A: Sequence B: FibSequence A n: Graph.graph0 sequence_graph a: A n b: B (n; a)
ap pr1
(legs_comm
{|
legs :=
fun (n : Graph.graph0 sequence_graph)
(X : sig_seq B n) =>
(inj A n X.1;
inj (fib_seq_to_seq B (n; X.1)) 0 X.2);
legs_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m)
(x : sig_seq B n) =>
match
p as p0 in (_ = n0)
return
((inj A n0
(((sig_seq B) _f p0) (x.1; x.2)).1;
inj
(fib_seq_to_seq B
(n0;
(((sig_seq B) _f p0) (x.1; x.2)).1))
0 (((sig_seq B) _f p0) (x.1; x.2)).2) =
(inj A n x.1;
inj (fib_seq_to_seq B (n; x.1)) 0 x.2))
with
| 1 =>
Delta (colimp n n.+11 x.1)
(fib_seq_to_type_fam_beta_glue B n x.1)
(inj
(fib_seq_to_seq B
(n.+1; ((x.1; x.2) ^+).1)) 0
((x.1; x.2) ^+).2) @
ap
(exist (fib_seq_to_type_fam B)
(inj A n x.1)) (colimp 011 x.2)
end
|} n n.+11 (a; b)) =
legs_comm
{|
legs :=
fun (n : Graph.graph0 sequence_graph)
(X : sig_seq B n) => inj A n X.1;
legs_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m)
(x : sig_seq B n) =>
match
p as p0 in (_ = n0)
return
(inj A n0 (((sig_seq B) _f p0) (x.1; x.2)).1 =
inj A n x.1)
with
| 1 => colimp n n.+11 x.1end
|} n n.+11 (a; b)
H: Univalence A: Sequence B: FibSequence A n: Graph.graph0 sequence_graph a: A n b: B (n; a)
colimp n n.+11 a @
ap pr1
(ap (exist (fib_seq_to_type_fam B) (inj A n a))
(colimp 011 b)) =
legs_comm
{|
legs :=
fun (n : Graph.graph0 sequence_graph)
(X : sig_seq B n) => inj A n X.1;
legs_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m)
(x : sig_seq B n) =>
match
p as p0 in (_ = n0)
return
(inj A n0 (((sig_seq B) _f p0) (x.1; x.2)).1 =
inj A n x.1)
with
| 1 => colimp n n.+11 x.1end
|} n n.+11 (a; b)
H: Univalence A: Sequence B: FibSequence A n: Graph.graph0 sequence_graph a: A n b: B (n; a)
ap
(fun_ : Colimit (fib_seq_to_seq B (n; a)) =>
inj A n a) (colimp 011 b) = 1
rewrite ap_const; reflexivity.Defined.(** The characterization of path spaces in sequential colimits; Theorem 7.4, first part. *)Definitionpath_seq (A : Sequence) (a1a2 : A 0)
:= Build_Sequence (funk => a1^+k = a2^+k) (funkp => ap (funa => a^+) p).
H: Univalence A: Sequence a1, a2: A 0
inj A 0 a1 = inj A 0 a2 <~> Colimit (path_seq A a1 a2)
H: Univalence A: Sequence a1, a2: A 0
inj A 0 a1 = inj A 0 a2 <~> Colimit (path_seq A a1 a2)
H: Univalence A: Sequence a1, a2: A 0 B:= {|
fibSequence :=
funx : {x : _ & A x} => a1 ^+ (x.1) = x.2;
fibSequenceArr :=
funx : {x : _ & A x} =>
ap (funa : A x.1 => a ^+)
|}: FibSequence A
inj A 0 a1 = inj A 0 a2 <~> Colimit (path_seq A a1 a2)
H: Univalence A: Sequence a1, a2: A 0 B:= {|
fibSequence :=
funx : {x : _ & A x} => a1 ^+ (x.1) = x.2;
fibSequenceArr :=
funx : {x : _ & A x} =>
ap (funa : A x.1 => a ^+)
|}: FibSequence A
inj A 0 a1 = inj A 0 a2 <~>
fib_seq_to_type_fam B (inj A 0 a2)
H: Univalence A: Sequence a1, a2: A 0 B:= {|
fibSequence :=
funx : {x : _ & A x} => a1 ^+ (x.1) = x.2;
fibSequenceArr :=
funx : {x : _ & A x} =>
ap (funa : A x.1 => a ^+)
|}: FibSequence A
fib_seq_to_type_fam B (inj A 0 a2) <~>
Colimit (path_seq A a1 a2)
H: Univalence A: Sequence a1, a2: A 0 B:= {|
fibSequence :=
funx : {x : _ & A x} => a1 ^+ (x.1) = x.2;
fibSequenceArr :=
funx : {x : _ & A x} =>
ap (funa : A x.1 => a ^+)
|}: FibSequence A
inj A 0 a1 = inj A 0 a2 <~>
fib_seq_to_type_fam B (inj A 0 a2)
H: Univalence A: Sequence a1, a2: A 0 B:= {|
fibSequence :=
funx : {x : _ & A x} => a1 ^+ (x.1) = x.2;
fibSequenceArr :=
funx : {x : _ & A x} =>
ap (funa : A x.1 => a ^+)
|}: FibSequence A
fib_seq_to_type_fam B (inj A 0 a1)
H: Univalence A: Sequence a1, a2: A 0 B:= {|
fibSequence :=
funx : {x : _ & A x} => a1 ^+ (x.1) = x.2;
fibSequenceArr :=
funx : {x : _ & A x} =>
ap (funa : A x.1 => a ^+)
|}: FibSequence A
Contr {y : Colimit A & fib_seq_to_type_fam B y}
H: Univalence A: Sequence a1, a2: A 0 B:= {|
fibSequence :=
funx : {x : _ & A x} => a1 ^+ (x.1) = x.2;
fibSequenceArr :=
funx : {x : _ & A x} =>
ap (funa : A x.1 => a ^+)
|}: FibSequence A
fib_seq_to_type_fam B (inj A 0 a1)
exact (inj (fib_seq_to_seq B (0;a1)) 0 idpath).
H: Univalence A: Sequence a1, a2: A 0 B:= {|
fibSequence :=
funx : {x : _ & A x} => a1 ^+ (x.1) = x.2;
fibSequenceArr :=
funx : {x : _ & A x} =>
ap (funa : A x.1 => a ^+)
|}: FibSequence A
Contr {y : Colimit A & fib_seq_to_type_fam B y}
H: Univalence A: Sequence a1, a2: A 0 B:= {|
fibSequence :=
funx : {x : _ & A x} => a1 ^+ (x.1) = x.2;
fibSequenceArr :=
funx : {x : _ & A x} =>
ap (funa : A x.1 => a ^+)
|}: FibSequence A
H: Univalence A: Sequence a1, a2: A 0 B:= {|
fibSequence :=
funx : {x : _ & A x} => a1 ^+ (x.1) = x.2;
fibSequenceArr :=
funx : {x : _ & A x} =>
ap (funa : A x.1 => a ^+)
|}: FibSequence A
DiagramMap (fib_seq_to_seq' B (0; a2))
(path_seq A a1 a2)
H: Univalence A: Sequence a1, a2: A 0 B:= {|
fibSequence :=
funx : {x : _ & A x} => a1 ^+ (x.1) = x.2;
fibSequenceArr :=
funx : {x : _ & A x} =>
ap (funa : A x.1 => a ^+)
|}: FibSequence A
foralli : Graph.graph0 sequence_graph,
fib_seq_to_seq' B (0; a2) i -> path_seq A a1 a2 i
H: Univalence A: Sequence a1, a2: A 0 B:= {|
fibSequence :=
funx : {x : _ & A x} => a1 ^+ (x.1) = x.2;
fibSequenceArr :=
funx : {x : _ & A x} =>
ap (funa : A x.1 => a ^+)
|}: FibSequence A
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j)
(x : fib_seq_to_seq' B (0; a2) i),
((path_seq A a1 a2) _f g) (?DiagramMap_obj i x) =
?DiagramMap_obj j
(((fib_seq_to_seq' B (0; a2)) _f g) x)
H: Univalence A: Sequence a1, a2: A 0 B:= {|
fibSequence :=
funx : {x : _ & A x} => a1 ^+ (x.1) = x.2;
fibSequenceArr :=
funx : {x : _ & A x} =>
ap (funa : A x.1 => a ^+)
|}: FibSequence A
foralli : Graph.graph0 sequence_graph,
fib_seq_to_seq' B (0; a2) i -> path_seq A a1 a2 i
exact (funn => coe (ap B (seq_shift_pair_from_zero a2 n))).
H: Univalence A: Sequence a1, a2: A 0 B:= {|
fibSequence :=
funx : {x : _ & A x} => a1 ^+ (x.1) = x.2;
fibSequenceArr :=
funx : {x : _ & A x} =>
ap (funa : A x.1 => a ^+)
|}: FibSequence A
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j)
(x : fib_seq_to_seq' B (0; a2) i),
((path_seq A a1 a2) _f g)
((funn : Graph.graph0 sequence_graph =>
coe (ap B (seq_shift_pair_from_zero a2 n))) i x) =
(funn : Graph.graph0 sequence_graph =>
coe (ap B (seq_shift_pair_from_zero a2 n))) j
(((fib_seq_to_seq' B (0; a2)) _f g) x)
intros n m p b; destruct p; srapply (K _ _ (seq_shift_pair_from_zero a2 n)).
H: Univalence A: Sequence a1, a2: A 0 B:= {|
fibSequence :=
funx : {x : _ & A x} => a1 ^+ (x.1) = x.2;
fibSequenceArr :=
funx : {x : _ & A x} =>
ap (funa : A x.1 => a ^+)
|}: FibSequence A
foralli : Graph.graph0 sequence_graph,
IsEquiv
({|
DiagramMap_obj :=
funn : Graph.graph0 sequence_graph =>
coe (ap B (seq_shift_pair_from_zero a2 n));
DiagramMap_comm :=
fun (nm : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n m)
(b : fib_seq_to_seq' B (0; a2) n) =>
match
p as p0 in (_ = n0)
return
(((path_seq A a1 a2) _f p0)
(equiv_path (B (0; a2) ^++ n)
(B (n; a2 ^+ n))
(ap B (seq_shift_pair_from_zero a2 n))
b) =
equiv_path (B (0; a2) ^++ n0)
(B (n0; a2 ^+ n0))
(ap B (seq_shift_pair_from_zero a2 n0))
(((fib_seq_to_seq' B (0; a2)) _f p0) b))
with
| 1 =>
K seq_pair_shift (fibSequenceArr B)
(seq_shift_pair_from_zero a2 n)
end
|} i)
exact _.Defined.(** The characterization of path spaces in sequential colimits; Theorem 7.4, second part. *)
H: Univalence A: Sequence n: Graph.graph0 sequence_graph a1, a2: A n
inj A n a1 = inj A n a2 <~>
Colimit (path_seq (shift_seq A n) a1 a2)
H: Univalence A: Sequence n: Graph.graph0 sequence_graph a1, a2: A n
inj A n a1 = inj A n a2 <~>
Colimit (path_seq (shift_seq A n) a1 a2)
H: Univalence A: Sequence n: Graph.graph0 sequence_graph a1, a2: A n
inj (shift_seq A n) 0 a1 = inj (shift_seq A n) 0 a2 <~>
inj A n a1 = inj A n a2
srapply (@equiv_ap _ _ (colim_shift_seq_to_colim_seq A n)).Defined.Open Scope trunc_scope.(** Corollary 7.7.1, second part. *)
H: Univalence A: Sequence k: trunc_index
(foralln : Graph.graph0 sequence_graph,
IsTrunc k (A n)) -> IsTrunc k (Colimit A)
H: Univalence A: Sequence k: trunc_index
(foralln : Graph.graph0 sequence_graph,
IsTrunc k (A n)) -> IsTrunc k (Colimit A)
H: Univalence
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, Contr (A n)) ->
Contr (Colimit A)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A)
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) -> IsTrunc k.+1 (Colimit A)
H: Univalence
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, Contr (A n)) ->
Contr (Colimit A)
exact contr_colim_contr_seq.
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A)
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) -> IsTrunc k.+1 (Colimit A)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) A: Sequence trH: foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n)
forall (i : Graph.graph0 sequence_graph) (x : A i),
(funw : Colimit A =>
forally : Colimit A, IsTrunc k (w = y)) (inj A i x)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) A: Sequence trH: foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n)
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j) (x : A i),
transport
(funw : Colimit A =>
forally : Colimit A, IsTrunc k (w = y))
(colimp i j g x) (?q j ((A _f g) x)) = ?q i x
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) A: Sequence trH: foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n)
forall (i : Graph.graph0 sequence_graph) (x : A i),
(funw : Colimit A =>
forally : Colimit A, IsTrunc k (w = y)) (inj A i x)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A)
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forall (x : A 0%nat) (y : Colimit A),
IsTrunc k (inj A 0%nat x = y)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) n: nat IHn: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n)) ->
forall (x : A n) (y : Colimit A), IsTrunc k (inj A n x = y)
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forall (x : A n.+1%nat) (y : Colimit A),
IsTrunc k (inj A n.+1%nat x = y)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A)
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forall (x : A 0%nat) (y : Colimit A),
IsTrunc k (inj A 0%nat x = y)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) A: Sequence trH: foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n) a: A 0%nat
forall (i : Graph.graph0 sequence_graph) (x : A i),
(funw : Colimit A => IsTrunc k (inj A 0%nat a = w))
(inj A i x)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) A: Sequence trH: foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n) a: A 0%nat
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j) (x : A i),
transport
(funw : Colimit A => IsTrunc k (inj A 0%nat a = w))
(colimp i j g x) (?q j ((A _f g) x)) = ?q i x
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) A: Sequence trH: foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n) a: A 0%nat
forall (i : Graph.graph0 sequence_graph) (x : A i),
(funw : Colimit A => IsTrunc k (inj A 0%nat a = w))
(inj A i x)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A)
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forallab : A 0%nat,
IsTrunc k (inj A 0%nat a = inj A 0%nat b)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) m: nat IHm: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b : A m), IsTrunc k (inj A 0%nat a = inj A m b)
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b : A m.+1%nat),
IsTrunc k (inj A 0%nat a = inj A m.+1%nat b)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A)
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forallab : A 0%nat,
IsTrunc k (inj A 0%nat a = inj A 0%nat b)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) A: Sequence trH: foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n) a, b: A 0%nat
IsTrunc k (inj A 0%nat a = inj A 0%nat b)
exact (istrunc_equiv_istrunc _ (equiv_inverse (equiv_path_colim _ a b))).
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) m: nat IHm: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b : A m), IsTrunc k (inj A 0%nat a = inj A m b)
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b : A m.+1%nat),
IsTrunc k (inj A 0%nat a = inj A m.+1%nat b)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) m: nat IHm: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b : A m), IsTrunc k (inj A 0%nat a = inj A m b)
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b : A m.+1%nat),
IsTrunc k (inj A 0%nat a = inj A m.+1%nat b)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) m: nat IHm: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b : A m), IsTrunc k (inj A 0%nat a = inj A m b) A: Sequence trH: foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n) a: A 0%nat b: A m.+1%nat
IsTrunc k (inj A 0%nat a = inj A m.+1%nat b)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) m: nat IHm: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b : A m), IsTrunc k (inj A 0%nat a = inj A m b) A: Sequence trH: foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n) a: A 0%nat b: A m.+1%nat
IsTrunc k (inj A 1%nat a ^+ = inj A m.+1%nat b)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) m: nat IHm: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b : A m), IsTrunc k (inj A 0%nat a = inj A m b) A: Sequence trH: foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n) a: A 0%nat b: A m.+1%nat
inj (succ_seq A) 0%nat a ^+ = inj (succ_seq A) m b <~>
inj A 1%nat a ^+ = inj A m.+1%nat b
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) A: Sequence trH: foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n) a: A 0%nat
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j) (x : A i),
transport
(funw : Colimit A => IsTrunc k (inj A 0%nat a = w))
(colimp i j g x)
((fun (m : Graph.graph0 sequence_graph) (b : A m) =>
nat_rect
(funm0 : nat =>
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b0 : A m0),
IsTrunc k (inj A 0%nat a = inj A m0 b0))
(fun (A : Sequence)
(trH : foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) (ab0 : A 0%nat)
=>
istrunc_equiv_istrunc
(Colimit (path_seq (shift_seq A 0) a b0))
(equiv_path_colim 0%nat a b0)^-1)
(fun (m0 : nat)
(IHm : forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b0 : A m0),
IsTrunc k
(inj A 0%nat a = inj A m0 b0))
(A : Sequence)
(trH : foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) (a : A 0%nat)
(b0 : A m0.+1%nat) =>
istrunc_equiv_istrunc
(inj A 1%nat a ^+ = inj A m0.+1%nat b0)
(equiv_concat_l (glue A 0%nat a)
(inj A m0.+1%nat b0))^-1) m A trH a b) j
((A _f g) x)) =
(fun (m : Graph.graph0 sequence_graph) (b : A m) =>
nat_rect
(funm0 : nat =>
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b0 : A m0),
IsTrunc k (inj A 0%nat a = inj A m0 b0))
(fun (A : Sequence)
(trH : foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) (ab0 : A 0%nat) =>
istrunc_equiv_istrunc
(Colimit (path_seq (shift_seq A 0) a b0))
(equiv_path_colim 0%nat a b0)^-1)
(fun (m0 : nat)
(IHm : forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b0 : A m0),
IsTrunc k (inj A 0%nat a = inj A m0 b0))
(A : Sequence)
(trH : foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) (a : A 0%nat)
(b0 : A m0.+1%nat) =>
istrunc_equiv_istrunc
(inj A 1%nat a ^+ = inj A m0.+1%nat b0)
(equiv_concat_l (glue A 0%nat a)
(inj A m0.+1%nat b0))^-1) m A trH a b) i x
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) A: Sequence trH: foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n) a: A 0%nat
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j) (x : A i),
transport
(funw : Colimit A => IsTrunc k (inj A 0%nat a = w))
(colimp i j g x)
((fun (m : Graph.graph0 sequence_graph) (b : A m) =>
nat_rect
(funm0 : nat =>
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b0 : A m0),
IsTrunc k (inj A 0%nat a = inj A m0 b0))
(fun (A : Sequence)
(trH : foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) (ab0 : A 0%nat)
=>
istrunc_equiv_istrunc
(Colimit (path_seq (shift_seq A 0) a b0))
(equiv_path_colim 0%nat a b0)^-1)
(fun (m0 : nat)
(IHm : forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b0 : A m0),
IsTrunc k
(inj A 0%nat a = inj A m0 b0))
(A : Sequence)
(trH : foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) (a : A 0%nat)
(b0 : A m0.+1%nat) =>
istrunc_equiv_istrunc
(inj A 1%nat a ^+ = inj A m0.+1%nat b0)
(equiv_concat_l (glue A 0%nat a)
(inj A m0.+1%nat b0))^-1) m A trH a b) j
((A _f g) x)) =
(fun (m : Graph.graph0 sequence_graph) (b : A m) =>
nat_rect
(funm0 : nat =>
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b0 : A m0),
IsTrunc k (inj A 0%nat a = inj A m0 b0))
(fun (A : Sequence)
(trH : foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) (ab0 : A 0%nat) =>
istrunc_equiv_istrunc
(Colimit (path_seq (shift_seq A 0) a b0))
(equiv_path_colim 0%nat a b0)^-1)
(fun (m0 : nat)
(IHm : forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forall (a : A 0%nat) (b0 : A m0),
IsTrunc k (inj A 0%nat a = inj A m0 b0))
(A : Sequence)
(trH : foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) (a : A 0%nat)
(b0 : A m0.+1%nat) =>
istrunc_equiv_istrunc
(inj A 1%nat a ^+ = inj A m0.+1%nat b0)
(equiv_concat_l (glue A 0%nat a)
(inj A m0.+1%nat b0))^-1) m A trH a b) i x
intros n m p b; snapply path_ishprop; snapply ishprop_istrunc; exact _.}
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) n: nat IHn: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n)) ->
forall (x : A n) (y : Colimit A), IsTrunc k (inj A n x = y)
forallA : Sequence,
(foralln : Graph.graph0 sequence_graph,
IsTrunc k.+1 (A n)) ->
forall (x : A n.+1%nat) (y : Colimit A),
IsTrunc k (inj A n.+1%nat x = y)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) n: nat IHn: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n)) ->
forall (x : A n) (y : Colimit A), IsTrunc k (inj A n x = y) A: Sequence trH: foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n) a: A n.+1%nat
foralla0 : Colimit (succ_seq A),
(funb : Colimit A => IsTrunc k (inj A n.+1%nat a = b))
(colim_succ_seq_to_colim_seq A a0)
intro x; srapply (@istrunc_equiv_istrunc _ _ _ k (IHn (succ_seq A) _ a x)); srapply equiv_ap.
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) A: Sequence trH: foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n)
H: Univalence k: trunc_index IHk: forallA : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A n)) ->
IsTrunc k (Colimit A) A: Sequence trH: foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n) n, m: Graph.graph0 sequence_graph p: Graph.graph1 sequence_graph n m a: A n
foralla0 : Colimit A,
IsHProp
((funa1 : Colimit A => IsTrunc k (inj A n a = a1))
a0)