---

Step * 1 of Lemma type-functor-compose_wf


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)))
BY
{ OnMaybeHyp 8 (\h. ((InstHyp [⌜T⌝;⌜S⌝;⌜V⌝;⌜f⌝;⌜g⌝] h⋅ THENA Complete (Auto)) THEN RepUR ``compose`` -1)) }

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
15. (G1 (λx.(g (f x)))) = (λx.(G1 g (G1 f x))) ∈ ((F1 T) ⟶ (F1 V))
⊢ (F3 (G1 (λx.(g (f x))))) = (λx.(F3 (G1 g) (F3 (G1 f) x))) ∈ ((F2 (F1 T)) ⟶ (F2 (F1 V)))

---

Latex:

---

Latex:

1.  F2  :  Type  {}\mrightarrow{}  Type
2.  F3  :  \mcap{}T,S:Type.    ((T  {}\mrightarrow{}  S)  {}\mrightarrow{}  (F2  T)  {}\mrightarrow{}  (F2  S))
3.  \mforall{}T:Type.  ((F3  (\mlambda{}x.x))  =  (\mlambda{}x.x))
4.  \mforall{}T,S,V:Type.  \mforall{}f:T  {}\mrightarrow{}  S.  \mforall{}g:S  {}\mrightarrow{}  V.    ((F3  (g  o  f))  =  ((F3  g)  o  (F3  f)))
5.  F1  :  Type  {}\mrightarrow{}  Type
6.  G1  :  \mcap{}T,S:Type.    ((T  {}\mrightarrow{}  S)  {}\mrightarrow{}  (F1  T)  {}\mrightarrow{}  (F1  S))
7.  \mforall{}T:Type.  ((G1  (\mlambda{}x.x))  =  (\mlambda{}x.x))
8.  \mforall{}T,S,V:Type.  \mforall{}f:T  {}\mrightarrow{}  S.  \mforall{}g:S  {}\mrightarrow{}  V.    ((G1  (g  o  f))  =  ((G1  g)  o  (G1  f)))
9.  \mforall{}T:Type.  ((F3  (G1  (\mlambda{}x.x)))  =  (\mlambda{}x.x))
10.  T  :  Type
11.  S  :  Type
12.  V  :  Type
13.  f  :  T  {}\mrightarrow{}  S
14.  g  :  S  {}\mrightarrow{}  V
\mvdash{}  (F3  (G1  (\mlambda{}x.(g  (f  x)))))  =  (\mlambda{}x.(F3  (G1  g)  (F3  (G1  f)  x)))


By

---

Latex:
OnMaybeHyp  8  (\mbackslash{}h.  ((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
                                      ))

---

Home Index