# 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 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 = -- <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 ]`.