# Library CategoryMorphisms

Require Import Utf8.
Require Import ProofIrrelevance FunctionalExtensionality.
Require Import JMeq.
Require Export Category.
Require Import Notations.

Set Implicit Arguments.

Generalizable All Variables.

# Category Morphisms

Section category_morphisms.
Context `(C : @Category obj).

Local Open Scope morphism_scope.

Quoting Wikipedia,
In category theory, an epimorphism (also called an epic morphism or, colloquially, an epi) is a morphism f : X Y which is right-cancellative in the sense that, for all morphisms g, g' : Y Z, g f = g' f g = g'
Epimorphisms are analogues of surjective functions, but they are not exactly the same. The dual of an epimorphism is a monomorphism (i.e. an epimorphism in a category C is a monomorphism in the dual category C op).

Definition IsEpimorphism x y (m : C.(Morphism) x y) : Prop :=
z (m1 m2 : C.(Morphism) y z), m1 m = m2 m
m1 = m2.
Definition IsMonomorphism x y (m : C.(Morphism) x y) : Prop :=
z (m1 m2 : C.(Morphism) z x), m m1 = m m2
m1 = m2.

Section properties.
Lemma IdentityIsEpimorphism x : IsEpimorphism _ _ (Identity x).
repeat intro; autorewrite with category in *; trivial.
Qed.

Lemma IdentityIsMonomorphism x : IsMonomorphism _ _ (Identity x).
repeat intro; autorewrite with category in *; trivial.
Qed.

Lemma EpimorphismComposition s d d' m0 m1 :
IsEpimorphism _ _ m0
→ IsEpimorphism _ _ m1
→ IsEpimorphism _ _ (Compose (C := C) (s := s) (d := d) (d' := d') m0 m1).
repeat intro.
repeat match goal with | [ H : _ |- _ ] ⇒ rewrite <- Associativity in H end.
intuition.
Qed.

Lemma MonomorphismComposition s d d' m0 m1 :
IsMonomorphism _ _ m0
→ IsMonomorphism _ _ m1
→ IsMonomorphism _ _ (Compose (C := C) (s := s) (d := d) (d' := d') m0 m1).
repeat intro.
repeat match goal with | [ H : _ |- _ ] ⇒ rewrite Associativity in H end.
intuition.
Qed.
End properties.
End category_morphisms.

Hint Immediate @IdentityIsEpimorphism @IdentityIsMonomorphism @MonomorphismComposition @EpimorphismComposition : category.
Hint Immediate @IdentityIsEpimorphism @IdentityIsMonomorphism @MonomorphismComposition @EpimorphismComposition : morphism.

Arguments IsEpimorphism {obj} [C x y] m.
Arguments IsMonomorphism {obj} [C x y] m.

Section AssociativityComposition.
Context `(C : @Category obj).
Variables o0 o1 o2 o3 o4 : C.

Local Open Scope morphism_scope.

Lemma compose4associativity_helper
(a : Morphism C o3 o4) (b : Morphism C o2 o3)
(c : Morphism C o1 o2) (d : Morphism C o0 o1) :
(a b) (c d) = a ((b c) d).
repeat rewrite Associativity; reflexivity.
Qed.
End AssociativityComposition.

Ltac compose4associativity' a b c d :=
transitivity (a ((b c) d))%morphism;
try solve [ apply compose4associativity_helper ].
Ltac compose4associativity :=
match goal with
| [ |- ((?a ?b) (?c ?d))%morphism = _ ] ⇒ compose4associativity' a b c d
| [ |- _ = ((?a ?b) (?c ?d))%morphism ] ⇒ compose4associativity' a b c d
end.