---

Step * of Lemma pscm-presheaf-lambda

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[b:{X.A ⊢ _:B}]. ∀[H:ps_context{j:l}(C)].
∀[s:psc_map{j:l}(C; H; X)].
  (((λb))s = (λ(b)s+) ∈ {H ⊢ _:(ΠA B)s})
BY
{ (Intros
   THEN (PresheafTermEqual THENA Auto)
   THEN Fold `presheaf-term-at` 0
   THEN (RWO "pscm-ap-term-at pscm-ap-type-at" 0 THENA Auto)
   THEN (Assert (λb)((s)a) ∈ ΠA B((s)a) BY
               Auto)
   THEN RepUR ``presheaf-pi presheaf-pi-family`` -1
   THEN RepUR ``presheaf-pi presheaf-pi-family`` 0
   THEN (MemTypeHD (-1) THENA Auto)
   THEN EqTypeCD
   THEN Try (Trivial)
   THEN Try ((IsTypeD THEN Auto))
   THEN RepeatFor 2 (Thin (-1))) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. b : {X.A ⊢ _:B}
6. H : ps_context{j:l}(C)
7. s : psc_map{j:l}(C; H; X)
8. I : cat-ob(C)
9. a : H(I)
⊢ (λb)((s)a) = (λ(b)s+)(a) ∈ (J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A(f((s)a)) ⟶ B((f((s)a);u)))

---

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{}[H:ps\_context\{j:l\}(C)].  \mforall{}[s:psc\_map\{j:l\}(C;  H;  X)].
    (((\mlambda{}b))s  =  (\mlambda{}(b)s+))


By

---

Latex:
(Intros
  THEN  (PresheafTermEqual  THENA  Auto)
  THEN  Fold  `presheaf-term-at`  0
  THEN  (RWO  "pscm-ap-term-at  pscm-ap-type-at"  0  THENA  Auto)
  THEN  (Assert  (\mlambda{}b)((s)a)  \mmember{}  \mPi{}A  B((s)a)  BY
                          Auto)
  THEN  RepUR  ``presheaf-pi  presheaf-pi-family``  -1
  THEN  RepUR  ``presheaf-pi  presheaf-pi-family``  0
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  EqTypeCD
  THEN  Try  (Trivial)
  THEN  Try  ((IsTypeD  THEN  Auto))
  THEN  RepeatFor  2  (Thin  (-1)))

---

Home Index