Skip to content

Commit 8dcb5b6

Browse files
jamesmckinnajamesmckinna
authored
Merge branch 'agda:master' into refactor-heyting
2 parents fb2da3e + 4925719 commit 8dcb5b6

37 files changed

+141
-124
lines changed

‎src/Algebra/Construct/Add/Identity.agda

+8-6
Original file line numberDiff line numberDiff line change
@@ -9,17 +9,18 @@
99

1010
module Algebra.Construct.Add.Identity where
1111

12-
open import Algebra.Bundles
12+
open import Algebra.Bundles using (Semigroup; Monoid)
1313
open import Algebra.Core using (Op₂)
1414
open import Algebra.Definitions
15-
open import Algebra.Structures
15+
using (Congruent₂; Associative; LeftIdentity; RightIdentity; Identity)
16+
open import Algebra.Structures using (IsMagma; IsSemigroup; IsMonoid)
1617
open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈)
1718
open import Data.Product.Base using (_,_)
1819
open import Level using (Level; _⊔_)
19-
open import Relation.Binary.Core
20-
open import Relation.Binary.Definitions
21-
open import Relation.Binary.Structures
22-
open import Relation.Nullary.Construct.Add.Point
20+
open import Relation.Binary.Core using (Rel)
21+
open import Relation.Binary.Definitions using (Reflexive)
22+
open import Relation.Binary.Structures using (IsEquivalence)
23+
open import Relation.Nullary.Construct.Add.Point using (Pointed; [_]; ∙)
2324

2425
private
2526
variable
@@ -101,3 +102,4 @@ monoid : Semigroup a (a ⊔ ℓ) → Monoid a (a ⊔ ℓ)
101102
monoid S = record
102103
{ isMonoid = isMonoid S.isSemigroup
103104
} where module S = Semigroup S
105+

‎src/Algebra/Construct/Initial.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ open import Algebra.Bundles.Raw
2121
open import Algebra.Core using (Op₂)
2222
open import Algebra.Definitions using (Congruent₂)
2323
open import Algebra.Structures using (IsMagma; IsSemigroup; IsBand)
24-
open import Data.Empty.Polymorphic
24+
open import Data.Empty.Polymorphic using (⊥)
2525
open import Relation.Binary.Core using (Rel)
2626
open import Relation.Binary.Structures using (IsEquivalence)
2727
open import Relation.Binary.Definitions

‎src/Algebra/Construct/LiftedChoice.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ open import Algebra
1010

1111
module Algebra.Construct.LiftedChoice where
1212

13-
open import Algebra.Consequences.Base
13+
open import Algebra.Consequences.Base using (sel⇒idem)
1414
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
1515
open import Data.Product.Base using (_×_; _,_)
1616
open import Function.Base using (const; _$_)

‎src/Algebra/Construct/NaturalChoice/Base.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77

88
{-# OPTIONS --cubical-compatible --safe #-}
99

10-
open import Algebra.Core
10+
open import Algebra.Core using (Op₂)
1111
open import Level as L hiding (_⊔_)
1212
open import Function.Base using (flip)
1313
open import Relation.Binary.Bundles using (TotalPreorder)

‎src/Algebra/Construct/NaturalChoice/Max.agda

+2-3
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,8 @@ open import Relation.Binary.Bundles using (TotalOrder)
1111
module Algebra.Construct.NaturalChoice.Max
1212
{a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂) where
1313

14-
open import Algebra.Core
15-
open import Algebra.Definitions
16-
open import Algebra.Construct.NaturalChoice.Base
14+
open import Algebra.Core using (Op₂)
15+
open import Algebra.Construct.NaturalChoice.Base using (MaxOperator)
1716
open import Relation.Binary.Construct.Flip.EqAndOrd using ()
1817
renaming (totalOrder to flip)
1918

‎src/Algebra/Construct/NaturalChoice/MaxOp.agda

+8-8
Original file line numberDiff line numberDiff line change
@@ -7,21 +7,21 @@
77

88
{-# OPTIONS --cubical-compatible --safe #-}
99

10-
open import Algebra.Core
11-
open import Algebra.Construct.NaturalChoice.Base
12-
import Algebra.Construct.NaturalChoice.MinOp as MinOp
13-
open import Function.Base using (flip)
14-
open import Relation.Binary.Core using (_Preserves_⟶_)
10+
open import Algebra.Construct.NaturalChoice.Base using (MaxOperator; MaxOp⇒MinOp)
1511
open import Relation.Binary.Bundles using (TotalPreorder)
16-
open import Relation.Binary.Construct.Flip.EqAndOrd using ()
17-
renaming (totalPreorder to flipOrder)
1812

1913
module Algebra.Construct.NaturalChoice.MaxOp
2014
{a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (maxOp : MaxOperator O)
2115
where
2216

23-
open TotalPreorder O renaming (Carrier to A; _≲_ to _≤_)
17+
import Algebra.Construct.NaturalChoice.MinOp as MinOp
18+
open import Algebra.Core using (Op₂)
19+
open import Function.Base using (flip)
2420
open MaxOperator maxOp
21+
open import Relation.Binary.Core using (_Preserves_⟶_)
22+
open import Relation.Binary.Construct.Flip.EqAndOrd using ()
23+
renaming (totalPreorder to flipOrder)
24+
open TotalPreorder O renaming (Carrier to A; _≲_ to _≤_)
2525

2626
-- Max is just min with a flipped order
2727

‎src/Algebra/Construct/NaturalChoice/Min.agda

+6-7
Original file line numberDiff line numberDiff line change
@@ -6,19 +6,18 @@
66

77
{-# OPTIONS --cubical-compatible --safe #-}
88

9-
open import Algebra.Core
10-
open import Algebra.Bundles
11-
open import Algebra.Construct.NaturalChoice.Base
12-
open import Data.Sum.Base using (inj₁; inj₂; [_,_])
13-
open import Data.Product.Base using (_,_)
14-
open import Function.Base using (id)
159
open import Relation.Binary.Bundles using (TotalOrder)
16-
import Algebra.Construct.NaturalChoice.MinOp as MinOp
1710

1811
module Algebra.Construct.NaturalChoice.Min
1912
{a ℓ₁ ℓ₂} (O : TotalOrder a ℓ₁ ℓ₂)
2013
where
2114

15+
open import Algebra.Core using (Op₂)
16+
open import Algebra.Construct.NaturalChoice.Base
17+
import Algebra.Construct.NaturalChoice.MinOp as MinOp
18+
open import Data.Sum.Base using (inj₁; inj₂; [_,_])
19+
open import Data.Product.Base using (_,_)
20+
open import Function.Base using (id)
2221
open TotalOrder O renaming (Carrier to A)
2322

2423
------------------------------------------------------------------------

‎src/Algebra/Construct/NaturalChoice/MinMaxOp.agda

+6-8
Original file line numberDiff line numberDiff line change
@@ -7,22 +7,20 @@
77

88
{-# OPTIONS --cubical-compatible --safe #-}
99

10-
open import Algebra.Core
11-
open import Algebra.Bundles
12-
open import Algebra.Construct.NaturalChoice.Base
13-
open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
14-
open import Data.Product.Base using (_,_)
15-
open import Function.Base using (id; _∘_; flip)
16-
open import Relation.Binary.Core using (_Preserves_⟶_)
10+
open import Algebra.Construct.NaturalChoice.Base using (MinOperator; MaxOperator)
1711
open import Relation.Binary.Bundles using (TotalPreorder)
18-
open import Relation.Binary.Consequences
1912

2013
module Algebra.Construct.NaturalChoice.MinMaxOp
2114
{a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂}
2215
(minOp : MinOperator O)
2316
(maxOp : MaxOperator O)
2417
where
2518

19+
open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
20+
open import Data.Product.Base using (_,_)
21+
open import Function.Base using (id; _∘_; flip)
22+
open import Relation.Binary.Core using (_Preserves_⟶_)
23+
2624
open TotalPreorder O renaming
2725
( Carrier to A
2826
; _≲_ to _≤_

‎src/Algebra/Construct/NaturalChoice/MinOp.agda

+8-7
Original file line numberDiff line numberDiff line change
@@ -7,19 +7,20 @@
77

88
{-# OPTIONS --cubical-compatible --safe #-}
99

10-
open import Algebra.Core
10+
open import Relation.Binary.Bundles using (TotalPreorder)
11+
open import Algebra.Construct.NaturalChoice.Base using (MinOperator; MinOp⇒MaxOp)
12+
13+
module Algebra.Construct.NaturalChoice.MinOp
14+
{a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (minOp : MinOperator O) where
15+
16+
open import Algebra.Core using (Op₂)
1117
open import Algebra.Bundles
12-
open import Algebra.Construct.NaturalChoice.Base
18+
using (RawMagma; Magma; Semigroup; Band; CommutativeSemigroup; SelectiveMagma; Monoid)
1319
open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
1420
open import Data.Product.Base using (_,_)
1521
open import Function.Base using (id; _∘_)
1622
open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
17-
open import Relation.Binary.Bundles using (TotalPreorder)
1823
open import Relation.Binary.Definitions using (Maximum; Minimum)
19-
open import Relation.Binary.Consequences
20-
21-
module Algebra.Construct.NaturalChoice.MinOp
22-
{a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (minOp : MinOperator O) where
2324

2425
open TotalPreorder O renaming
2526
( Carrier to A

‎src/Algebra/Construct/Pointwise.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ open import Algebra.Core using (Op₁; Op₂)
1717
open import Algebra.Structures
1818
open import Data.Product.Base using (_,_)
1919
open import Function.Base using (id; _∘′_; const)
20-
open import Level
20+
open import Level using (Level; _⊔_)
2121
open import Relation.Binary.Core using (Rel)
2222
open import Relation.Binary.Bundles using (Setoid)
2323
open import Relation.Binary.Structures using (IsEquivalence)

‎src/Algebra/Construct/Subst/Equality.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010
{-# OPTIONS --cubical-compatible --safe #-}
1111

1212
open import Data.Product.Base as Product
13-
open import Relation.Binary.Core
13+
open import Relation.Binary.Core using (Rel; _⇔_)
1414

1515
module Algebra.Construct.Subst.Equality
1616
{a ℓ₁ ℓ₂} {A : Set a} {≈₁ : Rel A ℓ₁} {≈₂ : Rel A ℓ₂}
@@ -20,7 +20,7 @@ module Algebra.Construct.Subst.Equality
2020
open import Algebra.Definitions
2121
open import Algebra.Structures
2222
import Data.Sum.Base as Sum
23-
open import Function.Base
23+
open import Function.Base using (id; _∘_)
2424
open import Relation.Binary.Construct.Subst.Equality equiv
2525

2626
------------------------------------------------------------------------

‎src/Algebra/Construct/Terminal.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ open import Level using (Level)
1515
module Algebra.Construct.Terminal {c ℓ : Level} where
1616

1717
open import Algebra.Bundles
18-
open import Data.Unit.Polymorphic
18+
open import Data.Unit.Polymorphic using (⊤)
1919
open import Relation.Binary.Core using (Rel)
2020

2121
------------------------------------------------------------------------

‎src/Algebra/Construct/Zero.agda

+2-4
Original file line numberDiff line numberDiff line change
@@ -19,10 +19,8 @@ open import Level using (Level)
1919

2020
module Algebra.Construct.Zero {c ℓ : Level} where
2121

22-
open import Algebra.Bundles.Raw
23-
using (RawMagma)
24-
open import Algebra.Bundles
25-
using (Magma; Semigroup; Band)
22+
open import Algebra.Bundles.Raw using (RawMagma)
23+
open import Algebra.Bundles using (Magma; Semigroup; Band)
2624

2725
------------------------------------------------------------------------
2826
-- Re-export those algebras which are both initial and terminal

‎src/Algebra/Definitions/RawMonoid.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -7,11 +7,11 @@
77
{-# OPTIONS --cubical-compatible --safe #-}
88

99
open import Algebra.Bundles using (RawMonoid)
10-
open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
11-
open import Data.Vec.Functional as Vector using (Vector)
1210

1311
module Algebra.Definitions.RawMonoid {a ℓ} (M : RawMonoid a ℓ) where
1412

13+
open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
14+
open import Data.Vec.Functional as Vector using (Vector)
1515
open RawMonoid M renaming ( _∙_ to _+_ ; ε to 0# )
1616

1717
------------------------------------------------------------------------

‎src/Algebra/Definitions/RawSemiring.agda

+3-3
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,13 @@
77
{-# OPTIONS --cubical-compatible --safe #-}
88

99
open import Algebra.Bundles using (RawSemiring)
10+
11+
module Algebra.Definitions.RawSemiring {a ℓ} (M : RawSemiring a ℓ) where
12+
1013
open import Data.Sum.Base using (_⊎_)
1114
open import Data.Nat.Base using (ℕ; zero; suc)
1215
open import Level using (_⊔_)
1316
open import Relation.Binary.Core using (Rel)
14-
15-
module Algebra.Definitions.RawSemiring {a ℓ} (M : RawSemiring a ℓ) where
16-
1717
open RawSemiring M renaming (Carrier to A)
1818

1919
------------------------------------------------------------------------

‎src/Algebra/Lattice/Bundles/Raw.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88

99
module Algebra.Lattice.Bundles.Raw where
1010

11-
open import Algebra.Core
11+
open import Algebra.Core using (Op₂)
1212
open import Algebra.Bundles.Raw using (RawMagma)
1313
open import Level using (suc; _⊔_)
1414
open import Relation.Binary.Core using (Rel)

‎src/Algebra/Lattice/Construct/NaturalChoice/MaxOp.agda

+3-1
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,15 @@
88
{-# OPTIONS --cubical-compatible --safe #-}
99

1010
open import Algebra.Construct.NaturalChoice.Base
11-
import Algebra.Lattice.Construct.NaturalChoice.MinOp as MinOp
11+
using (MaxOperator; MaxOp⇒MinOp)
1212
open import Relation.Binary.Bundles using (TotalPreorder)
1313

1414
module Algebra.Lattice.Construct.NaturalChoice.MaxOp
1515
{a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (maxOp : MaxOperator O)
1616
where
1717

18+
import Algebra.Lattice.Construct.NaturalChoice.MinOp as MinOp
19+
1820
private
1921
module Min = MinOp (MaxOp⇒MinOp maxOp)
2022

‎src/Algebra/Lattice/Construct/NaturalChoice/MinMaxOp.agda

+2-2
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,7 @@
66

77
{-# OPTIONS --cubical-compatible --safe #-}
88

9-
open import Algebra.Lattice.Bundles
10-
open import Algebra.Construct.NaturalChoice.Base
9+
open import Algebra.Construct.NaturalChoice.Base using (MinOperator; MaxOperator)
1110
open import Relation.Binary.Bundles using (TotalPreorder)
1211

1312
module Algebra.Lattice.Construct.NaturalChoice.MinMaxOp
@@ -22,6 +21,7 @@ open MaxOperator maxOp
2221

2322
open import Algebra.Lattice.Structures _≈_
2423
open import Algebra.Construct.NaturalChoice.MinMaxOp minOp maxOp
24+
open import Algebra.Lattice.Bundles using (Lattice; DistributiveLattice)
2525
open import Relation.Binary.Reasoning.Preorder preorder
2626

2727
------------------------------------------------------------------------

‎src/Algebra/Lattice/Construct/NaturalChoice/MinOp.agda

+3-4
Original file line numberDiff line numberDiff line change
@@ -7,9 +7,7 @@
77

88
{-# OPTIONS --cubical-compatible --safe #-}
99

10-
open import Algebra.Bundles
11-
open import Algebra.Lattice.Bundles
12-
open import Algebra.Construct.NaturalChoice.Base
10+
open import Algebra.Construct.NaturalChoice.Base using (MinOperator)
1311
open import Relation.Binary.Bundles using (TotalPreorder)
1412

1513
module Algebra.Lattice.Construct.NaturalChoice.MinOp
@@ -18,8 +16,9 @@ module Algebra.Lattice.Construct.NaturalChoice.MinOp
1816
open TotalPreorder O
1917
open MinOperator minOp
2018

21-
open import Algebra.Lattice.Structures _≈_
2219
open import Algebra.Construct.NaturalChoice.MinOp minOp
20+
open import Algebra.Lattice.Bundles using (Semilattice)
21+
open import Algebra.Lattice.Structures _≈_
2322

2423
------------------------------------------------------------------------
2524
-- Structures

‎src/Algebra/Lattice/Morphism/Construct/Composition.agda

+3-1
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,14 @@
88

99
module Algebra.Lattice.Morphism.Construct.Composition where
1010

11-
open import Algebra.Lattice.Bundles
11+
open import Algebra.Lattice.Bundles using (RawLattice)
1212
open import Algebra.Lattice.Morphism.Structures
13+
using (IsLatticeHomomorphism; IsLatticeIsomorphism; IsLatticeMonomorphism)
1314
open import Function.Base using (_∘_)
1415
import Function.Construct.Composition as Func
1516
open import Level using (Level)
1617
open import Relation.Binary.Morphism.Construct.Composition
18+
using (isRelHomomorphism)
1719
open import Relation.Binary.Definitions using (Transitive)
1820

1921
private

‎src/Algebra/Lattice/Morphism/Construct/Identity.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88

99
module Algebra.Lattice.Morphism.Construct.Identity where
1010

11-
open import Algebra.Lattice.Bundles
11+
open import Algebra.Lattice.Bundles using (RawLattice)
1212
open import Algebra.Lattice.Morphism.Structures
1313
using ( module LatticeMorphisms )
1414
open import Data.Product.Base using (_,_)

‎src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda

+9-8
Original file line numberDiff line numberDiff line change
@@ -9,22 +9,23 @@
99

1010
{-# OPTIONS --cubical-compatible --safe #-}
1111

12-
open import Algebra
1312
open import Algebra.Lattice
14-
open import Algebra.Lattice.Morphism.Structures
15-
import Algebra.Consequences.Setoid as Consequences
13+
using (RawLattice; IsLattice; IsDistributiveLattice; isDistributiveLatticeʳʲᵐ)
14+
open import Algebra.Lattice.Morphism.Structures using (IsLatticeMonomorphism)
15+
16+
module Algebra.Lattice.Morphism.LatticeMonomorphism
17+
{a b ℓ₁ ℓ₂} {L₁ : RawLattice a ℓ₁} {L₂ : RawLattice b ℓ₂} {⟦_⟧}
18+
(isLatticeMonomorphism : IsLatticeMonomorphism L₁ L₂ ⟦_⟧)
19+
where
20+
21+
open import Algebra using (Absorptive; _Absorbs_; _DistributesOverʳ_)
1622
import Algebra.Morphism.MagmaMonomorphism as MagmaMonomorphisms
1723
import Algebra.Lattice.Properties.Lattice as LatticeProperties
1824
open import Data.Product.Base using (_,_; map)
1925
open import Relation.Binary.Bundles using (Setoid)
2026
import Relation.Binary.Morphism.RelMonomorphism as RelMonomorphisms
2127
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
2228

23-
module Algebra.Lattice.Morphism.LatticeMonomorphism
24-
{a b ℓ₁ ℓ₂} {L₁ : RawLattice a ℓ₁} {L₂ : RawLattice b ℓ₂} {⟦_⟧}
25-
(isLatticeMonomorphism : IsLatticeMonomorphism L₁ L₂ ⟦_⟧)
26-
where
27-
2829
open IsLatticeMonomorphism isLatticeMonomorphism
2930
open RawLattice L₁ renaming (_≈_ to _≈₁_; _∨_ to _∨_; _∧_ to _∧_)
3031
open RawLattice L₂ renaming (_≈_ to _≈₂_; _∨_ to _⊔_; _∧_ to _⊓_)

0 commit comments

Comments
 (0)