Topological Category
A topological category is a Category that has "joint cartesian lifts" of all families.
Properties
Every topological category is univalent; see Joy of Cats 21.5, though I think this may require excluded middle.
A topological category is a Category that has "joint cartesian lifts" of all families.
Every topological category is univalent; see Joy of Cats 21.5, though I think this may require excluded middle.