Step
*
of Lemma
presheaf-lambda_wf
No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[b:{X.A ⊢ _:B}].  ((λb) ∈ {X ⊢ _:ΠA B})
BY
{ (Auto THEN MemTypeCD) }
1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. b : {X.A ⊢ _:B}
⊢ (λb) ∈ I:cat-ob(C) ⟶ a:X(I) ⟶ ΠA B(a)
2
.....set predicate..... 
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. b : {X.A ⊢ _:B}
⊢ ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).  (((λb) I a a f) = ((λb) J f(a)) ∈ ΠA B(f(a)))
3
.....wf..... 
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. b : {X.A ⊢ _:B}
6. u : I:cat-ob(C) ⟶ a:X(I) ⟶ ΠA B(a)
⊢ istype(∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).  ((u I a a f) = (u J f(a)) ∈ ΠA B(f(a))))
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\}].
    ((\mlambda{}b)  \mmember{}  \{X  \mvdash{}  \_:\mPi{}A  B\})
By
Latex:
(Auto  THEN  MemTypeCD)
Home
Index