Data.Comp.Sum

type f :<: g

type f :=: g

data (f :+: g) e

Projections for Signatures and Terms

Injections for Signatures and Terms

Injections and Projections for Constants