From: Helmut Grohne Date: Fri, 6 Jun 2014 07:23:00 +0000 (+0200) Subject: drop-suc is cong pred X-Git-Url: https://git.linta.de/?p=~helmut%2Fbidiragda.git;a=commitdiff_plain;h=51dad2ec627203822e1879e3d58ae5331e58d414;hp=91db824bfa4d66f29066a381e88e6e3125e15576 drop-suc is cong pred --- diff --git a/Examples.agda b/Examples.agda index eca3c90..bda3ae1 100644 --- a/Examples.agda +++ b/Examples.agda @@ -1,6 +1,6 @@ module Examples where -open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; ⌈_/2⌉) +open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; ⌈_/2⌉ ; pred) open import Data.Nat.Properties using (cancel-+-left) import Algebra.Structures open Algebra.Structures.IsCommutativeSemiring Data.Nat.Properties.isCommutativeSemiring using (+-isCommutativeMonoid) @@ -34,11 +34,8 @@ double' = assume-get id↪ (≡-to-Π g) f double'' : Get double'' = assume-get id↪ (≡-to-Π _) (λ v → v ++ v) -drop-suc : {n m : ℕ} → suc n ≡ suc m → n ≡ m -drop-suc refl = refl - suc-injection : EqSetoid ℕ ↪ EqSetoid ℕ -suc-injection = record { to = ≡-to-Π suc; injective = drop-suc } +suc-injection = record { to = ≡-to-Π suc; injective = cong pred } tail' : Get tail' = assume-get suc-injection (≡-to-Π id) tail