ITP Blatt 03

Besprechung: ursprünglich für den 07.05.2026 angesetzt; verschoben auf 11.05.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

Definieren Sie einen Typ einer n-ären Operation auf einem Typen 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

Injektivität

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 = _ , _ , _ , {! !}

Surjektivität

Definieren und Beweisen Sie die entsprechenden Eigenschaften für Surjektivität

module surjectivity where

Index-basierter Zugriff

Definieren Sie eine (totale) Funktion, die das k-te Element einer Liste zurückgibt.

_at[_] : (l : List A) → (k : ℕ) → k < length l → A
_at[_] = {! !}

Elementbeziehung Entscheiden

Entscheiden Sie, ob ein gegebenes Element in einer Liste vorkommt. (Tipp: bei Fallunterscheidung über etwas vom Typ Dec x ist es ratsam, die Fälle yes und no manuell einzutragen)

module decide-∈ (A : Set a) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
    _∈?_ : (x : A) (l : List A) → Dec (x ∈ l)
    _∈?_ = {! !}

Agda Quellcode herunterladen