---

Step * of Lemma csm-rev-type-line

No Annotations
∀[G,K:j⊢]. ∀[A:{G.𝕀 ⊢ _}]. ∀[tau:K j⟶ G].  (((A)-)tau+ = ((A)tau+)- ∈ {K.𝕀 ⊢ _})
BY
{ (Auto
   THEN (Assert ⌜((A)-)tau+
                 = ((A)tau+)-
                 ∈ (A:I:fset(ℕ) ⟶ K.𝕀(I) ⟶ Type × (I:fset(ℕ)
                                                    ⟶ J:fset(ℕ)
                                                    ⟶ f:J ⟶ I
                                                    ⟶ a:K.𝕀(I)
                                                    ⟶ (A I a)
                                                    ⟶ (A J f(a))))⌝⋅
   THENM (BLemma `cubical-type-equal` THEN Auto)
   )
   THEN RepUR ``csm-ap-type rev-type-line`` 0
   THEN CsmUnfolding) }

1
1. G : CubicalSet{j}
2. K : CubicalSet{j}
3. A1 : I:fset(ℕ) ⟶ G.𝕀(I) ⟶ Type
4. A2 : I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:G.𝕀(I) ⟶ (A1 I a) ⟶ (A1 J f(a))
5. let A,F = <A1, A2> 
   in (∀I:fset(ℕ). ∀a:G.𝕀(I). ∀u:A I a.  ((F I I 1 a u) = u ∈ (A I a)))
      ∧ (∀I,J,K:fset(ℕ). ∀f:J ⟶ I. ∀g:K ⟶ J. ∀a:G.𝕀(I). ∀u:A I a.
           ((F I K f ⋅ g a u) = (F J K g f(a) (F I J f a u)) ∈ (A K f ⋅ g(a))))
6. tau : K j⟶ G
⊢ <λI,a. (A1 I <tau I (fst(a)), ¬(snd(a))>), λI,J,f,a,u. (A2 I J f <tau I (fst(a)), ¬(snd(a))> u)>
= <λI,a. (A1 I <tau I (fst(a)), ¬(snd(a))>), λI,J,f,a,u. (A2 I J f <tau I (fst(a)), ¬(snd(a))> u)>
∈ (A:I:fset(ℕ) ⟶ K.<λI,alpha. 𝕀(I), λI,J,f,alpha,w. f(w)>(I) ⟶ Type × (I:fset(ℕ)
                                                ⟶ J:fset(ℕ)
                                                ⟶ f:J ⟶ I
                                                ⟶ a:K.<λI,alpha. 𝕀(I), λI,J,f,alpha,w. f(w)>(I)
                                                ⟶ (A I a)
                                                ⟶ (A J f(a))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G,K:j\mvdash{}].  \mforall{}[A:\{G.\mBbbI{}  \mvdash{}  \_\}].  \mforall{}[tau:K  j{}\mrightarrow{}  G].    (((A)-)tau+  =  ((A)tau+)-)


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}((A)-)tau+  =  ((A)tau+)-\mkleeneclose{}\mcdot{}  THENM  (BLemma  `cubical-type-equal`  THEN  Auto))
  THEN  RepUR  ``csm-ap-type  rev-type-line``  0
  THEN  CsmUnfolding)

---

Home Index