Derivative.Basics.Unit

{-# OPTIONS --safe #-}
module Derivative.Basics.Unit where

open import Derivative.Prelude

open import Cubical.Foundations.Univalence

private
  variable
    β„“ : Level
    A : Type β„“

isContr-πŸ™* : isContr (πŸ™* {β„“})
isContr-πŸ™* .fst = β€’
isContr-πŸ™* .snd _ = refl

isOfHLevel-πŸ™* : βˆ€ n β†’ isOfHLevel n (πŸ™* {β„“})
isOfHLevel-πŸ™* n = isContrβ†’isOfHLevel n isContr-πŸ™*

isProp-πŸ™* : isProp (πŸ™* {β„“})
isProp-πŸ™* = isOfHLevel-πŸ™* 1

isSet-πŸ™* : isSet (πŸ™* {β„“})
isSet-πŸ™* = isOfHLevel-πŸ™* 2

πŸ™*-unit-Γ—-left-equiv : (πŸ™* {β„“} Γ— A) ≃ A
πŸ™*-unit-Γ—-left-equiv = strictEquiv (Ξ» { (β€’ , a) β†’ a }) (Ξ» a β†’ (β€’ , a))

isContrβ†’β‰‘πŸ™* : isContr A β†’ A ≑ πŸ™*
isContrβ†’β‰‘πŸ™* contr-A = ua $ (const β€’) , is-equiv-const where
  is-equiv-const : isEquiv (Ξ» _ β†’ β€’)
  is-equiv-const .equiv-proof β€’ .fst = contr-A .fst , refl
  is-equiv-const .equiv-proof β€’ .snd (a , p) = Ξ£PathP (contr-A .snd a , Ξ» i j β†’ β€’)