# What is the intuition behind the Glue type in Cubical Type Theories

I have some clues regarding Glue based on a paper here and the accepted answer here.

The first resource says that Glue "glues together" a partial and total types along a partial equivalence between them. Hm, okay, let's carry on.

The second resource references the fact that Glue extends a partial Ξ£(π:π) (πβπ΅) to total one. This is in line with the fact that univalence, the theorem Glue was devised for, is itself equivalent to Ξ£(π:π) (πβπ΅) being contractible which is, AFAIU, equivalent (in the Cubical setting) to asking that every partial Ξ£(π:π) (πβπ΅) can be extended to a total one. The last condition seems to be very similar to what Glue does, but I still don't see the full picture. Also I don't understand the intuition behind elements of Glue, i.e. glue and elimination of Glue, i.e. unglue whatsoever.

• In CCHM section 6.1, they have the typing & computation rules for glue and unglue.
– ice1000
Commented Jan 3, 2023 at 18:08
• I understand the typing and computation rules. But that unfortunately doesn't help me with intuition... Commented Jan 3, 2023 at 20:55

I would say Glue types are the "in-between" part of a path equality. For instance, take the Booleans. We can construct a type $$\mathsf{Glue}^i_{\color{brown}{\mathbb B}}\begin{cases} (i=0) \Rightarrow \mathbb B, \color{blue}{\mathrm{id}}\\ (i=1) \Rightarrow \mathbb B, \color{red}{\mathrm{not}}. \end{cases}$$ The picture of this type goes roughly like this:

The reason that these lines can be drawn is that you provided a way to align all the parts to $$\mathbb B$$, the "anchor-type" at the bottom-right corner of $$\mathsf{Glue}_{\mathbb B}^i$$. The constructor $$\mathsf{glue}$$ creates the gray points by providing an element of the anchor type. The deconstructor does the opposite.

The blue arrows denote the equivalence $$\mathrm{id}$$, and the red arrows the equivalence $$\mathrm{not}$$. Therefore, $$\mathsf{glue}$$ will follow the arrows: $$\mathsf{glue}^i(\mathsf{true})$$ will give the line connecting the lower left and upper right, etc.

• What is a "part"? What does it mean to "align a part"? It seems to me that the total type πΉ (the argument of Glue located at the bottom) is not drawn in the picture. The left and right vertical lines in the picture are partial πΉ. What would be the two values inside glue that create the upper grey dot? What is the intuition behind those two values? Commented Jan 4, 2023 at 21:34
• @Russoul Updated.
– Trebor
Commented Jan 5, 2023 at 5:14
• id shall exist only when i = 0 and not only when i = 1. So I would expect the rectangles containing blue lines and red lines be perpendicular to the i axis. But they are not... I am confused. Commented Jan 5, 2023 at 14:52
• @Russoul They are triangles sticking into the third dimension. Unfortunately your screen is two dimensional, so I can't draw into that. Also, the arrows are not paths. They only signify a correspondence.
– Trebor
Commented Jan 5, 2023 at 18:04
• Additionally, the isomorphisms don't have i coordinates. They are not in the coordinate system at all, overseeing everything else. If there are i,j coordinates, then the anchor type would be the top of a pyramid, overseeing the square.
– Trebor
Commented Jan 5, 2023 at 18:09