Quotient of a graph

Definition

The quotient of a graph is one of the simplest HITs that can be found in HoTT. It consists of a base type and a relation on it, and for every witness of a relation between two points of the type, a path. We use graph quotients to build up all our other non-recursive HITs. Their simplicity means that we can easily prove results about them and generalise them to other HITs.

Above we did a match with output type a function, and then outside of the match we provided the argument gqglue'. If we instead end with | gq a ⇒ gq' a end., the definition will not depend on gqglue', which would be incorrect. This is the idiom referred to in ../../test/bugs/github1758.v and github1759.v.

Descent

We study "equifibrant" type families over a graph A, with edges indexed by R. By univalence, the descent property tells us that these type families correspond to type families over the graph quotient, and we obtain an induction principle for such type families. Dependent descent data over some particular descent data are "equifibrant" type families over this descent data. The "equifibrancy" is only taken over the graph A and R, but there is an extra level of dependency coming from the descent data. In this case, we obtain an induction and recursion principle, but only with a computation rule for the recursion principle. The theory of descent is interesting to consider in itself. However, we will use it as a means to structure the code, and to obtain induction and recursion principles that are valuable in proving the flattening lemma, and characterizing path spaces. Thus we will gloss over the bigger picture, and not consider equivalences of descent data, nor homotopies of their sections. We will also not elaborate on uniqueness of the induced families. It's possible to prove the results in the Descent, Flattening and Paths Sections without univalence, by replacing all equivalences with paths, but in practice these results will be used with equivalences as input, making the form below more convenient. See https://github.com/HoTT/Coq-HoTT/pull/2147issuecomment-2521570830 for further information.

Descent data over a graph A and R is an "equifibrant" or "cartesian" type family gqd_fam : A → Type. If a b : A are related by r : R a b, then the fibers gqd_fam a and gqd_fam b are equivalent, witnessed by gqd_e.

Let A and R be a graph.

Descent data induces a type family over GraphQuotient R.

A type family over GraphQuotient R induces descent data.

Transporting over fam_gqdescent along gqglue r is given by gqd_e.

A section on the descent data is a fiberwise section that respects the equivalences.

A descent section induces a genuine section of fam_gqdescent Pe.

We record its computation rule

Dependent descent data over descent data Pe : gqDescent R consists of a type family gqdd_fam : ∀ (a : A), gqd_fam Pe a → Type together with coherences gqdd_e r pa.

A dependent type family over fam_gqdescent Pe induces dependent descent data over Pe.

Dependent descent data over Pe induces a dependent type family over fam_gqdescent Pe.

A section of dependent descent data Qe : gqDepDescent Pe is a fiberwise section gqdds_sect, together with coherences gqdd_e.

A dependent descent section induces a genuine section over the total space of fam_gqdescent Pe.

The data for a section into a constant type family.

The data for a section of a constant family induces a section over the total space of fam_gqdescent Pe.

Here is the computation rule on paths.

The flattening lemma

We saw above that given descent data Pe over a graph A and R we obtained a type family fam_gqdescent Pe over the graph quotient. The flattening lemma describes the total space sig (fam_gqdescent Pe) of this type family as a graph quotient of sig (gqd_fam Pe) by a certain relation. This follows from the work above, which shows that sig (fam_gqdescent Pe) has the same universal property as this graph quotient.

We mimic the constructors of GraphQuotient for the total space. Here is the point constructor, in curried form.

And here is the path constructor.

Now that we've shown that fam_gqdescent Pe acts like a GraphQuotient of sig (gqd_fam Pe) by an appropriate relation, we can use this to prove the flattening lemma. The maps back and forth are very easy so this could almost be a formal consequence of the induction principle.

Characterization of path spaces

A pointed type family over a graph quotient has an identity system structure precisely when its associated descent data satisfies Kraus and von Raumer's induction principle, https://arxiv.org/pdf/1901.06022.

Let A and R be a graph, with a distinguished point a0 : A. Let Pe : gqDescent R be descent data over A and R with a distinguished point p0 : gqd_fam Pe a0. Assume that any dependent descent data Qe : gqDepDescent Pe with a distinguished point q0 : gqdd_fam Qe a0 p0 has a section that respects the distinguished points. This is the induction principle provided by Kraus and von Raumer.

Under these hypotheses, we get an identity system structure on fam_gqdescent Pe.

It follows that the fibers fam_gqdescent Pe x are equivalent to path spaces (gq a0) = x.

Functoriality of graph quotients

Equivalence of graph quotients