# Blatt 06

Besprechung am 02.07.2026.
```
{-# OPTIONS --allow-unsolved-metas #-}

open import Level as L using (Level)

open import Data.Nat
open import Data.Product
open import Data.Fin as Fin hiding (_<_)
open import Data.Fin.Properties as Fin using (_≟_)
open import Data.List
open import Data.Sum
open import Data.Empty
open import Function.Definitions using (Injective; StrictlySurjective)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Definitions
open import Relation.Nullary using (¬_; yes; no; contraposition)
open import Data.List.Membership.Propositional
open import Function.Base

module _ where

private
  variable
    ℓ ℓ' ℓ'' : Level

```
## Finite Injections are Surjective
Zeigen Sie, dass eine injektive Funktion auf einer endlichen Menge zwingend surjektiv ist. 
Tipp: Nutzen Sie die Hilfsfunktion `Fin.punchOut` (und dessen Eigenschaften aus `Data.Fin.Properties`).
```
fininj-surjective : ∀ n → (f : Fin n → Fin n) → Injective _≡_ _≡_ f → StrictlySurjective _≡_ f
fininj-surjective = {! !}
```

## Infinite
Wir definieren Unendlichkeit mittels Injektivität:
```
record _↣_ (B : Set ℓ) (C : Set ℓ') : Set (ℓ L.⊔ ℓ') where
  field
    f : B → C
    f-injective : Injective _≡_ _≡_ f

Infinite : Set ℓ → Set ℓ
Infinite X = ℕ ↣ X
```
Um zu zeigen, dass Abbildungen aus den natürlichen Zahlen heraus injektiv sind,
nutzen wir dieses Hilfslemma
```
module Injective-< {B : Set ℓ} (f : ℕ → B) where
  open import Data.Nat.Properties using (<-cmp; <⇒<′)
  toInjective : (∀ m n → m <′ n → f m ≢ f n) → Injective _≡_ _≡_ f
  toInjective f-inj-< {m} {n} f[m]≡f[n] = {! !}
```
Zeigen Sie: wenn eine Menge sich nicht endlich auflisten lässt ist, dann lässt
sich ℕ in diese einbetten.
```
module always-something-fresh⇒infinite (A : Set) where
  open import Data.List.Relation.Unary.Any using (Any; here; there)
  open import Data.List.Membership.Propositional

  not-finite⇒infinite : (∀ (xs : List A) → ∃[ x ] x ∉ xs) → Infinite A
  not-finite⇒infinite = {! !}
```
Tipp: Definieren Sie innerhalb eines `interleaved mutual`-Blocks
zwei verschränkt rekursive Funktionen (vgl. `Logic`). Weiter Tipps finden Sie am
Ende dieser Datei.

## Image vs. Quotient
In der Vorlesung definierten wir das Bild einer Abbildung `f : Func X Y` als
Untermenge von `Y`. Definieren Sie alternativ das Quotientensetoid auf `Y`, das
zwei Elemente `x , x' : X` identifiziert wenn `f x ≈ f x'` in `Y`
```
module Image-vs-Quotient where
  open import Relation
  _/ker[_] : ∀ (X : Setoid) {Y : Setoid} → Func X Y → Setoid
  _/ker[_] X {Y} f = {! !}

  quot[_] : ∀ {X Y : Setoid} → (f : Func X Y) → Func X (X /ker[ f ])
  quot[_] f = {! !}

  infix 2 _≅_
  record _≅_ (X Y : Setoid) : Set where
    field
      ϕ : Func X Y
      ψ : Func Y X
    module ϕ = Func ϕ
    module ψ = Func ψ
    field
      id-on-X : ψ.to ∘ ϕ.to ≗ id
      id-on-Y : ϕ.to ∘ ψ.to ≗ id
      -- for a bijection in Setoids, it actually suffices for above
      -- equations to only hold up to _≈_ (in X res. Y). But for the
      -- next isomorphism, even pointwise propositional equality holds:

  Im[f]≅X/ker[f] : ∀ X Y → (f : Func X Y) → X /ker[ f ] ≅ Im[ f ]
  Im[f]≅X/ker[f] X Y f = {! !}
```

## Mehr Tipps zu `Infinite`
Definieren Sie
`f[0…<_] : ℕ → List A`, 
`f : ℕ → A`, und beweisen dann
`∀ {m} {n} → m <′ n → f m ∈ f[0…< n ]`.