ITP Exercise Sheet 03
Discussion: originally scheduled for 7 May 2026; moved to 11 May 2026
{-# OPTIONS --allow-unsolved-metas #-} open import Level using (Level) open import Data.Nat open import Data.List open import Data.Product open import Data.Bool hiding (_≤_; _<_) open import Relation.Nullary.Decidable using (Dec; map′; yes; no) open import Function.Base using (_∘_) import Level as L open import Relation.Binary.PropositionalEquality open import Relation.Nullary.Negation open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Relation.Unary.Any using (Any; here; there) module _ where private variable a b c : Level A : Set a B : Set b C : Set c
n-ary Operation
Define a type of n-ary operations on a type X:
_-ary-on_ : ℕ → {ℓ : Level} → (X : Set ℓ) → Set ℓ _-ary-on_ = {! !} -- _ : 2 -ary-on ℕ -- _ = _+_ -- addition is binary on ℕ -- _ : 1 -ary-on Set -- _ = ¬_ -- negation is a unary operation on sets -- _ : 0 -ary-on Bool -- _ = true
Injectivity
module injectivity where _injective : (f : A → B) → Set _ _injective f = {! !} ∘-injective : {f : A → B} {g : B → C} → f injective → g injective → (g ∘ f) injective ∘-injective {f = f} = {! !} ∘-cancelˡ-injective : {f : A → B} {g : B → C} → (g ∘ f) injective → f injective ∘-cancelˡ-injective {g = g} = {! !} no-∘-cancelʳ-injective : Σ[ A ∈ Set ] Σ[ B ∈ Set ] Σ[ C ∈ Set ] Σ[ f ∈ (A → B) ] Σ[ g ∈ (B → C) ] ((g ∘ f) injective × ¬ g injective) no-∘-cancelʳ-injective = _ , _ , _ , {! !}
Surjectivity
Define and prove the corresponding properties for surjectivity
module surjectivity where
Index-based access
Define a (total) function that returns the k-th element of a list.
_at[_] : (l : List A) → (k : ℕ) → k < length l → A _at[_] = {! !}
Deciding membership
Decide whether a given element occurs in a list.
(Hint: when case-splitting on something of type Dec x, it is advisable to
enter the cases yes and no manually.)
module decide-∈ (A : Set a) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where _∈?_ : (x : A) (l : List A) → Dec (x ∈ l) _∈?_ = {! !}