Notation 11.4.0.18. This tag became obsolete because the convention for $2$-categories of paths was changed.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Notation 11.4.0.18. This tag became obsolete because the convention for $2$-categories of paths was changed.