diff options
Diffstat (limited to 'FreeTheorems.agda')
| -rw-r--r-- | FreeTheorems.agda | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/FreeTheorems.agda b/FreeTheorems.agda index aacb95a..c22a68d 100644 --- a/FreeTheorems.agda +++ b/FreeTheorems.agda @@ -11,6 +11,8 @@ open import Relation.Binary.PropositionalEquality using (_≗_ ; cong) renaming open import Relation.Binary using (Setoid) open Injection using (to) +open import Generic using (≡-to-Π) + module ListList where get-type : Set₁ get-type = {A : Set} → List A → List A @@ -37,8 +39,5 @@ module PartialVecVec where open VecVec using () renaming (free-theorem-type to VecVec-free-theorem-type) - ≡-to-Π : {A B : Set} → (A → B) → EqSetoid A ⟶ EqSetoid B - ≡-to-Π f = record { _⟨$⟩_ = f; cong = cong f } - VecVec-free-theorem : VecVec-free-theorem-type VecVec-free-theorem {getlen} get = free-theorem Function.Injection.id (≡-to-Π getlen) get |