{-# OPTIONS --cubical #-}


open import Cubical.Foundations.Prelude public
     using (_≡_) renaming (_∙_ to _∙₂_)

open import Cubical.Data.Equality public
     using (eqToPath) -- S¹-rec)

open import Cubical.HITs.S1 public
     using () renaming (S¹ to S¹'; rec to S¹-rec)

-- cheat
data String : Set where