Re: [HoTT] Canonical forms for initiality

[Michael Shulman <shu...@sandiego.edu>]

On Tue, Oct 17, 2017 at 12:33 AM, Andrea Vezzosi <sanz...@gmail.com> wrote:
> This is interesting but I can't quite see it, what would be the type
> of the "graph of associativity" judgment?

So there is a judgment for context morphisms

σ : Γ -> Δ

and a judgment for composites thereof (2-simplices)

s : σ2 ∘ σ1 = σ3

then one for the graph of hereditary substitution:

tσ : t1 [ σ ] = t2

and then for "associativity", or I suppose better "functoriality" of
that, which is a 2-simplex of some (semi-)simplicial set lying over
the (semi-)simplicial set of contexts and context morphisms:

ts : tσ2 ∘ tσ1 =( s ) tσ3

where

tσ1 : t1 [ σ1 ] = t2
tσ2 : t2 [ σ2 ] = t3
tσ3 : t1 [ σ3 ] = t3
s : σ2 ∘ σ1 = σ3

and so on

> And how would you use it in the term/type judgments?

In an intrinsic presentation of dependent type theory, the rules for
variables are kind of forced to be de Bruijn, with something like

------------------------------
(Γ , A) ⊢ pop : A [ πA ]

Γ ⊢ t : B
------------------------------
(Γ , A) ⊢ shift t : B [ πA ]

where π : (Γ , A) -> Γ is the weakening context morphism.  When you
try to define hereditary substitution into these, I think you end up
having to compose context morphisms, and then when you try to prove
functoriality for substitutions into these, you end up having to talk
about 3-simplices, and so on.