proposition: Lemma Right_Functoriality x y (f : comma_proj (Right_Functor x) ~> comma_proj (Right_Functor y)) : snd f ∘ (snd (θ E (Right_Functor x))⁻¹ ∘ `2 ((lawvere_iso E)⁻¹ (Right_Functor x)) ∘ fmap[F] (fst (to (θ E (Right_Functor x))))) ≈ snd (θ E (Right_Functor y))⁻¹ ∘ `2 ((lawvere_iso E)⁻¹ (Right_Functor y)) ∘ fmap[F] (fst (to (θ E (Right_Functor y)))) ∘ fmap[F] (fmap[G] (snd f)).
proof: Proof. Opaque Right_Functor. given (ff : (Right_Functor x) ~{ Id[D] ↓ G }~> (Right_Functor y)). { exists (fmap[G] (snd f), snd f). abstract (simpl; rewrite id_left, id_right; reflexivity). } destruct (`2 (projG E) (Right_Functor x) (Right_Functor y) ff). symmetry. srewrite e. rewrite <- comp_assoc. rewrite <- fmap_comp. rewrite !comp_assoc. rewrite (fst (iso_to_from (θ E (Right_Functor y)))). rewrite id_left. symmetry. srewrite e0. comp_left. rewrite (comp_assoc (snd (to (θ E (Right_Functor x))))). rewrite (snd (iso_to_from (θ E (Right_Functor x)))). rewrite id_left. rewrite fmap_comp. comp_right. symmetry. apply (`2 (fmap[ψ E] ff)). 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