Library UniMath.CategoryTheory.Monoidal.Examples.PosetsMonoidal
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.exponentials.
Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure.
Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits.
Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructuresSmashProduct.
Require Import UniMath.CategoryTheory.DisplayedCats.Examples.PointedPosetStrict.
Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Cartesian.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed.
Require Import UniMath.CategoryTheory.Monoidal.Examples.CartesianMonoidal.
Require Import UniMath.CategoryTheory.Monoidal.Examples.SmashProductMonoidal.
Require Import UniMath.CategoryTheory.DisplayedCats.Examples.CategoryOfPosets.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.exponentials.
Require Import UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure.
Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits.
Require Import UniMath.CategoryTheory.DisplayedCats.Structures.StructuresSmashProduct.
Require Import UniMath.CategoryTheory.DisplayedCats.Examples.PointedPosetStrict.
Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors.
Require Import UniMath.CategoryTheory.Monoidal.Categories.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Cartesian.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric.
Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed.
Require Import UniMath.CategoryTheory.Monoidal.Examples.CartesianMonoidal.
Require Import UniMath.CategoryTheory.Monoidal.Examples.SmashProductMonoidal.
Require Import UniMath.CategoryTheory.DisplayedCats.Examples.CategoryOfPosets.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.terminal.
1. The cartesian monoidal category of posets
Definition poset_monoidal_cat
: monoidal_cat.
Show proof.
Proposition is_cartesian_poset_monoidal_cat
: is_cartesian poset_monoidal_cat.
Show proof.
Definition poset_sym_monoidal_cat
: sym_monoidal_cat
:= poset_monoidal_cat ,, symmetric_cartesian_monoidalcat _ _ _.
Definition poset_sym_mon_closed_cat
: sym_mon_closed_cat.
Show proof.
: monoidal_cat.
Show proof.
refine (category_of_posets ,, _).
use cartesian_monoidalcat.
- exact BinProducts_category_of_posets.
- exact Terminal_category_of_posets.
use cartesian_monoidalcat.
- exact BinProducts_category_of_posets.
- exact Terminal_category_of_posets.
Proposition is_cartesian_poset_monoidal_cat
: is_cartesian poset_monoidal_cat.
Show proof.
Definition poset_sym_monoidal_cat
: sym_monoidal_cat
:= poset_monoidal_cat ,, symmetric_cartesian_monoidalcat _ _ _.
Definition poset_sym_mon_closed_cat
: sym_mon_closed_cat.
Show proof.
use sym_mon_closed_cartesian_cat.
- exact category_of_posets.
- exact BinProducts_category_of_posets.
- exact Terminal_category_of_posets.
- exact Exponentials_category_of_posets.
- exact category_of_posets.
- exact BinProducts_category_of_posets.
- exact Terminal_category_of_posets.
- exact Exponentials_category_of_posets.
2. The symmetric monoidal category of pointed posets