# 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)
    _∈?_ = {! !}
```