28 lines
769 B
Agda
28 lines
769 B
Agda
{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}
|
||
|
||
module HoTT-UF-Agda where
|
||
open import Universes public
|
||
|
||
-- variable
|
||
-- 𝓤 𝓥 𝓦 𝓣 : Universe
|
||
|
||
-- data 𝟙 : 𝓤₀ ̇ where
|
||
-- ⋆ : 𝟙
|
||
|
||
-- 𝟙-induction : (A : 𝟙 → 𝓤̇ ) → A ⋆ → (x : 𝟙) → A x
|
||
-- 𝟙-induction A a ⋆ = a
|
||
|
||
-- 𝟙-induction : (A : 𝟙 → 𝓤 ̇) → A ⋆ → (x : 𝟙) → A x
|
||
-- 𝟙-induction A a ⋆ = a
|
||
|
||
-- 𝟙-induction : (A : 𝟙 → 𝓤 ̇) → A ⋆ → (x : 𝟙) → A x
|
||
-- 𝟙-induction A a ⋆ = a
|
||
|
||
variable
|
||
𝓤 𝓥 𝓦 𝓣 : Universe
|
||
|
||
data 𝟙 : 𝓤₀ ̇ where
|
||
⋆ : 𝟙
|
||
|
||
𝟙-induction : (A : 𝟙 → 𝓤 ̇ ) → A ⋆ → (x : 𝟙) → A x
|
||
𝟙-induction A a ⋆ = a |