New notion of equivalence: Bijective relations

Cubical/Foundations/Equiv/BijectiveRel.agda

@@ -0,0 +1,150 @@
+{-
+
+Bijective Relations ([BijectiveRel])
+
+- Path to BijectiveRel ([pathToBijectiveRel])
+- BijectiveRel is equivalent to Equiv ([BijectiveRel≃Equiv])
+
+-}
+module Cubical.Foundations.Equiv.BijectiveRel where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Univalence.Dependent
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Functions.FunExtEquiv
+open import Cubical.Relation.Binary
+open import Cubical.Reflection.RecordEquiv
+open import Cubical.Reflection.StrictEquiv
+open import Cubical.Data.Sigma
+
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B C : Type ℓ
+  R S : Rel A B ℓ
+
+open HeterogenousRelation
+
+record isBijectiveRel {A : Type ℓ} {B : Type ℓ'} (R : Rel A B ℓ'') : Type (ℓ-max ℓ (ℓ-max ℓ' ℓ'')) where
+  field
+    rContr : isFunctionalRel R
+    lContr : isFunctionalRel (flip R)
+
+  fun : A → B
+  fun a = rContr a .fst .fst
+
+  inv : B → A
+  inv b = lContr b .fst .fst
+
+  funR : ∀ a → R a (fun a)
+  funR a = rContr a .fst .snd
+
+  invR : ∀ b → R (inv b) b
+  invR b = lContr b .fst .snd
+
+  rightIsId : ∀ a → isIdentitySystem (fun a) (R a) (funR a)
+  rightIsId a = isContrTotal→isIdentitySystem (rContr a)
+
+  module _ (a : A) where
+    open isIdentitySystem (rightIsId a) using ()
+      renaming (isoPath to rightIsoPath; equivPath to rightEquivPath) public
+
+  leftIsId : ∀ b → isIdentitySystem (inv b) (flip R b) (invR b)
+  leftIsId b = isContrTotal→isIdentitySystem (lContr b)
+
+  module _ (b : B) where
+    open isIdentitySystem (leftIsId b) using ()
+      renaming (isoPath to leftIsoPath; equivPath to leftEquivPath) public
+
+  isEquivFun : isEquiv fun
+  isEquivFun .equiv-proof b = isOfHLevelRetractFromIso 0 (Σ-cong-iso-snd (λ a → rightIsoPath a b)) (lContr b)
+
+  isEquivInv : isEquiv inv
+  isEquivInv .equiv-proof a = isOfHLevelRetractFromIso 0 (Σ-cong-iso-snd (λ b → leftIsoPath b a)) (rContr a)
+
+open isBijectiveRel
+
+unquoteDecl isBijectiveRelIsoΣ = declareRecordIsoΣ isBijectiveRelIsoΣ (quote isBijectiveRel)
+
+isPropIsBijectiveRel : {R : Rel A B ℓ''} → isProp (isBijectiveRel R)
+isPropIsBijectiveRel x y i .rContr a = isPropIsContr (x .rContr a) (y .rContr a) i
+isPropIsBijectiveRel x y i .lContr a = isPropIsContr (x .lContr a) (y .lContr a) i
+
+BijectiveRel : ∀ (A : Type ℓ) (B : Type ℓ') ℓ'' → Type (ℓ-max (ℓ-max ℓ ℓ') (ℓ-suc ℓ''))
+BijectiveRel A B ℓ'' = Σ[ R ∈ Rel A B ℓ'' ] isBijectiveRel R
+
+BijectiveRelIsoΣ : Iso (BijectiveRel A B ℓ'') (Σ[ R ∈ Rel A B ℓ'' ] isFunctionalRel R × isFunctionalRel (flip R))
+BijectiveRelIsoΣ = Σ-cong-iso-snd λ _ → isBijectiveRelIsoΣ
+
+BijectiveRelPathP : {A : I → Type ℓ} {B : I → Type ℓ'} {R₀ : BijectiveRel (A i0) (B i0) ℓ''} {R₁ : BijectiveRel (A i1) (B i1) ℓ''}
+                  → PathP (λ i → Rel (A i) (B i) ℓ'') (R₀ .fst) (R₁ .fst)
+                  → PathP (λ i → BijectiveRel (A i) (B i) ℓ'') R₀ R₁
+BijectiveRelPathP = ΣPathPProp λ _ → isPropIsBijectiveRel
+
+BijectiveRelEq : {R₀ R₁ : BijectiveRel A B ℓ''} → (∀ a b → R₀ .fst a b ≃ R₁ .fst a b) → R₀ ≡ R₁
+BijectiveRelEq h = BijectiveRelPathP (funExt₂ λ a b → ua (h a b))
+
+BijectiveRel→Equiv : BijectiveRel A B ℓ → A ≃ B
+BijectiveRel→Equiv (R , Rbij) .fst = fun Rbij
+BijectiveRel→Equiv (R , Rbij) .snd = isEquivFun Rbij
+
+Equiv→BijectiveRel : A ≃ B → BijectiveRel A B _
+Equiv→BijectiveRel e .fst = graphRel (e .fst)
+Equiv→BijectiveRel e .snd .rContr a = isContrSingl (e .fst a)
+Equiv→BijectiveRel e .snd .lContr = e .snd .equiv-proof
+
+EquivIsoBijectiveRel : (A B : Type ℓ) → Iso (A ≃ B) (BijectiveRel A B ℓ)
+EquivIsoBijectiveRel A B .Iso.fun = Equiv→BijectiveRel
+EquivIsoBijectiveRel A B .Iso.inv = BijectiveRel→Equiv
+EquivIsoBijectiveRel A B .Iso.rightInv (R , Rbij) = BijectiveRelEq $ rightEquivPath Rbij
+EquivIsoBijectiveRel A B .Iso.leftInv e = equivEq refl
+
+Equiv≃BijectiveRel : (A B : Type ℓ) → (A ≃ B) ≃ (BijectiveRel A B ℓ)
+Equiv≃BijectiveRel A B = isoToEquiv (EquivIsoBijectiveRel A B)
+
+isBijectiveIdRel : isBijectiveRel (idRel A)
+isBijectiveIdRel .rContr = isContrSingl
+isBijectiveIdRel .lContr = isContrSingl'
+
+idBijectiveRel : BijectiveRel A A _
+idBijectiveRel = _ , isBijectiveIdRel
+
+isBijectiveInvRel : isBijectiveRel R → isBijectiveRel (invRel R)
+isBijectiveInvRel Rbij .rContr = Rbij .lContr
+isBijectiveInvRel Rbij .lContr = Rbij .rContr
+
+invBijectiveRel : BijectiveRel A B ℓ' → BijectiveRel B A ℓ'
+invBijectiveRel (_ , Rbij) = _ , isBijectiveInvRel Rbij
+
+isBijectiveCompRel : isBijectiveRel R → isBijectiveRel S → isBijectiveRel (compRel R S)
+isBijectiveCompRel Rbij Sbij .rContr = isFunctionalCompRel   (Rbij .rContr) (Sbij .rContr)
+isBijectiveCompRel Rbij Sbij .lContr = isCofunctionalCompRel (Rbij .lContr) (Sbij .lContr)
+
+compBijectiveRel : BijectiveRel A B ℓ → BijectiveRel B C ℓ' → BijectiveRel A C _
+compBijectiveRel (_ , Rbij) (_ , Sbij) = _ , isBijectiveCompRel Rbij Sbij
+
+isBijectivePathP : (A : I → Type ℓ) → isBijectiveRel (PathP A)
+isBijectivePathP A .rContr = isContrSinglP A
+isBijectivePathP A .lContr = isContrSinglP' A
+
+pathToBijectiveRel : A ≡ B → BijectiveRel A B _
+pathToBijectiveRel P = _ , isBijectivePathP λ i → P i
+
+BijectiveRelToPath : BijectiveRel A B ℓ → A ≡ B
+BijectiveRelToPath R = ua (BijectiveRel→Equiv R)
+
+path→BijectiveRel→Equiv : (P : A ≡ B) → BijectiveRel→Equiv (pathToBijectiveRel P) ≡ pathToEquiv P
+path→BijectiveRel→Equiv P = equivEq refl
+
+pathIsoBijectiveRel : Iso (A ≡ B) (BijectiveRel A B _)
+pathIsoBijectiveRel .Iso.fun = pathToBijectiveRel
+pathIsoBijectiveRel .Iso.inv = BijectiveRelToPath
+pathIsoBijectiveRel .Iso.rightInv (R , Rbij) = BijectiveRelEq λ a b → ua-ungluePath-Equiv _ ∙ₑ rightEquivPath Rbij a b
+pathIsoBijectiveRel .Iso.leftInv P = cong ua (path→BijectiveRel→Equiv P) ∙ ua-pathToEquiv P
+
+path≡BijectiveRel : (A ≡ B) ≡ BijectiveRel A B _
+path≡BijectiveRel = isoToPath pathIsoBijectiveRel

Cubical/Foundations/Function.agda

@@ -156,8 +156,8 @@ module _ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} where
               })
           (downleft x y i j)
 
-homotopyNatural : {B : Type ℓ'} {f g : A → B} (H : ∀ a → f a ≡ g a) {x y : A} (p : x ≡ y) →
-                  H x ∙ cong g p ≡ cong f p ∙ H y
+homotopyNatural : {B : Type ℓ'} {f g : A → B} (H : ∀ a → f a ≡ g a) {x y : A} (p : x ≡ y)
+                → H x ∙ cong g p ≡ cong f p ∙ H y
 homotopyNatural {f = f} {g = g} H {x} {y} p i j =
     hcomp (λ k → λ { (i = i0) → compPath-filler (H x) (cong g p) k j
                    ; (i = i1) → compPath-filler' (cong f p) (H y) k j
@@ -173,3 +173,12 @@ homotopySymInv {f = f} H a j i =
                  ; (j = i0) → H (H a (~ i)) i
                  ; (j = i1) → H a (i ∧ ~ k)})
         (H (H a (~ i ∨ j)) i)
+
+homotopyIdComm : {f : A → A} (H : ∀ a → f a ≡ a) (a : A)
+               → H (f a) ≡ cong f (H a)
+homotopyIdComm {f = f} H a i j = hcomp (λ k → λ where
+    (i = i0) → H (H a (~ k)) j
+    (i = i1) → H (H a j) (j ∧ ~ k)
+    (j = i0) → f (H a (~ k ∧ ~ i))
+    (j = i1) → H a (~ k)
+  ) (H (H a (~ i ∨ j)) j)

Cubical/Foundations/Interpolate.agda

@@ -3,17 +3,25 @@ module Cubical.Foundations.Interpolate where
 
 open import Cubical.Foundations.Prelude
 
+private variable
+  ℓ : Level
+  A : Type ℓ
+  x y : A
+
 -- An "interpolation" operator on the De Morgan interval. Interpolates
 -- along t from i to j (see first two properties below.)
 interpolateI : I → I → I → I
 interpolateI t i j = (~ t ∧ i) ∨ (t ∧ j) ∨ (i ∧ j)
 
+pathSlice : ∀ (p : x ≡ y) i j → p i ≡ p j
+pathSlice p i j t = p (interpolateI t i j)
+
 -- I believe this is the simplest De Morgan function on three
 -- variables which satisfies all (or even most) of the nice properties
 -- below.
 
 module _
-  {A : Type} {p : I → A} {i j k l m : I}
+  {p : I → A} {i j k l m : I}
   where
   _ : p (interpolateI i0 i j) ≡ p i
   _ = refl

Cubical/Foundations/Path.agda

@@ -151,6 +151,17 @@ isProp→isContrPathP : {A : I → Type ℓ} → (∀ i → isProp (A i))
                     → isContr (PathP A x y)
 isProp→isContrPathP h x y = isProp→PathP h x y , isProp→isPropPathP h x y _
 
+-- A useful lemma for proving that a path is trivial
+triangle→≡refl : {x : A} {p : x ≡ x}
+                → Square refl p p p
+                → p ≡ refl
+triangle→≡refl {x = x} {p} sq i j = hcomp (λ k → λ where
+    (i = i0) → p j
+    (i = i1) → p k
+    (j = i0) → p (~ i ∨ k)
+    (j = i1) → p (~ i ∨ k)
+  ) (sq (~ i) j)
+
 -- Flipping a square along its diagonal
 
 flipSquare : {a₀₀ a₀₁ : A} {a₀₋ : a₀₀ ≡ a₀₁}

Cubical/Foundations/Prelude.agda

@@ -15,8 +15,6 @@ This file proves a variety of basic results about paths:
 
 - Direct definitions of lower h-levels
 
-- Export natural numbers
-
 - Export universe lifting
 
 -}
@@ -485,18 +483,36 @@ is2Groupoid A = ∀ a b → isGroupoid (Path A a b)
 singlP : (A : I → Type ℓ) (a : A i0) → Type _
 singlP A a = Σ[ x ∈ A i1 ] PathP A a x
 
+singlP' : (A : I → Type ℓ) (a : A i1) → Type _
+singlP' A a = Σ[ x ∈ A i0 ] PathP A x a
+
 singl : (a : A) → Type _
 singl {A = A} a = singlP (λ _ → A) a
 
+singl' : (a : A) → Type _
+singl' {A = A} a = singlP' (λ _ → A) a
+
 isContrSingl : (a : A) → isContr (singl a)
-isContrSingl a .fst = (a , refl)
-isContrSingl a .snd p i .fst = p .snd i
-isContrSingl a .snd p i .snd j = p .snd (i ∧ j)
+isContrSingl a .fst = _ , refl
+isContrSingl a .snd (x , p) i = _ , λ j → p (i ∧ j)
+
+isContrSingl' : (a : A) → isContr (singl' a)
+isContrSingl' a .fst = _ , refl
+isContrSingl' a .snd (x , p) i = _ , λ j → p (~ i ∨ j)
 
 isContrSinglP : (A : I → Type ℓ) (a : A i0) → isContr (singlP A a)
 isContrSinglP A a .fst = _ , transport-filler (λ i → A i) a
-isContrSinglP A a .snd (x , p) i =
-  _ , λ j → fill A (λ j → λ {(i = i0) → transport-filler (λ i → A i) a j; (i = i1) → p j}) (inS a) j
+isContrSinglP A a .snd (x , p) i = _ , λ k → fill A (λ j → λ where
+    (i = i0) → transport-filler (λ i → A i) a j
+    (i = i1) → p j
+  ) (inS a) k
+
+isContrSinglP' : (A : I → Type ℓ) (a : A i1) → isContr (singlP' A a)
+isContrSinglP' A a .fst = _ , symP (transport-filler (λ i → A (~ i)) a)
+isContrSinglP' A a .snd (x , p) i = _ , λ k → fill (λ i → A (~ i)) (λ j → λ where
+    (i = i0) → transport-filler (λ i → A (~ i)) a j
+    (i = i1) → p (~ j)
+  ) (inS a) (~ k)
 
 -- Higher cube types
 
@@ -508,6 +524,13 @@ SquareP :
   → Type ℓ
 SquareP A a₀₋ a₁₋ a₋₀ a₋₁ = PathP (λ i → PathP (λ j → A i j) (a₋₀ i) (a₋₁ i)) a₀₋ a₁₋
 
+-- This is the type of squares:
+-- a₀₀ =====> a₀₁
+-- ||         ||
+-- ||         ||
+-- \/         \/
+-- a₁₀ =====> a₁₁
+
 Square :
   {a₀₀ a₀₁ : A} (a₀₋ : a₀₀ ≡ a₀₁)
   {a₁₀ a₁₁ : A} (a₁₋ : a₁₀ ≡ a₁₁)
@@ -587,31 +610,29 @@ isProp→PathP : ∀ {B : I → Type ℓ} → ((i : I) → isProp (B i))
                → PathP B b0 b1
 isProp→PathP hB b0 b1 = toPathP (hB _ _ _)
 
-isPropIsContr : isProp (isContr A)
-isPropIsContr (c0 , h0) (c1 , h1) j .fst = h0 c1 j
-isPropIsContr (c0 , h0) (c1 , h1) j .snd y i =
-   hcomp (λ k → λ { (i = i0) → h0 (h0 c1 j) k;
-                    (i = i1) → h0 y k;
-                    (j = i0) → h0 (h0 y i) k;
-                    (j = i1) → h0 (h1 y i) k})
-         c0
-
 isContr→isProp : isContr A → isProp A
-isContr→isProp (x , p) a b = sym (p a) ∙ p b
+isContr→isProp (c , h) a b = sym (h a) ∙ h b
+
+isContr→isSet' : isContr A → isSet' A
+isContr→isSet' (c , h) p q r s i j = hcomp (λ k → λ where
+    (i = i0) → h (p j) k
+    (i = i1) → h (q j) k
+    (j = i0) → h (r i) k
+    (j = i1) → h (s i) k
+  ) c
+
+isContr→isSet : isContr A → isSet A
+isContr→isSet c = isSet'→isSet (isContr→isSet' c)
+
+isPropIsContr : isProp (isContr A)
+isPropIsContr (c0 , h0) (c1 , h1) i .fst = h0 c1 i
+isPropIsContr (c0 , h0) (c1 , h1) i .snd y = isContr→isSet' (c0 , h0) (h0 y) (h1 y) (h0 c1) refl i
 
 isProp→isSet : isProp A → isSet A
-isProp→isSet h a b p q j i =
-  hcomp (λ k → λ { (i = i0) → h a a k
-                 ; (i = i1) → h a b k
-                 ; (j = i0) → h a (p i) k
-                 ; (j = i1) → h a (q i) k }) a
+isProp→isSet h a = isContr→isSet (a , h a) a
 
 isProp→isSet' : isProp A → isSet' A
-isProp→isSet' h {a} p q r s i j =
-  hcomp (λ k → λ { (i = i0) → h a (p j) k
-                 ; (i = i1) → h a (q j) k
-                 ; (j = i0) → h a (r i) k
-                 ; (j = i1) → h a (s i) k}) a
+isProp→isSet' h {a} = isContr→isSet' (a , h a)
 
 isPropIsProp : isProp (isProp A)
 isPropIsProp f g i a b = isProp→isSet f a b (f a b) (g a b) i