(****************************************************************************)
Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
Require Import Categories_ch1_3.
Require Import Functors_ch1_4.
Require Import Isomorphisms_ch1_5.
Defined.
Coercion FullSubCategoriesAreCategories : FullSubcategory >-> Category.
-(* every category is a subcategory of itself! *)
+(* every category is a subcategory of itself *)
(*
Instance IdentitySubCategory `(C:Category Ob Hom) : SubCategory C (fun _ => True) (fun _ _ _ _ _ => True).
intros; apply Build_SubCategory.
; eqv := fun a b f g => eqv _ _ (projT1 f) (projT1 g)
; comp := fun a b c f g => existT (Pmor a c) (projT1 f >>> projT1 g)
(@wsc_comp_included _ _ _ _ wsc _ _ _ _ _ (projT2 f) (projT2 g))
-
}.
intros; apply Build_Equivalence. unfold Reflexive.
intros; reflexivity.
forall o2:C2, { o1:C1 & (F o1) ≅ o2 }.
(* Definition 7.1: (essentially) injective on objects *)
+(* TODO *)
+
Class ConservativeFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
{ cf_reflect_iso : forall (a b:C1), (F a) ≅ (F b) -> a ≅ b
; cf_reflect_iso1 : forall a b (i:(F a) ≅ (F b)), F \ #(cf_reflect_iso a b i) ~~ #i