---

Step * of Lemma csm-comp-structure-id

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[cA:Gamma ⊢ Compositon(A)]. ∀[tau:Gamma j⟶ Gamma].
  (cA)tau = cA ∈ Gamma ⊢ Compositon(A) supposing tau = 1(Gamma) ∈ Gamma j⟶ Gamma
BY
{ (Intros
   THEN Unhide
   THEN StrengthenEquation (-1)
   THEN (Assert (cA)tau = (cA)1(Gamma) ∈ Gamma ⊢ Compositon(A) BY
               (EquationFromHyp (-1)
                THEN (InferEqualTypeGen THEN Auto)
                THEN EqCDA
                THEN RepeatFor 2 (D -1)
                THEN RWO "-1" 0
                THEN Auto))
   THEN (Enough to prove (cA)1(Gamma) = cA ∈ Gamma ⊢ Compositon(A)
          Because Eq)
   THEN All Thin) }

1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. cA : Gamma ⊢ Compositon(A)
⊢ (cA)1(Gamma) = cA ∈ Gamma ⊢ Compositon(A)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[cA:Gamma  \mvdash{}  Compositon(A)].  \mforall{}[tau:Gamma  j{}\mrightarrow{}  Gamma].
    (cA)tau  =  cA  supposing  tau  =  1(Gamma)


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  StrengthenEquation  (-1)
  THEN  (Assert  (cA)tau  =  (cA)1(Gamma)  BY
                          (EquationFromHyp  (-1)
                            THEN  (InferEqualTypeGen  THEN  Auto)
                            THEN  EqCDA
                            THEN  RepeatFor  2  (D  -1)
                            THEN  RWO  "-1"  0
                            THEN  Auto))
  THEN  (Enough  to  prove  (cA)1(Gamma)  =  cA
                Because  Eq)
  THEN  All  Thin)

---

Home Index