--- Day changed Fri Aug 11 2017
apostolisI made this question a while ago, but this problem once more occured in my code. I want to prove that any two negations are equal.11/08 00:42
apostolisThis seems to require function extentionality.11/08 00:42
apostolisIs there another way or a tutorial to cubical type theory in agda?11/08 00:43
mietekSaizan_: ^^11/08 01:05
apostolismietek : I am the only european that does not sleep :)11/08 01:18
mieteknope11/08 01:18
mietekalthough the UK barely counts as Europe these days…11/08 01:19
apostolislol11/08 01:19
SrPxWhat exactly is the difference between having an universe of types, and just having Set : Box (one level far)?11/08 05:24
rntzhm. I want to define a type of "monotonically increasing streams", but there doesn't seem to be a way to do this without indirection: http://sprunge.us/hSPU11/08 17:55
joel135rntz: Maybe something like this? P : Stream -> Set, x : Stream, P x, ((x' : Stream and P x') -> (head x' ≤ head (tail x') and P (tail x')))11/08 21:30
adamserntz: http://lpaste.net/92916974589313024011/08 21:50
adamsesimilar to your awkward one11/08 21:51
adamsebut maybe a bit less awkward11/08 21:53
rntzadamse: hm, interesting! I like that because although <=Chain is needed for the definition, it can be forgotten about afterward11/08 22:05
rntzjoel135: I don't understand your notation.11/08 22:05
rntzI can define streams, and then separately define the property of being monotonically increasing, which seems to be what you're getting at11/08 22:06
rntzbut I was looking for a way to define it all-in-one-pass11/08 22:07
joel135Ok11/08 22:07

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