(*|
圏
==
|*)

Import EqNotations.
Require Import preorder.
From Stdlib Require Import Logic.ProofIrrelevance.

Set Printing Universes.

Record category_data : Type :=
  make_category_data {
    ob  :> Type;
    hom : ob -> ob -> Type;

    identity {x} : hom x x;

    comp {x y z} :
      hom y z ->
      hom x y ->
      hom x z;
  }.

Print category_data.

Definition id {C : category_data} {x}
  : C.(hom) x x :=
  identity C.

Notation "C [ g +++ f ]" := (comp C g f) (at level 1).

Notation "g ∘ f" := (comp _ g f) (at level 50).

Notation "C [ a , b ]" := (hom C a b) (at level 1).

Check _ ∘ _.
Check (_ [_ , _]).
Check _ [ _ , _ ].

Record is_category (C : category_data) : Prop :=
  make_is_category {
    lunit {a b} {f : C [ a , b ]}
      : id ∘ f = f;

    runit {a b} {f : C [ a , b ]}
      : f ∘ id = f;

    assoc {a b c d}
      {f : C [ a , b ]}
      {g : C [ b , c ]}
      {h : C [ c , d ]}
      : (h ∘ g) ∘ f = h ∘ (g ∘ f);
  }.

Record category : Type :=
  make_category {
    C :> category_data;
    C_is_category :> is_category C;
  }.

Section Categories.
  Variable C : category.
  Variable a b c : C.
  Variable f : C.(hom) a b.
  Variable g : C.(hom) b c.

  Check id (x := a).
  Check C [ g +++ f ].
End Categories.

Definition preorder_as_category_data
  (P : preordered_type)
  : category_data.
Proof.
  unshelve econstructor.
  -
    exact P.
  -
    intros x y.
    exact (P.(preorder_on_A).(R) x y).
  -
    simpl.
    intros.
    apply (P.(preorder_on_A).(refl)).
  -
    simpl.
    intros.
    apply (P.(preorder_on_A).(trans) H0 H).
Defined.

Lemma preorder_is_category
  (P : preordered_type)
  : is_category (preorder_as_category_data P).
Proof.
  constructor;
    (
      simpl;
      intros;
      apply proof_irrelevance
    ).
Qed.

Definition preorder_as_category
  (P : preordered_type)
  : category.
Proof.
  exists (preorder_as_category_data P).
  apply preorder_is_category.
Defined.

(*|
型の圏
------
|*)

Definition category_of_types_data : category_data :=
  {|
    ob       := Type;
    hom      := fun A B => A -> B;
    identity := fun _ x => x;
    comp     := fun _ _ _ g f x => g (f x);
  |}.

Lemma category_of_types_is_category
  : is_category category_of_types_data.
Proof.
  constructor.
  -
    intros.
    simpl in *.
    reflexivity.
  -
    intros.
    simpl in *.
    reflexivity.
  -
    intros.
    simpl in *.
    reflexivity.
Qed.

Definition category_of_types : category.
Proof.
  exists category_of_types_data.
  apply category_of_types_is_category.
Defined.

Print category_of_types.

Check nat : category_of_types.
Check (fun n => n) : category_of_types [nat, nat].

(*|
Displayed category
------------------
|*)

Record displayed_category_data
  (C : category_data)
  : Type :=
  make_displayed_category_data {
    d_ob : C.(ob) -> Type;

    d_hom {a b} (f : C[a, b])
      : d_ob a -> d_ob b -> Type;

    d_identity {a} {x : d_ob a}
      : d_hom id x x;

    d_comp {a b c} {x y z}
      {g : C[b, c]}
      {f : C[a, b]}
      (g' : d_hom g y z)
      (f' : d_hom f x y)
      : d_hom (g ∘ f) x z;
  }.

Print displayed_category_data.

Definition d_id
  {C : category_data}
  {D : displayed_category_data C}
  {a}
  {x : D.(d_ob _) a}
  : D.(d_hom _) id x x :=
  d_identity C D.

Notation "D [ g +++' f ]" := (d_comp _ D g f) (at level 1).

Notation "g' ∘' f'" := (d_comp _ _ g' f') (at level 50).

Notation "D [ f | x , y ]" := (d_hom _ D f x y) (at level 1).

Check _ [ _ +++' _ ].
Check _ [ _ | _ , _ ].

Definition eq_dep
  {A : Type}
  (P : A -> Type)
  {a b : A}
  (e : a = b)
  (x : P a)
  (y : P b)
  : Prop :=
  (rew [P] e in x) = y.

Record is_displayed_category
  (C : category)
  (D : displayed_category_data C)
  : Prop :=
  make_is_displayed_category {
    d_lunit
      {a b}
      {f : C [ a , b ]}
      {x y}
      {f' : D [ f | x , y ]}
      :
      eq_dep
        (fun r => D [ r | x , y ])
        (C.(lunit _))
        (d_id ∘' f')
        f';

    d_runit
      {a b}
      {f : C [ a , b ]}
      {x y}
      {f' : D [ f | x , y ]}
      :
      eq_dep
        (fun r => D [ r | x , y ])
        (C.(runit _))
        (f' ∘' d_id)
        f';

    d_assoc
      {a b c d}
      {f : C [ a , b ]}
      {g : C [ b , c ]}
      {h : C [ c , d ]}
      {w x y z}
      {f' : D [ f | w , x ]}
      {g' : D [ g | x , y ]}
      {h' : D [ h | y , z ]}
      :
      eq_dep
        (fun r => D [ r | w , z ])
        (C.(assoc _))
        ((h' ∘' g') ∘' f')
        (h' ∘' (g' ∘' f'));
  }.

Print is_displayed_category.