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 ⊢ _:ΠB})
BY
(Auto THEN MemTypeCD) }

1
1. SmallCategory
2. ps_context{j:l}(C)
3. {X ⊢ _}
4. {X.A ⊢ _}
5. {X.A ⊢ _:B}
⊢ b) ∈ I:cat-ob(C) ⟶ a:X(I) ⟶ ΠB(a)

2
.....set predicate..... 
1. SmallCategory
2. ps_context{j:l}(C)
3. {X ⊢ _}
4. {X.A ⊢ _}
5. {X.A ⊢ _:B}
⊢ ∀I,J:cat-ob(C). ∀f:cat-arrow(C) I. ∀a:X(I).  (((λb) f) ((λb) f(a)) ∈ ΠB(f(a)))

3
.....wf..... 
1. SmallCategory
2. ps_context{j:l}(C)
3. {X ⊢ _}
4. {X.A ⊢ _}
5. {X.A ⊢ _:B}
6. I:cat-ob(C) ⟶ a:X(I) ⟶ ΠB(a)
⊢ istype(∀I,J:cat-ob(C). ∀f:cat-arrow(C) I. ∀a:X(I).  ((u f) (u f(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