--- Day changed Thu Jul 27 2017 | ||

augur | is there a new conventional way to do something kind of like a proof that the type checker tries to provide automatically? | 27/07 05:24 |
---|---|---|

augur | like, implicit membership proofs? | 27/07 05:24 |

augur | ah! there is! | 27/07 05:26 |

apostolis | Hello | 27/07 16:26 |

apostolis | I had a problem a few months ago where I wanted to prove that the function (\neg fun) is unique. | 27/07 16:30 |

apostolis | I used irrelevance to avoid doing this. | 27/07 16:31 |

apostolis | Now it seems that I cannot use irrelevance because the function is used. | 27/07 16:32 |

apostolis | Now I am looking into proving the equality in Cubical TT, but I was wondering if there are easier solutions. | 27/07 16:33 |

apostolis | The fact that you are unable to prove uniqueness when you negate seems a very big problem to me. | 27/07 16:34 |

akr | Is there a better way to write this? https://gist.github.com/osense/b2a24d5ac433a098a9b09e7d0968b974#file-print-agda-L38 | 27/07 19:25 |

glguy | akr: Probably not without dropping into the macro system | 27/07 21:58 |

akr | ah ok, nevermind then :) | 27/07 22:51 |

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