replace WithK with a file in Axiom containing statement and consequences of UIP/K

Cubical/Axiom/UniquenessOfIdentity.agda

@@ -0,0 +1,58 @@
+{-
+
+Uniqueness of identity proofs and axiom K
+
+-}
+
+{-# OPTIONS --safe #-}
+
+module Cubical.Axiom.UniquenessOfIdentity where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Univalence
+open import Cubical.Data.Bool
+open import Cubical.Data.Empty
+open import Cubical.Relation.Nullary
+
+private
+ variable
+  ℓ : Level
+
+-- Define uniqueness of identity proofs and Axiom K for an individual type
+
+module _ (A : Type ℓ) where
+
+  UIP : Type ℓ
+  UIP = (x : A) (p : x ≡ x) → refl ≡ p
+
+  AxiomK : (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
+  AxiomK ℓ' = (x : A) (P : x ≡ x → Type ℓ') → P refl → (∀ p → P p)
+
+-- UIP, K, and isSet are logically equivalent
+
+module _ {A : Type ℓ} where
+
+  UIP→AxiomK : UIP A → ∀ ℓ' → AxiomK A ℓ'
+  UIP→AxiomK uip _ x P Prefl p = subst P (uip x p) Prefl
+
+  AxiomK→UIP : AxiomK A ℓ → UIP A
+  AxiomK→UIP K x p = K x (refl ≡_) refl p
+
+  UIP→isSet : UIP A → isSet A
+  UIP→isSet uip x = J> (uip x)
+
+  isSet→UIP : isSet A → UIP A
+  isSet→UIP setA x p = setA _ _ _ _
+
+-- Univalence implies that universes fail UIP
+
+¬UIPType : ∀ {ℓ} → ¬ UIP (Type ℓ)
+¬UIPType {ℓ} uip =
+  false≢true (cong lower (transport-uip p (lift true)))
+  where
+  B = Lift {j = ℓ} Bool
+  p = cong (Lift {j = ℓ}) (ua notEquiv)
+
+  transport-uip : (p : B ≡ B) → ∀ b → transport p b ≡ b
+  transport-uip = UIP→AxiomK uip _ B _ transportRefl

GNUmakefile

@@ -51,7 +51,6 @@ check-README:
 .PHONY : check
 check: gen-everythings
 	$(AGDA) Cubical/README.agda
-	$(AGDA) Cubical/WithK.agda
 
 .PHONY : timings
 timings: clean gen-everythings