---

Step * 1 of Lemma presheaf-type-iso_wf


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>)
BY
{ ((InstHyp [⌜<I, a>⌝] (-5)⋅ THENA Auto)
   THEN ApFunToHypEquands `Z' ⌜Z u⌝ ⌜F <I, a>⌝ (-1)⋅
   THEN Auto
   THEN Reduce -1
   THEN NthHypEqTrans (-1)
   THEN RepeatFor 4 (EqCDA)
   THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  F  :  (I:cat-ob(C)  \mtimes{}  X(I))  {}\mrightarrow{}  \mBbbU{}'
4.  x1  :  x:(I:cat-ob(C)  \mtimes{}  X(I))
{}\mrightarrow{}  y:(I:cat-ob(C)  \mtimes{}  X(I))
{}\mrightarrow{}  let  A,a  =  y 
      in  let  B,b  =  x 
            in  \{f:cat-arrow(C)  A  B|  f(b)  =  a\} 
{}\mrightarrow{}  (F  x)
{}\mrightarrow{}  (F  y)
5.  \mforall{}x:I:cat-ob(C)  \mtimes{}  X(I).  ((x1  x  x  (cat-id(C)  (fst(x))))  =  (\mlambda{}x.x))
6.  \mforall{}x,y,z:I:cat-ob(C)  \mtimes{}  X(I).  \mforall{}f:let  A,a  =  y 
                                                                  in  let  B,b  =  x 
                                                                        in  \{f:cat-arrow(C)  A  B|  f(b)  =  a\}  .  \mforall{}g:let  A,a  =  z 
                                                                                                                                                    in  let  B,b  =  y 
                                                                                                                                                          in  \{f:cat-arrow(C)  A 
                                                                                                                                                                      B| 
                                                                                                                                                                  f(b)  =  a\}  .
          ((x1  x  z  (cat-comp(C)  (fst(z))  (fst(y))  (fst(x))  g  f))  =  ((x1  y  z  g)  o  (x1  x  y  f)))
7.  I  :  cat-ob(C)
8.  a  :  X(I)
9.  u  :  F  <I,  a>
\mvdash{}  (x1  <I,  a>  <I,  cat-id(C)  I(a)>  (cat-id(C)  I)  u)  =  u


By

---

Latex:
((InstHyp  [\mkleeneopen{}<I,  a>\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
  THEN  ApFunToHypEquands  `Z'  \mkleeneopen{}Z  u\mkleeneclose{}  \mkleeneopen{}F  <I,  a>\mkleeneclose{}  (-1)\mcdot{}
  THEN  Auto
  THEN  Reduce  -1
  THEN  NthHypEqTrans  (-1)
  THEN  RepeatFor  4  (EqCDA)
  THEN  Auto)

---

Home Index