1 Generalizable All Variables.
2 Require Import Notations.
3 Require Import Categories_ch1_3.
4 Require Import Functors_ch1_4.
5 Require Import Isomorphisms_ch1_5.
7 (******************************************************************************)
8 (* Chapter 2.1: Epic and Monic morphisms *)
9 (******************************************************************************)
12 Class Monic `{C:Category}{a b:C}(f:a~>b) : Prop :=
13 monic : forall c (g1 g2:c~>a), g1>>>f ~~ g2>>>f -> g1~~g2.
14 Implicit Arguments monic [ C a b Ob Hom ].
17 Class Epic `{C:Category}{a b:C}(f:a~>b) : Prop :=
18 epic : forall c (g1 g2:b~>c), f>>>g1 ~~ f>>>g2 -> g1~~g2.
19 Implicit Arguments epic [ C a b Ob Hom ].
22 Instance iso_epic `(i:Isomorphic) : Epic #i.
23 simpl; unfold Epic; intros.
24 setoid_rewrite <- left_identity.
25 setoid_rewrite <- iso_comp2.
26 setoid_rewrite associativity.
27 setoid_rewrite H; reflexivity.
31 Instance iso_monic `(i:Isomorphic) : Monic #i.
32 simpl; unfold Monic; intros.
33 setoid_rewrite <- right_identity.
34 setoid_rewrite <- iso_comp1.
35 setoid_rewrite <- associativity.
36 setoid_rewrite H; reflexivity.
39 (* a BiMorphism is an epic monic *)
40 Class BiMorphism `{C:Category}{a b:C}(f:a~>b) : Prop :=
41 { bimorphism_epic :> Epic f
42 ; bimorphism_monic :> Monic f
44 Coercion bimorphism_epic : BiMorphism >-> Epic.
45 Coercion bimorphism_monic : BiMorphism >-> Monic.
47 Class EndoMorphism `{C:Category}(A:C) :=
50 Class AutoMorphism `{C:Category}(A:C) : Type :=
51 { auto_endo1 : EndoMorphism A
52 ; auto_endo2 : EndoMorphism A
53 ; auto_iso : Isomorphism (@endo _ _ _ _ auto_endo1) (@endo _ _ _ _ auto_endo2)
56 (*Class Balanced `{C:Category} : Prop :=
57 balanced : forall (a b:C)(f:a~>b), BiMorphism f -> Isomorphism f.*)