proposition: Lemma opp_rlp_is_llp_opp {C : category} (L : morphism_class C) : morphism_class_opp (rlp L) = (llp (morphism_class_opp L)).
proof: Proof. apply morphism_class_subset_antisymm; intros x y f. - intro rlpf. intros a b g hg. intros top bottom H. use (rlpf _ _ (rm_opp_mor g)). * exact hg. * exact (rm_opp_mor bottom). * exact (rm_opp_mor top). * symmetry. exact H. * intros hl. destruct hl as [l [hlg hlf]]. apply hinhpr. exists (opp_mor l). split; assumption. - intro rlpf. intros a b g hg. intros top bottom H. use (rlpf _ _ (rm_opp_mor g)). * exact hg. * exact (rm_opp_mor bottom). * exact (rm_opp_mor top). * symmetry. exact H. * intro hl. destruct hl as [l [hlg hlf]]. apply hinhpr. exists (opp_mor l). split; assumption. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Opp UniMath.ModelCategories.Retract UniMath.ModelCategories.MorphismClass UniMath.CategoryTheory.DisplayedCats.Examples.Arrow