diff --git a/Cubical/Foundations/Equiv/BijectiveRel.agda b/Cubical/Foundations/Equiv/BijectiveRel.agda
new file mode 100644
index 0000000000..e9ed01f83b
--- /dev/null
+++ b/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
diff --git a/Cubical/Foundations/Function.agda b/Cubical/Foundations/Function.agda
index 99f4a019ba..ab4fe4733d 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,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)
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/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..7eb09b64c6 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
 
 -}
@@ -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
diff --git a/Cubical/Relation/Binary/Base.agda b/Cubical/Relation/Binary/Base.agda
index 500c849b9c..50763fbe0e 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,30 +26,56 @@ private
 Rel : ∀ {ℓa ℓb} (A : Type ℓa) (B : Type ℓb) (ℓ' : Level) → Type (ℓ-max (ℓ-max ℓa ℓb) (ℓ-suc ℓ'))
 Rel A B ℓ' = A → B → Type ℓ'
 
-PropRel : ∀ {ℓ} (A B : Type ℓ) (ℓ' : Level) → Type (ℓ-max ℓ (ℓ-suc ℓ'))
+idRel : ∀ {ℓ} (A : Type ℓ) → Rel A A ℓ
+idRel A = _≡_
+
+invRel : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} → Rel A B ℓ'' → Rel B A ℓ''
+invRel R b a = R a b
+
+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} (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 : 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 .fst a a' = ∥ a ≡ a' ∥₁
-idPropRel A .snd _ _ = squash₁
+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 R S .fst a c = ∥ Σ[ b ∈ _ ] (R .fst a b × S .fst b c) ∥₁
-compPropRel R S .snd _ _ = squash₁
+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 _
+  isFunctionalRel = (a : A) → ∃! B (R a)
+
+  isCofunctionalRel : Type _
+  isCofunctionalRel = (b : B) → ∃! A (invRel R b)
+
+  isPropIsFunctional : isProp isFunctionalRel
+  isPropIsFunctional = isPropΠ λ _ → isPropIsContr
+
+open HeterogenousRelation
+
+graphRelIsFunctional : ∀ {ℓ ℓ'} {A : Type ℓ} {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 ℓ ℓ')
   isRefl = (a : A) → R a a
@@ -141,7 +168,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..189a74188e 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
@@ -5,6 +6,9 @@ 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.Foundations.Transport
 open import Cubical.Functions.FunExtEquiv
 
 open import Cubical.Data.Sigma
@@ -14,8 +18,59 @@ 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
+    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 (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)
+
+  equivPath : ∀ b → (a ≡ b) ≃ C b
+  equivPath b = isoToEquiv (isoPath b)
+
+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
@@ -39,6 +94,59 @@ 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
+  FunctionalRel : Type (ℓ-max ℓ (ℓ-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 ∘ isoPath (isContrTotal→isIdentitySystem $ Rfun a)
+
+  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 _~_