{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Everything where

-- Basic cubical prelude
open import Cubical.Foundations.Prelude public

-- Definition of Identity types and definitions of J, funExt,
-- univalence and propositional truncation using Id instead of Path
open import Cubical.Foundations.Id
  hiding ( _≡_ ; _≡⟨_⟩_ ; _∎ )
  renaming ( _≃_           to EquivId
           ; EquivContr    to EquivContrId
           ; J             to JId
           ; ap            to apId
           ; equivFun      to equivFunId
           ; equivCtr      to equivCtrId
           ; fiber         to fiberId
           ; funExt        to funExtId
           ; isContr       to isContrId
           ; isProp        to isPropId
           ; isSet         to isSetId
           ; isEquiv       to isEquivId
           ; equivIsEquiv  to equivIsEquivId
           ; refl          to reflId
           ; ∥_∥           to propTruncId
           ; ∣_∣           to incId
           ; isPropIsContr to isPropIsContrId
           ; isPropIsEquiv to isPropIsEquivId
           )

open import Cubical.Foundations.GroupoidLaws public
open import Cubical.Foundations.Function public
open import Cubical.Foundations.Equiv public
open import Cubical.Foundations.Equiv.Properties public
open import Cubical.Foundations.Equiv.Fiberwise
open import Cubical.Foundations.Equiv.PathSplit public
open import Cubical.Foundations.Equiv.BiInvertible public
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels public
open import Cubical.Foundations.Path public
open import Cubical.Foundations.Pointed public
open import Cubical.Foundations.RelationalStructure public
open import Cubical.Foundations.Structure public
open import Cubical.Foundations.Transport public
open import Cubical.Foundations.Univalence public
open import Cubical.Foundations.Univalence.Universe
open import Cubical.Foundations.GroupoidLaws public
open import Cubical.Foundations.Isomorphism public
open import Cubical.Foundations.CartesianKanOps
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.SIP