---

Step * of Lemma csm-fibrant-type-id

No Annotations
∀[G:j⊢]. ∀[FT:FibrantType(G)]. ∀[tau:G j⟶ G].
  csm-fibrant-type(G;G;tau;FT) = FT ∈ FibrantType(G) supposing tau = 1(G) ∈ G j⟶ G
BY
{ (Auto
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN ThinVar `tau'
   THEN D -1
   THEN RepUR ``csm-fibrant-type`` 0
   THEN Unfold `fibrant-type` 0
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[FT:FibrantType(G)].  \mforall{}[tau:G  j{}\mrightarrow{}  G].
    csm-fibrant-type(G;G;tau;FT)  =  FT  supposing  tau  =  1(G)


By

---

Latex:
(Auto
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  ThinVar  `tau'
  THEN  D  -1
  THEN  RepUR  ``csm-fibrant-type``  0
  THEN  Unfold  `fibrant-type`  0
  THEN  EqCD
  THEN  Auto)

---

Home Index