[ refactor ] proofs in Relation.Nullary.Decidable and a reexport in Function.Related.TypeIsomorphisms

src/Function/Related/TypeIsomorphisms.agda

@@ -37,16 +37,21 @@ open import Relation.Binary hiding (_⇔_)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
-open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (Dec; ¬_; _because_; ofⁿ; contradiction)
+open import Relation.Nullary.Negation.Core using (¬_)
 import Relation.Nullary.Indexed as I
-open import Relation.Nullary.Decidable using (True)
 
 private
   variable
     a b c d : Level
     A B C D : Set a
 
+------------------------------------------------------------------------
+-- A lemma relating True dec and P, where dec : Dec P
+
+open import Relation.Nullary.Decidable public
+  using ()
+  renaming (True-↔ to True↔)
+
 ------------------------------------------------------------------------
 -- Properties of Σ and _×_
 
@@ -350,16 +355,6 @@ Related-cong {A = A} {B = B} {C = C} {D = D} A≈B C≈D = mk⇔
             C  ∎)
   where open EquationalReasoning
 
-------------------------------------------------------------------------
--- A lemma relating True dec and P, where dec : Dec P
-
-True↔ : ∀ {p} {P : Set p}
-        (dec : Dec P) → ((p₁ p₂ : P) → p₁ ≡ p₂) → True dec ↔ P
-True↔ ( true because  [p]) irr =
-  mk↔ₛ′ (λ _ → invert [p]) (λ _ → _) (irr _) (λ _ → refl)
-True↔ (false because ofⁿ ¬p) _ =
-  mk↔ₛ′ (λ()) (invert (ofⁿ ¬p)) (λ x → flip contradiction ¬p x) (λ ())
-
 ------------------------------------------------------------------------
 -- Relating a predicate to an existentially quantified one with the
 -- restriction that the quantified variable is equal to the given one

src/Relation/Nullary/Decidable.agda

@@ -19,7 +19,7 @@ open import Relation.Nullary.Irrelevant using (Irrelevant)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; sym; trans; cong′)
+  using (_≡_; refl; sym; trans)
 
 private
   variable
@@ -41,18 +41,26 @@ map A⇔B = map′ to from
 -- If there is an injection from one setoid to another, and the
 -- latter's equivalence relation is decidable, then the former's
 -- equivalence relation is also decidable.
-via-injection : {S : Setoid a ℓ₁} {T : Setoid b ℓ₂}
-                (inj : Injection S T) (open Injection inj) →
-                Decidable Eq₂._≈_ → Decidable Eq₁._≈_
-via-injection inj _≟_ x y = map′ injective cong (to x ≟ to y)
-  where open Injection inj
+
+module _ {S : Setoid a ℓ₁} {T : Setoid b ℓ₂} (injection : Injection S T) where
+
+  open Injection injection
+
+  via-injection : Decidable Eq₂._≈_ → Decidable Eq₁._≈_
+  via-injection _≟_ x y = map′ injective cong (to x ≟ to y)
 
 ------------------------------------------------------------------------
 -- A lemma relating True and Dec
 
 True-↔ : (a? : Dec A) → Irrelevant A → True a? ↔ A
-True-↔ (true  because [a]) irr = let a = invert [a] in mk↔ₛ′ (λ _ → a) _ (irr a) cong′
-True-↔ (false because [¬a]) _  = let ¬a = invert [¬a] in mk↔ₛ′ (λ ()) ¬a (λ a → contradiction a ¬a) λ ()
+True-↔ a? irr = mk↔ₛ′ to from to-from (from-to a?)
+  where
+  to = toWitness {a? = a?}
+  from = fromWitness {a? = a?}
+  to-from : ∀ a → to (from a) ≡ a
+  to-from a = irr _ a
+  from-to : ∀ a? (x : True a?) → fromWitness (toWitness x) ≡ x
+  from-to (yes _) _ = refl
 
 ------------------------------------------------------------------------
 -- Result of decidability