module README where

-- Definitions of k-restricted semi-Segal types and wild
-- (k-2)-semicategories and proofs of their equivalence
import segal.composition

-- Definitions of k-degeneracy and k-identity structures for semi-Segal types
-- and wild semicategories respectively, and proofs of their equivalence
import segal.identities

-- Summary of the notions and equivalences proved:
-- Definitions of semi-Segal types with degeneracies (denoted `SegalDeg`),
-- wild precategories (denoted `WildId`), and their equivalences.
import segal.equivalences

-- Univalence for wild precategories
import segal.univalence