---

Step * of Lemma cc-snd-csm-adjoin

∀[Gamma,Delta:CubicalSet]. ∀[A:{Gamma ⊢ _}]. ∀[sigma:Delta ⟶ Gamma]. ∀[u:{Delta ⊢ _:(A)sigma}].
  ((q)(sigma;u) = u ∈ {Delta ⊢ _:(A)sigma})
BY
{ (Auto THEN Symmetry THEN D -1 THEN EqTypeCD THEN Try (Trivial)) }

1
1. Gamma : CubicalSet
2. Delta : CubicalSet
3. A : {Gamma ⊢ _}
4. sigma : Delta ⟶ Gamma
5. u : I:(Cname List) ⟶ a:Delta(I) ⟶ ((fst((A)sigma)) I a)
6. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:Delta(I).
     let A,F = (A)sigma 
     in (F I J f a (u I a)) = (u J f(a)) ∈ (A J f(a))
⊢ u = (q)(sigma;u) ∈ (I:(Cname List) ⟶ a:Delta(I) ⟶ ((fst((A)sigma)) I a))

2
.....wf..... 
1. Gamma : CubicalSet
2. Delta : CubicalSet
3. A : {Gamma ⊢ _}
4. sigma : Delta ⟶ Gamma
5. u : I:(Cname List) ⟶ a:Delta(I) ⟶ ((fst((A)sigma)) I a)
6. ∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:Delta(I).
     let A,F = (A)sigma 
     in (F I J f a (u I a)) = (u J f(a)) ∈ (A J f(a))
7. u1 : I:(Cname List) ⟶ a:Delta(I) ⟶ ((fst((A)sigma)) I a)
⊢ istype(∀I,J:Cname List. ∀f:name-morph(I;J). ∀a:Delta(I).
           let A,F = (A)sigma 
           in (F I J f a (u1 I a)) = (u1 J f(a)) ∈ (A J f(a)))

---

Latex:

---

Latex:
\mforall{}[Gamma,Delta:CubicalSet].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[sigma:Delta  {}\mrightarrow{}  Gamma].  \mforall{}[u:\{Delta  \mvdash{}  \_:(A)sigma\}].
    ((q)(sigma;u)  =  u)


By

---

Latex:
(Auto  THEN  Symmetry  THEN  D  -1  THEN  EqTypeCD  THEN  Try  (Trivial))

---

Home Index