---

Step * of Lemma presheaf-type-iso-inverse2

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)].
  ((presheaf-type-iso(X) o presheaf-type-rev-iso(X)) = (λx.x) ∈ ({X ⊢ _} ⟶ {X ⊢ _}))
BY
{ (Auto
   THEN (FunExt THENA Auto)
   THEN Reduce 0
   THEN Symmetry
   THEN D -1
   THEN MemTypeCD
   THEN Auto
   THEN DVar `x'
   THEN All Reduce
   THEN RepUR ``presheaf-type-iso presheaf-type-rev-iso mk-presheaf`` 0
   THEN EqCDA
   THEN Repeat ((FunExt THENA Auto))
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (FunExt  THENA  Auto)
  THEN  Reduce  0
  THEN  Symmetry
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  DVar  `x'
  THEN  All  Reduce
  THEN  RepUR  ``presheaf-type-iso  presheaf-type-rev-iso  mk-presheaf``  0
  THEN  EqCDA
  THEN  Repeat  ((FunExt  THENA  Auto))
  THEN  Reduce  0
  THEN  Auto)

---

Home Index