---

Step * 1 3 of Lemma presheaf-elements_wf


1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
⊢ ∀Aa,Bb:A:cat-ob(op-cat(C)) × (P A). ∀f:let A,a = Aa 
                                         in let B,b = Bb 
                                            in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} .
    (((cat-comp(op-cat(C)) (fst(Bb)) (fst(Aa)) (fst(Aa)) f (cat-id(op-cat(C)) (fst(Aa))))
    = f
    ∈ let A,a = Aa 
      in let B,b = Bb 
         in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} )
    ∧ ((cat-comp(op-cat(C)) (fst(Bb)) (fst(Bb)) (fst(Aa)) (cat-id(op-cat(C)) (fst(Bb))) f)
      = f
      ∈ let A,a = Aa 
        in let B,b = Bb 
           in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} ))
BY
{ (RepeatFor 2 (((D 0 THENA Auto) THEN 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
5. A2 : cat-ob(op-cat(C))
6. B1 : P A2
⊢ ∀f:{f:cat-arrow(op-cat(C)) A2 A| (P A2 A f B1) = A1 ∈ (P A)} 
    (((cat-comp(op-cat(C)) A2 A A f (cat-id(op-cat(C)) A))
    = f
    ∈ {f:cat-arrow(op-cat(C)) A2 A| (P A2 A f B1) = A1 ∈ (P A)} )
    ∧ ((cat-comp(op-cat(C)) A2 A2 A (cat-id(op-cat(C)) A2) f)
      = f
      ∈ {f:cat-arrow(op-cat(C)) A2 A| (P A2 A f B1) = A1 ∈ (P A)} ))

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  P  :  Functor(op-cat(C);TypeCat)
\mvdash{}  \mforall{}Aa,Bb:A:cat-ob(op-cat(C))  \mtimes{}  (P  A).  \mforall{}f:let  A,a  =  Aa 
                                                                                  in  let  B,b  =  Bb 
                                                                                        in  \{f:cat-arrow(op-cat(C))  B  A|  (P  B  A  f  b)  =  a\}  .
        (((cat-comp(op-cat(C))  (fst(Bb))  (fst(Aa))  (fst(Aa))  f  (cat-id(op-cat(C))  (fst(Aa))))  =  f)
        \mwedge{}  ((cat-comp(op-cat(C))  (fst(Bb))  (fst(Bb))  (fst(Aa))  (cat-id(op-cat(C))  (fst(Bb)))  f)  =  f))


By

---

Latex:
(RepeatFor  2  (((D  0  THENA  Auto)  THEN  D  -1))  THEN  Reduce  0)

---

Home Index