From HoTT Require Import Basics.From HoTT Require Import Basics.
Require Import Types.
Require Import Diagrams.Diagram.
Require Import Diagrams.Graph.
Require Import Diagrams.Cocone.
Require Import Colimits.Colimit.

(** * Colimit of the dependent sum of a family of diagrams *)

(** Given a family of diagrams [D y], and a colimit [Q y] of each diagram, one can consider the diagram of the sigmas of the types of the [D y]s. Then, a colimit of such a diagram is the sigma of the [Q y]s. *)

Section ColimitSigma.

  Context `{Funext} {G : Graph} {Y : Type} (D : Y -> Diagram G).

  (** The diagram of the sigmas. *)

  Definition sigma_diagram : Diagram G.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Diagram G
  Proof.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Diagram G
    srapply Build_Diagram.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
G -> Type
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
forall i j : G, G i j -> ?obj i -> ?obj j
    -
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
G -> Type exact (fun i => {y: Y & D y i}).
    -
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
forall i j : G,
G i j ->
(fun i0 : G => {y : Y & D y i0}) i -> (fun i0 : G => {y : Y & D y i0}) j simpl; intros i j g x.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
i, j: G
g: G i j
x: {y : Y & D y i}
{y : Y & D y j}
      exact (x.1; D x.1 _f g x.2).
  Defined.

  (** The embedding, for a particular [y], of [D(y)] in the sigma diagram. *)

  Definition sigma_diagram_map (y: Y) : DiagramMap (D y) sigma_diagram.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
y: Y
DiagramMap (D y) sigma_diagram
  Proof.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
y: Y
DiagramMap (D y) sigma_diagram
    srapply Build_DiagramMap.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
y: Y
forall i : G, D y i -> sigma_diagram i
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
y: Y
forall (i j : G) (g : G i j) (x : D y i),
(sigma_diagram _f g) (?DiagramMap_obj i x) =
?DiagramMap_obj j (((D y) _f g) x)
    1: exact (fun i x => (y; x)).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
y: Y
forall (i j : G) (g : G i j) (x : D y i),
(sigma_diagram _f g) ((fun (i0 : G) (x0 : D y i0) => (y; x0)) i x) =
(fun (i0 : G) (x0 : D y i0) => (y; x0)) j (((D y) _f g) x)
    reflexivity.
  Defined.

  Context {Q : Y -> Type}.

  (** The sigma of a family of cocones. *)

  Definition sigma_cocone (C : forall y, Cocone (D y) (Q y))
    : Cocone sigma_diagram (sig Q).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
Cocone sigma_diagram {x : _ & Q x}
  Proof.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
Cocone sigma_diagram {x : _ & Q x}
    srapply Build_Cocone; simpl; intros i x.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
i: G
x: {y : Y & D y i}
{x : _ & Q x}
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
i, x: G
forall g : G i x,
(fun x0 : {y : Y & D y i} =>
 (fun (i0 : G) (x1 : {y : Y & D y i0}) => ?Goal@{i:=i0; x:=x1}) x
   (x0.1; ((D x0.1) _f g) x0.2)) ==
(fun (i0 : G) (x0 : {y : Y & D y i0}) => ?Goal@{i:=i0; x:=x0}) i
    1: exact (x.1; legs (C x.1) i x.2).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
i, x: G
forall g : G i x,
(fun x0 : {y : Y & D y i} =>
 (fun (i0 : G) (x1 : {y : Y & D y i0}) => (x1.1; C x1.1 i0 x1.2)) x
   (x0.1; ((D x0.1) _f g) x0.2)) ==
(fun (i0 : G) (x0 : {y : Y & D y i0}) => (x0.1; C x0.1 i0 x0.2)) i
    simpl; intros g x'.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
i, x: G
g: G i x
x': {y : Y & D y i}
(x'.1; C x'.1 x (((D x'.1) _f g) x'.2)) = (x'.1; C x'.1 i x'.2)
    srapply path_sigma'.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
i, x: G
g: G i x
x': {y : Y & D y i}
x'.1 = x'.1
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
i, x: G
g: G i x
x': {y : Y & D y i}
transport Q ?p (C x'.1 x (((D x'.1) _f g) x'.2)) = C x'.1 i x'.2
    1: reflexivity.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
C: forall y : Y, Cocone (D y) (Q y)
i, x: G
g: G i x
x': {y : Y & D y i}
transport Q 1 (C x'.1 x (((D x'.1) _f g) x'.2)) = C x'.1 i x'.2
    apply legs_comm.
  Defined.

  (** The main result: [sig Q] is a colimit of the diagram of sigma types. *)

  Lemma iscolimit_sigma (HQ : forall y, IsColimit (D y) (Q y))
  : IsColimit sigma_diagram (sig Q).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
IsColimit sigma_diagram {x : _ & Q x}
  Proof.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
IsColimit sigma_diagram {x : _ & Q x}
    pose (SigmaC := sigma_cocone (fun y => HQ y)).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
IsColimit sigma_diagram {x : _ & Q x}
    srapply (Build_IsColimit SigmaC).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
UniversalCocone SigmaC
    srapply Build_UniversalCocone.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
forall Y0 : Type, IsEquiv (cocone_postcompose SigmaC)
    intros X; srapply isequiv_adjointify.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
Cocone sigma_diagram X -> {x : _ & Q x} -> X
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
cocone_postcompose SigmaC o ?g == idmap
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
?g o cocone_postcompose SigmaC == idmap
    -
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
Cocone sigma_diagram X -> {x : _ & Q x} -> X intros CX x.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
x: {x : _ & Q x}
X
      srapply (cocone_postcompose_inv (HQ x.1) _ x.2).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
x: {x : _ & Q x}
Cocone (D x.1) X
      srapply (cocone_precompose _ CX).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
x: {x : _ & Q x}
DiagramMap (D x.1) sigma_diagram
      apply sigma_diagram_map.
    -
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
cocone_postcompose SigmaC
o (fun (CX : Cocone sigma_diagram X) (x : {x : _ & Q x}) =>
   cocone_postcompose_inv (HQ x.1)
     (cocone_precompose (sigma_diagram_map x.1) CX) x.2) ==
idmap intro CX.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
cocone_postcompose SigmaC
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1)
     (cocone_precompose (sigma_diagram_map x.1) CX) x.2) =
CX
      pose (CXy := fun y => cocone_precompose (sigma_diagram_map y) CX).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y => cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
cocone_postcompose SigmaC
  (fun x : {x : _ & Q x} =>
   cocone_postcompose_inv (HQ x.1)
     (cocone_precompose (sigma_diagram_map x.1) CX) x.2) =
CX
      change (cocone_postcompose SigmaC
        (fun x => cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2) = CX).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y => cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
cocone_postcompose SigmaC
  (fun x : {x : _ & Q x} => cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2) =
CX
      srapply path_cocone; simpl.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y => cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
forall i : G,
(fun x : {y : Y & D y i} =>
 cocone_postcompose_inv (HQ x.1) (CXy x.1) (HQ x.1 i x.2)) ==
CX i
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y => cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
forall (i j : G) (g : G i j) (x : {y : Y & D y i}),
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ x.1) i j g x.2)) @
?Goal i x = ?Goal j (x.1; ((D x.1) _f g) x.2) @ legs_comm CX i j g x
      +
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y => cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
forall i : G,
(fun x : {y : Y & D y i} =>
 cocone_postcompose_inv (HQ x.1) (CXy x.1) (HQ x.1 i x.2)) ==
CX i intros i x.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y => cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i: G
x: {y : Y & D y i}
cocone_postcompose_inv (HQ x.1) (CXy x.1) (HQ x.1 i x.2) = CX i x
        change (legs (cocone_postcompose (HQ x.1)
                 (cocone_postcompose_inv (HQ x.1) (CXy x.1))) i x.2 = CX i x).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y => cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
i: G
x: {y : Y & D y i}
cocone_postcompose (HQ x.1) (cocone_postcompose_inv (HQ x.1) (CXy x.1)) i x.2 =
CX i x
        exact (ap10 (apD10 (ap legs (eisretr
          (cocone_postcompose (HQ x.1)) (CXy _))) i) x.2).
      +
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y : Y => cocone_precompose (sigma_diagram_map y) CX: forall y : Y, Cocone (D y) X
forall (i j : G) (g : G i j) (x : {y : Y & D y i}),
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ x.1) i j g x.2)) @
(fun i0 : G =>
 (fun x0 : {y : Y & D y i0} =>
  ap10
    (apD10 (ap legs (eisretr (cocone_postcompose (HQ x0.1)) (CXy x0.1))) i0)
    x0.2)
 :
 (fun x0 : {y : Y & D y i0} =>
  cocone_postcompose_inv (HQ x0.1) (CXy x0.1) (HQ x0.1 i0 x0.2)) ==
 CX i0) i x =
(fun i0 : G =>
 (fun x0 : {y : Y & D y i0} =>
  ap10
    (apD10 (ap legs (eisretr (cocone_postcompose (HQ x0.1)) (CXy x0.1))) i0)
    x0.2)
 :
 (fun x0 : {y : Y & D y i0} =>
  cocone_postcompose_inv (HQ x0.1) (CXy x0.1) (HQ x0.1 i0 x0.2)) ==
 CX i0) j (x.1; ((D x.1) _f g) x.2) @
legs_comm CX i j g x intros i j g [y x]; simpl.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 (ap legs (eisretr (cocone_postcompose (HQ y)) (CXy y))) i) x =
ap10 (apD10 (ap legs (eisretr (cocone_postcompose (HQ y)) (CXy y))) j)
  (((D y) _f g) x) @
legs_comm CX i j g (y; x)
        set (py := (eisretr (cocone_postcompose (HQ y)) (CXy y))).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): (cocone_postcompose (HQ y) o (cocone_postcompose (HQ y))^-1) (CXy y) =
idmap (CXy y)
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 (ap legs py) i) x =
ap10 (apD10 (ap legs py) j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
        set (py1 := ap legs py).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): (cocone_postcompose (HQ y) o (cocone_postcompose (HQ y))^-1) (CXy y) =
idmap (CXy y)
py1:= ap legs py: cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
        specialize (apD legs_comm py); intro py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): (cocone_postcompose (HQ y) o (cocone_postcompose (HQ y))^-1) (CXy y) =
idmap (CXy y)
py1:= ap legs py: cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py2: transport
  (fun C : Cocone (D y) X =>
   forall (i0 j0 : G) (g0 : G i0 j0), C j0 o (D y) _f g0 == C i0)
  py
  (legs_comm
     (cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)))) =
legs_comm (CXy y)
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
          simpl in *.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py1:= ap legs py: (fun (i0 : G) (x0 : D y i0) =>
 (cocone_postcompose (HQ y))^-1 (CXy y) (HQ y i0 x0)) =
(fun (i0 : G) (x0 : D y i0) => CX i0 (y; x0))
py2: transport
  (fun C : Cocone (D y) X =>
   forall (i0 j0 : G) (g0 : G i0 j0),
   (fun x0 : D y i0 => C j0 (((D y) _f g0) x0)) == C i0)
  py
  (fun (i0 j0 : G) (g0 : G i0 j0) (x0 : D y i0) =>
   ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i0 j0 g0 x0)) =
(fun (i0 j0 : G) (g0 : G i0 j0) (x0 : D y i0) =>
 1 @ legs_comm CX i0 j0 g0 (y; x0))
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
          rewrite (path_forall _ _(transport_forall_constant _ _)) in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py1:= ap legs py: (fun (i0 : G) (x0 : D y i0) =>
 (cocone_postcompose (HQ y))^-1 (CXy y) (HQ y i0 x0)) =
(fun (i0 : G) (x0 : D y i0) => CX i0 (y; x0))
py2: (fun y0 : G =>
 transport
   (fun x0 : Cocone (D y) X =>
    forall (j0 : G) (g0 : G y0 j0),
    (fun x1 : D y y0 => x0 j0 (((D y) _f g0) x1)) == x0 y0)
   py
   (fun (j0 : G) (g0 : G y0 j0) (x0 : D y y0) =>
    ap ((cocone_postcompose (HQ y))^-1 (CXy y))
      (legs_comm (HQ y) y0 j0 g0 x0))) =
(fun (i0 j0 : G) (g0 : G i0 j0) (x0 : D y i0) =>
 1 @ legs_comm CX i0 j0 g0 (y; x0))
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
          apply apD10 in py2; specialize (py2 i); simpl in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py1:= ap legs py: (fun (i0 : G) (x0 : D y i0) =>
 (cocone_postcompose (HQ y))^-1 (CXy y) (HQ y i0 x0)) =
(fun (i0 : G) (x0 : D y i0) => CX i0 (y; x0))
py2: transport
  (fun x0 : Cocone (D y) X =>
   forall (j0 : G) (g0 : G i j0),
   (fun x1 : D y i => x0 j0 (((D y) _f g0) x1)) == x0 i)
  py
  (fun (j0 : G) (g0 : G i j0) (x0 : D y i) =>
   ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j0 g0 x0)) =
(fun (j0 : G) (g0 : G i j0) (x0 : D y i) => 1 @ legs_comm CX i j0 g0 (y; x0))
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
          rewrite (path_forall _ _(transport_forall_constant _ _)) in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py1:= ap legs py: (fun (i0 : G) (x0 : D y i0) =>
 (cocone_postcompose (HQ y))^-1 (CXy y) (HQ y i0 x0)) =
(fun (i0 : G) (x0 : D y i0) => CX i0 (y; x0))
py2: (fun y0 : G =>
 transport
   (fun x0 : Cocone (D y) X =>
    forall g0 : G i y0, (fun x1 : D y i => x0 y0 (((D y) _f g0) x1)) == x0 i)
   py
   (fun (g0 : G i y0) (x0 : D y i) =>
    ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i y0 g0 x0))) =
(fun (j0 : G) (g0 : G i j0) (x0 : D y i) => 1 @ legs_comm CX i j0 g0 (y; x0))
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
          apply apD10 in py2; specialize (py2 j); simpl in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py1:= ap legs py: (fun (i0 : G) (x0 : D y i0) =>
 (cocone_postcompose (HQ y))^-1 (CXy y) (HQ y i0 x0)) =
(fun (i0 : G) (x0 : D y i0) => CX i0 (y; x0))
py2: transport
  (fun x0 : Cocone (D y) X =>
   forall g0 : G i j, (fun x1 : D y i => x0 j (((D y) _f g0) x1)) == x0 i)
  py
  (fun (g0 : G i j) (x0 : D y i) =>
   ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g0 x0)) =
(fun (g0 : G i j) (x0 : D y i) => 1 @ legs_comm CX i j g0 (y; x0))
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
          rewrite (path_forall _ _(transport_forall_constant _ _)) in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py1:= ap legs py: (fun (i0 : G) (x0 : D y i0) =>
 (cocone_postcompose (HQ y))^-1 (CXy y) (HQ y i0 x0)) =
(fun (i0 : G) (x0 : D y i0) => CX i0 (y; x0))
py2: (fun y0 : G i j =>
 transport
   (fun x0 : Cocone (D y) X =>
    (fun x1 : D y i => x0 j (((D y) _f y0) x1)) == x0 i)
   py
   (fun x0 : D y i =>
    ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j y0 x0))) =
(fun (g0 : G i j) (x0 : D y i) => 1 @ legs_comm CX i j g0 (y; x0))
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
          apply apD10 in py2; specialize (py2 g); simpl in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py1:= ap legs py: (fun (i0 : G) (x0 : D y i0) =>
 (cocone_postcompose (HQ y))^-1 (CXy y) (HQ y i0 x0)) =
(fun (i0 : G) (x0 : D y i0) => CX i0 (y; x0))
py2: transport
  (fun x0 : Cocone (D y) X =>
   (fun x1 : D y i => x0 j (((D y) _f g) x1)) == x0 i)
  py
  (fun x0 : D y i =>
   ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x0)) =
(fun x0 : D y i => 1 @ legs_comm CX i j g (y; x0))
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
          rewrite (path_forall _ _(transport_forall_constant _ _)) in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py1:= ap legs py: (fun (i0 : G) (x0 : D y i0) =>
 (cocone_postcompose (HQ y))^-1 (CXy y) (HQ y i0 x0)) =
(fun (i0 : G) (x0 : D y i0) => CX i0 (y; x0))
py2: (fun y0 : D y i =>
 transport (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) y0) = x0 i y0) py
   (ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g y0))) =
(fun x0 : D y i => 1 @ legs_comm CX i j g (y; x0))
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
          apply apD10 in py2; specialize (py2 x); simpl in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py1:= ap legs py: (fun (i0 : G) (x0 : D y i0) =>
 (cocone_postcompose (HQ y))^-1 (CXy y) (HQ y i0 x0)) =
(fun (i0 : G) (x0 : D y i0) => CX i0 (y; x0))
py2: transport (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x) = x0 i x) py
  (ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x)) =
1 @ legs_comm CX i j g (y; x)
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
          rewrite transport_paths_FlFr in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py1:= ap legs py: (fun (i0 : G) (x0 : D y i0) =>
 (cocone_postcompose (HQ y))^-1 (CXy y) (HQ y i0 x0)) =
(fun (i0 : G) (x0 : D y i0) => CX i0 (y; x0))
py2: ((ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py)^ @
 ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x)) @
ap (fun x0 : Cocone (D y) X => x0 i x) py = 1 @ legs_comm CX i j g (y; x)
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
          rewrite concat_1p, concat_pp_p in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py1:= ap legs py: (fun (i0 : G) (x0 : D y i0) =>
 (cocone_postcompose (HQ y))^-1 (CXy y) (HQ y i0 x0)) =
(fun (i0 : G) (x0 : D y i0) => CX i0 (y; x0))
py2: (ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py)^ @
(ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
 ap (fun x0 : Cocone (D y) X => x0 i x) py) =
legs_comm CX i j g (y; x)
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
          apply moveL_Mp in py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py1:= ap legs py: (fun (i0 : G) (x0 : D y i0) =>
 (cocone_postcompose (HQ y))^-1 (CXy y) (HQ y i0 x0)) =
(fun (i0 : G) (x0 : D y i0) => CX i0 (y; x0))
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap
  (fun x0 : {x : _ & Q x} => cocone_postcompose_inv (HQ x0.1) (CXy x0.1) x0.2)
  (path_sigma' Q 1 (legs_comm (HQ y) i j g x)) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
        rewrite (ap_path_sigma_1p
          (fun x01 x02 => cocone_postcompose_inv (HQ x01) (CXy x01) x02)).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py1:= ap legs py: (fun (i0 : G) (x0 : D y i0) =>
 (cocone_postcompose (HQ y))^-1 (CXy y) (HQ y i0 x0)) =
(fun (i0 : G) (x0 : D y i0) => CX i0 (y; x0))
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap (fun z : Q y => cocone_postcompose_inv (HQ y) (CXy y) z)
  (legs_comm (HQ y) i j g x) @
ap10 (apD10 py1 i) x =
ap10 (apD10 py1 j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
        (* Set Printing Coercions. (* to understand what happens *)   *)
        subst py1.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap (fun z : Q y => cocone_postcompose_inv (HQ y) (CXy y) z)
  (legs_comm (HQ y) i j g x) @
ap10 (apD10 (ap legs py) i) x =
ap10 (apD10 (ap legs py) j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
        etransitivity.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap (fun z : Q y => cocone_postcompose_inv (HQ y) (CXy y) z)
  (legs_comm (HQ y) i j g x) @
ap10 (apD10 (ap legs py) i) x = ?Goal
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
?Goal =
ap10 (apD10 (ap legs py) j) (((D y) _f g) x) @ legs_comm CX i j g (y; x)
        *
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap (fun z : Q y => cocone_postcompose_inv (HQ y) (CXy y) z)
  (legs_comm (HQ y) i j g x) @
ap10 (apD10 (ap legs py) i) x = ?Goal etransitivity.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap (fun z : Q y => cocone_postcompose_inv (HQ y) (CXy y) z)
  (legs_comm (HQ y) i j g x) @
ap10 (apD10 (ap legs py) i) x = ?Goal1
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
?Goal1 = ?Goal
          2:exact py2.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap (fun z : Q y => cocone_postcompose_inv (HQ y) (CXy y) z)
  (legs_comm (HQ y) i j g x) @
ap10 (apD10 (ap legs py) i) x =
ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py
          apply ap.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap10 (apD10 (ap legs py) i) x = ap (fun x0 : Cocone (D y) X => x0 i x) py
          rewrite (ap_compose legs (fun x0 => x0 i x)).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap10 (apD10 (ap legs py) i) x =
ap (fun x0 : forall i0 : G, D y i0 -> X => x0 i x) (ap legs py)
          rewrite (ap_apply_lD2 _ i x).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap10 (apD10 (ap legs py) i) x = apD10 (apD10 (ap legs py) i) x
          reflexivity.
        *
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x) =
ap10 (apD10 (ap legs py) j) (((D y) _f g) x) @ legs_comm CX i j g (y; x) apply ap10, ap.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py =
ap10 (apD10 (ap legs py) j) (((D y) _f g) x)
          rewrite (ap_compose legs (fun x0 => x0 j _)).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
ap (fun x0 : forall i0 : G, D y i0 -> X => x0 j (((D y) _f g) x))
  (ap legs py) =
ap10 (apD10 (ap legs py) j) (((D y) _f g) x)
          rewrite (ap_apply_lD2 _ j _).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
CX: Cocone sigma_diagram X
CXy:= fun y0 : Y => cocone_precompose (sigma_diagram_map y0) CX: forall y0 : Y, Cocone (D y0) X
i, j: G
g: G i j
y: Y
x: D y i
py:= eisretr (cocone_postcompose (HQ y)) (CXy y): cocone_postcompose (HQ y) ((cocone_postcompose (HQ y))^-1 (CXy y)) = CXy y
py2: ap ((cocone_postcompose (HQ y))^-1 (CXy y)) (legs_comm (HQ y) i j g x) @
ap (fun x0 : Cocone (D y) X => x0 i x) py =
ap (fun x0 : Cocone (D y) X => x0 j (((D y) _f g) x)) py @
legs_comm CX i j g (y; x)
apD10 (apD10 (ap legs py) j) (((D y) _f g) x) =
ap10 (apD10 (ap legs py) j) (((D y) _f g) x)
          reflexivity.
    -
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
(fun (CX : Cocone sigma_diagram X) (x : {x : _ & Q x}) =>
 cocone_postcompose_inv (HQ x.1)
   (cocone_precompose (sigma_diagram_map x.1) CX) x.2)
o cocone_postcompose SigmaC == idmap intros f.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y : Y, IsColimit (D y) (Q y)
SigmaC:= sigma_cocone (fun y : Y => HQ y): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
(fun x : {x : _ & Q x} =>
 cocone_postcompose_inv (HQ x.1)
   (cocone_precompose (sigma_diagram_map x.1) (cocone_postcompose SigmaC f))
   x.2) =
f
      apply path_forall; intros [y x]; simpl.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
cocone_postcompose_inv (HQ y)
  (cocone_precompose (sigma_diagram_map y) (cocone_postcompose SigmaC f)) x =
f (y; x)
      rewrite <- cocone_precompose_postcompose.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
cocone_postcompose_inv (HQ y)
  (cocone_postcompose (cocone_precompose (sigma_diagram_map y) SigmaC) f) x =
f (y; x)
      srapply (apD10 (g := fun x => f (y; x)) _ x).
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
cocone_postcompose_inv (HQ y)
  (cocone_postcompose (cocone_precompose (sigma_diagram_map y) SigmaC) f) =
(fun x0 : Q y => f (y; x0))
      snapply equiv_moveR_equiv_V.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
cocone_postcompose (cocone_precompose (sigma_diagram_map y) SigmaC) f =
cocone_postcompose (HQ y) (fun x0 : Q y => f (y; x0))
      srapply path_cocone.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
forall i : G,
cocone_postcompose (cocone_precompose (sigma_diagram_map y) SigmaC) f i ==
cocone_postcompose (HQ y) (fun x0 : Q y => f (y; x0)) i
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
forall (i j : G) (g : G i j) (x0 : D y i),
legs_comm
  (cocone_postcompose (cocone_precompose (sigma_diagram_map y) SigmaC) f) i j
  g x0 @
?path_legs i x0 =
?path_legs j (((D y) _f g) x0) @
legs_comm (cocone_postcompose (HQ y) (fun x1 : Q y => f (y; x1))) i j g x0
      1: reflexivity.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
forall (i j : G) (g : G i j) (x0 : D y i),
legs_comm
  (cocone_postcompose (cocone_precompose (sigma_diagram_map y) SigmaC) f) i j
  g x0 @
(fun (i0 : G) (x1 : D y i0) => 1) i x0 =
(fun (i0 : G) (x1 : D y i0) => 1) j (((D y) _f g) x0) @
legs_comm (cocone_postcompose (HQ y) (fun x1 : Q y => f (y; x1))) i j g x0
      intros i j g x'; simpl.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
i, j: G
g: G i j
x': D y i
ap f (1 @ path_sigma' Q 1 (legs_comm (HQ y) i j g x')) @ 1 =
1 @ ap (fun x0 : Q y => f (y; x0)) (legs_comm (HQ y) i j g x')
      hott_simpl.
H: Funext
G: Graph
Y: Type
D: Y -> Diagram G
Q: Y -> Type
HQ: forall y0 : Y, IsColimit (D y0) (Q y0)
SigmaC:= sigma_cocone (fun y0 : Y => HQ y0): Cocone sigma_diagram {x : _ & Q x}
X: Type
f: {x : _ & Q x} -> X
y: Y
x: Q y
i, j: G
g: G i j
x': D y i
ap f (path_sigma' Q 1 (legs_comm (HQ y) i j g x')) =
ap (fun x0 : Q y => f (y; x0)) (legs_comm (HQ y) i j g x')
      exact (ap_compose _ _ _)^.
  Defined.

End ColimitSigma.

(** ** Sigma diagrams and diagram maps / equivalences *)

Section SigmaDiagram.

  Context {G : Graph} {Y : Type} (D1 D2 : Y -> Diagram G).

  Definition sigma_diagram_functor (m : forall y, DiagramMap (D1 y) (D2 y))
  : DiagramMap (sigma_diagram D1) (sigma_diagram D2).
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
DiagramMap (sigma_diagram D1) (sigma_diagram D2)
  Proof.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
DiagramMap (sigma_diagram D1) (sigma_diagram D2)
    srapply Build_DiagramMap.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
forall i : G, sigma_diagram D1 i -> sigma_diagram D2 i
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
forall (i j : G) (g : G i j) (x : sigma_diagram D1 i),
((sigma_diagram D2) _f g) (?DiagramMap_obj i x) =
?DiagramMap_obj j (((sigma_diagram D1) _f g) x)
    -
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
forall i : G, sigma_diagram D1 i -> sigma_diagram D2 i intros i.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
i: G
sigma_diagram D1 i -> sigma_diagram D2 i
      srapply (functor_sigma idmap _).
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
i: G
forall a : Y, (fun y : Y => D1 y i) a -> (fun y : Y => D2 y i) (idmap a)
      intros y; apply m.
    -
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
forall (i j : G) (g : G i j) (x : sigma_diagram D1 i),
((sigma_diagram D2) _f g)
  ((fun i0 : G =>
    functor_sigma idmap
      (fun y : Y => let X := fun y0 : Y => DiagramMap_obj (m y0) in X y i0))
     i x) =
(fun i0 : G =>
 functor_sigma idmap
   (fun y : Y => let X := fun y0 : Y => DiagramMap_obj (m y0) in X y i0))
  j (((sigma_diagram D1) _f g) x) intros i j g x; simpl in *.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
i, j: G
g: G i j
x: {y : Y & D1 y i}
(x.1; ((D2 x.1) _f g) (m x.1 i x.2)) =
functor_sigma idmap (fun y : Y => m y j) (x.1; ((D1 x.1) _f g) x.2)
    srapply path_sigma'.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
i, j: G
g: G i j
x: {y : Y & D1 y i}
x.1 = (x.1; ((D1 x.1) _f g) x.2).1
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
i, j: G
g: G i j
x: {y : Y & D1 y i}
transport (fun y : Y => D2 y j) ?p (((D2 x.1) _f g) (m x.1 i x.2)) =
m (x.1; ((D1 x.1) _f g) x.2).1 j (x.1; ((D1 x.1) _f g) x.2).2
    1: reflexivity.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
i, j: G
g: G i j
x: {y : Y & D1 y i}
transport (fun y : Y => D2 y j) 1 (((D2 x.1) _f g) (m x.1 i x.2)) =
m (x.1; ((D1 x.1) _f g) x.2).1 j (x.1; ((D1 x.1) _f g) x.2).2
    simpl.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, DiagramMap (D1 y) (D2 y)
i, j: G
g: G i j
x: {y : Y & D1 y i}
((D2 x.1) _f g) (m x.1 i x.2) = m x.1 j (((D1 x.1) _f g) x.2)
    apply (DiagramMap_comm (m x.1)).
  Defined.

  Definition sigma_diag_functor_equiv (m : forall y, (D1 y) ~d~ (D2 y))
    : (sigma_diagram D1) ~d~ (sigma_diagram D2).
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, D1 y ~d~ D2 y
sigma_diagram D1 ~d~ sigma_diagram D2
  Proof.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, D1 y ~d~ D2 y
sigma_diagram D1 ~d~ sigma_diagram D2
    srapply (Build_diagram_equiv (sigma_diagram_functor m)).
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, D1 y ~d~ D2 y
forall i : G, IsEquiv (sigma_diagram_functor (fun y : Y => m y) i)
    intros i.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, D1 y ~d~ D2 y
i: G
IsEquiv (sigma_diagram_functor (fun y : Y => m y) i)
    srapply isequiv_functor_sigma.
G: Graph
Y: Type
D1, D2: Y -> Diagram G
m: forall y : Y, D1 y ~d~ D2 y
i: G
forall a : Y,
IsEquiv
  ((fun y : Y =>
    let X :=
      fun y0 : Y => DiagramMap_obj ((fun y1 : Y => diag_equiv_map (m y1)) y0)
      in
    X y i) a)
    intros y; apply m.
  Defined.

End SigmaDiagram.