I'm reading Bart Jacobs. They have defined "CT-structures" to be a pair (B, T) where B is a category and T is a subset of Ob(B). A morphism between CT-structures (B, T) and (A, S) is basically a functor K: B → A such that X∈T implies K(X) ∈ S.

Is this definition used by anyone else? I think it makes sense (as a motivation of display map categories) but I don't see people using it.

I implwement dependent type theory.

Joined Sep 2021