---

Step * of Lemma composition-type-lemma3

No Annotations
∀Gamma:j⊢. ∀phi:{Gamma ⊢ _:𝔽}. ∀A:{Gamma.𝕀 ⊢ _}. ∀u:{Gamma, phi.𝕀 ⊢ _:A}. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:Gamma(I).
  ((u)<(s(f(a));<new-name(J)>)> o iota
  = ((u)<(s(a);<new-name(I)>)> o iota)subset-trans(I+new-name(I);J+new-name(J);f,new-name(I)=new-name(J);s(phi(a)))
  ∈ {J+new-name(J),s(phi(f(a))) ⊢ _:(A)<(s(f(a));<new-name(J)>)> o iota})
BY
{ (RepeatFor 3 (Intro)
   THEN (InstLemma `context-subset-adjoin-subtype` [⌜Gamma⌝;⌜𝕀⌝;⌜phi⌝]⋅ THENA Auto)
   THEN Intros
   THEN (Assert ⌜∀I:fset(ℕ). ∀[rho:Gamma(I)]. ((s(rho);<new-name(I)>) ∈ Gamma.𝕀(I+new-name(I)))⌝⋅
         THENA (Auto THEN (RWO "interval-type-at" 0 THENA Auto) THEN RepUR ``interval-presheaf`` 0 THEN Auto)
         )
   THEN (Assert (s(phi(a)))<f,new-name(I)=new-name(J)> = s(phi(f(a))) ∈ 𝔽(J+new-name(J)) BY
               Auto)
   THEN (Assert J+new-name(J),(s(phi(a)))<f,new-name(I)=new-name(J)> = J+new-name(J),s(phi(f(a))) ∈ CubicalSet{j} BY
               (EqCD THEN Auto))
   THEN (InstLemma `context-map-lemma2` [⌜Gamma⌝;⌜phi⌝;⌜J⌝;⌜f(a)⌝]⋅ THENA Auto)
   THEN (Assert <(s(f(a));<new-name(J)>)> o iota ∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀 BY
               (NthHypSq (-1)
                THEN EqCD
                THEN Try (Trivial)
                THEN RepUR ``context-map csm-comp subset-iota compose`` 0
                THEN Auto))
   THEN (Assert <(s(a);<new-name(I)>)> o iota ∈ I+new-name(I),s(phi(a)) j⟶ Gamma, phi.𝕀 BY
               ((InstLemma `context-map-lemma2` [⌜Gamma⌝;⌜phi⌝;⌜I⌝;⌜a⌝]⋅ THENA Auto)
                THEN (Subst' <(s(a);<new-name(I)>)> o iota ~ <(s(a);<new-name(I)>)> 0
                      THENA (RepUR ``context-map csm-comp subset-iota compose`` 0 THEN Auto)
                      )
                THEN Auto))
   THEN (Subst' <(s(f(a));<new-name(J)>)> o iota ~ <(s(f(a));<new-name(J)>)> 0
         THENA (RepUR ``context-map csm-comp subset-iota compose`` 0 THEN Auto)
         )) }

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. a : Gamma(I)
10. ∀I:fset(ℕ). ∀[rho:Gamma(I)]. ((s(rho);<new-name(I)>) ∈ Gamma.𝕀(I+new-name(I)))
11. (s(phi(a)))<f,new-name(I)=new-name(J)> = s(phi(f(a))) ∈ 𝔽(J+new-name(J))
12. J+new-name(J),(s(phi(a)))<f,new-name(I)=new-name(J)> = J+new-name(J),s(phi(f(a))) ∈ CubicalSet{j}
13. <(s(f(a));<new-name(J)>)> ∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
14. <(s(f(a));<new-name(J)>)> o iota ∈ J+new-name(J),s(phi(f(a))) j⟶ Gamma, phi.𝕀
15. <(s(a);<new-name(I)>)> o iota ∈ I+new-name(I),s(phi(a)) j⟶ Gamma, phi.𝕀
⊢ (u)<(s(f(a));<new-name(J)>)>
= ((u)<(s(a);<new-name(I)>)> o iota)subset-trans(I+new-name(I);J+new-name(J);f,new-name(I)=new-name(J);s(phi(a)))
∈ {J+new-name(J),s(phi(f(a))) ⊢ _:(A)<(s(f(a));<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{}a:Gamma(I).
    ((u)<(s(f(a));<new-name(J)>)>  o  iota
    =  ((u)<(s(a);<new-name(I)>)>  o  iota)subset-trans(I+new-name(I);J+new-name(J);
                                                                                                      f,new-name(I)=new-name(J);s(phi(a))))


By

---

Latex:
(RepeatFor  3  (Intro)
  THEN  (InstLemma  `context-subset-adjoin-subtype`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}\mBbbI{}\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Intros
  THEN  (Assert  \mkleeneopen{}\mforall{}I:fset(\mBbbN{}).  \mforall{}[rho:Gamma(I)].  ((s(rho);<new-name(I)>)  \mmember{}  Gamma.\mBbbI{}(I+new-name(I)))\mkleeneclose{}\mcdot{}
              THENA  (Auto
                            THEN  (RWO  "interval-type-at"  0  THENA  Auto)
                            THEN  RepUR  ``interval-presheaf``  0
                            THEN  Auto)
              )
  THEN  (Assert  (s(phi(a)))<f,new-name(I)=new-name(J)>  =  s(phi(f(a)))  BY
                          Auto)
  THEN  (Assert  J+new-name(J),(s(phi(a)))<f,new-name(I)=new-name(J)>  =  J+new-name(J),s(phi(f(a)))  BY
                          (EqCD  THEN  Auto))
  THEN  (InstLemma  `context-map-lemma2`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}f(a)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  <(s(f(a));<new-name(J)>)>  o  iota  \mmember{}  J+new-name(J),s(phi(f(a)))  j{}\mrightarrow{}  Gamma,  phi.\mBbbI{}  BY
                          (NthHypSq  (-1)
                            THEN  EqCD
                            THEN  Try  (Trivial)
                            THEN  RepUR  ``context-map  csm-comp  subset-iota  compose``  0
                            THEN  Auto))
  THEN  (Assert  <(s(a);<new-name(I)>)>  o  iota  \mmember{}  I+new-name(I),s(phi(a))  j{}\mrightarrow{}  Gamma,  phi.\mBbbI{}  BY
                          ((InstLemma  `context-map-lemma2`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (Subst'  <(s(a);<new-name(I)>)>  o  iota  \msim{}  <(s(a);<new-name(I)>)>  0
                                        THENA  (RepUR  ``context-map  csm-comp  subset-iota  compose``  0  THEN  Auto)
                                        )
                            THEN  Auto))
  THEN  (Subst'  <(s(f(a));<new-name(J)>)>  o  iota  \msim{}  <(s(f(a));<new-name(J)>)>  0
              THENA  (RepUR  ``context-map  csm-comp  subset-iota  compose``  0  THEN  Auto)
              ))

---

Home Index