proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.FunctorCoalgebras