---

Step * 1 of Lemma ps-subset-restriction


1. Cob : Type
2. Carrow : Cob ⟶ Cob ⟶ Type
3. Cid : x:Cob ⟶ (Carrow x x)
4. Ccomp : x:Cob ⟶ y:Cob ⟶ z:Cob ⟶ (Carrow x y) ⟶ (Carrow y z) ⟶ (Carrow x z)
5. ∀x,y:Cob. ∀f:Carrow x y.
     (((Ccomp x x y (Cid x) f) = f ∈ (Carrow x y)) ∧ ((Ccomp x y y f (Cid y)) = f ∈ (Carrow x y)))
6. ∀x,y,z,w:Cob. ∀f:Carrow x y. ∀g:Carrow y z. ∀h:Carrow z w.
     ((Ccomp x z w (Ccomp x y z f g) h) = (Ccomp x y w f (Ccomp y z w g h)) ∈ (Carrow x w))
7. X : ps_context{j:l}(<Cob, Carrow, Cid, Ccomp>)
8. Y : ps_context{j:l}(<Cob, Carrow, Cid, Ccomp>)
9. λA,x. x ∈ A:Cob ⟶ Y(A) ⟶ X(A)
10. ∀A,B:Cob. ∀g:Carrow B A.  ((λx.g(x)) = (λx.g(x)) ∈ (Y(A) ⟶ X(B)))
11. I : Cob
12. J : Cob
13. f : Carrow J I
14. a : Y(I)
15. <Cob, Carrow, Cid, Ccomp> ∈ SmallCategory
⊢ f(a) = f(a) ∈ X(J)
BY
{ ((InstHyp [⌜I⌝;⌜J⌝;⌜f⌝] (-6)⋅ THENA Auto)
   THEN (ApFunToHypEquands `Z' ⌜Z a⌝ ⌜X(J)⌝ (-1)⋅ THENA Auto)
   THEN Reduce -1
   THEN Auto) }

---

Latex:

---

Latex:

1.  Cob  :  Type
2.  Carrow  :  Cob  {}\mrightarrow{}  Cob  {}\mrightarrow{}  Type
3.  Cid  :  x:Cob  {}\mrightarrow{}  (Carrow  x  x)
4.  Ccomp  :  x:Cob  {}\mrightarrow{}  y:Cob  {}\mrightarrow{}  z:Cob  {}\mrightarrow{}  (Carrow  x  y)  {}\mrightarrow{}  (Carrow  y  z)  {}\mrightarrow{}  (Carrow  x  z)
5.  \mforall{}x,y:Cob.  \mforall{}f:Carrow  x  y.    (((Ccomp  x  x  y  (Cid  x)  f)  =  f)  \mwedge{}  ((Ccomp  x  y  y  f  (Cid  y))  =  f))
6.  \mforall{}x,y,z,w:Cob.  \mforall{}f:Carrow  x  y.  \mforall{}g:Carrow  y  z.  \mforall{}h:Carrow  z  w.
          ((Ccomp  x  z  w  (Ccomp  x  y  z  f  g)  h)  =  (Ccomp  x  y  w  f  (Ccomp  y  z  w  g  h)))
7.  X  :  ps\_context\{j:l\}(<Cob,  Carrow,  Cid,  Ccomp>)
8.  Y  :  ps\_context\{j:l\}(<Cob,  Carrow,  Cid,  Ccomp>)
9.  \mlambda{}A,x.  x  \mmember{}  A:Cob  {}\mrightarrow{}  Y(A)  {}\mrightarrow{}  X(A)
10.  \mforall{}A,B:Cob.  \mforall{}g:Carrow  B  A.    ((\mlambda{}x.g(x))  =  (\mlambda{}x.g(x)))
11.  I  :  Cob
12.  J  :  Cob
13.  f  :  Carrow  J  I
14.  a  :  Y(I)
15.  <Cob,  Carrow,  Cid,  Ccomp>  \mmember{}  SmallCategory
\mvdash{}  f(a)  =  f(a)


By

---

Latex:
((InstHyp  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  (-6)\mcdot{}  THENA  Auto)
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}Z  a\mkleeneclose{}  \mkleeneopen{}X(J)\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  Reduce  -1
  THEN  Auto)

---

Home Index