[Wed Jul 3 20:34:54 2013] #hott + ##hott ? [Wed Jul 3 20:39:27 2013] :O [Wed Jul 3 21:05:19 2013] yeah [Wed Jul 3 21:05:50 2013] only that the ## one is registered [Wed Jul 3 21:06:06 2013] when I first joined here, the other one was registered but nobody was there [Wed Jul 3 21:06:21 2013] but no one actually talked in here [Wed Jul 3 21:06:28 2013] so I'm gonna do this: [Fri Jul 5 01:05:53 2013] #hott + ##hott ? [Tue Jul 9 06:02:33 2013] Thank you! [Wed Jul 10 17:16:11 2013] tunixman: you know about ##hott right? :] [Wed Jul 10 17:18:53 2013] I do now. [Wed Jul 10 17:20:57 2013] I think freenode must register some of these topics beforehand because both #hott and #homotopytypetheory were unavailable [Wed Jul 10 17:23:32 2013] Oh, wow. [Wed Jul 10 17:23:51 2013] I'd expect #hott and ##hott, but not #hott and #homotopytypetheory [Thu Jul 11 16:35:28 2013] So I hear this channel is hott [Thu Jul 11 18:39:31 2013] it's getting hott in here (so hot!) [Thu Jul 11 20:30:31 2013] shapr: maybe you're looking for ##hott? :] [Thu Jul 11 20:40:24 2013] Is this about homotopy type theory? [Thu Jul 11 20:40:39 2013] There's no topic! [Thu Jul 11 20:52:39 2013] shapr: it's in ##hott [Thu Jul 11 20:52:51 2013] freenode topic channel policy dictates two ## [Thu Jul 11 20:53:00 2013] I tried to register this one but couldn't [Thu Jul 11 20:53:07 2013] its the same with ##categorytheory and ##logic [Thu Jul 11 20:53:15 2013] you can only have single # for project channels [Thu Jul 11 20:53:24 2013] like #haskell, #idris, #coq [Thu Jul 11 20:54:55 2013] shapr: though in ##hott there are about 16 people and a proper topic :] [Thu Jul 11 21:02:27 2013] bah [Thu Jul 11 22:48:01 2013] hi :) [Thu Jul 11 22:50:49 2013] structuralist: hi [Thu Jul 11 22:51:01 2013] structuralist: you probably want to go to ##hott (note the double hash) [Thu Jul 11 22:51:08 2013] if you're looking for the homotopy type theory [Thu Jul 11 22:51:10 2013] channel [Thu Jul 11 22:51:17 2013] ah yup thanks [Fri Jul 12 03:20:58 2013] hmm, not sure if that went through [Fri Jul 12 03:21:07 2013] as I was saying… [Fri Jul 12 03:21:23 2013] raichoo: you probably want to join ##hott (with the double hash) [Fri Jul 12 03:21:38 2013] that's where the homotopy type theory channel is [Fri Jul 12 03:25:12 2013] darinmorrison: Ah thanks. [Fri Jul 12 03:25:18 2013] np [Fri Jul 12 05:07:47 2013] drbalor: you're probably looking for ##hott which is the actual homotopy type theory channel :] [Fri Jul 12 05:17:21 2013] ah [Fri Jul 12 05:17:24 2013] thanks [Fri Jul 12 21:10:20 2013] Just wondering if this is the channel for http://homotopytypetheory.org/ ? [Sat Jul 13 10:19:59 2013] mcclurmc: if you're looking for the homotopy type theory channel, it's at ##hott (note the double hash) [Sat Jul 13 11:29:35 2013] darinmorrison: ah, that's better :) [Sat Jul 13 11:29:37 2013] thanks! [Sat Jul 13 11:30:12 2013] darinmorrison: you may want to mention that in the topic of this channel... [Sat Jul 13 11:31:03 2013] mcclurmc: unfortunately I don't have access to that or I would :[ [Sat Jul 13 11:31:22 2013] darinmorrison: understood [Mon Jul 15 20:11:28 2013] hello. [Mon Jul 15 20:11:55 2013] has anyone read carefully the definition of a loop space in the HoTT book? [Tue Jul 16 19:55:15 2013] been offline. can anyone help with sasl problem with colloquy on ios on cell? [Tue Jul 16 21:28:17 2013] rh: can you phrase it in the form of a type judgment? [Tue Jul 16 21:28:28 2013] * is still on the first chapter and hopelessly lost. [Thu Jul 18 08:05:06 2013] lambdas? [Thu Jul 18 08:05:15 2013] and homotopies [Thu Jul 18 08:05:16 2013] ? [Fri Jul 19 12:07:53 2013] blackdog IbnFirnas: think you might be looking for ##hott (with two #). This is not the actual homotopy type theory channel :] [Fri Jul 19 12:23:20 2013] darinmorrison: Thank you! :) [Fri Jul 19 12:24:17 2013] np [Fri Jul 19 15:42:31 2013] Hello [Fri Jul 19 16:04:31 2013] bakibour: wrong channel, you want ##hott with 2 hashes :] [Fri Jul 19 16:05:59 2013] heh [Fri Jul 19 16:06:03 2013] whats this one about then? [Fri Jul 19 16:06:10 2013] a secret level? [Fri Jul 19 16:06:22 2013] good question. Was registered a long time ago and abandoned [Fri Jul 19 16:06:31 2013] :) [Fri Jul 19 16:06:37 2013] nobody can change the topic so I keep having to redirect people :[ [Fri Jul 19 16:06:38 2013] some kind of old ruin [Fri Jul 19 16:06:41 2013] yep… [Thu Aug 1 09:21:12 2013] *** Notice -- TS for #hott changed from 1375363257 to 1339222263 [Fri Aug 2 00:09:22 2013] [freenode-info] if you're at a conference and other people are having trouble connecting, please mention it to staff: http://freenode.net/faq.shtml#gettinghelp [Sun Nov 24 14:16:43 2013] [freenode-info] channel trolls and no channel staff around to help? please check with freenode support: http://freenode.net/faq.shtml#gettinghelp [Mon Dec 2 04:59:08 2013] is this channel about HoTT? [Mon Dec 2 22:02:09 2013] You want ##hott, not #hott [Thu Dec 26 23:32:14 2013] i'm busy [Thu Dec 26 23:32:55 2013] leaving [Sun Jan 5 18:55:48 2014] [freenode-info] help freenode weed out clonebots -- please register your IRC nick and auto-identify: http://freenode.net/faq.shtml#nicksetup [Wed Jan 8 15:19:43 2014] hi jgross [Wed Jan 8 18:46:17 2014] Hi Anarchos. (If you're saying hi because I recently showed up: my client, which is supposed to be on all the time, crashed.) [Wed Jan 8 18:49:20 2014] jgross yes that was this reason :) [Thu Jan 16 14:07:33 2014] hi everybody [Fri Jan 17 14:11:54 2014] hi everybody [Fri Jan 17 14:11:59 2014] what is a Quillen model ? [Fri Jan 17 21:29:39 2014] A Quillen model category is, hand-wavily, a category that you can do homotopy theory in. If you're looking for a source, I think http://folk.uio.no/paularne/SUPh05/DS.pdf (Homotopy theories and model categories by W. G. Dwyer and J. Spalinski) is a decent introduction. [Fri Jan 17 21:29:39 2014] Also, you probably want to be in ##hott. [Fri Jan 17 22:05:13 2014] This might be the first time I've seen the adverbial form of 'hand-wave'. [Sat Jan 18 11:09:37 2014] hi funfunctor [Sat Jan 18 11:46:05 2014] hi jgross, no news about a computer implementation of hott ? [Sat Jan 18 13:48:58 2014] hi jgross [Sat Jan 18 13:49:04 2014] what are the news jgross ? [Sat Jan 18 16:48:08 2014] hu Anarchos [Sat Jan 18 16:48:23 2014] s/hi [Sat Jan 18 16:49:51 2014] funfunctor hi [Sat Jan 18 16:50:09 2014] funfunctor i come here to see if there are progress in implementing the hott book :) [Sat Jan 18 16:54:05 2014] Anarchos: How do you mean `implementing` the HoTT book? Its already published [Sat Jan 18 17:11:04 2014] funfunctor i mean that all of the demosntrations are written in a near formal language... [Sat Jan 18 17:12:05 2014] Anarchos: Do you mean something like Agda 2 ? [Sat Jan 18 17:12:26 2014] Anarchos: http://en.wikipedia.org/wiki/Agda_%28programming_language%29 [Sat Jan 18 17:20:51 2014] funfunctor yes, but i would prefer a language where it would be possible to write things very close to the presentation of the hott book [Sat Jan 18 17:22:50 2014] Anarchos: You should leave #hott and join ##hott instead. I announced https://groups.google.com/forum/#!topic/homotopytypetheory/GmXKEArD3HY when it happened there. It's an implementation of univalence based on cubical sets. [Sat Jan 18 17:23:47 2014] Alternatively, you might be looking for https://github.com/HoTT/HoTT and https://github.com/HoTT/HoTT-Agda? [Sat Jan 18 17:23:56 2014] jgross thanks [Tue Jan 28 09:57:57 2014] Is the interval type isomorphic to the unit type? [Tue Jan 28 12:34:55 2014] nevermind, it is [Thu Jan 30 10:22:32 2014] hola [Sun Feb 2 19:59:01 2014] *** Notice -- TS for #hott changed from 1391387964 to 1339222263 [Sun Feb 2 21:28:01 2014] [freenode-info] why register and identify? your IRC nick is how people know you. http://freenode.net/faq.shtml#nicksetup [Sun Feb 2 21:29:11 2014] *** Notice -- TS for #hott changed from 1391394475 to 1339222263 [Sun Feb 2 23:44:07 2014] [freenode-info] channel flooding and no channel staff around to help? Please check with freenode support: http://freenode.net/faq.shtml#gettinghelp [Mon Feb 3 00:38:44 2014] [freenode-info] if you're at a conference and other people are having trouble connecting, please mention it to staff: http://freenode.net/faq.shtml#gettinghelp [Tue Feb 11 14:21:07 2014] [freenode-info] help freenode weed out clonebots -- please register your IRC nick and auto-identify: http://freenode.net/faq.shtml#nicksetup [Mon Mar 3 12:12:58 2014] So … what is the distinction between here and ##hott? [Sat Mar 8 00:25:46 2014] [freenode-info] help freenode weed out clonebots -- please register your IRC nick and auto-identify: http://freenode.net/faq.shtml#nicksetup [Sat Mar 8 19:46:42 2014] Hello :-) [Tue Mar 25 23:00:08 2014] is there an explanation of homotopy theory for non-mathematicians. I am reading the paper but got lost at univalence foundations. [Tue Apr 1 07:45:18 2014] [freenode-info] please register your nickname...don't forget to auto-identify! http://freenode.net/faq.shtml#nicksetup [Tue Apr 1 14:29:57 2014] I am reading the hott book and I like the explanation of current type theory in the book. I am a non-mathematician. Just wanted to check if the type theory is better explained in any other book. [Sun Apr 6 16:23:45 2014] in what sense is the univalence axiom not yet "canonical", "computationally effective", "constructive", or whatever term i'm supposed to be using? [Sun Apr 6 16:23:56 2014] what is, formally, what we're missing? [Sun Apr 6 16:48:00 2014] tulcod: iiuc, the univalence axiom implies that, given two universes "T" and "U", two equivalent types "x" and "y" in "T", and a function "f : T -> U", then "f(x)" and "f(y)" must also be equivalent types (in "U")... but, again iiuc, there is no general way to compute the equivalence between "f(x)" an "f(y)" given the equivalence between "x" and "y" [Sun Apr 6 16:48:36 2014] wonderful - netsplit right after i say something [Sun Apr 6 16:48:43 2014] :( [Sun Apr 6 16:49:14 2014] anyway, every black cloud has a silver lining: if i was wrong, please tell me! [Sun Apr 6 16:51:51 2014] tulcod: "[15:46] tulcod: iiuc, the univalence axiom implies that, given two universes "T" and "U", two equivalent types "x" and "y" in "T", and a function "f : T -> U", then "f(x)" and "f(y)" must also be equivalent types (in "U")... but, again iiuc, there is no general way to compute the equivalence between "f(x)" an "f(y)" given the equivalence between "x" and "y"" [Sun Apr 6 16:52:21 2014] meaning, there is no way to find the transport? [Sun Apr 6 16:52:39 2014] tulcod: you can find for specific "x", "y" and "f" [Sun Apr 6 16:53:13 2014] tulcod: but there's no general "rule" for constructing it [Sun Apr 6 16:53:19 2014] got it [Sun Apr 6 16:53:23 2014] tulcod: but the important part is IIUC [Sun Apr 6 16:53:27 2014] IF I UNDERSTAND CORRECTLY [Sun Apr 6 16:54:00 2014] well it agrees with my understanding [Sun Apr 6 16:54:55 2014] and does anyone know the cubical sets paper by coquand? does it solve this? [Sun Apr 6 16:55:19 2014] i mean i suppose a big question i'm struggling with is: what does it mean for some theory or model or whatever to be constructive? [Tue Apr 8 05:42:30 2014] [freenode-info] why register and identify? your IRC nick is how people know you. http://freenode.net/faq.shtml#nicksetup [Sun Apr 13 19:10:17 2014] https://docs.google.com/drawings/d/1IhJ2Utmb9OpiBSCcjSpZFFIqfSaqDsqWtzZ9_A8D59Y [Sun Apr 13 19:10:24 2014] I has a question: what should be on place of ?1 and ?2 ? [Sun Apr 13 19:10:31 2014] When we do topology we use index space instead of them (X for indexing path and I for indexing homotopy's "instances"). [Sun Apr 13 19:10:37 2014] But in HoTT it isn't clear what to substitute, because our paths are just morphisms. [Sun Apr 13 19:11:07 2014] Are ?1 and ?2 just one-point sets? [Sun Apr 13 19:11:37 2014] There is in book different description of fibration =/ There we must lift path, but not homotopy as I did on picture. [Sun Apr 13 19:11:49 2014] Why first description is right? Isn't fibration defined for 2-paths? [Sun Apr 13 19:15:35 2014] Oh, it seems that there can be different lifting properties: homotopy / path at least. On wiki def of fibration is about homotopy lifting only. [Mon Apr 14 07:29:15 2014] in intensional type theory without univalence, we have canonicity, which, if i understood it correctly, means that every element can be expressed as this or that constructor of its type. however, don't we still have nontrivial identity paths? but by canonicity, these are just reflection, right? [Mon Apr 14 11:16:16 2014] or is intensional type theory compatible with extensional? [Mon Apr 14 11:16:48 2014] (that sounds... curious) [Mon Apr 14 15:24:15 2014] (did i miss anything?) [Tue Apr 15 18:47:44 2014] In Intensional TT how can we get "non-trivial" proof of propositional equality? [Tue Apr 15 18:47:52 2014] When we have not-coinciding definitional and propositional equalities? [Tue Apr 15 22:30:39 2014] Rc43: When your meta-theory gives them to you. For example, functional extensionality in OTT or HoTT, or univalence in HoTT. Vanilla MLTT is compatible with the axiom that all proofs of equality are trivial, so you need a stronger theory to find the non-trival ones. [Thu Apr 24 14:33:38 2014] hi ! When i try the code of hott/agda in agda 2.3.0.1 for windows, i get :"unresolved metas in Base:77 8-12 (the line is Paths = _==_) [Thu Apr 24 16:51:57 2014] Is the agda code accurate ? [Fri May 30 13:49:31 2014] Hi, I've read (and I think I've understood) this http://www.csie.ntu.edu.tw/~b94087/ITT.pdf [Fri May 30 13:49:48 2014] but i'm confused by the notation used in the HoTT book [Fri May 30 13:49:55 2014] (specially regarding equality) [Mon Jun 16 13:26:24 2014] Hi, I'm trying to get a vim plugin working with the coq released with HoTT [Mon Jun 16 13:26:54 2014] there's some strangeness with the xml being send back by hoqtop when in -ideslave mode [Mon Jun 16 13:27:12 2014] Does anyone know if there's been any changes to that part of coq? [Mon Jun 16 21:04:00 2014] Hi. I'm trying to get a vim plugin working with the HoTT version of Coq [Mon Jun 16 21:04:16 2014] Does anyone know if there's been any changes that should effect that part of the code? [Tue Jun 17 13:40:51 2014] tbelaire: HoTT/coq is based off of a trunk newer than 8.4. They've been changing the interaction in trunk (I think they might be done now), and I wouldn't be surprised if some (or all) of those changes were already in HoTT/coq. [Tue Jun 17 14:00:00 2014] I think I got it 90% fixed [Tue Jun 17 14:00:39 2014] It was just sending "12", which was throwing the xml parser for a loop [Tue Jun 17 14:00:47 2014] since there's no root node [Tue Jun 17 14:01:03 2014] before I think it flushed the stream between each one [Tue Jun 17 14:01:50 2014] I think it was actually just the warnings and other elements which the code wasn't expecting [Tue Jun 17 14:02:01 2014] and there was just a few more when parsing the HoTT library [Tue Jun 17 14:02:09 2014] or something [Tue Jun 17 14:02:17 2014] thanks jgross [Tue Jul 1 19:25:36 2014] How often does an actual conversation take place here? [Tue Jul 29 15:53:00 2014] hey [Tue Jul 29 15:53:49 2014] hey [Thu Aug 21 18:11:43 2014] Hey, is this the channel for homotopy type theory? [Thu Aug 21 18:13:44 2014] Looks like that's ##hott. [Thu Aug 21 18:13:51 2014] Ta-ta. [Sun Aug 31 10:43:15 2014] I am confused by section 1.4 "Dependent function types" [Sun Aug 31 10:43:29 2014] "Homotopy Type Theory: Univalent Foundations of Mathematics" [Sun Aug 31 10:45:14 2014] hard to explain what I am confused about... for starters I do not understand how they can be considered cartesian products over a type [Sun Aug 31 11:53:30 2014] I do not understand the difference between type families and dependent function types [Sun Aug 31 11:53:44 2014] how is B : A -> U a type family but not a dependent function type? [Sat Sep 6 14:28:45 2014] hi all [Fri Nov 28 19:34:10 2014] I have a question about the way quotients are defined in the book [Fri Nov 28 19:34:59 2014] It mentions that the underlying type doesn't have to be a set, but it doesn't seem to address whether the relation has to be a mere relation [Sun Nov 30 22:42:22 2014] is the new model of "cubical set weith connection" a faithful model of HoTT? [Sun Nov 30 22:42:47 2014] is the new model of "cubical set weith connection" a faithful model of HoTT? [Sun Jan 11 00:06:09 2015] I wonder if this is a good place to discuss or ask questions about the general concepts and technical language used by people working in the field of automated theorem provers, and if not, what's a better place for me to go to? [Thu Jan 22 08:06:30 2015] Hi there [Mon Jan 26 18:14:09 2015] I had a question related to judgmental equalities in Coq: I have some situations where for example y judgmentally equals f x, and maybe I know something like L: (h o f) == g, and I'm at goal h y = g x with f and (h o f) == g nowhere in sight, just out in the library somewhere. [Fri Mar 6 15:21:35 2015] hey guys, is measure theory hard? [Tue Mar 17 13:52:39 2015] Why Pi itself isn't Pi Set (Set -> Set)? [Tue Mar 17 14:08:41 2015] The "type" of Pi is Pi_{A : Set} (A -> Set) -> Set. But that would be a self-referential type, so Pi is not actually a type constructor. [Tue Mar 17 14:20:13 2015] jgross, couldn't we handle self-reference with universal polymorphism or any tricky fixpoint type? [Tue Mar 17 14:21:10 2015] (in latter case maybe we will have this "fixpoint" primitive instead of pi-type) [Tue Mar 17 14:26:42 2015] Or maybe make "pi-polymorphism" (i.e. Pi0, Pi1, etc.). Not sure if it is useful at all, just curious. [Tue Mar 17 14:27:08 2015] Rc43: no, the type of a term is never allowed to mention the term itself. Unless you want very dependent types (http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.4169) or insanely dependent types (https://github.com/UlfNorell/insane). [Tue Mar 17 14:27:45 2015] But if you have that, then your "Pi" type might be even more general, and not capturable in that formalism, but I'm not sure. [Tue Mar 17 14:52:43 2015] jgross, thanks for references! [Thu Mar 19 11:49:52 2015] I still don't understand concept of Pi-type completely. Why do we need it at all? Only because we need to have type of lambdas? [Thu Mar 19 11:50:00 2015] But when to use lambda and when Pi? [Thu Mar 19 11:50:04 2015] E.g. [(A : Set) -> (B : A -> Set) -> (a : A) -> (b : B a) -> Sigma A B] -- which binder we should chose here for A, B and b? Lambda or Pi-type? [Thu Mar 19 11:52:09 2015] Yes, because we need a type for lambdas. Without Pi, functions have no types. [Thu Mar 19 11:53:07 2015] Whether you chose Lambda or Pi depends on whether you want to end up with a type, or with a term that is not also a type (i.e., a function that you can pass arguments to). [Thu Mar 19 11:54:59 2015] jgross, if I chose Pi-type, then I don't pass arguments, but just stick them with some label a.k.a. type constructor? [Thu Mar 19 11:56:09 2015] Hmm, seems that I don't get it. [Thu Mar 19 11:57:05 2015] If I chose Pi-type, then I can define function that is of type of it, so in most cases I should use plain lambda... [Thu Mar 19 11:58:10 2015] Conventional binder here is lambda, right? [(A : Set) -> (B : A -> Set) -> (a : A) -> (b : B a) -> Sigma A B] [Thu Mar 19 12:01:00 2015] No, Pi; notice "a" and "b" are not used in the return. [Thu Mar 19 12:10:18 2015] "\Pi_(A : Set) \Pi_(B : A -> Set) \Pi_(a : A) B a -> Sigma A B" is the type of "\lambda (A : Set) (B : A -> Set) (a : A) (b : B a) => (a; b)" (where "(a; b)" is a dependent pair) [Thu Mar 19 12:24:35 2015] Oh, thanks [Thu Mar 19 12:25:04 2015] I have found that actually I don't know what generally term of Pi-type look like. [Thu Mar 19 12:25:25 2015] (With exception for non-dependent function, of course.) [Thu Mar 19 12:28:42 2015] Term of [\Pi (a : A) . B] is just [\lambda (a : A) . (b : B)]? [Thu Mar 19 12:30:10 2015] Yes. As long as by "b : B", you mean "an expression of type B" and not "a fresh binder named 'b' of type 'B'" [Thu Mar 19 12:31:59 2015] Yep, expr of type B. [Thu Mar 19 12:32:41 2015] And B is expr which depends on 'a'. [Thu Mar 19 15:01:46 2015] Am I right that we have normalization rules only for term? [Thu Mar 19 15:01:57 2015] I.e. only for lambdas, but not for pi. [Thu Mar 19 15:12:06 2015] Types are also terms. You can normalize underneath pi. [Thu Mar 19 21:38:59 2015] * wonders if mentioning HoTT in his 'purpose' statement for his Georgia Tech application will help his chances, or hurt them [Sun Mar 29 08:47:20 2015] hi [Sun Mar 29 08:47:26 2015] 1st question about homotopy type theory: the h-levels seem reminiscent to the chain complexes from homology, and they are also describing relationships between boundaries and interiors, is there a connection here? [Mon Aug 10 00:28:45 2015] Hey [Mon Aug 10 11:04:15 2015] Have the notions of operad or symmetric monoidal category been formalized in hott? [Sat Aug 29 01:08:21 2015] [freenode-info] please register your nickname...don't forget to auto-identify! http://freenode.net/faq.shtml#nicksetup [Thu Oct 29 18:38:00 2015] Oh, it's actually ##hott. [Wed Nov 4 13:07:50 2015] hello out there [Wed Nov 4 13:07:56 2015] is this the homotopy irc? [Sat Nov 14 01:19:39 2015] [freenode-info] help freenode weed out clonebots -- please register your IRC nick and auto-identify: http://freenode.net/faq.shtml#nicksetup [Tue Nov 24 10:46:33 2015] Hai [Mon Jan 18 05:06:27 2016] Yay, new join party! [Mon Jan 18 05:06:41 2016] nobody is here [Mon Jan 18 08:54:22 2016] I'm here. [Mon Jan 18 08:54:29 2016] still reading HoTT, slowly. [Fri Feb 19 16:32:58 2016] is this the irc chat for homotopy type theory? [Fri Feb 19 16:35:54 2016] actually that's ##hott, in here we just need A/C. [Fri Feb 19 16:37:18 2016] LOL [Fri Feb 19 16:38:16 2016] I was hoping for a funny answer and you have not failed to deliver :P [Fri Feb 19 16:39:35 2016] :P [Tue Feb 23 18:03:48 2016] *** Notice -- TS for #hott changed from 1456268545 to 1339222263 [Sat Mar 26 21:52:01 2016] Does the HoTT Coq Library come with tactics to automatically prove goals such as `x * (y * z) = y * (x * z)` where `*` is the product type? [Sat Mar 26 21:52:35 2016] Alternately, is there a way to call `congruence` (it doesn't seem to work if all I do is import `HoTT`). [Sat Mar 26 22:21:27 2016] Is there a way to use `setoid_rewrite` to rewrite under binders? [Sun Mar 27 01:46:51 2016] The HoTT book talks about the "-1 truncation"/"bracket type"/"squash type" in chapter 3.7. what is the equivalent to this type former in the HoTT library? [Mon Apr 25 10:01:41 2016] hello [Mon Apr 25 10:02:12 2016] Is this channel pertaining to the Homotopy Type Theory? [Wed Jun 1 02:17:22 2016] hi <3 [Sun Nov 6 11:55:49 2016] https://www.youtube.com/watch?v=3EsJLNGVJ7E & https://wikileaks.org/podesta-emails/emailid/15893, http://www.reuters.com/article/us-usa-election-foundation-idUSKBN12Z2SL & https://wikileaks.org/podesta-emails/emailid/3774 (ctrl+f qatar) - please don't let these be buried [Sun Nov 6 19:08:47 2016] no. [Wed Nov 9 01:24:11 2016] bollu: you mean the univalence [Wed Nov 9 01:24:14 2016] ? [Wed Nov 9 01:25:46 2016] univalence means that if A an B are equivalent then they are equal as types (It says some thing stronger actually) [Wed Nov 9 01:28:02 2016] The Id (of A) type is the type that witness the equality of elements of A [Wed Nov 9 01:28:29 2016] univalence talks about, in some sense the Id type of U for some universe [Wed Nov 9 01:29:32 2016] (note that in an intensional theory any universe U_i is also a type (in U_{i+1} of course) so it makes sense to talk about its Id type [Wed Nov 9 03:34:10 2016] quick HoTT question: so, sigma types is like a tuple with the second type dependant on the first type, right? [Wed Nov 9 14:50:35 2016] I think I'm in the wrong channel. I thought this place was for discussing things that are #hott [Wed Feb 1 01:06:39 2017] what are the applications of hott in cryptography? why are militaries spending a lot of money on hott? [Wed Feb 1 09:24:26 2017] militaries are spending a lot of money on HoTT? [Wed Feb 1 13:34:52 2017] Hi [Wed Feb 1 13:35:15 2017] I thought that this channel was for posting stuff we consider hott [Fri Feb 24 11:12:42 2017] In the first theorem of http://www.cs.cmu.edu/~rwh/papers/chitt/popl17.pdf, what does the notation bool [\cdot] mean? [Fri Feb 24 11:14:46 2017] I am also not sure what the point is of writing a paper in gibberish, as opposed to references where you get your syntax from. [Fri Feb 24 11:17:34 2017] Context: If M ∈ bool [·] then either M ⇓ true [Sat Feb 25 17:35:36 2017] HoTT question: how is the expression refl_x . refl_x well typed? refl_x is an inhabitant of the type (x =A x) where (x : A). Hence, it makes no sense to talk about "composition of refl" [Mon Feb 27 04:16:36 2017] So whats going on here? [Mon Feb 27 05:57:44 2017] bollu: why not [Mon Feb 27 05:58:40 2017] composition of p : x = y and q : y = z can be defined in the case of refl_x, x y and z are the same [Mon Feb 27 06:00:10 2017] bollu: looks like this is the wrong channel. The correct one is ##hott [Tue Feb 28 02:32:01 2017] is anyone here alive? [Fri Apr 14 05:09:23 2017] Hi to all. I would like to ask what are the most active areas of research today in mathematics related to (theoretical )computer science? [Sun Jul 23 09:30:33 2017] in a very simple language where the only types are nat and bool (not even functions), I'm trying to understand how to introduce propositions as first-class objects, to manipulate "proofs" that some boolean is true [Sun Jul 23 09:32:43 2017] if I understand correctly dependent type theory, I should add a type "Prop", and then a rule that says that if a term t has type bool, then "t is true" has type Prop [Sun Jul 23 09:33:34 2017] I should then also say that whatever has type Prop can also be used as a type, and then I should have rules to be able to derive that a term has type "t is true" [Mon Jul 31 15:28:16 2017] is this place about homotopy type theory? [Mon Jul 31 17:10:57 2017] no this is the plaace for hott mathematicians [Mon Jul 31 17:11:14 2017] in your area tonite [Mon Jul 31 17:11:23 2017] (yes this is apparently the channel got HoTT) [Mon Jul 31 17:44:12 2017] what's going on here? [Mon Jul 31 17:44:18 2017] seems not alive [Mon Jul 31 18:41:08 2017] * got = for i just cant type [Mon Jul 31 18:41:29 2017] i knew someting was wrong here [Mon Jul 31 18:41:33 2017] actual channel is ##hott [Mon Jul 31 18:41:36 2017] aoeu, ^ [Mon Aug 7 13:45:46 2017] I am just reading a basic description of what is up with HoTT and the big feature seems to be univalence, but I am not completely sure what raises the computability problem [Mon Aug 7 13:45:57 2017] is it the equivalence of functions that is a problem? [Mon Aug 7 15:04:46 2017] No; it's just that if you look at the definition of HoTT, definitions of functions out of the identity type proceed by using the elimination rule, which is kind of like a weak version of pattern matching. But you only ever specify what to do when the input is reflexivity, so it wasn't at all clear what to do when the input involved univalence, since univalence is an axiom rather than a definition. [Mon Aug 7 15:05:57 2017] Today, it is an open question whether it is even possible to give a computational model of HoTT. However, other type theories that support univalence and many other aspects of HoTT have been endowed with computational interpretations; principal among these is the Swedish "cubical type theory", which has univalence and computation. [Mon Aug 7 15:30:10 2017] okay, maybe in my mind I am just being more flexible with how univalence is allowed to be implemented ... whether it is an axiom or a definition (and it is a definition in cubical type theory, yes?) does not strike me as so important [Mon Aug 7 15:40:50 2017] erisco: This difference is important, because it is precisely the difference between something that can compute and something which gets stuck / is not computational. [Mon Aug 7 15:46:25 2017] what I mean is that I am not losing any sleep over having univalence not as an axiom, but I am also oblivious as to what the use of that is [Mon Aug 7 15:48:20 2017] erisco: The basic idea is that if you prove an existential statement in type theory, like "There exists a number 'n' such that P(n) holds", then you should be able to find out exactly what number that 'n' was. This is one of the most important things about type theory [Mon Aug 7 15:48:35 2017] But if univalence is an axiom, then you can't generally find out what number that 'n' actually is. [Mon Aug 7 15:49:45 2017] As an example, there is a very important number which a brilliant scientist named Guillaume Brunerie spent his entire dissertation calculating using very sophisticated mathematics—and this was necessary because univalence at the time was not computational. But if you do Brunerie's proof in a version of type theory with computational univalence, in principle you can mechanically determine that number. [Mon Aug 7 15:51:29 2017] So, it's very important in a practical sense to have a proper treatment of these principles that avoids axioms. Theoretically it is important too, since some people want to use HoTT as a logic. [Mon Aug 7 15:52:15 2017] "Logics" which have axioms and do not admit something called "cut elimination" (the proof-theoretic analogue of computation) are not well-behaved, and it is widely agreed that such formal systems shouldn't even be called logics. [Mon Aug 7 15:53:54 2017] (note the issue with cut elimination is subtly different from constructivity in the sense of the 'existential property' that I described above—classical logic has cut elimination too.) [Mon Aug 7 15:57:33 2017] when you introduce the existential the number n is part of the rule, usually, yes? [Mon Aug 7 18:30:11 2017] ha, just before leaving, it sounds like erisco discovered precisely the problem with breaking cut elimination ;-) [Sat Aug 12 23:19:07 2017] When selling dependent type theory often sized vectors are used, i.e. Vec n. What is a similar pitch for HoTT? [Sun Aug 13 17:56:00 2017] When selling dependent type theory often sized vectors are used, i.e. Vec n. What is a similar pitch for HoTT? [Sun Nov 26 02:10:04 2017] Hey there [Sun Nov 26 02:10:41 2017] What are the prerequisites for trying to understand Homotopy Type Theory?