---

Step * 3 of Lemma subset-trans_wf

.....wf..... 
1. 𝔽 ∈ small_cubical_set{j:l}
2. I : fset(ℕ)
3. J : fset(ℕ)
4. f : J ⟶ I
5. psi : 𝔽(I)
6. trans : A:fset(ℕ) ⟶ {f@0:A ⟶ J| ((psi)<f> f@0) = 1}  ⟶ {f:A ⟶ I| (psi f) = 1} 
⊢ istype(∀A,B:fset(ℕ). ∀g:B ⟶ A.
           ((λx.trans A x ⋅ g) = (λx.(trans B x ⋅ g)) ∈ ({f@0:A ⟶ J| ((psi)<f> f@0) = 1}  ⟶ {f:B ⟶ I| (psi f) = 1} ))\000C)
BY
{ (RepeatFor 3 ((D 0 THENL [Auto; Id])) THEN EqualityIsType1 THEN Auto) }

1
1. 𝔽 ∈ small_cubical_set{j:l}
2. I : fset(ℕ)
3. J : fset(ℕ)
4. f : J ⟶ I
5. psi : 𝔽(I)
6. trans : A:fset(ℕ) ⟶ {f@0:A ⟶ J| ((psi)<f> f@0) = 1}  ⟶ {f:A ⟶ I| (psi f) = 1} 
7. A : fset(ℕ)
8. B : fset(ℕ)
9. g : B ⟶ A
10. ∀f@0:A ⟶ J. (((psi)<f> f@0) = 1 ∈ Type)
11. x : A ⟶ J
12. ((psi)<f> x) = 1
⊢ trans A x ⋅ g ∈ {f:B ⟶ I| (psi f) = 1} 

2
1. 𝔽 ∈ small_cubical_set{j:l}
2. I : fset(ℕ)
3. J : fset(ℕ)
4. f : J ⟶ I
5. psi : 𝔽(I)
6. trans : A:fset(ℕ) ⟶ {f@0:A ⟶ J| ((psi)<f> f@0) = 1}  ⟶ {f:A ⟶ I| (psi f) = 1} 
7. A : fset(ℕ)
8. B : fset(ℕ)
9. g : B ⟶ A
10. ∀f@0:A ⟶ J. (((psi)<f> f@0) = 1 ∈ Type)
11. x : A ⟶ J
12. ((psi)<f> x) = 1
⊢ x ⋅ g ∈ {f@0:B ⟶ J| ((psi)<f> f@0) = 1} 

---

Latex:

---

Latex:
.....wf..... 
1.  \mBbbF{}  \mmember{}  small\_cubical\_set\{j:l\}
2.  I  :  fset(\mBbbN{})
3.  J  :  fset(\mBbbN{})
4.  f  :  J  {}\mrightarrow{}  I
5.  psi  :  \mBbbF{}(I)
6.  trans  :  A:fset(\mBbbN{})  {}\mrightarrow{}  \{f@0:A  {}\mrightarrow{}  J|  ((psi)<f>  f@0)  =  1\}    {}\mrightarrow{}  \{f:A  {}\mrightarrow{}  I|  (psi  f)  =  1\} 
\mvdash{}  istype(\mforall{}A,B:fset(\mBbbN{}).  \mforall{}g:B  {}\mrightarrow{}  A.    ((\mlambda{}x.trans  A  x  \mcdot{}  g)  =  (\mlambda{}x.(trans  B  x  \mcdot{}  g))))


By

---

Latex:
(RepeatFor  3  ((D  0  THENL  [Auto;  Id]))  THEN  EqualityIsType1  THEN  Auto)

---

Home Index