---

Step * of Lemma cubical-set-eqs-istype

∀[XF:X:L:(Cname List) ⟶ Type × (I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J))]
  istype(let X,F = XF 
         in (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
               ((F I K (f o g)) = ((F J K g) o (F I J f)) ∈ ((X I) ⟶ (X K))))
            ∧ (∀I:Cname List. ((F I I 1) = (λx.x) ∈ ((X I) ⟶ (X I)))))
BY
{ ((Intro THEN D -1) THEN Reduce 0 THEN RepeatFor 2 (D 0) THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:
\mforall{}[XF:X:L:(Cname  List)  {}\mrightarrow{}  Type  \mtimes{}  (I:(Cname  List)
                                                                {}\mrightarrow{}  J:(Cname  List)
                                                                {}\mrightarrow{}  name-morph(I;J)
                                                                {}\mrightarrow{}  (X  I)
                                                                {}\mrightarrow{}  (X  J))]
    istype(let  X,F  =  XF 
                  in  (\mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).
                              ((F  I  K  (f  o  g))  =  ((F  J  K  g)  o  (F  I  J  f))))
                        \mwedge{}  (\mforall{}I:Cname  List.  ((F  I  I  1)  =  (\mlambda{}x.x))))


By

---

Latex:
((Intro  THEN  D  -1)  THEN  Reduce  0  THEN  RepeatFor  2  (D  0)  THEN  Try  (Complete  (Auto)))

---

Home Index