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  _≅_
  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 ]. Agda Quellcode herunterladen