---

Step * of Lemma type-functor-sum_wf

∀[F,G:Functor].  (F + G ∈ Functor)
BY
{ (Intros
   THEN Unhide
   THEN RepeatFor 2 (D 2)
   THEN RepeatFor 2 (D 1)
   THEN All Reduce
   THEN RepUR ``type-functor-sum type-functor`` 0
   THEN MemTypeCD
   THEN (Reduce 0 THEN RepUR ``compose`` 0)
   THEN Auto
   THEN EqCD
   THEN Auto
   THEN ∀h:hyp. ((InstHyp [⌜T⌝] h⋅ THENA Complete (Auto)) THEN RWO "-1" 0 THEN Auto) 
   THEN ∀h:hyp. ((InstHyp [⌜T⌝;⌜S⌝;⌜V⌝;⌜f⌝;⌜g⌝] h⋅ THENA Complete (Auto))
                 THEN RepUR ``compose`` -1
                 THEN RWO "-1" 0
                 THEN Reduce 0
                 THEN Auto) ) }

---

Latex:

---

Latex:
\mforall{}[F,G:Functor].    (F  +  G  \mmember{}  Functor)


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  RepeatFor  2  (D  2)
  THEN  RepeatFor  2  (D  1)
  THEN  All  Reduce
  THEN  RepUR  ``type-functor-sum  type-functor``  0
  THEN  MemTypeCD
  THEN  (Reduce  0  THEN  RepUR  ``compose``  0)
  THEN  Auto
  THEN  EqCD
  THEN  Auto
  THEN  \mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}T\mkleeneclose{}]  h\mcdot{}  THENA  Complete  (Auto))  THEN  RWO  "-1"  0  THEN  Auto) 
  THEN  \mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}V\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]  h\mcdot{}  THENA  Complete  (Auto))
                              THEN  RepUR  ``compose``  -1
                              THEN  RWO  "-1"  0
                              THEN  Reduce  0
                              THEN  Auto)  )

---

Home Index