proposition: Lemma wfs_R_contains_isos {C : category} (w : wfs C) : (morphism_class_isos C) ⊆ (wfs_R w).
proof: Proof. intros x y f hf. set (opp_containment := wfs_L_contains_isos (opp_wfs w)). exact (opp_containment _ _ (opp_mor f) (opp_is_iso _ hf)). Qed.
imports: UniMath.MoreFoundations.All UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.ModelCategories.Retract UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.Lifting