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 = -- <LSG>
  solution 
  where
  solution : ∀ n → (f : Fin n → Fin n) → Injective _≡_ _≡_ f → StrictlySurjective _≡_ f
  solution zero f f-inj = λ ()
  solution (suc n) f f-inj y with (f zero Fin.≟ y)
  ... | yes f[0]≡y = zero , f[0]≡y
  ... | no f[0]≢y =
      let
        f[0]≢f[1+_] : ∀ (k : Fin n) → f zero ≢ f (suc k)
        f[0]≢f[1+_] n = Fin.0≢1+n ∘ f-inj 
        g : Fin n → Fin n
        g k = punchOut f[0]≢f[1+ k ]
        g-injective : Injective _≡_ _≡_ g
        g-injective {x} {y} = Fin.suc-injective
                              ∘ f-inj
                              ∘ Fin.punchOut-injective {n} f[0]≢f[1+ x ] f[0]≢f[1+ y ]
        y' = Fin.punchOut f[0]≢y
        x , g[x]≡y' = solution n g g-injective y'
      in
      suc x , Fin.punchOut-injective f[0]≢f[1+ x ] f[0]≢y g[x]≡y'
  -- </LSG>

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] = -- <LSG>
    case <-cmp m n of λ
      { (tri< m<n ¬b ¬c) → ⊥-elim (f-inj-< m n (<⇒<′ m<n) f[m]≡f[n])
      ; (tri≈ ¬a m≡n ¬c) → m≡n
      ; (tri> ¬a ¬b n<m) → ⊥-elim (f-inj-< n m (<⇒<′ n<m) (sym f[m]≡f[n]))
      }
    -- </LSG>

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 = -- <LSG>
    solution
    where
      solution : (∀ (xs : List A) → ∃[ x ] x ∉ xs) → Infinite A
      solution fresh-for = record
        { f = f
        ; f-injective = Injective-<.toInjective f m<n⇒f[m]≢f[n]
        }
        where
          interleaved mutual
            f[0…<_] : ℕ → List A
            f : ℕ → A

            f[0…< zero ] = []
            f[0…< suc n ] = f n ∷ f[0…< n ]

            f k = proj₁ (fresh-for (f[0…< k ]))

          f-fresh : ∀ k → f k ∉ f[0…< k ]
          f-fresh k = proj₂ (fresh-for (f[0…< k ]))

          f-m<n : ∀ {m} {n} → m <′ n → f m ∈ f[0…< n ]
          f-m<n (≤′-reflexive refl) = here refl
          f-m<n (≤′-step m<n) = there (f-m<n m<n)

          m<n⇒f[m]≢f[n] : ∀ m n → m <′ n → f m ≢ f n
          m<n⇒f[m]≢f[n] m n m<n f[m]≡f[n] = f-fresh n
            (subst (_∈ f[0…< n ]) f[m]≡f[n] (f-m<n m<n))

      -- alternative solution without mutual recursion
      solution-w/o-mutual : (∀ (xs : List A) → ∃[ x ] x ∉ xs) → Infinite A
      solution-w/o-mutual fresh-for = record { f = h ; f-injective = h-inj }
        where
          g : {k : ℕ} → Fin k → A
          g {zero} ()
          g {suc k} zero = proj₁ (fresh-for (tabulate (g {k})))
          g {suc k} (suc x) = g x

          h : ℕ → A
          h k = g {suc k} zero

          h-m<n : ∀ {m n : ℕ} → m <′ n → h m ∈ tabulate (g {n})
          h-m<n (≤′-reflexive refl) = here refl
          h-m<n (≤′-step m<n) = there (h-m<n m<n)

          h-inj : Injective _≡_ _≡_ h
          h-inj = Injective-<.toInjective h λ m n m<n h[m]≡h[n] →
            proj₂ (fresh-for (tabulate (g {n})))
            (subst (_∈ tabulate (g {n})) h[m]≡h[n] (h-m<n m<n))
    -- </LSG>

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 = -- <LSG>
    record
    { Carrier = X.Carrier
    ; _≈_ = λ x x' → f.to x Y.≈ f.to x'
    ; ≈-isEquivalence = record { refl = Y.refl ; sym = Y.sym ; trans = Y.trans }
    }
    where
      module f = Func f
      module X = Setoid X
      module Y = Setoid Y
      -- </LSG>

  quot[_] : ∀ {X Y : Setoid} → (f : Func X Y) → Func X (X /ker[ f ])
  quot[_] f = -- <LSG>
    record
    { to = λ x → x
    ; cong = λ x≈x' → f.cong x≈x'
    }
    where module f = Func f
    -- </LSG>

  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 = -- <LSG>
    record
    { ϕ = record
      { to = λ x → (f.to x) , (x , refl)
      ; cong = λ f[x]≡f[x'] → f[x]≡f[x']
      }
    ; ψ = record
      { to = λ { (y , x , f[x]≡y) → x }
      ; cong = λ { {y , x , eq1} {y' , x' , eq2} f[x]≈f[x'] → Y.trans (Y.trans ( Y.reflexive eq1) f[x]≈f[x']) (Y.sym (Y.reflexive eq2))  } -- f[x]≈f[x']
      }
    ; id-on-X = λ { x → refl }
    ; id-on-Y = λ { (_ , x , refl) → refl }
    }
    where
      module f = Func f
      module X = Setoid X
      module Y = Setoid Y
    -- </LSG>

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