From bf1e4fc1af142d278f2d5a67141dfac4b4caa65c Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Wed, 20 Aug 2025 23:25:03 +0530
Subject: [PATCH 01/10] Bifunctional relations

---
 Cubical/Relation/Binary/Base.agda | 32 +++++++++++++++++++++++++++----
 1 file changed, 28 insertions(+), 4 deletions(-)

diff --git a/Cubical/Relation/Binary/Base.agda b/Cubical/Relation/Binary/Base.agda
index 500c849b9c..931ec375c0 100644
--- a/Cubical/Relation/Binary/Base.agda
+++ b/Cubical/Relation/Binary/Base.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --safe #-}
 module Cubical.Relation.Binary.Base where
 
 open import Cubical.Foundations.Prelude
@@ -25,12 +26,25 @@ private
 Rel : ∀ {ℓa ℓb} (A : Type ℓa) (B : Type ℓb) (ℓ' : Level) → Type (ℓ-max (ℓ-max ℓa ℓb) (ℓ-suc ℓ'))
 Rel A B ℓ' = A → B → Type ℓ'
 
+idRel : ∀ {ℓ} (A : Type ℓ) → Rel A A ℓ
+idRel A = _≡_
+
+invRel : ∀ {ℓ ℓ'} {A B : Type ℓ} → Rel A B ℓ' → Rel B A ℓ'
+invRel R b a = R a b
+
+compRel : ∀ {ℓ ℓ' ℓ''} {A B C : Type ℓ}
+  → Rel A B ℓ' → Rel B C ℓ'' → Rel A C (ℓ-max ℓ (ℓ-max ℓ' ℓ''))
+compRel R S a c = Σ[ b ∈ _ ] R a b × S b c
+
 PropRel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
 PropRel A B ℓ' = Σ[ R ∈ Rel A B ℓ' ] ∀ a b → isProp (R a b)
 
+squashPropRel : ∀ {ℓ ℓ'} {A B : Type ℓ} → Rel A B ℓ' → PropRel A B ℓ'
+squashPropRel R .fst a b = ∥ R a b ∥₁
+squashPropRel R .snd a b = squash₁
+
 idPropRel : ∀ {ℓ} (A : Type ℓ) → PropRel A A ℓ
-idPropRel A .fst a a' = ∥ a ≡ a' ∥₁
-idPropRel A .snd _ _ = squash₁
+idPropRel A = squashPropRel (idRel A)
 
 invPropRel : ∀ {ℓ ℓ'} {A B : Type ℓ}
   → PropRel A B ℓ' → PropRel B A ℓ'
@@ -39,8 +53,7 @@ invPropRel R .snd b a = R .snd a b
 
 compPropRel : ∀ {ℓ ℓ' ℓ''} {A B C : Type ℓ}
   → PropRel A B ℓ' → PropRel B C ℓ'' → PropRel A C (ℓ-max ℓ (ℓ-max ℓ' ℓ''))
-compPropRel R S .fst a c = ∥ Σ[ b ∈ _ ] (R .fst a b × S .fst b c) ∥₁
-compPropRel R S .snd _ _ = squash₁
+compPropRel R S = squashPropRel (compRel (R .fst) (S .fst))
 
 graphRel : ∀ {ℓ} {A B : Type ℓ} → (A → B) → Rel A B ℓ
 graphRel f a b = f a ≡ b
@@ -49,6 +62,17 @@ module HeterogenousRelation {ℓ ℓ' : Level} {A B : Type ℓ} (R : Rel A B ℓ
   isUniversalRel : Type (ℓ-max ℓ ℓ')
   isUniversalRel = (a : A) (b : B) → R a b
 
+  isFunctionalRel : Type (ℓ-max ℓ ℓ')
+  isFunctionalRel = (a : A) → isContr (Σ B (R a))
+
+  isCofunctionalRel : Type (ℓ-max ℓ ℓ')
+  isCofunctionalRel = (b : B) → isContr (Σ A (invRel R b))
+
+  record isBifunctionalRel : Type (ℓ-max ℓ ℓ') where
+    field
+      rContrSingl : isFunctionalRel
+      lContrSingl : isCofunctionalRel
+
 module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where
   isRefl : Type (ℓ-max ℓ ℓ')
   isRefl = (a : A) → R a a

From 648993be0e56a537f1f556e03192ad5a712db07e Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Fri, 22 Aug 2025 23:54:35 +0530
Subject: [PATCH 02/10] Define based identity systems, prove equivalence of
 functional relations and functions
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

I also proved `isContr→isSet'` to simplify the proofs of `isPropIsContr`, `isProp→isSet` and `isProp→isSet'`
---
 Cubical/Foundations/Path.agda           | 11 +++++
 Cubical/Foundations/Prelude.agda        | 53 ++++++++++++----------
 Cubical/Relation/Binary/Base.agda       | 15 ++++---
 Cubical/Relation/Binary/Properties.agda | 60 +++++++++++++++++++++++++
 4 files changed, 108 insertions(+), 31 deletions(-)

diff --git a/Cubical/Foundations/Path.agda b/Cubical/Foundations/Path.agda
index 0dd6bdb72e..99c81f42e1 100644
--- a/Cubical/Foundations/Path.agda
+++ b/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₀₁}
diff --git a/Cubical/Foundations/Prelude.agda b/Cubical/Foundations/Prelude.agda
index a9454e5875..4f8d743756 100644
--- a/Cubical/Foundations/Prelude.agda
+++ b/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
 
 -}
@@ -495,8 +493,10 @@ isContrSingl a .snd p i .snd j = p .snd (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
 
 -- Higher cube types
 
@@ -508,6 +508,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 +594,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
diff --git a/Cubical/Relation/Binary/Base.agda b/Cubical/Relation/Binary/Base.agda
index 931ec375c0..436f2c3cad 100644
--- a/Cubical/Relation/Binary/Base.agda
+++ b/Cubical/Relation/Binary/Base.agda
@@ -65,13 +65,14 @@ module HeterogenousRelation {ℓ ℓ' : Level} {A B : Type ℓ} (R : Rel A B ℓ
   isFunctionalRel : Type (ℓ-max ℓ ℓ')
   isFunctionalRel = (a : A) → isContr (Σ B (R a))
 
-  isCofunctionalRel : Type (ℓ-max ℓ ℓ')
-  isCofunctionalRel = (b : B) → isContr (Σ A (invRel R b))
+  isPropIsFunctional : isProp isFunctionalRel
+  isPropIsFunctional = isPropΠ λ _ → isPropIsContr
 
-  record isBifunctionalRel : Type (ℓ-max ℓ ℓ') where
-    field
-      rContrSingl : isFunctionalRel
-      lContrSingl : isCofunctionalRel
+open HeterogenousRelation
+
+graphRelIsFunctional : ∀ {ℓ} {A B : Type ℓ} (f : A → B)
+                     → isFunctionalRel (graphRel f)
+graphRelIsFunctional f a = isContrSingl (f a)
 
 module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where
   isRefl : Type (ℓ-max ℓ ℓ')
@@ -165,7 +166,7 @@ module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where
       symmetric : isSym
       transitive : isTrans
 
-  isUniversalRel→isEquivRel : HeterogenousRelation.isUniversalRel R → isEquivRel
+  isUniversalRel→isEquivRel : isUniversalRel R → isEquivRel
   isUniversalRel→isEquivRel u .isEquivRel.reflexive a = u a a
   isUniversalRel→isEquivRel u .isEquivRel.symmetric a b _ = u b a
   isUniversalRel→isEquivRel u .isEquivRel.transitive a _ c _ _ = u a c
diff --git a/Cubical/Relation/Binary/Properties.agda b/Cubical/Relation/Binary/Properties.agda
index 175a6262f8..f74fbafc43 100644
--- a/Cubical/Relation/Binary/Properties.agda
+++ b/Cubical/Relation/Binary/Properties.agda
@@ -5,6 +5,8 @@ open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Functions.FunExtEquiv
 
 open import Cubical.Data.Sigma
@@ -17,6 +19,48 @@ private
     ℓ ℓ' : Level
     A B : Type ℓ
 
+record isIdentitySystem {A : Type ℓ} (a : A) (C : A → Type ℓ') (r : C a) : Type (ℓ-max ℓ ℓ') where
+  field
+    toPath : ∀ {b} → C b → a ≡ b
+    toPathOver : ∀ {b} (p : C b) → PathP (λ i → C (toPath p i)) r p
+
+  isContrTotal : ∃! A C
+  isContrTotal = (a , r) , λ (b , p) → ΣPathP (toPath p , toPathOver p)
+
+  -- Useful corollary
+  toPathTotal-η : ΣPathP (toPath r , toPathOver r) ≡ refl
+  toPathTotal-η = isContr→isSet isContrTotal _ _ _ _
+
+  toPath-η : toPath r ≡ refl
+  toPath-η = cong (cong fst) toPathTotal-η
+
+  toPathOver-η : SquareP (λ i j → C (toPath-η i j)) (toPathOver r) refl refl refl
+  toPathOver-η = cong (cong snd) toPathTotal-η
+
+  IdsJ : ∀ {ℓ''} (P : ∀ b → C b → Type ℓ'') (Pr : P a r) {b} p → P b p
+  IdsJ P Pr p = subst (uncurry P) (ΣPathP (toPath p , toPathOver p)) Pr
+
+  IdsJ>_ : ∀ {ℓ''} {P : ∀ b → C b → Type ℓ''} (Pr : P a r) b p → P b p
+  IdsJ>_ {P = P} Pr _ = IdsJ P Pr
+
+  IdsJ-η : ∀ {ℓ''} (P : ∀ b → C b → Type ℓ'') (Pr : P a r) → IdsJ P Pr r ≡ Pr
+  IdsJ-η P Pr i = transp (λ j → uncurry P (toPathTotal-η i j)) i Pr
+
+  open Iso
+
+  isoPath : ∀ b → Iso (C b) (a ≡ b)
+  isoPath b .fun = toPath
+  isoPath b .inv p = subst C p r
+  isoPath b .rightInv = J (λ b p → toPath (subst C p r) ≡ p) $ cong toPath (transportRefl r) ∙ toPath-η
+  isoPath b .leftInv p = fromPathP (toPathOver p)
+
+open isIdentitySystem
+
+isContrTotal→isIdentitySystem : {C : A → Type ℓ} (contr : ∃! A C)
+                              → isIdentitySystem (contr .fst .fst) C (contr .fst .snd)
+isContrTotal→isIdentitySystem contr .toPath     p = cong fst $ contr .snd (_ , p)
+isContrTotal→isIdentitySystem contr .toPathOver p = cong snd $ contr .snd (_ , p)
+
 -- Theorem 7.2.2 in the HoTT Book
 module _ (R : Rel A A ℓ') where
   open BinaryRelation R
@@ -39,6 +83,22 @@ module _ (R : Rel A A ℓ') where
     Aset : isSet A
     Aset = reflPropRelImpliesIdentity→isSet Rrefl Rprop R→≡
 
+-- Functional relations are equivalent to functions
+module _ (A B : Type ℓ) where
+  open HeterogenousRelation
+
+  FunctionalRel : Type (ℓ-suc ℓ)
+  FunctionalRel = Σ[ R ∈ Rel A B ℓ ] isFunctionalRel R
+
+  open Iso
+
+  FunctionalRelIsoFunction : Iso FunctionalRel (A → B)
+  FunctionalRelIsoFunction .fun (R , Rfun) a = Rfun a .fst .fst
+  FunctionalRelIsoFunction .inv f = graphRel f , graphRelIsFunctional f
+  FunctionalRelIsoFunction .rightInv f = refl
+  FunctionalRelIsoFunction .leftInv (R , Rfun) = Σ≡Prop isPropIsFunctional $ funExt₂ λ a →
+    isoToPath ∘ invIso ∘ isoPath (isContrTotal→isIdentitySystem $ Rfun a)
+
 -- Pulling back a relation along a function.
 -- This can for example be used when restricting an equivalence relation to a subset:
 --   _~'_ = on fst _~_

From 643c0a356e89d9a4d9b5bb1a95b32848b7796983 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sat, 23 Aug 2025 14:32:33 +0530
Subject: [PATCH 03/10] yo dawg I heard u liek hcomp so we put a hcomp in your
 hcomp so you can hcomp while you hcomp

---
 Cubical/Foundations/Function.agda       | 14 ++++++++++++--
 Cubical/Foundations/Interpolate.agda    | 10 +++++++++-
 Cubical/Relation/Binary/Properties.agda |  7 ++++++-
 3 files changed, 27 insertions(+), 4 deletions(-)

diff --git a/Cubical/Foundations/Function.agda b/Cubical/Foundations/Function.agda
index 99f4a019ba..5c6ebefee8 100644
--- a/Cubical/Foundations/Function.agda
+++ b/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,13 @@ 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)
+ 
diff --git a/Cubical/Foundations/Interpolate.agda b/Cubical/Foundations/Interpolate.agda
index c203efabc4..ae3a032da5 100644
--- a/Cubical/Foundations/Interpolate.agda
+++ b/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
diff --git a/Cubical/Relation/Binary/Properties.agda b/Cubical/Relation/Binary/Properties.agda
index f74fbafc43..eb2cbf7492 100644
--- a/Cubical/Relation/Binary/Properties.agda
+++ b/Cubical/Relation/Binary/Properties.agda
@@ -51,7 +51,12 @@ record isIdentitySystem {A : Type ℓ} (a : A) (C : A → Type ℓ') (r : C a) :
   isoPath : ∀ b → Iso (C b) (a ≡ b)
   isoPath b .fun = toPath
   isoPath b .inv p = subst C p r
-  isoPath b .rightInv = J (λ b p → toPath (subst C p r) ≡ p) $ cong toPath (transportRefl r) ∙ toPath-η
+  isoPath b .rightInv p i j = hcomp (λ k → λ where
+      (i = i0) → toPath (transport-filler (cong C p) r k) j
+      (i = i1) → p (j ∧ k)
+      (j = i0) → a
+      (j = i1) → p k
+    ) (toPath-η i j)
   isoPath b .leftInv p = fromPathP (toPathOver p)
 
 open isIdentitySystem

From 5600413101d263a4384d7c332bdf3ee4ee23e3e4 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sat, 23 Aug 2025 22:30:51 +0530
Subject: [PATCH 04/10] Actually define bijective relations

---
 Cubical/Foundations/Equiv/BijectiveRel.agda | 64 +++++++++++++++++++++
 Cubical/Foundations/Prelude.agda            | 22 ++++++-
 Cubical/Relation/Binary/Base.agda           | 29 +++++-----
 Cubical/Relation/Binary/Properties.agda     | 15 +++--
 4 files changed, 107 insertions(+), 23 deletions(-)
 create mode 100644 Cubical/Foundations/Equiv/BijectiveRel.agda

diff --git a/Cubical/Foundations/Equiv/BijectiveRel.agda b/Cubical/Foundations/Equiv/BijectiveRel.agda
new file mode 100644
index 0000000000..486e50930d
--- /dev/null
+++ b/Cubical/Foundations/Equiv/BijectiveRel.agda
@@ -0,0 +1,64 @@
+{-
+
+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.GroupoidLaws
+open import Cubical.Foundations.Function
+open import Cubical.Relation.Binary
+open import Cubical.Reflection.RecordEquiv
+open import Cubical.Reflection.StrictEquiv
+open import Cubical.Data.Sigma
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+    A : Type ℓ
+    B : Type ℓ'
+
+open HeterogenousRelation
+
+record isBijectiveRel {A : Type ℓ} {B : Type ℓ'} (R : Rel A B ℓ'') : Type (ℓ-max ℓ (ℓ-max ℓ' ℓ'')) where
+  field
+    rContr : isFunctionalRel R
+    lContr : isFunctionalRel (flip R)
+
+unquoteDecl isBijectiveRelIsoΣ = declareRecordIsoΣ isBijectiveRelIsoΣ (quote isBijectiveRel)
+
+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Σ
+
+EquivIsoBijectiveRel : (A B : Type ℓ) → Iso (A ≃ B) (BijectiveRel A B ℓ)
+EquivIsoBijectiveRel A B = 
+  (A ≃ B)                                                                 Iso⟨ Σ-cong-iso-snd isEquiv-isEquiv'-Iso ⟩
+  (Σ[ f ∈ (A → B) ] (∀ a → isContr (fiber f a)))                          Iso⟨ Σ-cong-iso-fst (invIso (FunctionalRelIsoFunction A B)) ⟩
+  (Σ[ (R , _) ∈ Σ (Rel A B _) isFunctionalRel ] isFunctionalRel (flip R)) Iso⟨ Σ-assoc-Iso ⟩
+  (Σ[ R ∈ Rel A B _ ] isFunctionalRel R × isFunctionalRel (flip R))       Iso⟨ invIso BijectiveRelIsoΣ ⟩
+  BijectiveRel A B _                                                     ∎Iso
+
+Equiv≃BijectiveRel : (A B : Type ℓ) → (A ≃ B) ≃ (BijectiveRel A B ℓ)
+Equiv≃BijectiveRel A B = isoToEquiv (EquivIsoBijectiveRel A B)
+
+open isBijectiveRel
+
+isBijectiveIdRel : isBijectiveRel (idRel A)
+isBijectiveIdRel .rContr = isContrSingl
+isBijectiveIdRel .lContr = isContrSingl'
+
+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
diff --git a/Cubical/Foundations/Prelude.agda b/Cubical/Foundations/Prelude.agda
index 4f8d743756..7eb09b64c6 100644
--- a/Cubical/Foundations/Prelude.agda
+++ b/Cubical/Foundations/Prelude.agda
@@ -483,13 +483,22 @@ 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
@@ -498,6 +507,13 @@ isContrSinglP A a .snd (x , p) i = _ , λ k → fill A (λ j → λ where
     (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
 
 SquareP :
diff --git a/Cubical/Relation/Binary/Base.agda b/Cubical/Relation/Binary/Base.agda
index 436f2c3cad..c8972fc1b4 100644
--- a/Cubical/Relation/Binary/Base.agda
+++ b/Cubical/Relation/Binary/Base.agda
@@ -29,48 +29,47 @@ Rel A B ℓ' = A → B → Type ℓ'
 idRel : ∀ {ℓ} (A : Type ℓ) → Rel A A ℓ
 idRel A = _≡_
 
-invRel : ∀ {ℓ ℓ'} {A B : Type ℓ} → Rel A B ℓ' → Rel B A ℓ'
+invRel : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} → Rel A B ℓ'' → Rel B A ℓ''
 invRel R b a = R a b
 
-compRel : ∀ {ℓ ℓ' ℓ''} {A B C : Type ℓ}
-  → Rel A B ℓ' → Rel B C ℓ'' → Rel A C (ℓ-max ℓ (ℓ-max ℓ' ℓ''))
+compRel : ∀ {ℓ ℓ' ℓ'' ℓ''' ℓ''''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
+        → Rel A B ℓ''' → Rel B C ℓ'''' → Rel A C (ℓ-max (ℓ-max ℓ' ℓ''') ℓ'''')
 compRel R S a c = Σ[ b ∈ _ ] R a b × S b c
 
-PropRel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
+PropRel : ∀ {ℓa ℓb} (A : Type ℓa) (B : Type ℓb) (ℓ' : Level) → Type (ℓ-max (ℓ-max ℓa ℓb) (ℓ-suc ℓ'))
 PropRel A B ℓ' = Σ[ R ∈ Rel A B ℓ' ] ∀ a b → isProp (R a b)
 
-squashPropRel : ∀ {ℓ ℓ'} {A B : Type ℓ} → Rel A B ℓ' → PropRel A B ℓ'
+squashPropRel : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} → Rel A B ℓ'' → PropRel A B ℓ''
 squashPropRel R .fst a b = ∥ R a b ∥₁
 squashPropRel R .snd a b = squash₁
 
 idPropRel : ∀ {ℓ} (A : Type ℓ) → PropRel A A ℓ
 idPropRel A = squashPropRel (idRel A)
 
-invPropRel : ∀ {ℓ ℓ'} {A B : Type ℓ}
-  → PropRel A B ℓ' → PropRel B A ℓ'
+invPropRel : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} → PropRel A B ℓ'' → PropRel B A ℓ''
 invPropRel R .fst b a = R .fst a b
 invPropRel R .snd b a = R .snd a b
 
-compPropRel : ∀ {ℓ ℓ' ℓ''} {A B C : Type ℓ}
-  → PropRel A B ℓ' → PropRel B C ℓ'' → PropRel A C (ℓ-max ℓ (ℓ-max ℓ' ℓ''))
+compPropRel : ∀ {ℓ ℓ' ℓ'' ℓ''' ℓ''''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
+            → PropRel A B ℓ''' → PropRel B C ℓ'''' → PropRel A C (ℓ-max (ℓ-max ℓ' ℓ''') ℓ'''')
 compPropRel R S = squashPropRel (compRel (R .fst) (S .fst))
 
-graphRel : ∀ {ℓ} {A B : Type ℓ} → (A → B) → Rel A B ℓ
+graphRel : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (A → B) → Rel A B ℓ'
 graphRel f a b = f a ≡ b
 
-module HeterogenousRelation {ℓ ℓ' : Level} {A B : Type ℓ} (R : Rel A B ℓ') where
-  isUniversalRel : Type (ℓ-max ℓ ℓ')
+module HeterogenousRelation {ℓ ℓ' ℓ'' : Level} {A : Type ℓ} {B : Type ℓ'} (R : Rel A B ℓ'') where
+  isUniversalRel : Type _
   isUniversalRel = (a : A) (b : B) → R a b
 
-  isFunctionalRel : Type (ℓ-max ℓ ℓ')
-  isFunctionalRel = (a : A) → isContr (Σ B (R a))
+  isFunctionalRel : Type _
+  isFunctionalRel = (a : A) → ∃! B (R a)
 
   isPropIsFunctional : isProp isFunctionalRel
   isPropIsFunctional = isPropΠ λ _ → isPropIsContr
 
 open HeterogenousRelation
 
-graphRelIsFunctional : ∀ {ℓ} {A B : Type ℓ} (f : A → B)
+graphRelIsFunctional : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B)
                      → isFunctionalRel (graphRel f)
 graphRelIsFunctional f a = isContrSingl (f a)
 
diff --git a/Cubical/Relation/Binary/Properties.agda b/Cubical/Relation/Binary/Properties.agda
index eb2cbf7492..f93f34485c 100644
--- a/Cubical/Relation/Binary/Properties.agda
+++ b/Cubical/Relation/Binary/Properties.agda
@@ -1,3 +1,4 @@
+{-# OPTIONS --hidden-argument-puns #-}
 module Cubical.Relation.Binary.Properties where
 
 open import Cubical.Foundations.Prelude
@@ -16,8 +17,9 @@ open import Cubical.Relation.Nullary
 
 private
   variable
-    ℓ ℓ' : Level
-    A B : Type ℓ
+    ℓ ℓ' ℓ'' : Level
+    A B C : Type ℓ
+    R S : Rel A B ℓ''
 
 record isIdentitySystem {A : Type ℓ} (a : A) (C : A → Type ℓ') (r : C a) : Type (ℓ-max ℓ ℓ') where
   field
@@ -89,11 +91,11 @@ module _ (R : Rel A A ℓ') where
     Aset = reflPropRelImpliesIdentity→isSet Rrefl Rprop R→≡
 
 -- Functional relations are equivalent to functions
-module _ (A B : Type ℓ) where
+module _ (A : Type ℓ) (B : Type ℓ') where
   open HeterogenousRelation
 
-  FunctionalRel : Type (ℓ-suc ℓ)
-  FunctionalRel = Σ[ R ∈ Rel A B ℓ ] isFunctionalRel R
+  FunctionalRel : Type (ℓ-max ℓ (ℓ-suc ℓ'))
+  FunctionalRel = Σ[ R ∈ Rel A B ℓ' ] isFunctionalRel R
 
   open Iso
 
@@ -104,6 +106,9 @@ module _ (A B : Type ℓ) where
   FunctionalRelIsoFunction .leftInv (R , Rfun) = Σ≡Prop isPropIsFunctional $ funExt₂ λ a →
     isoToPath ∘ invIso ∘ isoPath (isContrTotal→isIdentitySystem $ Rfun a)
 
+  Function≃FunctionalRel : (A → B) ≃ FunctionalRel
+  Function≃FunctionalRel = isoToEquiv (invIso FunctionalRelIsoFunction)
+
 -- Pulling back a relation along a function.
 -- This can for example be used when restricting an equivalence relation to a subset:
 --   _~'_ = on fst _~_

From 896d912de40b13180d14dca50cb894017809993d Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sun, 24 Aug 2025 11:01:58 +0530
Subject: [PATCH 05/10] more bijective relations

---
 Cubical/Foundations/Equiv/BijectiveRel.agda | 25 +++++++++++++++++++--
 1 file changed, 23 insertions(+), 2 deletions(-)

diff --git a/Cubical/Foundations/Equiv/BijectiveRel.agda b/Cubical/Foundations/Equiv/BijectiveRel.agda
index 486e50930d..d972390f72 100644
--- a/Cubical/Foundations/Equiv/BijectiveRel.agda
+++ b/Cubical/Foundations/Equiv/BijectiveRel.agda
@@ -31,11 +31,24 @@ record isBijectiveRel {A : Type ℓ} {B : Type ℓ'} (R : Rel A B ℓ'') : Type
     rContr : isFunctionalRel R
     lContr : isFunctionalRel (flip R)
 
+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
 
+BijectiveRelPathP : {A : I → Type ℓ} {B : I → Type ℓ'} {R₀ : BijectiveRel (A i0) (B i0) ℓ''} {R₁ : BijectiveRel (A i1) (B i1) ℓ''}
+                  → PathP (λ i → A i → B i → Type ℓ'') (R₀ .fst) (R₁ .fst) → PathP (λ i → BijectiveRel (A i) (B i) ℓ'') R₀ R₁
+BijectiveRelPathP = ΣPathPProp λ _ → isPropIsBijectiveRel
+
+BijectiveRelEq : {R₀ R₁ : BijectiveRel A B ℓ''} → R₀ .fst ≡ R₁ .fst → R₀ ≡ R₁
+BijectiveRelEq = Σ≡Prop λ _ → isPropIsBijectiveRel
+
 BijectiveRelIsoΣ : Iso (BijectiveRel A B ℓ'') (Σ[ R ∈ Rel A B ℓ'' ] isFunctionalRel R × isFunctionalRel (flip R))
 BijectiveRelIsoΣ = Σ-cong-iso-snd λ _ → isBijectiveRelIsoΣ
 
@@ -50,12 +63,20 @@ EquivIsoBijectiveRel A B =
 Equiv≃BijectiveRel : (A B : Type ℓ) → (A ≃ B) ≃ (BijectiveRel A B ℓ)
 Equiv≃BijectiveRel A B = isoToEquiv (EquivIsoBijectiveRel A B)
 
-open isBijectiveRel
-
 isBijectiveIdRel : isBijectiveRel (idRel A)
 isBijectiveIdRel .rContr = isContrSingl
 isBijectiveIdRel .lContr = isContrSingl'
 
+idBijectiveRel : BijectiveRel A A _
+idBijectiveRel = _ , isBijectiveIdRel
+
+isBijectiveInvRel : {R : Rel A B ℓ'} → 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
+
 isBijectivePathP : (A : I → Type ℓ) → isBijectiveRel (PathP A)
 isBijectivePathP A .rContr = isContrSinglP A
 isBijectivePathP A .lContr = isContrSinglP' A

From 3f16baa7e931c87027467e6348848480f121a9ed Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sun, 24 Aug 2025 19:39:00 +0530
Subject: [PATCH 06/10] composition of BijectiveRelations

---
 Cubical/Foundations/Equiv/BijectiveRel.agda | 27 ++++++++------
 Cubical/Relation/Binary/Base.agda           |  3 ++
 Cubical/Relation/Binary/Properties.agda     | 39 +++++++++++++++++++--
 3 files changed, 57 insertions(+), 12 deletions(-)

diff --git a/Cubical/Foundations/Equiv/BijectiveRel.agda b/Cubical/Foundations/Equiv/BijectiveRel.agda
index d972390f72..58c5f5c6fd 100644
--- a/Cubical/Foundations/Equiv/BijectiveRel.agda
+++ b/Cubical/Foundations/Equiv/BijectiveRel.agda
@@ -18,11 +18,10 @@ open import Cubical.Reflection.RecordEquiv
 open import Cubical.Reflection.StrictEquiv
 open import Cubical.Data.Sigma
 
-private
-  variable
-    ℓ ℓ' ℓ'' : Level
-    A : Type ℓ
-    B : Type ℓ'
+private variable
+  ℓ ℓ' ℓ'' : Level
+  A B C : Type ℓ
+  R S : Rel A B ℓ
 
 open HeterogenousRelation
 
@@ -42,16 +41,17 @@ isPropIsBijectiveRel x y i .lContr a = isPropIsContr (x .lContr a) (y .lContr a)
 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 → A i → B i → Type ℓ'') (R₀ .fst) (R₁ .fst) → PathP (λ i → BijectiveRel (A i) (B i) ℓ'') R₀ R₁
+                  → PathP (λ i → A i → B i → Type ℓ'') (R₀ .fst) (R₁ .fst)
+                  → PathP (λ i → BijectiveRel (A i) (B i) ℓ'') R₀ R₁
 BijectiveRelPathP = ΣPathPProp λ _ → isPropIsBijectiveRel
 
 BijectiveRelEq : {R₀ R₁ : BijectiveRel A B ℓ''} → R₀ .fst ≡ R₁ .fst → R₀ ≡ R₁
 BijectiveRelEq = Σ≡Prop λ _ → isPropIsBijectiveRel
 
-BijectiveRelIsoΣ : Iso (BijectiveRel A B ℓ'') (Σ[ R ∈ Rel A B ℓ'' ] isFunctionalRel R × isFunctionalRel (flip R))
-BijectiveRelIsoΣ = Σ-cong-iso-snd λ _ → isBijectiveRelIsoΣ
-
 EquivIsoBijectiveRel : (A B : Type ℓ) → Iso (A ≃ B) (BijectiveRel A B ℓ)
 EquivIsoBijectiveRel A B = 
   (A ≃ B)                                                                 Iso⟨ Σ-cong-iso-snd isEquiv-isEquiv'-Iso ⟩
@@ -70,13 +70,20 @@ isBijectiveIdRel .lContr = isContrSingl'
 idBijectiveRel : BijectiveRel A A _
 idBijectiveRel = _ , isBijectiveIdRel
 
-isBijectiveInvRel : {R : Rel A B ℓ'} → isBijectiveRel R → isBijectiveRel (invRel R)
+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
diff --git a/Cubical/Relation/Binary/Base.agda b/Cubical/Relation/Binary/Base.agda
index c8972fc1b4..50763fbe0e 100644
--- a/Cubical/Relation/Binary/Base.agda
+++ b/Cubical/Relation/Binary/Base.agda
@@ -64,6 +64,9 @@ module HeterogenousRelation {ℓ ℓ' ℓ'' : Level} {A : Type ℓ} {B : Type 
   isFunctionalRel : Type _
   isFunctionalRel = (a : A) → ∃! B (R a)
 
+  isCofunctionalRel : Type _
+  isCofunctionalRel = (b : B) → ∃! A (invRel R b)
+
   isPropIsFunctional : isProp isFunctionalRel
   isPropIsFunctional = isPropΠ λ _ → isPropIsContr
 
diff --git a/Cubical/Relation/Binary/Properties.agda b/Cubical/Relation/Binary/Properties.agda
index f93f34485c..8c99150688 100644
--- a/Cubical/Relation/Binary/Properties.agda
+++ b/Cubical/Relation/Binary/Properties.agda
@@ -8,6 +8,7 @@ open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Path
 open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Transport
 open import Cubical.Functions.FunExtEquiv
 
 open import Cubical.Data.Sigma
@@ -90,10 +91,10 @@ module _ (R : Rel A A ℓ') where
     Aset : isSet A
     Aset = reflPropRelImpliesIdentity→isSet Rrefl Rprop R→≡
 
+open HeterogenousRelation
+
 -- Functional relations are equivalent to functions
 module _ (A : Type ℓ) (B : Type ℓ') where
-  open HeterogenousRelation
-
   FunctionalRel : Type (ℓ-max ℓ (ℓ-suc ℓ'))
   FunctionalRel = Σ[ R ∈ Rel A B ℓ' ] isFunctionalRel R
 
@@ -109,6 +110,40 @@ module _ (A : Type ℓ) (B : Type ℓ') where
   Function≃FunctionalRel : (A → B) ≃ FunctionalRel
   Function≃FunctionalRel = isoToEquiv (invIso FunctionalRelIsoFunction)
 
+-- Functional relations are closed under composition
+isFunctionalCompRel : {R : Rel A B ℓ} {S : Rel B C ℓ'} → isFunctionalRel R → isFunctionalRel S → isFunctionalRel (compRel R S)
+isFunctionalCompRel {A} {B} {C} {R} {S} Rfun Sfun a = isOfHLevelRetractFromIso 0 isom contr where
+
+  contr : ∃! C (S (Rfun a .fst .fst))
+  contr = Sfun (Rfun a .fst .fst)
+
+  open Iso
+
+  isom : Iso (Σ C (compRel R S a)) (Σ C (S (Rfun a .fst .fst)))
+  isom = Σ-cong-iso-snd λ where
+    -- This is almost Σ-contractFstIso (Rfun a), but I also reassociate the Σ-type
+    c .fun (b , ab , bc) → subst⁻ (invRel S c) (cong fst (Rfun a .snd (b , ab))) bc
+    c .inv ac → Rfun a .fst .fst , Rfun a .fst .snd , ac
+    c .rightInv ac i → transp (λ j → S (isContr→isSet (Rfun a) _ _ (Rfun a .snd (Rfun a .fst)) refl i (~ j) .fst) c) i ac
+    c .leftInv (b , ab , bc) i → _ , Rfun a .snd (b , ab) i .snd , subst⁻-filler (invRel S c) (cong fst (Rfun a .snd (b , ab))) bc (~ i)
+
+-- Cofunctional relations are also closed under composition
+isCofunctionalCompRel : {R : Rel A B ℓ} {S : Rel B C ℓ'} → isCofunctionalRel R → isCofunctionalRel S → isCofunctionalRel (compRel R S)
+isCofunctionalCompRel {A} {B} {C} {R} {S} Rfun Sfun c = isOfHLevelRetractFromIso 0 isom contr where
+
+  contr : ∃! A (invRel R (Sfun c .fst .fst))
+  contr = Rfun (Sfun c .fst .fst)
+
+  open Iso
+
+  isom : Iso (Σ A (invRel (compRel R S) c)) (Σ A (invRel R (Sfun c .fst .fst)))
+  isom = Σ-cong-iso-snd λ where
+    -- This is almost Σ-contractFstIso (Sfun c), but I also reassociate the Σ-type
+    a .fun (b , ab , bc) → subst⁻ (R a) (cong fst (Sfun c .snd (b , bc))) ab
+    a .inv ab → Sfun c .fst .fst , ab , Sfun c .fst .snd
+    a .rightInv ab i → transp (λ j → R a (isContr→isSet (Sfun c) _ _ (Sfun c .snd (Sfun c .fst)) refl i (~ j) .fst)) i ab
+    a .leftInv (b , ab , bc) i → _ , subst⁻-filler (R a) (cong fst (Sfun c .snd (b , bc))) ab (~ i) , Sfun c .snd (b , bc) i .snd
+
 -- Pulling back a relation along a function.
 -- This can for example be used when restricting an equivalence relation to a subset:
 --   _~'_ = on fst _~_

From 7fcb3e0ce894a32a3e4990117d079cb9b3bbb034 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Mon, 25 Aug 2025 18:32:09 +0530
Subject: [PATCH 07/10] Explicit construction of `EquivIsoBijectiveRel`,
 `pathIsoBijectiveRel`

---
 Cubical/Foundations/Equiv/BijectiveRel.agda | 44 ++++++++++++++++-----
 Cubical/Relation/Binary/Properties.agda     |  3 ++
 2 files changed, 38 insertions(+), 9 deletions(-)

diff --git a/Cubical/Foundations/Equiv/BijectiveRel.agda b/Cubical/Foundations/Equiv/BijectiveRel.agda
index 58c5f5c6fd..f2a8aaf1c4 100644
--- a/Cubical/Foundations/Equiv/BijectiveRel.agda
+++ b/Cubical/Foundations/Equiv/BijectiveRel.agda
@@ -11,8 +11,12 @@ 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
@@ -45,20 +49,26 @@ BijectiveRelIsoΣ : Iso (BijectiveRel A B ℓ'') (Σ[ R ∈ Rel A B ℓ'' ] isFu
 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 → A i → B i → Type ℓ'') (R₀ .fst) (R₁ .fst)
+                  → 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 ℓ''} → R₀ .fst ≡ R₁ .fst → R₀ ≡ R₁
-BijectiveRelEq = Σ≡Prop λ _ → 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 .fst a = R .snd .rContr a .fst .fst
+BijectiveRel→Equiv (R , Rbij) .snd .equiv-proof b = flip (isOfHLevelRetractFromIso 0) (Rbij .lContr b) $
+  Σ-cong-iso-snd $ invIso ∘ flip isIdentitySystem.isoPath b ∘ isContrTotal→isIdentitySystem ∘ Rbij .rContr
 
 EquivIsoBijectiveRel : (A B : Type ℓ) → Iso (A ≃ B) (BijectiveRel A B ℓ)
-EquivIsoBijectiveRel A B = 
-  (A ≃ B)                                                                 Iso⟨ Σ-cong-iso-snd isEquiv-isEquiv'-Iso ⟩
-  (Σ[ f ∈ (A → B) ] (∀ a → isContr (fiber f a)))                          Iso⟨ Σ-cong-iso-fst (invIso (FunctionalRelIsoFunction A B)) ⟩
-  (Σ[ (R , _) ∈ Σ (Rel A B _) isFunctionalRel ] isFunctionalRel (flip R)) Iso⟨ Σ-assoc-Iso ⟩
-  (Σ[ R ∈ Rel A B _ ] isFunctionalRel R × isFunctionalRel (flip R))       Iso⟨ invIso BijectiveRelIsoΣ ⟩
-  BijectiveRel A B _                                                     ∎Iso
+EquivIsoBijectiveRel A B .Iso.fun e .fst = graphRel (e .fst)
+EquivIsoBijectiveRel A B .Iso.fun e .snd .rContr a = isContrSingl (e .fst a)
+EquivIsoBijectiveRel A B .Iso.fun e .snd .lContr = e .snd .equiv-proof
+EquivIsoBijectiveRel A B .Iso.inv = BijectiveRel→Equiv
+EquivIsoBijectiveRel A B .Iso.rightInv (R , Rbij) = sym $ BijectiveRelEq $
+  isIdentitySystem.equivPath ∘ isContrTotal→isIdentitySystem ∘ Rbij .rContr
+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)
@@ -90,3 +100,19 @@ 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 = BijectiveRelEq λ a b → compEquiv (ua-ungluePath-Equiv _) $
+  invEquiv $ isIdentitySystem.equivPath (isContrTotal→isIdentitySystem $ R .snd .rContr 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
diff --git a/Cubical/Relation/Binary/Properties.agda b/Cubical/Relation/Binary/Properties.agda
index 8c99150688..37387b8f2d 100644
--- a/Cubical/Relation/Binary/Properties.agda
+++ b/Cubical/Relation/Binary/Properties.agda
@@ -62,6 +62,9 @@ record isIdentitySystem {A : Type ℓ} (a : A) (C : A → Type ℓ') (r : C a) :
     ) (toPath-η i j)
   isoPath b .leftInv p = fromPathP (toPathOver p)
 
+  equivPath : ∀ b → C b ≃ (a ≡ b)
+  equivPath b = isoToEquiv (isoPath b)
+
 open isIdentitySystem
 
 isContrTotal→isIdentitySystem : {C : A → Type ℓ} (contr : ∃! A C)

From bf41a312572f7356ccaa33d64a28eb0aa651f775 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Fri, 29 Aug 2025 22:51:36 +0530
Subject: [PATCH 08/10] more

---
 Cubical/Foundations/Equiv/BijectiveRel.agda | 52 +++++++++++++++++----
 Cubical/Relation/Binary/Properties.agda     | 14 +++---
 2 files changed, 49 insertions(+), 17 deletions(-)

diff --git a/Cubical/Foundations/Equiv/BijectiveRel.agda b/Cubical/Foundations/Equiv/BijectiveRel.agda
index f2a8aaf1c4..b2d527c75f 100644
--- a/Cubical/Foundations/Equiv/BijectiveRel.agda
+++ b/Cubical/Foundations/Equiv/BijectiveRel.agda
@@ -34,6 +34,38 @@ record isBijectiveRel {A : Type ℓ} {B : Type ℓ'} (R : Rel A B ℓ'') : Type
     rContr : isFunctionalRel R
     lContr : isFunctionalRel (flip R)
 
+  trr : A → B
+  trr a = rContr a .fst .fst
+
+  trl : B → A
+  trl b = lContr b .fst .fst
+
+  liftr : ∀ a → R a (trr a)
+  liftr a = rContr a .fst .snd
+
+  liftl : ∀ b → R (trl b) b
+  liftl b = lContr b .fst .snd
+
+  rightIsId : ∀ a → isIdentitySystem (trr a) (R a) (liftr 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 (trl b) (flip R b) (liftl b)
+  leftIsId b = isContrTotal→isIdentitySystem (lContr b)
+
+  module _ (b : B) where
+    open isIdentitySystem (leftIsId b) using ()
+      renaming (isoPath to leftIsoPath; equivPath to leftEquivPath) public
+
+  isEquivTrr : isEquiv trr
+  isEquivTrr .equiv-proof b = isOfHLevelRetractFromIso 0 (Σ-cong-iso-snd (λ a → rightIsoPath a b)) (lContr b)
+
+  isEquivTrl : isEquiv trl
+  isEquivTrl .equiv-proof a = isOfHLevelRetractFromIso 0 (Σ-cong-iso-snd (λ b → leftIsoPath b a)) (rContr a)
+
 open isBijectiveRel
 
 unquoteDecl isBijectiveRelIsoΣ = declareRecordIsoΣ isBijectiveRelIsoΣ (quote isBijectiveRel)
@@ -57,17 +89,18 @@ BijectiveRelEq : {R₀ R₁ : BijectiveRel A B ℓ''} → (∀ a b → R₀ .fst
 BijectiveRelEq h = BijectiveRelPathP (funExt₂ λ a b → ua (h a b))
 
 BijectiveRel→Equiv : BijectiveRel A B ℓ → A ≃ B
-BijectiveRel→Equiv R .fst a = R .snd .rContr a .fst .fst
-BijectiveRel→Equiv (R , Rbij) .snd .equiv-proof b = flip (isOfHLevelRetractFromIso 0) (Rbij .lContr b) $
-  Σ-cong-iso-snd $ invIso ∘ flip isIdentitySystem.isoPath b ∘ isContrTotal→isIdentitySystem ∘ Rbij .rContr
+BijectiveRel→Equiv (R , Rbij) .fst = trr Rbij
+BijectiveRel→Equiv (R , Rbij) .snd = isEquivTrr 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 e .fst = graphRel (e .fst)
-EquivIsoBijectiveRel A B .Iso.fun e .snd .rContr a = isContrSingl (e .fst a)
-EquivIsoBijectiveRel A B .Iso.fun e .snd .lContr = e .snd .equiv-proof
+EquivIsoBijectiveRel A B .Iso.fun = Equiv→BijectiveRel
 EquivIsoBijectiveRel A B .Iso.inv = BijectiveRel→Equiv
-EquivIsoBijectiveRel A B .Iso.rightInv (R , Rbij) = sym $ BijectiveRelEq $
-  isIdentitySystem.equivPath ∘ isContrTotal→isIdentitySystem ∘ Rbij .rContr
+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 ℓ)
@@ -110,8 +143,7 @@ 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 = BijectiveRelEq λ a b → compEquiv (ua-ungluePath-Equiv _) $
-  invEquiv $ isIdentitySystem.equivPath (isContrTotal→isIdentitySystem $ R .snd .rContr a) b
+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 _
diff --git a/Cubical/Relation/Binary/Properties.agda b/Cubical/Relation/Binary/Properties.agda
index 37387b8f2d..189a74188e 100644
--- a/Cubical/Relation/Binary/Properties.agda
+++ b/Cubical/Relation/Binary/Properties.agda
@@ -51,18 +51,18 @@ record isIdentitySystem {A : Type ℓ} (a : A) (C : A → Type ℓ') (r : C a) :
 
   open Iso
 
-  isoPath : ∀ b → Iso (C b) (a ≡ b)
-  isoPath b .fun = toPath
-  isoPath b .inv p = subst C p r
-  isoPath b .rightInv p i j = hcomp (λ k → λ where
+  isoPath : ∀ b → Iso (a ≡ b) (C b)
+  isoPath b .fun p = subst C p r
+  isoPath b .inv = toPath
+  isoPath b .rightInv p = fromPathP (toPathOver p)
+  isoPath b .leftInv p i j = hcomp (λ k → λ where
       (i = i0) → toPath (transport-filler (cong C p) r k) j
       (i = i1) → p (j ∧ k)
       (j = i0) → a
       (j = i1) → p k
     ) (toPath-η i j)
-  isoPath b .leftInv p = fromPathP (toPathOver p)
 
-  equivPath : ∀ b → C b ≃ (a ≡ b)
+  equivPath : ∀ b → (a ≡ b) ≃ C b
   equivPath b = isoToEquiv (isoPath b)
 
 open isIdentitySystem
@@ -108,7 +108,7 @@ module _ (A : Type ℓ) (B : Type ℓ') where
   FunctionalRelIsoFunction .inv f = graphRel f , graphRelIsFunctional f
   FunctionalRelIsoFunction .rightInv f = refl
   FunctionalRelIsoFunction .leftInv (R , Rfun) = Σ≡Prop isPropIsFunctional $ funExt₂ λ a →
-    isoToPath ∘ invIso ∘ isoPath (isContrTotal→isIdentitySystem $ Rfun a)
+    isoToPath ∘ isoPath (isContrTotal→isIdentitySystem $ Rfun a)
 
   Function≃FunctionalRel : (A → B) ≃ FunctionalRel
   Function≃FunctionalRel = isoToEquiv (invIso FunctionalRelIsoFunction)

From 5479bcf1be041cb49b0b5bd0180770b22b2d0ce6 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Thu, 2 Oct 2025 19:49:01 +0530
Subject: [PATCH 09/10] rename trr and trl

---
 Cubical/Foundations/Equiv/BijectiveRel.agda | 32 ++++++++++-----------
 1 file changed, 16 insertions(+), 16 deletions(-)

diff --git a/Cubical/Foundations/Equiv/BijectiveRel.agda b/Cubical/Foundations/Equiv/BijectiveRel.agda
index b2d527c75f..e9ed01f83b 100644
--- a/Cubical/Foundations/Equiv/BijectiveRel.agda
+++ b/Cubical/Foundations/Equiv/BijectiveRel.agda
@@ -34,37 +34,37 @@ record isBijectiveRel {A : Type ℓ} {B : Type ℓ'} (R : Rel A B ℓ'') : Type
     rContr : isFunctionalRel R
     lContr : isFunctionalRel (flip R)
 
-  trr : A → B
-  trr a = rContr a .fst .fst
+  fun : A → B
+  fun a = rContr a .fst .fst
 
-  trl : B → A
-  trl b = lContr b .fst .fst
+  inv : B → A
+  inv b = lContr b .fst .fst
 
-  liftr : ∀ a → R a (trr a)
-  liftr a = rContr a .fst .snd
+  funR : ∀ a → R a (fun a)
+  funR a = rContr a .fst .snd
 
-  liftl : ∀ b → R (trl b) b
-  liftl b = lContr b .fst .snd
+  invR : ∀ b → R (inv b) b
+  invR b = lContr b .fst .snd
 
-  rightIsId : ∀ a → isIdentitySystem (trr a) (R a) (liftr a)
+  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 (trl b) (flip R b) (liftl b)
+  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
 
-  isEquivTrr : isEquiv trr
-  isEquivTrr .equiv-proof b = isOfHLevelRetractFromIso 0 (Σ-cong-iso-snd (λ a → rightIsoPath a b)) (lContr b)
+  isEquivFun : isEquiv fun
+  isEquivFun .equiv-proof b = isOfHLevelRetractFromIso 0 (Σ-cong-iso-snd (λ a → rightIsoPath a b)) (lContr b)
 
-  isEquivTrl : isEquiv trl
-  isEquivTrl .equiv-proof a = isOfHLevelRetractFromIso 0 (Σ-cong-iso-snd (λ b → leftIsoPath b a)) (rContr a)
+  isEquivInv : isEquiv inv
+  isEquivInv .equiv-proof a = isOfHLevelRetractFromIso 0 (Σ-cong-iso-snd (λ b → leftIsoPath b a)) (rContr a)
 
 open isBijectiveRel
 
@@ -89,8 +89,8 @@ BijectiveRelEq : {R₀ R₁ : BijectiveRel A B ℓ''} → (∀ a b → R₀ .fst
 BijectiveRelEq h = BijectiveRelPathP (funExt₂ λ a b → ua (h a b))
 
 BijectiveRel→Equiv : BijectiveRel A B ℓ → A ≃ B
-BijectiveRel→Equiv (R , Rbij) .fst = trr Rbij
-BijectiveRel→Equiv (R , Rbij) .snd = isEquivTrr Rbij
+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)

From 861451e7989984b45b5fe33efbcab2000cdbec5f Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Thu, 2 Oct 2025 21:01:33 +0530
Subject: [PATCH 10/10] fix whitespace

---
 Cubical/Foundations/Function.agda | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Cubical/Foundations/Function.agda b/Cubical/Foundations/Function.agda
index 5c6ebefee8..ab4fe4733d 100644
--- a/Cubical/Foundations/Function.agda
+++ b/Cubical/Foundations/Function.agda
@@ -182,4 +182,3 @@ homotopyIdComm {f = f} H a i j = hcomp (λ k → λ where
     (j = i0) → f (H a (~ k ∧ ~ i))
     (j = i1) → H a (~ k)
   ) (H (H a (~ i ∨ j)) j)
-