[Coq] Category in Coq

先日、スタートCoqで圏論 in honor of こんさんというイベントがあり、その時に書いたコード。ConCaTというライブラリを使い、オブジェクトが２つ、その間に射が１つという圏を書いてみた、というものです。


Add LoadPath "~/coq/ConCat/ConCaT" as ConCaT.
Print LoadPath.
Require Import ConCaT.CATEGORY_THEORY.CATEGORY.Category.

Inductive Two_ob : Type := Ob_A | Ob_B.
Inductive Two_mor : Two_ob -> Two_ob -> Type :=
| Id_A : Two_mor Ob_A Ob_A
| Id_B : Two_mor Ob_B Ob_B
| Mor_AB : Two_mor Ob_A Ob_B.
Section equal_two_mor.
Variable a b:Two_ob.

Definition Equal_Two_mor(f g:Two_mor a b) := True.
Check Equal_Two_mor.
(* Two_mor a b -> Two_mor a b -> Prop *)
Lemma Equal_Two_mor_equiv : Equivalence Equal_Two_mor.
Proof.
unfold Equal_Two_mor.
apply Build_Equivalence.
unfold Reflexive. intro x. auto.
apply Build_Partial_equivalence.
unfold Transitive. intros. auto.
unfold Symmetric. intros. auto.
Qed.
Canonical Structure Two_mor_setoid : Setoid :=
Equal_Two_mor_equiv.
End equal_two_mor.
Definition Comp_Two_mor : forall a b c:Two_ob,
Two_mor_setoid a b -> Two_mor_setoid b c ->
Two_mor_setoid a c.
Proof.
intros a b c Sab Sbc.
inversion Sab.
inversion Sbc.
apply Id_A.
rewrite <- H0 in H1. discriminate H1.
apply Mor_AB.
inversion Sbc.
rewrite <- H0 in H1. discriminate H1.
apply Id_B.
rewrite <- H0 in H1. discriminate H1.
inversion Sbc.
rewrite <- H0 in H1. discriminate H1.
apply Mor_AB.
rewrite <- H0 in H1. discriminate H1.
Defined.

Lemma Comp_Two_mor_congl : Congl_law Comp_Two_mor.
Proof.
unfold Congl_law. intros. simpl.
unfold Two_mor_setoid in *.
unfold Equal_Two_mor.
auto.
Qed.

Lemma Comp_Two_mor_congr : Congr_law Comp_Two_mor.
Proof.
unfold Congr_law. intros. simpl.
unfold Two_mor_setoid in *.
unfold Equal_Two_mor.
auto.
Qed.

Definition Comp_Two :=
Build_Comp Comp_Two_mor_congl Comp_Two_mor_congr.

Lemma Assoc_Two : Assoc_law Comp_Two.
Proof.
unfold Assoc_law. intros. simpl in *.
unfold Equal_Two_mor in *. auto.
Qed.

Definition Id_Two (a:Two_ob) : Two_mor_setoid a a :=
match a as a0 return (Two_mor a0 a0) with
| Ob_A => Id_A
| Ob_B => Id_B
end.

Lemma Idl_Two : Idl_law Comp_Two Id_Two.
Proof.
unfold Idl_law; simpl.
unfold Comp_Two; unfold Id_Two; unfold Equal_Two_mor; simpl.
intros; auto.
Qed.

Lemma Idr_Two : Idr_law Comp_Two Id_Two.
Proof.
unfold Idr_law; simpl.
unfold Comp_Two; unfold Id_Two; unfold Equal_Two_mor; simpl.
intros; auto.
Qed.

Canonical Structure Two := Build_Category Assoc_Two Idl_Two Idr_Two.