graph-connectedness.agda

open import Data.Product
open import Data.Unit
open import Level

record Graph i j : Set (suc (i ⊔ j)) where
  field node : Set i
  field edge : (a b : node) -> Set j

open Graph public

record Functor {i j k l} (A : Graph i j) (B : Graph k l) : Set (i ⊔ j ⊔ k ⊔ l) where
  field ap : node A -> node B
  field cov : ∀{a b} -> edge A a b -> edge B (ap a) (ap b)

open Functor public

-- the graph with one edge with a self-edge
unit : Graph _ _
node unit = ⊤
edge unit a b = ⊤

-- the graph where nodes are Sets and edges are functions
sets : Graph _ _
node sets = Set
edge sets a b = a -> b

connected : ∀{i j} -> Graph i j -> Set _
connected G = ∀ (P : Functor G sets) (a b : node G) -> ap P a -> ap P b