Re: [HoTT] Definition of semantic composition in CCHM cubical type theory

[Simon Huber <hub...@gmail.com>]

Hi Jasper,

On Tue, Oct 24, 2017 at 6:10 AM,  <jas...@cs.washington.edu> wrote:
> 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]]ρ′ ?

You are right, this is not quite right and a typo--it should be:

  ρ' = (ρ s_j, j).

(ρ' should be an element of [[Γ, i : II]](I,j).)

Cheers,
Simon