--- Day changed Wed Jul 05 2017
joel135Can you write this in agda? For (V, E) to be a connected digraph means that for every "predicate" P such that (for all a, b. if V a, V b, E a b, P a then P b) and for all c, d. if V c, V d, P c then P d.05/07 21:38
joel135The purpose of that mess is to avoid mentioning natural numbers and lists.05/07 21:42
rntzthat doesn't look right05/07 21:47
rntzit doesn't seem to imply transitivity properly05/07 21:48
rntzoh, wait, I see what you're doing05/07 21:48
rntzyes, I think that should work?05/07 21:48
rntzsomething like05/07 21:50
rntzconnected V E = forall P -> (forall a b -> V a -> V b -> E a b -> P a -> P b) -> forall c d -> V c -> V d -> P c -> P d05/07 21:50
rntzand if you assume that (E a b) implies (V a) and (V b), you can simplify that a bit05/07 21:51
joel135Very cool!05/07 21:52
joel135Can you construct a connected V E consisting of two nodes?05/07 21:54
rntzI assume so. why not try yourself?05/07 21:54
rntzhm, is a digraph connected iff there's a morphism from it to the unit graph which has one node and one self-loop?05/07 21:57
rntz... no, every graph has a morphism to the unit graph05/07 21:58
rntzim dum05/07 21:58
rntzjoel135: I think V = Bool; E a b = \top should work05/07 21:58
joel135Ok05/07 21:59
rntzoh, except V for you is a predicate, not a set05/07 22:00
rntzwell, (V : Bool -> Set; V _ = \top) should work :P05/07 22:01
joel135:p05/07 22:02
joel135The first (forall ...) part is like saying that P is a graph homomorphism from (V, E) to (proposition, implies).05/07 22:04
rntzhm, yeah.05/07 22:04
joel135Can you write (proposition, implies) in agda?05/07 22:04
rntzyes. you have to be a bit finicky about Levels, but you can do it.05/07 22:04
joel135Ok05/07 22:05
joel135Thanks05/07 22:07
rntzhm, I *think* this does what you want?: https://gist.github.com/rntz/c0da26c83d028b8f677a430b31d92d4005/07 22:07
rntz"Functor" is misnamed, it should be "GraphHomomorphism", but w/e05/07 22:08
joel135Perfect05/07 22:18
joel135Do you use emacs to write agda code?05/07 22:19
rntzyes05/07 22:33
joel135Ok05/07 22:33

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