proposition: Lemma Left_Functoriality x y (f : comma_proj (Left_Functor x) ~> comma_proj (Left_Functor y)) : fmap[G] (fmap[F] (fst f)) ∘ (fmap[G] (snd (κ E (Left_Functor x))⁻¹) ∘ `2 (φ E (Left_Functor x)) ∘ fst (to (κ E (Left_Functor x)))) ≈ fmap[G] (snd (κ E (Left_Functor y))⁻¹) ∘ `2 (φ E (Left_Functor y)) ∘ fst (to (κ E (Left_Functor y))) ∘ fst f.
proof: Proof. Opaque Left_Functor. given (ff : (Left_Functor x) ~{ F ↓ Id[C] }~> (Left_Functor y)). { exists (fst f, fmap[F] (fst f)). abstract (simpl; rewrite id_left, id_right; reflexivity). } destruct (`2 (projF E) (Left_Functor x) (Left_Functor y) ff). srewrite e0. do 2 rewrite fmap_comp. comp_left. rewrite (comp_assoc (fmap[G] (snd (to (κ E (Left_Functor x)))))). rewrite <- fmap_comp. rewrite (snd (iso_to_from (κ E (Left_Functor x)))). simpl snd. rewrite fmap_id. rewrite id_left. symmetry. spose (`2 (fmap[φ E] ff)) as X. rewrite !comp_assoc. rewrite <- X. comp_left. srewrite e. comp_right. rewrite (fst (iso_to_from (κ E (Left_Functor y)))). rewrite id_left. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Theory.Adjunction Category.Adjunction.Natural.Transformation Category.Adjunction.Natural.Transformation.Universal Category.Construction.Comma Category.Construction.Product Category.Instance.Cat Category.Instance.Fun Category.Instance.Sets