Built with Alectryon. 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. *)From HoTT Require Import Basics.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) <~>
{H0 : foralli : Graph.graph0 sequence_graph, A i -> P &
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
(funx : A i => H0 j ((A _f g) x)) == H0 i}
H: Funext A: Sequence P: Type IsHProp0: IsHProp P
{H0 : foralli : Graph.graph0 sequence_graph, A i -> P &
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
(funx : A i => H0 j ((A _f g) x)) == H0 i} <~>
(foralln : Graph.graph0 sequence_graph, A n -> P)
H: Funext A: Sequence P: Type IsHProp0: IsHProp P
{H0 : foralli : Graph.graph0 sequence_graph, A i -> P &
forall (ij : Graph.graph0 sequence_graph)
(g : Graph.graph1 sequence_graph i j),
(funx : A i => H0 j ((A _f g) x)) == H0 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: foralln0 : Graph.graph0 sequence_graph, A n0 H: foralln0 : nat, const (a n0.+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: foralln0 : Graph.graph0 sequence_graph, A n0 H: foralln0 : nat, const (a n0.+1) == A _f 1 B:= Build_Sequence A (funn0 : nat => const (a n0.+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: foralln0 : Graph.graph0 sequence_graph, A n0 H: foralln0 : nat, const (a n0.+1) == A _f 1 B:= Build_Sequence A (funn0 : nat => const (a n0.+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: foralln0 : Graph.graph0 sequence_graph, A n0 H: foralln0 : nat, const (a n0.+1) == A _f 1 B:= Build_Sequence A (funn0 : nat => const (a n0.+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: foralln0 : Graph.graph0 sequence_graph, A n0 H: foralln0 : nat, const (a n0.+1) == A _f 1 B:= Build_Sequence A (funn0 : nat => const (a n0.+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: forallx0 : B i, colim 1 (a 1) = colim i x0
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: forallx0 : B i, colim 1 (a 1) = colim i x0
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: forallx0 : B i, colim 1 (a 1) = colim i x0
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: forallx0 : B i, colim 1 (a 1) = colim i x0
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: forallx0 : B i, colim 1 (a 1) = colim i x0
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: foralln0 : Graph.graph0 sequence_graph, A n0 H: foralln0 : nat, const (a n0.+1) == A _f 1 B:= Build_Sequence A (funn0 : nat => const (a n0.+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 => forallx0 : B i, colim 1 (a 1) = colim i x0)
(funx0 : B 0 => colimp 011 x0)
(fun (i : nat) (IHi : forallx0 : B i, colim 1 (a 1) = colim i x0)
(x0 : 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 x0)))
n.+1 x ^+) =
nat_rect (funi : nat => forallx0 : B i, colim 1 (a 1) = colim i x0)
(funx0 : B 0 => colimp 011 x0)
(fun (i : nat) (IHi : forallx0 : B i, colim 1 (a 1) = colim i x0)
(x0 : 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 x0)))
n x
funext: Funext A: Sequence a: foralln0 : Graph.graph0 sequence_graph, A n0 H: foralln0 : nat, const (a n0.+1) == A _f 1 B:= Build_Sequence A (funn0 : nat => const (a n0.+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 => forallx0 : B i, colim 1 (a 1) = colim i x0)
(funx0 : B 0 => colimp 011 x0)
(fun (i : nat) (IHi : forallx0 : B i, colim 1 (a 1) = colim i x0)
(x0 : 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 x0)))
n.+1 x ^+) @
ap idmap (colimp n n.+11 x) =
nat_rect (funi : nat => forallx0 : B i, colim 1 (a 1) = colim i x0)
(funx0 : B 0 => colimp 011 x0)
(fun (i : nat) (IHi : forallx0 : B i, colim 1 (a 1) = colim i x0)
(x0 : 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 x0)))
n x
funext: Funext A: Sequence a: foralln0 : Graph.graph0 sequence_graph, A n0 H: foralln0 : nat, const (a n0.+1) == A _f 1 B:= Build_Sequence A (funn0 : nat => const (a n0.+1)): Sequence n, m: Graph.graph0 sequence_graph x: B n
(1^ @
nat_rect (funi : nat => forallx0 : B i, colim 1 (a 1) = colim i x0)
(funx0 : B 0 => colimp 011 x0)
(fun (i : nat) (IHi : forallx0 : B i, colim 1 (a 1) = colim i x0)
(x0 : 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 x0)))
n.+1 x ^+) @
ap idmap (colimp n n.+11 x) =
nat_rect (funi : nat => forallx0 : B i, colim 1 (a 1) = colim i x0)
(funx0 : B 0 => colimp 011 x0)
(fun (i : nat) (IHi : forallx0 : B i, colim 1 (a 1) = colim i x0)
(x0 : 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 x0)))
n x
funext: Funext A: Sequence a: foralln0 : Graph.graph0 sequence_graph, A n0 H: foralln0 : nat, const (a n0.+1) == A _f 1 B:= Build_Sequence A (funn0 : nat => const (a n0.+1)): Sequence n, m: Graph.graph0 sequence_graph x: B n
(1^ @
nat_rect (funi : nat => forallx0 : B i, colim 1 (a 1) = colim i x0)
(funx0 : B 0 => colimp 011 x0)
(fun (i : nat) (IHi : forallx0 : B i, colim 1 (a 1) = colim i x0)
(x0 : 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 x0)))
n.+1 x ^+) @
colimp n n.+11 x =
nat_rect (funi : nat => forallx0 : B i, colim 1 (a 1) = colim i x0)
(funx0 : B 0 => colimp 011 x0)
(fun (i : nat) (IHi : forallx0 : B i, colim 1 (a 1) = colim i x0)
(x0 : 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 x0)))
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: foralln0 : Graph.graph0 sequence_graph, F o inj A n0 == G o inj A n0 H: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0),
ap F (glue A n0 a0) @ h n0 a0 = h n0.+1 a0 ^+ @ ap G (glue A n0 a0) 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: foralln0 : Graph.graph0 sequence_graph, F o inj A n0 == G o inj A n0 H: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0),
ap F (glue A n0 a0) @ h n0 a0 = h n0.+1 a0 ^+ @ ap G (glue A n0 a0) 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 ((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
|} 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 ((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
|} 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 (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)
(a0 : 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 => colimp n0 n0.+11 a0 ^+
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 (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)
(a0 : 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 => colimp n0 n0.+11 a0 ^+
end
|})
(legs_comm
{|
legs :=
fun (n0 : Graph.graph0 sequence_graph) (a0 : succ_seq A n0) =>
inj A n0.+1 a0;
legs_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m) =>
match
p as p0 in (_ = n1)
return
((funx : succ_seq A n0 => inj A n1.+1 (((succ_seq A) _f p0) x)) ==
(funa0 : succ_seq A n0 => inj A n0.+1 a0))
with
| 1 => colimp n0.+1 n0.+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) (y0 : Y x), I (F x) (G x y0) = I x y0
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) (y0 : Y x), I (F x) (G x y0) = I x y0
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) (y0 : Y x), I (F x) (G x y0) = I x y0
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) (y0 : Y x), I (F x) (G x y0) = I x y0
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 (A (k0 + 0)) (A k0)
(ap A (nat_add_zero_r k0)) 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 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 (A (k0 + 0)) (A k0)
(ap A (nat_add_zero_r k0)) 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 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 (n0 : nat) (a0 : A n0) => 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 (n0 : nat) (a0 : A n0) => 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 (n1 : nat) (a0 : A n1) => 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 (shift_seq A n)) _f p0)
(equiv_path (A (k + n.+1))
(A (k + n).+1) (ap A (nat_add_succ_r k n)) a0) =
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) a0))
with
| 1 =>
K S (fun (n1 : nat) (a1 : A n1) => 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 (n1 : nat) (a0 : A n1) => 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
(((succ_seq (shift_seq A n)) _f p0)
(equiv_path (A (k0 + n.+1)) (A (k0 + n).+1)
(ap A (nat_add_succ_r k0 n)) a0) =
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) a0))
with
| 1 =>
K S (fun (n1 : nat) (a1 : A n1) => 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
(((succ_seq (shift_seq A n)) _f p0)
(equiv_path (A (k0 + n.+1)) (A (k0 + n).+1)
(ap A (nat_add_succ_r k0 n)) a0) =
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) a0))
with
| 1 =>
K S (fun (n1 : nat) (a1 : A n1) => 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 (shift_seq A n)) _f p0)
(equiv_path (A (k + n.+1))
(A (k + n).+1) (ap A (nat_add_succ_r k n)) a0) =
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) a0))
with
| 1 =>
K S (fun (n1 : nat) (a1 : A n1) => 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 :=
funk0 : nat => transport idmap (ap A (nat_add_succ_r k0 n));
DiagramMap_comm :=
fun (k0l : nat) (p : k0.+1 = l) (a0 : A (k0 + n.+1)) =>
match
p as p0 in (_ = n0)
return
(match
p0 in (_ = n1) return (A (k0 + n).+1 -> A (n1 + n).+1)
with
| 1 => funa1 : A (k0 + n).+1 => a1 ^+
end (transport idmap (ap A (nat_add_succ_r k0 n)) a0) =
transport idmap (ap A (nat_add_succ_r n0 n))
(match
p0 in (_ = n1)
return (A (k0 + n.+1) -> A (n1 + n.+1))
with
| 1 => funa1 : A (k0 + n.+1) => a1 ^+
end a0))
with
| 1 =>
K S (fun (n0 : nat) (a1 : A n0) => a1 ^+)
(nat_add_succ_r k0 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 :=
funk0 : nat => transport idmap (ap A (nat_add_succ_r k0 n));
DiagramMap_comm :=
fun (k0l : nat) (p : k0.+1 = l) (a0 : A (k0 + n.+1)) =>
match
p as p0 in (_ = n0)
return
(match
p0 in (_ = n1) return (A (k0 + n).+1 -> A (n1 + n).+1)
with
| 1 => funa1 : A (k0 + n).+1 => a1 ^+
end (transport idmap (ap A (nat_add_succ_r k0 n)) a0) =
transport idmap (ap A (nat_add_succ_r n0 n))
(match
p0 in (_ = n1)
return (A (k0 + n.+1) -> A (n1 + n.+1))
with
| 1 => funa1 : A (k0 + n.+1) => a1 ^+
end a0))
with
| 1 =>
K S (fun (n0 : nat) (a1 : A n0) => a1 ^+)
(nat_add_succ_r k0 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 :=
funk0 : nat => transport idmap (ap A (nat_add_succ_r k0 n));
DiagramMap_comm :=
fun (k0l : nat) (p : k0.+1 = l) (a0 : A (k0 + n.+1)) =>
match
p as p0 in (_ = n0)
return
(match
p0 in (_ = n1) return (A (k0 + n).+1 -> A (n1 + n).+1)
with
| 1 => funa1 : A (k0 + n).+1 => a1 ^+
end (transport idmap (ap A (nat_add_succ_r k0 n)) a0) =
transport idmap (ap A (nat_add_succ_r n0 n))
(match
p0 in (_ = n1)
return (A (k0 + n.+1) -> A (n1 + n.+1))
with
| 1 => funa1 : A (k0 + n.+1) => a1 ^+
end a0))
with
| 1 =>
K S (fun (n0 : nat) (a1 : A n0) => a1 ^+)
(nat_add_succ_r k0 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 :=
funk0 : nat => transport idmap (ap A (nat_add_succ_r k0 n));
DiagramMap_comm :=
fun (k0l : nat) (p : k0.+1 = l) (a0 : A (k0 + n.+1)) =>
match
p as p0 in (_ = n0)
return
(match
p0 in (_ = n1) return (A (k0 + n).+1 -> A (n1 + n).+1)
with
| 1 => funa1 : A (k0 + n).+1 => a1 ^+
end (transport idmap (ap A (nat_add_succ_r k0 n)) a0) =
transport idmap (ap A (nat_add_succ_r n0 n))
(match
p0 in (_ = n1) return (A (k0 + n.+1) -> A (n1 + n.+1))
with
| 1 => funa1 : A (k0 + n.+1) => a1 ^+
end a0))
with
| 1 =>
K S (fun (n0 : nat) (a1 : A n0) => a1 ^+) (nat_add_succ_r k0 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 :=
funk0 : nat => transport idmap (ap A (nat_add_succ_r k0 n));
DiagramMap_comm :=
fun (k0l : nat) (p : k0.+1 = l) (a0 : A (k0 + n.+1)) =>
match
p as p0 in (_ = n0)
return
(match
p0 in (_ = n1) return (A (k0 + n).+1 -> A (n1 + n).+1)
with
| 1 => funa1 : A (k0 + n).+1 => a1 ^+
end (transport idmap (ap A (nat_add_succ_r k0 n)) a0) =
transport idmap (ap A (nat_add_succ_r n0 n))
(match
p0 in (_ = n1)
return (A (k0 + n.+1) -> A (n1 + n.+1))
with
| 1 => funa1 : A (k0 + n.+1) => a1 ^+
end a0))
with
| 1 =>
K S (fun (n0 : nat) (a1 : A n0) => a1 ^+)
(nat_add_succ_r k0 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 :=
funk0 : nat => transport idmap (ap A (nat_add_succ_r k0 n));
DiagramMap_comm :=
fun (k0l : nat) (p : k0.+1 = l) (a0 : A (k0 + n.+1)) =>
match
p as p0 in (_ = n0)
return
(match
p0 in (_ = n1) return (A (k0 + n).+1 -> A (n1 + n).+1)
with
| 1 => funa1 : A (k0 + n).+1 => a1 ^+
end (transport idmap (ap A (nat_add_succ_r k0 n)) a0) =
transport idmap (ap A (nat_add_succ_r n0 n))
(match
p0 in (_ = n1) return (A (k0 + n.+1) -> A (n1 + n.+1))
with
| 1 => funa1 : A (k0 + n.+1) => a1 ^+
end a0))
with
| 1 =>
K S (fun (n0 : nat) (a1 : A n0) => a1 ^+) (nat_add_succ_r k0 n)
end
|} 1 a)^ @
ap (colim_shift_seq_to_colim_seq A n)
(colimp k.+1 k.+21
({|
DiagramMap_obj :=
funk0 : nat => transport idmap (ap A (nat_add_succ_r k0 n));
DiagramMap_comm :=
fun (k0l : nat) (p : k0.+1 = l) (a0 : A (k0 + n.+1)) =>
match
p as p0 in (_ = n0)
return
(match
p0 in (_ = n1) return (A (k0 + n).+1 -> A (n1 + n).+1)
with
| 1 => funa1 : A (k0 + n).+1 => a1 ^+
end (transport idmap (ap A (nat_add_succ_r k0 n)) a0) =
transport idmap (ap A (nat_add_succ_r n0 n))
(match
p0 in (_ = n1) return (A (k0 + n.+1) -> A (n1 + n.+1))
with
| 1 => funa1 : A (k0 + n.+1) => a1 ^+
end a0))
with
| 1 =>
K S (fun (n0 : nat) (a1 : A n0) => a1 ^+)
(nat_add_succ_r k0 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) (h0 : {x : _ & A x} -> Type) (x0 : {x : _ & A x}) =>
h0 x0 ^++)
k x ->
nat_rect (fun_ : nat => {x : _ & A x} -> Type)
(funx0 : {x : _ & A x} => B x0)
(fun (_ : nat) (h0 : {x : _ & A x} -> Type) (x0 : {x : _ & A x}) =>
h0 x0 ^++)
k.+1 x
forallx : {x : _ & A x},
nat_rect (fun_ : nat => {x : _ & A x} -> Type)
(funx0 : {x : _ & A x} => B x0)
(fun (_ : nat) (h0 : {x : _ & A x} -> Type) (x0 : {x : _ & A x}) =>
h0 x0 ^++)
k.+1 x ->
nat_rect (fun_ : nat => {x : _ & A x} -> Type)
(funx0 : {x : _ & A x} => B x0)
(fun (_ : nat) (h0 : {x : _ & A x} -> Type) (x0 : {x : _ & A x}) =>
h0 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 =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(funx1 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(x1 : {x : _ & A x}) =>
coe (ap B (seq_pair_shift_assoc x1 n0)) o e x1 ^++)
n x)
i x0) =
(funn : Graph.graph0 sequence_graph =>
nat_rect
(funn0 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(funx1 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(x1 : {x : _ & A x}) =>
coe (ap B (seq_pair_shift_assoc x1 n0)) o e x1 ^++)
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
(funn0 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(funx1 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n0) =>
equiv_path (B (x1 ^++) ^++ n0) (B x1 ^++ (n0.+1))
(ap B (seq_pair_shift_assoc x1 n0)) (e x1 ^++ x2))
n x x0)
^+ =
nat_rect
(funn0 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(funx1 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n0) =>
equiv_path (B (x1 ^++) ^++ n0) (B x1 ^++ (n0.+1))
(ap B (seq_pair_shift_assoc x1 n0)) (e x1 ^++ x2))
n.+1 x x0 ^+
forall (x : {x : _ & A x}) (x0 : fib_seq_to_seq B x n.+1),
(nat_rect
(funn0 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(funx1 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n0) =>
equiv_path (B (x1 ^++) ^++ n0) (B x1 ^++ (n0.+1))
(ap B (seq_pair_shift_assoc x1 n0)) (e x1 ^++ x2))
n.+1 x x0)
^+ =
nat_rect
(funn0 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(funx1 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n0) =>
equiv_path (B (x1 ^++) ^++ n0) (B x1 ^++ (n0.+1))
(ap B (seq_pair_shift_assoc x1 n0)) (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
(funn0 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(funx1 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n0) =>
equiv_path (B (x1 ^++) ^++ n0) (B x1 ^++ (n0.+1))
(ap B (seq_pair_shift_assoc x1 n0)) (e x1 ^++ x2))
n x x0)
^+ =
nat_rect
(funn0 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(funx1 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n0) =>
equiv_path (B (x1 ^++) ^++ n0) (B x1 ^++ (n0.+1))
(ap B (seq_pair_shift_assoc x1 n0)) (e x1 ^++ x2))
n.+1 x x0 ^+
forall (x : {x : _ & A x}) (x0 : fib_seq_to_seq B x n.+1),
(nat_rect
(funn0 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(funx1 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n0) =>
equiv_path (B (x1 ^++) ^++ n0) (B x1 ^++ (n0.+1))
(ap B (seq_pair_shift_assoc x1 n0)) (e x1 ^++ x2))
n.+1 x x0)
^+ =
nat_rect
(funn0 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(funx1 : {x : _ & A x} => idmap)
(fun (n0 : nat)
(e : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n0 -> fib_seq_to_seq' B x1 n0)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n0) =>
equiv_path (B (x1 ^++) ^++ n0) (B x1 ^++ (n0.+1))
(ap B (seq_pair_shift_assoc x1 n0)) (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 =>
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}) =>
coe (ap B (seq_pair_shift_assoc x0 n0)) o e x0 ^++)
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 : _ & 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 ^+)
(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
(((fix F (n1 : nat) :
(fun_ : nat => {x : _ & A x}) n1 :=
match
n1 as n2
return ((fun_ : nat => {x : _ & A x}) n2)
with
| 0 => x0
| n2.+1 =>
(fun (_ : nat) (y : {x : _ & A x}) => y ^++)
n2 (F n2)
end)
n0)
^++)
^++)
(ap B (ap seq_pair_shift (seq_pair_shift_assoc x0 n0))))
(p0 x0 ^++ 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 : _ & 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 ^+)
(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 :=
funn0 : Graph.graph0 sequence_graph =>
nat_rect
(funn1 : nat =>
forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n1 -> fib_seq_to_seq' B x0 n1)
(funx0 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e0 : forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n1 -> fib_seq_to_seq' B x0 n1)
(x0 : {x : _ & A x}) (x1 : fib_seq_to_seq B x0 ^++ n1) =>
equiv_path (B (x0 ^++) ^++ n1) (B x0 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x0 n1)) (e0 x0 ^++ x1))
n0 x;
DiagramMap_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m) =>
match
p as p0 in (_ = n1)
return
(forallx0 : fib_seq_to_seq B x n0,
((fib_seq_to_seq' B x) _f p0)
(nat_rect
(funn2 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(funx1 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n2) =>
equiv_path (B (x1 ^++) ^++ n2) (B x1 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x1 n2))
(e0 x1 ^++ x2))
n0 x x0) =
nat_rect
(funn2 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(funx1 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n2) =>
equiv_path (B (x1 ^++) ^++ n2) (B x1 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x1 n2))
(e0 x1 ^++ x2))
n1 x (((fib_seq_to_seq B x) _f p0) x0))
with
| 1 =>
nat_rect
(funn1 : nat =>
forall (x0 : {x : _ & A x}) (x1 : fib_seq_to_seq B x0 n1),
(nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x}) (x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2) (B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1 x0 x1)
^+ =
nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x}) (x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2) (B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1.+1 x0 x1 ^+)
(fun (x0 : {x : _ & A x}) (x1 : fib_seq_to_seq B x0 0) => 1)
(fun (n1 : nat)
(p0 : forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n1),
(nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 ->
fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2)
(B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1 x0 x1)
^+ =
nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 ->
fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2)
(B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1.+1 x0 x1 ^+)
(x0 : {x : _ & A x}) (b : fib_seq_to_seq B x0 n1.+1) =>
K seq_pair_shift (fibSequenceArr B)
(seq_pair_shift_assoc x0 n1) @
ap
(equiv_path (B ((x0 ^++) ^++ n1) ^++)
(B ((nat_iter n1 seq_pair_shift x0) ^++) ^++)
(ap B (ap seq_pair_shift (seq_pair_shift_assoc x0 n1))))
(p0 x0 ^++ b))
n0 x
end
|} n)
forallx : {x : _ & A x},
IsEquiv
({|
DiagramMap_obj :=
funn0 : Graph.graph0 sequence_graph =>
nat_rect
(funn1 : nat =>
forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n1 -> fib_seq_to_seq' B x0 n1)
(funx0 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e0 : forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n1 -> fib_seq_to_seq' B x0 n1)
(x0 : {x : _ & A x}) (x1 : fib_seq_to_seq B x0 ^++ n1) =>
equiv_path (B (x0 ^++) ^++ n1) (B x0 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x0 n1)) (e0 x0 ^++ x1))
n0 x;
DiagramMap_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m) =>
match
p as p0 in (_ = n1)
return
(forallx0 : fib_seq_to_seq B x n0,
((fib_seq_to_seq' B x) _f p0)
(nat_rect
(funn2 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(funx1 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n2) =>
equiv_path (B (x1 ^++) ^++ n2) (B x1 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x1 n2))
(e0 x1 ^++ x2))
n0 x x0) =
nat_rect
(funn2 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(funx1 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n2) =>
equiv_path (B (x1 ^++) ^++ n2) (B x1 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x1 n2))
(e0 x1 ^++ x2))
n1 x (((fib_seq_to_seq B x) _f p0) x0))
with
| 1 =>
nat_rect
(funn1 : nat =>
forall (x0 : {x : _ & A x}) (x1 : fib_seq_to_seq B x0 n1),
(nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x}) (x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2) (B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1 x0 x1)
^+ =
nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x}) (x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2) (B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1.+1 x0 x1 ^+)
(fun (x0 : {x : _ & A x}) (x1 : fib_seq_to_seq B x0 0) => 1)
(fun (n1 : nat)
(p0 : forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n1),
(nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 ->
fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2)
(B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1 x0 x1)
^+ =
nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 ->
fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2)
(B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1.+1 x0 x1 ^+)
(x0 : {x : _ & A x}) (b : fib_seq_to_seq B x0 n1.+1) =>
K seq_pair_shift (fibSequenceArr B)
(seq_pair_shift_assoc x0 n1) @
ap
(equiv_path (B ((x0 ^++) ^++ n1) ^++)
(B ((nat_iter n1 seq_pair_shift x0) ^++) ^++)
(ap B (ap seq_pair_shift (seq_pair_shift_assoc x0 n1))))
(p0 x0 ^++ b))
n0 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 : _ & 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 ^+)
(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 :=
funn0 : Graph.graph0 sequence_graph =>
nat_rect
(funn1 : nat =>
forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n1 -> fib_seq_to_seq' B x0 n1)
(funx0 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e0 : forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n1 -> fib_seq_to_seq' B x0 n1)
(x0 : {x : _ & A x}) (x1 : fib_seq_to_seq B x0 ^++ n1) =>
equiv_path (B (x0 ^++) ^++ n1) (B x0 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x0 n1)) (e0 x0 ^++ x1))
n0 x;
DiagramMap_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m) =>
match
p as p0 in (_ = n1)
return
(forallx0 : fib_seq_to_seq B x n0,
((fib_seq_to_seq' B x) _f p0)
(nat_rect
(funn2 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(funx1 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n2) =>
equiv_path (B (x1 ^++) ^++ n2) (B x1 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x1 n2))
(e0 x1 ^++ x2))
n0 x x0) =
nat_rect
(funn2 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(funx1 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n2) =>
equiv_path (B (x1 ^++) ^++ n2) (B x1 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x1 n2))
(e0 x1 ^++ x2))
n1 x (((fib_seq_to_seq B x) _f p0) x0))
with
| 1 =>
nat_rect
(funn1 : nat =>
forall (x0 : {x : _ & A x}) (x1 : fib_seq_to_seq B x0 n1),
(nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x}) (x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2) (B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1 x0 x1)
^+ =
nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x}) (x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2) (B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1.+1 x0 x1 ^+)
(fun (x0 : {x : _ & A x}) (x1 : fib_seq_to_seq B x0 0) => 1)
(fun (n1 : nat)
(p0 : forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n1),
(nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 ->
fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2)
(B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1 x0 x1)
^+ =
nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 ->
fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2)
(B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1.+1 x0 x1 ^+)
(x0 : {x : _ & A x}) (b : fib_seq_to_seq B x0 n1.+1) =>
K seq_pair_shift (fibSequenceArr B)
(seq_pair_shift_assoc x0 n1) @
ap
(equiv_path (B ((x0 ^++) ^++ n1) ^++)
(B ((nat_iter n1 seq_pair_shift x0) ^++) ^++)
(ap B (ap seq_pair_shift (seq_pair_shift_assoc x0 n1))))
(p0 x0 ^++ b))
n0 x
end
|} n)
forallx : {x : _ & A x},
IsEquiv
({|
DiagramMap_obj :=
funn0 : Graph.graph0 sequence_graph =>
nat_rect
(funn1 : nat =>
forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n1 -> fib_seq_to_seq' B x0 n1)
(funx0 : {x : _ & A x} => idmap)
(fun (n1 : nat)
(e0 : forallx0 : {x : _ & A x},
fib_seq_to_seq B x0 n1 -> fib_seq_to_seq' B x0 n1)
(x0 : {x : _ & A x}) (x1 : fib_seq_to_seq B x0 ^++ n1) =>
equiv_path (B (x0 ^++) ^++ n1) (B x0 ^++ (n1.+1))
(ap B (seq_pair_shift_assoc x0 n1)) (e0 x0 ^++ x1))
n0 x;
DiagramMap_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m) =>
match
p as p0 in (_ = n1)
return
(forallx0 : fib_seq_to_seq B x n0,
((fib_seq_to_seq' B x) _f p0)
(nat_rect
(funn2 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(funx1 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n2) =>
equiv_path (B (x1 ^++) ^++ n2) (B x1 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x1 n2))
(e0 x1 ^++ x2))
n0 x x0) =
nat_rect
(funn2 : nat =>
forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(funx1 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx1 : {x : _ & A x},
fib_seq_to_seq B x1 n2 -> fib_seq_to_seq' B x1 n2)
(x1 : {x : _ & A x}) (x2 : fib_seq_to_seq B x1 ^++ n2) =>
equiv_path (B (x1 ^++) ^++ n2) (B x1 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x1 n2))
(e0 x1 ^++ x2))
n1 x (((fib_seq_to_seq B x) _f p0) x0))
with
| 1 =>
nat_rect
(funn1 : nat =>
forall (x0 : {x : _ & A x}) (x1 : fib_seq_to_seq B x0 n1),
(nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x}) (x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2) (B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1 x0 x1)
^+ =
nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x}) (x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2) (B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1.+1 x0 x1 ^+)
(fun (x0 : {x : _ & A x}) (x1 : fib_seq_to_seq B x0 0) => 1)
(fun (n1 : nat)
(p0 : forall (x0 : {x : _ & A x})
(x1 : fib_seq_to_seq B x0 n1),
(nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 ->
fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2)
(B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1 x0 x1)
^+ =
nat_rect
(funn2 : nat =>
forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 -> fib_seq_to_seq' B x2 n2)
(funx2 : {x : _ & A x} => idmap)
(fun (n2 : nat)
(e0 : forallx2 : {x : _ & A x},
fib_seq_to_seq B x2 n2 ->
fib_seq_to_seq' B x2 n2)
(x2 : {x : _ & A x})
(x3 : fib_seq_to_seq B x2 ^++ n2) =>
equiv_path (B (x2 ^++) ^++ n2)
(B x2 ^++ (n2.+1))
(ap B (seq_pair_shift_assoc x2 n2))
(e0 x2 ^++ x3))
n1.+1 x0 x1 ^+)
(x0 : {x : _ & A x}) (b : fib_seq_to_seq B x0 n1.+1) =>
K seq_pair_shift (fibSequenceArr B)
(seq_pair_shift_assoc x0 n1) @
ap
(equiv_path (B ((x0 ^++) ^++ n1) ^++)
(B ((nat_iter n1 seq_pair_shift x0) ^++) ^++)
(ap B (ap seq_pair_shift (seq_pair_shift_assoc x0 n1))))
(p0 x0 ^++ b))
n0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0) =>
Colimit (fib_seq_to_seq B (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
(Colimit (fib_seq_to_seq B (n1; (A _f p0) a0)) =
Colimit (fib_seq_to_seq B (n0; a0)))
with
| 1 =>
path_universe_uncurried
(equiv_colim_succ_seq_to_colim_seq
(fib_seq_to_seq B (n0; a0)))
end)
:
(fun (n1 : Graph.graph0 sequence_graph) (a0 : A n1) =>
Colimit (fib_seq_to_seq B (n1; a0))) m
o A _f p ==
(fun (n1 : Graph.graph0 sequence_graph) (a0 : A n1) =>
Colimit (fib_seq_to_seq B (n1; a0))) n0
|} 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: (funa0 : A n => B (n; a0)) 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: (funa0 : A n => B (n; a0)) 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b0))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b0)))
(e n0.+1 a0 ^+ b0 ^+f) =
e n0 a0 b0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b0))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b0)))
(e n0.+1 a0 ^+ b0 ^+f) =
e n0 a0 b0 k: nat h: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : fib_seq_to_seq B (n0; a0) k),
transport (funx : fib_seq_to_type_fam B (inj A n0 a0) => E (inj A n0 a0; x))
(colimp k k.+11 b0) (Q k.+1 n0 a0 b0 ^+) =
Q k n0 a0 b0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b)))
(e n0.+1 a0 ^+ b ^+f) =
e n0 a0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b)))
(e n0.+1 a0 ^+ b ^+f) =
e n0 a0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b)))
(e n0.+1 a0 ^+ b ^+f) =
e n0 a0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b)))
(e n0.+1 a0 ^+ b ^+f) =
e n0 a0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b)))
(e n0.+1 a0 ^+ b ^+f) =
e n0 a0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b)))
(e n0.+1 a0 ^+ b ^+f) =
e n0 a0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b0))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b0)))
(e n0.+1 a0 ^+ b0 ^+f) =
e n0 a0 b0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b0))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b0)))
(e n0.+1 a0 ^+ b0 ^+f) =
e n0 a0 b0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b)))
(e n0.+1 a0 ^+ b ^+f) =
e n0 a0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b)))
(e n0.+1 a0 ^+ b ^+f) =
e n0 a0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b)))
(e n0.+1 a0 ^+ b ^+f) =
e n0 a0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b)))
(e n0.+1 a0 ^+ b ^+f) =
e n0 a0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b)))
(e n0.+1 a0 ^+ b ^+f) =
e n0 a0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b)))
(e n0.+1 a0 ^+ b ^+f) =
e n0 a0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b0))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b0)))
(e n0.+1 a0 ^+ b0 ^+f) =
e n0 a0 b0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b0))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b0)))
(e n0.+1 a0 ^+ b0 ^+f) =
e n0 a0 b0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b0))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b0)))
(e n0.+1 a0 ^+ b0 ^+f) =
e n0 a0 b0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b0))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b0)))
(e n0.+1 a0 ^+ b0 ^+f) =
e n0 a0 b0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b)))
(e n0.+1 a0 ^+ b ^+f) =
e n0 a0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b)))
(e n0.+1 a0 ^+ b ^+f) =
e n0 a0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b)))
(e n0.+1 a0 ^+ b ^+f) =
e n0 a0 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: forally0 : Y x1,
(funy1 : Y x2 => G (x2; y1)) (F y0) =
transport Z (Delta p psi y0) ((funy1 : Y x1 => G (x1; y1)) y0) theta: I psi (apD (fun (x : X) (y0 : Y x) => G (x; y0)) 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: forally0 : Y x1,
(funy1 : Y x2 => G (x2; y1)) (F y0) =
transport Z (Delta p psi y0) ((funy1 : Y x1 => G (x1; y1)) y0) theta: I psi (apD (fun (x : X) (y0 : Y x) => G (x; y0)) 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b0))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b0)))
(e n0.+1 a0 ^+ b0 ^+f) =
e n0 a0 b0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b0))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b0)))
(e n0.+1 a0 ^+ b0 ^+f) =
e n0 a0 b0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
E (seq_colim_sum_to_sum_seq_colim B (inj (sig_seq B) n0 (a0; b0))) t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0),
transport E
(ap (seq_colim_sum_to_sum_seq_colim B) (glue (sig_seq B) n0 (a0; b0)))
(e n0.+1 a0 ^+ b0 ^+f) =
e n0 a0 b0 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0), B (n0; a0) -> E t: forall (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : B (n0; a0)), e n0.+1 a0 ^+ b0 ^+f = e n0 a0 b0 n: Graph.graph0 sequence_graph a: A n b: (funa0 : A n => B (n; a0)) 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: (funa0 : A n => B (n; a0)) 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 (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0) =>
h (inj (sig_seq B) n0 (a0; b0))) n.+1 a ^+ b ^+f) =
(fun (n0 : Graph.graph0 sequence_graph) (a0 : A n0)
(b0 : (funa1 : A n0 => B (n0; a1)) a0) =>
h (inj (sig_seq B) n0 (a0; b0))) 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
{G0
: {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) => G0 (seq_colim_sum_to_sum_seq_colim B x)) ==
idmap}
H: Univalence A: Sequence B: FibSequence A L: {G0
: {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})
& G0 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
{G0
: {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) => G0 (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
(funG0 : {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) => G0 (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
(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}))
(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)) =>
colimp n0 n0.+11 (a0; 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: {G0
: {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})
& G0 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: {G0
: {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})
& G0 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 (n0 : Graph.graph0 sequence_graph) (X : sig_seq B n0) =>
(inj A n0 X.1; inj (fib_seq_to_seq B (n0; X.1)) 0 X.2);
legs_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m)
(x : sig_seq B n0) =>
match
p as p0 in (_ = n1)
return
((inj A n1 (((sig_seq B) _f p0) (x.1; x.2)).1;
inj (fib_seq_to_seq B (n1; (((sig_seq B) _f p0) (x.1; x.2)).1))
0 (((sig_seq B) _f p0) (x.1; x.2)).2) =
(inj A n0 x.1; inj (fib_seq_to_seq B (n0; x.1)) 0 x.2))
with
| 1 =>
Delta (colimp n0 n0.+11 x.1)
(fib_seq_to_type_fam_beta_glue B n0 x.1)
(inj (fib_seq_to_seq B (n0.+1; ((x.1; x.2) ^+).1)) 0
((x.1; x.2) ^+).2) @
ap (exist (fib_seq_to_type_fam B) (inj A n0 x.1))
(colimp 011 x.2)
end
|} n n.+11 (a; b)) =
legs_comm
{|
legs :=
fun (n0 : Graph.graph0 sequence_graph) (X : sig_seq B n0) =>
inj A n0 X.1;
legs_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m) (x : sig_seq B n0) =>
match
p as p0 in (_ = n1)
return (inj A n1 (((sig_seq B) _f p0) (x.1; x.2)).1 = inj A n0 x.1)
with
| 1 => colimp n0 n0.+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 (n0 : Graph.graph0 sequence_graph) (X : sig_seq B n0) =>
inj A n0 X.1;
legs_comm :=
fun (n0m : Graph.graph0 sequence_graph)
(p : Graph.graph1 sequence_graph n0 m) (x : sig_seq B n0) =>
match
p as p0 in (_ = n1)
return (inj A n1 (((sig_seq B) _f p0) (x.1; x.2)).1 = inj A n0 x.1)
with
| 1 => colimp n0 n0.+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
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
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,
(foralln0 : Graph.graph0 sequence_graph, IsTrunc k (A n0)) ->
IsTrunc k (Colimit A) n: nat IHn: forallA : Sequence,
(foralln0 : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n0)) ->
forall (x : A n) (y : Colimit A), IsTrunc k (inj A n x = y)
forallA : Sequence,
(foralln0 : Graph.graph0 sequence_graph, IsTrunc k.+1 (A n0)) ->
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: forallA0 : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A0 n)) ->
IsTrunc k (Colimit A0) 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: forallA0 : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A0 n)) ->
IsTrunc k (Colimit A0) 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: forallA0 : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A0 n)) ->
IsTrunc k (Colimit A0) 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: forallA0 : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A0 n)) ->
IsTrunc k (Colimit A0) 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: forallA0 : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A0 n)) ->
IsTrunc k (Colimit A0) m: nat IHm: forallA0 : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A0 n)) ->
forall (a0 : A0 0%nat) (b0 : A0 m), IsTrunc k (inj A0 0%nat a0 = inj A0 m b0) 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: forallA0 : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A0 n)) ->
IsTrunc k (Colimit A0) m: nat IHm: forallA0 : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A0 n)) ->
forall (a0 : A0 0%nat) (b0 : A0 m), IsTrunc k (inj A0 0%nat a0 = inj A0 m b0) 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: forallA0 : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k (A0 n)) ->
IsTrunc k (Colimit A0) m: nat IHm: forallA0 : Sequence,
(foralln : Graph.graph0 sequence_graph, IsTrunc k.+1 (A0 n)) ->
forall (a0 : A0 0%nat) (b0 : A0 m), IsTrunc k (inj A0 0%nat a0 = inj A0 m b0) 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