Bartosz Milewski Category Theory Lectures → 3.1 Examples of categories, orders, monoids → Thick Categories #card #bidirectional →
#
>

Defines a proof-relevant relation

→
#
>

Becomes relevant in Homotopy Type Theory

→