Step * 2 of Lemma csm-constrained-cubical-term


1. [Gamma] CubicalSet{j}
2. [K] CubicalSet{j}
3. [s] j⟶ Gamma
4. [A] {Gamma ⊢ _}
5. [phi] {Gamma ⊢ _:𝔽}
6. Gamma, phi ⊢ A
⊢ ∀[t:{Gamma, phi ⊢ _:A}]. ∀[v:{Gamma ⊢ _:A[phi |⟶ t]}].  ((v)s ∈ {K ⊢ _:(A)s[(phi)s |⟶ (t)s]})
BY
(Intros THEN (MemTypeCD THENL [Auto; Id; (EqualityIsType1 THEN Auto)])) }

1
.....set predicate..... 
1. Gamma CubicalSet{j}
2. CubicalSet{j}
3. j⟶ Gamma
4. {Gamma ⊢ _}
5. phi {Gamma ⊢ _:𝔽}
6. Gamma, phi ⊢ A
7. {Gamma, phi ⊢ _:A}
8. {Gamma ⊢ _:A[phi |⟶ t]}
⊢ (t)s (v)s ∈ {K, (phi)s ⊢ _:(A)s}

2
1. Gamma CubicalSet{j}
2. CubicalSet{j}
3. j⟶ Gamma
4. {Gamma ⊢ _}
5. phi {Gamma ⊢ _:𝔽}
6. Gamma, phi ⊢ A
7. {Gamma, phi ⊢ _:A}
8. {Gamma ⊢ _:A[phi |⟶ t]}
9. {K ⊢ _:(A)s}
⊢ a ∈ {K, (phi)s ⊢ _:(A)s}


Latex:


Latex:

1.  [Gamma]  :  CubicalSet\{j\}
2.  [K]  :  CubicalSet\{j\}
3.  [s]  :  K  j{}\mrightarrow{}  Gamma
4.  [A]  :  \{Gamma  \mvdash{}  \_\}
5.  [phi]  :  \{Gamma  \mvdash{}  \_:\mBbbF{}\}
6.  Gamma,  phi  \mvdash{}  A
\mvdash{}  \mforall{}[t:\{Gamma,  phi  \mvdash{}  \_:A\}].  \mforall{}[v:\{Gamma  \mvdash{}  \_:A[phi  |{}\mrightarrow{}  t]\}].    ((v)s  \mmember{}  \{K  \mvdash{}  \_:(A)s[(phi)s  |{}\mrightarrow{}  (t)s]\})


By


Latex:
(Intros  THEN  (MemTypeCD  THENL  [Auto;  Id;  (EqualityIsType1  THEN  Auto)]))




Home Index