#Contents# * table of contents {:toc} ## 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. ## See also ## * [[partial function]] * [[omega-complete poset]] * [[Sierpinski space]] ## References ## * Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type ([abs:1610.09254](https://arxiv.org/abs/1610.09254)) * Martin Escardó, Cory Knapp, Partial Elements and Recursion via Dominances in Univalent Type Theory ([pdf](https://drops.dagstuhl.de/opus/volltexte/2017/7682/))