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
|