Skip to content

Instantly share code, notes, and snippets.

@pnlph

pnlph/HoTT-UF-Natural

Created April 7, 2020 11:09
Show Gist options
  • Save pnlph/bb867bde410aec1441db43de61b0d528 to your computer and use it in GitHub Desktop.
Save pnlph/bb867bde410aec1441db43de61b0d528 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
HoTT-UF-Natural
β„•-induction : (A : β„• β†’ 𝓀 Μ‡ ) β†’ A 0 β†’ ((n : β„•) β†’ A n β†’ A (succ n)) β†’ (n : β„•) β†’ A n
β„•-induction A aβ‚€ f = h where h : (n : β„•) β†’ A n
h 0 = aβ‚€
h (succ n) = f n (h n)
β„•-recursion : (X : 𝓀 Μ‡ ) β†’ X β†’ (β„• β†’ X β†’ X) β†’ β„• β†’ X
β„•-recursion X = β„•-induction (Ξ» _ β†’ X)
β„•-iteration : (X : 𝓀 Μ‡ ) β†’ X β†’ (X β†’ X) β†’ β„• β†’ X
β„•-iteration X x f = β„•-recursion X x (Ξ» _ x β†’ f x)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment