Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Require Import Types.
Require Import Diagrams.Diagram.
Require Import Colimits.Colimit.
Require Import Colimits.Colimit_Sigma.
Require Import Diagrams.Graph.

(** * Colimit of product by a constant type *)

(** Given a diagram [D], one of his colimits [Q] and a type [A], one can consider the diagram of the products of the types of [D] and [A]. Then, a colimit of such a diagram is [A * Q]. *)

(** This is the constant case of the file [Colimit_Sigma] and we reuse its results. *)

Section ColimitProd.

  Context `{Funext} {G : Graph} (D : Diagram G) (A : Type).

  
H: Funext
G: Graph
D: Diagram G
A: Type
Diagram G

  
H: Funext
G: Graph
D: Diagram G
A: Type
Diagram G

    
H: Funext
G: Graph
D: Diagram G
A: Type
G -> Type
H: Funext
G: Graph
D: Diagram G
A: Type
forall i j : G, G i j -> ?obj i -> ?obj j

    
H: Funext
G: Graph
D: Diagram G
A: Type
G -> Type
 exact (fun i => A * (D i)).
    
H: Funext
G: Graph
D: Diagram G
A: Type
forall i j : G,
G i j ->
(fun i0 : G => A * D i0) i ->
(fun i0 : G => A * D i0) j
 
H: Funext
G: Graph
D: Diagram G
A: Type
i, j: G
f: G i j
x: A * D i
A * D j

      exact (fst x, D _f f (snd x)).
  Defined.

  
H: Funext
G: Graph
D: Diagram G
A: Type
sigma_diagram (fun _ : A => D) ~d~ prod_diagram

  
H: Funext
G: Graph
D: Diagram G
A: Type
sigma_diagram (fun _ : A => D) ~d~ prod_diagram

    
H: Funext
G: Graph
D: Diagram G
A: Type
DiagramMap (sigma_diagram (fun _ : A => D))
  prod_diagram
H: Funext
G: Graph
D: Diagram G
A: Type
forall i : G, IsEquiv (?m i)

    
H: Funext
G: Graph
D: Diagram G
A: Type
DiagramMap (sigma_diagram (fun _ : A => D))
  prod_diagram
 
H: Funext
G: Graph
D: Diagram G
A: Type
forall i : G, {_ : A & D i} -> A * D i
H: Funext
G: Graph
D: Diagram G
A: Type
forall (i j : G) (g : G i j) (x : {_ : A & D i}),
(fst (?Goal0 i x), (D _f g) (snd (?Goal0 i x))) =
?Goal0 j (x.1; (D _f g) x.2)

      
H: Funext
G: Graph
D: Diagram G
A: Type
forall i : G, {_ : A & D i} -> A * D i
 intro i; apply equiv_sigma_prod0.
      
H: Funext
G: Graph
D: Diagram G
A: Type
forall (i j : G) (g : G i j) (x : {_ : A & D i}),
(fst
   ((fun i0 : G =>
     let X :=
       fun A B : Type =>
       equiv_fun (equiv_sigma_prod0 A B) in
     X A (D i0)) i x),
(D _f g)
  (snd
     ((fun i0 : G =>
       let X :=
         fun A B : Type =>
         equiv_fun (equiv_sigma_prod0 A B) in
       X A (D i0)) i x))) =
(fun i0 : G =>
 let X :=
   fun A B : Type => equiv_fun (equiv_sigma_prod0 A B)
   in
 X A (D i0)) j (x.1; (D _f g) x.2)
 reflexivity.
    
H: Funext
G: Graph
D: Diagram G
A: Type
forall i : G,
IsEquiv
  ({|
     DiagramMap_obj :=
       (fun i0 : G =>
        let X :=
          fun A B : Type =>
          equiv_fun (equiv_sigma_prod0 A B) in
        X A (D i0))
       :
       forall i0 : G,
       sigma_diagram (fun _ : A => D) i0 ->
       prod_diagram i0;
     DiagramMap_comm :=
       (fun (i0 j : G) (g : G i0 j)
          (x : {_ : A & D i0}) => 1)
       :
       forall (i0 j : G) (g : G i0 j)
       (x : sigma_diagram (fun _ : A => D) i0),
       (prod_diagram _f g)
         (((fun i1 : G =>
            let X :=
              fun A B : Type =>
              equiv_fun (equiv_sigma_prod0 A B) in
            X A (D i1))
           :
           forall i1 : G,
           sigma_diagram (fun _ : A => D) i1 ->
           prod_diagram i1) i0 x) =
       ((fun i1 : G =>
         let X :=
           fun A B : Type =>
           equiv_fun (equiv_sigma_prod0 A B) in
         X A (D i1))
        :
        forall i1 : G,
        sigma_diagram (fun _ : A => D) i1 ->
        prod_diagram i1) j
         (((sigma_diagram (fun _ : A => D)) _f g) x)
   |} i)
 
H: Funext
G: Graph
D: Diagram G
A: Type
i: G
IsEquiv (fun H : {_ : A & D i} => (H.1, H.2))

      apply equiv_sigma_prod0.
  Defined.

  
H: Funext
G: Graph
D: Diagram G
A, Q: Type
HQ: IsColimit D Q
IsColimit prod_diagram (A * Q)

  
H: Funext
G: Graph
D: Diagram G
A, Q: Type
HQ: IsColimit D Q
IsColimit prod_diagram (A * Q)

    
H: Funext
G: Graph
D: Diagram G
A, Q: Type
HQ: IsColimit D Q
?Q <~> A * Q
H: Funext
G: Graph
D: Diagram G
A, Q: Type
HQ: IsColimit D Q
IsColimit prod_diagram ?Q

    
H: Funext
G: Graph
D: Diagram G
A, Q: Type
HQ: IsColimit D Q
?Q <~> A * Q
 apply equiv_sigma_prod0.
    
H: Funext
G: Graph
D: Diagram G
A, Q: Type
HQ: IsColimit D Q
IsColimit prod_diagram {_ : A & Q}
 
H: Funext
G: Graph
D: Diagram G
A, Q: Type
HQ: IsColimit D Q
prod_diagram ~d~ ?D2
H: Funext
G: Graph
D: Diagram G
A, Q: Type
HQ: IsColimit D Q
IsColimit ?D2 {_ : A & Q}

      
H: Funext
G: Graph
D: Diagram G
A, Q: Type
HQ: IsColimit D Q
prod_diagram ~d~ ?D2
 symmetry; exact diagram_equiv_prod_sigma.
      
H: Funext
G: Graph
D: Diagram G
A, Q: Type
HQ: IsColimit D Q
IsColimit (sigma_diagram (fun _ : A => D)) {_ : A & Q}
 by apply iscolimit_sigma.
  Defined.

End ColimitProd.