Library HoTT.Diagrams.Span

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

The underlying graph of a span.

Definition span_graph : Graph.
Proof.
  srapply (Build_Graph (Unit + Bool)).
  intros [i|i] [j|j].
  2: exact Unit.
  all: exact Empty.
Defined.

Section Span.

  Context {A B C : Type}.

A span is a diagram: f g B <-- A --> C

  Definition span (f : A → B) (g : A → C) : Diagram span_graph.
  Proof.
    srapply Build_Diagram.
    - intros [i|i].
      + exact A.
      + exact (if i then B else C).
    - intros [i|i] [j|j] u; cbn; try contradiction.
      destruct j.
      + exact f.
      + exact g.
  Defined.

End Span.