---

Step * 1 of Lemma compU-wf-lemma1

.....subterm..... T:t
1:n
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. {G, phi.𝕀 ⊢ _:c𝕌} ∈ 𝕌{[i'' | j'']}
4. E : {G, phi.𝕀 ⊢ _:c𝕌}
5. (E)[0(𝕀)] ∈ {G, phi ⊢ _:c𝕌}
6. {G ⊢ _:c𝕌[phi |⟶ (E)[0(𝕀)]]} ∈ 𝕌{[i' | j']}
7. A : {G ⊢ _:c𝕌[phi |⟶ (E)[0(𝕀)]]}
⊢ encode(Glue [phi ⊢→ (decode((E)[1(𝕀)]);equiv-fun(equivU(G, phi;(decode(E))-;(compOp(E))-)))] decode(A);
         cfun-to-cop(G;Glue [phi ⊢→ (decode((E)[1(𝕀)]);equiv-fun(equivU(G, phi;(decode(E))-;(compOp(E))-)))] decode(A)
             ;comp(Glue [phi ⊢→ (decode((E)[1(𝕀)]), equivU(G, phi;(decode(E))-;(compOp(E))-))] decode(A)) ))
  ∈ {G ⊢ _:c𝕌[phi |⟶ (E)[1(𝕀)]]}
BY
{ ((InstLemma `rev-type-line_wf` [⌜G, phi⌝;⌜decode(E)⌝]⋅ THENA Auto)
   THEN (InstLemma  `equivU_wf` [⌜G, phi⌝;⌜(decode(E))-⌝;⌜(compOp(E))-⌝]⋅ THENA Auto)
   THEN (RWO "rev-type-line-0 rev-type-line-1" (-1) THENA Auto)
   THEN ((Assert (E)[1(𝕀)] ∈ {G, phi ⊢ _:c𝕌} BY
                ((InstLemma `csm-ap-term_wf` [⌜parm{j}⌝;⌜parm{i'}⌝;⌜G, phi⌝;⌜G, phi.𝕀⌝;⌜c𝕌⌝;⌜[1(𝕀)]⌝;⌜E⌝]⋅ THENA Auto)
                 THEN RWO "csm-cubical-universe" (-1)
                 THEN Auto))
         THEN (Assert G, phi ⊢ decode((E)[1(𝕀)]) BY
                     Auto)
         )
   THEN DVar `A'
   THEN (ApFunToHypEquands `Z' ⌜decode(Z)⌝ ⌜{G, phi ⊢ _}⌝ (-5)⋅ THENA (Fold `member` 0 THEN MemCD THEN Auto))) }

1
1. G : CubicalSet{j}
2. phi : {G ⊢ _:𝔽}
3. {G, phi.𝕀 ⊢ _:c𝕌} ∈ 𝕌{[i'' | j'']}
4. E : {G, phi.𝕀 ⊢ _:c𝕌}
5. (E)[0(𝕀)] ∈ {G, phi ⊢ _:c𝕌}
6. {G ⊢ _:c𝕌[phi |⟶ (E)[0(𝕀)]]} ∈ 𝕌{[i' | j']}
7. A : {G ⊢ _:c𝕌}
8. (E)[0(𝕀)] = A ∈ {G, phi ⊢ _:c𝕌}
9. G, phi.𝕀 ⊢ (decode(E))-
10. equivU(G, phi;(decode(E))-;(compOp(E))-) ∈ {G, phi ⊢ _:Equiv((decode(E))[1(𝕀)];(decode(E))[0(𝕀)])}
11. (E)[1(𝕀)] ∈ {G, phi ⊢ _:c𝕌}
12. G, phi ⊢ decode((E)[1(𝕀)])
13. decode((E)[0(𝕀)]) = decode(A) ∈ {G, phi ⊢ _}
⊢ encode(Glue [phi ⊢→ (decode((E)[1(𝕀)]);equiv-fun(equivU(G, phi;(decode(E))-;(compOp(E))-)))] decode(A);
         cfun-to-cop(G;Glue [phi ⊢→ (decode((E)[1(𝕀)]);equiv-fun(equivU(G, phi;(decode(E))-;(compOp(E))-)))] decode(A)
             ;comp(Glue [phi ⊢→ (decode((E)[1(𝕀)]), equivU(G, phi;(decode(E))-;(compOp(E))-))] decode(A)) ))
  ∈ {G ⊢ _:c𝕌[phi |⟶ (E)[1(𝕀)]]}

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  G  :  CubicalSet\{j\}
2.  phi  :  \{G  \mvdash{}  \_:\mBbbF{}\}
3.  \{G,  phi.\mBbbI{}  \mvdash{}  \_:c\mBbbU{}\}  \mmember{}  \mBbbU{}\{[i''  |  j'']\}
4.  E  :  \{G,  phi.\mBbbI{}  \mvdash{}  \_:c\mBbbU{}\}
5.  (E)[0(\mBbbI{})]  \mmember{}  \{G,  phi  \mvdash{}  \_:c\mBbbU{}\}
6.  \{G  \mvdash{}  \_:c\mBbbU{}[phi  |{}\mrightarrow{}  (E)[0(\mBbbI{})]]\}  \mmember{}  \mBbbU{}\{[i'  |  j']\}
7.  A  :  \{G  \mvdash{}  \_:c\mBbbU{}[phi  |{}\mrightarrow{}  (E)[0(\mBbbI{})]]\}
\mvdash{}  encode(Glue  [phi  \mvdash{}\mrightarrow{}  (decode((E)[1(\mBbbI{})]);equiv-fun(equivU(G,  phi;(decode(E))-;(compOp(E))-)))]
                            decode(A);cfun-to-cop(G;Glue  [phi  \mvdash{}\mrightarrow{}  (decode((E)[1(\mBbbI{})]);
                                                                                                        equiv-fun(equivU(G,  phi;(decode(E))-;
                                                                                                                                          (compOp(E))-)))]  decode(A)
                                                        ;comp(Glue  [phi  \mvdash{}\mrightarrow{}  (decode((E)[1(\mBbbI{})]),  equivU(G,  phi;(decode(E))-;
                                                                                                                                                    (compOp(E))-))]
                                                                            decode(A))  ))  \mmember{}  \{G  \mvdash{}  \_:c\mBbbU{}[phi  |{}\mrightarrow{}  (E)[1(\mBbbI{})]]\}


By

---

Latex:
((InstLemma  `rev-type-line\_wf`  [\mkleeneopen{}G,  phi\mkleeneclose{};\mkleeneopen{}decode(E)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma    `equivU\_wf`  [\mkleeneopen{}G,  phi\mkleeneclose{};\mkleeneopen{}(decode(E))-\mkleeneclose{};\mkleeneopen{}(compOp(E))-\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "rev-type-line-0  rev-type-line-1"  (-1)  THENA  Auto)
  THEN  ((Assert  (E)[1(\mBbbI{})]  \mmember{}  \{G,  phi  \mvdash{}  \_:c\mBbbU{}\}  BY
                            ((InstLemma  `csm-ap-term\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}G,  phi\mkleeneclose{};\mkleeneopen{}G,  phi.\mBbbI{}\mkleeneclose{};\mkleeneopen{}c\mBbbU{}\mkleeneclose{};\mkleeneopen{}[1(\mBbbI{})]\mkleeneclose{};
                                \mkleeneopen{}E\mkleeneclose{}]\mcdot{}
                                THENA  Auto
                                )
                              THEN  RWO  "csm-cubical-universe"  (-1)
                              THEN  Auto))
              THEN  (Assert  G,  phi  \mvdash{}  decode((E)[1(\mBbbI{})])  BY
                                      Auto)
              )
  THEN  DVar  `A'
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}decode(Z)\mkleeneclose{}  \mkleeneopen{}\{G,  phi  \mvdash{}  \_\}\mkleeneclose{}  (-5)\mcdot{}
              THENA  (Fold  `member`  0  THEN  MemCD  THEN  Auto)
              ))

---

Home Index