\import Category
\import Paths
\import Paths.Meta
\import Set.SetCategory

-- | Proves univalence for categories. The type of objects must extend `BaseSet` and the Hom-set must extend `SetHom` with properties only.
\meta sip => _ (exts, Map.dom, Map.cod, Map.f, Iso, SplitMono.hinv, Iso.f_hinv, SplitMono.hinv_f, SIP_Set, transport, Jl, *>, Cat.makeUnivalence)