---

Step * of Lemma presheaf-type-iso-inverse

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)].
  ((presheaf-type-rev-iso(X) o presheaf-type-iso(X)) = (λx.x) ∈ (presheaf_type{i:l}(C; X) ⟶ presheaf_type{i:l}(C; X)))
BY
{ (Auto
   THEN (FunExt THENA Auto)
   THEN Reduce 0
   THEN Symmetry
   THEN RepeatFor 2 (DVar `x')
   THEN All Reduce
   THEN EqTypeCD
   THEN Try ((Reduce 0 THEN Trivial))
   THEN All (RWO "cat_ob_op_lemma op-cat-arrow op-cat-comp op-cat-id")
   THEN Auto
   THEN (All (RWO "sets-ob sets-arrow sets-id sets-comp") THENA Auto)
   THEN RepUR ``presheaf-type-iso presheaf-type-rev-iso mk-presheaf`` 0
   THEN RepUR ``mk-functor`` 0
   THEN EqCDA
   THEN (FunExt THENA Auto)
   THEN Reduce 0) }

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

2
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. F : (I:cat-ob(C) × X(I)) ⟶ cat-ob(TypeCat')
4. x1 : x:(I:cat-ob(C) × X(I))
⟶ y:(I:cat-ob(C) × X(I))
⟶ ((λAa,Bb. let A,a = Aa in let B,b = Bb in {f:cat-arrow(C) A B| f(b) = a ∈ (X A)} ) y x)
⟶ (cat-arrow(TypeCat') (F x) (F y))
5. ∀x:I:cat-ob(C) × X(I)
     ((x1 x x ((λA.(cat-id(C) (fst(A)))) x)) = (cat-id(TypeCat') (F x)) ∈ (cat-arrow(TypeCat') (F x) (F x)))
6. ∀x,y,z:I:cat-ob(C) × X(I). ∀f:(λAa,Bb. let A,a = Aa in let B,b = Bb in {f:cat-arrow(C) A B| f(b) = a ∈ (X A)} ) y x.
   ∀g:(λAa,Bb. let A,a = Aa in let B,b = Bb in {f:cat-arrow(C) A B| f(b) = a ∈ (X A)} ) z y.
     ((x1 x z ((λAa,Bb,Dd,f,g. (cat-comp(C) (fst(Aa)) (fst(Bb)) (fst(Dd)) f g)) z y x g f))
     = (cat-comp(TypeCat') (F x) (F y) (F z) (x1 x y f) (x1 y z g))
     ∈ (cat-arrow(TypeCat') (F x) (F z)))
7. x : I:cat-ob(C) × X(I)
⊢ (x1 x)
= (λq,f,a. (x1 <fst(x), snd(x)> <fst(q), f(snd(x))> f a))
∈ (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)} 
  ⟶ (cat-arrow(TypeCat') (F x) (F y)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].
    ((presheaf-type-rev-iso(X)  o  presheaf-type-iso(X))  =  (\mlambda{}x.x))


By

---

Latex:
(Auto
  THEN  (FunExt  THENA  Auto)
  THEN  Reduce  0
  THEN  Symmetry
  THEN  RepeatFor  2  (DVar  `x')
  THEN  All  Reduce
  THEN  EqTypeCD
  THEN  Try  ((Reduce  0  THEN  Trivial))
  THEN  All  (RWO  "cat\_ob\_op\_lemma  op-cat-arrow  op-cat-comp  op-cat-id")
  THEN  Auto
  THEN  (All  (RWO  "sets-ob  sets-arrow  sets-id  sets-comp")  THENA  Auto)
  THEN  RepUR  ``presheaf-type-iso  presheaf-type-rev-iso  mk-presheaf``  0
  THEN  RepUR  ``mk-functor``  0
  THEN  EqCDA
  THEN  (FunExt  THENA  Auto)
  THEN  Reduce  0)

---

Home Index