{-# 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