{-# 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