---

Step * of Lemma csm-ap-id-term

∀[Gamma:CubicalSet]. ∀[A:{Gamma ⊢ _}]. ∀[t:{Gamma ⊢ _:A}].  ((t)1(Gamma) = t ∈ {Gamma ⊢ _:A})
BY
{ (Auto THEN Symmetry THEN D -1 THEN EqTypeCD THEN Try (Trivial)) }

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

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

---

Latex:

---

Latex:
\mforall{}[Gamma:CubicalSet].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[t:\{Gamma  \mvdash{}  \_:A\}].    ((t)1(Gamma)  =  t)


By

---

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

---

Home Index