The Pst fragment: an L-set whose carrier is a finite chain (IsFiniteChain), so χ is a finite table and normalisation by evaluation is complete. Products of finite chains follow with IsProduct. More...

Concept definition

template<typename S>

concept dedekind::category::IsFiniteLSet = IsLSet<S> && IsFiniteChain<typename S::Domain>

dedekind::category::IsFiniteChain

A carrier that is a finite chain by its representation: totally ordered and either a machine integer ...

Definition topoi.cppm:434

dedekind::category::IsFiniteLSet

The Pst fragment: an L-set whose carrier is a finite chain (IsFiniteChain), so χ is a finite table an...

Definition topoi.cppm:443

dedekind::category::IsLSet

An L-set: a subobject of a carrier with into a named bounded chain (Codomain = L::Ω)....

Definition topoi.cppm:420

Detailed Description

The Pst fragment: an L-set whose carrier is a finite chain (IsFiniteChain), so χ is a finite table and normalisation by evaluation is complete. Products of finite chains follow with IsProduct.

Template Parameters

S	the candidate set type.