---

Step * of Lemma csm-ap-id-type

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

1
1. Gamma : CubicalSet
2. A : A:I:(Cname List) ⟶ Gamma(I) ⟶ Type × (I:(Cname List)
                                              ⟶ J:(Cname List)
                                              ⟶ f:name-morph(I;J)
                                              ⟶ a:Gamma(I)
                                              ⟶ (A I a)
                                              ⟶ (A J f(a)))
3. let A,F = A 
   in (∀I:Cname List. ∀a:Gamma(I). ∀u:A I a.  ((F I I 1 a u) = u ∈ (A I a)))
      ∧ (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K). ∀a:Gamma(I). ∀u:A I a.
           ((F I K (f o g) a u) = (F J K g f(a) (F I J f a u)) ∈ (A K (f o g)(a))))
⊢ A
= (A)1(Gamma)
∈ (A:I:(Cname List) ⟶ Gamma(I) ⟶ Type × (I:(Cname List)
                                          ⟶ J:(Cname List)
                                          ⟶ f:name-morph(I;J)
                                          ⟶ a:Gamma(I)
                                          ⟶ (A I a)
                                          ⟶ (A J f(a))))

---

Latex:

---

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


By

---

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

---

Home Index