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