Examples.Demos.ContraX

Inconsistency in first formalization attempt

This is the Examples.Demos.ContraX module of the Agda Universal Algebra Library.

A cautionary counterexample kept from an early formalization attempt. It is tempting to posit a surjection from an arbitrary context type onto every algebra's domain; this module shows the global form of that assumption is inconsistent, so any such surjection must be a hypothesis about a suitably chosen context, never a theorem about all of them.

{-# OPTIONS --without-K --exact-split --safe #-}

open import Overture using ( 𝓞 ; 𝓥 ; Signature )

module Examples.Demos.ContraX {𝑆 : Signature 𝓞 𝓥} where
open import  Data.Unit.Polymorphic                  using ( ⊤ ; tt )
open import  Data.Empty.Polymorphic                 using ( ⊥ )
open import  Level                                  using ( 0ℓ )
open import  Relation.Binary                        using ( Setoid )
open import  Relation.Binary.PropositionalEquality  using ( setoid )
open import  Data.Product                           using ( Σ-syntax )
open import  Function    renaming (Func to _⟶_ )    using ()


open import Overture                 using ( proj₁ ; proj₂ )
open import Setoid.Algebras  using ( Algebra ; 𝔻[_] )
open import Setoid.Functions         using (IsSurjective ; Image_∋_)

open Algebra

_↠_ packages a setoid function from setoid X into the algebra's domain together with a proof that it is surjective. myA is the one-point setoid with the trivial equality, and myAlg an algebra on it whose interpretation Agda infers, the codomain being a one-point setoid. contradiction refutes ∀ X 𝑨 → X ↠ 𝑨: instantiating at the empty type and myAlg, the assumed surjection must witness the point in its image, and that witness is an element of ⊥.

_↠_ : Set → Algebra {𝑆 = 𝑆} 0ℓ 0ℓ → _
X ↠ 𝑨 = Σ[ h ∈ (setoid X ⟶ 𝔻[ 𝑨 ])] IsSurjective h

myA : Setoid 0ℓ 0ℓ
myA = record  { Carrier = ⊤
              ; _≈_ = λ x x₁ → ⊤
              ; isEquivalence = record  { refl = tt
                                        ; sym = λ _ → tt
                                        ; trans = λ _ _ → tt } }

myAlg : Algebra {𝑆 = 𝑆} _ _
myAlg = record { Domain = myA ; Interp = _ }

contradiction : (∀ X 𝑨 → X ↠ 𝑨) → ⊥
contradiction h1 = ex falso
 where
 h : Σ[ h ∈ (setoid ⊥ ⟶ 𝔻[ myAlg ])] IsSurjective h
 h = h1 ⊥ myAlg

 falso : Image (proj₁ h) ∋ tt
 falso = (proj₂ h)

 ex : Image (proj₁ h) ∋ tt → ⊥
 ex (Image_∋_.eq a x) = a