Documentation

Mathlib.CategoryTheory.Sites.Coherent.Equivalence

Coherence and equivalence of categories #

This file proves that the coherent and regular topologies transfer nicely along equivalences of categories.