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.

(** The underlying graph of a span. *)

Definition span_graph : Graph.
Graph
Proof.
Graph
  srapply (Build_Graph (Unit + Bool)).
Unit + Bool -> Unit + Bool -> Type
  intros [i|i] [j|j].
i, j: Unit
Type
i: Unit
j: Bool
Type
i: Bool
j: Unit
Type
i, j: Bool
Type
  2: exact Unit.
i, j: Unit
Type
i: Bool
j: Unit
Type
i, j: Bool
Type
  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.
A, B, C: Type
f: A -> B
g: A -> C
Diagram span_graph
  Proof.
A, B, C: Type
f: A -> B
g: A -> C
Diagram span_graph
    srapply Build_Diagram.
A, B, C: Type
f: A -> B
g: A -> C
span_graph -> Type
A, B, C: Type
f: A -> B
g: A -> C
forall i j : span_graph,
span_graph i j -> ?obj i -> ?obj j
    -
A, B, C: Type
f: A -> B
g: A -> C
span_graph -> Type intros [i|i].
A, B, C: Type
f: A -> B
g: A -> C
i: Unit
Type
A, B, C: Type
f: A -> B
g: A -> C
i: Bool
Type
      +
A, B, C: Type
f: A -> B
g: A -> C
i: Unit
Type exact A.
      +
A, B, C: Type
f: A -> B
g: A -> C
i: Bool
Type exact (if i then B else C).
    -
A, B, C: Type
f: A -> B
g: A -> C
forall i j : span_graph,
span_graph i j ->
(fun X : span_graph =>
 match X with
 | inl u => unit_name A u
 | inr b => (fun i0 : Bool => if i0 then B else C) b
 end) i ->
(fun X : span_graph =>
 match X with
 | inl u => unit_name A u
 | inr b => (fun i0 : Bool => if i0 then B else C) b
 end) j intros [i|i] [j|j] u; cbn; try contradiction.
A, B, C: Type
f: A -> B
g: A -> C
i: Unit
j: Bool
u: span_graph (inl i) (inr j)
A -> if j then B else C
      destruct j.
A, B, C: Type
f: A -> B
g: A -> C
i: Unit
u: span_graph (inl i) (inr true)
A -> B
A, B, C: Type
f: A -> B
g: A -> C
i: Unit
u: span_graph (inl i) (inr false)
A -> C
      +
A, B, C: Type
f: A -> B
g: A -> C
i: Unit
u: span_graph (inl i) (inr true)
A -> B exact f.
      +
A, B, C: Type
f: A -> B
g: A -> C
i: Unit
u: span_graph (inl i) (inr false)
A -> C exact g.
  Defined.

End Span.