Definition Equalizers_category_of_posets : Equalizers category_of_posets. Proof. intros X Y f g. simple refine ((_ ,, _) ,, (_ ,, _)). - exact (_ ,, Equalizer_order (pr2 X) (pr1 Y) (pr1 f) (pr1 g)). - exact (_ ,, Equalizer_pr1_monotone (pr2 X) (pr1 Y) (pr1 f) (pr1 g)). - abstract (use eq_monotone_function ; intro w ; cbn in w ; cbn ; exact (pr2 w)). - simpl. intros W h p. use iscontraprop1. + abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply homset_property | ] ; use eq_monotone_function ; intro w ; use subtypePath ; [ intro ; apply (pr1 Y) | ] ; refine (eqtohomot (maponpaths pr1 (pr2 φ₁)) w @ !_) ; exact (eqtohomot (maponpaths pr1 (pr2 φ₂)) w)). + simple refine (_ ,, _). * exact (_ ,, Equalizer_map_monotone _ _ _ _ _ (pr2 h) (eqtohomot (maponpaths pr1 p))). * abstract (use eq_monotone_function ; intro w ; apply idpath). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.DisplayedCats.Binproducts. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Categories.HSET.All.