{-# OPTIONS --cubical-compatible #-}
module Padova2025.Explorations.Uncountability.Lawvere
  {A X : Set} (f : A → (A → X)) (g : X → X) where

Lawvere’s fixed point theorem#

open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProvingBasics.Connectives.Existential

Exercise 1canary

canary : A → X
canary = {!!}

Your solution

Reference solution

canary : A → X
canary a = g (f a a)

Exercise 2fix

fix : ∃[ a ] canary ≗ f a → ∃[ x ] g x ≡ x
fix = {!!}

The reference solution uses: _,_

Your solution

Reference solution

fix : ∃[ a ] canary ≗ f a → ∃[ x ] g x ≡ x
fix (a , p) = f a a , p a

Exercise 3fix₀

fix₀ : ((h : A → X) → ∃[ a ] h ≗ f a) → ∃[ x ] g x ≡ x
fix₀ = {!!}

The reference solution uses: fix canary

Your solution

Reference solution

fix₀ : ((h : A → X) → ∃[ a ] h ≗ f a) → ∃[ x ] g x ≡ x
fix₀ split-surjectivity = fix (split-surjectivity canary)