Exercise Sheet 06

Discussion: 2 July 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

Show that an injective function on a finite set is necessarily surjective. Hint: use the auxiliary function Fin.punchOut (and its properties from Data.Fin.Properties).

fininj-surjective : ∀ n → (f : Fin n → Fin n) → Injective _≡_ _≡_ f → StrictlySurjective _≡_ f
fininj-surjective = {! !}

Infinite

We define infinity by means of injectivity:

record _↣_ (B : Set ℓ) (C : Set ℓ') : Set (ℓ L.⊔ ℓ') where
  field
    f : B → C
    f-injective : Injective _≡_ _≡_ f

Infinite : Set ℓ → Set ℓ
Infinite X = ℕ ↣ X

To show that maps out of the natural numbers are injective, we use this auxiliary lemma

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

Show: if a set cannot be listed finitely, then ℕ can be embedded into it.

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

Hint: inside an interleaved mutual block, define two mutually recursive functions (cf. Logic). Further hints can be found at the end of this file.

Image vs. Quotient

In the lecture we defined the image of a map f : Func X Y as a subset of Y. As an alternative, define the quotient setoid on Y that identifies two elements x , x' : X whenever 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 = {! !}

More hints on Infinite

Define f[0…<_] : ℕ → List A, f : ℕ → A, and then prove ∀ {m} {n} → m <′ n → f m ∈ f[0…< n ]. Agda Quellcode herunterladen