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