---
layout: default
title : "Examples.Demos.ContraX module"
date : "2022-04-27"
author: "the agda-algebras development team"
---

### 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.

<!--
```agda
{-# 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 `⊥`.

```agda
_↠_ : 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
```