圏

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.
Record
category_data
    : Type@{max(category_data.u0+1,category_data.u1+1)} := make_category_data
  { ob : Type@{category_data.u0};
    hom : ob -> ob -> Type@{category_data.u1};
    identity : forall x : ob, hom x x;
    comp : forall x y z : ob, hom y z -> hom x y -> hom x z }.

Arguments make_category_data ob%_type_scope
  (hom identity comp)%_function_scope
Arguments ob c
Arguments hom c _ _
Arguments identity c {x}
Arguments comp c {x y z} _ _

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 _ ∘ _.
?h ∘ ?h0
     : ?c [?x, ?z]
where
?c : [ |- category_data]
?x : [ |- ob ?c]
?y : [ |- ob ?c]
?z : [ |- ob ?c]
?h : [ |- ?c [?y, ?z]]
?h0 : [ |- ?c [?x, ?y]]
Check (_ [_ , _]).
?c [?o, ?o0]
     : Type@{category_data.u1}
where
?c : [ |- category_data]
?o : [ |- ob ?c]
?o0 : [ |- ob ?c]
Check _ [ _ , _ ].
?c [?o, ?o0]
     : Type@{category_data.u1}
where
?c : [ |- category_data]
?o : [ |- ob ?c]
?o0 : [ |- ob ?c]

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).
id
     : C [a, a]
  Check C [ g +++ f ].
g ∘ f
     : C [a, c]
End Categories.

Definition preorder_as_category_data
  (P : preordered_type)
  : category_data.
P: preordered_type
category_data
Proof.
P: preordered_type
category_data
  unshelve econstructor.
P: preordered_type
Type@{category_data.u0}
P: preordered_type
?ob -> ?ob -> Type@{category_data.u1}
P: preordered_type
forall x : ?ob, ?hom x x
P: preordered_type
forall x y z : ?ob, ?hom y z -> ?hom x y -> ?hom x z
  -
P: preordered_type
Type@{category_data.u0}
    exact P.
  -
P: preordered_type
P -> P -> Type@{category_data.u1}
    intros x y.
P: preordered_type
x, y: P
Type@{category_data.u1}
    exact (P.(preorder_on_A).(R) x y).
  -
P: preordered_type
forall x : P, (fun x0 y : P => preorder_on_A P x0 y) x x
    simpl.
P: preordered_type
forall x : P, preorder_on_A P x x
    intros.
P: preordered_type
x: P
preorder_on_A P x x
    apply (P.(preorder_on_A).(refl)).
  -
P: preordered_type
forall x y z : P,
(fun x0 y0 : P => preorder_on_A P x0 y0) y z ->
(fun x0 y0 : P => preorder_on_A P x0 y0) x y ->
(fun x0 y0 : P => preorder_on_A P x0 y0) x z
    simpl.
P: preordered_type
forall x y z : P,
preorder_on_A P y z -> preorder_on_A P x y -> preorder_on_A P x z
    intros.
P: preordered_type
x, y, z: P
H: preorder_on_A P y z
H0: preorder_on_A P x y
preorder_on_A P x z
    apply (P.(preorder_on_A).(trans) H0 H).
Defined.

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

Definition preorder_as_category
  (P : preordered_type)
  : category.
P: preordered_type
category
Proof.
P: preordered_type
category
  exists (preorder_as_category_data P).
P: preordered_type
is_category (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.
is_category category_of_types_data
Proof.
is_category category_of_types_data
  constructor.
forall (a b : category_of_types_data) (f : category_of_types_data [a, b]),
id ∘ f = f
forall (a b : category_of_types_data) (f : category_of_types_data [a, b]),
f ∘ id = f
forall (a b c d : category_of_types_data) (f : category_of_types_data [a, b])
  (g : category_of_types_data [b, c]) (h : category_of_types_data [c, d]),
(h ∘ g) ∘ f = h ∘ (g ∘ f)
  -
forall (a b : category_of_types_data) (f : category_of_types_data [a, b]),
id ∘ f = f
    intros.
a, b: category_of_types_data
f: category_of_types_data [a, b]
id ∘ f = f
    simpl in *.
a, b: Type@{category_of_types_data.u0}
f: a -> b
(fun x : a => f x) = f
    reflexivity.
  -
forall (a b : category_of_types_data) (f : category_of_types_data [a, b]),
f ∘ id = f
    intros.
a, b: category_of_types_data
f: category_of_types_data [a, b]
f ∘ id = f
    simpl in *.
a, b: Type@{category_of_types_data.u0}
f: a -> b
(fun x : a => f x) = f
    reflexivity.
  -
forall (a b c d : category_of_types_data) (f : category_of_types_data [a, b])
  (g : category_of_types_data [b, c]) (h : category_of_types_data [c, d]),
(h ∘ g) ∘ f = h ∘ (g ∘ f)
    intros.
a, b, c, d: category_of_types_data
f: category_of_types_data [a, b]
g: category_of_types_data [b, c]
h: category_of_types_data [c, d]
(h ∘ g) ∘ f = h ∘ (g ∘ f)
    simpl in *.
a, b, c, d: Type@{category_of_types_data.u0}
f: a -> b
g: b -> c
h: c -> d
(fun x : a => h (g (f x))) = (fun x : a => h (g (f x)))
    reflexivity.
Qed.

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

Print category_of_types.
category_of_types =
{|
  C := category_of_types_data; C_is_category := category_of_types_is_category
|}
     : category

Check nat : category_of_types.
nat : category_of_types
     : category_of_types
(* {} | Set <= category_of_types_data.u0
Normalized constraints:
  *)
Check (fun n => n) : category_of_types [nat, nat].
(fun n : nat => n) : category_of_types [nat, nat]
     : category_of_types [nat, nat]
(* {} | Set <= category_of_types_data.u0
Normalized constraints:
  *)

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.
Record
displayed_category_data (C : category_data)
  : Type@{max(category_data.u0,category_data.u1,displayed_category_data.u0+1,displayed_category_data.u1+1)} := make_displayed_category_data
  { d_ob : C -> Type@{displayed_category_data.u0};
    d_hom : forall a b : C,
            C [a, b] -> d_ob a -> d_ob b -> Type@{displayed_category_data.u1};
    d_identity : forall (a : C) (x : d_ob a), d_hom a a id x x;
    d_comp : forall (a b c : C) (x : d_ob a) (y : d_ob b) 
               (z : d_ob c) (g : C [b, c]) (f : C [a, b]),
             d_hom b c g y z -> d_hom a b f x y -> d_hom a c (g ∘ f) x z }.

Arguments displayed_category_data C
Arguments make_displayed_category_data C
  (d_ob d_hom d_identity d_comp)%_function_scope
Arguments d_ob C d _
Arguments d_hom C d {a b} f _ _
Arguments d_identity C d {a x}
Arguments d_comp C d {a b c x y z g f} g' f'

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 _ [ _ +++' _ ].
?g' ∘' ?f'
     : ?d [?g ∘ ?f | ?x, ?z]
where
?C : [ |- category_data]
?d : [ |- displayed_category_data ?C]
?a : [ |- ob ?C]
?b : [ |- ob ?C]
?c : [ |- ob ?C]
?x : [ |- d_ob ?C ?d ?a]
?y : [ |- d_ob ?C ?d ?b]
?z : [ |- d_ob ?C ?d ?c]
?g : [ |- ?C [?b, ?c]]
?f : [ |- ?C [?a, ?b]]
?g' : [ |- ?d [?g | ?y, ?z]]
?f' : [ |- ?d [?f | ?x, ?y]]
Check _ [ _ | _ , _ ].
?d [?f | ?d0, ?d1]
     : Type@{displayed_category_data.u1}
where
?C : [ |- category_data]
?d : [ |- displayed_category_data ?C]
?a : [ |- ob ?C]
?b : [ |- ob ?C]
?f : [ |- ?C [?a, ?b]]
?d0 : [ |- d_ob ?C ?d ?a]
?d1 : [ |- d_ob ?C ?d ?b]

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.
Record
is_displayed_category (C : category) (D : displayed_category_data C)
  : Prop := make_is_displayed_category
  { d_lunit : forall (a b : C) (f : C [a, b]) (x : d_ob C D a)
                (y : d_ob C D b) (f' : D [f | x, y]),
              eq_dep (fun r : C [a, b] => D [r | x, y]) 
                (lunit C C) (d_id ∘' f') f';
    d_runit : forall (a b : C) (f : C [a, b]) (x : d_ob C D a)
                (y : d_ob C D b) (f' : D [f | x, y]),
              eq_dep (fun r : C [a, b] => D [r | x, y]) 
                (runit C C) (f' ∘' d_id) f';
    d_assoc : forall (a b c d : C) (f : C [a, b]) 
                (g : C [b, c]) (h : C [c, d]) (w : d_ob C D a)
                (x : d_ob C D b) (y : d_ob C D c) 
                (z : d_ob C D d) (f' : D [f | w, x]) 
                (g' : D [g | x, y]) (h' : D [h | y, z]),
              eq_dep (fun r : C [a, d] => D [r | w, z]) 
                (assoc C C) ((h' ∘' g') ∘' f') (h' ∘' (g' ∘' f')) }.

Arguments is_displayed_category C D
Arguments make_is_displayed_category C D
  (d_lunit d_runit d_assoc)%_function_scope
Arguments d_lunit C D i {a b f x y f'}
Arguments d_runit C D i {a b f x y f'}
Arguments d_assoc C D i {a b c d f g h w x y z f' g' h'}