Step
*
of Lemma
csm-adjoin_wf
∀[Gamma,Delta:CubicalSet]. ∀[A:{Gamma ⊢ _}]. ∀[sigma:Delta ⟶ Gamma]. ∀[u:{Delta ⊢ _:(A)sigma}].
((sigma;u) ∈ Delta ⟶ Gamma.A)
BY
{ (Auto THEN (RWO "cube-set-map-is" 0 THENA Auto) THEN MemTypeCD THEN Auto THEN RepUR ``csm-adjoin`` 0 THEN Auto) }
1
1. Gamma : CubicalSet
2. Delta : CubicalSet
3. A : {Gamma ⊢ _}
4. sigma : Delta ⟶ Gamma
5. u : {Delta ⊢ _:(A)sigma}
6. I : Cname List
7. a : Delta(I)
⊢ <(sigma)a, u I a> ∈ Gamma.A(I)
2
1. Gamma : CubicalSet
2. Delta : CubicalSet
3. A : {Gamma ⊢ _}
4. sigma : Delta ⟶ Gamma
5. u : {Delta ⊢ _:(A)sigma}
6. I : Cname List
7. J : Cname List
8. g : name-morph(I;J)
⊢ (λs.g(<(sigma)s, u I s>)) = (λs.<(sigma)g(s), u J g(s)>) ∈ (Delta(I) ⟶ Gamma.A(J))
Latex:
Latex:
\mforall{}[Gamma,Delta:CubicalSet]. \mforall{}[A:\{Gamma \mvdash{} \_\}]. \mforall{}[sigma:Delta {}\mrightarrow{} Gamma]. \mforall{}[u:\{Delta \mvdash{} \_:(A)sigma\}].
((sigma;u) \mmember{} Delta {}\mrightarrow{} Gamma.A)
By
Latex:
(Auto
THEN (RWO "cube-set-map-is" 0 THENA Auto)
THEN MemTypeCD
THEN Auto
THEN RepUR ``csm-adjoin`` 0
THEN Auto)
Home
Index