Proof of Nuprl Lemma : case-type-comp

Step * 1 of Lemma case-type-comp_wf1

1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. cA : Gamma, phi ⊢ Compositon(A)
7. cB : Gamma, psi ⊢ Compositon(B)
8. Gamma, (phi ∧ psi) ⊢ A = B
9. compatible-composition{j:l, i:l}(Gamma; phi; psi; A; B; cA; cB)
10. Gamma, (phi ∨ psi) ⊢ (if phi then A else B)
11. H : CubicalSet{j}
12. sigma : H.𝕀 j⟶ Gamma, (phi ∨ psi)
13. chi : {H ⊢ _:𝔽}
14. H.𝕀 ⊢ (1(𝔽) ⇒ ((phi)sigma ∨ (psi)sigma))
15. (∀ (phi)sigma) ∈ {H ⊢ _:𝔽}
16. (∀ (psi)sigma) ∈ {H ⊢ _:𝔽}
17. H.𝕀, ((phi)sigma ∧ (psi)sigma) ⊢ (A)sigma = (B)sigma
18. H.𝕀 ⊢ ((if phi then A else B))sigma
19. H, chi.𝕀 ⊢ ((if phi then A else B))sigma
20. u : {H, chi.𝕀 ⊢ _:((if phi then A else B))sigma}
21. a0 : {H ⊢ _:(((if phi then A else B))sigma)[0(𝕀)][chi |⟶ (u)[0(𝕀)]]}
⊢ (cA H, (∀ (phi)sigma) sigma chi u a0 ∨ cB H, (∀ (psi)sigma) sigma chi u a0)
∈ {H ⊢ _:(((if phi then A else B))sigma)[1(𝕀)][chi |⟶ (u)[1(𝕀)]]}
BY
{ ((All (RWW "csm-case-type") THENA Auto)
THEN (Assert u ∈ {H, (∀ (phi)sigma), chi.𝕀 ⊢ _:(A)sigma} BY

               ((Assert u ∈ {H, (∀ (phi)sigma), chi.𝕀 ⊢ _:(if (phi)sigma then (A)sigma else (B)sigma)} BY

                       ((DoSubsume THEN Try (Trivial))
                        THEN BLemma `subset-cubical-term`
                        THEN Auto
                        THEN BLemma `context-adjoin-subset`
                        THEN Auto))
                THEN InferEqualType
                THEN Try (Trivial)
                THEN EqCDA
                THEN (SubsumeC  ⌜{H.𝕀, (phi)sigma ⊢ _}⌝⋅
                THENL [(Fold `same-cubical-type` 0
                        THEN Using [`psi',⌜(psi)sigma⌝] (BLemma `case-type-same1`)⋅
                        THEN Auto); (BLemma `subset-cubical-type`
                                     THEN Auto

                                     THEN Using [`Y',⌜H, (∀ (phi)sigma).𝕀⌝] (BLemma  `sub_cubical_set_transitivity`)⋅

THEN Auto)⋅])))
) }

1
1. Gamma : CubicalSet{j}
2. phi : {Gamma ⊢ _:𝔽}
3. psi : {Gamma ⊢ _:𝔽}
4. A : {Gamma, phi ⊢ _}
5. B : {Gamma, psi ⊢ _}
6. cA : Gamma, phi ⊢ Compositon(A)
7. cB : Gamma, psi ⊢ Compositon(B)
8. Gamma, (phi ∧ psi) ⊢ A = B
9. compatible-composition{j:l, i:l}(Gamma; phi; psi; A; B; cA; cB)
10. Gamma, (phi ∨ psi) ⊢ (if phi then A else B)
11. H : CubicalSet{j}
12. sigma : H.𝕀 j⟶ Gamma, (phi ∨ psi)
13. chi : {H ⊢ _:𝔽}
14. H.𝕀 ⊢ (1(𝔽) ⇒ ((phi)sigma ∨ (psi)sigma))
15. (∀ (phi)sigma) ∈ {H ⊢ _:𝔽}
16. (∀ (psi)sigma) ∈ {H ⊢ _:𝔽}
17. H.𝕀, ((phi)sigma ∧ (psi)sigma) ⊢ (A)sigma = (B)sigma
18. H.𝕀 ⊢ (if (phi)sigma then (A)sigma else (B)sigma)
19. H, chi.𝕀 ⊢ (if (phi)sigma then (A)sigma else (B)sigma)
20. u : {H, chi.𝕀 ⊢ _:(if (phi)sigma then (A)sigma else (B)sigma)}

21. a0 : {H ⊢ _:(if ((phi)sigma)[0(𝕀)] then ((A)sigma)[0(𝕀)] else ((B)sigma)[0(𝕀)])[chi |⟶ (u)[0(𝕀)]]}

22. u ∈ {H, (∀ (phi)sigma), chi.𝕀 ⊢ _:(A)sigma}
⊢ (cA H, (∀ (phi)sigma) sigma chi u a0 ∨ cB H, (∀ (psi)sigma) sigma chi u a0)

  ∈ {H ⊢ _:(if ((phi)sigma)[1(𝕀)] then ((A)sigma)[1(𝕀)] else ((B)sigma)[1(𝕀)])[chi |⟶ (u)[1(𝕀)]]}

Latex:

Latex:
1. Gamma : CubicalSet\{j\} 2. phi : \{Gamma \mvdash{} \_:\mBbbF{}\} 3. psi : \{Gamma \mvdash{} \_:\mBbbF{}\} 4. A : \{Gamma, phi \mvdash{} \_\} 5. B : \{Gamma, psi \mvdash{} \_\} 6. cA : Gamma, phi \mvdash{} Compositon(A) 7. cB : Gamma, psi \mvdash{} Compositon(B) 8. Gamma, (phi \mwedge{} psi) \mvdash{} A = B 9. compatible-composition\{j:l, i:l\}(Gamma; phi; psi; A; B; cA; cB) 10. Gamma, (phi \mvee{} psi) \mvdash{} (if phi then A else B) 11. H : CubicalSet\{j\} 12. sigma : H.\mBbbI{} j{}\mrightarrow{} Gamma, (phi \mvee{} psi) 13. chi : \{H \mvdash{} \_:\mBbbF{}\} 14. H.\mBbbI{} \mvdash{} (1(\mBbbF{}) {}\mRightarrow{} ((phi)sigma \mvee{} (psi)sigma)) 15. (\mforall{} (phi)sigma) \mmember{} \{H \mvdash{} \_:\mBbbF{}\} 16. (\mforall{} (psi)sigma) \mmember{} \{H \mvdash{} \_:\mBbbF{}\} 17. H.\mBbbI{}, ((phi)sigma \mwedge{} (psi)sigma) \mvdash{} (A)sigma = (B)sigma 18. H.\mBbbI{} \mvdash{} ((if phi then A else B))sigma 19. H, chi.\mBbbI{} \mvdash{} ((if phi then A else B))sigma 20. u : \{H, chi.\mBbbI{} \mvdash{} \_:((if phi then A else B))sigma\} 21. a0 : \{H \mvdash{} \_:(((if phi then A else B))sigma)[0(\mBbbI{})][chi |{}\mrightarrow{} (u)[0(\mBbbI{})]]\} \mvdash{} (cA H, (\mforall{} (phi)sigma) sigma chi u a0 \mvee{} cB H, (\mforall{} (psi)sigma) sigma chi u a0) \mmember{} \{H \mvdash{} \_:(((if phi then A else B))sigma)[1(\mBbbI{})][chi |{}\mrightarrow{} (u)[1(\mBbbI{})]]\} By Latex: ((All (RWW "csm-case-type") THENA Auto) THEN (Assert u \mmember{} \{H, (\mforall{} (phi)sigma), chi.\mBbbI{} \mvdash{} \_:(A)sigma\} BY ((Assert u \mmember{} \{H, (\mforall{} (phi)sigma), chi.\mBbbI{} \mvdash{} \_ :(if (phi)sigma then (A)sigma else (B)sigma)\} BY ((DoSubsume THEN Try (Trivial)) THEN BLemma `subset-cubical-term` THEN Auto THEN BLemma `context-adjoin-subset` THEN Auto)) THEN InferEqualType THEN Try (Trivial) THEN EqCDA THEN (SubsumeC \mkleeneopen{}\{H.\mBbbI{}, (phi)sigma \mvdash{} \_\}\mkleeneclose{}\mcdot{} THENL [(Fold `same-cubical-type` 0 THEN Using [`psi',\mkleeneopen{}(psi)sigma\mkleeneclose{}] (BLemma `case-type-same1`)\mcdot{} THEN Auto); (BLemma `subset-cubical-type` THEN Auto THEN Using [`Y',\mkleeneopen{}H, (\mforall{} (phi)sigma).\mBbbI{}\mkleeneclose{} ] (BLemma `sub\_cubical\_set\_transitivity`)\mcdot{} THEN Auto)\mcdot{}]))) ) Home Index