Skip to content

Commit 7ea9852

Browse files
jmougeotJacquesCarettejamesmckinna
authored
[Import] Relation.Unary (#2651)
* [Import] `Relation.Unary` * Update src/Relation/Unary/Consequences.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * Update src/Relation/Unary/Indexed.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * Update src/Relation/Unary/Properties.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * Update src/Relation/Unary/Algebra.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> * Update src/Relation/Unary/Closure/Base.agda Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> --------- Co-authored-by: Jacques Carette <carette@mcmaster.ca> Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>
1 parent 7a5660f commit 7ea9852

File tree

12 files changed

+35
-20
lines changed

12 files changed

+35
-20
lines changed

‎src/Relation/Nary.agda‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ module Relation.Nary where
1414
-- behind the design decisions.
1515
------------------------------------------------------------------------
1616

17-
open import Level using (Level; _⊔_; Lift)
1817
open import Data.Unit.Base using (⊤)
1918
open import Data.Bool.Base using (true; false)
2019
open import Data.Empty using (⊥; ⊥-elim)
@@ -24,12 +23,13 @@ open import Data.Product.Nary.NonDependent
2423
open import Data.Sum.Base using (_⊎_)
2524
open import Function.Base using (_$_; _∘′_)
2625
open import Function.Nary.NonDependent
27-
open import Relation.Nullary.Negation using (¬_)
26+
open import Level using (Level; _⊔_; Lift)
27+
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)
28+
open import Relation.Nullary.Negation.Core using (¬_)
2829
open import Relation.Nullary.Decidable.Core as Dec
2930
using (Dec; yes; no; _because_; _×-dec_)
3031
import Relation.Unary as Unary
3132
using (Pred; Satisfiable; Universal; IUniversal)
32-
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)
3333

3434
private
3535
variable

‎src/Relation/Unary/Algebra.agda‎

Lines changed: 11 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,16 +9,25 @@
99
module Relation.Unary.Algebra where
1010

1111
open import Algebra.Bundles
12+
using (Magma; Semigroup; Band
13+
; Monoid; CommutativeMonoid; IdempotentCommutativeMonoid
14+
; SemiringWithoutAnnihilatingZero; Semiring; CommutativeSemiring)
1215
import Algebra.Definitions as AlgebraicDefinitions
1316
open import Algebra.Lattice.Bundles
17+
using (Semilattice; Lattice; DistributiveLattice)
1418
import Algebra.Lattice.Structures as AlgebraicLatticeStructures
19+
using (IsLattice; IsDistributiveLattice; IsSemilattice)
1520
import Algebra.Structures as AlgebraicStructures
21+
using (IsMagma; IsSemigroup; IsBand; IsMonoid; IsCommutativeMonoid
22+
; IsIdempotentCommutativeMonoid; IsSemiringWithoutAnnihilatingZero
23+
; IsSemiring; IsCommutativeSemiring)
1624
open import Data.Empty.Polymorphic using (⊥-elim)
17-
open import Data.Product.Base as Product using (_,_; proj₁; proj₂; <_,_>; curry; uncurry)
25+
open import Data.Product.Base as Product
26+
using (_,_; proj₁; proj₂; <_,_>; curry; uncurry)
1827
open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
1928
open import Data.Unit.Polymorphic using (tt)
2029
open import Function.Base using (id; const; _∘_)
21-
open import Level
30+
open import Level using (Level; _⊔_)
2231
open import Relation.Unary hiding (∅; U)
2332
open import Relation.Unary.Polymorphic using (∅; U)
2433
open import Relation.Unary.Relation.Binary.Equality using (≐-isEquivalence)

‎src/Relation/Unary/Closure/Base.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,13 @@
77
{-# OPTIONS --cubical-compatible --safe #-}
88

99
open import Relation.Binary.Core using (Rel)
10-
open import Relation.Binary.Definitions using (Transitive; Reflexive)
1110

1211
module Relation.Unary.Closure.Base {a b} {A : Set a} (R : Rel A b) where
1312

14-
open import Level
13+
open import Level using (_⊔_)
1514
open import Data.Product.Base using (Σ-syntax; _×_; _,_; -,_)
1615
open import Function.Base using (flip)
16+
open import Relation.Binary.Definitions using (Reflexive; Transitive)
1717
open import Relation.Unary using (Pred)
1818

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

‎src/Relation/Unary/Closure/Preorder.agda‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,9 +10,10 @@ open import Relation.Binary.Bundles using (Preorder)
1010

1111
module Relation.Unary.Closure.Preorder {a r e} (P : Preorder a e r) where
1212

13-
open Preorder P
1413
open import Relation.Unary using (Pred)
1514

15+
open Preorder P
16+
1617
-- Specialising the results proven generically in `Base`.
1718
import Relation.Unary.Closure.Base _∼_ as Base
1819
open Base public

‎src/Relation/Unary/Closure/StrictPartialOrder.agda‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,10 @@ open import Relation.Binary.Bundles using (StrictPartialOrder)
1111
module Relation.Unary.Closure.StrictPartialOrder
1212
{a r e} (P : StrictPartialOrder a e r) where
1313

14-
open StrictPartialOrder P renaming (_<_ to _∼_)
1514
open import Relation.Unary using (Pred)
1615

16+
open StrictPartialOrder P renaming (_<_ to _∼_)
17+
1718
-- Specialising the results proven generically in `Base`.
1819
import Relation.Unary.Closure.Base _∼_ as Base
1920
open Base public

‎src/Relation/Unary/Consequences.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@
88

99
module Relation.Unary.Consequences where
1010

11-
open import Relation.Unary
12-
open import Relation.Nullary using (recompute)
11+
open import Relation.Unary using (Pred; Recomputable; Decidable)
12+
open import Relation.Nullary.Decidable.Core using (recompute)
1313

1414
dec⇒recomputable : {a ℓ : _} {A : Set a} {P : Pred A ℓ} → Decidable P → Recomputable P
1515
dec⇒recomputable P-dec = recompute (P-dec _)

‎src/Relation/Unary/Indexed.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@
99
module Relation.Unary.Indexed where
1010

1111
open import Data.Product.Base using (∃; _×_)
12-
open import Level
13-
open import Relation.Nullary.Negation using (¬_)
12+
open import Level using (Level)
13+
open import Relation.Nullary.Negation.Core using (¬_)
1414

1515
IPred : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _
1616
IPred A ℓ = ∀ {i} → A i → Set ℓ

‎src/Relation/Unary/Polymorphic/Properties.agda‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,12 +9,12 @@
99

1010
module Relation.Unary.Polymorphic.Properties where
1111

12+
open import Data.Unit.Polymorphic.Base using (tt)
1213
open import Level using (Level)
1314
open import Relation.Binary.Definitions hiding (Decidable; Universal; Empty)
14-
open import Relation.Nullary.Decidable using (yes; no)
15+
open import Relation.Nullary.Decidable.Core using (yes; no)
1516
open import Relation.Unary hiding (∅; U)
16-
open import Relation.Unary.Polymorphic
17-
open import Data.Unit.Polymorphic.Base using (tt)
17+
open import Relation.Unary.Polymorphic using (∅; U)
1818

1919
private
2020
variable

‎src/Relation/Unary/PredicateTransformer.agda‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ module Relation.Unary.PredicateTransformer where
1111
open import Data.Product.Base using (∃)
1212
open import Function.Base using (_∘_)
1313
open import Level hiding (_⊔_)
14-
open import Relation.Nullary
1514
open import Relation.Unary
1615
open import Relation.Binary.Core using (REL)
1716

‎src/Relation/Unary/Properties.agda‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,8 @@ open import Relation.Binary.Definitions
1717
hiding (Decidable; Universal; Irrelevant; Empty)
1818
open import Relation.Binary.PropositionalEquality.Core using (refl; _≗_)
1919
open import Relation.Unary
20-
open import Relation.Nullary.Decidable as Dec using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does)
20+
open import Relation.Nullary.Decidable as Dec
21+
using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does)
2122
open import Function.Base using (id; _$_; _∘_)
2223

2324
private

0 commit comments

Comments
 (0)