7
record Σ (A : Set) (P : A → Set) : Set where
12
data _≡_ {A : Set} : A → A → Set where
13
refl : (a : A) → a ≡ a
16
is-contr A = Σ A (λ x → ((y : A) → y ≡ x))
18
is-hlevel : (n : ℕ) → (Set → Set)
19
is-hlevel O A = is-contr A
20
is-hlevel (S n) A = (x y : A) → is-hlevel n (x ≡ y)
24
t-is-hlevel : {n : ℕ} {A : Set} → is-hlevel n (t n A)
26
f : (n : ℕ) (B : Set) ⦃ x : is-hlevel n B ⦄ → Set
29
g n = f n (t n A) {- ⦃ t-is-hlevel {n} ⦄ -}