(*
Instance IdentitySubCategory `(C:Category Ob Hom) : SubCategory C (fun _ => True) (fun _ _ _ _ _ => True).
intros; apply Build_SubCategory.
(*
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))
; 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))
forall o2:C2, { o1:C1 & (F o1) ≅ o2 }.
(* Definition 7.1: (essentially) injective on objects *)
forall o2:C2, { o1:C1 & (F o1) ≅ o2 }.
(* Definition 7.1: (essentially) injective on objects *)
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
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