9
$\begingroup$

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.

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

1 Answer 1

Reset to default
4
$\begingroup$

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:

1 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.

Improve this answer
$\endgroup$
7
  • 1
    $\begingroup$ 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? $\endgroup$
    – Russoul
    Commented Jan 4, 2023 at 21:34
  • $\begingroup$ @Russoul Updated. $\endgroup$
    – Trebor ♦
    Commented Jan 5, 2023 at 5:14
  • 1
    $\begingroup$ 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. $\endgroup$
    – Russoul
    Commented Jan 5, 2023 at 14:52
  • $\begingroup$ @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. $\endgroup$
    – Trebor ♦
    Commented Jan 5, 2023 at 18:04
  • 1
    $\begingroup$ 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. $\endgroup$
    – Trebor ♦
    Commented Jan 5, 2023 at 18:09

Not the answer you're looking for? Browse other questions tagged or ask your own question.