Definition of semantic composition in CCHM cubical type theory

[jas...@cs.washington.edu]

[-- Attachment #1.1: Type: text/plain, Size: 2832 bytes --]

Hello,

I've been reading through Cubical Type Theory: a constructive 
interpretation of the univalence axiom 
<https://arxiv.org/pdf/1611.02108.pdf>, 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.


[-- Attachment #1.2: Type: text/html, Size: 3177 bytes --]