I've been reading through Cubical Type Theory: a constructive interpretation of the univalence axiom, trying to understand the model constructed there.

I got confused about a few details, and I hoped someone on this list could help clarify them.

The semantic composition structure (p.19) takes as an argument ρ ∈ Γ(I, i). For f : J → I (a map I to dM(J)) and fresh j, we have restrictions using ρ(f, i = j), which I am reading as the restriction of ρ along g : J, j -> I, i (a map I, i to dm(J, j)) that takes I by f (with the inclusion of dM(J) into dM(J, j)) and takes i to j in dM(J, j). That part I think I can follow.

Then down in the interpretation from syntax (bottom of p.22, top of p.23), we define the interpretation of comp as

[[Γ; comp i A [ϕ → u] a0]]ρ = comp El [[Γ,i:II;A]] (I, j, ρ′ , [[Γ; ϕ]]ρ, [[Γ, ϕ, i: II; u]]ρ′ , [[Γ; a0]]ρ)

using ρ′ = (ρ s_j , i = j), supposedly in Γ(I, j). We have ρ ∈ [[Γ]](I) and  s_j : I, j → I is the inclusion.

I don't understand how to read ρ′ = (ρ s_j , i = j). Where does i come from, and what does it mean to set ρ′ to be a pair of ρ s_j and the substitution i = j? I think, we have El [[Γ,i:II;A]] in Ty([[Γ,i:II]]), so we expect ρ′ in [[Γ,i:II]](I, i), so ρ′ is a pair of [[Γ]](I, i) and II(I, i), so i guess we have ρ s_j in [[Γ]](I, i) and i = j in II(I, i)?

As I was writing this I think I made some progress, but I still don't understand what it means to have  i = j in II(I, i).

Does it have anything to do with the other place ρ′  is used, in [[Γ, ϕ, i: II; u]]ρ′ ?

Thanks in advance for any clarification,

- Jasper Hugunin

p.s. I've been studying the CCHM model with an eye towards giving the comp operation a (hopefully fibrant) type. The only place I've seen (semantic) comp used is in the translation from syntax, which would mean that ρ always has the form (ρ s_j , i = j), and so possibly we could replace comp with something like "a composition structure for A in Ty(Γ . II) is, for all I and ρ in Γ(I) (which looks like a cubical type) ... (with ρ replaced with (ρ s_j , i = j) in the body).

I'm still just taking stabs in the dark in the area of model theory, so any thoughts on the feasibility of this would also be appreciated (if it isn't obviously ridiculous).

The hope being that we could then define operations like fill and contr inside the theory, and possibly making progress towards a higher-inductive-recursive universe in the style of https://homotopytypetheory.org/2014/06/08/hiru-tdd/.

I don't understand Glue types very well, and they seem to be the most complicated part of the system, so I've been pondering ways to do without them.