proposition: Theorem ψ_φ_equiv : ∀ x, snd (from (κ E x)) ∘ snd (from (θ E (φ E x))) ∘ `2 (ψ E (φ E x)) ∘ fmap[F] (fst (to (θ E (φ E x)))) ∘ fmap[F] (fst (to (κ E x))) ≈ `2 x.
proof: Proof. intros [[a b] f]; simpl in f |- *. rewrite (snd_comp _ _ _ (κ E ((a, b); f))⁻¹ (θ E (φ E _))⁻¹). rewrite <- !comp_assoc. rewrite <- fmap_comp. rewrite (fst_comp _ _ _ (θ E (φ E _)) (κ E ((a, b); f))). rewrite <- η_θ_κ. rewrite (`2 (η E ((a, b); f))). rewrite η_θ_κ. rewrite comp_assoc. rewrite (snd_comp _ _ _ ((κ E _)⁻¹ ∘ (θ E (φ E _))⁻¹) (θ E (φ E _) ∘ κ E ((a, b); f))). rewrite <- comp_assoc. rewrite (comp_assoc (θ E (φ E ((a, b); f)))⁻¹ _). rewrite iso_from_to, id_left. now rewrite iso_from_to; 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