diff options
Diffstat (limited to 'LiftGet.agda')
| -rw-r--r-- | LiftGet.agda | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/LiftGet.agda b/LiftGet.agda index c4f1acd..b6d99de 100644 --- a/LiftGet.agda +++ b/LiftGet.agda @@ -11,9 +11,9 @@ open import Relation.Binary.Core using (_≡_) open import Relation.Binary.PropositionalEquality using (_≗_ ; sym ; cong ; refl ; subst ; trans ; proof-irrelevance) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) -import BFF -open BFF.ListBFF using (get-type) -open BFF.VecBFF using () renaming (get-type to getV-type) +import FreeTheorems +open FreeTheorems.ListList using (get-type ; free-theorem) +open FreeTheorems.VecVec using () renaming (get-type to getV-type) getVec-to-getList : {getlen : ℕ → ℕ} → (getV-type getlen) → get-type getVec-to-getList get = toList ∘ get ∘ fromList @@ -21,9 +21,6 @@ getVec-to-getList get = toList ∘ get ∘ fromList getList-to-getlen : get-type → ℕ → ℕ getList-to-getlen get = length ∘ get ∘ flip replicate tt -postulate - free-theorem-list-list : {β γ : Set} → (get : get-type) → (f : β → γ) → get ∘ map f ≗ map f ∘ get - replicate-length : {A : Set} → (l : List A) → map (const tt) l ≡ replicate (length l) tt replicate-length [] = refl replicate-length (_ ∷ l) = cong (_∷_ tt) (replicate-length l) @@ -33,7 +30,7 @@ getList-length get l = begin length (get l) ≡⟨ sym (length-map (const tt) (get l)) ⟩ length (map (const tt) (get l)) - ≡⟨ cong length (sym (free-theorem-list-list get (const tt) l)) ⟩ + ≡⟨ cong length (sym (free-theorem get (const tt) l)) ⟩ length (get (map (const tt) l)) ≡⟨ cong (length ∘ get) (replicate-length l) ⟩ length (get (replicate (length l) tt)) ∎ |