From 934f2003d4f47c2af3a91cd827d75caeded7ec7a Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 30 Jan 2014 14:01:10 +0100 Subject: express VecBFF via PartialVecBFF --- FreeTheorems.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'FreeTheorems.agda') 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 -- cgit v1.2.3