--- Day changed Sat Jul 01 2017 | ||

Nik05 | mietek i think i saw a lecture of wadler onces | 01/07 00:11 |
---|---|---|

Nik05 | but i stopped watching because i was annoyed by the way he spoke to his audiance | 01/07 00:11 |

Nik05 | mietek the talk about propositions and types is nice | 01/07 13:30 |

canndrew | how long til agda supports higher inductive types? | 01/07 16:28 |

canndrew | now that we have cubical types. | 01/07 16:28 |

joel135 | What is cubical types? | 01/07 16:30 |

canndrew | as in cubical type theory: https://arxiv.org/abs/1611.02108 | 01/07 16:32 |

canndrew | which is an implementation of homotopy type theory | 01/07 16:34 |

canndrew | it generalises the equality type to let you prove that (eg.) isomorphic types are equal, and the pointwise-equal functions are equal | 01/07 16:34 |

joel135 | Looks like fun. | 01/07 16:53 |

joel135 | Looks like I might understand it. | 01/07 17:02 |

rntz | so, 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/578aecff3269202bbd611f5439ada27d | 01/07 17:22 |

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