Lemma nat_z_iso_preserve_ωlimits {A B : category} (F G : functor A B) : is_omega_cont F -> nat_z_iso F G -> is_omega_cont G. Proof. intros Fc i. intros coch a a_con a_lim. intros b b_con. set (b'_con := nat_trans_preserve_cone (nat_z_iso_inv i) b_con). set (t := Fc coch a a_con a_lim b b'_con). use tpair. - exists (pr11 t · pr1 i a). intro v. etrans. 1: apply assoc'. etrans. 1: apply maponpaths, pathsinv0, (pr21 i). etrans. 1: apply assoc. etrans. 1: apply maponpaths_2, (pr21 t v). etrans. 1: apply assoc'. etrans. 1: apply maponpaths, (pr2 i (dob coch v)). apply id_right. - intro f. use total2_paths_f. + use (cancel_z_iso _ _ (_ ,, pr2 (nat_z_iso_inv i) a)). etrans. 2: apply assoc. etrans. 2: apply maponpaths, pathsinv0, (pr2 (pr2 i a)). etrans. 2: apply pathsinv0, id_right. transparent assert (c' : (∑ x : B ⟦ b, F a ⟧, Limits.is_cone_mor b'_con (Limits.mapcone F coch a_con) x)). { exists (pr1 f · pr1 (pr2 i a)). intro v. cbn. etrans. 1: apply assoc'. etrans. 1: apply maponpaths, pathsinv0, (pr21 (nat_z_iso_inv i)). etrans. 1: apply assoc. apply maponpaths_2, (pr2 f v). } exact (base_paths _ _ (pr2 t c')). + apply (impred_isaprop) ; intro ; apply homset_property. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Chains.All.