Step
*
1
1
of Lemma
presheaf-elements_wf
.....subterm..... T:t
3:n
1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
3. Aa : A:cat-ob(op-cat(C)) × (P A)
⊢ cat-id(op-cat(C)) (fst(Aa)) ∈ let A,a = Aa
in let B,b = Aa
in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)}
BY
{ (D -1 THEN Reduce 0) }
1
1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
3. A : cat-ob(op-cat(C))
4. A1 : P A
⊢ cat-id(op-cat(C)) A ∈ {f:cat-arrow(op-cat(C)) A A| (P A A f A1) = A1 ∈ (P A)}
Latex:
Latex:
.....subterm..... T:t
3:n
1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
3. Aa : A:cat-ob(op-cat(C)) \mtimes{} (P A)
\mvdash{} cat-id(op-cat(C)) (fst(Aa)) \mmember{} let A,a = Aa
in let B,b = Aa
in \{f:cat-arrow(op-cat(C)) B A| (P B A f b) = a\}
By
Latex:
(D -1 THEN Reduce 0)
Home
Index