---

Step * 1 1 of Lemma compU-wf-lemma1


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(𝕀)]]}
BY
{ ((Assert G ⊢ decode(A) BY
          Auto)
   THEN (Assert G, phi ⊢ decode((E)[0(𝕀)]) BY
               Eq)
   THEN DupHyp (-4)
   THEN DupHyp (-2)
   THEN ((RWO "csm-universe-decode<" (-2) THENA Auto) THEN (RWO "csm-universe-decode<" (-1) THENA Auto))
   THEN (Assert G, phi ⊢ Equiv((decode(E))[1(𝕀)];(decode(E))[0(𝕀)]) BY
               (InstLemma `cubical-equiv_wf` [⌜G, phi⌝;⌜(decode(E))[1(𝕀)]⌝;⌜(decode(E))[0(𝕀)]⌝]⋅ 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 ⊢ _}
14. G ⊢ decode(A)
15. G, phi ⊢ decode((E)[0(𝕀)])
16. G, phi ⊢ (decode(E))[1(𝕀)]
17. G, phi ⊢ (decode(E))[0(𝕀)]
18. G, phi ⊢ Equiv((decode(E))[1(𝕀)];(decode(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(𝕀)]]}

---

Latex:

---

Latex:

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{}\}
8.  (E)[0(\mBbbI{})]  =  A
9.  G,  phi.\mBbbI{}  \mvdash{}  (decode(E))-
10.  equivU(G,  phi;(decode(E))-;(compOp(E))-)
        \mmember{}  \{G,  phi  \mvdash{}  \_:Equiv((decode(E))[1(\mBbbI{})];(decode(E))[0(\mBbbI{})])\}
11.  (E)[1(\mBbbI{})]  \mmember{}  \{G,  phi  \mvdash{}  \_:c\mBbbU{}\}
12.  G,  phi  \mvdash{}  decode((E)[1(\mBbbI{})])
13.  decode((E)[0(\mBbbI{})])  =  decode(A)
\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:
((Assert  G  \mvdash{}  decode(A)  BY
                Auto)
  THEN  (Assert  G,  phi  \mvdash{}  decode((E)[0(\mBbbI{})])  BY
                          Eq)
  THEN  DupHyp  (-4)
  THEN  DupHyp  (-2)
  THEN  ((RWO  "csm-universe-decode<"  (-2)  THENA  Auto)
              THEN  (RWO  "csm-universe-decode<"  (-1)  THENA  Auto)
              )
  THEN  (Assert  G,  phi  \mvdash{}  Equiv((decode(E))[1(\mBbbI{})];(decode(E))[0(\mBbbI{})])  BY
                          (InstLemma  `cubical-equiv\_wf`  [\mkleeneopen{}G,  phi\mkleeneclose{};\mkleeneopen{}(decode(E))[1(\mBbbI{})]\mkleeneclose{};\mkleeneopen{}(decode(E))[0(\mBbbI{})]\mkleeneclose{}]\mcdot{}
                            THEN  Auto
                            )))

---

Home Index