Homotopy Type Theory partial function classifier > history (Rev #2)



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

  • a function inj:TT inj:T \to T_\bot
  • a term :T \bot:T_\bot
  • a function n:()(n):(T)T\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π(a,b):isProp(ab)a:T, b:T \vdash \pi(a,b):isProp(a \leq b)

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

  • a family of dependent terms

    a:Tρ(a):aaa:T \vdash \rho(a):a \leq a

    representing the reflexive property of \leq.

  • a family of dependent terms

    a:T,b:T,c:Tτ(a,b,c):(ab)×(bc)(ac)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σ(a,b):(ab)×(ba)(a=b)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:Pt(a):aa:P \vdash t(a):\bot \leq a

    representing that \bot is initial in the poset.

  • a family of dependent terms

    n:,s:Ti(n,s):s(n) n:s(n)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:Σ,s:Σi(s,x):( n:(s(n)x))( n:s(n)x)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


  • Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type (abs:1610.09254)

  • Martin Escardó, Cory Knapp, Partial Elements and Recursion via Dominances in Univalent Type Theory (pdf)

Revision on March 12, 2022 at 19:02:59 by Anonymous?. See the history of this page for a list of all contributions to it.