Induction and recursion principles for the triple join

We show that the triple join satisfies symmetrical induction and recursion principles and prove that the recursion principle gives an equivalence of 0-groupoids. We use this in JoinAssoc.v to prove that the join is associative. Our approach parallels what is done in the two-variable case in Join/Core.v, especially starting with TriJoinRecData here and JoinRecData there. That case is much simpler, so should be read first.

ap_trijoin and ap_trijoin_transport

Functions send triangles to triangles.

This general result abstracts away the situation where J is TriJoin A B C, a is joinl a' for some a', jr is joinr : Join B C → J, jg is fun w ⇒ jglue a' w, and p is jglue b c. By working in this generality, we can do induction on p. This also allows us to inline the proof of triangle_v.

Functions send the canonical triangles in triple joins to triangles.

The induction principle for the triple join

A lemma that handles the path algebra in the final step.

An induction principle for the triple join. Note that the hypotheses are phrased completely in terms of the "constructors" of TriJoin A B C.

The recursion principle for the triple join, and many results about it

We'll bundle up the arguments into a record.

Beta rules for the recursion principle.

We're next going to define a map in the other direction. We do it via showing that TriJoinRecData is a 0-coherent 1-functor to Type. We'll later show that it is a 1-functor to 0-groupoids.

The triple join itself has canonical TriJoinRecData.

Combining these gives a function going in the opposite direction to trijoin_rec.

Under Funext, trijoin_rec and trijoin_rec_inv should be inverse equivalences. We'll avoid Funext and show that they are equivalences of 0-groupoids, where we choose the path structures carefully.

The graph structure on TriJoinRecData A B C P

The type of fillers for a triangular prism with five 2d faces abc, abc', k12, k13, k23.

The "identity" filler is slightly non-trivial, because the fillers for the squares, e.g. ab @ 1 = 1 @ ab, must be non-trivial.

The paths between elements of TriJoinRecData A B C P. Under Funext, this type will be equivalent to the identity type. But without Funext, this definition will be more useful.

We also define data for trijoin_rec that unbundles the first three components. This lets us talk about paths between two such when the first three components are definitionally equal. This is a common special case, and this set-up greatly simplifies a lot of path algebra in later proofs.

We can bundle and unbundle these types of data. For unbundling, we just handle TriJoinRecData for now.

The proof by induction that is easily available to us here is what saves work in more complicated contexts.

A tactic that helps us apply the previous result.

Using these paths, we can restate the beta rule for trijoin_rec. The statement using TriJoinRecPath' typechecks only because trijoin_rec computes definitionally on the path constructors.

We can upgrade this to an unprimed path. This says that trijoin_rec_inv is split surjective.

trijoin_rec_inv is an injective map between 0-groupoids

We begin with a general purpose lemma.

This lemma handles the path algebra in the last goal of the next result.

trijoin_rec_inv is essentially injective, as a map between 0-groupoids.

Lemmas and tactics about triangles and prisms

We now introduce several lemmas and tactics that will dispense with some routine goals. The idea is that a generic triangle can be assumed to be trivial on the first vertex, and a generic prism can be assumed to be the identity on the domain. In order to apply the triangle_ind and prism_ind lemmas that make this precise, we need to generalize various terms in the goal. This destructs a seven component term f, tries to generalize each piece evaluated appropriately, and clears all pieces. If called with a, b and c all valid terms, we expect all seven components to be generalized. But one can also call it with one of a, b and c a dummy value (e.g. _X_) that causes four of the generalize tactics to fail. In this case, four components will be simply cleared, and three will be generalized and cleared, so this applies when the goal only depends on three of the seven components.

Use this with f : TriJoinRecData A B C P, a : A, b : B, c : C.

Use this with f : TriJoinRecData A B C P. Two of the arguments a, b and c should be elements of A, B and C, respectively, and the third should be a dummy value (e.g. _X_) that causes the generalize tactic to fail. It applies to goals that only depend on the components of f involving just two of A, B and C.

The prism analog of the function triangle_ind from earlier in the file. To prove something about all prisms, it's enough to prove it for the "identity" prism. Note that we don't specialize to a prism concentrated on a single vertex, since sometimes we have to deal with a composite of two prisms.

Use this with f g : TriJoinRecData A B C P, h : TriJoinRecPath f g (so g is the *co*domain of h), a : A, b : B, c : C.

Use this with f g : TriJoinRecData A B C P, h : TriJoinRecPath f g (so g is the *co*domain of h). Two of the arguments a, b and c should be elements of A, B and C, respectively, and the third should be a dummy value (e.g. _X_) that causes the generalize tactic to fail. It applies to goals that only depend on the components of g and h involving just two of A, B and C. So it is dealing with one square face of the prism.

Use the WildCat library to organize things

We begin by showing that TriJoinRecData A B C P is a 0-groupoid, one piece at a time.

trijoinrecdata_0gpd A B C is a 1-functor from Type to ZeroGpd

It's a 1-functor that lands in ZeroGpd, and the morphisms of ZeroGpd are 0-functors, so it's easy to get confused about the levels. First we need to show that the induced map is a morphism in ZeroGpd, i.e. that it is a 0-functor.

trijoinrecdata_0gpd A B C is a 0-functor from Type to ZeroGpd (one level up).

trijoinrecdata_0gpd A B C is a 1-functor from Type to ZeroGpd.

By the Yoneda lemma, it follows from TriJoinRecData being a 1-functor that given TriJoinRecData in J, we get a map (J → P) $-> (TriJoinRecData A B C P) of 0-groupoids which is natural in P. Below we will specialize to the case where J is TriJoin A B C with the canonical TriJoinRecData.

Thus we get a map (TriJoin A B C → P) $-> (TriJoinRecData A B C P) of 0-groupoids, natural in P. The underlying map is trijoin_rec_inv A B C P.

This natural transformation is in fact a natural equivalence of 0-groupoids.

It will be handy to name the inverse natural equivalence.

trijoin_rec_natequiv A B C P is an equivalence of 0-groupoids whose underlying function is definitionally trijoin_rec.

It follows that trijoin_rec A B C P is a 0-functor.

And that trijoin_rec A B C is natural. The $== in the statement is just ==, but we use WildCat notation so that we can invert and compose these with WildCat notation.

It is also useful to record this.

This comes up a lot as well, and if you inline the proof, you get an ugly goal.

Functoriality of the triple join

Precomposition of TriJoinRecData

First observe that we can precompose k : TriJoinRecData with a triple of maps.