19 lines
414 B
Plaintext
19 lines
414 B
Plaintext
# -*- 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 |