proposition: Lemma lawvere_to_functorial {a b} (f : F a ~{C}~> b) {a' b'} (i : a' ~> a) (j : b ~> b') : φ' E (j ∘ f ∘ fmap[F] i) ≈ fmap[G] j ∘ φ' E f ∘ i.
proof: Proof. given (Fi : ((a', b'); j ∘ f ∘ fmap[F] i) ~{ F ↓ Id[C] }~> ((a, b'); j ∘ f)). { now refine ((i, id); _); abstract cat. } spose (`2 (to (lawvere_iso_to (j ∘ f)) ∘ fmap[φ E] Fi ∘ from (lawvere_iso_to (j ∘ f ∘ fmap[F] i)))) as H. spose (`2 (projF E) ((a', b'); j ∘ f ∘ fmap[F] i) ((a, b'); j ∘ f) Fi) as H1. destruct H1 as [H1 H2]. rewrite <- H1 in H; clear H1. rewrite <- H2 in H; clear H2. rewrite fmap_id, id_left in H. rewrite <- H. clear Fi H. given (Fi : ((a', F a); fmap[F] i) ~{ F ↓ Id[C] }~> ((a, b'); j ∘ f)). { now refine ((i, j ∘ f); _); abstract cat. } spose (`2 (to (lawvere_iso_to (j ∘ f)) ∘ fmap[φ E] Fi ∘ from (lawvere_iso_to (fmap[F] i)))) as H. spose (`2 (projF E) ((a', F a); fmap[F] i) ((a, b'); j ∘ f) Fi) as H1. destruct H1 as [H1 H2]. rewrite <- H1 in H; clear H1. rewrite <- H2 in H; clear H2. rewrite H. clear Fi H. rewrite fmap_comp. given (Fi : ((a', F a); fmap[F] i) ~{ F ↓ Id[C] }~> ((a, b); f)). { now refine ((i, f); _); abstract cat. } spose (`2 (to (lawvere_iso_to f) ∘ fmap[φ E] Fi ∘ from (lawvere_iso_to (fmap[F] i)))) as H. spose (`2 (projF E) ((a', F a); fmap[F] i) ((a, b); f) Fi) as H1. destruct H1 as [H1 H2]. rewrite <- H1 in H; clear H1. rewrite <- H2 in H; clear H2. rewrite <- comp_assoc. rewrite <- H. now cat. 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