---

Step * 2 of Lemma cubical-type-ap-morph-comp-eq-general

.....subterm..... T:t
2:n
1. X : CubicalSet{j}
2. A : {X ⊢j _}
3. I : fset(ℕ)
4. J : fset(ℕ)
5. K : fset(ℕ)
6. f : J ⟶ I
7. g : K ⟶ J
8. a : X(I)
9. b : X(J)
10. u : A(a)
11. b = f(a) ∈ X(J)
12. b = f(a) ∈ {z:X(J)| (z = b ∈ X(J)) ∧ (z = f(a) ∈ X(J))} 
13. z : X(J)
14. (z = b ∈ X(J)) ∧ (z = f(a) ∈ X(J))
⊢ ((u a f) z g) ∈ A(f ⋅ g(a))
BY
{ InferEqualType_j }

1
1. X : CubicalSet{j}
2. A : {X ⊢j _}
3. I : fset(ℕ)
4. J : fset(ℕ)
5. K : fset(ℕ)
6. f : J ⟶ I
7. g : K ⟶ J
8. a : X(I)
9. b : X(J)
10. u : A(a)
11. b = f(a) ∈ X(J)
12. b = f(a) ∈ {z:X(J)| (z = b ∈ X(J)) ∧ (z = f(a) ∈ X(J))} 
13. z : X(J)
14. (z = b ∈ X(J)) ∧ (z = f(a) ∈ X(J))
⊢ A(g(z)) = A(f ⋅ g(a)) ∈ 𝕌{j}

2
1. X : CubicalSet{j}
2. A : {X ⊢j _}
3. I : fset(ℕ)
4. J : fset(ℕ)
5. K : fset(ℕ)
6. f : J ⟶ I
7. g : K ⟶ J
8. a : X(I)
9. b : X(J)
10. u : A(a)
11. b = f(a) ∈ X(J)
12. b = f(a) ∈ {z:X(J)| (z = b ∈ X(J)) ∧ (z = f(a) ∈ X(J))} 
13. z : X(J)
14. (z = b ∈ X(J)) ∧ (z = f(a) ∈ X(J))
15. A(g(z)) = A(f ⋅ g(a)) ∈ 𝕌{j}
⊢ ((u a f) z g) ∈ A(g(z))

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  X  :  CubicalSet\{j\}
2.  A  :  \{X  \mvdash{}j  \_\}
3.  I  :  fset(\mBbbN{})
4.  J  :  fset(\mBbbN{})
5.  K  :  fset(\mBbbN{})
6.  f  :  J  {}\mrightarrow{}  I
7.  g  :  K  {}\mrightarrow{}  J
8.  a  :  X(I)
9.  b  :  X(J)
10.  u  :  A(a)
11.  b  =  f(a)
12.  b  =  f(a)
13.  z  :  X(J)
14.  (z  =  b)  \mwedge{}  (z  =  f(a))
\mvdash{}  ((u  a  f)  z  g)  \mmember{}  A(f  \mcdot{}  g(a))


By

---

Latex:
InferEqualType\_j

---

Home Index