text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Sums of binary relations
------------------------------------------------------------------------

module Relation.Binary.Sum where

open import Data.Sum as Sum
open import Data.Product
open import Data.Unit using (⊤)
open import Data.Empty
open import Function
open import Function.Equality as F using (_⟶_; _⟨$⟩_)
open import Function.Equivalence as Eq
  using (Equivalence; _⇔_; module Equivalence)
open import Function.Injection as Inj
  using (Injection; _↣_; module Injection)
open import Function.Inverse as Inv
  using (Inverse; _↔_; module Inverse)
open import Function.LeftInverse as LeftInv
  using (LeftInverse; _↞_; module LeftInverse)
open import Function.Related
open import Function.Surjection as Surj
  using (Surjection; _↠_; module Surjection)
open import Level
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

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

  ----------------------------------------------------------------------
  -- Sums of relations

  infixr 1 _⊎-Rel_ _⊎-<_

  -- Generalised sum.

  data ⊎ʳ {ℓ₁ ℓ₂} (P : Set) (_∼₁_ : Rel A₁ ℓ₁) (_∼₂_ : Rel A₂ ℓ₂) :
          A₁ ⊎ A₂ → A₁ ⊎ A₂ → Set (a₁ ⊔ a₂ ⊔ ℓ₁ ⊔ ℓ₂) where
    ₁∼₂ : ∀ {x y} (p : P)         → ⊎ʳ P _∼₁_ _∼₂_ (inj₁ x) (inj₂ y)
    ₁∼₁ : ∀ {x y} (x∼₁y : x ∼₁ y) → ⊎ʳ P _∼₁_ _∼₂_ (inj₁ x) (inj₁ y)
    ₂∼₂ : ∀ {x y} (x∼₂y : x ∼₂ y) → ⊎ʳ P _∼₁_ _∼₂_ (inj₂ x) (inj₂ y)

  -- Pointwise sum.

  _⊎-Rel_ : ∀ {ℓ₁ ℓ₂} → Rel A₁ ℓ₁ → Rel A₂ ℓ₂ → Rel (A₁ ⊎ A₂) _
  _⊎-Rel_ = ⊎ʳ ⊥

  -- All things to the left are "smaller than" all things to the
  -- right.

  _⊎-<_ : ∀ {ℓ₁ ℓ₂} → Rel A₁ ℓ₁ → Rel A₂ ℓ₂ → Rel (A₁ ⊎ A₂) _
  _⊎-<_ = ⊎ʳ ⊤

  ----------------------------------------------------------------------
  -- Helpers

  private

    ₁≁₂ : ∀ {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
          ∀ {x y} → ¬ (inj₁ x ⟨ ∼₁ ⊎-Rel ∼₂ ⟩ inj₂ y)
    ₁≁₂ (₁∼₂ ())

    drop-inj₁ : ∀ {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
                ∀ {P x y} → inj₁ x ⟨ ⊎ʳ P ∼₁ ∼₂ ⟩ inj₁ y → ∼₁ x y
    drop-inj₁ (₁∼₁ x∼y) = x∼y

    drop-inj₂ : ∀ {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
                ∀ {P x y} → inj₂ x ⟨ ⊎ʳ P ∼₁ ∼₂ ⟩ inj₂ y → ∼₂ x y
    drop-inj₂ (₂∼₂ x∼y) = x∼y

  ----------------------------------------------------------------------
  -- Some properties which are preserved by the relation formers above

  _⊎-reflexive_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {∼₁ : Rel A₁ ℓ₁′}
                    {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {∼₂ : Rel A₂ ℓ₂′} →
                  ≈₁ ⇒ ∼₁ → ≈₂ ⇒ ∼₂ →
                  ∀ {P} → (≈₁ ⊎-Rel ≈₂) ⇒ (⊎ʳ P ∼₁ ∼₂)
  refl₁ ⊎-reflexive refl₂ = refl
    where
    refl : (_ ⊎-Rel _) ⇒ (⊎ʳ _ _ _)
    refl (₁∼₁ x₁≈y₁) = ₁∼₁ (refl₁ x₁≈y₁)
    refl (₂∼₂ x₂≈y₂) = ₂∼₂ (refl₂ x₂≈y₂)
    refl (₁∼₂ ())

  _⊎-refl_ : ∀ {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
             Reflexive ∼₁ → Reflexive ∼₂ → Reflexive (∼₁ ⊎-Rel ∼₂)
  refl₁ ⊎-refl refl₂ = refl
    where
    refl : Reflexive (_ ⊎-Rel _)
    refl {x = inj₁ _} = ₁∼₁ refl₁
    refl {x = inj₂ _} = ₂∼₂ refl₂

  _⊎-irreflexive_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {<₁ : Rel A₁ ℓ₁′}
                      {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {<₂ : Rel A₂ ℓ₂′} →
                    Irreflexive ≈₁ <₁ → Irreflexive ≈₂ <₂ →
                    ∀ {P} → Irreflexive (≈₁ ⊎-Rel ≈₂) (⊎ʳ P <₁ <₂)
  irrefl₁ ⊎-irreflexive irrefl₂ = irrefl
    where
    irrefl : Irreflexive (_ ⊎-Rel _) (⊎ʳ _ _ _)
    irrefl (₁∼₁ x₁≈y₁) (₁∼₁ x₁<y₁) = irrefl₁ x₁≈y₁ x₁<y₁
    irrefl (₂∼₂ x₂≈y₂) (₂∼₂ x₂<y₂) = irrefl₂ x₂≈y₂ x₂<y₂
    irrefl (₁∼₂ ())    _

  _⊎-symmetric_ : ∀ {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
                  Symmetric ∼₁ → Symmetric ∼₂ → Symmetric (∼₁ ⊎-Rel ∼₂)
  sym₁ ⊎-symmetric sym₂ = sym
    where
    sym : Symmetric (_ ⊎-Rel _)
    sym (₁∼₁ x₁∼y₁) = ₁∼₁ (sym₁ x₁∼y₁)
    sym (₂∼₂ x₂∼y₂) = ₂∼₂ (sym₂ x₂∼y₂)
    sym (₁∼₂ ())

  _⊎-transitive_ : ∀ {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
                   Transitive ∼₁ → Transitive ∼₂ →
                   ∀ {P} → Transitive (⊎ʳ P ∼₁ ∼₂)
  trans₁ ⊎-transitive trans₂ = trans
    where
    trans : Transitive (⊎ʳ _ _ _)
    trans (₁∼₁ x∼y) (₁∼₁ y∼z) = ₁∼₁ (trans₁ x∼y y∼z)
    trans (₂∼₂ x∼y) (₂∼₂ y∼z) = ₂∼₂ (trans₂ x∼y y∼z)
    trans (₁∼₂ p)   (₂∼₂ _)     = ₁∼₂ p
    trans (₁∼₁ _)   (₁∼₂ p)     = ₁∼₂ p

  _⊎-antisymmetric_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {≤₁ : Rel A₁ ℓ₁′}
                        {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {≤₂ : Rel A₂ ℓ₂′} →
                      Antisymmetric ≈₁ ≤₁ → Antisymmetric ≈₂ ≤₂ →
                      ∀ {P} → Antisymmetric (≈₁ ⊎-Rel ≈₂) (⊎ʳ P ≤₁ ≤₂)
  antisym₁ ⊎-antisymmetric antisym₂ = antisym
    where
    antisym : Antisymmetric (_ ⊎-Rel _) (⊎ʳ _ _ _)
    antisym (₁∼₁ x≤y) (₁∼₁ y≤x) = ₁∼₁ (antisym₁ x≤y y≤x)
    antisym (₂∼₂ x≤y) (₂∼₂ y≤x) = ₂∼₂ (antisym₂ x≤y y≤x)
    antisym (₁∼₂ _)   ()

  _⊎-asymmetric_ : ∀ {ℓ₁ ℓ₂} {<₁ : Rel A₁ ℓ₁} {<₂ : Rel A₂ ℓ₂} →
                   Asymmetric <₁ → Asymmetric <₂ →
                   ∀ {P} → Asymmetric (⊎ʳ P <₁ <₂)
  asym₁ ⊎-asymmetric asym₂ = asym
    where
    asym : Asymmetric (⊎ʳ _ _ _)
    asym (₁∼₁ x<y) (₁∼₁ y<x) = asym₁ x<y y<x
    asym (₂∼₂ x<y) (₂∼₂ y<x) = asym₂ x<y y<x
    asym (₁∼₂ _)   ()

  _⊎-≈-respects₂_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {∼₁ : Rel A₁ ℓ₁′}
                      {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {∼₂ : Rel A₂ ℓ₂′} →
                    ∼₁ Respects₂ ≈₁ → ∼₂ Respects₂ ≈₂ →
                    ∀ {P} → (⊎ʳ P ∼₁ ∼₂) Respects₂ (≈₁ ⊎-Rel ≈₂)
  _⊎-≈-respects₂_ {≈₁ = ≈₁} {∼₁ = ∼₁}{≈₂ = ≈₂} {∼₂ = ∼₂}
                  resp₁ resp₂ {P} =
    (λ {_ _ _} → resp¹) ,
    (λ {_ _ _} → resp²)
    where
    resp¹ : ∀ {x} → ((⊎ʳ P ∼₁ ∼₂) x) Respects (≈₁ ⊎-Rel ≈₂)
    resp¹ (₁∼₁ y≈y') (₁∼₁ x∼y) = ₁∼₁ (proj₁ resp₁ y≈y' x∼y)
    resp¹ (₂∼₂ y≈y') (₂∼₂ x∼y) = ₂∼₂ (proj₁ resp₂ y≈y' x∼y)
    resp¹ (₂∼₂ y≈y') (₁∼₂ p)   = (₁∼₂ p)
    resp¹ (₁∼₂ ())   _

    resp² :  ∀ {y}
          → (flip (⊎ʳ P ∼₁ ∼₂) y) Respects (≈₁ ⊎-Rel ≈₂)
    resp² (₁∼₁ x≈x') (₁∼₁ x∼y) = ₁∼₁ (proj₂ resp₁ x≈x' x∼y)
    resp² (₂∼₂ x≈x') (₂∼₂ x∼y) = ₂∼₂ (proj₂ resp₂ x≈x' x∼y)
    resp² (₁∼₁ x≈x') (₁∼₂ p)   = (₁∼₂ p)
    resp² (₁∼₂ ())   _

  _⊎-substitutive_ : ∀ {ℓ₁ ℓ₂ ℓ₃} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
                     Substitutive ∼₁ ℓ₃ → Substitutive ∼₂ ℓ₃ →
                     Substitutive (∼₁ ⊎-Rel ∼₂) ℓ₃
  subst₁ ⊎-substitutive subst₂ = subst
    where
    subst : Substitutive (_ ⊎-Rel _) _
    subst P (₁∼₁ x∼y) Px = subst₁ (λ z → P (inj₁ z)) x∼y Px
    subst P (₂∼₂ x∼y) Px = subst₂ (λ z → P (inj₂ z)) x∼y Px
    subst P (₁∼₂ ())  Px

  ⊎-decidable : ∀ {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂} →
                Decidable ∼₁ → Decidable ∼₂ →
                ∀ {P} → (∀ {x y} → Dec (inj₁ x ⟨ ⊎ʳ P ∼₁ ∼₂ ⟩ inj₂ y)) →
                Decidable (⊎ʳ P ∼₁ ∼₂)
  ⊎-decidable {∼₁ = ∼₁} {∼₂ = ∼₂} dec₁ dec₂ {P} dec₁₂ = dec
    where
    dec : Decidable (⊎ʳ P ∼₁ ∼₂)
    dec (inj₁ x) (inj₁ y) with dec₁ x y
    ...                   | yes x∼y = yes (₁∼₁ x∼y)
    ...                   | no  x≁y = no (x≁y ∘ drop-inj₁)
    dec (inj₂ x) (inj₂ y) with dec₂ x y
    ...                   | yes x∼y = yes (₂∼₂ x∼y)
    ...                   | no  x≁y = no (x≁y ∘ drop-inj₂)
    dec (inj₁ x) (inj₂ y) = dec₁₂
    dec (inj₂ x) (inj₁ y) = no (λ())

  _⊎-<-total_ : ∀ {ℓ₁ ℓ₂} {≤₁ : Rel A₁ ℓ₁} {≤₂ : Rel A₂ ℓ₂} →
                Total ≤₁ → Total ≤₂ → Total (≤₁ ⊎-< ≤₂)
  total₁ ⊎-<-total total₂ = total
    where
    total : Total (_ ⊎-< _)
    total (inj₁ x) (inj₁ y) = Sum.map ₁∼₁ ₁∼₁ $ total₁ x y
    total (inj₂ x) (inj₂ y) = Sum.map ₂∼₂ ₂∼₂ $ total₂ x y
    total (inj₁ x) (inj₂ y) = inj₁ (₁∼₂ _)
    total (inj₂ x) (inj₁ y) = inj₂ (₁∼₂ _)

  _⊎-<-trichotomous_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {<₁ : Rel A₁ ℓ₁′}
                         {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {<₂ : Rel A₂ ℓ₂′} →
                       Trichotomous ≈₁ <₁ → Trichotomous ≈₂ <₂ →
                       Trichotomous (≈₁ ⊎-Rel ≈₂) (<₁ ⊎-< <₂)
  _⊎-<-trichotomous_ {≈₁ = ≈₁} {<₁ = <₁} {≈₂ = ≈₂} {<₂ = <₂}
                     tri₁ tri₂ = tri
    where
    tri : Trichotomous (≈₁ ⊎-Rel ≈₂) (<₁ ⊎-< <₂)
    tri (inj₁ x) (inj₂ y) = tri< (₁∼₂ _) ₁≁₂ (λ())
    tri (inj₂ x) (inj₁ y) = tri> (λ()) (λ()) (₁∼₂ _)
    tri (inj₁ x) (inj₁ y) with tri₁ x y
    ...                   | tri< x<y x≉y x≯y =
      tri< (₁∼₁ x<y)        (x≉y ∘ drop-inj₁) (x≯y ∘ drop-inj₁)
    ...                   | tri≈ x≮y x≈y x≯y =
      tri≈ (x≮y ∘ drop-inj₁) (₁∼₁ x≈y)    (x≯y ∘ drop-inj₁)
    ...                   | tri> x≮y x≉y x>y =
      tri> (x≮y ∘ drop-inj₁) (x≉y ∘ drop-inj₁) (₁∼₁ x>y)
    tri (inj₂ x) (inj₂ y) with tri₂ x y
    ...                   | tri< x<y x≉y x≯y =
      tri< (₂∼₂ x<y)        (x≉y ∘ drop-inj₂) (x≯y ∘ drop-inj₂)
    ...                   | tri≈ x≮y x≈y x≯y =
      tri≈ (x≮y ∘ drop-inj₂) (₂∼₂ x≈y)    (x≯y ∘ drop-inj₂)
    ...                   | tri> x≮y x≉y x>y =
      tri> (x≮y ∘ drop-inj₂) (x≉y ∘ drop-inj₂) (₂∼₂ x>y)

  ----------------------------------------------------------------------
  -- Some collections of properties which are preserved

  _⊎-isEquivalence_ : ∀ {ℓ₁ ℓ₂} {≈₁ : Rel A₁ ℓ₁} {≈₂ : Rel A₂ ℓ₂} →
                      IsEquivalence ≈₁ → IsEquivalence ≈₂ →
                      IsEquivalence (≈₁ ⊎-Rel ≈₂)
  eq₁ ⊎-isEquivalence eq₂ = record
    { refl  = refl  eq₁ ⊎-refl        refl  eq₂
    ; sym   = sym   eq₁ ⊎-symmetric   sym   eq₂
    ; trans = trans eq₁ ⊎-transitive  trans eq₂
    }
    where open IsEquivalence

  _⊎-isPreorder_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {∼₁ : Rel A₁ ℓ₁′}
                     {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {∼₂ : Rel A₂ ℓ₂′} →
                   IsPreorder ≈₁ ∼₁ → IsPreorder ≈₂ ∼₂ →
                   ∀ {P} → IsPreorder (≈₁ ⊎-Rel ≈₂) (⊎ʳ P ∼₁ ∼₂)
  pre₁ ⊎-isPreorder pre₂ = record
    { isEquivalence = isEquivalence pre₁ ⊎-isEquivalence
                      isEquivalence pre₂
    ; reflexive     = reflexive pre₁ ⊎-reflexive   reflexive pre₂
    ; trans         = trans     pre₁ ⊎-transitive  trans     pre₂
    }
    where open IsPreorder

  _⊎-isDecEquivalence_ : ∀ {ℓ₁ ℓ₂} {≈₁ : Rel A₁ ℓ₁} {≈₂ : Rel A₂ ℓ₂} →
                         IsDecEquivalence ≈₁ → IsDecEquivalence ≈₂ →
                         IsDecEquivalence (≈₁ ⊎-Rel ≈₂)
  eq₁ ⊎-isDecEquivalence eq₂ = record
    { isEquivalence = isEquivalence eq₁ ⊎-isEquivalence
                      isEquivalence eq₂
    ; _≟_           = ⊎-decidable (_≟_ eq₁) (_≟_ eq₂) (no ₁≁₂)
    }
    where open IsDecEquivalence

  _⊎-isPartialOrder_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {≤₁ : Rel A₁ ℓ₁′}
                         {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {≤₂ : Rel A₂ ℓ₂′} →
                       IsPartialOrder ≈₁ ≤₁ → IsPartialOrder ≈₂ ≤₂ →
                       ∀ {P} → IsPartialOrder (≈₁ ⊎-Rel ≈₂) (⊎ʳ P ≤₁ ≤₂)
  po₁ ⊎-isPartialOrder po₂ = record
    { isPreorder = isPreorder po₁ ⊎-isPreorder    isPreorder po₂
    ; antisym    = antisym    po₁ ⊎-antisymmetric antisym    po₂
    }
    where open IsPartialOrder

  _⊎-isStrictPartialOrder_ :
    ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {<₁ : Rel A₁ ℓ₁′}
      {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {<₂ : Rel A₂ ℓ₂′} →
    IsStrictPartialOrder ≈₁ <₁ → IsStrictPartialOrder ≈₂ <₂ →
    ∀ {P} → IsStrictPartialOrder (≈₁ ⊎-Rel ≈₂) (⊎ʳ P <₁ <₂)
  spo₁ ⊎-isStrictPartialOrder spo₂ = record
    { isEquivalence = isEquivalence spo₁ ⊎-isEquivalence
                      isEquivalence spo₂
    ; irrefl        = irrefl   spo₁ ⊎-irreflexive irrefl   spo₂
    ; trans         = trans    spo₁ ⊎-transitive  trans    spo₂
    ; <-resp-≈      = <-resp-≈ spo₁ ⊎-≈-respects₂ <-resp-≈ spo₂
    }
    where open IsStrictPartialOrder

  _⊎-<-isTotalOrder_ : ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {≤₁ : Rel A₁ ℓ₁′}
                         {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {≤₂ : Rel A₂ ℓ₂′} →
                       IsTotalOrder ≈₁ ≤₁ → IsTotalOrder ≈₂ ≤₂ →
                       IsTotalOrder (≈₁ ⊎-Rel ≈₂) (≤₁ ⊎-< ≤₂)
  to₁ ⊎-<-isTotalOrder to₂ = record
    { isPartialOrder = isPartialOrder to₁ ⊎-isPartialOrder
                       isPartialOrder to₂
    ; total          = total to₁ ⊎-<-total total to₂
    }
    where open IsTotalOrder

  _⊎-<-isDecTotalOrder_ :
    ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {≤₁ : Rel A₁ ℓ₁′}
      {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {≤₂ : Rel A₂ ℓ₂′} →
    IsDecTotalOrder ≈₁ ≤₁ → IsDecTotalOrder ≈₂ ≤₂ →
    IsDecTotalOrder (≈₁ ⊎-Rel ≈₂) (≤₁ ⊎-< ≤₂)
  to₁ ⊎-<-isDecTotalOrder to₂ = record
    { isTotalOrder = isTotalOrder to₁ ⊎-<-isTotalOrder isTotalOrder to₂
    ; _≟_          = ⊎-decidable (_≟_  to₁) (_≟_  to₂) (no ₁≁₂)
    ; _≤?_         = ⊎-decidable (_≤?_ to₁) (_≤?_ to₂) (yes (₁∼₂ _))
    }
    where open IsDecTotalOrder

  _⊎-<-isStrictTotalOrder_ :
    ∀ {ℓ₁ ℓ₁′} {≈₁ : Rel A₁ ℓ₁} {<₁ : Rel A₁ ℓ₁′}
      {ℓ₂ ℓ₂′} {≈₂ : Rel A₂ ℓ₂} {<₂ : Rel A₂ ℓ₂′} →
    IsStrictTotalOrder ≈₁ <₁ → IsStrictTotalOrder ≈₂ <₂ →
    IsStrictTotalOrder (≈₁ ⊎-Rel ≈₂) (<₁ ⊎-< <₂)
  sto₁ ⊎-<-isStrictTotalOrder sto₂ = record
    { isEquivalence = isEquivalence sto₁ ⊎-isEquivalence
                      isEquivalence sto₂
    ; trans         = trans    sto₁ ⊎-transitive     trans    sto₂
    ; compare       = compare  sto₁ ⊎-<-trichotomous compare  sto₂
    ; <-resp-≈      = <-resp-≈ sto₁ ⊎-≈-respects₂    <-resp-≈ sto₂
    }
    where open IsStrictTotalOrder

------------------------------------------------------------------------
-- The game can be taken even further...

_⊎-setoid_ : ∀ {s₁ s₂ s₃ s₄} →
             Setoid s₁ s₂ → Setoid s₃ s₄ → Setoid _ _
s₁ ⊎-setoid s₂ = record
  { isEquivalence = isEquivalence s₁ ⊎-isEquivalence isEquivalence s₂
  } where open Setoid

_⊎-preorder_ : ∀ {p₁ p₂ p₃ p₄ p₅ p₆} →
               Preorder p₁ p₂ p₃ → Preorder p₄ p₅ p₆ → Preorder _ _ _
p₁ ⊎-preorder p₂ = record
  { _∼_          = _∼_        p₁ ⊎-Rel        _∼_        p₂
  ; isPreorder   = isPreorder p₁ ⊎-isPreorder isPreorder p₂
  } where open Preorder

_⊎-decSetoid_ : ∀ {s₁ s₂ s₃ s₄} →
                DecSetoid s₁ s₂ → DecSetoid s₃ s₄ → DecSetoid _ _
ds₁ ⊎-decSetoid ds₂ = record
  { isDecEquivalence = isDecEquivalence ds₁ ⊎-isDecEquivalence
                       isDecEquivalence ds₂
  } where open DecSetoid

_⊎-poset_ : ∀ {p₁ p₂ p₃ p₄ p₅ p₆} →
            Poset p₁ p₂ p₃ → Poset p₄ p₅ p₆ → Poset _ _ _
po₁ ⊎-poset po₂ = record
  { _≤_            = _≤_ po₁ ⊎-Rel _≤_ po₂
  ; isPartialOrder = isPartialOrder po₁ ⊎-isPartialOrder
                     isPartialOrder po₂
  } where open Poset

_⊎-<-poset_ : ∀ {p₁ p₂ p₃ p₄ p₅ p₆} →
              Poset p₁ p₂ p₃ → Poset p₄ p₅ p₆ → Poset _ _ _
po₁ ⊎-<-poset po₂ = record
  { _≤_            = _≤_ po₁ ⊎-< _≤_ po₂
  ; isPartialOrder = isPartialOrder po₁ ⊎-isPartialOrder
                     isPartialOrder po₂
  } where open Poset

_⊎-<-strictPartialOrder_ :
  ∀ {p₁ p₂ p₃ p₄ p₅ p₆} →
  StrictPartialOrder p₁ p₂ p₃ → StrictPartialOrder p₄ p₅ p₆ →
  StrictPartialOrder _ _ _
spo₁ ⊎-<-strictPartialOrder spo₂ = record
  { _<_                  = _<_ spo₁ ⊎-< _<_ spo₂
  ; isStrictPartialOrder = isStrictPartialOrder spo₁
                             ⊎-isStrictPartialOrder
                           isStrictPartialOrder spo₂
  } where open StrictPartialOrder

_⊎-<-totalOrder_ :
  ∀ {t₁ t₂ t₃ t₄ t₅ t₆} →
  TotalOrder t₁ t₂ t₃ → TotalOrder t₄ t₅ t₆ → TotalOrder _ _ _
to₁ ⊎-<-totalOrder to₂ = record
  { isTotalOrder = isTotalOrder to₁ ⊎-<-isTotalOrder isTotalOrder to₂
  } where open TotalOrder

_⊎-<-decTotalOrder_ :
  ∀ {t₁ t₂ t₃ t₄ t₅ t₆} →
  DecTotalOrder t₁ t₂ t₃ → DecTotalOrder t₄ t₅ t₆ → DecTotalOrder _ _ _
to₁ ⊎-<-decTotalOrder to₂ = record
  { isDecTotalOrder = isDecTotalOrder to₁ ⊎-<-isDecTotalOrder
                      isDecTotalOrder to₂
  } where open DecTotalOrder

_⊎-<-strictTotalOrder_ :
  ∀ {p₁ p₂ p₃ p₄ p₅ p₆} →
  StrictTotalOrder p₁ p₂ p₃ → StrictTotalOrder p₄ p₅ p₆ →
  StrictTotalOrder _ _ _
sto₁ ⊎-<-strictTotalOrder sto₂ = record
  { _<_                = _<_ sto₁ ⊎-< _<_ sto₂
  ; isStrictTotalOrder = isStrictTotalOrder sto₁
                           ⊎-<-isStrictTotalOrder
                         isStrictTotalOrder sto₂
  } where open StrictTotalOrder

------------------------------------------------------------------------
-- Some properties related to "relatedness"

private

  to-cong : ∀ {a b} {A : Set a} {B : Set b} →
            (_≡_ ⊎-Rel _≡_) ⇒ _≡_ {A = A ⊎ B}
  to-cong (₁∼₂ ())
  to-cong (₁∼₁ P.refl) = P.refl
  to-cong (₂∼₂ P.refl) = P.refl

  from-cong : ∀ {a b} {A : Set a} {B : Set b} →
              _≡_ {A = A ⊎ B} ⇒ (_≡_ ⊎-Rel _≡_)
  from-cong P.refl = P.refl ⊎-refl P.refl

⊎-Rel↔≡ : ∀ {a b} (A : Set a) (B : Set b) →
          Inverse (P.setoid A ⊎-setoid P.setoid B) (P.setoid (A ⊎ B))
⊎-Rel↔≡ _ _ = record
  { to         = record { _⟨$⟩_ = id; cong = to-cong   }
  ; from       = record { _⟨$⟩_ = id; cong = from-cong }
  ; inverse-of = record
    { left-inverse-of  = λ _ → P.refl ⊎-refl P.refl
    ; right-inverse-of = λ _ → P.refl
    }
  }

_⊎-≟_ : ∀ {a b} {A : Set a} {B : Set b} →
        Decidable {A = A} _≡_ → Decidable {A = B} _≡_ →
        Decidable {A = A ⊎ B} _≡_
(dec₁ ⊎-≟ dec₂) s₁ s₂ = Dec.map′ to-cong from-cong (s₁ ≟ s₂)
  where
  open DecSetoid (P.decSetoid dec₁ ⊎-decSetoid P.decSetoid dec₂)

_⊎-⟶_ :
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
  A ⟶ B → C ⟶ D → (A ⊎-setoid C) ⟶ (B ⊎-setoid D)
_⊎-⟶_ {A = A} {B} {C} {D} f g = record
  { _⟨$⟩_ = fg
  ; cong  = fg-cong
  }
  where
  open Setoid (A ⊎-setoid C) using () renaming (_≈_ to _≈AC_)
  open Setoid (B ⊎-setoid D) using () renaming (_≈_ to _≈BD_)

  fg = Sum.map (_⟨$⟩_ f) (_⟨$⟩_ g)

  fg-cong : _≈AC_ =[ fg ]⇒ _≈BD_
  fg-cong (₁∼₂ ())
  fg-cong (₁∼₁ x∼₁y) = ₁∼₁ $ F.cong f x∼₁y
  fg-cong (₂∼₂ x∼₂y) = ₂∼₂ $ F.cong g x∼₂y

_⊎-equivalence_ :
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
  Equivalence A B → Equivalence C D →
  Equivalence (A ⊎-setoid C) (B ⊎-setoid D)
A⇔B ⊎-equivalence C⇔D = record
  { to   = to   A⇔B ⊎-⟶ to   C⇔D
  ; from = from A⇔B ⊎-⟶ from C⇔D
  } where open Equivalence

_⊎-⇔_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
        A ⇔ B → C ⇔ D → (A ⊎ C) ⇔ (B ⊎ D)
_⊎-⇔_ {A = A} {B} {C} {D} A⇔B C⇔D =
  Inverse.equivalence (⊎-Rel↔≡ B D) ⟨∘⟩
  A⇔B ⊎-equivalence C⇔D ⟨∘⟩
  Eq.sym (Inverse.equivalence (⊎-Rel↔≡ A C))
  where open Eq using () renaming (_∘_ to _⟨∘⟩_)

_⊎-injection_ :
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
  Injection A B → Injection C D →
  Injection (A ⊎-setoid C) (B ⊎-setoid D)
_⊎-injection_ {A = A} {B} {C} {D} A↣B C↣D = record
  { to        = to A↣B ⊎-⟶ to C↣D
  ; injective = inj _ _
  }
  where
  open Injection
  open Setoid (A ⊎-setoid C) using () renaming (_≈_ to _≈AC_)
  open Setoid (B ⊎-setoid D) using () renaming (_≈_ to _≈BD_)

  inj : ∀ x y →
        (to A↣B ⊎-⟶ to C↣D) ⟨$⟩ x ≈BD (to A↣B ⊎-⟶ to C↣D) ⟨$⟩ y →
        x ≈AC y
  inj (inj₁ x) (inj₁ y) (₁∼₁ x∼₁y) = ₁∼₁ (injective A↣B x∼₁y)
  inj (inj₂ x) (inj₂ y) (₂∼₂ x∼₂y) = ₂∼₂ (injective C↣D x∼₂y)
  inj (inj₁ x) (inj₂ y) (₁∼₂ ())
  inj (inj₂ x) (inj₁ y) ()

_⊎-↣_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
        A ↣ B → C ↣ D → (A ⊎ C) ↣ (B ⊎ D)
_⊎-↣_ {A = A} {B} {C} {D} A↣B C↣D =
  Inverse.injection (⊎-Rel↔≡ B D) ⟨∘⟩
  A↣B ⊎-injection C↣D ⟨∘⟩
  Inverse.injection (Inv.sym (⊎-Rel↔≡ A C))
  where open Inj using () renaming (_∘_ to _⟨∘⟩_)

_⊎-left-inverse_ :
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
  LeftInverse A B → LeftInverse C D →
  LeftInverse (A ⊎-setoid C) (B ⊎-setoid D)
A↞B ⊎-left-inverse C↞D = record
  { to              = Equivalence.to eq
  ; from            = Equivalence.from eq
  ; left-inverse-of = [ ₁∼₁ ∘ left-inverse-of A↞B
                      , ₂∼₂ ∘ left-inverse-of C↞D
                      ]
  }
  where
  open LeftInverse
  eq = LeftInverse.equivalence A↞B ⊎-equivalence
       LeftInverse.equivalence C↞D

_⊎-↞_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
        A ↞ B → C ↞ D → (A ⊎ C) ↞ (B ⊎ D)
_⊎-↞_ {A = A} {B} {C} {D} A↞B C↞D =
  Inverse.left-inverse (⊎-Rel↔≡ B D) ⟨∘⟩
  A↞B ⊎-left-inverse C↞D ⟨∘⟩
  Inverse.left-inverse (Inv.sym (⊎-Rel↔≡ A C))
  where open LeftInv using () renaming (_∘_ to _⟨∘⟩_)

_⊎-surjection_ :
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
  Surjection A B → Surjection C D →
  Surjection (A ⊎-setoid C) (B ⊎-setoid D)
A↠B ⊎-surjection C↠D = record
  { to         = LeftInverse.from inv
  ; surjective = record
    { from             = LeftInverse.to inv
    ; right-inverse-of = LeftInverse.left-inverse-of inv
    }
  }
  where
  open Surjection
  inv = right-inverse A↠B ⊎-left-inverse right-inverse C↠D

_⊎-↠_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
        A ↠ B → C ↠ D → (A ⊎ C) ↠ (B ⊎ D)
_⊎-↠_ {A = A} {B} {C} {D} A↠B C↠D =
  Inverse.surjection (⊎-Rel↔≡ B D) ⟨∘⟩
  A↠B ⊎-surjection C↠D ⟨∘⟩
  Inverse.surjection (Inv.sym (⊎-Rel↔≡ A C))
  where open Surj using () renaming (_∘_ to _⟨∘⟩_)

_⊎-inverse_ :
  ∀ {s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈}
    {A : Setoid s₁ s₂} {B : Setoid s₃ s₄}
    {C : Setoid s₅ s₆} {D : Setoid s₇ s₈} →
  Inverse A B → Inverse C D → Inverse (A ⊎-setoid C) (B ⊎-setoid D)
A↔B ⊎-inverse C↔D = record
  { to         = Surjection.to   surj
  ; from       = Surjection.from surj
  ; inverse-of = record
    { left-inverse-of  = LeftInverse.left-inverse-of inv
    ; right-inverse-of = Surjection.right-inverse-of surj
    }
  }
  where
  open Inverse
  surj = Inverse.surjection   A↔B ⊎-surjection
         Inverse.surjection   C↔D
  inv  = Inverse.left-inverse A↔B ⊎-left-inverse
         Inverse.left-inverse C↔D

_⊎-↔_ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
        A ↔ B → C ↔ D → (A ⊎ C) ↔ (B ⊎ D)
_⊎-↔_ {A = A} {B} {C} {D} A↔B C↔D =
  ⊎-Rel↔≡ B D ⟨∘⟩ A↔B ⊎-inverse C↔D ⟨∘⟩ Inv.sym (⊎-Rel↔≡ A C)
  where open Inv using () renaming (_∘_ to _⟨∘⟩_)

_⊎-cong_ : ∀ {k a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d} →
           A ∼[ k ] B → C ∼[ k ] D → (A ⊎ C) ∼[ k ] (B ⊎ D)
_⊎-cong_ {implication}         = Sum.map
_⊎-cong_ {reverse-implication} = λ f g → lam (Sum.map (app-← f) (app-← g))
_⊎-cong_ {equivalence}         = _⊎-⇔_
_⊎-cong_ {injection}           = _⊎-↣_
_⊎-cong_ {reverse-injection}   = λ f g → lam (app-↢ f ⊎-↣ app-↢ g)
_⊎-cong_ {left-inverse}        = _⊎-↞_
_⊎-cong_ {surjection}          = _⊎-↠_
_⊎-cong_ {bijection}           = _⊎-↔_


text:
module Eq where

open import Prelude
open import T
open import Contexts
open import Eq.Defs
import Eq.KleeneTheory
import Eq.ObsTheory
import Eq.LogicalTheory
import Eq.Theory

open Eq.Defs public
open Eq.KleeneTheory public using (kleene-is-equivalence ; nats-halt)
open Eq.ObsTheory public using (obs-is-coarsest ; obs-is-con-congruence)
open Eq.LogicalTheory public using (log-is-con-congruence)
open Eq.Theory public

ext: agda

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


text:
-- Andreas, 2014-09-01 restored this test case

module ClashingModuleImport where

module M where

open import Imports.Module public

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
{-# OPTIONS --type-in-type #-}
module pisearch where
open import Type hiding (★_)
open import Function.NP
open import Data.Product
open import Data.Sum
open import Data.Bool.NP
open import Search.Type
open import Search.Searchable.Product
open import Search.Searchable
open import sum

fromFun-searchInd : ∀ {A} {sA : Search A} → SearchInd sA → FromFun sA
fromFun-searchInd indA = indA (λ s → Data s _) _,_

open import Relation.Binary.PropositionalEquality hiding ([_])
ToFrom : ∀ {A} (sA : Search A)
           (toFunA : ToFun sA)
           (fromFunA : FromFun sA)
         → ★
ToFrom {A} sA toFunA fromFunA = ∀ {B} (f : Π A B) x → toFunA (fromFunA f) x ≡ f x

FromTo : ∀ {A} (sA : Search A)
           (toFunA : ToFun sA)
           (fromFunA : FromFun sA)
         → ★
FromTo sA toFunA fromFunA = ∀ {B} (d : Data sA B) → fromFunA (toFunA d) ≡ d

module Σ-props {A} {B : A → ★}
                (μA : Searchable A) (μB : ∀ {x} → Searchable (B x)) where
    sA = search μA
    sB : ∀ {x} → Search (B x)
    sB {x} = search (μB {x})
    fromFunA : FromFun sA
    fromFunA = fromFun-searchInd (search-ind μA)
    fromFunB : ∀ {x} → FromFun (sB {x})
    fromFunB {x} = fromFun-searchInd (search-ind (μB {x}))
    module ToFrom
             (toFunA : ToFun sA)
             (toFunB : ∀ {x} → ToFun (sB {x}))
             (toFromA : ToFrom sA toFunA fromFunA)
             (toFromB : ∀ {x} → ToFrom (sB {x}) toFunB fromFunB) where
        toFrom-Σ : ToFrom (ΣSearch sA (λ {x} → sB {x})) (toFun-Σ sA sB toFunA toFunB) (fromFun-Σ sA sB fromFunA fromFunB)
        toFrom-Σ f (x , y) rewrite toFromA (fromFunB ∘ curry f) x = toFromB (curry f x) y

    {- we need a search-ind-ext...
    module FromTo
                 (toFunA : ToFun sA)
                 (toFunB : ∀ {x} → ToFun (sB {x}))
                 (toFromA : FromTo sA toFunA fromFunA)
                 (toFromB : ∀ {x} → FromTo (sB {x}) toFunB fromFunB) where
        toFrom-Σ : FromTo (ΣSearch sA (λ {x} → sB {x})) (toFun-Σ sA sB toFunA toFunB) (fromFun-Σ sA sB fromFunA fromFunB)
        toFrom-Σ t = {!toFromA!} -- {!(λ x → toFromB (toFunA t x))!}
    -}

toFun-× : ∀ {A B} (sA : Search A) (sB : Search B) → ToFun sA → ToFun sB → ToFun (sA ×Search sB)
toFun-× sA sB toFunA toFunB = toFun-Σ sA sB toFunA toFunB

fromFun-× : ∀ {A B} (sA : Search A) (sB : Search B) → FromFun sA → FromFun sB → FromFun (sA ×Search sB)
fromFun-× sA sB fromFunA fromFunB = fromFun-Σ sA sB fromFunA fromFunB

toFun-Bit : ToFun (search μBit)
toFun-Bit (f , t) false = f
toFun-Bit (f , t) true  = t

fromFun-Bit : FromFun (search μBit)
fromFun-Bit f = f false , f true

toFun-⊎ : ∀ {A B} (sA : Search A) (sB : Search B) → ToFun sA → ToFun sB → ToFun (sA +Search sB)
toFun-⊎ sA sB toFunA toFunB (x , y) = [ toFunA x , toFunB y ]

fromFun-⊎ : ∀ {A B} (sA : Search A) (sB : Search B) → FromFun sA → FromFun sB → FromFun (sA +Search sB)
fromFun-⊎ sA sB fromFunA fromFunB f = fromFunA (f ∘ inj₁) , fromFunB (f ∘ inj₂)

toPair-searchInd : ∀ {A} {sA : Search A} → SearchInd sA → ToPair sA
toPair-searchInd indA = indA ToPair (λ P0 P1 → [ P0 , P1 ]) (λ η → _,_ η)

-- toFun-searchInd : ∀ {A} {sA : Search A} → SearchInd sA → ToFun sA
-- toFun-searchInd {A} {sA} indA {B} t = ?

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


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

module Math.NumberTheory.Summation.Generic.Properties where

-- agda-stdlib
open import Algebra
import Algebra.Operations.CommutativeMonoid as CommutativeMonoidOperations
open import Data.Nat as ℕ hiding (_+_; _*_)
import Data.Fin as Fin
import Data.Nat.Properties as ℕₚ
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Function.Base

-- agda-misc
open import Math.NumberTheory.Summation.Generic
import Math.NumberTheory.Summation.Generic.Properties.Lemma as Lemma

module MonoidSummationProperties {c e} (M : Monoid c e) where
  open MonoidSummation M
  open Monoid M
  open SetoidReasoning setoid

  -- Congruence
  Σ<-cong : ∀ {m n f g} → m ≡ n → (∀ x → f x ≈ g x) → Σ< m f ≈ Σ< n g
  Σ<-cong {0}     {.0}       {f} {g} ≡.refl f≈g = refl
  Σ<-cong {suc m} {.(suc m)} {f} {g} ≡.refl f≈g = begin
    Σ< m f ∙ f m ≈⟨ ∙-cong (Σ<-cong {m = m} {n = m} ≡.refl f≈g) (f≈g m) ⟩
    Σ< m g ∙ g m ∎

  Σ<-congˡ : ∀ n {f g} → (∀ x → f x ≈ g x) → Σ< n f ≈ Σ< n g
  Σ<-congˡ n f≈g = Σ<-cong {m = n} ≡.refl f≈g

  Σ<-congʳ : ∀ {m n} f → m ≡ n → Σ< m f ≈ Σ< n f
  Σ<-congʳ f m≡n = Σ<-cong {f = f} m≡n (λ _ → refl)

  Σ≤-cong : ∀ {m n f g} → m ≡ n → (∀ x → f x ≈ g x) → Σ≤ m f ≈ Σ≤ n g
  Σ≤-cong m≡n f≈g = Σ<-cong (≡.cong suc m≡n) f≈g

  Σ≤-congˡ : ∀ n {f g} → (∀ x → f x ≈ g x) → Σ≤ n f ≈ Σ≤ n g
  Σ≤-congˡ n = Σ<-congˡ (suc n)

  Σ≤-congʳ : ∀ {m n} f → m ≡ n → Σ≤ m f ≈ Σ≤ n f
  Σ≤-congʳ f m≡n = Σ<-congʳ f (≡.cong suc m≡n)

  Σ<range-cong : ∀ {m n o p} {f g : ℕ → Carrier} → m ≡ n → o ≡ p →
    (∀ x → f x ≈ g x) → Σ<range m o f ≈ Σ<range n p g
  Σ<range-cong {m} {.m} {o} {.o} {f} {g} ≡.refl ≡.refl f≈g = begin
    Σ< (o ∸ m) (λ k → f (m ℕ.+ k)) ≈⟨ Σ<-congˡ (o ∸ m) (λ x → f≈g (m ℕ.+ x)) ⟩
    Σ< (o ∸ m) (λ k → g (m ℕ.+ k)) ∎

  Σ<range-cong₃ : ∀ m n {f g : ℕ → Carrier} →
    (∀ x → f x ≈ g x) → Σ<range m n f ≈ Σ<range m n g
  Σ<range-cong₃ m n f≈g = Σ<range-cong {m = m} {o = n} ≡.refl ≡.refl f≈g

  Σ<range-cong₁₂ : ∀ {m n o p} (f : ℕ → Carrier) →
    m ≡ n → o ≡ p → Σ<range m o f ≈ Σ<range n p f
  Σ<range-cong₁₂ f ≡.refl ≡.refl = refl

  Σ<range-cong₁ : ∀ {m n} o (f : ℕ → Carrier)→
    m ≡ n → Σ<range m o f ≈ Σ<range n o f
  Σ<range-cong₁ o f m≡n = Σ<range-cong₁₂ {o = o} f m≡n ≡.refl

  Σ<range-cong₂ : ∀ m {n o} (f : ℕ → Carrier) →
    n ≡ o → Σ<range m n f ≈ Σ<range m o f
  Σ<range-cong₂ m f n≡o = Σ<range-cong₁₂ {m = m} f ≡.refl n≡o

  Σ≤range-cong : ∀ {m n o p} {f g : ℕ → Carrier} →
    m ≡ n → o ≡ p → (∀ x → f x ≈ g x) → Σ≤range m o f ≈ Σ≤range n p g
  Σ≤range-cong m≡n o≡p f≈g = Σ<range-cong m≡n (≡.cong suc o≡p) f≈g

  Σ<-congˡ-with-< : ∀ n {f g} → (∀ i → i < n → f i ≈ g i) → Σ< n f ≈ Σ< n g
  Σ<-congˡ-with-< 0       {f} {g} f≈g = refl
  Σ<-congˡ-with-< (suc n) {f} {g} f≈g =
    ∙-cong (Σ<-congˡ-with-< n (λ i i<n → f≈g i (ℕₚ.≤-step i<n))) (f≈g n ℕₚ.≤-refl)

  Σ≤-congˡ-with-≤ : ∀ n {f g} → (∀ i → i ≤ n → f i ≈ g i) → Σ≤ n f ≈ Σ≤ n g
  Σ≤-congˡ-with-≤ n f≈g = Σ<-congˡ-with-< (suc n) λ i 1+i≤1+n → f≈g i (ℕₚ.≤-pred 1+i≤1+n)

  Σ<-0 : ∀ n → Σ< n (λ _ → ε) ≈ ε
  Σ<-0 zero    = refl
  Σ<-0 (suc n) = begin
    Σ< n (λ _ → ε) ∙ ε ≈⟨ ∙-congʳ $ Σ<-0 n ⟩
    ε ∙ ε              ≈⟨ identityʳ ε ⟩
    ε                  ∎

  Σ≤-0 : ∀ n → Σ≤ n (λ _ → ε) ≈ ε
  Σ≤-0 n = Σ<-0 (suc n)

  Σ<[1,f]≈f[0] : ∀ f → Σ< 1 f ≈ f 0
  Σ<[1,f]≈f[0] f = identityˡ (f 0)

  Σ≤[0,f]≈f[0] : ∀ f → Σ≤ 0 f ≈ f 0
  Σ≤[0,f]≈f[0] f = Σ<[1,f]≈f[0] f

  n≤m⇒Σ<range[m,n,f]≈0 : ∀ {m n} f → n ≤ m → Σ<range m n f ≈ ε
  n≤m⇒Σ<range[m,n,f]≈0 {m} {n} f n≤m = begin
    Σ< (n ∸ m) (λ k → f (m ℕ.+ k)) ≈⟨ Σ<-congʳ (λ k → f (m ℕ.+ k)) $ ℕₚ.m≤n⇒m∸n≡0 n≤m ⟩
    Σ< 0       (λ k → f (m ℕ.+ k)) ∎

  n<m⇒Σ≤range[m,n,f]≈0 : ∀ {m n} f → n < m → Σ≤range m n f ≈ ε
  n<m⇒Σ≤range[m,n,f]≈0 {m} {n} f n<m = n≤m⇒Σ<range[m,n,f]≈0 f n<m

  Σ<range[n,n,f]≈0 : ∀ n f → Σ<range n n f ≈ ε
  Σ<range[n,n,f]≈0 n f = n≤m⇒Σ<range[m,n,f]≈0 {n} {n} f ℕₚ.≤-refl

  Σ<range-cong₃-with-< : ∀ m n {f g} →
    (∀ i → m ≤ i → i < n → f i ≈ g i) → Σ<range m n f ≈ Σ<range m n g
  Σ<range-cong₃-with-< m n {f} {g} f≈g with m ℕₚ.≤? n
  ... | yes m≤n =
    Σ<-congˡ-with-< (n ∸ m) {λ i → f (m ℕ.+ i)} {λ i → g (m ℕ.+ i)}
      λ i i<n∸m → f≈g (m ℕ.+ i) (ℕₚ.m≤m+n m i) (≤R.begin
        1 ℕ.+ (m ℕ.+ i) ≤R.≡⟨ ≡.cong (1 ℕ.+_) $ ℕₚ.+-comm m i ⟩
        suc i ℕ.+ m     ≤R.≤⟨ ℕₚ.+-monoˡ-≤ m i<n∸m ⟩
        o ℕ.+ m         ≤R.≡⟨ ≡.sym n≡o+m ⟩
        n               ≤R.∎ )
      where o = n ∸ m
            n≡o+m : n ≡ o ℕ.+ m
            n≡o+m = ≡.sym $ ℕₚ.m∸n+n≡m m≤n
            module ≤R = ℕₚ.≤-Reasoning
  ... | no m≰n = trans (n≤m⇒Σ<range[m,n,f]≈0 f n≤m) (sym $ n≤m⇒Σ<range[m,n,f]≈0 g n≤m)
    where n≤m = ℕₚ.<⇒≤ $ ℕₚ.≰⇒> m≰n

  Σ≤range-cong₃-with-≤ : ∀ m n {f g} →
    (∀ i → m ≤ i → i ≤ n → f i ≈ g i) → Σ≤range m n f ≈ Σ≤range m n g
  Σ≤range-cong₃-with-≤ m n {f} {g} f≈g = Σ<range-cong₃-with-< m (suc n)
    λ i i≤n 1+i≤1+n → f≈g i i≤n (ℕₚ.≤-pred 1+i≤1+n)

  Σ<range[n,1+n,f]≈f[n] : ∀ n f → Σ<range n (suc n) f ≈ f n
  Σ<range[n,1+n,f]≈f[n] n f = begin
    Σ< (suc n ∸ n) (λ k → f (n ℕ.+ k))
      ≈⟨ Σ<-congʳ (λ k → f (n ℕ.+ k)) $ ℕₚ.m+n∸n≡m 1 n ⟩
    Σ< 1 (λ k → f (n ℕ.+ k))
      ≈⟨ Σ<[1,f]≈f[0] (λ k → f (n ℕ.+ k)) ⟩
    f (n ℕ.+ 0)
      ≈⟨ reflexive (≡.cong f (ℕₚ.+-identityʳ n)) ⟩
    f n
      ∎

  Σ≤range[n,n,f]≈f[n] : ∀ n f → Σ≤range n n f ≈ f n
  Σ≤range[n,n,f]≈f[n] = Σ<range[n,1+n,f]≈f[n]

  Σ<-+ : ∀ m n f → Σ< (m ℕ.+ n) f ≈ Σ< m f ∙ Σ< n (λ k → f (m ℕ.+ k))
  Σ<-+ m zero    f = begin
    Σ< (m ℕ.+ 0) f ≈⟨ Σ<-congʳ f $ ℕₚ.+-identityʳ m ⟩
    Σ< m f         ≈⟨ sym $ identityʳ (Σ< m f) ⟩
    Σ< m f ∙ ε     ∎
  Σ<-+ m (suc n) f = begin
    Σ< (m ℕ.+ suc n) f
      ≈⟨ Σ<-congʳ f $ ℕₚ.+-suc m n ⟩
    Σ< (suc m ℕ.+ n) f
      ≡⟨⟩
    Σ< (m ℕ.+ n) f ∙ f (m ℕ.+ n)
      ≈⟨ ∙-congʳ $ Σ<-+ m n f ⟩
    Σ< m f ∙ Σ< n (λ k → f (m ℕ.+ k)) ∙ f (m ℕ.+ n)
      ≈⟨ assoc (Σ< m f) (Σ< n (λ k → f (m ℕ.+ k))) (f (m ℕ.+ n)) ⟩
    Σ< m f ∙ Σ< (suc n) (λ k → f (m ℕ.+ k))
      ∎

  Σ≤-Σ<-+ : ∀ m n f →
    Σ≤ (m ℕ.+ n) f ≈ Σ≤ m f ∙ Σ< n (λ k → f (1 ℕ.+ m ℕ.+ k))
  Σ≤-Σ<-+ m n f = Σ<-+ (suc m) n f

  Σ≤-+ : ∀ m n f →
    Σ≤ (1 ℕ.+ m ℕ.+ n) f ≈ Σ≤ m f ∙ Σ≤ n (λ k → f (1 ℕ.+ m ℕ.+ k))
  Σ≤-+ m n f = begin
    Σ< (2 ℕ.+ m ℕ.+ n) f
      ≈⟨ Σ<-congʳ f $ Lemma.lemma₁ m n ⟩
    Σ< (suc m ℕ.+ suc n) f
      ≈⟨ Σ<-+ (suc m) (suc n) f ⟩
    Σ< (suc m) f ∙ Σ< (suc n) (λ k → f (1 ℕ.+ m ℕ.+ k))
      ∎

  Σ<-push-suc : ∀ n f → Σ< (suc n) f ≈ f 0 ∙ Σ< n (λ k → f (suc k))
  Σ<-push-suc n f = begin
    Σ< (suc n) f                   ≈⟨ Σ<-+ 1 n f ⟩
    Σ< 1 f ∙ Σ< n (λ k → f (suc k)) ≈⟨ ∙-congʳ $ Σ<[1,f]≈f[0] f ⟩
    f 0 ∙ Σ< n (λ k → f (suc k))    ∎

  Σ≤-push-suc : ∀ n f → Σ≤ (suc n) f ≈ f 0 ∙ Σ≤ n (λ k → f (suc k))
  Σ≤-push-suc n f = Σ<-push-suc (suc n) f

  Σ<range[0,n,f]≈Σ<[n,f] : ∀ n f → Σ<range 0 n f ≈ Σ< n f
  Σ<range[0,n,f]≈Σ<[n,f] n f = refl

  Σ≤range[0,n,f]≈Σ≤[n,f] : ∀ n f → Σ≤range 0 n f ≈ Σ≤ n f
  Σ≤range[0,n,f]≈Σ≤[n,f] n f = refl

  Σ<range[m,m+n+o,f]≈Σ<range[m,m+n,f]+Σ<range[m+n,m+n+o,f] : ∀ m n o f →
    Σ<range m (m ℕ.+ n ℕ.+ o) f ≈
    Σ<range m (m ℕ.+ n) f ∙ Σ<range (m ℕ.+ n) (m ℕ.+ n ℕ.+ o) f
  Σ<range[m,m+n+o,f]≈Σ<range[m,m+n,f]+Σ<range[m+n,m+n+o,f] m n o f = begin
    Σ< (m+n+o ∸ m) f′
      ≈⟨ Σ<-congʳ f′ (≡.cong (_∸ m) $ ℕₚ.+-assoc m n o) ⟩
    Σ< (m ℕ.+ n+o ∸ m) f′
      ≈⟨ Σ<-congʳ f′ (ℕₚ.m+n∸m≡n m n+o) ⟩
    Σ< n+o f′
      ≈⟨ Σ<-+ n o f′ ⟩
    Σ< n f′ ∙ Σ< o (λ k → f (m ℕ.+ (n ℕ.+ k)))
      ≈⟨ ∙-cong (sym $ Σ<-congʳ f′ $ ℕₚ.m+n∸m≡n m n)
                (sym $ Σ<-cong (ℕₚ.m+n∸m≡n m+n o)
                               (λ x → reflexive (≡.cong f (ℕₚ.+-assoc m n x)))) ⟩
    Σ< (m+n ∸ m) f′ ∙ Σ< (m+n+o ∸ m+n) (λ k → f (m+n ℕ.+ k))
      ∎
    where
    m+n = m ℕ.+ n
    n+o = n ℕ.+ o
    m+n+o = m+n ℕ.+ o
    f′ = λ k → f (m ℕ.+ k)

  Σ<range[m,n,f]≈Σ<range[m,o,f]+Σ<range[o,n,f] : ∀ {m n o} f →
    m ≤ o → o ≤ n →
    Σ<range m n f ≈ Σ<range m o f ∙ Σ<range o n f
  Σ<range[m,n,f]≈Σ<range[m,o,f]+Σ<range[o,n,f] {m} {n} {o} f m≤o o≤n = begin
    Σ<range m n f
      ≈⟨ reflexive (≡.cong (λ v → Σ<range m v f) n≡m+p+q) ⟩
    Σ<range m m+p+q f
      ≈⟨ Σ<range[m,m+n+o,f]≈Σ<range[m,m+n,f]+Σ<range[m+n,m+n+o,f] m p q f ⟩
    Σ<range m m+p f ∙ Σ<range m+p m+p+q f
      ≈⟨ sym $ ∙-cong (Σ<range-cong₂ m f o≡m+p) (Σ<range-cong₁₂ f o≡m+p n≡m+p+q) ⟩
    Σ<range m o f ∙ Σ<range o n f
      ∎
    where
    p = o ∸ m
    q = n ∸ o
    m+p = m ℕ.+ p
    m+p+q = m+p ℕ.+ q
    o≡m+p : o ≡ m+p
    o≡m+p = ≡.sym $ ℕₚ.m+[n∸m]≡n m≤o
    n≡m+p+q : n ≡ m+p+q
    n≡m+p+q = ≡.sym ( ≡R.begin
      m ℕ.+ p ℕ.+ q ≡R.≡⟨ ≡.cong (ℕ._+ q) $ ≡.sym o≡m+p ⟩
      o ℕ.+ (n ∸ o) ≡R.≡⟨ ℕₚ.m+[n∸m]≡n o≤n ⟩
      n             ≡R.∎ )
      where module ≡R = ≡.≡-Reasoning

  -- Reindex
  Σ<range[m,n,f]≈Σ<range[o+m,o+n,i→f[i∸o]] : ∀ m n o f →
    Σ<range m n f ≈ Σ<range (o ℕ.+ m) (o ℕ.+ n) (λ i → f (i ∸ o))
  Σ<range[m,n,f]≈Σ<range[o+m,o+n,i→f[i∸o]] m n o f = begin
    Σ< (n ∸ m) (λ k → f (m ℕ.+ k))
      ≈⟨ Σ<-cong (≡.sym $ ℕₚ.[m+n]∸[m+o]≡n∸o o n m)
                 (λ x → reflexive $ ≡.cong f $ ≡.sym $ (≡R.begin
          o ℕ.+ m ℕ.+ x ∸ o   ≡R.≡⟨ ≡.cong (_∸ o) $ ℕₚ.+-assoc o m x ⟩
          o ℕ.+ (m ℕ.+ x) ∸ o ≡R.≡⟨ ℕₚ.m+n∸m≡n o (m ℕ.+ x) ⟩
          m ℕ.+ x             ≡R.∎ ))  ⟩
    Σ< ((o ℕ.+ n) ∸ (o ℕ.+ m)) (λ k → f ((o ℕ.+ m ℕ.+ k) ∸ o))
      ∎
    where module ≡R = ≡.≡-Reasoning

  Σ≤range[m,n,f]≈Σ≤range[o+m,o+n,i→f[i∸o]] : ∀ m n o f →
    Σ≤range m n f ≈ Σ≤range (o ℕ.+ m) (o ℕ.+ n) (λ i → f (i ∸ o))
  Σ≤range[m,n,f]≈Σ≤range[o+m,o+n,i→f[i∸o]] m n o f = begin
    Σ<range m (suc n) f
      ≈⟨ Σ<range[m,n,f]≈Σ<range[o+m,o+n,i→f[i∸o]] m (suc n) o f ⟩
    Σ<range (o ℕ.+ m) (o ℕ.+ suc n) (λ i → f (i ∸ o))
      ≈⟨ Σ<range-cong₂ (o ℕ.+ m) (λ i → f (i ∸ o)) $ ℕₚ.+-suc o n ⟩
    Σ<range (o ℕ.+ m) (suc o ℕ.+ n) (λ i → f (i ∸ o))
      ∎

module CommutativeMonoidSummationProperties
  {c e} (CM : CommutativeMonoid c e) where
  open CommutativeMonoid CM
  open MonoidSummation monoid
  open MonoidSummationProperties monoid public
  open CommutativeMonoidOperations CM
  open SetoidReasoning setoid

  private
    n×x+x≈x+n×x : ∀ n x → n × x ∙ x ≈ x ∙ n × x
    n×x+x≈x+n×x zero    x = trans (identityˡ x) (sym $ identityʳ x)
    n×x+x≈x+n×x (suc n) x = begin
      x ∙ n × x ∙ x   ≈⟨ assoc x (n × x) x ⟩
      x ∙ (n × x ∙ x) ≈⟨ ∙-congˡ $ n×x+x≈x+n×x n x ⟩
      x ∙ (x ∙ n × x) ∎

  Σ<-const : ∀ n x → Σ< n (const x) ≈ n × x
  Σ<-const zero    x = refl
  Σ<-const (suc n) x = begin
    Σ< n (const x) ∙ x ≈⟨ ∙-congʳ $ Σ<-const n x ⟩
    n × x ∙ x          ≈⟨ n×x+x≈x+n×x n x ⟩
    x ∙ n × x          ∎

  Σ≤-const : ∀ n x → Σ≤ n (const x) ≈ suc n × x
  Σ≤-const n x = Σ<-const (suc n) x

  Σ<range-const : ∀ m n x → Σ<range m n (const x) ≈ (n ∸ m) × x
  Σ<range-const m n x = Σ<-const (n ∸ m) x

  Σ≤range-const : ∀ m n x → Σ≤range m n (const x) ≈ (suc n ∸ m) × x
  Σ≤range-const m n x = Σ<range-const m (suc n) x

  private
    lemma : ∀ a b c d → a ∙ b ∙ (c ∙ d) ≈ a ∙ c ∙ (b ∙ d)
    lemma a b c d = begin
      (a ∙ b) ∙ (c ∙ d) ≈⟨ assoc a b (c ∙ d) ⟩
      a ∙ (b ∙ (c ∙ d)) ≈⟨ sym $ ∙-congˡ $ assoc b c d ⟩
      a ∙ ((b ∙ c) ∙ d) ≈⟨ ∙-congˡ $ ∙-congʳ $ comm b c ⟩
      a ∙ ((c ∙ b) ∙ d) ≈⟨ ∙-congˡ $ assoc c b d ⟩
      a ∙ (c ∙ (b ∙ d)) ≈⟨ sym $ assoc a c (b ∙ d) ⟩
      (a ∙ c) ∙ (b ∙ d) ∎

  Σ<-distrib-+ : ∀ n f g → Σ< n (λ k → f k ∙ g k) ≈ Σ< n f ∙ Σ< n g
  Σ<-distrib-+ zero    f g = sym $ identityʳ ε
  Σ<-distrib-+ (suc n) f g = begin
    Σ< n (λ k → f k ∙ g k) ∙ (f n ∙ g n) ≈⟨ ∙-congʳ $ Σ<-distrib-+ n f g ⟩
    (Σ< n f ∙ Σ< n g) ∙ (f n ∙ g n)      ≈⟨ lemma (Σ< n f) (Σ< n g) (f n) (g n) ⟩
    (Σ< n f ∙ f n) ∙ (Σ< n g ∙ g n)      ∎

  Σ≤-distrib-+ : ∀ n f g → Σ≤ n (λ k → f k ∙ g k) ≈ Σ≤ n f ∙ Σ≤ n g
  Σ≤-distrib-+ n f g = Σ<-distrib-+ (suc n) f g

  Σ<range-distrib-+ : ∀ m n f g →
    Σ<range m n (λ k → f k ∙ g k) ≈ Σ<range m n f ∙ Σ<range m n g
  Σ<range-distrib-+ m n f g =
    Σ<-distrib-+ (n ∸ m) (λ k → f (m ℕ.+ k)) (λ k → g (m ℕ.+ k))

  Σ≤range-distrib-+ : ∀ m n f g →
    Σ≤range m n (λ k → f k ∙ g k) ≈ Σ≤range m n f ∙ Σ≤range m n g
  Σ≤range-distrib-+ m n f g = Σ<range-distrib-+ m (suc n) f g

  Σ<-comm : ∀ m n (f : ℕ → ℕ → Carrier) →
    Σ< m (λ i → Σ< n (λ j → f i j)) ≈ Σ< n (λ j → Σ< m (λ i → f i j))
  Σ<-comm zero    n f = sym $ Σ<-0 n
  Σ<-comm (suc m) n f = begin
    Σ< (suc m) (λ i → Σ< n (f i))
     ≡⟨⟩
    Σ< m (λ i → Σ< n (f i)) ∙ Σ< n (f m)
      ≈⟨ ∙-congʳ $ Σ<-comm m n f ⟩
    Σ< n (λ j → Σ< m (λ i → f i j)) ∙ Σ< n (λ j → f m j)
      ≈⟨ sym $ Σ<-distrib-+ n (λ j → Σ< m (λ i → f i j)) (λ j → f m j) ⟩
    Σ< n (λ j → Σ< m (λ i → f i j) ∙ f m j)
      ≡⟨⟩
    Σ< n (λ j → Σ< (suc m) (λ i → f i j))
      ∎

  Σ≤-comm : ∀ m n (f : ℕ → ℕ → Carrier) →
    Σ≤ m (λ i → Σ≤ n (λ j → f i j)) ≈ Σ≤ n (λ j → Σ≤ m (λ i → f i j))
  Σ≤-comm m n f = Σ<-comm (suc m) (suc n) f

  Σ<range-comm : ∀ m n o p (f : ℕ → ℕ → Carrier) →
    Σ<range m n (λ i → Σ<range o p (λ j → f i j)) ≈
    Σ<range o p (λ j → Σ<range m n (λ i → f i j))
  Σ<range-comm m n o p f =
    Σ<-comm (n ∸ m) (p ∸ o) (λ i j → f (m ℕ.+ i) (o ℕ.+ j))

  Σ≤range-comm : ∀ m n o p (f : ℕ → ℕ → Carrier) →
    Σ≤range m n (λ i → Σ≤range o p (λ j → f i j)) ≈
    Σ≤range o p (λ j → Σ≤range m n (λ i → f i j))
  Σ≤range-comm m n o p f = Σ<range-comm m (suc n) o (suc p) f

  Σ<-sumₜ-syntax : ∀ n f → Σ< n f ≈ sumₜ-syntax n (λ i → f (Fin.toℕ i))
  Σ<-sumₜ-syntax 0       f = refl
  Σ<-sumₜ-syntax (suc n) f = begin
    Σ< (suc n) f
      ≈⟨ Σ<-push-suc n f ⟩
    f 0 ∙ Σ< n (λ k → f (suc k))
      ≈⟨ ∙-congˡ $ Σ<-sumₜ-syntax n (λ k → f (suc k)) ⟩
    f 0 ∙ sumₜ-syntax n (λ i → f (Fin.toℕ (Fin.suc i)))
      ∎

  Σ<-reverse : ∀ n f → Σ< n f ≈ Σ< n (λ i → f (n ∸ suc i))
  Σ<-reverse 0       f = refl
  Σ<-reverse (suc n) f = begin
    Σ< (suc n) f
      ≈⟨ Σ<-push-suc n f ⟩
    f 0 ∙ Σ< n (λ i → f (suc i))
      ≈⟨ comm (f 0) (Σ< n (λ i → f (suc i))) ⟩
    Σ< n (λ i → f (suc i)) ∙ f 0
      ≈⟨ ∙-congʳ $ Σ<-reverse n (λ i → f (suc i)) ⟩
    Σ< n (λ i → f (suc (n ∸ suc i))) ∙ f 0
      ≈⟨ ∙-congʳ $ Σ<-congˡ-with-< n $ (λ i i<n → reflexive $ ≡.cong f $ ≡.sym $ ℕₚ.+-∸-assoc 1 i<n) ⟩
    Σ< n (λ i → f (suc n ∸ suc i)) ∙ f 0
      ≈⟨ ∙-congˡ $ reflexive $ ≡.cong f $ ≡.sym $ ℕₚ.n∸n≡0 (suc n) ⟩
    Σ< n (λ i → f (suc n ∸ suc i)) ∙ f (suc n ∸ suc n)
      ≡⟨⟩
    Σ< (suc n) (λ i → f (suc n ∸ suc i))
      ∎

  Σ≤-reverse : ∀ n f → Σ≤ n f ≈ Σ≤ n (λ i → f (n ∸ i))
  Σ≤-reverse n f = Σ<-reverse (suc n) f

  Σ<range-reverse : ∀ m n f → Σ<range m n f ≈ Σ<range m n (λ i → f (m ℕ.+ (n ∸ suc i)))
  Σ<range-reverse m n f = begin
    Σ< (n ∸ m) (λ i → f (m ℕ.+ i))
      ≈⟨ Σ<-reverse (n ∸ m) (λ i → f (m ℕ.+ i)) ⟩
    Σ< (n ∸ m) (λ i → f (m ℕ.+ ((n ∸ m) ∸ suc i)))
      ≈⟨ Σ<-congˡ (n ∸ m) $ (λ i → reflexive $ ≡.cong f $ ≡.cong (m ℕ.+_) $ (≤R.begin-equality
         n ∸ m ∸ suc i     ≤R.≡⟨ ℕₚ.∸-+-assoc n m (suc i) ⟩
         n ∸ (m ℕ.+ suc i) ≤R.≡⟨ ≡.cong (n ∸_) $ ℕₚ.+-suc m i ⟩
         n ∸ suc (m ℕ.+ i) ≤R.∎) ) ⟩
    Σ< (n ∸ m) (λ i → f (m ℕ.+ (n ∸ suc (m ℕ.+ i))))
      ≡⟨⟩
    Σ<range m n (λ i → f (m ℕ.+ (n ∸ suc i))) ∎
    where module ≤R = ℕₚ.≤-Reasoning

  Σ≤range-reverse : ∀ m n f → Σ≤range m n f ≈ Σ≤range m n (λ i → f (m ℕ.+ (n ∸ i)))
  Σ≤range-reverse m n f = Σ<range-reverse m (suc n) f

  Σ<-split-even : ∀ n f →
    Σ< (2 ℕ.* n) f ≈ Σ< n (λ i → f (2 ℕ.* i)) ∙ Σ< n (λ i → f (1 ℕ.+ 2 ℕ.* i))
  Σ<-split-even 0       f = sym $ identityʳ ε
  Σ<-split-even (suc n) f = begin
    Σ< (2 ℕ.* suc n) f
      ≈⟨ Σ<-congʳ f $ ℕₚ.*-distribˡ-+ 2 1 n ⟩
    Σ< (2 ℕ.+ 2 ℕ.* n) f
      ≡⟨⟩
    Σ< (2 ℕ.* n) f ∙ f[2n] ∙ f[1+2n]
      ≈⟨ ∙-congʳ $ ∙-congʳ $ Σ<-split-even n f ⟩
    Σ< n ev ∙ Σ< n od ∙ f[2n] ∙ f[1+2n]
      ≈⟨ assoc (Σ< n ev ∙ Σ< n od) f[2n] f[1+2n] ⟩
    Σ< n ev ∙ Σ< n od ∙ (f[2n] ∙ f[1+2n])
      ≈⟨ lemma (Σ< n ev) (Σ< n od) f[2n] f[1+2n] ⟩
    Σ< (suc n) ev ∙ Σ< (suc n) od
      ∎
      where
      f[2n]   = f (2 ℕ.* n)
      f[1+2n] = f (1 ℕ.+ 2 ℕ.* n)
      ev = λ i → f (2 ℕ.* i)
      od = λ i → f (1 ℕ.+ 2 ℕ.* i)

  Σ<-split-odd : ∀ n f →
    Σ< (1 ℕ.+ 2 ℕ.* n) f ≈ Σ< (suc n) (λ i → f (2 ℕ.* i)) ∙ Σ< n (λ i → f (1 ℕ.+ 2 ℕ.* i))
  Σ<-split-odd n f = begin
    Σ< (2 ℕ.* n) f ∙ f[2n]
      ≈⟨ ∙-congʳ $ Σ<-split-even n f ⟩
    Σ< n ev ∙ Σ< n od ∙ f[2n]
      ≈⟨ trans (assoc (Σ< n ev) (Σ< n od) f[2n]) (∙-congˡ $ comm (Σ< n od) f[2n]) ⟩
    Σ< n ev ∙ (f[2n] ∙ Σ< n od)
      ≈⟨ sym $ assoc (Σ< n ev) f[2n] (Σ< n od) ⟩
    Σ< n ev ∙ f[2n] ∙ Σ< n od
      ∎
    where
    f[2n] = f (2 ℕ.* n)
    ev = λ i → f (2 ℕ.* i)
    od = λ i → f (1 ℕ.+ 2 ℕ.* i)

  -- Σ<-comm-triangle : ∀ n f → Σ n (λ i → Σ< i (λ j → f i j)) ≈

module SemiringSummationProperties {c e} (SR : Semiring c e) where
  open Semiring SR
  open MonoidSummation +-monoid
  open CommutativeMonoidSummationProperties +-commutativeMonoid public
  open SetoidReasoning setoid

  Σ<-*-commute : ∀ n c f → Σ< n (λ k → c * f k) ≈ c * Σ< n f
  Σ<-*-commute ℕ.zero  c f = sym $ zeroʳ c
  Σ<-*-commute (suc n) c f = begin
    Σ< n (λ k → c * f k) + c * f n ≈⟨ +-congʳ $ Σ<-*-commute n c f ⟩
    c * Σ< n f + c * f n           ≈⟨ sym $ distribˡ c (Σ< n f) (f n) ⟩
    c * (Σ< n f + f n)             ∎

  Σ≤-*-commute : ∀ n c f → Σ≤ n (λ k → c * f k) ≈ c * Σ≤ n f
  Σ≤-*-commute n c f = Σ<-*-commute (suc n) c f

  Σ<range-*-commute : ∀ m n c f →
    Σ<range  m n (λ k → c * f k) ≈ c * Σ<range m n f
  Σ<range-*-commute m n c f = Σ<-*-commute (n ∸ m) c (λ k → f (m ℕ.+ k))

  Σ≤range-*-commute : ∀ m n c f →
    Σ≤range m n (λ k → c * f k) ≈ c * Σ≤range m n f
  Σ≤range-*-commute m n c f = Σ<range-*-commute m (suc n) c f

  Σ<-distrib-* : ∀ m n f g →
    Σ< m f * Σ< n g ≈ Σ< m (λ i → Σ< n (λ j → f i * g j))
  Σ<-distrib-* 0       n f g = zeroˡ (Σ< n g)
  Σ<-distrib-* (suc m) n f g = begin
    Σ< (suc m) f * Σ< n g
      ≡⟨⟩
    (Σ< m f + f m) * Σ< n g
      ≈⟨ distribʳ (Σ< n g) (Σ< m f) (f m) ⟩
    Σ< m f * Σ< n g + f m * Σ< n g
      ≈⟨ +-cong (Σ<-distrib-* m n f g) (sym $ Σ<-*-commute n (f m) g) ⟩
    Σ< m (λ i → Σ< n (λ j → f i * g j)) + Σ< n (λ j → f m * g j)
      ≡⟨⟩
    Σ< (suc m) (λ i → Σ< n (λ j → f i * g j))
      ∎

  Σ≤-distrib-* : ∀ m n f g →
    Σ≤ m f * Σ≤ n g ≈ Σ≤ m (λ i → Σ≤ n (λ j → f i * g j))
  Σ≤-distrib-* m n f g = Σ<-distrib-* (suc m) (suc n) f g

  Σ<range-distrib-* : ∀ m n o p f g →
    Σ<range m n f * Σ<range o p g ≈ Σ<range m n (λ i → Σ<range o p (λ j → f i * g j))
  Σ<range-distrib-* m n o p f g =
    Σ<-distrib-* (n ∸ m) (p ∸ o) (λ i → f (m ℕ.+ i)) λ j → g (o ℕ.+ j)

  Σ≤range-distrib-* : ∀ m n o p f g →
    Σ≤range m n f * Σ≤range o p g ≈ Σ≤range m n (λ i → Σ≤range o p (λ j → f i * g j))
  Σ≤range-distrib-* m n o p = Σ<range-distrib-* m (suc n) o (suc p)

module GroupSummationProperties {c e} (G : Group c e) where
  open Group G
  open MonoidSummation monoid
  open MonoidSummationProperties monoid
  open SetoidReasoning setoid

  Σ<-telescope : ∀ n (f : ℕ → Carrier) →
    Σ< n (λ i → f i - f (suc i)) ≈ f 0 - f n
  Σ<-telescope 0       f = sym $ inverseʳ (f 0)
  Σ<-telescope (suc n) f = begin
    Σ< n (λ i → f i - f (suc i)) ∙ (f n - f (suc n))
      ≈⟨ ∙-congʳ $ Σ<-telescope n f ⟩
    (f 0 - f n) ∙ (f n - f (suc n))
      ≈⟨ assoc (f 0) (f n ⁻¹) (f n - f (suc n)) ⟩
    f 0 ∙ (f n ⁻¹ ∙ (f n - f (suc n)))
      ≈⟨ ∙-congˡ $ sym $ assoc (f n ⁻¹) (f n) (f (suc n) ⁻¹) ⟩
    f 0 ∙ ((f n ⁻¹ ∙ f n) - f (suc n))
      ≈⟨ ∙-congˡ $ ∙-congʳ $ inverseˡ (f n) ⟩
    f 0 ∙ (ε - f (suc n))
      ≈⟨ ∙-congˡ $ identityˡ (f (suc n) ⁻¹) ⟩
    f 0 - f (suc n)
      ∎

  Σ≤-telescope : ∀ n (f : ℕ → Carrier) →
    Σ≤ n (λ i → f i - f (suc i)) ≈ f 0 - f (suc n)
  Σ≤-telescope n f = Σ<-telescope (suc n) f

  Σ<range-telescope : ∀ {m n} (f : ℕ → Carrier) → m ≤ n →
    Σ<range m n (λ i → f i - f (suc i)) ≈ f m - f n
  Σ<range-telescope {m} {n} f m≤n = begin
    Σ< (n ∸ m) (λ i → f (m ℕ.+ i) - f (suc (m ℕ.+ i)))
      ≈⟨ Σ<-congˡ (n ∸ m) $ (λ i → ∙-congˡ $ ⁻¹-cong $ reflexive $ ≡.cong f $ ≡.sym $ ℕₚ.+-suc m i) ⟩
    Σ< (n ∸ m) (λ i → f (m ℕ.+ i) - f (m ℕ.+ suc i))
      ≈⟨ Σ<-telescope (n ∸ m) (λ i → f (m ℕ.+ i)) ⟩
    f (m ℕ.+ 0) - f (m ℕ.+ (n ∸ m))
      ≈⟨ ∙-cong (reflexive $ ≡.cong f $ ℕₚ.+-identityʳ m) (⁻¹-cong $ reflexive $ ≡.cong f $ ℕₚ.m+[n∸m]≡n m≤n) ⟩
    f m - f n
      ∎

  Σ≤range-telescope : ∀ {m n} (f : ℕ → Carrier) → m ≤ suc n →
    Σ≤range m n (λ i → f i - f (suc i)) ≈ f m - f (suc n)
  Σ≤range-telescope {m} {n} f m≤1+n = Σ<range-telescope {m} {suc n} f m≤1+n

-- module AbelianGroupSummationProperties
--  Σ<-minus-commute : ∀ n f → Σ< n (λ i → f i ⁻¹) ≈ Σ< n f ⁻¹


text:
-- Andreas, 2013-03-22
module Issue473a where

data D : Set where
  d : D

data P : D → Set where
  p : P d

record Rc : Set where
  constructor c
  field f : D

works : {r : Rc} → P (Rc.f r) → Set
works p = D

works' : (r : Rc) → P (Rc.f r) → Set
works' (c .d) p = D

-- If we remove the constructor, the example fails:

record R : Set where
  field f : D

fails : {r : R} → P (R.f r) → Set
fails p = D

-- d != R.f r of type D
-- when checking that the pattern p has type P (R.f r)

-- The error is justified since there is no pattern we could write down
-- for r.  It would have to look like
--
--   record { f = .d }
--
-- but anonymous record patterns are not supported.

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module Data.List.Relation.Quantification where

import      Lvl
open import Data.List
open import Logic
open import Type

private variable ℓ ℓₑ : Lvl.Level
private variable T A B : Type{ℓ}
private variable l l₁ l₂ : List(T)
private variable x y px py : T
private variable P : T → Stmt{ℓ}

-- TODO: How about this as an alternative definition?
-- module _ (P : T → Type{ℓ}) where
--   open import Type.Dependent
--   open Data.IndexedList(Σ T P){List(T)} using (IndexedList ; intro)
--
--   AllElements : List(T) → Stmt{Lvl.of(T) Lvl.⊔ ℓ}
--   AllElements = IndexedList(intro ∅ ((_⊰_) ∘ Σ.left))
data AllElements (P : T → Stmt{ℓ}) : List(T) → Stmt{Lvl.of(T) Lvl.⊔ ℓ} where
  ∅   : AllElements(P)(∅)
  _⊰_ : P(x) → AllElements(P)(l) → AllElements(P)(x ⊰ l)

data ExistsElement (P : T → Stmt{ℓ}) : List(T) → Stmt{Lvl.of(T) Lvl.⊔ ℓ} where
  •_ : P(x)                → ExistsElement(P)(x ⊰ l)
  ⊰_ : ExistsElement(P)(l) → ExistsElement(P)(x ⊰ l)

-- TODO: Maybe remove this and use AllElements with map₂ instead
data AllElements₂ (P : A → B → Stmt{ℓ}) : List(A) → List(B) → Stmt{Lvl.of(A) Lvl.⊔ Lvl.of(B) Lvl.⊔ ℓ} where
  ∅   : AllElements₂(P)(∅)(∅)
  _⊰_ : P(x)(y) → AllElements₂(P)(l₁)(l₂) → AllElements₂(P)(x ⊰ l₁)(y ⊰ l₂)

∀ₗᵢₛₜ : List(T) → (T → Stmt{ℓ}) → Stmt
∀ₗᵢₛₜ(l) P = AllElements P l

∃ₗᵢₛₜ : List(T) → (T → Stmt{ℓ}) → Stmt
∃ₗᵢₛₜ(l) P = ExistsElement P l

module _ {P : T → Type{ℓ}} where
  open import Logic.Propositional
  open import Structure.Relator.Equivalence
  import      Structure.Relator.Names as Names
  open import Structure.Relator.Properties
  open import Structure.Setoid

  data ExistsElementEquivalence : ExistsElement(P)(l) → ExistsElement(P)(l) → Stmt{Lvl.of(T) Lvl.⊔ ℓ} where
    use  : ExistsElementEquivalence{l = x ⊰ l}(• px)(• py)
    skip : ExistsElementEquivalence(px)(py) → ExistsElementEquivalence{l = x ⊰ l}(⊰ px)(⊰ py)

  instance
    ExistsElementEquivalence-equiv : Equiv(ExistsElement(P)(l))
    Equiv._≡_ ExistsElementEquivalence-equiv = ExistsElementEquivalence
    Equiv.equivalence ExistsElementEquivalence-equiv = intro ⦃ intro refl ⦄ ⦃ intro sym ⦄ ⦃ intro trans ⦄ where
      refl : Names.Reflexivity(ExistsElementEquivalence{l = l})
      refl{x = • _} = use
      refl{x = ⊰ p} = skip(refl{x = p})

      sym : Names.Symmetry(ExistsElementEquivalence{l = l})
      sym {x = • px} {y = • py} use      = use
      sym {x = ⊰ px} {y = ⊰ py} (skip p) = skip(sym{x = px}{y = py} p)

      trans : Names.Transitivity(ExistsElementEquivalence{l = l})
      trans {x = • px} {y = • py} {z = • pz} use      use      = use
      trans {x = ⊰ px} {y = ⊰ py} {z = ⊰ pz} (skip p) (skip q) = skip(trans {x = px} {y = py} {z = pz} p q)

module _ where
  open import Type.Properties.Singleton

  ExistsUniqueElement : (T → Stmt{ℓ}) → List(T) → Stmt
  ExistsUniqueElement P l = IsUnit(ExistsElement(P)(l)) ⦃ ExistsElementEquivalence-equiv ⦄

  ∃!ₗᵢₛₜ : List(T) → (T → Stmt{ℓ}) → Stmt
  ∃!ₗᵢₛₜ(l) P = ExistsUniqueElement P l

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.HalfAdjoint
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Function using (_∘_; id)
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Functions.Embedding
open import Cubical.Data.Sigma

open import Cubical.Algebra
open import Cubical.Algebra.Properties
open import Cubical.Algebra.Semigroup.Morphism

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Pointed

open import Cubical.Algebra.Magma.Properties using (isPropIsMagma)

open import Cubical.Relation.Binary.Reasoning.Equality

open Iso

private
  variable
    ℓ ℓ′ ℓ′′ : Level
    R : Semigroup ℓ
    S : Semigroup ℓ′
    T : Semigroup ℓ′′

isPropIsSemigroupHom : ∀ (S : Semigroup ℓ) (T : Semigroup ℓ′) f → isProp (IsSemigroupHom S T f)
isPropIsSemigroupHom S T f = isPropHomomorphic₂ (Semigroup.is-set T) f (Semigroup._•_ S) (Semigroup._•_ T)

isSetSemigroupHom : isSet (S ⟶ᴴ T)
isSetSemigroupHom {S = S} {T = T} = isOfHLevelRespectEquiv 2 equiv
                                      (isSetΣ (isSetΠ λ _ → is-set T)
                                              (λ f → isProp→isSet (isPropIsSemigroupHom S T f)))
  where
    open Semigroup
    equiv : (Σ[ g ∈ (⟨ S ⟩ → ⟨ T ⟩) ] IsSemigroupHom S T g) ≃ SemigroupHom S T
    equiv = isoToEquiv (iso (λ (g , m) → semigrouphom g m)
                            (λ (semigrouphom g m) → g , m)
                            (λ _ → refl) λ _ → refl)

isSemigroupHomComp : {f : ⟨ R ⟩ → ⟨ S ⟩} {g : ⟨ S ⟩ → ⟨ T ⟩}
                      → IsSemigroupHom R S f → IsSemigroupHom S T g
                      → IsSemigroupHom R T (g ∘ f)
isSemigroupHomComp {g = g} fHom gHom _ _ = cong g (fHom _ _) ∙ gHom _ _

private
  isSemigroupHomComp′ : (f : R ⟶ᴴ S) (g : S ⟶ᴴ T)
                        → IsSemigroupHom R T (SemigroupHom.fun g ∘ SemigroupHom.fun f)
  isSemigroupHomComp′ (semigrouphom f fHom) (semigrouphom g gHom) _ _ =
    cong g (fHom _ _) ∙ gHom _ _

compSemigroupHom : (R ⟶ᴴ S) → (S ⟶ᴴ T) → (R ⟶ᴴ T)
compSemigroupHom f g =
  semigrouphom _ (isSemigroupHomComp′ f g)

compSemigroupEquiv : R ≃ᴴ S → S ≃ᴴ T → R ≃ᴴ T
compSemigroupEquiv f g =
  semigroupequiv (compEquiv f.eq g.eq) (isSemigroupHomComp′ f.hom g.hom)
  where
    module f = SemigroupEquiv f
    module g = SemigroupEquiv g

isSemigroupHomId : (S : Semigroup ℓ) → IsSemigroupHom S S id
isSemigroupHomId S _ _ = refl

idSemigroupHom : (S : Semigroup ℓ) → (S ⟶ᴴ S)
idSemigroupHom S = record
  { fun   = id
  ; isHom = isSemigroupHomId S
  }

idSemigroupEquiv : (S : Semigroup ℓ) → S ≃ᴴ S
idSemigroupEquiv S = record
  { eq    = idEquiv ⟨ S ⟩
  ; isHom = isSemigroupHomId S
  }

-- Isomorphism inversion
isSemigroupHomInv : (eqv : S ≃ᴴ T) → IsSemigroupHom T S (invEq (SemigroupEquiv.eq eqv))
isSemigroupHomInv {S = S} {T = T} (semigroupequiv eq isHom) x y = isInj-f _ _ (
  f (f⁻¹ (x •ᵀ y))       ≡⟨ retEq eq _ ⟩
  x •ᵀ y                 ≡˘⟨ cong₂ _•ᵀ_ (retEq eq x) (retEq eq y) ⟩
  f (f⁻¹ x) •ᵀ f (f⁻¹ y) ≡˘⟨ isHom (f⁻¹ x) (f⁻¹ y) ⟩
  f (f⁻¹ x • f⁻¹ y)      ∎)
  where
    _•_ = Semigroup._•_ S -- superscript S isn't available for some reason
    _•ᵀ_ = Semigroup._•_ T
    f = equivFun eq
    f⁻¹ = invEq eq
    isInj-f : (x y : ⟨ S ⟩) → f x ≡ f y → x ≡ y
    isInj-f x y = invEq (_ , isEquiv→isEmbedding (eq .snd) x y)

invSemigroupHom : S ≃ᴴ T → (T ⟶ᴴ S)
invSemigroupHom eq = record { isHom = isSemigroupHomInv eq }

invSemigroupEquiv : S ≃ᴴ T → T ≃ᴴ S
invSemigroupEquiv eq = record
  { eq    = invEquiv (SemigroupEquiv.eq eq)
  ; isHom = isSemigroupHomInv eq
  }

semigroupHomEq : {f g : S ⟶ᴴ T} → (SemigroupHom.fun f ≡ SemigroupHom.fun g) → f ≡ g
semigroupHomEq {S = S} {T = T} {semigrouphom f fm} {semigrouphom g gm} p i =
  semigrouphom (p i) (p-hom i)
  where
    p-hom : PathP (λ i → IsSemigroupHom S T (p i)) fm gm
    p-hom = toPathP (isPropIsSemigroupHom S T _ _ _)

semigroupEquivEq : {f g : S ≃ᴴ T} → (SemigroupEquiv.eq f ≡ SemigroupEquiv.eq g) → f ≡ g
semigroupEquivEq {S = S} {T = T} {semigroupequiv f fm} {semigroupequiv g gm} p i =
  semigroupequiv (p i) (p-hom i)
  where
    p-hom : PathP (λ i → IsSemigroupHom S T (p i .fst)) fm gm
    p-hom = toPathP (isPropIsSemigroupHom S T _ _ _)

module SemigroupΣTheory {ℓ} where

  RawSemigroupStructure : Type ℓ → Type ℓ
  RawSemigroupStructure X = X → X → X

  RawSemigroupEquivStr = AutoEquivStr RawSemigroupStructure

  rawSemigroupUnivalentStr : UnivalentStr _ RawSemigroupEquivStr
  rawSemigroupUnivalentStr = autoUnivalentStr RawSemigroupStructure

  SemigroupAxioms : (A : Type ℓ) → RawSemigroupStructure A → Type ℓ
  SemigroupAxioms A _•_ = IsMagma A _•_ × Associative _•_

  SemigroupStructure : Type ℓ → Type ℓ
  SemigroupStructure = AxiomsStructure RawSemigroupStructure SemigroupAxioms

  SemigroupΣ : Type (ℓ-suc ℓ)
  SemigroupΣ = TypeWithStr ℓ SemigroupStructure

  isPropSemigroupAxioms : (A : Type ℓ) (_•_ : RawSemigroupStructure A) →
                          isProp (SemigroupAxioms A _•_)
  isPropSemigroupAxioms A _•_ = isPropΣ isPropIsMagma λ isMagmaA → isPropAssociative (IsMagma.is-set isMagmaA) _•_

  SemigroupEquivStr : StrEquiv SemigroupStructure ℓ
  SemigroupEquivStr = AxiomsEquivStr RawSemigroupEquivStr SemigroupAxioms

  SemigroupAxiomsIsoIsSemigroup : {A : Type ℓ} {_•_ : RawSemigroupStructure A} →
                                  Iso (SemigroupAxioms A _•_) (IsSemigroup A _•_)
  fun SemigroupAxiomsIsoIsSemigroup (x , y)           = issemigroup x y
  inv SemigroupAxiomsIsoIsSemigroup (issemigroup x y) = (x , y)
  rightInv SemigroupAxiomsIsoIsSemigroup _            = refl
  leftInv SemigroupAxiomsIsoIsSemigroup _             = refl

  SemigroupAxioms≡IsSemigroup : {A : Type ℓ} {_•_ : RawSemigroupStructure A} →
                                SemigroupAxioms _ _•_ ≡ IsSemigroup A _•_
  SemigroupAxioms≡IsSemigroup = isoToPath SemigroupAxiomsIsoIsSemigroup

  Semigroup→SemigroupΣ : Semigroup ℓ → SemigroupΣ
  Semigroup→SemigroupΣ (mksemigroup A _•_ isSemigroupA) =
    A , _•_ , SemigroupAxiomsIsoIsSemigroup .inv isSemigroupA

  SemigroupΣ→Semigroup : SemigroupΣ → Semigroup ℓ
  SemigroupΣ→Semigroup (A , _•_ , isSemigroupA) =
    mksemigroup A _•_ (SemigroupAxiomsIsoIsSemigroup .fun isSemigroupA)

  SemigroupIsoSemigroupΣ : Iso (Semigroup ℓ) SemigroupΣ
  SemigroupIsoSemigroupΣ =
    iso Semigroup→SemigroupΣ SemigroupΣ→Semigroup (λ _ → refl) (λ _ → refl)

  semigroupUnivalentStr : UnivalentStr SemigroupStructure SemigroupEquivStr
  semigroupUnivalentStr = axiomsUnivalentStr _ isPropSemigroupAxioms rawSemigroupUnivalentStr

  SemigroupΣPath : (S T : SemigroupΣ) → (S ≃[ SemigroupEquivStr ] T) ≃ (S ≡ T)
  SemigroupΣPath = SIP semigroupUnivalentStr

  SemigroupEquivΣ : (S T : Semigroup ℓ) → Type ℓ
  SemigroupEquivΣ S T = Semigroup→SemigroupΣ S ≃[ SemigroupEquivStr ] Semigroup→SemigroupΣ T

  SemigroupIsoΣPath : {S T : Semigroup ℓ} → Iso (SemigroupEquiv S T) (SemigroupEquivΣ S T)
  fun SemigroupIsoΣPath (semigroupequiv e h) = (e , h)
  inv SemigroupIsoΣPath (e , h)            = semigroupequiv e h
  rightInv SemigroupIsoΣPath _             = refl
  leftInv SemigroupIsoΣPath _              = refl

  SemigroupPath : (S T : Semigroup ℓ) → (SemigroupEquiv S T) ≃ (S ≡ T)
  SemigroupPath S T =
    SemigroupEquiv S T                                ≃⟨ isoToEquiv SemigroupIsoΣPath ⟩
    SemigroupEquivΣ S T                               ≃⟨ SemigroupΣPath _ _ ⟩
    Semigroup→SemigroupΣ S ≡ Semigroup→SemigroupΣ T   ≃⟨ isoToEquiv (invIso (congIso SemigroupIsoSemigroupΣ)) ⟩
    S ≡ T                                             ■

  RawSemigroupΣ : Type (ℓ-suc ℓ)
  RawSemigroupΣ = TypeWithStr ℓ RawSemigroupStructure

  Semigroup→RawSemigroupΣ : Semigroup ℓ → RawSemigroupΣ
  Semigroup→RawSemigroupΣ S = (⟨ S ⟩ , Semigroup._•_ S)

  InducedSemigroup : (S : Semigroup ℓ) (T : RawSemigroupΣ) (e : ⟨ S ⟩ ≃ ⟨ T ⟩) →
                      RawSemigroupEquivStr (Semigroup→RawSemigroupΣ S) T e → Semigroup ℓ
  InducedSemigroup S T e r =
    SemigroupΣ→Semigroup (inducedStructure rawSemigroupUnivalentStr (Semigroup→SemigroupΣ S) T (e , r))

  InducedSemigroupPath : (S : Semigroup ℓ) (T : RawSemigroupΣ) (e : ⟨ S ⟩ ≃ ⟨ T ⟩)
                          (E : RawSemigroupEquivStr (Semigroup→RawSemigroupΣ S) T e) →
                          S ≡ InducedSemigroup S T e E
  InducedSemigroupPath S T e E =
    SemigroupPath S (InducedSemigroup S T e E) .fst (semigroupequiv e E)

-- We now extract the important results from the above module

open SemigroupΣTheory public using (InducedSemigroup; InducedSemigroupPath)

SemigroupPath : (S ≃ᴴ T) ≃ (S ≡ T)
SemigroupPath = SemigroupΣTheory.SemigroupPath _ _

isPropIsSemigroup : {A : Type ℓ} {_•_ : Op₂ A} → isProp (IsSemigroup A _•_)
isPropIsSemigroup =
  subst isProp SemigroupΣTheory.SemigroupAxioms≡IsSemigroup
        (SemigroupΣTheory.isPropSemigroupAxioms _ _)

open Semigroup

uaSemigroup : S ≃ᴴ T → S ≡ T
uaSemigroup = equivFun SemigroupPath

carac-uaSemigroup : {S T : Semigroup ℓ} (f : S ≃ᴴ T)
                    → cong Carrier (uaSemigroup f) ≡ ua (SemigroupEquiv.eq f)
carac-uaSemigroup (semigroupequiv f m) =
  (refl ∙∙ ua f ∙∙ refl)
    ≡˘⟨ rUnit (ua f) ⟩
  ua f ∎

Semigroup≡ : (S T : Semigroup ℓ) → (
  Σ[ p ∈ ⟨ S ⟩ ≡ ⟨ T ⟩ ]
  Σ[ q ∈ PathP (λ i → p i → p i → p i) (_•_ S) (_•_ T) ]
  PathP (λ i → IsSemigroup (p i) (q i)) (isSemigroup S) (isSemigroup T))
  ≃ (S ≡ T)
Semigroup≡ S T = isoToEquiv (iso
  (λ (p , q , r) i → mksemigroup (p i) (q i) (r i))
  (λ p → cong Carrier p , cong _•_ p , cong isSemigroup p)
  (λ _ → refl) (λ _ → refl))

caracSemigroup≡ : {S T : Semigroup ℓ} (p q : S ≡ T) → cong Carrier p ≡ cong Carrier q → p ≡ q
caracSemigroup≡ {S = S} {T} p q t = cong (fst (Semigroup≡ S T)) (Σ≡Prop (λ _ →
    isPropΣ
    (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set T) _ _) λ _ →
    isOfHLevelPathP 1 isPropIsSemigroup _ _)
  t)

uaSemigroupId : (S : Semigroup ℓ) → uaSemigroup (idSemigroupEquiv S) ≡ refl
uaSemigroupId S = caracSemigroup≡ _ _ (carac-uaSemigroup (idSemigroupEquiv S) ∙ uaIdEquiv)

uaCompSemigroupEquiv : {R S T : Semigroup ℓ} (f : R ≃ᴴ S) (g : S ≃ᴴ T)
                        → uaSemigroup (compSemigroupEquiv f g) ≡ uaSemigroup f ∙ uaSemigroup g
uaCompSemigroupEquiv f g = caracSemigroup≡ _ _ (
  cong Carrier (uaSemigroup (compSemigroupEquiv f g))
    ≡⟨ carac-uaSemigroup (compSemigroupEquiv f g) ⟩
  ua (eq (compSemigroupEquiv f g))
    ≡⟨ uaCompEquiv _ _ ⟩
  ua (eq f) ∙ ua (eq g)
    ≡˘⟨ cong (_∙ ua (eq g)) (carac-uaSemigroup f) ⟩
  cong Carrier (uaSemigroup f) ∙ ua (eq g)
    ≡˘⟨ cong (cong Carrier (uaSemigroup f) ∙_) (carac-uaSemigroup g) ⟩
  cong Carrier (uaSemigroup f) ∙ cong Carrier (uaSemigroup g)
    ≡˘⟨ cong-∙ Carrier (uaSemigroup f) (uaSemigroup g) ⟩
  cong Carrier (uaSemigroup f ∙ uaSemigroup g) ∎)
  where open SemigroupEquiv


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Unary.Any.Properties directly.
------------------------------------------------------------------------

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

module Data.List.Any.Properties where

open import Data.List.Relation.Unary.Any.Properties public

{-# WARNING_ON_IMPORT
"Data.List.Any.Properties was deprecated in v1.0.
Use Data.List.Relation.Unary.Any.Properties instead."
#-}


text:
module Thesis.ANormalDTerm where

open import Thesis.ANormal public
open import Thesis.Changes public
open import Thesis.LangChanges public

ΔΔ : Context → Context
ΔΔ ∅ = ∅
ΔΔ (τ • Γ) = Δt τ • ΔΔ Γ

-- Because the standard name is so irregular.
Δτ = Δt

ChΔ : ∀ (Δ : Context) → Set
ChΔ Δ = ⟦ ΔΔ Δ ⟧Context

-- [_]Δ_from_to_ : ∀ Δ → ChΔ Δ → (ρ1 ρ2 : ⟦ Δ ⟧Context) → Set
-- [ ∅ ]Δ ∅ from ∅ to ∅ = ⊤
-- [ τ • Δ ]Δ dv • dρ from v1 • ρ1 to (v2 • ρ2) = [ τ ]τ dv from v1 to v2 × [ Δ ]Δ dρ from ρ1 to ρ2

data [_]Δ_from_to_ : ∀ Δ → ChΔ Δ → (ρ1 ρ2 : ⟦ Δ ⟧Context) → Set where
  v∅ : [ ∅ ]Δ ∅ from ∅ to ∅
  _v•_ : ∀ {τ Δ dv v1 v2 dρ ρ1 ρ2} →
    (dvv : [ τ ]τ dv from v1 to v2) →
    (dρρ : [ Δ ]Δ dρ from ρ1 to ρ2) →
    [ τ • Δ ]Δ (dv • dρ) from (v1 • ρ1) to (v2 • ρ2)

derive-dvar : ∀ {Δ σ} → (x : Var Δ σ) → Var (ΔΔ Δ) (Δτ σ)
derive-dvar this = this
derive-dvar (that x) = that (derive-dvar x)

fromtoDeriveDVar : ∀ {Δ τ} → (x : Var Δ τ) →
  ∀ {dρ ρ1 ρ2} → [ Δ ]Δ dρ from ρ1 to ρ2 →
  [ τ ]τ (⟦ derive-dvar x ⟧Var dρ) from (⟦ x ⟧Var ρ1) to (⟦ x ⟧Var ρ2)
fromtoDeriveDVar this (dvv v• dρρ) = dvv
fromtoDeriveDVar (that x) (dvv v• dρρ) = fromtoDeriveDVar x dρρ

-- A DTerm evaluates in normal context Δ, change context (ΔΔ Δ), and produces
-- a result of type (Δt τ).
data DTerm : (Δ : Context) (τ : Type) → Set where
  dvar : ∀ {Δ τ} (x : Var (ΔΔ Δ) (Δt τ)) →
    DTerm Δ τ
  dlett : ∀ {Δ τ σ τ₁} →
    (f : Var Δ (σ ⇒ τ₁)) →
    (x : Var Δ σ) →
    (t : Term (τ₁ • Δ) τ) →
    (df : Var (ΔΔ Δ) (Δτ (σ ⇒ τ₁))) →
    (dx : Var (ΔΔ Δ) (Δτ σ)) →
    (dt : DTerm (τ₁ • Δ) τ) →
    DTerm Δ τ

data DFun (Δ : Context) : (τ : Type) → Set where
  dterm : ∀ {τ} → DTerm Δ τ → DFun Δ τ
  dabs : ∀ {σ τ} → DFun (σ • Δ) τ → DFun Δ (σ ⇒ τ)

derive-dterm : ∀ {Δ σ} → (t : Term Δ σ) → DTerm Δ σ
derive-dterm (var x) = dvar (derive-dvar x)
derive-dterm (lett f x t) =
  dlett f x t (derive-dvar f) (derive-dvar x) (derive-dterm t)

⟦_⟧DTerm : ∀ {Δ τ} → DTerm Δ τ → ⟦ Δ ⟧Context → ⟦ ΔΔ Δ ⟧Context → ⟦ Δt τ ⟧Type
⟦ dvar x ⟧DTerm ρ dρ = ⟦ x ⟧Var dρ
⟦ dlett f x t df dx dt ⟧DTerm ρ dρ =
  let v = (⟦ x ⟧Var ρ)
  in
    ⟦ dt ⟧DTerm
      (⟦ f ⟧Var ρ v • ρ)
      (⟦ df ⟧Var dρ v (⟦ dx ⟧Var dρ) • dρ)

fromtoDeriveDTerm : ∀ {Δ τ} → (t : Term Δ τ) →
  ∀ {dρ ρ1 ρ2} → [ Δ ]Δ dρ from ρ1 to ρ2 →
  [ τ ]τ (⟦ derive-dterm t ⟧DTerm ρ1 dρ) from (⟦ t ⟧Term ρ1) to (⟦ t ⟧Term ρ2)
fromtoDeriveDTerm (var x) dρρ = fromtoDeriveDVar x dρρ
fromtoDeriveDTerm (lett f x t) dρρ =
  let fromToF = fromtoDeriveDVar f dρρ
      fromToX = fromtoDeriveDVar x dρρ
      fromToFX = fromToF _ _ _ fromToX
  in fromtoDeriveDTerm t (fromToFX v• dρρ)

derive-dfun : ∀ {Δ σ} → (t : Fun Δ σ) → DFun Δ σ
derive-dfun (term t) = dterm (derive-dterm t)
derive-dfun (abs f) = dabs (derive-dfun f)

⟦_⟧DFun : ∀ {Δ τ} → DFun Δ τ → ⟦ Δ ⟧Context → ⟦ ΔΔ Δ ⟧Context → ⟦ Δt τ ⟧Type
⟦ dterm t ⟧DFun = ⟦ t ⟧DTerm
⟦ dabs df ⟧DFun ρ dρ = λ v dv → ⟦ df ⟧DFun (v • ρ) (dv • dρ)

fromtoDeriveDFun : ∀ {Δ τ} → (f : Fun Δ τ) →
  ∀ {dρ ρ1 ρ2} → [ Δ ]Δ dρ from ρ1 to ρ2 →
  [ τ ]τ (⟦ derive-dfun f ⟧DFun ρ1 dρ) from (⟦ f ⟧Fun ρ1) to (⟦ f ⟧Fun ρ2)
fromtoDeriveDFun (term t) = fromtoDeriveDTerm t
fromtoDeriveDFun (abs f) dρρ = λ dv v1 v2 dvv → fromtoDeriveDFun f (dvv v• dρρ)

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module _ where

postulate
  A B C D E F : Set
  a : A
  b : B
  c : C
  d : D
  e : E
  f : F
  T : {A : Set} → A → Set

module M1 (a : A) where
  module M2 (b : B) where
    postulate g : T a → T b
    module M3 (c : C) where
      postulate h : T a → T b → T c
  module M4 (d : D) where
    module M5 (e : E) (f : F) where
      open M2 public
      open M2.M3 public
      open M3 public renaming (h to h')

module M  = M1.M4 a d
module M' = M.M5 e f

M'g : (x : B) → T a → T x
M'g = M'.g

M'M3h M'h M'h' : (x : B) (y : C) → T a → T x → T y
M'M3h = M'.M3.h
M'h = M'.h
M'h' = M'.h'

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Identity
open import HoTT.Homotopy

module HoTT.Equivalence where

open variables
private variable C : 𝒰 i

module _ (f : A → B) where
  qinv = Σ[ g ∶ (B → A) ] (g ∘ f ~ id) × (f ∘ g ~ id)

  -- Bi-invertible map
  linv = Σ[ g ∶ (B → A) ] g ∘ f ~ id
  rinv = Σ[ g ∶ (B → A) ] f ∘ g ~ id
  -- The book uses a flipped version rinv × linv for the definition in §2.4.
  biinv = linv × rinv

  -- Half-adjoint equivalence
  ishae = Σ[ g ∶ (B → A) ] Σ[ η ∶ g ∘ f ~ id ] Σ[ ε ∶ f ∘ g ~ id ] ap f ∘ η ~ ε ∘ f

module _ {f : A → B} where
  module qinv (e : qinv f) where
    g = pr₁ e
    η = pr₁ (pr₂ e)
    ε = pr₂ (pr₂ e)

  qinv→linv : qinv f → linv f
  qinv→linv e = g , η
    where open qinv e

  qinv→rinv : qinv f → rinv f
  qinv→rinv e = g , ε
    where open qinv e

  module ishae (e : ishae f) where
    g = pr₁ e
    η = pr₁ (pr₂ e)
    ε = pr₁ (pr₂ (pr₂ e))
    τ = pr₂ (pr₂ (pr₂ e))

  ishae→qinv : ishae f → qinv f
  ishae→qinv e = g , η , ε
    where open ishae e

  qinv→ishae : qinv f → ishae f
  qinv→ishae e = g , η , ε' , τ
    where
    open qinv e
    ε' : f ∘ g ~ id
    ε' b = ε (f (g b)) ⁻¹ ∙ (ap f (η (g b)) ∙ ε b)
    τ : ap f ∘ η ~ ε' ∘ f
    τ a =
      ap f (η a)                        =⟨ unitₗ ⟩
      refl ∙ ap f (η a)                 =⟨ invₗ ⁻¹ ∙ᵣ _ ⟩
      _ ∙ ε (f (g (f a))) ∙ ap f (η a)  =⟨ assoc ⁻¹ ⟩
      _ ∙ (_ ∙ ap f (η a))              =⟨ _ ∙ₗ (_ ∙ₗ ap-id (ap f (η a)) ⁻¹) ⟩
      _ ∙ (ε (f (g (f a))) ∙ ap id _)   =⟨ _ ∙ₗ ~-natural ε (ap f (η a)) ⟩
      _ ∙ (ap (f ∘ g) (ap f (η a)) ∙ _) =⟨ _ ∙ₗ (ap-∘ (f ∘ g) f (η a) ⁻¹ ∙ᵣ _) ⟩
      _ ∙ (ap (f ∘ g ∘ f) (η a) ∙ _)    =⟨ _ ∙ₗ (ap-∘ f (g ∘ f) (η a) ∙ᵣ _) ⟩
      _ ∙ (ap f (ap (g ∘ f) (η a)) ∙ _) =⟨ _ ∙ₗ (ap (ap f) (~-natural-comm η a ⁻¹) ∙ᵣ _) ⟩
      ε' (f a)                          ∎
      where open =-Reasoning

  module biinv (e : biinv f) where
    h = pr₁ (pr₁ e)
    β = pr₂ (pr₁ e)
    g = pr₁ (pr₂ e)
    α = pr₂ (pr₂ e)

  biinv→qinv : biinv f → qinv f
  biinv→qinv e = g , β' , α
    where
    open biinv e
    γ : g ~ h
    γ x = β (g x) ⁻¹ ∙ ap h (α x)
    β' : g ∘ f ~ id
    β' x = γ (f x) ∙ β x

  qinv→biinv : qinv f → biinv f
  qinv→biinv e = (g , η) , (g , ε)
    where open qinv e

module _ {f₁ : B → C} {f₂ : A → B} where
  ishae-∘ : ishae f₁ → ishae f₂ → ishae (f₁ ∘ f₂)
  ishae-∘ e₁ e₂ = g , η , ε , τ
    where
    open ishae e₁ renaming (g to g₁ ; η to η₁ ; ε to ε₁ ; τ to τ₁)
    open ishae e₂ renaming (g to g₂ ; η to η₂ ; ε to ε₂ ; τ to τ₂)
    f = f₁ ∘ f₂
    g = g₂ ∘ g₁
    η : g ∘ f ~ id
    η x = ap g₂ (η₁ (f₂ x)) ∙ η₂ x
    ε : f ∘ g ~ id
    ε x = ap f₁ (ε₂ (g₁ x)) ∙ ε₁ x
    τ : ap f ∘ η ~ ε ∘ f
    τ x =
      ap f (η x)                                       =⟨ ap-∘ f₁ f₂ (ap g₂ (η₁ (f₂ x)) ∙ η₂ x) ⟩
      ap f₁ (ap f₂ (η x))                              =⟨ ap (ap f₁) (ap-∙ f₂ (ap g₂ (η₁ (f₂ x))) (η₂ x)) ⟩
      ap f₁ (ap f₂ (ap g₂ (η₁ (f₂ x))) ∙ ap f₂ (η₂ x)) =⟨ ap (ap f₁) (ap f₂ _ ∙ₗ τ₂ x) ⟩
      ap f₁ (ap f₂ (ap g₂ (η₁ (f₂ x))) ∙ ε₂ (f₂ x))    =⟨ ap (ap f₁) (ap-∘ f₂ g₂ _ ⁻¹ ∙ᵣ ε₂ (f₂ x)) ⟩
      ap f₁ (ap (f₂ ∘ g₂) (η₁ (f₂ x)) ∙ ε₂ (f₂ x))     =⟨ ap (ap f₁) (~-natural ε₂ (η₁ (f₂ x))) ⁻¹ ⟩
      ap f₁ (ε₂ (g₁ (f x)) ∙ ap id (η₁ (f₂ x)))        =⟨ ap (ap f₁) (ε₂ (g₁ (f x)) ∙ₗ ap-id (η₁ (f₂ x))) ⟩
      ap f₁ (ε₂ (g₁ (f x)) ∙ η₁ (f₂ x))                =⟨ ap-∙ f₁ (ε₂ (g₁ (f x))) (η₁ (f₂ x)) ⟩
      ap f₁ (ε₂ (g₁ (f x))) ∙ ap f₁ (η₁ (f₂ x))        =⟨ _ ∙ₗ τ₁ (f₂ x) ⟩
      ε (f x)                                          ∎
      where open =-Reasoning

  biinv-∘ : biinv f₁ → biinv f₂ → biinv (f₁ ∘ f₂)
  biinv-∘ e₁ e₂ = (h , β) , (g , α)
    where
    open biinv e₁ renaming (h to h₁ ; β to β₁ ; g to g₁ ; α to α₁)
    open biinv e₂ renaming (h to h₂ ; β to β₂ ; g to g₂ ; α to α₂)
    f = f₁ ∘ f₂
    h = h₂ ∘ h₁
    β : h ∘ f ~ id
    β x = ap h₂ (β₁ (f₂ x)) ∙ β₂ x
    g = g₂ ∘ g₁
    α : f ∘ g ~ id
    α x = ap f₁ (α₂ (g₁ x)) ∙ α₁ x

-- Choose isequiv :≡ biinv since it is quicker to compute.
isequiv = biinv
qinv→isequiv = qinv→biinv
isequiv→qinv = biinv→qinv
isequiv-∘ = biinv-∘

_≃_ : 𝒰 i → 𝒰 j → 𝒰 (i ⊔ j)
A ≃ B = Σ (A → B) isequiv
infixr 5 _≃_

record Iso (A : 𝒰 i) (B : 𝒰 j) : 𝒰 (i ⊔ j) where
  field
    f : A → B
    g : B → A
    η : g ∘ f ~ id
    ε : f ∘ g ~ id

iso→eqv : Iso A B → A ≃ B
iso→eqv iso = f , qinv→isequiv (g , η , ε)
  where open Iso iso

eqv→iso : A ≃ B → Iso A B
eqv→iso e = record { f = pr₁ e ; g = g ; η = η ; ε = ε }
  where open qinv (isequiv→qinv (pr₂ e))

module Eqv {i} {j} {A : 𝒰 i} {B : 𝒰 j} (e : A ≃ B) = Iso (eqv→iso e)

-- Lemma 2.4.12
--  (i)
reflₑ : A ≃ A
reflₑ = id , qinv→isequiv (id , (λ _ → refl) , (λ _ → refl))

--  (ii)
_⁻¹ₑ : A ≃ B → B ≃ A
e ⁻¹ₑ = g , qinv→isequiv (pr₁ e , ε , η)
  where
  open qinv (isequiv→qinv (pr₂ e))
infix 30 _⁻¹ₑ

--  (iii)
_∙ₑ_ : A ≃ B → B ≃ C → A ≃ C
e₁ ∙ₑ e₂ = pr₁ e₂ ∘ pr₁ e₁ , isequiv-∘ (pr₂ e₂) (pr₂ e₁)
infixl 20 _∙ₑ_

idtoeqv : A == B → A ≃ B
idtoeqv p = transport id p , e
  where
  e : isequiv (transport id p)
  e rewrite p = pr₂ reflₑ

module ≃-Reasoning
  where
  _≃⟨_⟩_ : (A : 𝒰 i) → A ≃ B → B ≃ C → A ≃ C
  x ≃⟨ e₁ ⟩ e₂ = e₁ ∙ₑ e₂
  infixr 2 _≃⟨_⟩_

  _∎ : (A : 𝒰 i) → A ≃ A
  _ ∎ = reflₑ
  infix 3 _∎

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


text:
module CTL.Modalities.EU where

-- TODO

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


text:
module BBHeap.Last {A : Set}(_≤_ : A → A → Set) where

open import BBHeap _≤_
open import BBHeap.Compound _≤_
open import BBHeap.DropLast _≤_
open import Bound.Lower A
open import Data.Sum

last : {b : Bound}(h : BBHeap b) → Compound h → A
last (left {b} {x} {l} {r} b≤x l⋘r) (cl .b≤x .l⋘r)
    with l | r | l⋘r | lemma-dropLast⋘ l⋘r
... | leaf | leaf | lf⋘ | _ = x
... | left x≤y₁ l₁⋘r₁ | left x≤y₂ l₂⋘r₂ | ll⋘ .x≤y₁ .x≤y₂ .l₁⋘r₁ .l₂⋘r₂ l₂≃r₂ r₁≃l₂ | inj₁ l≃r = last (left x≤y₂ l₂⋘r₂) (cl x≤y₂ l₂⋘r₂)
... | left x≤y₁ l₁⋘r₁ | left x≤y₂ l₂⋘r₂ | ll⋘ .x≤y₁ .x≤y₂ .l₁⋘r₁ .l₂⋘r₂ l₂≃r₂ r₁≃l₂ | inj₂ dl⋘r = last (left x≤y₁ l₁⋘r₁) (cl x≤y₁ l₁⋘r₁)
... | right x≤y₁ l₁⋙r₁ | left x≤y₂ l₂⋘r₂ | lr⋘ .x≤y₁ .x≤y₂ .l₁⋙r₁ .l₂⋘r₂ l₂≃r₂ l₁⋗l₂ | inj₁ ()
... | right x≤y₁ l₁⋙r₁ | left x≤y₂ l₂⋘r₂ | lr⋘ .x≤y₁ .x≤y₂ .l₁⋙r₁ .l₂⋘r₂ l₂≃r₂ l₁⋗l₂ | inj₂ dl⋘r = last (right x≤y₁ l₁⋙r₁) (cr x≤y₁ l₁⋙r₁)
last (right {b} {x} {l} {r} b≤x l⋙r) (cr .b≤x .l⋙r)
    with l | r | l⋙r | lemma-dropLast⋙ l⋙r
... | left x≤y lf⋘ | leaf | ⋙lf {x = y} .x≤y | _ = y
... | left x≤y₁ l₁⋘r₁ | left x≤y₂ l₂⋘r₂ | ⋙rl .x≤y₁ .x≤y₂ .l₁⋘r₁ l₁≃r₁ .l₂⋘r₂ l₁⋗r₂ | inj₁ l⋗r = last (left x≤y₁ l₁⋘r₁) (cl x≤y₁ l₁⋘r₁)
... | left x≤y₁ l₁⋘r₁ | left x≤y₂ l₂⋘r₂ | ⋙rl .x≤y₁ .x≤y₂ .l₁⋘r₁ l₁≃r₁ .l₂⋘r₂ l₁⋗r₂ | inj₂ l⋙dr = last (left x≤y₂ l₂⋘r₂) (cl x≤y₂ l₂⋘r₂)
... | left x≤y₁ l₁⋘r₁ | right x≤y₂ l₂⋙r₂ | ⋙rr .x≤y₁ .x≤y₂ .l₁⋘r₁ l₁≃r₁ .l₂⋙r₂ l₁≃l₂ | inj₁ ()
... | left x≤y₁ l₁⋘r₁ | right x≤y₂ l₂⋙r₂ | ⋙rr .x≤y₁ .x≤y₂ .l₁⋘r₁ l₁≃r₁ .l₂⋙r₂ l₁≃l₂ | inj₂ l⋙dr = last (right x≤y₂ l₂⋙r₂) (cr x≤y₂ l₂⋙r₂)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Categories.Functor.Discrete where

open import Categories.Category
open import Categories.Functor
open import Categories.Agda
open import Categories.Categories
open import Categories.Support.PropositionalEquality
import Categories.Discrete as D

Discrete : ∀ {o} -> Functor (Sets o) (Categories o o _)
Discrete {o} = record {
             F₀ = D.Discrete;
             F₁ = F₁;
             identity = λ f → Heterogeneous.≡⇒∼ _;
             homomorphism = λ f → Heterogeneous.≡⇒∼ _;
             F-resp-≡ = F-resp-≡}
  where
    F₁ : {A B : Category.Obj (Sets o)} → Sets o [ A , B ] →
                        Categories o o _ [ D.Discrete A , D.Discrete B ]
    F₁ f = record {
             F₀ = f;
             F₁ = ≣-cong f;
             identity = _;
             homomorphism = _;
             F-resp-≡ = _ }

    F-resp-≡ : {A B : Set o} {F G : Sets o [ A , B ]} →
                  Sets o [ F ≡ G ] → Categories o o _ [ F₁ F ≡ F₁ G ]
    F-resp-≡ F≡G {a} ≣-refl rewrite F≡G {a} = Heterogeneous.≡⇒∼ _

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


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

module Cubical.Data.Queue where

open import Cubical.Data.Queue.Base public


text:
open import OutsideIn.Prelude
open import OutsideIn.X
module OutsideIn.Proof.Soundness(x : X) where
  open import Data.Vec hiding (map; _>>=_)

  open X(x)
  import OutsideIn.Environments as EV
  import OutsideIn.Expressions as E
  import OutsideIn.TypeSchema as TS
  import OutsideIn.TopLevel as TL
  import OutsideIn.Constraints as CN
  import OutsideIn.Inference as I
  import OutsideIn.Inference.Separator as S
  import OutsideIn.Inference.Prenexer as P
  import OutsideIn.Inference.ConstraintGen as CG
  import OutsideIn.Inference.Solver as SL
  open EV(x)
  open E(x)
  open CN(x)
  open TS(x)
  open TL(x)
  open I(x)
  open CG(x)
  open S(x)
  open SL(x)
  open P(x)
  open import Relation.Binary.PropositionalEquality renaming ([_] to inspectC)
  module Ax-f = Functor(axiomscheme-is-functor)
  module QC-f = Functor(qconstraint-is-functor)
  module Exp-f {r}{s} = Functor(expression-is-functor₂ {r}{s})
  module TS-f {n} = Functor(type-schema-is-functor {n})
  module pn-m {n} = Monad(PlusN-is-monad{n})
  module Vec-f {n} = Functor(vec-is-functor {n})

  open Monad(type-is-monad)
  open Functor(is-functor)

  type-substitute : ∀{a b} → (a → Type b) → Type a → Type b
  type-substitute f t = (join ∘ map f) t

  applyAll : ∀{tv}(n : ℕ) → Type tv → Type (tv ⨁ n)
  applyAll zero x = x
  applyAll (suc n) x = applyAll n (appType (map suc x) (unit zero))

  constraint-substitute : ∀{a b} → (a → Type b) → QConstraint a → QConstraint b
  constraint-substitute f t = constraint-types (type-substitute f) t

  mutual
    data _,_,_⊢_∶_ {ev tv : Set}(Q : AxiomScheme tv)(Qg : QConstraint tv)(Γ : Environment ev tv): {r : Shape} → Expression ev tv r →  Type tv → Set where
      TyEq : ∀ {τ₁ τ₂}{r}{e : Expression ev tv r}
           → Q , Qg , Γ ⊢ e ∶ τ₁
           → Q , Qg ⊩ (τ₁ ∼ τ₂)
           → Q , Qg , Γ ⊢ e ∶ τ₂
      Abst : ∀ {τ₁ τ₂}{r}{e : Expression (Ⓢ ev) tv r}
           → Q , Qg , (⟨ ∀′ 0 · ε ⇒ τ₁ ⟩, Γ) ⊢ e ∶ τ₂
           → Q , Qg , Γ ⊢ λ′ e ∶ funType τ₁ τ₂
      Appl : ∀ {τ₁ τ₂}{r₁ r₂}{e₁ : Expression ev tv r₁}{e₂ : Expression ev tv r₂}
           → Q , Qg , Γ ⊢ e₁ ∶ funType τ₁ τ₂
           → Q , Qg , Γ ⊢ e₂ ∶ τ₁
           → Q , Qg , Γ ⊢ (e₁ · e₂) ∶ τ₂
      Let1 : ∀ {τ₁ τ₂}{r₁ r₂}{e₁ : Expression ev tv r₁}{e₂ : Expression (Ⓢ ev) tv r₂}
           → Q , Qg , Γ ⊢ e₁ ∶ τ₁
           → Q , Qg , (⟨ ∀′ 0 · ε ⇒ τ₁ ⟩, Γ) ⊢ e₂ ∶ τ₂
           → Q , Qg , Γ ⊢ (let₁ e₁ in′ e₂) ∶ τ₂
      Let2 : ∀ {τ₁ τ₂}{r₁ r₂}{e₁ : Expression ev tv r₁}{e₂ : Expression (Ⓢ ev) tv r₂}
           → Q , Qg , Γ ⊢ e₁ ∶ τ₁
           → Q , Qg , (⟨ ∀′ 0 · ε ⇒ τ₁ ⟩, Γ) ⊢ e₂ ∶ τ₂
           → Q , Qg , Γ ⊢ (let₂ e₁ ∷ τ₁ in′ e₂) ∶ τ₂
      Let3 : ∀ {n}{τ₁ τ₂}{r₁ r₂}{Qv}{e₁ : Expression ev (tv ⨁ n) r₁}{e₂ : Expression (Ⓢ ev) tv r₂}
           → Ax-f.map (pn-m.unit {n}) Q , QC-f.map (pn-m.unit {n}) Qg ∧ Qv , TS-f.map (pn-m.unit {n}) ∘ Γ ⊢ e₁ ∶ τ₁
           → Q , Qg , (⟨ ∀′ n · Qv ⇒ τ₁ ⟩, Γ) ⊢ e₂ ∶ τ₂
           → Q , Qg , Γ ⊢ (let₃ n · e₁ ∷ Qv ⇒ τ₁ in′ e₂) ∶ τ₂
      VarN : ∀ {n}{v}{τ}{Qv}
           → (θ : (tv ⨁ n) → Type tv)
           → Γ v ≡ ∀′ n · Qv ⇒ τ
           → Q , Qg ⊩ constraint-substitute θ Qv
           → Q , Qg , Γ ⊢ (Var {_}{_}{Regular} v) ∶ (τ >>= θ )
      DCn1 : ∀ {n}{l}{v}{K}{args}
           → (θ : (tv ⨁ n) → Type tv)
           → Γ v ≡ (DC∀ n · args ⟶ K)
           → Q , Qg , Γ ⊢ (Var {_}{_}{Datacon l} v) ∶ (applyAll n (unit K) >>= θ)
      DCn2 : ∀ {a b}{l}{v}{K}{args}{Qv}
           → (θ : (tv ⨁ a) ⨁ b → Type tv)
           → Γ v ≡ (DC∀′ a , b · Qv ⇒ args ⟶ K)
           → Q , Qg ⊩ constraint-substitute θ Qv
           → Q , Qg , Γ ⊢ (Var {_}{_}{Datacon l} v) ∶ (map (pn-m.unit {b}) (applyAll a (unit K)) >>= θ)
      Case : ∀ {τ}{r r′}{e : Expression ev tv r}{alts : Alternatives ev tv r′} {n : ℕ}
           → (T : tv)
           → (θ : (tv ⨁ n) → Type tv)
           → Q , Qg , Γ ⊢ e ∶ (applyAll n (unit T) >>= θ)
           → AltsType {n = n} Q Qg Γ θ T alts τ
           → Q , Qg , Γ ⊢ case e of alts ∶ τ

    data AltsType {ev tv : Set}{n : ℕ}(Q : AxiomScheme tv)(Qg : QConstraint tv)(Γ : Environment ev tv)( θ : (tv ⨁ n) → Type tv)(T : tv)
                : {r : Shape} → Alternatives ev tv r → Type tv → Set where
       NoAlts : ∀ {τ} → AltsType Q Qg Γ θ T esac τ
       OneAlt : ∀ {τ}{a}{r₁ r₂}{p : Name ev (Datacon a)}{e : Expression (ev ⨁ a) tv r₁}{as : Alternatives ev tv r₂}{vs}
              → AltsType {n = n} Q Qg Γ θ T as τ
              → Γ p ≡ DC∀ n · vs ⟶ T
              → Q , Qg , addAll (Vec-f.map (λ x → x >>= θ) vs) Γ ⊢ e ∶ τ
              → AltsType Q Qg Γ θ T ((p →′ e) ∣ as) τ
       GATAlt : ∀ {x}{τ}{a}{r₁ r₂}{p : Name ev (Datacon a)}{e : Expression (ev ⨁ a) tv r₁}{as : Alternatives ev tv r₂}{vs}{Qv}
              → let θ′ :  PlusN x (PlusN n tv) → Type (PlusN x tv)
                    θ′ v = sequence-PlusN {Type}{x} ⦃ type-is-monad ⦄ (Functor.map (pn-m.is-functor {x}) θ v)
                    Q′  = Ax-f.map (pn-m.unit {x}) Q
                    Qg′ = QC-f.map (pn-m.unit {x}) Qg
             in AltsType {n = n} Q Qg Γ θ T as τ
              → Γ p ≡ DC∀′ n , x · Qv ⇒ vs ⟶ T
              → Q′ , Qg′ ∧ (constraint-substitute θ′ Qv) ,  addAll (Vec-f.map (λ x → x >>= θ′) vs) (TS-f.map (pn-m.unit {x}) ∘ Γ)
                ⊢ Exp-f.map (pn-m.unit {x}) e ∶ map (pn-m.unit {x}) τ
              → AltsType Q Qg Γ θ T ((p →′ e) ∣ as) τ

  data _,_,_⊢′_ {ev tv : Set}(Q : AxiomScheme tv)(Qg : QConstraint tv)(Γ : Environment ev tv):  Program ev tv → Set where
    Empty : Q , Qg , Γ ⊢′ end
    Bind : {r : Shape}{n : ℕ}{e : Expression ev tv r}{p : Program (Ⓢ ev) tv}{Qv Q₁ : QConstraint (tv ⨁ n)}{τ : Type (tv ⨁ n)}
          → let Q′  = Ax-f.map (pn-m.unit {n}) Q
                Qg′ = QC-f.map (pn-m.unit {n}) Qg
                e′  = Exp-f.map (pn-m.unit {n}) e
         in Q′ , Qv ∧ Qg′ ⊩ Q₁
          → Q′ , Q₁ , (TS-f.map (pn-m.unit {n}) ∘ Γ) ⊢ e′ ∶ τ
          → Q , Qg , (⟨ ∀′ n · Qv ⇒ τ  ⟩, Γ) ⊢′ p
          → Q , Qg , Γ ⊢′ bind₁ e , p
    BindA : {r : Shape}{n : ℕ}{e : Expression ev (tv ⨁ n) r}{p : Program (Ⓢ ev) tv}{Qv Q₁ : QConstraint (tv ⨁ n)}{τ : Type (tv ⨁ n)}
          → let Q′  = Ax-f.map (pn-m.unit {n}) Q
                Qg′ = QC-f.map (pn-m.unit {n}) Qg
         in Q′ , Qv ∧ Qg′ ⊩ Q₁
          → Q′ , Q₁ , (TS-f.map (pn-m.unit {n}) ∘ Γ) ⊢ e ∶ τ
          → Q , Qg , (⟨ ∀′ n · Qv ⇒ τ ⟩, Γ) ⊢′ p
          → Q , Qg , Γ ⊢′ bind₂ n · e ∷ Qv ⇒ τ , p

  open import Data.Empty

  -- I know that Γ (N v) == ∀′ α · q₁ ⇒ τ₁
  -- I know that gen≡

  soundness-lemma : ∀{r}{n}{ev}{tv}{Γ : Environment ev tv}{e : Expression ev tv r}{r′}{τ}{C}{C′}{C′′}{n′}{Q}{Qg}{Qr}{θ}{eq : Eq (tv ⨁ n)}{Cext}
                  → Γ ► e ∶ τ ↝ C → C prenex: n , C′ → C′ separate: r′ , C′′ →  Q , Qg , n solv► C′′ ↝ n′ , Qr , θ
                  →  let Q′  = Ax-f.map (pn-m.unit {n′}) Q
                         Qg′ = QC-f.map (pn-m.unit {n′}) Qg
                         e′  = Exp-f.map (pn-m.unit {n′}) e
                      in ∃ (λ Qe → (Q′ , Qe , TS-f.map (pn-m.unit {n′}) ∘ Γ ⊢ e′ ∶ map (pn-m.unit {n′}) τ)
                            × Q′ , (Qg′ ∧ Qr) ⊩ Qe  )
{-  soundness-lemma (VarCon₁ Γv≡∀n·q⇒t) pnx sep sol = {!_ , VarN ? ? ? , ?!} -}
{-  soundness-lemma (App {C₁ = C₁}{C₂} Pe₁ Pe₂) pnx sep sol with prenex (C₁ ∧′ C₂) | prenex (C₂ ∧′ C₁)
  ... | f₁ , C₁′  , p₁  | f₂ , C₂′  , p₂  with separate C₁′ | separate C₂′
  ... | r₁ , C₁′′ , p₁′ | r₂ , C₂′′ , p₂′ with soundness-lemma Pe₁ p₁ p₁′ {!!} | soundness-lemma Pe₂ p₂ p₂′ {!!}
  ... | Q₁ , P₁   , P₁′ | Q₂ , P₂ , P₂′  = Q₁ ∧ (Q₂ ∧ {!!}) , Appl P₁ P₂ , {!!}  -}
  soundness-lemma {n = suc (suc .(na + nb))} {e = λ′ e′} {τ = τ}
                  (Abs {C = Ⅎ Ⅎ (C ∧′ rest)} p)
                  (PN-Ext (PN-Ext (PN-∧ {._}{._}{na}{nb} p₁ p₂)))
                  (Separate (Simpl-∧ p₁s p₂s) (Implic-∧ p₁i p₂i)) (SOLVE simpl impls) with soundness-lemma {e = Exp-f.map (suc ∘ suc) e′} p p₁ (Separate {!p₁s!} {!!}) {!!}
  ... | Q₁ , t , e = {!!}
  soundness-lemma (_) pnx sep sol = {!!}

{-
  soundness-proof : ∀ {ev}{tv}{eq : Eq tv}{Q}{Γ : Environment ev tv}{p} → Q , Γ ► p →  Q , ε , Γ ⊢′ p
  soundness-proof (Empty) = Empty
  soundness-proof (Bind _ _ _ _ _) = Bind {!!} {!!} {!!}
  soundness-proof (BindA _ _ _ _ _) = BindA {!!} {!!} {!!}
-}

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


text:
open import SOAS.Common
open import SOAS.Families.Core

-- Algebras for a signature endofunctor
module SOAS.Metatheory.Algebra {T : Set} (⅀F : Functor (𝔽amiliesₛ {T}) (𝔽amiliesₛ {T})) where

module ⅀ = Functor ⅀F

⅀ : Familyₛ → Familyₛ
⅀ = ⅀.₀

⅀₁ : {𝒳 𝒴 : Familyₛ} → 𝒳 ⇾̣ 𝒴 → ⅀ 𝒳 ⇾̣ ⅀ 𝒴
⅀₁ = Functor.₁ ⅀F

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
-- Jesper, 2017-08-13: This test case now fails since instantiation
-- of metavariables during case splitting was disabled (see #2621).

{-# OPTIONS --allow-unsolved-metas #-}

record ⊤ : Set where
  constructor tt

data I : Set where
  i : ⊤ → I

data D : I → Set where
  d : D (i tt)

postulate
  P : (x : I) → D x → Set

foo : (y : _) → P _ y
foo d = {!!}

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda


text:
{-
  Day 2 task of https://adventofcode.com/
-}
module a2 where

open import Agda.Builtin.IO using (IO)
open import Agda.Builtin.Unit using (⊤)
open import Agda.Builtin.String using (String; primShowNat; primStringAppend)
open import Agda.Builtin.Equality

open import Data.Nat
open import Data.Bool using (if_then_else_)
open import Data.List
open import Data.Maybe renaming (map to maybeMap)

postulate putStrLn : String → IO ⊤
{-# FOREIGN GHC import qualified Data.Text as T #-}
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}

-- helper
shopMaybeNat : Maybe ℕ → String
shopMaybeNat (just n) = primShowNat n
shopMaybeNat nothing = "nothing"

data Command : Set where
  forward : ℕ → Command
  up      : ℕ → Command
  down    : ℕ → Command

record Position : Set where
  constructor pos
  field
    h : ℕ
    d : ℕ

open Position

apply : Command → Position → Maybe Position

apply (forward x) (pos h d) = just (pos (h + x) d)

apply (up x)      (pos h d) = if d <ᵇ x
                              then nothing
                              else just (pos h ∣ d - x ∣)

apply (down x)    (pos h d) = just (pos h (d + x))

iterate : List Command → Position → Maybe Position
iterate [] p = just p
iterate (command ∷ list) p with apply command p
...                           | just q  = iterate list q
...                           | nothing = nothing

doTask : List Command → Maybe ℕ
doTask list = let maybeResult = iterate list (pos 0 0)
              in maybeMap multiplyComponents maybeResult
  where multiplyComponents : Position → ℕ
        multiplyComponents (pos h d) = h * d

input : List Command
input =
  forward 2 ∷
  forward 3 ∷
  forward 5 ∷
  forward 6 ∷
  down 7 ∷
  forward 8 ∷
  forward 4 ∷
  forward 7 ∷
  forward 5 ∷
  forward 5 ∷
  down 4 ∷
  down 9 ∷
  forward 8 ∷
  forward 5 ∷
  up 5 ∷
  down 5 ∷
  forward 3 ∷
  down 4 ∷
  down 8 ∷
  forward 9 ∷
  down 1 ∷
  up 9 ∷
  down 7 ∷
  up 7 ∷
  up 1 ∷
  forward 1 ∷
  down 1 ∷
  down 4 ∷
  down 4 ∷
  down 8 ∷
  down 4 ∷
  up 3 ∷
  down 1 ∷
  down 3 ∷
  forward 7 ∷
  down 6 ∷
  forward 3 ∷
  forward 5 ∷
  forward 2 ∷
  up 9 ∷
  forward 7 ∷
  up 5 ∷
  down 3 ∷
  forward 1 ∷
  forward 2 ∷
  down 3 ∷
  down 8 ∷
  down 3 ∷
  forward 8 ∷
  up 5 ∷
  down 5 ∷
  forward 3 ∷
  down 5 ∷
  forward 9 ∷
  down 3 ∷
  down 4 ∷
  down 9 ∷
  down 7 ∷
  up 3 ∷
  down 9 ∷
  up 9 ∷
  up 1 ∷
  forward 3 ∷
  up 4 ∷
  down 3 ∷
  forward 7 ∷
  forward 7 ∷
  up 7 ∷
  forward 6 ∷
  down 7 ∷
  down 6 ∷
  forward 2 ∷
  forward 9 ∷
  down 5 ∷
  forward 4 ∷
  up 6 ∷
  down 1 ∷
  down 9 ∷
  down 9 ∷
  forward 4 ∷
  down 1 ∷
  forward 6 ∷
  down 1 ∷
  down 5 ∷
  down 4 ∷
  down 4 ∷
  forward 4 ∷
  forward 9 ∷
  up 1 ∷
  down 2 ∷
  down 8 ∷
  down 5 ∷
  down 8 ∷
  down 8 ∷
  up 2 ∷
  forward 8 ∷
  up 1 ∷
  forward 4 ∷
  down 5 ∷
  down 1 ∷
  up 2 ∷
  forward 6 ∷
  forward 9 ∷
  forward 2 ∷
  forward 6 ∷
  forward 9 ∷
  up 6 ∷
  forward 9 ∷
  up 4 ∷
  down 7 ∷
  up 6 ∷
  forward 2 ∷
  down 1 ∷
  up 3 ∷
  forward 1 ∷
  forward 8 ∷
  down 6 ∷
  down 8 ∷
  down 8 ∷
  forward 8 ∷
  forward 2 ∷
  forward 2 ∷
  down 2 ∷
  up 1 ∷
  down 9 ∷
  up 9 ∷
  down 9 ∷
  up 3 ∷
  forward 9 ∷
  up 4 ∷
  up 7 ∷
  up 6 ∷
  down 9 ∷
  forward 1 ∷
  down 3 ∷
  down 4 ∷
  forward 8 ∷
  down 3 ∷
  down 9 ∷
  up 3 ∷
  forward 2 ∷
  up 5 ∷
  down 3 ∷
  forward 8 ∷
  up 3 ∷
  down 3 ∷
  forward 2 ∷
  forward 9 ∷
  down 1 ∷
  down 9 ∷
  down 4 ∷
  up 7 ∷
  down 4 ∷
  up 6 ∷
  forward 5 ∷
  down 6 ∷
  forward 3 ∷
  down 2 ∷
  forward 1 ∷
  forward 8 ∷
  down 4 ∷
  forward 1 ∷
  up 7 ∷
  forward 6 ∷
  up 9 ∷
  forward 6 ∷
  down 3 ∷
  forward 2 ∷
  down 4 ∷
  forward 6 ∷
  down 3 ∷
  down 6 ∷
  down 1 ∷
  down 1 ∷
  down 5 ∷
  forward 3 ∷
  forward 9 ∷
  forward 8 ∷
  down 3 ∷
  forward 7 ∷
  up 9 ∷
  forward 9 ∷
  up 2 ∷
  forward 4 ∷
  up 3 ∷
  forward 1 ∷
  up 6 ∷
  up 8 ∷
  down 5 ∷
  down 6 ∷
  up 9 ∷
  down 6 ∷
  down 9 ∷
  up 9 ∷
  down 4 ∷
  forward 5 ∷
  up 2 ∷
  down 3 ∷
  up 3 ∷
  down 1 ∷
  forward 3 ∷
  down 5 ∷
  forward 7 ∷
  down 6 ∷
  down 7 ∷
  down 5 ∷
  forward 2 ∷
  up 6 ∷
  down 9 ∷
  down 4 ∷
  down 3 ∷
  forward 9 ∷
  up 8 ∷
  forward 2 ∷
  down 2 ∷
  forward 4 ∷
  up 6 ∷
  down 4 ∷
  up 8 ∷
  down 7 ∷
  down 2 ∷
  up 6 ∷
  up 4 ∷
  down 2 ∷
  forward 5 ∷
  up 4 ∷
  down 8 ∷
  forward 3 ∷
  forward 1 ∷
  down 7 ∷
  forward 8 ∷
  forward 7 ∷
  down 7 ∷
  up 4 ∷
  forward 8 ∷
  down 5 ∷
  up 9 ∷
  forward 1 ∷
  forward 4 ∷
  forward 9 ∷
  forward 7 ∷
  down 9 ∷
  up 9 ∷
  down 1 ∷
  down 7 ∷
  forward 7 ∷
  down 7 ∷
  down 7 ∷
  down 3 ∷
  down 5 ∷
  forward 3 ∷
  down 2 ∷
  forward 6 ∷
  down 9 ∷
  up 5 ∷
  up 3 ∷
  forward 5 ∷
  down 6 ∷
  down 1 ∷
  forward 4 ∷
  down 3 ∷
  forward 8 ∷
  down 7 ∷
  forward 7 ∷
  forward 7 ∷
  up 7 ∷
  up 2 ∷
  up 3 ∷
  forward 9 ∷
  down 5 ∷
  up 2 ∷
  forward 5 ∷
  up 5 ∷
  forward 2 ∷
  forward 2 ∷
  down 8 ∷
  forward 2 ∷
  up 4 ∷
  forward 1 ∷
  forward 3 ∷
  up 8 ∷
  up 9 ∷
  forward 5 ∷
  down 1 ∷
  up 8 ∷
  down 4 ∷
  down 8 ∷
  up 4 ∷
  forward 9 ∷
  down 6 ∷
  down 8 ∷
  up 2 ∷
  up 3 ∷
  down 7 ∷
  down 4 ∷
  forward 5 ∷
  down 6 ∷
  forward 3 ∷
  forward 3 ∷
  forward 8 ∷
  down 1 ∷
  down 7 ∷
  down 9 ∷
  down 2 ∷
  down 7 ∷
  forward 7 ∷
  down 7 ∷
  down 6 ∷
  up 6 ∷
  forward 8 ∷
  forward 5 ∷
  up 5 ∷
  down 2 ∷
  up 8 ∷
  up 4 ∷
  down 9 ∷
  up 2 ∷
  forward 5 ∷
  up 2 ∷
  down 4 ∷
  up 4 ∷
  forward 2 ∷
  forward 4 ∷
  forward 9 ∷
  forward 9 ∷
  up 4 ∷
  up 5 ∷
  down 1 ∷
  down 6 ∷
  down 1 ∷
  down 4 ∷
  down 5 ∷
  down 3 ∷
  forward 3 ∷
  down 9 ∷
  forward 6 ∷
  down 3 ∷
  down 9 ∷
  down 2 ∷
  up 2 ∷
  down 2 ∷
  down 7 ∷
  forward 9 ∷
  down 3 ∷
  down 3 ∷
  down 2 ∷
  down 3 ∷
  forward 2 ∷
  down 9 ∷
  down 9 ∷
  up 5 ∷
  up 3 ∷
  forward 4 ∷
  up 7 ∷
  forward 8 ∷
  up 6 ∷
  forward 7 ∷
  down 7 ∷
  down 1 ∷
  forward 5 ∷
  down 2 ∷
  up 1 ∷
  down 8 ∷
  up 3 ∷
  forward 2 ∷
  up 9 ∷
  down 1 ∷
  down 3 ∷
  down 6 ∷
  down 2 ∷
  down 7 ∷
  up 2 ∷
  forward 5 ∷
  forward 7 ∷
  down 2 ∷
  forward 5 ∷
  forward 4 ∷
  forward 5 ∷
  down 3 ∷
  forward 7 ∷
  down 7 ∷
  forward 8 ∷
  down 3 ∷
  down 2 ∷
  up 1 ∷
  forward 6 ∷
  down 4 ∷
  down 2 ∷
  forward 7 ∷
  up 3 ∷
  down 4 ∷
  forward 2 ∷
  up 6 ∷
  down 3 ∷
  up 6 ∷
  up 8 ∷
  down 9 ∷
  up 6 ∷
  forward 8 ∷
  forward 9 ∷
  forward 4 ∷
  forward 7 ∷
  down 2 ∷
  forward 9 ∷
  down 7 ∷
  up 9 ∷
  down 5 ∷
  down 6 ∷
  up 5 ∷
  down 4 ∷
  forward 8 ∷
  forward 4 ∷
  forward 4 ∷
  down 6 ∷
  forward 3 ∷
  forward 6 ∷
  down 9 ∷
  down 9 ∷
  up 2 ∷
  forward 7 ∷
  down 8 ∷
  down 9 ∷
  down 9 ∷
  forward 7 ∷
  forward 3 ∷
  down 7 ∷
  down 8 ∷
  forward 8 ∷
  down 6 ∷
  down 5 ∷
  down 9 ∷
  down 3 ∷
  forward 1 ∷
  down 5 ∷
  forward 2 ∷
  forward 8 ∷
  down 2 ∷
  forward 6 ∷
  forward 3 ∷
  down 7 ∷
  down 4 ∷
  forward 8 ∷
  forward 1 ∷
  down 6 ∷
  forward 9 ∷
  forward 6 ∷
  up 1 ∷
  up 3 ∷
  down 8 ∷
  forward 1 ∷
  up 5 ∷
  down 4 ∷
  forward 7 ∷
  up 3 ∷
  down 2 ∷
  forward 1 ∷
  forward 9 ∷
  down 9 ∷
  down 7 ∷
  forward 8 ∷
  down 4 ∷
  up 3 ∷
  down 4 ∷
  forward 2 ∷
  forward 6 ∷
  down 7 ∷
  forward 6 ∷
  down 6 ∷
  down 4 ∷
  down 1 ∷
  up 9 ∷
  down 4 ∷
  down 7 ∷
  up 4 ∷
  down 9 ∷
  forward 6 ∷
  down 3 ∷
  forward 2 ∷
  down 4 ∷
  forward 3 ∷
  down 5 ∷
  up 9 ∷
  forward 8 ∷
  up 7 ∷
  up 6 ∷
  up 4 ∷
  forward 1 ∷
  down 1 ∷
  forward 4 ∷
  up 6 ∷
  forward 5 ∷
  forward 4 ∷
  forward 5 ∷
  up 6 ∷
  down 1 ∷
  forward 3 ∷
  up 7 ∷
  down 9 ∷
  up 9 ∷
  down 5 ∷
  forward 6 ∷
  forward 4 ∷
  up 1 ∷
  down 4 ∷
  up 1 ∷
  forward 3 ∷
  forward 1 ∷
  down 3 ∷
  forward 7 ∷
  down 2 ∷
  forward 3 ∷
  up 2 ∷
  forward 8 ∷
  down 3 ∷
  up 9 ∷
  down 5 ∷
  forward 6 ∷
  down 1 ∷
  down 8 ∷
  down 5 ∷
  forward 1 ∷
  down 6 ∷
  up 2 ∷
  forward 6 ∷
  down 2 ∷
  down 1 ∷
  up 6 ∷
  up 7 ∷
  down 5 ∷
  forward 7 ∷
  forward 6 ∷
  forward 6 ∷
  down 7 ∷
  forward 4 ∷
  down 5 ∷
  up 5 ∷
  down 1 ∷
  up 8 ∷
  down 8 ∷
  down 2 ∷
  down 2 ∷
  down 9 ∷
  up 9 ∷
  forward 2 ∷
  forward 7 ∷
  down 7 ∷
  down 4 ∷
  down 4 ∷
  down 8 ∷
  forward 5 ∷
  forward 2 ∷
  up 9 ∷
  down 9 ∷
  forward 7 ∷
  up 9 ∷
  down 2 ∷
  down 7 ∷
  up 2 ∷
  up 8 ∷
  forward 8 ∷
  down 4 ∷
  forward 3 ∷
  forward 4 ∷
  forward 6 ∷
  forward 2 ∷
  down 1 ∷
  down 2 ∷
  forward 2 ∷
  up 1 ∷
  down 1 ∷
  forward 5 ∷
  up 3 ∷
  up 3 ∷
  down 3 ∷
  down 1 ∷
  down 4 ∷
  up 5 ∷
  up 6 ∷
  forward 5 ∷
  up 7 ∷
  forward 6 ∷
  down 4 ∷
  down 7 ∷
  up 8 ∷
  forward 1 ∷
  down 5 ∷
  up 4 ∷
  up 3 ∷
  up 5 ∷
  down 1 ∷
  up 5 ∷
  forward 3 ∷
  up 5 ∷
  forward 2 ∷
  forward 2 ∷
  forward 5 ∷
  forward 2 ∷
  up 9 ∷
  forward 4 ∷
  down 1 ∷
  down 3 ∷
  down 5 ∷
  up 2 ∷
  down 8 ∷
  forward 8 ∷
  forward 9 ∷
  down 1 ∷
  down 3 ∷
  forward 8 ∷
  forward 2 ∷
  down 2 ∷
  down 1 ∷
  up 7 ∷
  forward 2 ∷
  forward 8 ∷
  down 9 ∷
  forward 1 ∷
  forward 4 ∷
  down 7 ∷
  down 4 ∷
  up 7 ∷
  down 3 ∷
  down 1 ∷
  down 4 ∷
  up 7 ∷
  down 6 ∷
  forward 7 ∷
  down 8 ∷
  up 2 ∷
  up 4 ∷
  up 6 ∷
  down 9 ∷
  down 9 ∷
  down 8 ∷
  forward 6 ∷
  up 3 ∷
  up 1 ∷
  forward 9 ∷
  forward 6 ∷
  up 4 ∷
  up 2 ∷
  up 7 ∷
  forward 5 ∷
  up 9 ∷
  up 9 ∷
  forward 9 ∷
  up 6 ∷
  down 1 ∷
  down 3 ∷
  forward 3 ∷
  down 2 ∷
  down 2 ∷
  down 6 ∷
  down 9 ∷
  forward 3 ∷
  forward 7 ∷
  up 3 ∷
  forward 3 ∷
  down 5 ∷
  forward 9 ∷
  up 6 ∷
  down 2 ∷
  forward 8 ∷
  down 3 ∷
  up 5 ∷
  down 6 ∷
  forward 9 ∷
  down 5 ∷
  down 2 ∷
  down 6 ∷
  forward 8 ∷
  forward 6 ∷
  down 1 ∷
  forward 6 ∷
  up 1 ∷
  up 7 ∷
  down 4 ∷
  down 7 ∷
  forward 4 ∷
  forward 7 ∷
  down 4 ∷
  forward 8 ∷
  down 8 ∷
  down 7 ∷
  forward 9 ∷
  down 1 ∷
  down 3 ∷
  down 6 ∷
  forward 7 ∷
  forward 6 ∷
  forward 3 ∷
  forward 8 ∷
  down 5 ∷
  down 3 ∷
  up 1 ∷
  down 9 ∷
  down 8 ∷
  forward 3 ∷
  down 6 ∷
  down 1 ∷
  forward 5 ∷
  forward 5 ∷
  forward 9 ∷
  up 5 ∷
  down 6 ∷
  up 9 ∷
  down 7 ∷
  down 6 ∷
  up 1 ∷
  forward 5 ∷
  forward 7 ∷
  forward 8 ∷
  forward 7 ∷
  forward 6 ∷
  forward 3 ∷
  forward 1 ∷
  forward 2 ∷
  up 4 ∷
  forward 3 ∷
  forward 4 ∷
  forward 5 ∷
  up 2 ∷
  up 3 ∷
  forward 4 ∷
  down 9 ∷
  up 4 ∷
  forward 7 ∷
  down 6 ∷
  down 6 ∷
  down 1 ∷
  forward 2 ∷
  down 2 ∷
  forward 2 ∷
  down 3 ∷
  forward 7 ∷
  forward 8 ∷
  down 4 ∷
  up 7 ∷
  forward 7 ∷
  down 7 ∷
  forward 7 ∷
  forward 9 ∷
  down 7 ∷
  up 2 ∷
  down 3 ∷
  forward 7 ∷
  down 1 ∷
  forward 8 ∷
  forward 2 ∷
  up 9 ∷
  down 3 ∷
  forward 2 ∷
  up 4 ∷
  forward 9 ∷
  down 4 ∷
  down 4 ∷
  forward 4 ∷
  down 2 ∷
  down 9 ∷
  forward 4 ∷
  down 2 ∷
  down 6 ∷
  forward 9 ∷
  forward 2 ∷
  up 1 ∷
  forward 2 ∷
  forward 3 ∷
  down 5 ∷
  up 8 ∷
  down 4 ∷
  down 4 ∷
  forward 7 ∷
  down 2 ∷
  up 6 ∷
  down 9 ∷
  forward 9 ∷
  up 1 ∷
  forward 3 ∷
  down 5 ∷
  forward 3 ∷
  down 3 ∷
  forward 4 ∷
  up 3 ∷
  down 6 ∷
  down 7 ∷
  down 4 ∷
  down 8 ∷
  down 4 ∷
  down 5 ∷
  up 9 ∷
  up 1 ∷
  down 7 ∷
  up 3 ∷
  up 3 ∷
  down 3 ∷
  up 4 ∷
  up 6 ∷
  forward 8 ∷
  down 1 ∷
  forward 7 ∷
  forward 4 ∷
  down 9 ∷
  down 1 ∷
  forward 7 ∷
  forward 9 ∷
  forward 1 ∷
  down 3 ∷
  down 2 ∷
  forward 3 ∷
  forward 2 ∷
  down 7 ∷
  forward 9 ∷
  forward 6 ∷
  up 9 ∷
  down 2 ∷
  forward 9 ∷
  up 6 ∷
  forward 8 ∷
  up 1 ∷
  down 5 ∷
  down 8 ∷
  forward 1 ∷
  down 1 ∷
  forward 9 ∷
  up 1 ∷
  forward 9 ∷
  forward 1 ∷
  forward 1 ∷
  down 7 ∷
  forward 3 ∷
  forward 6 ∷
  down 5 ∷
  forward 7 ∷
  forward 1 ∷
  down 7 ∷
  down 6 ∷
  down 6 ∷
  forward 5 ∷
  up 6 ∷
  down 6 ∷
  forward 8 ∷
  up 2 ∷
  down 8 ∷
  down 3 ∷
  up 5 ∷
  up 8 ∷
  down 6 ∷
  forward 4 ∷
  forward 2 ∷
  up 3 ∷
  forward 5 ∷
  forward 3 ∷
  up 8 ∷
  forward 6 ∷
  up 8 ∷
  forward 1 ∷
  up 8 ∷
  up 7 ∷
  up 6 ∷
  forward 2 ∷
  down 9 ∷
  down 9 ∷
  forward 3 ∷
  down 7 ∷
  forward 3 ∷
  down 6 ∷
  forward 9 ∷
  up 5 ∷
  down 1 ∷
  forward 7 ∷
  down 1 ∷
  down 5 ∷
  down 9 ∷
  forward 8 ∷
  forward 9 ∷
  forward 7 ∷
  down 9 ∷
  up 4 ∷
  forward 5 ∷
  down 5 ∷
  forward 5 ∷
  down 9 ∷
  forward 9 ∷
  forward 3 ∷
  up 5 ∷
  forward 8 ∷
  up 5 ∷
  down 1 ∷
  forward 8 ∷
  down 3 ∷
  forward 6 ∷
  up 9 ∷
  forward 8 ∷
  down 4 ∷
  forward 3 ∷
  down 5 ∷
  forward 8 ∷
  forward 9 ∷
  forward 2 ∷
  down 1 ∷
  down 6 ∷
  down 4 ∷
  forward 9 ∷
  up 2 ∷
  down 3 ∷
  down 6 ∷
  down 3 ∷
  down 9 ∷
  down 1 ∷
  up 6 ∷
  down 2 ∷
  down 7 ∷
  up 5 ∷
  forward 5 ∷
  up 1 ∷
  down 7 ∷
  forward 6 ∷
  up 6 ∷
  down 2 ∷
  down 3 ∷
  forward 3 ∷
  down 5 ∷
  forward 8 ∷
  down 9 ∷
  down 7 ∷
  down 8 ∷
  up 7 ∷
  down 1 ∷
  forward 1 ∷
  forward 1 ∷
  down 2 ∷
  up 4 ∷
  forward 2 ∷
  down 3 ∷
  up 2 ∷
  down 3 ∷
  down 2 ∷
  forward 7 ∷
  down 1 ∷
  up 7 ∷
  down 2 ∷
  down 1 ∷
  forward 6 ∷
  down 9 ∷
  up 9 ∷
  down 4 ∷
  down 6 ∷
  up 9 ∷
  forward 7 ∷
  forward 9 ∷
  forward 7 ∷
  down 4 ∷
  down 1 ∷
  forward 7 ∷
  down 4 ∷
  down 7 ∷
  down 3 ∷
  down 5 ∷
  forward 3 ∷
  down 8 ∷
  forward 8 ∷
  forward 7 ∷
  forward 8 ∷
  down 4 ∷
  down 9 ∷
  forward 2 ∷
  forward 7 ∷
  up 8 ∷
  forward 4 ∷
  down 6 ∷
  up 8 ∷
  down 2 ∷
  forward 3 ∷
  down 6 ∷
  down 8 ∷
  forward 8 ∷
  forward 2 ∷
  forward 9 ∷
  up 6 ∷
  forward 7 ∷
  down 3 ∷
  down 5 ∷
  forward 8 ∷
  forward 9 ∷
  down 3 ∷
  forward 3 ∷
  forward 2 ∷
  forward 3 ∷
  down 8 ∷
  up 9 ∷
  up 5 ∷
  up 2 ∷
  up 6 ∷
  up 1 ∷
  up 1 ∷
  up 5 ∷
  forward 3 ∷
  forward 2 ∷
  down 3 ∷
  forward 4 ∷
  []

main : IO ⊤
main = putStrLn (shopMaybeNat (doTask input))

private
  -- checks from the exercise text
  _ : apply (forward 5) (pos 0 0) ≡ just (pos 5 0)
  _ = refl

  _ : apply (down 5) (pos 5 0) ≡ just (pos 5 5)
  _ = refl

  _ : apply (forward 8) (pos 5 5) ≡ just (pos 13 5)
  _ = refl

  _ : apply (up 3) (pos 13 5) ≡ just (pos 13 2)
  _ = refl

  _ : apply (down 8) (pos 13 2) ≡ just (pos 13 10)
  _ = refl

  _ : apply (forward 2) (pos 13 10) ≡ just (pos 15 10)
  _ = refl

  -- submarine does not 'fly'
  _ : apply (up 7) (pos 13 2) ≡ nothing
  _ = refl

max_stars_repo_name: felixwellen/adventOfCode

max_issues_repo_name: felixwellen/adventOfCode

max_forks_repo_name: felixwellen/adventOfCode