module QW where

{-
Here we give the non-indexed version of quotient inductive types,
QW-types and their construction from quotient and inductive types
using the WISC axiom
-}

-- Section 3. Indexed Polynomial Functors and Equational Systems
open import QW.PolynomialFunctorsAndEquationalSystems

-- Section 5. Size
open import QW.Size
open import QW.ColimitsOfSizedIndexedDiagrams

-- Section 6. Construction of QW-Types
open import QW.SizeIndexedStructure
open import QW.FixedPointsAreQWTypes
open import QW.ConstructionOfQWTypes

-- Section 7. Encoding QITs as QW-Types
open import QW.EncodingQITsAsQWTypes