📥 Download raw
{-# 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
canary : A  X
canary = {!!}
fix : ∃[ a ] canary  f a  ∃[ x ] g x  x
fix = {!!}
fix₀ : ((h : A  X)  ∃[ a ] h  f a)  ∃[ x ] g x  x
fix₀ = {!!}