math.CT — Category Theory
Isomorphism Loci and Coherence in Equivalence Extension
We study the restriction data carried by dependent-product extension along a monomorphism. In a locally cartesian closed category, the extended map is an isomorphism after a change of base if and only if the input map is an isomorphism on the restricted base. In a topos, its isomorphism locus is therefore the universal quantification of the input locus. A terminal characterization gives coherent comparisons for base change and successive extension, together with formulas for intersections and unions. Under explicit homotopical, cartesian, and universe hypotheses, this construction gives equivalence extension and preserves the boundary identifications used to prove fibrancy of a universe. Graph comparisons and strict fillers of a fixed universe boundary are represented by trivially fibrant objects. A single realignment over the comparison object induces a weak equivalence between these parameter objects, and both admit extensions of every finite cubical boundary. A finite-groupoid example shows that graph comparisons cannot be selected naturally under all isomorphisms of unstructured input.