Add some conversions

src/Function/Bijection/Strict.agda

@@ -15,8 +15,16 @@ open import Relation.Binary.PropositionalEquality as P
 open import Function.Equality as F
  using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_)
 open import Function.Injection as Inj hiding (id; _∘_; injection)
-open import Function.Surjection.Strict as Surj hiding (id; _∘_; surjection)
-open import Function.LeftInverse.Strict as Left hiding (id; _∘_; leftInverse)
+open import Function.Surjection.Strict as Surj hiding (id; _∘_;
+ surjection;
+ non-strict-to-strict;
+ strict-to-non-strict)
+open import Function.LeftInverse.Strict as Left hiding (id; _∘_;
+ leftInverse;
+ non-strict-to-strict;
+ strict-to-non-strict)
+
+import Function.Bijection as NonStrict
 
 ------------------------------------------------------------------------
 -- Bijective functions.
@@ -34,6 +42,29 @@ record Bijective {f₁ f₂ t₁ t₂}
  left-inverse-of : from LeftInverseOf to
  left-inverse-of x y y≈tox = injective (right-inverse-of (to ⟨$⟩ x) (from ⟨$⟩ y) (F.cong from y≈tox))
 
+------------------------------------------------------------------------
+-- Relation to non-strict versions
+
+non-strict-to-strict :
+ ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
+ (f : To ⟶ From) →
+ NonStrict.Bijective f →
+ Bijective f
+non-strict-to-strict f ns = record
+ { injective = injective
+ ; surjective = Surj.non-strict-to-strict f surjective
+ } where open NonStrict.Bijective ns
+
+strict-to-non-strict :
+ ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
+ (f : From ⟶ To) →
+ Bijective f →
+ NonStrict.Bijective f
+strict-to-non-strict f ns = record
+ { injective = injective
+ ; surjective = Surj.strict-to-non-strict f surjective
+ } where open Bijective ns
+
 ------------------------------------------------------------------------
 -- The set of all bijections between two setoids.
 

src/Function/Inverse/Strict.agda

@@ -10,14 +10,20 @@ module Function.Inverse.Strict where
 
 open import Level
 open import Function.Base using (flip)
-open import Function.Bijection.Strict hiding (id; _∘_; bijection)
+open import Function.Bijection.Strict hiding (id; _∘_; bijection;
+ non-strict-to-strict;
+ strict-to-non-strict)
 open import Function.Equality as F
  using (_⟶_) renaming (_∘_ to _⟪∘⟫_)
-open import Function.LeftInverse.Strict as Left hiding (id; _∘_)
+open import Function.LeftInverse.Strict as Left hiding (id; _∘_;
+ non-strict-to-strict;
+ strict-to-non-strict)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P using (_≗_; _≡_)
 open import Relation.Unary using (Pred)
 
+import Function.Inverse as NonStrict
+
 ------------------------------------------------------------------------
 -- Inverses
 
@@ -29,6 +35,31 @@ record _InverseOf_ {f₁ f₂ t₁ t₂}
  left-inverse-of : from LeftInverseOf to
  right-inverse-of : from RightInverseOf to
 
+------------------------------------------------------------------------
+-- Relation to non-strict versions
+
+non-strict-to-strict :
+ ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
+ (f : To ⟶ From) →
+ (g : From ⟶ To) →
+ f NonStrict.InverseOf g →
+ f InverseOf g
+non-strict-to-strict f g ns = record
+ { left-inverse-of = Left.non-strict-to-strict f g left-inverse-of
+ ; right-inverse-of = Left.non-strict-to-strict g f right-inverse-of
+ } where open NonStrict._InverseOf_ ns
+
+strict-to-non-strict :
+ ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
+ (f : To ⟶ From) →
+ (g : From ⟶ To) →
+ f InverseOf g →
+ f NonStrict.InverseOf g
+strict-to-non-strict f g ns = record
+ { left-inverse-of = Left.strict-to-non-strict f g left-inverse-of
+ ; right-inverse-of = Left.strict-to-non-strict g f right-inverse-of
+ } where open _InverseOf_ ns
+
 ------------------------------------------------------------------------
 -- The set of all inverses between two setoids
 

src/Function/LeftInverse/Strict.agda

@@ -18,7 +18,7 @@ open import Function.Equivalence using (Equivalence)
 open import Function.Injection using (Injective; Injection)
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
-import Function.LeftInverse as LI
+import Function.LeftInverse as NonStrict
 
 ------------------------------------------------------------------------
 -- Left and right inverses.
@@ -41,19 +41,23 @@ f RightInverseOf g = g LeftInverseOf f
 
 non-strict-to-strict :
  ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
- LI._LeftInverseOf_ {From = From} {To = To} ⇒
- _LeftInverseOf_ {From = From} {To = To}
-non-strict-to-strict {From = From} {x = f} {y = g} ns x y y∼gx = begin
+ (f : To ⟶ From) →
+ (g : From ⟶ To) →
+ f NonStrict.LeftInverseOf g →
+ f LeftInverseOf g
+non-strict-to-strict {From = From} f g ns x y y∼gx = begin
  f ⟨$⟩ y ≈⟨ Eq.cong f y∼gx ⟩
  f ⟨$⟩ (g ⟨$⟩ x) ≈⟨ ns x ⟩
  x ∎
  where open EqReasoning From
 
 strict-to-non-strict :
  ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
- _LeftInverseOf_ {From = From} {To = To} ⇒
- LI._LeftInverseOf_ {From = From} {To = To}
-strict-to-non-strict {To = To} {x = f} {y = g} str x = str x (g ⟨$⟩ x) refl
+ (f : To ⟶ From) →
+ (g : From ⟶ To) →
+ f LeftInverseOf g →
+ f NonStrict.LeftInverseOf g
+strict-to-non-strict {To = To} f g str x = str x (g ⟨$⟩ x) refl
  where open Setoid To
 
 ------------------------------------------------------------------------
@@ -70,8 +74,8 @@ record LeftInverse {f₁ f₂ t₁ t₂}
  private
  open module F = Setoid From
  open module T = Setoid To
- non-strict : from LI.LeftInverseOf to
- non-strict = strict-to-non-strict {x = from} {y = to} left-inverse-of
+ non-strict : from NonStrict.LeftInverseOf to
+ non-strict = strict-to-non-strict from to left-inverse-of
  open EqReasoning From
 
  injective : Injective to

src/Function/Surjection/Strict.agda

@@ -13,11 +13,15 @@ open import Function.Equality as F
  using (_⟶_) renaming (_∘_ to _⟪∘⟫_)
 open import Function.Equivalence using (Equivalence)
 open import Function.Injection hiding (id; _∘_; injection)
-open import Function.LeftInverse.Strict as Left hiding (id; _∘_)
+open import Function.LeftInverse.Strict as Left hiding (id; _∘_;
+ non-strict-to-strict;
+ strict-to-non-strict)
 open import Data.Product
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
+import Function.Surjection as NonStrict
+
 ------------------------------------------------------------------------
 -- Surjective functions.
 
@@ -29,6 +33,29 @@ record Surjective {f₁ f₂ t₁ t₂}
  from : To ⟶ From
  right-inverse-of : from RightInverseOf to
 
+------------------------------------------------------------------------
+-- Relation to non-strict versions
+
+non-strict-to-strict :
+ ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
+ (f : To ⟶ From) →
+ NonStrict.Surjective f →
+ Surjective f
+non-strict-to-strict f ns = record
+ { from = from
+ ; right-inverse-of = Left.non-strict-to-strict f from right-inverse-of
+ } where open NonStrict.Surjective ns
+
+strict-to-non-strict :
+ ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
+ (f : From ⟶ To) →
+ Surjective f →
+ NonStrict.Surjective f
+strict-to-non-strict f ns = record
+ { from = from
+ ; right-inverse-of = Left.strict-to-non-strict f from right-inverse-of
+ } where open Surjective ns
+
 ------------------------------------------------------------------------
 -- The set of all surjections from one setoid to another.