--- Day changed Sat Jul 01 2017
Nik05mietek i think i saw a lecture of wadler onces01/07 00:11
Nik05but i stopped watching because i was annoyed by the way he spoke to his audiance01/07 00:11
Nik05mietek the talk about propositions and types is nice01/07 13:30
canndrewhow long til agda supports higher inductive types?01/07 16:28
canndrewnow that we have cubical types.01/07 16:28
joel135What is cubical types?01/07 16:30
canndrewas in cubical type theory: https://arxiv.org/abs/1611.0210801/07 16:32
canndrewwhich is an implementation of homotopy type theory01/07 16:34
canndrewit generalises the equality type to let you prove that (eg.) isomorphic types are equal, and the pointwise-equal functions are equal01/07 16:34
joel135Looks like fun.01/07 16:53
joel135Looks like I might understand it.01/07 17:02
rntzso, I have a problem with agda instance arguments / instance search. I'm getting an ambiguity problem where I don't expect one. can someone explain the source of the problem to me? I've tried to minimize the example, but it's still a few dozen lines: https://gist.github.com/rntz/578aecff3269202bbd611f5439ada27d01/07 17:22

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!