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 = (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 β†’ β€’)

isContrβ†’β‰‘πŸ™* : isContr A β†’ A ≑ πŸ™*
isContrβ†’β‰‘πŸ™* contr-A = ua $ isContrβ†’β‰ƒπŸ™* contr-A

Ξ πŸ™*-equiv : βˆ€ {β„“A} (A : πŸ™* {β„“} β†’ Type β„“A) β†’ (βˆ€ t β†’ A t) ≃ (A β€’)
Ξ πŸ™*-equiv A = strictIsoToEquiv iso module Ξ πŸ™*-equiv where
  iso : Iso _ _
  iso .Iso.fun = _$ β€’
  iso .Iso.inv = const
  iso .Iso.rightInv _ = refl
  iso .Iso.leftInv _ = refl