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

open import Algebra.Structures.Bundles.Field
open import Algebra.Linear.Structures.Bundles

module Algebra.Linear.Space.Hom
  {k ℓ} (K : Field k ℓ)
  {a₁ ℓ₁} (V₁-space : VectorSpace K a₁ ℓ₁)
  {a₂ ℓ₂} (V₂-space : VectorSpace K a₂ ℓ₂)
  where

open import Relation.Binary
open import Level using (_⊔_; suc)
open import Data.Nat using (ℕ) renaming (_+_ to _+ℕ_)
open import Algebra.Linear.Morphism.Bundles K
open import Algebra.Linear.Morphism.Properties K
open import Algebra.Linear.Structures.VectorSpace

open import Data.Product

open VectorSpaceField K

open VectorSpace V₁-space
  using ()
  renaming
  ( Carrier       to V₁
  ; _≈_           to _≈₁_
  ; isEquivalence to ≈₁-isEquiv
  ; refl          to ≈₁-refl
  ; sym           to ≈₁-sym
  ; trans         to ≈₁-trans
  ; setoid        to setoid₁
  ; _+_           to _+₁_
  ; _∙_           to _∙₁_
  ; -_            to -₁_
  ; 0#            to 0₁
  ; +-identityˡ    to +₁-identityˡ
  ; +-identityʳ    to +₁-identityʳ
  ; +-identity    to +₁-identity
  ; +-cong        to +₁-cong
  ; +-assoc       to +₁-assoc
  ; +-comm        to +₁-comm
  ; *ᵏ-∙-compat   to *ᵏ-∙₁-compat
  ; ∙-+-distrib   to ∙₁-+₁-distrib
  ; ∙-+ᵏ-distrib  to ∙₁-+ᵏ-distrib
  ; ∙-cong        to ∙₁-cong
  ; ∙-identity    to ∙₁-identity
  ; ∙-absorbˡ      to ∙₁-absorbˡ
  ; ∙-absorbʳ      to ∙₁-absorbʳ
  ; -‿cong        to -₁‿cong
  ; -‿inverseˡ    to -₁‿inverseˡ
  ; -‿inverseʳ    to -₁‿inverseʳ
  )

open VectorSpace V₂-space
  using ()
  renaming
  ( Carrier       to V₂
  ; _≈_           to _≈₂_
  ; isEquivalence to ≈₂-isEquiv
  ; refl          to ≈₂-refl
  ; sym           to ≈₂-sym
  ; trans         to ≈₂-trans
  ; setoid        to setoid₂
  ; _+_           to _+₂_
  ; _∙_           to _∙₂_
  ; -_            to -₂_
  ; 0#            to 0₂
  ; +-identityˡ    to +₂-identityˡ
  ; +-identityʳ    to +₂-identityʳ
  ; +-identity    to +₂-identity
  ; +-cong        to +₂-cong
  ; +-assoc       to +₂-assoc
  ; +-comm        to +₂-comm
  ; *ᵏ-∙-compat   to *ᵏ-∙₂-compat
  ; ∙-+-distrib   to ∙₂-+₂-distrib
  ; ∙-+ᵏ-distrib  to ∙₂-+ᵏ-distrib
  ; ∙-cong        to ∙₂-cong
  ; ∙-identity    to ∙₂-identity
  ; ∙-absorbˡ      to ∙₂-absorbˡ
  ; ∙-absorbʳ      to ∙₂-absorbʳ
  ; ∙-∙-comm      to ∙₂-∙₂-comm
  ; -‿cong        to -₂‿cong
  ; -‿inverseˡ    to -₂‿inverseˡ
  ; -‿inverseʳ    to -₂‿inverseʳ
  ; -‿+-comm     to -₂‿+₂-comm
  ; -1∙u≈-u       to -1∙u≈₂-u
  )

import Function

private
  V : Set (suc (k ⊔ a₁ ⊔ a₂ ⊔ ℓ₁ ⊔ ℓ₂))
  V = LinearMap V₁-space V₂-space

open LinearMap using (_⟪$⟫_; ⟦⟧-cong; distrib-linear)

setoid : Setoid (suc (k ⊔ a₁ ⊔ a₂ ⊔ ℓ₁ ⊔ ℓ₂)) _
setoid = linearMap-setoid V₁-space V₂-space

open Setoid setoid public
  renaming (isEquivalence to ≈-isEquiv)

open import Algebra.FunctionProperties _≈_
open import Algebra.Structures _≈_
open import Function.Equality hiding (setoid; _∘_)

open import Relation.Binary.EqReasoning setoid₂

0# : V
0# = record
  { ⟦_⟧ = λ x → 0₂
  ; isLinearMap = linear V₁-space V₂-space π
    λ a b u v →
      begin
        0₂
      ≈⟨ ≈₂-trans (≈₂-sym (∙₂-absorbʳ b)) (≈₂-sym (+₂-identityˡ (b ∙₂ 0₂))) ⟩
        0₂ +₂ b ∙₂ 0₂
      ≈⟨ +₂-cong (≈₂-sym (∙₂-absorbʳ a)) ≈₂-refl ⟩
        a ∙₂ 0₂ +₂ b ∙₂ 0₂
      ∎
  }
  where π : setoid₁ ⟶ setoid₂
        π = record
          { _⟨$⟩_ = λ x → 0₂
          ; cong  = λ r → ≈₂-refl }

-_ : Op₁ V
- f = record
  { ⟦_⟧ = λ x → -₂ f ⟪$⟫ x
  ; isLinearMap = linear V₁-space V₂-space π
    let -[a∙u]≈₂a∙[-u] : ∀ (a : K') (u : V₂) -> (-₂ (a ∙₂ u)) ≈₂ a ∙₂ (-₂ u)
        -[a∙u]≈₂a∙[-u] a u =
          begin
            (-₂ (a ∙₂ u))
          ≈⟨ ≈₂-sym (-1∙u≈₂-u (a ∙₂ u)) ⟩
            (-ᵏ 1ᵏ) ∙₂ (a ∙₂ u)
          ≈⟨ ≈₂-sym (*ᵏ-∙₂-compat (-ᵏ 1ᵏ) a u) ⟩
            ((-ᵏ 1ᵏ) *ᵏ a) ∙₂ u
          ≈⟨ ∙₂-cong (≈ᵏ-trans (≈ᵏ-sym (-ᵏ‿distribˡ-*ᵏ 1ᵏ a)) (-ᵏ‿cong (*ᵏ-identityˡ a))) ≈₂-refl ⟩
            (-ᵏ a) ∙₂ u
          ≈⟨ ∙₂-cong (≈ᵏ-trans (-ᵏ‿cong (≈ᵏ-sym (*ᵏ-identityʳ a))) (-ᵏ‿distribʳ-*ᵏ a 1ᵏ)) ≈₂-refl ⟩
            (a *ᵏ (-ᵏ 1ᵏ)) ∙₂ u
          ≈⟨ ≈₂-trans (*ᵏ-∙₂-compat a (-ᵏ 1ᵏ) u) (∙₂-cong ≈ᵏ-refl (-1∙u≈₂-u u)) ⟩
             a ∙₂ (-₂ u)
          ∎
    in λ a b u v →
      begin
        π ⟨$⟩ a ∙₁ u +₁ b ∙₁ v
      ≈⟨ -₂‿cong (distrib-linear f a b u v) ⟩
        -₂ (a ∙₂ (f ⟪$⟫ u) +₂ b ∙₂ (f ⟪$⟫ v))
      ≈⟨ ≈₂-sym (-₂‿+₂-comm (a ∙₂ (f ⟪$⟫ u)) ( b ∙₂ (f ⟪$⟫ v))) ⟩
        ((-₂ (a ∙₂ (f ⟪$⟫ u))) +₂ (-₂ (b ∙₂ (f ⟪$⟫ v))))
      ≈⟨ +₂-cong (-[a∙u]≈₂a∙[-u] a (f ⟪$⟫ u)) (-[a∙u]≈₂a∙[-u] b (f ⟪$⟫ v)) ⟩
        a ∙₂ (π ⟨$⟩ u) +₂ b ∙₂ (π ⟨$⟩ v)
      ∎
  } where π : setoid₁ ⟶ setoid₂
          π = record
            { _⟨$⟩_ = λ x → -₂ f ⟪$⟫ x
            ; cong  = λ r → -₂‿cong (⟦⟧-cong f r)
            }

infixr 25 _+_
_+_ : Op₂ V
f + g = record
  { ⟦_⟧ = λ x -> (f ⟪$⟫ x) +₂ (g ⟪$⟫ x)
  ; isLinearMap = linear V₁-space V₂-space π
    let reassoc : ∀ (u v u' v' : V₂) -> (u +₂ v) +₂ (u' +₂ v') ≈₂ (u +₂ u') +₂ (v +₂ v')
        reassoc u v u' v' =
          begin
            (u +₂ v) +₂ (u' +₂ v')
          ≈⟨ +₂-assoc u v (u' +₂ v') ⟩
            u +₂ (v +₂ (u' +₂ v'))
          ≈⟨ +₂-cong ≈₂-refl (≈₂-trans (≈₂-sym (+₂-assoc v u' v')) (+₂-cong (+₂-comm v u') ≈₂-refl)) ⟩
            u +₂ ((u' +₂ v) +₂ v')
          ≈⟨ ≈₂-trans (+₂-cong ≈₂-refl (+₂-assoc u' v v')) (≈₂-sym (+₂-assoc u u' (v +₂ v'))) ⟩
            (u +₂ u') +₂ (v +₂ v')
          ∎
        distrib-f-g k w = ≈₂-sym (∙₂-+₂-distrib k (f ⟪$⟫ w) (g ⟪$⟫ w))
    in λ a b u v →
      begin
        π ⟨$⟩ a ∙₁ u +₁ b ∙₁ v
      ≡⟨⟩
        (f ⟪$⟫ (a ∙₁ u +₁ b ∙₁ v)) +₂ (g ⟪$⟫ (a ∙₁ u +₁ b ∙₁ v))
      ≈⟨ +₂-cong (distrib-linear f a b u v) (distrib-linear g a b u v) ⟩
        (a ∙₂ (f ⟪$⟫ u) +₂ b ∙₂ (f ⟪$⟫ v)) +₂ ((a ∙₂ (g ⟪$⟫ u) +₂ b ∙₂ (g ⟪$⟫ v)))
      ≈⟨ reassoc (a ∙₂ (f ⟪$⟫ u)) (b ∙₂ (f ⟪$⟫ v)) (a ∙₂ (g ⟪$⟫ u)) (b ∙₂ (g ⟪$⟫ v)) ⟩
        (a ∙₂ (f ⟪$⟫ u) +₂ a ∙₂ (g ⟪$⟫ u)) +₂ ((b ∙₂ (f ⟪$⟫ v)) +₂ b ∙₂ (g ⟪$⟫ v))
      ≈⟨ +₂-cong (distrib-f-g a u) (distrib-f-g b v) ⟩
        a ∙₂ (π ⟨$⟩ u) +₂ b ∙₂ (π ⟨$⟩ v)
      ∎
  } where π : setoid₁ ⟶ setoid₂
          π = record
            { _⟨$⟩_ = λ x → (f ⟪$⟫ x) +₂ (g ⟪$⟫ x)
            ; cong  = λ r → +₂-cong (⟦⟧-cong f r) (⟦⟧-cong g r)
            }

infixr 30 _∙_
_∙_ : K' -> V -> V
c ∙ f = record
  { ⟦_⟧ = λ x → c ∙₂ (f ⟪$⟫ x)
  ; isLinearMap = linear V₁-space V₂-space π
    λ a b u v →
      begin
        π ⟨$⟩ a ∙₁ u +₁ b ∙₁ v
      ≈⟨ ∙₂-cong ≈ᵏ-refl (distrib-linear f a b u v) ⟩
        c ∙₂ (a ∙₂ (f ⟪$⟫ u) +₂ b ∙₂ (f ⟪$⟫ v))
      ≈⟨ ∙₂-+₂-distrib c (a ∙₂ (f ⟪$⟫ u)) ( b ∙₂ (f ⟪$⟫ v)) ⟩
        (c ∙₂ (a ∙₂ (f ⟪$⟫ u))) +₂ (c ∙₂ (b ∙₂ (f ⟪$⟫ v)))
      ≈⟨ +₂-cong (∙₂-∙₂-comm c a (f ⟪$⟫ u)) (∙₂-∙₂-comm c b (f ⟪$⟫ v)) ⟩
        a ∙₂ (π ⟨$⟩ u) +₂ b ∙₂ (π ⟨$⟩ v)
      ∎
  } where π : setoid₁ ⟶ setoid₂
          π = record
            { _⟨$⟩_ = λ x → c ∙₂ (f ⟪$⟫ x)
            ; cong  = λ r → ∙₂-cong ≈ᵏ-refl (⟦⟧-cong f r)
            }

+-cong : Congruent₂ _+_
+-cong r₁ r₂ = λ rₓ -> +₂-cong (r₁ rₓ) (r₂ rₓ)

+-assoc : Associative _+_
+-assoc f g h {y = y} rₓ = ≈₂-trans
  (+₂-cong (+₂-cong (⟦⟧-cong f rₓ) (⟦⟧-cong g rₓ)) (⟦⟧-cong h rₓ))
  (+₂-assoc (f ⟪$⟫ y) (g ⟪$⟫ y) (h ⟪$⟫ y))

+-identityˡ : LeftIdentity 0# _+_
+-identityˡ  f {x} rₓ = ≈₂-trans
  (+₂-identityˡ (f ⟪$⟫ x))
  (⟦⟧-cong f rₓ)

+-identityʳ : RightIdentity 0# _+_
+-identityʳ f {x} rₓ = ≈₂-trans
  (+₂-identityʳ (f ⟪$⟫ x))
  (⟦⟧-cong f rₓ)

+-identity : Identity 0# _+_
+-identity = +-identityˡ , +-identityʳ

+-comm : Commutative _+_
+-comm f g {x} rₓ = ≈₂-trans
  (+₂-comm (f ⟪$⟫ x) (g ⟪$⟫ x))
  (+₂-cong (⟦⟧-cong g rₓ) (⟦⟧-cong f rₓ))

*ᵏ-∙-compat : ∀ (a b : K') (f : V) -> ((a *ᵏ b) ∙ f) ≈ (a ∙ (b ∙ f))
*ᵏ-∙-compat a b f {x} rₓ = ≈₂-trans
  (*ᵏ-∙₂-compat a b (f ⟪$⟫ x))
  (∙₂-cong ≈ᵏ-refl (∙₂-cong ≈ᵏ-refl (⟦⟧-cong f rₓ)))

∙-+-distrib : ∀ (a : K') (f g : V) -> (a ∙ (f + g)) ≈ ((a ∙ f) + (a ∙ g))
∙-+-distrib a f g {x} rₓ = ≈₂-trans
  (∙₂-+₂-distrib a (f ⟪$⟫ x) (g ⟪$⟫ x))
  (+₂-cong (∙₂-cong ≈ᵏ-refl (⟦⟧-cong f rₓ)) (∙₂-cong ≈ᵏ-refl (⟦⟧-cong g rₓ)))

∙-+ᵏ-distrib : ∀ (a b : K') (f : V) -> ((a +ᵏ b) ∙ f) ≈ ((a ∙ f) + (b ∙ f))
∙-+ᵏ-distrib a b f {x} rₓ = ≈₂-trans
  (∙₂-+ᵏ-distrib a b (f ⟪$⟫ x))
  (+₂-cong cf cf)
  where cf : ∀ {c : K'} -> _
        cf {c} = ∙₂-cong (≈ᵏ-refl {c}) (⟦⟧-cong f rₓ)

∙-cong : ∀ {a b : K'} {f g : V} -> a ≈ᵏ b -> f ≈ g -> (a ∙ f) ≈ (b ∙ g)
∙-cong {f = f} {g = g} rk rf rₓ = ≈₂-trans
  (∙₂-cong rk (rf rₓ))
  (∙₂-cong ≈ᵏ-refl (⟦⟧-cong g ≈₁-refl))

∙-identity : ∀ (f : V) → (1ᵏ ∙ f) ≈ f
∙-identity f {x} rₓ = ≈₂-trans (∙₂-identity (f ⟪$⟫ x)) (⟦⟧-cong f rₓ)

∙-absorbˡ : ∀ (x : V) → (0ᵏ ∙ x) ≈ 0#
∙-absorbˡ f {x} _ = ≈₂-trans (∙₂-absorbˡ (f ⟪$⟫ x)) ≈₂-refl

-‿inverseˡ : LeftInverse 0# -_ _+_
-‿inverseˡ f {x} _ = ≈₂-trans (-₂‿inverseˡ (f ⟪$⟫ x)) ≈₂-refl

-‿inverseʳ : RightInverse 0# -_ _+_
-‿inverseʳ f {x} _ = -₂‿inverseʳ (f ⟪$⟫ x)

-‿inverse : Inverse 0# -_ _+_
-‿inverse = -‿inverseˡ , -‿inverseʳ

-‿cong : Congruent₁ -_
-‿cong r rₓ = -₂‿cong (r rₓ)

isMagma : IsMagma _+_
isMagma = record
  { isEquivalence = ≈-isEquiv
  -- I don't know how to solve this: I'd like to write simply ∙-cong = +-cong
  ; ∙-cong        = λ {f} {g} {u} {v} -> +-cong {f} {g} {u} {v}
  }

isSemigroup : IsSemigroup _+_
isSemigroup = record
  { isMagma = isMagma
  ; assoc   = +-assoc
  }

isMonoid : IsMonoid _+_ 0#
isMonoid = record
  { isSemigroup = isSemigroup
  ; identity    = +-identity
  }

isGroup : IsGroup _+_ 0# -_
isGroup = record
  { isMonoid = isMonoid
  ; inverse  = -‿inverse
  ; ⁻¹-cong   = λ {f} {g} -> -‿cong {f} {g}
  }

isAbelianGroup : IsAbelianGroup _+_ 0# -_
isAbelianGroup = record
  { isGroup = isGroup
  ; comm    = +-comm
  }

isVectorSpace : IsVectorSpace K _≈_ _+_ _∙_ -_ 0#
isVectorSpace = record
  { isAbelianGroup = isAbelianGroup
  ; *ᵏ-∙-compat      = *ᵏ-∙-compat
  ; ∙-+-distrib      = ∙-+-distrib
  ; ∙-+ᵏ-distrib     = ∙-+ᵏ-distrib
  ; ∙-cong           = λ {a} {b} {f} {g} -> ∙-cong {a} {b} {f} {g}
  ; ∙-identity       = ∙-identity
  ; ∙-absorbˡ         = ∙-absorbˡ
  }

vectorSpace : VectorSpace K (suc (k ⊔ a₁ ⊔ a₂ ⊔ ℓ₁ ⊔ ℓ₂)) (a₁ ⊔ ℓ₁ ⊔ ℓ₂)
vectorSpace = record { isVectorSpace = isVectorSpace }

max_stars_repo_name: felko/linear-algebra

max_issues_repo_name: felko/linear-algebra

max_forks_repo_name: felko/linear-algebra


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Functions.Definition
open import Groups.Groups
open import Groups.Definition
open import Rings.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Naturals
open import Numbers.Naturals.Order
open import Numbers.Naturals.Order.Lemmas
open import Numbers.Integers.Integers
open import Numbers.Primes.PrimeNumbers
open import Numbers.Modulo.Definition
open import Numbers.Modulo.Group
open import Numbers.Naturals.EuclideanAlgorithm
open import Orders.Total.Definition

module Rings.Examples.Proofs where
  nToZn' : (n : ℕ) (pr : 0 <N n) (x : ℕ) → ℤn n pr
  nToZn' 0 ()
  nToZn' (succ n) pr x with divisionAlg (succ n) x
  nToZn' (succ n) pr1 x | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl thing ; quotSmall = quotSmall } = record { x = rem ; xLess = thing }
  nToZn' (succ n) pr1 x | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inr () ; quotSmall = quotSmall }

  mod' : (n : ℕ) → (pr : 0 <N n) → ℤ → ℤn n pr
  mod' zero () a
  mod' (succ n) pr (nonneg x) = nToZn' (succ n) pr x
  mod' (succ n) pr (negSucc x) = Group.inverse (ℤnGroup (succ n) pr) (nToZn' (succ n) pr (succ x))

  subtractionEquiv : (a : ℕ) → {b c : ℕ} → (c<b : c <N b) → a +N c ≡ b → a ≡ subtractionNResult.result (-N (inl c<b))
  subtractionEquiv 0 {b} {c} c<b pr rewrite pr = exFalso (TotalOrder.irreflexive ℕTotalOrder c<b)
  subtractionEquiv (succ a) {b} {c} c<b pr = equivalentSubtraction 0 b (succ a) c (succIsPositive a) c<b (equalityCommutative pr)

  modNExampleSurjective' : (n : ℕ) → (pr : 0 <N n) → Surjection (mod' n pr)
  modNExampleSurjective' zero ()
  modNExampleSurjective' (succ n) pr record { x = x ; xLess = xLess } with divisionAlg (succ n) x
  modNExampleSurjective' (succ n) p record { x = x ; xLess = xLess } | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = q } = nonneg x , lhs'
    where
      rs' : rem ≡ x
      rs' = modIsUnique (record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = q }) (record { quot = 0 ; rem = x ; pr = blah ; remIsSmall = inl (<NProp xLess) ; quotSmall = inl (succIsPositive n) })
        where
          blah : n *N 0 +N x ≡ x
          blah rewrite multiplicationNIsCommutative n 0 = refl
      lhs : nToZn' (succ n) p x ≡ record { x = rem ; xLess = remIsSmall }
      lhs with divisionAlg (succ n) x
      lhs | record { quot = quot' ; rem = rem' ; pr = pr' ; remIsSmall = inl t ; quotSmall = quotSmall } = equalityZn (equalityCommutative rs)
        where
          rs : rem ≡ rem'
          rs = modIsUnique (record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl remIsSmall; quotSmall = q }) (record { quot = quot' ; rem = rem' ; pr = pr' ; remIsSmall = inl t ; quotSmall = quotSmall })
      lhs | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inr () ; quotSmall = quotSmall }
      lhs' : nToZn' (succ n) p x ≡ record { x = x ; xLess = xLess }
      lhs' = transitivity lhs (equalityZn rs')
  modNExampleSurjective' (succ n) p record { x = x ; xLess = xLess } | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inr () ; quotSmall = quotSmall }

{-
  modNExampleGroupHom' : (n : ℕ) → (pr : 0 <N n) → GroupHom ℤGroup (ℤnGroup n pr) (mod' n pr)
  modNExampleGroupHom' 0 ()
  GroupHom.wellDefined (modNExampleGroupHom' (succ n) pr) {x} {.x} refl = refl
  GroupHom.groupHom (modNExampleGroupHom' (succ n) _) {nonneg a} {nonneg b} with divisionAlg (succ n) a
  GroupHom.groupHom (modNExampleGroupHom' (succ n) _) {nonneg a} {nonneg b} | record { quot = quotA ; rem = remA ; pr = prA ; remIsSmall = inl remA<sn ; quotSmall = quotSmallA } with divisionAlg (succ n) b
  GroupHom.groupHom (modNExampleGroupHom' (succ n) _) {nonneg a} {nonneg b} | record { quot = quotA ; rem = remA ; pr = prA ; remIsSmall = inl remA<sn ; quotSmall = quotSmallA } | record { quot = quotB ; rem = remB ; pr = prB ; remIsSmall = inl remB<sn ; quotSmall = quotSmallB } with orderIsTotal (remA +N remB) (succ n)
  GroupHom.groupHom (modNExampleGroupHom' (succ n) pr1) {nonneg a} {nonneg b} | record { quot = quotA ; rem = remA ; pr = prA ; remIsSmall = inl remA<sn ; quotSmall = _ } | record { quot = quotB ; rem = remB ; pr = prB ; remIsSmall = inl remB<sn ; quotSmall = _ } | inl (inl rarb<sn) rewrite addingNonnegIsHom a b = equalityZn _ _ lemma
    where
      lemma : ℤn.x (nToZn' (succ n) pr1 (a +N b)) ≡ remA +N remB
      lemma with divisionAlg (succ n) (a +N b)
      lemma | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl x ; quotSmall = inl _ } = equalityCommutative thing5
        where
          thing : ((succ n) *N quotA +N remA) +N ((succ n) *N quotB +N remB) ≡ a +N b
          thing rewrite prA | prB = refl
          thing2 : ((succ n) *N quotA +N remA) +N ((succ n) *N quotB +N remB) ≡ (succ n) *N quot +N rem
          thing2 rewrite pr = thing
          thing3 : (((succ n) *N quotA) +N ((succ n) *N quotB)) +N (remA +N remB) ≡ (succ n) *N quot +N rem
          thing3 rewrite equalityCommutative (additionNIsAssociative (((succ n) *N quotA) +N ((succ n) *N quotB)) remA remB) | additionNIsAssociative ((succ n) *N quotA) ((succ n) *N quotB) remA | additionNIsCommutative ((succ n) *N quotB) remA | equalityCommutative (additionNIsAssociative ((succ n) *N quotA) remA ((succ n) *N quotB)) | additionNIsAssociative ((succ n) *N quotA +N remA) ((succ n) *N quotB) remB = thing2
          thing4 : (succ n) *N (quotA +N quotB) +N (remA +N remB) ≡ (succ n) *N quot +N rem
          thing4 rewrite productDistributes (succ n) quotA quotB = thing3
          thing5 : remA +N remB ≡ rem
          thing5 = modUniqueLemma {remA +N remB} {rem} {succ n} (quotA +N quotB) quot rarb<sn x thing4
      lemma | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl x ; quotSmall = inr () }
      lemma | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inr () ; quotSmall = quotSmall }
  GroupHom.groupHom (modNExampleGroupHom' (succ n) pr1) {nonneg a} {nonneg b} | record { quot = quotA ; rem = remA ; pr = prA ; remIsSmall = inl remA<sn } | record { quot = quotB ; rem = remB ; pr = prB ; remIsSmall = inl remB<sn } | inl (inr sn<rarb) rewrite addingNonnegIsHom a b = equalityZn _ _ lemma
    where
      lemma : ℤn.x (nToZn' (succ n) pr1 (a +N b)) ≡ subtractionNResult.result (-N (inl sn<rarb))
      lemma with divisionAlg (succ n) (a +N b)
      lemma | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl x ; quotSmall = q } = modIsUnique record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl x ; quotSmall = q } record { quot = succ quotA +N quotB ; rem = subtractionNResult.result (-N (inl sn<rarb)) ; pr = answer ; remIsSmall = inl remSmall ; quotSmall = inl (succIsPositive n) }
        where
          transform : (a : ℕ) → {b c : ℕ} → (p : b <N c) → c <N a +N b → subtractionNResult.result (-N (inl p)) <N a
          transform a {b} {c} pr (le y proof1) with addIntoSubtraction (succ y) {b} {c} (inl pr)
          ... | bl = le y (transitivity bl (equalityCommutative (subtractionEquiv a (orderIsTransitive pr (addingIncreases c y)) (equalityCommutative (identityOfIndiscernablesLeft _ _ _ _≡_ proof1 (additionNIsCommutative (succ y) c))))))
          thing : ((succ n) *N quotA +N remA) +N ((succ n) *N quotB +N remB) ≡ a +N b
          thing rewrite prA | prB = refl
          thing2 : (((succ n) *N quotA) +N ((succ n) *N quotB)) +N (remA +N remB) ≡ a +N b
          thing2 = identityOfIndiscernablesLeft _ _ _ _≡_ thing (transitivity (equalityCommutative (additionNIsAssociative ((quotA +N n *N quotA) +N remA) (succ n *N quotB) remB)) (transitivity (applyEquality (λ i → i +N remB) (additionNIsAssociative (quotA +N n *N quotA) remA (quotB +N n *N quotB))) (transitivity (applyEquality (λ i → ((quotA +N n *N quotA) +N i) +N remB) (additionNIsCommutative remA (quotB +N n *N quotB))) (transitivity (applyEquality (λ i → i +N remB) (equalityCommutative (additionNIsAssociative (quotA +N n *N quotA) (quotB +N n *N quotB) remA))) (additionNIsAssociative _ remA remB)))))
          thing3 : (succ n) *N (quotA +N quotB) +N (remA +N remB) ≡ a +N b
          thing3 = identityOfIndiscernablesLeft _ _ _ _≡_ thing2 (equalityCommutative (applyEquality (λ i → i +N (remA +N remB)) (productDistributes (succ n) (quotA) quotB)))
          answer : (succ n *N succ (quotA +N quotB)) +N subtractionNResult.result (-N (inl sn<rarb)) ≡ a +N b
          answer with addIntoSubtraction (succ n *N succ (quotA +N quotB)) (inl sn<rarb)
          ... | bl = transitivity bl (moveOneSubtraction' {a<=b = inl (orderIsTransitive sn<rarb (addingIncreases (remA +N remB) ((quotA +N quotB) +N n *N succ (quotA +N quotB))))} answer')
            where
              snTimes1 : succ n ≡ succ n *N 1
              snTimes1 rewrite multiplicationNIsCommutative (succ n) 1 | additionNIsCommutative (succ n) 0 = refl
              q' : succ n *N succ (quotA +N quotB) ≡ succ n +N (succ n *N (quotA +N quotB))
              q' rewrite additionNIsCommutative (succ n) (succ n *N (quotA +N quotB)) | snTimes1 | equalityCommutative (productDistributes (succ n) (quotA +N quotB) 1) = applyEquality (λ i → (succ n) *N i) (succIsAddOne (quotA +N quotB))
              answer'' : (succ n *N succ (quotA +N quotB)) +N (remA +N remB) ≡ (succ n) +N ((succ n *N (quotA +N quotB)) +N (remA +N remB))
              answer'' rewrite equalityCommutative (additionNIsAssociative (succ n) (succ n *N (quotA +N quotB)) (remA +N remB)) = applyEquality (λ i → i +N (remA +N remB)) q'
              answer' : (remA +N remB) +N (succ n *N succ (quotA +N quotB)) ≡ succ n +N (a +N b)
              answer' rewrite equalityCommutative thing3 = transitivity (additionNIsCommutative (remA +N remB) (succ n *N succ (quotA +N quotB))) answer''
          remSmall : subtractionNResult.result (-N (inl sn<rarb)) <N succ n
          remSmall = transform (succ n) sn<rarb (addStrongInequalities remA<sn remB<sn)
      lemma | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inr () ; quotSmall = quotSmall }
  GroupHom.groupHom (modNExampleGroupHom' (succ n) pr1) {nonneg a} {nonneg b} | record { quot = quotA ; rem = remA ; pr = prA ; remIsSmall = inl remA<sn } | record { quot = quotB ; rem = remB ; pr = prB ; remIsSmall = inl remB<sn } | inr rarb=sn rewrite addingNonnegIsHom a b = equalityZn _ _ lemma
    where
      lemma : ℤn.x (nToZn' (succ n) pr1 (a +N b)) ≡ 0
      lemma with divisionAlg (succ n) (a +N b)
      lemma | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl x } = equalityCommutative (modUniqueLemma ((quotA +N quotB) +N 1) quot pr1 x thing7)
        where
          thing : ((succ n) *N quotA +N remA) +N ((succ n) *N quotB +N remB) ≡ a +N b
          thing rewrite prA | prB = refl
          thing2 : ((succ n) *N quotA +N remA) +N ((succ n) *N quotB +N remB) ≡ (succ n) *N quot +N rem
          thing2 rewrite pr = thing
          thing3 : (((succ n) *N quotA) +N ((succ n) *N quotB)) +N (remA +N remB) ≡ (succ n) *N quot +N rem
          thing3 rewrite equalityCommutative (additionNIsAssociative (((succ n) *N quotA) +N ((succ n) *N quotB)) remA remB) | additionNIsAssociative ((succ n) *N quotA) ((succ n) *N quotB) remA | additionNIsCommutative ((succ n) *N quotB) remA | equalityCommutative (additionNIsAssociative ((succ n) *N quotA) remA ((succ n) *N quotB)) | additionNIsAssociative ((succ n) *N quotA +N remA) ((succ n) *N quotB) remB = thing2
          thing4 : (succ n) *N (quotA +N quotB) +N (remA +N remB) ≡ (succ n) *N quot +N rem
          thing4 rewrite productDistributes (succ n) quotA quotB = thing3
          thing5 : (succ n) *N (quotA +N quotB) +N (succ n) ≡ (succ n) *N quot +N rem
          thing5 rewrite equalityCommutative rarb=sn = thing4
          thing6 : (succ n) *N ((quotA +N quotB) +N 1) ≡ (succ n) *N quot +N rem
          thing6 rewrite productDistributes (succ n) (quotA +N quotB) 1 | multiplicationNIsCommutative n 1 | additionNIsCommutative n 0 = thing5
          thing7 : (succ n) *N ((quotA +N quotB) +N 1) +N 0 ≡ (succ n) *N quot +N rem
          thing7 = identityOfIndiscernablesLeft _ _ _ _≡_ thing6 (additionNIsCommutative 0 _)
      lemma | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inr () ; quotSmall = quotSmall }
  GroupHom.groupHom (modNExampleGroupHom' (succ n) _) {nonneg a} {nonneg b} | record { quot = quotA ; rem = remA ; pr = prA ; remIsSmall = inl remA<sn ; quotSmall = quotSmallA } | record { quot = quotB ; rem = remB ; pr = prB ; remIsSmall = inr () ; quotSmall = quotSmallB }
  GroupHom.groupHom (modNExampleGroupHom' (succ n) _) {nonneg a} {nonneg b} | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inr () ; quotSmall = quotSmall }
  GroupHom.groupHom (modNExampleGroupHom' (succ n) _) {nonneg a} {negSucc b} with divisionAlg (succ n) a
  GroupHom.groupHom (modNExampleGroupHom' (succ n) _) {nonneg a} {negSucc b} | record { quot = quotA ; rem = remA ; pr = prA ; remIsSmall = remIsSmallA ; quotSmall = quotSmallA } = {!!}
  GroupHom.groupHom (modNExampleGroupHom' (succ n) _) {negSucc x} {nonneg b} with divisionAlg (succ n) (succ x)
  ... | bl = {!!}
  GroupHom.groupHom (modNExampleGroupHom' (succ n) _) {negSucc x} {negSucc b} with divisionAlg (succ n) (succ x)
  ... | bl = {!!}

-}

ext: agda


text:
module Common.Weakening where

-- open import Agda.Primitive
import Data.List as List
open import Data.List.Base
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.All as All
open import Data.List.Prefix
open import Function
open import Level

{-
  The following `Weakenable` record defines a class of weakenable (or
  monotone) predicates over lists.

  We can make the definitions of `Weakenable` available using the
  syntax:

  open Weakenable ⦃...⦄ public

  Whenever we use `wk e p` where `e : x ⊑ x'`, `p : P x` where `x x' :
  List X`, Agda will use instance argument search to find a defined
  instance of `Weakenable {X} P`.  See also
  http://agda.readthedocs.io/en/v2.5.3/language/instance-arguments.html
-}

record Weakenable {i j}{A : Set i}(p : List A → Set j) : Set (i ⊔ j) where
  field wk : ∀ {w w'} → w ⊑ w' → p w → p w'

{-
  In general, weakenable predicates can be defined over *any* preorder.
  See `Experiments.Category` for a more general definition and
  treatment.

  The definition of `Weakenable` above is specialized to the
  interpreters in our paper which are all defined in terms of
  weakenable predicates over lists.
-}

open Weakenable ⦃...⦄ public

{-
  We define a few derived instances of `Weakenable` that appear
  commonly.
-}

module _ {i} {A : Set i} where
  instance
    any-weakenable : ∀ {x : A} → Weakenable (λ xs → x ∈ xs)
    any-weakenable = record { wk = λ ext l → ∈-⊒ l ext }

    all-weakenable : ∀ {j} {B : Set j} {xs : List B}
                   → ∀ {k} {C : B → List A → Set k} {{wₐ : ∀ {x} → Weakenable (C x)}}
                   → Weakenable (λ ys → All (λ x → C x ys) xs)
    all-weakenable {{wₐ}} = record {
      wk = λ ext v → All.map (λ {a} y → Weakenable.wk wₐ ext y) v }

    -- const-weakenable : ∀ {j}{I : Set j} → Weakenable {A = I} (λ _ → A)
    -- const-weakenable = record { wk = λ ext c → c }

    list-weakenable : ∀ {b}{B : List A → Set b}
                    → {{wb : Weakenable B}} → Weakenable (λ W → List (B W))
    list-weakenable {{ wₐ }} = record {wk = λ ext v → List.map (wk ext) v }

-- Nicer syntax for transitivity of prefixes:
infixl 30 _⊚_
_⊚_ : ∀ {i} {A : Set i} {W W' W'' : List A} → W' ⊒ W → W'' ⊒ W' → W'' ⊒ W
_⊚_ co₁ co₂ = ⊑-trans co₁ co₂

{-
  Another common construction is that of products of weakenable
  predicates.  Section 3.4 defines this type, which corresponds to
  `_∩_` from the Agda Standard Library:
-}
open import Relation.Unary
open import Data.Product
_⊗_ : ∀ {a}{i j}{W : Set a}(p : W → Set i)(q : W → Set j)(w : W) → Set (i ⊔ j)
_⊗_ = _∩_

-- We prove that when `_⊗_` is a product of two weakenable predicates,
-- then `_⊗_` is an instance of `Weakenable`:
instance
  weaken-pair : ∀ {a}{A : Set a}{i j}{p : List A → Set i}{q : List A → Set j}
              → {{wp : Weakenable p}} {{wq : Weakenable q}}
              → Weakenable (p ⊗ q)
  weaken-pair = record { wk = λ{ ext (x , y) → (wk ext x , wk ext y) } }


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

open import Cubical.Foundations.Pointed.Base public
open import Cubical.Foundations.Pointed.Properties public
open import Cubical.Foundations.Pointed.FunExt public
open import Cubical.Foundations.Pointed.Homotopy public

open import Cubical.Foundations.Pointed.Homogeneous

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
postulate
  A B : Set
  f : A → B

data D : B → Set where
  c : {n : A} → D (f n)

test : (x : B) → D x → Set
test n c = {!!}

test2 : Set
test2 =
  let X = A in
  let X = B in
  {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module ProcessRun where

open import Data.Bool
open import Data.List
open import Data.Maybe
open import Data.Product

open import Relation.Binary.PropositionalEquality

open import Typing
open import ProcessSyntax

open import Channel
open import Global
open import Values
open import Session
open import Schedule

-- auxiliary lemmas
list-right-zero : ∀ {A : Set} → (xs : List A) → xs ++ [] ≡ xs
list-right-zero [] = refl
list-right-zero (x ∷ xs) = cong (_∷_ x) (list-right-zero xs)

list-assoc : ∀ {A : Set} → (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
list-assoc [] ys zs = refl
list-assoc (x ∷ xs) ys zs = cong (_∷_ x) (list-assoc xs ys zs)

cons-assoc : ∀ {A : Set} → (x : A) (xs ys : List A) → (x ∷ xs) ++ ys ≡ x ∷ (xs ++ ys)
cons-assoc x xs ys = refl

inactive-clone : (G : SCtx) → SCtx
inactive-clone [] = []
inactive-clone (x ∷ G) = nothing ∷ inactive-clone G

inactive-extension : ∀ {G} → Inactive G → (G' : SCtx) → Inactive (inactive-clone G' ++ G)
inactive-extension inaG [] = inaG
inactive-extension inaG (x ∷ G') = ::-inactive (inactive-extension inaG G')

splitting-extension : ∀ {G G₁ G₂} (G' : SCtx)
  → SSplit G G₁ G₂ → SSplit (inactive-clone G' ++ G) (inactive-clone G' ++ G₁) (inactive-clone G' ++ G₂)
splitting-extension [] ss = ss
splitting-extension (x ∷ G') ss = ss-both (splitting-extension G' ss)

left-right : (G' G'' : SCtx)
  → SSplit (G' ++ G'') (G' ++ inactive-clone G'') (inactive-clone G' ++ G'')
left-right [] [] = ss-[]
left-right [] (just x ∷ G'') = ss-right (left-right [] G'')
left-right [] (nothing ∷ G'') = ss-both (left-right [] G'')
left-right (x ∷ G') G'' with left-right G' G''
... | ss-G'G'' with x
left-right (x ∷ G') G'' | ss-G'G'' | just x₁ = ss-left ss-G'G''
left-right (x ∷ G') G'' | ss-G'G'' | nothing = ss-both ss-G'G''

ssplit-append : { G11 G12  G21 G22 : SCtx} (G1 G2 : SCtx) → SSplit G1 G11 G12 → SSplit G2 G21 G22 → SSplit (G1 ++ G2) (G11 ++ G21) (G12 ++ G22)
ssplit-append _ _ ss-[] ss2 = ss2
ssplit-append _ _ (ss-both ss1) ss2 = ss-both (ssplit-append _ _ ss1 ss2)
ssplit-append _ _ (ss-left ss1) ss2 = ss-left (ssplit-append _ _ ss1 ss2)
ssplit-append _ _ (ss-right ss1) ss2 = ss-right (ssplit-append _ _ ss1 ss2)
ssplit-append _ _ (ss-posneg ss1) ss2 = ss-posneg (ssplit-append _ _ ss1 ss2)
ssplit-append _ _ (ss-negpos ss1) ss2 = ss-negpos (ssplit-append _ _ ss1 ss2)

-- weakening #1
weaken1-cr : ∀ {G b s} G' → ChannelRef G b s → ChannelRef (inactive-clone G' ++ G) b s
weaken1-cr [] cr = cr
weaken1-cr (x ∷ G') cr = there (weaken1-cr G' cr)

weaken1-val : ∀ {G t} G' → Val G t → Val (inactive-clone G' ++ G) t
weaken1-venv : ∀ {G Φ} G' → VEnv G Φ → VEnv (inactive-clone G' ++ G) Φ

weaken1-val G' (VUnit inaG) = VUnit (inactive-extension inaG G')
weaken1-val G' (VInt i inaG) = VInt i (inactive-extension inaG G')
weaken1-val G' (VPair ss-GG₁G₂ v v₁) = VPair (splitting-extension G' ss-GG₁G₂) (weaken1-val G' v) (weaken1-val G' v₁)
weaken1-val G' (VChan b vcr) = VChan b (weaken1-cr G' vcr)
weaken1-val G' (VFun x ϱ e) = VFun x (weaken1-venv G' ϱ) e
weaken1-venv G' (vnil ina) = vnil (inactive-extension ina G')
weaken1-venv G' (vcons ssp v ϱ) = vcons (splitting-extension G' ssp) (weaken1-val G' v) (weaken1-venv G' ϱ)

weaken1-cont : ∀ {G t φ} G' → Cont G φ t → Cont (inactive-clone G' ++ G) φ t
weaken1-cont G' (halt inaG un-t) = halt (inactive-extension inaG G') un-t
weaken1-cont G' (bind ts ss e₂ ϱ₂ κ) = bind ts (splitting-extension G' ss) e₂ (weaken1-venv G' ϱ₂) (weaken1-cont G' κ)
weaken1-cont G' (bind-thunk ts ss e₂ ϱ₂ κ) = bind-thunk ts (splitting-extension G' ss) e₂ (weaken1-venv G' ϱ₂) (weaken1-cont G' κ)
weaken1-cont G' (subsume x κ) = subsume x (weaken1-cont G' κ)

weaken1-command : ∀ {G} G' → Command G → Command (inactive-clone G' ++ G)
weaken1-command G' (Fork ss κ₁ κ₂) = Fork (splitting-extension G' ss) (weaken1-cont G' κ₁) (weaken1-cont G' κ₂)
weaken1-command G' (Ready ss v κ) = Ready (splitting-extension G' ss) (weaken1-val G' v) (weaken1-cont G' κ)
weaken1-command G' (Halt x x₁ x₂) = Halt (inactive-extension x G') x₁ (weaken1-val G' x₂)
weaken1-command G' (New s κ) = New s (weaken1-cont G' κ)
weaken1-command G' (Close ss v κ) = Close (splitting-extension G' ss) (weaken1-val G' v) (weaken1-cont G' κ)
weaken1-command G' (Wait ss v κ) = Wait (splitting-extension G' ss) (weaken1-val G' v) (weaken1-cont G' κ)
weaken1-command G' (Send ss ss-args vch v κ) = Send (splitting-extension G' ss) (splitting-extension G' ss-args) (weaken1-val G' vch) (weaken1-val G' v) (weaken1-cont G' κ)
weaken1-command G' (Recv ss vch κ) = Recv (splitting-extension G' ss) (weaken1-val G' vch) (weaken1-cont G' κ)
weaken1-command G' (Select ss lab vch κ) = Select (splitting-extension G' ss) lab (weaken1-val G' vch) (weaken1-cont G' κ)
weaken1-command G' (Branch ss vch dcont) = Branch (splitting-extension G' ss) (weaken1-val G' vch) λ lab → weaken1-cont G' (dcont lab)
weaken1-command G' (NSelect ss lab vch κ) = NSelect (splitting-extension G' ss) lab (weaken1-val G' vch) (weaken1-cont G' κ)
weaken1-command G' (NBranch ss vch dcont) = NBranch (splitting-extension G' ss) (weaken1-val G' vch) λ lab → weaken1-cont G' (dcont lab)

weaken1-threadpool : ∀ {G} G' → ThreadPool G → ThreadPool (inactive-clone G' ++ G)
weaken1-threadpool G' (tnil ina) = tnil (inactive-extension ina G')
weaken1-threadpool G' (tcons ss cmd tp) = tcons (splitting-extension G' ss) (weaken1-command G' cmd) (weaken1-threadpool G' tp)

-- auxiliary

inactive-insertion : ∀ {G} G' G'' → Inactive (G' ++ G) → Inactive (G' ++ inactive-clone G'' ++ G)
inactive-insertion [] G'' ina-G'G = inactive-extension ina-G'G G''
inactive-insertion (just x ∷ G') G'' ()
inactive-insertion (nothing ∷ G') G'' (::-inactive ina-G'G) = ::-inactive (inactive-insertion G' G'' ina-G'G)

splitting-insertion : ∀ {G G₁ G₂} {G' G₁' G₂'} G''
  → SSplit G' G₁' G₂'
  → SSplit G G₁ G₂
  → SSplit (G' ++ inactive-clone G'' ++ G) (G₁' ++ inactive-clone G'' ++ G₁) (G₂' ++ inactive-clone G'' ++ G₂)
splitting-insertion G'' ss-[] ss = splitting-extension G'' ss
splitting-insertion G'' (ss-both ss') ss = ss-both (splitting-insertion G'' ss' ss)
splitting-insertion G'' (ss-left ss') ss = ss-left (splitting-insertion G'' ss' ss)
splitting-insertion G'' (ss-right ss') ss = ss-right (splitting-insertion G'' ss' ss)
splitting-insertion G'' (ss-posneg ss') ss = ss-posneg (splitting-insertion G'' ss' ss)
splitting-insertion G'' (ss-negpos ss') ss = ss-negpos (splitting-insertion G'' ss' ss)

split-append : ∀ {G G1 G2} G'
  → SSplit (G' ++ G) G1 G2
  → ∃ λ G₁' → ∃ λ G₂' → ∃ λ G₁ → ∃ λ G₂
  → SSplit G' G₁' G₂' × SSplit G G₁ G₂ × G1 ≡ G₁' ++ G₁ × G2 ≡ G₂' ++ G₂
split-append [] ss = _ , _ , _ , _ , ss-[] , ss , refl , refl
split-append (.nothing ∷ G') (ss-both ss) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = _ , _ , _ , _ , (ss-both ss') , ss0 , refl , refl
split-append (.(just _) ∷ G') (ss-left ss) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = _ , _ , _ , _ , (ss-left ss') , ss0 , refl , refl
split-append (.(just _) ∷ G') (ss-right ss) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = _ , _ , _ , _ , (ss-right ss') , ss0 , refl , refl
split-append (.(just (_ , POSNEG)) ∷ G') (ss-posneg ss) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = _ , _ , _ , _ , (ss-posneg ss') , ss0 , refl , refl
split-append (.(just (_ , POSNEG)) ∷ G') (ss-negpos ss) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = _ , _ , _ , _ , (ss-negpos ss') , ss0 , refl , refl

-- weakening #2

weaken2-cr : ∀ {G b s} G' G'' → ChannelRef (G' ++ G) b s → ChannelRef (G' ++ inactive-clone G'' ++ G) b s
weaken2-cr [] G'' cr = weaken1-cr G'' cr
weaken2-cr (.(just (_ , POS)) ∷ G') G'' (here-pos ina-G x) = here-pos (inactive-insertion G' G'' ina-G) x
weaken2-cr (.(just (_ , NEG)) ∷ G') G'' (here-neg ina-G x) = here-neg (inactive-insertion G' G'' ina-G) x
weaken2-cr (.nothing ∷ G') G'' (there cr) = there (weaken2-cr G' G'' cr)

weaken2-val : ∀ {G t} G' G'' → Val (G' ++ G) t → Val (G' ++ inactive-clone G'' ++ G) t
weaken2-venv : ∀ {G Φ} G' G'' → VEnv (G' ++ G) Φ → VEnv (G' ++ inactive-clone G'' ++ G) Φ

weaken2-val G' G'' (VUnit inaG) = VUnit (inactive-insertion G' G'' inaG)
weaken2-val G' G'' (VInt i inaG) = VInt i (inactive-insertion G' G'' inaG)
weaken2-val G' G'' (VPair ss-GG₁G₂ v₁ v₂) with split-append G' ss-GG₁G₂
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = VPair (splitting-insertion G'' ss' ss0) (weaken2-val G₁' G'' v₁) (weaken2-val G₂' G'' v₂)
weaken2-val G' G'' (VChan b vcr) = VChan b (weaken2-cr G' G'' vcr)
weaken2-val G' G'' (VFun x ϱ e) = VFun x (weaken2-venv G' G'' ϱ) e

weaken2-venv G' G'' (vnil ina) = vnil (inactive-insertion G' G'' ina)
weaken2-venv G' G'' (vcons{G₁ = Gv}{G₂ = Gϱ} ssp v ϱ) with split-append G' ssp
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = vcons (splitting-insertion G'' ss' ss0) (weaken2-val G₁' G'' v) (weaken2-venv G₂' G'' ϱ)

weaken2-cont : ∀ {G t φ} G' G'' → Cont (G' ++ G) φ t → Cont (G' ++ inactive-clone G'' ++ G) φ t
weaken2-cont G' G'' (halt x un-t) = halt (inactive-insertion G' G'' x) un-t
weaken2-cont G' G'' (bind ts ss e₂ ϱ₂ κ) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = bind ts (splitting-insertion G'' ss' ss0) e₂ (weaken2-venv G₁' G'' ϱ₂) (weaken2-cont G₂' G'' κ)
weaken2-cont G' G'' (bind-thunk ts ss e₂ ϱ₂ κ) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = bind-thunk ts (splitting-insertion G'' ss' ss0) e₂ (weaken2-venv G₁' G'' ϱ₂) (weaken2-cont G₂' G'' κ)
weaken2-cont G' G'' (subsume x κ) = subsume x (weaken2-cont G' G'' κ)

weaken2-command : ∀ {G} G' G'' → Command (G' ++ G) → Command (G' ++ inactive-clone G'' ++ G)
weaken2-command G' G'' (Fork ss κ₁ κ₂) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = Fork (splitting-insertion G'' ss' ss0) (weaken2-cont G₁' G'' κ₁) (weaken2-cont G₂' G'' κ₂)
weaken2-command G' G'' (Ready ss v κ) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = Ready (splitting-insertion G'' ss' ss0) (weaken2-val G₁' G'' v) (weaken2-cont G₂' G'' κ)
weaken2-command G' G'' (Halt x x₁ x₂) = Halt (inactive-insertion G' G'' x) x₁ (weaken2-val G' G'' x₂)
weaken2-command G' G'' (New s κ) = New s (weaken2-cont G' G'' κ)
weaken2-command G' G'' (Close ss v κ) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = Close (splitting-insertion G'' ss' ss0) (weaken2-val G₁' G'' v) (weaken2-cont G₂' G'' κ)
weaken2-command G' G'' (Wait ss v κ) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = Wait (splitting-insertion G'' ss' ss0) (weaken2-val G₁' G'' v) (weaken2-cont G₂' G'' κ)
weaken2-command G' G'' (Send ss ss-args vch v κ) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl with split-append G₁' ss-args
... | G₁₁' , G₁₂' , G₁₁ , G₁₂ , ss-args' , ss0-args , refl , refl = Send (splitting-insertion G'' ss' ss0) (splitting-insertion G'' ss-args' ss0-args) (weaken2-val G₁₁' G'' vch) (weaken2-val G₁₂' G'' v) (weaken2-cont G₂' G'' κ)
weaken2-command G' G'' (Recv ss vch κ) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = Recv (splitting-insertion G'' ss' ss0) (weaken2-val G₁' G'' vch) (weaken2-cont G₂' G'' κ)
weaken2-command G' G'' (Select ss lab vch κ) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = Select (splitting-insertion G'' ss' ss0) lab (weaken2-val G₁' G'' vch) (weaken2-cont G₂' G'' κ)
weaken2-command G' G'' (Branch ss vch dcont) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = Branch (splitting-insertion G'' ss' ss0) (weaken2-val G₁' G'' vch) λ lab → weaken2-cont G₂' G'' (dcont lab)
weaken2-command G' G'' (NSelect ss lab vch κ) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = NSelect (splitting-insertion G'' ss' ss0) lab (weaken2-val G₁' G'' vch) (weaken2-cont G₂' G'' κ)
weaken2-command G' G'' (NBranch ss vch dcont) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = NBranch (splitting-insertion G'' ss' ss0) (weaken2-val G₁' G'' vch) λ lab → weaken2-cont G₂' G'' (dcont lab)

weaken2-threadpool : ∀ {G} G' G'' → ThreadPool (G' ++ G) → ThreadPool (G' ++ inactive-clone G'' ++ G)
weaken2-threadpool G' G'' (tnil ina) = tnil (inactive-insertion G' G'' ina)
weaken2-threadpool G' G'' (tcons ss cmd tp) with split-append G' ss
... | G₁' , G₂' , G₁ , G₂ , ss' , ss0 , refl , refl = tcons (splitting-insertion G'' ss' ss0) (weaken2-command G₁' G'' cmd) (weaken2-threadpool G₂' G'' tp)

-- translate a process term to semantics (i.e., a list of commands)
runProc : ∀ {Φ} → (G : SCtx) → Proc Φ → VEnv G Φ → ∃ λ G' → ThreadPool (G' ++ G)

runProc G (exp e) ϱ with ssplit-refl-left-inactive G
... | G' , ina-G' , sp-GGG' = [] , (tcons sp-GGG' (run (split-all-left _) sp-GGG' e ϱ (halt ina-G' UUnit)) (tnil ina-G'))

runProc G (par sp P₁ P₂) ϱ with split-env sp ϱ
... | (G₁ , G₂) , ss-GG1G2 , ϱ₁ , ϱ₂ with runProc G₁ P₁ ϱ₁ | runProc G₂ P₂ ϱ₂
... | (G₁' , tp1) | (G₂' , tp2) with weaken1-threadpool G₁' tp2
... | tp2' with weaken2-threadpool G₁' G₂' tp1
... | tp1' with left-right G₁' G₂'
... | ss-G1'G2' rewrite sym (list-assoc G₁' (inactive-clone G₂') G₁) | sym (list-assoc (inactive-clone G₁') G₂' G₂) = (G₁' ++ G₂') , tappend ssfinal tp1' tp2'
  where
    ssfinal : SSplit ((G₁' ++ G₂') ++ G) ((G₁' ++ inactive-clone G₂') ++ G₁) ((inactive-clone G₁' ++ G₂') ++ G₂)
    ssfinal = ssplit-append (G₁' ++ G₂') G ss-G1'G2' ss-GG1G2

runProc G (res s P) ϱ with ssplit-refl-right-inactive G
... | G1 , ina-G1 , ss-GG1G with runProc (just (SType.force s , POSNEG) ∷ G) P (vcons (ss-posneg ss-GG1G) (VChan POS (here-pos ina-G1 (subF-refl _))) (vcons (ss-left ss-GG1G) (VChan NEG (here-neg ina-G1 (subF-refl _))) (lift-venv ϱ)))
... | G' , tp = G' ++ just (SType.force s , POSNEG) ∷ [] , tp'
  where
    tp' : ThreadPool ((G' ++ just (SType.force s , POSNEG) ∷ []) ++ G)
    tp' rewrite list-assoc G' (just (SType.force s , POSNEG) ∷ []) G = tp

startProc : Gas → Proc [] → Outcome
startProc f P with runProc [] P (vnil []-inactive)
... | G , tp = schedule f tp

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text:
{-# OPTIONS --safe --warning=error --without-K --guardedness #-}

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Groups.Lemmas
open import Groups.Definition
open import Setoids.Orders.Total.Definition
open import Setoids.Setoids
open import Functions.Definition
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Rings.Orders.Total.Definition
open import Rings.Orders.Partial.Definition
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Modulo.Definition
open import Semirings.Definition
open import Orders.Total.Definition
open import Sequences
open import Numbers.Integers.Definition
open import Numbers.Integers.Addition
open import Numbers.Integers.Multiplication
open import Numbers.Integers.Order
open import Numbers.Rationals.Definition
open import Vectors
open import Fields.Fields

module Rings.Orders.Total.Examples where

open import Rings.Orders.Total.BaseExpansion (ℚOrdered) {10} (le 8 refl)
open Field ℚField

t : Vec ℚ 5
t = take 5 (partialSums (funcToSequence injectionNQ))

u : Vec ℚ 5
u = vecMap injectionNQ (0 ,- (1 ,- (3 ,- (6 ,- (10 ,- [])))))

pr : Vec (ℚ && ℚ) 5
pr = vecZip t u

ans : vecAllTrue (λ x → _&&_.fst x =Q _&&_.snd x) pr
ans = refl ,, (refl ,, (refl ,, (refl ,, (refl ,, record {}))))

open import Rings.InitialRing ℚRing

a : Sequence ℚ
a with allInvertible (fromN 10) (λ ())
... | 1/10 , pr1/10 = approximations 1/10 pr1/10 (baseNExpansion (underlying (allInvertible (injectionNQ 7) λ ())) (lessInherits (succIsPositive 0)) (lessInherits (le 5 refl)))

expected : Vec ℚ _
expected = record { num = nonneg 1 ; denom = nonneg 10 ; denomNonzero = f } ,- record { num = nonneg 14 ; denom = nonneg 100 ; denomNonzero = λ () } ,- record { num = nonneg 142 ; denom = nonneg 1000 ; denomNonzero = λ () } ,- []
  where
    f : nonneg 10 ≡ nonneg 0 → False
    f ()

ans' : vecAllTrue (λ x → _&&_.fst x =Q _&&_.snd x) (vecZip (take _ a) expected)
ans' = refl ,, (refl ,, (refl ,, record {}))


text:
module Haskell.Prim.Eq where

open import Agda.Builtin.Nat as Nat hiding (_==_)
open import Agda.Builtin.Char
open import Agda.Builtin.Unit
open import Agda.Builtin.List

open import Haskell.Prim
open import Haskell.Prim.Bool
open import Haskell.Prim.Integer
open import Haskell.Prim.Int
open import Haskell.Prim.Word
open import Haskell.Prim.Double
open import Haskell.Prim.Tuple
open import Haskell.Prim.Maybe
open import Haskell.Prim.Either

--------------------------------------------------
-- Eq

record Eq (a : Set) : Set where
  infix 4 _==_ _/=_
  field
    _==_ : a → a → Bool

  _/=_ : a → a → Bool
  x /= y = not (x == y)

open Eq ⦃ ... ⦄ public

{-# COMPILE AGDA2HS Eq existing-class #-}

instance
  iEqNat : Eq Nat
  iEqNat ._==_ = Nat._==_

  iEqInteger : Eq Integer
  iEqInteger ._==_ = eqInteger

  iEqInt : Eq Int
  iEqInt ._==_ = eqInt

  iEqWord : Eq Word
  iEqWord ._==_ = eqWord

  iEqDouble : Eq Double
  iEqDouble ._==_ = primFloatNumericalEquality

  iEqBool : Eq Bool
  iEqBool ._==_ false false = true
  iEqBool ._==_ true  true  = true
  iEqBool ._==_ _     _     = false

  iEqChar : Eq Char
  iEqChar ._==_ = primCharEquality

  iEqUnit : Eq ⊤
  iEqUnit ._==_ _ _ = true

  iEqTuple₀ : Eq (Tuple [])
  iEqTuple₀ ._==_ _ _ = true

  iEqTuple : ∀ {as} → ⦃ Eq a ⦄ → ⦃ Eq (Tuple as) ⦄ → Eq (Tuple (a ∷ as))
  iEqTuple ._==_ (x ∷ xs) (y ∷ ys) = x == y && xs == ys

  iEqList : ⦃ Eq a ⦄ → Eq (List a)
  iEqList ._==_ []       []       = true
  iEqList ._==_ (x ∷ xs) (y ∷ ys) = x == y && xs == ys
  iEqList ._==_ _        _        = false

  iEqMaybe : ⦃ Eq a ⦄ → Eq (Maybe a)
  iEqMaybe ._==_ Nothing  Nothing  = true
  iEqMaybe ._==_ (Just x) (Just y) = x == y
  iEqMaybe ._==_ _        _        = false

  iEqEither : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (Either a b)
  iEqEither ._==_ (Left  x) (Left  y) = x == y
  iEqEither ._==_ (Right x) (Right y) = x == y
  iEqEither ._==_ _        _          = false


text:
-- 2017-05-11, Reported by Ulf
-- Implicit absurd matches should be treated in the same way as explicit ones
-- when it comes to being used/unused.

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

data ⊥ : Set where
record ⊤ : Set where

abort : (A : Set) {_ : ⊥} → A
abort A {}

test : (x y : ⊥) → abort Bool {x} ≡ abort Bool {y}
test x y = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module logical_foundations.Naturals where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ  #-}

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)
{-# BUILTIN NATPLUS _+_  #-}
-- zero + n = n             -- 0 + n = n
-- suc m + n = suc (m + n)  -- (1 + m) + n = 1 + (m + n)

infixl 6 _+_

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩
    5
  ∎

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩
    suc (1 + 3)
  ≡⟨⟩
    suc (suc (0 + 3))
  ≡⟨⟩
    suc (suc 3)
  ≡⟨⟩
    5
  ∎

_ : 2 + 3 ≡ 5
_ = refl

_ : 3 + 4 ≡ 7
_ =
  begin
    3 + 4
  ≡⟨⟩
    suc (2 + 4)
  ≡⟨⟩
    suc (suc (1 + 4))
  ≡⟨⟩
    suc (suc (suc (0 + 4)))
  ≡⟨⟩
    suc (suc (suc 4))
  ≡⟨⟩
    7
  ∎

_*_ : ℕ → ℕ → ℕ
zero * n = zero            -- 0 * n = 0
suc m * n = n + (m * n)    -- (1 + m) * n = n + (m * n)
{-# BUILTIN NATTIMES _*_  #-}

infixl 7 _*_

_ : 2 * 3 ≡ 6
_ =
  begin
    2 * 3
  ≡⟨⟩
    3 + (1 * 3)
  ≡⟨⟩
    3 + (3 + (0 * 3))
  ≡⟨⟩
    3 + (3 + 0)
  ≡⟨⟩
    6
  ∎

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

infixl 8 _^_

_ : 2 ^ 3 ≡ 8
_ =
  begin
    2 ^ 3
  ≡⟨⟩
    2 * (2 ^ 2)
  ≡⟨⟩
    2 * (2 * (2 ^ 1))
  ≡⟨⟩
    2 * (2 * (2 * (2 ^ 0)))
  ≡⟨⟩
    2 * (2 * (2 * 1))
  ≡⟨⟩
    8
  ∎

_ : 3 ^ 4 ≡ 81
_ = refl

_∸_ : ℕ → ℕ → ℕ
m ∸ zero = m
zero ∸ suc n = zero
suc m ∸ suc n = m ∸ n
{-# BUILTIN NATMINUS _∸_  #-}

infixl 6 _∸_

_ =
  begin
    3 ∸ 2
  ≡⟨⟩
    2 ∸ 1
  ≡⟨⟩
    1 ∸ 0
  ≡⟨⟩
    1
  ∎

_ =
  begin
    2 ∸ 3
  ≡⟨⟩
    1 ∸ 2
  ≡⟨⟩
    0 ∸ 1
  ≡⟨⟩
    0
  ∎

data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

inc : Bin → Bin
inc nil = x1 nil
inc (x0 b) = x1 b
inc (x1 b) = x0 (inc b)

_ : inc (x1 x1 x0 x1 nil) ≡ x0 x0 x1 x1 nil
_ = refl

_ : inc (x1 x1 x1 x1 nil) ≡ x0 x0 x0 x0 x1 nil
_ = refl

to : ℕ → Bin
to zero = x0 nil
to (suc n) = inc (to n)

_ : to 0 ≡ x0 nil
_ = refl

_ : to 1 ≡ x1 nil
_ = refl

_ : to 2 ≡ x0 x1 nil
_ = refl

_ : to 3 ≡ x1 x1 nil
_ = refl

_ : to 14 ≡ x0 x1 x1 x1 nil
_ = refl

two = suc (suc zero)

from : Bin → ℕ
from nil = zero
from (x0 n) = two * (from n)
from (x1 n) = suc (two * (from n))

_ : from nil ≡ zero
_ = refl

_ : from (x0 nil) ≡ zero
_ = refl

_ : from (x1 nil) ≡ suc zero
_ = refl

_ : from (x0 x1 nil) ≡ two
_ = refl

_ : from (x0 x1 nil) ≡ two * suc zero
_ = refl

_ : from (x1 x1 nil) ≡ suc (suc (suc zero))
_ = refl

_ : from (x1 x1 nil) ≡ suc (two * suc zero)
_ = refl

_ : from (x0 x0 x1 nil) ≡ suc (suc (suc (suc zero)))
_ = refl

_ : from (x0 x0 x1 nil) ≡ two * (two * suc zero)
_ = refl

_ : from (x1 x0 x1 nil) ≡ suc (suc (suc (suc (suc zero))))
_ = refl

_ : from (x1 x0 x1 nil) ≡ suc (two * (two * suc zero))
_ = refl

max_stars_repo_name: tobal/plfa

max_issues_repo_name: tobal/plfa

max_forks_repo_name: tobal/plfa


text:
open import HoTT
open import cohomology.FunctionOver

module cohomology.Exactness where

module _ {i j k} {G : Group i} {H : Group j} {K : Group k}
  (φ : G →ᴳ H) (ψ : H →ᴳ K) where

  private
    module G = Group G
    module H = Group H
    module K = Group K
    module φ = GroupHom φ
    module ψ = GroupHom ψ

  {- in image of φ ⇒ in kernel of ψ -}
  is-exact-itok : Type (lmax k (lmax j i))
  is-exact-itok = (h : H.El)
    → Trunc -1 (Σ G.El (λ g → φ.f g == h)) → ψ.f h == K.ident

  {- in kernel of ψ ⇒ in image of φ -}
  is-exact-ktoi : Type (lmax k (lmax j i))
  is-exact-ktoi = (h : H.El)
    → ψ.f h == K.ident → Trunc -1 (Σ G.El (λ g → φ.f g == h))

  record is-exact : Type (lmax k (lmax j i)) where
    field
      itok : is-exact-itok
      ktoi : is-exact-ktoi

  open is-exact public

  {- an equivalent version of is-exact-ktoi  -}
  itok-alt-in : ((g : G.El) → ψ.f (φ.f g) == K.ident) → is-exact-itok
  itok-alt-in r h = Trunc-rec (K.El-level _ _) (λ {(g , p) → ap ψ.f (! p) ∙ r g})

  itok-alt-out : is-exact-itok → ((g : G.El) → ψ.f (φ.f g) == K.ident)
  itok-alt-out s g = s (φ.f g) [ g , idp ]

{- Convenient notation for sequences of homomorphisms -}

infix 15 _⊣|
infixr 10 _⟨_⟩→_

data HomSequence {i} : Group i → Group i → Type (lsucc i) where
  _⊣| : (G : Group i) → HomSequence G G
  _⟨_⟩→_ : (G : Group i) {H K : Group i} (φ : G →ᴳ H)
             → HomSequence H K → HomSequence G K

data Sequence= {i} : {G₁ H₁ G₂ H₂ : Group i}
  (S₁ : HomSequence G₁ H₁) (S₂ : HomSequence G₂ H₂)
  → G₁ == G₂ → H₁ == H₂ → Type (lsucc i) where
  _∥⊣| : ∀ {G₁ G₂} (p : G₁ == G₂) → Sequence= (G₁ ⊣|) (G₂ ⊣|) p p
  _∥⟨_⟩∥_ : ∀ {G₁ G₂} (pG : G₁ == G₂)
    {H₁ K₁ H₂ K₂ : Group i} {φ₁ : G₁ →ᴳ H₁} {φ₂ : G₂ →ᴳ H₂}
    {S₁ : HomSequence H₁ K₁} {S₂ : HomSequence H₂ K₂}
    {pH : H₁ == H₂} {pK : K₁ == K₂}
    (over : φ₁ == φ₂ [ uncurry _→ᴳ_ ↓ pair×= pG pH ])
    → Sequence= S₁ S₂ pH pK
    → Sequence= (G₁ ⟨ φ₁ ⟩→ S₁) (G₂ ⟨ φ₂ ⟩→ S₂) pG pK

infix 15 _↓⊣| _∥⊣|
infixr 10 _↓⟨_⟩↓_ _∥⟨_⟩∥_

data SequenceIso {i j} : {G₁ H₁ : Group i} {G₂ H₂ : Group j}
  (S₁ : HomSequence G₁ H₁) (S₂ : HomSequence G₂ H₂)
  → G₁ ≃ᴳ G₂ → H₁ ≃ᴳ H₂ → Type (lsucc (lmax i j)) where
  _↓⊣| : ∀ {G₁ G₂} (iso : G₁ ≃ᴳ G₂) → SequenceIso (G₁ ⊣|) (G₂ ⊣|) iso iso
  _↓⟨_⟩↓_ : ∀ {G₁ G₂} (isoG : G₁ ≃ᴳ G₂)
    {H₁ K₁ : Group i} {H₂ K₂ : Group j} {φ₁ : G₁ →ᴳ H₁} {φ₂ : G₂ →ᴳ H₂}
    {S₁ : HomSequence H₁ K₁} {S₂ : HomSequence H₂ K₂}
    {isoH : H₁ ≃ᴳ H₂} {isoK : K₁ ≃ᴳ K₂}
    (over : fst isoH ∘ᴳ φ₁ == φ₂ ∘ᴳ fst isoG)
    → SequenceIso S₁ S₂ isoH isoK
    → SequenceIso (G₁ ⟨ φ₁ ⟩→ S₁) (G₂ ⟨ φ₂ ⟩→ S₂) isoG isoK

seq-iso-to-path : ∀ {i} {G₁ H₁ G₂ H₂ : Group i}
  {S₁ : HomSequence G₁ H₁} {S₂ : HomSequence G₂ H₂}
  {isoG : G₁ ≃ᴳ G₂} {isoH : H₁ ≃ᴳ H₂}
  → SequenceIso S₁ S₂ isoG isoH
  → Sequence= S₁ S₂ (group-ua isoG) (group-ua isoH)
seq-iso-to-path (iso ↓⊣|) = group-ua iso ∥⊣|
seq-iso-to-path (iso ↓⟨ over ⟩↓ si') =
  group-ua iso
    ∥⟨ hom-over-isos $ function-over-equivs _ _ $ ap GroupHom.f over ⟩∥
  seq-iso-to-path si'

sequence= : ∀ {i} {G₁ H₁ G₂ H₂ : Group i}
  {S₁ : HomSequence G₁ H₁} {S₂ : HomSequence G₂ H₂}
  (pG : G₁ == G₂) (pH : H₁ == H₂) → Sequence= S₁ S₂ pG pH
  → S₁ == S₂ [ uncurry HomSequence ↓ pair×= pG pH ]
sequence= idp .idp (.idp ∥⊣|) = idp
sequence= {G₁ = G₁} idp idp
  (_∥⟨_⟩∥_ .idp {φ₁ = φ₁} {pH = idp} idp sp') =
    ap (λ S' → G₁ ⟨ φ₁ ⟩→ S') (sequence= idp idp sp')

sequence-iso-ua : ∀ {i} {G₁ H₁ G₂ H₂ : Group i}
  {S₁ : HomSequence G₁ H₁} {S₂ : HomSequence G₂ H₂}
  (isoG : G₁ ≃ᴳ G₂) (isoH : H₁ ≃ᴳ H₂) → SequenceIso S₁ S₂ isoG isoH
  → S₁ == S₂ [ uncurry HomSequence ↓ pair×= (group-ua isoG) (group-ua isoH) ]
sequence-iso-ua isoG isoH si = sequence= _ _ (seq-iso-to-path si)

data is-exact-seq {i} : {G H : Group i} → HomSequence G H → Type (lsucc i) where
  exact-seq-zero : {G : Group i} → is-exact-seq (G ⊣|)
  exact-seq-one : {G H : Group i} {φ : G →ᴳ H} → is-exact-seq (G ⟨ φ ⟩→ H ⊣|)
  exact-seq-two : {G H K J : Group i} {φ : G →ᴳ H} {ψ : H →ᴳ K}
    {diag : HomSequence K J} → is-exact φ ψ
    → is-exact-seq (H ⟨ ψ ⟩→ diag) → is-exact-seq (G ⟨ φ ⟩→ H ⟨ ψ ⟩→ diag)

private
  exact-get-type : ∀ {i} {G H : Group i} → HomSequence G H → ℕ → Type i
  exact-get-type (G ⊣|) _ = Lift Unit
  exact-get-type (G ⟨ φ ⟩→ H ⊣|) _ = Lift Unit
  exact-get-type (G ⟨ φ ⟩→ (H ⟨ ψ ⟩→ s)) O = is-exact φ ψ
  exact-get-type (_ ⟨ _ ⟩→ s) (S n) = exact-get-type s n

exact-get : ∀ {i} {G H : Group i} {diag : HomSequence G H}
  → is-exact-seq diag → (n : ℕ) → exact-get-type diag n
exact-get exact-seq-zero _ = lift unit
exact-get exact-seq-one _ = lift unit
exact-get (exact-seq-two ex s) O = ex
exact-get (exact-seq-two ex s) (S n) = exact-get s n

private
  exact-build-arg-type : ∀ {i} {G H : Group i} → HomSequence G H → List (Type i)
  exact-build-arg-type (G ⊣|) = nil
  exact-build-arg-type (G ⟨ φ ⟩→ H ⊣|) = nil
  exact-build-arg-type (G ⟨ φ ⟩→ H ⟨ ψ ⟩→ s) =
    is-exact φ ψ :: exact-build-arg-type (H ⟨ ψ ⟩→ s)

  exact-build-helper : ∀ {i} {G H : Group i} (seq : HomSequence G H)
    → HList (exact-build-arg-type seq) → is-exact-seq seq
  exact-build-helper (G ⊣|) nil = exact-seq-zero
  exact-build-helper (G ⟨ φ ⟩→ H ⊣|) nil = exact-seq-one
  exact-build-helper (G ⟨ φ ⟩→ H ⟨ ψ ⟩→ s) (ie :: ies) =
    exact-seq-two ie (exact-build-helper (H ⟨ ψ ⟩→ s) ies)

exact-build : ∀ {i} {G H : Group i} (seq : HomSequence G H)
  → hlist-curry-type (exact-build-arg-type seq) (λ _ → is-exact-seq seq)
exact-build seq = hlist-curry (exact-build-helper seq)

private
  hom-seq-snoc : ∀ {i} {G H K : Group i}
    → HomSequence G H → (H →ᴳ K) → HomSequence G K
  hom-seq-snoc (G ⊣|) ψ = G ⟨ ψ ⟩→ _ ⊣|
  hom-seq-snoc (G ⟨ φ ⟩→ s) ψ = G ⟨ φ ⟩→ hom-seq-snoc s ψ

hom-seq-concat : ∀ {i} {G H K : Group i}
  → HomSequence G H → HomSequence H K → HomSequence G K
hom-seq-concat (G ⊣|) s₂ = s₂
hom-seq-concat (G ⟨ φ ⟩→ s₁) s₂ = G ⟨ φ ⟩→ (hom-seq-concat s₁ s₂)

abstract
  exact-concat : ∀ {i} {G H K L : Group i}
    {seq₁ : HomSequence G H} {φ : H →ᴳ K} {seq₂ : HomSequence K L}
    → is-exact-seq (hom-seq-snoc seq₁ φ) → is-exact-seq (H ⟨ φ ⟩→ seq₂)
    → is-exact-seq (hom-seq-concat seq₁ (H ⟨ φ ⟩→ seq₂))
  exact-concat {seq₁ = G ⊣|} exact-seq-one es₂ = es₂
  exact-concat {seq₁ = G ⟨ ψ ⟩→ H ⊣|} (exact-seq-two ex _) es₂ =
    exact-seq-two ex es₂
  exact-concat {seq₁ = G ⟨ ψ ⟩→ H ⟨ χ ⟩→ s} (exact-seq-two ex es₁) es₂ =
    exact-seq-two ex (exact-concat {seq₁ = H ⟨ χ ⟩→ s} es₁ es₂)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


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

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.CommRing

module _ where
  open import Cubical.HITs.Ints.BiInvInt
    renaming (
      _+_ to _+ℤ_;
      -_ to _-ℤ_;
      +-assoc to +ℤ-assoc;
      +-comm to +ℤ-comm
    )

  BiInvIntAsCommRing : CommRing {ℓ-zero}
  BiInvIntAsCommRing =
    makeCommRing
      zero (suc zero) _+ℤ_ _·_ _-ℤ_
      isSetBiInvInt
      +ℤ-assoc +-zero +-invʳ +ℤ-comm
      ·-assoc ·-identityʳ
      (λ x y z → sym (·-distribˡ x y z))
      ·-comm

-- makeCommRing ? ? ? ? ? ? ? ? ? ? ? ? ? ?

module _ where
  open import Cubical.Data.Int

  IntAsCommRing : CommRing {ℓ-zero}
  IntAsCommRing = makeCommRing {R = Int} 0 1 _+_ _·_ -_ isSetInt
    +-assoc +-identityʳ +-inverseʳ +-comm (λ x y z → sym (·-assoc x y z)) ·-identityʳ
    (λ x y z → sym (·-distribˡ x y z)) ·-comm

module _ where
  open import Cubical.HITs.Ints.QuoInt

  QuoIntAsCommRing : CommRing {ℓ-zero}
  QuoIntAsCommRing = makeCommRing {R = ℤ} 0 1 _+_ _·_ -_ isSetℤ
    +-assoc +-identityʳ +-inverseʳ +-comm ·-assoc ·-identityʳ
    (λ x y z → sym (·-distribˡ x y z)) ·-comm

module _ where
  open import Cubical.Data.DiffInt

  DiffIntAsCommRing : CommRing {ℓ-zero}
  DiffIntAsCommRing = makeCommRing {R = ℤ} 0 1 _+_ _·_ -_ isSetℤ
    +-assoc +-identityʳ +-inverseʳ +-comm ·-assoc ·-identityʳ ·-distribˡ ·-comm

open import Cubical.Algebra.Ring using (ringequiv)
open import Cubical.Foundations.Equiv
open import Cubical.Reflection.Base using (_$_) -- TODO: add this to Foundation.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Structure
open import Cubical.HITs.Ints.BiInvInt using (BiInvInt)
open import Cubical.Data.Nat using (suc; zero) renaming (_·_ to _·ⁿ_; _+_ to _+ⁿ_)
open import Cubical.Data.Int as Int using (sucInt; predInt; Int) renaming
  ( _+_ to _+'_
  ; _·_ to _·'_
  ; -_ to -'_
  ; pos to pos'
  ; negsuc to negsuc'
  ; sgn to sgn'
  ; abs to abs'
  ; signed to signed'
  )

module _ where
  open import Cubical.HITs.Ints.BiInvInt renaming
    ( fwd to ⟦_⟧
    ; suc to sucᵇ
    )

  private
    suc-⟦⟧ : ∀ x → sucᵇ ⟦ x ⟧ ≡ ⟦ sucInt x ⟧
    suc-⟦⟧ (pos' n) = refl
    suc-⟦⟧ (negsuc' zero) = suc-pred _
    suc-⟦⟧ (negsuc' (suc n)) = suc-pred _

    pred-⟦⟧ : ∀ x → predl ⟦ x ⟧ ≡ ⟦ predInt x ⟧
    pred-⟦⟧ (pos' zero) = refl
    pred-⟦⟧ (pos' (suc n)) = pred-suc _
    pred-⟦⟧ (negsuc' zero) = refl
    pred-⟦⟧ (negsuc' (suc n)) = refl

    neg-⟦⟧ : ∀ x → - ⟦ x ⟧ ≡ ⟦ -' x ⟧
    neg-⟦⟧ (pos' zero) = refl
    neg-⟦⟧ (pos' (suc n)) = (λ i → predl (neg-⟦⟧ (pos' n) i)) ∙ pred-⟦⟧ (-' pos' n) ∙ cong ⟦_⟧ (Int.predInt-neg (pos' n))
    neg-⟦⟧ (negsuc' zero) = refl
    neg-⟦⟧ (negsuc' (suc n)) = (λ i → sucᵇ (neg-⟦⟧ (negsuc' n) i))

    pres1 : 1 ≡ ⟦ 1 ⟧
    pres1 = refl

    isHom+ : ∀ x y → ⟦ x +' y ⟧ ≡ ⟦ x ⟧ + ⟦ y ⟧
    isHom+ (pos' zero) y i = ⟦ Int.+-comm 0 y i ⟧
    isHom+ (pos' (suc n)) y =
      ⟦ pos' (suc n) +' y ⟧     ≡[ i ]⟨ ⟦ Int.sucInt+ (pos' n) y (~ i) ⟧ ⟩
      ⟦ sucInt (pos' n +' y) ⟧  ≡⟨ sym $ suc-⟦⟧ _ ⟩
      sucᵇ  ⟦ pos' n +' y ⟧     ≡[ i ]⟨ sucᵇ $ isHom+ (pos' n) y i ⟩
      sucᵇ (⟦ pos' n ⟧ + ⟦ y ⟧) ≡⟨ refl ⟩
      sucᵇ  ⟦ pos' n ⟧ + ⟦ y ⟧  ∎
    isHom+ (negsuc' zero) y = pred-suc-inj _ _ (λ i → predl (γ i)) where
      -- γ =   sucᵇ ⟦  negsuc' zero +' y ⟧  ≡⟨ suc-⟦⟧ (negsuc' zero +' y) ⟩
      --     ⟦ sucInt (negsuc' zero +' y)⟧  ≡⟨ cong ⟦_⟧ $ Int.sucInt+ (negsuc' zero) y ∙ Int.+-comm 0 y ⟩
      --                       ⟦       y ⟧  ≡⟨ sym (suc-pred ⟦ y ⟧) ⟩
      --     sucᵇ (pred zero + ⟦       y ⟧) ∎
      γ = suc-⟦⟧ (negsuc' zero +' y) ∙ (λ i → ⟦ (Int.sucInt+ (negsuc' zero) y ∙ Int.+-comm 0 y) i ⟧) ∙ sym (suc-pred ⟦ y ⟧)
    isHom+ (negsuc' (suc n)) y = (λ i → ⟦ Int.predInt+ (negsuc' n) y (~ i) ⟧) ∙ sym (pred-⟦⟧ (negsuc' n +' y))
                               ∙ (λ i → pred $ isHom+ (negsuc' n) y i)

    isHom· : ∀ x y → ⟦ x ·' y ⟧ ≡ ⟦ x ⟧ · ⟦ y ⟧
    isHom· (pos' zero) y i = ⟦ Int.signed-zero (Int.sgn y) i ⟧
    isHom· (pos' (suc n)) y =
      ⟦ pos' (suc n) ·' y ⟧      ≡⟨ cong ⟦_⟧ $ Int.·-pos-suc n y ⟩
      ⟦ y +' pos' n ·' y ⟧       ≡⟨ isHom+ y _ ⟩
      ⟦ y ⟧ + ⟦ pos' n ·' y ⟧    ≡[ i ]⟨ ⟦ y ⟧ + isHom· (pos' n) y i ⟩
      ⟦ y ⟧ + ⟦ pos' n ⟧ · ⟦ y ⟧ ≡⟨ (λ i → ⟦ y ⟧ + ·-comm ⟦ pos' n ⟧ ⟦ y ⟧ i)
                                  ∙ sym (·-suc ⟦ y ⟧ ⟦ pos' n ⟧) ∙ ·-comm ⟦ y ⟧ _ ⟩
      sucᵇ ⟦ pos' n ⟧ · ⟦ y ⟧ ∎
    isHom· (negsuc' zero) y =
      ⟦ -1 ·'  y ⟧ ≡⟨ cong ⟦_⟧ (Int.·-neg1 y) ⟩
      ⟦ -'     y ⟧ ≡⟨ sym (neg-⟦⟧ y) ⟩
        -    ⟦ y ⟧ ≡⟨ sym (·-neg1 ⟦ y ⟧) ⟩
        -1 · ⟦ y ⟧ ∎
    isHom· (negsuc' (suc n)) y =
      ⟦ negsuc' (suc n) ·' y ⟧         ≡⟨ cong ⟦_⟧ $ Int.·-negsuc-suc n y ⟩
      ⟦ -' y   +'  negsuc' n   ·'  y ⟧ ≡⟨ isHom+ (-' y) _ ⟩
      ⟦ -' y ⟧ + ⟦ negsuc' n   ·'  y ⟧ ≡[ i ]⟨ ⟦ -' y ⟧ + isHom· (negsuc' n) y i ⟩
      ⟦ -' y ⟧ + ⟦ negsuc' n ⟧ · ⟦ y ⟧ ≡⟨ cong₂ _+_ (sym (neg-⟦⟧ y)) refl ⟩
      -  ⟦ y ⟧ + ⟦ negsuc' n ⟧ · ⟦ y ⟧ ≡⟨ (λ i → - ⟦ y ⟧ + ·-comm ⟦ negsuc' n ⟧ ⟦ y ⟧ i)
                                        ∙ sym (·-pred ⟦ y ⟧ ⟦ negsuc' n ⟧) ∙ ·-comm ⟦ y ⟧ _ ⟩
      pred ⟦ negsuc' n ⟧ · ⟦ y ⟧       ∎

    ⟦⟧-isEquiv : isEquiv ⟦_⟧
    ⟦⟧-isEquiv = isoToIsEquiv (iso ⟦_⟧ bwd fwd-bwd bwd-fwd)

  Int≃BiInvInt-CommRingEquivΣ : Σ[ e ∈ ⟨ IntAsCommRing ⟩ ≃ ⟨ BiInvIntAsCommRing ⟩ ] CommRingEquiv IntAsCommRing BiInvIntAsCommRing e
  Int≃BiInvInt-CommRingEquivΣ .fst = ⟦_⟧ , ⟦⟧-isEquiv
  Int≃BiInvInt-CommRingEquivΣ .snd = ringequiv pres1 isHom+ isHom·

  Int≡BiInvInt-AsCommRing : IntAsCommRing ≡ BiInvIntAsCommRing
  Int≡BiInvInt-AsCommRing = CommRingPath _ _ .fst Int≃BiInvInt-CommRingEquivΣ

module _ where
  open import Cubical.HITs.Ints.QuoInt as QuoInt renaming
    ( Int→ℤ to ⟦_⟧
    )
  open import Cubical.Data.Bool

  private
    suc-⟦⟧ : ∀ x → sucℤ ⟦ x ⟧ ≡ ⟦ sucInt x ⟧
    suc-⟦⟧ (pos' n) = refl
    suc-⟦⟧ (negsuc' zero) = sym posneg
    suc-⟦⟧ (negsuc' (suc n)) = refl

    pred-⟦⟧ : ∀ x → predℤ ⟦ x ⟧ ≡ ⟦ predInt x ⟧
    pred-⟦⟧ (pos' zero) = refl
    pred-⟦⟧ (pos' (suc n)) = refl
    pred-⟦⟧ (negsuc' n) = refl

    neg-⟦⟧ : ∀ x → - ⟦ x ⟧ ≡ ⟦ -' x ⟧
    neg-⟦⟧ (pos' zero) = sym posneg
    neg-⟦⟧ (pos' (suc n)) = refl
    neg-⟦⟧ (negsuc' n) = refl

    pres1 : 1 ≡ ⟦ 1 ⟧
    pres1 = refl

    isHom+ : ∀ x y → ⟦ x +' y ⟧ ≡ ⟦ x ⟧ + ⟦ y ⟧
    isHom+ (pos' zero) y i = ⟦ Int.+-comm 0 y i ⟧
    isHom+ (pos' (suc n)) y =
      ⟦ pos' (suc n)   +' y  ⟧ ≡[ i ]⟨ ⟦ Int.sucInt+ (pos' n) y (~ i) ⟧ ⟩
      ⟦ sucInt (pos' n +' y) ⟧ ≡⟨ sym $ suc-⟦⟧ _ ⟩
      sucℤ  ⟦ pos' n   +' y  ⟧ ≡[ i ]⟨ sucℤ $ isHom+ (pos' n) y i ⟩
      sucℤ (⟦ pos' n ⟧ + ⟦ y ⟧) ≡⟨ refl ⟩
      sucℤ  ⟦ pos' n ⟧ + ⟦ y ⟧  ∎
    isHom+ (negsuc'  zero  ) y = sucℤ-inj _ _ (suc-⟦⟧ (negsuc' zero +' y)
                               ∙ (cong ⟦_⟧ $ Int.sucInt+ (negsuc' zero) y
                               ∙ Int.+-identityˡ y)
                               ∙ sym (sucPredℤ ⟦ y ⟧))
    isHom+ (negsuc' (suc n)) y = cong ⟦_⟧ (sym (Int.predInt+ (negsuc' n) y))
                               ∙ (sym $ pred-⟦⟧ (negsuc' n +' y))
                               ∙ (λ i → predℤ $ isHom+ (negsuc' n) y i)

    isHom· : ∀ x y → ⟦ x ·' y ⟧ ≡ ⟦ x ⟧ · ⟦ y ⟧
    isHom· (pos' zero) y = (cong ⟦_⟧ $ Int.signed-zero (sgn' y)) ∙ sym (signed-zero (sign ⟦ y ⟧) spos)
    isHom· (pos' (suc n)) y =
      ⟦ pos' (suc n)     ·'  y ⟧ ≡⟨ cong ⟦_⟧ $ Int.·-pos-suc n y ⟩
      ⟦ y   +'  pos' n   ·'  y ⟧ ≡⟨ isHom+ y _ ⟩
      ⟦ y ⟧ + ⟦ pos' n   ·'  y ⟧ ≡[ i ]⟨ ⟦ y ⟧ + isHom· (pos' n) y i ⟩
      ⟦ y ⟧ + ⟦ pos' n ⟧ · ⟦ y ⟧ ≡⟨ sym $ ·-pos-suc n ⟦ y ⟧ ⟩
      sucℤ ⟦ pos' n ⟧ · ⟦ y ⟧ ∎
    isHom· (negsuc' zero) y =
      ⟦ -1 ·'  y ⟧ ≡⟨ cong ⟦_⟧ (Int.·-neg1 y) ⟩
      ⟦ -'     y ⟧ ≡⟨ sym (neg-⟦⟧ y) ⟩
        -    ⟦ y ⟧ ≡⟨ sym (·-neg1 ⟦ y ⟧) ⟩
        -1 · ⟦ y ⟧ ∎
    isHom· (negsuc' (suc n)) y =
      ⟦ negsuc' (suc n) ·' y ⟧         ≡⟨ cong ⟦_⟧ $ Int.·-negsuc-suc n y ⟩
      ⟦ -' y   +'  negsuc' n   ·'  y ⟧ ≡⟨ isHom+ (-' y) _ ⟩
      ⟦ -' y ⟧ + ⟦ negsuc' n   ·'  y ⟧ ≡[ i ]⟨ ⟦ -' y ⟧ + isHom· (negsuc' n) y i ⟩
      ⟦ -' y ⟧ + ⟦ negsuc' n ⟧ · ⟦ y ⟧ ≡⟨ cong₂ _+_ (sym (neg-⟦⟧ y)) refl ⟩
      -  ⟦ y ⟧ + ⟦ negsuc' n ⟧ · ⟦ y ⟧ ≡⟨ sym (·-neg-suc (suc n) ⟦ y ⟧) ⟩
      predℤ ⟦ negsuc' n ⟧ · ⟦ y ⟧      ∎

    ⟦⟧-isEquiv : isEquiv ⟦_⟧
    ⟦⟧-isEquiv = isoToIsEquiv (iso ⟦_⟧ ℤ→Int ℤ→Int→ℤ Int→ℤ→Int)

  Int≃QuoInt-CommRingEquivΣ : Σ[ e ∈ ⟨ IntAsCommRing ⟩ ≃ ⟨ QuoIntAsCommRing ⟩ ] CommRingEquiv IntAsCommRing QuoIntAsCommRing e
  Int≃QuoInt-CommRingEquivΣ .fst = ⟦_⟧ , ⟦⟧-isEquiv
  Int≃QuoInt-CommRingEquivΣ .snd = ringequiv pres1 isHom+ isHom·

  Int≡QuoInt-AsCommRing : IntAsCommRing ≡ QuoIntAsCommRing
  Int≡QuoInt-AsCommRing = CommRingPath _ _ .fst Int≃QuoInt-CommRingEquivΣ

QuoInt≡BiInvInt-AsCommRing : QuoIntAsCommRing ≡ BiInvIntAsCommRing
QuoInt≡BiInvInt-AsCommRing = sym Int≡QuoInt-AsCommRing ∙ Int≡BiInvInt-AsCommRing

open import Cubical.HITs.SetQuotients

module _ where
  open import Cubical.Data.Sigma
  open import Cubical.Data.Bool
  open import Cubical.Data.Nat using (ℕ) renaming (_·_ to _·ⁿ_)
  open import Cubical.HITs.Rationals.QuoQ using (ℚ) renaming (_+_ to _+ʳ_)
  open import Cubical.HITs.Ints.QuoInt using (ℤ; sign; signed; abs) renaming (_+_ to _+ᶻ_)
  open import Cubical.Data.NatPlusOne using (ℕ₊₁; 1+_)

  test1 : ℤ → _
  test1 x = {! x +ᶻ x  !}
  -- Normal form:
  --   x +ᶻ x

  test2 : ℤ × ℕ₊₁  → _
  test2 x = {! [ x ] +ʳ [ x ]  !}
  -- Normal form:
  --   [  signed (sign (fst x) ⊕ false) (abs (fst x) ·ⁿ suc (ℕ₊₁.n (snd x)))
  --   +ᶻ signed (sign (fst x) ⊕ false) (abs (fst x) ·ⁿ suc (ℕ₊₁.n (snd x)))
  --   , (1+ (ℕ₊₁.n (snd x) +ⁿ ℕ₊₁.n (snd x) ·ⁿ suc (ℕ₊₁.n (snd x))))
  --   ]

  test3 : ℚ → ℤ × ℕ₊₁  → _
  test3 x y = {! x +ʳ [ y ]  !}
  -- Normal form:
  --   rec
  --   (λ f g F G i j z →
  --      squash/ (f z) (g z) (λ i₁ → F i₁ z) (λ i₁ → G i₁ z) i j)
  --   (λ a → ...
  --     ...
  --   ... 2000 more lines ...

open import Cubical.Data.DiffInt as DiffInt hiding (_+'_; _·'_)

⟦⟧-isEquiv : isEquiv ⟦_⟧
⟦⟧-isEquiv = isoToIsEquiv (iso ⟦_⟧ bwd fwd-bwd bwd-fwd)

pres1 : 1 ≡ ⟦ 1 ⟧
pres1 = refl

isHom+ : ∀ x y → ⟦ x +' y ⟧ ≡ ⟦ x ⟧ + ⟦ y ⟧
isHom+ (pos' zero) y = {!   !}
isHom+ (pos' (suc n)) y = {!   !} -- ? ∙ λ i → sucℤ (isHom+ (pos' n) y i)
isHom+ (negsuc' zero) y = {! [ 0 , 1 ] + ⟦ y ⟧  !}
isHom+ (negsuc' (suc n)) y = {!   !}

isHom· : ∀ x y → ⟦ x ·' y ⟧ ≡ ⟦ x ⟧ · ⟦ y ⟧
isHom· = {!   !}

Int≃DiffInt-CommRingEquivΣ : Σ[ e ∈ ⟨ IntAsCommRing ⟩ ≃ ⟨ DiffIntAsCommRing ⟩ ] CommRingEquiv IntAsCommRing DiffIntAsCommRing e
Int≃DiffInt-CommRingEquivΣ .fst = ⟦_⟧ , ⟦⟧-isEquiv
Int≃DiffInt-CommRingEquivΣ .snd = ringequiv pres1 isHom+ isHom·

Int≡DiffInt-AsCommRing : IntAsCommRing ≡ DiffIntAsCommRing
Int≡DiffInt-AsCommRing = CommRingPath _ _ .fst Int≃DiffInt-CommRingEquivΣ

DiffInt≡BiInvInt-AsCommRing : DiffIntAsCommRing ≡ BiInvIntAsCommRing
DiffInt≡BiInvInt-AsCommRing = sym Int≡DiffInt-AsCommRing ∙ Int≡BiInvInt-AsCommRing

max_stars_repo_name: mchristianl/cubical

max_issues_repo_name: mchristianl/cubical

max_forks_repo_name: mchristianl/cubical


text:
-- Andreas, 2018-10-18, issue #3289 reported by Ulf
--
-- For postfix projections, we have no hiding info
-- for the eliminated record value.

-- Thus, contrary to the prefix case, it cannot be
-- taken into account (e.g. for projection disambiguation).

open import Agda.Builtin.Nat

record R : Set where
  field
    p : Nat

open R {{...}}

test : R
test .p = 0

-- Error WAS:  Wrong hiding used for projection  R.p

-- Should work now.


text:
-- Test that postponing tactic applications work properly

module _ where

open import Common.Prelude
open import Common.Reflection

data Zero : Set where
  zero : Zero

macro
  fill : Term → Tactic
  fill = give

_asTypeOf_ : {A : Set} → A → A → A
x asTypeOf _ = x

-- Requires postponing the macro evaluation until the 'zero' has been
-- disambiguated.
foo : Nat
foo = let z = zero in
      fill z asTypeOf z


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Surjections
------------------------------------------------------------------------

module Function.Surjection where

open import Level
open import Function.Equality as F
  using (_⟶_) renaming (_∘_ to _⟪∘⟫_)
open import Function.Equivalence using (Equivalence)
open import Function.Injection           hiding (id; _∘_)
open import Function.LeftInverse as Left hiding (id; _∘_)
open import Data.Product
open import Relation.Binary
import Relation.Binary.PropositionalEquality as P

-- Surjective functions.

record Surjective {f₁ f₂ t₁ t₂}
                  {From : Setoid f₁ f₂} {To : Setoid t₁ t₂}
                  (to : From ⟶ To) :
                  Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
  field
    from             : To ⟶ From
    right-inverse-of : from RightInverseOf to

-- The set of all surjections from one setoid to another.

record Surjection {f₁ f₂ t₁ t₂}
                  (From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
                  Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
  field
    to         : From ⟶ To
    surjective : Surjective to

  open Surjective surjective public

  right-inverse : RightInverse From To
  right-inverse = record
    { to              = from
    ; from            = to
    ; left-inverse-of = right-inverse-of
    }

  open LeftInverse right-inverse public
    using () renaming (to-from to from-to)

  injective : Injective from
  injective = LeftInverse.injective right-inverse

  injection : Injection To From
  injection = LeftInverse.injection right-inverse

  equivalence : Equivalence From To
  equivalence = record
    { to   = to
    ; from = from
    }

-- Right inverses can be turned into surjections.

fromRightInverse :
  ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} →
  RightInverse From To → Surjection From To
fromRightInverse r = record
  { to         = from
  ; surjective = record
    { from             = to
    ; right-inverse-of = left-inverse-of
    }
  } where open LeftInverse r

-- The set of all surjections from one set to another.

infix 3 _↠_

_↠_ : ∀ {f t} → Set f → Set t → Set _
From ↠ To = Surjection (P.setoid From) (P.setoid To)

-- Identity and composition.

id : ∀ {s₁ s₂} {S : Setoid s₁ s₂} → Surjection S S
id {S = S} = record
  { to         = F.id
  ; surjective = record
    { from             = LeftInverse.to              id′
    ; right-inverse-of = LeftInverse.left-inverse-of id′
    }
  } where id′ = Left.id {S = S}

infixr 9 _∘_

_∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂}
        {F : Setoid f₁ f₂} {M : Setoid m₁ m₂} {T : Setoid t₁ t₂} →
      Surjection M T → Surjection F M → Surjection F T
f ∘ g = record
  { to         = to f ⟪∘⟫ to g
  ; surjective = record
    { from             = LeftInverse.to              g∘f
    ; right-inverse-of = LeftInverse.left-inverse-of g∘f
    }
  }
  where
  open Surjection
  g∘f = Left._∘_ (right-inverse g) (right-inverse f)


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

open import Agda.Primitive renaming (Set to Set; Prop to Set₁)

test : Set₁
test = Set

max_forks_repo_name: shlevy/agda


text:
{-

Index a structure T a positive structure S: X ↦ S X → T X

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Relational.Function where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.RelationalStructure
open import Cubical.Foundations.Univalence
open import Cubical.Functions.FunExtEquiv
open import Cubical.Data.Sigma
open import Cubical.Relation.Binary.Base
open import Cubical.Relation.ZigZag.Base
open import Cubical.HITs.SetQuotients
open import Cubical.HITs.PropositionalTruncation as Trunc

open import Cubical.Structures.Function

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

FunctionRelStr : {S : Type ℓ → Type ℓ₁} {T : Type ℓ → Type ℓ₂}
  → StrRel S ℓ₁' → StrRel T ℓ₂' → StrRel (FunctionStructure S T) (ℓ-max ℓ₁ (ℓ-max ℓ₁' ℓ₂'))
FunctionRelStr ρ₁ ρ₂ R f g =
  ∀ {x y} → ρ₁ R x y → ρ₂ R (f x) (g y)

open isEquivRel

private
  composeWith[_] : {A : Type ℓ} (R : EquivPropRel A ℓ)
    → compPropRel (R .fst) (quotientPropRel (R .fst .fst)) .fst ≡ graphRel [_]
  composeWith[_] R =
    funExt₂ λ a t →
    hPropExt squash (squash/ _ _)
      (Trunc.rec (squash/ _ _) (λ {(b , r , p) → eq/ a b r ∙ p }))
      (λ p → ∣ a , R .snd .reflexive a , p ∣)

  [_]∙[_]⁻¹ : {A : Type ℓ} (R : EquivPropRel A ℓ)
    → compPropRel (quotientPropRel (R .fst .fst)) (invPropRel (quotientPropRel (R .fst .fst))) .fst
      ≡ R .fst .fst
  [_]∙[_]⁻¹ R =
    funExt₂ λ a b →
    hPropExt squash (R .fst .snd a b)
      (Trunc.rec (R .fst .snd a b)
        (λ {(c , p , q) → effective (R .fst .snd) (R .snd) a b (p ∙ sym q)}))
      (λ r → ∣ _ , eq/ a b r , refl ∣)

functionSuitableRel : {S : Type ℓ → Type ℓ₁} {T : Type ℓ → Type ℓ₂}
  {ρ₁ : StrRel S ℓ₁'} {ρ₂ : StrRel T ℓ₂'}
  (θ₁ : SuitableStrRel S ρ₁)
  → PositiveStrRel θ₁
  → SuitableStrRel T ρ₂
  → SuitableStrRel (FunctionStructure S T) (FunctionRelStr ρ₁ ρ₂)
functionSuitableRel {S = S} {T = T} {ρ₁ = ρ₁} {ρ₂} θ₁ σ₁ θ₂ .quo (X , f) R h =
  final
  where
  ref : (s : S X) → ρ₁ (R .fst .fst) s s
  ref = posRelReflexive σ₁ R

  [f] : S X / ρ₁ (R .fst .fst) → T (X / R .fst .fst)
  [f] [ s ] = θ₂ .quo (X , f s) R (h (ref s)) .fst .fst
  [f] (eq/ s₀ s₁ r i) =
    cong fst
      (θ₂ .quo (X , f s₀) R (h (ref s₀)) .snd
        ( [f] [ s₁ ]
        , subst (λ R' → ρ₂ R' (f s₀) ([f] [ s₁ ]))
          (composeWith[_] R)
          (θ₂ .transitive (R .fst) (quotientPropRel (R .fst .fst))
            (h r)
            (θ₂ .quo (X , f s₁) R (h (ref s₁)) .fst .snd))
        ))
      i
  [f] (squash/ _ _ p q j i) =
    θ₂ .set squash/ _ _ (cong [f] p) (cong [f] q) j i

  relLemma : (s : S X) (t : S X)
    → ρ₁ (graphRel [_]) s (funIsEq (σ₁ .quo R) [ t ])
    → ρ₂ (graphRel [_]) (f s) ([f] [ t ])
  relLemma s t r =
    subst (λ R' → ρ₂ R' (f s) ([f] [ t ]))
      (composeWith[_] R)
      (θ₂ .transitive (R .fst) (quotientPropRel (R .fst .fst))
        (h r')
        (θ₂ .quo (X , f t) R (h (ref t)) .fst .snd))
    where
    r' : ρ₁ (R .fst .fst) s t
    r' =
      subst (λ R' → ρ₁ R' s t) ([_]∙[_]⁻¹ R)
        (θ₁ .transitive
          (quotientPropRel (R .fst .fst))
          (invPropRel (quotientPropRel (R .fst .fst)))
          r
          (θ₁ .symmetric (quotientPropRel (R .fst .fst))
            (subst
              (λ t' → ρ₁ (graphRel [_]) t' (funIsEq (σ₁ .quo R) [ t ]))
              (σ₁ .act .actStrId t)
              (σ₁ .act .actRel eq/ t t (ref t)))))

  quoRelLemma : (s : S X) (t : S X / ρ₁ (R .fst .fst))
    → ρ₁ (graphRel [_]) s (funIsEq (σ₁ .quo R) t)
    → ρ₂ (graphRel [_]) (f s) ([f] t)
  quoRelLemma s =
    elimProp (λ _ → isPropΠ λ _ → θ₂ .prop (λ _ _ → squash/ _ _) _ _)
      (relLemma s)

  final : Σ (Σ _ _) _
  final .fst .fst = [f] ∘ invIsEq (σ₁ .quo R)
  final .fst .snd {s} {t} r =
    quoRelLemma s
      (invIsEq (σ₁ .quo R) t)
      (subst (ρ₁ (graphRel [_]) s) (sym (secIsEq (σ₁ .quo R) t)) r)
  final .snd (f' , c) =
    Σ≡Prop
      (λ _ → isPropImplicitΠ λ s →
        isPropImplicitΠ λ t →
        isPropΠ λ _ → θ₂ .prop (λ _ _ → squash/ _ _) _ _)
      (funExt λ s → contractorLemma (invIsEq (σ₁ .quo R) s) ∙ cong f' (secIsEq (σ₁ .quo R) s))
    where
    contractorLemma : (s : S X / ρ₁ (R .fst .fst))
      → [f] s ≡ f' (funIsEq (σ₁ .quo R) s)
    contractorLemma =
      elimProp
        (λ _ → θ₂ .set squash/ _ _)
        (λ s →
          cong fst
            (θ₂ .quo (X , f s) R (h (ref s)) .snd
              ( f' (funIsEq (σ₁ .quo R) [ s ])
              , c
                (subst
                  (λ s' → ρ₁ (graphRel [_]) s' (funIsEq (σ₁ .quo R) [ s ]))
                  (σ₁ .act .actStrId s)
                  (σ₁ .act .actRel eq/ s s (ref s)))
              )))
functionSuitableRel {ρ₁ = ρ₁} {ρ₂} θ₁ σ θ₂ .symmetric R h r =
  θ₂ .symmetric R (h (θ₁ .symmetric (invPropRel R) r))
functionSuitableRel {ρ₁ = ρ₁} {ρ₂} θ₁ σ θ₂ .transitive R R' h h' rr' =
  Trunc.rec
    (θ₂ .prop (λ _ _ → squash) _ _)
    (λ {(_ , r , r') → θ₂ .transitive R R' (h r) (h' r')})
    (σ .detransitive R R' rr')
functionSuitableRel {ρ₁ = ρ₁} {ρ₂} θ₁ σ θ₂ .set setX =
  isSetΠ λ _ → θ₂ .set setX
functionSuitableRel {ρ₁ = ρ₁} {ρ₂} θ₁ σ θ₂ .prop propR f g =
  isPropImplicitΠ λ _ →
  isPropImplicitΠ λ _ →
  isPropΠ λ _ →
  θ₂ .prop propR _ _

functionRelMatchesEquiv : {S : Type ℓ → Type ℓ₁} {T : Type ℓ → Type ℓ₂}
  (ρ₁ : StrRel S ℓ₁') {ι₁ : StrEquiv S ℓ₁''}
  (ρ₂ : StrRel T ℓ₂') {ι₂ : StrEquiv T ℓ₂''}
  → StrRelMatchesEquiv ρ₁ ι₁
  → StrRelMatchesEquiv ρ₂ ι₂
  → StrRelMatchesEquiv (FunctionRelStr ρ₁ ρ₂) (FunctionEquivStr ι₁ ι₂)
functionRelMatchesEquiv ρ₁ ρ₂ μ₁ μ₂ (X , f) (Y , g) e =
  equivImplicitΠCod (equivImplicitΠCod (equiv→ (μ₁ _ _ e) (μ₂ _ _ e)))

functionRelMatchesEquiv+ : {S : Type ℓ → Type ℓ₁} {T : Type ℓ → Type ℓ₂}
  (ρ₁ : StrRel S ℓ₁') (α₁ : EquivAction S)
  (ρ₂ : StrRel T ℓ₂') (ι₂ : StrEquiv T ℓ₂'')
  → StrRelMatchesEquiv ρ₁ (EquivAction→StrEquiv α₁)
  → StrRelMatchesEquiv ρ₂ ι₂
  → StrRelMatchesEquiv (FunctionRelStr ρ₁ ρ₂) (FunctionEquivStr+ α₁ ι₂)
functionRelMatchesEquiv+ ρ₁ α₁ ρ₂ ι₂ μ₁ μ₂ (X , f) (Y , g) e =
  compEquiv
    (functionRelMatchesEquiv ρ₁ ρ₂ μ₁ μ₂ (X , f) (Y , g) e)
    (isoToEquiv isom)
  where
  open Iso
  isom : Iso
    (FunctionEquivStr (EquivAction→StrEquiv α₁) ι₂ (X , f) (Y , g) e)
    (FunctionEquivStr+ α₁ ι₂ (X , f) (Y , g) e)
  isom .fun h s = h refl
  isom .inv k {x} = J (λ y _ → ι₂ (X , f x) (Y , g y) e) (k x)
  isom .rightInv k i x = JRefl (λ y _ → ι₂ (X , f x) (Y , g y) e) (k x) i
  isom .leftInv h =
    implicitFunExt λ {x} →
    implicitFunExt λ {y} →
    funExt λ p →
    J (λ y p → isom .inv (isom .fun h) p ≡ h p)
      (funExt⁻ (isom .rightInv (isom .fun h)) x)
      p

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


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

open import lib.Basics
open import lib.cubical.Square
open import lib.types.Group
open import lib.types.EilenbergMacLane1.Core
open import lib.types.EilenbergMacLane1.DoubleElim

module lib.types.EilenbergMacLane1.DoublePathElim where

private

  emloop-emloop-eq-helper : ∀ {i j k} {A : Type i} {B : Type j} {C : Type k}
    (f g : A → B → C)
    {a₀ a₁ : A} (p : a₀ == a₁)
    {b₀ b₁ : B} (q : b₀ == b₁)
    {u₀₀ : f a₀ b₀ == g a₀ b₀}
    {u₀₁ : f a₀ b₁ == g a₀ b₁}
    {u₁₀ : f a₁ b₀ == g a₁ b₀}
    {u₁₁ : f a₁ b₁ == g a₁ b₁}
    (sq₀₋ : Square u₀₀ (ap (f a₀) q) (ap (g a₀) q) u₀₁)
    (sq₁₋ : Square u₁₀ (ap (f a₁) q) (ap (g a₁) q) u₁₁)
    (sq₋₀ : Square u₀₀ (ap (λ a → f a b₀) p) (ap (λ a → g a b₀) p) u₁₀)
    (sq₋₁ : Square u₀₁ (ap (λ a → f a b₁) p) (ap (λ a → g a b₁) p) u₁₁)
    → ap-comm f p q ∙v⊡ (sq₀₋ ⊡h sq₋₁)
      ==
      (sq₋₀ ⊡h sq₁₋) ⊡v∙ ap-comm g p q
    → ↓-ap-in (λ Z → Z) (λ a → f a b₀ == g a b₀) (↓-='-from-square sq₋₀) ∙'ᵈ
      ↓-ap-in (λ Z → Z) (λ b → f a₁ b == g a₁ b) (↓-='-from-square sq₁₋)
      ==
      ↓-ap-in (λ Z → Z) (λ b → f a₀ b == g a₀ b) (↓-='-from-square sq₀₋) ∙ᵈ
      ↓-ap-in (λ Z → Z) (λ a → f a b₁ == g a b₁) (↓-='-from-square sq₋₁)
        [ (λ p → u₀₀ == u₁₁ [ (λ Z → Z) ↓ p ]) ↓
          ap-comm' (λ a b → f a b == g a b) p q ]
  emloop-emloop-eq-helper f g idp idp sq₀₋ sq₁₋ sq₋₀ sq₋₁ r =
    horiz-degen-path sq₋₀ ∙' horiz-degen-path sq₁₋
      =⟨ ∙'=∙ (horiz-degen-path sq₋₀) (horiz-degen-path sq₁₋) ⟩
    horiz-degen-path sq₋₀ ∙ horiz-degen-path sq₁₋
      =⟨ ! (horiz-degen-path-⊡h sq₋₀ sq₁₋) ⟩
    horiz-degen-path (sq₋₀ ⊡h sq₁₋)
      =⟨ ap horiz-degen-path (! r) ⟩
    horiz-degen-path (sq₀₋ ⊡h sq₋₁)
      =⟨ horiz-degen-path-⊡h sq₀₋ sq₋₁ ⟩
    horiz-degen-path sq₀₋ ∙ horiz-degen-path sq₋₁ =∎

module _ {i j} (G : Group i) (H : Group j) where

  private
    module G = Group G
    module H = Group H

  module EM₁Level₂DoublePathElim {k} {C : Type k}
    {{C-level : has-level 2 C}}
    (f₁ f₂ : EM₁ G → EM₁ H → C)
    (embase-embase* : f₁ embase embase == f₂ embase embase)
    (embase-emloop* : ∀ h →
      Square embase-embase* (ap (f₁ embase) (emloop h))
             (ap (f₂ embase) (emloop h)) embase-embase*)
    (emloop-embase* : ∀ g →
      Square embase-embase* (ap (λ x → f₁ x embase) (emloop g))
             (ap (λ x → f₂ x embase) (emloop g)) embase-embase*)
    (embase-emloop-comp* : ∀ h₁ h₂ →
      embase-emloop* (H.comp h₁ h₂) ⊡v∙
      ap (ap (f₂ embase)) (emloop-comp' H h₁ h₂)
      ==
      ap (ap (f₁ embase)) (emloop-comp' H h₁ h₂) ∙v⊡
      ↓-='-square-comp (embase-emloop* h₁) (embase-emloop* h₂))
    (emloop-comp-embase* : ∀ g₁ g₂ →
      emloop-embase* (G.comp g₁ g₂) ⊡v∙
      ap (ap (λ x → f₂ x embase)) (emloop-comp' G g₁ g₂)
      ==
      ap (ap (λ x → f₁ x embase)) (emloop-comp' G g₁ g₂) ∙v⊡
      ↓-='-square-comp (emloop-embase* g₁) (emloop-embase* g₂))
    (emloop-emloop* : ∀ g h →
      ap-comm f₁ (emloop g) (emloop h) ∙v⊡
      (embase-emloop* h ⊡h emloop-embase* g)
      ==
      (emloop-embase* g ⊡h embase-emloop* h) ⊡v∙
      ap-comm f₂ (emloop g) (emloop h))
    where

    private
      module M =
        EM₁Level₁DoubleElim G H
          {P = λ x y → f₁ x y == f₂ x y}
          {{λ x y → has-level-apply C-level _ _}}
          embase-embase*
          (λ h → ↓-='-from-square (embase-emloop* h))
          (λ g → ↓-='-from-square (emloop-embase* g))
          (λ h₁ h₂ →
            ↓-='-from-square-comp-path (emloop-comp h₁ h₂)
                                       (embase-emloop* h₁)
                                       (embase-emloop* h₂)
                                       (embase-emloop* (H.comp h₁ h₂))
                                       (embase-emloop-comp* h₁ h₂))
          (λ g₁ g₂ →
            ↓-='-from-square-comp-path (emloop-comp g₁ g₂)
                                       (emloop-embase* g₁)
                                       (emloop-embase* g₂)
                                       (emloop-embase* (G.comp g₁ g₂))
                                       (emloop-comp-embase* g₁ g₂))
          (λ g h →
            emloop-emloop-eq-helper f₁ f₂
                                    (emloop g) (emloop h)
                                    (embase-emloop* h)
                                    (embase-emloop* h)
                                    (emloop-embase* g)
                                    (emloop-embase* g)
                                    (emloop-emloop* g h) )

    open M public

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


text:
module Progress where

open import Data.Bool
open import Data.Empty
open import Data.Maybe hiding (Any ; All)
open import Data.Nat
open import Data.List
open import Data.List.All
open import Data.List.Any
open import Data.Product
open import Data.Unit

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

open import Typing
open import Syntax
open import Global
open import Channel
open import Values
open import Session
open import Schedule

open import ProcessSyntax
open import ProcessRun

-- resources appear in pairs
data Paired : SEntry → Set where
  aon-nothing : Paired nothing
  aon-all : ∀ {s} → Paired (just (s , POSNEG))

-- need lemmas for matchXAndGo ...
-- matchXandGo-preserves-paired

matchWaitAndGo-preserves-paired :
  ∀ {G G₁ G₂  G₁₁ G₁₂ φ G₂₁ G₂₂ Gnext tpnext}
    {ss : SSplit G G₁ G₂}
    {ss-cl : SSplit G₁ G₁₁ G₁₂}
    {v : Val G₁₁ (TChan send!)}
    {cl-κ : Cont G₁₂ φ TUnit}
    {ss-GG' : SSplit G₂ G₂₁ G₂₂}
  → All Paired G
  → (tp' : ThreadPool G₂₁)
  → (tp'' : ThreadPool G₂₂)
  → matchWaitAndGo ss (ss-cl , v , cl-κ) ss-GG' tp' tp'' ≡ just (Gnext , tpnext)
  → All Paired Gnext
matchWaitAndGo-preserves-paired all-paired (tnil ina) tp'' ()
matchWaitAndGo-preserves-paired {ss-GG' =  ss-GG'} all-paired (tcons ss cmd@(Fork ss₁ κ₁ κ₂) tp') tp'' match-≡
  with ssplit-compose5 ss-GG' ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo-preserves-paired all-paired tp' (tcons ss' cmd tp'') match-≡
matchWaitAndGo-preserves-paired {ss-GG' =  ss-GG'} all-paired (tcons ss cmd@(Ready ss₁ v κ) tp') tp'' match-≡  with ssplit-compose5 ss-GG' ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo-preserves-paired all-paired tp' (tcons ss' cmd tp'') match-≡
matchWaitAndGo-preserves-paired {ss-GG' =  ss-GG'} all-paired (tcons ss cmd@(Halt x x₁ x₂) tp') tp'' match-≡  with ssplit-compose5 ss-GG' ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo-preserves-paired all-paired tp' (tcons ss' cmd tp'') match-≡
matchWaitAndGo-preserves-paired {ss-GG' =  ss-GG'} all-paired (tcons ss cmd@(New s κ) tp') tp'' match-≡  with ssplit-compose5 ss-GG' ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo-preserves-paired all-paired tp' (tcons ss' cmd tp'') match-≡
matchWaitAndGo-preserves-paired {ss-GG' =  ss-GG'} all-paired (tcons ss cmd@(Close ss₁ v κ) tp') tp'' match-≡ with ssplit-compose5 ss-GG' ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo-preserves-paired all-paired tp' (tcons ss' cmd tp'') match-≡
matchWaitAndGo-preserves-paired {ss-GG' =  ss-GG'} all-paired (tcons ss cmd@(Send ss₁ ss-args vch v κ) tp') tp'' match-≡  with ssplit-compose5 ss-GG' ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo-preserves-paired all-paired tp' (tcons ss' cmd tp'') match-≡
matchWaitAndGo-preserves-paired {ss-GG' =  ss-GG'} all-paired (tcons ss cmd@(Recv ss₁ vch κ) tp') tp'' match-≡  with ssplit-compose5 ss-GG' ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo-preserves-paired all-paired tp' (tcons ss' cmd tp'') match-≡
matchWaitAndGo-preserves-paired {ss-GG' =  ss-GG'} all-paired (tcons ss cmd@(Select ss₁ lab vch κ) tp') tp'' match-≡  with ssplit-compose5 ss-GG' ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo-preserves-paired all-paired tp' (tcons ss' cmd tp'') match-≡
matchWaitAndGo-preserves-paired {ss-GG' =  ss-GG'} all-paired (tcons ss cmd@(Branch ss₁ vch dcont) tp') tp'' match-≡  with ssplit-compose5 ss-GG' ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo-preserves-paired all-paired tp' (tcons ss' cmd tp'') match-≡
matchWaitAndGo-preserves-paired {ss-GG' =  ss-GG'} all-paired (tcons ss cmd@(NSelect ss₁ lab vch κ) tp') tp'' match-≡  with ssplit-compose5 ss-GG' ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo-preserves-paired all-paired tp' (tcons ss' cmd tp'') match-≡
matchWaitAndGo-preserves-paired {ss-GG' =  ss-GG'} all-paired (tcons ss cmd@(NBranch ss₁ vch dcont) tp') tp'' match-≡  with ssplit-compose5 ss-GG' ss
... | Gi , ss-tp' , ss' =
  matchWaitAndGo-preserves-paired all-paired tp' (tcons ss' cmd tp'') match-≡
matchWaitAndGo-preserves-paired {ss = ss-top} {ss-cl = ss-cl} {v = VChan cl-b cl-vcr} {ss-GG' =  ss-tp}
  all-paired (tcons ss cmd@(Wait ss₁ (VChan w-b w-vcr) κ) tp-wl) tp-acc match-≡
  with ssplit-compose6 ss ss₁
... | Gi , ss-g3gi , ss-g4g2
  with ssplit-compose6 ss-tp ss-g3gi
... | Gi' , ss-g3gi' , ss-gtpacc
  with ssplit-join ss-top ss-cl ss-g3gi'
... | Gchannels , Gother , ss-top' , ss-channels , ss-others
   with vcr-match ss-channels cl-vcr w-vcr
matchWaitAndGo-preserves-paired {ss = ss-top} {ss-cl} {VChan cl-b cl-vcr} {ss-GG' = ss-tp} all-paired (tcons ss cmd@(Wait ss₁ (VChan w-b w-vcr) κ) tp-wl) tp-acc match-≡ | Gi , ss-g3gi , ss-g4g2 | Gi' , ss-g3gi' , ss-gtpacc | Gchannels , Gother , ss-top' , ss-channels , ss-others | nothing with ssplit-compose5 ss-tp ss
... | _ , ss-tp' , ss' =
  matchWaitAndGo-preserves-paired all-paired tp-wl (tcons ss' cmd tp-acc) match-≡
matchWaitAndGo-preserves-paired {ss = ss-top} {ss-cl} {VChan cl-b cl-vcr} {ss-GG' = ss-tp} all-paired (tcons ss cmd@(Wait ss₁ (VChan w-b w-vcr) κ) tp-wl) tp-acc refl | Gi , ss-g3gi , ss-g4g2 | Gi' , ss-g3gi' , ss-gtpacc | Gchannels , Gother , ss-top' , ss-channels , ss-others | just x = {!!}
-- remains to prove All Paired Gother

step-preserves-paired : ∀ {G G' ev tp'} → All Paired G → (tp : ThreadPool G) → Original.step tp ≡ (_,_ {G'} ev tp') → All Paired G'
step-preserves-paired all-paired tp step-≡ with tp
step-preserves-paired all-paired tp refl | tnil ina = all-paired
step-preserves-paired all-paired tp refl | tcons ss (Fork ss₁ κ₁ κ₂) tp' = all-paired
step-preserves-paired all-paired tp refl | tcons ss (Ready ss₁ v κ) tp' = all-paired
step-preserves-paired all-paired tp step-≡ | tcons ss (Halt x x₁ x₂) tp' with inactive-left-ssplit ss x
step-preserves-paired all-paired tp refl | tcons ss (Halt x x₁ x₂) tp' | refl = all-paired
step-preserves-paired all-paired tp refl | tcons ss (New s κ) tp' = aon-all ∷ all-paired
step-preserves-paired all-paired tp step-≡ | tcons{G₁}{G₂} ss (Close ss-vκ v κ) tp'
  with ssplit-refl-left-inactive G₂
... | G' , ina-G' , ss-GG'
  with matchWaitAndGo ss (ss-vκ , v , κ) ss-GG' tp' (tnil ina-G')
step-preserves-paired all-paired tp refl | tcons {G₁} {G₂} ss (Close ss-vκ v κ) tp' | G' , ina-G' , ss-GG' | just (Gnext , tpnext) = matchWaitAndGo-preserves-paired {ss = ss}{ss-cl = ss-vκ}{v = v}{cl-κ = κ}{ss-GG'} all-paired tp' (tnil ina-G') p
  where
    p : matchWaitAndGo ss (ss-vκ , v , κ) ss-GG' tp' (tnil ina-G') ≡ just (Gnext , tpnext)
    p = sym {!refl!}
step-preserves-paired all-paired tp refl | tcons {G₁} {G₂} ss (Close ss-vκ v κ) tp' | G' , ina-G' , ss-GG' | nothing = all-paired
step-preserves-paired all-paired tp refl | tcons ss (Wait ss₁ v κ) tp' = all-paired
step-preserves-paired all-paired tp refl | tcons ss (Send ss₁ ss-args vch v κ) tp' = all-paired
step-preserves-paired all-paired tp step-≡ | tcons{G₁}{G₂} ss (Recv ss-vκ vch κ) tp' with ssplit-refl-left-inactive G₂
... | G' , ina-G' , ss-GG' with matchSendAndGo ss (ss-vκ , vch , κ) ss-GG' tp' (tnil ina-G')
... | just (G-next , tp-next) = {!!}
step-preserves-paired all-paired tp refl | tcons {G₁} {G₂} ss (Recv ss-vκ vch κ) tp' | G' , ina-G' , ss-GG' | nothing = all-paired
step-preserves-paired all-paired tp step-≡ | tcons{G₁}{G₂} ss (Select ss-vκ lab vch κ) tp' with ssplit-refl-left-inactive G₂
... | G' , ina-G' , ss-GG' with matchBranchAndGo ss (ss-vκ , lab , vch , κ) ss-GG' tp' (tnil ina-G')
... | just (G-next , tp-next) = {!!}
step-preserves-paired all-paired tp refl | tcons {G₁} {G₂} ss (Select ss-vκ lab vch κ) tp' | G' , ina-G' , ss-GG' | nothing = all-paired
step-preserves-paired all-paired tp refl | tcons ss (Branch ss₁ vch dcont) tp' = all-paired
step-preserves-paired all-paired tp step-≡ | tcons{G₁}{G₂} ss (NSelect ss-vκ lab vch κ) tp' with ssplit-refl-left-inactive G₂
... | G' , ina-G' , ss-GG' with matchNBranchAndGo ss (ss-vκ , lab , vch , κ) ss-GG' tp' (tnil ina-G')
... | just (G-next , tp-next) = {!!}
step-preserves-paired all-paired tp refl | tcons {G₁} {G₂} ss (NSelect ss-vκ lab vch κ) tp' | G' , ina-G' , ss-GG' | nothing = all-paired
step-preserves-paired all-paired tp refl | tcons ss (NBranch ss₁ vch dcont) tp' = all-paired

-- check if the first thread can make a step
topCanStep : ∀ {G} → ThreadPool G → Set
topCanStep (tnil ina) = ⊥
topCanStep (tcons ss (Fork ss₁ κ₁ κ₂) tp) = ⊤
topCanStep (tcons ss (Ready ss₁ v κ) tp) = ⊤
topCanStep (tcons ss (Halt x x₁ x₂) tp) = ⊤
topCanStep (tcons ss (New s κ) tp) = ⊤
topCanStep (tcons{G₁}{G₂} ss (Close ss-vκ v κ) tp) with ssplit-refl-left-inactive G₂
... |  G' , ina-G' , ss-GG' = Is-just (matchWaitAndGo ss (ss-vκ , v , κ) ss-GG' tp (tnil ina-G'))
topCanStep (tcons ss (Wait ss₁ v κ) tp) = ⊥
topCanStep (tcons ss (Send ss₁ ss-args vch v κ) tp) = ⊥
topCanStep (tcons{G₁}{G₂} ss (Recv ss-vκ vch κ) tp) with ssplit-refl-left-inactive G₂
... | G' , ina-G' , ss-GG' = Is-just (matchSendAndGo ss (ss-vκ , vch , κ) ss-GG' tp (tnil ina-G'))
topCanStep (tcons{G₁}{G₂} ss (Select ss-vκ lab vch κ) tp) with ssplit-refl-left-inactive G₂
... | G' , ina-G' , ss-GG' = Is-just (matchBranchAndGo ss (ss-vκ , lab , vch , κ) ss-GG' tp (tnil ina-G'))
topCanStep (tcons ss (Branch ss₁ vch dcont) tp) = ⊥
topCanStep (tcons{G₁}{G₂} ss (NSelect ss-vκ lab vch κ) tp) with ssplit-refl-left-inactive G₂
... | G' , ina-G' , ss-GG' = Is-just (matchNBranchAndGo ss (ss-vκ , lab , vch , κ) ss-GG' tp (tnil ina-G'))
topCanStep (tcons ss (NBranch ss₁ vch dcont) tp) = ⊥

tpLength : ∀ {G} → ThreadPool G → ℕ
tpLength (tnil ina) = 0
tpLength (tcons ss cmd tp) = suc (tpLength tp)

allRotations : ∀ {G} → ThreadPool G → List (ThreadPool G)
allRotations tp = nRotations (tpLength tp) tp
  where
    rotate : ∀ {G} → ThreadPool G → ThreadPool G
    rotate (tnil ina) = tnil ina
    rotate (tcons ss cmd tp) = tsnoc ss tp cmd
    nRotations : ∀ {G} ℕ → ThreadPool G → List (ThreadPool G)
    nRotations zero tp = []
    nRotations (suc n) tp = tp ∷ nRotations n (rotate tp)

-- the thread pool can step if any command in the pool can make a step
canStep : ∀ {G} → ThreadPool G → Set
canStep tp = Any topCanStep (allRotations tp)

deadlocked : ∀ {G} → ThreadPool G → Set
deadlocked (tnil ina) = ⊥
deadlocked tp@(tcons _ _ _) = ¬ canStep tp

-- progress