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