---

Step * 2 of Lemma sigma-unelim-pscm_wf

.....subterm..... T:t
2:n
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. I : cat-ob(C)
6. J : cat-ob(C)
7. g : cat-arrow(C) J I
8. a1 : X(I)
9. a2 : A(a1)
10. x1 : B(<a1, a2>)
⊢ ((a2;x1) a1 g) = ((a2 a1 g);(x1 <a1, a2> g)) ∈ Σ A B(g(a1))
BY
{ (RepUR ``presheaf-sigma psc-adjoin-set`` 0
   THEN EqCD
   THEN Try (Fold `psc-adjoin-set` 0)
   THEN Try (Fold `psc-adjoin-set` (-1))
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  A  :  \{X  \mvdash{}  \_\}
4.  B  :  \{X.A  \mvdash{}  \_\}
5.  I  :  cat-ob(C)
6.  J  :  cat-ob(C)
7.  g  :  cat-arrow(C)  J  I
8.  a1  :  X(I)
9.  a2  :  A(a1)
10.  x1  :  B(<a1,  a2>)
\mvdash{}  ((a2;x1)  a1  g)  =  ((a2  a1  g);(x1  <a1,  a2>  g))


By

---

Latex:
(RepUR  ``presheaf-sigma  psc-adjoin-set``  0
  THEN  EqCD
  THEN  Try  (Fold  `psc-adjoin-set`  0)
  THEN  Try  (Fold  `psc-adjoin-set`  (-1))
  THEN  Auto)

---

Home Index