Module arrow

open_hypergraphs::finite_function

Module arrow 

Source

Structs§

FiniteFunction
A finite function is an array of indices in a range {0..N} for some N ∈ Nat

Functions§

coequalizer_universal
Compute the universal map for a coequalizer q : B → Q and arrow f : B → T, generalised to the case where T is an arbitrary set (i.e., f is an array of T)