Merge pull request #288 from Akshobhya1234/master

JacquesCarette · web-flow · commit 3102666ade15 · 2021-06-27T07:34:43.000-04:00
Version compatible to stdlib 1.7 and agda 2.6.2
diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
@@ -45,8 +45,8 @@ on:
 ########################################################################
 
 env:
-  AGDA_COMMIT: 8eb0d01811a663cf2b27b482b3b18690adfa094b
-  STDLIB_VERSION: 1.6
+  AGDA_COMMIT: tags/v2.6.2
+  STDLIB_VERSION: 1.7
 
   GHC_VERSION: 8.6.5
   CABAL_VERSION: 3.2.0.0
diff --git a/agda-categories.agda-lib b/agda-categories.agda-lib
@@ -1,3 +1,3 @@
 name: agda-categories
-depend: standard-library-1.6
+depend: standard-library-1.7
 include: src/
diff --git a/src/Categories/NaturalTransformation/NaturalIsomorphism/Monoidal/Braided.agda b/src/Categories/NaturalTransformation/NaturalIsomorphism/Monoidal/Braided.agda
@@ -83,7 +83,6 @@ module Lax where
         }
       ; trans = λ α β → β ⓘᵥ α
       }
-      where
 
   open BraidedMonoidalNaturalIsomorphism
 
@@ -238,7 +237,6 @@ module Strong where
         }
       ; trans = λ α β → β ⓘᵥ α
       }
-      where
 
   open BraidedMonoidalNaturalIsomorphism
 
diff --git a/src/Categories/NaturalTransformation/NaturalIsomorphism/Monoidal/Symmetric.agda b/src/Categories/NaturalTransformation/NaturalIsomorphism/Monoidal/Symmetric.agda
@@ -84,7 +84,6 @@ module Lax where
         }
       ; trans = λ α β → β ⓘᵥ α
       }
-      where
 
   open SymmetricMonoidalNaturalIsomorphism
 
@@ -240,7 +239,6 @@ module Strong where
         }
       ; trans = λ α β → β ⓘᵥ α
       }
-      where
 
   open SymmetricMonoidalNaturalIsomorphism
 

Original file line number	Diff line number	Diff line change
`@@ -83,7 +83,6 @@ module Lax where`
`83`	`83`	`}`
`84`	`84`	`; trans = λ α β → β ⓘᵥ α`
`85`	`85`	`}`
`86`		`- where`
`87`	`86`
`88`	`87`	`open BraidedMonoidalNaturalIsomorphism`
`89`	`88`
`@@ -238,7 +237,6 @@ module Strong where`
`238`	`237`	`}`
`239`	`238`	`; trans = λ α β → β ⓘᵥ α`
`240`	`239`	`}`
`241`		`- where`
`242`	`240`
`243`	`241`	`open BraidedMonoidalNaturalIsomorphism`
`244`	`242`
Original file line number	Diff line number	Diff line change
`@@ -84,7 +84,6 @@ module Lax where`
`84`	`84`	`}`
`85`	`85`	`; trans = λ α β → β ⓘᵥ α`
`86`	`86`	`}`
`87`		`- where`
`88`	`87`
`89`	`88`	`open SymmetricMonoidalNaturalIsomorphism`
`90`	`89`
`@@ -240,7 +239,6 @@ module Strong where`
`240`	`239`	`}`
`241`	`240`	`; trans = λ α β → β ⓘᵥ α`
`242`	`241`	`}`
`243`		`- where`
`244`	`242`
`245`	`243`	`open SymmetricMonoidalNaturalIsomorphism`
`246`	`244`