quotients by equivalence relations. see HoTT Book 6.10 > On Aug 8, 2019, at 2:32 PM, Timothy Carstens wrote: > > Sorry for the broad & naive question. I'm a geometer by training but have been working in compsci for most of my career (with lots of time spent in Coq verifying programs). > > I've got a naive question that I hope isn't too inappropriate for this list: can anyone suggest some papers that show applications of HITs? I'm embarrassed to admit it, but I don't know any applications outside of synthetic homotopy theory and higher categories. > > Perhaps categorical semantics? But even still I'm not personally aware of any applied results from that domain (contrast with operational semantics; but I am extremely ignorant, so please correct me!) > > All my best and apologies in advance if this is off-topic for this list, > -t > > > -- > 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 . > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJGt_zG%2B04Rfbs_py%3DPYkubbwzeYb0TRhhfek-RT663uVUo%3D-A%40mail.gmail.com . -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/728FA1EA-014C-4242-8B34-33A17D7B9208%40gmail.com.