StringLab.Data.Dec

1Lab
  • Misc. results about decidability🔗
This page was written by Reed Mullanix

back to index 
open import 1Lab.Prelude
open import Meta.Invariant

module StringLab.Data.Dec where

private variable
  â„“ : Level
  A B : Type â„“

open import Data.Dec public

Misc. results about decidability🔗

Decidability is stable under equivalence.

Equiv→Dec : B ≃ A → Dec A → Dec B
Equiv→Dec f d? = invmap (Equiv.from f) (Equiv.to f) d?