Contents

  1. Double and triple negation
  2. Negation of equality
  3. Equality of Types and Function Types
  4. Decidability
{-# OPTIONS --without-K --safe #-}

module negation where

Double and Triple Negation

First, let us import our skeleton Martin-LΓΆf Type Theory. 
open import mltt
Recall that we defined maps to the empty type to indicate that either a type is empty or that the proposition it represents is false: Β¬ A = A β†’ 𝟘. Iterating, we have the double and triple negation: 
¬¬ : βˆ€ {β„“} (A : Set β„“) β†’ Set β„“
¬¬ A = ¬ (¬ A)
If A has a term, then it is non-empty: namely if a : A then we are able to construct a term of ¬¬ A = (A β†’ 𝟘) β†’ 𝟘 
¬¬-intro : βˆ€ {β„“} {A : Set β„“} β†’ A β†’ (¬¬ A)
¬¬-intro a = Ξ» x β†’ x a
There is no general procedure to implement the converse.1 In general this would amount to be able to choose, for each non-empty type A a term in it: this a form of global choice, ultimately, if assumed as a postulate, incompatible with univalence. Going further, the following is the straightforward contrapositive. 
contra : βˆ€ {β„“ β„“'} {A : Set β„“} {B : Set β„“'} β†’ (A β†’ B) β†’ (Β¬ B β†’ Β¬ A)
contra f = Ξ» y a β†’ y (f a)

Note the proof: if a : A, i.e.Β A has a term, then so does B via f, and hence, by evaluating y : B β†’ 𝟘 at it, we get a contradiction, i.e.Β something in 𝟘.

We can iterate the negation: 
¬¬¬ : βˆ€ {β„“} (A : Set β„“) β†’ Set β„“
¬¬¬ A = ¬ (¬¬ A)
and notice that three negation imply just one: 
three-to-oneΒ¬ : βˆ€ {β„“} {A : Set β„“} β†’ ¬¬¬ A β†’ Β¬ A
three-to-one¬ = contra ( ¬¬-intro )
In fact, an easy application of the ¬¬-intro gives the converse to this statement: 
one-to-threeΒ¬ : βˆ€ {β„“} {A : Set β„“} β†’ Β¬ A β†’ ¬¬¬ A
one-to-threeΒ¬ = Ξ» x β†’ ¬¬-intro x
The type (A β†’ B) Γ— (B β†’ A) corresponds to the logical equivalence of A and B. Formally: 
_⟺_ : βˆ€ {β„“ β„“'} β†’ Set β„“ β†’  Set β„“' β†’ Set (β„“ βŠ” β„“')
A ⟺ B = (A β†’ B) Γ— (B β†’ A)
We can summarize the above by the statement 
three-is-oneΒ¬ : βˆ€ {β„“} (A : Set β„“) β†’ Β¬ A ⟺ ¬¬¬ A 
Σ.fst (three-is-one¬ A) = one-to-three¬ {A = A}
Σ.snd (three-is-one¬ A) = three-to-one¬ {A = A}

top ⇑

Negation of Equality

_β‰’_ : βˆ€ {β„“} {A : Set β„“} β†’ A β†’ A β†’ Set β„“
x β‰’ y = Β¬ (x ≑ y)

Inequality also satisfies a symmetry condition analogous to ≑-inv = . ⁻¹

β‰’-inv : βˆ€ {β„“} {A : Set β„“} {x y : A} β†’ x β‰’ y β†’ y β‰’ x
β‰’-inv u = Ξ» p β†’ u (p ⁻¹)

In the proof, given u : x ≑ y β†’ 𝟘, and given p : y ≑ x, we evaluate u at the inverse of p.

top ⇑

Equality of Types and Function Types

Consider, for two types A B : Set β„“, the identity type A ≑ B (note that A ≑ B : Set (lsuc β„“). This turns into (there is a map to) the type of functions, or implications, A β†’ B. 
Id-to-Fun : βˆ€ {β„“} {A B : Set β„“} β†’ A ≑ B β†’ A β†’ B
Id-to-Fun {β„“} {A} {.A} refl = id

By induction on p : A ≑ B, we prove the statement by assigning to the reflexivity term of A the identity function id : A β†’ A.

We can take a different approach to proving the above statement by employing the transport function defined in MLTT. 
Id-to-Fun' : βˆ€ {β„“} {A B : Set β„“} β†’ A ≑ B β†’ A β†’ B
Id-to-Fun' {β„“} = transport (id {A = Set β„“})
When we introduce the univalence principle, this correspondence will be part of a more interesting, or more complete, one between A ≑ B and the type of weak equivalences between A and B. The two versions agree: 
Id-to-Fun-agree : βˆ€ {β„“} {A B : Set β„“} (p : A ≑ B) β†’ Id-to-Fun p ≑ Id-to-Fun' p
Id-to-Fun-agree refl = idp (id )

Following are some interesting applications: we can prove that πŸ™ β‰’ 𝟘 and that the terms β‚€ : 𝟚 and ₁ : 𝟚 are not equal.

For the fact that πŸ™ β‰’ 𝟘, if p : πŸ™ ≑ 𝟘 is a potential identification, then Id-to-Fun p : πŸ™ β†’ 𝟘, and evaluating that at the sole constructor of πŸ™ derives a contradiction, i.e.Β something in 𝟘.

one-is-not-zero : πŸ™ β‰’ 𝟘
one-is-not-zero = Ξ» p β†’ Id-to-Fun p *
As for the proving that β‚€ : 𝟚 and ₁ : 𝟚 are not equal, we can reduce it to the previous case: if p : ₁ ≑ β‚€, we can map it to an identification q : πŸ™ ≑ 𝟘, which gives the sought-after contradiction: 
₁-is-not-β‚€ : ₁ β‰’ β‚€
₁-is-not-β‚€ p = one-is-not-zero q
  where
    q : πŸ™ ≑ 𝟘
    q = ap (𝟚-to-dep 𝟘 πŸ™) p
In effect this in an instance of a more general statement, namely that in a sum type (disjoint union) the left and right constructors are not equal. That is, we have 
inl-is-not-inr : βˆ€{β„“ β„“'} {A : Set β„“} {B : Set β„“'} {a : A} {b : B} β†’ inl a β‰’ inr b
inl-is-not-inr {β„“} {β„“'} {A} {B} p = one-is-not-zero q
  where
    -- assign πŸ™ to A and 𝟘 to B
    f : A + B β†’ Set
    f (inl a) = πŸ™
    f (inr b) = 𝟘

    q : πŸ™ ≑ 𝟘
    q = ap f p
On the other hand, Agda’s absurd pattern allows us to obtain a fast proof: 
inl-is-not-inr' : βˆ€{β„“ β„“'} {A : Set β„“} {B : Set β„“'} {a : A} {b : B} β†’ inl a β‰’ inr b
inl-is-not-inr' ()

top ⇑

Decidability

Alternative between A and Β¬ A:

decidable : βˆ€ {β„“} β†’ Set β„“ β†’ Set β„“
decidable A = A + Β¬ A

decidable-equality : βˆ€ {β„“} β†’ Set β„“ β†’ Set β„“
decidable-equality A = (x y : A) β†’ decidable (x ≑ y)
-- Alternatively, write as:
-- Ξ [ x ∈ A ] Ξ [ y ∈ A ] decidable (x ≑ y)
-- Ξ [ xy ∈ A Γ— A ] decidable ( π₁ x ≑ Ο€β‚‚ y)

Formally, decidable equality states that for any two terms of a given type they either are equal, in the sense that there exists an identification, or not.

As an experiment, let us check that 𝟚 has a decidable equality:

𝟚-decidable-equality : decidable-equality 𝟚
𝟚-decidable-equality β‚€ β‚€ = inl (idp β‚€)
𝟚-decidable-equality β‚€ ₁ = inr (β‰’-inv ₁-is-not-β‚€)
𝟚-decidable-equality ₁ β‚€ = inr (₁-is-not-β‚€)
𝟚-decidable-equality ₁ ₁ = inl (idp ₁)

top ⇑

  1. https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#82220β†©οΈŽ