joel135 joel135 --- Day changed Wed Jul 05 2017 Can 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 The purpose of that mess is to avoid mentioning natural numbers and lists. 05/07 21:42 that doesn't look right 05/07 21:47 it doesn't seem to imply transitivity properly 05/07 21:48 oh, wait, I see what you're doing 05/07 21:48 yes, I think that should work? 05/07 21:48 something like 05/07 21:50 connected 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 d 05/07 21:50 and if you assume that (E a b) implies (V a) and (V b), you can simplify that a bit 05/07 21:51 Very cool! 05/07 21:52 Can you construct a connected V E consisting of two nodes? 05/07 21:54 I assume so. why not try yourself? 05/07 21:54 hm, 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 ... no, every graph has a morphism to the unit graph 05/07 21:58 im dum 05/07 21:58 joel135: I think V = Bool; E a b = \top should work 05/07 21:58 Ok 05/07 21:59 oh, except V for you is a predicate, not a set 05/07 22:00 well, (V : Bool -> Set; V _ = \top) should work :P 05/07 22:01 :p 05/07 22:02 The first (forall ...) part is like saying that P is a graph homomorphism from (V, E) to (proposition, implies). 05/07 22:04 hm, yeah. 05/07 22:04 Can you write (proposition, implies) in agda? 05/07 22:04 yes. you have to be a bit finicky about Levels, but you can do it. 05/07 22:04 Ok 05/07 22:05 Thanks 05/07 22:07 hm, I *think* this does what you want?: https://gist.github.com/rntz/c0da26c83d028b8f677a430b31d92d40 05/07 22:07 "Functor" is misnamed, it should be "GraphHomomorphism", but w/e 05/07 22:08 Perfect 05/07 22:18 Do you use emacs to write agda code? 05/07 22:19 yes 05/07 22:33 Ok 05/07 22:33

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