---

Step * of Lemma presheaf-type-iso_wf

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)].  (presheaf-type-iso(X) ∈ presheaf_type{i:l}(C; X) ⟶ {X ⊢' _})
BY
{ (Auto
   THEN (FunExt THENA Auto)
   THEN D -1
   THEN D -2
   THEN RepUR ``presheaf-type presheaf-type-iso`` 0
   THEN All Reduce
   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 (RepUR ``type-cat``)
   THEN ((MemTypeCD THEN Reduce 0) THENL [Auto; (D 0 THEN Intros THEN ExRepD); Auto])) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. F : (I:cat-ob(C) × X(I)) ⟶ 𝕌'
4. x1 : x:(I:cat-ob(C) × X(I))
⟶ y:(I:cat-ob(C) × X(I))
⟶ let A,a = y 
   in let B,b = x 
      in {f:cat-arrow(C) A B| f(b) = a ∈ (X A)} 
⟶ (F x)
⟶ (F y)
5. ∀x:I:cat-ob(C) × X(I). ((x1 x x (cat-id(C) (fst(x)))) = (λx.x) ∈ ((F x) ⟶ (F x)))
6. ∀x,y,z:I:cat-ob(C) × X(I). ∀f:let A,a = y 
                                 in let B,b = x 
                                    in {f:cat-arrow(C) A B| f(b) = a ∈ (X A)} . ∀g:let A,a = z 
                                                                                  in let B,b = y 
                                                                                     in {f:cat-arrow(C) A B| 
                                                                                         f(b) = a ∈ (X A)} .
     ((x1 x z (cat-comp(C) (fst(z)) (fst(y)) (fst(x)) g f)) = ((x1 y z g) o (x1 x y f)) ∈ ((F x) ⟶ (F z)))
7. I : cat-ob(C)
8. a : X(I)
9. u : F <I, a>
⊢ (x1 <I, a> <I, cat-id(C) I(a)> (cat-id(C) I) u) = u ∈ (F <I, a>)

2
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. F : (I:cat-ob(C) × X(I)) ⟶ 𝕌'
4. x1 : x:(I:cat-ob(C) × X(I))
⟶ y:(I:cat-ob(C) × X(I))
⟶ let A,a = y 
   in let B,b = x 
      in {f:cat-arrow(C) A B| f(b) = a ∈ (X A)} 
⟶ (F x)
⟶ (F y)
5. ∀x:I:cat-ob(C) × X(I). ((x1 x x (cat-id(C) (fst(x)))) = (λx.x) ∈ ((F x) ⟶ (F x)))
6. ∀x,y,z:I:cat-ob(C) × X(I). ∀f:let A,a = y 
                                 in let B,b = x 
                                    in {f:cat-arrow(C) A B| f(b) = a ∈ (X A)} . ∀g:let A,a = z 
                                                                                  in let B,b = y 
                                                                                     in {f:cat-arrow(C) A B| 
                                                                                         f(b) = a ∈ (X A)} .
     ((x1 x z (cat-comp(C) (fst(z)) (fst(y)) (fst(x)) g f)) = ((x1 y z g) o (x1 x y f)) ∈ ((F x) ⟶ (F z)))
7. I : cat-ob(C)
8. J : cat-ob(C)
9. K : cat-ob(C)
10. f : cat-arrow(C) J I
11. g : cat-arrow(C) K J
12. a : X(I)
13. u : F <I, a>
⊢ (x1 <I, a> <K, cat-comp(C) K J I g f(a)> (cat-comp(C) K J I g f) u)
= (x1 <J, f(a)> <K, g(f(a))> g (x1 <I, a> <J, f(a)> f u))
∈ (F <K, cat-comp(C) K J I g f(a)>)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (FunExt  THENA  Auto)
  THEN  D  -1
  THEN  D  -2
  THEN  RepUR  ``presheaf-type  presheaf-type-iso``  0
  THEN  All  Reduce
  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  (RepUR  ``type-cat``)
  THEN  ((MemTypeCD  THEN  Reduce  0)  THENL  [Auto;  (D  0  THEN  Intros  THEN  ExRepD);  Auto]))

---

Home Index