adding equalizers and coequalizers to a cartesian closed category amounts to enriching the corresponding type system with refinement types and quotient types respectively.