--- Day changed Sun Jun 11 2017 | ||

Nik05 | thank you mietek :) | 11/06 00:00 |
---|---|---|

joel135 | What's de Bruijn for λx. x λy. y — λ. 0 λ. 0 or λ. 1 λ. 0? | 11/06 10:30 |

adamse | joel135: the first one | 11/06 11:01 |

joel135 | ok good | 11/06 11:22 |

Nik05 | Why is Relation.Nullary called this way? Arent those Unary relations? | 11/06 22:04 |

Nik05 | mietek if I want to define a homogenous binary relation, does this type exists in Set_1? | 11/06 22:47 |

Nik05 | HomoRel A = A \to A \to Set | 11/06 22:49 |

mietek | Nik05: well, have you tried defining it? | 11/06 22:49 |

Nik05 | yes it doesnt let me :P | 11/06 22:49 |

mietek | I don’t know why it is called that way. | 11/06 22:49 |

mietek | show your work | 11/06 22:49 |

Nik05 | well it does when the type is HomoRel : Set \to Set\_1 | 11/06 22:50 |

Nik05 | Set -> Set1 | 11/06 22:50 |

mietek | so… what’s your question again? :) | 11/06 22:50 |

Nik05 | oh wait ofcourse it has to be in Set1 | 11/06 22:50 |

Nik05 | It was just, you said I dont need to take care of these set levels yet :P | 11/06 22:51 |

mietek | I said Set1 will solve most of your issues | 11/06 22:51 |

Nik05 | oh oke | 11/06 22:51 |

Nik05 | sorry about that | 11/06 22:51 |

mietek | no worries | 11/06 22:51 |

mietek | I mean, it really depends what are you going to try | 11/06 22:52 |

mietek | if you’re going to want to have relations of relations next | 11/06 22:52 |

mietek | you’re going to need a bigger hammer | 11/06 22:52 |

Nik05 | Oké, I dont think I well reach those | 11/06 22:53 |

Nik05 | Also tried some Coq, and there this is all implicit | 11/06 22:54 |

mietek | you should try Idris | 11/06 22:54 |

Nik05 | Why? | 11/06 22:55 |

mietek | it’s similar to Agda, unlike Coq | 11/06 22:55 |

mietek | and it has universe cumulativity | 11/06 22:55 |

mietek | so you never have to think about universe levels — I think. {AS} would know more | 11/06 22:55 |

mietek | I’m not a huge fan of Coq | 11/06 22:56 |

mietek | but YMMV | 11/06 22:56 |

mietek | Agda and Idris have the de Bruijn criterion | 11/06 22:56 |

Nik05 | I learned some haskell, so I like agda more than Coq | 11/06 22:56 |

mietek | indeed | 11/06 22:56 |

Nik05 | with all these tactics i have no idea what im even doing | 11/06 22:56 |

mietek | exactly | 11/06 22:56 |

mietek | that’s the de Bruijn criterion | 11/06 22:57 |

mietek | we want to have explicit proof objects that could be checked independently from the system | 11/06 22:57 |

mietek | while Coq forces you to write imperative scripts that operate on implicit (hidden) proof objects | 11/06 22:57 |

{AS} | Yeah, the latest Coq has a nice blend of cumulativity and universe polymorphism | 11/06 22:57 |

mietek | the latest Coq? or Idris? | 11/06 22:58 |

{AS} | I think the latest version of Coq is really good | 11/06 22:58 |

{AS} | Idris does only have cumulativity and simple universe polymorphism on top-level functions | 11/06 22:58 |

{AS} | has | 11/06 22:59 |

{AS} | I think that I would prefer to use Coq if I have to prove large systems | 11/06 22:59 |

{AS} | The automation there is much better than Agda | 11/06 22:59 |

{AS} | But I think I like Agda's style of interactive proving more when working with DTP | 11/06 23:01 |

{AS} | It is much nicer if you like correct by construction kind of proofs | 11/06 23:01 |

Nik05 | I dont really got anything to prove. I just started having an interest in logic and the Curry-Howard polymorphism | 11/06 23:02 |

Nik05 | With tactics I dont really see this polymorphism | 11/06 23:03 |

{AS} | Yeah, Agda and Idris would be much better for this as mietek mentioned | 11/06 23:04 |

mietek | (isomorphism) | 11/06 23:21 |

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