Re: [HoTT] about the HTS

[Matt Oliveri <atm...@gmail.com>]

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

Mike has explained to me that the approach I'm thinking of is not cohesion. 
Sorry about that.

On Thursday, March 23, 2017 at 7:33:32 AM UTC-4, Michael Shulman wrote:
>
> Unless I misunderstand, that's not at all what cohesion is about. 
> Lawvere's cohesion is about relating discrete sets to space-like 
> objects (in the non-homotopical up-to-homeomorphism sense).  Higher 
> cohesion is about relating oo-groupoids to "topological oo-groupoids" 
> in an analogous way. 
>
> On Thu, Mar 23, 2017 at 4:22 AM, Matt Oliveri <atm...@gmail.com 
> <javascript:>> wrote: 
> > Thanks. 
> > 
> > I agree that with the sSet option, with an equality reflection rule, it 
> > would be infeasible to check judgments without extra stuff from outside 
> the 
> > type theory proper. But what's wrong with that? We add extra stuff 
> anyway, 
> > like type classes, proof scripts, and implicit arguments. To me, it 
> seems 
> > that the practical concern of checking the truth of judgments does not 
> need 
> > to be solved by the design of the core type theory. Indeed, it seems 
> like 
> > better separation of concerns *not* to solve it there. 
> > 
> > Anyway, my understanding of bSet, from what Thierry Coquand said, is 
> that 
> > it'd be a more OTT-like version of sSet, which is more ETT-like. So 
> instead 
> > of paths between bSets being reflectable to judgmental equalities, they 
> > would be "strict propositions" (sProp), whose elements are not only all 
> > (typally) equal, but they also have no computational content. So any 
> > "transport" across a strict equality reduces away, as long as it doesn't 
> > change the type. (It doesn't have to be (judgmentally equal to) 
> > reflexivity.) 
> > 
> > I figure the idea is that bSet should be able to do everything sSet can, 
> > just with extra computationally-irrelevant transports thrown in to 
> appease a 
> > decidable type checker. 
> > 
> > I don't actually see how either of these universes would help define 
> > semi-simplicial types. I didn't realize that was the goal here. I 
> thought we 
> > were just trying to make set-level math more convenient. 
> > 
> > ----------- 
> > 
> > Though I haven't given it a serious thinking-about, I figured that stuff 
> > with cohesion would be a good way to make semi-simplicial types 
> definable, 
> > without adding non-fibrant types. 
> > (https://homotopytypetheory.org/2015/09/25/realcohesion/) It sounded 
> like 
> > cohesion gives you a set-level view of non-hsets, so I figured you 
> should be 
> > able to use strict equality in the construction of non-hsets that way. 
> > 
> > I suppose strict sets and cohesion can be combined. A set-level view of 
> > things should yield only strict sets, not arbitrary hsets. (I guess that 
> > requires a whole hierarchy of strict set universes. But unlike HTS, 
> they're 
> > all "included" in the univalent universes, not the other way around.) 
> > 
> > On Wednesday, March 22, 2017 at 5:01:16 PM UTC-4, v v wrote: 
> >> 
> >> 1. As Thierry pointed out previously, the problem with sSet is that if 
> we 
> >> postulate that nat:sSet, then for any (small) type T, the function type 
> T -> 
> >> nat is in sSet, e.g. nat -> nat is in sSet. 
> >> 
> >> Since it is possible to construct two elements of nat -> nat the 
> equality 
> >> between which is an undecidable proposition, it implies that the 
> >> definitional equality in any sufficiently advanced type system with 
> sSet and 
> >> nat:sSet is undecidable. 
> >> 
> >> That means that witnesses, in some language, of definitional equality 
> need 
> >> to be carried around and therefore the design of a proof assistant 
> where the 
> >> proof term is the proof is not possible in this system. 
> >> 
> >> 2. It is not so clear what would happen with only bSet and nat:bSet. 
> >> 
> >> Vladimir. 
> >> 
> >> 
> >> 
> >> 
> >> 
> >> On Mar 22, 2017, at 5:49 PM, Thierry Coquand <Thier...@cse.gu.se> 
> wrote: 
> >> 
> >> 
> >> If my note was correct, it describes in the cubical set model two 
> >> univalent universes 
> >> (subpresheaf of the first universe)  that satisfy 
> >> 
> >>  (1)   if   A : sSet    and   p : Path A a b   then   a = b : A  and p 
> is 
> >> the constant path a 
> >> (equality reflection rule) 
> >> 
> >>  (2)   if A : bSet and p and q of type Path A a b   then p = q : Path A 
> a 
> >> b 
> >> (judgemental form of UIP) 
> >> 
> >>  Maybe (1) or (2) could be used instead of HTS (and we would remain in 
> an 
> >> univalent 
> >> theory, where all types are fibrant) 
> >> 
> >>  For testing this, one question is:  can we define semi-simplicial 
> types 
> >> in (1)? in (2)? 
> >> 
> >>  Best regards, 
> >>  Thierry 
> >> 
> >> 
> >> 
> >> On 20 Mar 2017, at 16:12, Matt Oliveri <atm...@gmail.com> wrote: 
> >> 
> >> So the answer was yes, right? Problem solved? 
> >> 
> >> On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote: 
> >>> 
> >>> Just a thought… Can we devise a version of the HTS where exact 
> equality 
> >>> types are not available for the universes such that, even with the 
> exact 
> >>> equality, HTS would remain a univalent theory. 
> >>> 
> >>> Maybe only some types should be equipped with the exact equality and 
> this 
> >>> should be a special quality of types. 
> >>> 
> >>> Vladimir. 
> >>> 
> >>> PS If there are higher inductive types then the exact equality should 
> not 
> >>> be available for them either. 
> >> 
> >> 
> >> -- 
> >> 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 HomotopyTypeThe...@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 HomotopyTypeThe...@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 HomotopyTypeThe...@googlegroups.com <javascript:>. 
> > For more options, visit https://groups.google.com/d/optout. 
>

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