From f69b6e695930c19c2af23f3e12e02a57b2c7a366 Mon Sep 17 00:00:00 2001 From: depsterr Date: Thu, 23 Jun 2022 22:12:24 +0200 Subject: [PATCH] add some agda stuff --- misc/Agda.Builtin.Bool.html | 17 + misc/Agda.Builtin.Equality.html | 12 + misc/Agda.Builtin.Maybe.html | 12 + misc/Agda.Builtin.Nat.html | 136 +++ misc/Agda.Builtin.Sigma.html | 20 + misc/Agda.Builtin.Strict.html | 12 + misc/Agda.Builtin.Unit.html | 12 + misc/Agda.Primitive.html | 39 + misc/Agda.css | 41 + misc/Algebra.Bundles.html | 934 ++++++++++++++++++ misc/Algebra.Consequences.Base.html | 24 + misc/Algebra.Consequences.Setoid.html | 216 ++++ misc/Algebra.Core.html | 33 + misc/Algebra.Definitions.html | 134 +++ misc/Algebra.Structures.html | 571 +++++++++++ misc/Algebra.html | 17 + misc/Axiom.Extensionality.Propositional.html | 64 ++ misc/Axiom.UniquenessOfIdentityProofs.html | 79 ++ misc/Data.Bool.Base.html | 75 ++ misc/Data.Empty.Irrelevant.html | 16 + misc/Data.Empty.html | 26 + misc/Data.Maybe.Base.html | 140 +++ misc/Data.Product.html | 208 ++++ misc/Data.Sum.Base.html | 88 ++ misc/Data.These.Base.html | 82 ++ misc/Data.Unit.Base.html | 39 + misc/Function.Base.html | 259 +++++ misc/Function.Bundles.html | 424 ++++++++ misc/Function.Core.html | 30 + misc/Function.Definitions.Core1.html | 27 + misc/Function.Definitions.Core2.html | 31 + misc/Function.Definitions.html | 49 + misc/Function.Equality.html | 126 +++ misc/Function.Structures.html | 154 +++ misc/Function.html | 17 + misc/Level.html | 36 + misc/Relation.Binary.Bundles.html | 301 ++++++ misc/Relation.Binary.Consequences.html | 287 ++++++ misc/Relation.Binary.Core.html | 68 ++ misc/Relation.Binary.Definitions.html | 225 +++++ ....Binary.Indexed.Heterogeneous.Bundles.html | 45 + ...dexed.Heterogeneous.Construct.Trivial.html | 60 ++ ...ion.Binary.Indexed.Heterogeneous.Core.html | 42 + ...ary.Indexed.Heterogeneous.Definitions.html | 37 + ...nary.Indexed.Heterogeneous.Structures.html | 48 + ...Relation.Binary.Indexed.Heterogeneous.html | 49 + ....Binary.PropositionalEquality.Algebra.html | 35 + ...ion.Binary.PropositionalEquality.Core.html | 127 +++ ...nary.PropositionalEquality.Properties.html | 146 +++ ...Relation.Binary.PropositionalEquality.html | 148 +++ ...Relation.Binary.Reasoning.Base.Single.html | 90 ++ misc/Relation.Binary.Reasoning.Setoid.html | 49 + misc/Relation.Binary.Structures.html | 288 ++++++ misc/Relation.Binary.html | 19 + misc/Relation.Nullary.Decidable.Core.html | 132 +++ misc/Relation.Nullary.Reflects.html | 53 + misc/Relation.Nullary.html | 72 ++ misc/Relation.Unary.html | 299 ++++++ misc/Strict.html | 33 + misc/wlpo.html | 111 +++ 60 files changed, 6964 insertions(+) create mode 100644 misc/Agda.Builtin.Bool.html create mode 100644 misc/Agda.Builtin.Equality.html create mode 100644 misc/Agda.Builtin.Maybe.html create mode 100644 misc/Agda.Builtin.Nat.html create mode 100644 misc/Agda.Builtin.Sigma.html create mode 100644 misc/Agda.Builtin.Strict.html create mode 100644 misc/Agda.Builtin.Unit.html create mode 100644 misc/Agda.Primitive.html create mode 100644 misc/Agda.css create mode 100644 misc/Algebra.Bundles.html create mode 100644 misc/Algebra.Consequences.Base.html create mode 100644 misc/Algebra.Consequences.Setoid.html create mode 100644 misc/Algebra.Core.html create mode 100644 misc/Algebra.Definitions.html create mode 100644 misc/Algebra.Structures.html create mode 100644 misc/Algebra.html create mode 100644 misc/Axiom.Extensionality.Propositional.html create mode 100644 misc/Axiom.UniquenessOfIdentityProofs.html create mode 100644 misc/Data.Bool.Base.html create mode 100644 misc/Data.Empty.Irrelevant.html create mode 100644 misc/Data.Empty.html create mode 100644 misc/Data.Maybe.Base.html create mode 100644 misc/Data.Product.html create mode 100644 misc/Data.Sum.Base.html create mode 100644 misc/Data.These.Base.html create mode 100644 misc/Data.Unit.Base.html create mode 100644 misc/Function.Base.html create mode 100644 misc/Function.Bundles.html create mode 100644 misc/Function.Core.html create mode 100644 misc/Function.Definitions.Core1.html create mode 100644 misc/Function.Definitions.Core2.html create mode 100644 misc/Function.Definitions.html create mode 100644 misc/Function.Equality.html create mode 100644 misc/Function.Structures.html create mode 100644 misc/Function.html create mode 100644 misc/Level.html create mode 100644 misc/Relation.Binary.Bundles.html create mode 100644 misc/Relation.Binary.Consequences.html create mode 100644 misc/Relation.Binary.Core.html create mode 100644 misc/Relation.Binary.Definitions.html create mode 100644 misc/Relation.Binary.Indexed.Heterogeneous.Bundles.html create mode 100644 misc/Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html create mode 100644 misc/Relation.Binary.Indexed.Heterogeneous.Core.html create mode 100644 misc/Relation.Binary.Indexed.Heterogeneous.Definitions.html create mode 100644 misc/Relation.Binary.Indexed.Heterogeneous.Structures.html create mode 100644 misc/Relation.Binary.Indexed.Heterogeneous.html create mode 100644 misc/Relation.Binary.PropositionalEquality.Algebra.html create mode 100644 misc/Relation.Binary.PropositionalEquality.Core.html create mode 100644 misc/Relation.Binary.PropositionalEquality.Properties.html create mode 100644 misc/Relation.Binary.PropositionalEquality.html create mode 100644 misc/Relation.Binary.Reasoning.Base.Single.html create mode 100644 misc/Relation.Binary.Reasoning.Setoid.html create mode 100644 misc/Relation.Binary.Structures.html create mode 100644 misc/Relation.Binary.html create mode 100644 misc/Relation.Nullary.Decidable.Core.html create mode 100644 misc/Relation.Nullary.Reflects.html create mode 100644 misc/Relation.Nullary.html create mode 100644 misc/Relation.Unary.html create mode 100644 misc/Strict.html create mode 100644 misc/wlpo.html diff --git a/misc/Agda.Builtin.Bool.html b/misc/Agda.Builtin.Bool.html new file mode 100644 index 0000000..4196669 --- /dev/null +++ b/misc/Agda.Builtin.Bool.html @@ -0,0 +1,17 @@ + +Agda.Builtin.Bool
{-# OPTIONS --without-K --safe --no-universe-polymorphism
+            --no-sized-types --no-guardedness  --no-subtyping #-}
+
+module Agda.Builtin.Bool where
+
+data Bool : Set where
+  false true : Bool
+
+{-# BUILTIN BOOL  Bool  #-}
+{-# BUILTIN FALSE false #-}
+{-# BUILTIN TRUE  true  #-}
+
+{-# COMPILE JS Bool  = function (x,v) { return ((x)? v["true"]() : v["false"]()); } #-}
+{-# COMPILE JS false = false #-}
+{-# COMPILE JS true  = true  #-}
+
\ No newline at end of file diff --git a/misc/Agda.Builtin.Equality.html b/misc/Agda.Builtin.Equality.html new file mode 100644 index 0000000..7bb16ef --- /dev/null +++ b/misc/Agda.Builtin.Equality.html @@ -0,0 +1,12 @@ + +Agda.Builtin.Equality
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
+            --no-subtyping #-}
+
+module Agda.Builtin.Equality where
+
+infix 4 _≡_
+data _≡_ {a} {A : Set a} (x : A) : A → Set a where
+  instance refl : x ≡ x
+
+{-# BUILTIN EQUALITY _≡_ #-}
+
\ No newline at end of file diff --git a/misc/Agda.Builtin.Maybe.html b/misc/Agda.Builtin.Maybe.html new file mode 100644 index 0000000..e055f03 --- /dev/null +++ b/misc/Agda.Builtin.Maybe.html @@ -0,0 +1,12 @@ + +Agda.Builtin.Maybe
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
+            --no-subtyping #-}
+
+module Agda.Builtin.Maybe where
+
+data Maybe {a} (A : Set a) : Set a where
+  just : A → Maybe A
+  nothing : Maybe A
+
+{-# BUILTIN MAYBE Maybe #-}
+
\ No newline at end of file diff --git a/misc/Agda.Builtin.Nat.html b/misc/Agda.Builtin.Nat.html new file mode 100644 index 0000000..7bf950e --- /dev/null +++ b/misc/Agda.Builtin.Nat.html @@ -0,0 +1,136 @@ + +Agda.Builtin.Nat
{-# OPTIONS --without-K --safe --no-universe-polymorphism
+            --no-sized-types --no-guardedness --no-subtyping #-}
+
+module Agda.Builtin.Nat where
+
+open import Agda.Builtin.Bool
+
+data Nat : Set where
+  zero : Nat
+  suc  : (n : Nat) → Nat
+
+{-# BUILTIN NATURAL Nat #-}
+
+infix  4 _==_ _<_
+infixl 6 _+_ _-_
+infixl 7 _*_
+
+_+_ : Nat → Nat → Nat
+zero  + m = m
+suc n + m = suc (n + m)
+
+{-# BUILTIN NATPLUS _+_ #-}
+
+_-_ : Nat → Nat → Nat
+n     - zero = n
+zero  - suc m = zero
+suc n - suc m = n - m
+
+{-# BUILTIN NATMINUS _-_ #-}
+
+_*_ : Nat → Nat → Nat
+zero  * m = zero
+suc n * m = m + n * m
+
+{-# BUILTIN NATTIMES _*_ #-}
+
+_==_ : Nat → Nat → Bool
+zero  == zero  = true
+suc n == suc m = n == m
+_     == _     = false
+
+{-# BUILTIN NATEQUALS _==_ #-}
+
+_<_ : Nat → Nat → Bool
+_     < zero  = false
+zero  < suc _ = true
+suc n < suc m = n < m
+
+{-# BUILTIN NATLESS _<_ #-}
+
+-- Helper function  div-helper  for Euclidean division.
+---------------------------------------------------------------------------
+--
+-- div-helper computes n / 1+m via iteration on n.
+--
+--   n div (suc m) = div-helper 0 m n m
+--
+-- The state of the iterator has two accumulator variables:
+--
+--   k: The quotient, returned once n=0.  Initialized to 0.
+--
+--   j: A counter, initialized to the divisor m, decreased on each iteration step.
+--      Once it reaches 0, the quotient k is increased and j reset to m,
+--      starting the next countdown.
+--
+-- Under the precondition j ≤ m, the invariant is
+--
+--   div-helper k m n j = k + (n + m - j) div (1 + m)
+
+div-helper : (k m n j : Nat) → Nat
+div-helper k m  zero    j      = k
+div-helper k m (suc n)  zero   = div-helper (suc k) m n m
+div-helper k m (suc n) (suc j) = div-helper k       m n j
+
+{-# BUILTIN NATDIVSUCAUX div-helper #-}
+
+-- Proof of the invariant by induction on n.
+--
+--   clause 1: div-helper k m 0 j
+--           = k                                        by definition
+--           = k + (0 + m - j) div (1 + m)              since m - j < 1 + m
+--
+--   clause 2: div-helper k m (1 + n) 0
+--           = div-helper (1 + k) m n m                 by definition
+--           = 1 + k + (n + m - m) div (1 + m)          by induction hypothesis
+--           = 1 + k +          n  div (1 + m)          by simplification
+--           = k +   (n + (1 + m)) div (1 + m)          by expansion
+--           = k + (1 + n + m - 0) div (1 + m)          by expansion
+--
+--   clause 3: div-helper k m (1 + n) (1 + j)
+--           = div-helper k m n j                       by definition
+--           = k + (n + m - j) div (1 + m)              by induction hypothesis
+--           = k + ((1 + n) + m - (1 + j)) div (1 + m)  by expansion
+--
+-- Q.e.d.
+
+-- Helper function  mod-helper  for the remainder computation.
+---------------------------------------------------------------------------
+--
+-- (Analogous to div-helper.)
+--
+-- mod-helper computes n % 1+m via iteration on n.
+--
+--   n mod (suc m) = mod-helper 0 m n m
+--
+-- The invariant is:
+--
+--   m = k + j  ==>  mod-helper k m n j = (n + k) mod (1 + m).
+
+mod-helper : (k m n j : Nat) → Nat
+mod-helper k m  zero    j      = k
+mod-helper k m (suc n)  zero   = mod-helper 0       m n m
+mod-helper k m (suc n) (suc j) = mod-helper (suc k) m n j
+
+{-# BUILTIN NATMODSUCAUX mod-helper #-}
+
+-- Proof of the invariant by induction on n.
+--
+--   clause 1: mod-helper k m 0 j
+--           = k                               by definition
+--           = (0 + k) mod (1 + m)             since m = k + j, thus k < m
+--
+--   clause 2: mod-helper k m (1 + n) 0
+--           = mod-helper 0 m n m              by definition
+--           = (n + 0)       mod (1 + m)       by induction hypothesis
+--           = (n + (1 + m)) mod (1 + m)       by expansion
+--           = (1 + n) + k)  mod (1 + m)       since k = m (as l = 0)
+--
+--   clause 3: mod-helper k m (1 + n) (1 + j)
+--           = mod-helper (1 + k) m n j        by definition
+--           = (n + (1 + k)) mod (1 + m)       by induction hypothesis
+--           = ((1 + n) + k) mod (1 + m)       by commutativity
+--
+-- Q.e.d.
+
\ No newline at end of file diff --git a/misc/Agda.Builtin.Sigma.html b/misc/Agda.Builtin.Sigma.html new file mode 100644 index 0000000..bc1b183 --- /dev/null +++ b/misc/Agda.Builtin.Sigma.html @@ -0,0 +1,20 @@ + +Agda.Builtin.Sigma
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
+            --no-subtyping #-}
+
+module Agda.Builtin.Sigma where
+
+open import Agda.Primitive
+
+record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
+  constructor _,_
+  field
+    fst : A
+    snd : B fst
+
+open Σ public
+
+infixr 4 _,_
+
+{-# BUILTIN SIGMA Σ #-}
+
\ No newline at end of file diff --git a/misc/Agda.Builtin.Strict.html b/misc/Agda.Builtin.Strict.html new file mode 100644 index 0000000..3700db7 --- /dev/null +++ b/misc/Agda.Builtin.Strict.html @@ -0,0 +1,12 @@ + +Agda.Builtin.Strict
{-# OPTIONS --without-K --safe --no-sized-types --no-guardedness
+            --no-subtyping #-}
+
+module Agda.Builtin.Strict where
+
+open import Agda.Builtin.Equality
+
+primitive
+  primForce      : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x
+  primForceLemma : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) (f : ∀ x → B x) → primForce x f ≡ f x
+
\ No newline at end of file diff --git a/misc/Agda.Builtin.Unit.html b/misc/Agda.Builtin.Unit.html new file mode 100644 index 0000000..f41f4bb --- /dev/null +++ b/misc/Agda.Builtin.Unit.html @@ -0,0 +1,12 @@ + +Agda.Builtin.Unit
{-# OPTIONS --without-K --safe --no-universe-polymorphism
+            --no-sized-types --no-guardedness --no-subtyping #-}
+
+module Agda.Builtin.Unit where
+
+record ⊤ : Set where
+  instance constructor tt
+
+{-# BUILTIN UNIT ⊤ #-}
+{-# COMPILE GHC ⊤ = data () (()) #-}
+
\ No newline at end of file diff --git a/misc/Agda.Primitive.html b/misc/Agda.Primitive.html new file mode 100644 index 0000000..6e742cc --- /dev/null +++ b/misc/Agda.Primitive.html @@ -0,0 +1,39 @@ + +Agda.Primitive
-- The Agda primitives (preloaded).
+
+{-# OPTIONS --without-K --no-subtyping --no-import-sorts #-}
+
+module Agda.Primitive where
+
+------------------------------------------------------------------------
+-- Universe levels
+------------------------------------------------------------------------
+
+infixl 6 _⊔_
+
+{-# BUILTIN TYPE Set #-}
+{-# BUILTIN PROP Prop #-}
+{-# BUILTIN SETOMEGA Setω #-}
+{-# BUILTIN STRICTSET      SSet  #-}
+{-# BUILTIN STRICTSETOMEGA SSetω #-}
+
+-- Level is the first thing we need to define.
+-- The other postulates can only be checked if built-in Level is known.
+
+postulate
+  Level : Set
+
+-- MAlonzo compiles Level to (). This should be safe, because it is
+-- not possible to pattern match on levels.
+
+{-# BUILTIN LEVEL Level #-}
+
+postulate
+  lzero : Level
+  lsuc  : (ℓ : Level) → Level
+  _⊔_   : (ℓ₁ ℓ₂ : Level) → Level
+
+{-# BUILTIN LEVELZERO lzero #-}
+{-# BUILTIN LEVELSUC  lsuc  #-}
+{-# BUILTIN LEVELMAX  _⊔_   #-}
+
\ No newline at end of file diff --git a/misc/Agda.css b/misc/Agda.css new file mode 100644 index 0000000..86813a5 --- /dev/null +++ b/misc/Agda.css @@ -0,0 +1,41 @@ +/* Aspects. */ +.Agda .Comment { color: #B22222 } +.Agda .Background {} +.Agda .Markup { color: #000000 } +.Agda .Keyword { color: #CD6600 } +.Agda .String { color: #B22222 } +.Agda .Number { color: #A020F0 } +.Agda .Symbol { color: #404040 } +.Agda .PrimitiveType { color: #0000CD } +.Agda .Pragma { color: black } +.Agda .Operator {} +.Agda .Hole { background: #B4EEB4 } + +/* NameKinds. */ +.Agda .Bound { color: black } +.Agda .Generalizable { color: black } +.Agda .InductiveConstructor { color: #008B00 } +.Agda .CoinductiveConstructor { color: #8B7500 } +.Agda .Datatype { color: #0000CD } +.Agda .Field { color: #EE1289 } +.Agda .Function { color: #0000CD } +.Agda .Module { color: #A020F0 } +.Agda .Postulate { color: #0000CD } +.Agda .Primitive { color: #0000CD } +.Agda .Record { color: #0000CD } + +/* OtherAspects. */ +.Agda .DottedPattern {} +.Agda .UnsolvedMeta { color: black; background: yellow } +.Agda .UnsolvedConstraint { color: black; background: yellow } +.Agda .TerminationProblem { color: black; background: #FFA07A } +.Agda .IncompletePattern { color: black; background: #F5DEB3 } +.Agda .Error { color: red; text-decoration: underline } +.Agda .TypeChecks { color: black; background: #ADD8E6 } +.Agda .Deadcode { color: black; background: #808080 } +.Agda .ShadowingInTelescope { color: black; background: #808080 } + +/* Standard attributes. */ +.Agda a { text-decoration: none } +.Agda a[href]:hover { background-color: #B4EEB4 } +.Agda [href].hover-highlight { background-color: #B4EEB4; } diff --git a/misc/Algebra.Bundles.html b/misc/Algebra.Bundles.html new file mode 100644 index 0000000..da4f183 --- /dev/null +++ b/misc/Algebra.Bundles.html @@ -0,0 +1,934 @@ + +Algebra.Bundles
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definitions of algebraic structures like monoids and rings
+-- (packed in records together with sets, operations, etc.)
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via `Algebra`.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Algebra.Bundles where
+
+open import Algebra.Core
+open import Algebra.Structures
+open import Relation.Binary
+open import Function.Base
+import Relation.Nullary as N
+open import Level
+
+------------------------------------------------------------------------
+-- Bundles with 1 binary operation
+------------------------------------------------------------------------
+
+record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _∙_     : Op₂ Carrier
+
+  infix 4 _≉_
+  _≉_ : Rel Carrier _
+  x ≉ y = N.¬ (x ≈ y)
+
+
+record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _∙_     : Op₂ Carrier
+    isMagma : IsMagma _≈_ _∙_
+
+  open IsMagma isMagma public
+
+  rawMagma : RawMagma _ _
+  rawMagma = record { _≈_ = _≈_; _∙_ = _∙_ }
+
+  open RawMagma rawMagma public
+    using (_≉_)
+
+
+record SelectiveMagma c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier          : Set c
+    _≈_              : Rel Carrier ℓ
+    _∙_              : Op₂ Carrier
+    isSelectiveMagma : IsSelectiveMagma _≈_ _∙_
+
+  open IsSelectiveMagma isSelectiveMagma public
+
+  magma : Magma c ℓ
+  magma = record { isMagma = isMagma }
+
+  open Magma magma public using (rawMagma)
+
+
+record CommutativeMagma c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier            : Set c
+    _≈_                : Rel Carrier ℓ
+    _∙_                : Op₂ Carrier
+    isCommutativeMagma : IsCommutativeMagma _≈_ _∙_
+
+  open IsCommutativeMagma isCommutativeMagma public
+
+  magma : Magma c ℓ
+  magma = record { isMagma = isMagma }
+
+  open Magma magma public using (rawMagma)
+
+
+record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier     : Set c
+    _≈_         : Rel Carrier ℓ
+    _∙_         : Op₂ Carrier
+    isSemigroup : IsSemigroup _≈_ _∙_
+
+  open IsSemigroup isSemigroup public
+
+  magma : Magma c ℓ
+  magma = record { isMagma = isMagma }
+
+  open Magma magma public
+    using (_≉_; rawMagma)
+
+
+record Band c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _∙_     : Op₂ Carrier
+    isBand  : IsBand _≈_ _∙_
+
+  open IsBand isBand public
+
+  semigroup : Semigroup c ℓ
+  semigroup = record { isSemigroup = isSemigroup }
+
+  open Semigroup semigroup public
+    using (_≉_; magma; rawMagma)
+
+
+record CommutativeSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier                 : Set c
+    _≈_                     : Rel Carrier ℓ
+    _∙_                     : Op₂ Carrier
+    isCommutativeSemigroup  : IsCommutativeSemigroup _≈_ _∙_
+
+  open IsCommutativeSemigroup isCommutativeSemigroup public
+
+  semigroup : Semigroup c ℓ
+  semigroup = record { isSemigroup = isSemigroup }
+
+  open Semigroup semigroup public
+    using (_≉_; magma; rawMagma)
+
+  commutativeMagma : CommutativeMagma c ℓ
+  commutativeMagma = record { isCommutativeMagma = isCommutativeMagma }
+
+
+record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixr 7 _∧_
+  infix  4 _≈_
+  field
+    Carrier       : Set c
+    _≈_           : Rel Carrier ℓ
+    _∧_           : Op₂ Carrier
+    isSemilattice : IsSemilattice _≈_ _∧_
+
+  open IsSemilattice isSemilattice public
+
+  band : Band c ℓ
+  band = record { isBand = isBand }
+
+  open Band band public
+    using (_≉_; rawMagma; magma; semigroup)
+
+
+------------------------------------------------------------------------
+-- Bundles with 1 binary operation & 1 element
+------------------------------------------------------------------------
+
+-- A raw monoid is a monoid without any laws.
+
+record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _∙_     : Op₂ Carrier
+    ε       : Carrier
+
+  rawMagma : RawMagma c ℓ
+  rawMagma = record
+    { _≈_ = _≈_
+    ; _∙_ = _∙_
+    }
+
+  open RawMagma rawMagma public
+    using (_≉_)
+
+
+record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier  : Set c
+    _≈_      : Rel Carrier ℓ
+    _∙_      : Op₂ Carrier
+    ε        : Carrier
+    isMonoid : IsMonoid _≈_ _∙_ ε
+
+  open IsMonoid isMonoid public
+
+  semigroup : Semigroup _ _
+  semigroup = record { isSemigroup = isSemigroup }
+
+  open Semigroup semigroup public
+    using (_≉_; rawMagma; magma)
+
+  rawMonoid : RawMonoid _ _
+  rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε}
+
+
+record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier             : Set c
+    _≈_                 : Rel Carrier ℓ
+    _∙_                 : Op₂ Carrier
+    ε                   : Carrier
+    isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε
+
+  open IsCommutativeMonoid isCommutativeMonoid public
+
+  monoid : Monoid _ _
+  monoid = record { isMonoid = isMonoid }
+
+  open Monoid monoid public
+    using (_≉_; rawMagma; magma; semigroup; rawMonoid)
+
+  commutativeSemigroup : CommutativeSemigroup _ _
+  commutativeSemigroup = record { isCommutativeSemigroup = isCommutativeSemigroup }
+
+  open CommutativeSemigroup commutativeSemigroup public
+    using (commutativeMagma)
+
+
+record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier                       : Set c
+    _≈_                           : Rel Carrier ℓ
+    _∙_                           : Op₂ Carrier
+    ε                             : Carrier
+    isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _≈_ _∙_ ε
+
+  open IsIdempotentCommutativeMonoid isIdempotentCommutativeMonoid public
+
+  commutativeMonoid : CommutativeMonoid _ _
+  commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
+
+  open CommutativeMonoid commutativeMonoid public
+    using
+    ( _≉_; rawMagma; magma; commutativeMagma; semigroup; commutativeSemigroup
+    ; rawMonoid; monoid
+    )
+
+
+-- Idempotent commutative monoids are also known as bounded lattices.
+-- Note that the BoundedLattice necessarily uses the notation inherited
+-- from monoids rather than lattices.
+
+BoundedLattice = IdempotentCommutativeMonoid
+
+module BoundedLattice {c ℓ} (idemCommMonoid : IdempotentCommutativeMonoid c ℓ) =
+       IdempotentCommutativeMonoid idemCommMonoid
+
+
+------------------------------------------------------------------------
+-- Bundles with 1 binary operation, 1 unary operation & 1 element
+------------------------------------------------------------------------
+
+record RawGroup c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 _⁻¹
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _∙_     : Op₂ Carrier
+    ε       : Carrier
+    _⁻¹     : Op₁ Carrier
+
+  rawMonoid : RawMonoid c ℓ
+  rawMonoid = record
+    { _≈_ = _≈_
+    ; _∙_ = _∙_
+    ; ε   = ε
+    }
+
+  open RawMonoid rawMonoid public
+    using (_≉_; rawMagma)
+
+
+record Group c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 _⁻¹
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _∙_     : Op₂ Carrier
+    ε       : Carrier
+    _⁻¹     : Op₁ Carrier
+    isGroup : IsGroup _≈_ _∙_ ε _⁻¹
+
+  open IsGroup isGroup public
+
+  rawGroup : RawGroup _ _
+  rawGroup = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹}
+
+  monoid : Monoid _ _
+  monoid = record { isMonoid = isMonoid }
+
+  open Monoid monoid public
+    using (_≉_; rawMagma; magma; semigroup; rawMonoid)
+
+record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 _⁻¹
+  infixl 7 _∙_
+  infix  4 _≈_
+  field
+    Carrier        : Set c
+    _≈_            : Rel Carrier ℓ
+    _∙_            : Op₂ Carrier
+    ε              : Carrier
+    _⁻¹            : Op₁ Carrier
+    isAbelianGroup : IsAbelianGroup _≈_ _∙_ ε _⁻¹
+
+  open IsAbelianGroup isAbelianGroup public
+
+  group : Group _ _
+  group = record { isGroup = isGroup }
+
+  open Group group public
+    using (_≉_; rawMagma; magma; semigroup; monoid; rawMonoid; rawGroup)
+
+  commutativeMonoid : CommutativeMonoid _ _
+  commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }
+
+  open CommutativeMonoid commutativeMonoid public
+    using (commutativeMagma; commutativeSemigroup)
+
+
+------------------------------------------------------------------------
+-- Bundles with 2 binary operations
+------------------------------------------------------------------------
+
+record RawLattice c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixr 7 _∧_
+  infixr 6 _∨_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _∧_     : Op₂ Carrier
+    _∨_     : Op₂ Carrier
+
+  ∨-rawMagma : RawMagma c ℓ
+  ∨-rawMagma = record { _≈_ = _≈_; _∙_ = _∨_ }
+
+  ∧-rawMagma : RawMagma c ℓ
+  ∧-rawMagma = record { _≈_ = _≈_; _∙_ = _∧_ }
+
+  open RawMagma ∨-rawMagma public
+    using (_≉_)
+
+
+record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixr 7 _∧_
+  infixr 6 _∨_
+  infix  4 _≈_
+  field
+    Carrier   : Set c
+    _≈_       : Rel Carrier ℓ
+    _∨_       : Op₂ Carrier
+    _∧_       : Op₂ Carrier
+    isLattice : IsLattice _≈_ _∨_ _∧_
+
+  open IsLattice isLattice public
+
+  rawLattice : RawLattice c ℓ
+  rawLattice = record
+    { _≈_  = _≈_
+    ; _∧_  = _∧_
+    ; _∨_  = _∨_
+    }
+
+  open RawLattice rawLattice
+    using (∨-rawMagma; ∧-rawMagma)
+
+  setoid : Setoid _ _
+  setoid = record { isEquivalence = isEquivalence }
+
+  open Setoid setoid public
+    using (_≉_)
+
+
+record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixr 7 _∧_
+  infixr 6 _∨_
+  infix  4 _≈_
+  field
+    Carrier               : Set c
+    _≈_                   : Rel Carrier ℓ
+    _∨_                   : Op₂ Carrier
+    _∧_                   : Op₂ Carrier
+    isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_
+
+  open IsDistributiveLattice isDistributiveLattice public
+
+  lattice : Lattice _ _
+  lattice = record { isLattice = isLattice }
+
+  open Lattice lattice public
+    using (_≉_; rawLattice; setoid)
+
+
+------------------------------------------------------------------------
+-- Bundles with 2 binary operations & 1 element
+------------------------------------------------------------------------
+
+record RawNearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _+_     : Op₂ Carrier
+    _*_     : Op₂ Carrier
+    0#      : Carrier
+
+  +-rawMonoid : RawMonoid c ℓ
+  +-rawMonoid = record
+    { _≈_ = _≈_
+    ; _∙_ = _+_
+    ;  ε  = 0#
+    }
+
+  open RawMonoid +-rawMonoid public
+    using (_≉_) renaming (rawMagma to +-rawMagma)
+
+  *-rawMagma : RawMagma c ℓ
+  *-rawMagma = record
+    { _≈_ = _≈_
+    ; _∙_ = _*_
+    }
+
+
+record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier        : Set c
+    _≈_            : Rel Carrier ℓ
+    _+_            : Op₂ Carrier
+    _*_            : Op₂ Carrier
+    0#             : Carrier
+    isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0#
+
+  open IsNearSemiring isNearSemiring public
+
+  rawNearSemiring : RawNearSemiring _ _
+  rawNearSemiring = record
+    { _≈_ = _≈_
+    ; _+_ = _+_
+    ; _*_ = _*_
+    ; 0#  = 0#
+    }
+
+  +-monoid : Monoid _ _
+  +-monoid = record { isMonoid = +-isMonoid }
+
+  open Monoid +-monoid public
+    using (_≉_) renaming
+    ( rawMagma  to +-rawMagma
+    ; magma     to +-magma
+    ; semigroup to +-semigroup
+    ; rawMonoid to +-rawMonoid
+    )
+
+  *-semigroup : Semigroup _ _
+  *-semigroup = record { isSemigroup = *-isSemigroup }
+
+  open Semigroup *-semigroup public
+    using () renaming
+    ( rawMagma to *-rawMagma
+    ; magma    to *-magma
+    )
+
+
+record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier              : Set c
+    _≈_                  : Rel Carrier ℓ
+    _+_                  : Op₂ Carrier
+    _*_                  : Op₂ Carrier
+    0#                   : Carrier
+    isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0#
+
+  open IsSemiringWithoutOne isSemiringWithoutOne public
+
+  nearSemiring : NearSemiring _ _
+  nearSemiring = record { isNearSemiring = isNearSemiring }
+
+  open NearSemiring nearSemiring public
+    using
+    ( _≉_; +-rawMagma; +-magma; +-semigroup
+    ; +-rawMonoid; +-monoid
+    ; *-rawMagma; *-magma; *-semigroup
+    ; rawNearSemiring
+    )
+
+  +-commutativeMonoid : CommutativeMonoid _ _
+  +-commutativeMonoid = record { isCommutativeMonoid = +-isCommutativeMonoid }
+
+  open CommutativeMonoid +-commutativeMonoid public
+    using () renaming
+    ( commutativeMagma     to +-commutativeMagma
+    ; commutativeSemigroup to +-commutativeSemigroup
+    )
+
+
+record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier                         : Set c
+    _≈_                             : Rel Carrier ℓ
+    _+_                             : Op₂ Carrier
+    _*_                             : Op₂ Carrier
+    0#                              : Carrier
+    isCommutativeSemiringWithoutOne :
+      IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0#
+
+  open IsCommutativeSemiringWithoutOne
+         isCommutativeSemiringWithoutOne public
+
+  semiringWithoutOne : SemiringWithoutOne _ _
+  semiringWithoutOne =
+    record { isSemiringWithoutOne = isSemiringWithoutOne }
+
+  open SemiringWithoutOne semiringWithoutOne public
+    using
+    ( _≉_; +-rawMagma; +-magma; +-semigroup; +-commutativeSemigroup
+    ; *-rawMagma; *-magma; *-semigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; nearSemiring; rawNearSemiring
+    )
+
+------------------------------------------------------------------------
+-- Bundles with 2 binary operations & 2 elements
+------------------------------------------------------------------------
+
+record RawSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _+_     : Op₂ Carrier
+    _*_     : Op₂ Carrier
+    0#      : Carrier
+    1#      : Carrier
+
+  rawNearSemiring : RawNearSemiring c ℓ
+  rawNearSemiring = record
+    { _≈_ = _≈_
+    ; _+_ = _+_
+    ; _*_ = _*_
+    ; 0#  = 0#
+    }
+
+  open RawNearSemiring rawNearSemiring public
+    using (_≉_; +-rawMonoid; +-rawMagma; *-rawMagma)
+
+  *-rawMonoid : RawMonoid c ℓ
+  *-rawMonoid = record
+    { _≈_ = _≈_
+    ; _∙_ = _*_
+    ; ε   = 1#
+    }
+
+
+record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier                           : Set c
+    _≈_                               : Rel Carrier ℓ
+    _+_                               : Op₂ Carrier
+    _*_                               : Op₂ Carrier
+    0#                                : Carrier
+    1#                                : Carrier
+    isSemiringWithoutAnnihilatingZero :
+      IsSemiringWithoutAnnihilatingZero _≈_ _+_ _*_ 0# 1#
+
+  open IsSemiringWithoutAnnihilatingZero
+         isSemiringWithoutAnnihilatingZero public
+
+  rawSemiring : RawSemiring c ℓ
+  rawSemiring = record
+    { _≈_ = _≈_
+    ; _+_ = _+_
+    ; _*_ = _*_
+    ; 0#  = 0#
+    ; 1#  = 1#
+    }
+
+  open RawSemiring rawSemiring public
+    using (rawNearSemiring)
+
+  +-commutativeMonoid : CommutativeMonoid _ _
+  +-commutativeMonoid =
+    record { isCommutativeMonoid = +-isCommutativeMonoid }
+
+  open CommutativeMonoid +-commutativeMonoid public
+    using (_≉_) renaming
+    ( rawMagma             to +-rawMagma
+    ; magma                to +-magma
+    ; commutativeMagma     to +-commutativeMagma
+    ; semigroup            to +-semigroup
+    ; commutativeSemigroup to +-commutativeSemigroup
+    ; rawMonoid            to +-rawMonoid
+    ; monoid               to +-monoid
+    )
+
+  *-monoid : Monoid _ _
+  *-monoid = record { isMonoid = *-isMonoid }
+
+  open Monoid *-monoid public
+    using () renaming
+    ( rawMagma  to *-rawMagma
+    ; magma     to *-magma
+    ; semigroup to *-semigroup
+    ; rawMonoid to *-rawMonoid
+    )
+
+
+record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier    : Set c
+    _≈_        : Rel Carrier ℓ
+    _+_        : Op₂ Carrier
+    _*_        : Op₂ Carrier
+    0#         : Carrier
+    1#         : Carrier
+    isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#
+
+  open IsSemiring isSemiring public
+
+  semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero _ _
+  semiringWithoutAnnihilatingZero = record
+    { isSemiringWithoutAnnihilatingZero =
+        isSemiringWithoutAnnihilatingZero
+    }
+
+  open SemiringWithoutAnnihilatingZero
+         semiringWithoutAnnihilatingZero public
+    using
+    ( _≉_; +-rawMagma;  +-magma;  +-commutativeMagma; +-semigroup; +-commutativeSemigroup
+    ; *-rawMagma;  *-magma;  *-semigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid
+    ; rawNearSemiring ; rawSemiring
+    )
+
+  semiringWithoutOne : SemiringWithoutOne _ _
+  semiringWithoutOne =
+    record { isSemiringWithoutOne = isSemiringWithoutOne }
+
+  open SemiringWithoutOne semiringWithoutOne public
+    using (nearSemiring)
+
+
+record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier               : Set c
+    _≈_                   : Rel Carrier ℓ
+    _+_                   : Op₂ Carrier
+    _*_                   : Op₂ Carrier
+    0#                    : Carrier
+    1#                    : Carrier
+    isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#
+
+  open IsCommutativeSemiring isCommutativeSemiring public
+
+  semiring : Semiring _ _
+  semiring = record { isSemiring = isSemiring }
+
+  open Semiring semiring public
+    using
+    ( _≉_; +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
+    ; *-rawMagma; *-magma; *-semigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid
+    ; nearSemiring; semiringWithoutOne
+    ; semiringWithoutAnnihilatingZero
+    ; rawSemiring
+    )
+
+  *-commutativeMonoid : CommutativeMonoid _ _
+  *-commutativeMonoid = record
+    { isCommutativeMonoid = *-isCommutativeMonoid
+    }
+
+  open CommutativeMonoid *-commutativeMonoid public
+    using () renaming
+    ( commutativeMagma     to *-commutativeMagma
+    ; commutativeSemigroup to *-commutativeSemigroup
+    )
+
+  commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne _ _
+  commutativeSemiringWithoutOne = record
+    { isCommutativeSemiringWithoutOne = isCommutativeSemiringWithoutOne
+    }
+
+
+record CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier                           : Set c
+    _≈_                               : Rel Carrier ℓ
+    _+_                               : Op₂ Carrier
+    _*_                               : Op₂ Carrier
+    0#                                : Carrier
+    1#                                : Carrier
+    isCancellativeCommutativeSemiring : IsCancellativeCommutativeSemiring _≈_ _+_ _*_ 0# 1#
+
+  open IsCancellativeCommutativeSemiring isCancellativeCommutativeSemiring public
+
+  commutativeSemiring : CommutativeSemiring c ℓ
+  commutativeSemiring = record
+    { isCommutativeSemiring = isCommutativeSemiring
+    }
+
+  open CommutativeSemiring commutativeSemiring public
+    using
+    ( +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
+    ; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid; *-commutativeMonoid
+    ; nearSemiring; semiringWithoutOne
+    ; semiringWithoutAnnihilatingZero
+    ; rawSemiring
+    ; semiring
+    ; _≉_
+    )
+
+
+------------------------------------------------------------------------
+-- Bundles with 2 binary operations, 1 unary operation & 2 elements
+------------------------------------------------------------------------
+
+-- A raw ring is a ring without any laws.
+
+record RawRing c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 -_
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _+_     : Op₂ Carrier
+    _*_     : Op₂ Carrier
+    -_      : Op₁ Carrier
+    0#      : Carrier
+    1#      : Carrier
+
+  rawSemiring : RawSemiring c ℓ
+  rawSemiring = record
+    { _≈_ = _≈_
+    ; _+_ = _+_
+    ; _*_ = _*_
+    ; 0#  = 0#
+    ; 1#  = 1#
+    }
+
+  open RawSemiring rawSemiring public
+    using
+    ( _≉_
+    ; +-rawMagma; +-rawMonoid
+    ; *-rawMagma; *-rawMonoid
+    )
+
+  +-rawGroup : RawGroup c ℓ
+  +-rawGroup = record
+    { _≈_ = _≈_
+    ; _∙_ = _+_
+    ; ε   = 0#
+    ; _⁻¹ = -_
+    }
+
+record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 -_
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier : Set c
+    _≈_     : Rel Carrier ℓ
+    _+_     : Op₂ Carrier
+    _*_     : Op₂ Carrier
+    -_      : Op₁ Carrier
+    0#      : Carrier
+    1#      : Carrier
+    isRing  : IsRing _≈_ _+_ _*_ -_ 0# 1#
+
+  open IsRing isRing public
+
+  +-abelianGroup : AbelianGroup _ _
+  +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }
+
+  semiring : Semiring _ _
+  semiring = record { isSemiring = isSemiring }
+
+  open Semiring semiring public
+    using
+    ( _≉_; +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
+    ; *-rawMagma; *-magma; *-semigroup
+    ; +-rawMonoid; +-monoid ; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid
+    ; nearSemiring; semiringWithoutOne
+    ; semiringWithoutAnnihilatingZero
+    )
+
+  open AbelianGroup +-abelianGroup public
+    using () renaming (group to +-group)
+
+  rawRing : RawRing _ _
+  rawRing = record
+    { _≈_ = _≈_
+    ; _+_ = _+_
+    ; _*_ = _*_
+    ; -_  = -_
+    ; 0#  = 0#
+    ; 1#  = 1#
+    }
+
+
+record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 -_
+  infixl 7 _*_
+  infixl 6 _+_
+  infix  4 _≈_
+  field
+    Carrier           : Set c
+    _≈_               : Rel Carrier ℓ
+    _+_               : Op₂ Carrier
+    _*_               : Op₂ Carrier
+    -_                : Op₁ Carrier
+    0#                : Carrier
+    1#                : Carrier
+    isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1#
+
+  open IsCommutativeRing isCommutativeRing public
+
+  ring : Ring _ _
+  ring = record { isRing = isRing }
+
+  open Ring ring public using (_≉_; rawRing; +-group; +-abelianGroup)
+
+  commutativeSemiring : CommutativeSemiring _ _
+  commutativeSemiring =
+    record { isCommutativeSemiring = isCommutativeSemiring }
+
+  open CommutativeSemiring commutativeSemiring public
+    using
+    ( +-rawMagma; +-magma; +-commutativeMagma; +-semigroup; +-commutativeSemigroup
+    ; *-rawMagma; *-magma; *-commutativeMagma; *-semigroup; *-commutativeSemigroup
+    ; +-rawMonoid; +-monoid; +-commutativeMonoid
+    ; *-rawMonoid; *-monoid; *-commutativeMonoid
+    ; nearSemiring; semiringWithoutOne
+    ; semiringWithoutAnnihilatingZero; semiring
+    ; commutativeSemiringWithoutOne
+    )
+
+
+record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix  8 ¬_
+  infixr 7 _∧_
+  infixr 6 _∨_
+  infix  4 _≈_
+  field
+    Carrier          : Set c
+    _≈_              : Rel Carrier ℓ
+    _∨_              : Op₂ Carrier
+    _∧_              : Op₂ Carrier
+    ¬_               : Op₁ Carrier
+    ⊤                : Carrier
+    ⊥                : Carrier
+    isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥
+
+  open IsBooleanAlgebra isBooleanAlgebra public
+
+  distributiveLattice : DistributiveLattice _ _
+  distributiveLattice = record { isDistributiveLattice = isDistributiveLattice }
+
+  open DistributiveLattice distributiveLattice public
+    using (_≉_; setoid; lattice)
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 1.0
+
+RawSemigroup = RawMagma
+{-# WARNING_ON_USAGE RawSemigroup
+"Warning: RawSemigroup was deprecated in v1.0.
+Please use RawMagma instead."
+#-}
+
\ No newline at end of file diff --git a/misc/Algebra.Consequences.Base.html b/misc/Algebra.Consequences.Base.html new file mode 100644 index 0000000..49b64eb --- /dev/null +++ b/misc/Algebra.Consequences.Base.html @@ -0,0 +1,24 @@ + +Algebra.Consequences.Base
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Lemmas relating algebraic definitions (such as associativity and
+-- commutativity) that don't the equality relation to be a setoid.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Algebra.Consequences.Base
+  {a} {A : Set a} where
+
+open import Algebra.Core
+open import Algebra.Definitions
+open import Data.Sum.Base
+open import Relation.Binary.Core
+
+sel⇒idem : ∀ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) →
+           Selective _≈_ _•_ → Idempotent _≈_ _•_
+sel⇒idem _ sel x with sel x x
+... | inj₁ x•x≈x = x•x≈x
+... | inj₂ x•x≈x = x•x≈x
+
\ No newline at end of file diff --git a/misc/Algebra.Consequences.Setoid.html b/misc/Algebra.Consequences.Setoid.html new file mode 100644 index 0000000..86ec30a --- /dev/null +++ b/misc/Algebra.Consequences.Setoid.html @@ -0,0 +1,216 @@ + +Algebra.Consequences.Setoid
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Relations between properties of functions, such as associativity and
+-- commutativity, when the underlying relation is a setoid
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Rel; Setoid; Substitutive; Symmetric; Total)
+
+module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where
+
+open Setoid S renaming (Carrier to A)
+open import Algebra.Core
+open import Algebra.Definitions _≈_
+open import Data.Sum.Base using (inj₁; inj₂)
+open import Data.Product using (_,_)
+open import Function.Base using (_$_)
+import Relation.Binary.Consequences as Bin
+open import Relation.Binary.Reasoning.Setoid S
+open import Relation.Unary using (Pred)
+
+------------------------------------------------------------------------
+-- Re-exports
+
+-- Export base lemmas that don't require the setoid
+
+open import Algebra.Consequences.Base public
+
+------------------------------------------------------------------------
+-- Magma-like structures
+
+module _ {_•_ : Op₂ A} (comm : Commutative _•_) where
+
+  comm+cancelˡ⇒cancelʳ : LeftCancellative _•_ → RightCancellative _•_
+  comm+cancelˡ⇒cancelʳ cancelˡ {x} y z eq = cancelˡ x $ begin
+    x • y ≈⟨ comm x y ⟩
+    y • x ≈⟨ eq ⟩
+    z • x ≈⟨ comm z x ⟩
+    x • z ∎
+
+  comm+cancelʳ⇒cancelˡ : RightCancellative _•_ → LeftCancellative _•_
+  comm+cancelʳ⇒cancelˡ cancelʳ x {y} {z} eq = cancelʳ y z $ begin
+    y • x ≈⟨ comm y x ⟩
+    x • y ≈⟨ eq ⟩
+    x • z ≈⟨ comm x z ⟩
+    z • x ∎
+
+------------------------------------------------------------------------
+-- Monoid-like structures
+
+module _ {_•_ : Op₂ A} (comm : Commutative _•_) {e : A} where
+
+  comm+idˡ⇒idʳ : LeftIdentity e _•_ → RightIdentity e _•_
+  comm+idˡ⇒idʳ idˡ x = begin
+    x • e ≈⟨ comm x e ⟩
+    e • x ≈⟨ idˡ x ⟩
+    x     ∎
+
+  comm+idʳ⇒idˡ : RightIdentity e _•_ → LeftIdentity e _•_
+  comm+idʳ⇒idˡ idʳ x = begin
+    e • x ≈⟨ comm e x ⟩
+    x • e ≈⟨ idʳ x ⟩
+    x     ∎
+
+  comm+zeˡ⇒zeʳ : LeftZero e _•_ → RightZero e _•_
+  comm+zeˡ⇒zeʳ zeˡ x = begin
+    x • e ≈⟨ comm x e ⟩
+    e • x ≈⟨ zeˡ x ⟩
+    e     ∎
+
+  comm+zeʳ⇒zeˡ : RightZero e _•_ → LeftZero e _•_
+  comm+zeʳ⇒zeˡ zeʳ x = begin
+    e • x ≈⟨ comm e x ⟩
+    x • e ≈⟨ zeʳ x ⟩
+    e     ∎
+
+  comm+almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _•_ →
+                                     AlmostRightCancellative e _•_
+  comm+almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero {x} y z x≉e yx≈zx =
+    cancelˡ-nonZero y z x≉e $ begin
+      x • y ≈⟨ comm x y ⟩
+      y • x ≈⟨ yx≈zx ⟩
+      z • x ≈⟨ comm z x ⟩
+      x • z ∎
+
+  comm+almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _•_ →
+                                     AlmostLeftCancellative e _•_
+  comm+almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero {x} y z x≉e xy≈xz =
+    cancelʳ-nonZero y z x≉e $ begin
+      y • x ≈⟨ comm y x ⟩
+      x • y ≈⟨ xy≈xz ⟩
+      x • z ≈⟨ comm x z ⟩
+      z • x ∎
+
+------------------------------------------------------------------------
+-- Group-like structures
+
+module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _•_) where
+
+  comm+invˡ⇒invʳ : LeftInverse e _⁻¹ _•_ → RightInverse e _⁻¹ _•_
+  comm+invˡ⇒invʳ invˡ x = begin
+    x • (x ⁻¹) ≈⟨ comm x (x ⁻¹) ⟩
+    (x ⁻¹) • x ≈⟨ invˡ x ⟩
+    e          ∎
+
+  comm+invʳ⇒invˡ : RightInverse e _⁻¹ _•_ → LeftInverse e _⁻¹ _•_
+  comm+invʳ⇒invˡ invʳ x = begin
+    (x ⁻¹) • x ≈⟨ comm (x ⁻¹) x ⟩
+    x • (x ⁻¹) ≈⟨ invʳ x ⟩
+    e          ∎
+
+module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _•_) where
+
+  assoc+id+invʳ⇒invˡ-unique : Associative _•_ →
+                              Identity e _•_ → RightInverse e _⁻¹ _•_ →
+                              ∀ x y → (x • y) ≈ e → x ≈ (y ⁻¹)
+  assoc+id+invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x y eq = begin
+    x                ≈⟨ sym (idʳ x) ⟩
+    x • e            ≈⟨ cong refl (sym (invʳ y)) ⟩
+    x • (y • (y ⁻¹)) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩
+    (x • y) • (y ⁻¹) ≈⟨ cong eq refl ⟩
+    e • (y ⁻¹)       ≈⟨ idˡ (y ⁻¹) ⟩
+    y ⁻¹             ∎
+
+  assoc+id+invˡ⇒invʳ-unique : Associative _•_ →
+                              Identity e _•_ → LeftInverse e _⁻¹ _•_ →
+                              ∀ x y → (x • y) ≈ e → y ≈ (x ⁻¹)
+  assoc+id+invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ x y eq = begin
+    y                ≈⟨ sym (idˡ y) ⟩
+    e • y            ≈⟨ cong (sym (invˡ x)) refl ⟩
+    ((x ⁻¹) • x) • y ≈⟨ assoc (x ⁻¹) x y ⟩
+    (x ⁻¹) • (x • y) ≈⟨ cong refl eq ⟩
+    (x ⁻¹) • e       ≈⟨ idʳ (x ⁻¹) ⟩
+    x ⁻¹             ∎
+
+----------------------------------------------------------------------
+-- Bisemigroup-like structures
+
+module _ {_•_ _◦_ : Op₂ A}
+         (◦-cong : Congruent₂ _◦_)
+         (•-comm : Commutative _•_)
+         where
+
+  comm+distrˡ⇒distrʳ :  _•_ DistributesOverˡ _◦_ → _•_ DistributesOverʳ _◦_
+  comm+distrˡ⇒distrʳ distrˡ x y z = begin
+    (y ◦ z) • x       ≈⟨ •-comm (y ◦ z) x ⟩
+    x • (y ◦ z)       ≈⟨ distrˡ x y z ⟩
+    (x • y) ◦ (x • z) ≈⟨ ◦-cong (•-comm x y) (•-comm x z) ⟩
+    (y • x) ◦ (z • x) ∎
+
+  comm+distrʳ⇒distrˡ : _•_ DistributesOverʳ _◦_ → _•_ DistributesOverˡ _◦_
+  comm+distrʳ⇒distrˡ distrˡ x y z = begin
+    x • (y ◦ z)       ≈⟨ •-comm x (y ◦ z) ⟩
+    (y ◦ z) • x       ≈⟨ distrˡ x y z ⟩
+    (y • x) ◦ (z • x) ≈⟨ ◦-cong (•-comm y x) (•-comm z x) ⟩
+    (x • y) ◦ (x • z) ∎
+
+  comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y • z)) ≈ ((x ◦ y) • (x ◦ z)))
+  comm⇒sym[distribˡ] x {y} {z} prf = begin
+    x ◦ (z • y)       ≈⟨ ◦-cong refl (•-comm z y) ⟩
+    x ◦ (y • z)       ≈⟨ prf ⟩
+    (x ◦ y) • (x ◦ z) ≈⟨ •-comm (x ◦ y) (x ◦ z) ⟩
+    (x ◦ z) • (x ◦ y) ∎
+
+----------------------------------------------------------------------
+-- Ring-like structures
+
+module _ {_+_ _*_ : Op₂ A}
+         {_⁻¹ : Op₁ A} {0# : A}
+         (+-cong : Congruent₂ _+_)
+         (*-cong : Congruent₂ _*_)
+         where
+
+  assoc+distribʳ+idʳ+invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
+                                RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
+                                LeftZero 0# _*_
+  assoc+distribʳ+idʳ+invʳ⇒zeˡ +-assoc distribʳ idʳ invʳ  x = begin
+    0# * x                                 ≈⟨ sym (idʳ _) ⟩
+    (0# * x) + 0#                          ≈⟨ +-cong refl (sym (invʳ _)) ⟩
+    (0# * x) + ((0# * x)  + ((0# * x)⁻¹))  ≈⟨ sym (+-assoc _ _ _) ⟩
+    ((0# * x) +  (0# * x)) + ((0# * x)⁻¹)  ≈⟨ +-cong (sym (distribʳ _ _ _)) refl ⟩
+    ((0# + 0#) * x) + ((0# * x)⁻¹)         ≈⟨ +-cong (*-cong (idʳ _) refl) refl ⟩
+    (0# * x) + ((0# * x)⁻¹)                ≈⟨ invʳ _ ⟩
+    0#                                     ∎
+
+  assoc+distribˡ+idʳ+invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
+                                RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
+                                RightZero 0# _*_
+  assoc+distribˡ+idʳ+invʳ⇒zeʳ +-assoc distribˡ idʳ invʳ  x = begin
+     x * 0#                                ≈⟨ sym (idʳ _) ⟩
+     (x * 0#) + 0#                         ≈⟨ +-cong refl (sym (invʳ _)) ⟩
+     (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹))  ≈⟨ sym (+-assoc _ _ _) ⟩
+     ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹)  ≈⟨ +-cong (sym (distribˡ _ _ _)) refl ⟩
+     (x * (0# + 0#)) + ((x * 0#)⁻¹)        ≈⟨ +-cong (*-cong refl (idʳ _)) refl ⟩
+     ((x * 0#) + ((x * 0#)⁻¹))             ≈⟨ invʳ _ ⟩
+     0#                                    ∎
+
+------------------------------------------------------------------------
+-- Without Loss of Generality
+
+module _ {p} {f : Op₂ A} {P : Pred A p}
+         (≈-subst : Substitutive _≈_ p)
+         (comm : Commutative f)
+         where
+
+  subst+comm⇒sym : Symmetric (λ a b → P (f a b))
+  subst+comm⇒sym = ≈-subst P (comm _ _)
+
+  wlog : ∀ {r} {_R_ : Rel _ r} → Total _R_ →
+         (∀ a b → a R b → P (f a b)) →
+         ∀ a b → P (f a b)
+  wlog r-total = Bin.wlog r-total subst+comm⇒sym
+
\ No newline at end of file diff --git a/misc/Algebra.Core.html b/misc/Algebra.Core.html new file mode 100644 index 0000000..7c99a27 --- /dev/null +++ b/misc/Algebra.Core.html @@ -0,0 +1,33 @@ + +Algebra.Core
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Core algebraic definitions
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via `Algebra`.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Algebra.Core where
+
+open import Level using (_⊔_)
+
+------------------------------------------------------------------------
+-- Unary and binary operations
+
+Op₁ : ∀ {ℓ} → Set ℓ → Set ℓ
+Op₁ A = A → A
+
+Op₂ : ∀ {ℓ} → Set ℓ → Set ℓ
+Op₂ A = A → A → A
+
+------------------------------------------------------------------------
+-- Left and right actions
+
+Opₗ : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
+Opₗ A B = A → B → B
+
+Opᵣ : ∀ {a b} → Set a → Set b → Set (a ⊔ b)
+Opᵣ A B = B → A → B
+
\ No newline at end of file diff --git a/misc/Algebra.Definitions.html b/misc/Algebra.Definitions.html new file mode 100644 index 0000000..cdce7ee --- /dev/null +++ b/misc/Algebra.Definitions.html @@ -0,0 +1,134 @@ + +Algebra.Definitions
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of functions, such as associativity and commutativity
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via `Algebra`, unless
+-- you want to parameterise it via the equality relation.
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Core
+open import Relation.Nullary using (¬_)
+
+module Algebra.Definitions
+  {a ℓ} {A : Set a}   -- The underlying set
+  (_≈_ : Rel A ℓ)     -- The underlying equality
+  where
+
+open import Algebra.Core
+open import Data.Product
+open import Data.Sum.Base
+
+------------------------------------------------------------------------
+-- Properties of operations
+
+Congruent₁ : Op₁ A → Set _
+Congruent₁ f = f Preserves _≈_ ⟶ _≈_
+
+Congruent₂ : Op₂ A → Set _
+Congruent₂ ∙ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
+
+LeftCongruent : Op₂ A → Set _
+LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_
+
+RightCongruent : Op₂ A → Set _
+RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_
+
+Associative : Op₂ A → Set _
+Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))
+
+Commutative : Op₂ A → Set _
+Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x)
+
+LeftIdentity : A → Op₂ A → Set _
+LeftIdentity e _∙_ = ∀ x → (e ∙ x) ≈ x
+
+RightIdentity : A → Op₂ A → Set _
+RightIdentity e _∙_ = ∀ x → (x ∙ e) ≈ x
+
+Identity : A → Op₂ A → Set _
+Identity e ∙ = (LeftIdentity e ∙) × (RightIdentity e ∙)
+
+LeftZero : A → Op₂ A → Set _
+LeftZero z _∙_ = ∀ x → (z ∙ x) ≈ z
+
+RightZero : A → Op₂ A → Set _
+RightZero z _∙_ = ∀ x → (x ∙ z) ≈ z
+
+Zero : A → Op₂ A → Set _
+Zero z ∙ = (LeftZero z ∙) × (RightZero z ∙)
+
+LeftInverse : A → Op₁ A → Op₂ A → Set _
+LeftInverse e _⁻¹ _∙_ = ∀ x → ((x ⁻¹) ∙ x) ≈ e
+
+RightInverse : A → Op₁ A → Op₂ A → Set _
+RightInverse e _⁻¹ _∙_ = ∀ x → (x ∙ (x ⁻¹)) ≈ e
+
+Inverse : A → Op₁ A → Op₂ A → Set _
+Inverse e ⁻¹ ∙ = (LeftInverse e ⁻¹) ∙ × (RightInverse e ⁻¹ ∙)
+
+LeftConical : A → Op₂ A → Set _
+LeftConical e _∙_ = ∀ x y → (x ∙ y) ≈ e → x ≈ e
+
+RightConical : A → Op₂ A → Set _
+RightConical e _∙_ = ∀ x y → (x ∙ y) ≈ e → y ≈ e
+
+Conical : A → Op₂ A → Set _
+Conical e ∙ = (LeftConical e ∙) × (RightConical e ∙)
+
+_DistributesOverˡ_ : Op₂ A → Op₂ A → Set _
+_*_ DistributesOverˡ _+_ =
+  ∀ x y z → (x * (y + z)) ≈ ((x * y) + (x * z))
+
+_DistributesOverʳ_ : Op₂ A → Op₂ A → Set _
+_*_ DistributesOverʳ _+_ =
+  ∀ x y z → ((y + z) * x) ≈ ((y * x) + (z * x))
+
+_DistributesOver_ : Op₂ A → Op₂ A → Set _
+* DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)
+
+_IdempotentOn_ : Op₂ A → A → Set _
+_∙_ IdempotentOn x = (x ∙ x) ≈ x
+
+Idempotent : Op₂ A → Set _
+Idempotent ∙ = ∀ x → ∙ IdempotentOn x
+
+IdempotentFun : Op₁ A → Set _
+IdempotentFun f = ∀ x → f (f x) ≈ f x
+
+Selective : Op₂ A → Set _
+Selective _∙_ = ∀ x y → (x ∙ y) ≈ x ⊎ (x ∙ y) ≈ y
+
+_Absorbs_ : Op₂ A → Op₂ A → Set _
+_∙_ Absorbs _∘_ = ∀ x y → (x ∙ (x ∘ y)) ≈ x
+
+Absorptive : Op₂ A → Op₂ A → Set _
+Absorptive ∙ ∘ = (∙ Absorbs ∘) × (∘ Absorbs ∙)
+
+Involutive : Op₁ A → Set _
+Involutive f = ∀ x → f (f x) ≈ x
+
+LeftCancellative : Op₂ A → Set _
+LeftCancellative _•_ = ∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z
+
+RightCancellative : Op₂ A → Set _
+RightCancellative _•_ = ∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z
+
+Cancellative : Op₂ A → Set _
+Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_)
+
+AlmostLeftCancellative : A → Op₂ A → Set _
+AlmostLeftCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z
+
+AlmostRightCancellative : A → Op₂ A → Set _
+AlmostRightCancellative e _•_ = ∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z
+
+AlmostCancellative : A → Op₂ A → Set _
+AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_
+
+Interchangable : Op₂ A → Op₂ A → Set _
+Interchangable _∘_ _∙_ = ∀ w x y z → ((w ∙ x) ∘ (y ∙ z)) ≈ ((w ∘ y) ∙ (x ∘ z))
+
\ No newline at end of file diff --git a/misc/Algebra.Structures.html b/misc/Algebra.Structures.html new file mode 100644 index 0000000..baade22 --- /dev/null +++ b/misc/Algebra.Structures.html @@ -0,0 +1,571 @@ + +Algebra.Structures
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some algebraic structures (not packed up with sets, operations,
+-- etc.)
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via `Algebra`, unless
+-- you want to parameterise it via the equality relation.
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+
+module Algebra.Structures
+  {a ℓ} {A : Set a}  -- The underlying set
+  (_≈_ : Rel A ℓ)    -- The underlying equality relation
+  where
+
+-- The file is divided into sections depending on the arities of the
+-- components of the algebraic structure.
+
+open import Algebra.Core
+open import Algebra.Definitions _≈_
+import Algebra.Consequences.Setoid as Consequences
+open import Data.Product using (_,_; proj₁; proj₂)
+open import Level using (_⊔_)
+
+------------------------------------------------------------------------
+-- Structures with 1 binary operation
+------------------------------------------------------------------------
+
+record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
+  field
+    isEquivalence : IsEquivalence _≈_
+    ∙-cong        : Congruent₂ ∙
+
+  open IsEquivalence isEquivalence public
+
+  setoid : Setoid a ℓ
+  setoid = record { isEquivalence = isEquivalence }
+
+  ∙-congˡ : LeftCongruent ∙
+  ∙-congˡ y≈z = ∙-cong refl y≈z
+
+  ∙-congʳ : RightCongruent ∙
+  ∙-congʳ y≈z = ∙-cong y≈z refl
+
+
+record IsCommutativeMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
+  field
+    isMagma : IsMagma ∙
+    comm    : Commutative ∙
+
+  open IsMagma isMagma public
+
+
+record IsSelectiveMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
+  field
+    isMagma : IsMagma ∙
+    sel     : Selective ∙
+
+  open IsMagma isMagma public
+
+
+record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
+  field
+    isMagma : IsMagma ∙
+    assoc   : Associative ∙
+
+  open IsMagma isMagma public
+
+
+record IsBand (∙ : Op₂ A) : Set (a ⊔ ℓ) where
+  field
+    isSemigroup : IsSemigroup ∙
+    idem        : Idempotent ∙
+
+  open IsSemigroup isSemigroup public
+
+
+record IsCommutativeSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ) where
+  field
+    isSemigroup : IsSemigroup ∙
+    comm        : Commutative ∙
+
+  open IsSemigroup isSemigroup public
+
+  isCommutativeMagma : IsCommutativeMagma ∙
+  isCommutativeMagma = record
+    { isMagma = isMagma
+    ; comm    = comm
+    }
+
+
+record IsSemilattice (∧ : Op₂ A) : Set (a ⊔ ℓ) where
+  field
+    isBand : IsBand ∧
+    comm   : Commutative ∧
+
+  open IsBand isBand public
+    renaming (∙-cong to ∧-cong; ∙-congˡ to ∧-congˡ; ∙-congʳ to ∧-congʳ)
+
+
+
+------------------------------------------------------------------------
+-- Structures with 1 binary operation & 1 element
+------------------------------------------------------------------------
+
+record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
+  field
+    isSemigroup : IsSemigroup ∙
+    identity    : Identity ε ∙
+
+  open IsSemigroup isSemigroup public
+
+  identityˡ : LeftIdentity ε ∙
+  identityˡ = proj₁ identity
+
+  identityʳ : RightIdentity ε ∙
+  identityʳ = proj₂ identity
+
+
+record IsCommutativeMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where
+  field
+    isMonoid : IsMonoid ∙ ε
+    comm     : Commutative ∙
+
+  open IsMonoid isMonoid public
+
+  isCommutativeSemigroup : IsCommutativeSemigroup ∙
+  isCommutativeSemigroup = record
+    { isSemigroup = isSemigroup
+    ; comm        = comm
+    }
+
+  open IsCommutativeSemigroup isCommutativeSemigroup public
+    using (isCommutativeMagma)
+
+
+record IsIdempotentCommutativeMonoid (∙ : Op₂ A)
+                                     (ε : A) : Set (a ⊔ ℓ) where
+  field
+    isCommutativeMonoid : IsCommutativeMonoid ∙ ε
+    idem                : Idempotent ∙
+
+  open IsCommutativeMonoid isCommutativeMonoid public
+
+
+-- Idempotent commutative monoids are also known as bounded lattices.
+-- Note that the BoundedLattice necessarily uses the notation inherited
+-- from monoids rather than lattices.
+
+IsBoundedLattice = IsIdempotentCommutativeMonoid
+
+module IsBoundedLattice {∙ : Op₂ A}
+                        {ε : A}
+                        (isIdemCommMonoid : IsIdempotentCommutativeMonoid ∙ ε) =
+       IsIdempotentCommutativeMonoid isIdemCommMonoid
+
+
+------------------------------------------------------------------------
+-- Structures with 1 binary operation, 1 unary operation & 1 element
+------------------------------------------------------------------------
+
+record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
+  field
+    isMonoid  : IsMonoid _∙_ ε
+    inverse   : Inverse ε _⁻¹ _∙_
+    ⁻¹-cong   : Congruent₁ _⁻¹
+
+  open IsMonoid isMonoid public
+
+  infixl 6 _-_
+  _-_ : Op₂ A
+  x - y = x ∙ (y ⁻¹)
+
+  inverseˡ : LeftInverse ε _⁻¹ _∙_
+  inverseˡ = proj₁ inverse
+
+  inverseʳ : RightInverse ε _⁻¹ _∙_
+  inverseʳ = proj₂ inverse
+
+  uniqueˡ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → x ≈ (y ⁻¹)
+  uniqueˡ-⁻¹ = Consequences.assoc+id+invʳ⇒invˡ-unique
+                setoid ∙-cong assoc identity inverseʳ
+
+  uniqueʳ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → y ≈ (x ⁻¹)
+  uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique
+                setoid ∙-cong assoc identity inverseˡ
+
+
+record IsAbelianGroup (∙ : Op₂ A)
+                      (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ) where
+  field
+    isGroup : IsGroup ∙ ε ⁻¹
+    comm    : Commutative ∙
+
+  open IsGroup isGroup public
+
+  isCommutativeMonoid : IsCommutativeMonoid ∙ ε
+  isCommutativeMonoid = record
+    { isMonoid = isMonoid
+    ; comm     = comm
+    }
+
+  open IsCommutativeMonoid isCommutativeMonoid public
+    using (isCommutativeMagma; isCommutativeSemigroup)
+
+
+------------------------------------------------------------------------
+-- Structures with 2 binary operations
+------------------------------------------------------------------------
+
+-- Note that `IsLattice` is not defined in terms of `IsSemilattice`
+-- because the idempotence laws of ∨ and ∧ can be derived from the
+-- absorption laws, which makes the corresponding "idem" fields
+-- redundant.  The derived idempotence laws are stated and proved in
+-- `Algebra.Properties.Lattice` along with the fact that every lattice
+-- consists of two semilattices.
+
+record IsLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
+  field
+    isEquivalence : IsEquivalence _≈_
+    ∨-comm        : Commutative ∨
+    ∨-assoc       : Associative ∨
+    ∨-cong        : Congruent₂ ∨
+    ∧-comm        : Commutative ∧
+    ∧-assoc       : Associative ∧
+    ∧-cong        : Congruent₂ ∧
+    absorptive    : Absorptive ∨ ∧
+
+  open IsEquivalence isEquivalence public
+
+  ∨-absorbs-∧ : ∨ Absorbs ∧
+  ∨-absorbs-∧ = proj₁ absorptive
+
+  ∧-absorbs-∨ : ∧ Absorbs ∨
+  ∧-absorbs-∨ = proj₂ absorptive
+
+  ∧-congˡ : LeftCongruent ∧
+  ∧-congˡ y≈z = ∧-cong refl y≈z
+
+  ∧-congʳ : RightCongruent ∧
+  ∧-congʳ y≈z = ∧-cong y≈z refl
+
+  ∨-congˡ : LeftCongruent ∨
+  ∨-congˡ y≈z = ∨-cong refl y≈z
+
+  ∨-congʳ : RightCongruent ∨
+  ∨-congʳ y≈z = ∨-cong y≈z refl
+
+
+record IsDistributiveLattice (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where
+  field
+    isLattice    : IsLattice ∨ ∧
+    ∨-distribʳ-∧ : ∨ DistributesOverʳ ∧
+
+  open IsLattice isLattice public
+
+  ∨-∧-distribʳ = ∨-distribʳ-∧
+  {-# WARNING_ON_USAGE ∨-∧-distribʳ
+  "Warning: ∨-∧-distribʳ was deprecated in v1.1.
+  Please use ∨-distribʳ-∧ instead."
+  #-}
+
+------------------------------------------------------------------------
+-- Structures with 2 binary operations & 1 element
+------------------------------------------------------------------------
+
+record IsNearSemiring (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
+  field
+    +-isMonoid    : IsMonoid + 0#
+    *-isSemigroup : IsSemigroup *
+    distribʳ      : * DistributesOverʳ +
+    zeroˡ         : LeftZero 0# *
+
+  open IsMonoid +-isMonoid public
+    renaming
+    ( assoc       to +-assoc
+    ; ∙-cong      to +-cong
+    ; ∙-congˡ     to +-congˡ
+    ; ∙-congʳ     to +-congʳ
+    ; identity    to +-identity
+    ; identityˡ   to +-identityˡ
+    ; identityʳ   to +-identityʳ
+    ; isMagma     to +-isMagma
+    ; isSemigroup to +-isSemigroup
+    )
+
+  open IsSemigroup *-isSemigroup public
+    using ()
+    renaming
+    ( assoc    to *-assoc
+    ; ∙-cong   to *-cong
+    ; ∙-congˡ  to *-congˡ
+    ; ∙-congʳ  to *-congʳ
+    ; isMagma  to *-isMagma
+    )
+
+
+record IsSemiringWithoutOne (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
+  field
+    +-isCommutativeMonoid : IsCommutativeMonoid + 0#
+    *-isSemigroup         : IsSemigroup *
+    distrib               : * DistributesOver +
+    zero                  : Zero 0# *
+
+  open IsCommutativeMonoid +-isCommutativeMonoid public
+    using ()
+    renaming
+    ( comm                   to +-comm
+    ; isMonoid               to +-isMonoid
+    ; isCommutativeMagma     to +-isCommutativeMagma
+    ; isCommutativeSemigroup to +-isCommutativeSemigroup
+    )
+
+  zeroˡ : LeftZero 0# *
+  zeroˡ = proj₁ zero
+
+  zeroʳ : RightZero 0# *
+  zeroʳ = proj₂ zero
+
+  isNearSemiring : IsNearSemiring + * 0#
+  isNearSemiring = record
+    { +-isMonoid    = +-isMonoid
+    ; *-isSemigroup = *-isSemigroup
+    ; distribʳ      = proj₂ distrib
+    ; zeroˡ         = zeroˡ
+    }
+
+  open IsNearSemiring isNearSemiring public
+    hiding (+-isMonoid; zeroˡ; *-isSemigroup)
+
+
+record IsCommutativeSemiringWithoutOne
+         (+ * : Op₂ A) (0# : A) : Set (a ⊔ ℓ) where
+  field
+    isSemiringWithoutOne : IsSemiringWithoutOne + * 0#
+    *-comm               : Commutative *
+
+  open IsSemiringWithoutOne isSemiringWithoutOne public
+
+  *-isCommutativeSemigroup : IsCommutativeSemigroup *
+  *-isCommutativeSemigroup = record
+    { isSemigroup = *-isSemigroup
+    ; comm        = *-comm
+    }
+
+  open IsCommutativeSemigroup *-isCommutativeSemigroup public
+    using () renaming (isCommutativeMagma to *-isCommutativeMagma)
+
+------------------------------------------------------------------------
+-- Structures with 2 binary operations & 2 elements
+------------------------------------------------------------------------
+
+record IsSemiringWithoutAnnihilatingZero (+ * : Op₂ A)
+                                         (0# 1# : A) : Set (a ⊔ ℓ) where
+  field
+    -- Note that these structures do have an additive unit, but this
+    -- unit does not necessarily annihilate multiplication.
+    +-isCommutativeMonoid : IsCommutativeMonoid + 0#
+    *-isMonoid            : IsMonoid * 1#
+    distrib               : * DistributesOver +
+
+  distribˡ : * DistributesOverˡ +
+  distribˡ = proj₁ distrib
+
+  distribʳ : * DistributesOverʳ +
+  distribʳ = proj₂ distrib
+
+  open IsCommutativeMonoid +-isCommutativeMonoid public
+    renaming
+    ( assoc                  to +-assoc
+    ; ∙-cong                 to +-cong
+    ; ∙-congˡ                to +-congˡ
+    ; ∙-congʳ                to +-congʳ
+    ; identity               to +-identity
+    ; identityˡ              to +-identityˡ
+    ; identityʳ              to +-identityʳ
+    ; comm                   to +-comm
+    ; isMagma                to +-isMagma
+    ; isSemigroup            to +-isSemigroup
+    ; isMonoid               to +-isMonoid
+    ; isCommutativeMagma     to +-isCommutativeMagma
+    ; isCommutativeSemigroup to +-isCommutativeSemigroup
+    )
+
+  open IsMonoid *-isMonoid public
+    using ()
+    renaming
+    ( assoc       to *-assoc
+    ; ∙-cong      to *-cong
+    ; ∙-congˡ     to *-congˡ
+    ; ∙-congʳ     to *-congʳ
+    ; identity    to *-identity
+    ; identityˡ   to *-identityˡ
+    ; identityʳ   to *-identityʳ
+    ; isMagma     to *-isMagma
+    ; isSemigroup to *-isSemigroup
+    )
+
+
+record IsSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+  field
+    isSemiringWithoutAnnihilatingZero :
+      IsSemiringWithoutAnnihilatingZero + * 0# 1#
+    zero : Zero 0# *
+
+  open IsSemiringWithoutAnnihilatingZero
+         isSemiringWithoutAnnihilatingZero public
+
+  isSemiringWithoutOne : IsSemiringWithoutOne + * 0#
+  isSemiringWithoutOne = record
+    { +-isCommutativeMonoid = +-isCommutativeMonoid
+    ; *-isSemigroup         = *-isSemigroup
+    ; distrib               = distrib
+    ; zero                  = zero
+    }
+
+  open IsSemiringWithoutOne isSemiringWithoutOne public
+    using
+    ( isNearSemiring
+    ; zeroˡ
+    ; zeroʳ
+    )
+
+
+record IsCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+  field
+    isSemiring : IsSemiring + * 0# 1#
+    *-comm     : Commutative *
+
+  open IsSemiring isSemiring public
+
+  isCommutativeSemiringWithoutOne :
+    IsCommutativeSemiringWithoutOne + * 0#
+  isCommutativeSemiringWithoutOne = record
+    { isSemiringWithoutOne = isSemiringWithoutOne
+    ; *-comm = *-comm
+    }
+
+  open IsCommutativeSemiringWithoutOne isCommutativeSemiringWithoutOne public
+    using
+    ( *-isCommutativeMagma
+    ; *-isCommutativeSemigroup
+    )
+
+  *-isCommutativeMonoid : IsCommutativeMonoid * 1#
+  *-isCommutativeMonoid = record
+    { isMonoid = *-isMonoid
+    ; comm     = *-comm
+    }
+
+
+record IsCancellativeCommutativeSemiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+  field
+    isCommutativeSemiring : IsCommutativeSemiring + * 0# 1#
+    *-cancelˡ-nonZero     : AlmostLeftCancellative 0# *
+
+  open IsCommutativeSemiring isCommutativeSemiring public
+
+
+
+------------------------------------------------------------------------
+-- Structures with 2 binary operations, 1 unary operation & 2 elements
+------------------------------------------------------------------------
+
+record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+  field
+    +-isAbelianGroup : IsAbelianGroup + 0# -_
+    *-isMonoid       : IsMonoid * 1#
+    distrib          : * DistributesOver +
+    zero             : Zero 0# *
+
+  open IsAbelianGroup +-isAbelianGroup public
+    renaming
+    ( assoc                  to +-assoc
+    ; ∙-cong                 to +-cong
+    ; ∙-congˡ                to +-congˡ
+    ; ∙-congʳ                to +-congʳ
+    ; identity               to +-identity
+    ; identityˡ              to +-identityˡ
+    ; identityʳ              to +-identityʳ
+    ; inverse                to -‿inverse
+    ; inverseˡ               to -‿inverseˡ
+    ; inverseʳ               to -‿inverseʳ
+    ; ⁻¹-cong                to -‿cong
+    ; comm                   to +-comm
+    ; isMagma                to +-isMagma
+    ; isSemigroup            to +-isSemigroup
+    ; isMonoid               to +-isMonoid
+    ; isCommutativeMagma     to +-isCommutativeMagma
+    ; isCommutativeMonoid    to +-isCommutativeMonoid
+    ; isCommutativeSemigroup to +-isCommutativeSemigroup
+    ; isGroup                to +-isGroup
+    )
+
+  open IsMonoid *-isMonoid public
+    using ()
+    renaming
+    ( assoc       to *-assoc
+    ; ∙-cong      to *-cong
+    ; ∙-congˡ     to *-congˡ
+    ; ∙-congʳ     to *-congʳ
+    ; identity    to *-identity
+    ; identityˡ   to *-identityˡ
+    ; identityʳ   to *-identityʳ
+    ; isMagma     to *-isMagma
+    ; isSemigroup to *-isSemigroup
+    )
+
+  zeroˡ : LeftZero 0# *
+  zeroˡ = proj₁ zero
+
+  zeroʳ : RightZero 0# *
+  zeroʳ = proj₂ zero
+
+  isSemiringWithoutAnnihilatingZero
+    : IsSemiringWithoutAnnihilatingZero + * 0# 1#
+  isSemiringWithoutAnnihilatingZero = record
+    { +-isCommutativeMonoid = +-isCommutativeMonoid
+    ; *-isMonoid            = *-isMonoid
+    ; distrib               = distrib
+    }
+
+  isSemiring : IsSemiring + * 0# 1#
+  isSemiring = record
+    { isSemiringWithoutAnnihilatingZero =
+        isSemiringWithoutAnnihilatingZero
+    ; zero = zero
+    }
+
+  open IsSemiring isSemiring public
+    using (distribˡ; distribʳ; isNearSemiring; isSemiringWithoutOne)
+
+
+record IsCommutativeRing
+         (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
+  field
+    isRing : IsRing + * - 0# 1#
+    *-comm : Commutative *
+
+  open IsRing isRing public
+
+  isCommutativeSemiring : IsCommutativeSemiring + * 0# 1#
+  isCommutativeSemiring = record
+    { isSemiring = isSemiring
+    ; *-comm = *-comm
+    }
+
+  open IsCommutativeSemiring isCommutativeSemiring public
+    using
+    ( isCommutativeSemiringWithoutOne
+    ; *-isCommutativeMagma
+    ; *-isCommutativeSemigroup
+    ; *-isCommutativeMonoid
+    )
+
+
+record IsBooleanAlgebra
+         (∨ ∧ : Op₂ A) (¬ : Op₁ A) (⊤ ⊥ : A) : Set (a ⊔ ℓ) where
+  field
+    isDistributiveLattice : IsDistributiveLattice ∨ ∧
+    ∨-complementʳ         : RightInverse ⊤ ¬ ∨
+    ∧-complementʳ         : RightInverse ⊥ ¬ ∧
+    ¬-cong                : Congruent₁ ¬
+
+  open IsDistributiveLattice isDistributiveLattice public
+
\ No newline at end of file diff --git a/misc/Algebra.html b/misc/Algebra.html new file mode 100644 index 0000000..c85aeae --- /dev/null +++ b/misc/Algebra.html @@ -0,0 +1,17 @@ + +Algebra
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definitions of algebraic structures like monoids and rings
+-- (packed in records together with sets, operations, etc.)
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Algebra where
+
+open import Algebra.Core public
+open import Algebra.Definitions public
+open import Algebra.Structures public
+open import Algebra.Bundles public
+
\ No newline at end of file diff --git a/misc/Axiom.Extensionality.Propositional.html b/misc/Axiom.Extensionality.Propositional.html new file mode 100644 index 0000000..0effe28 --- /dev/null +++ b/misc/Axiom.Extensionality.Propositional.html @@ -0,0 +1,64 @@ + +Axiom.Extensionality.Propositional
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Results concerning function extensionality for propositional equality
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Axiom.Extensionality.Propositional where
+
+open import Function.Base
+open import Level using (Level; _⊔_; suc; lift)
+open import Relation.Binary.Core
+open import Relation.Binary.PropositionalEquality.Core
+
+------------------------------------------------------------------------
+-- Function extensionality states that if two functions are
+-- propositionally equal for every input, then the functions themselves
+-- must be propositionally equal.
+
+Extensionality : (a b : Level) → Set _
+Extensionality a b =
+  {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
+  (∀ x → f x ≡ g x) → f ≡ g
+
+-- A variant for implicit function spaces.
+
+ExtensionalityImplicit : (a b : Level) → Set _
+ExtensionalityImplicit a b =
+  {A : Set a} {B : A → Set b} {f g : {x : A} → B x} →
+  (∀ {x} → f {x} ≡ g {x}) → (λ {x} → f {x}) ≡ (λ {x} → g {x})
+
+
+------------------------------------------------------------------------
+-- Properties
+
+-- If extensionality holds for a given universe level, then it also
+-- holds for lower ones.
+
+lower-extensionality : ∀ {a₁ b₁} a₂ b₂ →
+                       Extensionality (a₁ ⊔ a₂) (b₁ ⊔ b₂) →
+                       Extensionality a₁ b₁
+lower-extensionality a₂ b₂ ext f≡g = cong (λ h → Level.lower ∘ h ∘ lift) $
+    ext (cong (lift {ℓ = b₂}) ∘ f≡g ∘ Level.lower {ℓ = a₂})
+
+-- Functional extensionality implies a form of extensionality for
+-- Π-types.
+
+∀-extensionality : ∀ {a b} → Extensionality a (suc b) →
+                   {A : Set a} (B₁ B₂ : A → Set b) →
+                   (∀ x → B₁ x ≡ B₂ x) →
+                   (∀ x → B₁ x) ≡ (∀ x → B₂ x)
+∀-extensionality ext B₁ B₂ B₁≡B₂ with ext B₁≡B₂
+... | refl = refl
+
+-- Extensionality for explicit function spaces implies extensionality
+-- for implicit function spaces.
+
+implicit-extensionality : ∀ {a b} →
+                          Extensionality a b →
+                          ExtensionalityImplicit a b
+implicit-extensionality ext f≡g = cong _$- (ext (λ x → f≡g))
+
\ No newline at end of file diff --git a/misc/Axiom.UniquenessOfIdentityProofs.html b/misc/Axiom.UniquenessOfIdentityProofs.html new file mode 100644 index 0000000..276fd33 --- /dev/null +++ b/misc/Axiom.UniquenessOfIdentityProofs.html @@ -0,0 +1,79 @@ + +Axiom.UniquenessOfIdentityProofs
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Results concerning uniqueness of identity proofs
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Axiom.UniquenessOfIdentityProofs where
+
+open import Data.Bool.Base using (true; false)
+open import Data.Empty
+open import Relation.Nullary.Reflects using (invert)
+open import Relation.Nullary hiding (Irrelevant)
+open import Relation.Binary.Core
+open import Relation.Binary.Definitions
+open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality.Properties
+
+------------------------------------------------------------------------
+-- Definition
+--
+-- Uniqueness of Identity Proofs (UIP) states that all proofs of
+-- equality are themselves equal. In other words, the equality relation
+-- is irrelevant. Here we define UIP relative to a given type.
+
+UIP : ∀ {a} (A : Set a) → Set a
+UIP A = Irrelevant {A = A} _≡_
+
+------------------------------------------------------------------------
+-- Properties
+
+-- UIP always holds when using axiom K
+-- (see `Axiom.UniquenessOfIdentityProofs.WithK`).
+
+-- The existence of a constant function over proofs of equality for
+-- elements in A is enough to prove UIP for A. Indeed, we can relate any
+-- proof to its image via this function which we then know is equal to
+-- the image of any other proof.
+
+module Constant⇒UIP
+  {a} {A : Set a} (f : _≡_ {A = A} ⇒ _≡_)
+  (f-constant : ∀ {a b} (p q : a ≡ b) → f p ≡ f q)
+  where
+
+  ≡-canonical : ∀ {a b} (p : a ≡ b) → trans (sym (f refl)) (f p) ≡ p
+  ≡-canonical refl = trans-symˡ (f refl)
+
+  ≡-irrelevant : UIP A
+  ≡-irrelevant p q = begin
+    p                          ≡⟨ sym (≡-canonical p) ⟩
+    trans (sym (f refl)) (f p) ≡⟨ cong (trans _) (f-constant p q) ⟩
+    trans (sym (f refl)) (f q) ≡⟨ ≡-canonical q ⟩
+    q                          ∎
+    where open ≡-Reasoning
+
+-- If equality is decidable for a given type, then we can prove UIP for
+-- that type. Indeed, the decision procedure allows us to define a
+-- function over proofs of equality which is constant: it returns the
+-- proof produced by the decision procedure.
+
+module Decidable⇒UIP
+  {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
+  where
+
+  ≡-normalise : _≡_ {A = A} ⇒ _≡_
+  ≡-normalise {a} {b} a≡b with a ≟ b
+  ... | true  because  [p] = invert [p]
+  ... | false because [¬p] = ⊥-elim (invert [¬p] a≡b)
+
+  ≡-normalise-constant : ∀ {a b} (p q : a ≡ b) → ≡-normalise p ≡ ≡-normalise q
+  ≡-normalise-constant {a} {b} p q with a ≟ b
+  ... | true  because   _  = refl
+  ... | false because [¬p] = ⊥-elim (invert [¬p] p)
+
+  ≡-irrelevant : UIP A
+  ≡-irrelevant = Constant⇒UIP.≡-irrelevant ≡-normalise ≡-normalise-constant
+
\ No newline at end of file diff --git a/misc/Data.Bool.Base.html b/misc/Data.Bool.Base.html new file mode 100644 index 0000000..cea82ed --- /dev/null +++ b/misc/Data.Bool.Base.html @@ -0,0 +1,75 @@ + +Data.Bool.Base
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The type for booleans and some operations
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Bool.Base where
+
+open import Data.Unit.Base using (⊤)
+open import Data.Empty
+open import Level using (Level)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+------------------------------------------------------------------------
+-- The boolean type
+
+open import Agda.Builtin.Bool public
+
+------------------------------------------------------------------------
+-- Relations
+
+infix 4 _≤_ _<_
+
+data _≤_ : Bool → Bool → Set where
+  f≤t : false ≤ true
+  b≤b : ∀ {b} → b ≤ b
+
+data _<_ : Bool → Bool → Set where
+  f<t : false < true
+
+------------------------------------------------------------------------
+-- Boolean operations
+
+infixr 6 _∧_
+infixr 5 _∨_ _xor_
+
+not : Bool → Bool
+not true  = false
+not false = true
+
+_∧_ : Bool → Bool → Bool
+true  ∧ b = b
+false ∧ b = false
+
+_∨_ : Bool → Bool → Bool
+true  ∨ b = true
+false ∨ b = b
+
+_xor_ : Bool → Bool → Bool
+true  xor b = not b
+false xor b = b
+
+------------------------------------------------------------------------
+-- Other operations
+
+infix  0 if_then_else_
+
+if_then_else_ : Bool → A → A → A
+if true  then t else f = t
+if false then t else f = f
+
+-- A function mapping true to an inhabited type and false to an empty
+-- type.
+
+T : Bool → Set
+T true  = ⊤
+T false = ⊥
+
\ No newline at end of file diff --git a/misc/Data.Empty.Irrelevant.html b/misc/Data.Empty.Irrelevant.html new file mode 100644 index 0000000..f78d9fe --- /dev/null +++ b/misc/Data.Empty.Irrelevant.html @@ -0,0 +1,16 @@ + +Data.Empty.Irrelevant
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- An irrelevant version of ⊥-elim
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Empty.Irrelevant where
+
+open import Data.Empty hiding (⊥-elim)
+
+⊥-elim : ∀ {w} {Whatever : Set w} → .⊥ → Whatever
+⊥-elim ()
+
\ No newline at end of file diff --git a/misc/Data.Empty.html b/misc/Data.Empty.html new file mode 100644 index 0000000..5400ac8 --- /dev/null +++ b/misc/Data.Empty.html @@ -0,0 +1,26 @@ + +Data.Empty
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Empty type
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Empty where
+
+------------------------------------------------------------------------
+-- Definition
+
+-- Note that by default the empty type is not universe polymorphic as it
+-- often results in unsolved metas. See `Data.Empty.Polymorphic` for a
+-- universe polymorphic variant.
+
+data ⊥ : Set where
+
+------------------------------------------------------------------------
+-- Functions
+
+⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
+⊥-elim ()
+
\ No newline at end of file diff --git a/misc/Data.Maybe.Base.html b/misc/Data.Maybe.Base.html new file mode 100644 index 0000000..a2a6f2a --- /dev/null +++ b/misc/Data.Maybe.Base.html @@ -0,0 +1,140 @@ + +Data.Maybe.Base
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The Maybe type and some operations
+------------------------------------------------------------------------
+
+-- The definitions in this file are reexported by Data.Maybe.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Maybe.Base where
+
+open import Level
+open import Data.Bool.Base using (Bool; true; false; not)
+open import Data.Unit.Base using (⊤)
+open import Data.These.Base using (These; this; that; these)
+open import Data.Product as Prod using (_×_; _,_)
+open import Function.Base
+open import Relation.Nullary.Reflects
+open import Relation.Nullary
+
+private
+  variable
+    a b c : Level
+    A : Set a
+    B : Set b
+    C : Set c
+
+------------------------------------------------------------------------
+-- Definition
+
+open import Agda.Builtin.Maybe public
+  using (Maybe; just; nothing)
+
+------------------------------------------------------------------------
+-- Some operations
+
+boolToMaybe : Bool → Maybe ⊤
+boolToMaybe true  = just _
+boolToMaybe false = nothing
+
+is-just : Maybe A → Bool
+is-just (just _) = true
+is-just nothing  = false
+
+is-nothing : Maybe A → Bool
+is-nothing = not ∘ is-just
+
+decToMaybe : Dec A → Maybe A
+decToMaybe ( true because [a]) = just (invert [a])
+decToMaybe (false because  _ ) = nothing
+
+-- A dependent eliminator.
+
+maybe : ∀ {A : Set a} {B : Maybe A → Set b} →
+        ((x : A) → B (just x)) → B nothing → (x : Maybe A) → B x
+maybe j n (just x) = j x
+maybe j n nothing  = n
+
+-- A non-dependent eliminator.
+
+maybe′ : (A → B) → B → Maybe A → B
+maybe′ = maybe
+
+-- A defaulting mechanism
+
+fromMaybe : A → Maybe A → A
+fromMaybe = maybe′ id
+
+-- A safe variant of "fromJust". If the value is nothing, then the
+-- return type is the unit type.
+
+module _ {a} {A : Set a} where
+
+  From-just : Maybe A → Set a
+  From-just (just _) = A
+  From-just nothing  = Lift a ⊤
+
+  from-just : (x : Maybe A) → From-just x
+  from-just (just x) = x
+  from-just nothing  = _
+
+-- Functoriality: map
+
+map : (A → B) → Maybe A → Maybe B
+map f = maybe (just ∘ f) nothing
+
+-- Applicative: ap
+
+ap : Maybe (A → B) → Maybe A → Maybe B
+ap nothing  = const nothing
+ap (just f) = map f
+
+-- Monad: bind
+
+infixl 1 _>>=_
+_>>=_ : Maybe A → (A → Maybe B) → Maybe B
+nothing >>= f = nothing
+just a  >>= f = f a
+
+-- Alternative: <∣>
+
+_<∣>_ : Maybe A → Maybe A → Maybe A
+just x  <∣> my = just x
+nothing <∣> my = my
+
+-- Just when the boolean is true
+
+when : Bool → A → Maybe A
+when b c = map (const c) (boolToMaybe b)
+
+------------------------------------------------------------------------
+-- Aligning and zipping
+
+alignWith : (These A B → C) → Maybe A → Maybe B → Maybe C
+alignWith f (just a) (just b) = just (f (these a b))
+alignWith f (just a) nothing  = just (f (this a))
+alignWith f nothing  (just b) = just (f (that b))
+alignWith f nothing  nothing  = nothing
+
+zipWith : (A → B → C) → Maybe A → Maybe B → Maybe C
+zipWith f (just a) (just b) = just (f a b)
+zipWith _ _        _        = nothing
+
+align : Maybe A → Maybe B → Maybe (These A B)
+align = alignWith id
+
+zip : Maybe A → Maybe B → Maybe (A × B)
+zip = zipWith _,_
+
+------------------------------------------------------------------------
+-- Injections.
+
+thisM : A → Maybe B → These A B
+thisM a = maybe′ (these a) (this a)
+
+thatM : Maybe A → B → These A B
+thatM = maybe′ these that
+
\ No newline at end of file diff --git a/misc/Data.Product.html b/misc/Data.Product.html new file mode 100644 index 0000000..cc3b755 --- /dev/null +++ b/misc/Data.Product.html @@ -0,0 +1,208 @@ + +Data.Product
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Products
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Product where
+
+open import Function.Base
+open import Level
+open import Relation.Nullary
+open import Agda.Builtin.Equality
+
+private
+  variable
+    a b c d e f ℓ p q r : Level
+    A : Set a
+    B : Set b
+    C : Set c
+    D : Set d
+    E : Set e
+    F : Set f
+
+------------------------------------------------------------------------
+-- Definition of dependent products
+
+open import Agda.Builtin.Sigma public
+  renaming (fst to proj₁; snd to proj₂)
+  hiding (module Σ)
+
+module Σ = Agda.Builtin.Sigma.Σ
+  renaming (fst to proj₁; snd to proj₂)
+
+-- The syntax declaration below is attached to Σ-syntax, to make it
+-- easy to import Σ without the special syntax.
+
+infix 2 Σ-syntax
+
+Σ-syntax : (A : Set a) → (A → Set b) → Set (a ⊔ b)
+Σ-syntax = Σ
+
+syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B
+
+------------------------------------------------------------------------
+-- Definition of non-dependent products
+
+infixr 4 _,′_
+infixr 2 _×_
+
+_×_ : ∀ (A : Set a) (B : Set b) → Set (a ⊔ b)
+A × B = Σ[ x ∈ A ] B
+
+_,′_ : A → B → A × B
+_,′_ = _,_
+
+------------------------------------------------------------------------
+-- Existential quantifiers
+
+∃ : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
+∃ = Σ _
+
+∄ : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
+∄ P = ¬ ∃ P
+
+∃₂ : ∀ {A : Set a} {B : A → Set b}
+     (C : (x : A) → B x → Set c) → Set (a ⊔ b ⊔ c)
+∃₂ C = ∃ λ a → ∃ λ b → C a b
+
+-- Unique existence (parametrised by an underlying equality).
+
+∃! : {A : Set a} → (A → A → Set ℓ) → (A → Set b) → Set (a ⊔ b ⊔ ℓ)
+∃! _≈_ B = ∃ λ x → B x × (∀ {y} → B y → x ≈ y)
+
+-- Syntax
+
+infix 2 ∃-syntax
+
+∃-syntax : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
+∃-syntax = ∃
+
+syntax ∃-syntax (λ x → B) = ∃[ x ] B
+
+infix 2 ∄-syntax
+
+∄-syntax : ∀ {A : Set a} → (A → Set b) → Set (a ⊔ b)
+∄-syntax = ∄
+
+syntax ∄-syntax (λ x → B) = ∄[ x ] B
+
+------------------------------------------------------------------------
+-- Operations over dependent products
+
+infix  4 -,_
+infixr 2 _-×-_ _-,-_
+infixl 2 _<*>_
+
+-- Sometimes the first component can be inferred.
+
+-,_ : ∀ {A : Set a} {B : A → Set b} {x} → B x → ∃ B
+-, y = _ , y
+
+<_,_> : ∀ {A : Set a} {B : A → Set b} {C : ∀ {x} → B x → Set c}
+        (f : (x : A) → B x) → ((x : A) → C (f x)) →
+        ((x : A) → Σ (B x) C)
+< f , g > x = (f x , g x)
+
+map : ∀ {P : A → Set p} {Q : B → Set q} →
+      (f : A → B) → (∀ {x} → P x → Q (f x)) →
+      Σ A P → Σ B Q
+map f g (x , y) = (f x , g y)
+
+map₁ : (A → B) → A × C → B × C
+map₁ f = map f id
+
+map₂ : ∀ {A : Set a} {B : A → Set b} {C : A → Set c} →
+       (∀ {x} → B x → C x) → Σ A B → Σ A C
+map₂ f = map id f
+
+-- A version of map where the output can depend on the input
+dmap : ∀ {B : A → Set b} {P : A → Set p} {Q : ∀ {a} → P a → B a → Set q} →
+       (f : (a : A) → B a) → (∀ {a} (b : P a) → Q b (f a)) →
+       ((a , b) : Σ A P) → Σ (B a) (Q b)
+dmap f g (x , y) = f x , g y
+
+zip : ∀ {P : A → Set p} {Q : B → Set q} {R : C → Set r} →
+      (_∙_ : A → B → C) →
+      (∀ {x y} → P x → Q y → R (x ∙ y)) →
+      Σ A P → Σ B Q → Σ C R
+zip _∙_ _∘_ (a , p) (b , q) = ((a ∙ b) , (p ∘ q))
+
+curry : ∀ {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
+        ((p : Σ A B) → C p) →
+        ((x : A) → (y : B x) → C (x , y))
+curry f x y = f (x , y)
+
+uncurry : ∀ {A : Set a} {B : A → Set b} {C : Σ A B → Set c} →
+          ((x : A) → (y : B x) → C (x , y)) →
+          ((p : Σ A B) → C p)
+uncurry f (x , y) = f x y
+
+-- Rewriting dependent products
+assocʳ : {B : A → Set b} {C : (a : A) → B a → Set c} →
+          Σ (Σ A B) (uncurry C) → Σ A (λ a → Σ (B a) (C a))
+assocʳ ((a , b) , c) = (a , (b , c))
+
+assocˡ : {B : A → Set b} {C : (a : A) → B a → Set c} →
+          Σ A (λ a → Σ (B a) (C a)) → Σ (Σ A B) (uncurry C)
+assocˡ (a , (b , c)) = ((a , b) , c)
+
+-- Alternate form of associativity for dependent products
+-- where the C parameter is uncurried.
+assocʳ-curried : {B : A → Set b} {C : Σ A B → Set c} →
+                 Σ (Σ A B) C → Σ A (λ a → Σ (B a) (curry C a))
+assocʳ-curried ((a , b) , c) = (a , (b , c))
+
+assocˡ-curried : {B : A → Set b} {C : Σ A B → Set c} →
+          Σ A (λ a → Σ (B a) (curry C a)) → Σ (Σ A B) C
+assocˡ-curried (a , (b , c)) = ((a , b) , c)
+
+------------------------------------------------------------------------
+-- Operations for non-dependent products
+
+-- Any of the above operations for dependent products will also work for
+-- non-dependent products but sometimes Agda has difficulty inferring
+-- the non-dependency. Primed (′ = \prime) versions of the operations
+-- are therefore provided below that sometimes have better inference
+-- properties.
+
+zip′ : (A → B → C) → (D → E → F) → A × D → B × E → C × F
+zip′ f g = zip f g
+
+curry′ : (A × B → C) → (A → B → C)
+curry′ = curry
+
+uncurry′ : (A → B → C) → (A × B → C)
+uncurry′ = uncurry
+
+dmap′ : ∀ {x y} {X : A → Set x} {Y : B → Set y} →
+        ((a : A) → X a) → ((b : B) → Y b) →
+        ((a , b) : A × B) → X a × Y b
+dmap′ f g = dmap f g
+
+_<*>_ : ∀ {x y} {X : A → Set x} {Y : B → Set y} →
+        ((a : A) → X a) × ((b : B) → Y b) →
+        ((a , b) : A × B) → X a × Y b
+_<*>_ = uncurry dmap′
+
+-- Operations that can only be defined for non-dependent products
+
+swap : A × B → B × A
+swap (x , y) = (y , x)
+
+_-×-_ : (A → B → Set p) → (A → B → Set q) → (A → B → Set _)
+f -×- g = f -⟪ _×_ ⟫- g
+
+_-,-_ : (A → B → C) → (A → B → D) → (A → B → C × D)
+f -,- g = f -⟪ _,_ ⟫- g
+
+-- Rewriting non-dependent products
+assocʳ′ : (A × B) × C → A × (B × C)
+assocʳ′ ((a , b) , c) = (a , (b , c))
+
+assocˡ′ : A × (B × C) → (A × B) × C
+assocˡ′ (a , (b , c)) = ((a , b) , c)
+
\ No newline at end of file diff --git a/misc/Data.Sum.Base.html b/misc/Data.Sum.Base.html new file mode 100644 index 0000000..11acc8f --- /dev/null +++ b/misc/Data.Sum.Base.html @@ -0,0 +1,88 @@ + +Data.Sum.Base
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Sums (disjoint unions)
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Sum.Base where
+
+open import Data.Bool.Base using (true; false)
+open import Function.Base using (_∘_; _∘′_; _-⟪_⟫-_ ; id)
+open import Relation.Nullary.Reflects using (invert)
+open import Relation.Nullary using (Dec; yes; no; _because_; ¬_)
+open import Level using (Level; _⊔_)
+
+private
+  variable
+    a b c d : Level
+    A : Set a
+    B : Set b
+    C : Set c
+    D : Set d
+
+------------------------------------------------------------------------
+-- Definition
+
+infixr 1 _⊎_
+
+data _⊎_ (A : Set a) (B : Set b) : Set (a ⊔ b) where
+  inj₁ : (x : A) → A ⊎ B
+  inj₂ : (y : B) → A ⊎ B
+
+------------------------------------------------------------------------
+-- Functions
+
+[_,_] : ∀ {C : A ⊎ B → Set c} →
+        ((x : A) → C (inj₁ x)) → ((x : B) → C (inj₂ x)) →
+        ((x : A ⊎ B) → C x)
+[ f , g ] (inj₁ x) = f x
+[ f , g ] (inj₂ y) = g y
+
+[_,_]′ : (A → C) → (B → C) → (A ⊎ B → C)
+[_,_]′ = [_,_]
+
+fromInj₁ : (B → A) → A ⊎ B → A
+fromInj₁ = [ id ,_]′
+
+fromInj₂ : (A → B) → A ⊎ B → B
+fromInj₂ = [_, id ]′
+
+reduce : A ⊎ A → A
+reduce = [ id , id ]′
+
+swap : A ⊎ B → B ⊎ A
+swap (inj₁ x) = inj₂ x
+swap (inj₂ x) = inj₁ x
+
+map : (A → C) → (B → D) → (A ⊎ B → C ⊎ D)
+map f g = [ inj₁ ∘ f , inj₂ ∘ g ]′
+
+map₁ : (A → C) → (A ⊎ B → C ⊎ B)
+map₁ f = map f id
+
+map₂ : (B → D) → (A ⊎ B → A ⊎ D)
+map₂ = map id
+
+assocʳ : (A ⊎ B) ⊎ C → A ⊎ B ⊎ C
+assocʳ = [ map₂ inj₁ , inj₂ ∘′ inj₂ ]′
+
+assocˡ : A ⊎ B ⊎ C → (A ⊎ B) ⊎ C
+assocˡ = [ inj₁ ∘′ inj₁ , map₁ inj₂ ]′
+
+infixr 1 _-⊎-_
+_-⊎-_ : (A → B → Set c) → (A → B → Set d) → (A → B → Set (c ⊔ d))
+f -⊎- g = f -⟪ _⊎_ ⟫- g
+
+-- Conversion back and forth with Dec
+
+fromDec : Dec A → A ⊎ ¬ A
+fromDec ( true because  [p]) = inj₁ (invert  [p])
+fromDec (false because [¬p]) = inj₂ (invert [¬p])
+
+toDec : A ⊎ ¬ A → Dec A
+toDec (inj₁ p)  = yes p
+toDec (inj₂ ¬p) = no ¬p
+
\ No newline at end of file diff --git a/misc/Data.These.Base.html b/misc/Data.These.Base.html new file mode 100644 index 0000000..a5493fa --- /dev/null +++ b/misc/Data.These.Base.html @@ -0,0 +1,82 @@ + +Data.These.Base
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- An either-or-both data type, basic type and operations
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.These.Base where
+
+open import Level
+open import Data.Sum.Base using (_⊎_; [_,_]′)
+open import Function.Base
+
+private
+  variable
+    a b c d e f : Level
+    A : Set a
+    B : Set b
+    C : Set c
+    D : Set d
+    E : Set e
+    F : Set f
+
+data These {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
+  this  : A     → These A B
+  that  :     B → These A B
+  these : A → B → These A B
+
+------------------------------------------------------------------------
+-- Operations
+
+-- injection
+
+fromSum : A ⊎ B → These A B
+fromSum = [ this , that ]′
+
+-- map
+
+map : (f : A → B) (g : C → D) → These A C → These B D
+map f g (this a)    = this (f a)
+map f g (that b)    = that (g b)
+map f g (these a b) = these (f a) (g b)
+
+map₁ : (f : A → B) → These A C → These B C
+map₁ f = map f id
+
+map₂ : (g : B → C) → These A B → These A C
+map₂ = map id
+
+-- fold
+
+fold : (A → C) → (B → C) → (A → B → C) → These A B → C
+fold l r lr (this a)    = l a
+fold l r lr (that b)    = r b
+fold l r lr (these a b) = lr a b
+
+foldWithDefaults : A → B → (A → B → C) → These A B → C
+foldWithDefaults a b lr = fold (flip lr b) (lr a) lr
+
+-- swap
+
+swap : These A B → These B A
+swap = fold that this (flip these)
+
+-- align
+
+alignWith : (These A C → E) → (These B D → F) → These A B → These C D → These E F
+alignWith f g (this a)    (this c)    = this (f (these a c))
+alignWith f g (this a)    (that d)    = these (f (this a)) (g (that d))
+alignWith f g (this a)    (these c d) = these (f (these a c)) (g (that d))
+alignWith f g (that b)    (this c)    = these (f (that c)) (g (this b))
+alignWith f g (that b)    (that d)    = that (g (these b d))
+alignWith f g (that b)    (these c d) = these (f (that c)) (g (these b d))
+alignWith f g (these a b) (this c)    = these (f (these a c)) (g (this b))
+alignWith f g (these a b) (that d)    = these (f (this a)) (g (these b d))
+alignWith f g (these a b) (these c d) = these (f (these a c)) (g (these b d))
+
+align : These A B → These C D → These (These A C) (These B D)
+align = alignWith id id
+
\ No newline at end of file diff --git a/misc/Data.Unit.Base.html b/misc/Data.Unit.Base.html new file mode 100644 index 0000000..ecf680d --- /dev/null +++ b/misc/Data.Unit.Base.html @@ -0,0 +1,39 @@ + +Data.Unit.Base
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The unit type and the total relation on unit
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Agda.Builtin.Equality using (_≡_)
+
+module Data.Unit.Base where
+
+------------------------------------------------------------------------
+-- A unit type defined as a record type
+
+-- Note that by default the unit type is not universe polymorphic as it
+-- often results in unsolved metas. See `Data.Unit.Polymorphic` for a
+-- universe polymorphic variant.
+
+-- Note also that the name of this type is "\top", not T.
+
+open import Agda.Builtin.Unit public
+  using (⊤; tt)
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 1.2
+
+record _≤_ (x y : ⊤) : Set where
+{-# WARNING_ON_USAGE _≤_
+"Warning: _≤_ was deprecated in v1.2.
+Please use _≡_ from Relation.Binary.PropositionalEquality instead."
+#-}
+
\ No newline at end of file diff --git a/misc/Function.Base.html b/misc/Function.Base.html new file mode 100644 index 0000000..9833d5b --- /dev/null +++ b/misc/Function.Base.html @@ -0,0 +1,259 @@ + +Function.Base
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Simple combinators working solely on and with functions
+------------------------------------------------------------------------
+
+-- The contents of this file can be accessed from `Function`.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Function.Base where
+
+open import Level
+open import Strict
+
+private
+  variable
+    a b c d e : Level
+    A : Set a
+    B : Set b
+    C : Set c
+    D : Set d
+    E : Set e
+
+------------------------------------------------------------------------
+-- Some simple functions
+
+id : A → A
+id x = x
+
+const : A → B → A
+const x = λ _ → x
+
+constᵣ : A → B → B
+constᵣ _ = id
+
+------------------------------------------------------------------------
+-- Operations on dependent functions
+
+-- These are functions whose output has a type that depends on the
+-- value of the input to the function.
+
+infixr 9 _∘_ _∘₂_
+infixl 8 _ˢ_
+infixl 0 _|>_
+infix  0 case_return_of_
+infixr -1 _$_ _$!_
+
+-- Composition
+
+_∘_ : ∀ {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
+      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
+      ((x : A) → C (g x))
+f ∘ g = λ x → f (g x)
+{-# INLINE _∘_ #-}
+
+_∘₂_ : ∀ {A₁ : Set a} {A₂ : A₁ → Set d}
+         {B : (x : A₁) → A₂ x → Set b}
+         {C : {x : A₁} → {y : A₂ x} → B x y → Set c} →
+       ({x : A₁} → {y : A₂ x} → (z : B x y) → C z) →
+       (g : (x : A₁) → (y : A₂ x) → B x y) →
+       ((x : A₁) → (y : A₂ x) → C (g x y))
+f ∘₂ g = λ x y → f (g x y)
+
+-- Flipping order of arguments
+
+flip : ∀ {A : Set a} {B : Set b} {C : A → B → Set c} →
+       ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
+flip f = λ y x → f x y
+{-# INLINE flip #-}
+
+-- Application - note that _$_ is right associative, as in Haskell.
+-- If you want a left associative infix application operator, use
+-- Category.Functor._<$>_ from Category.Monad.Identity.IdentityMonad.
+
+_$_ : ∀ {A : Set a} {B : A → Set b} →
+      ((x : A) → B x) → ((x : A) → B x)
+f $ x = f x
+{-# INLINE _$_ #-}
+
+-- Strict (call-by-value) application
+
+_$!_ : ∀ {A : Set a} {B : A → Set b} →
+       ((x : A) → B x) → ((x : A) → B x)
+_$!_ = flip force
+
+-- Flipped application (aka pipe-forward)
+
+_|>_ : ∀ {A : Set a} {B : A → Set b} →
+       (a : A) → (∀ a → B a) → B a
+_|>_ = flip _$_
+{-# INLINE _|>_ #-}
+
+-- The S combinator - written infix as in Conor McBride's paper
+-- "Outrageous but Meaningful Coincidences: Dependent type-safe syntax
+-- and evaluation".
+
+_ˢ_ : ∀ {A : Set a} {B : A → Set b} {C : (x : A) → B x → Set c} →
+      ((x : A) (y : B x) → C x y) →
+      (g : (x : A) → B x) →
+      ((x : A) → C x (g x))
+f ˢ g = λ x → f x (g x)
+{-# INLINE _ˢ_ #-}
+
+-- Converting between implicit and explicit function spaces.
+
+_$- : ∀ {A : Set a} {B : A → Set b} → ((x : A) → B x) → ({x : A} → B x)
+f $- = f _
+{-# INLINE _$- #-}
+
+λ- : ∀ {A : Set a} {B : A → Set b} → ({x : A} → B x) → ((x : A) → B x)
+λ- f = λ x → f
+{-# INLINE λ- #-}
+
+-- Case expressions (to be used with pattern-matching lambdas, see
+-- README.Case).
+
+case_return_of_ : ∀ {A : Set a} (x : A) (B : A → Set b) →
+                  ((x : A) → B x) → B x
+case x return B of f = f x
+{-# INLINE case_return_of_ #-}
+
+------------------------------------------------------------------------
+-- Non-dependent versions of dependent operations
+
+-- Any of the above operations for dependent functions will also work
+-- for non-dependent functions but sometimes Agda has difficulty
+-- inferring the non-dependency. Primed (′ = \prime) versions of the
+-- operations are therefore provided below that sometimes have better
+-- inference properties.
+
+infixr 9 _∘′_ _∘₂′_
+infixl 0 _|>′_
+infix  0 case_of_
+infixr -1 _$′_ _$!′_
+
+-- Composition
+
+_∘′_ : (B → C) → (A → B) → (A → C)
+f ∘′ g = _∘_ f g
+
+_∘₂′_ : (C → D) → (A → B → C) → (A → B → D)
+f ∘₂′ g = _∘₂_ f g
+
+-- Application
+
+_$′_ : (A → B) → (A → B)
+_$′_ = _$_
+
+-- Strict (call-by-value) application
+
+_$!′_ : (A → B) → (A → B)
+_$!′_ = _$!_
+
+-- Flipped application (aka pipe-forward)
+
+_|>′_ : A → (A → B) → B
+_|>′_ = _|>_
+
+-- Case expressions (to be used with pattern-matching lambdas, see
+-- README.Case).
+
+case_of_ : A → (A → B) → B
+case x of f = case x return _ of f
+{-# INLINE case_of_ #-}
+
+------------------------------------------------------------------------
+-- Operations that are only defined for non-dependent functions
+
+infixl 1 _⟨_⟩_
+infixl 0 _∋_
+
+-- Binary application
+
+_⟨_⟩_ : A → (A → B → C) → B → C
+x ⟨ f ⟩ y = f x y
+
+-- In Agda you cannot annotate every subexpression with a type
+-- signature. This function can be used instead.
+
+_∋_ : (A : Set a) → A → A
+A ∋ x = x
+
+-- Conversely it is sometimes useful to be able to extract the
+-- type of a given expression.
+
+typeOf : {A : Set a} → A → Set a
+typeOf {A = A} _ = A
+
+-- Construct an element of the given type by instance search.
+
+it : {A : Set a} → {{A}} → A
+it {{x}} = x
+
+------------------------------------------------------------------------
+-- Composition of a binary function with other functions
+
+infixr 0 _-⟪_⟫-_ _-⟨_⟫-_
+infixl 0 _-⟪_⟩-_
+infixr 1 _-⟨_⟩-_ ∣_⟫-_ ∣_⟩-_
+infixl 1 _on_ _on₂_ _-⟪_∣ _-⟨_∣
+
+-- Two binary functions
+
+_-⟪_⟫-_ : (A → B → C) → (C → D → E) → (A → B → D) → (A → B → E)
+f -⟪ _*_ ⟫- g = λ x y → f x y * g x y
+
+-- A single binary function on the left
+
+_-⟪_∣ : (A → B → C) → (C → B → D) → (A → B → D)
+f -⟪ _*_ ∣ = f -⟪ _*_ ⟫- constᵣ
+
+-- A single binary function on the right
+
+∣_⟫-_ : (A → C → D) → (A → B → C) → (A → B → D)
+∣ _*_ ⟫- g = const -⟪ _*_ ⟫- g
+
+-- A single unary function on the left
+
+_-⟨_∣ : (A → C) → (C → B → D) → (A → B → D)
+f -⟨ _*_ ∣ = f ∘₂ const -⟪ _*_ ∣
+
+-- A single unary function on the right
+
+∣_⟩-_ : (A → C → D) → (B → C) → (A → B → D)
+∣ _*_ ⟩- g = ∣ _*_ ⟫- g ∘₂ constᵣ
+
+-- A binary function and a unary function
+
+_-⟪_⟩-_ : (A → B → C) → (C → D → E) → (B → D) → (A → B → E)
+f -⟪ _*_ ⟩- g = f -⟪ _*_ ⟫- ∣ constᵣ ⟩- g
+
+-- A unary function and a binary function
+
+_-⟨_⟫-_ : (A → C) → (C → D → E) → (A → B → D) → (A → B → E)
+f -⟨ _*_ ⟫- g = f -⟨ const ∣ -⟪ _*_ ⟫- g
+
+-- Two unary functions
+
+_-⟨_⟩-_ : (A → C) → (C → D → E) → (B → D) → (A → B → E)
+f -⟨ _*_ ⟩- g = f -⟨ const ∣ -⟪ _*_ ⟫- ∣ constᵣ ⟩- g
+
+-- A single binary function on both sides
+
+_on₂_ : (C → C → D) → (A → B → C) → (A → B → D)
+_*_ on₂ f = f -⟪ _*_ ⟫- f
+
+-- A single unary function on both sides
+
+_on_ : (B → B → C) → (A → B) → (A → A → C)
+_*_ on f = f -⟨ _*_ ⟩- f
+
+_-[_]-_ = _-⟪_⟫-_
+{-# WARNING_ON_USAGE _-[_]-_
+"Warning: Function._-[_]-_ was deprecated in v1.4.
+Please use _-⟪_⟫-_ instead."
+#-}
+
\ No newline at end of file diff --git a/misc/Function.Bundles.html b/misc/Function.Bundles.html new file mode 100644 index 0000000..56184b7 --- /dev/null +++ b/misc/Function.Bundles.html @@ -0,0 +1,424 @@ + +Function.Bundles
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Bundles for types of functions
+------------------------------------------------------------------------
+
+-- The contents of this file should usually be accessed from `Function`.
+
+-- Note that these bundles differ from those found elsewhere in other
+-- library hierarchies as they take Setoids as parameters. This is
+-- because a function is of no use without knowing what its domain and
+-- codomain is, as well which equalities are being considered over them.
+-- One consequence of this is that they are not built from the
+-- definitions found in `Function.Structures` as is usually the case in
+-- other library hierarchies, as this would duplicate the equality
+-- axioms.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Function.Bundles where
+
+import Function.Definitions as FunctionDefinitions
+import Function.Structures as FunctionStructures
+open import Level using (Level; _⊔_; suc)
+open import Data.Product using (_,_; proj₁; proj₂)
+open import Relation.Binary hiding (_⇔_)
+open import Relation.Binary.PropositionalEquality as ≡
+  using (_≡_)
+open Setoid using (isEquivalence)
+
+private
+  variable
+    a b ℓ₁ ℓ₂ : Level
+
+------------------------------------------------------------------------
+-- Setoid bundles
+------------------------------------------------------------------------
+
+module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where
+
+  open Setoid From using () renaming (Carrier to A; _≈_ to _≈₁_)
+  open Setoid To   using () renaming (Carrier to B; _≈_ to _≈₂_)
+  open FunctionDefinitions _≈₁_ _≈₂_
+  open FunctionStructures  _≈₁_ _≈₂_
+
+------------------------------------------------------------------------
+-- Bundles with one element
+
+  -- Called `Func` rather than `Function` in order to avoid clashing
+  -- with the top-level module.
+  record Func : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      f    : A → B
+      cong : f Preserves _≈₁_ ⟶ _≈₂_
+
+    isCongruent : IsCongruent f
+    isCongruent = record
+      { cong           = cong
+      ; isEquivalence₁ = isEquivalence From
+      ; isEquivalence₂ = isEquivalence To
+      }
+
+    open IsCongruent isCongruent public
+      using (module Eq₁; module Eq₂)
+
+
+  record Injection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      f           : A → B
+      cong        : f Preserves _≈₁_ ⟶ _≈₂_
+      injective   : Injective f
+
+    function : Func
+    function = record
+      { f    = f
+      ; cong = cong
+      }
+
+    open Func function public
+      hiding (f; cong)
+
+    isInjection : IsInjection f
+    isInjection = record
+      { isCongruent = isCongruent
+      ; injective   = injective
+      }
+
+
+  record Surjection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      f          : A → B
+      cong       : f Preserves _≈₁_ ⟶ _≈₂_
+      surjective : Surjective f
+
+    isCongruent : IsCongruent f
+    isCongruent = record
+      { cong           = cong
+      ; isEquivalence₁ = isEquivalence From
+      ; isEquivalence₂ = isEquivalence To
+      }
+
+    open IsCongruent isCongruent public using (module Eq₁; module Eq₂)
+
+    isSurjection : IsSurjection f
+    isSurjection = record
+      { isCongruent = isCongruent
+      ; surjective  = surjective
+      }
+
+
+  record Bijection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      f         : A → B
+      cong      : f Preserves _≈₁_ ⟶ _≈₂_
+      bijective : Bijective f
+
+    injective : Injective f
+    injective = proj₁ bijective
+
+    surjective : Surjective f
+    surjective = proj₂ bijective
+
+    injection : Injection
+    injection = record
+      { cong      = cong
+      ; injective = injective
+      }
+
+    surjection : Surjection
+    surjection = record
+      { cong       = cong
+      ; surjective = surjective
+      }
+
+    open Injection  injection  public using (isInjection)
+    open Surjection surjection public using (isSurjection)
+
+    isBijection : IsBijection f
+    isBijection = record
+      { isInjection = isInjection
+      ; surjective  = surjective
+      }
+
+    open IsBijection isBijection public using (module Eq₁; module Eq₂)
+
+
+------------------------------------------------------------------------
+-- Bundles with two elements
+
+  record Equivalence : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      f     : A → B
+      g     : B → A
+      cong₁ : f Preserves _≈₁_ ⟶ _≈₂_
+      cong₂ : g Preserves _≈₂_ ⟶ _≈₁_
+
+
+  record LeftInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      f         : A → B
+      g         : B → A
+      cong₁     : f Preserves _≈₁_ ⟶ _≈₂_
+      cong₂     : g Preserves _≈₂_ ⟶ _≈₁_
+      inverseˡ  : Inverseˡ f g
+
+    isCongruent : IsCongruent f
+    isCongruent = record
+      { cong           = cong₁
+      ; isEquivalence₁ = isEquivalence From
+      ; isEquivalence₂ = isEquivalence To
+      }
+
+    open IsCongruent isCongruent public using (module Eq₁; module Eq₂)
+
+    isLeftInverse : IsLeftInverse f g
+    isLeftInverse = record
+      { isCongruent = isCongruent
+      ; cong₂       = cong₂
+      ; inverseˡ    = inverseˡ
+      }
+
+    equivalence : Equivalence
+    equivalence = record
+      { cong₁ = cong₁
+      ; cong₂ = cong₂
+      }
+
+
+  record RightInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      f         : A → B
+      g         : B → A
+      cong₁     : f Preserves _≈₁_ ⟶ _≈₂_
+      cong₂     : g Preserves _≈₂_ ⟶ _≈₁_
+      inverseʳ  : Inverseʳ f g
+
+    isCongruent : IsCongruent f
+    isCongruent = record
+      { cong           = cong₁
+      ; isEquivalence₁ = isEquivalence From
+      ; isEquivalence₂ = isEquivalence To
+      }
+
+    isRightInverse : IsRightInverse f g
+    isRightInverse = record
+      { isCongruent = isCongruent
+      ; cong₂       = cong₂
+      ; inverseʳ    = inverseʳ
+      }
+
+    equivalence : Equivalence
+    equivalence = record
+      { cong₁ = cong₁
+      ; cong₂ = cong₂
+      }
+
+
+  record Inverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      f         : A → B
+      f⁻¹       : B → A
+      cong₁     : f Preserves _≈₁_ ⟶ _≈₂_
+      cong₂     : f⁻¹ Preserves _≈₂_ ⟶ _≈₁_
+      inverse   : Inverseᵇ f f⁻¹
+
+    inverseˡ : Inverseˡ f f⁻¹
+    inverseˡ = proj₁ inverse
+
+    inverseʳ : Inverseʳ f f⁻¹
+    inverseʳ = proj₂ inverse
+
+    leftInverse : LeftInverse
+    leftInverse = record
+      { cong₁    = cong₁
+      ; cong₂    = cong₂
+      ; inverseˡ = inverseˡ
+      }
+
+    rightInverse : RightInverse
+    rightInverse = record
+      { cong₁    = cong₁
+      ; cong₂    = cong₂
+      ; inverseʳ = inverseʳ
+      }
+
+    open LeftInverse leftInverse   public using (isLeftInverse)
+    open RightInverse rightInverse public using (isRightInverse)
+
+    isInverse : IsInverse f f⁻¹
+    isInverse = record
+      { isLeftInverse = isLeftInverse
+      ; inverseʳ      = inverseʳ
+      }
+
+    open IsInverse isInverse public using (module Eq₁; module Eq₂)
+
+
+------------------------------------------------------------------------
+-- Bundles with three elements
+
+  record BiEquivalence : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      f     : A → B
+      g₁    : B → A
+      g₂    : B → A
+      cong₁ : f Preserves _≈₁_ ⟶ _≈₂_
+      cong₂ : g₁ Preserves _≈₂_ ⟶ _≈₁_
+      cong₃ : g₂ Preserves _≈₂_ ⟶ _≈₁_
+
+
+  record BiInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+    field
+      f         : A → B
+      g₁        : B → A
+      g₂        : B → A
+      cong₁     : f Preserves _≈₁_ ⟶ _≈₂_
+      cong₂     : g₁ Preserves _≈₂_ ⟶ _≈₁_
+      cong₃     : g₂ Preserves _≈₂_ ⟶ _≈₁_
+      inverseˡ  : Inverseˡ f g₁
+      inverseʳ  : Inverseʳ f g₂
+
+    f-isCongruent : IsCongruent f
+    f-isCongruent = record
+      { cong           = cong₁
+      ; isEquivalence₁ = isEquivalence From
+      ; isEquivalence₂ = isEquivalence To
+      }
+
+    isBiInverse : IsBiInverse f g₁ g₂
+    isBiInverse = record
+      { f-isCongruent = f-isCongruent
+      ; cong₂         = cong₂
+      ; inverseˡ      = inverseˡ
+      ; cong₃         = cong₃
+      ; inverseʳ      = inverseʳ
+      }
+
+    biEquivalence : BiEquivalence
+    biEquivalence = record
+      { cong₁ = cong₁
+      ; cong₂ = cong₂
+      ; cong₃ = cong₃
+      }
+
+
+------------------------------------------------------------------------
+-- Bundles specialised for propositional equality
+------------------------------------------------------------------------
+
+infix 3 _⟶_ _↣_ _↠_ _⤖_ _⇔_ _↩_ _↪_ _↩↪_ _↔_
+_⟶_ : Set a → Set b → Set _
+A ⟶ B = Func (≡.setoid A) (≡.setoid B)
+
+_↣_ : Set a → Set b → Set _
+A ↣ B = Injection (≡.setoid A) (≡.setoid B)
+
+_↠_ : Set a → Set b → Set _
+A ↠ B = Surjection (≡.setoid A) (≡.setoid B)
+
+_⤖_ : Set a → Set b → Set _
+A ⤖ B = Bijection (≡.setoid A) (≡.setoid B)
+
+_⇔_ : Set a → Set b → Set _
+A ⇔ B = Equivalence (≡.setoid A) (≡.setoid B)
+
+_↩_ : Set a → Set b → Set _
+A ↩ B = LeftInverse (≡.setoid A) (≡.setoid B)
+
+_↪_ : Set a → Set b → Set _
+A ↪ B = RightInverse (≡.setoid A) (≡.setoid B)
+
+_↩↪_ : Set a → Set b → Set _
+A ↩↪ B = BiInverse (≡.setoid A) (≡.setoid B)
+
+_↔_ : Set a → Set b → Set _
+A ↔ B = Inverse (≡.setoid A) (≡.setoid B)
+
+-- We now define some constructors for the above that
+-- automatically provide the required congruency proofs.
+
+module _ {A : Set a} {B : Set b} where
+
+  open FunctionDefinitions {A = A} {B} _≡_ _≡_
+
+  mk⟶ : (A → B) → A ⟶ B
+  mk⟶ f = record
+    { f         = f
+    ; cong      = ≡.cong f
+    }
+
+  mk↣ : ∀ {f : A → B} → Injective f → A ↣ B
+  mk↣ {f} inj = record
+    { f         = f
+    ; cong      = ≡.cong f
+    ; injective = inj
+    }
+
+  mk↠ : ∀ {f : A → B} → Surjective f → A ↠ B
+  mk↠ {f} surj = record
+    { f          = f
+    ; cong       = ≡.cong f
+    ; surjective = surj
+    }
+
+  mk⤖ : ∀ {f : A → B} → Bijective f → A ⤖ B
+  mk⤖ {f} bij = record
+    { f         = f
+    ; cong      = ≡.cong f
+    ; bijective = bij
+    }
+
+  mk⇔ : ∀ (f : A → B) (g : B → A) → A ⇔ B
+  mk⇔ f g = record
+    { f     = f
+    ; g     = g
+    ; cong₁ = ≡.cong f
+    ; cong₂ = ≡.cong g
+    }
+
+  mk↩ : ∀ {f : A → B} {g : B → A} → Inverseˡ f g → A ↩ B
+  mk↩ {f} {g} invˡ = record
+    { f        = f
+    ; g        = g
+    ; cong₁    = ≡.cong f
+    ; cong₂    = ≡.cong g
+    ; inverseˡ = invˡ
+    }
+
+  mk↪ : ∀ {f : A → B} {g : B → A} → Inverseʳ f g → A ↪ B
+  mk↪ {f} {g} invʳ = record
+    { f        = f
+    ; g        = g
+    ; cong₁    = ≡.cong f
+    ; cong₂    = ≡.cong g
+    ; inverseʳ = invʳ
+    }
+
+  mk↩↪ : ∀ {f : A → B} {g₁ : B → A} {g₂ : B → A} →
+         Inverseˡ f g₁ → Inverseʳ f g₂ → A ↩↪ B
+  mk↩↪ {f} {g₁} {g₂} invˡ invʳ = record
+    { f        = f
+    ; g₁       = g₁
+    ; g₂       = g₂
+    ; cong₁    = ≡.cong f
+    ; cong₂    = ≡.cong g₁
+    ; cong₃    = ≡.cong g₂
+    ; inverseˡ = invˡ
+    ; inverseʳ = invʳ
+    }
+
+  mk↔ : ∀ {f : A → B} {f⁻¹ : B → A} → Inverseᵇ f f⁻¹ → A ↔ B
+  mk↔ {f} {f⁻¹} inv = record
+    { f       = f
+    ; f⁻¹     = f⁻¹
+    ; cong₁   = ≡.cong f
+    ; cong₂   = ≡.cong f⁻¹
+    ; inverse = inv
+    }
+
+  -- Sometimes the implicit arguments above cannot be inferred
+  mk↔′ : ∀ (f : A → B) (f⁻¹ : B → A) → Inverseˡ f f⁻¹ → Inverseʳ f f⁻¹ → A ↔ B
+  mk↔′ f f⁻¹ invˡ invʳ = mk↔ {f = f} {f⁻¹ = f⁻¹} (invˡ , invʳ)
+
\ No newline at end of file diff --git a/misc/Function.Core.html b/misc/Function.Core.html new file mode 100644 index 0000000..9b1afe1 --- /dev/null +++ b/misc/Function.Core.html @@ -0,0 +1,30 @@ + +Function.Core
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Core definitions for Functions
+------------------------------------------------------------------------
+
+-- The contents of this file should usually be accessed from `Function`.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Function.Core where
+
+open import Level using (_⊔_)
+
+------------------------------------------------------------------------
+-- Types
+
+Fun₁ : ∀ {a} → Set a → Set a
+Fun₁ A = A → A
+
+Fun₂ : ∀ {a} → Set a → Set a
+Fun₂ A = A → A → A
+
+------------------------------------------------------------------------
+-- Morphism
+
+Morphism : ∀ {a} → ∀ {b} → Set a → Set b → Set (a ⊔ b)
+Morphism A B = A → B
+
\ No newline at end of file diff --git a/misc/Function.Definitions.Core1.html b/misc/Function.Definitions.Core1.html new file mode 100644 index 0000000..7251560 --- /dev/null +++ b/misc/Function.Definitions.Core1.html @@ -0,0 +1,27 @@ + +Function.Definitions.Core1
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definitions for types of functions that only require an equality
+-- relation over the domain.
+------------------------------------------------------------------------
+
+-- The contents of this file should usually be accessed from `Function`.
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary
+
+module Function.Definitions.Core1
+  {a ℓ₁} {A : Set a} (_≈₁_ : Rel A ℓ₁)
+  where
+
+open import Level using (_⊔_)
+
+------------------------------------------------------------------------
+-- Definitions
+
+-- (Note the name `RightInverse` is used for the bundle)
+Inverseʳ : ∀ {b} {B : Set b} → (A → B) → (B → A) → Set (a ⊔ ℓ₁)
+Inverseʳ f g = ∀ x → g (f x) ≈₁ x
+
\ No newline at end of file diff --git a/misc/Function.Definitions.Core2.html b/misc/Function.Definitions.Core2.html new file mode 100644 index 0000000..01694f4 --- /dev/null +++ b/misc/Function.Definitions.Core2.html @@ -0,0 +1,31 @@ + +Function.Definitions.Core2
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definitions for types of functions that only require an equality
+-- relation over the co-domain.
+------------------------------------------------------------------------
+
+-- The contents of this file should usually be accessed from `Function`.
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary
+
+module Function.Definitions.Core2
+  {b ℓ₂} {B : Set b} (_≈₂_ : Rel B ℓ₂)
+  where
+
+open import Data.Product using (∃)
+open import Level using (Level; _⊔_)
+
+------------------------------------------------------------------------
+-- Definitions
+
+Surjective : ∀ {a} {A : Set a} → (A → B) → Set (a ⊔ b ⊔ ℓ₂)
+Surjective f = ∀ y → ∃ λ x → f x ≈₂ y
+
+-- (Note the name `LeftInverse` is used for the bundle)
+Inverseˡ : ∀ {a} {A : Set a} → (A → B) → (B → A) → Set (b ⊔ ℓ₂)
+Inverseˡ f g = ∀ x → f (g x) ≈₂ x
+
\ No newline at end of file diff --git a/misc/Function.Definitions.html b/misc/Function.Definitions.html new file mode 100644 index 0000000..1ecbf49 --- /dev/null +++ b/misc/Function.Definitions.html @@ -0,0 +1,49 @@ + +Function.Definitions
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definitions for types of functions.
+------------------------------------------------------------------------
+
+-- The contents of this file should usually be accessed from `Function`.
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary
+
+module Function.Definitions
+  {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b}
+  (_≈₁_ : Rel A ℓ₁) -- Equality over the domain
+  (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
+  where
+
+open import Data.Product using (∃; _×_)
+import Function.Definitions.Core1 as Core₁
+import Function.Definitions.Core2 as Core₂
+open import Function.Base
+open import Level using (_⊔_)
+
+------------------------------------------------------------------------
+-- Definitions
+
+Congruent : (A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+Congruent f = ∀ {x y} → x ≈₁ y →  f x ≈₂ f y
+
+Injective : (A → B) → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+Injective f = ∀ {x y} → f x ≈₂ f y → x ≈₁ y
+
+open Core₂ _≈₂_ public
+  using (Surjective)
+
+Bijective : (A → B) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
+Bijective f = Injective f × Surjective f
+
+open Core₂ _≈₂_ public
+  using (Inverseˡ)
+
+open Core₁ _≈₁_ public
+  using (Inverseʳ)
+
+Inverseᵇ : (A → B) → (B → A) → Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
+Inverseᵇ f g = Inverseˡ f g × Inverseʳ f g
+
\ No newline at end of file diff --git a/misc/Function.Equality.html b/misc/Function.Equality.html new file mode 100644 index 0000000..3526602 --- /dev/null +++ b/misc/Function.Equality.html @@ -0,0 +1,126 @@ + +Function.Equality
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Function setoids and related constructions
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+-- Note: use of the standard function hierarchy is encouraged. The
+-- module `Function` re-exports `Congruent`, `IsBijection` and
+-- `Bijection`. The alternative definitions found in this file will
+-- eventually be deprecated.
+
+module Function.Equality where
+
+import Function.Base as Fun
+open import Level
+open import Relation.Binary using (Setoid)
+open import Relation.Binary.Indexed.Heterogeneous
+  using (IndexedSetoid; _=[_]⇒_)
+import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
+  as Trivial
+
+------------------------------------------------------------------------
+-- Functions which preserve equality
+
+record Π {f₁ f₂ t₁ t₂}
+         (From : Setoid f₁ f₂)
+         (To : IndexedSetoid (Setoid.Carrier From) t₁ t₂) :
+         Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
+  infixl 5 _⟨$⟩_
+  field
+    _⟨$⟩_ : (x : Setoid.Carrier From) → IndexedSetoid.Carrier To x
+    cong  : Setoid._≈_ From =[ _⟨$⟩_ ]⇒ IndexedSetoid._≈_ To
+
+open Π public
+
+infixr 0 _⟶_
+
+_⟶_ : ∀ {f₁ f₂ t₁ t₂} → Setoid f₁ f₂ → Setoid t₁ t₂ → Set _
+From ⟶ To = Π From (Trivial.indexedSetoid To)
+
+------------------------------------------------------------------------
+-- Identity and composition.
+
+id : ∀ {a₁ a₂} {A : Setoid a₁ a₂} → A ⟶ A
+id = record { _⟨$⟩_ = Fun.id; cong = Fun.id }
+
+infixr 9 _∘_
+
+_∘_ : ∀ {a₁ a₂} {A : Setoid a₁ a₂}
+        {b₁ b₂} {B : Setoid b₁ b₂}
+        {c₁ c₂} {C : Setoid c₁ c₂} →
+      B ⟶ C → A ⟶ B → A ⟶ C
+f ∘ g = record
+  { _⟨$⟩_ = Fun._∘_ (_⟨$⟩_ f) (_⟨$⟩_ g)
+  ; cong  = Fun._∘_ (cong  f) (cong  g)
+  }
+
+-- Constant equality-preserving function.
+
+const : ∀ {a₁ a₂} {A : Setoid a₁ a₂}
+          {b₁ b₂} {B : Setoid b₁ b₂} →
+        Setoid.Carrier B → A ⟶ B
+const {B = B} b = record
+  { _⟨$⟩_ = Fun.const b
+  ; cong  = Fun.const (Setoid.refl B)
+  }
+
+------------------------------------------------------------------------
+-- Function setoids
+
+-- Dependent.
+
+setoid : ∀ {f₁ f₂ t₁ t₂}
+         (From : Setoid f₁ f₂) →
+         IndexedSetoid (Setoid.Carrier From) t₁ t₂ →
+         Setoid _ _
+setoid From To = record
+  { Carrier       = Π From To
+  ; _≈_           = λ f g → ∀ {x y} → x ≈₁ y → f ⟨$⟩ x ≈₂ g ⟨$⟩ y
+  ; isEquivalence = record
+    { refl  = λ {f} → cong f
+    ; sym   = λ f∼g x∼y → To.sym (f∼g (From.sym x∼y))
+    ; trans = λ f∼g g∼h x∼y → To.trans (f∼g From.refl) (g∼h x∼y)
+    }
+  }
+  where
+  open module From = Setoid From using () renaming (_≈_ to _≈₁_)
+  open module To = IndexedSetoid To   using () renaming (_≈_ to _≈₂_)
+
+-- Non-dependent.
+
+infixr 0 _⇨_
+
+_⇨_ : ∀ {f₁ f₂ t₁ t₂} → Setoid f₁ f₂ → Setoid t₁ t₂ → Setoid _ _
+From ⇨ To = setoid From (Trivial.indexedSetoid To)
+
+-- A variant of setoid which uses the propositional equality setoid
+-- for the domain, and a more convenient definition of _≈_.
+
+≡-setoid : ∀ {f t₁ t₂} (From : Set f) → IndexedSetoid From t₁ t₂ → Setoid _ _
+≡-setoid From To = record
+  { Carrier       = (x : From) → Carrier x
+  ; _≈_           = λ f g → ∀ x → f x ≈ g x
+  ; isEquivalence = record
+    { refl  = λ {f} x → refl
+    ; sym   = λ f∼g x → sym (f∼g x)
+    ; trans = λ f∼g g∼h x → trans (f∼g x) (g∼h x)
+    }
+  } where open IndexedSetoid To
+
+-- Parameter swapping function.
+
+flip : ∀ {a₁ a₂} {A : Setoid a₁ a₂}
+         {b₁ b₂} {B : Setoid b₁ b₂}
+         {c₁ c₂} {C : Setoid c₁ c₂} →
+       A ⟶ B ⇨ C → B ⟶ A ⇨ C
+flip {B = B} f = record
+  { _⟨$⟩_ = λ b → record
+    { _⟨$⟩_ = λ a → f ⟨$⟩ a ⟨$⟩ b
+    ; cong  = λ a₁≈a₂ → cong f a₁≈a₂ (Setoid.refl B) }
+  ; cong  = λ b₁≈b₂ a₁≈a₂ → cong f a₁≈a₂ b₁≈b₂
+  }
+
\ No newline at end of file diff --git a/misc/Function.Structures.html b/misc/Function.Structures.html new file mode 100644 index 0000000..486a86c --- /dev/null +++ b/misc/Function.Structures.html @@ -0,0 +1,154 @@ + +Function.Structures
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Structures for types of functions
+------------------------------------------------------------------------
+
+-- The contents of this file should usually be accessed from `Function`.
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary
+
+module Function.Structures {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 using (∃; _×_; _,_)
+open import Function.Base
+open import Function.Definitions
+open import Level using (_⊔_)
+
+------------------------------------------------------------------------
+-- One element structures
+------------------------------------------------------------------------
+
+record IsCongruent (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+  field
+    cong           : Congruent _≈₁_ _≈₂_ f
+    isEquivalence₁ : IsEquivalence _≈₁_
+    isEquivalence₂ : IsEquivalence _≈₂_
+
+  module Eq₁ where
+
+    setoid : Setoid a ℓ₁
+    setoid = record
+      { isEquivalence = isEquivalence₁
+      }
+
+    open Setoid setoid public
+
+  module Eq₂ where
+
+    setoid : Setoid b ℓ₂
+    setoid = record
+      { isEquivalence = isEquivalence₂
+      }
+
+    open Setoid setoid public
+
+
+record IsInjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+  field
+    isCongruent : IsCongruent f
+    injective   : Injective _≈₁_ _≈₂_ f
+
+  open IsCongruent isCongruent public
+
+
+record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+  field
+    isCongruent : IsCongruent f
+    surjective  : Surjective _≈₁_ _≈₂_ f
+
+  open IsCongruent isCongruent public
+
+
+record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+  field
+    isInjection : IsInjection f
+    surjective  : Surjective _≈₁_ _≈₂_ f
+
+  open IsInjection isInjection public
+
+  bijective : Bijective _≈₁_ _≈₂_ f
+  bijective = injective , surjective
+
+  isSurjection : IsSurjection f
+  isSurjection = record
+    { isCongruent = isCongruent
+    ; surjective  = surjective
+    }
+
+
+------------------------------------------------------------------------
+-- Two element structures
+------------------------------------------------------------------------
+
+record IsLeftInverse (f : A → B) (g : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+  field
+    isCongruent  : IsCongruent f
+    cong₂        : Congruent _≈₂_ _≈₁_ g
+    inverseˡ     : Inverseˡ _≈₁_ _≈₂_ f g
+
+  open IsCongruent isCongruent public
+    renaming (cong to cong₁)
+
+
+record IsRightInverse (f : A → B) (g : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+  field
+    isCongruent : IsCongruent f
+    cong₂       : Congruent _≈₂_ _≈₁_ g
+    inverseʳ    : Inverseʳ _≈₁_ _≈₂_ f g
+
+  open IsCongruent isCongruent public
+    renaming (cong to cong₁)
+
+
+record IsInverse (f : A → B) (g : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+  field
+    isLeftInverse : IsLeftInverse f g
+    inverseʳ      : Inverseʳ _≈₁_ _≈₂_ f g
+
+  open IsLeftInverse isLeftInverse public
+
+  isRightInverse : IsRightInverse f g
+  isRightInverse = record
+    { isCongruent = isCongruent
+    ; cong₂       = cong₂
+    ; inverseʳ    = inverseʳ
+    }
+
+  inverse : Inverseᵇ _≈₁_ _≈₂_ f g
+  inverse = inverseˡ , inverseʳ
+
+
+------------------------------------------------------------------------
+-- Three element structures
+------------------------------------------------------------------------
+
+record IsBiEquivalence
+  (f : A → B) (g₁ : B → A) (g₂ : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+  field
+    f-isCongruent : IsCongruent f
+    cong₂         : Congruent _≈₂_ _≈₁_ g₁
+    cong₃         : Congruent _≈₂_ _≈₁_ g₂
+
+  open IsCongruent f-isCongruent public
+    renaming (cong to cong₁)
+
+
+record IsBiInverse
+  (f : A → B) (g₁ : B → A) (g₂ : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
+  field
+    f-isCongruent : IsCongruent f
+    cong₂         : Congruent _≈₂_ _≈₁_ g₁
+    inverseˡ      : Inverseˡ _≈₁_ _≈₂_ f g₁
+    cong₃         : Congruent _≈₂_ _≈₁_ g₂
+    inverseʳ      : Inverseʳ _≈₁_ _≈₂_ f g₂
+
+  open IsCongruent f-isCongruent public
+    renaming (cong to cong₁)
+
\ No newline at end of file diff --git a/misc/Function.html b/misc/Function.html new file mode 100644 index 0000000..8867803 --- /dev/null +++ b/misc/Function.html @@ -0,0 +1,17 @@ + +Function
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Functions
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Function where
+
+open import Function.Core public
+open import Function.Base public
+open import Function.Definitions public
+open import Function.Structures public
+open import Function.Bundles public
+
\ No newline at end of file diff --git a/misc/Level.html b/misc/Level.html new file mode 100644 index 0000000..c6ba37c --- /dev/null +++ b/misc/Level.html @@ -0,0 +1,36 @@ + +Level
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Universe levels
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Level where
+
+-- Levels.
+
+open import Agda.Primitive as Prim public
+  using    (Level; _⊔_; Setω)
+  renaming (lzero to zero; lsuc to suc)
+
+-- Lifting.
+
+record Lift {a} ℓ (A : Set a) : Set (a ⊔ ℓ) where
+  constructor lift
+  field lower : A
+
+open Lift public
+
+-- Synonyms
+
+0ℓ : Level
+0ℓ = zero
+
+levelOfType : ∀ {a} → Set a → Level
+levelOfType {a} _ = a
+
+levelOfTerm : ∀ {a} {A : Set a} → A → Level
+levelOfTerm {a} _ = a
+
\ No newline at end of file diff --git a/misc/Relation.Binary.Bundles.html b/misc/Relation.Binary.Bundles.html new file mode 100644 index 0000000..0f5ce65 --- /dev/null +++ b/misc/Relation.Binary.Bundles.html @@ -0,0 +1,301 @@ + +Relation.Binary.Bundles
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Bundles for homogeneous binary relations
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via `Relation.Binary`.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.Bundles where
+
+open import Level
+open import Relation.Nullary using (¬_)
+open import Relation.Binary.Core
+open import Relation.Binary.Definitions
+open import Relation.Binary.Structures
+
+------------------------------------------------------------------------
+-- Setoids
+------------------------------------------------------------------------
+
+record PartialSetoid a ℓ : Set (suc (a ⊔ ℓ)) where
+  field
+    Carrier              : Set a
+    _≈_                  : Rel Carrier ℓ
+    isPartialEquivalence : IsPartialEquivalence _≈_
+
+  open IsPartialEquivalence isPartialEquivalence public
+
+  infix 4 _≉_
+  _≉_ : Rel Carrier _
+  x ≉ y = ¬ (x ≈ y)
+
+
+record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix 4 _≈_
+  field
+    Carrier       : Set c
+    _≈_           : Rel Carrier ℓ
+    isEquivalence : IsEquivalence _≈_
+
+  open IsEquivalence isEquivalence public
+
+  partialSetoid : PartialSetoid c ℓ
+  partialSetoid = record
+    { isPartialEquivalence = isPartialEquivalence
+    }
+
+  open PartialSetoid partialSetoid public using (_≉_)
+
+
+record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where
+  infix 4 _≈_
+  field
+    Carrier          : Set c
+    _≈_              : Rel Carrier ℓ
+    isDecEquivalence : IsDecEquivalence _≈_
+
+  open IsDecEquivalence isDecEquivalence public
+
+  setoid : Setoid c ℓ
+  setoid = record
+    { isEquivalence = isEquivalence
+    }
+
+  open Setoid setoid public using (partialSetoid; _≉_)
+
+
+------------------------------------------------------------------------
+-- Preorders
+------------------------------------------------------------------------
+
+record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _∼_
+  field
+    Carrier    : Set c
+    _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
+    _∼_        : Rel Carrier ℓ₂  -- The relation.
+    isPreorder : IsPreorder _≈_ _∼_
+
+  open IsPreorder isPreorder public
+    hiding (module Eq)
+
+  module Eq where
+    setoid : Setoid c ℓ₁
+    setoid = record
+      { isEquivalence = isEquivalence
+      }
+
+    open Setoid setoid public
+
+
+record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _≲_
+  field
+    Carrier         : Set c
+    _≈_             : Rel Carrier ℓ₁  -- The underlying equality.
+    _≲_             : Rel Carrier ℓ₂  -- The relation.
+    isTotalPreorder : IsTotalPreorder _≈_ _≲_
+
+  open IsTotalPreorder isTotalPreorder public
+    hiding (module Eq)
+
+  preorder : Preorder c ℓ₁ ℓ₂
+  preorder = record { isPreorder = isPreorder }
+
+  open Preorder preorder public
+    using (module Eq)
+
+
+------------------------------------------------------------------------
+-- Partial orders
+------------------------------------------------------------------------
+
+record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _≤_
+  field
+    Carrier        : Set c
+    _≈_            : Rel Carrier ℓ₁
+    _≤_            : Rel Carrier ℓ₂
+    isPartialOrder : IsPartialOrder _≈_ _≤_
+
+  open IsPartialOrder isPartialOrder public
+    hiding (module Eq)
+
+  preorder : Preorder c ℓ₁ ℓ₂
+  preorder = record
+    { isPreorder = isPreorder
+    }
+
+  open Preorder preorder public
+    using (module Eq)
+
+
+record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _≤_
+  field
+    Carrier           : Set c
+    _≈_               : Rel Carrier ℓ₁
+    _≤_               : Rel Carrier ℓ₂
+    isDecPartialOrder : IsDecPartialOrder _≈_ _≤_
+
+  private
+    module DPO = IsDecPartialOrder isDecPartialOrder
+  open DPO public hiding (module Eq)
+
+  poset : Poset c ℓ₁ ℓ₂
+  poset = record
+    { isPartialOrder = isPartialOrder
+    }
+
+  open Poset poset public
+    using (preorder)
+
+  module Eq where
+    decSetoid : DecSetoid c ℓ₁
+    decSetoid = record
+      { isDecEquivalence = DPO.Eq.isDecEquivalence
+      }
+
+    open DecSetoid decSetoid public
+
+
+record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _<_
+  field
+    Carrier              : Set c
+    _≈_                  : Rel Carrier ℓ₁
+    _<_                  : Rel Carrier ℓ₂
+    isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
+
+  open IsStrictPartialOrder isStrictPartialOrder public
+    hiding (module Eq)
+
+  module Eq where
+    setoid : Setoid c ℓ₁
+    setoid = record
+      { isEquivalence = isEquivalence
+      }
+
+    open Setoid setoid public
+
+
+record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _<_
+  field
+    Carrier                 : Set c
+    _≈_                     : Rel Carrier ℓ₁
+    _<_                     : Rel Carrier ℓ₂
+    isDecStrictPartialOrder : IsDecStrictPartialOrder _≈_ _<_
+
+  private
+    module DSPO = IsDecStrictPartialOrder isDecStrictPartialOrder
+  open DSPO public hiding (module Eq)
+
+  strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
+  strictPartialOrder = record
+    { isStrictPartialOrder = isStrictPartialOrder
+    }
+
+  module Eq where
+
+    decSetoid : DecSetoid c ℓ₁
+    decSetoid = record
+      { isDecEquivalence = DSPO.Eq.isDecEquivalence
+      }
+
+    open DecSetoid decSetoid public
+
+
+------------------------------------------------------------------------
+-- Total orders
+------------------------------------------------------------------------
+
+record TotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _≤_
+  field
+    Carrier      : Set c
+    _≈_          : Rel Carrier ℓ₁
+    _≤_          : Rel Carrier ℓ₂
+    isTotalOrder : IsTotalOrder _≈_ _≤_
+
+  open IsTotalOrder isTotalOrder public
+    hiding (module Eq)
+
+  poset : Poset c ℓ₁ ℓ₂
+  poset = record
+    { isPartialOrder = isPartialOrder
+    }
+
+  open Poset poset public
+    using (module Eq; preorder)
+
+  totalPreorder : TotalPreorder c ℓ₁ ℓ₂
+  totalPreorder = record
+    { isTotalPreorder = isTotalPreorder
+    }
+
+
+record DecTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _≤_
+  field
+    Carrier         : Set c
+    _≈_             : Rel Carrier ℓ₁
+    _≤_             : Rel Carrier ℓ₂
+    isDecTotalOrder : IsDecTotalOrder _≈_ _≤_
+
+  private
+    module DTO = IsDecTotalOrder isDecTotalOrder
+  open DTO public hiding (module Eq)
+
+  totalOrder : TotalOrder c ℓ₁ ℓ₂
+  totalOrder = record
+    { isTotalOrder = isTotalOrder
+    }
+
+  open TotalOrder totalOrder public using (poset; preorder)
+
+  decPoset : DecPoset c ℓ₁ ℓ₂
+  decPoset = record
+    { isDecPartialOrder = isDecPartialOrder
+    }
+
+  open DecPoset decPoset public using (module Eq)
+
+
+-- Note that these orders are decidable. The current implementation
+-- of `Trichotomous` subsumes irreflexivity and asymmetry. Any reasonable
+-- definition capturing these three properties implies decidability
+-- as `Trichotomous` necessarily separates out the equality case.
+
+record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _<_
+  field
+    Carrier            : Set c
+    _≈_                : Rel Carrier ℓ₁
+    _<_                : Rel Carrier ℓ₂
+    isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_
+
+  open IsStrictTotalOrder isStrictTotalOrder public
+    hiding (module Eq)
+
+  strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
+  strictPartialOrder = record
+    { isStrictPartialOrder = isStrictPartialOrder
+    }
+
+  open StrictPartialOrder strictPartialOrder public
+    using (module Eq)
+
+  decSetoid : DecSetoid c ℓ₁
+  decSetoid = record
+    { isDecEquivalence = isDecEquivalence
+    }
+  {-# WARNING_ON_USAGE decSetoid
+  "Warning: decSetoid was deprecated in v1.3.
+  Please use Eq.decSetoid instead."
+  #-}
+
\ No newline at end of file diff --git a/misc/Relation.Binary.Consequences.html b/misc/Relation.Binary.Consequences.html new file mode 100644 index 0000000..0f4829a --- /dev/null +++ b/misc/Relation.Binary.Consequences.html @@ -0,0 +1,287 @@ + +Relation.Binary.Consequences
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some properties imply others
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.Consequences where
+
+open import Data.Maybe.Base using (just; nothing; decToMaybe)
+open import Data.Sum.Base as Sum using (inj₁; inj₂)
+open import Data.Product using (_,_)
+open import Data.Empty.Irrelevant using (⊥-elim)
+open import Function.Base using (_∘_; _$_; flip)
+open import Level using (Level)
+open import Relation.Binary.Core
+open import Relation.Binary.Definitions
+open import Relation.Nullary using (yes; no; recompute)
+open import Relation.Nullary.Decidable.Core using (map′)
+open import Relation.Unary using (∁; Pred)
+
+private
+  variable
+    a ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ p : Level
+    A B : Set a
+
+------------------------------------------------------------------------
+-- Substitutive properties
+
+module _ {_∼_ : Rel A ℓ} (R : Rel A p) where
+
+  subst⇒respˡ : Substitutive _∼_ p → R Respectsˡ _∼_
+  subst⇒respˡ subst {y} x′∼x Px′y = subst (flip R y) x′∼x Px′y
+
+  subst⇒respʳ : Substitutive _∼_ p → R Respectsʳ _∼_
+  subst⇒respʳ subst {x} y′∼y Pxy′ = subst (R x) y′∼y Pxy′
+
+  subst⇒resp₂ : Substitutive _∼_ p → R Respects₂ _∼_
+  subst⇒resp₂ subst = subst⇒respʳ subst , subst⇒respˡ subst
+
+module _ {_∼_ : Rel A ℓ} {P : Pred A p} where
+
+  resp⇒¬-resp : Symmetric _∼_ → P Respects _∼_ → (∁ P) Respects _∼_
+  resp⇒¬-resp sym resp x∼y ¬Px Py = ¬Px (resp (sym x∼y) Py)
+
+------------------------------------------------------------------------
+-- Proofs for non-strict orders
+
+module _ {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} where
+
+  total⇒refl : _≤_ Respects₂ _≈_ → Symmetric _≈_ →
+               Total _≤_ → _≈_ ⇒ _≤_
+  total⇒refl (respʳ , respˡ) sym total {x} {y} x≈y with total x y
+  ... | inj₁ x∼y = x∼y
+  ... | inj₂ y∼x = respʳ x≈y (respˡ (sym x≈y) y∼x)
+
+  total∧dec⇒dec : _≈_ ⇒ _≤_ → Antisymmetric _≈_ _≤_ →
+                  Total _≤_ → Decidable _≈_ → Decidable _≤_
+  total∧dec⇒dec refl antisym total _≟_ x y with total x y
+  ... | inj₁ x≤y = yes x≤y
+  ... | inj₂ y≤x = map′ refl (flip antisym y≤x) (x ≟ y)
+
+module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {≤₁ : Rel A ℓ₃} {≤₂ : Rel B ℓ₄} where
+
+  mono⇒cong : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ →
+              ∀ {f} → f Preserves ≤₁ ⟶ ≤₂ → f Preserves ≈₁ ⟶ ≈₂
+  mono⇒cong sym reflexive antisym mono x≈y = antisym
+    (mono (reflexive x≈y))
+    (mono (reflexive (sym x≈y)))
+
+  antimono⇒cong : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ →
+                  ∀ {f} → f Preserves ≤₁ ⟶ (flip ≤₂) → f Preserves ≈₁ ⟶ ≈₂
+  antimono⇒cong sym reflexive antisym antimono p≈q = antisym
+    (antimono (reflexive (sym p≈q)))
+    (antimono (reflexive p≈q))
+
+------------------------------------------------------------------------
+-- Proofs for strict orders
+
+module _ {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where
+
+  trans∧irr⇒asym : Reflexive _≈_ → Transitive _<_ →
+                   Irreflexive _≈_ _<_ → Asymmetric _<_
+  trans∧irr⇒asym refl trans irrefl x<y y<x =
+    irrefl refl (trans x<y y<x)
+
+  irr∧antisym⇒asym : Irreflexive _≈_ _<_ → Antisymmetric _≈_ _<_ →
+                     Asymmetric _<_
+  irr∧antisym⇒asym irrefl antisym x<y y<x =
+    irrefl (antisym x<y y<x) x<y
+
+  asym⇒antisym : Asymmetric _<_ → Antisymmetric _≈_ _<_
+  asym⇒antisym asym x<y y<x = ⊥-elim (asym x<y y<x)
+
+  asym⇒irr : _<_ Respects₂ _≈_ → Symmetric _≈_ →
+             Asymmetric _<_ → Irreflexive _≈_ _<_
+  asym⇒irr (respʳ , respˡ) sym asym {x} {y} x≈y x<y =
+    asym x<y (respʳ (sym x≈y) (respˡ x≈y x<y))
+
+  tri⇒asym : Trichotomous _≈_ _<_ → Asymmetric _<_
+  tri⇒asym tri {x} {y} x<y x>y with tri x y
+  ... | tri< _   _ x≯y = x≯y x>y
+  ... | tri≈ _   _ x≯y = x≯y x>y
+  ... | tri> x≮y _ _   = x≮y x<y
+
+  tri⇒irr : Trichotomous _≈_ _<_ → Irreflexive _≈_ _<_
+  tri⇒irr compare {x} {y} x≈y x<y with compare x y
+  ... | tri< _   x≉y y≮x = x≉y x≈y
+  ... | tri> x≮y x≉y y<x = x≉y x≈y
+  ... | tri≈ x≮y _   y≮x = x≮y x<y
+
+  tri⇒dec≈ : Trichotomous _≈_ _<_ → Decidable _≈_
+  tri⇒dec≈ compare x y with compare x y
+  ... | tri< _ x≉y _ = no  x≉y
+  ... | tri≈ _ x≈y _ = yes x≈y
+  ... | tri> _ x≉y _ = no  x≉y
+
+  tri⇒dec< : Trichotomous _≈_ _<_ → Decidable _<_
+  tri⇒dec< compare x y with compare x y
+  ... | tri< x<y _ _ = yes x<y
+  ... | tri≈ x≮y _ _ = no  x≮y
+  ... | tri> x≮y _ _ = no  x≮y
+
+  trans∧tri⇒respʳ : Symmetric _≈_ → Transitive _≈_ →
+                    Transitive _<_ → Trichotomous _≈_ _<_ →
+                    _<_ Respectsʳ _≈_
+  trans∧tri⇒respʳ sym ≈-tr <-tr tri {x} {y} {z} y≈z x<y with tri x z
+  ... | tri< x<z _ _ = x<z
+  ... | tri≈ _ x≈z _ = ⊥-elim (tri⇒irr tri (≈-tr x≈z (sym y≈z)) x<y)
+  ... | tri> _ _ z<x = ⊥-elim (tri⇒irr tri (sym y≈z) (<-tr z<x x<y))
+
+  trans∧tri⇒respˡ : Transitive _≈_ →
+                    Transitive _<_ → Trichotomous _≈_ _<_ →
+                    _<_ Respectsˡ _≈_
+  trans∧tri⇒respˡ ≈-tr <-tr tri {z} {_} {y} x≈y x<z with tri y z
+  ... | tri< y<z _ _ = y<z
+  ... | tri≈ _ y≈z _ = ⊥-elim (tri⇒irr tri (≈-tr x≈y y≈z) x<z)
+  ... | tri> _ _ z<y = ⊥-elim (tri⇒irr tri x≈y (<-tr x<z z<y))
+
+  trans∧tri⇒resp : Symmetric _≈_ → Transitive _≈_ →
+                   Transitive _<_ → Trichotomous _≈_ _<_ →
+                   _<_ Respects₂ _≈_
+  trans∧tri⇒resp sym ≈-tr <-tr tri =
+    trans∧tri⇒respʳ sym ≈-tr <-tr tri ,
+    trans∧tri⇒respˡ ≈-tr <-tr tri
+
+------------------------------------------------------------------------
+-- Without Loss of Generality
+
+module _  {_R_ : Rel A ℓ₁} {Q : Rel A ℓ₂} where
+
+  wlog : Total _R_ → Symmetric Q →
+         (∀ a b → a R b → Q a b) →
+         ∀ a b → Q a b
+  wlog r-total q-sym prf a b with r-total a b
+  ... | inj₁ aRb = prf a b aRb
+  ... | inj₂ bRa = q-sym (prf b a bRa)
+
+------------------------------------------------------------------------
+-- Other proofs
+
+module _ {R : REL A B p} where
+
+  dec⇒weaklyDec : Decidable R → WeaklyDecidable R
+  dec⇒weaklyDec dec x y = decToMaybe (dec x y)
+
+  dec⇒recomputable : Decidable R → Recomputable R
+  dec⇒recomputable dec {a} {b} = recompute $ dec a b
+
+module _ {R : REL A B ℓ₁} {S : REL A B ℓ₂} where
+
+  map-NonEmpty : R ⇒ S → NonEmpty R → NonEmpty S
+  map-NonEmpty f x = nonEmpty (f (NonEmpty.proof x))
+
+module _ {R : REL A B ℓ₁} {S : REL B A ℓ₂} where
+
+  flip-Connex : Connex R S → Connex S R
+  flip-Connex f x y = Sum.swap (f y x)
+
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 1.6
+
+subst⟶respˡ = subst⇒respˡ
+{-# WARNING_ON_USAGE subst⟶respˡ
+"Warning: subst⟶respˡ was deprecated in v1.6.
+Please use subst⇒respˡ instead."
+#-}
+subst⟶respʳ = subst⇒respʳ
+{-# WARNING_ON_USAGE subst⟶respʳ
+"Warning: subst⟶respʳ was deprecated in v1.6.
+Please use subst⇒respʳ instead."
+#-}
+subst⟶resp₂ = subst⇒resp₂
+{-# WARNING_ON_USAGE subst⟶resp₂
+"Warning: subst⟶resp₂ was deprecated in v1.6.
+Please use subst⇒resp₂ instead."
+#-}
+P-resp⟶¬P-resp = resp⇒¬-resp
+{-# WARNING_ON_USAGE P-resp⟶¬P-resp
+"Warning: P-resp⟶¬P-resp was deprecated in v1.6.
+Please use resp⇒¬-resp instead."
+#-}
+total⟶refl = total⇒refl
+{-# WARNING_ON_USAGE total⟶refl
+"Warning: total⟶refl was deprecated in v1.6.
+Please use total⇒refl instead."
+#-}
+total+dec⟶dec = total∧dec⇒dec
+{-# WARNING_ON_USAGE total+dec⟶dec
+"Warning: total+dec⟶dec was deprecated in v1.6.
+Please use total∧dec⇒dec instead."
+#-}
+trans∧irr⟶asym = trans∧irr⇒asym
+{-# WARNING_ON_USAGE trans∧irr⟶asym
+"Warning: trans∧irr⟶asym was deprecated in v1.6.
+Please use trans∧irr⇒asym instead."
+#-}
+irr∧antisym⟶asym = irr∧antisym⇒asym
+{-# WARNING_ON_USAGE irr∧antisym⟶asym
+"Warning: irr∧antisym⟶asym was deprecated in v1.6.
+Please use irr∧antisym⇒asym instead."
+#-}
+asym⟶antisym = asym⇒antisym
+{-# WARNING_ON_USAGE asym⟶antisym
+"Warning: asym⟶antisym was deprecated in v1.6.
+Please use asym⇒antisym instead."
+#-}
+asym⟶irr = asym⇒irr
+{-# WARNING_ON_USAGE asym⟶irr
+"Warning: asym⟶irr was deprecated in v1.6.
+Please use asym⇒irr instead."
+#-}
+tri⟶asym = tri⇒asym
+{-# WARNING_ON_USAGE tri⟶asym
+"Warning: tri⟶asym was deprecated in v1.6.
+Please use tri⇒asym instead."
+#-}
+tri⟶irr = tri⇒irr
+{-# WARNING_ON_USAGE tri⟶irr
+"Warning: tri⟶irr was deprecated in v1.6.
+Please use tri⇒irr instead."
+#-}
+tri⟶dec≈ = tri⇒dec≈
+{-# WARNING_ON_USAGE tri⟶dec≈
+"Warning: tri⟶dec≈ was deprecated in v1.6.
+Please use tri⇒dec≈ instead."
+#-}
+tri⟶dec< = tri⇒dec<
+{-# WARNING_ON_USAGE tri⟶dec<
+"Warning: tri⟶dec< was deprecated in v1.6.
+Please use tri⇒dec< instead."
+#-}
+trans∧tri⟶respʳ≈ = trans∧tri⇒respʳ
+{-# WARNING_ON_USAGE trans∧tri⟶respʳ≈
+"Warning: trans∧tri⟶respʳ≈ was deprecated in v1.6.
+Please use trans∧tri⇒respʳ instead."
+#-}
+trans∧tri⟶respˡ≈ = trans∧tri⇒respˡ
+{-# WARNING_ON_USAGE trans∧tri⟶respˡ≈
+"Warning: trans∧tri⟶respˡ≈ was deprecated in v1.6.
+Please use trans∧tri⇒respˡ instead."
+#-}
+trans∧tri⟶resp≈ = trans∧tri⇒resp
+{-# WARNING_ON_USAGE trans∧tri⟶resp≈
+"Warning: trans∧tri⟶resp≈ was deprecated in v1.6.
+Please use trans∧tri⇒resp instead."
+#-}
+dec⟶weaklyDec = dec⇒weaklyDec
+{-# WARNING_ON_USAGE dec⟶weaklyDec
+"Warning: dec⟶weaklyDec was deprecated in v1.6.
+Please use dec⇒weaklyDec instead."
+#-}
+dec⟶recomputable = dec⇒recomputable
+{-# WARNING_ON_USAGE dec⟶recomputable
+"Warning: dec⟶recomputable was deprecated in v1.6.
+Please use dec⇒recomputable instead."
+#-}
+
\ No newline at end of file diff --git a/misc/Relation.Binary.Core.html b/misc/Relation.Binary.Core.html new file mode 100644 index 0000000..7ab98e0 --- /dev/null +++ b/misc/Relation.Binary.Core.html @@ -0,0 +1,68 @@ + +Relation.Binary.Core
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of binary relations
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via `Relation.Binary`.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.Core where
+
+open import Data.Product using (_×_)
+open import Function.Base using (_on_)
+open import Level using (Level; _⊔_; suc)
+
+private
+  variable
+    a b c ℓ ℓ₁ ℓ₂ ℓ₃ : Level
+    A : Set a
+    B : Set b
+    C : Set c
+
+------------------------------------------------------------------------
+-- Definitions
+------------------------------------------------------------------------
+
+-- Heterogeneous binary relations
+
+REL : Set a → Set b → (ℓ : Level) → Set (a ⊔ b ⊔ suc ℓ)
+REL A B ℓ = A → B → Set ℓ
+
+-- Homogeneous binary relations
+
+Rel : Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
+Rel A ℓ = REL A A ℓ
+
+------------------------------------------------------------------------
+-- Relationships between relations
+------------------------------------------------------------------------
+
+infix 4 _⇒_ _⇔_ _=[_]⇒_
+
+-- Implication/containment - could also be written _⊆_.
+-- and corresponding notion of equivalence
+
+_⇒_ : REL A B ℓ₁ → REL A B ℓ₂ → Set _
+P ⇒ Q = ∀ {x y} → P x y → Q x y
+
+_⇔_ : REL A B ℓ₁ → REL A B ℓ₂ → Set _
+P ⇔ Q = P ⇒ Q × Q ⇒ P
+
+-- Generalised implication - if P ≡ Q it can be read as "f preserves P".
+
+_=[_]⇒_ : Rel A ℓ₁ → (A → B) → Rel B ℓ₂ → Set _
+P =[ f ]⇒ Q = P ⇒ (Q on f)
+
+-- A synonym for _=[_]⇒_.
+
+_Preserves_⟶_ : (A → B) → Rel A ℓ₁ → Rel B ℓ₂ → Set _
+f Preserves P ⟶ Q = P =[ f ]⇒ Q
+
+-- A binary variant of _Preserves_⟶_.
+
+_Preserves₂_⟶_⟶_ : (A → B → C) → Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → Set _
+_∙_ Preserves₂ P ⟶ Q ⟶ R = ∀ {x y u v} → P x y → Q u v → R (x ∙ u) (y ∙ v)
+
\ No newline at end of file diff --git a/misc/Relation.Binary.Definitions.html b/misc/Relation.Binary.Definitions.html new file mode 100644 index 0000000..c8b7f3f --- /dev/null +++ b/misc/Relation.Binary.Definitions.html @@ -0,0 +1,225 @@ + +Relation.Binary.Definitions
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of binary relations
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via `Relation.Binary`.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.Definitions where
+
+open import Agda.Builtin.Equality using (_≡_)
+
+open import Data.Maybe.Base using (Maybe)
+open import Data.Product using (_×_)
+open import Data.Sum.Base using (_⊎_)
+open import Function.Base using (_on_; flip)
+open import Level
+open import Relation.Binary.Core
+open import Relation.Nullary using (Dec; ¬_)
+
+private
+  variable
+    a b c ℓ ℓ₁ ℓ₂ ℓ₃ : Level
+    A : Set a
+    B : Set b
+    C : Set c
+
+------------------------------------------------------------------------
+-- Definitions
+------------------------------------------------------------------------
+
+-- Reflexivity - defined without an underlying equality. It could
+-- alternatively be defined as `_≈_ ⇒ _∼_` for some equality `_≈_`.
+
+-- Confusingly the convention in the library is to use the name "refl"
+-- for proofs of Reflexive and `reflexive` for proofs of type `_≈_ ⇒ _∼_`,
+-- e.g. in the definition of `IsEquivalence` later in this file. This
+-- convention is a legacy from the early days of the library.
+
+Reflexive : Rel A ℓ → Set _
+Reflexive _∼_ = ∀ {x} → x ∼ x
+
+-- Generalised symmetry.
+
+Sym : REL A B ℓ₁ → REL B A ℓ₂ → Set _
+Sym P Q = P ⇒ flip Q
+
+-- Symmetry.
+
+Symmetric : Rel A ℓ → Set _
+Symmetric _∼_ = Sym _∼_ _∼_
+
+-- Generalised transitivity.
+
+Trans : REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
+Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k
+
+-- A flipped variant of generalised transitivity.
+
+TransFlip : REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
+TransFlip P Q R = ∀ {i j k} → Q j k → P i j → R i k
+
+-- Transitivity.
+
+Transitive : Rel A ℓ → Set _
+Transitive _∼_ = Trans _∼_ _∼_ _∼_
+
+-- Generalised antisymmetry
+
+Antisym : REL A B ℓ₁ → REL B A ℓ₂ → REL A B ℓ₃ → Set _
+Antisym R S E = ∀ {i j} → R i j → S j i → E i j
+
+-- Antisymmetry.
+
+Antisymmetric : Rel A ℓ₁ → Rel A ℓ₂ → Set _
+Antisymmetric _≈_ _≤_ = Antisym _≤_ _≤_ _≈_
+
+-- Irreflexivity - this is defined terms of the underlying equality.
+
+Irreflexive : REL A B ℓ₁ → REL A B ℓ₂ → Set _
+Irreflexive _≈_ _<_ = ∀ {x y} → x ≈ y → ¬ (x < y)
+
+-- Asymmetry.
+
+Asymmetric : Rel A ℓ → Set _
+Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)
+
+-- Generalised connex - exactly one of the two relations holds.
+
+Connex : REL A B ℓ₁ → REL B A ℓ₂ → Set _
+Connex P Q = ∀ x y → P x y ⊎ Q y x
+
+-- Totality.
+
+Total : Rel A ℓ → Set _
+Total _∼_ = Connex _∼_ _∼_
+
+-- Generalised trichotomy - exactly one of three types has a witness.
+
+data Tri (A : Set a) (B : Set b) (C : Set c) : Set (a ⊔ b ⊔ c) where
+  tri< : ( a :   A) (¬b : ¬ B) (¬c : ¬ C) → Tri A B C
+  tri≈ : (¬a : ¬ A) ( b :   B) (¬c : ¬ C) → Tri A B C
+  tri> : (¬a : ¬ A) (¬b : ¬ B) ( c :   C) → Tri A B C
+
+-- Trichotomy.
+
+Trichotomous : Rel A ℓ₁ → Rel A ℓ₂ → Set _
+Trichotomous _≈_ _<_ = ∀ x y → Tri (x < y) (x ≈ y) (x > y)
+  where _>_ = flip _<_
+
+-- Generalised maximum element.
+
+Max : REL A B ℓ → B → Set _
+Max _≤_ T = ∀ x → x ≤ T
+
+-- Maximum element.
+
+Maximum : Rel A ℓ → A → Set _
+Maximum = Max
+
+-- Generalised minimum element.
+
+Min : REL A B ℓ → A → Set _
+Min R = Max (flip R)
+
+-- Minimum element.
+
+Minimum : Rel A ℓ → A → Set _
+Minimum = Min
+
+-- Unary relations respecting a binary relation.
+
+_⟶_Respects_ : (A → Set ℓ₁) → (B → Set ℓ₂) → REL A B ℓ₃ → Set _
+P ⟶ Q Respects _∼_ = ∀ {x y} → x ∼ y → P x → Q y
+
+-- Unary relation respects a binary relation.
+
+_Respects_ : (A → Set ℓ₁) → Rel A ℓ₂ → Set _
+P Respects _∼_ = P ⟶ P Respects _∼_
+
+-- Right respecting - relatedness is preserved on the right by equality.
+
+_Respectsʳ_ : REL A B ℓ₁ → Rel B ℓ₂ → Set _
+_∼_ Respectsʳ _≈_ = ∀ {x} → (x ∼_) Respects _≈_
+
+-- Left respecting - relatedness is preserved on the left by equality.
+
+_Respectsˡ_ : REL A B ℓ₁ → Rel A ℓ₂ → Set _
+P Respectsˡ _∼_ = ∀ {y} → (flip P y) Respects _∼_
+
+-- Respecting - relatedness is preserved on both sides by equality
+
+_Respects₂_ : Rel A ℓ₁ → Rel A ℓ₂ → Set _
+P Respects₂ _∼_ = (P Respectsʳ _∼_) × (P Respectsˡ _∼_)
+
+-- Substitutivity - any two related elements satisfy exactly the same
+-- set of unary relations. Note that only the various derivatives
+-- of propositional equality can satisfy this property.
+
+Substitutive : Rel A ℓ₁ → (ℓ₂ : Level) → Set _
+Substitutive {A = A} _∼_ p = (P : A → Set p) → P Respects _∼_
+
+-- Decidability - it is possible to determine whether a given pair of
+-- elements are related.
+
+Decidable : REL A B ℓ → Set _
+Decidable _∼_ = ∀ x y → Dec (x ∼ y)
+
+-- Weak decidability - it is sometimes possible to determine if a given
+-- pair of elements are related.
+
+WeaklyDecidable : REL A B ℓ → Set _
+WeaklyDecidable _∼_ = ∀ x y → Maybe (x ∼ y)
+
+-- Propositional equality is decidable for the type.
+
+DecidableEquality : (A : Set a) → Set _
+DecidableEquality A = Decidable {A = A} _≡_
+
+-- Irrelevancy - all proofs that a given pair of elements are related
+-- are indistinguishable.
+
+Irrelevant : REL A B ℓ → Set _
+Irrelevant _∼_ = ∀ {x y} (a b : x ∼ y) → a ≡ b
+
+-- Recomputability - we can rebuild a relevant proof given an
+-- irrelevant one.
+
+Recomputable : REL A B ℓ → Set _
+Recomputable _∼_ = ∀ {x y} → .(x ∼ y) → x ∼ y
+
+-- Universal - all pairs of elements are related
+
+Universal : REL A B ℓ → Set _
+Universal _∼_ = ∀ x y → x ∼ y
+
+-- Non-emptiness - at least one pair of elements are related.
+
+record NonEmpty {A : Set a} {B : Set b}
+                (T : REL A B ℓ) : Set (a ⊔ b ⊔ ℓ) where
+  constructor nonEmpty
+  field
+    {x}   : A
+    {y}   : B
+    proof : T x y
+
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 1.1
+
+Conn = Connex
+{-# WARNING_ON_USAGE Conn
+"Warning: Conn was deprecated in v1.1.
+Please use Connex instead."
+#-}
+
\ No newline at end of file diff --git a/misc/Relation.Binary.Indexed.Heterogeneous.Bundles.html b/misc/Relation.Binary.Indexed.Heterogeneous.Bundles.html new file mode 100644 index 0000000..b38113f --- /dev/null +++ b/misc/Relation.Binary.Indexed.Heterogeneous.Bundles.html @@ -0,0 +1,45 @@ + +Relation.Binary.Indexed.Heterogeneous.Bundles
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Indexed binary relations
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via
+-- `Relation.Binary.Indexed.Heterogeneous`.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.Indexed.Heterogeneous.Bundles where
+
+open import Function.Base
+open import Level using (suc; _⊔_)
+open import Relation.Binary using (_⇒_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.Indexed.Heterogeneous.Core
+open import Relation.Binary.Indexed.Heterogeneous.Structures
+
+------------------------------------------------------------------------
+-- Definitions
+
+record IndexedSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
+  infix 4 _≈_
+  field
+    Carrier       : I → Set c
+    _≈_           : IRel Carrier ℓ
+    isEquivalence : IsIndexedEquivalence Carrier _≈_
+
+  open IsIndexedEquivalence isEquivalence public
+
+
+record IndexedPreorder {i} (I : Set i) c ℓ₁ ℓ₂ :
+                       Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _∼_
+  field
+    Carrier    : I → Set c
+    _≈_        : IRel Carrier ℓ₁  -- The underlying equality.
+    _∼_        : IRel Carrier ℓ₂  -- The relation.
+    isPreorder : IsIndexedPreorder Carrier _≈_ _∼_
+
+  open IsIndexedPreorder isPreorder public
+
\ No newline at end of file diff --git a/misc/Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html b/misc/Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html new file mode 100644 index 0000000..1b43cf4 --- /dev/null +++ b/misc/Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html @@ -0,0 +1,60 @@ + +Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Creates trivially indexed records from their non-indexed counterpart.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
+  {i} {I : Set i} where
+
+open import Relation.Binary
+open import Relation.Binary.Indexed.Heterogeneous hiding (Rel)
+  hiding (IsEquivalence; Setoid)
+
+------------------------------------------------------------------------
+-- Structures
+
+module _ {a} {A : Set a} where
+
+  private
+    Aᵢ : I → Set a
+    Aᵢ i = A
+
+  isIndexedEquivalence : ∀ {ℓ} {_≈_ : Rel A ℓ} → IsEquivalence _≈_ →
+                         IsIndexedEquivalence Aᵢ _≈_
+  isIndexedEquivalence isEq = record
+    { refl  = refl
+    ; sym   = sym
+    ; trans = trans
+    }
+    where open IsEquivalence isEq
+
+  isIndexedPreorder : ∀ {ℓ₁ ℓ₂} {_≈_ : Rel A ℓ₁} {_∼_ : Rel A ℓ₂} →
+                      IsPreorder _≈_ _∼_ →
+                      IsIndexedPreorder Aᵢ _≈_ _∼_
+  isIndexedPreorder isPreorder = record
+    { isEquivalence = isIndexedEquivalence isEquivalence
+    ; reflexive     = reflexive
+    ; trans         = trans
+    }
+    where open IsPreorder isPreorder
+
+------------------------------------------------------------------------
+-- Bundles
+
+indexedSetoid : ∀ {a ℓ} → Setoid a ℓ → IndexedSetoid I a ℓ
+indexedSetoid S = record
+  { isEquivalence = isIndexedEquivalence isEquivalence
+  }
+  where open Setoid S
+
+indexedPreorder : ∀ {a ℓ₁ ℓ₂} → Preorder a ℓ₁ ℓ₂ →
+                  IndexedPreorder I a ℓ₁ ℓ₂
+indexedPreorder O = record
+  { isPreorder = isIndexedPreorder isPreorder
+  }
+  where open Preorder O
+
\ No newline at end of file diff --git a/misc/Relation.Binary.Indexed.Heterogeneous.Core.html b/misc/Relation.Binary.Indexed.Heterogeneous.Core.html new file mode 100644 index 0000000..3c7acd1 --- /dev/null +++ b/misc/Relation.Binary.Indexed.Heterogeneous.Core.html @@ -0,0 +1,42 @@ + +Relation.Binary.Indexed.Heterogeneous.Core
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Indexed binary relations
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via
+-- `Relation.Binary.Indexed.Heterogeneous`.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.Indexed.Heterogeneous.Core where
+
+open import Level
+import Relation.Binary.Core as B
+import Relation.Binary.Definitions as B
+import Relation.Binary.PropositionalEquality.Core as P
+
+------------------------------------------------------------------------
+-- Indexed binary relations
+
+-- Heterogeneous types
+
+IREL : ∀ {i₁ i₂ a₁ a₂} {I₁ : Set i₁} {I₂ : Set i₂} →
+      (I₁ → Set a₁) → (I₂ → Set a₂) → (ℓ : Level) → Set _
+IREL A₁ A₂ ℓ = ∀ {i₁ i₂} → A₁ i₁ → A₂ i₂ → Set ℓ
+
+-- Homogeneous types
+
+IRel : ∀ {i a} {I : Set i} → (I → Set a) → (ℓ : Level) → Set _
+IRel A ℓ = IREL A A ℓ
+
+------------------------------------------------------------------------
+-- Generalised implication.
+
+infixr 4 _=[_]⇒_
+
+_=[_]⇒_ : ∀ {a b ℓ₁ ℓ₂} {A : Set a} {B : A → Set b} →
+          B.Rel A ℓ₁ → ((x : A) → B x) → IRel B ℓ₂ → Set _
+P =[ f ]⇒ Q = ∀ {i j} → P i j → Q (f i) (f j)
+
\ No newline at end of file diff --git a/misc/Relation.Binary.Indexed.Heterogeneous.Definitions.html b/misc/Relation.Binary.Indexed.Heterogeneous.Definitions.html new file mode 100644 index 0000000..3886ea9 --- /dev/null +++ b/misc/Relation.Binary.Indexed.Heterogeneous.Definitions.html @@ -0,0 +1,37 @@ + +Relation.Binary.Indexed.Heterogeneous.Definitions
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Indexed binary relations
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via
+-- `Relation.Binary.Indexed.Heterogeneous`.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.Indexed.Heterogeneous.Definitions where
+
+open import Level
+import Relation.Binary.Core as B
+import Relation.Binary.Definitions as B
+import Relation.Binary.PropositionalEquality.Core as P
+open import Relation.Binary.Indexed.Heterogeneous.Core
+
+private
+  variable
+    i a ℓ : Level
+    I : Set i
+
+------------------------------------------------------------------------
+-- Simple properties of indexed binary relations
+
+Reflexive : (A : I → Set a) → IRel A ℓ → Set _
+Reflexive _ _∼_ = ∀ {i} → B.Reflexive (_∼_ {i})
+
+Symmetric : (A : I → Set a) → IRel A ℓ → Set _
+Symmetric _ _∼_ = ∀ {i j} → B.Sym (_∼_ {i} {j}) _∼_
+
+Transitive : (A : I → Set a) → IRel A ℓ → Set _
+Transitive _ _∼_ = ∀ {i j k} → B.Trans _∼_ (_∼_ {j}) (_∼_ {i} {k})
+
\ No newline at end of file diff --git a/misc/Relation.Binary.Indexed.Heterogeneous.Structures.html b/misc/Relation.Binary.Indexed.Heterogeneous.Structures.html new file mode 100644 index 0000000..00a4767 --- /dev/null +++ b/misc/Relation.Binary.Indexed.Heterogeneous.Structures.html @@ -0,0 +1,48 @@ + +Relation.Binary.Indexed.Heterogeneous.Structures
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Indexed binary relations
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via
+-- `Relation.Binary.Indexed.Heterogeneous`.
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Indexed.Heterogeneous.Core
+
+module Relation.Binary.Indexed.Heterogeneous.Structures
+  {i a ℓ} {I : Set i} (A : I → Set a) (_≈_ : IRel A ℓ)
+  where
+
+open import Function.Base
+open import Level using (suc; _⊔_)
+open import Relation.Binary using (_⇒_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.Indexed.Heterogeneous.Definitions
+
+------------------------------------------------------------------------
+-- Equivalences
+
+record IsIndexedEquivalence : Set (i ⊔ a ⊔ ℓ) where
+  field
+    refl  : Reflexive  A _≈_
+    sym   : Symmetric  A _≈_
+    trans : Transitive A _≈_
+
+  reflexive : ∀ {i} → _≡_ ⟨ _⇒_ ⟩ _≈_ {i}
+  reflexive P.refl = refl
+
+
+record IsIndexedPreorder {ℓ₂} (_∼_ : IRel A ℓ₂) : Set (i ⊔ a ⊔ ℓ ⊔ ℓ₂) where
+  field
+    isEquivalence : IsIndexedEquivalence
+    reflexive     : ∀ {i j} → (_≈_ {i} {j}) ⟨ _⇒_ ⟩ _∼_
+    trans         : Transitive A _∼_
+
+  module Eq = IsIndexedEquivalence isEquivalence
+
+  refl : Reflexive A _∼_
+  refl = reflexive Eq.refl
+
\ No newline at end of file diff --git a/misc/Relation.Binary.Indexed.Heterogeneous.html b/misc/Relation.Binary.Indexed.Heterogeneous.html new file mode 100644 index 0000000..b7a823b --- /dev/null +++ b/misc/Relation.Binary.Indexed.Heterogeneous.html @@ -0,0 +1,49 @@ + +Relation.Binary.Indexed.Heterogeneous
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Heterogeneously-indexed binary relations
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.Indexed.Heterogeneous where
+
+------------------------------------------------------------------------
+-- Publicly export core definitions
+
+open import Relation.Binary.Indexed.Heterogeneous.Core public
+open import Relation.Binary.Indexed.Heterogeneous.Definitions public
+open import Relation.Binary.Indexed.Heterogeneous.Structures public
+open import Relation.Binary.Indexed.Heterogeneous.Bundles public
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 0.17
+
+REL = IREL
+{-# WARNING_ON_USAGE REL
+"Warning: REL was deprecated in v0.17.
+Please use IREL instead."
+#-}
+Rel = IRel
+{-# WARNING_ON_USAGE Rel
+"Warning: Rel was deprecated in v0.17.
+Please use IRel instead."
+#-}
+Setoid = IndexedSetoid
+{-# WARNING_ON_USAGE Setoid
+"Warning: Setoid was deprecated in v0.17.
+Please use IndexedSetoid instead."
+#-}
+IsEquivalence = IsIndexedEquivalence
+{-# WARNING_ON_USAGE IsEquivalence
+"Warning: IsEquivalence was deprecated in v0.17.
+Please use IsIndexedEquivalence instead."
+#-}
+
\ No newline at end of file diff --git a/misc/Relation.Binary.PropositionalEquality.Algebra.html b/misc/Relation.Binary.PropositionalEquality.Algebra.html new file mode 100644 index 0000000..ba5404d --- /dev/null +++ b/misc/Relation.Binary.PropositionalEquality.Algebra.html @@ -0,0 +1,35 @@ + +Relation.Binary.PropositionalEquality.Algebra
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Propositional (intensional) equality - Algebraic structures
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.PropositionalEquality.Algebra where
+
+open import Algebra
+open import Level
+open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality.Properties
+
+private
+  variable
+    a : Level
+    A : Set a
+
+------------------------------------------------------------------------
+-- Any operation forms a magma over _≡_
+
+isMagma : (_∙_ : Op₂ A) → IsMagma _≡_ _∙_
+isMagma _∙_ = record
+  { isEquivalence = isEquivalence
+  ; ∙-cong        = cong₂ _∙_
+  }
+
+magma : (_∙_ : Op₂ A) → Magma _ _
+magma _∙_ = record
+  { isMagma = isMagma _∙_
+  }
+
\ No newline at end of file diff --git a/misc/Relation.Binary.PropositionalEquality.Core.html b/misc/Relation.Binary.PropositionalEquality.Core.html new file mode 100644 index 0000000..f006c02 --- /dev/null +++ b/misc/Relation.Binary.PropositionalEquality.Core.html @@ -0,0 +1,127 @@ + +Relation.Binary.PropositionalEquality.Core
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Propositional equality
+--
+-- This file contains some core definitions which are re-exported by
+-- Relation.Binary.PropositionalEquality.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.PropositionalEquality.Core where
+
+open import Data.Product using (_,_)
+open import Function.Base using (_∘_)
+open import Level
+open import Relation.Binary.Core
+open import Relation.Binary.Definitions
+open import Relation.Nullary using (¬_)
+
+private
+  variable
+    a b ℓ : Level
+    A B C : Set a
+
+------------------------------------------------------------------------
+-- Propositional equality
+
+open import Agda.Builtin.Equality public
+
+infix 4 _≢_
+_≢_ : {A : Set a} → Rel A a
+x ≢ y = ¬ x ≡ y
+
+------------------------------------------------------------------------
+-- A variant of `refl` where the argument is explicit
+
+pattern erefl x = refl {x = x}
+
+------------------------------------------------------------------------
+-- Congruence lemmas
+
+cong : ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y
+cong f refl = refl
+
+cong′ : ∀ {f : A → B} x → f x ≡ f x
+cong′ _ = refl
+
+icong : ∀ {f : A → B} {x y} → x ≡ y → f x ≡ f y
+icong = cong _
+
+icong′ : ∀ {f : A → B} x → f x ≡ f x
+icong′ _ = refl
+
+cong₂ : ∀ (f : A → B → C) {x y u v} → x ≡ y → u ≡ v → f x u ≡ f y v
+cong₂ f refl refl = refl
+
+cong-app : ∀ {A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
+           f ≡ g → (x : A) → f x ≡ g x
+cong-app refl x = refl
+
+------------------------------------------------------------------------
+-- Properties of _≡_
+
+sym : Symmetric {A = A} _≡_
+sym refl = refl
+
+trans : Transitive {A = A} _≡_
+trans refl eq = eq
+
+subst : Substitutive {A = A} _≡_ ℓ
+subst P refl p = p
+
+subst₂ : ∀ (_∼_ : REL A B ℓ) {x y u v} → x ≡ y → u ≡ v → x ∼ u → y ∼ v
+subst₂ _ refl refl p = p
+
+resp : ∀ (P : A → Set ℓ) → P Respects _≡_
+resp P refl p = p
+
+respˡ : ∀ (∼ : Rel A ℓ) → ∼ Respectsˡ _≡_
+respˡ _∼_ refl x∼y = x∼y
+
+respʳ : ∀ (∼ : Rel A ℓ) → ∼ Respectsʳ _≡_
+respʳ _∼_ refl x∼y = x∼y
+
+resp₂ : ∀ (∼ : Rel A ℓ) → ∼ Respects₂ _≡_
+resp₂ _∼_ = respʳ _∼_ , respˡ _∼_
+
+------------------------------------------------------------------------
+-- Properties of _≢_
+
+≢-sym : Symmetric {A = A} _≢_
+≢-sym x≢y =  x≢y ∘ sym
+
+------------------------------------------------------------------------
+-- Convenient syntax for equational reasoning
+
+-- This is a special instance of `Relation.Binary.Reasoning.Setoid`.
+-- Rather than instantiating the latter with (setoid A), we reimplement
+-- equation chains from scratch since then goals are printed much more
+-- readably.
+
+module ≡-Reasoning {A : Set a} where
+
+  infix  3 _∎
+  infixr 2 _≡⟨⟩_ step-≡ step-≡˘
+  infix  1 begin_
+
+  begin_ : ∀{x y : A} → x ≡ y → x ≡ y
+  begin_ x≡y = x≡y
+
+  _≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y
+  _ ≡⟨⟩ x≡y = x≡y
+
+  step-≡ : ∀ (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
+  step-≡ _ y≡z x≡y = trans x≡y y≡z
+
+  step-≡˘ : ∀ (x {y z} : A) → y ≡ z → y ≡ x → x ≡ z
+  step-≡˘ _ y≡z y≡x = trans (sym y≡x) y≡z
+
+  _∎ : ∀ (x : A) → x ≡ x
+  _∎ _ = refl
+
+  syntax step-≡  x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z
+  syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z
+
\ No newline at end of file diff --git a/misc/Relation.Binary.PropositionalEquality.Properties.html b/misc/Relation.Binary.PropositionalEquality.Properties.html new file mode 100644 index 0000000..769c1fa --- /dev/null +++ b/misc/Relation.Binary.PropositionalEquality.Properties.html @@ -0,0 +1,146 @@ + +Relation.Binary.PropositionalEquality.Properties
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Propositional equality
+--
+-- This file contains some core properies of propositional equality which
+-- are re-exported by Relation.Binary.PropositionalEquality. They are
+-- ``equality rearrangement'' lemmas.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.PropositionalEquality.Properties where
+
+open import Function.Base using (id; _∘_)
+open import Level
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Unary using (Pred)
+
+private
+  variable
+    a p : Level
+    A B C : Set a
+
+------------------------------------------------------------------------
+-- Various equality rearrangement lemmas
+
+trans-reflʳ : ∀ {x y : A} (p : x ≡ y) → trans p refl ≡ p
+trans-reflʳ refl = refl
+
+trans-assoc : ∀ {x y z u : A} (p : x ≡ y) {q : y ≡ z} {r : z ≡ u} →
+  trans (trans p q) r ≡ trans p (trans q r)
+trans-assoc refl = refl
+
+trans-symˡ : ∀ {x y : A} (p : x ≡ y) → trans (sym p) p ≡ refl
+trans-symˡ refl = refl
+
+trans-symʳ : ∀ {x y : A} (p : x ≡ y) → trans p (sym p) ≡ refl
+trans-symʳ refl = refl
+
+trans-injectiveˡ : ∀ {x y z : A} {p₁ p₂ : x ≡ y} (q : y ≡ z) →
+                   trans p₁ q ≡ trans p₂ q → p₁ ≡ p₂
+trans-injectiveˡ refl = subst₂ _≡_ (trans-reflʳ _) (trans-reflʳ _)
+
+trans-injectiveʳ : ∀ {x y z : A} (p : x ≡ y) {q₁ q₂ : y ≡ z} →
+                   trans p q₁ ≡ trans p q₂ → q₁ ≡ q₂
+trans-injectiveʳ refl eq = eq
+
+cong-id : ∀ {x y : A} (p : x ≡ y) → cong id p ≡ p
+cong-id refl = refl
+
+cong-∘ : ∀ {x y : A} {f : B → C} {g : A → B} (p : x ≡ y) →
+         cong (f ∘ g) p ≡ cong f (cong g p)
+cong-∘ refl = refl
+
+trans-cong : ∀ {x y z : A} {f : A → B} (p : x ≡ y) {q : y ≡ z} →
+             trans (cong f p) (cong f q) ≡ cong f (trans p q)
+trans-cong refl = refl
+
+cong₂-reflˡ : ∀ {_∙_ : A → B → C} {x u v} → (p : u ≡ v) →
+              cong₂ _∙_ refl p ≡ cong (x ∙_) p
+cong₂-reflˡ refl = refl
+
+cong₂-reflʳ : ∀ {_∙_ : A → B → C} {x y u} → (p : x ≡ y) →
+              cong₂ _∙_ p refl ≡ cong (_∙ u) p
+cong₂-reflʳ refl = refl
+
+module _ {P : Pred A p} {x y : A} where
+
+  subst-injective : ∀ (x≡y : x ≡ y) {p q : P x} →
+                    subst P x≡y p ≡ subst P x≡y q → p ≡ q
+  subst-injective refl p≡q = p≡q
+
+  subst-subst : ∀ {z} (x≡y : x ≡ y) {y≡z : y ≡ z} {p : P x} →
+                subst P y≡z (subst P x≡y p) ≡ subst P (trans x≡y y≡z) p
+  subst-subst refl = refl
+
+  subst-subst-sym : (x≡y : x ≡ y) {p : P y} →
+                    subst P x≡y (subst P (sym x≡y) p) ≡ p
+  subst-subst-sym refl = refl
+
+  subst-sym-subst : (x≡y : x ≡ y) {p : P x} →
+                    subst P (sym x≡y) (subst P x≡y p) ≡ p
+  subst-sym-subst refl = refl
+
+subst-∘ : ∀ {x y : A} {P : Pred B p} {f : A → B}
+          (x≡y : x ≡ y) {p : P (f x)} →
+          subst (P ∘ f) x≡y p ≡ subst P (cong f x≡y) p
+subst-∘ refl = refl
+
+subst-application : ∀ {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
+                    (B₁ : A₁ → Set b₁) {B₂ : A₂ → Set b₂}
+                    {f : A₂ → A₁} {x₁ x₂ : A₂} {y : B₁ (f x₁)}
+                    (g : ∀ x → B₁ (f x) → B₂ x) (eq : x₁ ≡ x₂) →
+                    subst B₂ eq (g x₁ y) ≡ g x₂ (subst B₁ (cong f eq) y)
+subst-application _ _ refl = refl
+
+------------------------------------------------------------------------
+-- Structure of equality as a binary relation
+
+isEquivalence : IsEquivalence {A = A} _≡_
+isEquivalence = record
+  { refl  = refl
+  ; sym   = sym
+  ; trans = trans
+  }
+
+isDecEquivalence : Decidable _≡_ → IsDecEquivalence {A = A} _≡_
+isDecEquivalence _≟_ = record
+  { isEquivalence = isEquivalence
+  ; _≟_           = _≟_
+  }
+
+isPreorder : IsPreorder {A = A} _≡_ _≡_
+isPreorder = record
+  { isEquivalence = isEquivalence
+  ; reflexive     = id
+  ; trans         = trans
+  }
+
+------------------------------------------------------------------------
+-- Bundles for equality as a binary relation
+
+setoid : Set a → Setoid _ _
+setoid A = record
+  { Carrier       = A
+  ; _≈_           = _≡_
+  ; isEquivalence = isEquivalence
+  }
+
+decSetoid : Decidable {A = A} _≡_ → DecSetoid _ _
+decSetoid _≟_ = record
+  { _≈_              = _≡_
+  ; isDecEquivalence = isDecEquivalence _≟_
+  }
+
+preorder : Set a → Preorder _ _ _
+preorder A = record
+  { Carrier    = A
+  ; _≈_        = _≡_
+  ; _∼_        = _≡_
+  ; isPreorder = isPreorder
+  }
+
\ No newline at end of file diff --git a/misc/Relation.Binary.PropositionalEquality.html b/misc/Relation.Binary.PropositionalEquality.html new file mode 100644 index 0000000..8199ce2 --- /dev/null +++ b/misc/Relation.Binary.PropositionalEquality.html @@ -0,0 +1,148 @@ + +Relation.Binary.PropositionalEquality
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Propositional (intensional) equality
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary.PropositionalEquality where
+
+import Axiom.Extensionality.Propositional as Ext
+open import Axiom.UniquenessOfIdentityProofs
+open import Function.Base using (id; _∘_)
+open import Function.Equality using (Π; _⟶_; ≡-setoid)
+open import Level using (Level; _⊔_)
+open import Data.Product using (∃)
+
+open import Relation.Nullary using (yes ; no)
+open import Relation.Nullary.Decidable.Core
+open import Relation.Binary
+open import Relation.Binary.Indexed.Heterogeneous
+  using (IndexedSetoid)
+import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
+  as Trivial
+
+private
+  variable
+    a b c ℓ p : Level
+    A : Set a
+    B : Set b
+    C : Set c
+
+------------------------------------------------------------------------
+-- Re-export contents modules that make up the parts
+
+open import Relation.Binary.PropositionalEquality.Core public
+open import Relation.Binary.PropositionalEquality.Properties public
+open import Relation.Binary.PropositionalEquality.Algebra public
+
+------------------------------------------------------------------------
+-- Pointwise equality
+
+infix 4 _≗_
+
+_→-setoid_ : ∀ (A : Set a) (B : Set b) → Setoid _ _
+A →-setoid B = ≡-setoid A (Trivial.indexedSetoid (setoid B))
+
+_≗_ : (f g : A → B) → Set _
+_≗_ {A = A} {B = B} = Setoid._≈_ (A →-setoid B)
+
+:→-to-Π : ∀ {A : Set a} {B : IndexedSetoid A b ℓ} →
+          ((x : A) → IndexedSetoid.Carrier B x) → Π (setoid A) B
+:→-to-Π {B = B} f = record
+  { _⟨$⟩_ = f
+  ; cong  = λ { refl → IndexedSetoid.refl B }
+  }
+  where open IndexedSetoid B using (_≈_)
+
+→-to-⟶ : ∀ {A : Set a} {B : Setoid b ℓ} →
+         (A → Setoid.Carrier B) → setoid A ⟶ B
+→-to-⟶ = :→-to-Π
+
+------------------------------------------------------------------------
+-- Inspect
+
+-- Inspect can be used when you want to pattern match on the result r
+-- of some expression e, and you also need to "remember" that r ≡ e.
+
+-- See README.Inspect for an explanation of how/why to use this.
+
+record Reveal_·_is_ {A : Set a} {B : A → Set b}
+                    (f : (x : A) → B x) (x : A) (y : B x) :
+                    Set (a ⊔ b) where
+  constructor [_]
+  field eq : f x ≡ y
+
+inspect : ∀ {A : Set a} {B : A → Set b}
+          (f : (x : A) → B x) (x : A) → Reveal f · x is f x
+inspect f x = [ refl ]
+
+------------------------------------------------------------------------
+-- Propositionality
+
+isPropositional : Set a → Set a
+isPropositional A = (a b : A) → a ≡ b
+
+------------------------------------------------------------------------
+-- More complex rearrangement lemmas
+
+-- A lemma that is very similar to Lemma 2.4.3 from the HoTT book.
+
+naturality : ∀ {x y} {x≡y : x ≡ y} {f g : A → B}
+             (f≡g : ∀ x → f x ≡ g x) →
+             trans (cong f x≡y) (f≡g y) ≡ trans (f≡g x) (cong g x≡y)
+naturality {x = x} {x≡y = refl} f≡g =
+  f≡g x               ≡⟨ sym (trans-reflʳ _) ⟩
+  trans (f≡g x) refl  ∎
+  where open ≡-Reasoning
+
+-- A lemma that is very similar to Corollary 2.4.4 from the HoTT book.
+
+cong-≡id : ∀ {f : A → A} {x : A} (f≡id : ∀ x → f x ≡ x) →
+           cong f (f≡id x) ≡ f≡id (f x)
+cong-≡id {f = f} {x} f≡id =
+  cong f fx≡x                                    ≡⟨ sym (trans-reflʳ _) ⟩
+  trans (cong f fx≡x) refl                       ≡⟨ cong (trans _) (sym (trans-symʳ fx≡x)) ⟩
+  trans (cong f fx≡x) (trans fx≡x (sym fx≡x))    ≡⟨ sym (trans-assoc (cong f fx≡x)) ⟩
+  trans (trans (cong f fx≡x) fx≡x) (sym fx≡x)    ≡⟨ cong (λ p → trans p (sym _)) (naturality f≡id) ⟩
+  trans (trans f²x≡x (cong id fx≡x)) (sym fx≡x)  ≡⟨ cong (λ p → trans (trans f²x≡x p) (sym fx≡x)) (cong-id _) ⟩
+  trans (trans f²x≡x fx≡x) (sym fx≡x)            ≡⟨ trans-assoc f²x≡x ⟩
+  trans f²x≡x (trans fx≡x (sym fx≡x))            ≡⟨ cong (trans _) (trans-symʳ fx≡x) ⟩
+  trans f²x≡x refl                               ≡⟨ trans-reflʳ _ ⟩
+  f≡id (f x)                                     ∎
+  where open ≡-Reasoning; fx≡x = f≡id x; f²x≡x = f≡id (f x)
+
+module _ (_≟_ : Decidable {A = A} _≡_) {x y : A} where
+
+  ≡-≟-identity : (eq : x ≡ y) → x ≟ y ≡ yes eq
+  ≡-≟-identity eq = dec-yes-irr (x ≟ y) (Decidable⇒UIP.≡-irrelevant _≟_) eq
+
+  ≢-≟-identity : x ≢ y → ∃ λ ¬eq → x ≟ y ≡ no ¬eq
+  ≢-≟-identity ¬eq = dec-no (x ≟ y) ¬eq
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 1.0
+
+Extensionality = Ext.Extensionality
+{-# WARNING_ON_USAGE Extensionality
+"Warning: Extensionality was deprecated in v1.0.
+Please use Extensionality from `Axiom.Extensionality.Propositional` instead."
+#-}
+extensionality-for-lower-levels = Ext.lower-extensionality
+{-# WARNING_ON_USAGE extensionality-for-lower-levels
+"Warning: extensionality-for-lower-levels was deprecated in v1.0.
+Please use lower-extensionality from `Axiom.Extensionality.Propositional` instead."
+#-}
+∀-extensionality = Ext.∀-extensionality
+{-# WARNING_ON_USAGE ∀-extensionality
+"Warning: ∀-extensionality was deprecated in v1.0.
+Please use ∀-extensionality from `Axiom.Extensionality.Propositional` instead."
+#-}
+
\ No newline at end of file diff --git a/misc/Relation.Binary.Reasoning.Base.Single.html b/misc/Relation.Binary.Reasoning.Base.Single.html new file mode 100644 index 0000000..fbb3d41 --- /dev/null +++ b/misc/Relation.Binary.Reasoning.Base.Single.html @@ -0,0 +1,90 @@ + +Relation.Binary.Reasoning.Base.Single
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- The basic code for equational reasoning with a single relation
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary
+
+module Relation.Binary.Reasoning.Base.Single
+  {a ℓ} {A : Set a} (_∼_ : Rel A ℓ)
+  (refl : Reflexive _∼_) (trans : Transitive _∼_)
+  where
+
+-- TODO: the following part is copied from Relation.Binary.Reasoning.Base.Partial
+-- in order to avoid larger refactors. We will refactor this part later
+-- so taht we use the same framework as Relation.Binary.Reasoning.Base.Partial.
+
+open import Level using (_⊔_)
+open import Relation.Binary.PropositionalEquality.Core as P
+  using (_≡_)
+
+infix  4 _IsRelatedTo_
+
+------------------------------------------------------------------------
+-- Definition of "related to"
+
+-- This seemingly unnecessary type is used to make it possible to
+-- infer arguments even if the underlying equality evaluates.
+
+data _IsRelatedTo_ (x y : A) : Set ℓ where
+  relTo : (x∼y : x ∼ y) → x IsRelatedTo y
+
+------------------------------------------------------------------------
+-- Reasoning combinators
+
+-- Note that the arguments to the `step`s are not provided in their
+-- "natural" order and syntax declarations are later used to re-order
+-- them. This is because the `step` ordering allows the type-checker to
+-- better infer the middle argument `y` from the `_IsRelatedTo_`
+-- argument (see issue 622).
+--
+-- This has two practical benefits. First it speeds up type-checking by
+-- approximately a factor of 5. Secondly it allows the combinators to be
+-- used with macros that use reflection, e.g. `Tactic.RingSolver`, where
+-- they need to be able to extract `y` using reflection.
+
+infix  1 begin_
+infixr 2 step-∼ step-≡ step-≡˘
+infixr 2 _≡⟨⟩_
+infix  3 _∎
+
+-- Beginning of a proof
+
+begin_ : ∀ {x y} → x IsRelatedTo y → x ∼ y
+begin relTo x∼y = x∼y
+
+-- Standard step with the relation
+
+step-∼ : ∀ x {y z} → y IsRelatedTo z → x ∼ y → x IsRelatedTo z
+step-∼ _ (relTo y∼z) x∼y = relTo (trans x∼y y∼z)
+
+-- Step with a non-trivial propositional equality
+
+step-≡ : ∀ x {y z} → y IsRelatedTo z → x ≡ y → x IsRelatedTo z
+step-≡ _ x∼z P.refl = x∼z
+
+-- Step with a flipped non-trivial propositional equality
+
+step-≡˘ : ∀ x {y z} → y IsRelatedTo z → y ≡ x → x IsRelatedTo z
+step-≡˘ _ x∼z P.refl = x∼z
+
+-- Step with a trivial propositional equality
+
+_≡⟨⟩_ : ∀ x {y} → x IsRelatedTo y → x IsRelatedTo y
+_ ≡⟨⟩ x∼y = x∼y
+
+-- Termination
+
+_∎ : ∀ x → x IsRelatedTo x
+x ∎ = relTo refl
+
+-- Syntax declarations
+
+syntax step-∼  x y∼z x∼y = x ∼⟨  x∼y ⟩ y∼z
+syntax step-≡  x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z
+syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z
+
\ No newline at end of file diff --git a/misc/Relation.Binary.Reasoning.Setoid.html b/misc/Relation.Binary.Reasoning.Setoid.html new file mode 100644 index 0000000..d7241ff --- /dev/null +++ b/misc/Relation.Binary.Reasoning.Setoid.html @@ -0,0 +1,49 @@ + +Relation.Binary.Reasoning.Setoid
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Convenient syntax for reasoning with a setoid
+------------------------------------------------------------------------
+
+-- Example use:
+
+-- n*0≡0 : ∀ n → n * 0 ≡ 0
+-- n*0≡0 zero    = refl
+-- n*0≡0 (suc n) = begin
+--   suc n * 0 ≈⟨ refl ⟩
+--   n * 0 + 0 ≈⟨ ... ⟩
+--   n * 0     ≈⟨ n*0≡0 n ⟩
+--   0         ∎
+
+-- Module `≡-Reasoning` in `Relation.Binary.PropositionalEquality`
+-- is recommended for equational reasoning when the underlying equality is
+-- `_≡_`.
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary
+
+module Relation.Binary.Reasoning.Setoid {s₁ s₂} (S : Setoid s₁ s₂) where
+
+open Setoid S
+
+------------------------------------------------------------------------
+-- Reasoning combinators
+
+-- open import Relation.Binary.Reasoning.PartialSetoid partialSetoid public
+open import Relation.Binary.Reasoning.Base.Single _≈_ refl trans as Base public
+  hiding (step-∼)
+
+infixr 2 step-≈ step-≈˘
+
+-- A step using an equality
+
+step-≈ = Base.step-∼
+syntax step-≈ x y≈z x≈y = x ≈⟨ x≈y ⟩ y≈z
+
+-- A step using a symmetric equality
+
+step-≈˘ : ∀ x {y z} → y IsRelatedTo z → y ≈ x → x IsRelatedTo z
+step-≈˘ x y∼z y≈x = x ≈⟨ sym y≈x ⟩ y∼z
+syntax step-≈˘ x y≈z y≈x = x ≈˘⟨ y≈x ⟩ y≈z
+
\ No newline at end of file diff --git a/misc/Relation.Binary.Structures.html b/misc/Relation.Binary.Structures.html new file mode 100644 index 0000000..0903d4c --- /dev/null +++ b/misc/Relation.Binary.Structures.html @@ -0,0 +1,288 @@ + +Relation.Binary.Structures
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Structures for homogeneous binary relations
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via `Relation.Binary`.
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Core
+
+module Relation.Binary.Structures
+  {a ℓ} {A : Set a} -- The underlying set
+  (_≈_ : Rel A ℓ)   -- The underlying equality relation
+  where
+
+open import Data.Product using (proj₁; proj₂; _,_)
+open import Level using (Level; _⊔_)
+open import Relation.Nullary using (¬_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.Consequences
+open import Relation.Binary.Definitions
+
+private
+  variable
+    ℓ₂ : Level
+
+------------------------------------------------------------------------
+-- Equivalences
+------------------------------------------------------------------------
+-- Note all the following equivalences refer to the equality provided
+-- as a module parameter at the top of this file.
+
+record IsPartialEquivalence : Set (a ⊔ ℓ) where
+  field
+    sym   : Symmetric _≈_
+    trans : Transitive _≈_
+
+-- The preorders of this library are defined in terms of an underlying
+-- equivalence relation, and hence equivalence relations are not
+-- defined in terms of preorders.
+
+-- To preserve backwards compatability, equivalence relations are
+-- not defined in terms of their partial counterparts.
+
+record IsEquivalence : Set (a ⊔ ℓ) where
+  field
+    refl  : Reflexive _≈_
+    sym   : Symmetric _≈_
+    trans : Transitive _≈_
+
+  reflexive : _≡_ ⇒ _≈_
+  reflexive P.refl = refl
+
+  isPartialEquivalence : IsPartialEquivalence
+  isPartialEquivalence = record
+    { sym = sym
+    ; trans = trans
+    }
+
+
+record IsDecEquivalence : Set (a ⊔ ℓ) where
+  infix 4 _≟_
+  field
+    isEquivalence : IsEquivalence
+    _≟_           : Decidable _≈_
+
+  open IsEquivalence isEquivalence public
+
+
+------------------------------------------------------------------------
+-- Preorders
+------------------------------------------------------------------------
+
+record IsPreorder (_∼_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+  field
+    isEquivalence : IsEquivalence
+    -- Reflexivity is expressed in terms of the underlying equality:
+    reflexive     : _≈_ ⇒ _∼_
+    trans         : Transitive _∼_
+
+  module Eq = IsEquivalence isEquivalence
+
+  refl : Reflexive _∼_
+  refl = reflexive Eq.refl
+
+  ∼-respˡ-≈ : _∼_ Respectsˡ _≈_
+  ∼-respˡ-≈ x≈y x∼z = trans (reflexive (Eq.sym x≈y)) x∼z
+
+  ∼-respʳ-≈ : _∼_ Respectsʳ _≈_
+  ∼-respʳ-≈ x≈y z∼x = trans z∼x (reflexive x≈y)
+
+  ∼-resp-≈ : _∼_ Respects₂ _≈_
+  ∼-resp-≈ = ∼-respʳ-≈ , ∼-respˡ-≈
+
+
+record IsTotalPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+  field
+    isPreorder : IsPreorder _≲_
+    total      : Total _≲_
+
+  open IsPreorder isPreorder public
+    renaming
+    ( ∼-respˡ-≈ to ≲-respˡ-≈
+    ; ∼-respʳ-≈ to ≲-respʳ-≈
+    ; ∼-resp-≈  to ≲-resp-≈
+    )
+
+
+------------------------------------------------------------------------
+-- Partial orders
+------------------------------------------------------------------------
+
+record IsPartialOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+  field
+    isPreorder : IsPreorder _≤_
+    antisym    : Antisymmetric _≈_ _≤_
+
+  open IsPreorder isPreorder public
+    renaming
+    ( ∼-respˡ-≈ to ≤-respˡ-≈
+    ; ∼-respʳ-≈ to ≤-respʳ-≈
+    ; ∼-resp-≈  to ≤-resp-≈
+    )
+
+
+record IsDecPartialOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+  infix 4 _≟_ _≤?_
+  field
+    isPartialOrder : IsPartialOrder _≤_
+    _≟_            : Decidable _≈_
+    _≤?_           : Decidable _≤_
+
+  open IsPartialOrder isPartialOrder public
+    hiding (module Eq)
+
+  module Eq where
+
+    isDecEquivalence : IsDecEquivalence
+    isDecEquivalence = record
+      { isEquivalence = isEquivalence
+      ; _≟_           = _≟_
+      }
+
+    open IsDecEquivalence isDecEquivalence public
+
+
+record IsStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+  field
+    isEquivalence : IsEquivalence
+    irrefl        : Irreflexive _≈_ _<_
+    trans         : Transitive _<_
+    <-resp-≈      : _<_ Respects₂ _≈_
+
+  module Eq = IsEquivalence isEquivalence
+
+  asym : Asymmetric _<_
+  asym {x} {y} = trans∧irr⇒asym Eq.refl trans irrefl {x = x} {y}
+
+  <-respʳ-≈ : _<_ Respectsʳ _≈_
+  <-respʳ-≈ = proj₁ <-resp-≈
+
+  <-respˡ-≈ : _<_ Respectsˡ _≈_
+  <-respˡ-≈ = proj₂ <-resp-≈
+
+  asymmetric = asym
+  {-# WARNING_ON_USAGE asymmetric
+  "Warning: asymmetric was deprecated in v0.16.
+  Please use asym instead."
+  #-}
+
+
+record IsDecStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+  infix 4 _≟_ _<?_
+  field
+    isStrictPartialOrder : IsStrictPartialOrder _<_
+    _≟_                  : Decidable _≈_
+    _<?_                 : Decidable _<_
+
+  private
+    module SPO = IsStrictPartialOrder isStrictPartialOrder
+
+  open SPO public hiding (module Eq)
+
+  module Eq where
+
+    isDecEquivalence : IsDecEquivalence
+    isDecEquivalence = record
+      { isEquivalence = SPO.isEquivalence
+      ; _≟_           = _≟_
+      }
+
+    open IsDecEquivalence isDecEquivalence public
+
+
+------------------------------------------------------------------------
+-- Total orders
+------------------------------------------------------------------------
+
+record IsTotalOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+  field
+    isPartialOrder : IsPartialOrder _≤_
+    total          : Total _≤_
+
+  open IsPartialOrder isPartialOrder public
+
+  isTotalPreorder : IsTotalPreorder _≤_
+  isTotalPreorder = record
+    { isPreorder = isPreorder
+    ; total      = total
+    }
+
+
+record IsDecTotalOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+  infix 4 _≟_ _≤?_
+  field
+    isTotalOrder : IsTotalOrder _≤_
+    _≟_          : Decidable _≈_
+    _≤?_         : Decidable _≤_
+
+  open IsTotalOrder isTotalOrder public
+    hiding (module Eq)
+
+  isDecPartialOrder : IsDecPartialOrder _≤_
+  isDecPartialOrder = record
+    { isPartialOrder = isPartialOrder
+    ; _≟_            = _≟_
+    ; _≤?_           = _≤?_
+    }
+
+  module Eq where
+
+    isDecEquivalence : IsDecEquivalence
+    isDecEquivalence = record
+      { isEquivalence = isEquivalence
+      ; _≟_           = _≟_
+      }
+
+    open IsDecEquivalence isDecEquivalence public
+
+
+-- Note that these orders are decidable. The current implementation
+-- of `Trichotomous` subsumes irreflexivity and asymmetry. Any reasonable
+-- definition capturing these three properties implies decidability
+-- as `Trichotomous` necessarily separates out the equality case.
+
+record IsStrictTotalOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+  field
+    isEquivalence : IsEquivalence
+    trans         : Transitive _<_
+    compare       : Trichotomous _≈_ _<_
+
+  infix 4 _≟_ _<?_
+
+  _≟_ : Decidable _≈_
+  _≟_ = tri⇒dec≈ compare
+
+  _<?_ : Decidable _<_
+  _<?_ = tri⇒dec< compare
+
+  isDecEquivalence : IsDecEquivalence
+  isDecEquivalence = record
+    { isEquivalence = isEquivalence
+    ; _≟_           = _≟_
+    }
+
+  module Eq = IsDecEquivalence isDecEquivalence
+
+  isStrictPartialOrder : IsStrictPartialOrder _<_
+  isStrictPartialOrder = record
+    { isEquivalence = isEquivalence
+    ; irrefl        = tri⇒irr compare
+    ; trans         = trans
+    ; <-resp-≈      = trans∧tri⇒resp Eq.sym Eq.trans trans compare
+    }
+
+  isDecStrictPartialOrder : IsDecStrictPartialOrder _<_
+  isDecStrictPartialOrder = record
+    { isStrictPartialOrder = isStrictPartialOrder
+    ; _≟_                  = _≟_
+    ; _<?_                 = _<?_
+    }
+
+  open IsStrictPartialOrder isStrictPartialOrder public
+    using (irrefl; asym; <-respʳ-≈; <-respˡ-≈; <-resp-≈)
+
\ No newline at end of file diff --git a/misc/Relation.Binary.html b/misc/Relation.Binary.html new file mode 100644 index 0000000..4fe3199 --- /dev/null +++ b/misc/Relation.Binary.html @@ -0,0 +1,19 @@ + +Relation.Binary
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of homogeneous binary relations
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Binary where
+
+------------------------------------------------------------------------
+-- Re-export various components of the binary relation hierarchy
+
+open import Relation.Binary.Core public
+open import Relation.Binary.Definitions public
+open import Relation.Binary.Structures public
+open import Relation.Binary.Bundles public
+
\ No newline at end of file diff --git a/misc/Relation.Nullary.Decidable.Core.html b/misc/Relation.Nullary.Decidable.Core.html new file mode 100644 index 0000000..77b8dba --- /dev/null +++ b/misc/Relation.Nullary.Decidable.Core.html @@ -0,0 +1,132 @@ + +Relation.Nullary.Decidable.Core
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Operations on and properties of decidable relations
+--
+-- This file contains some core definitions which are re-exported by
+-- Relation.Nullary.Decidable
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Nullary.Decidable.Core where
+
+open import Level using (Level; Lift)
+open import Data.Bool.Base using (Bool; false; true; not; T)
+open import Data.Unit.Base using (⊤)
+open import Data.Empty
+open import Data.Product
+open import Function.Base
+
+open import Agda.Builtin.Equality
+open import Relation.Nullary.Reflects
+open import Relation.Nullary
+
+private
+  variable
+    p q : Level
+    P : Set p
+    Q : Set q
+
+-- `isYes` is a stricter version of `does`. The lack of computation means that
+-- we can recover the proposition `P` from `isYes P?` by unification. This is
+-- useful when we are using the decision procedure for proof automation.
+
+isYes : Dec P → Bool
+isYes ( true because _) = true
+isYes (false because _) = false
+
+isYes≗does : (P? : Dec P) → isYes P? ≡ does P?
+isYes≗does ( true because _) = refl
+isYes≗does (false because _) = refl
+
+-- The traditional name for isYes is ⌊_⌋, indicating the stripping of evidence.
+⌊_⌋ = isYes
+
+isNo : Dec P → Bool
+isNo = not ∘ isYes
+
+True : Dec P → Set
+True Q = T (isYes Q)
+
+False : Dec P → Set
+False Q = T (isNo Q)
+
+-- Gives a witness to the "truth".
+
+toWitness : {Q : Dec P} → True Q → P
+toWitness {Q = true  because [p]} _  = invert [p]
+toWitness {Q = false because  _ } ()
+
+-- Establishes a "truth", given a witness.
+
+fromWitness : {Q : Dec P} → P → True Q
+fromWitness {Q = true  because   _ } = const _
+fromWitness {Q = false because [¬p]} = invert [¬p]
+
+-- Variants for False.
+
+toWitnessFalse : {Q : Dec P} → False Q → ¬ P
+toWitnessFalse {Q = true  because   _ } ()
+toWitnessFalse {Q = false because [¬p]} _  = invert [¬p]
+
+fromWitnessFalse : {Q : Dec P} → ¬ P → False Q
+fromWitnessFalse {Q = true  because [p]} = flip _$_ (invert [p])
+fromWitnessFalse {Q = false because  _ } = const _
+
+-- If a decision procedure returns "yes", then we can extract the
+-- proof using from-yes.
+
+module _ {p} {P : Set p} where
+
+  From-yes : Dec P → Set p
+  From-yes (true  because _) = P
+  From-yes (false because _) = Lift p ⊤
+
+  from-yes : (p : Dec P) → From-yes p
+  from-yes (true  because [p]) = invert [p]
+  from-yes (false because _ ) = _
+
+-- If a decision procedure returns "no", then we can extract the proof
+-- using from-no.
+
+  From-no : Dec P → Set p
+  From-no (false because _) = ¬ P
+  From-no (true  because _) = Lift p ⊤
+
+  from-no : (p : Dec P) → From-no p
+  from-no (false because [¬p]) = invert [¬p]
+  from-no (true  because   _ ) = _
+
+------------------------------------------------------------------------
+-- Result of decidability
+
+dec-true : (p? : Dec P) → P → does p? ≡ true
+dec-true (true  because   _ ) p = refl
+dec-true (false because [¬p]) p = ⊥-elim (invert [¬p] p)
+
+dec-false : (p? : Dec P) → ¬ P → does p? ≡ false
+dec-false (false because  _ ) ¬p = refl
+dec-false (true  because [p]) ¬p = ⊥-elim (¬p (invert [p]))
+
+dec-yes : (p? : Dec P) → P → ∃ λ p′ → p? ≡ yes p′
+dec-yes p? p with dec-true p? p
+dec-yes (yes p′) p | refl = p′ , refl
+
+dec-no : (p? : Dec P) → ¬ P → ∃ λ ¬p′ → p? ≡ no ¬p′
+dec-no p? ¬p with dec-false p? ¬p
+dec-no (no ¬p′) ¬p | refl = ¬p′ , refl
+
+dec-yes-irr : (p? : Dec P) → Irrelevant P → (p : P) → p? ≡ yes p
+dec-yes-irr p? irr p with dec-yes p? p
+... | p′ , eq rewrite irr p p′ = eq
+
+------------------------------------------------------------------------
+-- Maps
+
+map′ : (P → Q) → (Q → P) → Dec P → Dec Q
+does  (map′ P→Q Q→P p?)                   = does p?
+proof (map′ P→Q Q→P (true  because  [p])) = ofʸ (P→Q (invert [p]))
+proof (map′ P→Q Q→P (false because [¬p])) = ofⁿ (invert [¬p] ∘ Q→P)
+
\ No newline at end of file diff --git a/misc/Relation.Nullary.Reflects.html b/misc/Relation.Nullary.Reflects.html new file mode 100644 index 0000000..24a6476 --- /dev/null +++ b/misc/Relation.Nullary.Reflects.html @@ -0,0 +1,53 @@ + +Relation.Nullary.Reflects
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of the `Reflects` construct
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Nullary.Reflects where
+
+open import Agda.Builtin.Equality
+open import Data.Bool.Base
+open import Data.Empty
+open import Level
+open import Relation.Nullary
+
+private
+  variable
+    p : Level
+    P : Set p
+
+------------------------------------------------------------------------
+-- `Reflects P b` is equivalent to `if b then P else ¬ P`.
+
+-- These lemmas are intended to be used mostly when `b` is a value, so
+-- that the `if` expressions have already been evaluated away.
+-- In this case, `of` works like the relevant constructor (`ofⁿ` or
+-- `ofʸ`), and `invert` strips off the constructor to just give either
+-- the proof of `P` or the proof of `¬ P`.
+
+of : ∀ {b} → if b then P else ¬ P → Reflects P b
+of {b = false} ¬p = ofⁿ ¬p
+of {b = true }  p = ofʸ p
+
+invert : ∀ {b} → Reflects P b → if b then P else ¬ P
+invert (ofʸ  p) = p
+invert (ofⁿ ¬p) = ¬p
+
+------------------------------------------------------------------------
+-- Other lemmas
+
+fromEquivalence : ∀ {b} → (T b → P) → (P → T b) → Reflects P b
+fromEquivalence {b = true}  sound complete = ofʸ (sound _)
+fromEquivalence {b = false} sound complete = ofⁿ complete
+
+-- `Reflects` is deterministic.
+det : ∀ {b b′} → Reflects P b → Reflects P b′ → b ≡ b′
+det (ofʸ  p) (ofʸ  p′) = refl
+det (ofʸ  p) (ofⁿ ¬p′) = ⊥-elim (¬p′ p)
+det (ofⁿ ¬p) (ofʸ  p′) = ⊥-elim (¬p p′)
+det (ofⁿ ¬p) (ofⁿ ¬p′) = refl
+
\ No newline at end of file diff --git a/misc/Relation.Nullary.html b/misc/Relation.Nullary.html new file mode 100644 index 0000000..64ab07b --- /dev/null +++ b/misc/Relation.Nullary.html @@ -0,0 +1,72 @@ + +Relation.Nullary
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Operations on nullary relations (like negation and decidability)
+------------------------------------------------------------------------
+
+-- Some operations on/properties of nullary relations, i.e. sets.
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Nullary where
+
+open import Agda.Builtin.Equality
+open import Agda.Builtin.Bool
+
+open import Data.Empty hiding (⊥-elim)
+open import Data.Empty.Irrelevant
+open import Level
+
+------------------------------------------------------------------------
+-- Negation.
+
+infix 3 ¬_
+infix 2 _because_
+
+¬_ : ∀ {ℓ} → Set ℓ → Set ℓ
+¬ P = P → ⊥
+
+------------------------------------------------------------------------
+-- `Reflects` idiom.
+
+-- The truth value of P is reflected by a boolean value.
+
+data Reflects {p} (P : Set p) : Bool → Set p where
+  ofʸ : ( p :   P) → Reflects P true
+  ofⁿ : (¬p : ¬ P) → Reflects P false
+
+------------------------------------------------------------------------
+-- Decidability.
+
+-- Decidability proofs have two parts: the `does` term which contains
+-- the boolean result and the `proof` term which contains a proof that
+-- reflects the boolean result. This definition allows the boolean
+-- part of the decision procedure to compute independently from the
+-- proof. This leads to better computational behaviour when we only care
+-- about the result and not the proof. See README.Decidability for
+-- further details.
+
+record Dec {p} (P : Set p) : Set p where
+  constructor _because_
+  field
+    does  : Bool
+    proof : Reflects P does
+
+open Dec public
+
+pattern yes p =  true because ofʸ  p
+pattern no ¬p = false because ofⁿ ¬p
+
+-- Given an irrelevant proof of a decidable type, a proof can
+-- be recomputed and subsequently used in relevant contexts.
+recompute : ∀ {a} {A : Set a} → Dec A → .A → A
+recompute (yes x) _ = x
+recompute (no ¬p) x = ⊥-elim (¬p x)
+
+------------------------------------------------------------------------
+-- Irrelevant types
+
+Irrelevant : ∀ {p} → Set p → Set p
+Irrelevant P = ∀ (p₁ p₂ : P) → p₁ ≡ p₂
+
\ No newline at end of file diff --git a/misc/Relation.Unary.html b/misc/Relation.Unary.html new file mode 100644 index 0000000..8b7b89f --- /dev/null +++ b/misc/Relation.Unary.html @@ -0,0 +1,299 @@ + +Relation.Unary
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Unary relations
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Relation.Unary where
+
+open import Data.Empty
+open import Data.Unit.Base using (⊤)
+open import Data.Product
+open import Data.Sum.Base using (_⊎_; [_,_])
+open import Function.Base
+open import Level
+open import Relation.Nullary hiding (Irrelevant)
+open import Relation.Nullary.Decidable.Core using (True)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+
+private
+  variable
+    a b c ℓ ℓ₁ ℓ₂ : Level
+    A : Set a
+    B : Set b
+    C : Set c
+
+------------------------------------------------------------------------
+-- Definition
+
+-- Unary relations are known as predicates and `Pred A ℓ` can be viewed
+-- as some property that elements of type A might satisfy.
+
+-- Consequently `P : Pred A ℓ` can also be seen as a subset of A
+-- containing all the elements of A that satisfy property P. This view
+-- informs much of the notation used below.
+
+Pred : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
+Pred A ℓ = A → Set ℓ
+
+------------------------------------------------------------------------
+-- Special sets
+
+-- The empty set.
+
+∅ : Pred A 0ℓ
+∅ = λ _ → ⊥
+
+-- The singleton set.
+
+｛_｝ : A → Pred A _
+｛ x ｝ = x ≡_
+
+-- The universal set.
+
+U : Pred A 0ℓ
+U = λ _ → ⊤
+
+------------------------------------------------------------------------
+-- Membership
+
+infix 4 _∈_ _∉_
+
+_∈_ : A → Pred A ℓ → Set _
+x ∈ P = P x
+
+_∉_ : A → Pred A ℓ → Set _
+x ∉ P = ¬ x ∈ P
+
+------------------------------------------------------------------------
+-- Subset relations
+
+infix 4 _⊆_ _⊇_ _⊈_ _⊉_ _⊂_ _⊃_ _⊄_ _⊅_
+
+_⊆_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊆ Q = ∀ {x} → x ∈ P → x ∈ Q
+
+_⊇_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊇ Q = Q ⊆ P
+
+_⊈_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊈ Q = ¬ (P ⊆ Q)
+
+_⊉_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊉ Q = ¬ (P ⊇ Q)
+
+_⊂_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊂ Q = P ⊆ Q × Q ⊈ P
+
+_⊃_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊃ Q = Q ⊂ P
+
+_⊄_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊄ Q = ¬ (P ⊂ Q)
+
+_⊅_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊅ Q = ¬ (P ⊃ Q)
+
+-- The following primed variants of _⊆_ can be used when 'x' can't
+-- be inferred from 'x ∈ P'.
+
+infix 4 _⊆′_ _⊇′_ _⊈′_ _⊉′_ _⊂′_ _⊃′_ _⊄′_ _⊅′_
+
+_⊆′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊆′ Q = ∀ x → x ∈ P → x ∈ Q
+
+_⊇′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+Q ⊇′ P = P ⊆′ Q
+
+_⊈′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊈′ Q = ¬ (P ⊆′ Q)
+
+_⊉′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊉′ Q = ¬ (P ⊇′ Q)
+
+_⊂′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊂′ Q = P ⊆′ Q × Q ⊈′ P
+
+_⊃′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊃′ Q = Q ⊂′ P
+
+_⊄′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊄′ Q = ¬ (P ⊂′ Q)
+
+_⊅′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ⊅′ Q = ¬ (P ⊃′ Q)
+
+------------------------------------------------------------------------
+-- Properties of sets
+
+infix 10 Satisfiable Universal IUniversal
+
+-- Emptiness - no element satisfies P.
+
+Empty : Pred A ℓ → Set _
+Empty P = ∀ x → x ∉ P
+
+-- Satisfiable - at least one element satisfies P.
+
+Satisfiable : Pred A ℓ → Set _
+Satisfiable P = ∃ λ x → x ∈ P
+
+syntax Satisfiable P = ∃⟨ P ⟩
+
+-- Universality - all elements satisfy P.
+
+Universal : Pred A ℓ → Set _
+Universal P = ∀ x → x ∈ P
+
+syntax Universal  P = Π[ P ]
+
+-- Implicit universality - all elements satisfy P.
+
+IUniversal : Pred A ℓ → Set _
+IUniversal P = ∀ {x} → x ∈ P
+
+syntax IUniversal P = ∀[ P ]
+
+-- Decidability - it is possible to determine if an arbitrary element
+-- satisfies P.
+
+Decidable : Pred A ℓ → Set _
+Decidable P = ∀ x → Dec (P x)
+
+-- Erasure: A decidable predicate gives rise to another one, more
+-- amenable to η-expansion
+
+⌊_⌋ : {P : Pred A ℓ} → Decidable P → Pred A ℓ
+⌊ P? ⌋ a = Lift _ (True (P? a))
+
+-- Irrelevance - any two proofs that an element satifies P are
+-- indistinguishable.
+
+Irrelevant : Pred A ℓ → Set _
+Irrelevant P = ∀ {x} (a : P x) (b : P x) → a ≡ b
+
+-- Recomputability - we can rebuild a relevant proof given an
+-- irrelevant one.
+
+Recomputable : Pred A ℓ → Set _
+Recomputable P = ∀ {x} → .(P x) → P x
+
+------------------------------------------------------------------------
+-- Operations on sets
+
+infix 10 ⋃ ⋂
+infixr 9 _⊢_
+infixr 8 _⇒_
+infixr 7 _∩_
+infixr 6 _∪_
+infix 4 _≬_
+
+-- Complement.
+
+∁ : Pred A ℓ → Pred A ℓ
+∁ P = λ x → x ∉ P
+
+-- Implication.
+
+_⇒_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
+P ⇒ Q = λ x → x ∈ P → x ∈ Q
+
+-- Union.
+
+_∪_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
+P ∪ Q = λ x → x ∈ P ⊎ x ∈ Q
+
+-- Intersection.
+
+_∩_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
+P ∩ Q = λ x → x ∈ P × x ∈ Q
+
+-- Infinitary union.
+
+⋃ : ∀ {i} (I : Set i) → (I → Pred A ℓ) → Pred A _
+⋃ I P = λ x → Σ[ i ∈ I ] P i x
+
+syntax ⋃ I (λ i → P) = ⋃[ i ∶ I ] P
+
+-- Infinitary intersection.
+
+⋂ : ∀ {i} (I : Set i) → (I → Pred A ℓ) → Pred A _
+⋂ I P = λ x → (i : I) → P i x
+
+syntax ⋂ I (λ i → P) = ⋂[ i ∶ I ] P
+
+-- Positive version of non-disjointness, dual to inclusion.
+
+_≬_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
+P ≬ Q = ∃ λ x → x ∈ P × x ∈ Q
+
+-- Update.
+
+_⊢_ : (A → B) → Pred B ℓ → Pred A ℓ
+f ⊢ P = λ x → P (f x)
+
+------------------------------------------------------------------------
+-- Predicate combinators
+
+-- These differ from the set operations above, as the carrier set of the
+-- resulting predicates are not the same as the carrier set of the
+-- component predicates.
+
+infixr  2 _⟨×⟩_
+infixr  2 _⟨⊙⟩_
+infixr  1 _⟨⊎⟩_
+infixr  0 _⟨→⟩_
+infixl  9 _⟨·⟩_
+infix  10 _~
+infixr  9 _⟨∘⟩_
+infixr  2 _//_ _\\_
+
+-- Product.
+
+_⟨×⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A × B) _
+(P ⟨×⟩ Q) (x , y) = x ∈ P × y ∈ Q
+
+-- Sum over one element.
+
+_⟨⊎⟩_ : Pred A ℓ → Pred B ℓ → Pred (A ⊎ B) _
+P ⟨⊎⟩ Q = [ P , Q ]
+
+-- Sum over two elements.
+
+_⟨⊙⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A × B) _
+(P ⟨⊙⟩ Q) (x , y) = x ∈ P ⊎ y ∈ Q
+
+-- Implication.
+
+_⟨→⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A → B) _
+(P ⟨→⟩ Q) f = P ⊆ Q ∘ f
+
+-- Product.
+
+_⟨·⟩_ : (P : Pred A ℓ₁) (Q : Pred B ℓ₂) →
+        (P ⟨×⟩ (P ⟨→⟩ Q)) ⊆ Q ∘ uncurry (flip _$_)
+(P ⟨·⟩ Q) (p , f) = f p
+
+-- Converse.
+
+_~ : Pred (A × B) ℓ → Pred (B × A) ℓ
+P ~ = P ∘ swap
+
+-- Composition.
+
+_⟨∘⟩_ : Pred (A × B) ℓ₁ → Pred (B × C) ℓ₂ → Pred (A × C) _
+(P ⟨∘⟩ Q) (x , z) = ∃ λ y → (x , y) ∈ P × (y , z) ∈ Q
+
+-- Post-division.
+
+_//_ : Pred (A × C) ℓ₁ → Pred (B × C) ℓ₂ → Pred (A × B) _
+(P // Q) (x , y) = Q ∘ (y ,_) ⊆ P ∘ (x ,_)
+
+-- Pre-division.
+
+_\\_ : Pred (A × C) ℓ₁ → Pred (A × B) ℓ₂ → Pred (B × C) _
+P \\ Q = (P ~ // Q ~) ~
+
\ No newline at end of file diff --git a/misc/Strict.html b/misc/Strict.html new file mode 100644 index 0000000..244a7ad --- /dev/null +++ b/misc/Strict.html @@ -0,0 +1,33 @@ + +Strict
------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Strictness combinators
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Strict where
+
+open import Level
+open import Agda.Builtin.Equality
+
+open import Agda.Builtin.Strict
+     renaming ( primForce to force
+              ; primForceLemma to force-≡) public
+
+-- Derived combinators
+module _ {ℓ ℓ′ : Level} {A : Set ℓ} {B : Set ℓ′} where
+
+  force′ : A → (A → B) → B
+  force′ = force
+
+  force′-≡ : (a : A) (f : A → B) → force′ a f ≡ f a
+  force′-≡ = force-≡
+
+  seq : A → B → B
+  seq a b = force a (λ _ → b)
+
+  seq-≡ : (a : A) (b : B) → seq a b ≡ b
+  seq-≡ a b = force-≡ a (λ _ → b)
+
\ No newline at end of file diff --git a/misc/wlpo.html b/misc/wlpo.html new file mode 100644 index 0000000..35761c5 --- /dev/null +++ b/misc/wlpo.html @@ -0,0 +1,111 @@ + +wlpo
{-# OPTIONS --safe --without-K #-}
+
+open import Agda.Primitive renaming (Set to 𝒰)
+open import Agda.Builtin.Nat renaming (Nat to ℕ) hiding (_+_)
+open import Agda.Builtin.Bool renaming (Bool to 𝟚; false to 𝟘; true to 𝟙)
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import Function using (_∘_; const)
+
+{- Variables -}
+variable
+  ₙ : Level
+  ₘ : Level
+  A : 𝒰 ₙ
+  B : 𝒰 ₙ
+  C : 𝒰 ₙ
+
+{- Types -}
+
+data ⊥ : 𝒰₀ where
+
+infixr 8 ¬_
+¬_ : 𝒰 ₙ → 𝒰 ₙ
+¬ p = p → ⊥
+
+infixr 2 _+_
+data _+_ (A : 𝒰 ₙ) (B : 𝒰 ₘ) : 𝒰 (ₙ ⊔ ₘ) where
+  inl : A → A + B
+  inr : B → A + B
+
+binary-sequence : 𝒰₀
+binary-sequence = ℕ → 𝟚  
+
+all-zeros : binary-sequence → 𝒰₀
+all-zeros α = (n : ℕ) → α n ≡ 𝟘
+
+has-WLPO : binary-sequence → 𝒰₀
+has-WLPO α = all-zeros α + ¬ (all-zeros α)   
+
+WLPO : 𝒰₀
+WLPO = (α : binary-sequence) → has-WLPO α   
+
+at-most-one-one : binary-sequence → 𝒰₀
+at-most-one-one α = (a b : ℕ) → α a ≡ 𝟙 → α b ≡ 𝟙 → a ≡ b
+
+-- needed for LLPO
+dup : ℕ → ℕ
+dup 0 = 0
+dup (suc n) = suc (suc (dup n))
+
+evens : ℕ → ℕ
+evens = dup
+
+odds : ℕ → ℕ
+odds = suc ∘ dup
+
+LLPO : 𝒰₀
+LLPO = (α : binary-sequence) → at-most-one-one α → all-zeros (α ∘ evens) + all-zeros (α ∘ odds)
+
+{- Eliminators -}
+⊥-elim : ⊥ → A
+⊥-elim ()
+
++-elim : A + B → (A → C) → (B → C) → C
++-elim (inl a) f _ = f a
++-elim (inr b) _ g = g b
+
+-- A bit funky, but comes in handy
+𝟚-elim : (C : 𝟚 → 𝒰 ₙ) → (b : 𝟚) → (b ≡ 𝟘 → C 𝟘) → (b ≡ 𝟙 → C 𝟙) → C b
+𝟚-elim _ 𝟘 z _ = z refl
+𝟚-elim _ 𝟙 _ o = o refl
+
+{- Lemmas -}
+
+-- I think this is a bit ugly, but it works and I'm tired
+e≢o : {n m : ℕ} → ¬ (evens n ≡ odds m)
+e≢o {zero} {zero} ()
+e≢o {zero} {suc m} ()
+e≢o {suc n} {zero} ()
+e≢o {suc n} {suc m} p = e≢o {n} {m} (ds (tr (he n) (ho m) p))
+  where
+    he : (q : ℕ) → evens (suc q) ≡ suc (suc (evens q))
+    he _ = refl
+
+    ho : (q : ℕ) → odds (suc q) ≡ suc (suc (odds q))
+    ho _ = refl
+
+    tr : ∀ {a b c d : ℕ} → a ≡ b → c ≡ d → a ≡ c → b ≡ d
+    tr refl refl refl = refl
+
+    ds : ∀ {q r : ℕ} → suc (suc q) ≡ suc (suc r) → q ≡ r
+    ds {zero} {zero} _ = refl
+    ds {suc q} {suc r} refl = refl
+
+
+lemma : (α : binary-sequence) → at-most-one-one α → ¬ all-zeros (α ∘ evens) → all-zeros (α ∘ odds)
+lemma α am11 na0e i = 𝟚-elim (_≡ 𝟘) ((α ∘ odds) i)
+                             (const refl)
+                             (λ p₁ → ⊥-elim (na0e (λ j → 𝟚-elim (_≡ 𝟘) ((α ∘ evens) j)
+                                                                (const refl)
+                                                                (λ p₂ → ⊥-elim (e≢o (am11 (evens j) (odds i) p₂ p₁))))))
+
+
+{- The main dish -}
+WLPO→LLPO : WLPO → LLPO
+WLPO→LLPO wlpo α am11 = +-elim (wlpo (α ∘ evens))
+                              inl
+                              (λ na0e → +-elim (wlpo (α ∘ odds))
+                                               inr
+                                               (λ na0o → ⊥-elim (na0o (lemma α am11 na0e))))
+
\ No newline at end of file