---

Step * of Lemma presheaf-type-rev-iso_wf

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)].  (presheaf-type-rev-iso(X) ∈ {X ⊢ _} ⟶ presheaf_type{i:l}(C; X))
BY
{ (Auto
   THEN (FunExt THENA Auto)
   THEN D -1
   THEN D -2
   THEN RepUR ``presheaf_type presheaf-type-rev-iso mk-presheaf presheaf`` 0
   THEN All Reduce
   THEN (MemCD THEN (All (RWO "cat_ob_op_lemma op-cat-arrow op-cat-comp op-cat-id") THENA Auto))
   THEN (All (RWO "sets-ob sets-arrow sets-id sets-comp") THENA Auto)
   THEN All Reduce
   THEN Auto
   THEN DProdsAndUnions
   THEN All Reduce
   THEN RepUR ``type-cat`` 0
   THEN (FunExt THENW Auto)
   THEN Reduce 0
   THEN DSetVars
   THEN Try (QuickAuto)) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : I:cat-ob(C) ⟶ X(I) ⟶ Type
4. x1 : I:cat-ob(C) ⟶ J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ a:X(I) ⟶ (A I a) ⟶ (A J f(a))
5. ∀I:cat-ob(C). ∀a:X(I). ∀u:A I a.  ((x1 I I (cat-id(C) I) a u) = u ∈ (A I a))
6. ∀I,J,K:cat-ob(C). ∀f:cat-arrow(C) J I. ∀g:cat-arrow(C) K J. ∀a:X(I). ∀u:A I a.
     ((x1 I K (cat-comp(C) K J I g f) a u) = (x1 J K g f(a) (x1 I J f a u)) ∈ (A K cat-comp(C) K J I g f(a)))
7. I2 : cat-ob(C)
8. p1 : X(I2)
9. I1 : cat-ob(C)
10. q1 : X(I1)
11. I : cat-ob(C)
12. z1 : X(I)
13. f : cat-arrow(C) I1 I2
14. f(p1) = q1 ∈ (X I1)
15. g : cat-arrow(C) I I1
16. g(q1) = z1 ∈ (X I)
17. x : A I2 p1
⊢ (x1 I2 I (cat-comp(C) I I1 I2 g f) p1 x) = (x1 I1 I g q1 (x1 I2 I1 f p1 x)) ∈ (A I z1)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].
    (presheaf-type-rev-iso(X)  \mmember{}  \{X  \mvdash{}  \_\}  {}\mrightarrow{}  presheaf\_type\{i:l\}(C;  X))


By

---

Latex:
(Auto
  THEN  (FunExt  THENA  Auto)
  THEN  D  -1
  THEN  D  -2
  THEN  RepUR  ``presheaf\_type  presheaf-type-rev-iso  mk-presheaf  presheaf``  0
  THEN  All  Reduce
  THEN  (MemCD  THEN  (All  (RWO  "cat\_ob\_op\_lemma  op-cat-arrow  op-cat-comp  op-cat-id")  THENA  Auto))
  THEN  (All  (RWO  "sets-ob  sets-arrow  sets-id  sets-comp")  THENA  Auto)
  THEN  All  Reduce
  THEN  Auto
  THEN  DProdsAndUnions
  THEN  All  Reduce
  THEN  RepUR  ``type-cat``  0
  THEN  (FunExt  THENW  Auto)
  THEN  Reduce  0
  THEN  DSetVars
  THEN  Try  (QuickAuto))

---

Home Index