⊤set.agda

{-# OPTIONS --without-K #-}

open import Agda.Primitive

private variable
  ℓ ℓ' : Level
  A B : Set ℓ

data _≡_ {A : Set ℓ} : A → A → Set ℓ where
  refl : {a : A} → a ≡ a

data _≡[_]_ {A : Set ℓ} {B : A → Set ℓ'} : {x y : A} → B x → (p : x ≡ y) → B y → Set (ℓ ⊔ ℓ') where
  reflrefl : {a : A} {b : B a} → b ≡[ refl ] b

apd : {B : A → Set ℓ} {x y : A} → (f : (a : A) → B a) → (p : x ≡ y) → f x ≡[ p ] f y
apd f refl = reflrefl

transpose : {x : A} {p : x ≡ x} (pp : _≡[_]_ {B = λ y → y ≡ x} refl p refl) → p ≡ refl
transpose reflrefl = refl

data ⊤ : Set where
  ⋆ : ⊤

⊤contractible : (t : ⊤) → t ≡ ⋆
⊤contractible ⋆ = refl

⊤set : (p : ⋆ ≡ ⋆) → p ≡ refl
⊤set p = transpose (apd ⊤contractible p)