Remove mentions of the Id type

Cubical/Core/Everything.agda

@@ -6,6 +6,3 @@ open import Cubical.Core.Primitives public
 
 -- Definition of equivalences and Glue types
 open import Cubical.Core.Glue public
-
--- Definition of cubical Identity types
-open import Cubical.Core.Id

Cubical/Data/Equality.agda

@@ -76,6 +76,14 @@ apd f refl = refl
 congPathd : {C : A → Type ℓ} (f : (x : A) → C x) {x y : A} (p : Path A x y) → Path (C y) (substPath C p (f x)) (f y)
 congPathd f p = fromPathP (congPath f p)
 
+module _ {x : A} (P : ∀ (y : A) → x ≡ y → Type ℓ') (d : P x refl) where
+  J : ∀ {y : A} (w : x ≡ y) → P y w
+  J {y = y} refl = d
+
+  -- Check that J of refl is the identity function
+  Jdefeq : Path _ (J refl) d
+  Jdefeq _ = d
+
 -- Equality between Path and equality
 eqToPath : {x y : A} → x ≡ y → Path A x y
 eqToPath refl = reflPath

Cubical/Experiments/HoTT-UF.agda

@@ -16,44 +16,41 @@ For the moment, this requires the development version of Agda.
 module Cubical.Experiments.HoTT-UF where
 
 open import Cubical.Core.Primitives hiding ( _≡_ )
-open import Cubical.Core.Id public
-
-open import Cubical.Foundations.Id public
-     using ( _≡_            -- The identity type.
-           ; refl           -- Unfortunately, pattern matching on refl is not available.
-           ; J              -- Until it is, you have to use the induction principle J.
-
-           ; transport      -- As in the HoTT Book.
-           ; ap
-           ; _∙_
-           ; _⁻¹
-
-           ; _≡⟨_⟩_         -- Standard equational reasoning.
-           ; _∎
-
-           ; funExt         -- Function extensionality
-                            -- (can also be derived from univalence).
-
-           ; Σ              -- Sum type. Needed to define contractible types, equivalences
-           ; _,_            -- and univalence.
-           ; pr₁            -- The eta rule is available.
-           ; pr₂
-
-           ; isProp         -- The usual notions of proposition, contractible type, set.
-           ; isContr
-           ; isSet
-
-           ; isEquiv        -- A map with contractible fibers
-                            -- (Voevodsky's version of the notion).
-           ; _≃_            -- The type of equivalences between two given types.
-           ; EquivContr     -- A formulation of univalence.
-
-           ; ∥_∥₁            -- Propositional truncation.
-           ; ∣_∣₁             -- Map into the propositional truncation.
-           ; ∥∥-isProp       -- A truncated type is a proposition.
-           ; ∥∥-recursion    -- Non-dependent elimination.
-           ; ∥∥-induction    -- Dependent elimination.
-           )
+  renaming ( fst to pr₁ ; snd to pr₂ )
+
+open import Cubical.Data.Equality using
+  ( _≡_            -- The identity type.
+  ; refl           -- Pattern matching on refl is available.
+  ; J              -- You can also use the induction principle J.
+
+  ; transport      -- As in the HoTT Book.
+  ; ap
+  ; _∙_
+
+  ; _≡⟨_⟩_         -- Standard equational reasoning.
+  ; _∎
+
+  ; funExt         -- Function extensionality
+                  -- (can also be derived from univalence).
+
+  ; isProp         -- The usual notions of proposition, contractible type, set.
+  ; isContr
+  ; isSet
+
+  ; isEquiv        -- A map with contractible fibers
+                  -- (Voevodsky's version of the notion).
+  ; _≃_           -- The type of equivalences between two given types.
+  ; univalenceEq  -- A formulation of univalence.
+
+  ; ∥_∥₁            -- Propositional truncation.
+  ; ∣_∣₁             -- Map into the propositional truncation.
+  ; ∥∥-isProp       -- A truncated type is a proposition.
+  ; ∥∥-recursion    -- Non-dependent elimination.
+  ; ∥∥-induction    -- Dependent elimination.
+  )
+  renaming
+  ( sym to _⁻¹ )
+  public
 
 {-
 

Cubical/Foundations/Everything.agda

@@ -4,30 +4,6 @@ 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.Function public
 open import Cubical.Foundations.Equiv public
 open import Cubical.Foundations.Equiv.Properties public