Cograph

cograph.agda

{-# OPTIONS --safe #-}
module Cograph where

open import Prelude

record Graph {A B : 𝒰} (f : A → B) : 𝒰 where
  field
    x : A
    y : B
    sub : f x ＝ y

open Graph public

data Cograph {A B : 𝒰} (f : A → B) : 𝒰 where
  arg : A → Cograph f
  res : B → Cograph f
  quo : ∀ {a b} → f a ＝ b → arg a ＝ res b

f : ℕ → Maybe ℕ
f n = just (2 + n)

foo : Graph f
foo .x   = 2
foo .y   = just 4
foo .sub = refl

bar : Cograph f
bar = arg 2

baz : Cograph f
baz = res (just 4)

quux : bar ＝ baz
quux = quo refl