text:
{-# OPTIONS --cubical-compatible #-}

postulate w/e : Set

data _==_ {A : Set} : A → A → Set where
  idp : {a : A} → a == a

data Square {A : Set} {a : A} : {b c d : A} (p : a == b) (q : c == d) (r : a == c) (s : b == d) → Set where
  ids : Square {a = a} idp idp idp idp

J1 : {A : Set} {a : A} {p : a == a} → Square p idp idp idp → Set
J1 ids = w/e

J2 : {A : Set} {a : A} {p : a == a} → Square idp p idp idp → Set
J2 ids = w/e

J3 : {A : Set} {a : A} {p : a == a} → Square idp idp p idp → Set
J3 ids = w/e

J4 : {A : Set} {a : A} {p : a == a} → Square idp idp idp p → Set
J4 ids = w/e


text:
{-# OPTIONS --cubical --no-import-sorts #-}

module SpacesFirstAttempt where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

private
  variable
    ℓ ℓ' ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Relation.Binary.Base -- Rel
open import Data.Nat.Base using (ℕ) renaming (_≤_ to _≤ₙ_)

record PoorField : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    Carrier : Type ℓ
    -- comm ring
    0f   : Carrier
    1f   : Carrier
    _+_  : Carrier → Carrier → Carrier
    _·_  : Carrier → Carrier → Carrier
    -_   : Carrier → Carrier
    -- lattice
    _<_  : Rel Carrier Carrier ℓ' -- stronger than _#_ and _≤_
    min  : Carrier → Carrier → Carrier
    max  : Carrier → Carrier → Carrier
    -- other
    _#_  : Rel Carrier Carrier ℓ'
    _≤_  : Rel Carrier Carrier ℓ'
    ∣_∣ᶠ' : Carrier → Σ[ x ∈ Carrier ] 0f ≤ x -- absolute value
    _⁻¹ᶠ : (x : Carrier) → {{x # 0f}} → Carrier
    conj : Carrier → Carrier -- complex conjugation (only for ℂ; this is the identity function on ℝ)
    -- sqrt -- need that on ℝ₀⁺ to define a norm from an inner product

  ∣_∣ᶠ : Carrier → Carrier -- NOTE: well, this should be "into" ℝ₀⁺
  ∣ x ∣ᶠ = fst (∣ x ∣ᶠ')

  _-_ : Carrier → Carrier → Carrier
  x - y = x + (- y)

  infix  9 _⁻¹ᶠ
  infix  8 -_
  infixl 7 _·_
  infixl 6 _+_
  infixl 6 _-_
  infixl 4 _#_
  infixl 4 _<_
  infixl 4 _≤_

-- different "variants" of reals
--   this might be a "basis" for an instance-based, typeclass-like coercion "mechanism" between different "numbers"
--
-- NOTE: the intuition with "variants" might align with "subset" where different properties are available
--       from a "subset" in this manner, we want that it is "easy" to
--       - make use of properties from the "full" set
--         - this might be realized with an abuse of Agda's record-update syntax
--         - the "core" of such a mechanism is to have a proper naming-scheme (because record-update basically just matches names)
--       - "spontaneously enrich" some current context with a subset proof
--         and then make use of the subset lemmas on elements of the "whole" set

{- IDEA: for the organization of these definitions

we might have some "ur"-reals
  these are "the" "numbers"
or even better: just "ur-numbers" to support functions from 𝕂 into ℝ₀⁺
being part of some concrete number type is attached via a hidden instance-proof property
  this should be similar to a typeclass mechanism in Coq or Isabelle/HOL
  TODO: maybe, when re-reading their papers, it becomes apparent that this is how it's done in Hölzl 2013 and the Coq-Port of their work
    because I remember them writing something like "this work makes heavy use of typeclasses"
so we explicitly quantify over "numbers" and implicitly quantify over "properties"
the available properties must have the same name in each different number type
  that way we can make use of Agda's record update syntax
  (well, there can be exceptions since it is possible to rename stuff on the fly, but it'd be more convenient if the names already match)
we might decide NOT (!) to overload operations such as _<_ and similar
  because having both overloaded - operations and numbers - is likely to generate resolving issues
AND we must be very aware when a type depends on a hidden argument
  because in that case, we need to add an explicit coercion to our result
  so we just accept that "inconvenience" and embrace a style where these "important" arguments/instances are treated differently
    especially they should not be used anonymously
    and this might also embrace an anonymous-module style to create a scope that is shared by both: the declaration and the definition of something
      This might look ugly at first but that's okay if it works out

-}

record IsℝField (PF : PoorField {ℓ} {ℓ'}) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  open PoorField PF

record Isℝ₀⁺Field (PF : PoorField {ℓ} {ℓ'}) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  open PoorField PF
  field
    isℝField : IsℝField PF
    isNonnegative : ∀ x → 0f ≤ x
  open IsℝField isℝField public

record Isℝ⁺Field (PF : PoorField {ℓ} {ℓ'}) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  open PoorField PF
  field
    isℝField : IsℝField PF
    -- NOTE: 0f is not an element of ℝ⁺, so we do not have a neutral element for addition
    --       so the following holds in a different way
    -- isPositive : ∀ x → 0f < x
  open IsℝField isℝField public

record Is𝕂Field (PF : PoorField {ℓ} {ℓ'}) : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  open PoorField PF

record ℝField : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    poorField : PoorField {ℓ} {ℓ'}
    isℝField : IsℝField poorField
  open PoorField poorField public
  open IsℝField isℝField public

record ℝ₀⁺Field : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    poorField : PoorField {ℓ} {ℓ'}
    isℝ₀⁺Field : Isℝ₀⁺Field poorField
  open PoorField poorField public
  open Isℝ₀⁺Field isℝ₀⁺Field public

record ℝ⁺Field : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    poorField : PoorField {ℓ} {ℓ'}
    isℝ⁺Field : Isℝ⁺Field poorField
  open PoorField poorField public
  open Isℝ⁺Field isℝ⁺Field public

record 𝕂Field : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
  field
    poorField : PoorField {ℓ} {ℓ'}
    is𝕂Field : Is𝕂Field poorField
  open PoorField poorField public
  open Is𝕂Field is𝕂Field public

postulate
  ℝℓ ℝℓ' : Level
  ℝF    : ℝField   {ℝℓ} {ℝℓ'} -- reals
  ℝ⁺F   : ℝ⁺Field  {ℝℓ} {ℝℓ'} -- positive reals without 0
  ℝ₀⁺F  : ℝ₀⁺Field {ℝℓ} {ℝℓ'} -- positive reals with 0
  -- we also often use ℂ in the application
  -- we might often use ℝ in places where ℚ would suffice
  -- we use 𝕂 for "ℝ or ℂ"
  -- and we use ℕ, Fin k, ℤ of course
  -- then, there is (exterior) algebra

-- NOTE: one could bring different "variants" of the reals into scope like so
--       but we are likely to omit populating the scope with overlapping reals as much as possible

open ℝField ℝF using () renaming
  ( Carrier to ℝ
  )

open ℝ₀⁺Field ℝ₀⁺F using () renaming
  ( Carrier to ℝ₀⁺
  ; 0f to 0f₀⁺
  )

open ℝ⁺Field ℝ⁺F using () renaming
  ( Carrier to ℝ⁺
  )

---------- application -------------

{-
-- ∅ : ⊥ →

-- topology on a set X
record IsTopology
  (X : Type ℓ)
  (isOpen : X → Type ℓ')
  (_∪_ : X → X → X)
  (_∩_ : X → X → X)
  : Type _ where
  field

record TopologicalSpace : Type _ where
-}

record IsMetric {ℓ} {X : Type ℓ} (d : X → X → ℝ₀⁺) : Type (ℓ-max ℓ (ℓ-max ℝℓ ℝℓ')) where
  open ℝ₀⁺Field ℝ₀⁺F
  field
    -- identity of indiscernibles
    isPositiveOnNonzero      : ∀ x y → 0f ≡ d x y → x ≡ y
    isPositiveOnNonzero-back : ∀ x y → x ≡ y → 0f ≡ d x y
    isSym                    : ∀ x y → d x y ≡ d y x
    -- subadditivity / triangle inequality
    isTriangleIneq           : ∀ x y z → d x y ≤ d x z + d z y

record MetricSpace : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max ℝℓ' ℝℓ)) where
  field
    Carrier  : Type ℓ
    d        : Carrier → Carrier → ℝ₀⁺
    isMetric : IsMetric d
  open IsMetric isMetric public

𝕂ℓ  = ℝℓ
𝕂ℓ' = ℝℓ'

module _ (𝕂F : 𝕂Field {𝕂ℓ} {𝕂ℓ'}) where
  open 𝕂Field 𝕂F renaming (Carrier to 𝕂; 0f to 0ₛ; _+_ to _+ₛ_)
  postulate
    ∣_∣ᵣ : 𝕂 → ℝ₀⁺
  record IsVectorAddition {X : Type ℓ} (0v : X) (_+_ : X → X → X) (-_ : X → X) : Type (ℓ-max ℓ (ℓ-max 𝕂ℓ 𝕂ℓ')) where
    field
      isCommutative : ∀ x y → x + y ≡ y + x
      isAssociative : ∀ x y z → (x + y) + z ≡ x + (y + z)
      rid           : ∀ x → x + 0v ≡ x
      rid-back      : ∀ x y → x + y ≡ x → y ≡ 0v
      invr          : ∀ x → x + (- x) ≡ 0v

  record IsScalarMultiplication {X : Type ℓ} (0v : X) (_+_ : X → X → X) (-_ : X → X) (_·ₛ_ : 𝕂 → X → X) : Type (ℓ-max ℓ (ℓ-max 𝕂ℓ 𝕂ℓ')) where
    field
      ·ₛ-dist-+ : ∀ α x y → α ·ₛ (x + y) ≡ (α ·ₛ x) + (α ·ₛ y)
      0-left-nullifies : ∀ x → 0ₛ ·ₛ x ≡ 0v
      +ₛ-dist-· : ∀ α β x → (α +ₛ β) ·ₛ x ≡ (α ·ₛ x) + (β ·ₛ x)

  record VectorSpace : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max 𝕂ℓ 𝕂ℓ')) where
    field
      Carrier : Type ℓ
      0v      : Carrier
      _+_     : Carrier → Carrier → Carrier
      -_      : Carrier → Carrier
      _·ₛ_    : 𝕂 → Carrier → Carrier
      isVectorAddition : IsVectorAddition 0v _+_ (-_)
      isScalarMultiplication : IsScalarMultiplication 0v _+_ -_ _·ₛ_

    open IsVectorAddition isVectorAddition public
    open IsScalarMultiplication isScalarMultiplication public

  module _ (VS : VectorSpace {ℓ}) where
    open VectorSpace VS using (_+_; _·ₛ_) renaming (Carrier to V; 0v to 0ᵥ)
    open ℝ₀⁺Field ℝ₀⁺F using () renaming (0f to 0ᵣ; _≤_ to _≤ᵣ_; _+_ to _+ᵣ_; _·_ to _·ᵣ_)
    record IsNorm (‖_‖ᵥ : V → ℝ₀⁺) : Type (ℓ-max ℓ (ℓ-max 𝕂ℓ 𝕂ℓ')) where
      field
        idToIndisc      : ∀ x → ‖ x ‖ᵥ ≡ 0ᵣ → x ≡ 0ᵥ
        idToIndisc-back : ∀ x → x ≡ 0ᵥ → ‖ x ‖ᵥ ≡ 0ᵣ
        triangleIneq    : ∀ x y → ‖ x + y ‖ᵥ ≤ᵣ ‖ x ‖ᵥ +ᵣ ‖ y ‖ᵥ
        absLinear       : ∀ α x → ‖ α ·ₛ x ‖ᵥ ≡ ∣ α ∣ᵣ ·ᵣ ‖ x ‖ᵥ

  record NormedVectorSpace : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max 𝕂ℓ 𝕂ℓ')) where
    field
      VS : VectorSpace {ℓ}
    open VectorSpace VS public
    field
      ‖_‖ᵥ : Carrier → ℝ₀⁺
      isNorm : IsNorm VS ‖_‖ᵥ
    open IsNorm isNorm public

-- cauchy w.r.t. a distance function
-- NOTE: Booij defines cauchy w.r.t. the rationals ℚ

IsCauchy : {X : Type ℓ} (d : X → X → ℝ₀⁺) → IsMetric d → (x : ℕ → X) → Type (ℓ-max ℝℓ ℝℓ')
IsCauchy d isMetric x =
  let open ℝ₀⁺Field ℝ₀⁺F using () renaming (0f to 0ᵣ; _<_ to _<ᵣ_; _≤_ to _≤ᵣ_; _+_ to _+ᵣ_; _·_ to _·ᵣ_)
  in ∀(ε : ℝ₀⁺) → 0ᵣ <ᵣ ε → Σ[ I ∈ ℕ ] ∀ m n → I ≤ₙ m → I ≤ₙ n → d (x m) (x n) <ᵣ ε

-- limit w.r.t. a metric
IsLimit : {X : Type ℓ} {d : X → X → ℝ₀⁺} → (isMetric : IsMetric d) → (x : ℕ → X) → X → Type (ℓ-max ℝℓ ℝℓ')
IsLimit {d = d} isMetric x a =
  let open ℝ₀⁺Field ℝ₀⁺F using () renaming (0f to 0ᵣ; _<_ to _<ᵣ_; _≤_ to _≤ᵣ_; _+_ to _+ᵣ_; _·_ to _·ᵣ_)
  in ∀(ε : ℝ₀⁺) → 0ᵣ <ᵣ ε → Σ[ I ∈ ℕ ] ∀ m → I ≤ₙ m → d (x m) a <ᵣ ε

IsCauchyConvergent : {X : Type ℓ} (d : X → X → ℝ₀⁺) → (isMetric : IsMetric d) → (x : ℕ → X) → IsCauchy d isMetric x → Type (ℓ-max ℓ (ℓ-max ℝℓ ℝℓ'))
IsCauchyConvergent {X = X} d isMetric x isCauchy = Σ[ a ∈ X ] IsLimit isMetric x a

record CompleteMetricSpace : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max ℝℓ' ℝℓ)) where
  field
    MS : MetricSpace {ℓ}

  open MetricSpace MS public

  field
    isCauchyComplete : ∀ x → (isCauchy : IsCauchy d isMetric x) → Σ[ a ∈ Carrier ] IsLimit isMetric x a

module Lemma-1 (𝕂F : 𝕂Field {𝕂ℓ} {𝕂ℓ'}) (NVS : NormedVectorSpace 𝕂F {ℓ}) where
  open NormedVectorSpace NVS renaming (Carrier to V)
  open ℝ₀⁺Field ℝ₀⁺F using () renaming (_≤_ to _≤ᵣ_; _+_ to _+ᵣ_)

  d : V → V → ℝ₀⁺
  d x y = ‖ x + (- y) ‖ᵥ

  lemma-1 : IsMetric d
  lemma-1 = record
    { isPositiveOnNonzero      = {!!}
    ; isPositiveOnNonzero-back = {!!}
    ; isSym                    = {! λ x y → ?!}
    ; isTriangleIneq           = {!!}
    }

  IsNormMetric : (V → V → ℝ₀⁺) → Type (ℓ-max ℓ ℝℓ)
  IsNormMetric d' = ∀ x y → d' x y ≡ d x y

module _ (𝕂F : 𝕂Field {𝕂ℓ} {𝕂ℓ'}) where
  record CompleteNormedVectorSpace : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max 𝕂ℓ' 𝕂ℓ)) where
    field
      NVS : NormedVectorSpace 𝕂F {ℓ}

    open NormedVectorSpace NVS public

    d : Carrier → Carrier → ℝ₀⁺
    d x y = ‖ x + (- y) ‖ᵥ

    isMetric : IsMetric d
    isMetric = Lemma-1.lemma-1 𝕂F NVS

    field
      isCauchyComplete : ∀ x → (isCauchy : IsCauchy d isMetric x) → Σ[ a ∈ Carrier ] IsLimit isMetric x a

  BanachSpace = CompleteNormedVectorSpace

module _ (𝕂F : 𝕂Field {𝕂ℓ} {𝕂ℓ'}) (VS : VectorSpace 𝕂F {ℓ}) where
  open 𝕂Field 𝕂F using (conj) renaming (Carrier to 𝕂; _·_ to _·ₖ_; _+_ to _+ₖ_)
  open VectorSpace VS renaming (Carrier to V)

  record IsInnerProduct (‹_,_›ᵥ : V → V → 𝕂) : Type (ℓ-max ℓ (ℓ-max 𝕂ℓ' 𝕂ℓ)) where
    field
      -- pos-definite : ∀ x → x ≠ 0v → ‹ x , x › ∈ ℝ⁺ -- TODO
      conj-sym  : ∀ x y → ‹ x , y ›ᵥ ≡ conj (‹ y , x ›ᵥ)
      lin₁      : ∀ α x y → ‹ α ·ₛ x , y ›ᵥ ≡ α ·ₖ ‹ x , y ›ᵥ
      +distrib₁ : ∀ x y z → ‹ x + y , z ›ᵥ ≡ ‹ x , z ›ᵥ +ₖ ‹ y , z ›ᵥ

  -- If the positive-definite condition is replaced by merely requiring that ⟨ x , x ⟩ ≥ 0 for all x,
  --   then one obtains the definition of positive semi-definite Hermitian form.

module _ (𝕂F : 𝕂Field {𝕂ℓ} {𝕂ℓ'}) where
  open 𝕂Field 𝕂F using (conj) renaming (Carrier to 𝕂; _·_ to _·ₖ_; _+_ to _+ₖ_)

  record InnerProductSpace : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max 𝕂ℓ' 𝕂ℓ)) where
    field
      VS : VectorSpace 𝕂F {ℓ}
    open VectorSpace VS public
    field
      ‹_,_›ᵥ : Carrier → Carrier → 𝕂
      isInnerProduct : IsInnerProduct 𝕂F VS ‹_,_›ᵥ
    open IsInnerProduct isInnerProduct public

    -- ‖_‖ᵥ : Carrier →  ℝ₀⁺
    -- ‖ x ‖ᵥ = sqrt (‹ x , x ›ᵥ)

    -- isNorm : IsNorm VS ‖_‖ᵥ
    -- isNorm = ?

    -- d : Carrier → Carrier → ℝ₀⁺
    -- d x y = ‖ x + (- y) ‖ᵥ

    -- isMetric : IsMetric d
    -- isMetric = Lemma-1.lemma-1 𝕂F NVS

  -- NOTE: there are a lot of properties for InnerProductSpaces: https://en.wikipedia.org/wiki/Inner_product_space#Norm

  record HilbertSpace : Type (ℓ-max (ℓ-suc ℓ) (ℓ-max 𝕂ℓ' 𝕂ℓ)) where
    field
      VS : VectorSpace 𝕂F {ℓ}
    open VectorSpace VS public

    field
      ‹_,_›ᵥ : Carrier → Carrier → 𝕂
      isInnerProduct : IsInnerProduct 𝕂F VS ‹_,_›ᵥ
    open IsInnerProduct isInnerProduct public

    -- ‖_‖ᵥ : Carrier →  ℝ₀⁺
    -- ‖ x ‖ᵥ = sqrt (‹ x , x ›ᵥ)

    -- isNorm : IsNorm VS ‖_‖ᵥ
    -- isNorm = ?

    -- d : Carrier → Carrier → ℝ₀⁺
    -- d x y = ‖ x + (- y) ‖ᵥ

    -- isMetric : IsMetric d
    -- isMetric = Lemma-1.lemma-1 𝕂F NVS

    -- field
    --   isCauchyComplete : ∀ x → (isCauchy : IsCauchy d isMetric x) → Σ[ a ∈ Carrier ] IsLimit isMetric x a

-- NOTE:
--   we observe that stronger structure "replaces" weaker structure in the sequence
--     InnerProductSpace < NormedVectorSpace < MetricSpace
--   when we add Cauchy completeness, we get
--     HilbertSpace < BanachSpace < CompleteMetricSpace

-- next up: EuclideanSpace ?
--   see "Hölzl, Immler, Huffman 2013 - Type Classes and Filters for Mathematical Analysis in Isabelle/HOL"
--   here, they start with topological spaces, where we start with the real numbers

-- what about subspaces? How to formulate these?

{-

observed issues
- subspaces
- inclusions/coercions between different variants of "numbers"
- conj
- sqrt
- topological spaces (do we need them after all?)
  - can we follow "Hölzl 2013" ?
- size issues:
  the "amount" of ℓs is "high" and we are not ℓ-suc-ing to 𝕂ℓ and 𝕂ℓ'
  but we are ℓ-suc-ing to ℓ in the definition of PoorField
  so PoorField cannot be in ℓ-zero
- is IsCauchy defined for ε ∈ ℚ or for ε ∈ ℝ ?

in `Cubical.Data.Fin.Base` is written

  Finite types.

  Currently it is most convenient to define these as a subtype of the
  natural numbers, because indexed inductive definitions don't behave
  well with cubical Agda. This definition also has some more general
  attractive properties, of course, such as easy conversion back to ℕ.

and then they state

  Fin : ℕ → Type₀
  Fin n = Σ[ k ∈ ℕ ] k < n

so Σ[ x ∈ 𝕏 ] (P x) kind of falls under what is called a "subtype"

next-up
- infimum and supremum on posets (and sub-posets / sub-lattices ?)
  - we do only really need these on ℝ
  - these do not necessarily exist in the subspace that we regard
- morphisms on these spaces
- (potentially) unbounded linear operators
- algebraic and continuous dual spaces
- Formulation of Riesz representation Theorem on Hilbert spaces

-}

ext: agda

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
open import Relation.Binary.Core

module Order.Total  {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)  where

open import Data.Sum

refl≤ : {x : A} → x ≤ x
refl≤ {x}
    with tot≤ x x
... | inj₁ x≤x = x≤x
... | inj₂ x≤x = x≤x

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module hott.topology.loopspace.theorems where

open import hott.core
open import hott.core.theorems

open import hott.topology.loopspace.eckmann-hilton public

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
module Data.Int.Literal where

open import Data.Nat using (ℕ)
open import Level using (suc)

record Negative {a} (A : Set a) : Set (suc a) where
  field
    Constraint : ℕ → Set a
    fromNeg : (n : ℕ) → ⦃ Constraint n ⦄ → A

open Negative {{...}} public using (fromNeg)
{-# BUILTIN FROMNEG fromNeg #-}

max_stars_repo_name: brunoczim/Celeste

max_issues_repo_name: brunoczim/Celeste

max_forks_repo_name: brunoczim/Celeste


text:
{-# OPTIONS --prop --cubical-compatible #-}

data _≡_ {A : Set} (x : A) : A → Prop where
  refl : x ≡ x


text:
------------------------------------------------------------------------
-- A type for values that should be erased at run-time
------------------------------------------------------------------------

-- This module contains some basic definitions with few dependencies
-- (in particular, not Function-universe) that do not rely on
-- equality. See Erased and other modules under Erased for more
-- definitions. The definitions below are reexported from Erased.

{-# OPTIONS --without-K --safe #-}

module Erased.Basics where

open import Prelude

private
  variable
    a p q : Level

-- Erased A is like A, but the values are (supposed to be) erased at
-- run-time.

record Erased (@0 A : Type a) : Type a where
  constructor [_]
  field
    @0 erased : A

open Erased public

-- A variant of [_] that does not take an erased argument.

[_]→ : {@0 A : Type a} → A → Erased A
[ x ]→ = [ x ]

-- A variant of [_]→.

[_∣_]→ : (@0 A : Type a) → A → Erased A
[_∣_]→ _ = [_]→

-- Erased preserves dependent functions.

map :
  {@0 A : Type a} {@0 P : A → Type p} →
  @0 ((x : A) → P x) → (x : Erased A) → Erased (P (erased x))
map f [ x ] = [ f x ]

-- A binary variant of map.

zip :
  {@0 A : Type a} {@0 P : A → Type p} {@0 Q : {x : A} → P x → Type q} →
  @0 ((x : A) (p : P x) → Q p) →
  (([ x ]) : Erased A) (([ p ]) : Erased (P x)) → Erased (Q p)
zip f [ x ] [ p ] = [ f x p ]

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
{-# OPTIONS --without-K #-}

{-
Imports everything that is not imported by something else.
This is not supposed to be used anywhere, this is just a simple way to
do `make all'

This file is intentionally named index.agda so that
Agda will generate index.html.
-}

module index where

-- import Spaces.IntervalProps

-- import Algebra.F2NotCommutative

import homotopy.LoopSpaceCircle

import homotopy.HopfJunior
import homotopy.Hopf

-- cohomology
import cohomology.EMModel
import cohomology.Torus

import homotopy.SpaceFromGroups

import homotopy.CoverClassification
import homotopy.AnyUniversalCoverIsPathSet
import homotopy.PathSetIsInital

-- import Spaces.LoopSpaceDecidableWedgeCircles

-- import Homotopy.PullbackIsPullback

-- import Homotopy.PushoutIsPushout

-- import Homotopy.Truncation

-- import Sets.QuotientUP

import homotopy.PinSn

-- import Homotopy.VanKampen

import cw.CW
import cw.Sphere
import cw.Degree

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module Groups.Symm.S3 where

open import Equality

------------------------------------------------------------------------
-- definitions

bin-op : ∀ {a} (A : Set a) → Set a
bin-op A = A → A → A

------------------------------------------------------------------------
-- internal stuffs

private

  record S₃ {a} (A : Set a) : Set a where
    constructor ⟨_,_,_⟩-⟨_,_,_⟩-⟨_,_,_⟩
    infixl 5 _×_
    field
      x y {e} : A
      _×_ : bin-op A
      assoc : ∀ a b c → a × b × c ≡ a × (b × c)
      idₗ : ∀ n → n × e ≡ n
      idᵣ : ∀ n → e × n ≡ n
      law-xxx=e : x × x × x ≡ e
      law-yy=e : y × y ≡ e
      law-yx=xxy : y × x ≡ x × x × y

    law-xyx=y : Set a
    law-xyx=y = x × y × x ≡ y

    xyx=y : law-xyx=y
    xyx=y
      rewrite assoc x y x
            | law-yx=xxy
            | sym (assoc x (x × x) y)
            | sym (assoc x x x)
            | law-xxx=e
              = idᵣ y

------------------------------------------------------------------------
-- public aliases

s3-property-1 : ∀ {a} (A : S₃ (Set a)) → S₃.law-xyx=y A
s3-property-1 = S₃.xyx=y


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Order-theoretic lattices
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Relation.Binary.Lattice where

open import Algebra.FunctionProperties
open import Data.Product using (_×_; _,_)
open import Function using (flip)
open import Level using (suc; _⊔_)
open import Relation.Binary

------------------------------------------------------------------------
-- Relationships between orders and operators

open import Relation.Binary public using (Maximum; Minimum)

Supremum : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Op₂ A → Set _
Supremum _≤_ _∨_ =
  ∀ x y → x ≤ (x ∨ y) × y ≤ (x ∨ y) × ∀ z → x ≤ z → y ≤ z → (x ∨ y) ≤ z

Infimum : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Op₂ A → Set _
Infimum _≤_ = Supremum (flip _≤_)

Exponential : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Op₂ A → Op₂ A → Set _
Exponential _≤_ _∧_ _⇨_ =
  ∀ w x y → ((w ∧ x) ≤ y → w ≤ (x ⇨ y)) × (w ≤ (x ⇨ y) → (w ∧ x) ≤ y)

------------------------------------------------------------------------
-- Join semilattices

record IsJoinSemilattice {a ℓ₁ ℓ₂} {A : Set a}
                         (_≈_ : Rel A ℓ₁) -- The underlying equality.
                         (_≤_ : Rel A ℓ₂) -- The partial order.
                         (_∨_ : Op₂ A)    -- The join operation.
                         : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isPartialOrder : IsPartialOrder _≈_ _≤_
    supremum       : Supremum _≤_ _∨_

  x≤x∨y : ∀ x y → x ≤ (x ∨ y)
  x≤x∨y x y = let pf , _ , _ = supremum x y in pf

  y≤x∨y : ∀ x y → y ≤ (x ∨ y)
  y≤x∨y x y = let _ , pf , _ = supremum x y in pf

  ∨-least : ∀ {x y z} → x ≤ z → y ≤ z → (x ∨ y) ≤ z
  ∨-least {x} {y} {z} = let _ , _ , pf = supremum x y in pf z

  open IsPartialOrder isPartialOrder public

record JoinSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixr 6 _∨_
  field
    Carrier           : Set c
    _≈_               : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_               : Rel Carrier ℓ₂  -- The partial order.
    _∨_               : Op₂ Carrier     -- The join operation.
    isJoinSemilattice : IsJoinSemilattice _≈_ _≤_ _∨_

  open IsJoinSemilattice isJoinSemilattice public

  poset : Poset c ℓ₁ ℓ₂
  poset = record { isPartialOrder = isPartialOrder }

  open Poset poset public using (preorder)

record IsBoundedJoinSemilattice {a ℓ₁ ℓ₂} {A : Set a}
                                (_≈_ : Rel A ℓ₁) -- The underlying equality.
                                (_≤_ : Rel A ℓ₂) -- The partial order.
                                (_∨_ : Op₂ A)    -- The join operation.
                                (⊥   : A)        -- The minimum.
                                : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isJoinSemilattice : IsJoinSemilattice _≈_ _≤_ _∨_
    minimum           : Minimum _≤_ ⊥

  open IsJoinSemilattice isJoinSemilattice public

record BoundedJoinSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixr 6 _∨_
  field
    Carrier                  : Set c
    _≈_                      : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_                      : Rel Carrier ℓ₂  -- The partial order.
    _∨_                      : Op₂ Carrier     -- The join operation.
    ⊥                        : Carrier         -- The minimum.
    isBoundedJoinSemilattice : IsBoundedJoinSemilattice _≈_ _≤_ _∨_ ⊥

  open IsBoundedJoinSemilattice isBoundedJoinSemilattice public

  joinSemilattice : JoinSemilattice c ℓ₁ ℓ₂
  joinSemilattice = record { isJoinSemilattice = isJoinSemilattice }

  joinSemiLattice = joinSemilattice
  {-# WARNING_ON_USAGE joinSemiLattice
  "Warning: joinSemiLattice was deprecated in v0.17.
  Please use joinSemilattice instead."
  #-}

  open JoinSemilattice joinSemilattice public using (preorder; poset)

------------------------------------------------------------------------
-- Meet semilattices

record IsMeetSemilattice {a ℓ₁ ℓ₂} {A : Set a}
                         (_≈_ : Rel A ℓ₁) -- The underlying equality.
                         (_≤_ : Rel A ℓ₂) -- The partial order.
                         (_∧_ : Op₂ A)    -- The meet operation.
                         : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isPartialOrder : IsPartialOrder _≈_ _≤_
    infimum        : Infimum _≤_ _∧_

  x∧y≤x : ∀ x y → (x ∧ y) ≤ x
  x∧y≤x x y = let pf , _ , _ = infimum x y in pf

  x∧y≤y : ∀ x y → (x ∧ y) ≤ y
  x∧y≤y x y = let _ , pf , _ = infimum x y in pf

  ∧-greatest : ∀ {x y z} → x ≤ y → x ≤ z → x ≤ (y ∧ z)
  ∧-greatest {x} {y} {z} = let _ , _ , pf = infimum y z in pf x

  open IsPartialOrder isPartialOrder public

record MeetSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixr 7 _∧_
  field
    Carrier           : Set c
    _≈_               : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_               : Rel Carrier ℓ₂  -- The partial order.
    _∧_               : Op₂ Carrier     -- The meet operation.
    isMeetSemilattice : IsMeetSemilattice _≈_ _≤_ _∧_

  open IsMeetSemilattice isMeetSemilattice public

  poset : Poset c ℓ₁ ℓ₂
  poset = record { isPartialOrder = isPartialOrder }

  open Poset poset public using (preorder)

record IsBoundedMeetSemilattice {a ℓ₁ ℓ₂} {A : Set a}
                                (_≈_ : Rel A ℓ₁) -- The underlying equality.
                                (_≤_ : Rel A ℓ₂) -- The partial order.
                                (_∧_ : Op₂ A)    -- The join operation.
                                (⊤   : A)        -- The maximum.
                                : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isMeetSemilattice : IsMeetSemilattice _≈_ _≤_ _∧_
    maximum           : Maximum _≤_ ⊤

  open IsMeetSemilattice isMeetSemilattice public

record BoundedMeetSemilattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixr 7 _∧_
  field
    Carrier                  : Set c
    _≈_                      : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_                      : Rel Carrier ℓ₂  -- The partial order.
    _∧_                      : Op₂ Carrier     -- The join operation.
    ⊤                        : Carrier         -- The maximum.
    isBoundedMeetSemilattice : IsBoundedMeetSemilattice _≈_ _≤_ _∧_ ⊤

  open IsBoundedMeetSemilattice isBoundedMeetSemilattice public

  meetSemilattice : MeetSemilattice c ℓ₁ ℓ₂
  meetSemilattice = record { isMeetSemilattice = isMeetSemilattice }

  meetSemiLattice = meetSemilattice
  {-# WARNING_ON_USAGE meetSemiLattice
  "Warning: meetSemiLattice was deprecated in v0.17.
  Please use meetSemilattice instead."
  #-}

  open MeetSemilattice meetSemilattice public using (preorder; poset)

------------------------------------------------------------------------
-- Lattices

record IsLattice {a ℓ₁ ℓ₂} {A : Set a}
                 (_≈_ : Rel A ℓ₁) -- The underlying equality.
                 (_≤_ : Rel A ℓ₂) -- The partial order.
                 (_∨_ : Op₂ A)    -- The join operation.
                 (_∧_ : Op₂ A)    -- The meet operation.
                 : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isPartialOrder : IsPartialOrder _≈_ _≤_
    supremum       : Supremum _≤_ _∨_
    infimum        : Infimum _≤_ _∧_

  isJoinSemilattice : IsJoinSemilattice _≈_ _≤_ _∨_
  isJoinSemilattice = record
    { isPartialOrder = isPartialOrder
    ; supremum       = supremum
    }

  isMeetSemilattice : IsMeetSemilattice _≈_ _≤_ _∧_
  isMeetSemilattice = record
    { isPartialOrder = isPartialOrder
    ; infimum        = infimum
    }

  open IsJoinSemilattice isJoinSemilattice public
    using (x≤x∨y; y≤x∨y; ∨-least)
  open IsMeetSemilattice isMeetSemilattice public
    using (x∧y≤x; x∧y≤y; ∧-greatest)
  open IsPartialOrder isPartialOrder public

record Lattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixr 6 _∨_
  infixr 7 _∧_
  field
    Carrier   : Set c
    _≈_       : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_       : Rel Carrier ℓ₂  -- The partial order.
    _∨_       : Op₂ Carrier     -- The join operation.
    _∧_       : Op₂ Carrier     -- The meet operation.
    isLattice : IsLattice _≈_ _≤_ _∨_ _∧_

  open IsLattice isLattice public

  setoid : Setoid c ℓ₁
  setoid = record { isEquivalence = isEquivalence }

  joinSemilattice : JoinSemilattice c ℓ₁ ℓ₂
  joinSemilattice = record { isJoinSemilattice = isJoinSemilattice }

  meetSemilattice : MeetSemilattice c ℓ₁ ℓ₂
  meetSemilattice = record { isMeetSemilattice = isMeetSemilattice }

  open JoinSemilattice joinSemilattice public using (poset; preorder)

record IsDistributiveLattice {a ℓ₁ ℓ₂} {A : Set a}
                             (_≈_ : Rel A ℓ₁) -- The underlying equality.
                             (_≤_ : Rel A ℓ₂) -- The partial order.
                             (_∨_ : Op₂ A)    -- The join operation.
                             (_∧_ : Op₂ A)    -- The meet operation.
                             : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isLattice    : IsLattice _≈_ _≤_ _∨_ _∧_
    ∧-distribˡ-∨ : _DistributesOverˡ_ _≈_ _∧_ _∨_

  open IsLattice isLattice public

record DistributiveLattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixr 6 _∨_
  infixr 7 _∧_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_     : Rel Carrier ℓ₂  -- The partial order.
    _∨_     : Op₂ Carrier     -- The join operation.
    _∧_     : Op₂ Carrier     -- The meet operation.
    isDistributiveLattice : IsDistributiveLattice _≈_ _≤_ _∨_ _∧_

  open IsDistributiveLattice isDistributiveLattice using (∧-distribˡ-∨) public
  open IsDistributiveLattice isDistributiveLattice using (isLattice)

  lattice : Lattice c ℓ₁ ℓ₂
  lattice = record { isLattice = isLattice }

  open Lattice lattice hiding (Carrier; _≈_; _≤_; _∨_; _∧_) public

record IsBoundedLattice {a ℓ₁ ℓ₂} {A : Set a}
                        (_≈_ : Rel A ℓ₁) -- The underlying equality.
                        (_≤_ : Rel A ℓ₂) -- The partial order.
                        (_∨_ : Op₂ A)    -- The join operation.
                        (_∧_ : Op₂ A)    -- The meet operation.
                        (⊤   : A)        -- The maximum.
                        (⊥   : A)        -- The minimum.
                        : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isLattice : IsLattice _≈_ _≤_ _∨_ _∧_
    maximum   : Maximum _≤_ ⊤
    minimum   : Minimum _≤_ ⊥

  open IsLattice isLattice public

  isBoundedJoinSemilattice : IsBoundedJoinSemilattice _≈_ _≤_ _∨_ ⊥
  isBoundedJoinSemilattice = record
    { isJoinSemilattice = isJoinSemilattice
    ; minimum           = minimum
    }

  isBoundedMeetSemilattice : IsBoundedMeetSemilattice _≈_ _≤_ _∧_ ⊤
  isBoundedMeetSemilattice = record
    { isMeetSemilattice = isMeetSemilattice
    ; maximum           = maximum
    }

record BoundedLattice c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixr 6 _∨_
  infixr 7 _∧_
  field
    Carrier          : Set c
    _≈_              : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_              : Rel Carrier ℓ₂  -- The partial order.
    _∨_              : Op₂ Carrier     -- The join operation.
    _∧_              : Op₂ Carrier     -- The meet operation.
    ⊤                : Carrier         -- The maximum.
    ⊥                : Carrier         -- The minimum.
    isBoundedLattice : IsBoundedLattice _≈_ _≤_ _∨_ _∧_ ⊤ ⊥

  open IsBoundedLattice isBoundedLattice public

  boundedJoinSemilattice : BoundedJoinSemilattice c ℓ₁ ℓ₂
  boundedJoinSemilattice = record
    { isBoundedJoinSemilattice = isBoundedJoinSemilattice }

  boundedMeetSemilattice : BoundedMeetSemilattice c ℓ₁ ℓ₂
  boundedMeetSemilattice = record
    { isBoundedMeetSemilattice = isBoundedMeetSemilattice }

  lattice : Lattice c ℓ₁ ℓ₂
  lattice = record { isLattice = isLattice }

  open Lattice lattice public
    using (joinSemilattice; meetSemilattice; poset; preorder; setoid)

------------------------------------------------------------------------
-- Heyting algebras (a bounded lattice with exponential operator)

record IsHeytingAlgebra {a ℓ₁ ℓ₂} {A : Set a}
                        (_≈_ : Rel A ℓ₁) -- The underlying equality.
                        (_≤_ : Rel A ℓ₂) -- The partial order.
                        (_∨_ : Op₂ A)    -- The join operation.
                        (_∧_ : Op₂ A)    -- The meet operation.
                        (_⇨_ : Op₂ A)    -- The exponential operation.
                        (⊤   : A)        -- The maximum.
                        (⊥   : A)        -- The minimum.
                        : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  field
    isBoundedLattice : IsBoundedLattice _≈_ _≤_ _∨_ _∧_ ⊤ ⊥
    exponential      : Exponential _≤_ _∧_ _⇨_

  transpose-⇨ : ∀ {w x y} → (w ∧ x) ≤ y → w ≤ (x ⇨ y)
  transpose-⇨ {w} {x} {y} = let pf , _ = exponential w x y in pf

  transpose-∧ : ∀ {w x y} → w ≤ (x ⇨ y) → (w ∧ x) ≤ y
  transpose-∧ {w} {x} {y} = let _ , pf = exponential w x y in pf

  open IsBoundedLattice isBoundedLattice public

record HeytingAlgebra c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixr 5 _⇨_
  infixr 6 _∨_
  infixr 7 _∧_
  field
    Carrier          : Set c
    _≈_              : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_              : Rel Carrier ℓ₂  -- The partial order.
    _∨_              : Op₂ Carrier     -- The join operation.
    _∧_              : Op₂ Carrier     -- The meet operation.
    _⇨_              : Op₂ Carrier     -- The exponential operation.
    ⊤                : Carrier         -- The maximum.
    ⊥                : Carrier         -- The minimum.
    isHeytingAlgebra : IsHeytingAlgebra _≈_ _≤_ _∨_ _∧_ _⇨_ ⊤ ⊥

  boundedLattice : BoundedLattice c ℓ₁ ℓ₂
  boundedLattice = record
    { isBoundedLattice = IsHeytingAlgebra.isBoundedLattice isHeytingAlgebra }

  open IsHeytingAlgebra isHeytingAlgebra
    using (exponential; transpose-⇨; transpose-∧) public
  open BoundedLattice boundedLattice
    hiding (Carrier; _≈_; _≤_; _∨_; _∧_; ⊤; ⊥) public

------------------------------------------------------------------------
-- Boolean algebras (a specialized Heyting algebra)

record IsBooleanAlgebra {a ℓ₁ ℓ₂} {A : Set a}
                        (_≈_ : Rel A ℓ₁) -- The underlying equality.
                        (_≤_ : Rel A ℓ₂) -- The partial order.
                        (_∨_ : Op₂ A)    -- The join operation.
                        (_∧_ : Op₂ A)    -- The meet operation.
                        (¬_ : Op₁ A)     -- The negation operation.
                        (⊤   : A)        -- The maximum.
                        (⊥   : A)        -- The minimum.
                        : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  infixr 5 _⇨_
  _⇨_ : Op₂ A
  x ⇨ y = (¬ x) ∨ y

  field
    isHeytingAlgebra : IsHeytingAlgebra _≈_ _≤_ _∨_ _∧_ _⇨_ ⊤ ⊥

  open IsHeytingAlgebra isHeytingAlgebra public

record BooleanAlgebra c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix  4 _≈_ _≤_
  infixr 6 _∨_
  infixr 7 _∧_
  infix 8 ¬_
  field
    Carrier          : Set c
    _≈_              : Rel Carrier ℓ₁  -- The underlying equality.
    _≤_              : Rel Carrier ℓ₂  -- The partial order.
    _∨_              : Op₂ Carrier     -- The join operation.
    _∧_              : Op₂ Carrier     -- The meet operation.
    ¬_               : Op₁ Carrier     -- The negation operation.
    ⊤                : Carrier         -- The maximum.
    ⊥                : Carrier         -- The minimum.
    isBooleanAlgebra : IsBooleanAlgebra _≈_ _≤_ _∨_ _∧_ ¬_ ⊤ ⊥

  open IsBooleanAlgebra isBooleanAlgebra using (isHeytingAlgebra)

  heytingAlgebra : HeytingAlgebra c ℓ₁ ℓ₂
  heytingAlgebra = record { isHeytingAlgebra = isHeytingAlgebra }

  open HeytingAlgebra heytingAlgebra public
    hiding (Carrier; _≈_; _≤_; _∨_; _∧_; ⊤; ⊥)


text:
open import Prelude
open import Nat
open import Bij

module Int where

  data Int : Set where
    +_     : Nat → Int
    -[1+_] : Nat → Int

  int→nat : Int → Nat
  int→nat (+ n) = 1+ (n + n)
  int→nat -[1+ n ] = n + n

  int→nat:inj : ∀{m n} →
                   int→nat m == int→nat n →
                   m == n
  int→nat:inj {+ m} {+ n} eq rewrite even-inj {m} {n} (1+inj eq) = refl
  int→nat:inj {+ m} { -[1+ n ]} eq = abort (even-not-odd {m} {n} eq)
  int→nat:inj { -[1+ m ]} {+ n} eq = abort (even-not-odd {n} {m} (! eq))
  int→nat:inj { -[1+ m ]} { -[1+ n ]} eq rewrite even-inj {m} {n} eq = refl

  int→nat:surj : (n : Nat) → Σ[ m ∈ Int ] (int→nat m == n)
  int→nat:surj Z = -[1+ Z ] , refl
  int→nat:surj (1+ Z) = (+ Z) , refl
  int→nat:surj (1+ (1+ n)) with int→nat:surj n
  int→nat:surj (1+ (1+ .(1+ (n + n)))) | (+ n) , refl = (+ 1+ n) , 1+ap (1+ap n+1+m==1+n+m)
  int→nat:surj (1+ (1+ .(n + n))) | -[1+ n ] , refl = -[1+ 1+ n ] , 1+ap n+1+m==1+n+m

  instance
    IntBij : bij Int Nat
    IntBij = record {
      convert = int→nat;
      inj     = int→nat:inj;
      surj    = int→nat:surj}

max_stars_repo_name: nickcollins/dependent-dicts-agda

max_issues_repo_name: nickcollins/dependent-dicts-agda

max_forks_repo_name: nickcollins/dependent-dicts-agda


text:
module Haskell.RangedSetsProp.RangesProperties where

open import Haskell.RangedSetsProp.library

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat renaming (_==_ to eqq; _<_ to ltt)

open import Haskell.Prim
open import Haskell.Prim.Ord
open import Haskell.Prim.Bool
open import Haskell.Prim.Maybe
open import Haskell.Prim.Enum
open import Haskell.Prim.Eq

open import Haskell.Prim.Foldable
open import Haskell.Prim.List
open import Haskell.Prim.Integer
open import Haskell.Prim.Double

open import Haskell.RangedSets.Boundaries
open import Haskell.RangedSets.Ranges
open import Haskell.RangedSetsProp.BoundariesProperties

postulate
  prop_range_creation : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → {r1 r2 : Boundary a} →
                        {r3 r4 : Boundary a} → (r1 ≡ r3) → (r2 ≡ r4) → (Rg r1 r2) ≡ Rg r3 r4

prop_intersection_sym : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (r1 : Range a) → (r2 : Range a) →
                        rangeIntersection r1 r2 ≡ rangeIntersection r2 r1
prop_intersection_sym ⦃ o ⦄ ⦃ dio ⦄ r1@(Rg l1 u1) r2@(Rg l2 u2) =
   begin
      rangeIntersection r1 r2
     =⟨⟩
      if_then_else_ (rangeIsEmpty r1 || rangeIsEmpty r2) emptyRange (Rg (max l1 l2) (min u1 u2))
     =⟨ cong (ifThenElseHelper emptyRange (Rg (max l1 l2) (min u1 u2))) (prop_or_sym (rangeIsEmpty r1) (rangeIsEmpty r2)) ⟩
      if_then_else_ (rangeIsEmpty r2 || rangeIsEmpty r1) emptyRange (Rg (max l1 l2) (min u1 u2))
     =⟨ cong (if_then_else_ (rangeIsEmpty r2 || rangeIsEmpty r1) emptyRange)
     (prop_range_creation (prop_max_sym l1 l2) (prop_min_sym u1 u2))  ⟩
      if_then_else_ (rangeIsEmpty r2 || rangeIsEmpty r1) emptyRange (Rg (max l2 l1) (min u2 u1))
     =⟨⟩
      rangeIntersection r2 r1
   end

prop_singletonRangeHas : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (x : a) → (rangeHas ⦃ o ⦄ (singletonRange x) x) ≡ true
prop_singletonRangeHas ⦃ o ⦄ ⦃ dio ⦄ x =
   begin
      (rangeHas (singletonRange x) x)
     =⟨⟩
      (rangeHas (Rg (BoundaryBelow x) (BoundaryAbove x)) x)
     =⟨⟩
      ((x />/ (BoundaryBelow x)) && (not (x />/ (BoundaryAbove x))))
     =⟨⟩
      ((x >= x) && (not (x > x)))
     =⟨ cong (_&& (not (x > x))) (gteq ⦃ o ⦄ refl) ⟩
      (true && (not (x > x)))
     =⟨ cong (true &&_) (gt ⦃ o ⦄ refl) ⟩
      (true && true)
     =⟨⟩
      true
   end

prop_singletonRangeHasOnly : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (x y : a) → (rangeHas ⦃ o ⦄ (singletonRange x) y) ≡ (x == y)
prop_singletonRangeHasOnly ⦃ o ⦄ ⦃ dio ⦄ v1 v2 =
   begin
      (rangeHas (singletonRange v1) v2)
     =⟨⟩
      (rangeHas (Rg (BoundaryBelow v1) (BoundaryAbove v1)) v2)
     =⟨⟩
      ((v2 />/ (BoundaryBelow v1)) && (not (v2 />/ (BoundaryAbove v1))))
     =⟨⟩
      ((v2 >= v1) && (not (v2 > v1)))
     =⟨ eq1 v2 v1 ⟩
      (v1 == v2)
   end

prop_singletonRangeConverse : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (x : a) → rangeSingletonValue (singletonRange x) ≡ Just x
prop_singletonRangeConverse ⦃ o ⦄ ⦃ dio ⦄ v =
   begin
      rangeSingletonValue (singletonRange v)
     =⟨⟩
      rangeSingletonValue (Rg (BoundaryBelow v) (BoundaryAbove v))
     =⟨⟩
      if_then_else_ (v == v) (Just v) Nothing
     =⟨ propIf2 (v == v) (eq0 ⦃ o ⦄ refl) ⟩
      Just v
   end

prop_emptyNonSingleton : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → rangeSingletonValue ⦃ o ⦄ ⦃ dio ⦄ emptyRange ≡ Nothing
prop_emptyNonSingleton = refl

prop_fullNonSingleton : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → rangeSingletonValue ⦃ o ⦄ ⦃ dio ⦄ fullRange ≡ Nothing
prop_fullNonSingleton = refl

rs : Double → Double → List (Range Double)
rs x y = (Rg (BoundaryBelow x) (BoundaryBelow y)) ∷ (Rg (BoundaryAbove x) (BoundaryBelow y)) ∷ (Rg (BoundaryBelow x) (BoundaryAbove y)) ∷ (Rg (BoundaryAbove x) (BoundaryAbove y)) ∷ []

length' : List a → Nat
length' [] = 0
length' (x ∷ []) = 1
length' (x ∷ xs) = 1 + (length' xs)

prop_unionRangeLengthHelper3 : ⦃ ord : Ord a ⦄ → ⦃ diso : DiscreteOrdered a ⦄
                 → (r1 r2 : (Range a)) → (b : Bool)
                 → ((eqq ((length' (if_then_else_ b ((Rg (min (rangeLower r1) (rangeLower r2)) (max (rangeUpper r1) (rangeUpper r2))) ∷ []) (r1 ∷ r2 ∷ [])))) 1)
                 || (eqq (length' ((if_then_else_ b ((Rg (min (rangeLower r1) (rangeLower r2)) (max (rangeUpper r1) (rangeUpper r2))) ∷ []) (r1 ∷ r2 ∷ [])))) 2)) ≡ true
prop_unionRangeLengthHelper3 ⦃ o ⦄ ⦃ dio ⦄ r1@(Rg l1 u1) r2@(Rg l2 u2) true =
  begin
    ((eqq (length' ((Rg (min l1 l2) (max u1 u2)) ∷ [])) 1) || (eqq (length' ((Rg (min l1 l2) (max u1 u2)) ∷ [])) 2))
   =⟨⟩
    ((eqq 1 1) || (eqq 1 2))
   =⟨⟩
     (true || false)
   =⟨⟩
     true
   end
prop_unionRangeLengthHelper3 ⦃ o ⦄ ⦃ dio ⦄ r1@(Rg l1 u1) r2@(Rg l2 u2) false =
  begin
    ((eqq (length' (r1 ∷ r2 ∷ [])) 1) || (eqq (length' (r1 ∷ r2 ∷ [])) 2))
   =⟨⟩
    ((eqq 2 1) || (eqq 2 2))
   =⟨⟩
     (false || true)
   =⟨⟩
     true
   end

prop_unionRangeLengthHelper2 : ⦃ ord : Ord a ⦄ → ⦃ diso : DiscreteOrdered a ⦄
                 → (r1 r2 : (Range a)) → (b : Bool)
                 → ((eqq (length' (if_then_else_ b (r1 ∷ []) (rangeU2 r1 r2))) 1) || (eqq (length' ((if_then_else_ b (r1 ∷ []) (rangeU2 r1 r2)))) 2)) ≡ true
prop_unionRangeLengthHelper2 ⦃ o ⦄ ⦃ dio ⦄ r1@(Rg l1 u1) r2@(Rg l2 u2) true =
    begin
     ((eqq (length' (r1 ∷ [])) 1) || (eqq (length' (r1 ∷ [])) 2))
   =⟨⟩
    ((eqq 1 1) || (eqq 1 2))
   =⟨⟩
     (true || false)
   =⟨⟩
     true
   end
prop_unionRangeLengthHelper2 ⦃ o ⦄ ⦃ dio ⦄ r1@(Rg l1 u1) r2@(Rg l2 u2) false =
    begin
     ((eqq (length' (rangeU2 r1 r2)) 1) || (eqq (length' (rangeU2 r1 r2)) 2))
   =⟨⟩
     ((eqq (length' (if_then_else_ ((max l1 l2) <= (min u1 u2)) ((Rg (min l1 l2) (max u1 u2)) ∷ []) (r1 ∷ r2 ∷ []))) 1)
     || (eqq (length' (if_then_else_ ((max l1 l2) <= (min u1 u2)) ((Rg (min l1 l2) (max u1 u2)) ∷ []) (r1 ∷ r2 ∷ []))) 2))
   =⟨ prop_unionRangeLengthHelper3 r1 r2 (((max l1 l2) <= (min u1 u2))) ⟩
     true
   end

prop_unionRangeLengthHelper : ⦃ ord : Ord a ⦄ → ⦃ diso : DiscreteOrdered a ⦄
                 → (r1 r2 : (Range a)) → (b : Bool)
                 → ((eqq (length' (if_then_else_ b (r2 ∷ []) (rangeU1 r1 r2))) 1) || (eqq (length' ((if_then_else_ b (r2 ∷ []) (rangeU1 r1 r2)))) 2)) ≡ true
prop_unionRangeLengthHelper ⦃ o ⦄ ⦃ dio ⦄ r1@(Rg l1 u1) r2@(Rg l2 u2) true =
    begin
     ((eqq (length' (r2 ∷ [])) 1) || (eqq (length' (r2 ∷ [])) 2))
   =⟨⟩
    ((eqq 1 1) || (eqq 1 2))
   =⟨⟩
     (true || false)
   =⟨⟩
     true
   end
prop_unionRangeLengthHelper ⦃ o ⦄ ⦃ dio ⦄ r1@(Rg l1 u1) r2@(Rg l2 u2) false =
    begin
     ((eqq (length' (rangeU1 r1 r2)) 1) || (eqq (length' (rangeU1 r1 r2)) 2))
   =⟨⟩
     ((eqq (length' (if_then_else_ (rangeIsEmpty r2) (r1 ∷ []) (rangeU2 r1 r2))) 1)
     || (eqq (length' (if_then_else_ (rangeIsEmpty r2) (r1 ∷ []) (rangeU2 r1 r2))) 2))
   =⟨ prop_unionRangeLengthHelper2 r1 r2 (rangeIsEmpty r2) ⟩
     true
   end

prop_unionRangeLength : ⦃ ord : Ord a ⦄ → ⦃ diso : DiscreteOrdered a ⦄
                 → (r1 r2 : (Range a)) → ((eqq (length' (rangeUnion r1 r2)) 1) || (eqq (length' (rangeUnion r1 r2)) 2)) ≡ true
prop_unionRangeLength ⦃ o ⦄ ⦃ dio ⦄ r1@(Rg l1 u1) r2@(Rg l2 u2) =
   begin
     ((eqq (length' (rangeUnion r1 r2)) 1) || (eqq (length' (rangeUnion r1 r2)) 2))
   =⟨⟩
     ((eqq (length' (if_then_else_ (rangeIsEmpty r1) (r2 ∷ []) (rangeU1 r1 r2))) 1) || (eqq (length' (if_then_else_ (rangeIsEmpty r1) (r2 ∷ []) (rangeU1 r1 r2))) 2))
   =⟨ prop_unionRangeLengthHelper r1 r2 (rangeIsEmpty r1) ⟩
     true
   end

prop_UnionRange1 : ⦃ ord : Ord a ⦄ → ⦃ diso : DiscreteOrdered a ⦄
                 → (r1 r2 : (Range a)) → ⦃ ne1 : IsFalse (rangeIsEmpty r1) ⦄ → ⦃ ne2 : IsFalse (rangeIsEmpty r2) ⦄
                 → ⦃ ne3 : IsFalse ((max (rangeLower r1) (rangeLower r2)) <= (min (rangeUpper r1) (rangeUpper r2))) ⦄ → (n : a)
                 → (rangeListHas1 n (rangeUnion ⦃ ord ⦄ ⦃ diso ⦄ r1 r2)) ≡ ((rangeHas ⦃ ord ⦄ r1 n) || (rangeHas ⦃ ord ⦄ r2 n))
prop_UnionRange1 ⦃ ord ⦄ ⦃ diso ⦄ r1@(Rg l1 u1) r2@(Rg l2 u2) ⦃ ne1 ⦄ ⦃ ne2 ⦄ ⦃ ne3 ⦄ n =
   begin
     (rangeListHas1 n (rangeUnion r1 r2))
   =⟨⟩
     (rangeListHas1 n (if_then_else_ (rangeIsEmpty r1) (r2 ∷ []) (rangeU1 r1 r2)))
   =⟨ propIf (rangeListHas1 n) (rangeIsEmpty r1) ⟩
     if_then_else_ (rangeIsEmpty r1) (rangeListHas1 n (r2 ∷ [])) (rangeListHas1 n (rangeU1 r1 r2))
   =⟨ propIf3 (rangeIsEmpty r1) ne1 ⟩
     rangeListHas1 n (rangeU1 r1 r2)
   =⟨ cong (rangeListHas1 n) (propIf3 (rangeIsEmpty r2) ne2) ⟩
     (rangeListHas1 n (rangeU2 r1 r2))
   =⟨ cong (rangeListHas1 n) (propIf3 ((max l1 l2) <= (min u1 u2)) ne3) ⟩
     (rangeListHas1 n (r1 ∷ r2 ∷ []))
   =⟨⟩
     ((rangeHas r1 n) || (rangeHas r2 n))
   end

-- prop_UnionRange1' : ⦃ ord : Ord a ⦄ → ⦃ diso : DiscreteOrdered a ⦄
--                  → (r1 r2 : (Range a)) → ⦃ne1 : IsFalse (rangeIsEmpty r1)⦄ → ⦃ne2 : IsFalse (rangeIsEmpty r2)⦄
--                  → ⦃ne3 : IsTrue ((max (rangeLower r1) (rangeLower r2)) <= (min (rangeUpper r1) (rangeUpper r2)))⦄ → (n : a)
--                  → (rangeListHas1 n (rangeUnion ⦃ord⦄ ⦃diso⦄ r1 r2)) ≡ ((rangeHas ⦃ord⦄ r1 n) || (rangeHas ⦃ord⦄ r2 n))
-- prop_UnionRange1' ⦃ord⦄ ⦃diso⦄ r1@(Rg l1 u1) r2@(Rg l2 u2) ⦃ne1⦄ ⦃ne2⦄ ⦃ne3⦄ n =
--    begin
--      (rangeListHas1 n (rangeUnion r1 r2))
--    =⟨⟩
--      (rangeListHas1 n (if_then_else_ (rangeIsEmpty r1) (r2 ∷ []) (rangeU1 r1 r2)))
--    =⟨ propIf (rangeListHas1 n) (rangeIsEmpty r1) ⟩
--      if_then_else_ (rangeIsEmpty r1) (rangeListHas1 n (r2 ∷ [])) (rangeListHas1 n (rangeU1 r1 r2))
--    =⟨ propIf3 (rangeIsEmpty r1) ne1 ⟩
--      rangeListHas1 n (rangeU1 r1 r2)
--    =⟨ cong (rangeListHas1 n) (propIf3 (rangeIsEmpty r2) ne2) ⟩
--      (rangeListHas1 n (rangeU2 r1 r2))
--    =⟨ cong (rangeListHas1 n) (propIf2 ((max l1 l2) <= (min u1 u2)) ne3) ⟩
--      (rangeListHas1 n ((Rg (min l1 l2) (max u1 u2)) ∷ []))
--    =⟨⟩
--     ((n />/ (min l1 l2)) && not (n />/ (max u1 u2)))
--    =⟨⟩
--     ((n />/ (if (compare l1 l2 == LT) then l1 else l2)) && not (n />/ (if (compare u1 u2 == GT) then u1 else u2)))
--    =⟨⟩
--      ((rangeHas r1 n) || (rangeHas r2 n))
--    end

prop_emptyRange : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (r : Range a) → not (rangeIsEmpty r) ≡ (rangeLower r <= rangeUpper r)
prop_emptyRange ⦃ o ⦄ ⦃ dio ⦄ r@(Rg l u) =
  begin
    not (rangeIsEmpty r)
  =⟨⟩
    not (u <= l)
  =⟨ eq2 u l ⟩
    l < u
  =⟨ lteq l u ⟩
    l <= u
  end

prop_rangeHas : ⦃ ord : Ord a ⦄ → ⦃ diso : DiscreteOrdered a ⦄ → {r : (Range a)} → {n : a}
                        → (rangeHas1 ⦃ ord ⦄ n r) ≡ (rangeHas ⦃ ord ⦄ r n)
prop_rangeHas {r = (Rg x y)} {n} =
   begin
     rangeHas1 n (Rg x y)
   =⟨⟩
     (n />/ x) && (not (n />/ y))
   =⟨⟩
     rangeHas (Rg x y) n
   end

prop_IntersectionRange : ⦃ ord : Ord a ⦄ → ⦃ diso : DiscreteOrdered a ⦄ → (r1 r2 : (Range a))
                        → ⦃ ff : IsFalse (rangeIsEmpty r1 || rangeIsEmpty r2) ⦄  → (n : a)
                        → ((rangeHas r1 n) && (rangeHas r2 n)) ≡ (rangeHas (rangeIntersection r1 r2) n)

prop_IntersectionRange ⦃ ord ⦄ ⦃ diso ⦄ r1@(Rg x1 y1) r2@(Rg x2 y2) ⦃ ff ⦄ n =
   begin
     ((rangeHas r1 n) && (rangeHas r2 n))
   =⟨⟩
     ((n />/ x1) && (not (n />/ y1))) && ((n />/ x2) && (not (n />/ y2)))
   =⟨ prop_and_assoc (n />/ x1) (not (n />/ y1)) (n />/ x2 && (not (n />/ y2))) ⟩
     ((n />/ x1) && ((not (n />/ y1)) && ((n />/ x2) && (not (n />/ y2)))))
   =⟨ cong ((n />/ x1) &&_) (sym (prop_and_assoc (not (n />/ y1)) (n />/ x2) (not (n />/ y2)))) ⟩
     ((n />/ x1) && (not (n />/ y1) && (n />/ x2)) && (not (n />/ y2)))
   =⟨ sym (prop_and_assoc (n />/ x1) (not (n />/ y1) && (n />/ x2)) (not (n />/ y2))) ⟩
     (((n />/ x1) && (not (n />/ y1) && (n />/ x2))) && (not (n />/ y2)))
   =⟨ cong (_&& (not (n />/ y2))) (cong ((n />/ x1) &&_) (prop_and_comm (not (n />/ y1)) (n />/ x2))) ⟩
     (((n />/ x1) && ((n />/ x2) && not (n />/ y1))) && (not (n />/ y2)))
   =⟨ cong (_&& (not (n />/ y2))) (sym (prop_and_assoc (n />/ x1) (n />/ x2) (not (n />/ y1)))) ⟩
     ((((n />/ x1) && (n />/ x2)) && not (n />/ y1)) && (not (n />/ y2)))
   =⟨ prop_and_assoc ((n />/ x1) && (n />/ x2)) (not (n />/ y1)) (not (n />/ y2)) ⟩
     (((n />/ x1) && (n />/ x2)) && (not (n />/ y1) && (not (n />/ y2))))
   =⟨ cong ((n />/ x1 && n />/ x2) &&_) (prop_demorgan2 (n />/ y1) (n />/ y2)) ⟩
     (n />/ x1 && n />/ x2) && (not ((n />/ y1) || (n />/ y2)))
   =⟨ cong (_&& (not ((n />/ y1) || (n />/ y2)))) (boundaries0 n x1 x2) ⟩
     (n />/ (max x1 x2)) && (not ((n />/ y1) || (n />/ y2)))
   =⟨ cong ((n />/ (max x1 x2)) &&_) (cong not (boundaries1 n y1 y2)) ⟩
     (n />/ (max x1 x2)) && not (n />/ (min y1 y2))
   =⟨⟩
     rangeHas (Rg (max (rangeLower r1) (rangeLower r2)) (min (rangeUpper r1) (rangeUpper r2))) n
   =⟨ sym (cong (rangeHas1 n) (propIf3 (rangeIsEmpty r1 || rangeIsEmpty r2) ff)) ⟩
     rangeHas1 n (rangeIntersection r1 r2)
   =⟨ prop_rangeHas ⦃ ord ⦄ ⦃ diso ⦄ {(rangeIntersection r1 r2)} ⟩
     rangeHas (rangeIntersection r1 r2) n
   end

prop_notEmptyRanges : ⦃ ord : Ord a ⦄ → ⦃ diso : DiscreteOrdered a ⦄ → (r1 r2 : (Range a))
                    → (not ((rangeIsEmpty r1) || (rangeIsEmpty r2))) ≡ (((rangeLower r1) < (rangeUpper r1)) && ((rangeLower r2) < (rangeUpper r2)))
prop_notEmptyRanges ⦃ ord ⦄ ⦃ diso ⦄ r1@(Rg l1 u1) r2@(Rg l2 u2) =
   begin
      not ((rangeIsEmpty r1 )|| (rangeIsEmpty r2))
   =⟨⟩
      (not (((rangeUpper r1) <= (rangeLower r1)) || ((rangeUpper r2) <= (rangeLower r2))))
   =⟨ sym (prop_demorgan2 ((rangeUpper r1) <= (rangeLower r1)) ((rangeUpper r2) <= (rangeLower r2))) ⟩
      ((not ((rangeUpper r1) <= (rangeLower r1)))) && (not ((rangeUpper r2) <= (rangeLower r2)))
   =⟨ cong (not ((rangeUpper r1) <= (rangeLower r1)) &&_) (eq2 (rangeUpper r2) (rangeLower r2)) ⟩
      ((not ((rangeUpper r1) <= (rangeLower r1))) && ((rangeLower r2) < (rangeUpper r2)))
   =⟨ cong (_&& ((rangeLower r2) < (rangeUpper r2))) (eq2 (rangeUpper r1) (rangeLower r1)) ⟩
      (((rangeLower r1) < (rangeUpper r1)) && ((rangeLower r2) < (rangeUpper r2)))
    end

prop_intersectionOverlap : ⦃ ord : Ord a ⦄ → ⦃ diso : DiscreteOrdered a ⦄ → (r1 r2 : (Range a))
                            → ⦃ ff : IsFalse (rangeIsEmpty r1 || rangeIsEmpty r2) ⦄
                            → ⦃ tr : IsTrue (((rangeLower r1) < (rangeUpper r1)) && ((rangeLower r2) < (rangeUpper r2))) ⦄
                            → (rangeIsEmpty (rangeIntersection r1 r2)) ≡ not (rangeOverlap r1 r2)
prop_intersectionOverlap ⦃ ord ⦄ ⦃ diso ⦄ r1@(Rg _ _) r2@(Rg _ _) ⦃ ff ⦄ ⦃ tr ⦄ =
   begin
     (rangeIsEmpty (rangeIntersection r1 r2))
   =⟨⟩
     rangeIsEmpty (if_then_else_ (rangeIsEmpty r1 || rangeIsEmpty r2) emptyRange (Rg (max (rangeLower r1) (rangeLower r2)) (min (rangeUpper r1) (rangeUpper r2))))
   =⟨ cong rangeIsEmpty (propIf3 (rangeIsEmpty r1 || rangeIsEmpty r2) ff) ⟩
     (rangeIsEmpty (Rg (max (rangeLower r1) (rangeLower r2)) (min (rangeUpper r1) (rangeUpper r2))))
   =⟨⟩
     ((min (rangeUpper r1) (rangeUpper r2)) <= (max (rangeLower r1) (rangeLower r2)))
   =⟨ sym (prop_or_false ((min (rangeUpper r1) (rangeUpper r2)) <= (max (rangeLower r1) (rangeLower r2)))) ⟩
     (false ||  ((min (rangeUpper r1) (rangeUpper r2)) <= (max (rangeLower r1) (rangeLower r2))))
   =⟨ cong (_|| ((min (rangeUpper r1) (rangeUpper r2)) <= (max (rangeLower r1) (rangeLower r2)))) (sym (propIsFalse (rangeIsEmpty r1 || rangeIsEmpty r2) ff)) ⟩
     (((rangeIsEmpty r1) || (rangeIsEmpty r2)) || ((min (rangeUpper r1) (rangeUpper r2)) <= (max (rangeLower r1) (rangeLower r2))))
   =⟨ prop_or_assoc (rangeIsEmpty r1) (rangeIsEmpty r2) ((min (rangeUpper r1) (rangeUpper r2)) <= (max (rangeLower r1) (rangeLower r2))) ⟩
     ((rangeIsEmpty r1) || ((rangeIsEmpty r2) || ((min (rangeUpper r1) (rangeUpper r2)) <= (max (rangeLower r1) (rangeLower r2)))))
   =⟨ cong ((rangeIsEmpty r1) ||_) (cong ((rangeIsEmpty r2) ||_) (eq3 (rangeUpper r1) (rangeUpper r2) (rangeLower r1) (rangeLower r2) ⦃ tr ⦄)) ⟩
     ((rangeIsEmpty r1) || ((rangeIsEmpty r2) || (rangeUpper r1 <= rangeLower r2 || rangeUpper r2 <= rangeLower r1)))
   =⟨ not-not ((rangeIsEmpty r1) || (rangeIsEmpty r2) || (rangeUpper r1 <= rangeLower r2 || rangeUpper r2 <= rangeLower r1)) ⟩
     not (not ((rangeIsEmpty r1) || (rangeIsEmpty r2) || (rangeUpper r1 <= rangeLower r2 || rangeUpper r2 <= rangeLower r1)))
   =⟨ cong (not) (demorgan3 (rangeIsEmpty r1) (rangeIsEmpty r2) (rangeUpper r1 <= rangeLower r2) (rangeUpper r2 <= rangeLower r1)) ⟩
     not (not (rangeIsEmpty r1) && not (rangeIsEmpty r2) && ((not (rangeUpper r1 <= rangeLower r2)) && (not (rangeUpper r2 <= rangeLower r1))))
   =⟨ cong not (cong ((not (rangeIsEmpty r1)) &&_) (cong ((not (rangeIsEmpty r2)) &&_) (prop_demorgan2 (rangeUpper r1 <= rangeLower r2) (rangeUpper r2 <= rangeLower r1)))) ⟩
     not (not (rangeIsEmpty r1) && not (rangeIsEmpty r2) && not ((rangeUpper r1 <= rangeLower r2) || (rangeUpper r2 <= rangeLower r1)))
   =⟨⟩
     not (rangeOverlap r1 r2)
   end


text:
module Haskell.RangedSetsProp.library where

open import Agda.Builtin.Equality
open import Agda.Builtin.Bool

open import Haskell.Prim
open import Haskell.Prim.Ord
open import Haskell.Prim.Bool
open import Haskell.Prim.Eq
open import Haskell.Prim.Int
open import Haskell.Prim.List
open import Haskell.RangedSets.Boundaries
open import Haskell.RangedSets.Ranges

-- symmetry of equality
sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

-- transitivity of equality
trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

-- congruence of equality
cong : {A B : Set} {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y
cong f refl = refl

begin_ : {A : Set} → {x y : A} → x ≡ y → x ≡ y
begin p = p

_end : {A : Set} → (x : A) → x ≡ x
x end = refl

_=⟨_⟩_ : {A : Set} → (x : A) → {y z : A}
       → x ≡ y → y ≡ z → x ≡ z
x =⟨ p ⟩ q = trans p q

_=⟨⟩_ : {A : Set} → (x : A) → {y : A} → x ≡ y → x ≡ y
x =⟨⟩ q = x =⟨ refl ⟩ q

infix   1  begin_
infix   3  _end
infixr  2  _=⟨_⟩_
infixr  2  _=⟨⟩_

subst : {A : Set} {x y : A} → (P : A → Set) → x ≡ y → P x → P y
subst P refl p = p

isTrue&&₁ : {x y : Bool} → IsTrue (x && y) → IsTrue x
isTrue&&₂ : {x y : Bool} → IsTrue (x && y) → IsTrue y

isTrue&&₁ {true} _ = IsTrue.itsTrue
isTrue&&₁ {false} ()

isTrue&&₂ {true} p = p
isTrue&&₂ {false} ()

ifThenElseHelper :  {a : Set ℓ} → a → a → Bool → a
ifThenElseHelper b c d = if_then_else_ d b c

propIf : {a b : Set} → {x y : a} (f : a → b) (c : Bool) → f (if c then x else y) ≡ (if c then f x else f y)
propIf f false = refl
propIf f true = refl

propIf2 : ⦃ Ord a ⦄ → {x y : a} (c : Bool) → IsTrue c → (if c then x else y) ≡ x
propIf2 true f = refl

propIf3 : ⦃ Ord a ⦄ → {x y : a} (c : Bool) → IsFalse c → (if c then x else y) ≡ y
propIf3 false f = refl

propIf2' : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ →  {x y : List (Range a)} (c : Bool) → IsTrue c → (if c then x else y) ≡ x
propIf2' true f = refl

propIf3' : ⦃  o : Ord a  ⦄ → ⦃  dio : DiscreteOrdered a  ⦄ →  {x y : List (Range a)} (c : Bool) → IsFalse c → (if c then x else y) ≡ y
propIf3' false f = refl

propIsFalse : (x : Bool) → IsFalse x → x ≡ false
propIsFalse false f = refl

propIsTrue : (x : Bool) → IsTrue x → x ≡ true
propIsTrue true f = refl

prop_or_and_eqiv_true : (x y : Bool) -> IsTrue x -> IsTrue y -> (x || y) ≡ (x && y)
prop_or_and_eqiv_true true true _ _ = refl

prop_or_and_eqiv_false : (x y : Bool) -> IsFalse x -> IsFalse y -> (x || y) ≡ (x && y)
prop_or_and_eqiv_false false false _ _ = refl

postulate
   isTrueAndIsFalse1 : {b : Bool} -> IsTrue b -> IsFalse (not b)
   isTrueAndIsFalse2 : {b : Bool} -> IsTrue (not b) -> IsFalse b
   isTrueAndIsFalse3 : {b : Bool} -> IsFalse (not b) -> IsTrue b
   isTrueAndIsFalse4 : {b : Bool} -> IsFalse b -> IsTrue (not b)
   gteq : ⦃ o : Ord a ⦄ → ∀ {x y : a} → (x ≡ y) → (_>=_ ⦃ o ⦄ x y) ≡ true
   lt : ⦃ o : Ord a ⦄ → (x y : a) → (x ≡ y) → IsFalse (_>_ ⦃ o ⦄ x y)
   lteq : ⦃ o : Ord a ⦄ → (x y : a) → (_<_ ⦃ o ⦄ x y) ≡ (_<=_ ⦃ o ⦄ x y)
   gt : ⦃ o : Ord a ⦄ → ∀ {x y : a} → (x ≡ y) → not (_>_ ⦃ o ⦄ x y) ≡ true
   eq0 : ⦃ o : Ord a ⦄ → ∀ {x y : a} → (x ≡ y) → IsTrue (x == y)
   eq1 : ⦃ o : Ord a ⦄ → (x y : a) → ((_>=_ ⦃ o ⦄ x y) && (not (_>_ ⦃ o ⦄ x y))) ≡ (y == x)
   eq2 : ⦃ o : Ord a ⦄ → (x y : a) → not (_<=_ ⦃ o ⦄ x y) ≡ (_<_ ⦃ o ⦄ y x)
   eq3 : ⦃ o : Ord a ⦄ → (x y i j : a) → ⦃ IsTrue ((_<_ ⦃ o ⦄ i x) && (_<_ ⦃ o ⦄ j y)) ⦄ → ((min ⦃ o ⦄ x y) <= (max ⦃ o ⦄ i j)) ≡ ((_<=_ ⦃ o ⦄ x j) || (_<=_ ⦃ o ⦄ y i))
   eq4 : ⦃ o : Ord a ⦄ → ∀ {x y : a} → (x ≡ y) → ((compare x y) == EQ) ≡ true

   boundaries0 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (x : a) → (b c : Boundary a) → ((x />/ b) && (x />/ c)) ≡ (x />/ (max b c))
   boundaries1 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (x : a) → (b c : Boundary a) → ((x />/ b) || (x />/ c)) ≡ (x />/ (min b c))

prop_and_assoc : (a b c : Bool) → ((a && b) && c) ≡ (a && (b && c))
prop_and_assoc true b c =
   begin
     ((true && b) && c)
   =⟨⟩
     (b && c)
   =⟨⟩
     (true && (b && c))
   end
prop_and_assoc false b c =
   begin
     ((false && b) && c)
   =⟨⟩
     (false && c)
   =⟨⟩
     false
   =⟨⟩
     (false && (b && c))
   end

prop_and_cancel : (a : Bool) {b : Bool} → (a && a && b) ≡ (a && b)
prop_and_cancel true = refl
prop_and_cancel false = refl

prop_or_assoc : (a b c : Bool) → ((a || b) || c) ≡ (a || (b || c))
prop_or_assoc true b c = refl
prop_or_assoc false b c = refl

prop_or_sym : (a b : Bool) → (a || b) ≡ (b || a)
prop_or_sym true true = refl
prop_or_sym true false = refl
prop_or_sym false true = refl
prop_or_sym false false = refl

prop_or_same_value : (a : Bool) → (a || a) ≡ a
prop_or_same_value true = refl
prop_or_same_value false = refl

prop_and_false : (a : Bool) → (a && false) ≡ false
prop_and_false true = refl
prop_and_false false = refl

prop_and_true : (a : Bool) → (a && true) ≡ a
prop_and_true true = refl
prop_and_true false = refl

prop_or_false : (a : Bool) → (false || a) ≡ a
prop_or_false true = refl
prop_or_false false = refl

prop_or_false2 : (a : Bool) →  (a || false) ≡ a
prop_or_false2 true = refl
prop_or_false2 false = refl

prop_or_false3 : (a : Bool) →  (a || true) ≡ true
prop_or_false3 true = refl
prop_or_false3 false = refl

prop_or_true : (a : Bool) → (true || a) ≡ true
prop_or_true true = refl
prop_or_true false = refl

prop_and_comm : (a b : Bool) → (a && b) ≡ (b && a)
prop_and_comm false b =
   begin
     (false && b)
   =⟨⟩
     false
   =⟨ sym (prop_and_false b) ⟩
     (b && false)
   end
prop_and_comm true b =
   begin
     (true && b)
   =⟨⟩
     b
   =⟨ sym (prop_and_true b) ⟩
     (b && true)
   end

prop_distr : (a b c : Bool) → ((a || b) && c) ≡ ((a && c) || (b && c))
prop_distr true b true = refl
prop_distr true true false = refl
prop_distr true false false = refl
prop_distr false true true = refl
prop_distr false true false = refl
prop_distr false false false = refl
prop_distr false false true = refl

prop_dnf : (a b c d : Bool) → ((a || b) && (c || d)) ≡ ((a && c) || (b && d) || (b && c) || (a && d))
prop_dnf true b true d = refl
prop_dnf true true false true = refl
prop_dnf true false false true = refl
prop_dnf true true false false = refl
prop_dnf true false false false = refl
prop_dnf false true true true = refl
prop_dnf false true false true = refl
prop_dnf false false true true = refl
prop_dnf false false true false = refl
prop_dnf false false false true = refl
prop_dnf false false false false = refl
prop_dnf false true true false = refl
prop_dnf false true false false = refl

prop_demorgan2 : (a b : Bool) → ((not a) && (not b)) ≡ (not (a || b))
prop_demorgan2 false b = refl
prop_demorgan2 true b = refl

prop_demorgan : (a b : Bool) → (not (a && b)) ≡ ((not a) || (not b))
prop_demorgan false b = refl
prop_demorgan true b = refl

not-not : (b : Bool) → b ≡ not (not b)
not-not false = refl
not-not true =
   begin
      not (not true)
     =⟨⟩
      not false
     =⟨⟩
     true
   end

demorgan3 : (a b c d : Bool) → (not (a || b || c || d)) ≡ ((not a) && (not b) && (not c) && (not d))
demorgan3 true b c d = refl
demorgan3 false true c d = refl
demorgan3 false false true d = refl
demorgan3 false false false true = refl
demorgan3 false false false false = refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Several kinds of "relatedness" for containers such as equivalences,
-- surjections and bijections
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Container.Related where

open import Level using (_⊔_)
open import Data.Container.Core
import Function.Related as Related
open import Relation.Binary
open import Data.Container.Membership

open Related public
  using (Kind; Symmetric-kind)
  renaming ( implication         to subset
           ; reverse-implication to superset
           ; equivalence         to set
           ; injection           to subbag
           ; reverse-injection   to superbag
           ; bijection           to bag
           )

[_]-Order : ∀ {s p ℓ} → Kind → Container s p → Set ℓ →
            Preorder (s ⊔ p ⊔ ℓ) (s ⊔ p ⊔ ℓ) (p ⊔ ℓ)
[ k ]-Order C X = Related.InducedPreorder₂ k (_∈_ {C = C} {X = X})

[_]-Equality : ∀ {s p ℓ} → Symmetric-kind → Container s p → Set ℓ →
               Setoid (s ⊔ p ⊔ ℓ) (p ⊔ ℓ)
[ k ]-Equality C X = Related.InducedEquivalence₂ k (_∈_ {C = C} {X = X})

infix 4 _∼[_]_
_∼[_]_ : ∀ {s p x} {C : Container s p} {X : Set x} →
         ⟦ C ⟧ X → Kind → ⟦ C ⟧ X → Set (p ⊔ x)
_∼[_]_ {C = C} {X} xs k ys = Preorder._∼_ ([ k ]-Order C X) xs ys


text:
{-# OPTIONS --without-K #-}

module EquivEquiv where

open import Level using (Level; _⊔_)
open import Data.Product using (_,_; proj₁; proj₂)
open import Data.Sum using (inj₁; inj₂)

open import Relation.Binary using (Setoid)
import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)

import Relation.Binary.EqReasoning as EqR

open import Function using (id; _∘_)

open import Equiv
 using (module isqinv; qinv; _≃_; id≃; sym≃; _●_;
   _∼_; refl∼; sym∼; trans∼; cong∘r; cong∘l;
   _⊎≃_; β₁; β₂; gg; β⊎₁; β⊎₂)

------------------------------------------------------------------------------
-- Extensional equivalence of equivalences

-- We need g to "pin down" the inverse, else we get lots of unsolved
-- metas.

infix 4 _≋_

record _≋_ {ℓ ℓ' : Level} {A : Set ℓ} {B : Set ℓ'} (eq₁ eq₂ : A ≃ B) :
  Set (ℓ ⊔ ℓ') where
  constructor eq
  open isqinv
  field
    f≡ : proj₁ eq₁ ∼ proj₁ eq₂
    g≡ : g (proj₂ eq₁) ∼ g (proj₂ eq₂)

  -- the proof could use ∼-Reasoning if we had defined it
  g≡′ : g (proj₂ eq₁) ∼ g (proj₂ eq₂)
  g≡′ =
    trans∼ (cong∘r g₁ (refl∼ {f = id})) ( -- id ∘ g₁
    trans∼ (cong∘r g₁ (sym∼ (β (proj₂ eq₂))))
    (trans∼ (cong∘l g₂ (cong∘r g₁ (sym∼ f≡))) (
                  (cong∘l g₂ (α (proj₂ eq₁))))))
    where
      g₁ = g (proj₂ eq₁)
      g₂ = g (proj₂ eq₂)
      f₁ = proj₁ eq₁
      f₂ = proj₁ eq₂

-- The equivalence of equivalences is an equivalence relation that
-- respects composition

id≋ : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {x : A ≃ B} → x ≋ x
id≋ = record { f≡ = λ _ → P.refl ; g≡ = λ _ → P.refl }

sym≋ : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {x y : A ≃ B} → x ≋ y → y ≋ x
sym≋ (eq f≡ g≡) = eq (λ a → P.sym (f≡ a)) (λ b → P.sym (g≡ b))

flip≋ : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {x y : A ≃ B} →
        x ≋ y → (sym≃ x) ≋ (sym≃ y)
flip≋ (eq f≡ g≡) = eq g≡ f≡

flip-sym≋ :  ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {x y : A ≃ B}→
        x ≋ y → sym≃ y ≋ sym≃ x
flip-sym≋ (eq f≡ g≡) = eq (sym∼ g≡) (sym∼ f≡)

trans≋ : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} {x y z : A ≃ B} →
         x ≋ y → y ≋ z → x ≋ z
trans≋ (eq f≡ g≡) (eq h≡ i≡) =
   eq (λ a → P.trans (f≡ a) (h≡ a)) (λ b → P.trans (g≡ b) (i≡ b))

_◎_ : {A B C : Set} {f h : B ≃ C} {g i : A ≃ B} → f ≋ h → g ≋ i →
  (f ● g) ≋ (h ● i)
_◎_ {f = f} {h} {g} {i}
  (eq f≡ g≡) (eq h≡ i≡) = eq fwd bwd
  -- eq (λ x → {!!} ) -- P.trans (P.cong f (h≡ x)) (f≡ (i x)))
  --   (λ x → {!!} ) -- P.trans (P.cong g⁻¹ (g≡ x)) (i≡ (h⁻¹ x)))
  where
    open P.≡-Reasoning
    fwd : proj₁  (f ● g) ∼ proj₁ (h ● i)
    fwd x =  begin (
      proj₁ (f ● g) x
        ≡⟨ β₁ x ⟩
      proj₁ f (proj₁ g x)
        ≡⟨ f≡ (proj₁ g x) ⟩
      proj₁ h (proj₁ g x)
        ≡⟨ P.cong (proj₁ h) (h≡ x) ⟩
      proj₁ h (proj₁ i x)
        ≡⟨ P.sym (β₁ x) ⟩
      proj₁ (h ● i) x ∎)
    bwd :  gg (f ● g) ∼ gg (h ● i)
    bwd x =
      begin (
        gg (f ● g) x
          ≡⟨ β₂ x ⟩
        gg g (gg f x)
          ≡⟨ i≡ (gg f x) ⟩
        gg i (gg f x)
          ≡⟨ P.cong (gg i) (g≡ x) ⟩
        gg i (gg h x)
          ≡⟨ P.sym (β₂ x) ⟩
        gg (h ● i) x ∎)

rinv≋ : ∀ {ℓ} {A B : Set ℓ} (x : A ≃ B) →
  (x ● (sym≃ x)) ≋ id≃ {A = B}
rinv≋ (_ , qinv _ α _) = eq (trans∼ β₁ α) (trans∼ β₂ α)

linv≋ : ∀ {ℓ} {A B : Set ℓ} (e : A ≃ B) → ((sym≃ e) ● e) ≋ id≃
linv≋ (_ , qinv _ _ β) = eq (trans∼ β₁ β) (trans∼ β₂ β)

lid≋ : ∀ {ℓ} {A B : Set ℓ} {f : A ≃ B} → (id≃ ● f) ≋ f
lid≋ = eq β₁ β₂

rid≋ : ∀ {ℓ} {A B : Set ℓ} {f : A ≃ B} → (f ● id≃) ≋ f
rid≋ = eq β₁ β₂

--
{-
symsym : ∀ {A B : Set} {f : A ≃ B} → sym≃ (sym≃ f) ≋ f
symsym = eq (λ _ → P.refl) (λ _ → P.refl)
-}

sym≃● : ∀ {A B C : Set} {g : B ≃ C} {f : A ≃ B} →
        sym≃ (g ● f) ≋ sym≃ f ● sym≃ g
sym≃● {g = (g , qinv g⁻¹ _ _)} {(f , qinv f⁻¹ _ _)} =
  eq (trans∼ β₂ (sym∼ β₁)) (trans∼ β₁ (sym∼ β₂))

-- underlying it all, it uses ∘ and ≡, thus associativity is immediate

●-assoc : {A B C D : Set} {f : A ≃ B} {g : B ≃ C} {h : C ≃ D} →
      ((h ● g) ● f) ≋ (h ● (g ● f))
●-assoc {f = f} {g} {h} = eq fwd bwd
  where
    open P.≡-Reasoning
    fwd : proj₁ ((h ● g) ● f) ∼ proj₁ (h ● (g ● f))
    fwd x = begin (
       proj₁ ((h ● g) ● f) x
         ≡⟨ β₁ x ⟩
      proj₁ (h ● g) (proj₁ f x)
         ≡⟨ β₁ (proj₁ f x) ⟩
      proj₁ h (proj₁ g (proj₁ f x))
         ≡⟨ P.cong (proj₁ h) (P.sym (β₁ x)) ⟩
      proj₁ h (proj₁ (g ● f) x)
         ≡⟨ P.sym (β₁ x) ⟩
       proj₁ (h ● (g ● f)) x ∎)
    bwd : gg ((h ● g) ● f) ∼ gg (h ● (g ● f))
    bwd x = begin (
      gg ((h ● g) ● f) x
         ≡⟨ β₂ x ⟩
      gg f (gg (h ● g) x)
         ≡⟨ P.cong (gg f) (β₂ x) ⟩
      gg f (gg g (gg h x))
         ≡⟨ P.sym (β₂ (gg h x)) ⟩
      gg (g ● f) (gg h x)
         ≡⟨ P.sym (β₂ x) ⟩
      gg (h ● (g ● f)) x ∎)

●-assocl : {A B C D : Set} {f : A ≃ B} {g : B ≃ C} {h : C ≃ D} →
       h ● (g ● f) ≋ (h ● g) ● f
●-assocl {f = f} {g} {h} = sym≋ (●-assoc {f = f} {g} {h})

-- The setoid of equivalences under ≋

_S≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Setoid (ℓ ⊔ ℓ') (ℓ ⊔ ℓ')
_S≃_ A B = record
 { Carrier = A ≃ B
 ; _≈_ = _≋_
 ; isEquivalence = record
   { refl = id≋
   ; sym = sym≋
   ; trans = trans≋
   }
 }

module ≋-Reasoning where
  module _ {a b} {A : Set a} {B : Set b} where
    open EqR (A S≃ B) public
      hiding (_≡⟨_⟩_; _≡⟨⟩_) renaming (_≈⟨_⟩_ to _≋⟨_⟩_)

------------------------------------------------------------------------------

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module Cats.Functor where

open import Level
open import Relation.Binary using (_Preserves_⟶_)

open import Cats.Category.Base
open import Cats.Util.Function using () renaming (_∘_ to _⊙_)
open import Cats.Util.SetoidMorphism using (_⇒_ ; IsInjective ; IsSurjective)
open import Cats.Util.SetoidMorphism.Iso using
  ( IsIso ; _≅_ ; IsIso→≅ ; Injective∧Surjective→Iso ; Iso→Injective
  ; Iso→Surjective )

import Cats.Category.Constructions.Iso as Iso

open Iso.Build._≅_

infixr 9 _∘_

record Functor {lo la l≈ lo′ la′ l≈′}
  (C : Category lo la l≈)
  (D : Category lo′ la′ l≈′)
  : Set (lo ⊔ la ⊔ l≈ ⊔ lo′ ⊔ la′ ⊔ l≈′) where
  private
    module C = Category C
    module C≅ = Iso.Build C
    module D = Category D
    module D≅ = Iso.Build D

  field
    fobj : C.Obj → D.Obj
    fmap : ∀ {A B} → A C.⇒ B → fobj A D.⇒ fobj B
    fmap-resp : ∀ {A B} → fmap {A} {B} Preserves C._≈_ ⟶ D._≈_
    fmap-id : ∀ {A} → fmap (C.id {A}) D.≈ D.id
    fmap-∘ : ∀ {A B C} {f : B C.⇒ C} {g : A C.⇒ B}
      → fmap f D.∘ fmap g D.≈ fmap (f C.∘ g)

  sfmap : ∀ {a b} → C.Hom a b ⇒ D.Hom (fobj a) (fobj b)
  sfmap = record
      { arr = fmap
      ; resp = fmap-resp
      }

  fobj-resp : fobj Preserves C≅._≅_ ⟶ D≅._≅_
  fobj-resp {i} {j} x≅y
      = record
      { forth = fmap (forth x≅y)
      ; back = fmap (back x≅y)
      ; back-forth
          = begin
              fmap (back x≅y) D.∘ fmap (forth x≅y)
            ≈⟨ fmap-∘ ⟩
              fmap (back x≅y C.∘ forth x≅y)
            ≈⟨  fmap-resp (back-forth x≅y) ⟩
              fmap C.id
            ≈⟨ fmap-id ⟩
              D.id
            ∎
      ; forth-back
          = begin
            fmap (forth x≅y) D.∘ fmap (back x≅y)
          ≈⟨ fmap-∘ ⟩
            fmap (forth x≅y C.∘ back x≅y)
          ≈⟨ fmap-resp (forth-back x≅y) ⟩
            fmap C.id
          ≈⟨ fmap-id ⟩
            D.id
          ∎
      }
    where
      open D.≈-Reasoning

open Functor public

id : ∀ {lo la l≈} {C : Category lo la l≈} → Functor C C
id {C = C} = record
    { fobj = λ x → x
    ; fmap = λ f → f
    ; fmap-resp = λ eq → eq
    ; fmap-id = C.≈.refl
    ; fmap-∘ = C.≈.refl
    }
  where
    module C = Category C

_∘_ : ∀ {lo la l≈ lo′ la′ l≈′ lo″ la″ l≈″}
  → {C : Category lo la l≈}
  → {D : Category lo′ la′ l≈′}
  → {E : Category lo″ la″ l≈″}
  → Functor D E → Functor C D → Functor C E
_∘_ {E = E} F G = record
    { fobj = fobj F ⊙ fobj G
    ; fmap = fmap F ⊙ fmap G
    ; fmap-resp = fmap-resp F ⊙ fmap-resp G
    ; fmap-id = E.≈.trans (fmap-resp F (fmap-id G)) (fmap-id F)
    ; fmap-∘ = E.≈.trans (fmap-∘ F) (fmap-resp F (fmap-∘ G))
    }
  where
    module E = Category E

module _ {lo la l≈ lo′ la′ l≈′}
  {C : Category lo la l≈} {D : Category lo′ la′ l≈′}
  (F : Functor C D)
  where

  private
    module C = Category C
    module D = Category D

  IsFaithful : Set (lo ⊔ la ⊔ l≈ ⊔ l≈′)
  IsFaithful = ∀ {a b} → IsInjective (sfmap F {a} {b})

  IsFull : Set (lo ⊔ la ⊔ la′ ⊔ l≈′)
  IsFull = ∀ {a b} → IsSurjective (sfmap F {a} {b})

  IsEmbedding : Set (lo ⊔ la ⊔ l≈ ⊔ la′ ⊔ l≈′)
  IsEmbedding = ∀ {a b} → IsIso (sfmap F {a} {b})

  Embedding→≅ : IsEmbedding → ∀ {a b} → C.Hom a b ≅ D.Hom (fobj F a) (fobj F b)
  Embedding→≅ embedding = IsIso→≅ (sfmap F) embedding

  Full∧Faithful→Embedding : IsFull → IsFaithful → IsEmbedding
  Full∧Faithful→Embedding full faithful
      = Injective∧Surjective→Iso faithful full

  Embedding→Full : IsEmbedding → IsFull
  Embedding→Full embedding = Iso→Surjective embedding

  Embedding→Faithful : IsEmbedding → IsFaithful
  Embedding→Faithful embedding = Iso→Injective embedding

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
{-# OPTIONS --prop --without-K --rewriting #-}

-- Step effect.

open import Calf.CostMonoid

module Calf.Step (costMonoid : CostMonoid) where

open CostMonoid costMonoid

open import Calf.Prelude
open import Calf.Metalanguage
open import Calf.PhaseDistinction
open import Relation.Binary.PropositionalEquality

cost : tp neg
cost = meta ℂ

postulate
  step : ∀ (B : tp neg) → cmp cost → cmp B → cmp B
  step/id : ∀ {B : tp neg} {e : cmp B} →
    step B zero e ≡ e
  {-# REWRITE step/id #-}
  step/concat : ∀ {B e p q} →
    step B p (step B q e) ≡ step B (p + q) e
  {-# REWRITE step/concat #-}

  U_step : ∀ {A} {X : val A → tp neg} {e n} → U (tbind {A} (step (F A) n e) X) ≡ U (tbind {A} e X)
  {-# REWRITE U_step #-}

  Π/step : ∀ {A} {X : val A → tp neg} {f : cmp (Π A X)} {n} → step (Π A X) n f ≡ λ x → step (X x) n (f x)
  {-# REWRITE Π/step #-}

  bind/step : ∀ {A} {X} {e f n} → bind {A} X (step (F A) n e) f ≡ step X n (bind {A} X e f)
  dbind/step : ∀ {A} {X : val A → tp neg} {e f n} → dbind {A} X (step (F A) n e) f ≡ step (tbind {A} e X) n (dbind {A} X e f)
  {-# REWRITE bind/step dbind/step #-}

  step/ext : ∀ X → (e : cmp X) → (c : ℂ) → ◯ (step X c e ≡ e)
  -- sadly the above cannot be made an Agda rewrite rule

max_stars_repo_name: jonsterling/agda-calf

max_issues_repo_name: jonsterling/agda-calf

max_forks_repo_name: jonsterling/agda-calf


text:
open import Prelude hiding (module Fin) renaming (_≟_ to _N≟_)

module Implicits.Syntax.Type where

open import Data.Fin.Substitution
open import Data.Nat.Properties as NatProps
open import Data.Star using (Star; ε; _◅_)
open import Data.List
open import Data.List.All hiding (map)
open import Data.Maybe hiding (map; All)
open import Data.Product hiding (map)
open import Data.Fin as Fin hiding (_+_)
open import Data.Fin.Properties as FinProp using ()

open import Extensions.Nat

import Data.Vec

infixr 10 _→'_
infixr 10 _⇒_

mutual
  data SimpleType (ν : ℕ) : Set where
    tc   : ℕ → SimpleType ν
    tvar : (n : Fin ν) → SimpleType ν
    _→'_ : Type ν → Type ν → SimpleType ν

  data Type (ν : ℕ) : Set where
    simpl : SimpleType ν → Type ν
    _⇒_  : Type ν → Type ν → Type ν
    ∀'   : Type (suc ν) → Type ν

TVar : ∀ {ν} → Fin ν → Type ν
TVar = simpl ∘ tvar

TC : ∀ {ν} → ℕ → Type ν
TC = simpl ∘ tc

is-∀' : ∀ {ν} → Type ν → Set
is-∀' (simpl x) = ⊥
is-∀' (_ ⇒ _) = ⊥
is-∀' (∀' x) = ⊤

fvars : ∀ {ν} → Type ν → List (Fin ν)
fvars (simpl (tc x)) = List.[]
fvars (simpl (tvar n)) = n List.∷ List.[]
fvars (simpl (x →' y)) = fvars x ++ fvars y
fvars (a ⇒ b) = fvars a ++ fvars b
fvars (∀' a) = gfilter (λ{ (Fin.zero) → nothing; (suc n) → just n}) (fvars a)

occ : ∀ {ν} → ℕ → Type ν → ℕ
occ α (simpl (tc x)) = 0
occ α (simpl (tvar n)) with α N≟ (toℕ n)
occ α (simpl (tvar n)) | yes p = 1
occ α (simpl (tvar n)) | no ¬p = 0
occ α (simpl (a →' b)) = occ α a + occ α b
occ α (a ⇒ b) = occ α a + occ α b
occ α (∀' b) = occ α b

module Functions where

  -- proposition that states that the given polytype
  -- is a (possibly polymorphic) function
  data IsFunction {ν : ℕ} : Type ν → Set where
    lambda : (a b : Type ν) → IsFunction (simpl $ a →' b)
    ∀'-lambda : ∀ {f} → IsFunction f → IsFunction (∀' f)

  -- decision procedure for IsFunction
  is-function : ∀ {ν} → (a : Type ν) → Dec (IsFunction a)
  is-function (simpl (tc _)) = no (λ ())
  is-function (simpl (tvar n)) = no (λ ())
  is-function (simpl (a →' b)) = yes (lambda a b)
  is-function (x ⇒ x₁) = no (λ ())
  is-function (∀' a) with is-function a
  is-function (∀' a) | yes a-is-f = yes $ ∀'-lambda a-is-f
  is-function (∀' a) | no a-not-f = no (λ{ (∀'-lambda a-is-f) → a-not-f a-is-f })

  domain : ∀ {ν} {f : Type ν} → IsFunction f → Type ν
  domain (lambda a b) = a
  domain (∀'-lambda f) = ∀' (domain f)

  codomain : ∀ {ν} {f : Type ν} → IsFunction f → Type ν
  codomain (lambda a b) = b
  codomain (∀'-lambda f) = ∀' (codomain f)

module Rules where

  -- proposition that states that the given polytype
  -- is a (possibly polymorphic) rule type
  data IsRule {ν : ℕ} : Type ν → Set where
    rule : (a b : Type ν) → IsRule (a ⇒ b)
    ∀'-rule : ∀ {f} → IsRule f → IsRule (∀' f)

  -- decision procedure for IsRule
  is-rule : ∀ {ν} → (a : Type ν) → Dec (IsRule a)
  is-rule (simpl (tc _)) = no (λ ())
  is-rule (simpl (tvar n)) = no (λ ())
  is-rule (simpl (a →' b)) = no (λ ())
  is-rule (a ⇒ b)  = yes (rule a b)
  is-rule (∀' a) with is-rule a
  is-rule (∀' a) | yes a-is-f = yes $ ∀'-rule a-is-f
  is-rule (∀' a) | no a-not-f = no (λ{ (∀'-rule a-is-f) → a-not-f a-is-f })

  domain : ∀ {ν} {f : Type ν} → IsRule f → Type ν
  domain (rule a b) = a
  domain (∀'-rule f) = ∀' (domain f)

  codomain : ∀ {ν} {f : Type ν} → IsRule f → Type ν
  codomain (rule a b) = b
  codomain (∀'-rule f) = ∀' (codomain f)

  to-function : ∀ {ν} {f : Type ν} → IsRule f → Type ν
  to-function (rule a b) = simpl (a →' b)
  to-function (∀'-rule f) = ∀' (to-function f)

-- decidable equality on types
_≟_ : ∀ {ν} → (a b : Type ν) → Dec (a ≡ b)
simpl (tc x) ≟ simpl (tc y) with x N≟ y
simpl (tc x) ≟ simpl (tc y) | yes p = yes (cong (simpl ∘ tc) p)
simpl (tc x) ≟ simpl (tc y) | no ¬p = no (λ x=y → ¬p $ helper x=y )
  where
    helper : ∀ {x y} → (simpl (tc x)) ≡ (simpl (tc y)) → x ≡ y
    helper refl = refl
simpl (tc x) ≟ simpl (tvar n) = no (λ ())
simpl (tc x) ≟ simpl (x₁ →' x₂) = no (λ ())
simpl (tvar n) ≟ simpl (tc x) = no (λ ())
simpl (tvar n) ≟ simpl (tvar m) with n FinProp.≟ m
simpl (tvar n) ≟ simpl (tvar m) | yes n≡m = yes (cong (simpl ∘ tvar) n≡m)
simpl (tvar n) ≟ simpl (tvar m) | no n≢m = no (λ x=y → n≢m $ helper x=y)
  where
    helper : ∀ {n m} → (simpl (tvar n)) ≡ (simpl (tvar m)) → n ≡ m
    helper refl = refl
simpl (tvar n) ≟ simpl (x →' x₁) = no (λ ())
simpl (a →' b) ≟ simpl (tc x₂) = no (λ ())
simpl (a →' b) ≟ simpl (tvar n) = no (λ ())
simpl (a →' b) ≟ simpl (a' →' b') with a ≟ a' | b ≟ b'
simpl (a →' b) ≟ simpl (a' →' b') | yes p | yes q = yes (cong₂ (λ u v → simpl $ u →' v) p q)
simpl (a →' b) ≟ simpl (a' →' b') | yes p | no ¬q = no (λ x → ¬q (helper x) )
   where
     helper : ∀ {a b a' b'} → (simpl $ a →' b) ≡ (simpl $ a' →' b') → b ≡ b'
     helper refl = refl
simpl (a →' b) ≟ simpl (a' →' b') | no ¬p | _ = no (λ x → ¬p (helper x) )
   where
     helper : ∀ {a b a' b'} → (simpl $ a →' b) ≡ (simpl $ a' →' b') → a ≡ a'
     helper refl = refl
simpl (tc x) ≟ (b ⇒ b₁) = no (λ ())
simpl (tvar n) ≟ (b ⇒ b₁) = no (λ ())
simpl (x →' x₁) ≟ (b ⇒ b₁) = no (λ ())
simpl (tc x) ≟ ∀' b = no (λ ())
simpl (tvar n) ≟ ∀' b = no (λ ())
simpl (x →' x₁) ≟ ∀' b = no (λ ())
(a ⇒ b) ≟ simpl x = no (λ ())
(a ⇒ b) ≟ (a' ⇒ b') with a ≟ a' | b ≟ b'
(a ⇒ b) ≟ (a' ⇒ b') | yes p | yes q = yes (cong₂ (λ u v → u ⇒ v) p q)
(a ⇒ b) ≟ (a' ⇒ b') | yes p | no ¬q = no (λ x → ¬q (helper x) )
   where
     helper : ∀ {a b a' b'} → (a ⇒ b) ≡ (a' ⇒ b') → b ≡ b'
     helper refl = refl
(a ⇒ b) ≟ (a' ⇒ b') | no ¬p | _ = no (λ x → ¬p (helper x) )
   where
     helper : ∀ {a b a' b'} → (a ⇒ b) ≡ (a' ⇒ b') → a ≡ a'
     helper refl = refl
(a ⇒ a₁) ≟ ∀' b = no (λ ())
∀' a ≟ simpl x = no (λ ())
∀' a ≟ (b ⇒ b₁) = no (λ ())
∀' a ≟ ∀' b with a ≟ b
∀' a ≟ ∀' b | yes p = yes (cong ∀' p)
∀' a ≟ ∀' b | no ¬p = no (λ u → ¬p (helper u))
    where
      helper : ∀ {ν} {a b : Type (suc ν)} → ∀' a ≡ ∀' b → a ≡ b
      helper refl = refl

-- 'head' of the context type
_◁ : ∀ {ν} → Type ν → ∃ λ μ → Type μ
simpl x ◁ = , simpl x
(a ⇒ b) ◁ = b ◁
∀' a ◁ = a ◁

mutual
  data occ' {ν} : Fin ν → Type ν → Set where
    ⇒-left : ∀ {n a b} → (occ' n a) → occ' n (a ⇒ b)
    ⇒-right : ∀ {n a b} → (occ' n b) → occ' n (a ⇒ b)
    ∀' : ∀ {a n} → (occ' (suc n) a) → occ' n (∀' a)

  data occS {ν} : Fin ν → SimpleType ν → Set where
    tvar    : (n : Fin ν) → occS n (tvar n)
    →'-left : ∀ {n a b} → (occ' n a) → occS n (a →' b)
    →'-right : ∀ {n a b} → (occ' n b) → occS n (a →' b)

  data _⊢unamb_ {ν} : List (Fin ν) → Type ν → Set where
    ua-simp : ∀ l {τ} → All (λ e → occS e τ) l → l ⊢unamb (simpl τ)
    ua-iabs : ∀ {l a b} → l ⊢unamb b → [] ⊢unamb a → l ⊢unamb (a ⇒ b)
    ua-tabs : ∀ {l} {a : Type (suc ν)} → (zero List.∷ (map suc l)) ⊢unamb a →
              l ⊢unamb (∀' a)

module unamb-test where

  x : Type 1
  x = ∀' (simpl (tvar zero))

  px : [] ⊢unamb x
  px = ua-tabs (ua-simp (zero ∷ []) (tvar zero All.∷ All.[]))

  y : Type 1
  y = ∀' (simpl (tvar (suc zero)))

  ¬py : ¬ ([] ⊢unamb y)
  ¬py (ua-tabs (ua-simp .(zero ∷ []) (() All.∷ x)))

  z : Type 1
  z = ∀' (β ⇒ α)
    where
      α = (simpl (tvar zero))
      β = (simpl (tvar (suc zero)))

  pz : [] ⊢unamb z
  pz = ua-tabs
         (ua-iabs (ua-simp (zero ∷ []) (tvar zero All.∷ All.[]))
          (ua-simp [] All.[]))

  z' : Type 1
  z' = ∀' (α ⇒ β)
    where
      α = (simpl (tvar zero))
      β = (simpl (tvar (suc zero)))

  ¬pz' : ¬ ([] ⊢unamb z')
  ¬pz' (ua-tabs (ua-iabs (ua-simp .(zero ∷ []) (() All.∷ pxs)) x₁))

  read∘show : Type 1
  read∘show = ∀' ((simpl (string →' α)) ⇒ ((simpl (α →' string)) ⇒ (simpl (string →' string))))
    where
      α = (simpl (tvar zero))
      string = (simpl (tvar (suc zero)))

  ¬pread∘show : ¬ [] ⊢unamb read∘show
  ¬pread∘show (ua-tabs (ua-iabs (ua-iabs (ua-simp .(zero ∷ []) (→'-left () All.∷ _)) _) _))
  ¬pread∘show (ua-tabs (ua-iabs (ua-iabs (ua-simp .(zero ∷ []) (→'-right () All.∷ _)) _) _))

open unamb-test


text:
module Lectures.Three where

open import Lectures.One
open import Lectures.Two

-- Introduce propositional equality

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}

-- Comment on precendences
infix 10 _≡_

record Equivalence (_~_ : ∀ {A : Set} → A → A → Set) : Set₁ where
  field
    reflexive  : ∀ {A} {a : A} → a ~ a
    symmetric  : ∀ {A} {a b : A} → a ~ b → b ~ a
    transitive : ∀ {A} {a b c : A} → a ~ b → b ~ c → a ~ c

open Equivalence

sym : ∀ {A} {a b : A} → a ≡ b → b ≡ a
sym refl = refl

trans : ∀ {A} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans refl refl = refl

-- Comment on copatterns
≡-Equivalence : Equivalence _≡_
reflexive ≡-Equivalence = refl
symmetric ≡-Equivalence = sym
transitive ≡-Equivalence = trans

cong : ∀ {A B} {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b
cong f refl = refl

-- Leibniz equality?
subst : ∀ {A} {x y : A} {P : A → Set} → P x → x ≡ y → P y
subst p refl = p

_ : _+_ ≡ _+_
_ = refl

-- _ : _+_ ≡ λ x y → y + x
-- _ = {!refl!}

-- Comment on postulates
postulate
  extensionality : {A B : Set} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g

+-idʳ : ∀ x → x ≡ x + 0
+-idʳ zero = refl
+-idʳ (suc x) = cong suc (+-idʳ _)

+-suc : ∀ x y → suc (x + y) ≡ x + suc y
+-suc zero y = refl
+-suc (suc x) y = cong suc (+-suc _ _)

+-comm : ∀ x y → x + y ≡ y + x
+-comm zero y = +-idʳ _
+-comm (suc x) y = trans (cong suc (+-comm x y)) (+-suc _ _)

+-assoc : ∀ x y z → x + (y + z) ≡ (x + y) + z
+-assoc zero y z = refl
+-assoc (suc x) y z = cong suc (+-assoc x y z)


text:
{-# OPTIONS --universe-polymorphism #-}

module Categories.Support.SetoidFunctions where

open import Level
open import Function using (_on_)
open import Relation.Binary as B using (_=[_]⇒_)
open import Relation.Binary.PropositionalEquality using () renaming (cong to ≡-cong; cong₂ to ≡-cong₂)
open import Data.Product using (<_,_>; _×_; _,_)

open import Categories.Support.Equivalence

infixr 0 _⟶_

record _⟶_ {cf ℓf ct ℓt} (From : Setoid cf ℓf) (To : Setoid ct ℓt) :
         Set (cf ⊔ ℓf ⊔ ct ⊔ ℓt) where
  infixl 5 _⟨$⟩_
  field
    _⟨$⟩_ : (x : Setoid.Carrier From) → Setoid.Carrier To
    .cong  : Setoid._≈_ From =[ _⟨$⟩_ ]⇒ Setoid._≈_ To

open _⟶_ public

id : ∀ {a₁ a₂} {A : Setoid a₁ a₂} → A ⟶ A
id = record { _⟨$⟩_ = Function.id; cong = Function.id }

infixr 9 _∙_

_∙_ : ∀ {ca ℓa} {A : Setoid ca ℓa}
        {cb ℓb} {B : Setoid cb ℓb}
        {cc ℓc} {C : Setoid cc ℓc} →
      B ⟶ C → A ⟶ B → A ⟶ C
f ∙ g = record
  { _⟨$⟩_ = Function._∘_ (_⟨$⟩_ f) (_⟨$⟩_ g)
  ; cong = Function._∘_ (cong f) (cong g)
  }

const : ∀ {ca ℓa} {A : Setoid ca ℓa}
          {cb ℓb} {B : Setoid cb ℓb} →
        Setoid.Carrier B → A ⟶ B
const {B = B} b = record
  { _⟨$⟩_ = Function.const b
  ; cong = Function.const (Setoid.refl B)
  }

→-to-⟶ : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → (set→setoid A ⟶ set→setoid B)
→-to-⟶ f = record { _⟨$⟩_ = f; cong = ≡-cong f }

------------------------------------------------------------------------
-- Function setoids

setoid : ∀ {cf ℓf ct ℓt}
         (From : Setoid cf ℓf) →
         Setoid ct ℓ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 = Setoid To using () renaming (_≈_ to _≈₂_)

infixr 0 _⇨_

_⇨_ : ∀ {cf ℓf ct ℓt} → Setoid cf ℓf → Setoid ct ℓt → Setoid _ _
From ⇨ To = setoid From To

⟪_,_⟫ : ∀ {cf ℓf ct₁ ℓt₁ ct₂ ℓt₂} {From : Setoid cf ℓf} {To₁ : Setoid ct₁ ℓt₁} {To₂ : Setoid ct₂ ℓt₂} (f₁ : From ⟶ To₁) (f₂ : From ⟶ To₂) → (From ⟶ (To₁ ×-setoid To₂))
⟪ f₁ , f₂ ⟫ = record { _⟨$⟩_ = < (_⟨$⟩_ f₁) , (_⟨$⟩_ f₂) >
                     ; cong = < cong f₁ , cong f₂ > }

⟪_,_⟫′ : ∀ {cf ℓf ct₁ ct₂} {From : Setoid cf ℓf} {To₁ : Set ct₁} {To₂ : Set ct₂} (f₁ : From ⟶ set→setoid To₁) (f₂ : From ⟶ set→setoid To₂) → (From ⟶ set→setoid (To₁ × To₂))
⟪ f₁ , f₂ ⟫′ = record { _⟨$⟩_ = < (_⟨$⟩_ f₁) , (_⟨$⟩_ f₂) >
                      ; cong = λ x≈y → ≡-cong₂ _,_ (cong f₁ x≈y) (cong f₂ x≈y) }

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --without-K --exact-split --safe #-}

module Fragment.Equational.Theory.Base where

open import Function using (_∘_)

open import Fragment.Algebra.Signature
open import Fragment.Algebra.Free
open import Fragment.Algebra.Algebra
open import Fragment.Algebra.Properties

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)
open import Data.Product using (_×_; map)

Eq : (Σ : Signature) → (n : ℕ) → Set
Eq Σ n = ∥ F Σ n ∥ × ∥ F Σ n ∥

record Theory : Set₁ where
  field
    Σ     : Signature
    eqs   : ℕ → Set
    _⟦_⟧ₑ : ∀ {arity} → eqs arity → Eq Σ arity

  open Signature Σ

open Theory public

data ExtendedEq (Θ : Theory) (E : ℕ → Set) : ℕ → Set where
  newₑ : ∀ {n} → E n → ExtendedEq Θ E n
  oldₑ : ∀ {n} → eqs Θ n → ExtendedEq Θ E n

_⦅_⦆ₒ : (Θ : Theory) → (O : ℕ → Set) → Theory
Θ ⦅ O ⦆ₒ = record { Σ     = (Σ Θ) ⦅ O ⦆
                  ; eqs   = eqs Θ
                  ; _⟦_⟧ₑ = (map extend extend) ∘ Θ ⟦_⟧ₑ
                  }

_⦅_/_⦆ : (Θ : Theory)
         → (E : ℕ → Set)
         → (∀ {n} → E n → Eq (Σ Θ) n)
         → Theory
Θ ⦅ E / ⟦_⟧' ⦆ = record { Σ     = Σ Θ
                        ; eqs   = ExtendedEq Θ E
                        ; _⟦_⟧ₑ = withE
                        }
  where withE : ∀ {n} → ExtendedEq Θ E n → Eq (Σ Θ) n
        withE (newₑ eq) = ⟦ eq ⟧'
        withE (oldₑ eq) = Θ ⟦ eq ⟧ₑ

_⦅_∣_/_⦆ : (Θ : Theory)
           → (O : ℕ → Set)
           → (E : ℕ → Set)
           → (∀ {n} → E n → Eq ((Σ Θ) ⦅ O ⦆) n)
           → Theory
Θ ⦅ O ∣ E / ⟦_⟧' ⦆ = (Θ ⦅ O ⦆ₒ) ⦅ E / ⟦_⟧' ⦆

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Group.Algebra where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Function using (_∘_)
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Sigma
open import Cubical.Data.Unit

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphism
open import Cubical.Algebra.Group.MorphismProperties

open import Cubical.HITs.PropositionalTruncation hiding (map)

open Iso
open GroupHom

private
  variable
    ℓ ℓ' ℓ₁ ℓ₂ ℓ₃ : Level

------- elementary properties of morphisms --------

module _ (G : Group {ℓ}) (H : Group {ℓ'}) where

  module G = GroupStr (snd G)
  module H = GroupStr (snd H)

  -0≡0 : G.- G.0g ≡ G.0g
  -0≡0 = sym (G.lid _) ∙ G.invr _

  -- ϕ(0) ≡ 0
  morph0→0 : (f : GroupHom G H) → f .fun G.0g ≡ H.0g
  morph0→0 fh@(grouphom f _) =
    f G.0g                         ≡⟨ sym (H.rid _) ⟩
    f G.0g H.+ H.0g                ≡⟨ (λ i → f G.0g H.+ H.invr (f G.0g) (~ i)) ⟩
    f G.0g H.+ (f G.0g H.- f G.0g) ≡⟨ H.assoc _ _ _ ⟩
    (f G.0g H.+ f G.0g) H.- f G.0g ≡⟨ sym (cong (λ x → x H.+ (H.- f G.0g))
                                                (sym (cong f (G.lid _)) ∙ isHom fh G.0g G.0g)) ⟩
    f G.0g H.- f G.0g              ≡⟨ H.invr _ ⟩
    H.0g ∎

  -- ϕ(- x) = - ϕ(x)
  morphMinus : (f : GroupHom G H) → (g : ⟨ G ⟩) → f .fun (G.- g) ≡ H.- (f .fun g)
  morphMinus fc@(grouphom f fh) g =
    f (G.- g)                   ≡⟨ sym (H.rid _) ⟩
    f (G.- g) H.+ H.0g          ≡⟨ cong (f (G.- g) H.+_) (sym (H.invr _)) ⟩
    f (G.- g) H.+ (f g H.- f g) ≡⟨ H.assoc _ _ _ ⟩
    (f (G.- g) H.+ f g) H.- f g ≡⟨ cong (H._+ (H.- f g)) helper ⟩
    H.0g H.- f g                ≡⟨ H.lid _ ⟩
    H.- f g ∎
    where
    helper : f (G.- g) H.+ f g ≡ H.0g
    helper = sym (fh (G.- g) g) ∙∙ cong f (G.invl g) ∙∙ morph0→0 fc

-- ----------- Alternative notions of isomorphisms --------------
record GroupIso {ℓ ℓ'} (G : Group {ℓ}) (H : Group {ℓ'}) : Type (ℓ-max ℓ ℓ') where

  constructor iso
  field
    map : GroupHom G H
    inv : ⟨ H ⟩ → ⟨ G ⟩
    rightInv : section (GroupHom.fun map) inv
    leftInv : retract (GroupHom.fun map) inv

record BijectionIso {ℓ ℓ'} (A : Group {ℓ}) (B : Group {ℓ'}) : Type (ℓ-max ℓ ℓ') where

  constructor bij-iso
  field
    map' : GroupHom A B
    inj : isInjective A B map'
    surj : isSurjective A B map'

-- "Very" short exact sequences
-- i.e. an exact sequence A → B → C → D where A and D are trivial
record vSES {ℓ ℓ' ℓ'' ℓ'''} (A : Group {ℓ}) (B : Group {ℓ'}) (leftGr : Group {ℓ''}) (rightGr : Group {ℓ'''})
           : Type (ℓ-suc (ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓ'' ℓ''')))) where

  constructor ses
  field
    isTrivialLeft : isProp ⟨ leftGr ⟩
    isTrivialRight : isProp ⟨ rightGr ⟩

    left : GroupHom leftGr A
    right : GroupHom B rightGr
    ϕ : GroupHom A B

    Ker-ϕ⊂Im-left : (x : ⟨ A ⟩)
                  → isInKer A B ϕ x
                  → isInIm leftGr A left x
    Ker-right⊂Im-ϕ : (x : ⟨ B ⟩)
                   → isInKer B rightGr right x
                   → isInIm A B ϕ x

open BijectionIso
open GroupIso
open vSES

Iso+Hom→GrIso : {G : Group {ℓ}} {H : Group {ℓ₁}} → (e : Iso ⟨ G ⟩ ⟨ H ⟩) → isGroupHom G H (Iso.fun e) → GroupIso G H
fun (map (Iso+Hom→GrIso e hom)) = Iso.fun e
isHom (map (Iso+Hom→GrIso e hom)) = hom
inv (Iso+Hom→GrIso e hom) = Iso.inv e
rightInv (Iso+Hom→GrIso e hom) = Iso.rightInv e
leftInv (Iso+Hom→GrIso e hom) = Iso.leftInv e

compGroupIso : {G : Group {ℓ}} {H : Group {ℓ₁}} {A : Group {ℓ₂}} → GroupIso G H → GroupIso H A → GroupIso G A
map (compGroupIso iso1 iso2) = compGroupHom (map iso1) (map iso2)
inv (compGroupIso iso1 iso2) = inv iso1 ∘ inv iso2
rightInv (compGroupIso iso1 iso2) a = cong (fun (map iso2)) (rightInv iso1 _) ∙ rightInv iso2 a
leftInv (compGroupIso iso1 iso2) a = cong (inv iso1) (leftInv iso2 _) ∙ leftInv iso1 a

isGroupHomInv' : {G : Group {ℓ}} {H : Group {ℓ₁}} (f : GroupIso G H) → isGroupHom H G (inv f)
isGroupHomInv' {G = G} {H = H}  f h h' = isInj-f _ _ (
  f' (g (h ⋆² h')) ≡⟨ (rightInv f) _ ⟩
  (h ⋆² h') ≡⟨ sym (cong₂ _⋆²_ (rightInv f h) (rightInv f h')) ⟩
  (f' (g h) ⋆² f' (g h')) ≡⟨ sym (isHom (map f) _ _) ⟩
  f' (g h ⋆¹ g h') ∎)
  where
  f' = fun (map f)
  _⋆¹_ = GroupStr._+_ (snd G)
  _⋆²_ = GroupStr._+_ (snd H)
  g = inv f

  isInj-f : (x y : ⟨ G ⟩) → f' x ≡ f' y → x ≡ y
  isInj-f x y p = sym (leftInv f _) ∙∙ cong g p ∙∙ leftInv f _

invGroupIso : {G : Group {ℓ}} {H : Group {ℓ₁}} → GroupIso G H → GroupIso H G
fun (map (invGroupIso iso1)) = inv iso1
isHom (map (invGroupIso iso1)) = isGroupHomInv' iso1
inv (invGroupIso iso1) = fun (map iso1)
rightInv (invGroupIso iso1) = leftInv iso1
leftInv (invGroupIso iso1) = rightInv iso1

dirProdGroupIso : {G : Group {ℓ}} {H : Group {ℓ₁}} {A : Group {ℓ₂}} {B : Group {ℓ₃}}
               → GroupIso G H → GroupIso A B → GroupIso (dirProd G A) (dirProd H B)
fun (map (dirProdGroupIso iso1 iso2)) prod = fun (map iso1) (fst prod) , fun (map iso2) (snd prod)
isHom (map (dirProdGroupIso iso1 iso2)) a b = ΣPathP (isHom (map iso1) (fst a) (fst b) , isHom (map iso2) (snd a) (snd b))
inv (dirProdGroupIso iso1 iso2) prod = (inv iso1) (fst prod) , (inv iso2) (snd prod)
rightInv (dirProdGroupIso iso1 iso2) a = ΣPathP (rightInv iso1 (fst a) , (rightInv iso2 (snd a)))
leftInv (dirProdGroupIso iso1 iso2) a = ΣPathP (leftInv iso1 (fst a) , (leftInv iso2 (snd a)))

GrIsoToGrEquiv : {G : Group {ℓ}} {H : Group {ℓ₂}} → GroupIso G H → GroupEquiv G H
GroupEquiv.eq (GrIsoToGrEquiv i) = isoToEquiv (iso (fun (map i)) (inv i) (rightInv i) (leftInv i))
GroupEquiv.isHom (GrIsoToGrEquiv i) = isHom (map i)

--- Proofs that BijectionIso and vSES both induce isomorphisms ---
BijectionIsoToGroupIso : {A : Group {ℓ}} {B : Group {ℓ'}} → BijectionIso A B → GroupIso A B
BijectionIsoToGroupIso {A = A} {B = B} i = grIso
  where
  module A = GroupStr (snd A)
  module B = GroupStr (snd B)
  f = fun (map' i)

  helper : (b : _) → isProp (Σ[ a ∈ ⟨ A ⟩ ] f a ≡ b)
  helper _ a b =
    Σ≡Prop (λ _ → isSetCarrier B _ _)
           (fst a                             ≡⟨ sym (A.rid _) ⟩
            fst a A.+ A.0g                    ≡⟨ cong (fst a A.+_) (sym (A.invl _)) ⟩
            fst a A.+ ((A.- fst b) A.+ fst b) ≡⟨ A.assoc _ _ _ ⟩
            (fst a A.- fst b) A.+ fst b       ≡⟨ cong (A._+ fst b) idHelper ⟩
            A.0g A.+ fst b                    ≡⟨ A.lid _ ⟩
            fst b ∎)
    where
    idHelper : fst a A.- fst b ≡ A.0g
    idHelper =
      inj i _
           (isHom (map' i) (fst a) (A.- (fst b))
         ∙ (cong (f (fst a) B.+_) (morphMinus A B (map' i) (fst b))
         ∙∙ cong (B._+ (B.- f (fst b))) (snd a ∙ sym (snd b))
         ∙∙ B.invr (f (fst b))))

  grIso : GroupIso A B
  map grIso = map' i
  inv grIso b = (rec (helper b) (λ a → a) (surj i b)) .fst
  rightInv grIso b = (rec (helper b) (λ a → a) (surj i b)) .snd
  leftInv grIso b j = rec (helper (f b)) (λ a → a) (propTruncIsProp (surj i (f b)) ∣ b , refl ∣ j) .fst

BijectionIsoToGroupEquiv : {A : Group {ℓ}} {B : Group {ℓ₂}} → BijectionIso A B → GroupEquiv A B
BijectionIsoToGroupEquiv i = GrIsoToGrEquiv (BijectionIsoToGroupIso i)

vSES→GroupIso : ∀ {ℓ ℓ' ℓ'' ℓ'''} {A : Group {ℓ}} {B : Group {ℓ'}} (leftGr : Group {ℓ''}) (rightGr : Group {ℓ'''})
                → vSES A B leftGr rightGr
                → GroupIso A B
vSES→GroupIso {A = A} lGr rGr vses = BijectionIsoToGroupIso theIso
  where
  theIso : BijectionIso _ _
  map' theIso = vSES.ϕ vses
  inj theIso a inker = rec (isSetCarrier A _ _)
                            (λ (a , p) → sym p
                                        ∙∙ cong (fun (left vses)) (isTrivialLeft vses a _)
                                        ∙∙ morph0→0 lGr A (left vses))
                            (Ker-ϕ⊂Im-left vses a inker)
  surj theIso a = Ker-right⊂Im-ϕ vses a (isTrivialRight vses _ _)

vSES→GroupEquiv : {A : Group {ℓ}} {B : Group {ℓ₁}} (leftGr : Group {ℓ₂}) (rightGr : Group {ℓ₃})
        → vSES A B leftGr rightGr
        → GroupEquiv A B
vSES→GroupEquiv {A = A} lGr rGr vses = GrIsoToGrEquiv (vSES→GroupIso lGr rGr vses)

-- The trivial group is a unit.
lUnitGroupIso : ∀ {ℓ} {G : Group {ℓ}} → GroupIso (dirProd trivialGroup G) G
fun (map lUnitGroupIso) = snd
isHom (map lUnitGroupIso) _ _ = refl
inv lUnitGroupIso g = tt , g
rightInv lUnitGroupIso _ = refl
leftInv lUnitGroupIso _ = refl

rUnitGroupIso : ∀ {ℓ} {G : Group {ℓ}} → GroupIso (dirProd G trivialGroup) G
fun (map rUnitGroupIso) = fst
isHom (map rUnitGroupIso) _ _ = refl
inv rUnitGroupIso g = g , tt
rightInv rUnitGroupIso _ = refl
leftInv rUnitGroupIso _ = refl

lUnitGroupEquiv : ∀ {ℓ} {G : Group {ℓ}} → GroupEquiv (dirProd trivialGroup G) G
lUnitGroupEquiv = GrIsoToGrEquiv lUnitGroupIso

rUnitGroupEquiv : ∀ {ℓ} {G : Group {ℓ}} → GroupEquiv (dirProd G trivialGroup) G
rUnitGroupEquiv = GrIsoToGrEquiv rUnitGroupIso

IsoContrGroupTrivialGroup : {G : Group {ℓ}} → isContr ⟨ G ⟩ → GroupIso G trivialGroup
fun (map (IsoContrGroupTrivialGroup contr)) _ = tt
isHom (map (IsoContrGroupTrivialGroup contr)) _ _ = refl
inv (IsoContrGroupTrivialGroup contr) x = fst contr
rightInv (IsoContrGroupTrivialGroup contr) x = refl
leftInv (IsoContrGroupTrivialGroup contr) x = snd contr x

contrGroup≅trivialGroup : {G : Group {ℓ}} → isContr ⟨ G ⟩ → GroupEquiv G trivialGroup
contrGroup≅trivialGroup contr = GrIsoToGrEquiv (IsoContrGroupTrivialGroup contr)

GroupIso→Iso : {A : Group {ℓ}} {B : Group {ℓ₁}} → GroupIso A B → Iso ⟨ A ⟩ ⟨ B ⟩
fun (GroupIso→Iso i) = fun (map i)
inv (GroupIso→Iso i) = inv i
rightInv (GroupIso→Iso i) = rightInv i
leftInv (GroupIso→Iso i) = leftInv i

congIdLeft≡congIdRight : {A : Type ℓ} (_+A_ : A → A → A) (-A_ : A → A)
            (0A : A)
            (rUnitA : (x : A) → x +A 0A ≡ x)
            (lUnitA : (x : A) → 0A +A x ≡ x)
          → (r≡l : rUnitA 0A ≡ lUnitA 0A)
          → (p : 0A ≡ 0A) →
            cong (0A +A_) p ≡ cong (_+A 0A) p
congIdLeft≡congIdRight _+A_ -A_ 0A rUnitA lUnitA r≡l p =
            rUnit (cong (0A +A_) p)
         ∙∙ ((λ i → (λ j → lUnitA 0A (i ∧ j)) ∙∙ cong (λ x → lUnitA x i) p ∙∙ λ j → lUnitA 0A (i ∧ ~ j))
         ∙∙ cong₂ (λ x y → x ∙∙ p ∙∙ y) (sym r≡l) (cong sym (sym r≡l))
         ∙∙ λ i → (λ j → rUnitA 0A (~ i ∧ j)) ∙∙ cong (λ x → rUnitA x (~ i)) p ∙∙ λ j → rUnitA 0A (~ i ∧ ~ j))
         ∙∙ sym (rUnit (cong (_+A 0A) p))

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
{-# OPTIONS --copatterns --sized-types #-}
-- {-# OPTIONS -v tc.size.solve:60 #-}

open import Common.Size
open import Common.Prelude
open import Common.Product

-- Sized streams via head/tail.

record Stream {i : Size} (A : Set) : Set where
  coinductive
  constructor delay
  field
    force : ∀ {j : Size< i} → A × Stream {j} A
open Stream public

_∷ˢ_ : ∀{i A} → A → Stream {i} A → Stream {↑ i} A
force (a ∷ˢ s) = a , s

-- Prepending a list to a stream.

_++ˢ_ : ∀ {i A} → List A → Stream {i} A → Stream {i} A
(a ∷ as) ++ˢ s = a ∷ˢ (as ++ˢ s)
[]       ++ˢ s = s

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda