--- Day changed Sun Jun 11 2017
Nik05thank you mietek :)11/06 00:00
joel135What's de Bruijn for λx. x λy. y — λ. 0 λ. 0 or λ. 1 λ. 0?11/06 10:30
adamsejoel135: the first one11/06 11:01
joel135ok good11/06 11:22
Nik05Why is Relation.Nullary called this way? Arent those Unary relations?11/06 22:04
Nik05mietek if I want to define a homogenous binary relation, does this type exists in Set_1?11/06 22:47
Nik05HomoRel A = A \to A \to Set11/06 22:49
mietekNik05: well, have you tried defining it?11/06 22:49
Nik05yes it doesnt let me :P11/06 22:49
mietekI don’t know why it is called that way.11/06 22:49
mietekshow your work11/06 22:49
Nik05well it does when the type is HomoRel : Set \to Set\_111/06 22:50
Nik05Set -> Set111/06 22:50
mietekso… what’s your question again? :)11/06 22:50
Nik05oh wait ofcourse it has to be in Set111/06 22:50
Nik05It was just, you said I dont need to take care of these set levels yet :P11/06 22:51
mietekI said Set1 will solve most of your issues11/06 22:51
Nik05oh oke11/06 22:51
Nik05sorry about that11/06 22:51
mietekno worries11/06 22:51
mietekI mean, it really depends what are you going to try 11/06 22:52
mietekif you’re going to want to have relations of relations next11/06 22:52
mietekyou’re going to need a bigger hammer11/06 22:52
Nik05Oké, I dont think I well reach those11/06 22:53
Nik05Also tried some Coq, and there this is all implicit11/06 22:54
mietekyou should try Idris11/06 22:54
Nik05Why?11/06 22:55
mietekit’s similar to Agda, unlike Coq11/06 22:55
mietekand it has universe cumulativity11/06 22:55
mietekso you never have to think about universe levels — I think. {AS} would know more11/06 22:55
mietekI’m not a huge fan of Coq11/06 22:56
mietekbut YMMV11/06 22:56
mietekAgda and Idris have the de Bruijn criterion11/06 22:56
Nik05I learned some haskell, so I like agda more than Coq11/06 22:56
mietekindeed11/06 22:56
Nik05with all these tactics i have no idea what im even doing11/06 22:56
mietekexactly11/06 22:56
mietekthat’s the de Bruijn criterion11/06 22:57
mietekwe want to have explicit proof objects that could be checked independently from the system11/06 22:57
mietekwhile Coq forces you to write imperative scripts that operate on implicit (hidden) proof objects11/06 22:57
{AS}Yeah, the latest Coq has a nice blend of cumulativity and universe polymorphism11/06 22:57
mietekthe latest Coq? or Idris?11/06 22:58
{AS}I think the latest version of Coq is really good11/06 22:58
{AS}Idris does only have cumulativity and simple universe polymorphism on top-level functions11/06 22:58
{AS}has11/06 22:59
{AS}I think that I would prefer to use Coq if I have to prove large systems11/06 22:59
{AS}The automation there is much better than Agda11/06 22:59
{AS}But I think I like Agda's style of interactive proving more when working with DTP11/06 23:01
{AS}It is much nicer if you like correct by construction kind of proofs11/06 23:01
Nik05I dont really got anything to prove. I just started having an interest in logic and the Curry-Howard polymorphism11/06 23:02
Nik05With tactics I dont really see this polymorphism11/06 23:03
{AS}Yeah, Agda and Idris would be much better for this as mietek mentioned11/06 23:04
mietek(isomorphism)11/06 23:21

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