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