16

As a follow-up to What is Axiom K?, I'm wondering what happens when you use Agda with the --without-k option. Is the result less powerful? Is it a different language or do all previous programs still type check?

1
  • 6
    The pattern matching implementation of K (which is thus not an axiom, for it computes) is the key example of a program which no longer typechecks when you select --without-K. It's strictly a disabling switch. But it then lets you add equational principles which contradict K but are consistent with J.
    – pigworker
    Commented Sep 1, 2016 at 8:21

1 Answer 1

21

The situation with Martin-Löf type theory and Axiom K is in some ways analogous to Euclidean geometry and the parallel postulate. With the parallel postulate more theorems can be proven, but those are only about Euclidean spaces. Without the parallel postulate provable theorems are true of non-Euclidean spaces too, and one has the freedom to add explicitly non-Euclidean axioms.

Axiom K roughly says that equality proofs carry no non-trivial information and have no computational content. It's logically equivalent to both following statements:

-- uniqueness of identity proofs
UIP : {A : Set}(x y : A)(p p' : x ≡ y) → p ≡ p'

-- reflexive equality elimination
EqRefl : {A : Set}(x : A)(p : x ≡ x) → p ≡ refl

Naturally, both of these are unprovable with --without-K. I give here a couple more specific statements that are unprovable without K, and whose unprovability may seem counter-intuitive at first sight:

{-# OPTIONS --without-K #-}

open import Relation.Binary.PropositionalEquality
open import Data.Bool
open import Data.Empty

-- this one is provable, we're just making use of it below
coerce : {A B : Set} → A ≡ B → A → B
coerce refl a = a

coerceTrue : (p : Bool ≡ Bool) → coerce p true ≡ true
coerceTrue = ? -- unprovable

data PointedSet : Set₁ where
  pointed : (A : Set) → A → PointedSet

BoolNEq : pointed Bool true ≡ pointed Bool false → ⊥
BoolNEq = ? -- unprovable

Axiom K seems intuitive, since we defined Agda's propositional equality with a single refl constructor. Why even bother with the mysterious non-refl equality proofs whose existence we can't disprove without K?

If we don't have axiom K, we're free to add axioms that contradict K, enabling us to vastly generalize our notion of types. We can postulate the univalence axiom and higher-inductive types, which essentially gives us the type theory that the Homotopy Type Theory book is about.

Turning back to the Euclidean analogy: the parallel postulate posits that space is flat, so we can prove things that depend on space's flatness, but can't say anything about non-flat spaces. Axiom K posits that all types have trivial equality proofs, so we can prove statements that depend on that, but we can't have types with higher-dimensional structures. Non-Euclidean spaces and higher-dimensional types alike have some factor of weirdness but they're ultimately rich and useful source of ideas.

If we switch to "book" homotopy type theory, then "having trivial equalities" becomes a property that we can talk about internally and prove it for specific types that do have that property.

7
  • 3
    Indexed type definitions could be interpreted as non-indexed definitions with extra equality proofs in constructors that set the indices. In Agda, what ultimately matters is the method for unifying indices in dependent pattern matching, so _≡_ can be seen as a wrapper for whatever notion of equality stems from pattern matching. But pattern matching is ultimately reducible to applications of either Axiom K or Axiom J. So, even in the context of Agda, you should just look at the bare-bones refl/Axiom J definition of equality to see where the extra equalities come from. Commented Sep 2, 2016 at 7:11
  • 6
    As to why Axiom J enables HoTT, I doubt there is a single immediately intuitive answer for everyone, so here's my own. First, we should try to forget about our prior notions of types and just simply view the axioms as specifying some weird unseen object. We may than think of J as the induction principle for paths in spaces with arbitrary structure, and then J says that a predicate is true of a path if it's true of the constant path at one endpoint (doesn't matter which one) of the path. Commented Sep 2, 2016 at 7:24
  • 4
    This should be intuitively true, since there is a 2-path (continuous deformation) between any path and the constant paths at its endpoints, and the theory we're defining only proves things up to equality/paths, so if A = B, then exactly the same things should be true of A and B, specifically here, the same things should be true of a constant path at an endpoint and the path in consideration. Commented Sep 2, 2016 at 7:31
  • 8
    With the same space-path goggles on, Axiom K says that a predicate holds for a loop whenever it holds for the constant path at the loop's base. If we have e. g. holes in the space, this is just false, so if we take Axiom K as axiom, it's not possible to there be holes (or any notable structure) in spaces. So we might as well forget about spaces and talk about types as if they were sets. Commented Sep 2, 2016 at 7:35
  • 5
    As to how extra equalities come into picture; well, without univalence or higher inductive types, they don't. But Axiom J talks about arbitrary spaces, so it already talks about univalent and higher inductive stuff, we just need to actually add them to our theory by some means, which can be unfortunately only postulate if we want to stay in MLTT. It seems that getting rid of postulates requires starting from a significantly different type theory (cubical type theory is the current best candidate). Commented Sep 2, 2016 at 7:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.