Exercise Sheet 08

Discussion: 16 July 2026.

{-# OPTIONS --allow-unsolved-metas --guardedness #-}

open import Level using (0ℓ)
open import Axiom.ExcludedMiddle using (ExcludedMiddle)
open import Data.Unit using (tt)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product
open import Data.Sum using (inj₁; inj₂)
open import Data.Maybe using (Maybe; just; nothing; Is-just; to-witness; _<∣>_)
open import Data.Maybe.Relation.Unary.Any using (just)
open import Relation.Binary using (_⇔_)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (yes; no)
open import Function.Base

module _ where

open import Partial

private
  variable
    A B X Y : Set

From spans to Maybe

We have already shown:

import Partial using (from-Maybe)

Prove the converse direction under the assumption of the law of excluded middle:

module Span→Maybe (lem : ExcludedMiddle 0ℓ) where
  ⊇⟶⇒⇀ : (A ⊇⟶ B) → (A ⇀ B)
  ⊇⟶⇒⇀ f a = {!!}

  module properties (f : A ⊇⟶ B) where
    open import Relation.Unary using (_⊆_)
    open _⊇⟶_ f
    g : A ⇀ B
    g = ⊇⟶⇒⇀ f
    dom-⊆ : Is-defined ⊆ (Is-just ∘ g)
    dom-⊆ = {!!}

    dom-⊇ : (Is-just ∘ g) ⊆ Is-defined
    dom-⊇ = {!!}

    same-value : ∀ a → (a↓ : Is-defined a)
               → g a ≡ just (app (a , a↓))
    same-value = {!!}

Step indexing is wlog

Given an arbitrary map f, turn it into a monotone one:

module Stabilize {A : Set} (f : ℕ → Maybe A) where
  stabilized : ℕ → Maybe A
  stabilized = {!!}

  stabilized-is-mono : is-mono stabilized
  stabilized-is-mono = {!!}

  stabilized-complete : ∀ n → Is-just (f n) → Is-just (stabilized n)
  stabilized-complete = {!!}

  stabilized-sound : ∀ n → Is-just (stabilized n) → ∃[ k ] f k ≡ stabilized n
  stabilized-sound = {!!}

Agda Quellcode herunterladen