Require Import Basics.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Types.
Require Import Diagrams.Graph.
Require Import Diagrams.Diagram.
Require Import Diagrams.Cocone.

(** Parallel pairs *)

Definition parallel_pair_graph : Graph.
Graph
Proof.
Graph
  srapply (Build_Graph Bool).
Bool -> Bool -> Type
  intros i j.
i, j: Bool
Type
  exact (if i then if j then Empty else Bool else Empty).
Defined.

(** Parallel pair diagram *)

Definition parallel_pair {A B : Type} (f g : A -> B)
  : Diagram parallel_pair_graph.
A, B: Type
f, g: A -> B
Diagram parallel_pair_graph
Proof.
A, B: Type
f, g: A -> B
Diagram parallel_pair_graph
  srapply Build_Diagram.
A, B: Type
f, g: A -> B
parallel_pair_graph -> Type
A, B: Type
f, g: A -> B
forall i j : parallel_pair_graph,
parallel_pair_graph i j -> ?obj i -> ?obj j
  1: intros []; [exact A | exact B].
A, B: Type
f, g: A -> B
forall i j : parallel_pair_graph,
parallel_pair_graph i j ->
(fun X : parallel_pair_graph => if X then A else B) i ->
(fun X : parallel_pair_graph => if X then A else B) j
  intros [] [] []; [exact f | exact g].
Defined.

(** Cones on [parallel_pair]s *)

Definition Build_parallel_pair_cocone {A B Q} {f g : B -> A}
  `(q: A -> Q) (Hq: q o g == q o f)
  : Cocone (parallel_pair f g) Q.
A, B, Q: Type
f, g: B -> A
q: A -> Q
Hq: q o g == q o f
Cocone (parallel_pair f g) Q
Proof.
A, B, Q: Type
f, g: B -> A
q: A -> Q
Hq: q o g == q o f
Cocone (parallel_pair f g) Q
  srapply Build_Cocone.
A, B, Q: Type
f, g: B -> A
q: A -> Q
Hq: q o g == q o f
forall i : parallel_pair_graph,
parallel_pair f g i -> Q
A, B, Q: Type
f, g: B -> A
q: A -> Q
Hq: q o g == q o f
forall (i j : parallel_pair_graph)
(g0 : parallel_pair_graph i j),
?legs j o (parallel_pair f g) _f g0 == ?legs i
  1: intros []; [exact (q o f) | exact q].
A, B, Q: Type
f, g: B -> A
q: A -> Q
Hq: q o g == q o f
forall (i j : parallel_pair_graph)
(g0 : parallel_pair_graph i j),
(fun i0 : parallel_pair_graph =>
 if i0 as b return (parallel_pair f g b -> Q)
 then q o f
 else q) j o (parallel_pair f g) _f g0 ==
(fun i0 : parallel_pair_graph =>
 if i0 as b return (parallel_pair f g b -> Q)
 then q o f
 else q) i
  intros [] [] []; [reflexivity | exact Hq].
Defined.