Skip to content

Instantly share code, notes, and snippets.

@pnlph

pnlph/_≤_Recursion.agda

Created April 7, 2020 13:14
Show Gist options
  • Save pnlph/9279b506ca84c22d0f036eddf25764fa to your computer and use it in GitHub Desktop.
Save pnlph/9279b506ca84c22d0f036eddf25764fa to your computer and use it in GitHub Desktop.
Download ZIP
Raw
_≤_Recursion.agda
_≤_ _≥_ : ℕ → ℕ → 𝓤₀ ̇
0 ≤ y = 𝟙
succ x ≤ 0 = 𝟘
succ x ≤ succ y = x ≤ y
_≤'_ : ℕ → ℕ → 𝓤₀ ̇
_≤'_ = ℕ-iteration (ℕ → 𝓤₀ ̇ ) (λ y → 𝟙) (λ f → ℕ-recursion (𝓤₀ ̇ ) 𝟘 (λ y P → f y))
x ≥ y = y ≤ x
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment