Add more tests

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

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

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

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