------------------------------------------------------------------------
-- Safe modules that use --cubical
------------------------------------------------------------------------

{-# OPTIONS --safe --cubical #-}

module README.Safe.Cubical where

-- A proof of univalence.

import Equality.Path.Univalence

-- A proof of univalence for an arbitrary "equality with J".

import Equality.Path.Isomorphisms.Univalence

-- Very stable booleans.

import Bool.Very-stable

-- A membership relation for listed finite subsets (defined using
-- non-erased univalence).

import Finite-subset.Listed.Membership

-- An alternative definition of listed finite subsets.

import Finite-subset.Listed.Alternative

-- A membership relation for Kuratowski finite subsets (defined using
-- non-erased univalence).

import Finite-subset.Kuratowski.Membership

-- An example related to Nat.Wrapper, defined in Cubical Agda.

import Nat.Wrapper.Cubical

-- Overview of code related to a paper.

import README.HITs-without-paths