[Import] Function.Nary...Function* (#2641)

jmougeot · jamesmckinna · web-flow · commit e65f729b8780 · 2025-03-17T11:48:58.000Z
* [Import] ...

* fix whitespace

* Update src/Function/Related/TypeIsomorphisms.agda

Co-authored-by: jamesmckinna &lt;31931406+jamesmckinna@users.noreply.github.com&gt;

* fix

---------

Co-authored-by: jamesmckinna &lt;31931406+jamesmckinna@users.noreply.github.com&gt;
diff --git a/src/Function/Bundles.agda b/src/Function/Bundles.agda
@@ -26,8 +26,7 @@ open import Level using (Level; _⊔_; suc)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Core using (_Preserves_⟶_)
-open import Relation.Binary.PropositionalEquality.Core as ≡
-  using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as ≡
 open import Function.Consequences.Propositional
 open Setoid using (isEquivalence)
diff --git a/src/Function/Nary/NonDependent.agda b/src/Function/Nary/NonDependent.agda
@@ -22,8 +22,7 @@ open import Data.Product.Nary.NonDependent
   using (Product; uncurryₙ; Equalₙ; curryₙ; fromEqualₙ; toEqualₙ)
 open import Function.Base using (_∘′_; _$′_; const; flip)
 open import Relation.Unary using (IUniversal)
-open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 
 private
   variable
diff --git a/src/Function/Nary/NonDependent/Base.agda b/src/Function/Nary/NonDependent/Base.agda
@@ -17,7 +17,7 @@ module Function.Nary.NonDependent.Base where
 open import Level using (Level; 0ℓ; _⊔_)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product.Base using (_×_; _,_)
-open import Data.Unit.Polymorphic.Base
+open import Data.Unit.Polymorphic.Base using (⊤; tt)
 open import Function.Base using (_∘′_; _$′_; const; flip)
 
 private
diff --git a/src/Function/Properties.agda b/src/Function/Properties.agda
@@ -11,7 +11,7 @@ module Function.Properties where
 open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Function.Base using (flip; _∘_)
 open import Function.Bundles using (_↔_; mk↔ₛ′; Inverse)
-open import Level
+open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core
   using (trans; cong; cong′)
 
diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda
@@ -8,8 +8,8 @@
 
 module Function.Properties.Bijection where
 
-open import Function.Bundles using (Bijection; Inverse; Equivalence;
-  _⤖_; _↔_; _⇔_)
+open import Function.Bundles
+  using (Bijection; Inverse; Equivalence; _⤖_; _↔_; _⇔_)
 open import Level using (Level)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)
diff --git a/src/Function/Properties/Equivalence.agda b/src/Function/Properties/Equivalence.agda
@@ -9,9 +9,9 @@
 
 module Function.Properties.Equivalence where
 
-open import Function.Bundles
-open import Level
-open import Relation.Binary.Definitions
+open import Function.Bundles using (Func; Equivalence; _⇔_; _⟶_)
+open import Level using (Level; suc; _⊔_)
+open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive; Sym; Trans)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)
 import Relation.Binary.PropositionalEquality.Properties as ≡
diff --git a/src/Function/Properties/Injection.agda b/src/Function/Properties/Injection.agda
@@ -8,11 +8,10 @@
 
 module Function.Properties.Injection where
 
-open import Function.Base
-open import Function.Definitions
-open import Function.Bundles
-import Function.Construct.Identity as Identity
-import Function.Construct.Composition as Compose
+open import Function.Definitions using (Injective)
+open import Function.Bundles using (Injection; Func; _⟶_; _↣_)
+import Function.Construct.Identity as Identity using (injection)
+import Function.Construct.Composition as Compose using (injection)
 open import Level using (Level)
 open import Data.Product.Base using (proj₁; proj₂)
 open import Relation.Binary.Definitions
diff --git a/src/Function/Properties/Inverse.agda b/src/Function/Properties/Inverse.agda
@@ -11,15 +11,15 @@ module Function.Properties.Inverse where
 open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Function.Bundles
-import Function.Properties.RightInverse as RightInverse
+import Function.Properties.RightInverse as RightInverse using (to-from)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (REL)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
-import Relation.Binary.PropositionalEquality.Properties as ≡
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 import Function.Consequences.Setoid as Consequences
+  using (inverseʳ⇒injective; inverseˡ⇒surjective; inverseᵇ⇒bijective)
 
 import Function.Construct.Identity as Identity
 import Function.Construct.Symmetry as Symmetry
diff --git a/src/Function/Properties/Inverse/HalfAdjointEquivalence.agda b/src/Function/Properties/Inverse/HalfAdjointEquivalence.agda
@@ -12,8 +12,8 @@ open import Function.Base using (id; _∘_)
 open import Function.Bundles using (Inverse; _↔_; mk↔ₛ′)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.PropositionalEquality
-  using (_≡_; refl; cong; sym; trans; trans-reflʳ; cong-≡id; cong-∘; naturality;
-         cong-id; trans-assoc; trans-symˡ; module ≡-Reasoning)
+  using (_≡_; refl; cong; sym; trans; trans-reflʳ; cong-≡id; cong-∘; naturality
+        ; cong-id; trans-assoc; trans-symˡ; module ≡-Reasoning)
 
 private
   variable
diff --git a/src/Function/Properties/RightInverse.agda b/src/Function/Properties/RightInverse.agda
@@ -8,8 +8,8 @@
 
 module Function.Properties.RightInverse where
 
-open import Function.Base
-open import Function.Definitions
+open import Function.Base using (id; _∘_)
+open import Function.Definitions using (Inverseˡ; Inverseʳ)
 open import Function.Bundles
 open import Function.Consequences using (inverseˡ⇒surjective)
 open import Level using (Level)
diff --git a/src/Function/Properties/Surjection.agda b/src/Function/Properties/Surjection.agda
@@ -10,13 +10,13 @@ module Function.Properties.Surjection where
 
 open import Function.Base using (_∘_; _$_)
 open import Function.Definitions using (Surjective; Injective; Congruent)
-open import Function.Bundles using (Func; Surjection; _↠_; _⟶_; _↪_; mk↪;
-  _⇔_; mk⇔)
-import Function.Construct.Identity as Identity
-import Function.Construct.Composition as Compose
+open import Function.Bundles
+  using (Func; Surjection; _↠_; _⟶_; _↪_; mk↪; _⇔_; mk⇔)
+import Function.Construct.Identity as Identity using (surjection)
+import Function.Construct.Composition as Compose using (surjection)
 open import Level using (Level)
 open import Data.Product.Base using (proj₁; proj₂)
-import Relation.Binary.PropositionalEquality.Core as ≡
+import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl)
 open import Relation.Binary.Definitions using (Reflexive; Trans)
 open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
diff --git a/src/Function/Related/Propositional.agda b/src/Function/Related/Propositional.agda
@@ -8,15 +8,16 @@
 
 module Function.Related.Propositional where
 
-open import Level
+open import Level using (Level; _⊔_)
 open import Relation.Binary
   using (Rel; REL; Sym; Reflexive; Trans; IsEquivalence; Setoid; IsPreorder; Preorder)
 open import Function.Bundles
-open import Function.Base
+  using (Func; Inverse; _⇔_; _↣_; _↠_; _↪_; _⟶_; _↔_; mk⟶; Equivalence; Injection
+        ; Surjection; RightInverse)
+open import Function.Base using (id; flip; _∘_; _∘′_; _$_)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as ≡
 open import Relation.Binary.Reasoning.Syntax
-
 open import Function.Properties.Surjection   using (↠⇒↪; ↠⇒⇔)
 open import Function.Properties.RightInverse using (↪⇒↠)
 open import Function.Properties.Bijection    using (⤖⇒↔; ⤖⇒⇔)
diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda
@@ -9,7 +9,14 @@
 
 module Function.Related.TypeIsomorphisms where
 
-open import Algebra
+open import Algebra.Bundles public
+  using (Magma; Semigroup; Monoid; CommutativeMonoid; CommutativeSemiring)
+open import Algebra.Definitions
+  using (Identity; LeftIdentity; RightIdentity; Zero; LeftZero; RightZero
+        ; Associative; _DistributesOverˡ_; _DistributesOverʳ_; _DistributesOver_)
+open import Algebra.Structures public
+  using (IsMagma; IsSemigroup; IsMonoid; IsCommutativeMonoid
+        ; IsCommutativeSemiring)
 open import Algebra.Structures.Biased using (isCommutativeSemiringˡ)
 open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Data.Bool.Base using (true; false)
@@ -360,3 +367,4 @@ True↔ (false because ofⁿ ¬p) _ =
 ∃-≡ : ∀ (P : A → Set b) {x} → P x ↔ (∃[ y ] y ≡ x × P y)
 ∃-≡ P {x} = mk↔ₛ′ (λ Px → x , refl , Px) (λ where (_ , refl , Py) → Py)
   (λ where (_ , refl , _) → refl) (λ where _ → refl)
+
diff --git a/src/Function/Related/TypeIsomorphisms/Solver.agda b/src/Function/Related/TypeIsomorphisms/Solver.agda
@@ -12,6 +12,7 @@ module Function.Related.TypeIsomorphisms.Solver where
 
 open import Algebra using (CommutativeSemiring)
 import Algebra.Solver.Ring.NaturalCoefficients.Default
+  using (solve; con; _:*_; _:+_; _:=_)
 open import Data.Empty.Polymorphic using (⊥)
 open import Data.Product.Base using (_×_)
 open import Data.Sum.Base using (_⊎_)
@@ -20,7 +21,7 @@ open import Level using (Level)
 open import Function.Bundles using (_↔_)
 open import Function.Properties.Inverse using (↔-refl)
 open import Function.Related.Propositional as Related
-open import Function.Related.TypeIsomorphisms
+open import Function.Related.TypeIsomorphisms using (×-⊎-commutativeSemiring)
 
 ------------------------------------------------------------------------
 -- The solver
diff --git a/src/Function/Structures/Biased.agda b/src/Function/Structures/Biased.agda
@@ -10,20 +10,24 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Structures using (IsEquivalence)
+
 
 module Function.Structures.Biased {a b ℓ₁ ℓ₂}
   {A : Set a} (_≈₁_ : Rel A ℓ₁) -- Equality over the domain
   {B : Set b} (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
   where
 
 open import Data.Product.Base as Product using (∃; _×_; _,_)
-open import Function.Base
-open import Function.Definitions
-open import Function.Structures _≈₁_ _≈₂_
+open import Function.Base using (_∘_; id)
+open import Function.Definitions using(StrictlySurjective; StrictlyInverseˡ; StrictlyInverseʳ; Congruent)
 open import Function.Consequences.Setoid
+  using (strictlySurjective⇒surjective; strictlyInverseˡ⇒inverseˡ
+        ; strictlyInverseʳ⇒inverseʳ)
 open import Level using (_⊔_)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
+
+open import Function.Structures _≈₁_ _≈₂_
 
 ------------------------------------------------------------------------
 -- Surjection
