# -*- mode: snippet -*- # name: __cubical # key: __cubical # -- {-# OPTIONS --safe --guardedness --cubical --without-K #-} module ${1:Module} where open import Cubical.Foundations.Prelude -- open import Cubical.Data.Sigma -- open import Cubical.HITs.PropositionalTruncation -- open import Cubical.Foundations.Function -- open import Cubical.Foundations.Function private variable ℓ ℓ' ℓ'' : Level $2