---

Step * of Lemma presheaf-beta

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[b:{X.A ⊢ _:B}]. ∀[u:{X ⊢ _:A}].
  (app((λb); u) = (b)[u] ∈ {X ⊢ _:(B)[u]})
BY
{ (Auto
   THEN Symmetry
   THEN UsingVars [`X'] (BLemma `presheaf-term-equal`)
   THEN Auto
   THEN RepeatFor 2 ((Ext THENA Auto))
   THEN RenameVar `I' (-2)
   THEN RenameVar `a' (-1)
   THEN RepUR ``presheaf-app presheaf-lambda presheaf-pi psc-fst psc-snd pscm-ap-term pscm-ap`` 0
   THEN DVar `b'
   THEN DVar `u'
   THEN RepUR ``pscm-id-adjoin pscm-adjoin pscm-id pscm-ap identity-trans type-cat`` 0
   THEN Fold `psc-adjoin-set` 0
   THEN (GenConclTerm ⌜u I a⌝⋅ THENA Auto)) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. b : I:cat-ob(C) ⟶ a:X.A(I) ⟶ B(a)
6. ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X.A(I).  ((b I a a f) = (b J f(a)) ∈ B(f(a)))
7. u : I:cat-ob(C) ⟶ a:X(I) ⟶ A(a)
8. ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).  ((u I a a f) = (u J f(a)) ∈ A(f(a)))
9. I : cat-ob(C)
10. a : X(I)
11. v : A(a)
12. (u I a) = v ∈ A(a)
⊢ (b I (a;v)) = (b I (cat-id(C) I(a);v)) ∈ B((a;v))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[B:\{X.A  \mvdash{}  \_\}].  \mforall{}[b:\{X.A  \mvdash{}  \_:B\}].
\mforall{}[u:\{X  \mvdash{}  \_:A\}].
    (app((\mlambda{}b);  u)  =  (b)[u])


By

---

Latex:
(Auto
  THEN  Symmetry
  THEN  UsingVars  [`X']  (BLemma  `presheaf-term-equal`)
  THEN  Auto
  THEN  RepeatFor  2  ((Ext  THENA  Auto))
  THEN  RenameVar  `I'  (-2)
  THEN  RenameVar  `a'  (-1)
  THEN  RepUR  ``presheaf-app  presheaf-lambda  presheaf-pi  psc-fst  psc-snd  pscm-ap-term  pscm-ap``  0
  THEN  DVar  `b'
  THEN  DVar  `u'
  THEN  RepUR  ``pscm-id-adjoin  pscm-adjoin  pscm-id  pscm-ap  identity-trans  type-cat``  0
  THEN  Fold  `psc-adjoin-set`  0
  THEN  (GenConclTerm  \mkleeneopen{}u  I  a\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index