∀[A,B:Type]. ∀[f:A ⟶ B].  ((f o Id{A}) = f ∈ (A ⟶ B))
{ Unfold `tidentity` 0 }
∀[A,B:Type]. ∀[f:A ⟶ B].  ((f o Id) = f ∈ (A ⟶ B))