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

open import HoTT
open import groups.Exactness
open import cohomology.Theory

{- Finite additivity is provable (and in a stronger form) without using
 - the additivity axiom. We have

         Cⁿ(X ∨ Y) == Cⁿ(X) × Cⁿ(Y)

 - and over this path
 -   ∙ Cⁿ(winl) corresponds to fst : Cⁿ(X) × Cⁿ(Y) → Cⁿ(X),
 -   ∙ Cⁿ(winr) corresponds to snd : Cⁿ(X) × Cⁿ(Y) → Cⁿ(Y),
 -   ∙ Cⁿ(Wedge-rec winl* winr* wglue*) : Cⁿ(Z) → Cⁿ(X ∨ Y)
       corresponds to Cⁿ(winl*) × Cⁿ(winr*).
 -   ∙ Cⁿ(f) : Cⁿ(X ∨ Y) → Cⁿ(Z)
       corresponds to Cⁿ(projl ∘ f) + Cⁿ(projr ∘ f) : Cⁿ(X) × Cⁿ(Y) → Cⁿ(Z)
 -}

module cohomology.Wedge {i} (CT : CohomologyTheory i) (n : ℤ) where

open CohomologyTheory CT

module _ (X Y : Ptd i) where

  open import homotopy.WedgeCofiber X Y

  open import cohomology.PtdMapSequence CT

  private
    abstract
      βl : ∀ x → CEl-fmap n ⊙winl (CEl-fmap n (⊙projl {X = X} {Y}) x) == x
      βl = CEl-fmap-inverse n ⊙winl ⊙projl λ _ → idp

      βr : ∀ y → CEl-fmap n ⊙winr (CEl-fmap n (⊙projr {X = X} {Y}) y) == y
      βr = CEl-fmap-inverse n ⊙winr ⊙projr λ _ → idp

      C-projr-C-winl-is-exact : is-exact (C-fmap n (⊙projr {X = X} {Y})) (C-fmap n ⊙winl)
      C-projr-C-winl-is-exact = equiv-preserves'-exact
        (C-comm-square n cfcod-winl-projr-comm-sqr)
        (C-comm-square n $ comm-sqr λ _ → idp)
        (snd (C-emap n CofWinl.⊙eq))
        (C-isemap n (⊙idf _) (idf-is-equiv _))
        (C-isemap n (⊙idf _) (idf-is-equiv _))
        (C-exact n ⊙winl)

      C-projl-C-winr-is-exact : is-exact (C-fmap n (⊙projl {X = X} {Y})) (C-fmap n ⊙winr)
      C-projl-C-winr-is-exact = equiv-preserves'-exact
        (C-comm-square n cfcod-winr-projl-comm-sqr)
        (C-comm-square n $ comm-sqr λ _ → idp)
        (snd (C-emap n CofWinr.⊙eq))
        (C-isemap n (⊙idf _) (idf-is-equiv _))
        (C-isemap n (⊙idf _) (idf-is-equiv _))
        (C-exact n ⊙winr)

  import groups.ProductRepr
    (C-fmap n (⊙projl {X = X} {Y})) (C-fmap n ⊙projr)
    (C-fmap n ⊙winl) (C-fmap n ⊙winr) βl βr
    C-projl-C-winr-is-exact
    C-projr-C-winl-is-exact as PR

  C-Wedge : C n (X ⊙∨ Y) ≃ᴳ C n X ×ᴳ C n Y
  C-Wedge = PR.iso

  {-
       projl
      *-----*
   id |     | C-W
      *-----*
        inl
  -}
  C-projl-inl-comm-sqr : CommSquareᴳ
    (C-fmap n ⊙projl) ×ᴳ-inl
    (idhom _) (–>ᴳ C-Wedge)
  C-projl-inl-comm-sqr = PR.i₁-inl-comm-sqr

  {-
       projr
      *-----*
   id |     | C-W
      *-----*
        inr
  -}
  C-projr-inr-comm-sqr : CommSquareᴳ
    (C-fmap n ⊙projr) ×ᴳ-inr
    (idhom _) (–>ᴳ C-Wedge)
  C-projr-inr-comm-sqr = PR.i₂-inr-comm-sqr

  abstract
    C-Wedge-rec-comm-sqr : ∀ {Z : Ptd i} (winl* : X ⊙→ Z) (winr* : Y ⊙→ Z)
      → CommSquareᴳ
          (C-fmap n (⊙Wedge-rec winl* winr*))
          (×ᴳ-fanout (C-fmap n winl*) (C-fmap n winr*))
          (idhom _) (–>ᴳ C-Wedge)
    C-Wedge-rec-comm-sqr winl* winr* = comm-sqrᴳ λ z → pair×=
      ( ∘-CEl-fmap n ⊙winl (⊙Wedge-rec winl* winr*) z
      ∙ CEl-fmap-base-indep n (λ _ → idp) z)
      ( ∘-CEl-fmap n ⊙winr (⊙Wedge-rec winl* winr*) z
      ∙ CEl-fmap-base-indep n (λ _ → idp) z)

    C-Wedge-rec-comm-sqr' : ∀ {Z : Ptd i} (winl* : X ⊙→ Z) (winr* : Y ⊙→ Z)
      → CommSquareᴳ
          (×ᴳ-fanout (C-fmap n winl*) (C-fmap n winr*))
          (C-fmap n (⊙Wedge-rec winl* winr*))
          (idhom _) (<–ᴳ C-Wedge)
    C-Wedge-rec-comm-sqr' winl* winr* = comm-sqrᴳ λ z →
      ! (ap (GroupIso.g C-Wedge) (C-Wedge-rec-comm-sqr winl* winr* □$ᴳ z))
      ∙ GroupIso.g-f C-Wedge (CEl-fmap n (⊙Wedge-rec winl* winr*) z)

    C-Wedge-out-η-comm-sqr : {Z : Ptd i} (φ : C n (⊙Wedge X Y) →ᴳ C n Z)
      → CommSquareᴳ φ
          (×ᴳ-fanin (C-is-abelian n _) (φ ∘ᴳ C-fmap n ⊙projl)
                                       (φ ∘ᴳ C-fmap n ⊙projr))
          (–>ᴳ C-Wedge) (idhom _)
    C-Wedge-out-η-comm-sqr φ = comm-sqrᴳ λ x∨y →
        ap (GroupHom.f φ) (! (GroupIso.g-f C-Wedge x∨y))
      ∙ ! (×ᴳ-fanin-pre∘ (C-is-abelian n _) (C-is-abelian n _)
             φ (C-fmap n ⊙projl) (C-fmap n ⊙projr) _)

    C-Wedge-out-η-comm-sqr' : {Z : Ptd i} (φ : C n (⊙Wedge X Y) →ᴳ C n Z)
      → CommSquareᴳ
          (×ᴳ-fanin (C-is-abelian n _) (φ ∘ᴳ C-fmap n ⊙projl)
                                       (φ ∘ᴳ C-fmap n ⊙projr))
          φ (<–ᴳ C-Wedge) (idhom _)
    C-Wedge-out-η-comm-sqr' {Z} φ = comm-sqrᴳ λ z →
      ×ᴳ-fanin-pre∘ (C-is-abelian n _) (C-is-abelian n _)
        φ (C-fmap n ⊙projl) (C-fmap n ⊙projr) _

    C-Wedge-in-comm-sqr : {Z : Ptd i} (f : Z ⊙→ ⊙Wedge X Y)
      → CommSquareᴳ (C-fmap n f)
          (×ᴳ-fanin (C-is-abelian n _) (C-fmap n (⊙projl ⊙∘ f))
                                       (C-fmap n (⊙projr ⊙∘ f)))
          (–>ᴳ C-Wedge) (idhom _)
    C-Wedge-in-comm-sqr f = comm-sqrᴳ λ x∨y →
        (C-Wedge-out-η-comm-sqr (C-fmap n f) □$ᴳ x∨y)
      ∙ ap2 (Group.comp (C n _))
          (∘-C-fmap n f ⊙projl _)
          (∘-C-fmap n f ⊙projr _)

    C-Wedge-in-comm-sqr' : {Z : Ptd i} (f : Z ⊙→ ⊙Wedge X Y)
      → CommSquareᴳ
          (×ᴳ-fanin (C-is-abelian n _) (C-fmap n (⊙projl ⊙∘ f))
                                       (C-fmap n (⊙projr ⊙∘ f)))
          (C-fmap n f) (<–ᴳ C-Wedge) (idhom _)
    C-Wedge-in-comm-sqr' f = comm-sqrᴳ λ z →
        ap2 (Group.comp (C n _))
          (C-fmap-∘ n ⊙projl f _)
          (C-fmap-∘ n ⊙projr f _)
      ∙ (C-Wedge-out-η-comm-sqr' (C-fmap n f) □$ᴳ z)

module _ (X : Ptd i) where

  abstract
    C-fold-comm-sqr : CommSquareᴳ
      (C-fmap n ⊙fold) ×ᴳ-diag
      (idhom (C n X)) (–>ᴳ (C-Wedge X X))
    C-fold-comm-sqr = comm-sqrᴳ λ x →
      GroupIso.f (C-Wedge X X) (CEl-fmap n ⊙fold x)
        =⟨ C-Wedge-rec-comm-sqr X X (⊙idf X) (⊙idf X) □$ᴳ x ⟩
      (CEl-fmap n (⊙idf X) x , CEl-fmap n (⊙idf X) x)
        =⟨ pair×= (CEl-fmap-idf n x) (CEl-fmap-idf n x) ⟩
      (x , x)
        =∎

    C-fold-comm-sqr' : CommSquareᴳ
      ×ᴳ-diag (C-fmap n ⊙fold)
      (idhom (C n X)) (<–ᴳ (C-Wedge X X))
    C-fold-comm-sqr' = comm-sqrᴳ λ x →
      ! (ap (GroupIso.g (C-Wedge X X)) (C-fold-comm-sqr □$ᴳ x))
      ∙ GroupIso.g-f (C-Wedge X X) (CEl-fmap n ⊙fold x)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.DirectSum.DirectSumFun.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Nat renaming (_+_ to _+n_ ; _·_ to _·n_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma

open import Cubical.HITs.PropositionalTruncation as PT

open import Cubical.Algebra.AbGroup

private variable
  ℓ : Level

open AbGroupStr

-----------------------------------------------------------------------------
-- Definition

AlmostNullProof : (G : ℕ → Type ℓ) → (Gstr : (n : ℕ) → AbGroupStr (G n))
                  → (f : (n : ℕ) → G n) → (k : ℕ) → Type ℓ
AlmostNullProof G Gstr f k = (n : ℕ) → k < n → f n ≡ 0g (Gstr n)

AlmostNull : (G : ℕ → Type ℓ) → (Gstr : (n : ℕ) → AbGroupStr (G n))
             → (f : (n : ℕ) → G n) → Type ℓ
AlmostNull G Gstr f = Σ[ k ∈ ℕ ] AlmostNullProof G Gstr f k

AlmostNullP : (G : ℕ → Type ℓ) → (Gstr : (n : ℕ) → AbGroupStr (G n))
             → (f : (n : ℕ) → G n) → Type ℓ
AlmostNullP G Gstr f = ∥ (AlmostNull G Gstr f) ∥₁

⊕Fun : (G : ℕ → Type ℓ) → (Gstr : (n : ℕ) → AbGroupStr (G n)) → Type ℓ
⊕Fun G Gstr = Σ[ f ∈ ((n : ℕ) → G n) ] AlmostNullP G Gstr f

ext: agda

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
------------------------------------------------------------------------
-- Functors
------------------------------------------------------------------------

-- Note that currently the functor laws are not included here.

module Category.Functor where

open import Data.Function

record RawFunctor (f : Set → Set) : Set₁ where
  infixl 4 _<$>_ _<$_

  field
    _<$>_ : ∀ {a b} → (a → b) → f a → f b

  _<$_ : ∀ {a b} → a → f b → f a
  x <$ y = const x <$> y

max_issues_repo_name: larrytheliquid/Lemmachine


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

--------------------------------------------------------------------------------
-- A simple reflection based solver for categories.
--
-- Based off 'Tactic.MonoidSolver' from 'agda-stdlib'
--------------------------------------------------------------------------------

open import Categories.Category

module Categories.Tactic.Category where

open import Level
open import Function using (_⟨_⟩_)

open import Data.Bool    as Bool    using (Bool; _∨_; if_then_else_)
open import Data.Maybe   as Maybe   using (Maybe; just; nothing; maybe)
open import Data.List    as List    using (List; _∷_; [])
open import Data.Product as Product using (_×_; _,_)

open import Agda.Builtin.Reflection
open import Reflection.Argument
open import Reflection.Term using (getName; _⋯⟅∷⟆_)
open import Reflection.TypeChecking.Monad.Syntax

module _ {o ℓ e} (𝒞 : Category o ℓ e) where

  open Category 𝒞
  open HomReasoning
  open Equiv

  private
    variable
      A B C : Obj
      f g   : A ⇒ B

  --------------------------------------------------------------------------------
  -- An 'Expr' reifies the parentheses/identity morphisms of some series of
  -- compositions of morphisms into a data structure. In fact, this is also
  -- a category!
  --------------------------------------------------------------------------------
  data Expr : Obj → Obj → Set (o ⊔ ℓ) where
    _∘′_ : ∀ {A B C} → Expr B C → Expr A B → Expr A C
    id′  : ∀ {A} → Expr A A
    [_↑] : ∀ {A B} → A ⇒ B → Expr A B

  -- Embed a morphism in 'Expr' back into '𝒞' without normalizing.
  [_↓] : Expr A B → A ⇒ B
  [ f ∘′ g ↓] = [ f ↓] ∘ [ g ↓]
  [ id′ ↓]    = id
  [ [ f ↑] ↓] = f

  -- Convert an 'Expr' back into a morphism, while normalizing
  --
  -- This actually embeds the morphism into the category of copresheaves
  -- on 𝒞, which obeys the category laws up to beta-eta equality.
  -- This lets us normalize away all the associations/identity morphisms.
  embed : Expr B C → A ⇒ B → A ⇒ C
  embed (f ∘′ g) h  = embed f (embed g h)
  embed id′ h       = h
  embed [ f ↑] h    = f ∘ h

  preserves-≈′ : ∀ (f : Expr B C) → (h : A ⇒ B) → embed f id ∘ h ≈ embed f h
  preserves-≈′ id′ f      = identityˡ
  preserves-≈′ [ x ↑] f   = ∘-resp-≈ˡ identityʳ
  preserves-≈′ (f ∘′ g) h = begin
    embed (f ∘′ g) id ∘ h         ≡⟨⟩
    embed f (embed g id) ∘ h      ≈˘⟨ preserves-≈′ f (embed g id) ⟩∘⟨refl ⟩
    (embed f id ∘ embed g id) ∘ h ≈⟨ assoc  ⟩
    embed f id ∘ embed g id ∘ h   ≈⟨ refl⟩∘⟨ preserves-≈′ g h ⟩
    embed f id ∘ embed g h        ≈⟨ preserves-≈′ f (embed g h) ⟩
    embed (f ∘′ g) h              ∎

  preserves-≈ : ∀ (f : Expr A B) → embed f id ≈ [ f ↓]
  preserves-≈ id′      = refl
  preserves-≈ [ x ↑]   = identityʳ
  preserves-≈ (f ∘′ g) = begin
    embed (f ∘′ g) id       ≈˘⟨ preserves-≈′ f (embed g id) ⟩
    embed f id ∘ embed g id ≈⟨ preserves-≈ f ⟩∘⟨ preserves-≈ g ⟩
    [ f ↓] ∘ [ g ↓]         ≡⟨⟩
    [ f ∘′ g ↓]             ∎

--------------------------------------------------------------------------------
-- Reflection Helpers
--------------------------------------------------------------------------------

_==_ = primQNameEquality
{-# INLINE _==_ #-}

getArgs : Term → Maybe (Term × Term)
getArgs (def _ xs) = go xs
  where
  go : List (Arg Term) → Maybe (Term × Term)
  go (vArg x ∷ vArg y ∷ []) = just (x , y)
  go (x ∷ xs)               = go xs
  go _                      = nothing
getArgs _ = nothing

--------------------------------------------------------------------------------
-- Getting Category Names
--------------------------------------------------------------------------------

record CategoryNames : Set where
  field
    is-∘ : Name → Bool
    is-id : Name → Bool

buildMatcher : Name → Maybe Name → Name → Bool
buildMatcher n nothing  x = n == x
buildMatcher n (just m) x = n == x ∨ m == x

findCategoryNames : Term → TC CategoryNames
findCategoryNames cat = do
  ∘-altName ← normalise (def (quote Category._∘_) (3 ⋯⟅∷⟆ cat ⟨∷⟩ []))
  id-altName ← normalise (def (quote Category.id) (3 ⋯⟅∷⟆ cat ⟨∷⟩ []))
  returnTC record
    { is-∘ = buildMatcher (quote Category._∘_) (getName ∘-altName)
    ; is-id = buildMatcher (quote Category.id) (getName id-altName)
    }

--------------------------------------------------------------------------------
-- Constructing an Expr
--------------------------------------------------------------------------------

″id″ : Term
″id″ = quote id′ ⟨ con ⟩ []

″[_↑]″ : Term → Term
″[ t ↑]″ = quote [_↑] ⟨ con ⟩ (t ⟨∷⟩ [])

module _ (names : CategoryNames) where

  open CategoryNames names

  mutual
    ″∘″ : List (Arg Term) → Term
    ″∘″ (x ⟨∷⟩ y ⟨∷⟩ xs) = quote _∘′_ ⟨ con ⟩ buildExpr x ⟨∷⟩ buildExpr y ⟨∷⟩ []
    ″∘″ (x ∷ xs) = ″∘″ xs
    ″∘″ _ = unknown

    buildExpr : Term → Term
    buildExpr t@(def n xs) =
      if (is-∘ n)
        then ″∘″ xs
      else if (is-id n)
        then ″id″
      else
        ″[ t ↑]″
    buildExpr t@(con n xs) =
      if (is-∘ n)
        then ″∘″ xs
      else if (is-id n)
        then ″id″
      else
        ″[ t ↑]″
    buildExpr t = ″[ t ↑]″

--------------------------------------------------------------------------------
-- Constructing the Solution
--------------------------------------------------------------------------------

constructSoln : Term → CategoryNames → Term → Term → Term
constructSoln cat names lhs rhs =
  quote Category.Equiv.trans ⟨ def ⟩ 3 ⋯⟅∷⟆ cat ⟨∷⟩
    (quote Category.Equiv.sym ⟨ def ⟩ 3 ⋯⟅∷⟆ cat ⟨∷⟩
      (quote preserves-≈ ⟨ def ⟩ 3 ⋯⟅∷⟆ cat ⟨∷⟩ buildExpr names lhs ⟨∷⟩ []) ⟨∷⟩ [])
    ⟨∷⟩
    (quote preserves-≈ ⟨ def ⟩ 3 ⋯⟅∷⟆ cat ⟨∷⟩ buildExpr names rhs ⟨∷⟩ [])
    ⟨∷⟩ []

solve-macro : Term → Term → TC _
solve-macro mon hole = do
  hole′ ← inferType hole >>= normalise
  names ← findCategoryNames mon
  just (lhs , rhs) ← returnTC (getArgs hole′)
    where nothing → typeError (termErr hole′ ∷ [])
  let soln = constructSoln mon names lhs rhs
  unify hole soln

macro
  solve : Term → Term → TC _
  solve = solve-macro

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Category.Test where
  open import Equality.Eq

  postulate A : Set
  postulate o : A → A
  postulate x : A
  postulate y : A
  postulate h : A → A → Set
  postulate f : h x y
  postulate I : A
  postulate i : h I I
  postulate m : h x y → h (o x) (o y)
  postulate pf₁ : o x ≅ I
  postulate pf₂ : o y ≅ I

  subst≅2 : {A : Set }{a a' b b' : A}{P : A → A → Set} → a ≅ a' → b ≅ b' → P a b → P a' b'
  subst≅2 refl refl x = x

  eq-f-i-m : Set
  eq-f-i-m = let i-m = let h-pf = eqApp2 pf₁ pf₂ (λ A B → h A B) in subst≅2 {A}{I}{(o x)}{I}{(o y)}{h} (sym pf₁) (sym pf₂) i in m f ≅ i-m

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
module Impure.STLCRef.Syntax where

open import Prelude hiding (subst)
open import Data.Vec
open import Data.List
open import Function

data Type : Set where
  Unit : Type
  _⇒_  : (a b : Type) → Type
  Ref  : Type → Type

infixl 10 _·_
data Exp : (n : ℕ) → Set where
  unit : ∀ {n} → Exp n
  var  : ∀ {n} → Fin n → Exp n
  loc  : ∀ {n} → ℕ → Exp n
  ƛ    : ∀ {n} → Type → Exp (suc n) → Exp n
  _·_  : ∀ {n} → (f e : Exp n) → Exp n
  ref  : ∀ {n} → (e : Exp n) → Exp n
  !_   : ∀ {n} → (e : Exp n) → Exp n
  _≔_  : ∀ {n} → (x y : Exp n) → Exp n

data Val : ∀ {n} → Exp n → Set where
  unit : ∀ {n} → Val {n} unit
  ƛ    : ∀ {n} A → (e : Exp (suc n)) → Val (ƛ A e)
  loc  : ∀ {n} i → Val {n} (loc i)

Store : ℕ → Set
Store n = List (∃ λ (e : Exp n) → Val e)

open import Data.Fin.Substitution

module ExpApp {T} (l : Lift T Exp) where
  open Lift l

  _/_ : ∀ {n n'} → Exp n → Sub T n n' → Exp n'
  var x / s = lift $ lookup x s
  ƛ A t / s = ƛ A (t / (s ↑))
  (f · e) / s = (f / s) · (e / s)
  unit / s = unit
  loc x / s = loc x
  ref e / s = ref (e / s)
  (! e) / s = ! (e / s)
  (e ≔ e₁) / s = (e / s) ≔ (e₁ / s)

  open Application (record { _/_ = _/_ }) using (_/✶_)

tmSubst : TermSubst Exp
tmSubst = record { var = var; app = ExpApp._/_ }

open TermSubst tmSubst hiding (var) public


text:
------------------------------------------------------------------------
-- Finite sets, based on AVL trees
------------------------------------------------------------------------

open import Relation.Binary

module Data.AVL.Sets (OrderedKeySet : StrictTotalOrder) where

import Data.AVL as AVL
open StrictTotalOrder OrderedKeySet renaming (carrier to Key)
open import Data.Unit
open import Data.Function
open import Data.Product as Prod using (_×_; _,_; proj₁)
open import Data.Maybe as Maybe
open import Data.Bool
open import Data.List
open import Category.Functor
open RawFunctor Maybe.functor

-- The set type. (Note that Set is a reserved word.)

private
  open module S = AVL OrderedKeySet (const₁ ⊤)
    public using () renaming (Tree to ⟨Set⟩)

-- Repackaged functions.

empty : ⟨Set⟩
empty = S.empty

singleton : Key → ⟨Set⟩
singleton k = S.singleton k _

insert : Key → ⟨Set⟩ → ⟨Set⟩
insert k = S.insert k _

delete : Key → ⟨Set⟩ → ⟨Set⟩
delete = S.delete

lookup : Key → ⟨Set⟩ → Maybe Key
lookup k s = proj₁ <$> S.lookup k s

_∈?_ : Key → ⟨Set⟩ → Bool
_∈?_ = S._∈?_

headTail : ⟨Set⟩ → Maybe (Key × ⟨Set⟩)
headTail s = Prod.map proj₁ id <$> S.headTail s

initLast : ⟨Set⟩ → Maybe (⟨Set⟩ × Key)
initLast s = Prod.map id proj₁ <$> S.initLast s

fromList : List Key → ⟨Set⟩
fromList = S.fromList ∘ map (λ k → (k , _))

toList : ⟨Set⟩ → List Key
toList = map proj₁ ∘ S.toList


text:
-- Andreas, 2013-10-26, reported by Jesper Cockx

{-# OPTIONS --cubical-compatible #-}

module Issue920a where

import Common.Level
open import Common.Equality

record ⊥ : Set where

data Bool : Set where
  true false : Bool

-- Standard eliminator for ≡
J : ∀ {a b} {A : Set a} {x : A} {Φ : (y : A) → x ≡ y → Set b} →
            Φ x refl → {y : A} → (e : x ≡ y) → Φ y e
J φ refl = φ

-- A kind of heterogeneous equality
_≃_ : {A : Set} (x : A) {A' : Set} → A' → Set _
_≃_ {A} x {A'} x' = (E : A ≡ A') → J x E ≡ x'

-- It shouldn't be possible to define this without K
≃refl : {A : Set} {x : A} → x ≃ x
≃refl {x = x} = λ E → J {Φ = λ A' E' → J x E' ≡ _} refl E

-- These can be given using univalence
postulate Swap : Bool ≡ Bool
postulate swap : true ≡ J {Φ = λ A _ → A} false Swap

-- Univalence and ≃refl don't play nice together
right : (true ≡ false) → ⊥
right ()

wrong : true ≡ false
wrong = trans swap (≃refl Swap)

madness : ⊥
madness = right wrong


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Standard evaluation (Def. 3.3 and Fig. 4i)
------------------------------------------------------------------------

import Parametric.Syntax.Type as Type
import Parametric.Syntax.Term as Term
import Parametric.Denotation.Value as Value

module Parametric.Denotation.Evaluation
    {Base : Type.Structure}
    (Const : Term.Structure Base)
    (⟦_⟧Base : Value.Structure Base)
  where

open Type.Structure Base
open Term.Structure Base Const
open Value.Structure Base ⟦_⟧Base

open import Base.Denotation.Notation

open import Relation.Binary.PropositionalEquality
open import Theorem.CongApp
open import Postulate.Extensionality

-- Extension Point: Evaluation of constants.
Structure : Set
Structure = ∀ {τ} → Const τ → ⟦ τ ⟧

module Structure (⟦_⟧Const : Structure) where
  ⟦_⟧Term : ∀ {Γ τ} → Term Γ τ → ⟦ Γ ⟧ → ⟦ τ ⟧

  -- We provide: Evaluation of arbitrary terms.
  ⟦ const c ⟧Term ρ = ⟦ c ⟧Const
  ⟦ var x ⟧Term ρ = ⟦ x ⟧ ρ
  ⟦ app s t ⟧Term ρ = (⟦ s ⟧Term ρ) (⟦ t ⟧Term ρ)
  ⟦ abs t ⟧Term ρ = λ v → ⟦ t ⟧Term (v • ρ)

  instance
    meaningOfTerm : ∀ {Γ τ} → Meaning (Term Γ τ)
    meaningOfTerm = meaning ⟦_⟧Term

  weaken-sound : ∀ {Γ₁ Γ₂ τ} {Γ₁≼Γ₂ : Γ₁ ≼ Γ₂}
    (t : Term Γ₁ τ) (ρ : ⟦ Γ₂ ⟧) → ⟦ weaken Γ₁≼Γ₂ t ⟧ ρ ≡ ⟦ t ⟧ (⟦ Γ₁≼Γ₂ ⟧ ρ)
  weaken-sound {Γ₁≼Γ₂ = Γ₁≼Γ₂} (var x) ρ = weaken-var-sound Γ₁≼Γ₂ x ρ
  weaken-sound (app s t) ρ = weaken-sound s ρ ⟨$⟩ weaken-sound t ρ
  weaken-sound (abs t) ρ = ext (λ v → weaken-sound t (v • ρ))
  weaken-sound (const c) ρ = refl

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
-- Andreas, 2012-03-15, example by Nisse
-- {-# OPTIONS --show-implicit -v tc.meta:20 #-}
module Issue585-17 where

data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

data ″ℕ″ : Set where
  suc : ″ℕ″ → ″ℕ″

replicate : {A : Set} → ″ℕ″ → A → List A
replicate (suc n) x = x ∷ replicate n x

data P (A B : Set) : List B → Set where
  p : (x : B) → P A B (x ∷ [])

data Q {A B xs} : List B → P A B xs → Set where
  q : ∀ {x xs p} → Q xs p → Q (x ∷ xs) p

foo : {A B : Set} (x : B) (n : ″ℕ″) → Q (replicate n x) (p {A = A} x)
foo x n = bar x n
  where
  bar : {B : Set} (x : B) (n : ″ℕ″) → Q (replicate n x) (p x)
  bar x (suc n) = q (bar x n)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Theorems of ⊃ connective.
------------------------------------------------------------------------------

open import Data.Nat using ( ℕ )

module Data.PropFormula.Theorems.Implication ( n : ℕ ) where

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

open import Data.PropFormula.Syntax n
open import Data.PropFormula.Theorems.Classical n

open import Function using ( _$_; _∘_; flip )

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

-- Theorem.
⊃-equiv
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ φ ⊃ ψ
  → Γ ⊢ ¬ φ ∨ ψ
⊃-to-¬∨ = ⊃-equiv

-- Proof.
⊃-equiv {φ = φ}{ψ} Γ⊢φ⊃ψ =
  (⊃-elim
    (⊃-intro
      (∨-elim
        (∨-intro₂ (¬ φ)
          (⊃-elim
            (weaken φ Γ⊢φ⊃ψ)
            (assume φ)))
        (∨-intro₁ ψ
          (assume (¬ φ)))))
      PEM)
-------------------------------------------------------------------------- ∎

-- Theorems from the book:
-- van Dalen 4th Edition. Chapter 2. Section 2.4.

-- Theorem.
vanDalen244a
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ φ ⊃ (ψ ⊃ φ)

-- Proof.
vanDalen244a {φ = φ}{ψ} =
  (⊃-intro
    (⊃-intro
      (weaken ψ
        (assume φ))))
-------------------------------------------------------------------------- ∎

-- Theorem.
vanDalen244b
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ φ ⊃ (¬ φ ⊃ ψ)

-- Proof.
vanDalen244b {Γ}{φ}{ψ} =
  ⊃-intro $
    ⊃-intro $
      ⊥-elim {Γ = (Γ , φ , ¬ φ)} ψ $
        ¬-elim
          (assume  {Γ = Γ , φ} (¬ φ))
          (weaken (¬ φ) (assume φ))
-------------------------------------------------------------------------- ∎

-- Theorem.
vanDalen244c
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ (φ ⊃ ψ) ⊃ ((ψ ⊃ γ) ⊃ (φ ⊃ γ))

-- Proof.
vanDalen244c {Γ}{φ}{ψ}{γ} =
  ⊃-intro $
    ⊃-intro $
      ⊃-intro $
        ⊃-elim
          (weaken φ $
            assume {Γ = Γ , φ ⊃ ψ} $ ψ ⊃ γ)
          (⊃-elim
            (weaken φ $
              weaken (ψ ⊃ γ) $
                assume $ φ ⊃ ψ)
            (assume {Γ = Γ , φ ⊃ ψ , ψ ⊃ γ} φ))
-------------------------------------------------------------------------- ∎

-- Theorem.
vanDalen244d
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ ¬ ψ ⊃ ¬ φ
  → Γ ⊢ φ ⊃ ψ
¬⊃¬-to-⊃ = vanDalen244d
contraposition₁ = vanDalen244d

-- Proof.
vanDalen244d {Γ}{φ}{ψ} Γ⊢¬ψ⊃¬φ =
  (⊃-elim
    (⊃-intro $
      (⊃-intro $
        RAA $
          ¬-elim
            (⊃-elim
              (weaken (¬ ψ) $
                weaken φ $
                  assume $ ¬ ψ  ⊃ ¬ φ)
              (assume {Γ = Γ , ¬ ψ ⊃ ¬ φ , φ} $ ¬ ψ))
            (weaken (¬ ψ) $
              assume {Γ = Γ , ¬ ψ ⊃ ¬ φ} φ)))
      Γ⊢¬ψ⊃¬φ)
-------------------------------------------------------------------------- ∎

-- Theorem.
contraposition₂
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ φ ⊃ ψ
  → Γ ⊢ ¬ ψ ⊃ ¬ φ
⊃-to-¬⊃¬ = contraposition₂

-- Proof.
contraposition₂ {Γ}{φ}{ψ} Γ⊢φ⊃ψ =
  ⊃-intro
    (¬-intro
      (¬-elim
        (weaken φ (assume (¬ ψ)))
        (⊃-elim
          (weaken φ (weaken (¬ ψ) Γ⊢φ⊃ψ))
          (assume {Γ = Γ , ¬ ψ} φ))))
-------------------------------------------------------------------------- ∎

-- Theorem.
vanDalen244e
  : ∀ {Γ} {φ}
  → Γ ⊢ ¬ (¬ φ) ⊃ φ

-- Proof.
vanDalen244e {Γ}{φ} =
  ⊃-intro $ RAA
    (¬-elim
      (weaken (¬ φ) $
        assume $ ¬ (¬ φ))
      (assume {Γ = Γ , ¬ (¬ φ)} $ ¬ φ))
-------------------------------------------------------------------------- ∎

-- Theorem.
⊃⊃-to-∧⊃
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ φ ⊃ (ψ ⊃ γ)
  → Γ ⊢ (φ ∧ ψ) ⊃ γ

-- Proof.
⊃⊃-to-∧⊃ {Γ}{φ}{ψ} Γ⊢φ⊃ψ⊃γ =
  ⊃-intro
    (⊃-elim
      (⊃-elim
        (weaken (φ ∧ ψ) Γ⊢φ⊃ψ⊃γ)
        (∧-proj₁ (assume (φ ∧ ψ))))
      (∧-proj₂ (assume (φ ∧ ψ))))
-------------------------------------------------------------------------- ∎

-- Theorem.
∧⊃-to-⊃⊃
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ (φ ∧ ψ) ⊃ γ
  → Γ ⊢ φ ⊃ (ψ ⊃ γ)

-- Proof.
∧⊃-to-⊃⊃ {Γ}{φ}{ψ} Γ⊢φ∧ψ⊃γ =
  ⊃-intro
    (⊃-intro
      (⊃-elim
        (weaken ψ (weaken φ Γ⊢φ∧ψ⊃γ))
        (∧-intro
          (weaken ψ (assume φ))
          (assume {Γ = Γ , φ} ψ))))
-------------------------------------------------------------------------- ∎

-- Theorem.
⊃∧⊃-to-⊃∧
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ (φ ⊃ ψ) ∧ (φ ⊃ γ)
  → Γ ⊢ φ ⊃ (ψ ∧ γ)

-- Proof.
⊃∧⊃-to-⊃∧ {φ = φ} Γ⊢⟨φ⊃ψ⟩∧⟨φ⊃γ⟩ =
  ⊃-intro
    (∧-intro
      (⊃-elim (∧-proj₁ (weaken φ Γ⊢⟨φ⊃ψ⟩∧⟨φ⊃γ⟩)) (assume φ))
      (⊃-elim (∧-proj₂ (weaken φ Γ⊢⟨φ⊃ψ⟩∧⟨φ⊃γ⟩)) (assume φ)))
-------------------------------------------------------------------------- ∎

-- Theorem.
subst⊢⊃₁
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ γ ⊃ φ
  → Γ ⊢ φ ⊃ ψ
  → Γ ⊢ γ ⊃ ψ

-- Proof.
subst⊢⊃₁ {γ = γ} Γ⊢ψ⊃γ Γ⊢φ⊃ψ =
  ⊃-intro
    (⊃-elim
      (weaken γ Γ⊢φ⊃ψ)
      (⊃-elim (weaken γ Γ⊢ψ⊃γ) (assume γ)))
-------------------------------------------------------------------------- ∎

-- Theorem.
subst⊢⊃₂
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ ψ ⊃ γ
  → Γ ⊢ φ ⊃ ψ
  → Γ ⊢ φ ⊃ γ

-- Proof.
subst⊢⊃₂ {φ = φ} Γ⊢γ⊃φ Γ⊢φ⊃ψ =
 ⊃-intro
   (⊃-elim
     (weaken φ Γ⊢γ⊃φ)
     (⊃-elim (weaken φ Γ⊢φ⊃ψ) (assume φ)))
-------------------------------------------------------------------------- ∎

-- Theorem.
⊃-trans
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ φ ⊃ ψ
  → Γ ⊢ ψ ⊃ γ
  → Γ ⊢ φ ⊃ γ

-- Proof.
⊃-trans Γ⊢φ⊃ψ Γ⊢ψ⊃γ = subst⊢⊃₂ Γ⊢ψ⊃γ Γ⊢φ⊃ψ
-------------------------------------------------------------------------- ∎

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
module Luau.Substitution where

open import Luau.Syntax using (Expr; Stat; Block; nil; addr; var; function⟨_⟩_end; _$_; block_is_end; local_←_; _∙_; done; function_⟨_⟩_end; return)
open import Luau.Value using (Value; val)
open import Luau.Var using (Var; _≡ⱽ_)
open import Properties.Dec using (Dec; yes; no)

_[_/_]ᴱ : Expr → Value → Var → Expr
_[_/_]ᴮ : Block → Value → Var → Block
var_[_/_]ᴱwhenever_ : ∀ {P} → Var → Value → Var → (Dec P) → Expr
_[_/_]ᴮunless_ : ∀ {P} → Block → Value → Var → (Dec P) → Block

nil [ v / x ]ᴱ = nil
var y [ v / x ]ᴱ = var y [ v / x ]ᴱwhenever (x ≡ⱽ y)
addr a [ v / x ]ᴱ = addr a
(M $ N) [ v / x ]ᴱ = (M [ v / x ]ᴱ) $ (N [ v / x ]ᴱ)
function⟨ y ⟩ C end [ v / x ]ᴱ = function⟨ y ⟩ C [ v / x ]ᴮunless (x ≡ⱽ y) end
block b is C end [ v / x ]ᴱ = block b is C [ v / x ]ᴮ end

(function f ⟨ y ⟩ C end ∙ B) [ v / x ]ᴮ = function f ⟨ y ⟩ (C [ v / x ]ᴮunless (x ≡ⱽ y)) end ∙ (B [ v / x ]ᴮunless (x ≡ⱽ f))
(local y ← M ∙ B) [ v / x ]ᴮ = local y ← (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮunless (x ≡ⱽ y))
(return M ∙ B) [ v / x ]ᴮ = return (M [ v / x ]ᴱ) ∙ (B [ v / x ]ᴮ)
done [ v / x ]ᴮ = done

var y [ v / x ]ᴱwhenever yes p = val v
var y [ v / x ]ᴱwhenever no p = var y

B [ v / x ]ᴮunless yes p = B
B [ v / x ]ᴮunless no p = B [ v / x ]ᴮ

max_stars_repo_name: FreakingBarbarians/luau

max_issues_repo_name: FreakingBarbarians/luau

max_forks_repo_name: FreakingBarbarians/luau


text:
module Issue1691.Nat where

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ #-}

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero  = m
zero  ∸ suc n = zero
suc m ∸ suc n = m ∸ n

pred : ℕ → ℕ
pred zero    = zero
pred (suc n) = n


text:
module Issue2579.Instance (A : Set) (a : A) where

open import Issue2579.Import

instance
  w : Wrap A
  w = wrap a

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module BuiltinMustBeConstructor where

data Bool : Set where
  true  : Bool
  other : Bool

false : Bool
false = true

{-# BUILTIN BOOL Bool #-}
{-# BUILTIN TRUE true #-}
{-# BUILTIN FALSE false #-}


text:
open import Relation.Binary.Core

module PLRTree.DropLast.Complete {A : Set}
                     (_≤_ : A → A → Set)
                     (tot≤ : Total _≤_)  where

open import Data.Sum renaming (_⊎_ to _∨_)
open import PLRTree {A}
open import PLRTree.Drop _≤_ tot≤
open import PLRTree.Complete {A}
open import PLRTree.Complete.Properties {A}
open import PLRTree.Compound {A}
open import PLRTree.Equality {A}
open import PLRTree.Equality.Properties {A}

lemma-dropLast-≃ : {l r : PLRTree} → l ≃ r → Compound l → l ⋙ dropLast r
lemma-dropLast-≃ (≃nd x x' ≃lf ≃lf ≃lf) compound = ⋙p (⋗lf x)
lemma-dropLast-≃ (≃nd x x' (≃nd _ _ _ _ _) ≃lf ()) compound
lemma-dropLast-≃ (≃nd x x' l≃r (≃nd x'₁ x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) (≃nd x₁ .x'₁ l₁≃r₁ _ l₁≃l'₁)) compound =
               let x'₁l'₁r'₁⋙dl-x'₂l'₂r'₂ = lemma-dropLast-≃ (≃nd x'₁ x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁≃l'₂) compound
               in ⋙r x x' l≃r x'₁l'₁r'₁⋙dl-x'₂l'₂r'₂ (≃nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁≃l'₁)

lemma-dropLast-⋗ : {l r : PLRTree} → l ⋗ r → Compound r → dropLast l ⋘ r
lemma-dropLast-⋗ (⋗nd _ _ ≃lf _ ()) compound
lemma-dropLast-⋗ (⋗nd x x' (≃nd x₁ x₂ ≃lf ≃lf ≃lf) ≃lf (⋗lf .x₁)) compound  = x⋘ x x₁ x'
lemma-dropLast-⋗ (⋗nd _ _ (≃nd x₁ _ ≃lf (≃nd _ _ _ _ _) ()) ≃lf (⋗lf .x₁)) compound
lemma-dropLast-⋗ (⋗nd x x' (≃nd {l₁} {r₁} x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) l'≃r' (⋗nd .x₁ x'₁ _ l'₁≃r'₁ l₁⋗l'₁)) compound =
               let x₁l₁r₁⋙dl-x₂l₂r₂ = lemma-dropLast-≃ (≃nd x₁ x₂ l₁≃r₁ l₂≃r₂ l₁≃l₂) compound
               in r⋘ x x' x₁l₁r₁⋙dl-x₂l₂r₂ l'≃r' (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁)

mutual
  lemma-dropLast-⋘ : {l r : PLRTree} → l ⋘ r → dropLast l ⋘ r ∨ dropLast l ≃ r
  lemma-dropLast-⋘ (x⋘ x _ z) = inj₂ (≃nd x z ≃lf ≃lf ≃lf)
  lemma-dropLast-⋘ (l⋘ x x' (x⋘ x₁ x₂ x₃) x'₁≃x'₂ (≃nd .x₃ x'₁ ≃lf ≃lf ≃lf)) = inj₂ (≃nd x x' (≃nd x₁ x₃ ≃lf ≃lf ≃lf) x'₁≃x'₂ (≃nd x₁ x'₁ ≃lf ≃lf ≃lf))
  lemma-dropLast-⋘ (l⋘ x x' (l⋘ {l₁} {r₁} x₁ x₂ l₁⋘r₁ l₂≃r₂ r₁≃l₂) l'≃r' (≃nd .x₂ x'₁ _ l'₁≃r'₁ l₂≃l'₁))
      with dropLast (node left x₁ l₁ r₁) | lemma-dropLast-⋘ (l⋘ x₁ x₂ l₁⋘r₁ l₂≃r₂ r₁≃l₂)
  ... | leaf | inj₁ ()
  ... | node perfect _ _ _ | inj₁ ()
  ... | node left _ _ _ | inj₁ dl-x₁l₁r₁⋘x₂l₂r₂ = inj₁ (l⋘ x x' dl-x₁l₁r₁⋘x₂l₂r₂ l'≃r' (≃nd x₂ x'₁ l₂≃r₂ l'₁≃r'₁ l₂≃l'₁))
  ... | node right _ _ _ | inj₁ dl-x₁l₁r₁⋘x₂l₂r₂ = inj₁ (l⋘ x x' dl-x₁l₁r₁⋘x₂l₂r₂ l'≃r' (≃nd x₂ x'₁ l₂≃r₂ l'₁≃r'₁ l₂≃l'₁))
  ... | leaf | inj₂ ()
  ... | node perfect x'' l'' r'' | inj₂ (≃nd .x'' .x₂ l''≃r'' _ l''≃l₂) =
               let l''≃l'₁ = trans≃ l''≃l₂ l₂≃l'₁
               in inj₂ (≃nd x x' (≃nd x'' x₂ l''≃r'' l₂≃r₂ l''≃l₂) l'≃r' (≃nd x'' x'₁ l''≃r'' l'₁≃r'₁ l''≃l'₁))
  ... | node left _ _ _ | inj₂ ()
  ... | node right _ _ _ | inj₂ ()
  lemma-dropLast-⋘ (l⋘ x x' (r⋘ {l₁} {r₁} x₁ x₂ l₁⋙r₁ l₂≃r₂ l₁⋗l₂) l'≃r' (≃nd .x₂ x'₁ _ l'₁≃r'₁ l₂≃l'₁))
      with dropLast (node right x₁ l₁ r₁) | lemma-dropLast-⋘ (r⋘ x₁ x₂ l₁⋙r₁ l₂≃r₂ l₁⋗l₂)
  ... | leaf | inj₁ ()
  ... | node perfect _ _ _ | inj₁ ()
  ... | node left _ _ _ | inj₁ dl-x₁l₁r₁⋘x₂l₂r₂ = inj₁ (l⋘ x x' dl-x₁l₁r₁⋘x₂l₂r₂ l'≃r' (≃nd x₂ x'₁ l₂≃r₂ l'₁≃r'₁ l₂≃l'₁))
  ... | node right _ _ _ | inj₁ dl-x₁l₁r₁⋘x₂l₂r₂ = inj₁ (l⋘ x x' dl-x₁l₁r₁⋘x₂l₂r₂ l'≃r' (≃nd x₂ x'₁ l₂≃r₂ l'₁≃r'₁ l₂≃l'₁))
  ... | leaf | inj₂ ()
  ... | node perfect x'' l'' r'' | inj₂ (≃nd .x'' .x₂ l''≃r'' _ l''≃l₂) =
               let l''≃l'₁ = trans≃ l''≃l₂ l₂≃l'₁
               in inj₂ (≃nd x x' (≃nd x'' x₂ l''≃r'' l₂≃r₂ l''≃l₂) l'≃r' (≃nd x'' x'₁ l''≃r'' l'₁≃r'₁ l''≃l'₁))
  ... | node left _ _ _ | inj₂ ()
  ... | node right _ _ _ | inj₂ ()
  lemma-dropLast-⋘ (r⋘ x x' (⋙p (⋗lf x₁)) ≃lf (⋗lf .x₁))  = inj₂ (≃nd x x' ≃lf ≃lf ≃lf)
  lemma-dropLast-⋘ (r⋘ _ _ (⋙p (⋗lf x₁)) l'≃r' (⋗nd .x₁ _ _ _ ()))
  lemma-dropLast-⋘ (r⋘ _ _ (⋙p (⋗nd x₁ _ ≃lf _ ())) ≃lf (⋗lf .x₁))
  lemma-dropLast-⋘ (r⋘ x x' (⋙p (⋗nd x₁ x₂ l₁≃r₁ l₂≃r₂ l₁⋗l₂)) l'≃r' (⋗nd .x₁ x'₁ _ l'₁≃r'₁ l₁⋗l'₁)) =
               let dl-x₁l₁r₁⋘x₂l₂r₂ = lemma-dropLast-⋗ (⋗nd x₁ x₂ l₁≃r₁ l₂≃r₂ l₁⋗l₂) compound ;
                    l₂≃l'₁ = lemma-⋗* l₁⋗l₂ l₁⋗l'₁
               in inj₁ (l⋘ x x' dl-x₁l₁r₁⋘x₂l₂r₂ l'≃r' (≃nd x₂ x'₁ l₂≃r₂ l'₁≃r'₁ l₂≃l'₁))
  lemma-dropLast-⋘ (r⋘ _ _ (⋙l x₁ _ ≃lf _ ()) ≃lf (⋗lf .x₁))
  lemma-dropLast-⋘ (r⋘ x x' (⋙l x₁ x₂ l₁≃r₁ l₂⋘r₂ l₁⋗r₂) l'≃r' (⋗nd .x₁ x'₁ _ l'₁≃r'₁ l₁⋗l'₁))
      with lemma-dropLast-⋙ (⋙l x₁ x₂ l₁≃r₁ l₂⋘r₂ l₁⋗r₂)
  ... | inj₁ dl-x₁l₁r₁⋘x₂l₂r₂ = inj₁ (r⋘ x x' dl-x₁l₁r₁⋘x₂l₂r₂ l'≃r' (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁))
  ... | inj₂ ()
  lemma-dropLast-⋘ (r⋘ x x' (⋙r x₁ x₂ ≃lf (⋙p ()) ≃lf) ≃lf (⋗lf .x₁))
  lemma-dropLast-⋘ (r⋘ _ _ (⋙r x₁ _ ≃lf (⋙l _ _ _ _ _) ()) ≃lf (⋗lf .x₁))
  lemma-dropLast-⋘ (r⋘ _ _ (⋙r x₁ _ ≃lf (⋙r _ _ _ _ _) ()) ≃lf (⋗lf .x₁))
  lemma-dropLast-⋘ (r⋘ x x' (⋙r x₁ x₂ l₁≃r₁ l₂⋙r₂ l₁≃l₂) l'≃r' (⋗nd .x₁ x'₁ _ l'₁≃r'₁ l₁⋗l'₁))
      with lemma-dropLast-⋙ (⋙r x₁ x₂ l₁≃r₁ l₂⋙r₂ l₁≃l₂)
  ... | inj₁ dl-x₁l₁r₁⋘x₂l₂r₂ = inj₁ (r⋘ x x' dl-x₁l₁r₁⋘x₂l₂r₂ l'≃r' (⋗nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁⋗l'₁))
  ... | inj₂ ()

  lemma-dropLast-⋙ : {l r : PLRTree} → l ⋙ r → l ⋙ dropLast r ∨ l ⋗ r
  lemma-dropLast-⋙ (⋙p l⋗r) = inj₂ l⋗r
  lemma-dropLast-⋙ (⋙l x x' l≃r (x⋘ x'₁ x'₂ x'₃) (⋗nd x₁ .x'₃ l₁≃r₁ ≃lf l₁⋗x'₂)) = inj₁ (⋙p (⋗nd x x' l≃r (≃nd x'₁ x'₃ ≃lf ≃lf ≃lf) (⋗nd x₁ x'₁ l₁≃r₁ ≃lf l₁⋗x'₂)))
  lemma-dropLast-⋙ (⋙l x x' l≃r (l⋘ {l'₁} {r'₁} x'₁ x'₂ l'₁⋘r'₁ l'₂≃r'₂ r'₁≃l'₂) (⋗nd x₁ .x'₂ l₁≃r₁ _ l₁⋗l'₂))
      with dropLast (node left x'₁ l'₁ r'₁) | lemma-dropLast-⋘ (l⋘ x'₁ x'₂ l'₁⋘r'₁ l'₂≃r'₂ r'₁≃l'₂)
  ... | leaf | inj₁ ()
  ... | node perfect _ _ _ | inj₁ ()
  ... | node left _ _ _ | inj₁ dl-x'₁l'₁r'₁⋘x'₂l'₂r'₂ = inj₁ (⋙l x x' l≃r dl-x'₁l'₁r'₁⋘x'₂l'₂r'₂ (⋗nd x₁ x'₂ l₁≃r₁ l'₂≃r'₂ l₁⋗l'₂))
  ... | node right _ _ _ | inj₁ dl-x'₁l'₁r'₁⋘x'₂l'₂r'₂ = inj₁ (⋙l x x' l≃r dl-x'₁l'₁r'₁⋘x'₂l'₂r'₂ (⋗nd x₁ x'₂ l₁≃r₁ l'₂≃r'₂ l₁⋗l'₂))
  ... | leaf | inj₂ ()
  ... | node perfect x'' l'' r'' | inj₂ (≃nd .x'' .x'₂ l''≃r'' _ l''≃l'₂) =
               let l₁⋗l'' = lemma-⋗-≃ l₁⋗l'₂ (sym≃ l''≃l'₂)
               in inj₁ (⋙p (⋗nd x x' l≃r (≃nd x'' x'₂ l''≃r'' l'₂≃r'₂ l''≃l'₂) (⋗nd x₁ x'' l₁≃r₁ l''≃r'' l₁⋗l'')))
  ... | node left _ _ _ | inj₂ ()
  ... | node right _ _ _ | inj₂ ()
  lemma-dropLast-⋙ (⋙l x x' l≃r (r⋘ {l'₁} {r'₁} x'₁ x'₂ l'₁⋙r'₁ l'₂≃r'₂ l'₁⋗l'₂) (⋗nd x₁ .x'₂ l₁≃r₁ _ l₁⋗l'₂))
      with dropLast (node right x'₁ l'₁ r'₁) | lemma-dropLast-⋘ (r⋘ x'₁ x'₂ l'₁⋙r'₁ l'₂≃r'₂ l'₁⋗l'₂)
  ... | leaf | inj₁ ()
  ... | node perfect _ _ _ | inj₁ ()
  ... | node left _ _ _ | inj₁ dl-x'₁l'₁r'₁⋘x'₂l'₂r'₂ = inj₁ (⋙l x x' l≃r dl-x'₁l'₁r'₁⋘x'₂l'₂r'₂ (⋗nd x₁ x'₂ l₁≃r₁ l'₂≃r'₂ l₁⋗l'₂))
  ... | node right _ _ _ | inj₁ dl-x'₁l'₁r'₁⋘x'₂l'₂r'₂ = inj₁ (⋙l x x' l≃r dl-x'₁l'₁r'₁⋘x'₂l'₂r'₂ (⋗nd x₁ x'₂ l₁≃r₁ l'₂≃r'₂ l₁⋗l'₂))
  ... | leaf | inj₂ ()
  ... | node perfect x'' l'' r'' | inj₂ (≃nd .x'' .x'₂ l''≃r'' _ l''≃l'₂) =
               let l₁⋗l'' = lemma-⋗-≃ l₁⋗l'₂ (sym≃ l''≃l'₂)
               in inj₁ (⋙p (⋗nd x x' l≃r (≃nd x'' x'₂ l''≃r'' l'₂≃r'₂ l''≃l'₂) (⋗nd x₁ x'' l₁≃r₁ l''≃r'' l₁⋗l'')))
  ... | node left _ _ _ | inj₂ ()
  ... | node right _ _ _ | inj₂ ()
  lemma-dropLast-⋙ (⋙r x x' l≃r (⋙p ()) ≃lf)
  lemma-dropLast-⋙ (⋙r x x' l≃r (⋙p (⋗lf x'₁)) (≃nd x₁ .x'₁ ≃lf ≃lf ≃lf)) = inj₁ (⋙p (⋗nd x x' l≃r ≃lf (⋗lf x₁)))
  lemma-dropLast-⋙ (⋙r x x' l≃r (⋙p (⋗nd x'₁ x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁⋗l'₂)) (≃nd x₁ .x'₁ l₁≃r₁ _ l₁≃l'₁)) =
               let dl-x'₁l'₁r'₁⋘x'₂l'₂r'₂ =  lemma-dropLast-⋗ (⋗nd x'₁ x'₂ l'₁≃r'₁ l'₂≃r'₂ l'₁⋗l'₂) compound ;
                    l₁⋗l'₂ = lemma-≃-⋗ (sym≃ l₁≃l'₁) l'₁⋗l'₂
               in inj₁ (⋙l x x' l≃r dl-x'₁l'₁r'₁⋘x'₂l'₂r'₂ (⋗nd x₁ x'₂ l₁≃r₁ l'₂≃r'₂ l₁⋗l'₂))
  lemma-dropLast-⋙ (⋙r x x' l≃r (⋙l x'₁ x'₂ l'₁≃r'₁ l'₂⋘r'₂ l'₁⋗r'₂) (≃nd x₁ .x'₁ l₁≃r₁ _ l₁≃l'₁))
      with lemma-dropLast-⋙ (⋙l x'₁ x'₂ l'₁≃r'₁ l'₂⋘r'₂ l'₁⋗r'₂)
  ... | inj₁ x'₁l'₁r'₁⋙dl-x'₂l'₂r'₂ = inj₁ (⋙r x x' l≃r x'₁l'₁r'₁⋙dl-x'₂l'₂r'₂ (≃nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁≃l'₁))
  ... | inj₂ ()
  lemma-dropLast-⋙ (⋙r x x' l≃r (⋙r x'₁ x'₂ l'₁≃r'₁ l'₂⋙r'₂ l'₁≃l'₂) (≃nd x₁ .x'₁ l₁≃r₁ _ l₁≃l'₁))
      with lemma-dropLast-⋙ (⋙r x'₁ x'₂ l'₁≃r'₁ l'₂⋙r'₂ l'₁≃l'₂)
  ... | inj₁ x'₁l'₁r'₁⋙dl-x'₂l'₂r'₂ = inj₁ (⋙r x x' l≃r x'₁l'₁r'₁⋙dl-x'₂l'₂r'₂ (≃nd x₁ x'₁ l₁≃r₁ l'₁≃r'₁ l₁≃l'₁))
  ... | inj₂ ()

lemma-dropLast-complete : {t : PLRTree} → Complete t → Complete (dropLast t)
lemma-dropLast-complete leaf = leaf
lemma-dropLast-complete (perfect {l} {r} x cl cr l≃r)
     with l | r | l≃r
... | leaf | leaf | ≃lf = leaf
... | node perfect x' l' r' | node perfect x'' l'' r'' | ≃nd .x' .x'' l'≃r' l''≃r'' l'≃l'' = right x cl (lemma-dropLast-complete cr) (lemma-dropLast-≃ (≃nd x' x'' l'≃r' l''≃r'' l'≃l'') compound)
lemma-dropLast-complete (left {l} {r} x cl cr l⋘r)
    with l | r | l⋘r | lemma-dropLast-⋘ l⋘r
... | leaf | _ | () | _
... | node perfect x' l' r' | _ | () | _
... | node left x' l' r' | node perfect x'' l'' r'' | l⋘ .x' .x'' l'⋘r' l''≃r'' r'≃l'' | inj₁ ld⋘r
    with dropLast (node left x' l' r') | ld⋘r | lemma-dropLast-complete cl
... | leaf | () | _
... | node perfect _ _ _ | () | _
... | node left x''' l''' r''' | ld⋘r' | cld = left x cld cr ld⋘r'
... | node right x''' l''' r''' | ld⋘r' | cld = left x cld cr ld⋘r'
lemma-dropLast-complete (left x cl cr l⋘r) | node left x' l' r' | node perfect x'' l'' r'' | l⋘ .x' .x'' l'⋘r' l''≃r'' r'≃l'' | inj₂ ld≃r
    with dropLast (node left x' l' r') | ld≃r | lemma-dropLast-complete cl
... | leaf | () | _
... | node perfect x''' l''' r''' | ld≃r' | cld = perfect x cld cr ld≃r'
... | node left _ _ _ | () | _
... | node right _ _ _ | () | _
lemma-dropLast-complete (left x cl cr l⋘r) | node right x' l' r' | leaf | () | _
lemma-dropLast-complete (left x cl cr l⋘r) | node right x' (node perfect x'' leaf leaf) leaf | node perfect x''' leaf leaf | x⋘ .x' .x'' .x''' | inj₁ ()
lemma-dropLast-complete (left x cl cr l⋘r) | node right x' (node perfect x'' leaf leaf) leaf | node perfect x''' leaf leaf | x⋘ .x' .x'' .x''' | inj₂ x'≃x''' =
           perfect x (perfect x' leaf leaf ≃lf) cr x'≃x'''
lemma-dropLast-complete (left x cl cr l⋘r) | node right x' l' r' | node perfect x'' l'' r'' | r⋘ .x' .x'' l⋙r l''≃r'' l'⋗l'' | inj₁ ld⋘r
    with dropLast (node right x' l' r') | ld⋘r | lemma-dropLast-complete cl
... | leaf | () | _
... | node perfect _ _ _ | () | _
... | node left x''' l''' r''' | ld⋘r' | cld = left x cld cr ld⋘r'
... | node right x''' l''' r''' | ld⋘r' | cld = left x cld cr ld⋘r'
lemma-dropLast-complete (left x cl cr l⋘r) | node right x' l' r' | node perfect x'' l'' r'' | r⋘ .x' .x'' l⋙r l''≃r'' l'⋗l'' | inj₂ ld≃r
    with dropLast (node right x' l' r') | ld≃r | lemma-dropLast-complete cl
... | leaf | () | _
... | node perfect x''' l''' r''' | ld≃r' | cld = perfect x cld cr ld≃r'
... | node left _ _ _ | () | _
... | node right _ _ _ | () | _
lemma-dropLast-complete (left x cl cr l⋘r) | node right x' l' r' | node left x'' l'' r'' | () | _
lemma-dropLast-complete (left x cl cr l⋘r) | node right x' l' r' | node right x'' l'' r'' | () | _
lemma-dropLast-complete (right {l} {r} x cl cr l⋙r)
    with l | r | l⋙r
... | leaf | _ | ⋙p ()
... | node perfect x' leaf leaf | leaf | ⋙p (⋗lf .x') = perfect x leaf leaf ≃lf
... | node perfect x' leaf leaf | node left _ _ _ | ⋙p ()
... | node perfect x' leaf leaf | node right _ _ _ | ⋙p ()
... | node perfect x' l' r' | node perfect x'' l'' r'' | ⋙p (⋗nd .x' .x'' l'≃r' l''≃r'' l'⋗l'') = left x (lemma-dropLast-complete cl) cr (lemma-dropLast-⋗ (⋗nd x' x'' l'≃r' l''≃r'' l'⋗l'') compound)
... | node perfect x' l' r' | node left x'' l'' r'' | ⋙l .x' .x'' l'≃r' l''⋘r'' l'⋗r''
    with lemma-dropLast-⋙ (⋙l x' x'' l'≃r' l''⋘r'' l'⋗r'')
... | inj₁ l⋙rd = right x cl (lemma-dropLast-complete  cr) l⋙rd
... | inj₂ ()
lemma-dropLast-complete (right x cl cr l⋙r) | node perfect x' l' r' | node right x'' l'' r'' | ⋙r .x' .x'' l'≃r' l''⋙r'' l'≃l''
    with lemma-dropLast-⋙ (⋙r x' x'' l'≃r' l''⋙r'' l'≃l'')
... | inj₁ l⋙rd = right x cl (lemma-dropLast-complete cr) l⋙rd
... | inj₂ ()
lemma-dropLast-complete (right x cl cr l⋙r) | node left _ _ _ | _ | ⋙p ()
lemma-dropLast-complete (right x cl cr l⋙r) | node right _ _ _ | _ | ⋙p ()

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Direction where

open import Relation.Binary.PropositionalEquality hiding (Extensionality)

----------------------------------------------------------------------
-- direction

data Dir : Set where
  SND RCV : Dir

variable
  d d₁ d₂ d₃ : Dir

-- dual
dual-dir : Dir → Dir
dual-dir SND = RCV
dual-dir RCV = SND

dual-dir-inv : (d : Dir) → dual-dir (dual-dir d) ≡ d
dual-dir-inv SND = refl
dual-dir-inv RCV = refl

max_stars_repo_name: kcaliban/dual-session

max_issues_repo_name: kcaliban/dual-session

max_forks_repo_name: kcaliban/dual-session


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

open import Setoids.Setoids
open import Groups.Definition
open import Groups.Abelian.Definition

module Groups.Abelian.DirectSum {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+1_ : A → A → A} {_+2_ : B → B → B} {G1' : Group S _+1_} {G2' : Group T _+2_} (G1 : AbelianGroup G1') (G2 : AbelianGroup G2') where

open import Groups.DirectSum.Definition G1' G2'
open import Setoids.Product S T

directSumAbGroup : AbelianGroup directSumGroup
AbelianGroup.commutative directSumAbGroup = productLift (AbelianGroup.commutative G1) (AbelianGroup.commutative G2)


text:
open import Nat
open import Prelude
open import contexts
open import core

module canonical-value-forms where
  canonical-value-forms-b : ∀{Δ d} →
                            Δ , ∅ ⊢ d :: b →
                            d val →
                            d == c
  canonical-value-forms-b TAConst VConst = refl
  canonical-value-forms-b (TAVar x₁) ()
  canonical-value-forms-b (TAAp wt wt₁) ()
  canonical-value-forms-b (TAEHole x x₁) ()
  canonical-value-forms-b (TANEHole x wt x₁) ()
  canonical-value-forms-b (TACast wt x) ()
  canonical-value-forms-b (TAFailedCast wt x x₁ x₂) ()

  canonical-value-forms-arr : ∀{Δ d τ1 τ2} →
                              Δ , ∅ ⊢ d :: (τ1 ==> τ2) →
                              d val →
                              Σ[ x ∈ Nat ] Σ[ d' ∈ ihexp ]
                                ((d == (·λ x [ τ1 ] d')) ×
                                 (Δ , ■ (x , τ1) ⊢ d' :: τ2))
  canonical-value-forms-arr (TAVar x₁) ()
  canonical-value-forms-arr (TALam _ wt) VLam = _ , _ , refl , wt
  canonical-value-forms-arr (TAAp wt wt₁) ()
  canonical-value-forms-arr (TAEHole x x₁) ()
  canonical-value-forms-arr (TANEHole x wt x₁) ()
  canonical-value-forms-arr (TACast wt x) ()
  canonical-value-forms-arr (TAFailedCast x x₁ x₂ x₃) ()

  -- this argues (somewhat informally, because you still have to inspect
  -- the types of the theorems above and manually verify this property)
  -- that we didn't miss any cases above; this intentionally will make this
  -- file fail to typecheck if we added more types, hopefully forcing us to
  -- remember to add canonical forms lemmas as appropriate
  canonical-value-forms-coverage1 : ∀{Δ d τ} →
                                   Δ , ∅ ⊢ d :: τ →
                                   d val →
                                   τ ≠ b →
                                   ((τ1 : htyp) (τ2 : htyp) → τ ≠ (τ1 ==> τ2)) →
                                   ⊥
  canonical-value-forms-coverage1 TAConst VConst = λ z _ → z refl
  canonical-value-forms-coverage1 (TAVar x₁) ()
  canonical-value-forms-coverage1 (TALam _ wt) VLam = λ _ z → z _ _ refl
  canonical-value-forms-coverage1 (TAAp wt wt₁) ()
  canonical-value-forms-coverage1 (TAEHole x x₁) ()
  canonical-value-forms-coverage1 (TANEHole x wt x₁) ()
  canonical-value-forms-coverage1 (TACast wt x) ()
  canonical-value-forms-coverage1 (TAFailedCast wt x x₁ x₂) ()

  canonical-value-forms-coverage2 : ∀{Δ d} →
                                   Δ , ∅ ⊢ d :: ⦇-⦈ →
                                   d val →
                                   ⊥
  canonical-value-forms-coverage2 (TAVar x₁) ()
  canonical-value-forms-coverage2 (TAAp wt wt₁) ()
  canonical-value-forms-coverage2 (TAEHole x x₁) ()
  canonical-value-forms-coverage2 (TANEHole x wt x₁) ()
  canonical-value-forms-coverage2 (TACast wt x) ()
  canonical-value-forms-coverage2 (TAFailedCast wt x x₁ x₂) ()

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


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

open import Agda.Builtin.Equality

data Unit : Set where
  unit : Unit

f : (x : Unit) → _ -- x ≡ x
g : (x : Unit) → x ≡ x

f unit = refl
g x = f x


text:
open import Level
open import Ordinals
module generic-filter {n : Level } (O : Ordinals {n})   where

import filter
open import zf
open import logic
-- open import partfunc {n} O
import OD

open import Relation.Nullary
open import Relation.Binary
open import Data.Empty
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
import BAlgbra

open BAlgbra O

open inOrdinal O
open OD O
open OD.OD
open ODAxiom odAxiom
import OrdUtil
import ODUtil
open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
open OrdUtil O
open ODUtil O

import ODC

open filter O

open _∧_
open _∨_
open Bool

open HOD

-------
--    the set of finite partial functions from ω to 2
--
--

open import Data.List hiding (filter)
open import Data.Maybe

import OPair
open OPair O

ODSuc : (y : HOD) → infinite ∋ y → HOD
ODSuc y lt = Union (y , (y , y))

data Hω2 :  (i : Nat) ( x : Ordinal  ) → Set n where
  hφ :  Hω2 0 o∅
  h0 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
    Hω2 (Suc i) (& (Union ((< nat→ω i , nat→ω 0 >) ,  * x )))
  h1 : {i : Nat} {x : Ordinal  } → Hω2 i x  →
    Hω2 (Suc i) (& (Union ((< nat→ω i , nat→ω 1 >) ,  * x )))
  he : {i : Nat} {x : Ordinal  } → Hω2 i x  →
    Hω2 (Suc i) x

record  Hω2r (x : Ordinal) : Set n where
  field
    count : Nat
    hω2 : Hω2 count x

open Hω2r

HODω2 :  HOD
HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where
    P  : (i j : Nat) (x : Ordinal ) → HOD
    P  i j x = ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , * x
    nat1 : (i : Nat) (x : Ordinal) → & (nat→ω i) o< next x
    nat1 i x =  next< nexto∅ ( <odmax infinite (ω∋nat→ω {i}))
    lemma1 : (i j : Nat) (x : Ordinal ) → osuc (& (P i j x)) o< next x
    lemma1 i j x = osuc<nx (pair-<xy (pair-<xy (pair-<xy (nat1 i x) (nat1 i x) ) (pair-<xy (nat1 i x) (nat1 j x) ) )
         (subst (λ k → k o< next x) (sym &iso) x<nx ))
    lemma : (i j : Nat) (x : Ordinal ) → & (Union (P i j x)) o< next x
    lemma i j x = next< (lemma1 i j x ) ho<
    odmax0 :  {y : Ordinal} → Hω2r y → y o< next o∅
    odmax0 {y} r with hω2 r
    ... | hφ = x<nx
    ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma i 0 x)
    ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma i 1 x)
    ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx

3→Hω2 : List (Maybe Two) → HOD
3→Hω2 t = list→hod t 0 where
   list→hod : List (Maybe Two) → Nat → HOD
   list→hod [] _ = od∅
   list→hod (just i0 ∷ t) i = Union (< nat→ω i , nat→ω 0 > , ( list→hod t (Suc i) ))
   list→hod (just i1 ∷ t) i = Union (< nat→ω i , nat→ω 1 > , ( list→hod t (Suc i) ))
   list→hod (nothing ∷ t) i = list→hod t (Suc i )

Hω2→3 : (x :  HOD) → HODω2 ∋ x → List (Maybe Two)
Hω2→3 x = lemma where
   lemma : { y : Ordinal } →  Hω2r y → List (Maybe Two)
   lemma record { count = 0 ; hω2 = hφ } = []
   lemma record { count = (Suc i) ; hω2 = (h0 hω3) } = just i0 ∷ lemma record { count = i ; hω2 =  hω3 }
   lemma record { count = (Suc i) ; hω2 = (h1 hω3) } = just i1 ∷ lemma record { count = i ; hω2 =  hω3 }
   lemma record { count = (Suc i) ; hω2 = (he hω3) } = nothing ∷ lemma record { count = i ; hω2 =  hω3 }

ω→2 : HOD
ω→2 = Power infinite

ω→2f : (x : HOD) → ω→2 ∋ x → Nat → Two
ω→2f x lt n with ODC.∋-p O x (nat→ω n)
ω→2f x lt n | yes p = i1
ω→2f x lt n | no ¬p = i0

fω→2-sel : ( f : Nat → Two ) (x : HOD) → Set n
fω→2-sel f x = (infinite ∋ x) ∧ ( (lt : odef infinite (&  x) ) → f (ω→nat x lt) ≡ i1 )

fω→2 : (Nat → Two) → HOD
fω→2 f = Select infinite (fω→2-sel f)

open _==_

import Axiom.Extensionality.Propositional
postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m

ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f
ω2∋f f = power← infinite (fω→2 f) (λ {x} lt →  proj1 ((proj2 (selection {fω→2-sel f} {infinite} )) lt))

ω→2f≡i1 : (X i : HOD) → (iω : infinite ∋ i) → (lt : ω→2 ∋ X ) → ω→2f X lt (ω→nat i iω)  ≡ i1 → X ∋ i
ω→2f≡i1 X i iω lt eq with ODC.∋-p O X (nat→ω (ω→nat i iω))
ω→2f≡i1 X i iω lt eq | yes p = subst (λ k → X ∋ k ) (nat→ω-iso iω) p

open _⊆_

-- someday ...
-- postulate
--    ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt )  =h= X
--    fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2∋f f) ≡ f

record CountableOrdinal : Set (suc (suc n)) where
   field
       ctl→ : Nat → Ordinal
       ctl← : Ordinal → Nat
       ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x
       ctl-iso← : { x : Nat }  → ctl← (ctl→ x ) ≡ x

record CountableHOD : Set (suc (suc n)) where
   field
       mhod : HOD
       mtl→ : Nat → Ordinal
       mtl→∈P : (i : Nat) → odef mhod (mtl→ i)
       mtl← : (x : Ordinal) → odef mhod x → Nat
       mtl-iso→ : { x : Ordinal } → (lt : odef mhod x ) → mtl→ (mtl← x lt ) ≡ x
       mtl-iso← : { x : Nat }  → mtl← (mtl→ x ) (mtl→∈P x) ≡ x

open CountableOrdinal
open CountableHOD

----
--   a(n) ∈ M
--   ∃ q ∈ Power P → q ∈ a(n) ∧ p(n) ⊆ q
--
PGHOD :  (i : Nat) → (C : CountableOrdinal) → (P : HOD) → (p : Ordinal) → HOD
PGHOD i C P p = record { od = record { def = λ x  →
       odef (Power P) x ∧ odef (* (ctl→ C i)) x  ∧  ( (y : Ordinal ) → odef (* p) y →  odef (* x) y ) }
   ; odmax = odmax (Power P)  ; <odmax = λ {y} lt → <odmax (Power P) (proj1 lt) }

---
--   p(n+1) = if PGHOD n qn otherwise p(n)
--
next-p :  (C : CountableOrdinal) (P : HOD ) (i : Nat) → (p : Ordinal) → Ordinal
next-p C P i p with is-o∅  ( & (PGHOD i C P p))
next-p C P i p | yes y = p
next-p C P i p | no not = & (ODC.minimal O (PGHOD i C P p ) (λ eq → not (=od∅→≡o∅ eq)))  -- axiom of choice

---
--  ascendant search on p(n)
--
find-p :  (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x : Ordinal) → Ordinal
find-p C P Zero x = x
find-p C P (Suc i) x = find-p C P i ( next-p C P i x )

---
-- G = { r ∈ Power P | ∃ n → r ⊆ p(n) }
--
record PDN  (C : CountableOrdinal) (P : HOD ) (x : Ordinal) : Set n where
   field
       gr : Nat
       pn<gr : (y : Ordinal) → odef (* x) y → odef (* (find-p C P gr o∅)) y
       x∈PP  : odef (Power P) x

open PDN

---
-- G as a HOD
--
PDHOD :  (C : CountableOrdinal) → (P : HOD ) → HOD
PDHOD C P = record { od = record { def = λ x →  PDN C P x }
    ; odmax = odmax (Power P) ; <odmax = λ {y} lt → <odmax (Power P) {y} (PDN.x∈PP lt)  }

open PDN

----
--  Generic Filter on Power P for HOD's Countable Ordinal (G ⊆ Power P ≡ G i.e. Nat → P → Set )
--
--  p 0 ≡ ∅
--  p (suc n) = if ∃ q ∈ * ( ctl→ n ) ∧ p n ⊆ q → q  (axiom of choice)
---             else p n

P∅ : {P : HOD} → odef (Power P) o∅
P∅ {P} =  subst (λ k → odef (Power P) k ) ord-od∅ (lemma o∅  o∅≡od∅) where
    lemma : (x : Ordinal ) → * x ≡ od∅ → odef (Power P) (& od∅)
    lemma x eq = power← P od∅  (λ {x} lt → ⊥-elim (¬x<0 lt ))
x<y→∋ : {x y : Ordinal} → odef (* x) y → * x ∋ * y
x<y→∋ {x} {y} lt = subst (λ k → odef (* x) k ) (sym &iso) lt

P-GenericFilter : (C : CountableOrdinal) → (P : HOD ) → GenericFilter P
P-GenericFilter C P = record {
      genf = record { filter = PDHOD C P ; f⊆PL =  f⊆PL ; filter1 = {!!} ; filter2 = {!!} }
    ; generic = λ D → {!!}
   } where
        find-p-⊆P : (C : CountableOrdinal) (P : HOD ) (i : Nat) → (x y : Ordinal)  → odef (Power P) x → odef (* (find-p C P i x)) y → odef P y
        find-p-⊆P C P Zero x y Px Py = subst (λ k → odef P k ) &iso
            ( incl (ODC.power→⊆ O P (* x) (d→∋ (Power P)  Px)) (x<y→∋ Py))
        find-p-⊆P C P (Suc i) x y Px Py = find-p-⊆P C P i (next-p C P i x)  y {!!} {!!}
        f⊆PL :  PDHOD C P ⊆ Power P
        f⊆PL = record { incl = λ {x} lt → power← P x (λ {y} y<x →
             find-p-⊆P C P (gr lt) o∅ (& y) P∅ (pn<gr lt (& y) (subst (λ k → odef k (& y)) (sym *iso) y<x))) }

open GenericFilter
open Filter

record Incompatible  (P : HOD ) : Set (suc (suc n)) where
   field
      except : HOD → ( HOD ∧ HOD )
      incompatible : { p : HOD } →  Power P ∋ p  →  Power P ∋ proj1 (except p )  →  Power P ∋ proj2 (except p )
          → ( p ⊆ proj1 (except p)  ) ∧ ( p ⊆ proj2 (except p)  )
          → ∀ ( r : HOD ) →  Power P ∋ r → ¬ (( proj1 (except p)  ⊆ r ) ∧ ( proj2 (except p)  ⊆ r ))

lemma725 : (M : CountableHOD ) (C : CountableOrdinal) (P : HOD ) →  mhod M ∋ Power P
    →  Incompatible P → ¬ ( mhod M ∋ filter ( genf ( P-GenericFilter C P )))
lemma725 = {!!}

lemma725-1 :   Incompatible HODω2
lemma725-1 = {!!}

lemma726 :  (C : CountableOrdinal) (P : HOD )
    →  Union ( filter ( genf ( P-GenericFilter C HODω2 ))) =h= ω→2
lemma726 = {!!}

--
--   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
--
--   W (ω , H ( ω , 2 )) = { p ∈ ( Nat → H (ω , 2) ) |  { i ∈ Nat → p i ≠ i1 } is finite }
--

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


text:
-- Andreas, 2015-07-13  Better parse errors for illegal type signatures

A with B : Set


text:
-- You are not allowed to export the same name twice from a
-- module. However, if the name is only exported once, ambiguity
-- is allowed.
module Issue154 where

module A where
  postulate X : Set

module B where
  postulate X : Set

  module C where
    open A public
    -- X is ambiguous here, but only exported once from C

module D where
  private postulate X : Set
  open A public
  -- same here

module E where
  postulate X : Set
  open A
  -- and here

module F where
  open A public
  open D public
  -- in this case there is no ambiguity, A.X and D.X refer
  -- to the same entity (A.X)

module G where
  open B public

module H where
  open G public
  open B public
  -- same as F but for modules

postulate
  test : A.X → B.X → B.C.X → D.X → E.X → F.X → G.X → H.X


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.NatSolver.NatExpression where

open import Cubical.Foundations.Prelude

open import Cubical.Data.FinData
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order using (zero-≤)
open import Cubical.Data.Vec.Base

infixl 6 _+'_
infixl 7 _·'_

-- Expression in a ring on A with n variables
data Expr (n : ℕ) : Type ℓ-zero where
  K : ℕ → Expr n
  ∣ : Fin n → Expr n
  _+'_ : Expr n → Expr n → Expr n
  _·'_ : Expr n → Expr n → Expr n

module Eval where
  open import Cubical.Data.Vec

  ⟦_⟧ : ∀ {n} → Expr n → Vec ℕ n → ℕ
  ⟦ K r ⟧ v = r
  ⟦ ∣ k ⟧ v = lookup k v
  ⟦ x +' y ⟧ v =  ⟦ x ⟧ v + ⟦ y ⟧ v
  ⟦ x ·' y ⟧ v = ⟦ x ⟧ v · ⟦ y ⟧ v

max_stars_repo_name: FernandoLarrain/cubical


text:
{-# OPTIONS --safe #-}
module Cubical.Relation.Nullary.DecidableEq where

open import Cubical.Relation.Nullary.Properties
  using (Dec→Stable; Discrete→isSet) public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
module Listy where

open import Measure
open import Data.List as List using (List; []; _∷_)
open import Data.Product using (_,_; _×_; proj₁; proj₂)
open import Data.Nat as ℕ using (ℕ; suc; zero)

open import Function

record Prob (A : Set) : Set where
  constructor weighted
  field
    runProb : List (A × ℙ)

open Prob

open import Category.Monad

monad : RawMonad Prob
monad = record
    { return = λ x → weighted ((x , fromNat 1) ∷ [])
    ; _>>=_  = bind
    }
  where
  import Data.List.Categorical
  open RawMonad Data.List.Categorical.monad
  bind : {A B : Set} → Prob A → (A → Prob B) → Prob B
  bind xs f = weighted do
    (x , xp) ← runProb xs
    (y , yp) ← runProb (f x)
    return (y , xp * yp)

support : {A : Set} → Prob A → List A
support = List.map proj₁ ∘ runProb

expect : {A : Set} → (A → ℙ) → Prob A → ℙ
expect p = List.foldl (λ ys y → ys + (p (proj₁ y) * (proj₂ y)) ) (fromNat 0) ∘ runProb

open import Data.Bool using (Bool; if_then_else_)

probOf : {A : Set} → (A → Bool) → Prob A → ℙ
probOf p = expect (λ x → if p x then fromNat 1 else fromNat 0)

uniform : {A : Set} → List A → Prob A
uniform [] = weighted []
uniform (x ∷ xs) = weighted (List.map (flip _,_ p) (x ∷ xs))
  where
  p : ℙ
  p = 1 ?÷ (suc (List.length xs))

open import Data.Fin as Fin using (Fin)

enumerate : (n : ℕ) → List (Fin n)
enumerate zero = []
enumerate (suc n) = Fin.zero ∷ List.map Fin.suc (enumerate n)

module Die where
  die : Prob (Fin 6)
  die = uniform (enumerate 6)

  open RawMonad monad

  pairadice : Prob ℕ
  pairadice = do
    x ← die
    y ← die
    return (suc (Fin.toℕ x) ℕ.+ suc (Fin.toℕ y))

open import Data.String using (String)
open import Relation.Nullary.Decidable using (⌊_⌋)

example : String
example = show (probOf (λ x → ⌊ x ℕ.≟ 7 ⌋) Die.pairadice)

max_stars_repo_name: oisdk/prob-presentation

max_issues_repo_name: oisdk/prob-presentation

max_forks_repo_name: oisdk/prob-presentation


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

module FRP.JS.Demo.Hello where

main : ∀ {w} → ⟦ Beh (DOM w) ⟧
main = text ["Hello, world."]

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
module Luau.TypeSaturation where

open import Luau.Type using (Type; _⇒_; _∩_; _∪_)
open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_)

-- So, there's a problem with overloaded functions
-- (of the form (S_1 ⇒ T_1) ∩⋯∩ (S_n ⇒ T_n))
-- which is that it's not good enough to compare them
-- for subtyping by comparing all of their overloads.

-- For example (nil → nil) is a subtype of (number? → number?) ∩ (string? → string?)
-- but not a subtype of any of its overloads.

-- To fix this, we adapt the semantic subtyping algorithm for
-- function types, given in
-- https://www.irif.fr/~gc/papers/covcon-again.pdf and
-- https://pnwamk.github.io/sst-tutorial/

-- A function type is *intersection-saturated* if for any overloads
-- (S₁ ⇒ T₁) and (S₂ ⇒ T₂), there exists an overload which is a subtype
-- of ((S₁ ∩ S₂) ⇒ (T₁ ∩ T₂)).

-- A function type is *union-saturated* if for any overloads
-- (S₁ ⇒ T₁) and (S₂ ⇒ T₂), there exists an overload which is a subtype
-- of ((S₁ ∪ S₂) ⇒ (T₁ ∪ T₂)).

-- A function type is *saturated* if it is both intersection- and
-- union-saturated.

-- For example (number? → number?) ∩ (string? → string?)
-- is not saturated, but (number? → number?) ∩ (string? → string?) ∩ (nil → nil) ∩ ((number ∪ string)? → (number ∪ string)?)
-- is.

-- Saturated function types have the nice property that they can ber
-- compared by just comparing their overloads: F <: G whenever for any
-- overload of G, there is an overload os F which is a subtype of it.

-- Forunately every function type can be saturated!
_⋓_ : Type → Type → Type
(S₁ ⇒ T₁) ⋓ (S₂ ⇒ T₂) = (S₁ ∪ⁿ S₂) ⇒ (T₁ ∪ⁿ T₂)
(F₁ ∩ G₁) ⋓ F₂ = (F₁ ⋓ F₂) ∩ (G₁ ⋓ F₂)
F₁ ⋓ (F₂ ∩ G₂) = (F₁ ⋓ F₂) ∩ (F₁ ⋓ G₂)
F ⋓ G = F ∩ G

_⋒_ : Type → Type → Type
(S₁ ⇒ T₁) ⋒ (S₂ ⇒ T₂) = (S₁ ∩ⁿ S₂) ⇒ (T₁ ∩ⁿ T₂)
(F₁ ∩ G₁) ⋒ F₂ = (F₁ ⋒ F₂) ∩ (G₁ ⋒ F₂)
F₁ ⋒ (F₂ ∩ G₂) = (F₁ ⋒ F₂) ∩ (F₁ ⋒ G₂)
F ⋒ G = F ∩ G

_∩ᵘ_ : Type → Type → Type
F ∩ᵘ G = (F ∩ G) ∩ (F ⋓ G)

_∩ⁱ_ : Type → Type → Type
F ∩ⁱ G = (F ∩ G) ∩ (F ⋒ G)

∪-saturate : Type → Type
∪-saturate (F ∩ G) = (∪-saturate F ∩ᵘ ∪-saturate G)
∪-saturate F = F

∩-saturate : Type → Type
∩-saturate (F ∩ G) = (∩-saturate F ∩ⁱ ∩-saturate G)
∩-saturate F = F

saturate : Type → Type
saturate F = ∪-saturate (∩-saturate F)

max_stars_repo_name: Libertus-Lab/luau

max_issues_repo_name: sthagen/Roblox-luau

max_forks_repo_name: sthagen/Roblox-luau


text:
module Base.Change.Products where

open import Relation.Binary.PropositionalEquality
open import Level

open import Base.Change.Algebra
open import Base.Change.Equivalence
open import Base.Change.Equivalence.Realizers

-- Also try defining sectioned change structures on the positives halves of
-- groups? Or on arbitrary subsets?

-- Restriction: we pair sets on the same level (because right now everything
-- else would risk getting in the way).
module ProductChanges ℓ {A B : Set ℓ} {{CA : ChangeAlgebra A}} {{CB : ChangeAlgebra B}} where
  -- Avoid having to specify A and B all the time; they'd often be ambiguous
  -- otherwise.
  import Data.Product as DP
  open DP.Σ {A = A} {B = λ _ → B}
  open DP using (_×_; _,_)

  -- The simplest possible definition of changes for products.

  PChange : A × B → Set ℓ
  PChange (a , b) = Δ a × Δ b

  -- An interesting alternative definition allows omitting the nil change of a
  -- component when that nil change can be computed from the type. For instance, the nil change for integers is always the same.

  -- However, the nil change for function isn't always the same (unless we
  -- defunctionalize them first), so nil changes for functions can't be omitted.

  _⊕_ : (v : A × B) → PChange v → A × B
  _⊕_ (a , b) (da , db) = a ⊞ da , b ⊞ db
  _⊝_ : A × B → (v : A × B) → PChange v
  _⊝_ (aNew , bNew) (a , b) = aNew ⊟ a , bNew ⊟ b

  p-nil : (v : A × B) → PChange v
  p-nil (a , b) = (nil a , nil b)

  p-update-diff : (u v : A × B) → v ⊕ (u ⊝ v) ≡ u
  p-update-diff (ua , ub) (va , vb) =
    let u = (ua , ub)
        v = (va , vb)
    in
      begin
        v ⊕ (u ⊝ v)
      ≡⟨⟩
        (va ⊞ (ua ⊟ va) , vb ⊞ (ub ⊟ vb))
        --v ⊕ ((ua ⊟ va , ub ⊟ vb))
      ≡⟨ cong₂ _,_ (update-diff ua va) (update-diff ub vb)⟩
        (ua , ub)
      ≡⟨⟩
        u
      ∎
    where
      open ≡-Reasoning

  p-update-nil : (v : A × B) → v ⊕ (p-nil v) ≡ v
  p-update-nil (a , b) =
    let v = (a , b)
    in
      begin
        v ⊕ (p-nil v)
      ≡⟨⟩
        (a ⊞ nil a , b ⊞ nil b)
      ≡⟨ cong₂ _,_ (update-nil a) (update-nil b)⟩
         (a , b)
      ≡⟨⟩
        v
      ∎
    where
      open ≡-Reasoning

  instance
    changeAlgebraProducts : ChangeAlgebra (A × B)
    changeAlgebraProducts = record
      { Change = PChange
      ; update = _⊕_
      ; diff = _⊝_
      ; nil = p-nil
      ; isChangeAlgebra = record
        { update-diff = p-update-diff
        ; update-nil = p-update-nil
        }
      }

  --
  -- Derivatives of introductions and elimination forms for products.
  --
  -- For each one define a naive derivative using nil, write a hand-optimized *realizer* for an efficient derivative, and prove they're equivalent.
  --
  proj₁′ : Δ proj₁
  proj₁′ = nil proj₁

  proj₁′-realizer : (v : A × B) → Δ v → Δ (proj₁ v)
  proj₁′-realizer (a , b) (da , db) = da

  proj₁′-realizer-correct : ∀ (p : A × B) (dp : Δ p) → apply proj₁′ p dp ≙₍ proj₁ p ₎ proj₁′-realizer p dp
  proj₁′-realizer-correct (a , b) (da , db) = diff-update {x = a} {dx = da}

  proj₁′Derivative : IsDerivative proj₁ proj₁′-realizer
  -- Implementation note: we do not need to pattern match on v and dv because
  -- they are records, hence Agda knows that pattern matching on records cannot
  -- fail. Technically, the required feature is the eta-rule on records.
  proj₁′Derivative v dv = refl

  -- An extended explanation.
  proj₁′Derivative₁ : IsDerivative proj₁ proj₁′-realizer
  proj₁′Derivative₁ (a , b) (da , db) =
    let v  = (a  , b)
        dv = (da , db)
    in
      begin
        proj₁ v ⊞ proj₁′-realizer v dv
      ≡⟨⟩
        a ⊞ da
      ≡⟨⟩
        proj₁ (v ⊞ dv)
      ∎
    where
      open ≡-Reasoning

  proj₁′-faster-w-proof : equiv-raw-change-to-change-ResType proj₁ proj₁′-realizer
  proj₁′-faster-w-proof = equiv-raw-change-to-change proj₁ proj₁′ proj₁′-realizer proj₁′-realizer-correct
  proj₁′-faster : Δ proj₁
  proj₁′-faster = DP.proj₁ proj₁′-faster-w-proof

  -- Same for the second extractor.
  proj₂′-realizer : (v : A × B) → Δ v → Δ (proj₂ v)
  proj₂′-realizer (a , b) (da , db) = db

  proj₂′ : Δ proj₂
  proj₂′ = nil proj₂

  proj₂′-realizer-correct : ∀ p (dp : Δ p) → apply proj₂′ p dp ≙₍ proj₂ p ₎ proj₂′-realizer p dp
  proj₂′-realizer-correct (a , b) (da , db) = diff-update

  proj₂′Derivative : IsDerivative proj₂ proj₂′-realizer
  proj₂′Derivative v dv = refl

  proj₂′-faster-w-proof : equiv-raw-change-to-change-ResType proj₂ proj₂′-realizer
  proj₂′-faster-w-proof = equiv-raw-change-to-change proj₂ proj₂′ proj₂′-realizer proj₂′-realizer-correct
  proj₂′-faster : Δ proj₂
  proj₂′-faster = DP.proj₁ proj₂′-faster-w-proof

  -- Morally, the following is a change:
  -- What one could wrongly expect to be the derivative of the constructor:
  _,_′-realizer : (a : A) → (da : Δ a) → (b : B) → (db : Δ b) → Δ (a , b)
  _,_′-realizer a da b db = da , db

  -- That has the correct behavior, in a sense, and it would be in the
  -- subset-based formalization in the paper.
  --
  -- But the above is not even a change, because it does not contain a proof of
  -- its own validity, and because after application it does not contain a
  -- proof.
  --
  -- However, the above is (morally) a "realizer" of the actual change, since it
  -- only represents its computational behavior, not its proof manipulation.

  -- Hence, we need to do some additional work.

  _,_′ : Δ (_,_ {A = A} {B = λ _ → B})
  _,_′ = _,_ ⊟ _,_
  _,_′-realizer-correct : ∀ a da b db → apply (apply _,_′ a da) b db ≙₍ a , b ₎ _,_′-realizer a da b db
  _,_′-realizer-correct a da b db = doe (≙-cong₂ _,_ diff-update diff-update)

  open import Data.Product using (Σ-syntax)

  _,_′-faster-w-proof : equiv-raw-change-to-change-binary-ResType _,_ _,_′-realizer
  _,_′-faster-w-proof = equiv-raw-change-to-change-binary _,_ _,_′ _,_′-realizer _,_′-realizer-correct

  _,_′-faster : Δ (_,_ {A = A} {B = λ _ → B})
  _,_′-faster = DP.proj₁ _,_′-faster-w-proof

  -- Define specialized variant of uncurry, and derive it.
  uncurry₀ : ∀ {C : Set ℓ} → (A → B → C) → A × B → C
  uncurry₀ f (a , b) = f a b

  module _ {C : Set ℓ} {{CC : ChangeAlgebra C}} where
    uncurry₀′ : Δ uncurry₀
    uncurry₀′ = nil (uncurry₀ {C = C})

    uncurry₀′-realizer : (f : A → B → C) → Δ f → (p : A × B) → Δ p → Δ (uncurry₀ f p)
    uncurry₀′-realizer f df (a , b) (da , db) = apply (apply df a da) b db

    uncurry₀′-realizer-correct : ∀ f df p dp → apply (apply uncurry₀′ f df) p dp ≙₍ uncurry₀ f p ₎ uncurry₀′-realizer f df p dp
    uncurry₀′-realizer-correct f df (a , b) (da , db) =
      begin
        (f ⊞ df) (a ⊞ da) (b ⊞ db) ⊟ f a b
      ≙⟨ equiv-cancel-2 _ _ (incrementalization-binary f df a da b db) ⟩
        apply (apply df a da) b db
      ∎
      where
        open ≙-Reasoning
        open BinaryFunctionChanges A B C

    uncurry₀′-faster-w-proof : equiv-raw-change-to-change-binary-ResType uncurry₀ uncurry₀′-realizer
    uncurry₀′-faster-w-proof = equiv-raw-change-to-change-binary uncurry₀ uncurry₀′ uncurry₀′-realizer uncurry₀′-realizer-correct

    uncurry₀′-faster : Δ uncurry₀
    uncurry₀′-faster = DP.proj₁ uncurry₀′-faster-w-proof


text:
-- This file gives the definition of Gaussian Integers, the addition
-- and multiplication on them, and shows that they form a commutative
-- ring, and other properties. All the proofs are straightforward.

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

module GauInt.Properties where

-- imports from local.
open import GauInt.Instances
open import Instances
open import GauInt.Base using (𝔾 ; _+_i ; _ᶜ ; Re ; Im ; _+0i ; _+0i' ; 0𝔾)
open import Integer.Properties

-- imports from stdlib and Agda.
open import Level using (0ℓ)
open import Relation.Nullary using (yes; no; ¬_)
open import Relation.Binary using (DecidableEquality ; Setoid ; DecSetoid ; tri< ; tri≈ ; tri>)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Data.Product using (proj₁; proj₂; _,_ ; _×_)
open import Data.Sum using (_⊎_ ; inj₁ ; inj₂) renaming ([_,_]′ to ⊎-elim)
open import Data.Nat as Nat using (ℕ; suc; zero)
import Data.Nat.Properties as NatP
open import Data.Integer.Properties as IntP
  using (+-assoc ; +-identityˡ ; +-identityʳ ; *-identityˡ ; +-inverseˡ ; +-inverseʳ ; +-comm ; 0≤i⇒+∣i∣≡i ; +-mono-≤ ; +-mono-<-≤ ; +-mono-≤-<)
open import Data.Integer as Int
  using (ℤ ; +_ ; NonNegative ; -[1+_] ; +[1+_] ; +≤+ ; +<+ ; ∣_∣ ; 0ℤ ; +0)
import Data.Integer.Solver as IS
open IS.+-*-Solver

open import Algebra.Bundles as B
import Algebra.Morphism as Morphism
open import Algebra.Structures {A = 𝔾} _≡_
open import Function.Base using (_$_)
module 𝔾toℕ = Morphism.Definitions 𝔾 ℕ _≡_
module ℕto𝔾 = Morphism.Definitions ℕ 𝔾 _≡_

open import Algebra.Definitions (_≡_ {A = 𝔾}) using (AlmostLeftCancellative)

-- ----------------------------------------------------------------------
-- Equality

-- Injections are injective.
+0i'-injective : ∀ {a b} -> a +0i' ≡ b +0i' → a ≡ b
+0i'-injective refl = refl

+0i-injective : ∀ {m n} -> m +0i ≡ n +0i → m ≡ n
+0i-injective refl = refl

-- Decidable equality on 𝔾.
infix 4 _≟_
_≟_ : DecidableEquality 𝔾
_≟_ x@(a + b i) y@(c + d i) with  a Int.≟ c | b Int.≟ d
... | yes p  | yes q = yes (cong₂ _+_i p q)
... | yes p  | no ¬q = no (λ { refl → ¬q refl})
... | no ¬p  | hyp = no (λ { refl → ¬p refl})

≡-setoid : Setoid 0ℓ 0ℓ
≡-setoid = setoid 𝔾

≡-decSetoid : DecSetoid 0ℓ 0ℓ
≡-decSetoid = decSetoid _≟_

-- ----------------------------------------------------------------------
-- Properties of _+_

-- Associativity of addition.
assoc-+ : ∀ (x y z : 𝔾) -> ((x + y) + z) ≡ (x + (y + z))
assoc-+ x@(a + b i) y@(c + d i) z@(e + f i) = begin
  (((a + b i) + (c + d i)) + (e + f i)) ≡⟨ refl ⟩
  ((a + c + e) + (b + d + f) i) ≡⟨ cong₂ _+_i (+-assoc a c e) (+-assoc b d f) ⟩
  ((a + (c + e)) + (b + (d + f)) i) ≡⟨ refl ⟩
  (x + (y + z)) ∎

-- Left additive identity.
leftId-+ : ∀ (x : 𝔾) -> 0# + x ≡ x
leftId-+ x@(a + b i) = begin
  (0# + 0# i) + (a + b i) ≡⟨ refl ⟩
  -- cannot parse if remove the outer layer parenthese.
  ((0# + a) + (0# + b) i) ≡⟨ cong₂  _+_i (+-identityˡ a) (+-identityˡ b) ⟩
  (a + b i) ∎

-- Right additive identity.
rightId-+ : ∀ (x : 𝔾) -> (x + 0#) ≡ x
rightId-+ x@(a + b i) = begin
  (a + b i) + (0# + 0# i)  ≡⟨ refl ⟩
  ((a + 0#) + (b + 0#) i) ≡⟨ cong₂  _+_i (+-identityʳ a) (+-identityʳ b) ⟩
  (a + b i) ∎

-- Left additive inverse.
leftInv-+ : ∀ (x : 𝔾) -> (- x) + x ≡ 0#
leftInv-+ x@(a + b i) = cong₂ _+_i (+-inverseˡ a) (+-inverseˡ b)

-- Right additive inverse.
rightInv-+ : ∀ (x : 𝔾) -> x + (- x) ≡ 0#
rightInv-+ x@(a + b i) = cong₂ _+_i (+-inverseʳ a) (+-inverseʳ b)

-- Addition is commutative.
comm-+ : (x y : 𝔾) → (x + y) ≡ (y + x)
comm-+ x@(a + b i) y@(c + d i) = cong₂ _+_i (+-comm a c) (+-comm b d)

-- ----------------------------------------------------------------------
-- Structures for addition

+-isMagma : IsMagma _+_
+-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = cong₂ _+_
  }

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

+-isCommutativeSemigroup : IsCommutativeSemigroup _+_
+-isCommutativeSemigroup = record
  { isSemigroup = +-isSemigroup
  ; comm        = comm-+
  }

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

+-0-isCommutativeMonoid : IsCommutativeMonoid _+_ 0#
+-0-isCommutativeMonoid = record
  { isMonoid = +-0-isMonoid
  ; comm     = comm-+
  }

+-0-isGroup : IsGroup _+_ 0# (-_)
+-0-isGroup = record
  { isMonoid = +-0-isMonoid
  ; inverse  = leftInv-+ , rightInv-+
  ; ⁻¹-cong  = cong (-_)
  }

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

-- ----------------------------------------------------------------------
-- Bundles for addition

+-magma : Magma 0ℓ 0ℓ
+-magma = record
  { isMagma = +-isMagma
  }

+-semigroup : Semigroup 0ℓ 0ℓ
+-semigroup = record
  { isSemigroup = +-isSemigroup
  }

+-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
+-commutativeSemigroup = record
  { isCommutativeSemigroup = +-isCommutativeSemigroup
  }

+-0-monoid : Monoid 0ℓ 0ℓ
+-0-monoid = record
  { isMonoid = +-0-isMonoid
  }

+-0-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
+-0-commutativeMonoid = record
  { isCommutativeMonoid = +-0-isCommutativeMonoid
  }

+-0-abelianGroup : AbelianGroup 0ℓ 0ℓ
+-0-abelianGroup = record
  { isAbelianGroup = +-isAbelianGroup
  }

-- ----------------------------------------------------------------------
-- Properties of multiplication

-- Associativity of multiplication.
assoc-* : ∀ (x y z : 𝔾) -> ((x * y) * z) ≡ (x * (y * z))
assoc-* x@(a + b i) y@(c + d i) z@(e + f i) = begin
  (((a + b i) * (c + d i)) * (e + f i)) ≡⟨ refl ⟩
  ((a * c - b * d) + (a * d + b * c) i)  * (e + f i) ≡⟨ refl ⟩
  ((a * c - b * d) * e - (a * d + b * c) * f) + ((a * c - b * d) * f + (a * d + b * c) * e) i ≡⟨ cong₂ _+_i (let _*_ = _:*_ in let _+_ = _:+_ in let _-_ = _:-_ in (solve 6 (\ a b c d e f -> (((a * c) - (b * d)) * e) - (((a * d) + (b * c)) * f) := (a * ((c * e) - (d * f))) - (b * ((c * f) + (d * e)))) refl a b c d e f)) ((let _*_ = _:*_ in let _+_ = _:+_ in let _-_ = _:-_ in
   (solve 6 (\ a b c d e f -> (((a * c) - (b * d)) * f) + (((a * d) + (b * c)) * e) := (a * ((c * f) + (d * e))) + (b * ((c * e) - (d * f)))) refl a b c d e f))) ⟩
  ((a * (c * e - d * f) - b * (c * f + d * e) ) + (a * (c * f + d * e) + b * (c * e - d * f)) i ) ≡⟨ refl ⟩
  ((a + b i) * ((c * e - d * f) + (c * f + d * e) i) ) ≡⟨ refl ⟩
  (x * (y * z)) ∎

-- Left multiplicative identity.
leftId-* : ∀ (x : 𝔾) -> (1# * x) ≡ x
leftId-* x@(a + b i) = begin
  (1# + 0# i) * (a + b i) ≡⟨ refl ⟩
  ((1# * a - 0# * b) + (1# * b + 0# * a) i) ≡⟨ cong₂ _+_i (let _*_ = _:*_ in let _-_ = _:-_ in (solve 2 (\ a b -> (con 1# * a) - (con 0# * b) := con 1# * a) refl a b)) ( (let _*_ = _:*_ in let _+_ = _:+_ in (solve 2 (\ a b -> (con 1# * b) + (con 0# * a) := con 1# * b) refl a b)))  ⟩
  ((1# * a) + (1# * b) i) ≡⟨ cong₂ _+_i (*-identityˡ a) (*-identityˡ b)  ⟩
  (a + b i) ∎

-- Right multiplicative identity.
rightId-* : ∀ (x : 𝔾) -> (x * 1#) ≡ x
rightId-* x@(a + b i) = begin
  (a + b i) * (1# + 0# i)  ≡⟨ refl ⟩
  (( a * 1# - b * 0#) + ( a * 0#  + b * 1# ) i) ≡⟨ cong₂ _+_i ((let _*_ = _:*_ in let _-_ = _:-_ in (solve 2 (\ a b -> (a * con 1# ) - (b * con 0# ) := con 1# * a) refl a b))) ((let _*_ = _:*_ in let _+_ = _:+_ in (solve 2 (\ a b -> (a * con 0#) + (b * con 1# )   := con 1# * b) refl a b)))   ⟩
  ((1# * a) + (1# * b) i) ≡⟨ cong₂ _+_i (*-identityˡ a) (*-identityˡ b)  ⟩
  (a + b i) ∎

-- Zero leftly times any number is zero.
leftZero : ∀ x -> (0# + 0# i) * x ≡ (0# + 0# i)
leftZero x@(a + b i)  = begin
  (0# + 0# i) * (a + b i) ≡⟨ refl ⟩
  (0#  * a - 0#  * b) +   (0#  * a - 0#  * b) i  ≡⟨ refl ⟩
  0# + 0# i ∎

-- Zero rightly times any number is zero.
rightZero : ∀ x -> x * (0# + 0# i) ≡ (0# + 0# i)
rightZero x@(a + b i)  = begin
  (a + b i) * (0# + 0# i)  ≡⟨ refl  ⟩
  (a * 0#  - b * 0# ) + (a * 0#  + b *  0# ) i  ≡⟨ cong₂ _+_i ((let _*_ = _:*_ in let _+_ = _:+_ in let _-_ = _:-_ in  (solve 2 (\ a b -> (a * con 0#) - (b * con 0# ) := con 0#) refl a b))) ((let _*_ = _:*_ in let _+_ = _:+_ in let _-_ = _:-_ in  (solve 2 (\ a b -> (a * con 0#) + (b * con 0# ) := con 0#) refl a b)))   ⟩
  0# + 0# i ∎

-- Left multiplication is distributive over addition.
*-DistributesOver-+ˡ : ∀ (x y z : 𝔾) -> (x * (y + z)) ≡ ((x * y) + (x * z))
*-DistributesOver-+ˡ x@(a + b i) y@(c + d i) z@(e + f i) = begin
  x * (y + z) ≡⟨ refl ⟩
  (a * (c + e) - b * (d + f) + (a * (d + f) + b * (c + e)) i) ≡⟨ cong₂ _+_i ((let _*_ = _:*_ in let _+_ = _:+_ in let _-_ = _:-_ in (solve 6 (\ a b c d e f -> (a * (c + e)) - (b * (d + f) ) := ((a * c) - (b * d)) + ((a * e) - (b * f)) ) refl a b c d e f))) ((let _*_ = _:*_ in let _+_ = _:+_ in let _-_ = _:-_ in (solve 6 (\ a b c d e f -> (a * (d + f)) + (b * (c + e) ) := ((a * d) + (b * c)) + ((a * f) + (b * e)) ) refl a b c d e f))) ⟩
  ((a * c - b * d)  + (a * e - b * f)) + ((a * d + b * c) + (a * f + b * e)) i ≡⟨ refl ⟩
  ((x * y) + (x * z)) ∎

-- Right multiplication is distributive over addition.
*-DistributesOver-+ʳ : ∀ (x y z : 𝔾) -> ((y + z) * x) ≡ (y * x) + (z * x)
*-DistributesOver-+ʳ x@(a + b i) y@(c + d i) z@(e + f i) = begin
  (y + z) * x ≡⟨ refl ⟩
  ((c + e) * a - (d + f) * b + ( (c + e) * b + (d + f) * a ) i) ≡⟨ cong₂ _+_i ((let _*_ = _:*_ in let _+_ = _:+_ in let _-_ = _:-_ in (solve 6 (\ a b c d e f -> ((c + e) * a) - ((d + f) * b ) := ((c * a ) - (d * b)) + ((e * a) - (f * b )) ) refl a b c d e f))) ((let _*_ = _:*_ in let _+_ = _:+_ in let _-_ = _:-_ in (solve 6 (\ a b c d e f -> ((c + e) * b) + ((d + f) * a ) := ((c * b ) + (d * a)) + ((e * b) + (f * a )) ) refl a b c d e f)))  ⟩
  ((c * a - d * b)  + (e * a - f * b)) + ((c * b + d * a ) + (e * b + f * a )) i ≡⟨ refl ⟩
  ((y * x) + (z * x)) ∎

-- Multiplicaton is commutative.
comm-* : ∀ (x y : 𝔾) -> x * y ≡ y * x
comm-* x@(a + b i) y@(c + d i) = begin
  x * y ≡⟨ refl ⟩
  (a * c - b * d) + (a * d + b * c) i ≡⟨ cong₂ _+_i ((let _*_ = _:*_ in let _+_ = _:+_ in let _-_ = _:-_ in (solve 4 (\ a b c d -> (a * c) - (b * d) := (c * a ) - (d * b)) refl a b c d))) ((let _*_ = _:*_ in let _+_ = _:+_ in let _-_ = _:-_ in  (solve 4 (\ a b c d -> (a * d) + (b * c) := (c * b) + (d * a)) refl a b c d)))  ⟩
  (c * a - d * b) + (c * b + d * a) i ≡⟨ refl ⟩
  (y * x) ∎

-- ----------------------------------------------------------------------
-- Structures for multiplication

*-isMagma : IsMagma _*_
*-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = cong₂ _*_
  }

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

*-isCommutativeSemigroup : IsCommutativeSemigroup _*_
*-isCommutativeSemigroup = record
  { isSemigroup = *-isSemigroup
  ; comm        = comm-*
  }

*-1-isMonoid : IsMonoid _*_ 1#
*-1-isMonoid = record
  { isSemigroup = *-isSemigroup
  ; identity    = leftId-* , rightId-*
  }

*-1-isCommutativeMonoid : IsCommutativeMonoid _*_ 1#
*-1-isCommutativeMonoid = record
  { isMonoid = *-1-isMonoid
  ; comm     = comm-*
  }

-- ----------------------------------------------------------------------
-- Structures for multiplication and addition

+-*-isSemiring : IsSemiring _+_ _*_ 0# 1#
+-*-isSemiring = record
  { isSemiringWithoutAnnihilatingZero = record
    { +-isCommutativeMonoid = +-0-isCommutativeMonoid
    ; *-isMonoid = *-1-isMonoid
    ; distrib = *-DistributesOver-+ˡ , *-DistributesOver-+ʳ
    }
  ; zero = leftZero , rightZero
  }

+-*-isCommutativeSemiring : IsCommutativeSemiring _+_ _*_ 0# 1#
+-*-isCommutativeSemiring = record
  { isSemiring = +-*-isSemiring
  ; *-comm = comm-*
  }

+-*-isRing : IsRing _+_ _*_ -_ 0# 1#
+-*-isRing = record
  { +-isAbelianGroup = +-isAbelianGroup
  ; *-isMonoid       = *-1-isMonoid
  ; distrib          = *-DistributesOver-+ˡ , *-DistributesOver-+ʳ
  ; zero             = leftZero , rightZero
  }

+-*-isCommutativeRing : IsCommutativeRing _+_ _*_ -_ 0# 1#
+-*-isCommutativeRing = record
  { isRing = +-*-isRing
  ; *-comm = comm-*
  }

------------------------------------------------------------------------
-- Bundles for multiplication

*-magma : Magma 0ℓ 0ℓ
*-magma = record
  { isMagma = *-isMagma
  }

*-semigroup : Semigroup 0ℓ 0ℓ
*-semigroup = record
  { isSemigroup = *-isSemigroup
  }

*-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
*-commutativeSemigroup = record
  { isCommutativeSemigroup = *-isCommutativeSemigroup
  }

*-1-monoid : Monoid 0ℓ 0ℓ
*-1-monoid = record
  { isMonoid = *-1-isMonoid
  }

*-1-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
*-1-commutativeMonoid = record
  { isCommutativeMonoid = *-1-isCommutativeMonoid
  }

------------------------------------------------------------------------
-- Bundles for multiplication and addition

+-*-semiring : Semiring 0ℓ 0ℓ
+-*-semiring = record
  { isSemiring = +-*-isSemiring
  }

+-*-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
+-*-commutativeSemiring = record
  { isCommutativeSemiring = +-*-isCommutativeSemiring
  }

+-*-ring : B.Ring 0ℓ 0ℓ
+-*-ring = record
  { isRing = +-*-isRing
  }

+-*-commutativeRing : CommutativeRing 0ℓ 0ℓ
+-*-commutativeRing = record
  { isCommutativeRing = +-*-isCommutativeRing
  }

-- ----------------------------------------------------------------------
-- Properties of Re and Im

-- Re x + Im x i = x
Re+Im*i : ∀ {x} -> Re x + Im x i ≡ x
Re+Im*i {x + x₁ i} = refl

-- Re (y * y ᶜ) ≡ + rank y
Re[yyᶜ]=rank : ∀ {y : 𝔾} -> Re (y * y ᶜ) ≡ + rank y
Re[yyᶜ]=rank {y@(a + b i)} = sym $ begin
  + (rank y) ≡⟨ refl ⟩
  + (rank (a + b i)) ≡⟨ refl ⟩
  + ∣ a * a + b * b ∣ ≡⟨ cong +_ (tri-eq' a b) ⟩
  + (∣ a * a ∣ + ∣ b * b ∣) ≡⟨ refl ⟩
  + ∣ a * a ∣ + + ∣ b * b ∣ ≡⟨ cong₂ _+_ (+∣a*a∣=a*a a) (+∣a*a∣=a*a b) ⟩
  a * a + b * b ≡⟨ solve 2 (\ a b -> a :* a :+ b :* b := a :* a :- b :* (:- b)) refl a b ⟩
  a * a - b * (- b) ≡⟨ refl ⟩
  Re ((a * a - b * (- b)) + 0ℤ i) ≡⟨ refl ⟩
  Re ((a * a - b * (- b)) + (a * (- b) + b * a) i) ≡⟨ refl ⟩
  Re (y * y ᶜ) ∎

-- Im y * y ᶜ = 0
Im[yyᶜ]=0 : ∀ {y : 𝔾} -> Im (y * y ᶜ) ≡ 0#
Im[yyᶜ]=0 {y@(a + b i)} = begin
  Im (y * y ᶜ) ≡⟨ refl ⟩
  Im ((a * a - b * (- b)) + (a * (- b) + b * a) i) ≡⟨ refl ⟩
  a * (- b) + b * a ≡⟨ solve 2 (\ a b -> a :* (:- b) :+ b :* a := con 0#) refl a b ⟩
  0# ∎

-- ----------------------------------------------------------------------
-- Properties of conjugation

-- Conjugation is injective.
ᶜ-injective : ∀ {x} -> x ᶜ ≡ 0# -> x ≡ 0#
ᶜ-injective {+ 0 + + 0 i} eq = refl

-- y * y ᶜ = rank y
y*yᶜ=rank : ∀ {y : 𝔾} -> y * y ᶜ ≡ rank y +0i
y*yᶜ=rank {y@(a + b i)} = begin
  y * y ᶜ ≡⟨ sym $ Re+Im*i ⟩
  Re (y * y ᶜ) + Im (y * y ᶜ) i  ≡⟨ cong₂ _+_i (Re[yyᶜ]=rank {y}) (Im[yyᶜ]=0 {y})  ⟩
  + rank y + 0# i ∎

-- ----------------------------------------------------------------------
-- Properties of rank

-- rank on 𝔾 is homomorphic in multiplication.
rank-*-commute : 𝔾toℕ.Homomorphic₂ rank _*_ Nat._*_
rank-*-commute x@(a + b i) y@(c + d i) = claim
  where
    claim : rank (x * y) ≡ rank x * rank y
    claim = begin
      rank (x * y)  ≡⟨ refl ⟩
      rank ((a * c - b * d) + (a * d + b * c) i) ≡⟨ refl ⟩
      ∣ (a * c - b * d)^2 + (a * d + b * c)^2 ∣ ≡⟨ cong ∣_∣ (solve 4 (λ a b c d → (a :* c :- b :* d) :* (a :* c :- b :* d) :+ (a :* d :+ b :* c) :* (a :* d :+ b :* c) := (a :* a :+ b :* b) :* (c :* c :+ d :* d)) refl a b c d) ⟩
      ∣ (a ^2 + b ^2) * (c ^2 + d ^2) ∣ ≡⟨ IntP.abs-*-commute ((a ^2 + b ^2)) ((c ^2 + d ^2)) ⟩
      ∣ a ^2 + b ^2 ∣ * ∣ c ^2 + d ^2 ∣ ≡⟨ refl ⟩
      rank x * rank y ∎

rank=∣Re[y*yᶜ]∣ : ∀ (x : 𝔾) -> rank x ≡ ∣ Re (x * x ᶜ) ∣
rank=∣Re[y*yᶜ]∣ x@(a + b i) = begin
  rank (a + b i) ≡⟨ refl ⟩
  ∣ a * a + b * b ∣ ≡⟨ cong ∣_∣ (solve 2 (λ a b → a :* a :+ b :* b := a :* a :- b :* (:- b)) refl a b) ⟩
  ∣ a * a - b * (- b) ∣ ≡⟨ refl ⟩
  ∣ Re ((a * a - b * (- b)) + 0ℤ i) ∣ ≡⟨ refl ⟩
  ∣ Re ((a * a - b * (- b)) + (a * (- b) + b * a) i) ∣ ≡⟨ refl ⟩
  ∣ Re (x * x ᶜ) ∣  ∎

-- rank y + 0 i = y * y ᶜ
rank+0i=y*yᶜ : ∀ {y : 𝔾} -> (rank y) +0i ≡ y * y ᶜ
rank+0i=y*yᶜ {y} = sym $ begin
  y * y ᶜ ≡⟨ sym $ Re+Im*i ⟩
  Re (y * y ᶜ) + Im (y * y ᶜ) i  ≡⟨ cong₂ _+_i (Re[yyᶜ]=rank {y}) (Im[yyᶜ]=0 {y})  ⟩
  + rank y + 0# i ∎

-- ----------------------------------------------------------------------
-- Injection preserves SemiRing Structure

+0i-+-commute : ℕto𝔾.Homomorphic₂ _+0i Nat._+_ _+_
+0i-+-commute a b = refl

+0i-*-commute : ℕto𝔾.Homomorphic₂ _+0i Nat._*_ _*_
+0i-*-commute a b rewrite NatP.*-zeroˡ a | NatP.*-zeroˡ b | NatP.*-zeroʳ a | NatP.*-zeroʳ b | sym (IntP.pos-distrib-* a b) | IntP.+-identityʳ (+ a * + b) = refl

0+0i=0 : 0 +0i ≡ 0#
0+0i=0 = refl

1+0i=1 : 1 +0i ≡ 1#
1+0i=1 = refl

-- ----------------------------------------------------------------------
-- Domain Structrue on 𝔾

-- Some auxillaries.

-- Zero is unique.
unique0 : ∀ {a b} -> (a + b i) ≡ 0# -> a ≡ 0ℤ × b ≡ 0ℤ
unique0 {.+0} {.+0} refl = refl , refl

-- Conversely, if a + bi ≠ 0 then at least one of a and b is not zero.
unique0' : ∀ {a b} -> ¬ (a + b i) ≡ 0# -> ¬ a ≡ 0ℤ ⊎ ¬ b ≡ 0ℤ
unique0' {a@(+_ zero)} {b@(+_ zero)} neq with neq refl
... | ()
unique0' {+_ zero} {+[1+ n ]} neq = inj₂ (λ ())
unique0' {+_ zero} { -[1+_] n} neq = inj₂ (λ ())
unique0' {+[1+ n ]} {b} neq = inj₁ (λ ())
unique0' { -[1+_] n} {b} neq = inj₁ (λ ())

-- Make an equation onesided.
oneside : ∀ {a b : 𝔾} -> a ≡ b -> a - b ≡ 0#
oneside {a} {b} eq rewrite eq = rightInv-+ b

-- Make an equation twosided.
twoside : ∀ {a b : 𝔾} -> a - b ≡ 0# -> a ≡ b
twoside {a} {b} eq = sym $ -‿injective $ +-inverseʳ-unique a (- b) eq
  where
    open import Algebra.Properties.Ring +-*-ring

-- Make an equation twosided, ℤ version.
twosideℤ : ∀ {a b : ℤ} -> a - b ≡ 0# -> a ≡ b
twosideℤ {a} {b} eq = sym (PRI.-‿injective (PRI.+-inverseʳ-unique a (- b) eq ))
  where
    import Algebra.Properties.Ring IntP.+-*-ring as PRI

-- We show zero divisor is necessary zero (equivalent to left or right
-- cancellation in a commutative ring), which makes 𝔾 an integral
-- domain.
zero-divisor-is-zero :  ∀ {x y : 𝔾} -> x * y ≡ 0# -> ¬ x ≡ 0# -> y ≡ 0#
zero-divisor-is-zero {x@(a + b i)} {y@(c + d i)} eq neq = cong₂ _+_i (proj₁ step6) (proj₂ step6)
  where
    open ≡-Reasoning
    open IS.+-*-Solver
    -- 0 = x * y = (a * c - b * d) + (a * d + b * c) i, together with
    -- c + d i ≠ 0, we can derive a = 0 and b = 0, contradicting x ≠
    -- 0. The proof idea is:
    --
    -- step0 : a * c - b * d = 0 and a * d + b * c = 0
    -- step1 : a * c * c - b * d * c = 0
    -- step2 : a * d * d + b * c * d = 0
    -- s1,s2 ⇒ step1&2 : a * (c * c + d * d) = 0
    -- step3 : a * c * d - b * d * d = 0
    -- step4 : a * d * c + b * c * c = 0
    -- s3,s4 ⇒ step3&4 : b * (c * c + d * d) = 0
    -- one of a b nonzero ⇒ step5 : (c * c + d * d) = 0
    -- step5 ⇒ step6 : c = 0 and d = 0

    -- step0 : a * c - b * d = 0 and a * d + b * c = 0
    step0 : a * c - b * d ≡ 0# × a * d + b * c ≡ 0#
    step0 = unique0 eq

    -- step1 : a * c * c - b * d * c = 0
    step1 : a * c * c - b * d * c ≡ 0#
    step1 = begin
        a * c * c - b * d * c ≡⟨ solve 4 (\ a b c d -> a :* c :* c :- b :* d :* c := (a :* c :- b :* d) :* c) refl a b c d ⟩
        (a * c - b * d) * c ≡⟨ cong (_* c) (proj₁ step0) ⟩
        0ℤ * c ≡⟨ refl ⟩
        0ℤ ∎

    -- step2 : a * d * d + b * c * d = 0
    step2 : a * d * d + b * c * d ≡ 0#
    step2 = begin
        a * d * d + b * c * d ≡⟨ solve 4 (\ a b c d -> a :* d :* d :+ b :* c :* d := (a :* d :+ b :* c) :* d) refl a b c d ⟩
        (a * d + (b * c)) * d ≡⟨ cong (_* d) (proj₂ step0) ⟩
        0ℤ * d ≡⟨ refl ⟩
        0ℤ ∎

    -- c1,c2 ⇒ step1&2 : a * (c * c + d * d) = 0
    step1&2 : a * (c * c + d * d) ≡ 0#
    step1&2 = begin
      a * (c * c + d * d) ≡⟨ solve 4 (\ a b c d -> a :* (c :* c :+ d :* d) := (a :* c :* c :- b :* d :* c) :+ (a :* d :* d :+ b :* c :* d) ) refl a b c d ⟩
      (a * c * c - b * d * c) + (a * d * d + b * c * d) ≡⟨ cong₂ _+_ step1 step2 ⟩
      0# ∎

    -- step3 : a * c * d - b * d * d = 0
    step3 : a * c * d - b * d * d ≡ 0#
    step3 = begin
        a * c * d - b * d * d ≡⟨ solve 4 (\ a b c d -> a :* c :* d :- b :* d :* d := (a :* c :- b :* d) :* d) refl a b c d ⟩
        (a * c - b * d) * d ≡⟨ cong (_* d) (proj₁ step0) ⟩
        0ℤ * d ≡⟨ refl ⟩
        0ℤ ∎

    -- step4 : a * d * c + b * c * c = 0
    step4 : a * d * c + b * c * c ≡ 0#
    step4 = begin
        a * d * c + b * c * c ≡⟨ solve 4 (\ a b c d -> a :* d :* c :+ b :* c :* c := (a :* d :+ b :* c) :* c) refl a b c d ⟩
        (a * d + (b * c)) * c ≡⟨ cong (_* c) (proj₂ step0) ⟩
        0ℤ * c ≡⟨ refl ⟩
        0ℤ ∎

    -- s3,s4 ⇒ step3&4 : b * (c * c + d * d) = 0
    step3&4 : b * (c * c + d * d) ≡ 0#
    step3&4 = begin
      b * (c * c + d * d) ≡⟨ solve 4 (\ a b c d -> b :* (c :* c :+ d :* d) := :- (a :* c :* d :- b :* d :* d) :+ (a :* d :* c :+ b :* c :* c) ) refl a b c d ⟩
      - (a * c * d - b * d * d) + (a * d * c + b * c * c) ≡⟨ cong₂ (\x y -> (- x) + y) step3 step4 ⟩
      0# ∎

    -- one of a b nonzero ⇒ step5 : (c * c + d * d) = 0
    -- some auxillary lemma.
    aux : ∀ {a : ℤ} -> a * 0# ≡ 0#
    aux {a} rewrite IntP.*-comm a 0# = refl

    step1&2' : a * (c * c + d * d) ≡ a * 0#
    step1&2' rewrite aux {a} = step1&2

    step3&4' : b * (c * c + d * d) ≡ b * 0#
    step3&4' rewrite aux {b} = step3&4

    step5 : c * c + d * d ≡ 0#
    step5 = ⊎-elim (λ x₁ → IntP.*-cancelˡ-≡ a (c * c + d * d) 0# {{myins2 {a} {x₁}}} step1&2') (λ x₁ → IntP.*-cancelˡ-≡ b (c * c + d * d) 0# {{myins2 {b} {x₁}}} step3&4') (unique0' neq)
      where
        -- We need a translation from non-equality to NonZero predicate.
        open import Agda.Builtin.Unit
        myins2 : ∀ {x : ℤ} -> {n0 : ¬ x ≡ 0ℤ} -> NonZero x
        myins2 {+_ zero} {n0} with n0 refl
        ... | ()
        myins2 {+[1+ n ]} {n0} = record { nonZero = tt }
        myins2 { -[1+_] n} {n0} = record { nonZero = tt }

    -- step5 ⇒ step6 : c = 0 and d = 0
    step6 : c ≡ 0# × d ≡ 0#
    step6 = aa+bb=0⇒a=0×b=0 step5

-- Almost left cancellative.
*-alc-𝔾 : AlmostLeftCancellative 0𝔾 _*_
*-alc-𝔾 {x@(a + b i)} y@(c + d i) z@(e + f i)  neq eq = y=z
  where
    onesided-eq : x * (y + (- z)) ≡ 0#
    onesided-eq = begin
      x * (y + (- z)) ≡⟨ *-DistributesOver-+ˡ x y (- z)  ⟩
      x * y + x * (- z) ≡⟨ refl ⟩
      x * y + (a + b i) * (- e + - f i) ≡⟨ cong (λ t → x * y + t) refl ⟩
      x * y + ((a * - e - b * - f ) + (a * - f + b * - e) i)  ≡⟨ cong (λ t → x * y + t) (cong₂ _+_i (solve 4 (\a e b f -> a :* :- e :- b :* :- f := :- (a :* e :- b :* f)) refl a e b f) (solve 4 (\a e b f -> a :* :- f :+ b :* :- e := :- (a :* f :+ b :* e)) refl a e b f)) ⟩
      x * y + (- (a * e - b * f) + - (a * f + b * e) i)  ≡⟨ cong (λ t → x * y + t) refl ⟩
      x * y + (- (x * z)) ≡⟨ oneside eq  ⟩
      0# ∎
        where
          open ≡-Reasoning
          open IS.+-*-Solver

    y-z=0 : (y + (- z)) ≡ 0#
    y-z=0 = zero-divisor-is-zero onesided-eq neq

    y=z : y ≡ z
    y=z = twoside y-z=0

-- Multiplication commutativity plus left cancellative implies 𝔾 is an
-- commutative Domain. Knowing this, we can show e.g.
y≠0⇒y*yᶜ≠0 : ∀ {y} -> ¬ y ≡ 0# -> ¬ y * y ᶜ ≡ 0#
y≠0⇒y*yᶜ≠0 {y} n0 eq  = ⊥-elim (n0' e0)
      where
        open import Data.Empty
        n0' : ¬ y ᶜ ≡ 0#
        n0' x with n0 (ᶜ-injective {y} x)
        ... | ()

        eq' : y * y ᶜ ≡ y * 0#
        eq' = begin
          y * y ᶜ ≡⟨ eq ⟩
          0# ≡⟨ sym $ rightZero y ⟩
          y * 0# ∎
            where
              open IS.+-*-Solver
              open ≡-Reasoning

        e0 : y ᶜ ≡ 0#
        e0 = *-alc-𝔾 {y} (y ᶜ) 0# n0 eq'

y≠0#⇒rank≠0 : ∀ {y : 𝔾} -> ¬ y ≡ 0# -> ¬ rank y ≡ 0#
y≠0#⇒rank≠0 {y} n0 = rank≠0
  where
    open import Data.Empty
    y*yᶜ≠0 : ¬ y * y ᶜ ≡ 0#
    y*yᶜ≠0 = y≠0⇒y*yᶜ≠0 n0
    rank≠0 : ¬ rank y ≡ 0#
    rank≠0 e = ⊥-elim (y*yᶜ≠0 y*yᶜ=0)
      where
        y*yᶜ=0 : y * y ᶜ ≡ 0#
        y*yᶜ=0 = begin
          y * y ᶜ ≡⟨ sym $ Re+Im*i ⟩
          Re (y * y ᶜ) + Im (y * y ᶜ) i ≡⟨ cong₂ _+_i (Re[yyᶜ]=rank {y}) refl ⟩
          + rank y  + Im (y * y ᶜ) i ≡⟨ cong₂ _+_i (cong +_ e) (Im[yyᶜ]=0 {y}) ⟩
          0# ∎
            where
              open IS.+-*-Solver
              open ≡-Reasoning

rank=0⇒y=0 : ∀ {y : 𝔾} -> rank y ≡ 0# -> y ≡ 0#
rank=0⇒y=0 {y@(a + b i)} eq0 = y=0
  where
    eq0' : a * a + b * b ≡ 0#
    eq0' = IntP.∣i∣≡0⇒i≡0 eq0
    s1 : a ≡ 0ℤ × b ≡ 0ℤ
    s1 = aa+bb=0⇒a=0×b=0 eq0'
    y=0 : y ≡ 0#
    y=0 with s1
    ... | fst , snd rewrite fst | snd = refl

rank≥1 : ∀ {y : 𝔾} -> ¬ y ≡ 0# -> 1# ≤ rank y
rank≥1 {y} n0 = aux (rank y) (y≠0#⇒rank≠0 {y} n0)
  where
    aux : ∀ (n : ℕ) -> ¬ n ≡ 0 -> 1 ≤ n
    aux zero n0' with n0' refl
    ... | ()
    aux (suc n) n0' = Nat.s≤s Nat.z≤n

ranky<1⇒y=0 : ∀ (y : 𝔾) -> rank y < 1# -> y ≡ 0#
ranky<1⇒y=0 y r = rank=0⇒y=0 {y} ranky=0
  where
    aux : ∀ (n : ℕ) -> n < 1 -> n ≡ 0
    aux .zero (Nat.s≤s Nat.z≤n) = refl

    ranky=0 : rank y ≡ 0
    ranky=0 = aux (rank y) r

-- ----------------------------------------------------------------------
-- Properties of NonZero

max_stars_repo_name: onestruggler/EucDomain

max_issues_repo_name: onestruggler/EucDomain

max_forks_repo_name: onestruggler/EucDomain