---

Step * of Lemma composition-type-lemma4

No Annotations
∀Gamma:j⊢. ∀phi:{Gamma ⊢ _:𝔽}. ∀A:{Gamma.𝕀 ⊢ _}. ∀u:{Gamma, phi.𝕀 ⊢ _:A}. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀rho:Gamma(I).
∀K:fset(ℕ). ∀g:J,phi(f(rho))(K).
  ((u)<(s(f(rho));<new-name(J)>)> o iota((new-name(J)0) ⋅ g)
  = ((u)<(s(rho);<new-name(I)>)> o iota)subset-trans(I+new-name(I);J+new-name(J);f,new-name(I)=new-name(J);
                                                     s(phi(rho)))((new-name(J)0) ⋅ g)
  ∈ A(g((new-name(J)0)((s(f(rho));<new-name(J)>)))))
BY
{ (InstLemma `composition-type-lemma3` []
   THEN RepeatFor 3 (ParallelLast')
   THEN (InstLemma `context-subset-adjoin-subtype` [⌜Gamma⌝;⌜𝕀⌝;⌜phi⌝]⋅ THENA Auto)
   THEN ParallelOp -2
   THEN Thin (-4)
   THEN RepeatFor 4 (ParallelLast')
   THEN Intros
   THEN ApFunToHypEquands `Z' ⌜Z((new-name(J)0) ⋅ g)⌝ ⌜A(g((new-name(J)0)((s(f(rho));<new-name(J)>))))⌝ (-3)⋅
   THEN Try (Trivial)
   THEN Fold `member` 0) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. A : {Gamma.𝕀 ⊢ _}
4. {Gamma.𝕀 ⊢ _} ⊆r {Gamma, phi.𝕀 ⊢ _}
5. u : {Gamma, phi.𝕀 ⊢ _:A}
6. I : fset(ℕ)
7. J : fset(ℕ)
8. f : J ⟶ I
9. rho : Gamma(I)
10. (u)<(s(f(rho));<new-name(J)>)> o iota
= ((u)<(s(rho);<new-name(I)>)> o iota)subset-trans(I+new-name(I);J+new-name(J);f,new-name(I)=new-name(J);s(phi(rho)))
∈ {J+new-name(J),s(phi(f(rho))) ⊢ _:(A)<(s(f(rho));<new-name(J)>)> o iota}
11. K : fset(ℕ)
12. g : J,phi(f(rho))(K)
13. Z : {J+new-name(J),s(phi(f(rho))) ⊢ _:(A)<(s(f(rho));<new-name(J)>)> o iota}
⊢ Z((new-name(J)0) ⋅ g) ∈ A(g((new-name(J)0)((s(f(rho));<new-name(J)>))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}Gamma:j\mvdash{}.  \mforall{}phi:\{Gamma  \mvdash{}  \_:\mBbbF{}\}.  \mforall{}A:\{Gamma.\mBbbI{}  \mvdash{}  \_\}.  \mforall{}u:\{Gamma,  phi.\mBbbI{}  \mvdash{}  \_:A\}.  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.
\mforall{}rho:Gamma(I).  \mforall{}K:fset(\mBbbN{}).  \mforall{}g:J,phi(f(rho))(K).
    ((u)<(s(f(rho));<new-name(J)>)>  o  iota((new-name(J)0)  \mcdot{}  g)
    =  ((u)<(s(rho);<new-name(I)>)>  o  iota)subset-trans(I+new-name(I);J+new-name(J);
                                                                                                          f,new-name(I)=new-name(J);
                                                                                                          s(phi(rho)))((new-name(J)0)  \mcdot{}  g))


By

---

Latex:
(InstLemma  `composition-type-lemma3`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (InstLemma  `context-subset-adjoin-subtype`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}\mBbbI{}\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelOp  -2
  THEN  Thin  (-4)
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Intros
  THEN  ApFunToHypEquands  `Z'  \mkleeneopen{}Z((new-name(J)0)  \mcdot{}  g)\mkleeneclose{} 
  \mkleeneopen{}A(g((new-name(J)0)((s(f(rho));<new-name(J)>))))\mkleeneclose{}  (-3)\mcdot{}
  THEN  Try  (Trivial)
  THEN  Fold  `member`  0)

---

Home Index