---

Step * of Lemma pscm-adjoin-wf

No Annotations
∀[C:SmallCategory]. ∀[Gamma,Delta:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢' _}]. ∀[sigma:psc_map{j:l}(C; Delta; Gamma)].
∀[u:{Delta ⊢ _:(A)sigma}].
  ((sigma;u) ∈ psc_map{[i | j]:l}(C; Delta; Gamma.A))
BY
{ (Intros
   THEN Unhide
   THEN (InstLemma `psc-map-is` [⌜parm{i}⌝;⌜parm{i|j}⌝;⌜C⌝;⌜Delta⌝;⌜Gamma.A⌝]⋅
         THENA (Auto THEN (BLemma `psc-adjoin-wf` THENA Auto))
         )
   THEN RWO "-1" 0
   THEN Thin (-1)
   THEN (MemTypeCD THENW Auto)
   THEN RepUR ``pscm-adjoin`` 0
   THEN Auto) }

1
1. C : SmallCategory
2. Gamma : ps_context{j:l}(C)
3. Delta : ps_context{j:l}(C)
4. A : {Gamma ⊢' _}
5. sigma : psc_map{j:l}(C; Delta; Gamma)
6. u : {Delta ⊢ _:(A)sigma}
7. I : cat-ob(C)
8. J : cat-ob(C)
9. g : cat-arrow(C) J I
⊢ (λs.g(<(sigma)s, u I s>)) = (λs.<(sigma)g(s), u J g(s)>) ∈ (Delta(I) ⟶ Gamma.A(J))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[Gamma,Delta:ps\_context\{j:l\}(C)].  \mforall{}[A:\{Gamma  \mvdash{}'  \_\}].
\mforall{}[sigma:psc\_map\{j:l\}(C;  Delta;  Gamma)].  \mforall{}[u:\{Delta  \mvdash{}  \_:(A)sigma\}].
    ((sigma;u)  \mmember{}  psc\_map\{[i  |  j]:l\}(C;  Delta;  Gamma.A))


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  (InstLemma  `psc-map-is`  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}parm\{i|j\}\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}Delta\mkleeneclose{};\mkleeneopen{}Gamma.A\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  (BLemma  `psc-adjoin-wf`  THENA  Auto))
              )
  THEN  RWO  "-1"  0
  THEN  Thin  (-1)
  THEN  (MemTypeCD  THENW  Auto)
  THEN  RepUR  ``pscm-adjoin``  0
  THEN  Auto)

---

Home Index