diff options
Diffstat (limited to 'FreeTheorems.agda')
| -rw-r--r-- | FreeTheorems.agda | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/FreeTheorems.agda b/FreeTheorems.agda index f37cada..d2ba3ef 100644 --- a/FreeTheorems.agda +++ b/FreeTheorems.agda @@ -10,12 +10,29 @@ module ListList where get-type : Set₁ get-type = {A : Set} → List A → List A + record Get : Set₁ where + field + get : {A : Set} → List A → List A + free-theorem : {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get + postulate free-theorem : (get : get-type) → {α β : Set} → (f : α → β) → get ∘ map f ≗ map f ∘ get + assume-get : get-type → Get + assume-get get = record { get = get; free-theorem = free-theorem get } + module VecVec where get-type : (ℕ → ℕ) → Set₁ get-type getlen = {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n) + record Get : Set₁ where + field + getlen : ℕ → ℕ + get : {A : Set} {n : ℕ} → Vec A n → Vec A (getlen n) + free-theorem : {α β : Set} (f : α → β) {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get + postulate free-theorem : {getlen : ℕ → ℕ} → (get : get-type getlen) → {α β : Set} → (f : α → β) → {n : ℕ} → get {_} {n} ∘ mapV f ≗ mapV f ∘ get + + assume-get : {getlen : ℕ → ℕ} → (get : get-type getlen) → Get + assume-get {getlen} get = record { getlen = getlen; get = get; free-theorem = free-theorem get } |