Library HoTT.Diagrams.ParallelPair

Require Import Basics.
Require Import Types.
Require Import Diagrams.Graph.
Require Import Diagrams.Diagram.
Require Import Diagrams.Cocone.

Parallel pairs

Definition parallel_pair_graph : Graph.
Proof.
  srapply (Build_Graph Bool).
  intros i j.
  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.
Proof.
  srapply Build_Diagram.
  1: intros []; [exact A | exact B].
  intros [] [] []; [exact f | exact g].
Defined.

Cones on parallel_pairs

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.
Proof.
  srapply Build_Cocone.
  1: intros []; [exact (q o f) | exact q].
  intros [] [] []; [reflexivity | exact Hq].
Defined.