FreeTheorems.agda

   1 module FreeTheorems 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   get-type : Set₁
  11   get-type = {A : Set} → List A → List A
  12
  13   postulate
  14     free-theorem : (get : get-type) → {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get
  15
  16 module VecVec where
  17   get-type : (ℕ → ℕ) → Set₁
  18   get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n)
  19
  20   postulate
  21     free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get