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 <javascript:>> 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 <javascript:>. 
>
> > For more options, visit https://groups.google.com/d/optout. 
>
>

-- 
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.