text:
module Structure.OrderedField where

import      Lvl
open import Data.Boolean
open import Data.Boolean.Proofs
import      Data.Either as Either
open import Data.Tuple as Tuple
open import Functional
open import Logic
open import Logic.Classical
open import Logic.IntroInstances
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Natural using (ℕ)
import      Numeral.Natural.Relation.Order as ℕ
open import Relator.Ordering
import      Relator.Ordering.Proofs as OrderingProofs
open import Structure.Setoid
open import Structure.Function
open import Structure.Function.Domain
open import Structure.Function.Ordering
open import Structure.Operator.Field
open import Structure.Operator.Monoid
open import Structure.Operator.Group
open import Structure.Operator.Proofs
open import Structure.Operator.Properties
open import Structure.Operator.Ring.Proofs
open import Structure.Operator.Ring
open import Structure.Operator
open import Structure.Relator
open import Structure.Relator.Ordering
open        Structure.Relator.Ordering.Weak.Properties
open import Structure.Relator.Properties
open import Structure.Relator.Proofs
open import Syntax.Implication
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₗ ℓₑ : Lvl.Level
private variable F : Type{ℓ}

-- TODO: Generalize so that this does not neccessarily need a rng. See linearly ordered groups and partially ordered groups. See also ordered semigroups and monoids where the property is called "compatible".
record Ordered ⦃ equiv : Equiv{ℓₑ}(F) ⦄ (_+_ _⋅_ : F → F → F) ⦃ rng : Rng(_+_)(_⋅_) ⦄ (_≤_ : F → F → Stmt{ℓₗ}) : Type{Lvl.of(F) Lvl.⊔ ℓₗ Lvl.⊔ ℓₑ} where
  open From-[≤] (_≤_) public
  open Rng(rng)

  field
    ⦃ [≤]-totalOrder ⦄    : Weak.TotalOrder(_≤_)(_≡_)
    [≤][+]ₗ-preserve      : ∀{x y z} → (x ≤ y) → ((x + z) ≤ (y + z))
    [≤][⋅]-zero           : ∀{x y} → (𝟎 ≤ x) → (𝟎 ≤ y) → (𝟎 ≤ (x ⋅ y)) -- TODO: Rename to preserve-sign
    ⦃ [≤]-binaryRelator ⦄ : BinaryRelator(_≤_)

  -- TODO: Move this to Structure.Relator.Order or something
  instance
    [≡][≤]-sub : (_≡_) ⊆₂ (_≤_)
    _⊆₂_.proof [≡][≤]-sub p = substitute₂ᵣ(_≤_) p (reflexivity(_≤_))

  open Weak.TotalOrder([≤]-totalOrder) public
  open OrderingProofs.From-[≤] (_≤_) public

  record NonNegative (x : F) : Stmt{ℓₗ} where
    constructor intro
    field proof : (x ≥ 𝟎)

  record Positive (x : F) : Stmt{ℓₗ} where
    constructor intro
    field proof : (x > 𝟎)

  [≤][+]ᵣ-preserve : ∀{x y z} → (y ≤ z) → ((x + y) ≤ (x + z))
  [≤][+]ᵣ-preserve {x}{y}{z} yz =
    x + y 🝖[ _≡_ ]-[ commutativity(_+_) ]-sub
    y + x 🝖[ _≤_ ]-[ [≤][+]ₗ-preserve yz ]
    z + x 🝖[ _≡_ ]-[ commutativity(_+_) ]-sub
    x + z 🝖-end

  [≤][+]-preserve : ∀{x₁ x₂ y₁ y₂} → (x₁ ≤ x₂) → (y₁ ≤ y₂) → ((x₁ + y₁) ≤ (x₂ + y₂))
  [≤][+]-preserve {x₁}{x₂}{y₁}{y₂} px py =
    x₁ + y₁ 🝖[ _≤_ ]-[ [≤][+]ₗ-preserve px ]
    x₂ + y₁ 🝖[ _≤_ ]-[ [≤][+]ᵣ-preserve py ]
    x₂ + y₂ 🝖[ _≤_ ]-end

  [≤]-flip-positive : ∀{x} → (𝟎 ≤ x) ↔ ((− x) ≤ 𝟎)
  [≤]-flip-positive {x} = [↔]-intro l r where
    l = \p →
      𝟎         🝖[ _≡_ ]-[ symmetry(_≡_) (inverseFunctionᵣ(_+_)(−_)) ]-sub
      x + (− x) 🝖[ _≤_ ]-[ [≤][+]ᵣ-preserve p ]
      x + 𝟎     🝖[ _≡_ ]-[ identityᵣ(_+_)(𝟎) ]-sub
      x         🝖-end
    r = \p →
      − x       🝖[ _≡_ ]-[ symmetry(_≡_) (identityₗ(_+_)(𝟎)) ]-sub
      𝟎 + (− x) 🝖[ _≤_ ]-[ [≤][+]ₗ-preserve p ]
      x + (− x) 🝖[ _≡_ ]-[ inverseFunctionᵣ(_+_)(−_) ]-sub
      𝟎         🝖-end

  [≤]-non-negative-difference : ∀{x y} → (𝟎 ≤ (y − x)) → (x ≤ y)
  [≤]-non-negative-difference {x}{y} 𝟎yx =
    x               🝖[ _≡_ ]-[ symmetry(_≡_) (identityₗ(_+_)(𝟎)) ]-sub
    𝟎 + x           🝖[ _≤_ ]-[ [≤][+]ₗ-preserve 𝟎yx ]
    (y − x) + x     🝖[ _≤_ ]-[]
    (y + (− x)) + x 🝖[ _≡_ ]-[ associativity(_+_) ]-sub
    y + ((− x) + x) 🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(_) (inverseFunctionₗ(_+_)(−_)) ]-sub
    y + 𝟎           🝖[ _≡_ ]-[ identityᵣ(_+_)(𝟎) ]-sub
    y               🝖-end

  [≤]-non-positive-difference : ∀{x y} → ((x − y) ≤ 𝟎) → (x ≤ y)
  [≤]-non-positive-difference {x}{y} xy𝟎 =
    x               🝖[ _≡_ ]-[ symmetry(_≡_) (identityᵣ(_+_)(𝟎)) ]-sub
    x + 𝟎           🝖[ _≡_ ]-[ symmetry(_≡_) (congruence₂ᵣ(_+_)(_) (inverseFunctionₗ(_+_)(−_))) ]-sub
    x + ((− y) + y) 🝖[ _≡_ ]-[ symmetry(_≡_) (associativity(_+_)) ]-sub
    (x + (− y)) + y 🝖[ _≤_ ]-[]
    (x − y) + y     🝖[ _≤_ ]-[ [≤][+]ₗ-preserve xy𝟎 ]
    𝟎 + y           🝖[ _≡_ ]-[ identityₗ(_+_)(𝟎) ]-sub
    y               🝖-end

  [≤]-with-[−] : ∀{x y} → (x ≤ y) → ((− y) ≤ (− x))
  [≤]-with-[−] {x}{y} xy = [≤]-non-positive-difference proof3 where
    proof3 : (((− y) − (− x)) ≤ 𝟎)
    proof3 =
      (− y) − (− x) 🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(_) (involution(−_)) ]-sub
      (− y) + x     🝖[ _≡_ ]-[ commutativity(_+_) ]-sub
      x − y         🝖[ _≤_ ]-[ [≤][+]ₗ-preserve xy ]
      y − y         🝖[ _≡_ ]-[ inverseFunctionᵣ(_+_)(−_) ]-sub
      𝟎             🝖-end

  [≤]-flip-negative : ∀{x} → (x ≤ 𝟎) ↔ (𝟎 ≤ (− x))
  [≤]-flip-negative {x} = [↔]-intro l r where
    r = \p →
      𝟎   🝖[ _≡_ ]-[ symmetry(_≡_) [−]-of-𝟎 ]-sub
      − 𝟎 🝖[ _≤_ ]-[ [≤]-with-[−] {x}{𝟎} p ]
      − x 🝖-end

    l = \p →
      x      🝖[ _≡_ ]-[ symmetry(_≡_) (involution(−_)) ]-sub
      −(− x) 🝖[ _≤_ ]-[ [≤]-with-[−] p ]
      − 𝟎    🝖[ _≡_ ]-[ [−]-of-𝟎 ]-sub
      𝟎      🝖-end

  [≤][−]ₗ-preserve : ∀{x y z} → (x ≤ y) → ((x − z) ≤ (y − z))
  [≤][−]ₗ-preserve = [≤][+]ₗ-preserve

  [≤][−]ᵣ-preserve : ∀{x y z} → (z ≤ y) → ((x − y) ≤ (x − z))
  [≤][−]ᵣ-preserve = [≤][+]ᵣ-preserve ∘ [≤]-with-[−]

  [≤][+]-withoutᵣ : ∀{x₁ x₂ y} → ((x₁ + y) ≤ (x₂ + y)) → (x₁ ≤ x₂)
  [≤][+]-withoutᵣ {x₁}{x₂}{y} p =
    x₁           🝖[ _≡_ ]-[ symmetry(_≡_) (inverseOperᵣ(_+_)(_−_)) ]-sub
    (x₁ + y) − y 🝖[ _≤_ ]-[ [≤][−]ₗ-preserve p ]
    (x₂ + y) − y 🝖[ _≡_ ]-[ inverseOperᵣ(_+_)(_−_) ]-sub
    x₂           🝖-end

  [≤][+]-withoutₗ : ∀{x y₁ y₂} → ((x + y₁) ≤ (x + y₂)) → (y₁ ≤ y₂)
  [≤][+]-withoutₗ {x}{y₁}{y₂} p =
    y₁               🝖[ _≡_ ]-[ symmetry(_≡_) (inversePropₗ(_+_)(−_)) ]-sub
    (− x) + (x + y₁) 🝖[ _≤_ ]-[ [≤][+]ᵣ-preserve p ]
    (− x) + (x + y₂) 🝖[ _≡_ ]-[ inversePropₗ(_+_)(−_) ]-sub
    y₂               🝖-end

  [<][+]-preserveₗ : ∀{x₁ x₂ y} → (x₁ < x₂) → ((x₁ + y) < (x₂ + y))
  [<][+]-preserveₗ {x₁}{x₂}{y} px p = px ([≤][+]-withoutᵣ p)

  [<][+]-preserveᵣ : ∀{x y₁ y₂} → (y₁ < y₂) → ((x + y₁) < (x + y₂))
  [<][+]-preserveᵣ {x₁}{x₂}{y} px p = px ([≤][+]-withoutₗ p)

  [<][+]-preserve : ∀{x₁ x₂ y₁ y₂} → (x₁ < x₂) → (y₁ < y₂) → ((x₁ + y₁) < (x₂ + y₂))
  [<][+]-preserve {x₁}{x₂}{y₁}{y₂} px py =
    x₁ + y₁ 🝖[ _<_ ]-[ [<][+]-preserveₗ px ]
    x₂ + y₁ 🝖-semiend
    x₂ + y₂ 🝖[ _<_ ]-end-from-[ [<][+]-preserveᵣ py ]

  postulate [<][+]-preserve-subₗ : ∀{x₁ x₂ y₁ y₂} → (x₁ ≤ x₂) → (y₁ < y₂) → ((x₁ + y₁) < (x₂ + y₂))
  postulate [<][+]-preserve-subᵣ : ∀{x₁ x₂ y₁ y₂} → (x₁ < x₂) → (y₁ ≤ y₂) → ((x₁ + y₁) < (x₂ + y₂))

-- Theory defining the axioms of an ordered field (a field with a weak total order).
record OrderedField ⦃ equiv : Equiv{ℓₑ}(F) ⦄ (_+_ _⋅_ : F → F → F) (_≤_ : F → F → Stmt{ℓₗ}) : Type{Lvl.of(F) Lvl.⊔ ℓₗ Lvl.⊔ ℓₑ} where
  field
    ⦃ [+][⋅]-field ⦄ : Field(_+_)(_⋅_)
    ⦃ ordered ⦄      : Ordered(_+_)(_⋅_)(_≤_)

  open Field([+][⋅]-field) public
  open Ordered(ordered) public


text:
module Global where

open import Data.List
open import Data.Maybe
open import Data.Product
open import Relation.Binary.PropositionalEquality

open import Typing

-- specific
data PosNeg : Set where
  POS NEG POSNEG : PosNeg

-- global session context
SEntry = Maybe (STypeF SType × PosNeg)
SCtx = List SEntry

-- SSplit G G₁ G₂
-- split G into G₁ and G₂
-- length and position preserving
data SSplit : SCtx → SCtx → SCtx → Set where
  ss-[]    : SSplit [] [] []
  ss-both  : ∀ {  G G₁ G₂ }
           → SSplit G G₁ G₂
           → SSplit (nothing ∷ G) (nothing ∷ G₁) (nothing ∷ G₂)
  ss-left  : ∀ { spn G G₁ G₂ }
           → SSplit G G₁ G₂
           → SSplit (just spn ∷ G) (just spn ∷ G₁) (nothing ∷ G₂)
  ss-right : ∀ { spn G G₁ G₂ }
           → SSplit G G₁ G₂
           → SSplit (just spn ∷ G) (nothing ∷ G₁) (just spn ∷ G₂)
  ss-posneg : ∀ {  s G G₁ G₂ }
          → SSplit G G₁ G₂
          → SSplit (just (s , POSNEG) ∷ G) (just (s , POS) ∷ G₁) (just (s , NEG) ∷ G₂)
  ss-negpos : ∀ {  s G G₁ G₂ }
          → SSplit G G₁ G₂
          → SSplit (just (s , POSNEG) ∷ G) (just (s , NEG) ∷ G₁) (just (s , POS) ∷ G₂)

ssplit-sym : ∀ {G G₁ G₂} → SSplit G G₁ G₂ → SSplit G G₂ G₁
ssplit-sym ss-[] = ss-[]
ssplit-sym (ss-both ss12) = ss-both (ssplit-sym ss12)
ssplit-sym (ss-left ss12) = ss-right (ssplit-sym ss12)
ssplit-sym (ss-right ss12) = ss-left (ssplit-sym ss12)
ssplit-sym (ss-posneg ss12) = ss-negpos (ssplit-sym ss12)
ssplit-sym (ss-negpos ss12) = ss-posneg (ssplit-sym ss12)

-- tedious but easy to prove
ssplit-compose : {G G₁ G₂ G₃ G₄ : SCtx}
  → (ss : SSplit G G₁ G₂)
  → (ss₁ : SSplit G₁ G₃ G₄)
  → ∃ λ Gi → SSplit G G₃ Gi × SSplit Gi G₄ G₂
ssplit-compose ss-[] ss-[] =  [] , (ss-[] , ss-[])
ssplit-compose (ss-both ss) (ss-both ss₁) with ssplit-compose ss ss₁
ssplit-compose (ss-both ss) (ss-both ss₁) | Gi , ss₁₃ , ss₂₄ = nothing ∷ Gi , ss-both ss₁₃ , ss-both ss₂₄
ssplit-compose (ss-left ss) (ss-left ss₁) with ssplit-compose ss ss₁
... | Gi , ss₁₃ , ss₂₄ = nothing ∷ Gi , ss-left ss₁₃ , ss-both ss₂₄
ssplit-compose (ss-left ss) (ss-right ss₁) with ssplit-compose ss ss₁
... | Gi , ss₁₃ , ss₂₄ = just _ ∷ Gi , ss-right ss₁₃ , ss-left ss₂₄
ssplit-compose (ss-left ss) (ss-posneg ss₁) with ssplit-compose ss ss₁
... | Gi , ss₁₃ , ss₂₄ =  just ( _ , NEG) ∷ Gi , ss-posneg ss₁₃ , ss-left ss₂₄
ssplit-compose (ss-left ss) (ss-negpos ss₁) with ssplit-compose ss ss₁
... | Gi , ss₁₃ , ss₂₄ = just ( _ , POS) ∷ Gi , ss-negpos ss₁₃ , ss-left ss₂₄
ssplit-compose (ss-right ss) (ss-both ss₁) with ssplit-compose ss ss₁
... | Gi , ss₁₃ , ss₂₄ = just _ ∷ Gi , ss-right ss₁₃ , ss-right ss₂₄
ssplit-compose (ss-posneg ss) (ss-left ss₁) with ssplit-compose ss ss₁
... | Gi , ss₁₃ , ss₂₄ = just ( _ , NEG) ∷ Gi , ss-posneg ss₁₃ , ss-right ss₂₄
ssplit-compose (ss-posneg ss) (ss-right ss₁) with ssplit-compose ss ss₁
... | Gi , ss₁₃ , ss₂₄ = just ( _ , POSNEG) ∷ Gi , ss-right ss₁₃ , ss-posneg ss₂₄
ssplit-compose (ss-negpos ss) (ss-left ss₁) with ssplit-compose ss ss₁
... | Gi , ss₁₃ , ss₂₄ = just ( _ , POS) ∷ Gi , ss-negpos ss₁₃ , ss-right ss₂₄
ssplit-compose (ss-negpos ss) (ss-right ss₁) with ssplit-compose ss ss₁
... | Gi , ss₁₃ , ss₂₄ = just ( _ , POSNEG) ∷ Gi , ss-right ss₁₃ , ss-negpos ss₂₄

ssplit-compose2 : {G G₁ G₂ G₂₁ G₂₂ : SCtx}
  → SSplit G G₁ G₂
  → SSplit G₂ G₂₁ G₂₂
  → ∃ λ Gi → (SSplit G Gi G₂₁ × SSplit Gi G₁ G₂₂)
ssplit-compose2 ss-[] ss-[] = [] , ss-[] , ss-[]
ssplit-compose2 (ss-both ss) (ss-both ss₂) with ssplit-compose2 ss ss₂
... | Gi , ssx , ssy = nothing ∷ Gi , ss-both ssx , ss-both ssy
ssplit-compose2 (ss-left ss) (ss-both ss₂) with ssplit-compose2 ss ss₂
... | Gi , ssx , ssy = just _ ∷ Gi , ss-left ssx , ss-left ssy
ssplit-compose2 (ss-right ss) (ss-left ss₂) with ssplit-compose2 ss ss₂
... | Gi , ssx , ssy = nothing ∷ Gi , ss-right ssx , ss-both ssy
ssplit-compose2 (ss-right ss) (ss-right ss₂) with ssplit-compose2 ss ss₂
... | Gi , ssx , ssy = just _ ∷ Gi , ss-left ssx , ss-right ssy
ssplit-compose2 (ss-right ss) (ss-posneg ss₂) with ssplit-compose2 ss ss₂
... | Gi , ssx , ssy = just (_ , NEG) ∷ Gi , ss-negpos ssx , ss-right ssy
ssplit-compose2 (ss-right ss) (ss-negpos ss₂) with ssplit-compose2 ss ss₂
... | Gi , ssx , ssy = just (_ , POS) ∷ Gi , ss-posneg ssx , ss-right ssy
ssplit-compose2 (ss-posneg ss) (ss-left ss₂) with ssplit-compose2 ss ss₂
... | Gi , ssx , ssy = just (_ , POS) ∷ Gi , ss-posneg ssx , ss-left ssy
ssplit-compose2 (ss-posneg ss) (ss-right ss₂) with ssplit-compose2 ss ss₂
... | Gi , ssx , ssy = just (_ , POSNEG) ∷ Gi , ss-left ssx , ss-posneg ssy
ssplit-compose2 (ss-negpos ss) (ss-left ss₂) with ssplit-compose2 ss ss₂
... | Gi , ssx , ssy = just (_ , NEG) ∷ Gi , ss-negpos ssx , ss-left ssy
ssplit-compose2 (ss-negpos ss) (ss-right ss₂) with ssplit-compose2 ss ss₂
... | Gi , ssx , ssy = just (_ , POSNEG) ∷ Gi , ss-left ssx , ss-negpos ssy

ssplit-compose3 : {G G₁ G₂ G₃ G₄ : SCtx}
  → SSplit G G₁ G₂
  → SSplit G₂ G₃ G₄
  → ∃ λ Gi → (SSplit G Gi G₄ × SSplit Gi G₁ G₃)
ssplit-compose3 ss-[] ss-[] = [] , ss-[] , ss-[]
ssplit-compose3 (ss-both ss12) (ss-both ss234) with ssplit-compose3 ss12 ss234
... | Gi , ssi4 , ssi13 = nothing ∷ Gi , ss-both ssi4 , ss-both ssi13
ssplit-compose3 (ss-left ss12) (ss-both ss234) with ssplit-compose3 ss12 ss234
... | Gi , ssi4 , ssi13 = just _ ∷ Gi , ss-left ssi4 , ss-left ssi13
ssplit-compose3 (ss-right ss12) (ss-left ss234) with ssplit-compose3 ss12 ss234
... | Gi , ssi4 , ssi13 = just _ ∷ Gi , ss-left ssi4 , ss-right ssi13
ssplit-compose3 (ss-right ss12) (ss-right ss234) with ssplit-compose3 ss12 ss234
... | Gi , ssi4 , ssi13 = nothing ∷ Gi , ss-right ssi4 , ss-both ssi13
ssplit-compose3 (ss-right ss12) (ss-posneg ss234) with ssplit-compose3 ss12 ss234
... | Gi , ssi4 , ssi13 = just ( _ , POS) ∷ Gi , ss-posneg ssi4 , ss-right ssi13
ssplit-compose3 (ss-right ss12) (ss-negpos ss234) with ssplit-compose3 ss12 ss234
... | Gi , ssi4 , ssi13 = just ( _ , NEG) ∷ Gi , ss-negpos ssi4 , ss-right ssi13
ssplit-compose3 (ss-posneg ss12) (ss-left ss234) with ssplit-compose3 ss12 ss234
... | Gi , ssi4 , ssi13 = just ( _ , POSNEG) ∷ Gi , ss-left ssi4 , ss-posneg ssi13
ssplit-compose3 (ss-posneg ss12) (ss-right ss234) with ssplit-compose3 ss12 ss234
... | Gi , ssi4 , ssi13 = just ( _ , POS) ∷ Gi , ss-posneg ssi4 , ss-left ssi13
ssplit-compose3 (ss-negpos ss12) (ss-left ss234) with ssplit-compose3 ss12 ss234
... | Gi , ssi4 , ssi13 = just ( _ , POSNEG) ∷ Gi , ss-left ssi4 , ss-negpos ssi13
ssplit-compose3 (ss-negpos ss12) (ss-right ss234) with ssplit-compose3 ss12 ss234
... | Gi , ssi4 , ssi13 = just ( _ , NEG) ∷ Gi , ss-negpos ssi4 , ss-left ssi13

ssplit-compose4
  : {G G₁ G₂ G₂₁ G₂₂ : SCtx}
  → (ss : SSplit G G₁ G₂)
  → (ss₁ : SSplit G₂ G₂₁ G₂₂)
  → ∃ λ Gi → SSplit G G₂₁ Gi × SSplit Gi G₁ G₂₂
ssplit-compose4 ss-[] ss-[] = [] , ss-[] , ss-[]
ssplit-compose4 (ss-both ss) (ss-both ss₁) with ssplit-compose4 ss ss₁
... | Gi , ss-21i , ss-122 = nothing ∷ Gi , ss-both ss-21i , ss-both ss-122
ssplit-compose4 (ss-left ss) (ss-both ss₁) with ssplit-compose4 ss ss₁
... | Gi , ss-21i , ss-122 = just _ ∷ Gi , ss-right ss-21i , ss-left ss-122
ssplit-compose4 (ss-right ss) (ss-left ss₁) with ssplit-compose4 ss ss₁
... | Gi , ss-21i , ss-122 = nothing ∷ Gi , ss-left ss-21i , ss-both ss-122
ssplit-compose4 (ss-right ss) (ss-right ss₁) with ssplit-compose4  ss ss₁
... | Gi , ss-21i , ss-122 = just _ ∷ Gi , ss-right ss-21i , ss-right ss-122
ssplit-compose4 (ss-right ss) (ss-posneg ss₁) with ssplit-compose4 ss ss₁
... | Gi , ss-21i , ss-122 = just (_ , NEG) ∷ Gi , ss-posneg ss-21i , ss-right ss-122
ssplit-compose4 (ss-right ss) (ss-negpos ss₁) with ssplit-compose4 ss ss₁
... | Gi , ss-21i , ss-122 = just (_ , POS) ∷ Gi , ss-negpos ss-21i , ss-right ss-122
ssplit-compose4 (ss-posneg ss) (ss-left ss₁) with ssplit-compose4 ss ss₁
... | Gi , ss-21i , ss-122 = just (_ , POS) ∷ Gi , ss-negpos ss-21i , ss-left ss-122
ssplit-compose4 (ss-posneg ss) (ss-right ss₁) with ssplit-compose4 ss ss₁
... | Gi , ss-21i , ss-122 = just (_ , POSNEG) ∷ Gi , ss-right ss-21i , ss-posneg ss-122
ssplit-compose4 (ss-negpos ss) (ss-left ss₁) with ssplit-compose4 ss ss₁
... | Gi , ss-21i , ss-122 = just (_ , NEG) ∷ Gi , ss-posneg ss-21i , ss-left ss-122
ssplit-compose4 (ss-negpos ss) (ss-right ss₁) with ssplit-compose4 ss ss₁
... | Gi , ss-21i , ss-122 = just (_ , POSNEG) ∷ Gi , ss-right ss-21i , ss-negpos ss-122

ssplit-compose5
  : ∀ {G G₁ G₂ G₁₁ G₁₂ : SCtx}
  → (ss : SSplit G G₁ G₂)
  → (ss₁ : SSplit G₁ G₁₁ G₁₂)
  → ∃ λ Gi → SSplit G G₁₂ Gi × SSplit Gi G₁₁ G₂
ssplit-compose5 ss-[] ss-[] = [] , ss-[] , ss-[]
ssplit-compose5 (ss-both ss) (ss-both ss₁) with ssplit-compose5 ss ss₁
... | Gi , ss-12i , ss-112 = nothing ∷ Gi , ss-both ss-12i , ss-both ss-112
ssplit-compose5 (ss-left ss) (ss-left ss₁) with ssplit-compose5 ss ss₁
... | Gi , ss-12i , ss-112 = just _ ∷ Gi , ss-right ss-12i , ss-left ss-112
ssplit-compose5 (ss-left ss) (ss-right ss₁) with ssplit-compose5 ss ss₁
... | Gi , ss-12i , ss-112 = nothing ∷ Gi , ss-left ss-12i , ss-both ss-112
ssplit-compose5 (ss-left ss) (ss-posneg ss₁) with ssplit-compose5 ss ss₁
... | Gi , ss-12i , ss-112 = just (_ , POS) ∷ Gi , ss-negpos ss-12i , ss-left ss-112
ssplit-compose5 (ss-left ss) (ss-negpos ss₁) with ssplit-compose5 ss ss₁
... | Gi , ss-12i , ss-112 = just (_ , NEG) ∷ Gi , ss-posneg ss-12i , ss-left ss-112
ssplit-compose5 (ss-right ss) (ss-both ss₁) with ssplit-compose5 ss ss₁
... | Gi , ss-12i , ss-112 = just _ ∷ Gi , ss-right ss-12i , ss-right ss-112
ssplit-compose5 (ss-posneg ss) (ss-left ss₁) with ssplit-compose5 ss ss₁
... | Gi , ss-12i , ss-112 = just (_ , POSNEG) ∷ Gi , ss-right ss-12i , ss-posneg ss-112
ssplit-compose5 (ss-posneg ss) (ss-right ss₁) with ssplit-compose5 ss ss₁
... | Gi , ss-12i , ss-112 = just (_ , NEG) ∷ Gi , ss-posneg ss-12i , ss-right ss-112
ssplit-compose5 (ss-negpos ss) (ss-left ss₁) with ssplit-compose5 ss ss₁
... | Gi , ss-12i , ss-112 = just (_ , POSNEG) ∷ Gi , ss-right ss-12i , ss-negpos ss-112
ssplit-compose5 (ss-negpos ss) (ss-right ss₁) with ssplit-compose5 ss ss₁
... | Gi , ss-12i , ss-112 = just (_ , POS) ∷ Gi , ss-negpos ss-12i , ss-right ss-112

ssplit-compose6
  : ∀ {G G₁ G₂ G₁₁ G₁₂ : SCtx}
  → (ss : SSplit G G₁ G₂)
  → (ss₁ : SSplit G₁ G₁₁ G₁₂)
  → ∃ λ Gi → SSplit G G₁₁ Gi × SSplit Gi G₁₂ G₂
ssplit-compose6 ss-[] ss-[] = [] , ss-[] , ss-[]
ssplit-compose6 (ss-both ss) (ss-both ss₁) with ssplit-compose6 ss ss₁
... | Gi , ss-g11i , ss-g122 = nothing ∷ Gi , ss-both ss-g11i , ss-both ss-g122
ssplit-compose6 (ss-left ss) (ss-left ss₁) with ssplit-compose6 ss ss₁
... | Gi , ss-g11i , ss-g122 = nothing ∷ Gi , ss-left ss-g11i , ss-both ss-g122
ssplit-compose6 (ss-left ss) (ss-right ss₁) with ssplit-compose6 ss ss₁
... | Gi , ss-g11i , ss-g122 = just _ ∷ Gi , ss-right ss-g11i , ss-left ss-g122
ssplit-compose6 (ss-left ss) (ss-posneg ss₁) with ssplit-compose6 ss ss₁
... | Gi , ss-g11i , ss-g122 = just (_ , NEG) ∷ Gi , ss-posneg ss-g11i , ss-left ss-g122
ssplit-compose6 (ss-left ss) (ss-negpos ss₁) with ssplit-compose6 ss ss₁
... | Gi , ss-g11i , ss-g122 = just (_ , POS) ∷ Gi , ss-negpos ss-g11i , ss-left ss-g122
ssplit-compose6 (ss-right ss) (ss-both ss₁) with ssplit-compose6 ss ss₁
... | Gi , ss-g11i , ss-g122 = just _ ∷ Gi , ss-right ss-g11i , ss-right ss-g122
ssplit-compose6 (ss-posneg ss) (ss-left ss₁) with ssplit-compose6 ss ss₁
... | Gi , ss-g11i , ss-g122 = just (_ , NEG) ∷ Gi , ss-posneg ss-g11i , ss-right ss-g122
ssplit-compose6 (ss-posneg ss) (ss-right ss₁) with ssplit-compose6 ss ss₁
... | Gi , ss-g11i , ss-g122 = just (_ , POSNEG) ∷ Gi , ss-right ss-g11i , ss-posneg ss-g122
ssplit-compose6 (ss-negpos ss) (ss-left ss₁) with ssplit-compose6 ss ss₁
... | Gi , ss-g11i , ss-g122 = just (_ , POS) ∷ Gi , ss-negpos ss-g11i , ss-right ss-g122
ssplit-compose6 (ss-negpos ss) (ss-right ss₁) with ssplit-compose6 ss ss₁
... | Gi , ss-g11i , ss-g122 = just (_ , POSNEG) ∷ Gi , ss-right ss-g11i , ss-negpos ss-g122

ssplit-join
  : ∀ {G G₁ G₂ G₁₁ G₁₂ G₂₁ G₂₂}
  → (ss : SSplit G G₁ G₂)
  → (ss₁ : SSplit G₁ G₁₁ G₁₂)
  → (ss₂ : SSplit G₂ G₂₁ G₂₂)
  → ∃ λ G₁' → ∃ λ G₂' → SSplit G G₁' G₂' × SSplit G₁' G₁₁ G₂₁ × SSplit G₂' G₁₂ G₂₂
ssplit-join ss-[] ss-[] ss-[] = [] , [] , ss-[] , ss-[] , ss-[]
ssplit-join (ss-both ss) (ss-both ss₁) (ss-both ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = nothing ∷ G₁' , nothing ∷ G₂' , ss-both ss-12 , ss-both ss-1121 , ss-both ss-2122
ssplit-join (ss-left ss) (ss-left ss₁) (ss-both ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = just _ ∷ G₁' , nothing ∷ G₂' , ss-left ss-12 ,  ss-left ss-1121 , ss-both ss-2122
ssplit-join (ss-left ss) (ss-right ss₁) (ss-both ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = nothing ∷ G₁' ,
                                                just _ ∷ G₂' ,
                                                ss-right ss-12 , ss-both ss-1121 , ss-left ss-2122
ssplit-join (ss-left ss) (ss-posneg ss₁) (ss-both ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = just _ ∷ G₁' , just _ ∷ G₂' , ss-posneg ss-12 , ss-left ss-1121 , ss-left ss-2122
ssplit-join (ss-left ss) (ss-negpos ss₁) (ss-both ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = just _ ∷ G₁' , just _ ∷ G₂' , ss-negpos ss-12 , ss-left ss-1121 , ss-left ss-2122
ssplit-join (ss-right ss) (ss-both ss₁) (ss-left ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = just _ ∷ G₁' ,
                                                nothing ∷ G₂' , ss-left ss-12 , ss-right ss-1121 , ss-both ss-2122
ssplit-join (ss-right ss) (ss-both ss₁) (ss-right ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = nothing ∷ G₁' ,
                                                just _ ∷ G₂' ,
                                                ss-right ss-12 , ss-both ss-1121 , ss-right ss-2122
ssplit-join (ss-right ss) (ss-both ss₁) (ss-posneg ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = just _ ∷ G₁' , just _ ∷ G₂' , ss-posneg ss-12 , ss-right ss-1121 , ss-right ss-2122
ssplit-join (ss-right ss) (ss-both ss₁) (ss-negpos ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = just _ ∷ G₁' , just _ ∷ G₂' , ss-negpos ss-12 , ss-right ss-1121 , ss-right ss-2122
ssplit-join (ss-posneg ss) (ss-left ss₁) (ss-left ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = just _ ∷ G₁' , nothing ∷ G₂' , ss-left ss-12 , ss-posneg ss-1121 , ss-both ss-2122
ssplit-join (ss-posneg ss) (ss-left ss₁) (ss-right ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = just _ ∷ G₁' , just _ ∷ G₂' , ss-posneg ss-12 , ss-left ss-1121 , ss-right ss-2122
ssplit-join (ss-posneg ss) (ss-right ss₁) (ss-left ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = just _ ∷ G₁' , just _ ∷ G₂' , ss-negpos ss-12 , ss-right ss-1121 , ss-left ss-2122
ssplit-join (ss-posneg ss) (ss-right ss₁) (ss-right ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = nothing ∷ G₁' ,
                                                just (_ , POSNEG) ∷ G₂' ,
                                                ss-right ss-12 , ss-both ss-1121 , ss-posneg ss-2122
ssplit-join (ss-negpos ss) (ss-left ss₁) (ss-left ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = just _ ∷ G₁' , nothing ∷ G₂' , ss-left ss-12 , ss-negpos ss-1121 , ss-both ss-2122
ssplit-join (ss-negpos ss) (ss-left ss₁) (ss-right ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = just _ ∷ G₁' , just _ ∷ G₂' , ss-negpos ss-12 , ss-left ss-1121 , ss-right ss-2122
ssplit-join (ss-negpos ss) (ss-right ss₁) (ss-left ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = just _ ∷ G₁' , just _ ∷ G₂' , ss-posneg ss-12 , ss-right ss-1121 , ss-left ss-2122
ssplit-join (ss-negpos ss) (ss-right ss₁) (ss-right ss₂) with ssplit-join ss ss₁ ss₂
... | G₁' , G₂' , ss-12 , ss-1121 , ss-2122 = nothing ∷ G₁' ,
                                                just (_ , POSNEG) ∷ G₂' ,
                                                ss-right ss-12 , ss-both ss-1121 , ss-negpos ss-2122

-- another rotation
ssplit-rotate : ∀ {G G1 G2 G21 G22 G211 G212 : SCtx}
  → SSplit G G1 G2
  → SSplit G2 G21 G22
  → SSplit G21 G211 G212
  → ∃ λ G2'
  → ∃ λ G21'
  → SSplit G G211 G2' × SSplit G2' G21' G22 × SSplit G21' G1 G212
ssplit-rotate ss-[] ss-[] ss-[] =
  [] , [] , ss-[] , ss-[] , ss-[]
ssplit-rotate (ss-both ss-g12) (ss-both ss-g2122) (ss-both ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  nothing ∷ G2' , nothing ∷ G21' , (ss-both ss-g12') , (ss-both ss-g2122') , (ss-both ss-g211212')
ssplit-rotate (ss-left ss-g12) (ss-both ss-g2122) (ss-both ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , (ss-right ss-g12') , ss-left ss-g2122' , ss-left ss-g211212'
ssplit-rotate (ss-right ss-g12) (ss-left ss-g2122) (ss-left ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , ss-left ss-g12' , ss-both ss-g2122' , ss-both ss-g211212'
ssplit-rotate (ss-right ss-g12) (ss-left ss-g2122) (ss-right ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , ss-right ss-g12' , ss-left ss-g2122' , ss-right ss-g211212'
ssplit-rotate (ss-right ss-g12) (ss-left ss-g2122) (ss-posneg ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , ss-posneg ss-g12' , ss-left ss-g2122' , ss-right ss-g211212'
ssplit-rotate (ss-right ss-g12) (ss-left ss-g2122) (ss-negpos ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , ss-negpos ss-g12' , ss-left ss-g2122' , ss-right ss-g211212'
ssplit-rotate (ss-right ss-g12) (ss-right ss-g2122) (ss-both ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , ss-right ss-g12' , ss-right ss-g2122' , ss-both ss-g211212'
ssplit-rotate (ss-right ss-g12) (ss-posneg ss-g2122) (ss-left ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , ss-posneg ss-g12' , ss-right ss-g2122' , ss-both ss-g211212'
ssplit-rotate (ss-right ss-g12) (ss-posneg ss-g2122) (ss-right ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , ss-right ss-g12' , ss-posneg ss-g2122' , ss-right ss-g211212'
ssplit-rotate (ss-right ss-g12) (ss-negpos ss-g2122) (ss-left ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , ss-negpos ss-g12' , ss-right ss-g2122' , ss-both ss-g211212'
ssplit-rotate (ss-right ss-g12) (ss-negpos ss-g2122) (ss-right ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , ss-right ss-g12' , ss-negpos ss-g2122' , ss-right ss-g211212'
ssplit-rotate (ss-posneg ss-g12) (ss-left ss-g2122) (ss-left ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , ss-negpos ss-g12' , ss-left ss-g2122' , ss-left ss-g211212'
ssplit-rotate (ss-posneg ss-g12) (ss-left ss-g2122) (ss-right ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , ss-right ss-g12' , ss-left ss-g2122' , ss-posneg ss-g211212'
ssplit-rotate (ss-posneg ss-g12) (ss-right ss-g2122) (ss-both ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , ss-right ss-g12' , ss-posneg ss-g2122' , ss-left ss-g211212'
ssplit-rotate (ss-negpos ss-g12) (ss-left ss-g2122) (ss-left ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , ss-posneg ss-g12' , ss-left ss-g2122' , ss-left ss-g211212'
ssplit-rotate (ss-negpos ss-g12) (ss-left ss-g2122) (ss-right ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , ss-right ss-g12' , ss-left ss-g2122' , ss-negpos ss-g211212'
ssplit-rotate (ss-negpos ss-g12) (ss-right ss-g2122) (ss-both ss-g211212) with ssplit-rotate ss-g12 ss-g2122 ss-g211212
... | G2' , G21' , ss-g12' , ss-g2122' , ss-g211212' =
  _ , _ , ss-right ss-g12' , ss-negpos ss-g2122' , ss-left ss-g211212'

-- a session context is inactive if all its entries are void
data Inactive : (G : SCtx) → Set where
  []-inactive : Inactive []
  ::-inactive : ∀ {G : SCtx} → Inactive G → Inactive (nothing ∷ G)

inactive-ssplit-trivial : ∀ {G} → Inactive G → SSplit G G G
inactive-ssplit-trivial []-inactive = ss-[]
inactive-ssplit-trivial (::-inactive ina) = ss-both (inactive-ssplit-trivial ina)

ssplit-inactive : ∀ {G G₁ G₂} → SSplit G G₁ G₂ → Inactive G₁ → Inactive G₂ → Inactive G
ssplit-inactive ss-[] []-inactive []-inactive = []-inactive
ssplit-inactive (ss-both ssp) (::-inactive ina1) (::-inactive ina2) = ::-inactive (ssplit-inactive ssp ina1 ina2)
ssplit-inactive (ss-left ssp) () ina2
ssplit-inactive (ss-right ssp) ina1 ()
ssplit-inactive (ss-posneg ssp) () ina2
ssplit-inactive (ss-negpos ssp) ina1 ()

ssplit-inactive-left : ∀ {G G'} → SSplit G G G' → Inactive G'
ssplit-inactive-left ss-[] = []-inactive
ssplit-inactive-left (ss-both ssp) = ::-inactive (ssplit-inactive-left ssp)
ssplit-inactive-left (ss-left ssp) = ::-inactive (ssplit-inactive-left ssp)

ssplit-refl-left : (G : SCtx) → Σ SCtx λ G' → SSplit G G G'
ssplit-refl-left [] = [] , ss-[]
ssplit-refl-left (just x ∷ G) with ssplit-refl-left G
... | G' , ssp' = nothing ∷ G' , ss-left ssp'
ssplit-refl-left (nothing ∷ G) with ssplit-refl-left G
... | G' , ssp' = nothing ∷ G' , ss-both ssp'

ssplit-refl-left-inactive : (G : SCtx) → Σ SCtx λ G' → Inactive G' × SSplit G G G'
ssplit-refl-left-inactive [] = [] , []-inactive , ss-[]
ssplit-refl-left-inactive (x ∷ G) with ssplit-refl-left-inactive G
ssplit-refl-left-inactive (just x ∷ G) | G' , ina-G' , ss-GG' = nothing ∷ G' , ::-inactive ina-G' , ss-left ss-GG'
ssplit-refl-left-inactive (nothing ∷ G) | G' , ina-G' , ss-GG' = nothing ∷ G' , ::-inactive ina-G' , ss-both ss-GG'

ssplit-inactive-right : ∀ {G G'} → SSplit G G' G → Inactive G'
ssplit-inactive-right ss-[] = []-inactive
ssplit-inactive-right (ss-both ss) = ::-inactive (ssplit-inactive-right ss)
ssplit-inactive-right (ss-right ss) = ::-inactive (ssplit-inactive-right ss)

ssplit-refl-right : (G : SCtx) → Σ SCtx λ G' → SSplit G G' G
ssplit-refl-right [] = [] , ss-[]
ssplit-refl-right (just x ∷ G) with ssplit-refl-right G
... | G' , ssp' = nothing ∷ G' , ss-right ssp'
ssplit-refl-right (nothing ∷ G) with ssplit-refl-right G
... | G' , ssp' = nothing ∷ G' , ss-both ssp'

ssplit-refl-right-inactive : (G : SCtx) → Σ SCtx λ G' → Inactive G' × SSplit G G' G
ssplit-refl-right-inactive [] = [] , []-inactive , ss-[]
ssplit-refl-right-inactive (x ∷ G) with ssplit-refl-right-inactive G
ssplit-refl-right-inactive (just x ∷ G) | G' , ina-G' , ssp' = nothing ∷ G' , ::-inactive ina-G' , ss-right ssp'
ssplit-refl-right-inactive (nothing ∷ G) | G' , ina-G' , ssp' = nothing ∷ G' , ::-inactive ina-G' , ss-both ssp'

inactive-left-ssplit : ∀ {G G₁ G₂} → SSplit G G₁ G₂ → Inactive G₁ → G ≡ G₂
inactive-left-ssplit ss-[] []-inactive = refl
inactive-left-ssplit (ss-both ss) (::-inactive inG₁) =
  cong (_∷_ nothing) (inactive-left-ssplit ss inG₁)
inactive-left-ssplit (ss-right ss) (::-inactive inG₁) =
  cong (_∷_ (just _)) (inactive-left-ssplit ss inG₁)

inactive-right-ssplit : ∀ {G G₁ G₂} → SSplit G G₁ G₂ → Inactive G₂ → G ≡ G₁
inactive-right-ssplit ss-[] []-inactive = refl
inactive-right-ssplit (ss-both ssp) (::-inactive ina) =
  cong (_∷_ nothing) (inactive-right-ssplit ssp ina)
inactive-right-ssplit (ss-left ssp) (::-inactive ina) =
  cong (_∷_ (just _)) (inactive-right-ssplit ssp ina)

inactive-right-ssplit-sym : ∀ {G G₁ G₂} → SSplit G G₁ G₂ → Inactive G₂ → G₁ ≡ G
inactive-right-ssplit-sym ssp ina = sym (inactive-right-ssplit ssp ina)

inactive-right-ssplit-transform : ∀ {G G₁ G₂} → SSplit G G₁ G₂ → Inactive G₂ → SSplit G G G₂
inactive-right-ssplit-transform ss-[] []-inactive = ss-[]
inactive-right-ssplit-transform (ss-both ss-GG1G2) (::-inactive ina-G2) = ss-both (inactive-right-ssplit-transform ss-GG1G2 ina-G2)
inactive-right-ssplit-transform (ss-left ss-GG1G2) (::-inactive ina-G2) = ss-left (inactive-right-ssplit-transform ss-GG1G2 ina-G2)
inactive-right-ssplit-transform (ss-right ss-GG1G2) ()
inactive-right-ssplit-transform (ss-posneg ss-GG1G2) ()
inactive-right-ssplit-transform (ss-negpos ss-GG1G2) ()

ssplit-function : ∀ {G G' G₁ G₂} → SSplit G G₁ G₂ → SSplit G' G₁ G₂ → G ≡ G'
ssplit-function ss-[] ss-[] = refl
ssplit-function (ss-both ssp-GG1G2) (ss-both ssp-G'G1G2) =
  cong (_∷_ nothing) (ssplit-function ssp-GG1G2 ssp-G'G1G2)
ssplit-function (ss-left ssp-GG1G2) (ss-left ssp-G'G1G2) =
  cong (_∷_ (just _)) (ssplit-function ssp-GG1G2 ssp-G'G1G2)
ssplit-function (ss-right ssp-GG1G2) (ss-right ssp-G'G1G2) =
  cong (_∷_ (just _)) (ssplit-function ssp-GG1G2 ssp-G'G1G2)
ssplit-function (ss-posneg ssp-GG1G2) (ss-posneg ssp-G'G1G2) =
  cong (_∷_ (just _)) (ssplit-function ssp-GG1G2 ssp-G'G1G2)
ssplit-function (ss-negpos ssp-GG1G2) (ss-negpos ssp-G'G1G2) =
  cong (_∷_ (just _)) (ssplit-function ssp-GG1G2 ssp-G'G1G2)

ssplit-function1 : ∀ {G G₁ G₁' G₂} → SSplit G G₁ G₂ → SSplit G G₁' G₂ → G₁ ≡ G₁'
ssplit-function1 ss-[] ss-[] = refl
ssplit-function1 (ss-both ssp-GG1G2) (ss-both ssp-GG1'G2) =
  cong (_∷_ nothing) (ssplit-function1 ssp-GG1G2 ssp-GG1'G2)
ssplit-function1 (ss-left ssp-GG1G2) (ss-left ssp-GG1'G2) =
  cong (_∷_ (just _)) (ssplit-function1 ssp-GG1G2 ssp-GG1'G2)
ssplit-function1 (ss-right ssp-GG1G2) (ss-right ssp-GG1'G2) =
  cong (_∷_ nothing) (ssplit-function1 ssp-GG1G2 ssp-GG1'G2)
ssplit-function1 (ss-posneg ssp-GG1G2) (ss-posneg ssp-GG1'G2) =
  cong (_∷_ (just _)) (ssplit-function1 ssp-GG1G2 ssp-GG1'G2)
ssplit-function1 (ss-negpos ssp-GG1G2) (ss-negpos ssp-GG1'G2) =
  cong (_∷_ (just _)) (ssplit-function1 ssp-GG1G2 ssp-GG1'G2)

ssplit-function2 : ∀ {G G₁ G₂ G₂'} → SSplit G G₁ G₂ → SSplit G G₁ G₂' → G₂ ≡ G₂'
ssplit-function2 ss-[] ss-[] = refl
ssplit-function2 (ss-both ssp-GG1G2) (ss-both ssp-GG1G2') =
  cong (_∷_ nothing) (ssplit-function2 ssp-GG1G2 ssp-GG1G2')
ssplit-function2 (ss-left ssp-GG1G2) (ss-left ssp-GG1G2') =
  cong (_∷_ nothing) (ssplit-function2 ssp-GG1G2 ssp-GG1G2')
ssplit-function2 (ss-right ssp-GG1G2) (ss-right ssp-GG1G2') =
  cong (_∷_ (just _)) (ssplit-function2 ssp-GG1G2 ssp-GG1G2')
ssplit-function2 (ss-posneg ssp-GG1G2) (ss-posneg ssp-GG1G2') =
  cong (_∷_ (just _)) (ssplit-function2 ssp-GG1G2 ssp-GG1G2')
ssplit-function2 (ss-negpos ssp-GG1G2) (ss-negpos ssp-GG1G2') =
  cong (_∷_ (just _)) (ssplit-function2 ssp-GG1G2 ssp-GG1G2')

ext: agda

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Products of nullary relations
------------------------------------------------------------------------

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

module Relation.Nullary.Product where

open import Data.Product
open import Function
open import Relation.Nullary

-- Some properties which are preserved by _×_.

infixr 2 _×-dec_

_×-dec_ : ∀ {p q} {P : Set p} {Q : Set q} →
          Dec P → Dec Q → Dec (P × Q)
yes p ×-dec yes q = yes (p , q)
no ¬p ×-dec _     = no (¬p ∘ proj₁)
_     ×-dec no ¬q = no (¬q ∘ proj₂)


text:
module Impure.STLCRef.Readme where

open import Impure.STLCRef.Syntax
open import Impure.STLCRef.Welltyped
open import Impure.STLCRef.Eval
open import Impure.STLCRef.Properties.Soundness


text:
-- You can omit the right hand side if you pattern match on an empty type. But
-- you have to do the matching.
module NoRHSRequiresAbsurdPattern where

data Zero : Set where

good : {A : Set} -> Zero -> A
good ()

bad : {A : Set} -> Zero -> A
bad h

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import FRP.JS.Maybe using ( Maybe ; just ; nothing )
open import FRP.JS.Bool using ( Bool ; true ; false ; _∨_ ; _∧_ )
open import FRP.JS.True using ( True ; tt ; contradiction ; ∧-intro ; ∧-elim₁ ; ∧-elim₂ )
open import FRP.JS.Nat using ( ℕ ; _+_ ; _∸_ )
open import FRP.JS.Keys using ( Keys ; IKeys ; _<?_ ; sorted ; head ; _∈i_ ; _∈_ )
  renaming ( keys to kkeys ; ikeys to ikeysk ; ikeys✓ to ikeysk✓ ; [] to []k ; _∷_ to _∷k_ )
open import FRP.JS.String using ( String ; _<_ ; _≟_ )
open import FRP.JS.String.Properties using ( <-trans )

module FRP.JS.Object where

infixr 4 _↦_∷_

data IObject {α} (A : Set α) : ∀ ks → True (sorted ks) → Set α where
  [] : IObject A []k tt
  _↦_∷_ : ∀ k (a : A) {ks k∷ks✓} →
    (as : IObject A ks (∧-elim₂ {k <? head ks} k∷ks✓)) →
      IObject A (k ∷k ks) k∷ks✓

{-# COMPILED_JS IObject function(x,v) {
  if ((x.array.length) <= (x.offset)) { return v["[]"](); }
  else { return v["_↦_∷_"](x.key(),x.value(),x.tail(),null,x.tail()); }
} #-}
{-# COMPILED_JS [] require("agda.object").iempty() #-}
{-# COMPILED_JS _↦_∷_ function(k) { return function(a) {
  return function () { return function() { return function(as) {
    return as.set(k,a);
}; }; }; }; } #-}

ikeys : ∀ {α A ks ks✓} → IObject {α} A ks ks✓ → IKeys
ikeys {ks = ks} as = ks

ikeys✓ : ∀ {α A ks ks✓} as → True (sorted (ikeys {α} {A} {ks} {ks✓} as))
ikeys✓ {ks✓ = ks✓} as = ks✓

record Object {α} (A : Set α) : Set α where
  constructor object
  field
    {keys} : Keys
    iobject : IObject A (ikeysk keys) (ikeysk✓ keys)

open Object public

{-# COMPILED_JS Object function(x,v) {
  return v.object(require("agda.object").keys(x),require("agda.object").iobject(x));
} #-}
{-# COMPILED_JS object function() { return function(as) { return as.object(); }; } #-}
{-# COMPILED_JS keys function() { return function() { return require("agda.object").keys; }; } #-}
{-# COMPILED_JS iobject function() { return function() { return require("agda.object").iobject; }; } #-}

open Object public

⟪⟫ : ∀ {α A} → Object {α} A
⟪⟫ = object []

{-# COMPILED_JS ⟪⟫ function() { return function() { return {}; }; } #-}

ilookup? : ∀ {α A ks ks✓} → IObject {α} A ks ks✓ → String → Maybe A
ilookup? [] l = nothing
ilookup? (k ↦ a ∷ as) l
 with k ≟ l
... | true  = just a
... | false
 with k < l
... | true  = ilookup? as l
... | false = nothing

lookup? : ∀ {α A} → Object {α} A → String → Maybe A
lookup? (object as) l = ilookup? as l

{-# COMPILED_JS lookup? function() { return function() { return function(as) { return function(l) {
  return require("agda.box").box(require("agda.object").lookup(as,l));
}; }; }; } #-}

ilookup : ∀ {α A ks ks✓} → IObject {α} A ks ks✓ → ∀ l → {l∈ks : True (l ∈i ks)} → A
ilookup [] l {l∈[]} = contradiction l∈[]
ilookup (k ↦ a ∷ as) l {l∈k∷ks}
 with k ≟ l
... | true  = a
... | false
 with k < l
... | true  = ilookup as l {l∈k∷ks}
... | false = contradiction l∈k∷ks

lookup : ∀ {α A} as l → {l∈ks : True (l ∈ keys {α} {A} as)} → A
lookup (object as) l {l∈ks} = ilookup as l {l∈ks}

{-# COMPILED_JS lookup function() { return function() { return function(as) { return function(l) { return function() {
  return require("agda.object").lookup(as,l);
}; }; }; }; } #-}

imap : ∀ {α β A B} → (String → A → B) → ∀ {ks ks✓} → IObject {α} A ks ks✓ → IObject {β} B ks ks✓
imap f []           = []
imap f (k ↦ a ∷ as) = (k ↦ f k a ∷ imap f as)

mapi : ∀ {α β A B} → (String → A → B) → Object {α} A → Object {β} B
mapi f (object as) = object (imap f as)

map : ∀ {α β A B} → (A → B) → Object {α} A → Object {β} B
map f = mapi (λ s → f)

{-# COMPILED_JS mapi function() { return function() { return function() { return function() {
  return function(f) { return function(as) {
    return require("agda.object").map(function(a,s) { return f(s)(a); },as);
  }; };
}; }; }; } #-}

{-# COMPILED_JS map function() { return function() { return function() { return function() {
  return function(f) { return function(as) {
    return require("agda.object").map(f,as);
  }; };
}; }; }; } #-}

iall : ∀ {α A} → (String → A → Bool) → ∀ {ks ks✓} → IObject {α} A ks ks✓ → Bool
iall f []           = true
iall f (k ↦ a ∷ as) = f k a ∧ iall f as

alli : ∀ {α A} → (String → A → Bool) → Object {α} A → Bool
alli f (object as) = iall f as

all : ∀ {α A} → (A → Bool) → Object {α} A → Bool
all f = alli (λ s → f)

{-# COMPILED_JS alli function() { return function() {
  return function(f) { return function(as) {
    return require("agda.object").all(function(a,s) { return f(s)(a); },as);
  }; };
}; } #-}

{-# COMPILED_JS all function() { return function() {
  return function(f) { return function(as) {
    return require("agda.object").all(f,as);
  }; };
}; } #-}

must : ∀ {α A} → (A → Bool) → (Maybe {α} A → Bool)
must p nothing  = false
must p (just a) = p a

_⊆[_]_ : ∀ {α β A B} → Object {α} A → (A → B → Bool) → Object {β} B → Bool
as ⊆[ p ] bs = alli (λ k a → must (p a) (lookup? bs k)) as

_≟[_]_ : ∀ {α β A B} → Object {α} A → (A → B → Bool) → Object {β} B → Bool
as ≟[ p ] bs = (as ⊆[ p ] bs) ∧ (bs ⊆[(λ a b → true)] as)

kfilter : ∀ {α A} → (String → A → Bool) → ∀ {ks ks✓} → IObject {α} A ks ks✓ → IKeys
kfilter f []           = []k
kfilter f (k ↦ a ∷ as)
 with f k a
... | true  = k ∷k kfilter f as
... | false = kfilter f as

<?-trans : ∀ {k l m} → True (k < l) → True (l <? m) → True (k <? m)
<?-trans {k} {l} {nothing} k<l l<m = tt
<?-trans {k} {l} {just m}  k<l l<m = <-trans {k} {l} {m} k<l l<m

kfilter-<? : ∀ {α A} f {ks ks✓} as k → True (k <? head ks) →
  True (k <? head (kfilter {α} {A} f {ks} {ks✓} as))
kfilter-<? f [] k tt = tt
kfilter-<? f {ks✓ = l∷ls✓} (l ↦ a ∷ as) k k<l
 with f l a
... | true  = k<l
... | false = kfilter-<? f as k (<?-trans {m = head (ikeys as)} k<l (∧-elim₁ l∷ls✓))

kfilter✓ : ∀ {α A} f {ks ks✓} as → True (sorted (kfilter {α} {A} f {ks} {ks✓} as))
kfilter✓ f [] = tt
kfilter✓ f {ks✓ = k∷ks✓} (k ↦ a ∷ as)
 with f k a
... | true  = ∧-intro (kfilter-<? f as k (∧-elim₁ k∷ks✓)) (kfilter✓ f as)
... | false = kfilter✓ f as

ifilter : ∀ {α A} f {ks ks✓} as → ∀ {ls✓} → IObject A (kfilter {α} {A} f {ks} {ks✓} as) ls✓
ifilter f [] = []
ifilter f (k ↦ a ∷ as)
 with f k a
... | true  = (k ↦ a ∷ ifilter f as)
... | false = ifilter f as

filteri : ∀ {α} {A} → (String → A → Bool) → Object {α} A → Object A
filteri f (object as) = object (ifilter f as {kfilter✓ f as})

filter : ∀ {α} {A} → (A → Bool) → Object {α} A → Object A
filter f = filteri (λ k → f)

{-# COMPILED_JS filteri function() { return function() {
  return function(p) { return function(as) {
    return require("agda.object").filter(function(a,s) { return p(s)(a); },as);
  }; };
}; } #-}

{-# COMPILED_JS filter function() { return function() {
  return function(p) { return function(as) {
    return require("agda.object").filter(p,as);
  }; };
}; } #-}

-- Syntax sugar, e.g. ⟪ "a" ↦ 1 , "b" ↦ 2 , "c" ↦ 3 ⟫ : Object ℕ

infix 3 ⟪_
infixr 4 _↦_,_ _↦_⟫

data Sugar {α} (A : Set α) : Set α where
  ε : Sugar A
  _↦_,_ : String → A → Sugar A → Sugar A

_↦_⟫ : ∀ {α A} → String → A → Sugar {α} A
k ↦ a ⟫ = (k ↦ a , ε)

skeys : ∀ {α A} → Sugar {α} A → IKeys
skeys ε            = []k
skeys (k ↦ a , as) = k ∷k skeys as

desugar : ∀ {α A} as {ks✓} → IObject A (skeys {α} {A} as) ks✓
desugar ε            = []
desugar (k ↦ a , as) = k ↦ a ∷ desugar as

⟪_ : ∀ {α A} as → {ks✓ : True (sorted (skeys {α} {A} as))} → Object A
⟪_ as {ks✓} = object {keys = kkeys (skeys as) {ks✓}} (desugar as)

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
open import Web.Semantic.DL.ABox.Interp using ( _*_ )
open import Web.Semantic.DL.Category.Object using ( Object )
open import Web.Semantic.DL.Category.Morphism using ( _⇒_ ; _≣_ ; _⊑_ ; _,_ )
open import Web.Semantic.DL.Category.Composition using ( _∙_ )
open import Web.Semantic.DL.Category.Properties.Composition.Lemmas using
  ( compose-left ; compose-mid ; compose-right ; compose-resp-⊨b )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox using ( TBox )
open import Web.Semantic.Util using ( left ; right )

module Web.Semantic.DL.Category.Properties.Composition.RespectsEquiv
  {Σ : Signature} {S T : TBox Σ} where

compose-resp-⊑ : ∀ {A B C : Object S T} (F₁ F₂ : A ⇒ B) (G₁ G₂ : B ⇒ C) →
  (F₁ ⊑ F₂) → (G₁ ⊑ G₂) → (F₁ ∙ G₁ ⊑ F₂ ∙ G₂)
compose-resp-⊑ F₁ F₂ G₁ G₂ F₁⊑F₂ G₁⊑G₂ I I⊨STA I⊨F₁⟫G₁ =
  compose-resp-⊨b F₂ G₂ I
    (F₁⊑F₂ (left * I) I⊨STA
      (compose-left F₁ G₁ I I⊨F₁⟫G₁))
    (G₁⊑G₂ (right * I) (compose-mid F₁ G₁ I I⊨STA I⊨F₁⟫G₁)
      (compose-right F₁ G₁ I I⊨F₁⟫G₁))

compose-resp-≣ : ∀ {A B C : Object S T} {F₁ F₂ : A ⇒ B} {G₁ G₂ : B ⇒ C} →
  (F₁ ≣ F₂) → (G₁ ≣ G₂) → (F₁ ∙ G₁ ≣ F₂ ∙ G₂)
compose-resp-≣ {A} {B} {C} {F₁} {F₂} {G₁} {G₂}
  (F₁⊑F₂ , F₂⊑F₁) (G₁⊑G₂ , G₂⊑G₁) =
    ( compose-resp-⊑ F₁ F₂ G₁ G₂ F₁⊑F₂ G₁⊑G₂
    , compose-resp-⊑ F₂ F₁ G₂ G₁ F₂⊑F₁ G₂⊑G₁ )

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
module Issue328 where

mutual

  postulate D : Set

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/Syntax/Concrete/Definitions.hs:398

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Elem where

open import Prelude
open import Star

Elem : {X : Set}(R : Rel X) -> Rel X
Elem R x y = Star (LeqBool [×] R) (false , x) (true , y)


text:
module Test where

open import LF
open import IID

-- r←→gArgs-subst eliminates the identity proof stored in the rArgs. If this proof is
-- by reflexivity r←→gArgs-subst is a definitional identity. This is the case
-- when a = g→rArgs a'
r←→gArgs-subst-identity :
  {I  : Set}(γ : OPg I)(U : I -> Set)
  (C  : (i : I) -> rArgs (ε γ) U i -> Set)
  (a' : Args γ U) ->
  let a = g→rArgs γ U a'
      i = index γ U a' in
  (h : C (index γ U (r→gArgs γ U i a))
	 (g→rArgs γ U (r→gArgs γ U i a))
  ) -> r←→gArgs-subst γ U C i a h ≡ h
r←→gArgs-subst-identity (ι i)	  U C _   h = refl-≡
r←→gArgs-subst-identity (σ A γ)	  U C arg h = r←→gArgs-subst-identity (γ (π₀ arg)) U C' (π₁ arg) h
  where C' = \i c -> C i (π₀ arg , c)
r←→gArgs-subst-identity (δ H i γ) U C arg h = r←→gArgs-subst-identity γ U C' (π₁ arg) h
  where C' = \i c -> C i (π₀ arg , c)

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module Erased-cubical.Without-K where

data D : Set where
  c : D


text:
open import Everything

module Test.Functor where

List = List⟨_⟩

module _
  {a b} {A : Set a} {B : Set b}
  where

  map-list : (A → B) → List A → List B
  map-list f ∅ = ∅
  map-list f (x , xs) = f x , map-list f xs

instance

  SurjtranscommutativityList : ∀ {ℓ} → Surjtranscommutativity.class Function⟦ ℓ ⟧ (MFunction List) _≡̇_ map-list transitivity transitivity
  SurjtranscommutativityList .⋆ f g ∅ = ∅
  SurjtranscommutativityList .⋆ f g (x , xs) rewrite SurjtranscommutativityList .⋆ f g xs = ∅

  SurjextensionalityList : ∀ {ℓ} → Surjextensionality.class Function⟦ ℓ ⟧ _≡̇_ (MFunction List) _≡̇_ _ map-list
  SurjextensionalityList .⋆ _ _ f₁ f₂ f₁≡̇f₂ ∅ = ∅
  SurjextensionalityList .⋆ _ _ f₁ f₂ f₁≡̇f₂ (x , xs) rewrite SurjextensionalityList .⋆ _ _ f₁ f₂ f₁≡̇f₂ xs | f₁≡̇f₂ x = ∅

  SurjidentityList : ∀ {ℓ} → Surjidentity.class Function⟦ ℓ ⟧ (MFunction List) _≡̇_ map-list ε ε
  SurjidentityList .⋆ ∅ = ∅
  SurjidentityList .⋆ (x , xs) rewrite SurjidentityList .⋆ xs = ∅

test-isprecategory-1 : ∀ {ℓ} → IsPrecategory {𝔒 = Ø ℓ} Function⟦ ℓ ⟧ _≡̇_ (flip _∘′_)
test-isprecategory-1 {ℓ} = IsPrecategoryExtension {A = Ø ℓ} {B = ¡}

test-isprecategory-2 : ∀ {ℓ} → IsPrecategory {𝔒 = Ø ℓ} Function⟦ ℓ ⟧ _≡̇_ (flip _∘′_)
test-isprecategory-2 {ℓ} = IsPrecategoryFunction {𝔬 = ℓ}

test-isprecategory-1a : ∀ {ℓ} → IsPrecategory {𝔒 = Ø ℓ} (Extension (¡ {𝔒 = Ø ℓ})) _≡̇_ (flip _∘′_)
test-isprecategory-1a {ℓ} = IsPrecategoryExtension {A = Ø ℓ} {B = ¡}

test-isprecategory-2a : ∀ {ℓ} → IsPrecategory {𝔒 = Ø ℓ} (Extension (¡ {𝔒 = Ø ℓ})) _≡̇_ (flip _∘′_)
test-isprecategory-2a {ℓ} = IsPrecategoryFunction {𝔬 = ℓ}

test-isprecategory-1b : IsPrecategory {𝔒 = ¶} (Extension (Term.Term ¶)) _≡̇_ (flip _∘′_)
test-isprecategory-1b = IsPrecategoryExtension {A = ¶} {B = Term.Term ¶}

-- test-isprecategory-2b : IsPrecategory {𝔒 = ¶} (Extension (Term.Term ¶)) _≡̇_ (flip _∘′_)
-- test-isprecategory-2b = {!!} -- IsPrecategoryFunction {𝔬 = ?}

instance

  HmapList : ∀ {a} → Hmap.class Function⟦ a ⟧ (MFunction List)
  HmapList = ∁ λ _ _ → map-list

instance

  isPrefunctorList : ∀ {ℓ} → IsPrefunctor (λ (x y : Ø ℓ) → x → y)
                                          Proposextensequality
                                          transitivity
                                          (λ (x y : Ø ℓ) → List x → List y)
                                          Proposextensequality
                                          transitivity
                                          smap
  isPrefunctorList = ∁

  isFunctorList : ∀ {ℓ} → IsFunctor (λ (x y : Ø ℓ) → x → y)
                                    Proposextensequality
                                    ε
                                    transitivity
                                    (λ (x y : Ø ℓ) → List x → List y)
                                    Proposextensequality
                                    ε
                                    transitivity
                                    smap
  isFunctorList = ∁

instance

  FmapList : ∀ {ℓ} → Fmap (List {ℓ})
  FmapList = ∁ smap

module _
  {a} {A : Set a} {B : Set a}
  where
  test-smap-list : (A → B) → List A → List B
  test-smap-list = smap

module _
  {a} {A : Set a} {B : Set a}
  where
  test-fmap-list : (A → B) → List A → List B
  test-fmap-list = fmap -- the intention here is to try to say "I want to invoke a functoral mapping, so that I can be sure that, for example, that `test-map-list ε₁ ≡ ε₂`.


text:
module Imports.Test where

open import Common.Level

record Foo (ℓ : Level) : Set ℓ where


text:
-- {-# OPTIONS -v scope:10 -v scope.inverse:100 #-}

open import Common.Equality
open import A.Issue1635 Set

test : ∀ x → x ≡ foo
test x = refl

-- ERROR:
-- x != .#A.Issue1635-225351734.foo of type Foo
-- when checking that the expression refl has type x ≡ foo

-- SLIGHTLY BETTER:
-- x != .A.Issue1635.Foo.foo of type Foo
-- when checking that the expression refl has type x ≡ foo

-- WANT: x != foo ...

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Generics.Prelude hiding (lookup)
open import Generics.Telescope
open import Generics.Desc
open import Generics.HasDesc

module Generics.Constructions.Case
  {P I ℓ} {A : Indexed P I ℓ}
  (H : HasDesc A) (open HasDesc H)
  {p c} (Pr : Pred′ I λ i → A′ (p , i) → Set c)
  where

private
  variable
    V : ExTele P
    i : ⟦ I ⟧tel p
    v : ⟦ V ⟧tel p

Pr′ : A′ (p , i) → Set c
Pr′ {i} = unpred′ I _ Pr i

--------------------------
-- Types of motives

levelCase : ConDesc P V I → Level
levelCase (var x) = c
levelCase (π {ℓ′} _ _ C) = ℓ′ ⊔ levelCase C
levelCase (A ⊗ B) = levelIndArg A ℓ ⊔ levelCase B

MotiveCon : (C : ConDesc P V I)
          → (∀ {i} → ⟦ C ⟧Con A′ (p , v , i) → Set c)
          → Set (levelCase C)
MotiveCon (var γ) X = X refl
MotiveCon (π ia S C) X = Π< ia > (S _) λ s → MotiveCon C (X ∘ (s ,_))
MotiveCon (A ⊗ B) X = (x : ⟦ A ⟧IndArg A′ (p , _))
                    → MotiveCon B (X ∘ (x ,_))

Motives : ∀ k → Set (levelCase (lookupCon D k))
Motives k = MotiveCon (lookupCon D k) (λ x → Pr′ (constr (k , x)))

--------------------------
-- Case-analysis principle

module _ (methods : Els Motives) where

  caseData : ∀ {i} → (x : ⟦ D ⟧Data A′ (p , i)) → Pr′ (constr x)
  caseData (k , x) = caseCon (lookupCon D k) (methods k) x
    where
      caseCon
        : (C   : ConDesc P V I)
          {mk  : ∀ {i} → ⟦ C ⟧Con A′ (p , v , i) → ⟦ D ⟧Data A′ (p , i)}
          (mot : MotiveCon C λ x → Pr′ (constr (mk x)))
          (x   : ⟦ C ⟧Con A′ (p , v , i))
        → Pr′ (constr (mk x))
      caseCon (var γ) mot refl = mot
      caseCon (π ia _ C) mot (s , x) = caseCon C (app< ia > mot s) x
      caseCon (A ⊗ B) mot (a , b) = caseCon B (mot a) b

  case : (x : A′ (p , i)) → Pr′ x
  case x = subst Pr′ (constr∘split x) (caseData (split x))

deriveCase : Arrows Motives (Pred′ I (λ i → (x : A′ (p , i)) → Pr′ x))
deriveCase = curryₙ (λ m → pred′ I _ λ i → case m)

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

P : Bool → Set
P true  = Bool
P false = Bool

f : (b : Bool) → P b
f true  = true
f false = false

pattern varg x = arg (arg-info visible relevant) x

create-constraint : TC Set
create-constraint =
  unquoteTC (def (quote P)
               (varg (def (quote f) (varg unknown ∷ [])) ∷ []))

macro

  should-fail : Term → TC ⊤
  should-fail _ =
    bindTC (noConstraints create-constraint) λ _ →
    returnTC tt

test : ⊤
test = should-fail


text:
module Numeric.Nat.LCM.Properties where

open import Prelude
open import Numeric.Nat.Divide
open import Numeric.Nat.Divide.Properties
open import Numeric.Nat.LCM

is-lcm-unique : ∀ {m m₁ a b} → IsLCM m a b → IsLCM m₁ a b → m ≡ m₁
is-lcm-unique {m} {m₁} (is-lcm a|m b|m lm) (is-lcm a|m₁ b|m₁ lm₁) =
  divides-antisym (lm m₁ a|m₁ b|m₁) (lm₁ m a|m b|m)

lcm-unique : ∀ {m a b} → IsLCM m a b → lcm! a b ≡ m
lcm-unique {a = a} {b} lm with lcm a b
... | lcm-res m₁ lm₁ = is-lcm-unique lm₁ lm

is-lcm-commute : ∀ {m a b} → IsLCM m a b → IsLCM m b a
is-lcm-commute (is-lcm a|m b|m g) = is-lcm b|m a|m (flip ∘ g)

lcm-commute : ∀ {a b} → lcm! a b ≡ lcm! b a
lcm-commute {a} {b} with lcm b a
... | lcm-res m lm = lcm-unique (is-lcm-commute lm)

private
  _|>_ = divides-trans

lcm-assoc : ∀ a b c → lcm! a (lcm! b c) ≡ lcm! (lcm! a b) c
lcm-assoc a b c with lcm a b | lcm b c
... | lcm-res ab (is-lcm a|ab b|ab lab)
    | lcm-res bc (is-lcm b|bc c|bc lbc) with lcm ab c
...    | lcm-res ab-c (is-lcm ab|abc c|abc labc) =
  lcm-unique {ab-c} {a} {bc}
    (is-lcm (a|ab |> ab|abc)
            (lbc ab-c (b|ab |> ab|abc) c|abc)
            λ k a|k bc|k → labc k (lab k a|k (b|bc |> bc|k)) (c|bc |> bc|k))

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
{-# OPTIONS --without-K #-}
module function.extensionality.computation where

open import equality
open import function.isomorphism
open import function.core
open import function.extensionality.core
open import function.extensionality.proof
open import function.extensionality.strong

funext-inv-hom : ∀ {i j}{X : Set i}{Y : X → Set j}
               → {f₁ f₂ f₃ : (x : X) → Y x}
               → (p₁ : f₁ ≡ f₂)
               → (p₂ : f₂ ≡ f₃)
               → funext-inv (p₁ · p₂)
               ≡ (λ x → funext-inv p₁ x · funext-inv p₂ x)
funext-inv-hom refl p₂ = refl

funext-hom : ∀ {i j}{X : Set i}{Y : X → Set j}
           → {f₁ f₂ f₃ : (x : X) → Y x}
           → (h₁ : (x : X) → f₁ x ≡ f₂ x)
           → (h₂ : (x : X) → f₂ x ≡ f₃ x)
           → funext (λ x → h₁ x · h₂ x)
           ≡ funext h₁ · funext h₂
funext-hom h₁ h₂ = begin
    funext (λ x → h₁ x · h₂ x)
  ≡⟨ sym (ap funext (ap₂ (λ u v x → u x · v x)
                         (_≅_.iso₁ strong-funext-iso h₁)
                         (_≅_.iso₁ strong-funext-iso h₂))) ⟩
    funext (λ x → funext-inv (funext h₁) x · funext-inv (funext h₂) x)
  ≡⟨ sym (ap funext (funext-inv-hom (funext h₁) (funext h₂))) ⟩
    funext (funext-inv (funext h₁ · funext h₂))
  ≡⟨ _≅_.iso₂ strong-funext-iso (funext h₁ · funext h₂) ⟩
    funext h₁ · funext h₂
  ∎
  where open ≡-Reasoning

funext-inv-ap : ∀ {i j k}{X : Set i}{Y : X → Set j}{Z : X → Set k}
              → (g : {x : X} → Y x → Z x)
              → {f₁ f₂ : (x : X) → Y x}
              → (p : f₁ ≡ f₂)
              → funext-inv (ap (_∘'_ g) p)
              ≡ ((λ x → ap g (funext-inv p x)))
funext-inv-ap g refl = refl

funext-ap : ∀ {i j k}{X : Set i}{Y : X → Set j}{Z : X → Set k}
          → (g : {x : X} → Y x → Z x)
          → {f₁ f₂ : (x : X) → Y x}
          → (h : (x : X) → f₁ x ≡ f₂ x)
          → funext (λ x → ap g (h x))
          ≡ ap (_∘'_ g) (funext h)
funext-ap g h = begin
    funext (λ x → ap g (h x))
  ≡⟨ sym (ap funext (ap (λ h x → ap g (h x))
                    (_≅_.iso₁ strong-funext-iso h))) ⟩
    funext (λ x → ap g (funext-inv (funext h) x))
  ≡⟨ ap funext (sym (funext-inv-ap g (funext h))) ⟩
    funext (funext-inv (ap (_∘'_ g) (funext h)))
  ≡⟨ _≅_.iso₂ strong-funext-iso _ ⟩
    ap (_∘'_ g) (funext h)
  ∎
  where open ≡-Reasoning

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
module trie where

open import string
open import maybe
open import trie-core public
open import empty

trie-lookup : ∀{A : Set} → trie A → string → maybe A
trie-lookup t s = trie-lookup-h t (string-to-𝕃char s)

trie-insert : ∀{A : Set} → trie A → string → A → trie A
trie-insert t s x = trie-insert-h t (string-to-𝕃char s) x

trie-remove : ∀{A : Set} → trie A → string → trie A
trie-remove t s = trie-remove-h t (string-to-𝕃char s)

open import trie-functions trie-lookup trie-insert trie-remove public

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
module Everything where

-- Categories
import Categories.Category

-- 2-categories
-- XXX need to finish the last 3 laws
import Categories.2-Category

-- The strict 2-category of categories
-- XXX laws not proven yet
-- import Categories.2-Category.Categories

-- Adjunctions between functors
import Categories.Adjunction

-- The Agda Set category
import Categories.Agda

-- The fact that one version of it is cocomplete
import Categories.Agda.ISetoids.Cocomplete

-- The arrow category construction on any category
import Categories.Arrow

-- Bifunctors (functors from a product category)
import Categories.Bifunctor

-- Natural transformations between bifunctors
import Categories.Bifunctor.NaturalTransformation

-- The category of (small) categories
import Categories.Categories

-- Cat has products
import Categories.Categories.Products

-- Closed categories
import Categories.Closed

-- Cocones
import Categories.Cocone

-- The category of cocones under a diagram (functor)
import Categories.Cocones

-- Coends
import Categories.Coend

-- Coequalizers
import Categories.Coequalizer

-- Colimits
import Categories.Colimit

-- Comma categories
import Categories.Comma

-- Comonads, defined directly (not as monads on the opposite category)
import Categories.Comonad

-- The cofree construction that gives a comonad for any functor
import Categories.Comonad.Cofree

-- Cones
import Categories.Cone

-- The category of cones over a diagram (functor)
import Categories.Cones

-- A coherent equivalence relation over the objects of a category
import Categories.Congruence

-- Discrete categories (they only have objects and identity morphisms)
import Categories.Discrete

-- Ends
import Categories.End

-- Enriched categories
import Categories.Enriched

-- Equalizers
import Categories.Equalizer

-- Strong equivalence
import Categories.Equivalence.Strong

-- Fibrations
import Categories.Fibration

-- Free category on a graph
import Categories.Free

-- The free category construction is a functor from Gph to Cat
import Categories.Free.Functor

-- Functors
import Categories.Functor

-- F-algebra (TODO: maybe the module should be renamed)
import Categories.Functor.Algebra

-- The category of F-algebras of a functor
import Categories.Functor.Algebras

-- An F-coalgebra
import Categories.Functor.Coalgebra

-- Constant functor
import Categories.Functor.Constant

-- The category of F-coalgebras of a functor
import Categories.Functor.Coalgebras

-- The diagonal functor (C → C × C, or same thing with an arbitrary indexed product)
import Categories.Functor.Diagonal

-- Strong functor equivalence
-- XXX doesn't seem to work because of the double negative in Full?
-- import Categories.Functor.Equivalence.Strong

-- The hom functor, mapping pairs of objects to the morphisms between them
import Categories.Functor.Hom

-- Monoidal functors (similar to Haskell's Applicative class)
import Categories.Functor.Monoidal

-- Products as functors
import Categories.Functor.Product

-- Properties of general functors
import Categories.Functor.Properties

-- Representable functors
import Categories.Functor.Representable

-- Functor categories (of functors between two categories and natural transformations between them)
import Categories.FunctorCategory

-- The category of graphs and graph homomorphisms (Gph)
import Categories.Graphs

-- The underlying graph of a category (forgetful functor Cat ⇒ Gph)
import Categories.Graphs.Underlying

-- The Grothendieck construction on categories (taking a Sets-valued functor and building a category containing all values)
import Categories.Grothendieck

-- The globe category, used for defining globular sets (with a presheaf on it)
import Categories.Globe

-- Globular sets
import Categories.GlobularSet

-- Left Kan extensions
import Categories.Lan

-- Small categories exist as large categories too
import Categories.Lift

-- Limits
import Categories.Limit

-- Monads, defined as simple triples of a functor and two natural transformations
import Categories.Monad

-- A monad algebra
import Categories.Monad.Algebra

-- The category of all algebras of a monad
import Categories.Monad.Algebras

-- The Eilenberg-Moore category for any monad
import Categories.Monad.EilenbergMoore

-- The Kleisli category for any monad
import Categories.Monad.Kleisli

-- Strong monads
import Categories.Monad.Strong

-- Monoidal categories, with an associative bi(endo)functor and an identity object
import Categories.Monoidal

-- A braided monoidal category (one that gives you a swap operation, but isn't quite commutative)
import Categories.Monoidal.Braided

-- A cartesian monoidal category (monoidal category whose monoid is the product with a terminal object)
import Categories.Monoidal.Cartesian

-- Closed monoidal categories, which are simply monoidal categories that are
-- also closed, such that the laws "fit"
import Categories.Monoidal.Closed

-- Both of the above. Separated into its own module because we can do many
-- interesting things with them.
import Categories.Monoidal.CartesianClosed

-- Simple definitions about morphisms, such as mono, epi, and iso
import Categories.Morphisms

-- Cartesian morphisms (used mostly for fibrations)
import Categories.Morphism.Cartesian

-- Families of morphisms indexed by a set
import Categories.Morphism.Indexed

-- Natural isomorphisms, defined as an isomorphism of natural transformations
import Categories.NaturalIsomorphism

-- Natural transformations
import Categories.NaturalTransformation

import Categories.DinaturalTransformation

-- Properties of the opposite category
import Categories.Opposite

--------------------------------------------------------------------------------
-- Objects
--------------------------------------------------------------------------------

-- The coproduct of two objects
import Categories.Object.Coproduct

-- A category has all binary coproducts
import Categories.Object.BinaryCoproducts

-- A category has all finite coproducts
import Categories.Object.Coproducts

-- An exponential object
import Categories.Object.Exponential

-- A choice of B^A for a given B and any A
import Categories.Object.Exponentiating

-- B^— is adjoint to its opposite
import Categories.Object.Exponentiating.Adjunction

-- B^— as a functor
import Categories.Object.Exponentiating.Functor

-- A family of objects indexed by a set
import Categories.Object.Indexed

-- An initial object
import Categories.Object.Initial

-- The product of two objects
import Categories.Object.Product

-- The usual nice constructions on products, conditionalized on existence
import Categories.Object.Product.Morphisms

-- All binary products
import Categories.Object.BinaryProducts

-- Products of a nonempty list of objects and the ability to reassociate them massively
import Categories.Object.BinaryProducts.N-ary

-- All finite products
import Categories.Object.Products
import Categories.Object.Products.Properties

-- Products of a list of objects and the ability to reassociate them massively
import Categories.Object.Products.N-ary

-- The product of a family of objects
import Categories.Object.IndexedProduct

-- All products of indexed families
import Categories.Object.IndexedProducts

-- Subobject classifiers (for topoi)
import Categories.Object.SubobjectClassifier

-- Terminal object
import Categories.Object.Terminal

-- A^1 and 1^A always exist
import Categories.Object.Terminal.Exponentials

-- A chosen 1^A exists
import Categories.Object.Terminal.Exponentiating

-- A×1 always exists
import Categories.Object.Terminal.Products

-- Zero object (initial and terminal)
import Categories.Object.Zero

-- A category containing n copies of objects/morphisms/equalities of another category
import Categories.Power

-- Demonstrations that Power categories are the same as functors from discrete categories
import Categories.Power.Functorial

-- Natural transformations for functors to/from power categories
import Categories.Power.NaturalTransformation

-- A preorder gives rise to a category
import Categories.Preorder

-- A presheaf (functor from C^op to V)
import Categories.Presheaf

-- The category of presheaves (a specific functor category)
import Categories.Presheaves

-- The product of two categories
import Categories.Product
import Categories.Product.Properties

-- Projection functors from a product category to its factors
import Categories.Product.Projections

-- Profunctors
import Categories.Profunctor

-- Pullbacks in a category
import Categories.Pullback

-- Pushouts in a category
import Categories.Pushout

-- All categories can have a slice category defined on them
import Categories.Slice

-- Utilities for gluing together commutative squares (and triangles)
-- (and other common patterns of equational reasoning)
import Categories.Square

-- The terminal category (a terminal object in the category of small categories)
import Categories.Terminal

-- A topos
import Categories.Topos

-- The Yoneda lemma
import Categories.Yoneda

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
open import Common.Prelude

module TestHarness where

record ⊤ : Set where

data ⊥ : Set where

T : Bool → Set
T true  = ⊤
T false = ⊥

infixr 4 _,_

data Asserts : Set where
  ε : Asserts
  _,_ : Asserts → Asserts → Asserts
  assert : (b : Bool) → {b✓ : T b} → String → Asserts

Tests : Set
Tests = ⊤ → Asserts


text:
open import Agda.Builtin.Coinduction
open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Nat

infixr 5 _∷_

data Stream (A : Set) : Set where
  _∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A

head : ∀ {A} → Stream A → A
head (x ∷ xs) = x

tail : ∀ {A} → Stream A → Stream A
tail (x ∷ xs) = ♭ xs

take : ∀ {A} n → Stream A → List A
take zero    xs       = []
take (suc n) (x ∷ xs) = x ∷ take n (♭ xs)

accepted : ∀ {A} {n} (xs : Stream A) →
           take (suc n) xs ≡ take (suc n) (head xs ∷ ♯ tail xs)
accepted (x ∷ xs) = refl

private
  rejected : ∀ {A} {n} (xs : Stream A) →
             take (suc n) xs ≡ take (suc n) (head xs ∷ ♯ tail xs)
  rejected (x ∷ xs) = refl

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


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

open import lib.Basics
open import lib.types.Pi
open import lib.types.TwoSemiCategory
open import lib.two-semi-categories.Functor

module lib.two-semi-categories.FunCategory where

module _ {i j k} (A : Type i) (G : TwoSemiCategory j k) where

  private
    module G = TwoSemiCategory G

  fun-El : Type (lmax i j)
  fun-El = A → G.El

  fun-Arr : fun-El → fun-El → Type (lmax i k)
  fun-Arr F G = ∀ a → G.Arr (F a) (G a)

  fun-Arr-level : (F G : fun-El) → has-level 1 (fun-Arr F G)
  fun-Arr-level F G = Π-level (λ a → G.Arr-level (F a) (G a))

  fun-comp : {F G H : fun-El} (α : fun-Arr F G) (β : fun-Arr G H)
    → fun-Arr F H
  fun-comp α β a = G.comp (α a) (β a)

  fun-assoc : {F G H I : fun-El} (α : fun-Arr F G) (β : fun-Arr G H) (γ : fun-Arr H I)
    → fun-comp (fun-comp α β) γ == fun-comp α (fun-comp β γ)
  fun-assoc α β γ = λ= (λ a → G.assoc (α a) (β a) (γ a))

  abstract
    fun-pentagon : {F G H I J : fun-El}
      (α : fun-Arr F G) (β : fun-Arr G H) (γ : fun-Arr H I) (δ : fun-Arr I J)
      → fun-assoc (fun-comp α β) γ δ ◃∙
        fun-assoc α β (fun-comp γ δ) ◃∎
        =ₛ
        ap (λ s → fun-comp s δ) (fun-assoc α β γ) ◃∙
        fun-assoc α (fun-comp β γ) δ ◃∙
        ap (fun-comp α) (fun-assoc β γ δ) ◃∎
    fun-pentagon α β γ δ =
      fun-assoc (fun-comp α β) γ δ ◃∙
      fun-assoc α β (fun-comp γ δ) ◃∎
        =ₛ⟨ ∙-λ= (λ a → G.assoc (G.comp (α a) (β a)) (γ a) (δ a))
                 (λ a → G.assoc (α a) (β a) (G.comp (γ a) (δ a))) ⟩
      λ= (λ a → G.assoc (G.comp (α a) (β a)) (γ a) (δ a) ∙
                G.assoc (α a) (β a) (G.comp (γ a) (δ a))) ◃∎
        =ₛ₁⟨ ap λ= (λ= (λ a → =ₛ-out (G.pentagon-identity (α a) (β a) (γ a) (δ a)))) ⟩
      λ= (λ a → ap (λ s → G.comp s (δ a)) (G.assoc (α a) (β a) (γ a)) ∙
                G.assoc (α a) (G.comp (β a) (γ a)) (δ a) ∙
                ap (G.comp (α a)) (G.assoc (β a) (γ a) (δ a))) ◃∎
        =ₛ⟨ λ=-∙∙ (λ a → ap (λ s → G.comp s (δ a)) (G.assoc (α a) (β a) (γ a)))
                  (λ a → G.assoc (α a) (G.comp (β a) (γ a)) (δ a))
                  (λ a → ap (G.comp (α a)) (G.assoc (β a) (γ a) (δ a))) ⟩
      λ= (λ a → ap (λ s → G.comp s (δ a)) (G.assoc (α a) (β a) (γ a))) ◃∙
      fun-assoc α (fun-comp β γ) δ ◃∙
      λ= (λ a → ap (G.comp (α a)) (G.assoc (β a) (γ a) (δ a))) ◃∎
        =ₛ₁⟨ 0 & 1 & ! (λ=-ap (λ a s → G.comp s (δ a)) (λ a → G.assoc (α a) (β a) (γ a))) ⟩
      ap (λ s → fun-comp s δ) (fun-assoc α β γ) ◃∙
      fun-assoc α (fun-comp β γ) δ ◃∙
      λ= (λ a → ap (G.comp (α a)) (G.assoc (β a) (γ a) (δ a))) ◃∎
        =ₛ₁⟨ 2 & 1 & ! (λ=-ap (λ a → G.comp (α a)) (λ a → G.assoc (β a) (γ a) (δ a))) ⟩
      ap (λ s → fun-comp s δ) (fun-assoc α β γ) ◃∙
      fun-assoc α (fun-comp β γ) δ ◃∙
      ap (fun-comp α) (fun-assoc β γ δ) ◃∎ ∎ₛ

  fun-cat : TwoSemiCategory (lmax i j) (lmax i k)
  fun-cat =
    record
    { El = fun-El
    ; Arr = fun-Arr
    ; Arr-level = fun-Arr-level
    ; two-semi-cat-struct =
      record
      { comp = fun-comp
      ; assoc = fun-assoc
      ; pentagon-identity = fun-pentagon
      }
    }

module _ {i j₁ k₁ j₂ k₂} (A : Type i) {G : TwoSemiCategory j₁ k₁} {H : TwoSemiCategory j₂ k₂}
  (F : TwoSemiFunctor G H) where

  private
    module G = TwoSemiCategory G
    module H = TwoSemiCategory H
    module F = TwoSemiFunctor F
    module fun-G = TwoSemiCategory (fun-cat A G)
    module fun-H = TwoSemiCategory (fun-cat A H)

  fun-F₀ : fun-G.El → fun-H.El
  fun-F₀ I = λ a → F.F₀ (I a)

  fun-F₁ : {I J : fun-G.El} → fun-G.Arr I J → fun-H.Arr (fun-F₀ I) (fun-F₀ J)
  fun-F₁ α = λ a → F.F₁ (α a)

  fun-pres-comp : {I J K : fun-G.El} (α : fun-G.Arr I J) (β : fun-G.Arr J K)
    → fun-F₁ (fun-G.comp α β) == fun-H.comp (fun-F₁ α) (fun-F₁ β)
  fun-pres-comp α β = λ= (λ a → F.pres-comp (α a) (β a))

  abstract
    fun-pres-comp-coh : {I J K L : fun-G.El}
      (α : fun-G.Arr I J) (β : fun-G.Arr J K) (γ : fun-G.Arr K L)
      → fun-pres-comp (fun-G.comp α β) γ ◃∙
        ap (λ s → fun-H.comp s (fun-F₁ γ)) (fun-pres-comp α β) ◃∙
        fun-H.assoc (fun-F₁ α) (fun-F₁ β) (fun-F₁ γ) ◃∎
        =ₛ
        ap fun-F₁ (fun-G.assoc α β γ) ◃∙
        fun-pres-comp α (fun-G.comp β γ) ◃∙
        ap (fun-H.comp (fun-F₁ α)) (fun-pres-comp β γ) ◃∎
    fun-pres-comp-coh α β γ =
      fun-pres-comp (fun-G.comp α β) γ ◃∙
      ap (λ s → fun-H.comp s (fun-F₁ γ)) (fun-pres-comp α β) ◃∙
      fun-H.assoc (fun-F₁ α) (fun-F₁ β) (fun-F₁ γ) ◃∎
        =ₛ₁⟨ 1 & 1 & λ=-ap (λ a s → H.comp s (fun-F₁ γ a) ) (λ a → F.pres-comp (α a) (β a)) ⟩
      fun-pres-comp (fun-G.comp α β) γ ◃∙
      λ= (λ a → ap (λ s → H.comp s (fun-F₁ γ a)) (F.pres-comp (α a) (β a))) ◃∙
      fun-H.assoc (fun-F₁ α) (fun-F₁ β) (fun-F₁ γ) ◃∎
        =ₛ⟨ ∙∙-λ= (λ a → F.pres-comp (G.comp (α a) (β a)) (γ a))
                  (λ a → ap (λ s → H.comp s (fun-F₁ γ a)) (F.pres-comp (α a) (β a)))
                  (λ a → H.assoc (fun-F₁ α a) (fun-F₁ β a) (fun-F₁ γ a)) ⟩
      λ= (λ a → F.pres-comp (G.comp (α a) (β a)) (γ a) ∙
                ap (λ s → H.comp s (fun-F₁ γ a)) (F.pres-comp (α a) (β a)) ∙
                H.assoc (fun-F₁ α a) (fun-F₁ β a) (fun-F₁ γ a)) ◃∎
        =ₛ₁⟨ ap λ= (λ= (λ a → =ₛ-out (F.pres-comp-coh (α a) (β a) (γ a)))) ⟩
      λ= (λ a → ap F.F₁ (G.assoc (α a) (β a) (γ a)) ∙
                F.pres-comp (α a) (G.comp (β a) (γ a)) ∙
                ap (H.comp (fun-F₁ α a)) (F.pres-comp (β a) (γ a))) ◃∎
        =ₛ⟨ λ=-∙∙ (λ a → ap F.F₁ (G.assoc (α a) (β a) (γ a)))
                  (λ a → F.pres-comp (α a) (G.comp (β a) (γ a)))
                  (λ a → ap (H.comp (fun-F₁ α a)) (F.pres-comp (β a) (γ a))) ⟩
      λ= (λ a → ap F.F₁ (G.assoc (α a) (β a) (γ a))) ◃∙
      fun-pres-comp α (fun-G.comp β γ) ◃∙
      λ= (λ a → ap (H.comp (fun-F₁ α a)) (F.pres-comp (β a) (γ a))) ◃∎
        =ₛ₁⟨ 0 & 1 & ! $ λ=-ap (λ _ → F.F₁) (λ a → G.assoc (α a) (β a) (γ a)) ⟩
      ap fun-F₁ (fun-G.assoc α β γ) ◃∙
      fun-pres-comp α (fun-G.comp β γ) ◃∙
      λ= (λ a → ap (H.comp (fun-F₁ α a)) (F.pres-comp (β a) (γ a))) ◃∎
        =ₛ₁⟨ 2 & 1 & ! $ λ=-ap (λ a → H.comp (fun-F₁ α a)) (λ a → F.pres-comp (β a) (γ a)) ⟩
      ap fun-F₁ (fun-G.assoc α β γ) ◃∙
      fun-pres-comp α (fun-G.comp β γ) ◃∙
      ap (fun-H.comp (fun-F₁ α)) (fun-pres-comp β γ) ◃∎ ∎ₛ

  fun-functor-map : TwoSemiFunctor (fun-cat A G) (fun-cat A H)
  fun-functor-map =
    record
    { F₀ = fun-F₀
    ; F₁ = fun-F₁
    ; pres-comp = fun-pres-comp
    ; pres-comp-coh = fun-pres-comp-coh
    }

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
module Prelude.Sum where

open import Agda.Primitive
open import Prelude.Empty
open import Prelude.Unit
open import Prelude.List
open import Prelude.Functor
open import Prelude.Applicative
open import Prelude.Monad
open import Prelude.Equality
open import Prelude.Decidable
open import Prelude.Product
open import Prelude.Function

data Either {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  left  : A → Either A B
  right : B → Either A B

{-# FOREIGN GHC type AgdaEither a b = Either #-}
{-# COMPILE GHC Either = data MAlonzo.Code.Prelude.Sum.AgdaEither (Left | Right) #-}

either : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
           (A → C) → (B → C) → Either A B → C
either f g (left  x) = f x
either f g (right x) = g x

lefts : ∀ {a b} {A : Set a} {B : Set b} → List (Either A B) → List A
lefts = concatMap λ { (left x) → [ x ]; (right _) → [] }

rights : ∀ {a b} {A : Set a} {B : Set b} → List (Either A B) → List B
rights = concatMap λ { (left _) → []; (right x) → [ x ] }

mapEither : ∀ {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂} {B₁ : Set b₁} {B₂ : Set b₂} →
            (A₁ → A₂) → (B₁ → B₂) → Either A₁ B₁ → Either A₂ B₂
mapEither f g = either (left ∘ f) (right ∘ g)

mapLeft : ∀ {a₁ a₂ b} {A₁ : Set a₁} {A₂ : Set a₂} {B : Set b} →
            (A₁ → A₂) → Either A₁ B → Either A₂ B
mapLeft f = either (left ∘ f) right

mapRight : ∀ {a b₁ b₂} {A : Set a} {B₁ : Set b₁} {B₂ : Set b₂} →
            (B₁ → B₂) → Either A B₁ → Either A B₂
mapRight f = either left (right ∘ f)

partitionMap : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
                 (A → Either B C) → List A → List B × List C
partitionMap f [] = [] , []
partitionMap f (x ∷ xs) = either (first ∘ _∷_)
                                 (λ y → second (_∷_ y))  -- second ∘ _∷_ doesn't work for some reason
                                 (f x) (partitionMap f xs)

--- Equality ---

left-inj : ∀ {a} {A : Set a} {x y : A} {b} {B : Set b} →
           left {B = B} x ≡ left y → x ≡ y
left-inj refl = refl

right-inj : ∀ {b} {B : Set b} {x y : B} {a} {A : Set a} →
            right {A = A} x ≡ right y → x ≡ y
right-inj refl = refl

private
  eqEither : ∀ {a b} {A : Set a} {B : Set b} {{EqA : Eq A}} {{EqB : Eq B}}
               (x y : Either A B) → Dec (x ≡ y)
  eqEither (left x)  (right y) = no (λ ())
  eqEither (right x) (left y)  = no (λ ())
  eqEither (left x)  (left y)  with x == y
  ... | yes eq = yes (left $≡ eq)
  ... | no neq = no λ eq → neq (left-inj eq)
  eqEither (right x) (right y) with x == y
  ... | yes eq = yes (right $≡ eq)
  ... | no neq = no λ eq → neq (right-inj eq)

instance
  EqEither : ∀ {a b} {A : Set a} {B : Set b} {{EqA : Eq A}} {{EqB : Eq B}} →
               Eq (Either A B)
  _==_ {{EqEither}} = eqEither

--- Monad instance ---

module _ {a b} {A : Set a} where
  instance
    FunctorEither : Functor (Either {b = b} A)
    fmap {{FunctorEither}} f (left x) = left x
    fmap {{FunctorEither}} f (right x) = right (f x)

    ApplicativeEither : Applicative (Either {b = b} A)
    pure  {{ApplicativeEither}} = right
    _<*>_ {{ApplicativeEither}} (right f) (right x) = right (f x)
    _<*>_ {{ApplicativeEither}} (right _) (left e)  = left e
    _<*>_ {{ApplicativeEither}} (left e)  _         = left e

    MonadEither : Monad (Either {b = b} A)
    _>>=_  {{MonadEither}} m f = either left f m


text:
module snoc where

open import unit
open import empty
open import bool
open import product

data Snoc (A : Set) : Set where
  [] : Snoc A
  _::_ : Snoc A → A → Snoc A

infixl 6 _::_ _++_

[_] : {A : Set} → A → Snoc A
[ x ] = [] :: x

_++_ : {A : Set} → Snoc A → Snoc A → Snoc A
[] ++ l₂ = l₂
(l₁ :: x) ++ l₂ = (l₁ ++ l₂) :: x

member : {A : Set} → (A → A → 𝔹) → A → Snoc A → 𝔹
member _=A_ x (l :: y) with x =A y
... | tt = tt
... | ff = ff
member _=A_ x _ = ff

inPairSnocFst : {A B : Set} → (A → A → 𝔹) → A → Snoc (A × B) → Set
inPairSnocFst _=A_ x [] = ⊥
inPairSnocFst _=A_ x (l :: (a , _)) with x =A a
... | tt = ⊤
... | ff = inPairSnocFst _=A_ x l

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
{-# OPTIONS --allow-unsolved-metas #-}
module nat where

open import Data.Nat
open import Data.Nat.Properties
open import Data.Empty
open import Relation.Nullary
open import  Relation.Binary.PropositionalEquality
open import  Relation.Binary.Core
open import  Relation.Binary.Definitions
open import  logic
open import Level hiding ( zero ; suc )

nat-<> : { x y : ℕ } → x < y → y < x → ⊥
nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x

nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x

nat-<≡ : { x : ℕ } → x < x → ⊥
nat-<≡  (s≤s lt) = nat-<≡ lt

nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
nat-≡< refl lt = nat-<≡ lt

¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
¬a≤a  (s≤s lt) = ¬a≤a  lt

a<sa : {la : ℕ} → la < suc la
a<sa {zero} = s≤s z≤n
a<sa {suc la} = s≤s a<sa

=→¬< : {x : ℕ  } → ¬ ( x < x )
=→¬< {zero} ()
=→¬< {suc x} (s≤s lt) = =→¬< lt

>→¬< : {x y : ℕ  } → (x < y ) → ¬ ( y < x )
>→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x

<-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) )
<-∨ {zero} {zero} (s≤s z≤n) = case1 refl
<-∨ {zero} {suc y} (s≤s lt) = case2 (s≤s z≤n)
<-∨ {suc x} {zero} (s≤s ())
<-∨ {suc x} {suc y} (s≤s lt) with <-∨ {x} {y} lt
<-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq)
<-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)

max : (x y : ℕ) → ℕ
max zero zero = zero
max zero (suc x) = (suc x)
max (suc x) zero = (suc x)
max (suc x) (suc y) = suc ( max x y )

-- _*_ : ℕ → ℕ → ℕ
-- _*_ zero _ = zero
-- _*_ (suc n) m = m + ( n * m )

-- x ^ y
exp : ℕ → ℕ → ℕ
exp _ zero = 1
exp n (suc m) = n * ( exp n m )

div2 : ℕ → (ℕ ∧ Bool )
div2 zero =  ⟪ 0 , false ⟫
div2 (suc zero) =  ⟪ 0 , true ⟫
div2 (suc (suc n)) =  ⟪ suc (proj1 (div2 n)) , proj2 (div2 n) ⟫ where
    open _∧_

div2-rev : (ℕ ∧ Bool ) → ℕ
div2-rev ⟪ x , true ⟫ = suc (x + x)
div2-rev ⟪ x , false ⟫ = x + x

div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x
div2-eq zero = refl
div2-eq (suc zero) = refl
div2-eq (suc (suc x)) with div2 x | inspect div2 x
... | ⟪ x1 , true ⟫ | record { eq = eq1 } = begin -- eq1 : div2 x ≡ ⟪ x1 , true ⟫
     div2-rev ⟪ suc x1 , true ⟫ ≡⟨⟩
     suc (suc (x1 + suc x1)) ≡⟨ cong (λ k → suc (suc k )) (+-comm x1  _ ) ⟩
     suc (suc (suc (x1 + x1))) ≡⟨⟩
     suc (suc (div2-rev ⟪ x1 , true ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩
     suc (suc (div2-rev (div2 x)))      ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩
     suc (suc x) ∎  where open ≡-Reasoning
... | ⟪ x1 , false ⟫ | record { eq = eq1 } = begin
     div2-rev ⟪ suc x1 , false ⟫ ≡⟨⟩
     suc (x1 + suc x1) ≡⟨ cong (λ k → (suc k )) (+-comm x1  _ ) ⟩
     suc (suc (x1 + x1)) ≡⟨⟩
     suc (suc (div2-rev ⟪ x1 , false ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩
     suc (suc (div2-rev (div2 x)))      ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩
     suc (suc x) ∎  where open ≡-Reasoning

sucprd : {i : ℕ } → 0 < i  → suc (pred i) ≡ i
sucprd {suc i} 0<i = refl

0<s : {x : ℕ } → zero < suc x
0<s {_} = s≤s z≤n

px<py : {x y : ℕ } → pred x  < pred y → x < y
px<py {zero} {suc y} lt = 0<s
px<py {suc zero} {suc (suc y)} (s≤s lt) = s≤s 0<s
px<py {suc (suc x)} {suc (suc y)} (s≤s lt) = s≤s (px<py {suc x} {suc y} lt)

minus : (a b : ℕ ) →  ℕ
minus a zero = a
minus zero (suc b) = zero
minus (suc a) (suc b) = minus a b

_-_ = minus

m+= : {i j  m : ℕ } → m + i ≡ m + j → i ≡ j
m+= {i} {j} {zero} refl = refl
m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq )

+m= : {i j  m : ℕ } → i + m ≡ j + m → i ≡ j
+m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq )

less-1 :  { n m : ℕ } → suc n < m → n < m
less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n
less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt)

sa=b→a<b :  { n m : ℕ } → suc n ≡ m → n < m
sa=b→a<b {0} {suc zero} refl = s≤s z≤n
sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl)

minus+n : {x y : ℕ } → suc x > y  → minus x y + y ≡ x
minus+n {x} {zero} _ = trans (sym (+-comm zero  _ )) refl
minus+n {zero} {suc y} (s≤s ())
minus+n {suc x} {suc y} (s≤s lt) = begin
           minus (suc x) (suc y) + suc y
        ≡⟨ +-comm _ (suc y)    ⟩
           suc y + minus x y
        ≡⟨ cong ( λ k → suc k ) (
           begin
                 y + minus x y
              ≡⟨ +-comm y  _ ⟩
                 minus x y + y
              ≡⟨ minus+n {x} {y} lt ⟩
                 x
           ∎
           ) ⟩
           suc x
        ∎  where open ≡-Reasoning

<-minus-0 : {x y z : ℕ } → z + x < z + y → x < y
<-minus-0 {x} {suc _} {zero} lt = lt
<-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt

<-minus : {x y z : ℕ } → x + z < y + z → x < y
<-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt )

x≤x+y : {z y : ℕ } → z ≤ z + y
x≤x+y {zero} {y} = z≤n
x≤x+y {suc z} {y} = s≤s  (x≤x+y {z} {y})

x≤y+x : {z y : ℕ } → z ≤ y + z
x≤y+x {z} {y} = subst (λ k → z ≤ k ) (+-comm _ y ) x≤x+y

<-plus : {x y z : ℕ } → x < y → x + z < y + z
<-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y  )
<-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt)

<-plus-0 : {x y z : ℕ } → x < y → z + x < z + y
<-plus-0 {x} {y} {z} lt = subst₂ (λ j k → j < k ) (+-comm _ z) (+-comm _ z) ( <-plus {x} {y} {z} lt )

≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z
≤-plus {0} {y} {zero} z≤n = z≤n
≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y
≤-plus {suc x} {suc y} {z} (s≤s lt) = s≤s ( ≤-plus {x} {y} {z} lt )

≤-plus-0 : {x y z : ℕ } → x ≤ y → z + x ≤ z + y
≤-plus-0 {x} {y} {zero} lt = lt
≤-plus-0 {x} {y} {suc z} lt = s≤s ( ≤-plus-0 {x} {y} {z} lt )

x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z
x+y<z→x<z {zero} {y} {suc z} (s≤s lt1) = s≤s z≤n
x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 )

*≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z
*≤ lt = *-mono-≤ lt ≤-refl

*< : {x y z : ℕ } → x < y → x * suc z < y * suc z
*< {zero} {suc y} lt = s≤s z≤n
*< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt)

<to<s : {x y  : ℕ } → x < y → x < suc y
<to<s {zero} {suc y} (s≤s lt) = s≤s z≤n
<to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt)

<tos<s : {x y  : ℕ } → x < y → suc x < suc y
<tos<s {zero} {suc y} (s≤s z≤n) = s≤s (s≤s z≤n)
<tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt)

<to≤ : {x y  : ℕ } → x < y → x ≤ y
<to≤ {zero} {suc y} (s≤s z≤n) = z≤n
<to≤ {suc x} {suc y} (s≤s lt) = s≤s (<to≤ {x} {y}  lt)

refl-≤s : {x : ℕ } → x ≤ suc x
refl-≤s {zero} = z≤n
refl-≤s {suc x} = s≤s (refl-≤s {x})

refl-≤ : {x : ℕ } → x ≤ x
refl-≤ {zero} = z≤n
refl-≤ {suc x} = s≤s (refl-≤ {x})

x<y→≤ : {x y : ℕ } → x < y →  x ≤ suc y
x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n
x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt)

≤→= : {i j : ℕ} → i ≤ j → j ≤ i → i ≡ j
≤→= {0} {0} z≤n z≤n = refl
≤→= {suc i} {suc j} (s≤s i<j) (s≤s j<i) = cong suc ( ≤→= {i} {j} i<j j<i )

px≤x : {x  : ℕ } → pred x ≤ x
px≤x {zero} = refl-≤
px≤x {suc x} = refl-≤s

px≤py : {x y : ℕ } → x ≤ y → pred x  ≤ pred y
px≤py {zero} {zero} lt = refl-≤
px≤py {zero} {suc y} lt = z≤n
px≤py {suc x} {suc y} (s≤s lt) = lt

open import Data.Product

i-j=0→i=j : {i j  : ℕ } → j ≤ i  → i - j ≡ 0 → i ≡ j
i-j=0→i=j {zero} {zero} _ refl = refl
i-j=0→i=j {zero} {suc j} () refl
i-j=0→i=j {suc i} {zero} z≤n ()
i-j=0→i=j {suc i} {suc j} (s≤s lt) eq = cong suc (i-j=0→i=j {i} {j} lt eq)

m*n=0⇒m=0∨n=0 : {i j : ℕ} → i * j ≡ 0 → (i ≡ 0) ∨ ( j ≡ 0 )
m*n=0⇒m=0∨n=0 {zero} {j} refl = case1 refl
m*n=0⇒m=0∨n=0 {suc i} {zero} eq = case2 refl

minus+1 : {x y  : ℕ } → y ≤ x  → suc (minus x y)  ≡ minus (suc x) y
minus+1 {zero} {zero} y≤x = refl
minus+1 {suc x} {zero} y≤x = refl
minus+1 {suc x} {suc y} (s≤s y≤x) = minus+1 {x} {y} y≤x

minus+yz : {x y z : ℕ } → z ≤ y  → x + minus y z  ≡ minus (x + y) z
minus+yz {zero} {y} {z} _ = refl
minus+yz {suc x} {y} {z} z≤y = begin
         suc x + minus y z ≡⟨ cong suc ( minus+yz z≤y ) ⟩
         suc (minus (x + y) z) ≡⟨ minus+1 {x + y} {z} (≤-trans z≤y (subst (λ g → y ≤ g) (+-comm y x) x≤x+y) ) ⟩
         minus (suc x + y) z ∎  where open ≡-Reasoning

minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0
minus<=0 {0} {zero} z≤n = refl
minus<=0 {0} {suc y} z≤n = refl
minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le

minus>0 : {x y : ℕ } → x < y → 0 < minus y x
minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n
minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt

minus>0→x<y : {x y : ℕ } → 0 < minus y x  → x < y
minus>0→x<y {x} {y} lt with <-cmp x y
... | tri< a ¬b ¬c = a
... | tri≈ ¬a refl ¬c = ⊥-elim ( nat-≡< (sym (minus<=0 {x} ≤-refl)) lt )
... | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (sym (minus<=0 {y} (≤-trans refl-≤s c ))) lt )

minus+y-y : {x y : ℕ } → (x + y) - y  ≡ x
minus+y-y {zero} {y} = minus<=0 {zero + y} {y} ≤-refl
minus+y-y {suc x} {y} = begin
         (suc x + y) - y ≡⟨ sym (minus+1 {_} {y} x≤y+x) ⟩
         suc ((x + y) - y) ≡⟨ cong suc (minus+y-y {x} {y}) ⟩
         suc x ∎  where open ≡-Reasoning

minus+yx-yz : {x y z : ℕ } → (y + x) - (y + z)  ≡ x - z
minus+yx-yz {x} {zero} {z} = refl
minus+yx-yz {x} {suc y} {z} = minus+yx-yz {x} {y} {z}

minus+xy-zy : {x y z : ℕ } → (x + y) - (z + y)  ≡ x - z
minus+xy-zy {x} {y} {z} = subst₂ (λ j k → j - k ≡ x - z  ) (+-comm y x) (+-comm y z) (minus+yx-yz {x} {y} {z})

y-x<y : {x y : ℕ } → 0 < x → 0 < y  → y - x  <  y
y-x<y {x} {y} 0<x 0<y with <-cmp x (suc y)
... | tri< a ¬b ¬c = +-cancelʳ-< {x} (y - x) y ( begin
         suc ((y - x) + x) ≡⟨ cong suc (minus+n {y} {x} a ) ⟩
         suc y  ≡⟨ +-comm 1 _ ⟩
         y + suc 0  ≤⟨ +-mono-≤ ≤-refl 0<x ⟩
         y + x ∎ )  where open ≤-Reasoning
... | tri≈ ¬a refl ¬c = subst ( λ k → k < y ) (sym (minus<=0 {y} {x} refl-≤s )) 0<y
... | tri> ¬a ¬b c = subst ( λ k → k < y ) (sym (minus<=0 {y} {x} (≤-trans (≤-trans refl-≤s refl-≤s) c))) 0<y -- suc (suc y) ≤ x → y ≤ x

open import Relation.Binary.Definitions

distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z)
distr-minus-* {x} {zero} {z} = refl
distr-minus-* {x} {suc y} {z} with <-cmp x y
distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin
          minus x (suc y) * z
        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x<y→≤ a)) ⟩
           0 * z
        ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩
          minus (x * z) (z + y * z)
        ∎  where
            open ≡-Reasoning
            le : x * z ≤ z + y * z
            le  = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where
               lemma : x * z ≤ y * z
               lemma = *≤ {x} {y} {z} (<to≤ a)
distr-minus-* {x} {suc y} {z} | tri≈ ¬a refl ¬c = begin
          minus x (suc y) * z
        ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} refl-≤s ) ⟩
           0 * z
        ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩
          minus (x * z) (z + y * z)
        ∎  where
            open ≡-Reasoning
            lt : {x z : ℕ } →  x * z ≤ z + x * z
            lt {zero} {zero} = z≤n
            lt {suc x} {zero} = lt {x} {zero}
            lt {x} {suc z} = ≤-trans lemma refl-≤s where
               lemma : x * suc z ≤   z + x * suc z
               lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z})
distr-minus-* {x} {suc y} {z} | tri> ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin
           minus x (suc y) * z + suc y * z
        ≡⟨ sym (proj₂ *-distrib-+ z  (minus x (suc y) )  _) ⟩
           ( minus x (suc y) + suc y ) * z
        ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c))  ⟩
           x * z
        ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩
           minus (x * z) (suc y * z) + suc y * z
        ∎ ) where
            open ≡-Reasoning
            lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z
            lt {x} {y} {z} le = *≤ le

distr-minus-*' : {z x y : ℕ } → z * (minus x y)  ≡ minus (z * x) (z * y)
distr-minus-*' {z} {x} {y} = begin
        z * (minus x y) ≡⟨ *-comm _ (x - y) ⟩
        (minus x y) * z ≡⟨ distr-minus-* {x} {y} {z} ⟩
        minus (x * z) (y * z) ≡⟨ cong₂ (λ j k → j - k ) (*-comm x z ) (*-comm y z) ⟩
        minus (z * x) (z * y) ∎  where open ≡-Reasoning

minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z)
minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin
           minus (minus x y) z + z
        ≡⟨ minus+n {_} {z} lemma ⟩
           minus x y
        ≡⟨ +m= {_} {_} {y} ( begin
              minus x y + y
           ≡⟨ minus+n {_} {y} lemma1 ⟩
              x
           ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩
              minus x (z + y) + (z + y)
           ≡⟨ sym ( +-assoc (minus x (z + y)) _  _ ) ⟩
              minus x (z + y) + z + y
           ∎ ) ⟩
           minus x (z + y) + z
        ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y )  ⟩
           minus x (y + z) + z
        ∎  ) where
             open ≡-Reasoning
             lemma1 : suc x > y
             lemma1 = x+y<z→x<z (subst (λ k → k < suc x ) (+-comm z _ ) gt )
             lemma : suc (minus x y) > z
             lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y}  lemma1 ))  gt )

minus-* : {M k n : ℕ } → n < k  → minus k (suc n) * M ≡ minus (minus k n * M ) M
minus-* {zero} {k} {n} lt = begin
           minus k (suc n) * zero
        ≡⟨ *-comm (minus k (suc n)) zero ⟩
           zero * minus k (suc n)
        ≡⟨⟩
           0 * minus k n
        ≡⟨ *-comm 0 (minus k n) ⟩
           minus (minus k n * 0 ) 0
        ∎  where
        open ≡-Reasoning
minus-* {suc m} {k} {n} lt with <-cmp k 1
minus-* {suc m} {.0} {zero} lt | tri< (s≤s z≤n) ¬b ¬c = refl
minus-* {suc m} {.0} {suc n} lt | tri< (s≤s z≤n) ¬b ¬c = refl
minus-* {suc zero} {.1} {zero} lt | tri≈ ¬a refl ¬c = refl
minus-* {suc (suc m)} {.1} {zero} lt | tri≈ ¬a refl ¬c = minus-* {suc m} {1} {zero} lt
minus-* {suc m} {.1} {suc n} (s≤s ()) | tri≈ ¬a refl ¬c
minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin
           minus k (suc n) * M
        ≡⟨ distr-minus-* {k} {suc n} {M}  ⟩
           minus (k * M ) ((suc n) * M)
        ≡⟨⟩
           minus (k * M ) (M + n * M  )
        ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩
           minus (k * M ) ((n * M) + M )
        ≡⟨ sym ( minus- {k * M} {n * M} (lemma lt) ) ⟩
           minus (minus (k * M ) (n * M)) M
        ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩
           minus (minus k n * M ) M
        ∎  where
             M = suc m
             lemma : {n k m : ℕ } → n < k  → suc (k * suc m) > suc m + n * suc m
             lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y ))
             lemma {suc n} {suc k} {m} lt = begin
                         suc (suc m + suc n * suc m)
                      ≡⟨⟩
                         suc ( suc (suc n) * suc m)
                      ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩
                         suc (suc k * suc m)
                      ∎   where open ≤-Reasoning
             open ≡-Reasoning

x=y+z→x-z=y : {x y z : ℕ } → x ≡ y + z → x - z ≡ y
x=y+z→x-z=y {x} {zero} {.x} refl = minus<=0 {x} {x} refl-≤ -- x ≡ suc (y + z) → (x ≡ y + z → x - z ≡ y)   → (x - z) ≡ suc y
x=y+z→x-z=y {suc x} {suc y} {zero} eq = begin -- suc x ≡ suc (y + zero) → (suc x - zero) ≡ suc y
       suc x - zero ≡⟨ refl ⟩
       suc x  ≡⟨ eq ⟩
       suc y + zero ≡⟨ +-comm _ zero ⟩
       suc y ∎  where open ≡-Reasoning
x=y+z→x-z=y {suc x} {suc y} {suc z} eq = x=y+z→x-z=y {x} {suc y} {z} ( begin
       x ≡⟨ cong pred eq ⟩
       pred (suc y + suc z) ≡⟨ +-comm _ (suc z)  ⟩
       suc z + y ≡⟨ cong suc ( +-comm _ y ) ⟩
       suc y + z ∎  ) where open ≡-Reasoning

m*1=m : {m : ℕ } → m * 1 ≡ m
m*1=m {zero} = refl
m*1=m {suc m} = cong suc m*1=m

record Finduction {n m : Level} (P : Set n ) (Q : P → Set m ) (f : P → ℕ) : Set  (n Level.⊔ m) where
  field
    fzero   : {p : P} → f p ≡ zero → Q p
    pnext : (p : P ) → P
    decline : {p : P} → 0 < f p  → f (pnext p) < f p
    ind : {p : P} → Q (pnext p) → Q p

y<sx→y≤x : {x y : ℕ} → y < suc x → y ≤ x
y<sx→y≤x (s≤s lt) = lt

fi0 : (x : ℕ) → x ≤ zero → x ≡ zero
fi0 .0 z≤n = refl

f-induction : {n m : Level} {P : Set n } → {Q : P → Set m }
  → (f : P → ℕ)
  → Finduction P Q f
  → (p : P ) → Q p
f-induction {n} {m} {P} {Q} f I p with <-cmp 0 (f p)
... | tri> ¬a ¬b ()
... | tri≈ ¬a b ¬c = Finduction.fzero I (sym b)
... | tri< lt _ _ = f-induction0 p (f p) (<to≤ (Finduction.decline I lt)) where
   f-induction0 : (p : P) → (x : ℕ) → (f (Finduction.pnext I p)) ≤ x → Q p
   f-induction0 p zero le = Finduction.ind I (Finduction.fzero I (fi0 _ le)) where
   f-induction0 p (suc x) le with <-cmp (f (Finduction.pnext I p)) (suc x)
   ... | tri< (s≤s a) ¬b ¬c = f-induction0 p x a
   ... | tri≈ ¬a b ¬c = Finduction.ind I (f-induction0 (Finduction.pnext I p) x (y<sx→y≤x f1)) where
       f1 : f (Finduction.pnext I (Finduction.pnext I p)) < suc x
       f1 = subst (λ k → f (Finduction.pnext I (Finduction.pnext I p)) < k ) b ( Finduction.decline I {Finduction.pnext I p}
         (subst (λ k → 0 < k ) (sym b) (s≤s z≤n ) ))
   ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c )

record Ninduction {n m : Level} (P : Set n ) (Q : P → Set m ) (f : P → ℕ) : Set  (n Level.⊔ m) where
  field
    pnext : (p : P ) → P
    fzero   : {p : P} → f (pnext p) ≡ zero → Q p
    decline : {p : P} → 0 < f p  → f (pnext p) < f p
    ind : {p : P} → Q (pnext p) → Q p

s≤s→≤ : { i j : ℕ} → suc i ≤ suc j → i ≤ j
s≤s→≤ (s≤s lt) = lt

n-induction : {n m : Level} {P : Set n } → {Q : P → Set m }
  → (f : P → ℕ)
  → Ninduction P Q f
  → (p : P ) → Q p
n-induction {n} {m} {P} {Q} f I p  = f-induction0 p (f (Ninduction.pnext I p)) ≤-refl where
   f-induction0 : (p : P) → (x : ℕ) → (f (Ninduction.pnext I p)) ≤ x  →  Q p
   f-induction0 p zero lt = Ninduction.fzero I {p} (fi0 _ lt)
   f-induction0 p (suc x) le with <-cmp (f (Ninduction.pnext I p)) (suc x)
   ... | tri< (s≤s a)  ¬b ¬c = f-induction0 p x a
   ... | tri≈ ¬a b ¬c = Ninduction.ind I (f-induction0 (Ninduction.pnext I p) x (s≤s→≤ nle) ) where
      f>0 :  0 < f (Ninduction.pnext I p)
      f>0 = subst (λ k → 0 < k ) (sym b) ( s≤s z≤n )
      nle : suc (f (Ninduction.pnext I (Ninduction.pnext I p))) ≤ suc x
      nle = subst (λ k → suc (f (Ninduction.pnext I (Ninduction.pnext I p))) ≤ k) b (Ninduction.decline I {Ninduction.pnext I p} f>0 )
   ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> le c )

max_stars_repo_name: shinji-kono/HyperReal-in-agda

max_issues_repo_name: shinji-kono/HyperReal-in-agda

max_forks_repo_name: shinji-kono/HyperReal-in-agda


text:
-- Andreas, 2021-04-21, issue #5334
-- Improve sorting of constructors to data for interleaved mutual blocks.

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

module Issue5334 where

module Works where

  data Nat : Set where
    zero : Nat
  data Fin : Nat → Set where
    zero : Fin {!!}

interleaved mutual

  data Nat : Set
  data Fin : Nat → Set
  data _ where
    zero : Nat
  data _ where
    zero : Fin {!!}  -- should work

-- Error was:
-- Could not find a matching data signature for constructor zero
-- There was no candidate.