[HoTT] Re: Why do we need judgmental equality?

["Martín Hötzel Escardó" <escardo.martin@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 3381 bytes --]

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



-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 4621 bytes --]