Nonempty finite linear orders #
This defines NonemptyFinLinOrd
, the category of nonempty finite linear
orders with monotone maps. This is the index category for simplicial objects.
Note: NonemptyFinLinOrd
is not a subcategory of FinBddDistLat
because its morphisms do not
preserve ⊥
and ⊤
.
A typeclass for nonempty finite linear orders.
- min : α → α → α
- max : α → α → α
- decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
- decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
- Nonempty : _root_.Nonempty α
Instances
The category of nonempty finite linear orders.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Construct a bundled NonemptyFinLinOrd
from the underlying type and typeclass.
Instances For
Equations
- NonemptyFinLinOrd.instInhabited = { default := NonemptyFinLinOrd.of PUnit.{?u.3 + 1} }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Constructs an equivalence between nonempty finite linear orders from an order isomorphism between them.
Equations
- NonemptyFinLinOrd.Iso.mk e = { hom := ↑e, inv := ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
OrderDual
as a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The equivalence between NonemptyFinLinOrd
and itself induced by OrderDual
both ways.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- NonemptyFinLinOrd.instFunLikeHomαNonemptyFiniteLinearOrder = { coe := fun (f : A ⟶ B) => ⇑(let_fun this := f; this), coe_injective' := ⋯ }
The forgetful functor NonemptyFinLinOrd ⥤ FinPartOrd
and OrderDual
commute.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The generating arrow i ⟶ i+1
in the category Fin n
.