---

Step * 1 4 of Lemma presheaf-elements_wf


1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
⊢ ∀Aa,Bb,z,Dd: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)} .
  ∀g:let A,a = Bb 
     in let B,b = z 
        in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} . ∀h:let A,a = z 
                                                                     in let B,b = Dd 
                                                                        in {f:cat-arrow(op-cat(C)) B A| 
                                                                            (P B A f b) = a ∈ (P A)} .
    ((cat-comp(op-cat(C)) (fst(Dd)) (fst(z)) (fst(Aa)) h (cat-comp(op-cat(C)) (fst(z)) (fst(Bb)) (fst(Aa)) g f))
    = (cat-comp(op-cat(C)) (fst(Dd)) (fst(Bb)) (fst(Aa)) (cat-comp(op-cat(C)) (fst(Dd)) (fst(z)) (fst(Bb)) h g) f)
    ∈ let A,a = Aa 
      in let B,b = Dd 
         in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} )
BY
{ (RepeatFor 4 (((D 0 THENA Auto) THEN D -1)) THEN Reduce 0 THEN RepeatFor 3 ((At ⌜Type⌝ (D 0)⋅ THENA Auto))) }

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
7. A3 : cat-ob(op-cat(C))
8. z1 : P A3
9. A4 : cat-ob(op-cat(C))
10. D1 : P A4
11. f : {f:cat-arrow(op-cat(C)) A2 A| (P A2 A f B1) = A1 ∈ (P A)} 
12. g : {f:cat-arrow(op-cat(C)) A3 A2| (P A3 A2 f z1) = B1 ∈ (P A2)} 
13. h : {f:cat-arrow(op-cat(C)) A4 A3| (P A4 A3 f D1) = z1 ∈ (P A3)} 
⊢ (cat-comp(op-cat(C)) A4 A3 A h (cat-comp(op-cat(C)) A3 A2 A g f))
= (cat-comp(op-cat(C)) A4 A2 A (cat-comp(op-cat(C)) A4 A3 A2 h g) f)
∈ {f:cat-arrow(op-cat(C)) A4 A| (P A4 A f D1) = A1 ∈ (P A)} 

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  P  :  Functor(op-cat(C);TypeCat)
\mvdash{}  \mforall{}Aa,Bb,z,Dd: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\}  .
    \mforall{}g:let  A,a  =  Bb 
          in  let  B,b  =  z 
                in  \{f:cat-arrow(op-cat(C))  B  A|  (P  B  A  f  b)  =  a\}  .  \mforall{}h:let  A,a  =  z 
                                                                                                                          in  let  B,b  =  Dd 
                                                                                                                                in  \{f:cat-arrow(op-cat(C))  B  A| 
                                                                                                                                        (P  B  A  f  b)  =  a\}  .
        ((cat-comp(op-cat(C))  (fst(Dd))  (fst(z))  (fst(Aa))  h 
            (cat-comp(op-cat(C))  (fst(z))  (fst(Bb))  (fst(Aa))  g  f))
        =  (cat-comp(op-cat(C))  (fst(Dd))  (fst(Bb))  (fst(Aa)) 
              (cat-comp(op-cat(C))  (fst(Dd))  (fst(z))  (fst(Bb))  h  g) 
              f))


By

---

Latex:
(RepeatFor  4  (((D  0  THENA  Auto)  THEN  D  -1))
  THEN  Reduce  0
  THEN  RepeatFor  3  ((At  \mkleeneopen{}Type\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)))

---

Home Index