Library UniMath.CategoryTheory.limits.StandardDiagrams


Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.

Require Import UniMath.Combinatorics.StandardFiniteSets.
Require Import UniMath.Combinatorics.FiniteSets.

Local Open Scope cat.
Local Open Scope stn.

Standard graphs and diagrams.

Contents 1. Graphs 2. Diagram constructors 3. Cocone constructors

Section graphs.
1. Graphs.

  Definition empty_graph : graph
    := make_graph empty (λ _ _, empty).

  Definition unit_graph : graph
    := make_graph unit (λ _ _, empty).

  Definition bool_graph : graph
    := make_graph bool (λ _ _, empty).

  Definition interval_graph : graph.
  Show proof.
    use make_graph.
    - exact bool.
    - intros a b.
      induction a; induction b.
      + exact empty.
      + exact unit.       + exact empty.
      + exact empty.

  Definition span_graph : graph.
  Show proof.
    use make_graph.
    - exact three.
    - use three_rec.
      + apply three_rec.
        * exact empty.
        * exact unit.
        * exact unit.
      + exact(λ _, empty).
      + exact(λ _, empty).

  Definition discrete_graph (X : UU) : graph
    := make_graph X (λ _ _, empty).


  Definition parallell_graph (X : UU) : graph.
  Show proof.
    use make_graph.
    - exact two.
    - use two_rec_dep.
      + exact(two_rec empty X).
      + exact(λ _, empty).

  Definition parallell_start {X : UU}
    : vertex (parallell_graph X)
    := (● 0).

  Definition parallell_end {X : UU}
    : vertex (parallell_graph X)
    := (● 1).

  Definition parallell_edge {X : UU}
    (e : X)
    : @edge (parallell_graph X) parallell_start parallell_end
    := e.


  Definition pair_graph : graph
    := parallell_graph (unit ⨿ unit).

  Definition pair_src : vertex pair_graph
    := (● 0).

  Definition pair_dst : vertex pair_graph
    := (● 1).

  Definition pair_left : @edge pair_graph pair_src pair_dst
    := inl tt.

  Definition pair_right : @edge pair_graph pair_src pair_dst
    := inr tt.

  Definition multispan_graph (X : UU) : graph.
  Show proof.
    use make_graph.
    - exact(X ⨿ unit).     - use coprod_rect.
      + exact(λ _ _, empty).       + apply unit_rect.
        apply coprod_rect.
        * exact(λ _, unit).         * exact(λ _, empty).

  Definition multispan_vertex {X : UU}
    (x : X)
    : vertex (multispan_graph X)
    := (inl x).

  Definition multispan_base {X : UU}
    : vertex (multispan_graph X)
    := (inr tt).

  Definition multispan_edge {X : UU}
    (x : X)
    : edge multispan_base (multispan_vertex x)
    := tt.

End graphs.

Section diagrams.
2. Diagram constructors.

  Definition make_empty_diagram {C : category}
    : diagram empty_graph C
    := make_diagram
         (fromempty : vertex empty_graph -> C)
         (λ _ _, fromempty).

  Definition make_unit_diagram {C : category}
    (point : C)
    : diagram unit_graph C.
  Show proof.
    use make_diagram.
    - exact(unit_rect _ point).
    - exact(λ _ _, empty_rect _).

  Definition make_bool_diagram {C : category}
    (a b : C)
    : diagram bool_graph C.
  Show proof.
    use make_diagram.
    - exact(bool_rect _ a b).
    - intros *; exact fromempty.

  Definition make_interval_diagram {C : category}
    (x : C)
    (y : C)
    (f : x --> y)
    : diagram interval_graph C.
  Show proof.
    use make_diagram.
    - exact(bool_rect _ x y).
    - intros a b; destruct a, b; try (exact fromempty).
      exact(λ _ , f).

  Definition make_span_diagram {C : category }
    (a b c : C)
    (f : C ⟦a, b⟧)
    (g : C⟦a, c⟧)
    : diagram span_graph C.
  Show proof.
    use make_diagram.
    - exact(three_rec a b c).
    - use three_rec_dep; use three_rec_dep; try exact(empty_rect _).
      + exact(unit_rect _ f).
      + exact(unit_rect _ g).

  Definition make_discrete_diagram {J : category} {X : UU}
    (objects : X -> J)
    : diagram (discrete_graph X) J.
  Show proof.
    use make_diagram.
    - exact objects.
    - exact(λ _ _, empty_rect _).

  Definition make_discrete_diagram' {J : category}
    {g : graph}
    (d : diagram g J)
    : diagram (discrete_graph (vertex g)) J.
  Show proof.
    use make_diagram.
    - exact(dob d).
    - exact(λ _ _, empty_rect _).

  Definition make_parallell_diagram {C : category}
    (X : UU)
    (x y : C)
    (f : ∏ (t : X), x --> y)
    : diagram (parallell_graph X) C.
  Show proof.
    use make_diagram.
    - exact(two_rec x y).
    - use two_rec_dep.
      + use(two_rec_dep _ (empty_rect _) f).
      + exact(λ _, empty_rect _).

  Definition make_pair_diagram {C : category}
    (a b : C)
    (f g : a --> b)
    : diagram pair_graph C.
  Show proof.
    apply(make_parallell_diagram (unit ⨿ unit) a b).
    exact(sumofmaps (λ _, f) (λ _, g)).

  Definition make_multispan_diagram {J : category}
    (X : UU)
    (base : J)
    (endpoint : ∏ (x : X), J)
    (morphism : ∏ (x : X), J⟦ base, endpoint x ⟧)
    : diagram (multispan_graph X) J.
  Show proof.
    use make_diagram.
    - exact(sumofmaps endpoint (λ _, base)).
    - use coprod_rect.
      + exact(λ _ _, empty_rect _).
      + apply unit_rect.
        use coprod_rect.
        * exact(λ (a : X) (_ : unit), morphism a).
        * exact(λ _, empty_rect _).
End diagrams.

Section cocones.

3. Constructors of cocones.
  Definition make_empty_cocone {J : category}
    (d : diagram empty_graph J)
    (j : J)
    : cocone d j.
  Show proof.
    use make_cocone.
    - exact(empty_rect _).
    - exact(λ _ _, empty_rect _).

  Definition make_discrete_cocone {J : category} {X : UU}
    (d : diagram (discrete_graph X) J)
    (z : J)
    (f : ∏ (x : X), J⟦dob d x, z⟧)
    : cocone d z.
  Show proof.
    use make_cocone.
    - exact f.
    - exact(λ _ _, empty_rect _).

  Definition make_parallell_cocone {J : category} {X : UU}
    (d : diagram (parallell_graph X) J)
    (z : J)
    (in₀ : dob d (stnpr 0) --> z)
    (in₁ : dob d (stnpr 1) --> z)
    (commutes : ∏ (x : X), dmor d (x : @edge (parallell_graph X) (stnpr 0) (stnpr 1)) · in₁ = in₀)
    : cocone d z.
  Show proof.
    use make_cocone.
    - exact(two_rec_dep _ in₀ in₁).
    - abstract(use(two_rec_dep _ (two_rec_dep _ (empty_rect _) commutes)); exact(λ _, empty_rect _)).

  Lemma parallell_cocone_commutes {J : category} {X : UU}
    {d : diagram (parallell_graph X) J}
    {j : J}
    (cc : cocone d j)
    (x : X)
    : dmor d (parallell_edge x) · coconeIn cc parallell_end = coconeIn cc parallell_start.
  Show proof.
    exact(coconeInCommutes cc parallell_start parallell_end (parallell_edge x)).

  Definition make_pair_cocone {J : category} {X : UU}
    (d : diagram pair_graph J)
    (j : J)
    (src_in : J⟦dob d pair_src, j⟧)
    (dst_in : J⟦dob d pair_dst, j⟧)
    (com_left : dmor d pair_left · dst_in = src_in)
    (com_right : dmor d pair_right · dst_in = src_in)
    : cocone d j.
  Show proof.
    use make_parallell_cocone.
    - exact src_in.
    - exact dst_in.
    - abstract(use coprod_rect; apply unit_rect; assumption).

  Lemma pair_cocone_commutes {J : category}
    {d : diagram pair_graph J}
    {j : J}
    (cc : cocone d j)
    (e : edge pair_src pair_dst)
    : dmor d e · coconeIn cc pair_dst = coconeIn cc pair_src.
  Show proof.
    exact(coconeInCommutes cc pair_src pair_dst e).

  Definition make_multispan_cocone {J : category} {X : UU}
    (d : diagram (multispan_graph X) J)
    (apex : J)
    (base_inject : J⟦ dob d multispan_base, apex ⟧)
    (inject : ∏ (x : X), J⟦ dob d (multispan_vertex x), apex ⟧)
    (commutes : ∏ (x : X), dmor d (multispan_edge x) · inject x = base_inject)
    : cocone d apex.
  Show proof.
    use make_cocone.
    - apply coprod_rect.
      + exact inject.
      + apply unit_rect.
        exact base_inject.
    - abstract(use coprod_rect; [exact(λ _ _, empty_rect _) | use unit_rect ];
               use coprod_rect; cbn; [exact(λ a, unit_rect _ (commutes a))
                                       |exact(λ _, empty_rect _)]).

  Lemma multispan_cocone_commutes {J : category} {X : UU}
    {d : diagram (multispan_graph X) J}
    {apex : J}
    (cc : cocone d apex)
    (z : X)
    : (dmor d (multispan_edge z)) · coconeIn cc (multispan_vertex z) = coconeIn cc multispan_base.
  Show proof.
    exact(coconeInCommutes cc multispan_base (multispan_vertex z) tt).

End cocones.

Section finite.
  Definition is_finite_graph (g : graph) : UU
    := isfinite (vertex g)
         × ∏ (a b : vertex g), isfinite (edge a b).

  Definition finite_vertexset {g : graph} (gfinite : is_finite_graph g)
    : isfinite (vertex g)
    := pr1 gfinite.

  Definition finite_edgeset {g : graph} (gfinite : is_finite_graph g)
    : ∏ (a b : vertex g), isfinite (edge a b)
    := pr2 gfinite.

  Lemma is_finite_graph_empty
    : is_finite_graph empty_graph.
  Show proof.
    split.
    - exact isfiniteempty.
    - exact(λ _ _, isfiniteempty).

  Lemma is_finite_graph_unit
    : is_finite_graph unit_graph.
  Show proof.
    split.
    - exact isfiniteunit.
    - exact(λ _ _, isfiniteempty).

  Lemma is_finite_graph_bool
    : is_finite_graph bool_graph.
  Show proof.
    split.
    - exact isfinitebool.
    - exact(λ _ _, isfiniteempty).

  Lemma is_finite_graph_pair
    : is_finite_graph pair_graph.
  Show proof.
    split.
    - exact(isfinitestn 2).
    - use two_rec_dep; use two_rec_dep; try exact isfiniteempty.
      apply isfinitecoprod; apply isfiniteunit.

  Lemma is_finite_graph_interval
    : is_finite_graph interval_graph.
  Show proof.
    split.
    - exact isfinitebool.
    - use bool_rect; use bool_rect; try exact isfiniteempty.
      exact isfiniteunit.
End finite.