On Friday, 8 February 2019 21:19:24 UTC, Martín Hötzel Escardó wrote:
why is it claimed that definitional equalities are essential to dependent type theories?
I've tested what happens if we replace definitional/judgmental
equalities in MLTT by identity types, working in the fragment of Agda
that only has Π and universes (built-in) and hence my Π has its usual
judgemental rules, including the η rule (but this rule could be disabled).
In order to switch off definitional equalities for the identity type
and Σ types, I work with them given as hypothetical arguments to a module
(and no hence with no definitions):
_≡_ : {X : 𝓤} → X → X → 𝓤 -- Identity type.
refl : {X : 𝓤} (x : X) → x ≡ x
J : {X : 𝓤} (x : X) (A : (y : X) → x ≡ y → 𝓤)
→ A x (refl x) → (y : X) (r : x ≡ y) → A y r
J-comp : {X : 𝓤} (x : X) (A : (y : X) → x ≡ y → 𝓤)
→ (a : A x (refl x)) → J x A a x (refl x) ≡ a
Σ : {X : 𝓤} → (X → 𝓤) → 𝓤
_,_ : {X : 𝓤} {Y : X → 𝓤} (x : X) → Y x → Σ Y
Σ-elim : {X : 𝓤} {Y : X → 𝓤} {A : Σ Y → 𝓤}
→ ((x : X) (y : Y x) → A (x , y))
→ (z : Σ Y) → A z
Σ-comp : {X : 𝓤} {Y : X → 𝓤} {A : Σ Y → 𝓤}
→ (f : (x : X) (y : Y x) → A (x , y))
→ (x : X)
→ (y : Y x)
→ Σ-elim f (x , y) ≡ f x y
Everything I try to do with the identity type just works, including
the more advanced things of univalent mathematics - but obviously I
haven't tried everything that can be tried.
However, although I can define both projections pr₁ and pr₂ for Σ, and
prove the η-rule σ ≡ (pr₁ σ , pr₂ σ), I get
p : pr₁ (x , y) ≡ x
but only
pr₂ (x , y) ≡ transport Y (p ⁻¹) y
It doesn't seem to be possible to get pr₂ (x , y) ≡ y without further
assumptions. But maybe I overlooked something.
One idea, which I haven't tested, is to replace Σ-elim and Σ-comp by
the the single axiom
Σ-single :
{X : 𝓤} {Y : X → 𝓤} (A : Σ Y → 𝓤)
→ (f : (x : X) (y : Y x) → A (x , y))
→ is-contr (Σ λ (g : (z : Σ Y) → A z)
→ (x : X) (y : Y x) → g (x , y) ≡ f x y)
I don't know whether this works. (I suspect the fact that "induction
principles ≃ contractibility of the given data with their computation
rules" is valid only in the presence of definitional equalities for
the induction principle, and that the contractibility version has a
better chance to work in the absence of definitional equalities.)
One can also wonder whether the presentation taking the projections
with their computation rules as primitive, and the η rule would
work. But again we can define Σ-elim but not Σ-comp for it.
In any case, without further identities, simply replacing definitional
equalities by identity types doesn't seem to work, although I may be
missing something.
Martin