Definition Exponentials_category_of_posets : Exponentials BinProducts_category_of_posets. Proof. intros X. use left_adjoint_from_partial. - exact (λ Y, _ ,, monotone_function_PartialOrder (pr2 X) (pr2 Y)). - exact (λ Y, eval_monotone_function (pr2 X) (pr2 Y)). - refine (λ Y Z f, _). use iscontraprop1. + abstract (use invproofirrelevance ; intros g₁ g₂ ; use subtypePath ; [ intro ; apply homset_property | ] ; use eq_monotone_function ; intro z ; use eq_monotone_function ; intro x ; refine (!(eqtohomot (maponpaths pr1 (pr2 g₁)) (x ,, z)) @ _) ; exact (eqtohomot (maponpaths pr1 (pr2 g₂)) (x ,, z))). + simple refine (_ ,, _). * exact (lam_monotone_function (pr2 X) (pr2 Y) f). * abstract (use subtypePath ; [ intro ; apply isaprop_is_monotone | ] ; 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.