---

Step * of Lemma type-functor-compose_wf

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

1
1. F2 : Type ⟶ Type
2. F3 : ⋂T,S:Type.  ((T ⟶ S) ⟶ (F2 T) ⟶ (F2 S))
3. ∀T:Type. ((F3 (λx.x)) = (λx.x) ∈ ((F2 T) ⟶ (F2 T)))
4. ∀T,S,V:Type. ∀f:T ⟶ S. ∀g:S ⟶ V.  ((F3 (g o f)) = ((F3 g) o (F3 f)) ∈ ((F2 T) ⟶ (F2 V)))
5. F1 : Type ⟶ Type
6. G1 : ⋂T,S:Type.  ((T ⟶ S) ⟶ (F1 T) ⟶ (F1 S))
7. ∀T:Type. ((G1 (λx.x)) = (λx.x) ∈ ((F1 T) ⟶ (F1 T)))
8. ∀T,S,V:Type. ∀f:T ⟶ S. ∀g:S ⟶ V.  ((G1 (g o f)) = ((G1 g) o (G1 f)) ∈ ((F1 T) ⟶ (F1 V)))
9. ∀T:Type. ((F3 (G1 (λx.x))) = (λx.x) ∈ ((F2 (F1 T)) ⟶ (F2 (F1 T))))
10. T : Type
11. S : Type
12. V : Type
13. f : T ⟶ S
14. g : S ⟶ V
⊢ (F3 (G1 (λx.(g (f x))))) = (λx.(F3 (G1 g) (F3 (G1 f) x))) ∈ ((F2 (F1 T)) ⟶ (F2 (F1 V)))

---

Latex:

---

Latex:
\mforall{}[F,G:Functor].    (F  o  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-compose  type-functor``  0
  THEN  Auto
  THEN  MemTypeCD
  THEN  RepUR  ``compose``  0
  THEN  Auto
  THEN  \mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}T\mkleeneclose{}]  h\mcdot{}  THENA  Complete  (Auto))  THEN  RWO  "-1"  0  THEN  Auto)  )

---

Home Index