---

Step * of Lemma presheaf-fst_wf

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[p:{X ⊢ _:Σ A B}].  (p.1 ∈ {X ⊢ _:A})
BY
{ (ProveWfLemma THEN D -1 THEN MemTypeCD THEN Reduce 0) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. p : I:cat-ob(C) ⟶ a:X(I) ⟶ Σ A B(a)
6. ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).  ((p I a a f) = (p J f(a)) ∈ Σ A B(f(a)))
⊢ λI,a. (fst((p I a))) ∈ I:cat-ob(C) ⟶ a:X(I) ⟶ A(a)

2
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. p : I:cat-ob(C) ⟶ a:X(I) ⟶ Σ A B(a)
6. ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).  ((p I a a f) = (p J f(a)) ∈ Σ A B(f(a)))
⊢ ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).  ((fst((p I a)) a f) = (fst((p J f(a)))) ∈ A(f(a)))

3
.....wf..... 
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. p : I:cat-ob(C) ⟶ a:X(I) ⟶ Σ A B(a)
6. ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).  ((p I a a f) = (p J f(a)) ∈ Σ A B(f(a)))
7. u : I:cat-ob(C) ⟶ a:X(I) ⟶ A(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(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{}[p:\{X  \mvdash{}  \_:\mSigma{}  A  B\}].
    (p.1  \mmember{}  \{X  \mvdash{}  \_:A\})


By

---

Latex:
(ProveWfLemma  THEN  D  -1  THEN  MemTypeCD  THEN  Reduce  0)

---

Home Index