module QWI where

{-
Here we give the indexed version of quotient inductive types,
QWI-types (section 3.3 in the paper) and their construction from
quotient and inductive types using the WISC axiom
-}

-- Section 3. Indexed Polynomial Functors and Equational Systems
open import QWI.IndexedPolynomialFunctorsAndEquationalSystems

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

-- Section 6. Construction of QWI-Types
open import QWI.SizeIndexedStructure
open import QWI.FixedPointsAreQWITypes
open import QWI.ConstructionOfQWITypes

-- Section 7. Encoding QITs as QWI-Types
open import QWI.EncodingQITsAsQWITypes