Sorry, I was being silly. Martin
On Monday, 18 February 2019 19:22:23 UTC, dlicata wrote:
Hi,
I’m confused — does it even type check to ask pr₂ (x , y) ≡ y ?
I would expect
x : A
y : B(x)
(x,y) : Σ A B
fst (x,y) : A
snd (x,y) : B(fst (x,y))
so if beta for fst is weak, then
pr₂ (x , y) ≡ transport Y (p ⁻¹) y
is the best you could hope for. I.e., you have a path for the first beta, and a path over it for the second.
-Dan
> On Feb 18, 2019, at 12:37 PM, Martín Hötzel Escardó <escardo...@gmail.com> wrote:
>
> 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.