text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lexicographic products of binary relations
------------------------------------------------------------------------

-- The definition of lexicographic product used here is suitable if
-- the left-hand relation is a strict partial order.

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

module Data.Product.Relation.Binary.Lex.Strict where

open import Data.Product
open import Data.Product.Relation.Binary.Pointwise.NonDependent as Pointwise
  using (Pointwise)
open import Data.Sum using (inj₁; inj₂; _-⊎-_; [_,_])
open import Data.Empty
open import Function
open import Level
open import Relation.Nullary
open import Relation.Nullary.Product
open import Relation.Nullary.Sum
open import Relation.Binary
open import Relation.Binary.Consequences

module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where

------------------------------------------------------------------------
-- A lexicographic ordering over products

  ×-Lex : (_≈₁_ _<₁_ : Rel A₁ ℓ₁) → (_≤₂_ : Rel A₂ ℓ₂) → Rel (A₁ × A₂) _
  ×-Lex _≈₁_ _<₁_ _≤₂_ =
    (_<₁_ on proj₁) -⊎- (_≈₁_ on proj₁) -×- (_≤₂_ on proj₂)

------------------------------------------------------------------------
-- Some properties which are preserved by ×-Lex (under certain
-- assumptions).

  ×-reflexive : ∀ _≈₁_ _∼₁_ {_≈₂_ : Rel A₂ ℓ₂} _≤₂_ →
                _≈₂_ ⇒ _≤₂_ → (Pointwise _≈₁_ _≈₂_) ⇒ (×-Lex _≈₁_ _∼₁_ _≤₂_)
  ×-reflexive _ _ _ refl₂ = λ x≈y →
    inj₂ (proj₁ x≈y , refl₂ (proj₂ x≈y))

  ×-irreflexive : ∀ {_≈₁_ _<₁_}             → Irreflexive _≈₁_ _<₁_ →
                  ∀ {_≈₂_ _<₂_ : Rel A₂ ℓ₂} → Irreflexive _≈₂_ _<₂_ →
                  Irreflexive (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_)
  ×-irreflexive ir₁ ir₂ x≈y (inj₁ x₁<y₁) = ir₁ (proj₁ x≈y) x₁<y₁
  ×-irreflexive ir₁ ir₂ x≈y (inj₂ x≈<y)  =
    ir₂ (proj₂ x≈y) (proj₂ x≈<y)

  ×-transitive : ∀ {_≈₁_ _<₁_} →
    IsEquivalence _≈₁_ → _<₁_ Respects₂ _≈₁_ → Transitive _<₁_ →
    ∀ {_≤₂_} → Transitive _≤₂_ → Transitive (×-Lex _≈₁_ _<₁_ _≤₂_)
  ×-transitive {_≈₁_} {_<₁_} eq₁ resp₁ trans₁ {_≤₂_} trans₂ = trans
    where
    module Eq₁ = IsEquivalence eq₁

    trans : Transitive (×-Lex _≈₁_ _<₁_ _≤₂_)
    trans (inj₁ x₁<y₁) (inj₁ y₁<z₁) = inj₁ (trans₁ x₁<y₁ y₁<z₁)
    trans (inj₁ x₁<y₁) (inj₂ y≈≤z)  =
      inj₁ (proj₁ resp₁ (proj₁ y≈≤z) x₁<y₁)
    trans (inj₂ x≈≤y)  (inj₁ y₁<z₁) =
      inj₁ (proj₂ resp₁ (Eq₁.sym $ proj₁ x≈≤y) y₁<z₁)
    trans (inj₂ x≈≤y)  (inj₂ y≈≤z)  =
      inj₂ ( Eq₁.trans (proj₁ x≈≤y) (proj₁ y≈≤z)
           , trans₂    (proj₂ x≈≤y) (proj₂ y≈≤z) )

  ×-antisymmetric : ∀ {_≈₁_ _<₁_} →
    Symmetric _≈₁_ → Irreflexive _≈₁_ _<₁_ → Asymmetric _<₁_ →
    ∀ {_≈₂_ _≤₂_ : Rel A₂ ℓ₂} → Antisymmetric _≈₂_ _≤₂_ →
    Antisymmetric (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _<₁_ _≤₂_)
  ×-antisymmetric {_≈₁_} {_<₁_} sym₁ irrefl₁ asym₁
                  {_≈₂_} {_≤₂_} antisym₂ = antisym
    where
    antisym : Antisymmetric (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _<₁_ _≤₂_)
    antisym (inj₁ x₁<y₁) (inj₁ y₁<x₁) =
      ⊥-elim $ asym₁ x₁<y₁ y₁<x₁
    antisym (inj₁ x₁<y₁) (inj₂ y≈≤x)  =
      ⊥-elim $ irrefl₁ (sym₁ $ proj₁ y≈≤x) x₁<y₁
    antisym (inj₂ x≈≤y)  (inj₁ y₁<x₁) =
      ⊥-elim $ irrefl₁ (sym₁ $ proj₁ x≈≤y) y₁<x₁
    antisym (inj₂ x≈≤y)  (inj₂ y≈≤x)  =
      proj₁ x≈≤y , antisym₂ (proj₂ x≈≤y) (proj₂ y≈≤x)

  ×-asymmetric : ∀ {_≈₁_ _<₁_} →
    Symmetric _≈₁_ → _<₁_ Respects₂ _≈₁_ → Asymmetric _<₁_ →
    ∀ {_<₂_} → Asymmetric _<₂_ →
    Asymmetric (×-Lex _≈₁_ _<₁_ _<₂_)
  ×-asymmetric {_≈₁_} {_<₁_} sym₁ resp₁ asym₁ {_<₂_} asym₂ = asym
    where
    irrefl₁ : Irreflexive _≈₁_ _<₁_
    irrefl₁ = asym⟶irr resp₁ sym₁ asym₁

    asym : Asymmetric (×-Lex _≈₁_ _<₁_ _<₂_)
    asym (inj₁ x₁<y₁) (inj₁ y₁<x₁) = asym₁ x₁<y₁ y₁<x₁
    asym (inj₁ x₁<y₁) (inj₂ y≈<x)  = irrefl₁ (sym₁ $ proj₁ y≈<x) x₁<y₁
    asym (inj₂ x≈<y)  (inj₁ y₁<x₁) = irrefl₁ (sym₁ $ proj₁ x≈<y) y₁<x₁
    asym (inj₂ x≈<y)  (inj₂ y≈<x)  = asym₂ (proj₂ x≈<y) (proj₂ y≈<x)

  ×-respects₂ :
    ∀ {_≈₁_ _<₁_} → IsEquivalence _≈₁_ → _<₁_ Respects₂ _≈₁_ →
    {_≈₂_ _<₂_ : Rel A₂ ℓ₂} → _<₂_ Respects₂ _≈₂_ →
    (×-Lex _≈₁_ _<₁_ _<₂_) Respects₂ (Pointwise _≈₁_ _≈₂_)
  ×-respects₂ {_≈₁_} {_<₁_} eq₁ resp₁
              {_≈₂_} {_<₂_}     resp₂ = resp¹ , resp²
    where
    _<_ = ×-Lex _≈₁_ _<₁_ _<₂_

    open IsEquivalence eq₁ renaming (sym to sym₁; trans to trans₁)

    resp¹ : ∀ {x} → (x <_) Respects (Pointwise _≈₁_ _≈₂_)
    resp¹ y≈y' (inj₁ x₁<y₁) = inj₁ (proj₁ resp₁ (proj₁ y≈y') x₁<y₁)
    resp¹ y≈y' (inj₂ x≈<y)  =
      inj₂ ( trans₁ (proj₁ x≈<y) (proj₁ y≈y')
           , proj₁ resp₂ (proj₂ y≈y') (proj₂ x≈<y) )

    resp² : ∀ {y} → (flip _<_ y) Respects (Pointwise _≈₁_ _≈₂_)
    resp² x≈x' (inj₁ x₁<y₁) = inj₁ (proj₂ resp₁ (proj₁ x≈x') x₁<y₁)
    resp² x≈x' (inj₂ x≈<y)  =
      inj₂ ( trans₁ (sym₁ $ proj₁ x≈x') (proj₁ x≈<y)
           , proj₂ resp₂ (proj₂ x≈x') (proj₂ x≈<y) )

  ×-decidable : ∀ {_≈₁_ _<₁_} → Decidable _≈₁_ → Decidable _<₁_ →
                ∀ {_≤₂_} → Decidable _≤₂_ →
                Decidable (×-Lex _≈₁_ _<₁_ _≤₂_)
  ×-decidable dec-≈₁ dec-<₁ dec-≤₂ x y =
    dec-<₁ (proj₁ x) (proj₁ y)
      ⊎-dec
    (dec-≈₁ (proj₁ x) (proj₁ y)
       ×-dec
     dec-≤₂ (proj₂ x) (proj₂ y))

  ×-total₁ : ∀ {_≈₁_ _<₁_} → Total _<₁_ →
             ∀ {_≤₂_} → Total (×-Lex _≈₁_ _<₁_ _≤₂_)
  ×-total₁ total₁ x y with total₁ (proj₁ x) (proj₁ y)
  ... | inj₁ x₁<y₁ = inj₁ (inj₁ x₁<y₁)
  ... | inj₂ x₁>y₁ = inj₂ (inj₁ x₁>y₁)

  ×-total₂ : ∀ {_≈₁_ _<₁_} → Symmetric _≈₁_ → Trichotomous _≈₁_ _<₁_ →
             ∀ {_≤₂_} → Total _≤₂_ →
             Total (×-Lex _≈₁_ _<₁_ _≤₂_)
  ×-total₂ sym tri₁ total₂ x y with tri₁ (proj₁ x) (proj₁ y)
  ... | tri< x₁<y₁ _ _ = inj₁ (inj₁ x₁<y₁)
  ... | tri> _ _ y₁<x₁ = inj₂ (inj₁ y₁<x₁)
  ... | tri≈ _ x₁≈y₁ _ with total₂ (proj₂ x) (proj₂ y)
  ...   | inj₁ x₂≤y₂ = inj₁ (inj₂ (x₁≈y₁     , x₂≤y₂))
  ...   | inj₂ y₂≤x₂ = inj₂ (inj₂ (sym x₁≈y₁ , y₂≤x₂))

  ×-compare :
    {_≈₁_ _<₁_ : Rel A₁ ℓ₁} → Symmetric _≈₁_ → Trichotomous _≈₁_ _<₁_ →
    {_≈₂_ _<₂_ : Rel A₂ ℓ₂} → Trichotomous _≈₂_ _<₂_ →
    Trichotomous (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_)
  ×-compare sym₁ cmp₁ cmp₂ (x₁ , x₂) (y₁ , y₂) with cmp₁ x₁ y₁
  ... | (tri< x₁<y₁ x₁≉y₁ x₁≯y₁) =
    tri< (inj₁ x₁<y₁)
         (x₁≉y₁ ∘ proj₁)
         [ x₁≯y₁ , x₁≉y₁ ∘ sym₁ ∘ proj₁ ]
  ... | (tri> x₁≮y₁ x₁≉y₁ x₁>y₁) =
    tri> [ x₁≮y₁ , x₁≉y₁ ∘ proj₁ ]
         (x₁≉y₁ ∘ proj₁)
         (inj₁ x₁>y₁)
  ... | (tri≈ x₁≮y₁ x₁≈y₁ x₁≯y₁) with cmp₂ x₂ y₂
  ...   | (tri< x₂<y₂ x₂≉y₂ x₂≯y₂) =
    tri< (inj₂ (x₁≈y₁ , x₂<y₂))
         (x₂≉y₂ ∘ proj₂)
         [ x₁≯y₁ , x₂≯y₂ ∘ proj₂ ]
  ...   | (tri> x₂≮y₂ x₂≉y₂ x₂>y₂) =
    tri> [ x₁≮y₁ , x₂≮y₂ ∘ proj₂ ]
         (x₂≉y₂ ∘ proj₂)
         (inj₂ (sym₁ x₁≈y₁ , x₂>y₂))
  ...   | (tri≈ x₂≮y₂ x₂≈y₂ x₂≯y₂) =
    tri≈ [ x₁≮y₁ , x₂≮y₂ ∘ proj₂ ]
         (x₁≈y₁ , x₂≈y₂)
         [ x₁≯y₁ , x₂≯y₂ ∘ proj₂ ]

------------------------------------------------------------------------
-- Collections of properties which are preserved by ×-Lex.

  ×-isPreorder : ∀ {_≈₁_ _∼₁_} → IsPreorder _≈₁_ _∼₁_ →
                   ∀ {_≈₂_ _∼₂_} → IsPreorder _≈₂_ _∼₂_ →
                   IsPreorder (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _∼₁_ _∼₂_)
  ×-isPreorder {_≈₁_} {_∼₁_} pre₁ {_∼₂_ = _∼₂_} pre₂ =
    record
      { isEquivalence = Pointwise.×-isEquivalence
                          (isEquivalence pre₁) (isEquivalence pre₂)
      ; reflexive     = ×-reflexive _≈₁_ _∼₁_ _∼₂_ (reflexive pre₂)
      ; trans         = ×-transitive
                          (isEquivalence pre₁) (∼-resp-≈ pre₁)
                          (trans pre₁) {_≤₂_ = _∼₂_} (trans pre₂)
      }
    where open IsPreorder

  ×-isStrictPartialOrder :
    ∀ {_≈₁_ _<₁_} → IsStrictPartialOrder _≈₁_ _<₁_ →
    ∀ {_≈₂_ _<₂_} → IsStrictPartialOrder _≈₂_ _<₂_ →
    IsStrictPartialOrder (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_)
  ×-isStrictPartialOrder {_<₁_ = _<₁_} spo₁ {_<₂_ = _<₂_} spo₂ =
    record
      { isEquivalence = Pointwise.×-isEquivalence
                          (isEquivalence spo₁) (isEquivalence spo₂)
      ; irrefl        = ×-irreflexive {_<₁_ = _<₁_} (irrefl spo₁)
                                      {_<₂_ = _<₂_} (irrefl spo₂)
      ; trans         = ×-transitive
                          {_<₁_ = _<₁_} (isEquivalence spo₁)
                                        (<-resp-≈ spo₁) (trans spo₁)
                          {_≤₂_ = _<₂_} (trans spo₂)
      ; <-resp-≈      = ×-respects₂ (isEquivalence spo₁)
                                      (<-resp-≈ spo₁)
                                      (<-resp-≈ spo₂)
      }
    where open IsStrictPartialOrder

  ×-isStrictTotalOrder :
    ∀ {_≈₁_ _<₁_} → IsStrictTotalOrder _≈₁_ _<₁_ →
    ∀ {_≈₂_ _<₂_} → IsStrictTotalOrder _≈₂_ _<₂_ →
    IsStrictTotalOrder (Pointwise _≈₁_ _≈₂_) (×-Lex _≈₁_ _<₁_ _<₂_)
  ×-isStrictTotalOrder {_<₁_ = _<₁_} spo₁ {_<₂_ = _<₂_} spo₂ =
    record
      { isEquivalence = Pointwise.×-isEquivalence
                          (isEquivalence spo₁) (isEquivalence spo₂)
      ; trans         = ×-transitive
                          {_<₁_ = _<₁_} (isEquivalence spo₁)
                                        (<-resp-≈ spo₁) (trans spo₁)
                          {_≤₂_ = _<₂_} (trans spo₂)
      ; compare       = ×-compare (Eq.sym spo₁) (compare spo₁)
                                                (compare spo₂)
      }
    where open IsStrictTotalOrder

------------------------------------------------------------------------
-- "Packages" can also be combined.

module _ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} where

  ×-preorder : Preorder ℓ₁ ℓ₂ _ → Preorder ℓ₃ ℓ₄ _ → Preorder _ _ _
  ×-preorder p₁ p₂ = record
    { isPreorder = ×-isPreorder (isPreorder p₁) (isPreorder p₂)
    } where open Preorder

  ×-strictPartialOrder :
    StrictPartialOrder ℓ₁ ℓ₂ _ → StrictPartialOrder ℓ₃ ℓ₄ _ →
    StrictPartialOrder _ _ _
  ×-strictPartialOrder s₁ s₂ = record
    { isStrictPartialOrder = ×-isStrictPartialOrder
        (isStrictPartialOrder s₁) (isStrictPartialOrder s₂)
    } where open StrictPartialOrder

  ×-strictTotalOrder :
    StrictTotalOrder ℓ₁ ℓ₂ _ → StrictTotalOrder ℓ₃ ℓ₄ _ →
    StrictTotalOrder _ _ _
  ×-strictTotalOrder s₁ s₂ = record
    { isStrictTotalOrder = ×-isStrictTotalOrder
        (isStrictTotalOrder s₁) (isStrictTotalOrder s₂)
    } where open StrictTotalOrder

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

_×-irreflexive_ = ×-irreflexive
{-# WARNING_ON_USAGE _×-irreflexive_
"Warning: _×-irreflexive_ was deprecated in v0.15.
Please use ×-irreflexive instead."
#-}
_×-isPreorder_           = ×-isPreorder
{-# WARNING_ON_USAGE _×-isPreorder_
"Warning: _×-isPreorder_ was deprecated in v0.15.
Please use ×-isPreorder instead."
#-}
_×-isStrictPartialOrder_ = ×-isStrictPartialOrder
{-# WARNING_ON_USAGE _×-isStrictPartialOrder_
"Warning: _×-isStrictPartialOrder_ was deprecated in v0.15.
Please use ×-isStrictPartialOrder instead."
#-}
_×-isStrictTotalOrder_   = ×-isStrictTotalOrder
{-# WARNING_ON_USAGE _×-isStrictTotalOrder_
"Warning: _×-isStrictTotalOrder_ was deprecated in v0.15.
Please use ×-isStrictTotalOrder instead."
#-}
_×-preorder_             = ×-preorder
{-# WARNING_ON_USAGE _×-preorder_
"Warning: _×-preorder_ was deprecated in v0.15.
Please use ×-preorder instead."
#-}
_×-strictPartialOrder_   = ×-strictPartialOrder
{-# WARNING_ON_USAGE _×-strictPartialOrder_
"Warning: _×-strictPartialOrder_ was deprecated in v0.15.
Please use ×-strictPartialOrder instead."
#-}
_×-strictTotalOrder_     = ×-strictTotalOrder
{-# WARNING_ON_USAGE _×-strictTotalOrder_
"Warning: _×-strictTotalOrder_ was deprecated in v0.15.
Please use ×-strictTotalOrder instead."
#-}
×-≈-respects₂            = ×-respects₂
{-# WARNING_ON_USAGE ×-≈-respects₂
"Warning: ×-≈-respects₂ was deprecated in v0.15.
Please use ×-respects₂ instead."
#-}


text:
data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

postulate
  M   : Set → Set
  _>>=_ : ∀{A B : Set} → M A → (A → M B) → M B

infixr 1 bind
bind : _
bind = _>>=_

infix 0 id
id : ∀{A : Set} → A → A
id = λ x → x

syntax id  x             = do x
syntax bind ma (λ x → f) = x ← ma , f

swapM′ : ∀ {A B} → M (A × B) → M (B × A)
swapM′ mAB =
  do
     (a , b) ← mAB
   , return $ b , a

-- Was:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error:
-- src/full/Agda/TypeChecking/Monad/Base.hs:1793

ext: agda


text:
{-# OPTIONS --cubical --no-import-sorts --allow-unsolved-metas #-}

module Number.Instances.QuoInt where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)
open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Foundations.Logic renaming (inl to inlᵖ; inr to inrᵖ)

open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Sigma
open import Cubical.Data.Bool using (not)
open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥) -- `⊥` and `elim`
open import Cubical.Foundations.Logic renaming (¬_ to ¬ᵖ_; inl to inlᵖ; inr to inrᵖ)
open import Function.Base using (it; _∋_; _$_)

open import Cubical.HITs.PropositionalTruncation --.Properties

open import Utils using (!_; !!_)
open import MoreLogic.Reasoning
open import MoreLogic.Definitions
open import MoreLogic.Properties
open import MorePropAlgebra.Definitions hiding (_≤''_)
open import MorePropAlgebra.Structures
open import MorePropAlgebra.Bundles
open import MorePropAlgebra.Consequences
open import Number.Structures2
open import Number.Bundles2

open import Number.Instances.Nat using (lemma10''; lemma12'') renaming
  ( _<_ to _<ⁿ_
  ; <-irrefl  to <ⁿ-irrefl
  ; <-cotrans to <ⁿ-cotrans
  ; suc-creates-< to sucⁿ-creates-<ⁿ
  ; 0<suc to 0<ⁿsuc
  )
open import Data.Nat.Base using () renaming
  ( _⊔_ to maxⁿ
  ; _⊓_ to minⁿ
  ; _+_ to _+ⁿ_
  )

open import Cubical.HITs.Ints.QuoInt
open import Cubical.HITs.Ints.QuoInt.Properties
open import Cubical.Data.Nat using (suc; zero; ℕ) renaming
  ( +-comm to +ⁿ-comm )
open import Cubical.Data.Nat.Order using () renaming
  ( <-trans to <ⁿ-trans
  ; _<_ to _<ⁿᵗ_
  ; _≟_ to _≟ⁿ_
  ; lt to ltⁿ
  ; gt to gtⁿ
  ; eq to eqⁿ
  ; ¬-<-zero to ¬-<ⁿ-zero
  )

-- hProp-valued _<_
_<_ : ∀(x y : ℤ) → hProp ℓ-zero
x < y with sign x | sign y
... | spos | spos = abs x <ⁿ abs y
... | spos | sneg = ⊥
... | sneg | spos = ⊤ -- ↯ NOTE: exploiting this specific behaviour of `sign` is not much different from using just `Int`
... | sneg | sneg = abs y <ⁿ abs x

-- _<_ on a representation `λ x → (sign x , abs x)` of QuoInt
_<ʳ_ : ∀(x y : Sign × ℕ) → hProp ℓ-zero
(spos , x) <ʳ (spos , y) = x <ⁿ y
(spos , x) <ʳ (sneg , y) = ⊥
(sneg , x) <ʳ (spos , y) = ⊤
(sneg , x) <ʳ (sneg , y) = y <ⁿ x

<≡<ʳ : ∀ x y → x < y ≡ (sign x , abs x) <ʳ (sign y , abs y)
<≡<ʳ x y with sign x | sign y
... | spos | spos = refl
... | spos | sneg = refl
... | sneg | spos = refl
... | sneg | sneg = refl

-- different version of _<_
_<'_ : ℤ → ℤ → hProp ℓ-zero
pos      n₀  <' pos      n₁  = n₀ <ⁿ n₁
pos      n₀  <' neg      n₁  = ⊥
neg      0   <' pos      0   = ⊥
neg      0   <' pos (suc n₁) = ⊤
neg (suc n₀) <' pos      0   = ⊤
neg (suc n₀) <' pos (suc n₁) = ⊤
neg      n₀  <' neg      n₁  = n₁ <ⁿ n₀
pos      n₀  <' posneg   j   = lemma10'' n₀    j
neg      0   <' posneg   j   = lemma10'' 0  (~ j)
neg (suc n₀) <' posneg   j   = lemma12'' n₀ (~ j)
posneg   i   <' pos      0   = lemma10'' 0     i
posneg   i   <' pos (suc n₁) = lemma12'' n₁    i
posneg   i   <' neg      n₁  = lemma10'' n₁ (~ i)
posneg   i   <' posneg   j   = lemma10'' 0 ((i ∨ j) ∧ ~(i ∧ j))

<'≡< : ∀ x y → x <' y ≡ x < y
<'≡< (pos  zero  ) (pos  zero  ) = refl
<'≡< (pos  zero  ) (pos (suc y)) = refl
<'≡< (pos (suc x)) (pos  zero  ) = refl
<'≡< (pos (suc x)) (pos (suc y)) = refl
<'≡< (pos  zero  ) (neg  zero  ) = sym (lemma10'' _)
<'≡< (pos  zero  ) (neg (suc y)) = refl
<'≡< (pos (suc x)) (neg  zero  ) = sym (lemma10'' _)
<'≡< (pos (suc x)) (neg (suc y)) = refl
<'≡< (neg  zero  ) (pos  zero  ) = sym (lemma10'' _)
<'≡< (neg  zero  ) (pos (suc y)) = sym (lemma12'' _)
<'≡< (neg (suc x)) (pos  zero  ) = refl
<'≡< (neg (suc x)) (pos (suc y)) = refl
<'≡< (neg  zero  ) (neg  zero  ) = refl
<'≡< (neg  zero  ) (neg (suc y)) = lemma10'' _
<'≡< (neg (suc x)) (neg  zero  ) = lemma12'' _
<'≡< (neg (suc x)) (neg (suc y)) = refl
<'≡< (pos  zero  ) (posneg i) j = lemma10'' 0 (~ j ∧ i)
<'≡< (pos (suc x)) (posneg i) j = lemma10'' (suc x) (~ j ∧ i)
<'≡< (neg  zero  ) (posneg i) j = lemma10'' 0 (~ j ∧ ~ i)
<'≡< (neg (suc x)) (posneg i) j = lemma12'' x (j ∨ ~ i)
<'≡< (posneg i) (pos  zero  ) j = lemma10'' 0 (~ j ∧ i)
<'≡< (posneg i) (pos (suc y)) j = lemma12'' y (~ j ∧ i)
<'≡< (posneg i) (neg  zero  ) j = lemma10'' 0 (~ j ∧ ~ i)
<'≡< (posneg i) (neg (suc y)) j = lemma10'' (suc y) (j ∨ ~ i)
<'≡< (posneg i) (posneg   j ) k = lemma10'' 0 (((i ∨ j) ∧ ~ i ∨ ~ j) ∧ ~ k)

min : ℤ → ℤ → ℤ
min x y with sign x | sign y
... | spos | spos = pos (minⁿ (abs x) (abs y))
... | spos | sneg = y
... | sneg | spos = x
... | sneg | sneg = neg (maxⁿ (abs x) (abs y))

max : ℤ → ℤ → ℤ
max x y with sign x | sign y
... | spos | spos = pos (maxⁿ (abs x) (abs y))
... | spos | sneg = x
... | sneg | spos = y
... | sneg | sneg = neg (minⁿ (abs x) (abs y))

<-irrefl : (a : ℤ) → [ ¬ (a < a) ]
<-irrefl (pos zero)    = <ⁿ-irrefl 0
<-irrefl (pos (suc n)) = <ⁿ-irrefl (suc n)
<-irrefl (neg zero)    = <ⁿ-irrefl 0
<-irrefl (neg (suc n)) = <ⁿ-irrefl (suc n)
<-irrefl (posneg i) p  = <ⁿ-irrefl 0 p

<-trans : (a b c : ℤ) → [ a < b ] → [ b < c ] → [ a < c ]
<-trans a b c a<b b<c with sign a | sign b | sign c
  | pathTo⇒ (<≡<ʳ a b) a<b
  | pathTo⇒ (<≡<ʳ b c) b<c
  | pathTo⇐ (<≡<ʳ a c)
... | spos | spos | spos | a<b' | b<c' | p = p (<ⁿ-trans a<b' b<c')
... | spos | spos | sneg | a<b' | b<c' | p = p b<c'
... | spos | sneg | spos | a<b' | b<c' | p = p (⊥-elim a<b')
... | spos | sneg | sneg | a<b' | b<c' | p = p a<b'
... | sneg | spos | spos | a<b' | b<c' | p = p a<b'
... | sneg | spos | sneg | a<b' | b<c' | p = p (⊥-elim b<c')
... | sneg | sneg | spos | a<b' | b<c' | p = p b<c'
... | sneg | sneg | sneg | a<b' | b<c' | p = p (<ⁿ-trans b<c' a<b')

<-cotrans : (a b : ℤ) → [ a < b ] → (x : ℤ) → [ (a < x) ⊔ (x < b) ]
<-cotrans a b a<b c with sign a , abs a | sign b , abs b | sign c , abs c
  | pathTo⇒ (<≡<ʳ a b) a<b
  | pathTo⇐ (λ i → (<≡<ʳ a c) i ⊔ (<≡<ʳ c b) i)
... | spos , a' | spos , b' | spos , c' | a<b' | p = p (<ⁿ-cotrans _ _ a<b' c')
... | spos , a' | spos , b' | sneg , c' | a<b' | p = p (inrᵖ tt)
... | sneg , a' | spos , b' | spos , c' | a<b' | p = p (inlᵖ tt)
... | sneg , a' | spos , b' | sneg , c' | a<b' | p = p (inrᵖ tt)
... | sneg , a' | sneg , b' | spos , c' | a<b' | p = p (inlᵖ tt)
... | sneg , a' | sneg , b' | sneg , c' | a<b' | p = p (pathTo⇒ (⊔-comm (b' <ⁿ c') (c' <ⁿ a')) (<ⁿ-cotrans _ _ a<b' c'))

data Trichotomy (m n : ℤ) : Type₀ where
  lt : [ m < n ] → Trichotomy m n
  eq :   m ≡ n   → Trichotomy m n
  gt : [ n < m ] → Trichotomy m n

record Reveal'_·_is_ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
                   (f⁻¹ : B → A)
                   (y : B) (x : A)
                   : Type ℓ where
  eta-equality
  constructor [_]ⁱ'
  field eq' : x ≡ f⁻¹ y

inspect' : ∀{ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
          (f⁻¹ : B → A) (f : A → B) (x : A) → f⁻¹ (f x) ≡ x → Reveal' f⁻¹ · (f x) is x
inspect' f⁻¹ f x p = [ sym p ]ⁱ'

reprℤ : ℤ → Sign × ℕ
reprℤ z = sign z , abs z

reprℤ⁻¹ : Sign × ℕ → ℤ
reprℤ⁻¹ (s , n) = signed s n

reprℤ-id : ∀ z → reprℤ⁻¹ (reprℤ z) ≡ z
reprℤ-id (pos  zero  ) = refl
reprℤ-id (pos (suc n)) = refl
reprℤ-id (neg  zero  ) = posneg
reprℤ-id (neg (suc n)) = refl
reprℤ-id (posneg   i ) = λ j → posneg (i ∧ j)

inspect-reprℤ : (x : ℤ) → Reveal' reprℤ⁻¹ · (reprℤ x) is x
inspect-reprℤ a = inspect' reprℤ⁻¹ reprℤ a (reprℤ-id a)

-- abs : ℤ → ℕ
-- abs (signed _ n) = n
-- abs (posneg i) = zero

-- NOTE: this would be easier to get from `Int≡QuoInt`
_≟_ : ∀ m n → Trichotomy m n
m ≟ n with reprℤ m | reprℤ n
  | inspect-reprℤ m
  | inspect-reprℤ n
  | abs m ≟ⁿ abs n
  | pathTo⇐ (<≡<ʳ m n)
  | pathTo⇐ (<≡<ʳ n m)
... | spos , m' | spos , n' | [ m≡ ]ⁱ' | [ n≡ ]ⁱ' | ltⁿ x | p | q = lt (p (transport (λ i → [ abs (m≡ i) <ⁿ abs (n≡ i) ]) x))
... | spos , m' | spos , n' | [ m≡ ]ⁱ' | [ n≡ ]ⁱ' | eqⁿ x | p | q = let m'≡n' = (λ i → abs (m≡ (~ i))) ∙ x ∙ (λ i → abs (n≡ i))
                                                                    in eq (transport (λ i → (m≡ (~ i)) ≡ (n≡ (~ i))) (λ i → pos (m'≡n' i)))
... | spos , m' | spos , n' | [ m≡ ]ⁱ' | [ n≡ ]ⁱ' | gtⁿ x | p | q = gt (q (transport (λ i → [ abs (n≡ i) <ⁿ abs (m≡ i) ]) x))
... | spos , m' | sneg , n' | [ m≡ ]ⁱ' | [ n≡ ]ⁱ' | o     | p | q = gt (q tt)
... | sneg , m' | spos , n' | [ m≡ ]ⁱ' | [ n≡ ]ⁱ' | o     | p | q = lt (p tt)
... | sneg , m' | sneg , n' | [ m≡ ]ⁱ' | [ n≡ ]ⁱ' | ltⁿ x | p | q = gt (q (transport (λ i → [ abs (m≡ i) <ⁿ abs (n≡ i) ]) x))
... | sneg , m' | sneg , n' | [ m≡ ]ⁱ' | [ n≡ ]ⁱ' | eqⁿ x | p | q = let m'≡n' = (λ i → abs (m≡ (~ i))) ∙ x ∙ (λ i → abs (n≡ i))
                                                                    in eq (transport (λ i → (m≡ (~ i)) ≡ (n≡ (~ i))) (λ i → neg (m'≡n' i)))
... | sneg , m' | sneg , n' | [ m≡ ]ⁱ' | [ n≡ ]ⁱ' | gtⁿ x | p | q = lt (p (transport (λ i → [ abs (n≡ i) <ⁿ abs (m≡ i) ]) x))

is-min : (x y z : ℤ) → [ ¬ᵖ (min x y < z) ⇔ ¬ᵖ (x < z) ⊓ ¬ᵖ (y < z) ]
is-min = {!  !}

is-max : (x y z : ℤ) → [ ¬ᵖ (z < max x y) ⇔ ¬ᵖ (z < x) ⊓ ¬ᵖ (z < y) ]
is-max = {!  !}

sucℤ-pos-suc : ∀ n → sucℤ (pos n) ≡ pos (suc n)
sucℤ-pos-suc x = refl -- holds definitionally

+-preserves-pos : ∀ x y → pos x + pos y ≡ pos (x +ⁿ y)
+-preserves-pos zero y = refl
+-preserves-pos (suc x) zero = transport (λ i → sucℤ (+-comm (pos 0) (pos x) i) ≡ pos (suc (+ⁿ-comm 0 x i))) refl
+-preserves-pos (suc x) (suc y) = λ i → sucℤ (+-preserves-pos x (suc y) i)

-- +-reflects-< : ∀ a b x → [ (a + x) < (b + x) ] → [ a < b ]
-- +-reflects-< a b x a+x<b+x with reprℤ a | reprℤ b | reprℤ x | reprℤ (a + x) | reprℤ (b + x)
--   | inspect-reprℤ a
--   | inspect-reprℤ b
--   | inspect-reprℤ x
--   | inspect-reprℤ (a + x)
--   | inspect-reprℤ (b + x)
--   | pathTo⇒ (<≡<ʳ (a + x) (b + x)) a+x<b+x
--   | pathTo⇐ (<≡<ʳ a b)
-- ... | spos , a' | spos , b' | sx , x' | spos , a+x | spos , b+x | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | [ x≡ ]ⁱ' | [ a+x≡ ]ⁱ' | [ b+x≡ ]ⁱ' | p | q = q {!   !}
-- ... | spos , a' | spos , b' | sx , x' | sneg , a+x | spos , b+x | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | [ x≡ ]ⁱ' | [ a+x≡ ]ⁱ' | [ b+x≡ ]ⁱ' | p | q = q {!   !}
-- ... | spos , a' | spos , b' | sx , x' | sneg , a+x | sneg , b+x | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | [ x≡ ]ⁱ' | [ a+x≡ ]ⁱ' | [ b+x≡ ]ⁱ' | p | q = q {!   !}
-- ... | spos , a' | sneg , b' | sx , x' | spos , a+x | spos , b+x | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | [ x≡ ]ⁱ' | [ a+x≡ ]ⁱ' | [ b+x≡ ]ⁱ' | p | q = q {!   !}
-- ... | spos , a' | sneg , b' | sx , x' | sneg , a+x | spos , b+x | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | [ x≡ ]ⁱ' | [ a+x≡ ]ⁱ' | [ b+x≡ ]ⁱ' | p | q = q {!   !}
-- ... | spos , a' | sneg , b' | sx , x' | sneg , a+x | sneg , b+x | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | [ x≡ ]ⁱ' | [ a+x≡ ]ⁱ' | [ b+x≡ ]ⁱ' | p | q = q {!   !}
-- ... | sneg , a' | spos , b' | sx , x' | spos , a+x | spos , b+x | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | [ x≡ ]ⁱ' | [ a+x≡ ]ⁱ' | [ b+x≡ ]ⁱ' | p | q = q {!   !}
-- ... | sneg , a' | spos , b' | sx , x' | sneg , a+x | spos , b+x | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | [ x≡ ]ⁱ' | [ a+x≡ ]ⁱ' | [ b+x≡ ]ⁱ' | p | q = q {!   !}
-- ... | sneg , a' | spos , b' | sx , x' | sneg , a+x | sneg , b+x | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | [ x≡ ]ⁱ' | [ a+x≡ ]ⁱ' | [ b+x≡ ]ⁱ' | p | q = q {!   !}
-- ... | sneg , a' | sneg , b' | sx , x' | spos , a+x | spos , b+x | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | [ x≡ ]ⁱ' | [ a+x≡ ]ⁱ' | [ b+x≡ ]ⁱ' | p | q = q {!   !}
-- ... | sneg , a' | sneg , b' | sx , x' | sneg , a+x | spos , b+x | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | [ x≡ ]ⁱ' | [ a+x≡ ]ⁱ' | [ b+x≡ ]ⁱ' | p | q = q {!   !}
-- ... | sneg , a' | sneg , b' | sx , x' | sneg , a+x | sneg , b+x | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | [ x≡ ]ⁱ' | [ a+x≡ ]ⁱ' | [ b+x≡ ]ⁱ' | p | q = q {!   !}

+-identity-posˡ : ∀ a → pos zero + a ≡ a
+-identity-posˡ a = refl

+-identity-posʳ : ∀ a → a + pos zero ≡ a
+-identity-posʳ a = +-comm a (pos zero) ∙ +-identity-posˡ a

-- -_ : ℤ → ℤ
-- - signed s n = signed (not s) n
-- - posneg i   = posneg (~ i)
--
-- _+_ : ℤ → ℤ → ℤ
-- (signed _ zero) + n = n
-- (posneg _)      + n = n
-- (pos (suc m))   + n = sucℤ  (pos m + n)
-- (neg (suc m))   + n = predℤ (neg m + n)

pos≡-neg : ∀ n → pos n ≡ - neg n
pos≡-neg n = refl

-pos≡neg : ∀ n → - pos n ≡ neg n
-pos≡neg n = refl

suc-neg-suc≡neg : ∀ n → sucℤ (neg (suc n)) ≡ neg n
suc-neg-suc≡neg n = refl

pos+neg≡0 : ∀ n → pos n + neg n ≡ 0
pos+neg≡0 zero = sym posneg
pos+neg≡0 (suc n) = transport (
  pos n + neg n                ≡ pos 0 ≡⟨ (λ i → +-comm (pos n) (neg n) i ≡ pos 0) ⟩
  neg n + pos n                ≡ pos 0 ≡⟨ refl ⟩
  (sucℤ (neg (suc n)) + pos n) ≡ pos 0 ≡⟨ (λ i → sucℤ-+ˡ (neg (suc n)) (pos n) (~ i) ≡ pos 0) ⟩
  sucℤ (neg (suc n) + pos n)   ≡ pos 0 ≡⟨ (λ i → sucℤ (+-comm (pos n) (neg (suc n)) (~ i)) ≡ pos 0) ⟩
  sucℤ (pos n + neg (suc n))   ≡ pos 0 ∎) (pos+neg≡0 n)

neg+pos≡0 : ∀ n → neg n + pos n ≡ 0
neg+pos≡0 n = +-comm (neg n) (pos n) ∙ pos+neg≡0 n

+-inverseʳ : ∀ a → a + (- a) ≡ 0
+-inverseʳ a with reprℤ a | inspect-reprℤ a
... | spos , a' | [ a≡ ]ⁱ' = transport (λ i → a≡ (~ i) + (- a≡ (~ i)) ≡ pos 0) (pos+neg≡0 a')
... | sneg , a' | [ a≡ ]ⁱ' = transport (λ i → a≡ (~ i) + (- a≡ (~ i)) ≡ pos 0) (neg+pos≡0 a')

+-inverseˡ : ∀ a → (- a) + a ≡ 0
+-inverseˡ a = +-comm (- a) a ∙ +-inverseʳ a

+-inverse : (x : ℤ) → (x + (- x) ≡ pos 0) × ((- x) + x ≡ pos 0)
+-inverse x .fst = +-inverseʳ x
+-inverse x .snd = +-inverseˡ x

-- -on-reprℤ : ∀ a → (sign (- a) , abs (- a)) ≡ (not (sign a) , abs a)
-- -on-reprℤ (pos zero) = {!   !} -- Goal (spos , 0) ≡ (sneg , 0)
-- -on-reprℤ (pos (suc n)) = {!   !}
-- -on-reprℤ (neg n) = {!   !}
-- -on-reprℤ (posneg i) = {!   !}

-flips-< : ∀ a b → [ a < b ] → [ (- b) < (- a) ]
-flips-< a b a<b with reprℤ a | reprℤ b
  | inspect-reprℤ a
  | inspect-reprℤ b
  | pathTo⇒ (<≡<ʳ a b) a<b
  | pathTo⇐ (<≡<ʳ (- b) (- a))
... | spos , zero   | spos , zero   | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (sym λ i → fst ((sign (- b≡ i) , abs (- b≡ i)) <ʳ (sign (- a≡ i) , abs (- a≡ i)))) in q (r p)
... | sneg , zero   | spos , zero   | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (sym λ i → fst ((sign (- b≡ i) , abs (- b≡ i)) <ʳ (sign (- a≡ i) , abs (- a≡ i)))) in q (r (⊥-elim $ <-irrefl a $ subst (λ p → [ a < p ]) (b≡ ∙ posneg ∙ sym a≡) a<b))
... | sneg , zero   | sneg , zero   | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (sym λ i → fst ((sign (- b≡ i) , abs (- b≡ i)) <ʳ (sign (- a≡ i) , abs (- a≡ i)))) in q (r p)
... | spos , zero   | spos , suc b' | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (sym λ i → fst ((sign (- b≡ i) , abs (- b≡ i)) <ʳ (sign (- a≡ i) , abs (- a≡ i)))) in q (r tt)
... | sneg , zero   | spos , suc b' | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (sym λ i → fst ((sign (- b≡ i) , abs (- b≡ i)) <ʳ (sign (- a≡ i) , abs (- a≡ i)))) in q (r tt)
... | sneg , zero   | sneg , suc b' | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (sym λ i → fst ((sign (- b≡ i) , abs (- b≡ i)) <ʳ (sign (- a≡ i) , abs (- a≡ i)))) in q (r p)
... | spos , suc a' | spos , zero   | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (sym λ i → fst ((sign (- b≡ i) , abs (- b≡ i)) <ʳ (sign (- a≡ i) , abs (- a≡ i)))) in q (r (¬-<ⁿ-zero p))
... | sneg , suc a' | spos , zero   | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (sym λ i → fst ((sign (- b≡ i) , abs (- b≡ i)) <ʳ (sign (- a≡ i) , abs (- a≡ i)))) in q (r (0<ⁿsuc _))
... | sneg , suc a' | sneg , zero   | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (sym λ i → fst ((sign (- b≡ i) , abs (- b≡ i)) <ʳ (sign (- a≡ i) , abs (- a≡ i)))) in q (r (0<ⁿsuc _))
... | spos , suc a' | spos , suc b' | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (sym λ i → fst ((sign (- b≡ i) , abs (- b≡ i)) <ʳ (sign (- a≡ i) , abs (- a≡ i)))) in q (r p)
... | sneg , suc a' | spos , suc b' | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (sym λ i → fst ((sign (- b≡ i) , abs (- b≡ i)) <ʳ (sign (- a≡ i) , abs (- a≡ i)))) in q (r tt)
... | sneg , suc a' | sneg , suc b' | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (sym λ i → fst ((sign (- b≡ i) , abs (- b≡ i)) <ʳ (sign (- a≡ i) , abs (- a≡ i)))) in q (r p)

-- suc-reflects-< : ∀ a b → [ sucℤ a < sucℤ b ] → [ a < b ]
-- suc-reflects-< (pos zero) (pos zero) sa<sb = ⊥-elim $ <-irrefl (pos 1) sa<sb
-- suc-reflects-< (pos zero) (pos (suc n₁)) sa<sb = sucⁿ-creates-<ⁿ 0 (suc n₁) .snd sa<sb
-- suc-reflects-< (pos zero) (neg zero) sa<sb = {!   !}
-- suc-reflects-< (pos zero) (neg (suc n₁)) sa<sb = {!   !}
-- suc-reflects-< (pos (suc n₀)) (pos zero) sa<sb = {!   !}
-- suc-reflects-< (pos (suc n₀)) (pos (suc n₁)) sa<sb = {!   !}
-- suc-reflects-< (pos (suc n₀)) (neg zero) sa<sb = {!   !}
-- suc-reflects-< (pos (suc n₀)) (neg (suc n₁)) sa<sb = {!   !}
-- suc-reflects-< (neg zero) (pos zero) sa<sb = {!   !}
-- suc-reflects-< (neg zero) (pos (suc n₁)) sa<sb = {!   !}
-- suc-reflects-< (neg zero) (neg zero) sa<sb = {!   !}
-- suc-reflects-< (neg zero) (neg (suc n₁)) sa<sb = {!   !}
-- suc-reflects-< (neg (suc n₀)) (pos zero) sa<sb = {!   !}
-- suc-reflects-< (neg (suc n₀)) (pos (suc n₁)) sa<sb = {!   !}
-- suc-reflects-< (neg (suc n₀)) (neg zero) sa<sb = {!   !}
-- suc-reflects-< (neg (suc n₀)) (neg (suc n₁)) sa<sb = {!   !}
-- suc-reflects-< (signed s₀ n₀) (posneg j) sa<sb = {!   !}
-- suc-reflects-< (posneg i) (signed s₁ n₁) sa<sb = {!   !}
-- suc-reflects-< (posneg i) (posneg j) sa<sb = {!   !}

suc-reflects-< : ∀ a b → [ sucℤ a < sucℤ b ] → [ a < b ]
suc-reflects-< a b sa<sb with reprℤ a | reprℤ b
  | inspect-reprℤ a
  | inspect-reprℤ b
  | pathTo⇒ (<≡<ʳ (sucℤ a) (sucℤ b)) sa<sb
  | pathTo⇐ (<≡<ʳ a b)
... | spos , a' | spos , b' | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (λ i → [ (sign (sucℤ (a≡ i)) , abs (sucℤ (a≡ i))) <ʳ (sign (sucℤ (b≡ i)) , abs (sucℤ (b≡ i))) ]) p
                                                          in q (sucⁿ-creates-<ⁿ a' b' .snd r)
-- ... | spos , a' | sneg , b' | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (λ i → [ (sign (sucℤ (a≡ i)) , abs (sucℤ (a≡ i))) <ʳ (sign (sucℤ (b≡ i)) , abs (sucℤ (b≡ i))) ]) p
--                                                           in q {!  !}
... | spos , a' | sneg , 0 | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (λ i → [ (sign (sucℤ (a≡ i)) , abs (sucℤ (a≡ i))) <ʳ (sign (sucℤ (b≡ i)) , abs (sucℤ (b≡ i))) ]) p
                                                          in q (¬-<ⁿ-zero $ sucⁿ-creates-<ⁿ a' 0 .snd r)
... | spos , a' | sneg , suc 0 | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (λ i → [ (sign (sucℤ (a≡ i)) , abs (sucℤ (a≡ i))) <ʳ (sign (sucℤ (b≡ i)) , abs (sucℤ (b≡ i))) ]) p
                                                          in q (¬-<ⁿ-zero r)
... | spos , a' | sneg , suc (suc b') | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (λ i → [ (sign (sucℤ (a≡ i)) , abs (sucℤ (a≡ i))) <ʳ (sign (sucℤ (b≡ i)) , abs (sucℤ (b≡ i))) ]) p
                                                          in q r
... | sneg , a' | spos , b' | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = q tt
... | sneg , zero | sneg , zero | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = q (⊥-elim $ <-irrefl (sucℤ a) $ subst (λ p → [ sucℤ a < sucℤ p ]) (b≡ ∙ sym a≡) sa<sb)
... | sneg , zero | sneg , suc b' | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = q {!   !}
... | sneg , suc a' | sneg , zero | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = q (0<ⁿsuc _)
... | sneg , suc a' | sneg , suc b' | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (λ i → [ (sign (sucℤ (a≡ i)) , abs (sucℤ (a≡ i))) <ʳ (sign (sucℤ (b≡ i)) , abs (sucℤ (b≡ i))) ]) p
                                                                    in q {!   !}
-- ... | sneg , a' | sneg , b' | [ a≡ ]ⁱ' | [ b≡ ]ⁱ' | p | q = let r = transport (λ i → [ (- sucℤ (b≡ i)) < (- sucℤ (a≡ i)) ] )
                                                          -- in q {!  sa<sb  !}

-- [ (a + pos (suc n)) < (b + pos (suc n)) ] →

+-reflects-< : ∀ a b x → [ (a + x) < (b + x) ] → [ a < b ]
+-reflects-< a b (pos (suc n)) a+x<b+x = +-reflects-< a b (pos n) {!   !}
+-reflects-< a b (neg (suc n)) a+x<b+x = {!   !}
-- +-reflects-< a b (pos zero) a+x<b+x = pathTo⇒ (λ i → +-identity-posʳ a i < +-identity-posʳ b i) a+x<b+x
+-reflects-< a b (pos zero) a+x<b+x = pathTo⇒ (λ i → +-comm a (pos zero) i < +-comm b (pos zero) i) a+x<b+x
+-reflects-< a b (neg zero) a+x<b+x = pathTo⇒ (λ i → +-comm a (neg zero) i < +-comm b (neg zero) i) a+x<b+x
+-reflects-< a b (posneg i) a+x<b+x = pathTo⇒ (λ j → +-comm a (posneg i) j < +-comm b (posneg i) j) a+x<b+x

+-<-ext : (w x y z : ℤ) → [ (w + x) < (y + z) ] → [ (w < y) ⊔ (x < z) ]
+-<-ext w x y z r with w ≟ y | x ≟ z
... | lt w<y | q = inlᵖ w<y
... | eq w≡y | q = inrᵖ {! +-injˡ y x z   !}
... | gt y<w | q = {!   !}

·-preserves-< : (x y z : ℤ) → [ 0 < z ] → [ x < y ] → [ (x * z) < (y * z) ]
·-preserves-< = {!  !}

+-Semigroup : [ isSemigroup _+_ ]
+-Semigroup .IsSemigroup.is-set   = isSetℤ
+-Semigroup .IsSemigroup.is-assoc = +-assoc

·-Semigroup : [ isSemigroup _*_ ]
·-Semigroup .IsSemigroup.is-set   = isSetℤ
·-Semigroup .IsSemigroup.is-assoc = *-assoc

+-Monoid : [ isMonoid 0 _+_ ]
+-Monoid .IsMonoid.is-Semigroup = +-Semigroup
+-Monoid .IsMonoid.is-identity x = +-identityʳ x , refl

·-Monoid : [ isMonoid 1 _*_ ]
·-Monoid .IsMonoid.is-Semigroup = ·-Semigroup
·-Monoid .IsMonoid.is-identity x = *-identityʳ x , *-identityˡ x

is-Semiring : [ isSemiring 0 1 _+_ _*_ ]
is-Semiring .IsSemiring.+-Monoid = +-Monoid
is-Semiring .IsSemiring.·-Monoid = ·-Monoid
is-Semiring .IsSemiring.+-comm   = +-comm
is-Semiring .IsSemiring.is-dist x y z = sym (*-distribˡ x y z) , sym (*-distribʳ x y z)

is-CommSemiring : [ isCommSemiring 0 1 _+_ _*_ ]
is-CommSemiring .IsCommSemiring.is-Semiring = is-Semiring
is-CommSemiring .IsCommSemiring.·-comm      = *-comm

<-StrictLinearOrder : [ isStrictLinearOrder _<_ ]
<-StrictLinearOrder .IsStrictLinearOrder.is-irrefl = <-irrefl
<-StrictLinearOrder .IsStrictLinearOrder.is-trans  a b c = <-trans a b c
<-StrictLinearOrder .IsStrictLinearOrder.is-tricho a b with a ≟ b
... | lt a<b = inl (inl a<b)
... | eq a≡b = inr ∣ a≡b ∣
... | gt b<a = inl (inr b<a)

≤-isLattice : [ isLattice (λ x y → ¬ᵖ (y < x)) min max ]
≤-isLattice .IsLattice.≤-PartialOrder = linearorder⇒partialorder _ (≤'-isLinearOrder <-StrictLinearOrder)
≤-isLattice .IsLattice.is-min         = is-min
≤-isLattice .IsLattice.is-max         = is-max

is-LinearlyOrderedCommSemiring : [ isLinearlyOrderedCommSemiring 0 1 _+_ _*_ _<_ min max ]
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.is-CommSemiring     = is-CommSemiring
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.<-StrictLinearOrder = <-StrictLinearOrder
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.≤-isLattice         = ≤-isLattice
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.+-<-ext             = +-<-ext
is-LinearlyOrderedCommSemiring .IsLinearlyOrderedCommSemiring.·-preserves-<       = ·-preserves-<

is-LinearlyOrderedCommRing : [ isLinearlyOrderedCommRing 0 1 _+_ _*_ -_ _<_ min max ]
is-LinearlyOrderedCommRing .IsLinearlyOrderedCommRing.is-LinearlyOrderedCommSemiring = is-LinearlyOrderedCommSemiring
is-LinearlyOrderedCommRing .IsLinearlyOrderedCommRing.+-inverse                      = +-inverse

ℤbundle : LinearlyOrderedCommRing {ℓ-zero} {ℓ-zero}
ℤbundle .LinearlyOrderedCommRing.Carrier                    = ℤ
ℤbundle .LinearlyOrderedCommRing.0f                         = 0
ℤbundle .LinearlyOrderedCommRing.1f                         = 1
ℤbundle .LinearlyOrderedCommRing._+_                        = _+_
ℤbundle .LinearlyOrderedCommRing._·_                        = _*_
ℤbundle .LinearlyOrderedCommRing.-_                         = -_
ℤbundle .LinearlyOrderedCommRing.min                        = min
ℤbundle .LinearlyOrderedCommRing.max                        = max
ℤbundle .LinearlyOrderedCommRing._<_                        = _<_
ℤbundle .LinearlyOrderedCommRing.is-LinearlyOrderedCommRing = is-LinearlyOrderedCommRing

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
open import Oscar.Prelude
open import Oscar.Data.Maybe
open import Oscar.Class
open import Oscar.Class.Fmap
open import Oscar.Class.Pure
open import Oscar.Class.Apply
open import Oscar.Class.Bind
open import Oscar.Class.IsFunctor
open import Oscar.Class.IsPrefunctor
open import Oscar.Class.IsPrecategory
open import Oscar.Class.IsCategory
import Oscar.Property.Category.Function
import Oscar.Class.Reflexivity.Function
import Oscar.Class.Transextensionality.Proposequality

module Oscar.Property.Monad.Maybe where

instance

  𝓕mapMaybe : ∀ {𝔬₁ 𝔬₂} → 𝓕map Maybe 𝔬₁ 𝔬₂
  𝓕mapMaybe .𝓕map.fmap′ f ∅ = ∅
  𝓕mapMaybe .𝓕map.fmap′ f (↑ x) = ↑ f x

  𝓟ureMaybe : ∀ {𝔬} → 𝓟ure (Maybe {𝔬})
  𝓟ureMaybe .𝓟ure.pure = ↑_

  𝓐pplyMaybe : ∀ {𝔬₁ 𝔬₂} → 𝓐pply Maybe 𝔬₁ 𝔬₂
  𝓐pplyMaybe .𝓐pply.apply ∅ x = ∅
  𝓐pplyMaybe .𝓐pply.apply (↑ f) x = fmap′ f x

  𝓑indMaybe : ∀ {𝔬₁ 𝔬₂} → 𝓑ind Maybe 𝔬₁ 𝔬₂
  𝓑indMaybe .𝓑ind.bind ∅ _ = ∅
  𝓑indMaybe .𝓑ind.bind (↑ x) f = f x
{-
  FmapMaybe : ∀ {𝔬} → Fmap (Maybe {𝔬})
  FmapMaybe .Fmap.fmap = fmap′
  FmapMaybe .Fmap.isFunctor .IsFunctor.`IsPrefunctor .IsPrefunctor.`IsPrecategory₁ = {!!}
  FmapMaybe .Fmap.isFunctor .IsFunctor.`IsPrefunctor .IsPrefunctor.`IsPrecategory₂ = {!!}
  FmapMaybe .Fmap.isFunctor .IsFunctor.`IsPrefunctor .IsPrefunctor.`𝓢urjtranscommutativity = {!!}
  FmapMaybe .Fmap.isFunctor .IsFunctor.`IsPrefunctor .IsPrefunctor.`𝓢urjextensionality = {!!}
  FmapMaybe .Fmap.isFunctor .IsFunctor.`IsCategory₁ = !
  FmapMaybe .Fmap.isFunctor .IsFunctor.`IsCategory₂ .IsCategory.`IsPrecategory .IsPrecategory.`𝓣ransextensionality = {!!!}
  FmapMaybe .Fmap.isFunctor .IsFunctor.`IsCategory₂ .IsCategory.`IsPrecategory .IsPrecategory.`𝓣ransassociativity = {!!}
  FmapMaybe .Fmap.isFunctor .IsFunctor.`IsCategory₂ .IsCategory.`𝓣ransleftidentity = {!!}
  FmapMaybe .Fmap.isFunctor .IsFunctor.`IsCategory₂ .IsCategory.`𝓣ransrightidentity = {!!}
  FmapMaybe .Fmap.isFunctor .IsFunctor.`𝒮urjidentity = {!!}
-}


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

open import HoTT

module homotopy.FiberOfWedgeToProduct {i j} (X : Ptd i) (Y : Ptd j) where

  private
    X⊙×Y = X ⊙× Y

  private
    to-glue-template : ∀ {x y}
      {p p' : (pt X , pt Y) == (x , y)}
      (q : p == p' [ (λ w → ∨-to-× w == (x , y)) ↓ wglue ])
      → jright (snd×= p) == jleft (fst×= p') :> (pt X == x) * (pt Y == y)
    to-glue-template {p = p} {p' = p'} q =
      ! (jglue (fst×= p) (snd×= p)) ∙' ap (jleft ∘ fst×=) (↓-∨to×=cst-out q)

    module To (x : de⊙ X) (y : de⊙ Y) = WedgeElim
      {P = λ x∨y → ∨-to-× x∨y == (x , y) → (pt X == x) * (pt Y == y)}
      (λ x p → jright (snd×= p)) (λ y p → jleft (fst×= p))
      (↓-app→cst-in to-glue-template)

  to : ∀ x y → hfiber ∨-to-× (x , y) → (pt X == x) * (pt Y == y)
  to x y = uncurry (To.f x y)

  private
    -- the only needed β-rule for [to] applied to [wglue].
    abstract
      to-glue-idp-β : ap (to (pt X) (pt Y)) (pair= wglue (↓-∨to×=cst-in idp))
        == ! (jglue idp idp)
      to-glue-idp-β =
          split-ap2 (to _ _) wglue (↓-∨to×=cst-in idp)
        ∙ ap (λ p → ↓-app→cst-out p (↓-∨to×=cst-in idp)) (To.glue-β _ _)
        ∙ ↓-app→cst-β to-glue-template (↓-∨to×=cst-in idp)
        ∙ ap (λ p → ! (jglue idp idp) ∙' ap (left ∘ fst×=) p) (↓-∨to×=cst-β idp)

  private
    from-glue-template : ∀ {x y} (x-path : pt X == x) (y-path : pt Y == y)
      → (winr y , pair×= x-path idp) == (winl x , pair×= idp y-path)
          :> hfiber ∨-to-× (x , y)
    from-glue-template idp idp = ! $ pair= wglue (↓-∨to×=cst-in idp)

    module From (x : de⊙ X) (y : de⊙ Y) = JoinRec
      {C = hfiber ∨-to-× (x , y)}
      (λ x-path → winr y , pair×= x-path idp)
      (λ y-path → winl x , pair×= idp y-path)
      from-glue-template

  from : ∀ x y → (pt X == x) * (pt Y == y) → hfiber ∨-to-× (x , y)
  from = From.f

  private
    abstract
      to-from-glue-template : ∀ {x y} (x-path : pt X == x) (y-path : pt Y == y)
        → ap left (fst×=-β x-path idp) == ap right (snd×=-β idp y-path)
            [ (λ j → to x y (from x y j) == j) ↓ jglue x-path y-path ]
      to-from-glue-template idp idp = ↓-∘=idf-in' (to _ _) (from _ _) $
          ap (ap (to _ _)) (From.glue-β _ _ idp idp)
        ∙ ap-! (to _ _) (pair= wglue (↓-∨to×=cst-in idp))
        ∙ ap ! to-glue-idp-β
        ∙ !-! (jglue idp idp)

    to-from : ∀ x y j → to x y (from x y j) == j
    to-from x y = Join-elim
      {P = λ j → to x y (from x y j) == j}
      (λ x-path → ap left (fst×=-β x-path idp))
      (λ y-path → ap right (snd×=-β idp y-path))
      to-from-glue-template

  private
    abstract
      from-to-winl-template : ∀ {x x' y} (xy-path : (x' , pt Y) == (x , y))
        → (winl x , pair×= idp (snd×= xy-path)) == (winl x' , xy-path)
            :> hfiber (∨-to-× {X = X} {Y = Y}) (x , y)
      from-to-winl-template idp = idp

      from-to-winr-template : ∀ {x y y'} (xy-path : (pt X , y') == (x , y))
        → (winr y , pair×= (fst×= xy-path) idp) == (winr y' , xy-path)
            :> hfiber (∨-to-× {X = X} {Y = Y}) (x , y)
      from-to-winr-template idp = idp

      -- this version enables path induction on [q] which
      -- turns *both* [p] and [p'] into [idp]. yay!
      from-to-glue-template' : ∀ {x y}
        (p p' : (pt X , pt Y) == (x , y)) (q : p == p')
        → from-to-winl-template p == from-to-winr-template p'
          [ (λ xy → from x y (to x y xy) == xy) ↓ pair= wglue (↓-∨to×=cst-in q) ]
      from-to-glue-template' idp .idp idp =
        ↓-∘=idf-in' (from (pt X) (pt Y)) (to (pt X) (pt Y)) $
            ap (ap (from _ _)) to-glue-idp-β
          ∙ ap-! (from _ _) (jglue idp idp)
          ∙ ap ! (From.glue-β _ _ idp idp)
          ∙ !-! (pair= wglue (↓-∨to×=cst-in idp))

      from-to-glue-template : ∀ {x y}
        (p p' : (pt X , pt Y) == (x , y))
        (q : p == p' [ (λ w → ∨-to-× w == (x , y)) ↓ wglue ])
        → from-to-winl-template p == from-to-winr-template p'
          [ (λ xy → from x y (to x y xy) == xy) ↓ pair= wglue q ]
      from-to-glue-template {x} {y} p p' q =
        transport
          (λ q →
            from-to-winl-template p == from-to-winr-template p'
            [ (λ xy → from x y (to x y xy) == xy) ↓ pair= wglue q ])
          (↓-∨to×=cst-η q)
          (from-to-glue-template' p p' (↓-∨to×=cst-out q))

    from-to : ∀ x y hf → from x y (to x y hf) == hf
    from-to x y = uncurry $ Wedge-elim
      {P = λ w → ∀ p → from x y (To.f x y w p) == (w , p)}
      (λ x → from-to-winl-template)
      (λ y → from-to-winr-template)
      (↓-Π-in λ {p} {p'} → from-to-glue-template p p')

  fiber-thm : ∀ x y → hfiber ∨-to-× (x , y) ≃ (pt X == x) * (pt Y == y)
  fiber-thm x y = equiv (to x y) (from x y) (to-from x y) (from-to x y)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import Relation.Binary

module Algorithms.List.Sort.IsSort {c l₁ l₂} (DTO : DecTotalOrder c l₁ l₂) where

-- agda-stdlib
open import Level
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Data.List
import      Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
import      Data.List.Relation.Binary.Permutation.Setoid as PermutationSetoid
open import Data.List.Relation.Unary.Linked as Linked

-- agda-misc
open import Algorithms.List.Sort.Common DTO
import Algorithms.List.Sort.Insertion as I
import Algorithms.List.Sort.Insertion.Properties as Iₚ

open DecTotalOrder DTO renaming (Carrier to A)
open PermutationSetoid Eq.setoid
open SetoidEquality Eq.setoid
open I.InsertionSortOperation _≤?_ renaming (sort to Isort)

record IsSort (sort : List A → List A) : Set (c ⊔ l₁ ⊔ l₂) where
  field
    sorted : (xs : List A) → Sorted (sort xs)
    perm   : (xs : List A) → sort xs ↭ xs

  open Iₚ DTO

  sort-Isort : ∀ xs → sort xs ≋ Isort xs
  sort-Isort xs =
    Sorted-unique (↭-trans (perm xs) (↭-sym (sort-permutation xs)))
                  (sorted xs)
                  (sort-Sorted xs)

isSort-unique : ∀ {sort₁ sort₂ : List A → List A} →
                IsSort sort₁ → IsSort sort₂ → ∀ xs → sort₁ xs ≋ sort₂ xs
isSort-unique {sort₁} {sort₂} sort₁-isSort sort₂-isSort xs = begin
  sort₁ xs ≈⟨ IsSort.sort-Isort sort₁-isSort xs ⟩
  Isort xs ≈⟨ ≋-sym (IsSort.sort-Isort sort₂-isSort xs) ⟩
  sort₂ xs ∎
  where open SetoidReasoning ≋-setoid


text:
module WithInParModule (A : Set) where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data Bool : Set where
  true : Bool
  false : Bool

isZero : Nat -> Bool
isZero zero = true
isZero (suc _) = false

f : Nat -> Nat
f n with isZero n
f n | true = zero
f n | false = suc zero

g : Nat -> Nat
g zero = zero
g (suc n) with g n
g (suc n) | zero  = n
g (suc n) | suc _ = n

-- Andreas, 2014-11-06 outlawing with on module parameter.
-- The following will trigger an error:

-- data T : Set where
--   tt : T

-- module A (x : T) where
--   h : T
--   h with x  -- illegal!
--   h | y = y

-- postulate
--   C : T -> Set

-- test : C (A.h tt) -> C tt
-- test x = x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Level using (_⊔_)
open import Function using (_$_)

open import Data.Empty using (⊥)

open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary using (Rel; Reflexive; Transitive; Antisymmetric; _Respects₂_; _Respectsʳ_; _Respectsˡ_; Symmetric; Decidable; Irrelevant)
open import Relation.Binary.PropositionalEquality using (_≡_) renaming (refl to ≡-refl; cong to ≡-cong)

open import Data.Product using (_×_; _,_; proj₁; proj₂)

open import Algebra.Bundles using (CommutativeSemiring)

module AKS.Algebra.Divisibility {c ℓ} (S : CommutativeSemiring c ℓ) where

open import AKS.Nat using (ℕ; _<_; <-irrelevant)
open import AKS.Nat.WellFounded using (Acc; acc; <-well-founded)

open CommutativeSemiring S using (_+_; _*_; 0#; 1#) renaming (Carrier to C)
open CommutativeSemiring S using (_≈_; setoid; refl; sym; trans)
open import Relation.Binary.Reasoning.Setoid setoid
open CommutativeSemiring S using (+-cong; +-congˡ; +-congʳ; +-identityʳ; +-comm; +-assoc)
open CommutativeSemiring S using (*-assoc; *-identityˡ; *-identityʳ; *-congˡ; *-congʳ; zeroˡ; zeroʳ; distribʳ; distribˡ; *-comm)
open import Algebra.Core using (Op₂)
open import Algebra.Definitions _≈_ using (Commutative; Congruent₂; LeftCongruent; RightCongruent)

open import AKS.Algebra.Structures C _≈_ using (module Divisibility; module Modulus)
open Divisibility _*_ using (_∣_; _∤_; divides; IsGCD) public

infix 4 _≉_
_≉_ : Rel C ℓ
x ≉ y = x ≈ y → ⊥

∣-refl : Reflexive _∣_
∣-refl {x} = divides 1# (sym (*-identityˡ x))

∣-trans : Transitive _∣_
∣-trans {x} {y} {z} (divides q₁ y≈q₁*x) (divides q₂ z≈q₂*y) = divides (q₂ * q₁) $ begin
  z ≈⟨ z≈q₂*y ⟩
  q₂ * y ≈⟨ *-congˡ y≈q₁*x ⟩
  q₂ * (q₁ * x) ≈⟨ sym (*-assoc q₂ q₁ x) ⟩
  (q₂ * q₁) * x ∎

∣-respʳ : _∣_ Respectsʳ _≈_
∣-respʳ {y} {x₁} {x₂} x₁≈x₂ (divides q x₁≈q*y) = divides q $ begin
  x₂    ≈⟨ sym x₁≈x₂ ⟩
  x₁    ≈⟨ x₁≈q*y ⟩
  q * y ∎

∣-respˡ : _∣_ Respectsˡ _≈_
∣-respˡ {y} {x₁} {x₂} x₁≈x₂ (divides q y≈q*x₁) = divides q $ begin
  y      ≈⟨ y≈q*x₁ ⟩
  q * x₁ ≈⟨ *-congˡ x₁≈x₂ ⟩
  q * x₂ ∎

∣-resp : _∣_ Respects₂ _≈_
∣-resp = ∣-respʳ , ∣-respˡ

infix 10 1∣_ _∣0

1∣_ : ∀ n → 1# ∣ n
1∣ n = divides n (sym (*-identityʳ n))

_∣0 : ∀ n → n ∣ 0#
n ∣0 = divides 0# (sym (zeroˡ n))

0∣n⇒n≈0 : ∀ {n} → 0# ∣ n → n ≈ 0#
0∣n⇒n≈0 {n} (divides q n≈q*0) = begin
  n      ≈⟨ n≈q*0 ⟩
  q * 0# ≈⟨ zeroʳ q ⟩
  0#     ∎

∣n⇒∣m*n : ∀ i n m → i ∣ n → i ∣ m * n
∣n⇒∣m*n i n m (divides q n≈q*i) = divides (m * q) $ begin
  m * n       ≈⟨ *-congˡ n≈q*i ⟩
  m * (q * i) ≈⟨ sym (*-assoc m q i) ⟩
  m * q * i   ∎

∣n⇒∣n*m : ∀ i n m → i ∣ n → i ∣ n * m
∣n⇒∣n*m i n m i∣n = ∣-respʳ (*-comm m n) (∣n⇒∣m*n i n m i∣n)

module GCD {gcd : Op₂ C} (isGCD : IsGCD gcd) (∣-antisym : Antisymmetric _≈_ _∣_) where
  open IsGCD isGCD

  ∣1⇒≈1 : ∀ {n} → n ∣ 1# → n ≈ 1#
  ∣1⇒≈1 {n} n∣1 = ∣-antisym n∣1 (1∣ n)

  gcd[0,0]≈0 : gcd 0# 0# ≈ 0#
  gcd[0,0]≈0 = ∣-antisym (gcd 0# 0# ∣0) (gcd-greatest ∣-refl ∣-refl)

  gcd-comm : Commutative gcd
  gcd-comm a b = ∣-antisym
    (gcd-greatest (gcd[a,b]∣b a b) (gcd[a,b]∣a a b))
    (gcd-greatest (gcd[a,b]∣b b a) (gcd[a,b]∣a b a))

  gcd[0,a]≈a : ∀ a → gcd 0# a ≈ a
  gcd[0,a]≈a a = ∣-antisym (gcd[a,b]∣b 0# a) (gcd-greatest (a ∣0) ∣-refl)

  gcd[a,0]≈a : ∀ a → gcd a 0# ≈ a
  gcd[a,0]≈a a = ∣-antisym (gcd[a,b]∣a a 0#) (gcd-greatest ∣-refl (a ∣0))

  gcd[0,a]≈1⇒a≈1 : ∀ a → gcd 0# a ≈ 1# → a ≈ 1#
  gcd[0,a]≈1⇒a≈1 a gcd[0,a]≈1 = ∣1⇒≈1 (∣-respʳ gcd[0,a]≈1 (gcd-greatest (a ∣0) ∣-refl))

  gcd[a,0]≈1⇒a≈1 : ∀ a → gcd a 0# ≈ 1# → a ≈ 1#
  gcd[a,0]≈1⇒a≈1 a gcd[a,0]≈1 = ∣1⇒≈1 (∣-respʳ gcd[a,0]≈1 (gcd-greatest ∣-refl (a ∣0)))

  gcd[a,b]≈0⇒a≈0 : ∀ {a b} → gcd a b ≈ 0# → a ≈ 0#
  gcd[a,b]≈0⇒a≈0 {a} {b} gcd[a,b]≈0 = 0∣n⇒n≈0 (∣-respˡ gcd[a,b]≈0 (gcd[a,b]∣a a b))

  gcd[a,b]≈0⇒b≈0 : ∀ {a b} → gcd a b ≈ 0# → b ≈ 0#
  gcd[a,b]≈0⇒b≈0 {a} {b} gcd[a,b]≈0 = 0∣n⇒n≈0 (∣-respˡ gcd[a,b]≈0 (gcd[a,b]∣b a b))

  gcd[a,1]≈1 : ∀ a → gcd a 1# ≈ 1#
  gcd[a,1]≈1 a = ∣-antisym (gcd[a,b]∣b a 1#) (gcd-greatest (1∣ a) ∣-refl)

  gcd[1,a]≈1 : ∀ a → gcd 1# a ≈ 1#
  gcd[1,a]≈1 a = ∣-antisym (gcd[a,b]∣a 1# a) (gcd-greatest ∣-refl (1∣ a))

  -- gcd[d*a,d*b]≈d*gcd[a,b] : ∀ a b d → gcd (d * a) (d * b) ≈ d * gcd a b
  -- gcd[d*a,d*b]≈d*gcd[a,b] = ?

  a≉0⇒gcd[a,b]≉0 : ∀ a b → a ≉ 0# → gcd a b ≉ 0#
  a≉0⇒gcd[a,b]≉0 a b a≉0 gcd[a,b]≈0 = a≉0 (gcd[a,b]≈0⇒a≈0 gcd[a,b]≈0)

  b≉0⇒gcd[a,b]≉0 : ∀ a b → b ≉ 0# → gcd a b ≉ 0#
  b≉0⇒gcd[a,b]≉0 a b b≉0 gcd[a,b]≈0 = b≉0 (gcd[a,b]≈0⇒b≈0 gcd[a,b]≈0)

  gcd-cong : Congruent₂ gcd
  gcd-cong {a} {b} {c} {d} a≈b c≈d = ∣-antisym
    (gcd-greatest (∣-respʳ a≈b (gcd[a,b]∣a a c)) (∣-respʳ c≈d (gcd[a,b]∣b a c)))
    (gcd-greatest (∣-respʳ (sym a≈b) (gcd[a,b]∣a b d)) (∣-respʳ (sym c≈d) (gcd[a,b]∣b b d)))

  gcd-congˡ : LeftCongruent gcd
  gcd-congˡ c≈d = gcd-cong refl c≈d

  gcd-congʳ : RightCongruent gcd
  gcd-congʳ a≈b = gcd-cong a≈b refl

  infix 4 _⊥_
  _⊥_ : C → C → Set ℓ
  n ⊥ m = gcd n m ≈ 1#

  ⊥-sym : Symmetric _⊥_
  ⊥-sym {x} {y} gcd[x,y]≡1 = begin
    gcd y x ≈⟨ gcd-comm y x ⟩
    gcd x y ≈⟨ gcd[x,y]≡1 ⟩
    1# ∎

  ⊥-respʳ : _⊥_ Respectsʳ _≈_
  ⊥-respʳ {y} {x₁} {x₂} x₁≈x₂ gcd[y,x₁]≈1 = begin
    gcd y x₂ ≈⟨ gcd-congˡ (sym x₁≈x₂) ⟩
    gcd y x₁ ≈⟨ gcd[y,x₁]≈1 ⟩
    1# ∎

  ⊥-respˡ : _⊥_ Respectsˡ _≈_
  ⊥-respˡ {y} {x₁} {x₂} x₁≈x₂ gcd[x₁,y]≈1 = begin
    gcd x₂ y ≈⟨ gcd-congʳ (sym x₁≈x₂) ⟩
    gcd x₁ y ≈⟨ gcd[x₁,y]≈1 ⟩
    1# ∎

  ⊥-resp : _⊥_ Respects₂ _≈_
  ⊥-resp = ⊥-respʳ , ⊥-respˡ

module _
  (∣_∣ : ∀ n {n≉0 : n ≉ 0#} → ℕ)
  (_div_ : ∀ (n m : C) {m≉0 : m ≉ 0#} → C)
  (_mod_ : ∀ (n m : C) {m≉0 : m ≉ 0#} → C)
  where
  open Modulus 0# ∣_∣ _mod_

  module Euclidean
    (_≈?_ : Decidable _≈_)
    (≈-irrelevant : Irrelevant _≈_)
    (≉-irrelevant : Irrelevant _≉_)
    (division : ∀ n m {m≉0 : m ≉ 0#} → n ≈ m * (n div m) {m≉0} + (n mod m) {m≉0})
    (modulus : ∀ n m {m≉0 : m ≉ 0#} → Remainder n m {m≉0})
    (mod-cong : ∀ {x₁ x₂} {y₁ y₂} → x₁ ≈ x₂ → y₁ ≈ y₂ → ∀ {y₁≉0 y₂≉0} → (x₁ mod y₁) {y₁≉0} ≈ (x₂ mod y₂) {y₂≉0})
    (mod-distribʳ-* : ∀ c a b {b≉0} {b*c≉0} → ((a * c) mod (b * c)) {b*c≉0} ≈ (a mod b) {b≉0} * c)
    where

    gcdₕ : ∀ (n m : C) {m≉0 : m ≉ 0#} → Acc _<_ (∣ m ∣ {m≉0}) → C
    gcdₕ n m {m≉0} (acc downward) with modulus n m {m≉0}
    ... | 0≈ r≈0 = m
    ... | 0≉ r≉0 r<m = gcdₕ m (n mod m) (downward r<m)

    gcd : C → C → C
    gcd n m with m ≈? 0#
    ... | yes m≈0 = n
    ... | no  m≉0 = gcdₕ n m {m≉0} <-well-founded

    ∣b∣a%b⇒∣a : ∀ {c a b} {b≉0 : b ≉ 0#} → c ∣ b → c ∣ (a mod b) {b≉0} → c ∣ a
    ∣b∣a%b⇒∣a {c} {a} {b} {b≉0} (divides q₁ b≈q₁*c) (divides q₂ a%b≈q₂*c) = divides ((a div b) {b≉0} * q₁ + q₂) $ begin
      a                             ≈⟨ division a b {b≉0} ⟩
      b * (a div b) + a mod b       ≈⟨ +-cong (*-congʳ b≈q₁*c) a%b≈q₂*c ⟩
      (q₁ * c) * (a div b) + q₂ * c ≈⟨ +-congʳ (*-comm (q₁ * c) (a div b)) ⟩
      (a div b) * (q₁ * c) + q₂ * c ≈⟨ +-congʳ (sym (*-assoc (a div b) q₁ c)) ⟩
      ((a div b) * q₁) * c + q₂ * c ≈⟨ sym (distribʳ c ((a div b) * q₁) q₂) ⟩
      ((a div b) * q₁ + q₂) * c     ∎

    gcd[a,b]∣a×gcd[a,b]∣b : ∀ a b → (gcd a b ∣ a) × (gcd a b ∣ b)
    gcd[a,b]∣a×gcd[a,b]∣b a b with b ≈? 0#
    ... | yes b≈0 = ∣-refl , (∣-respʳ (sym b≈0) (a ∣0))
    ... | no  b≉0 = loop a b {b≉0} <-well-founded
      where
      loop : ∀ a b {b≉0} (rec : Acc _<_ (∣ b ∣ {b≉0})) → (gcdₕ a b rec ∣ a) × (gcdₕ a b rec ∣ b)
      loop a b {b≉0} (acc downward) with modulus a b {b≉0}
      ... | 0≈ r≈0 = ∣b∣a%b⇒∣a ∣-refl (∣-respʳ (sym r≈0) (b ∣0)) , ∣-refl
      ... | 0≉ r≉0 r<m with loop b (a mod b) (downward r<m)
      ...   | gcd∣b , gcd∣a%b = ∣b∣a%b⇒∣a gcd∣b gcd∣a%b , gcd∣b

    ∣a∣b⇒∣a%b : ∀ {c a b} {b≉0 : b ≉ 0#} → c ∣ a → c ∣ b → c ∣ (a mod b) {b≉0}
    ∣a∣b⇒∣a%b {c} {a} {b} {b≉0} (divides q₁ a≈q₁*c) (divides q₂ b≈q₂*c) = divides ((q₁ mod q₂) {q≉0}) $ begin
      a mod b ≈⟨ mod-cong a≈q₁*c b≈q₂*c {b≉0} {q₂*c≉0} ⟩
      (q₁ * c) mod (q₂ * c) ≈⟨ mod-distribʳ-* c q₁ q₂ ⟩
      (q₁ mod q₂) * c ∎
      where
      q≉0 : q₂ ≉ 0#
      q≉0 q₂≈0 = b≉0 $ begin
        b      ≈⟨ b≈q₂*c ⟩
        q₂ * c ≈⟨ *-congʳ q₂≈0 ⟩
        0# * c ≈⟨ zeroˡ c ⟩
        0#     ∎
      q₂*c≉0 : q₂ * c ≉ 0#
      q₂*c≉0 q₂*c≈0 = b≉0 $ begin
        b ≈⟨ b≈q₂*c ⟩
        q₂ * c ≈⟨ q₂*c≈0 ⟩
        0# ∎

    gcd-greatest : ∀ {c a b} → c ∣ a → c ∣ b → c ∣ gcd a b
    gcd-greatest {c} {a} {b} c∣a c∣b with b ≈? 0#
    ... | yes b≈0 = c∣a
    ... | no  b≉0 = loop c a b <-well-founded c∣a c∣b
      where
      loop : ∀ c a b {b≉0} (rec : Acc _<_ (∣ b ∣ {b≉0})) → c ∣ a → c ∣ b → c ∣ gcdₕ a b rec
      loop c a b {b≉0} (acc downward) c∣a c∣b with modulus a b {b≉0}
      ... | 0≈ r≈0 = c∣b
      ... | 0≉ r≉0 r<m = loop c b (a mod b) (downward r<m) c∣b (∣a∣b⇒∣a%b c∣a c∣b)

    gcd-isGCD : IsGCD gcd
    gcd-isGCD = record
      { gcd[a,b]∣a = λ a b → proj₁ (gcd[a,b]∣a×gcd[a,b]∣b a b)
      ; gcd[a,b]∣b = λ a b → proj₂ (gcd[a,b]∣a×gcd[a,b]∣b a b)
      ; gcd-greatest = gcd-greatest
      }

    -- open GCD gcd-isGCD ∣-antisym public

    data Identity (d : C) (a : C) (b : C) : Set (c ⊔ ℓ) where
      +ʳ : ∀ (x y : C) → d + x * a ≈ y * b → Identity d a b
      +ˡ : ∀ (x y : C) → d + y * b ≈ x * a → Identity d a b

    identity-sym : ∀ {d} → Symmetric (Identity d)
    identity-sym (+ʳ x y pf) = +ˡ y x pf
    identity-sym (+ˡ x y pf) = +ʳ y x pf

    identity-base : ∀ {d a} → Identity d d a
    identity-base {d} {a} = +ˡ 1# 0# $ begin
      d + 0# * a  ≈⟨ +-congˡ (zeroˡ a) ⟩
      d + 0#      ≈⟨ +-identityʳ d ⟩
      d           ≈⟨ sym (*-identityˡ d) ⟩
      1# * d      ∎

    stepʳ
      : ∀ d x y a b {b≉0}
      → d + x * b ≈ y * (a mod b) {b≉0}
      → d + (x + y * (a div b) {b≉0}) * b ≈ y * a
    stepʳ d x y a b {b≉0} d+x*b≈y*[a%b] = begin
      d + (x + y * a div b) * b       ≈⟨ +-congˡ (distribʳ b x (y * (a div b) {b≉0})) ⟩
      d + (x * b + y * a div b * b)   ≈⟨ sym (+-assoc d (x * b) (y * a div b * b)) ⟩
      (d + x * b) + y * a div b * b   ≈⟨ +-cong d+x*b≈y*[a%b] (*-assoc y (a div b) b) ⟩
      y * a mod b + y * (a div b * b) ≈⟨ sym (distribˡ y (a mod b) (a div b * b)) ⟩
      y * (a mod b + a div b * b)     ≈⟨ *-congˡ (+-comm (a mod b) (a div b * b)) ⟩
      y * (a div b * b + a mod b)     ≈⟨ *-congˡ (+-congʳ (*-comm (a div b) b)) ⟩
      y * (b * a div b + a mod b)     ≈⟨ *-congˡ (sym (division a b)) ⟩
      y * a                           ∎

    stepˡ
      : ∀ d x y a b {b≉0}
      → d + y * (a mod b) {b≉0} ≈ x * b
      → d + y * a ≈ (x + y * (a div b) {b≉0}) * b
    stepˡ d x y a b {b≉0} d+x*b≈y*[a%b] = begin
      d + y * a                               ≈⟨ +-congˡ (*-congˡ (division a b {b≉0})) ⟩
      d + y * (b * a div b + a mod b)         ≈⟨ +-congˡ (*-congˡ (+-comm (b * a div b) (a mod b))) ⟩
      d + y * (a mod b + b * a div b)         ≈⟨ +-congˡ (distribˡ y (a mod b) (b * a div b)) ⟩
      d + (y * (a mod b) + y * (b * a div b)) ≈⟨ sym (+-assoc d (y * (a mod b)) (y * (b * a div b))) ⟩
      (d + y * (a mod b)) + y * (b * a div b) ≈⟨ +-cong d+x*b≈y*[a%b] (*-congˡ (*-comm b (a div b))) ⟩
      x * b + y * (a div b * b)               ≈⟨ +-congˡ (sym (*-assoc y (a div b) b)) ⟩
      x * b + (y * a div b) * b               ≈⟨ sym (distribʳ b x (y * a div b)) ⟩
      (x + y * (a div b)) * b                 ∎

    identity-step : ∀ {d a b} {b≉0} → Identity d b ((a mod b) {b≉0}) → Identity d a b
    identity-step {d} {a} {b} {b≉0} (+ʳ x y d+x*b≈y*[a%b]) = +ˡ y (x + y * (a div b)) (stepʳ d x y a b {b≉0} d+x*b≈y*[a%b])
    identity-step {d} {a} {b} {b≉0} (+ˡ x y d+y*[a%b]≈x*b) = +ʳ y (x + y * (a div b)) (stepˡ d x y a b {b≉0} d+y*[a%b]≈x*b)

    data Bézoutₕ (a : C) (b : C) {b≉0 : b ≉ 0#} (rec : Acc _<_ (∣ b ∣ {b≉0})) : Set (c ⊔ ℓ) where
      lemmaₕ : ∀ d → gcdₕ a b rec ≈ d → Identity d a b → Bézoutₕ a b rec

    gcdₕ-base : ∀ {a b} {b≉0} {rec : Acc _<_ (∣ b ∣ {b≉0})} (r≈0 : (a mod b) {b≉0} ≈ 0#) → gcdₕ a b rec ≈ b
    gcdₕ-base {a} {b} {b≉0} {acc downward} [r≈0]₁ with modulus a b {b≉0}
    ... | 0≈ [r≈0]₂ rewrite ≈-irrelevant [r≈0]₁ [r≈0]₂ = refl
    ... | 0≉ r≉0 _  = contradiction [r≈0]₁ r≉0

    gcdₕ-step
      : ∀ {d a b} {b≉0} {r≉0 : (a mod b) {b≉0} ≉ 0#}
          {r<m : ∣ a mod b ∣ {r≉0} < ∣ b ∣ {b≉0}}
          {downward : ∀ {x} → x < ∣ b ∣ {b≉0} → Acc _<_ x}
      → gcdₕ b (a mod b) (downward {∣ a mod b ∣} r<m) ≈ d → gcdₕ a b (acc downward) ≈ d
    gcdₕ-step {d} {a} {b} {b≉0} {[r≉0]₁} {[r<m]₁} gcdₕ[b,a%b]≈d with modulus a b {b≉0}
    ... | 0≈ r≈0 = contradiction r≈0 [r≉0]₁
    ... | 0≉ [r≉0]₂ [r<m]₂ rewrite ≉-irrelevant [r≉0]₁ [r≉0]₂ | <-irrelevant [r<m]₁ [r<m]₂ = gcdₕ[b,a%b]≈d

    bézoutₕ : ∀ a b {b≉0} (rec : Acc _<_ (∣ b ∣ {b≉0})) → Bézoutₕ a b rec
    bézoutₕ a b {b≉0} (acc downward) with modulus a b {b≉0}
    ... | 0≈ r≈0 = lemmaₕ b (gcdₕ-base r≈0) (identity-sym identity-base)
    ... | 0≉ r≉0 r<m with bézoutₕ b (a mod b) {r≉0} (downward r<m)
    ...   | lemmaₕ d gcdₕ[b,a%b]≈d ident = lemmaₕ d (gcdₕ-step gcdₕ[b,a%b]≈d) (identity-step ident)

    data Bézout (a : C) (b : C) : Set (c ⊔ ℓ) where
      lemma : ∀ d → gcd a b ≈ d → Identity d a b → Bézout a b

    b≈0⇒gcd[a,b]≈a : ∀ a b → b ≈ 0# → gcd a b ≈ a
    b≈0⇒gcd[a,b]≈a a b b≈0 with b ≈? 0#
    ... | yes _  = refl
    ... | no b≉0 = contradiction b≈0 b≉0

    gcdₕ⇒gcd : ∀ {d a b} {b≉0} → gcdₕ a b {b≉0} <-well-founded ≈ d → gcd a b ≈ d
    gcdₕ⇒gcd {d} {a} {b} {[b≉0]₁} gcdₕ[a,b]≈d with b ≈? 0#
    ... | yes b≈0 = contradiction b≈0 [b≉0]₁
    ... | no [b≉0]₂ rewrite ≉-irrelevant [b≉0]₁ [b≉0]₂ = gcdₕ[a,b]≈d

    bézout : ∀ a b → Bézout a b
    bézout a b with b ≈? 0#
    ... | yes b≈0 = lemma a (b≈0⇒gcd[a,b]≈a a b b≈0) identity-base
    ... | no  b≉0 with bézoutₕ a b {b≉0} <-well-founded
    ...   | lemmaₕ d gcdₕ[a,b]≈d ident = lemma d (gcdₕ⇒gcd gcdₕ[a,b]≈d) ident

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


text:
------------------------------------------------------------------------
-- A semantics which uses continuation-passing style
------------------------------------------------------------------------

module TotalParserCombinators.Semantics.Continuation where

open import Algebra
open import Codata.Musical.Notation
open import Data.List
import Data.List.Properties as ListProp
open import Data.List.Relation.Binary.BagAndSetEquality
  using (bag) renaming (_∼[_]_ to _List-∼[_]_)
open import Data.Maybe using (Maybe)
open import Data.Product as Prod
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_)

private
  module LM {Tok : Set} = Monoid (ListProp.++-monoid Tok)

open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics as S
  hiding ([_-_]_⊛_; [_-_]_>>=_)

-- The statement x ⊕ s₂ ∈ p · s means that there is some s₁ such that
-- s ≡ s₁ ++ s₂ and x ∈ p · s₁. This variant of the semantics is
-- perhaps harder to understand, but sometimes easier to work with
-- (and it is proved to be language equivalent to the semantics in
-- TotalParserCombinators.Semantics).

infix  60 <$>_
infixl 50 [_-_]_⊛_
infixl 10 [_-_]_>>=_
infix   4 _⊕_∈_·_

data _⊕_∈_·_ {Tok} : ∀ {R xs} → R → List Tok →
                     Parser Tok R xs → List Tok → Set₁ where
  return     : ∀ {R} {x : R} {s} → x ⊕ s ∈ return x · s
  token      : ∀ {x s} → x ⊕ s ∈ token · x ∷ s
  ∣-left     : ∀ {R x xs₁ xs₂ s s₁}
                 {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂}
               (x∈p₁ : x ⊕ s₁ ∈ p₁ · s) → x ⊕ s₁ ∈ p₁ ∣ p₂ · s
  ∣-right    : ∀ {R x xs₂ s s₁} xs₁
                 {p₁ : Parser Tok R xs₁} {p₂ : Parser Tok R xs₂}
               (x∈p₂ : x ⊕ s₁ ∈ p₂ · s) → x ⊕ s₁ ∈ p₁ ∣ p₂ · s
  <$>_       : ∀ {R₁ R₂ x s s₁ xs} {p : Parser Tok R₁ xs} {f : R₁ → R₂}
               (x∈p : x ⊕ s₁ ∈ p · s) → f x ⊕ s₁ ∈ f <$> p · s
  [_-_]_⊛_   : ∀ {R₁ R₂ f x s s₁ s₂} xs fs
                 {p₁ : ∞⟨ xs ⟩Parser Tok (R₁ → R₂) (flatten fs)}
                 {p₂ : ∞⟨ fs ⟩Parser Tok  R₁       (flatten xs)} →
               (f∈p₁ : f ⊕ s₁ ∈ ♭? p₁ · s)
               (x∈p₂ : x ⊕ s₂ ∈ ♭? p₂ · s₁) →
               f x ⊕ s₂ ∈ p₁ ⊛ p₂ · s
  [_-_]_>>=_ : ∀ {R₁ R₂ x y s s₁ s₂} (f : Maybe (R₁ → List R₂)) xs
                 {p₁ : ∞⟨ f ⟩Parser Tok R₁ (flatten xs)}
                 {p₂ : (x : R₁) → ∞⟨ xs ⟩Parser Tok R₂ (apply f x)} →
               (x∈p₁ : x ⊕ s₁ ∈ ♭? p₁ · s)
               (y∈p₂x : y ⊕ s₂ ∈ ♭? (p₂ x) · s₁) →
               y ⊕ s₂ ∈ p₁ >>= p₂ · s
  nonempty   : ∀ {R xs x y s₂} s₁ {p : Parser Tok R xs}
               (x∈p : y ⊕ s₂ ∈ p · x ∷ s₁ ++ s₂) →
               y ⊕ s₂ ∈ nonempty p · x ∷ s₁ ++ s₂
  cast       : ∀ {R xs₁ xs₂ x s₁ s₂} {xs₁≈xs₂ : xs₁ List-∼[ bag ] xs₂}
                 {p : Parser Tok R xs₁}
               (x∈p : x ⊕ s₂ ∈ p · s₁) → x ⊕ s₂ ∈ cast xs₁≈xs₂ p · s₁

-- A simple cast lemma.

private

  cast∈′ : ∀ {Tok R xs} {p : Parser Tok R xs} {x s s′ s₁} →
           s ≡ s′ → x ⊕ s₁ ∈ p · s → x ⊕ s₁ ∈ p · s′
  cast∈′ P.refl x∈ = x∈

-- The definition is sound and complete with respect to the one in
-- TotalParserCombinators.Semantics.

sound′ : ∀ {Tok R xs x s₂ s} {p : Parser Tok R xs} →
         x ⊕ s₂ ∈ p · s → ∃ λ s₁ → s ≡ s₁ ++ s₂ × x ∈ p · s₁
sound′ return                      = ([]    , P.refl , return)
sound′ {x = x} token               = ([ x ] , P.refl , token)
sound′ (∣-left x∈p₁)               = Prod.map id (Prod.map id ∣-left)       (sound′ x∈p₁)
sound′ (∣-right e₁ x∈p₁)           = Prod.map id (Prod.map id (∣-right e₁)) (sound′ x∈p₁)
sound′ (<$> x∈p)                   = Prod.map id (Prod.map id (<$>_))       (sound′ x∈p)
sound′ ([ xs - fs ] f∈p₁ ⊛ x∈p₂)   with sound′ f∈p₁ | sound′ x∈p₂
sound′ ([ xs - fs ] f∈p₁ ⊛ x∈p₂)   | (s₁ , P.refl , f∈p₁′) | (s₂ , P.refl , x∈p₂′) =
                                     (s₁ ++ s₂ , P.sym (LM.assoc s₁ s₂ _) ,
                                      S.[_-_]_⊛_ xs fs f∈p₁′ x∈p₂′)
sound′ (nonempty s₁ x∈p)           with sound′ x∈p
sound′ (nonempty s₁ x∈p)           | (y ∷ s , eq , x∈p′) = (y ∷ s , eq , nonempty x∈p′)
sound′ (nonempty s₁ x∈p)           | ([]    , eq , x∈p′)
                                     with ListProp.++-identityˡ-unique (_ ∷ s₁) (P.sym eq)
sound′ (nonempty s₁ x∈p)           | ([]    , eq , x∈p′) | ()
sound′ (cast x∈p)                  = Prod.map id (Prod.map id cast) (sound′ x∈p)
sound′ ([ f - xs ] x∈p₁ >>= y∈p₂x) with sound′ x∈p₁ | sound′ y∈p₂x
sound′ ([ f - xs ] x∈p₁ >>= y∈p₂x) | (s₁ , P.refl , x∈p₁′) | (s₂ , P.refl , y∈p₂x′) =
  (s₁ ++ s₂ , P.sym (LM.assoc s₁ s₂ _) , S.[_-_]_>>=_ f xs x∈p₁′ y∈p₂x′)

sound : ∀ {Tok R xs x s} {p : Parser Tok R xs} →
        x ⊕ [] ∈ p · s → x ∈ p · s
sound x∈p with sound′ x∈p
sound x∈p | (s , P.refl , x∈p′) with s ++ [] | Prod.proj₂ LM.identity s
sound x∈p | (s , P.refl , x∈p′) | .s | P.refl = x∈p′

extend : ∀ {Tok R xs x s s′ s″} {p : Parser Tok R xs} →
         x ⊕ s′ ∈ p · s → x ⊕ s′ ++ s″ ∈ p · s ++ s″
extend return                       = return
extend token                        = token
extend (∣-left x∈p₁)                = ∣-left     (extend x∈p₁)
extend (∣-right e₁ x∈p₂)            = ∣-right e₁ (extend x∈p₂)
extend (<$> x∈p)                    = <$> extend x∈p
extend ([ xs - fs ] f∈p₁ ⊛   x∈p₂)  = [ xs - fs ] extend f∈p₁ ⊛   extend x∈p₂
extend ([ f  - xs ] x∈p₁ >>= y∈p₂x) = [ f  - xs ] extend x∈p₁ >>= extend y∈p₂x
extend (cast x∈p)                   = cast (extend x∈p)
extend (nonempty s₁ x∈p)            = cast₂ (nonempty s₁ (cast₁ (extend x∈p)))
  where
  lem   = LM.assoc (_ ∷ s₁) _ _
  cast₁ = cast∈′        lem
  cast₂ = cast∈′ (P.sym lem)

complete : ∀ {Tok R xs x s} {p : Parser Tok R xs} →
           x ∈ p · s → x ⊕ [] ∈ p · s
complete return                                 = return
complete token                                  = token
complete (∣-left x∈p₁)                          = ∣-left     (complete x∈p₁)
complete (∣-right e₁ x∈p₂)                      = ∣-right e₁ (complete x∈p₂)
complete (<$> x∈p)                              = <$> complete x∈p
complete (_⊛_   {fs = fs} {xs = xs} f∈p₁ x∈p₂)  = [ xs - fs ] extend (complete f∈p₁) ⊛   complete x∈p₂
complete (_>>=_ {xs = xs} {f  = f}  x∈p₁ y∈p₂x) = [ f  - xs ] extend (complete x∈p₁) >>= complete y∈p₂x
complete (cast x∈p)                             = cast (complete x∈p)
complete (nonempty {s = s} x∈p)                 = cast₂ (nonempty s (cast₁ (complete x∈p)))
  where
  lem   = Prod.proj₂ LM.identity _
  cast₁ = cast∈′ (P.sym lem)
  cast₂ = cast∈′        lem

complete′ : ∀ {Tok R xs x s₂ s} {p : Parser Tok R xs} →
            (∃ λ s₁ → s ≡ s₁ ++ s₂ × x ∈ p · s₁) →
            x ⊕ s₂ ∈ p · s
complete′ (s₁ , P.refl , x∈p) = extend (complete x∈p)

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
open import FRP.JS.Behaviour using ( Beh ; [_] )
open import FRP.JS.DOM using ( DOM ; element ; attr ; text ; _++_ )
open import FRP.JS.RSet using ( ⟦_⟧ )

module FRP.JS.Demo.HRef where

main : ∀ {w} → ⟦ Beh (DOM w) ⟧
main = element ("a")
  ( attr "href" ["http://bell-labs.com/"] ++
    text ["A hyperlink."] )

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
open import Prelude

module Implicits.Resolution.Scala.Terminates where

open import Implicits.Syntax
open import Implicits.Substitutions
open import Implicits.Resolution.Infinite.Algorithm
open import Implicits.Resolution.Scala.Type
open import Category.Monad.Partiality

open import Category.Monad.Partiality as P
open Workaround
open import Category.Monad.Partiality.All using (All; module Alternative)
open Alternative renaming (sound to AllP-sound) hiding (complete)

private
  open import Relation.Binary.PropositionalEquality as PEq using (_≡_)
  open module PartialEq = P.Equality  {A = Bool} _≡_
  open module PartialReasoning  = P.Reasoning (PEq.isEquivalence {A = Bool})

match-terminates : ∀ {ν} (Δ : ICtx ν) → (τ : SimpleType ν) → (r : Type ν) → (match Δ τ r) ⇓
match-terminates Δ τ r = ?

match1st-terminates : ∀ {ν} (Δ : ICtx ν) → (ρs : ICtx ν) → (τ : SimpleType ν) → (match1st Δ ρs τ) ⇓
match1st-terminates Δ List.[] τ = false , (now refl)
match1st-terminates Δ (x List.∷ ρs) τ = {!!}

terminates : ∀ {ν} (Δ : ICtx ν) (a : Type ν) → ScalaICtx Δ → ScalaType a → (resolve Δ a) ⇓
terminates Δ (simpl x) p q = match1st-terminates Δ Δ x
terminates Δ (∀' a) p (∀' q) = terminates (ictx-weaken Δ) a (weaken-scalaictx p) q
terminates Δ (a ⇒ b) p ()


text:
-- {-# OPTIONS -v term:10 -v tc.pos:10 -v tc.decl:10 #-}

-- Andreas, 2018-02-26, issue #2975
-- Problem history:
--
-- The example below crashed with an internal error.
-- The problem is that the termination checker needs to know
-- whether force is the projection of a recursive coinductive
-- record.  However, the positivity checker has not run,
-- thus, this information is not available.

record R : Set where
  coinductive
  field force : R

  -- The following corecursive definition should pass the termination checker.
  r : R
  force r = r

-- Should succeed.

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.2-Category where

open import Level
open import Data.Product using (curry; _,_)
open import Function using () renaming (_∘_ to _·_)

open import Categories.Support.PropositionalEquality

open import Categories.Category
open import Categories.Categories
open import Categories.Object.Terminal
open import Categories.Terminal
open import Categories.Functor using (Functor) renaming (_∘_ to _∘F_; _≡_ to _≡F_; id to idF)
open import Categories.Bifunctor using (Bifunctor; reduce-×)
open import Categories.Product using (assocʳ; πˡ; πʳ)

record 2-Category (o ℓ t e : Level) : Set (suc (o ⊔ ℓ ⊔ t ⊔ e)) where
  open Terminal (One {ℓ} {t} {e})

  infix  4 _⇒_
  infixr 9 _∘_

  field
    Obj : Set o
    _⇒_ : (A B : Obj) → Category ℓ t e
    id : {A : Obj} → Functor ⊤ (A ⇒ A)
    —∘— : {A B C : Obj} → Bifunctor (B ⇒ C) (A ⇒ B) (A ⇒ C)
  _∘_ : {A B C : Obj} {L R : Category ℓ t e} → Functor L (B ⇒ C) → Functor R (A ⇒ B) → Bifunctor L R (A ⇒ C)
  _∘_ {A} {B} {C} F G = reduce-× {D₁ = B ⇒ C} {D₂ = A ⇒ B} —∘— F G
  field
    .assoc : ∀ {A B C D : Obj} → ((—∘— ∘ idF) ∘F assocʳ (C ⇒ D) (B ⇒ C) (A ⇒ B)) ≡F (idF ∘ —∘—)
    .identityˡ : {A B : Obj} → (id {B} ∘ idF {C = A ⇒ B}) ≡F πʳ {C = ⊤} {A ⇒ B}
    .identityʳ : {A B : Obj} → (idF {C = A ⇒ B} ∘ id {A}) ≡F πˡ {C = A ⇒ B} {⊤}

  -- convenience?
  module _⇒_ (A B : Obj) = Category (A ⇒ B)
  open _⇒_ public using () renaming (Obj to _⇒₁_)

  private module imp⇒ {X Y : Obj} = Category (X ⇒ Y)
  open imp⇒ public using () renaming (_⇒_ to _⇒₂_; id to id₂; _∘_ to _•_; assoc to vassoc′; identityˡ to videntityˡ′; identityʳ to videntityʳ′; ∘-resp-≡ to •-resp-≡′; ∘-resp-≡ˡ to •-resp-≡′ˡ; ∘-resp-≡ʳ to •-resp-≡′ʳ; hom-setoid to hom₂′-setoid; _≡_ to _≡′_; equiv to equiv′; module Equiv to Equiv′)

  module Equiv {X Y : Obj} = Heterogeneous (X ⇒ Y)
  open Equiv public using () renaming (_∼_ to _≡_; ≡⇒∼ to loosely)

  id₁ : ∀ {A} → A ⇒₁ A
  id₁ {A} = Functor.F₀ (id {A}) unit

  id₁₂ : ∀ {A} → id₁ {A} ⇒₂ id₁ {A}
  id₁₂ {A} = id₂ {A = id₁ {A}}

  infixr 9 _∘₁_
  _∘₁_ : ∀ {A B C} → B ⇒₁ C → A ⇒₁ B → A ⇒₁ C
  _∘₁_ = curry (Functor.F₀ —∘—)

  -- horizontal composition
  infixr 9 _∘₂_
  _∘₂_ : ∀ {A B C} {g g′ : B ⇒₁ C} {f f′ : A ⇒₁ B} (β : g ⇒₂ g′) (α : f ⇒₂ f′) → (g ∘₁ f) ⇒₂ (g′ ∘₁ f′)
  _∘₂_ = curry (Functor.F₁ —∘—)

  .∘₂-resp-≡′ : ∀ {A B C} {f h : B ⇒₁ C} {g i : A ⇒₁ B} {α γ : f ⇒₂ h} {β δ : g ⇒₂ i} → α ≡′ γ → β ≡′ δ → α ∘₂ β ≡′ γ ∘₂ δ
  ∘₂-resp-≡′ = curry (Functor.F-resp-≡ —∘—)

  .∘₂-resp-≡ : ∀ {A B C} {f f′ h h′ : B ⇒₁ C} {g g′ i i′ : A ⇒₁ B} {α : f ⇒₂ h} {γ : f′ ⇒₂ h′} {β : g ⇒₂ i} {δ : g′ ⇒₂ i′} → α ≡ γ → β ≡ δ → (α ∘₂ β) ≡ (γ ∘₂ δ)
  ∘₂-resp-≡ (loosely a) (loosely b) = loosely (∘₂-resp-≡′ a b)

  -- left whiskering
  infixl 9 _◃_
  _◃_ : ∀ {A B C} {g g′ : B ⇒₁ C} → g ⇒₂ g′ → (f : A ⇒₁ B) → (g ∘₁ f) ⇒₂ (g′ ∘₁ f)
  β ◃ f = β ∘₂ id₂

  -- right whiskering
  infixr 9 _▹_
  _▹_ : ∀ {A B C} (g : B ⇒₁ C) → {f f′ : A ⇒₁ B} → f ⇒₂ f′ → (g ∘₁ f) ⇒₂ (g ∘₁ f′)
  g ▹ α = id₂ ∘₂ α

  private
    ≡F-on-objects : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} (F G : Functor C D) → (F ≡F G) → (X : Category.Obj C) → Functor.F₀ F X ≣ Functor.F₀ G X
    ≡F-on-objects {C = C} F G eq X with Functor.F₀ F X | Functor.F₁ F (Category.id C {X}) | eq (Category.id C {X})
    ≡F-on-objects {C = C} F G eq X | ._ | _ | Heterogeneous.≡⇒∼ _ = ≣-refl

  private
    module Laws1A {A B} {f : A ⇒₁ B} where
      .assoc₁ : ∀ {C D} {g : B ⇒₁ C} {h : C ⇒₁ D} → ((h ∘₁ g) ∘₁ f) ≣ (h ∘₁ (g ∘₁ f))
      assoc₁ {C} {D} {g} {h} = ≡F-on-objects ((—∘— ∘ idF) ∘F assocʳ (C ⇒ D) (B ⇒ C) (A ⇒ B)) (idF ∘ —∘—) assoc (h , g , f)

      .identity₁ˡ : {- ∀ {A B} {f : A ⇒₁ B} → -} id₁ ∘₁ f ≣ f
      identity₁ˡ = ≡F-on-objects (id {B} ∘ idF {C = A ⇒ B}) (πʳ {C = ⊤} {A ⇒ B}) identityˡ (unit , f)

  .identity₁ʳ : ∀ {A B} {f : A ⇒₁ B} → f ∘₁ id₁ ≣ f
  identity₁ʳ {A} {B} {f} = ≡F-on-objects (idF {C = A ⇒ B} ∘ id {A}) (πˡ {C = A ⇒ B} {⊤}) identityʳ (f , unit)

  .vassoc : ∀ {A B} {f g h i : A ⇒₁ B} {η : f ⇒₂ g} {θ : g ⇒₂ h} {ι : h ⇒₂ i} → ((ι • θ) • η) ≡ (ι • (θ • η))
  vassoc = loosely vassoc′

  .hidentityˡ : ∀ {A B} {f f′ : A ⇒₁ B} {η : f ⇒₂ f′} → (id₁₂ ∘₂ η) ≡ η
  hidentityˡ {A} {B} {f} {f′} {η} = Equiv.trans (loosely (∘₂-resp-≡′ (Equiv′.sym (Functor.identity id)) Equiv′.refl)) (identityˡ (unit , η))

  .hidentityʳ : ∀ {A B} {f f′ : A ⇒₁ B} {η : f ⇒₂ f′} → (η ∘₂ id₁₂) ≡ η
  hidentityʳ {A} {B} {f} {f′} {η} = Equiv.trans (loosely (∘₂-resp-≡′ Equiv′.refl (Equiv′.sym (Functor.identity id)))) (identityʳ (η , unit))

  .im-id₂-closed-under-∘₂′ : ∀ {A B C} {f : A ⇒₁ B} {g : B ⇒₁ C} → id₂ {A = g} ∘₂ id₂ {A = f} ≡′ id₂ {A = g ∘₁ f}
  im-id₂-closed-under-∘₂′ = Functor.identity —∘—

  .im-id₂-closed-under-∘₂ : ∀ {A B C} {f : A ⇒₁ B} {g : B ⇒₁ C} → (id₂ {A = g} ∘₂ id₂ {A = f}) ≡ id₂ {A = g ∘₁ f}
  im-id₂-closed-under-∘₂ = loosely im-id₂-closed-under-∘₂′

  .lidentityˡ′ : ∀ {A B C} {f : A ⇒₁ B} {g : B ⇒₁ C} → id₂ {A = g} ◃ f ≡′ id₂
  lidentityˡ′ = Functor.identity —∘—

  .lidentityˡ : ∀ {A B C} {f : A ⇒₁ B} {g : B ⇒₁ C} → (id₂ {A = g} ◃ f) ≡ id₂ {A = g ∘₁ f}
  lidentityˡ = loosely lidentityˡ′

  .ridentityʳ′ : ∀ {A B C} {f : A ⇒₁ B} {g : B ⇒₁ C} → g ▹ id₂ {A = f} ≡′ id₂
  ridentityʳ′ = Functor.identity —∘—

  .ridentityʳ : ∀ {A B C} {f : A ⇒₁ B} {g : B ⇒₁ C} → (g ▹ id₂ {A = f}) ≡ id₂ {A = g ∘₁ f}
  ridentityʳ = loosely ridentityʳ′

  -- .lidentityʳ′ : ∀ {A B} {f f′ : A ⇒₁ B} {η : f ⇒₂ f′} → (η ◃ id₁) ≡′ η
  -- lidentityʳ′ = ?

  .lidentityʳ : ∀ {A B} {f f′ : A ⇒₁ B} {η : f ⇒₂ f′} → (η ◃ id₁) ≡ η
  lidentityʳ {η = η} = Equiv.trans (∘₂-resp-≡ Equiv.refl (Equiv.sym (loosely (Functor.identity id)))) (identityʳ (η , unit))

  -- .ridentityˡ′ : ∀ {A B} {f f′ : A ⇒₁ B} {η : f ⇒₂ f′} → (id₁ ▹ η) ≡′ η
  -- ridentityˡ′ = ?

  .ridentityˡ : ∀ {A B} {f f′ : A ⇒₁ B} {η : f ⇒₂ f′} → (id₁ ▹ η) ≡ η
  ridentityˡ {η = η} = Equiv.trans (∘₂-resp-≡ (Equiv.sym (loosely (Functor.identity id))) Equiv.refl) (identityˡ (unit , η))

  .interchange′ : ∀ {A B C} {f g h : A ⇒₁ B} {i j k : B ⇒₁ C} {α : f ⇒₂ g} {β : g ⇒₂ h} {γ : i ⇒₂ j} {δ : j ⇒₂ k} → ((δ • γ) ∘₂ (β • α)) ≡′ ((δ ∘₂ β) • (γ ∘₂ α))
  interchange′ = Functor.homomorphism —∘—

  .interchange : ∀ {A B C} {f g h : A ⇒₁ B} {i j k : B ⇒₁ C} {α : f ⇒₂ g} {β : g ⇒₂ h} {γ : i ⇒₂ j} {δ : j ⇒₂ k} → ((δ • γ) ∘₂ (β • α)) ≡ ((δ ∘₂ β) • (γ ∘₂ α))
  interchange = loosely interchange′

  .lvdistrib′ : ∀ {A B C} {f : A ⇒₁ B} {g h i : B ⇒₁ C} {η : g ⇒₂ h} {θ : h ⇒₂ i} → (θ • η) ◃ f ≡′ ((θ ◃ f) • (η ◃ f))
  lvdistrib′ = Equiv′.trans (∘₂-resp-≡′ Equiv′.refl (Equiv′.sym videntityˡ′)) interchange′

  .lvdistrib : ∀ {A B C} {f : A ⇒₁ B} {g h i : B ⇒₁ C} {η : g ⇒₂ h} {θ : h ⇒₂ i} → ((θ • η) ◃ f) ≡ ((θ ◃ f) • (η ◃ f))
  lvdistrib = loosely lvdistrib′

  .rvdistrib′ : ∀ {A B C} {f g h : A ⇒₁ B} {i : B ⇒₁ C} {η : f ⇒₂ g} {θ : g ⇒₂ h} → (i ▹ (θ • η)) ≡′ ((i ▹ θ) • (i ▹ η))
  rvdistrib′ = Equiv′.trans (∘₂-resp-≡′ (Equiv′.sym videntityˡ′) Equiv′.refl) interchange′

  .rvdistrib : ∀ {A B C} {f g h : A ⇒₁ B} {i : B ⇒₁ C} {η : f ⇒₂ g} {θ : g ⇒₂ h} → (i ▹ (θ • η)) ≡ ((i ▹ θ) • (i ▹ η))
  rvdistrib = loosely rvdistrib′

  -- XXX mixed assocs still need proving
  {-
  -- XXX not well-typed without a subst or something
  -- .lhassoc′ : ∀ {A B C D} {f : A ⇒₁ B} {g : B ⇒₁ C} {h i : C ⇒₁ D} {η : h ⇒₂ i} → (η ◃ (g ∘₁ f)) ≡′ {!((η ◃ g) ◃ f)!}
  -- lhassoc′ = {!!}

  .lhassoc : ∀ {A B C D} {f : A ⇒₁ B} {g : B ⇒₁ C} {h i : C ⇒₁ D} {η : h ⇒₂ i} → (η ◃ (g ∘₁ f)) ≡ ((η ◃ g) ◃ f)
  lhassoc = {!!}

  -- XXX ditto
  -- .rlassoc′ : ∀ {A B C D} {f : A ⇒₁ B} {g h : B ⇒₁ C} {i : C ⇒₁ D} {η : g ⇒₂ h} → (i ▹ (η ◃ f)) ≡′ {!((i ▹ η) ◃ f)!}
  -- rlassoc′ = {!!}

  .rlassoc : ∀ {A B C D} {f : A ⇒₁ B} {g h : B ⇒₁ C} {i : C ⇒₁ D} {η : g ⇒₂ h} → (i ▹ (η ◃ f)) ≡ ((i ▹ η) ◃ f)
  rlassoc = {!!}

  -- XXX tritto
  -- .hrassoc′ : ∀ {A B C D} {f g : A ⇒₁ B} {h : B ⇒₁ C} {i : C ⇒₁ D} {η : f ⇒₂ g} → (i ▹ (h ▹ η)) ≡′ {!((i ∘₁ h) ▹ η)!}
  -- hrassoc′ = {!!}

  .hrassoc : ∀ {A B C D} {f g : A ⇒₁ B} {h : B ⇒₁ C} {i : C ⇒₁ D} {η : f ⇒₂ g} → (i ▹ (h ▹ η)) ≡ ((i ∘₁ h) ▹ η)
  hrassoc = {!!}
  -}

  .lrsmoosh′ : ∀ {A B C} {f g : A ⇒₁ B} {h i : B ⇒₁ C} {η : f ⇒₂ g} {θ : h ⇒₂ i} → ((θ ◃ g) • (h ▹ η)) ≡′ (θ ∘₂ η)
  lrsmoosh′ = Equiv′.trans (Equiv′.sym interchange′) (∘₂-resp-≡′ videntityʳ′ videntityˡ′)

  .lrsmoosh : ∀ {A B C} {f g : A ⇒₁ B} {h i : B ⇒₁ C} {η : f ⇒₂ g} {θ : h ⇒₂ i} → ((θ ◃ g) • (h ▹ η)) ≡ (θ ∘₂ η)
  lrsmoosh = loosely lrsmoosh′

  .rlsmoosh′ : ∀ {A B C} {f g : A ⇒₁ B} {h i : B ⇒₁ C} {η : f ⇒₂ g} {θ : h ⇒₂ i} → ((i ▹ η) • (θ ◃ f)) ≡′ (θ ∘₂ η)
  rlsmoosh′ = Equiv′.trans (Equiv′.sym interchange′) (∘₂-resp-≡′ videntityˡ′ videntityʳ′)

  .rlsmoosh : ∀ {A B C} {f g : A ⇒₁ B} {h i : B ⇒₁ C} {η : f ⇒₂ g} {θ : h ⇒₂ i} → ((i ▹ η) • (θ ◃ f)) ≡ (θ ∘₂ η)
  rlsmoosh = loosely rlsmoosh′

  .lrexch′ : ∀ {A B C} {f g : A ⇒₁ B} {h i : B ⇒₁ C} {η : f ⇒₂ g} {θ : h ⇒₂ i} → ((i ▹ η) • (θ ◃ f)) ≡′ ((θ ◃ g) • (h ▹ η))
  lrexch′ = Equiv′.trans rlsmoosh′ (Equiv′.sym lrsmoosh′)

  .lrexch : ∀ {A B C} {f g : A ⇒₁ B} {h i : B ⇒₁ C} {η : f ⇒₂ g} {θ : h ⇒₂ i} → ((i ▹ η) • (θ ◃ f)) ≡ ((θ ◃ g) • (h ▹ η))
  lrexch = loosely lrexch′

  module Hom₁Reasoning = ≣-reasoning

  module Hom₂′Reasoning {A B : Obj} {f g : A ⇒₁ B} where
    open imp⇒.HomReasoning {A} {B} {f} {g} public renaming (_⟩∘⟨_ to _⟩•⟨_)

    -- XXX won't work if Hom₂′Reasoning is frozen
    infixr 4 _⟩∘₂⟨_
    ._⟩∘₂⟨_ : ∀ {C} {h i : C ⇒₁ A} {α β : f ⇒₂ g} {γ δ : h ⇒₂ i} → α ≡′ β → γ ≡′ δ → (α ∘₂ γ) ≡′ (β ∘₂ δ)
    _⟩∘₂⟨_ = ∘₂-resp-≡′

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

-- Tested with the development version of the Agda standard library on
-- 27 May 2011.

-- Nils' idea about databases in the Agda mailing list.
-- http://thread.gmane.org/gmane.comp.lang.agda/2911/focus=2917

module FOT.Agsy.DataBase where

open import Data.Nat
open import Data.Product

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

postulate
  right-identity : ∀ n → n + 0 ≡ n
  move-suc       : ∀ m n → suc (m + n) ≡ m + suc n

db = right-identity ,′ move-suc

comm : ∀ m n → m + n ≡ n + m  -- Via auto {!-c db!}
comm zero n     = sym (proj₁ db n)
comm (suc n) n' =
  begin
    suc (n + n') ≡⟨ cong suc (comm n n') ⟩
    suc (n' + n) ≡⟨ proj₂ db n' n ⟩ (n' + suc n)
  ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- A categorical view of List⁺
------------------------------------------------------------------------

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

module Data.List.NonEmpty.Categorical where

open import Agda.Builtin.List
import Data.List.Categorical as List
open import Data.List.NonEmpty
open import Data.Product using (uncurry)
open import Category.Functor
open import Category.Applicative
open import Category.Monad
open import Category.Comonad
open import Function

------------------------------------------------------------------------
-- List⁺ applicative functor

functor : ∀ {f} → RawFunctor {f} List⁺
functor = record
  { _<$>_ = map
  }

applicative : ∀ {f} → RawApplicative {f} List⁺
applicative = record
  { pure = [_]
  ; _⊛_  = λ fs as → concatMap (λ f → map f as) fs
  }

------------------------------------------------------------------------
-- List⁺ monad

monad : ∀ {f} → RawMonad {f} List⁺
monad = record
  { return = [_]
  ; _>>=_  = flip concatMap
  }

------------------------------------------------------------------------
-- List⁺ comonad

comonad : ∀ {f} → RawComonad {f} List⁺
comonad = record
  { extract = head
  ; extend  = λ f → uncurry (extend f) ∘′ uncons
  } where

  extend : ∀ {A B} → (List⁺ A → B) → A → List A → List⁺ B
  extend f x xs@[]       = f (x ∷ xs) ∷ []
  extend f x xs@(y ∷ ys) = f (x ∷ xs) ∷⁺ extend f y ys

------------------------------------------------------------------------
-- Get access to other monadic functions

module _ {f F} (App : RawApplicative {f} F) where

  open RawApplicative App

  sequenceA : ∀ {A} → List⁺ (F A) → F (List⁺ A)
  sequenceA (x ∷ xs) = _∷_ <$> x ⊛ List.sequenceA App xs

  mapA : ∀ {a} {A : Set a} {B} → (A → F B) → List⁺ A → F (List⁺ B)
  mapA f = sequenceA ∘ map f

  forA : ∀ {a} {A : Set a} {B} → List⁺ A → (A → F B) → F (List⁺ B)
  forA = flip mapA

module _ {m M} (Mon : RawMonad {m} M) where

  private App = RawMonad.rawIApplicative Mon

  sequenceM = sequenceA App
  mapM = mapA App
  forM = forA App

------------------------------------------------------------------------
-- List⁺ monad transformer

monadT : ∀ {f} → RawMonadT {f} (_∘′ List⁺)
monadT M = record
  { return = pure ∘′ [_]
  ; _>>=_  = λ mas f → mas >>= λ as → concat <$> mapM M f as
  } where open RawMonad M