--- Day changed Wed Jul 05 2017 | ||

joel135 | 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 |
---|---|---|

joel135 | The purpose of that mess is to avoid mentioning natural numbers and lists. | 05/07 21:42 |

rntz | that doesn't look right | 05/07 21:47 |

rntz | it doesn't seem to imply transitivity properly | 05/07 21:48 |

rntz | oh, wait, I see what you're doing | 05/07 21:48 |

rntz | yes, I think that should work? | 05/07 21:48 |

rntz | something like | 05/07 21:50 |

rntz | 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 |

rntz | and if you assume that (E a b) implies (V a) and (V b), you can simplify that a bit | 05/07 21:51 |

joel135 | Very cool! | 05/07 21:52 |

joel135 | Can you construct a connected V E consisting of two nodes? | 05/07 21:54 |

rntz | I assume so. why not try yourself? | 05/07 21:54 |

rntz | 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 |

rntz | ... no, every graph has a morphism to the unit graph | 05/07 21:58 |

rntz | im dum | 05/07 21:58 |

rntz | joel135: I think V = Bool; E a b = \top should work | 05/07 21:58 |

joel135 | Ok | 05/07 21:59 |

rntz | oh, except V for you is a predicate, not a set | 05/07 22:00 |

rntz | well, (V : Bool -> Set; V _ = \top) should work :P | 05/07 22:01 |

joel135 | :p | 05/07 22:02 |

joel135 | The first (forall ...) part is like saying that P is a graph homomorphism from (V, E) to (proposition, implies). | 05/07 22:04 |

rntz | hm, yeah. | 05/07 22:04 |

joel135 | Can you write (proposition, implies) in agda? | 05/07 22:04 |

rntz | yes. you have to be a bit finicky about Levels, but you can do it. | 05/07 22:04 |

joel135 | Ok | 05/07 22:05 |

joel135 | Thanks | 05/07 22:07 |

rntz | hm, I *think* this does what you want?: https://gist.github.com/rntz/c0da26c83d028b8f677a430b31d92d40 | 05/07 22:07 |

rntz | "Functor" is misnamed, it should be "GraphHomomorphism", but w/e | 05/07 22:08 |

joel135 | Perfect | 05/07 22:18 |

joel135 | Do you use emacs to write agda code? | 05/07 22:19 |

rntz | yes | 05/07 22:33 |

joel135 | Ok | 05/07 22:33 |

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