{-# OPTIONS --safe #-}
module Cubical.Data.Unit.Properties where
open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Data.Nat
open import Cubical.Data.Unit.Base
open import Cubical.Data.Prod.Base
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence
open import Cubical.Reflection.StrictEquiv
open Iso
private
  variable
     ℓ' : Level
isContrUnit : isContr Unit
isContrUnit = tt , λ {tt  refl}
isPropUnit : isProp Unit
isPropUnit _ _ i = tt -- definitionally equal to: isContr→isProp isContrUnit
isSetUnit : isSet Unit
isSetUnit = isProp→isSet isPropUnit
isOfHLevelUnit : (n : HLevel)  isOfHLevel n Unit
isOfHLevelUnit n = isContr→isOfHLevel n isContrUnit
module _ (A : Type ) where
  UnitToType≃ : (Unit  A)  A
  unquoteDef UnitToType≃ = defStrictEquiv UnitToType≃  f  f _) const
UnitToTypePath :  {} (A : Type )  (Unit  A)  A
UnitToTypePath A = ua (UnitToType≃ A)
module _ (A : Unit  Type ) where
  open Iso
  ΠUnitIso : Iso ((x : Unit)  A x) (A tt)
  fun ΠUnitIso f = f tt
  inv ΠUnitIso a tt = a
  rightInv ΠUnitIso a = refl
  leftInv ΠUnitIso f = refl
  ΠUnit : ((x : Unit)  A x)  A tt
  ΠUnit = isoToEquiv ΠUnitIso
module _ (A : Unit* {}  Type ℓ') where
  open Iso
  ΠUnit*Iso : Iso ((x : Unit*)  A x) (A tt*)
  fun ΠUnit*Iso f = f tt*
  inv ΠUnit*Iso a tt* = a
  rightInv ΠUnit*Iso a = refl
  leftInv ΠUnit*Iso f = refl
  ΠUnit* : ((x : Unit*)  A x)  A tt*
  ΠUnit* = isoToEquiv ΠUnit*Iso
fiberUnitIso : {A : Type }  Iso (fiber  (a : A)  tt) tt) A
fun fiberUnitIso = fst
inv fiberUnitIso a = a , refl
rightInv fiberUnitIso _ = refl
leftInv fiberUnitIso _ = refl
isContr→Iso2 : {A : Type } {B : Type ℓ'}  isContr A  Iso (A  B) B
fun (isContr→Iso2 iscontr) f = f (fst iscontr)
inv (isContr→Iso2 iscontr) b _ = b
rightInv (isContr→Iso2 iscontr) _ = refl
leftInv (isContr→Iso2 iscontr) f = funExt λ x  cong f (snd iscontr x)
diagonal-unit : Unit  Unit × Unit
diagonal-unit = isoToPath (iso  x  tt , tt)  x  tt)  {(tt , tt) i  tt , tt}) λ {tt i  tt})
fibId : (A : Type )  (fiber  (x : A)  tt) tt)  A
fibId A = ua e
  where
  unquoteDecl e = declStrictEquiv e fst  a  a , refl)
isContr→≃Unit : {A : Type }  isContr A  A  Unit
isContr→≃Unit contr = isoToEquiv (iso  _  tt)  _  fst contr)  _  refl) λ _  snd contr _)
isContr→≡Unit : {A : Type₀}  isContr A  A  Unit
isContr→≡Unit contr = ua (isContr→≃Unit contr)
isContrUnit* :  {}  isContr (Unit* {})
isContrUnit* = tt* , λ _  refl
isPropUnit* :  {}  isProp (Unit* {})
isPropUnit* _ _ = refl
isSetUnit* :  {}  isSet (Unit* {})
isSetUnit* _ _ _ _ = refl
isOfHLevelUnit* :  {} (n : HLevel)  isOfHLevel n (Unit* {})
isOfHLevelUnit* zero = tt* , λ _  refl
isOfHLevelUnit* (suc zero) _ _ = refl
isOfHLevelUnit* (suc (suc zero)) _ _ _ _ _ _ = tt*
isOfHLevelUnit* (suc (suc (suc n))) = isOfHLevelPlus 3 (isOfHLevelUnit* n)
Unit≃Unit* :  {}  Unit  Unit* {}
Unit≃Unit* = invEquiv (isContr→≃Unit isContrUnit*)
isContr→≃Unit* : {A : Type }  isContr A  A  Unit* {}
isContr→≃Unit* contr = compEquiv (isContr→≃Unit contr) Unit≃Unit*
isContr→≡Unit* : {A : Type }  isContr A  A  Unit*
isContr→≡Unit* contr = ua (isContr→≃Unit* contr)