Congruence in an Infinity Topos

A class of maps $\mathcal{K}\subseteq\mathcal{E}$ in an Infinity Topos is a congruence if it is:

• Closed under isomorphisms and compositions.
• Closed under colimits and finite limits (in the Arrow Category of $\mathcal{E}$).

If we think about the maps $E\to B$ as Bundles, then the first two conditions say that we have a subset of type families that contains all families equivalent to $\lambda x.\;\top$, and also is closed under Sigma Types.

The latter condition is a bit more mysterious, but makes more sense when viewed from the perspective of Logoi: in particular, it ensures that the inclusion $\mathcal{K}\to\mathcal{E}^{\to}$ is a Fully Faithful Morphism of Logoi.

Properties

• Every congruence satisfies 2-Out-Of-3 Property