proposition: Theorem adj_monic {x y} (f : F x ~> y) c (g h : c ~> x) : Faithful F → Monic f -> ⌊f⌋ ∘ g ≈ ⌊f⌋ ∘ h → g ≈ h.
proof: Proof. intros. rewrite <- !to_adj_nat_l in X1. assert (Proper (@equiv _ unit_setoid ==> equiv) (λ _ : unit_setoid_object, f ∘ fmap[F] g)) as XA by proper. assert (Proper (@equiv _ unit_setoid ==> equiv) (λ _ : unit_setoid_object, f ∘ fmap[F] h)) as XB by proper. pose proof (monic (Monic:=@iso_to_monic Sets {| is_setoid := homset (fobj[F] c) y |} {| is_setoid := homset c (fobj[U] y) |} (@adj H c y)) unit_setoid_object {| morphism := λ _ : unit_setoid_object, f ∘ fmap[F] g |} {| morphism := λ _ : unit_setoid_object, f ∘ fmap[F] h |}) as X2. simpl in X2. now apply X, X0, X2. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Instance.Sets