Last active
December 3, 2018 16:32
-
-
Save lthms/61dfad7486364687030984a5ff7f4b40 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Coq.Logic.ProofIrrelevance. | |
Require Import Coq.Program.Tactics. | |
Ltac simpl_exist_eq := | |
match goal with | |
| [ |- exist _ ?x _ = exist _ ?y _] | |
=> let H := fresh "H" | |
in cut (x = y); | |
[ intro H; | |
apply eq_sig with (p:=H); | |
apply proof_irrelevance | |
| (* nothing *) | |
] | |
end. | |
(** * Basic Constructions | |
** Categories | |
*** Definition | |
*) | |
Class category | |
{object: Type} | |
(arrow: object -> object -> Type) | |
:= { comp {c b a: object} | |
: arrow b c -> arrow a b -> arrow a c | |
; id (a: object) | |
: arrow a a | |
; comp_assoc_law {d c b a: object} | |
(h: arrow c d) | |
(g: arrow b c) | |
(f: arrow a b) | |
: comp (comp h g) f = comp h (comp g f) | |
; id_assoc_1_law {b a: object} | |
(f: arrow a b) | |
: comp (id b) f = f | |
; id_assoc_2_law {b a: object} | |
(f: arrow a b) | |
: comp f (id a) = f | |
}. | |
Arguments category [object] (arrow). | |
Arguments comp [object arrow _ c b a] (_ _). | |
Arguments id [object arrow _] (a). | |
Arguments comp_assoc_law [object arrow _ d c b a] (h g f). | |
Arguments id_assoc_1_law [object arrow _ b a] (f). | |
Arguments id_assoc_2_law [object arrow _ b a] (f). | |
Notation "f <<< g" := (comp f g) (at level 50). | |
Notation "g >>> f" := (f <<< g) (at level 50). | |
(** *** Example: the Set Category *) | |
Module SET. | |
Definition func := fun a b => a -> b. | |
Definition comp | |
{c b a: Type} | |
(g: func b c) | |
(f: func a b) | |
: func a c := | |
fun x => g (f x). | |
Definition id | |
(a: Type) | |
: func a a := | |
fun x => x. | |
Lemma comp_assoc_law | |
: forall {d c b a: Type} | |
(h: func c d) | |
(g: func b c) | |
(f: func a b), | |
comp (comp h g) f | |
= comp h (comp g f). | |
Proof. | |
reflexivity. | |
Qed. | |
Lemma id_assoc_1_law | |
: forall {b a: Type} | |
(f: func a b), | |
comp (id b) f = f. | |
Proof. | |
reflexivity. | |
Qed. | |
Lemma id_assoc_2_law | |
: forall {b a: Type} | |
(f: func a b), | |
comp f (id a) = f. | |
Proof. | |
reflexivity. | |
Qed. | |
Instance set_category | |
: category func := | |
{ comp := @comp | |
; id := id | |
; comp_assoc_law := @comp_assoc_law | |
; id_assoc_1_law := @id_assoc_1_law | |
; id_assoc_2_law := @id_assoc_2_law | |
}. | |
End SET. | |
(** *** Example: The 0 Category *) | |
Module O. | |
Inductive empty := . | |
Variable arrow : empty -> empty -> Type. | |
Definition comp | |
{c b a: empty} | |
(g: arrow b c) | |
(f: arrow a b) | |
: arrow a c. | |
inversion a. | |
Defined. | |
Definition id | |
(a: empty) | |
: arrow a a. | |
inversion a. | |
Defined. | |
Lemma comp_assoc_law | |
: forall {d c b a: empty} | |
(h: arrow c d) | |
(g: arrow b c) | |
(f: arrow a b), | |
comp (comp h g) f | |
= comp h (comp g f). | |
Proof. | |
inversion a. | |
Qed. | |
Lemma id_assoc_1_law | |
: forall {b a: empty} | |
(f: arrow a b), | |
comp (id b) f = f. | |
Proof. | |
inversion a. | |
Qed. | |
Lemma id_assoc_2_law | |
: forall {b a: empty} | |
(f: arrow a b), | |
comp f (id a) = f. | |
Proof. | |
inversion a. | |
Qed. | |
Instance empty_category | |
: category arrow := | |
{ comp := @comp | |
; id := id | |
; comp_assoc_law := @comp_assoc_law | |
; id_assoc_1_law := @id_assoc_1_law | |
; id_assoc_2_law := @id_assoc_2_law | |
}. | |
End O. | |
(** *** Example: Mon **) | |
Class monoid | |
{a: Type} | |
(op: a -> a -> a) | |
(e: a) := | |
{ op_assoc (x y z: a) | |
: op (op x y) z = op x (op y z) | |
; e_neutral_1_law (x: a) | |
: op x e = e | |
; e_neutral_2_law (x: a) | |
: op e x = e | |
}. | |
Section Homomorph. | |
Variables (a b: Type) | |
(op_a: a -> a -> a) | |
(e_a: a) | |
(op_b: b -> b -> b) | |
(e_b: b). | |
Definition homomorphism | |
`{monoid a op_a e_a} | |
`{monoid b op_b e_b} | |
:= { f: a -> b | f e_a = e_b /\ forall (x y: a), f (op_a x y) = op_b (f x) (f y) }. | |
End Homomorph. | |
Arguments homomorphism (a b) [op_a e_a op_b e_b _ _]. | |
Module Mon. | |
Record Monoid := | |
{ set: Type | |
; op: set -> set -> set | |
; e: set | |
; monoid_instance :> monoid op e | |
}. | |
Definition Homomorphism | |
(a b: Monoid) | |
:= homomorphism (H := monoid_instance a) | |
(H0 := monoid_instance b) | |
(set a) | |
(set b). | |
Program Definition comp | |
{c b a: Monoid} | |
(g: Homomorphism b c) | |
(f: Homomorphism a b) | |
: Homomorphism a c := | |
fun x => g (f x). | |
Next Obligation. | |
induction f as [f [Hf_e Hf_op]]. | |
induction g as [g [Hg_e Hg_op]]. | |
cbn in *. | |
split. | |
+ now (rewrite Hf_e; rewrite Hg_e). | |
+ intros x y. | |
now (rewrite Hf_op; rewrite Hg_op). | |
Defined. | |
Program Definition id | |
(a: Monoid) | |
: Homomorphism a a := | |
fun x => x. | |
Lemma comp_assoc_law | |
: forall {d c b a: Monoid} | |
(h: Homomorphism c d) | |
(g: Homomorphism b c) | |
(f: Homomorphism a b), | |
comp (comp h g) f | |
= comp h (comp g f). | |
Proof. | |
intros d c b a [h [Hh_e Hh_op]] [g [Hg_e Hg_op]] [f [Hf_e Hf_op]]. | |
unfold comp in *. | |
cbn in *. | |
simpl_exist_eq. | |
reflexivity. | |
Qed. | |
Lemma id_assoc_1_law | |
: forall {b a: Monoid} | |
(f: Homomorphism a b), | |
comp (id b) f = f. | |
Proof. | |
intros b a [f [Hf_e Hf_op]]. | |
unfold comp, id in *. | |
cbn in *. | |
simpl_exist_eq. | |
now repeat rewrite id_assoc_1_law. | |
Qed. | |
Lemma id_assoc_2_law | |
: forall {b a: Monoid} | |
(f: Homomorphism a b), | |
comp f (id a) = f. | |
Proof. | |
intros b a [f [Hf_e Hf_op]]. | |
unfold comp, id in *. | |
cbn in *. | |
simpl_exist_eq. | |
now repeat rewrite id_assoc_2_law. | |
Qed. | |
Instance mon_category | |
: category Homomorphism := | |
{ comp := @comp | |
; id := id | |
; comp_assoc_law := @comp_assoc_law | |
; id_assoc_1_law := @id_assoc_1_law | |
; id_assoc_2_law := @id_assoc_2_law | |
}. | |
End Mon. | |
(** *** Example: The Cat→ Category *) | |
Module CatArrow. | |
Variables (object: Type) | |
(arrow: object -> object -> Type). | |
Record cat_arrow_object := | |
{ dom: object | |
; cod: object | |
; fn: arrow dom cod | |
}. | |
Definition cat_arrow_arrow | |
`{category object arrow} | |
(f f': cat_arrow_object) := | |
{ o | comp (fn f') (fst o) = comp (snd o) (fn f)}. | |
Program Definition comp | |
`{category object arrow} | |
{c b a: cat_arrow_object} | |
(g: cat_arrow_arrow b c) | |
(f: cat_arrow_arrow a b) | |
: cat_arrow_arrow a c := | |
(comp (fst g) (fst f), comp (snd g) (snd f)). | |
Next Obligation. | |
induction f as [(x,y) Hf]; induction g as [(x',y') Hg]. | |
cbn in *. | |
rewrite <- (comp_assoc_law (fn c) _ _). | |
rewrite Hg. | |
rewrite (comp_assoc_law y' _ _). | |
rewrite Hf. | |
rewrite <- (comp_assoc_law y' _ _). | |
reflexivity. | |
Defined. | |
Program Definition id | |
`{category object arrow} | |
(a: cat_arrow_object) | |
: cat_arrow_arrow a a := | |
(id (dom a), id (cod a)). | |
Next Obligation. | |
rewrite id_assoc_1_law. | |
rewrite id_assoc_2_law. | |
reflexivity. | |
Defined. | |
Lemma comp_assoc_law | |
`{category object arrow} | |
: forall {d c b a: cat_arrow_object} | |
(h: cat_arrow_arrow c d) | |
(g: cat_arrow_arrow b c) | |
(f: cat_arrow_arrow a b), | |
comp (comp h g) f | |
= comp h (comp g f). | |
Proof. | |
intros [A B f] [A' B' f'] [A'' B'' f''] [A''' B''' f'''] | |
[(x,y) Hh] [(x',y') Hg] [(x'',y'') Hf]. | |
unfold comp. | |
cbn in *. | |
simpl_exist_eq. | |
now repeat rewrite comp_assoc_law. | |
Qed. | |
Lemma id_assoc_1_law | |
`{category object arrow} | |
: forall {b a: cat_arrow_object} | |
(f: cat_arrow_arrow a b), | |
comp (id b) f = f. | |
Proof. | |
intros [A B f] [A' B' f'] [(a,b) G]. | |
cbn. | |
unfold comp, id in *. | |
cbn in *. | |
simpl_exist_eq. | |
now repeat rewrite id_assoc_1_law. | |
Qed. | |
Lemma id_assoc_2_law | |
`{category object arrow} | |
: forall {b a: cat_arrow_object} | |
(f: cat_arrow_arrow a b), | |
comp f (id a) = f. | |
Proof. | |
intros [A B f] [A' B' f'] [(a,b) G]. | |
cbn. | |
unfold comp, id in *. | |
cbn in *. | |
simpl_exist_eq. | |
now repeat rewrite id_assoc_2_law. | |
Qed. | |
Instance cat_arrow_category | |
`{H: category object arrow} | |
: category cat_arrow_arrow := | |
{ comp := @comp H | |
; id := id | |
; comp_assoc_law := @comp_assoc_law H | |
; id_assoc_1_law := @id_assoc_1_law H | |
; id_assoc_2_law := @id_assoc_2_law H | |
}. | |
End CatArrow. | |
Section Morphism. | |
Variables (object: Type) | |
(arrow: object -> object -> Type). | |
Definition monomorphism | |
`{category object arrow} | |
{c b: object} | |
(f: arrow b c) | |
:= forall {a: object} | |
(g h: arrow a b), | |
g >>> f = h >>> f -> g = h. | |
Definition epimorphism | |
`{category object arrow} | |
{c b: object} | |
(f: arrow b c) | |
:= forall {a: object} | |
(g h: arrow c a), | |
f >>> g = f >>> h -> g = h. | |
End Morphism. | |
Arguments monomorphism [object arrow H c b] (f). | |
Arguments epimorphism [object arrow H c b] (f). |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment