# Contents

## Definition

Given a type $T$, the partial function classifier $T_\bot$ is inductively generated by

• a function $inj:T \to T_\bot$
• a term $\bot:T_\bot$
• a function $\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to T) \to T$

and the partial order type family $\leq$ is simultaneously inductively generated by

• a family of dependent terms

$a:T, b:T \vdash \pi(a,b):isProp(a \leq b)$

representing that each type $a \leq b$ is a proposition.

• a family of dependent terms

$a:T \vdash \rho(a):a \leq a$

representing the reflexive property of $\leq$.

• a family of dependent terms

$a:T, b:T, c:T \vdash \tau(a, b, c):(a \leq b) \times (b \leq c) \to (a \leq c)$

representing the transitive property of $\leq$.

• a family of dependent terms

$a:T, b:T \vdash \sigma(a, b):(a \leq b) \times (b \leq a) \to (a = b)$

representing the anti-symmetric property of $\leq$.

• a family of dependent terms

$a:P \vdash t(a):\bot \leq a$

representing that $\bot$ is initial in the poset.

• a family of dependent terms

$n:\mathbb{N}, s:\mathbb{N} \to T \vdash i(n, s):s(n) \leq \Vee_{n:\mathbb{N}} s(n)$
• a family of dependent terms

$x:\Sigma, s:\mathbb{N} \to \Sigma \vdash i(s, x):\left(\prod_{n:\mathbb{N}}(s(n) \leq x)\right) \to \left(\Vee_{n:\mathbb{N}} s(n) \leq x\right)$

representing that denumerable/countable joins exist in the poset.