Retracts of the type of natural numbers

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-02-14.
Last modified on 2023-06-15.

module elementary-number-theory.retracts-of-natural-numbers where
Imports 
open import elementary-number-theory.equality-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.decidable-maps
open import foundation.retractions
open import foundation.universe-levels

Idea

If i : A → ℕ has a retraction, then i is a decidable map.

is-decidable-map-retraction-ℕ :
  {l1 : Level} {A : UU l1} (i : A → ℕ) → retraction i → is-decidable-map i
is-decidable-map-retraction-ℕ =
  is-decidable-map-retraction has-decidable-equality-ℕ

Recent changes