diff --git a/src/Function/Bijection/Strict.agda b/src/Function/Bijection/Strict.agda
index dd23cf9903..147b508aaf 100644
--- a/src/Function/Bijection/Strict.agda
+++ b/src/Function/Bijection/Strict.agda
@@ -120,3 +120,13 @@ f ∘ g = record
     ; surjective = Surjection.surjective (Surj._∘_ (surjection f) (surjection g))
     }
   } where open Bijection
+
+private
+  test : ∀ {a b} {A : Setoid a b} {f g h : Bijection A A} → (f ∘ g) ∘ h ≡ f ∘ (g ∘ h)
+  test = P.refl
+
+  testid : ∀ {a b} {A : Setoid a b} {f : Bijection A A} → f ∘ id ≡ f
+  testid = P.refl
+
+  idtest : ∀ {a b} {A : Setoid a b} {f : Bijection A A} → id ∘ f ≡ f
+  idtest = P.refl
diff --git a/src/Function/Inverse/Strict.agda b/src/Function/Inverse/Strict.agda
index b46b230596..8173381c00 100644
--- a/src/Function/Inverse/Strict.agda
+++ b/src/Function/Inverse/Strict.agda
@@ -189,5 +189,11 @@ zip t f pres eq₁ eq₂ = record
   } where open Inverse
 
 private
-  test : ∀ {a b} {A : Setoid a b} {f g h : Inverse A A} → f ∘ (g ∘ h) ≡ (f ∘ g) ∘ h
+  test : ∀ {a b} {A : Setoid a b} {f g h : Inverse A A} → (f ∘ g) ∘ h ≡ f ∘ (g ∘ h)
   test = P.refl
+
+  testid : ∀ {a b} {A : Setoid a b} {f : Inverse A A} → f ∘ id ≡ f
+  testid = P.refl
+
+  idtest : ∀ {a b} {A : Setoid a b} {f : Inverse A A} → id ∘ f ≡ f
+  idtest = P.refl
diff --git a/src/Function/LeftInverse/Strict.agda b/src/Function/LeftInverse/Strict.agda
index e839960b22..e5bd7c7ff7 100644
--- a/src/Function/LeftInverse/Strict.agda
+++ b/src/Function/LeftInverse/Strict.agda
@@ -150,3 +150,9 @@ _∘_ {F = F} f g = record
 private
   test : ∀ {a b} {A : Setoid a b} {f g h : LeftInverse A A} → (f ∘ g) ∘ h ≡ f ∘ (g ∘ h)
   test = P.refl
+
+  testid : ∀ {a b} {A : Setoid a b} {f : LeftInverse A A} → f ∘ id ≡ f
+  testid = P.refl
+
+  idtest : ∀ {a b} {A : Setoid a b} {f : LeftInverse A A} → id ∘ f ≡ f
+  idtest = P.refl
diff --git a/src/Function/Surjection/Strict.agda b/src/Function/Surjection/Strict.agda
index 8a83eb74b8..f30420f9d3 100644
--- a/src/Function/Surjection/Strict.agda
+++ b/src/Function/Surjection/Strict.agda
@@ -126,5 +126,11 @@ f ∘ g = record
   g∘f = Left._∘_ (right-inverse g) (right-inverse f)
 
 private
-  test : ∀ {a b} {A : Setoid a b} {f g h : Surjection A A} → f ∘ (g ∘ h) ≡ (f ∘ g) ∘ h
+  test : ∀ {a b} {A : Setoid a b} {f g h : Surjection A A} → (f ∘ g) ∘ h ≡ f ∘ (g ∘ h)
   test = P.refl
+
+  testid : ∀ {a b} {A : Setoid a b} {f : Surjection A A} → f ∘ id ≡ f
+  testid = P.refl
+
+  idtest : ∀ {a b} {A : Setoid a b} {f : Surjection A A} → id ∘ f ≡ f
+  idtest = P.refl