Remove Pathy and Bij

src/Cat.agda

@@ -7,8 +7,6 @@ import Cat.Category.Product
 import Cat.Category.Exponential
 import Cat.Category.CartesianClosed
 import Cat.Category.NaturalTransformation
-import Cat.Category.Pathy
-import Cat.Category.Bij
 import Cat.Category.Yoneda
 import Cat.Category.Monad
 

src/Cat/Category/Bij.agda

@@ -1,46 +0,0 @@
-{-# OPTIONS --cubical --allow-unsolved-metas #-}
-
-module Cat.Category.Bij where
-
-open import Cubical hiding ( Id )
-open import Cubical.FromStdLib
-
-module _ {A : Set} {a : A} {P : A → Set} where
-  Q : A → Set
-  Q a = A
-
-  t : Σ[ a ∈ A ] P a → Q a
-  t (a , Pa) = a
-  u : Q a → Σ[ a ∈ A ] P a
-  u a = a , {!!}
-
-  tu-bij : (a : Q a) → (t ∘ u) a ≡ a
-  tu-bij a = refl
-
-  v : P a → Q a
-  v x = {!!}
-  w : Q a → P a
-  w x = {!!}
-
-  vw-bij : (a : P a) → (w ∘ v) a ≡ a
-  vw-bij a = {!!}
-  -- tubij a with (t ∘ u) a
-  -- ... | q = {!!}
-
-  data Id {A : Set} (a : A) : Set where
-    id : A → Id a
-
-  data Id' {A : Set} (a : A) : Set where
-    id' : A → Id' a
-
-  T U : Set
-  T = Id a
-  U = Id' a
-
-  f : T → U
-  f (id x) = id' x
-  g : U → T
-  g (id' x) = id x
-
-  fg-bij : (x : U) → (f ∘ g) x ≡ x
-  fg-bij (id' x) = {!!}

src/Cat/Category/Pathy.agda

@@ -1,53 +0,0 @@
-{-# OPTIONS --cubical #-}
-
-module Cat.Category.Pathy where
-
-open import Level
-open import Cubical
-
-{-
-module _ {ℓ ℓ'} {A : Set ℓ} {x : A}
-  (P : ∀ y → x ≡ y → Set ℓ') (d : P x ((λ i → x))) where
-  pathJ' : (y : A) → (p : x ≡ y) → P y p
-  pathJ' _ p = transp (λ i → uncurry P (contrSingl p i)) d
-
-  pathJprop' : pathJ' _ refl ≡ d
-  pathJprop' i
-    = primComp (λ _ → P x refl) i (λ {j (i = i1) → d}) d
-
-
-module _ {ℓ ℓ'} {A : Set ℓ}
-  (P : (x y : A) → x ≡ y → Set ℓ') (d : (x : A) → P x x refl) where
-  pathJ'' : (x y : A) → (p : x ≡ y) → P x y p
-  pathJ'' _ _ p = transp (λ i →
-    let
-      P' = uncurry P
-      q  = (contrSingl p i)
-    in
-      {!uncurry (uncurry P)!} ) d
--}
-
-module _ {ℓ ℓ'} {A : Set ℓ}
-  (C : (x y : A) → x ≡ y → Set ℓ')
-  (c : (x : A) → C x x refl) where
-
-  =-ind : (x y : A) → (p : x ≡ y) → C x y p
-  =-ind x y p = pathJ (C x) (c x) y p
-
-module _ {ℓ ℓ' : Level} {A : Set ℓ} {P : A → Set ℓ} {x y : A} where
-  private
-    D : (x y : A) → (x ≡ y) → Set ℓ
-    D x y p = P x → P y
-
-    id : {ℓ : Level} → {A : Set ℓ} → A → A
-    id x = x
-
-    d : (x : A) → D x x refl
-    d x = id {A = P x}
-
-  -- the p refers to the third argument
-  liftP : x ≡ y → P x → P y
-  liftP p = =-ind D d x y p
-
-  -- lift' : (u : P x) → (p : x ≡ y) → (x , u) ≡ (y , liftP p u)
-  -- lift' u p = {!!}