Merge pull request #406 from agda/bump-stdlib-2.0

Bump stdlib to 2.0

.github/workflows/ci-ubuntu.yml

@@ -45,8 +45,8 @@ on:
 ########################################################################
 
 env:
-  AGDA_COMMIT: tags/v2.6.3
-  STDLIB_VERSION: 1.7.2
+  AGDA_COMMIT: tags/v2.6.4
+  STDLIB_VERSION: "2.0"
 
   GHC_VERSION: 8.10.7
   CABAL_VERSION: 3.6.2.0

agda-categories.agda-lib

@@ -1,3 +1,3 @@
 name: agda-categories
-depend: standard-library-1.7.2
+depend: standard-library-2.0
 include: src/

src/Categories/Adjoint.agda

@@ -7,16 +7,14 @@ open import Level
 
 open import Data.Product using (_,_; _×_)
 open import Function using (_$_) renaming (_∘_ to _∙_)
-open import Function.Equality using (Π; _⟶_)
-import Function.Inverse as FI
+open import Function.Bundles using (Inverse)
 open import Relation.Binary using (Rel; IsEquivalence; Setoid)
 open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 
 -- be explicit in imports to 'see' where the information comes from
 open import Categories.Category.Core using (Category)
 open import Categories.Category.Product using (Product; _⁂_)
-open import Categories.Category.Instance.Setoids
-open import Categories.Morphism
+open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
 open import Categories.Functor.Bifunctor using (Bifunctor)
 open import Categories.Functor.Hom using (Hom[_][-,-])
@@ -91,23 +89,19 @@ record Adjoint (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ leve
   module Hom[-,R-] = Functor Hom[-,R-]
 
   -- Inverse is more 'categorical' than bijection defined via injection/surjection
-  Hom-inverse : ∀ A B → FI.Inverse (Hom[L-,-].F₀ (A , B)) (Hom[-,R-].F₀ (A , B))
+  Hom-inverse : ∀ A B → Inverse (Hom[L-,-].F₀ (A , B)) (Hom[-,R-].F₀ (A , B))
   Hom-inverse A B = record
-    { to = record
-      { _⟨$⟩_ = Ladjunct {A} {B}
-      ; cong = C.∘-resp-≈ˡ ∙ R.F-resp-≈
-      }
-    ; from = record
-      { _⟨$⟩_ = Radjunct {A} {B}
-      ; cong = D.∘-resp-≈ʳ ∙ L.F-resp-≈
-      }
-    ; inverse-of = record
-      { left-inverse-of = λ _ → RLadjunct≈id
-      ; right-inverse-of = λ _ → LRadjunct≈id
+    { to = Ladjunct {A} {B}
+    ; to-cong = C.∘-resp-≈ˡ ∙ R.F-resp-≈
+    ; from = Radjunct {A} {B}
+    ; from-cong = D.∘-resp-≈ʳ ∙ L.F-resp-≈
+    ; inverse = record
+      { fst = λ p → C.∘-resp-≈ˡ (R.F-resp-≈ p) C.HomReasoning.○ LRadjunct≈id
+      ; snd = λ p → D.∘-resp-≈ʳ (L.F-resp-≈ p) D.HomReasoning.○ RLadjunct≈id
       }
     }
 
-  module Hom-inverse {A} {B} = FI.Inverse (Hom-inverse A B)
+  module Hom-inverse {A} {B} = Inverse (Hom-inverse A B)
 
   op : Adjoint R.op L.op
   op = record
@@ -188,15 +182,15 @@ record Adjoint (L : Functor C D) (R : Functor D C) : Set (levelOfTerm L ⊔ leve
     Hom-NI = record
       { F⇒G = ntHelper record
         { η       = λ _ → record
-          { _⟨$⟩_ = λ f → lift (Ladjunct (lower f))
-          ; cong  = λ eq → lift (Ladjunct-resp-≈ (lower eq))
+          { to = λ f → lift (Ladjunct (lower f))
+          ; cong = λ eq → lift (Ladjunct-resp-≈ (lower eq))
           }
         ; commute = λ _ eq → lift $ Ladjunct-comm (lower eq)
         }
       ; F⇐G = ntHelper record
         { η       = λ _ → record
-          { _⟨$⟩_ = λ f → lift (Radjunct (lower f))
-          ; cong  = λ eq → lift (Radjunct-resp-≈ (lower eq))
+          { to = λ f → lift (Radjunct (lower f))
+          ; cong = λ eq → lift (Radjunct-resp-≈ (lower eq))
           }
         ; commute = λ _ eq → lift $ Radjunct-comm (lower eq)
         }

src/Categories/Adjoint/Compose.agda

@@ -7,8 +7,6 @@ open import Level
 
 open import Data.Product using (_,_; _×_)
 open import Function using (_$_) renaming (_∘_ to _∙_)
-open import Function.Equality using (Π; _⟶_)
-import Function.Inverse as FI
 open import Relation.Binary using (Rel; IsEquivalence; Setoid)
 
 -- be explicit in imports to 'see' where the information comes from

src/Categories/Adjoint/Equivalents.agda

@@ -8,16 +8,15 @@ open import Level
 
 open import Data.Product using (_,_; _×_)
 open import Function using (_$_) renaming (_∘_ to _∙_)
-open import Function.Equality using (Π; _⟶_)
-import Function.Inverse as FI
+open import Function.Bundles using (Equivalence; LeftInverse; Func; _⟨$⟩_)
 open import Relation.Binary using (Rel; IsEquivalence; Setoid)
 
 -- be explicit in imports to 'see' where the information comes from
 open import Categories.Adjoint using (Adjoint; _⊣_)
 open import Categories.Category.Core using (Category)
 open import Categories.Category.Product using (Product; _⁂_)
-open import Categories.Category.Instance.Setoids
-open import Categories.Morphism
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Morphism using (Iso)
 open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
 open import Categories.Functor.Bifunctor using (Bifunctor)
 open import Categories.Functor.Hom using (Hom[_][-,-])
@@ -50,11 +49,11 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R :
     Hom-NI′ : NaturalIsomorphism Hom[L-,-] Hom[-,R-]
     Hom-NI′ = record
       { F⇒G = ntHelper record
-        { η       = λ _ → Hom-inverse.to
+        { η       = λ _ → record { to = Hom-inverse.to ; cong = Hom-inverse.to-cong }
         ; commute = λ _ eq → Ladjunct-comm eq
         }
       ; F⇐G = ntHelper record
-        { η       = λ _ → Hom-inverse.from
+        { η       = λ _ → record { to = Hom-inverse.from ; cong = Hom-inverse.from-cong }
         ; commute = λ _ eq → Radjunct-comm eq
         }
       ; iso = λ _ → record
@@ -78,10 +77,10 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R :
     open NaturalIsomorphism Hni
     open NaturalTransformation
     open Functor
-    open Π
+    open Func
 
     private
-      unitη : ∀ X → F₀ Hom[L-,-] (X , L.F₀ X) ⟶ F₀ Hom[-,R-] (X , L.F₀ X)
+      unitη : ∀ X → Func (F₀ Hom[L-,-] (X , L.F₀ X)) (F₀ Hom[-,R-] (X , L.F₀ X))
       unitη X = ⇒.η (X , L.F₀ X)
 
       unit : NaturalTransformation idF (R ∘F L)
@@ -100,7 +99,7 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ e} {L : Functor C D} {R :
               open HomReasoning
               open MR C
 
-      counitη : ∀ X → F₀ Hom[-,R-] (R.F₀ X , X) ⟶ F₀ Hom[L-,-] (R.F₀ X , X)
+      counitη : ∀ X → Func (F₀ Hom[-,R-] (R.F₀ X , X)) (F₀ Hom[L-,-] (R.F₀ X , X))
       counitη X = ⇐.η (R.F₀ X , X)
 
       counit : NaturalTransformation (L ∘F R) idF
@@ -160,7 +159,7 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D
     module L = Functor L
     module R = Functor R
     open Functor
-    open Π
+    open Func
 
     Hom[L-,-] : Bifunctor C.op D (Setoids _ _)
     Hom[L-,-] = LiftSetoids ℓ e ∘F Hom[ D ][-,-] ∘F (L.op ⁂ idF)
@@ -171,7 +170,7 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D
   module _ (Hni : Hom[L-,-] ≃ Hom[-,R-]) where
     open NaturalIsomorphism Hni using (module ⇒; module ⇐; iso)
     private
-      unitη : ∀ X → F₀ Hom[L-,-] (X , L.F₀ X) ⟶ F₀ Hom[-,R-] (X , L.F₀ X)
+      unitη : ∀ X → Func (F₀ Hom[L-,-] (X , L.F₀ X)) (F₀ Hom[-,R-] (X , L.F₀ X))
       unitη X = ⇒.η (X , L.F₀ X)
 
       unit : NaturalTransformation idF (R ∘F L)
@@ -196,7 +195,7 @@ module _ {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {L : Functor C D
               open HomReasoning
               open MR C
 
-      counitη : ∀ X → F₀ Hom[-,R-] (R.F₀ X , X) ⟶ F₀ Hom[L-,-] (R.F₀ X , X)
+      counitη : ∀ X → Func (F₀ Hom[-,R-] (R.F₀ X , X)) (F₀ Hom[L-,-] (R.F₀ X , X))
       counitη X = ⇐.η (R.F₀ X , X)
 
       counit : NaturalTransformation (L ∘F R) idF

src/Categories/Adjoint/Instance/0-Truncation.agda

@@ -7,9 +7,10 @@ module Categories.Adjoint.Instance.0-Truncation where
 
 open import Level using (Lift)
 open import Data.Unit using (⊤)
-import Function
+open import Function.Base renaming (id to id→)
+open import Function.Bundles using (Func)
+import Function.Construct.Identity as Id
 open import Relation.Binary using (Setoid)
-open import Function.Equality using (Π) renaming (id to idΠ)
 
 open import Categories.Adjoint using (_⊣_)
 open import Categories.Category.Construction.0-Groupoid using (0-Groupoid)
@@ -26,7 +27,7 @@ open import Categories.NaturalTransformation.NaturalIsomorphism using (refl)
 Inclusion : ∀ {c ℓ} e → Functor (Setoids c ℓ) (Groupoids c ℓ e)
 Inclusion {c} {ℓ} e = record
   { F₀           = 0-Groupoid e
-  ; F₁           = λ f → record { F₀ = f ⟨$⟩_ ; F₁ = cong f }
+  ; F₁           = λ f → record { F₀ = to f; F₁ = cong f }
   ; identity     = refl
   ; homomorphism = refl
   ; F-resp-≈     = λ {S T f g} f≗g →
@@ -37,27 +38,27 @@ Inclusion {c} {ℓ} e = record
     ; F⇐G = record { η = λ _ → T.sym (f≗g S.refl) }
     }
   }
-  where open Π
+  where open Func
 
 -- Trunc is left-adjoint to the inclusion functor from Setoids to Groupoids
 
 TruncAdj : ∀ {o ℓ e} → Trunc ⊣ Inclusion {o} {ℓ} e
 TruncAdj {o} {ℓ} {e} = record
   { unit   = unit
   ; counit = counit
-  ; zig    = Function.id
+  ; zig    = id→
   ; zag    = refl
   }
   where
-    open Π
+    open Func
     open Groupoid using (category)
 
     unit : NaturalTransformation idF (Inclusion e ∘F Trunc)
     unit = record
-      { η           = λ _ → record { F₀ = Function.id ; F₁ = Function.id }
+      { η           = λ _ → record { F₀ = id→ ; F₁ = id→ }
       ; commute     = λ _ → refl
       ; sym-commute = λ _ → refl
       }
 
     counit : NaturalTransformation (Trunc ∘F Inclusion e) idF
-    counit = ntHelper record { η = λ S → idΠ ; commute = λ f → cong f }
+    counit = ntHelper record { η = Id.function; commute = λ f → cong f }

src/Categories/Adjoint/Instance/PosetCore.agda

@@ -7,16 +7,16 @@ module Categories.Adjoint.Instance.PosetCore where
 
 open import Level using (_⊔_)
 import Function
-open import Function.Equality using (Π; _⟶_)
+open import Function.Bundles using (Func)
 open import Relation.Binary using (Setoid; Poset)
 open import Relation.Binary.Morphism.Bundles using (PosetHomomorphism; mkPosetHomo)
 import Relation.Binary.Morphism.Construct.Composition as Comp
 
 open import Categories.Adjoint using (_⊣_)
 import Categories.Adjoint.Instance.0-Truncation as Setd
 import Categories.Adjoint.Instance.01-Truncation as Pos
-open import Categories.Category using (Category)
-open import Categories.Category.Construction.Thin
+open import Categories.Category.Core using (Category)
+open import Categories.Category.Construction.Thin using (Thin; module EqIsIso)
 open import Categories.Category.Instance.Posets using (Posets)
 open import Categories.Category.Instance.Setoids using (Setoids)
 open import Categories.Functor.Instance.Core using () renaming (Core to CatCore)
@@ -28,15 +28,16 @@ open import Categories.NaturalTransformation using (ntHelper)
 open import Categories.NaturalTransformation.NaturalIsomorphism
   using (_≃_; niHelper)
 
-open Π
 open PosetHomomorphism using (⟦_⟧; cong)
 
 -- The "forgetful" functor from Setoids to Posets (forgetting symmetry).
 
+open Func
+
 Forgetful : ∀ {c ℓ} → Functor (Setoids c ℓ) (Posets c ℓ ℓ)
 Forgetful = record
   { F₀           = Forgetful₀
-  ; F₁           = λ f → mkPosetHomo _ _ (f ⟨$⟩_) (cong f)
+  ; F₁           = λ f → mkPosetHomo _ _ (to f) (cong f)
   ; identity     = λ {S}       → refl S
   ; homomorphism = λ {_ _ S}   → refl S
   ; F-resp-≈     = λ {S _} f≗g → f≗g (refl S)
@@ -70,7 +71,7 @@ Forgetful = record
 Core : ∀ {c ℓ₁ ℓ₂} → Functor (Posets c ℓ₁ ℓ₂) (Setoids c ℓ₁)
 Core = record
   { F₀           = λ A → record { isEquivalence = isEquivalence A }
-  ; F₁           = λ f → record { _⟨$⟩_ = ⟦ f ⟧ ; cong = cong f }
+  ; F₁           = λ f → record { to = ⟦ f ⟧ ; cong = cong f }
   ; identity     = Function.id
   ; homomorphism = λ {_ _ _ f g} → cong (Comp.posetHomomorphism f g)
   ; F-resp-≈     = λ {_ B} {f _} f≗g x≈y → Eq.trans B (cong f x≈y) f≗g
@@ -91,8 +92,8 @@ CoreAdj = record
     open Functor Core      using () renaming (F₀ to Core₀; F₁ to Core₁)
     open Functor Forgetful using () renaming (F₀ to U₀   ; F₁ to U₁)
 
-    unit : ∀ S → S ⟶ Core₀ (U₀ S)
-    unit S = record { _⟨$⟩_ = Function.id ; cong = Function.id }
+    unit : ∀ S → Func S (Core₀ (U₀ S))
+    unit S = record { to = Function.id ; cong = Function.id }
 
     counit : ∀ A → PosetHomomorphism (U₀ (Core₀ A)) A
     counit A = mkPosetHomo (U₀ (Core₀ A)) A Function.id (reflexive A)

src/Categories/Adjoint/Mate.agda

@@ -6,7 +6,9 @@ module Categories.Adjoint.Mate where
 
 open import Level
 open import Data.Product using (Σ; _,_)
-open import Function.Equality using (Π; _⟶_; _⇨_) renaming (_∘_ to _∙_)
+open import Function.Bundles using (Func; _⟨$⟩_)
+open import Function.Construct.Composition using (function)
+open import Function.Construct.Setoid using () renaming (function to _⇨_)
 open import Relation.Binary using (Setoid; IsEquivalence)
 
 open import Categories.Category
@@ -107,14 +109,32 @@ module _ {L L′ : Functor C D} {R R′ : Functor D C}
 
   -- there are two squares to show
   module _ {X : C.Obj} {Y : D.Obj} where
-    open Setoid (L′⊣R′.Hom[L-,-].F₀ (X , Y) ⇨ L⊣R.Hom[-,R-].F₀ (X , Y))
+    private
+      From : Setoid _ _
+      From = L′⊣R′.Hom[L-,-].F₀ (X , Y)
+      To : Setoid _ _
+      To = L⊣R.Hom[-,R-].F₀ (X , Y)
+      SS = From ⇨ To
+    open Setoid SS using (_≈_)
     open C hiding (_≈_)
     open MR C
     open C.HomReasoning
     module DH = D.HomReasoning
-
-    mate-commute₁ : F₁ Hom[ C ][-,-] (C.id , β.η Y) ∙ L′⊣R′.Hom-inverse.to {X} {Y}
-                  ≈ L⊣R.Hom-inverse.to {X} {Y} ∙ F₁ Hom[ D ][-,-] (α.η X , D.id)
+    private
+      -- annoyingly the new bundles don't export this
+      D⟶C : Func (D.hom-setoid {F₀ L′ X} {Y}) (C.hom-setoid {X} {F₀ R′ Y})
+      D⟶C = record
+        { to = L′⊣R′.Hom-inverse.to {X} {Y}
+        ; cong = L′⊣R′.Hom-inverse.to-cong
+        }
+      D⟶C′ : Func D.hom-setoid C.hom-setoid
+      D⟶C′ = record
+        { to = L⊣R.Hom-inverse.to {X} {Y}
+        ; cong = L⊣R.Hom-inverse.to-cong
+        }
+
+    mate-commute₁ : function D⟶C (F₁ Hom[ C ][-,-] (C.id , β.η Y))
+                  ≈ function (F₁ Hom[ D ][-,-] (α.η X , D.id)) D⟶C′
     mate-commute₁ {f} {g} f≈g = begin
       β.η Y ∘ (F₁ R′ f ∘ L′⊣R′.unit.η X) ∘ C.id  ≈⟨ refl⟩∘⟨ identityʳ ⟩
       β.η Y ∘ F₁ R′ f ∘ L′⊣R′.unit.η X           ≈⟨ pullˡ (β.commute f) ⟩
@@ -124,14 +144,35 @@ module _ {L L′ : Functor C D} {R R′ : Functor D C}
       F₁ R (D.id D.∘ g D.∘ α.η X) ∘ L⊣R.unit.η X ∎
 
   module _ {X : C.Obj} {Y : D.Obj} where
-    open Setoid (L′⊣R′.Hom[-,R-].F₀ (X , Y) ⇨ L⊣R.Hom[L-,-].F₀ (X , Y))
     open D hiding (_≈_)
     open MR D
     open D.HomReasoning
     module CH = C.HomReasoning
-
-    mate-commute₂ : F₁ Hom[ D ][-,-] (α.η X , D.id) ∙ L′⊣R′.Hom-inverse.from {X} {Y}
-                  ≈ L⊣R.Hom-inverse.from {X} {Y} ∙ F₁ Hom[ C ][-,-] (C.id , β.η Y)
+    private
+      From : Setoid _ _
+      From = L′⊣R′.Hom[-,R-].F₀ (X , Y)
+      To : Setoid _ _
+      To = L⊣R.Hom[L-,-].F₀ (X , Y)
+      module From = Setoid From
+      module To = Setoid To
+      SS : Setoid _ _
+      SS = From ⇨ To
+    open Setoid SS using (_≈_)
+    private
+      -- annoyingly the new bundles don't export this
+      C⟶D : Func C.hom-setoid D.hom-setoid
+      C⟶D = record
+        { to = L′⊣R′.Hom-inverse.from {X} {Y}
+        ; cong = L′⊣R′.Hom-inverse.from-cong
+        }
+      C⟶D′ : Func C.hom-setoid D.hom-setoid
+      C⟶D′ = record
+        { to = L⊣R.Hom-inverse.from {X} {Y}
+        ; cong = L⊣R.Hom-inverse.from-cong
+        }
+
+    mate-commute₂ : function C⟶D (F₁ Hom[ D ][-,-] (α.η X , D.id))
+                  ≈ function (F₁ Hom[ C ][-,-] (C.id , β.η Y)) C⟶D′
     mate-commute₂ {f} {g} f≈g = begin
       D.id ∘ (L′⊣R′.counit.η Y ∘ F₁ L′ f) ∘ α.η X  ≈⟨ identityˡ ⟩
       (L′⊣R′.counit.η Y ∘ F₁ L′ f) ∘ α.η X         ≈˘⟨ pushʳ (α.commute f) ⟩