---

Step * 1 4 of Lemma subset-iota-is-id


1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. v : {H, phi ⊢ _}
⊢ v
= (v)iota
∈ (A:I:fset(ℕ) ⟶ H, phi(I) ⟶ Type × (I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:H, phi(I) ⟶ (A I a) ⟶ (A J f(a))))
BY
{ (RepeatFor 2 (DVar `v') THEN All Reduce THEN RepUR ``csm-ap-type csm-ap subset-iota`` 0 THEN EqCD THEN Auto) }

1
1. H : CubicalSet{j}
2. phi : {H ⊢ _:𝔽}
3. A : I:fset(ℕ) ⟶ H, phi(I) ⟶ Type
4. v1 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:H, phi(I) ⟶ (A I a) ⟶ (A J f(a))
5. ∀I:fset(ℕ). ∀a:H, phi(I). ∀u:A I a.  ((v1 I I 1 a u) = u ∈ (A I a))
6. ∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:H, phi(I). ∀u:A I a.
     ((v1 I K f ⋅ g a u) = (v1 J K g f(a) (v1 I J f a u)) ∈ (A K f ⋅ g(a)))
⊢ v1 = (λI,J,f,a,u. (v1 I J f a u)) ∈ (I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:H, phi(I) ⟶ (A I a) ⟶ (A J f(a)))

---

Latex:

---

Latex:

1.  H  :  CubicalSet\{j\}
2.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
3.  v  :  \{H,  phi  \mvdash{}  \_\}
\mvdash{}  v  =  (v)iota


By

---

Latex:
(RepeatFor  2  (DVar  `v')
  THEN  All  Reduce
  THEN  RepUR  ``csm-ap-type  csm-ap  subset-iota``  0
  THEN  EqCD
  THEN  Auto)

---

Home Index