Step * 1 3 1 1 1 of Lemma presheaf-elements_wf


1. SmallCategory
2. Functor(op-cat(C);TypeCat)
3. cat-ob(op-cat(C))
4. A1 A
5. A2 cat-ob(op-cat(C))
6. B1 A2
7. cat-arrow(op-cat(C)) A2 A
8. [%1] (P A2 B1) A1 ∈ (P A)
⊢ ((cat-comp(op-cat(C)) A2 (cat-id(op-cat(C)) A)) f ∈ {f:cat-arrow(op-cat(C)) A2 A| (P A2 B1) A1 ∈ (P A)} \000C)
∧ ((cat-comp(op-cat(C)) A2 A2 (cat-id(op-cat(C)) A2) f)
  f
  ∈ {f:cat-arrow(op-cat(C)) A2 A| (P A2 B1) A1 ∈ (P A)} )
BY
(InstLemma `cat-comp-ident` [⌜op-cat(C)⌝;⌜A2⌝;⌜A⌝;⌜f⌝]⋅ THENA Auto) }

1
1. SmallCategory
2. Functor(op-cat(C);TypeCat)
3. cat-ob(op-cat(C))
4. A1 A
5. A2 cat-ob(op-cat(C))
6. B1 A2
7. cat-arrow(op-cat(C)) A2 A
8. [%1] (P A2 B1) A1 ∈ (P A)
9. ((cat-comp(op-cat(C)) A2 A2 (cat-id(op-cat(C)) A2) f) f ∈ (cat-arrow(op-cat(C)) A2 A))
∧ ((cat-comp(op-cat(C)) A2 (cat-id(op-cat(C)) A)) f ∈ (cat-arrow(op-cat(C)) A2 A))
⊢ ((cat-comp(op-cat(C)) A2 (cat-id(op-cat(C)) A)) f ∈ {f:cat-arrow(op-cat(C)) A2 A| (P A2 B1) A1 ∈ (P A)} \000C)
∧ ((cat-comp(op-cat(C)) A2 A2 (cat-id(op-cat(C)) A2) f)
  f
  ∈ {f:cat-arrow(op-cat(C)) A2 A| (P A2 B1) A1 ∈ (P A)} )


Latex:


Latex:

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.  f  :  cat-arrow(op-cat(C))  A2  A
8.  [\%1]  :  (P  A2  A  f  B1)  =  A1
\mvdash{}  ((cat-comp(op-cat(C))  A2  A  A  f  (cat-id(op-cat(C))  A))  =  f)
\mwedge{}  ((cat-comp(op-cat(C))  A2  A2  A  (cat-id(op-cat(C))  A2)  f)  =  f)


By


Latex:
(InstLemma  `cat-comp-ident`  [\mkleeneopen{}op-cat(C)\mkleeneclose{};\mkleeneopen{}A2\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)




Home Index