Lemma ϕ_for_cia_has_equivalent_characteristic_formula (x : C) (e : x --> CP (F x) (alg_carrier _ Xinv)) (h : C ⟦ x, alg_carrier F Xinv ⟧) : primitive_corecursion_characteristic_formula CP (ϕ_for_cia x e) h ≃ cia_characteristic_formula Xinv e h. Proof. apply weqimplimpl. - intro H. red in H; red. apply pathsinv0 in H. apply (z_iso_inv_on_left _ _ _ _ (finalcoalgebra_z_iso _ _ _ isTerminalX)) in H. etrans; [ exact H |]. clear H. unfold ϕ_for_cia. repeat rewrite assoc'. apply maponpaths. cbn. rewrite postcompWithBinCoproductArrow. rewrite precompWithBinCoproductArrow. rewrite id_left. apply maponpaths_12. + rewrite assoc. rewrite <- functor_comp. rewrite BinCoproductIn1Commutes. apply idpath. + etrans. { rewrite assoc. apply cancel_postcomposition. rewrite assoc'. apply maponpaths. rewrite <- functor_comp. rewrite BinCoproductIn2Commutes. apply functor_id. } rewrite id_right. apply αα'_idA. - intro H. red in H; red. etrans. { apply cancel_postcomposition. exact H. } clear H. unfold ϕ_for_cia. repeat rewrite assoc'. apply maponpaths. cbn. do 2 rewrite postcompWithBinCoproductArrow. rewrite precompWithBinCoproductArrow. do 2 rewrite id_left. apply maponpaths_12. + rewrite <- functor_comp. rewrite BinCoproductIn1Commutes. etrans. { apply maponpaths. apply α'α_idFA. } apply id_right. + rewrite assoc'. rewrite <- functor_comp. rewrite BinCoproductIn2Commutes. rewrite functor_id. apply pathsinv0, id_right. - apply C. - apply isaprop_cia_characteristic_formula. Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.FunctorCoalgebras.