{-# OPTIONS --no-exact-split --safe #-} module Cubical.HITs.InfNat where open import Cubical.HITs.InfNat.Base public open import Cubical.HITs.InfNat.Properties public