GetTypes.agda

   1 module GetTypes where
   2
   3 open import Data.Nat using (ℕ)
   4 open import Data.List using (List ; map)
   5 open import Data.Vec using (Vec) renaming (map to mapV)
   6 open import Function using (_∘_)
   7 open import Relation.Binary.PropositionalEquality using (_≗_)
   8
   9 module ListList where
  10   record Get : Set₁ where
  11     field
  12       get : {A : Set} → List A → List A
  13       free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
  14
  15 module VecVec where
  16   record Get : Set₁ where
  17     field
  18       getlen : ℕ → ℕ
  19       get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
  20       free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get