text:
------------------------------------------------------------------------
-- Code related to the paper "Partiality, Revisited: The Partiality
-- Monad as a Quotient Inductive-Inductive Type"
--
-- Thorsten Altenkirch, Nils Anders Danielsson and Nicolai Kraus
------------------------------------------------------------------------

-- Note that this is a version of the code that does not quite match
-- the description in the paper. Some key changes (there might be
-- others):
--
-- * The partiality monad is not postulated, but defined as a QIIT
--   (Agda's cubical features are used). The types and eliminators are
--   marked as "abstract", so the eliminators do not compute.
--
-- * Rewrite rules are no longer used. Instead the propositional
--   truncation and set quotient operators are defined as
--   (non-abstract) QITs.
--
-- * The set quotient operator that is used can be applied to
--   arbitrary binary relations, not only propositional ones.

{-# OPTIONS --cubical --sized-types #-}

module README where

-- Note that our definition of the partiality monad and some of the
-- results are heavily inspired by the section on Cauchy reals in the
-- HoTT book (first edition).

-- The partiality algebra code uses ideas and concepts from "Inductive
-- types in homotopy type theory" by Awodey, Gambino and Sojakova,
-- "Inductive Types in Homotopy Type Theory" by Sojakova, "Quotient
-- inductive-inductive types" by Altenkirch, Capriotti, Dijkstra and
-- Nordvall Forsberg, and Gabe Dijkstra's PhD thesis.

------------------------------------------------------------------------
-- Pointers to results from the paper

-- In order to more easily find code corresponding to results from the
-- paper, see the following module. Note that some of the code
-- referenced below is not discussed at all in the paper.

import README.Pointers-to-results-from-the-paper

------------------------------------------------------------------------
-- Partiality algebras

-- Partiality algebras.

import Partiality-algebra

-- Some partiality algebra properties.

import Partiality-algebra.Properties

-- Partiality algebra categories.

import Partiality-algebra.Category

-- Eliminators and initiality.

import Partiality-algebra.Eliminators

-- Monotone functions.

import Partiality-algebra.Monotone

-- ω-continuous functions.

import Partiality-algebra.Omega-continuous

-- Strict ω-continuous functions.

import Partiality-algebra.Strict-omega-continuous

-- Fixpoint combinators.

import Partiality-algebra.Fixpoints

-- Pi with partiality algebra families as codomains.

import Partiality-algebra.Pi

------------------------------------------------------------------------
-- The partiality monad

-- A quotient inductive-inductive definition of the partiality monad.

import Partiality-monad.Inductive

-- Specialised eliminators.

import Partiality-monad.Inductive.Eliminators

-- A function that runs computations.

import Partiality-monad.Inductive.Approximate

-- An alternative characterisation of the information ordering, along
-- with related results.

import Partiality-monad.Inductive.Alternative-order

-- Monotone functions.

import Partiality-monad.Inductive.Monotone

-- ω-continuous functions.

import Partiality-monad.Inductive.Omega-continuous

-- The partiality monad's monad instance.

import Partiality-monad.Inductive.Monad

-- The partiality monad's monad instance, defined via an adjunction.

import Partiality-monad.Inductive.Monad.Adjunction

-- Strict ω-continuous functions.

import Partiality-monad.Inductive.Strict-omega-continuous

-- Fixpoint combinators.

import Partiality-monad.Inductive.Fixpoints

------------------------------------------------------------------------
-- Some examples

-- A function that, given a stream, tries to find an element
-- satisfying a predicate.

import Search

-- Examples involving simple λ-calculi.

import README.Lambda

------------------------------------------------------------------------
-- An alternative definition of the delay monad

-- The delay monad, defined using increasing sequences of potential
-- values.

import Delay-monad.Alternative

-- Various properties.

import Delay-monad.Alternative.Properties

-- Theorems relating the coinductive definition of the delay
-- monad to the alternative one and to another type.

import Delay-monad.Alternative.Equivalence

-- Termination predicates.

import Delay-monad.Alternative.Termination

-- Information orderings.

import Delay-monad.Alternative.Partial-order

-- Weak bisimilarity.

import Delay-monad.Alternative.Weak-bisimilarity

-- Two eliminators for Delay-monad.Alternative.Delay (A / R).

import Delay-monad.Alternative.Eliminators

------------------------------------------------------------------------
-- The delay monad quotiented by weak bisimilarity

-- The delay monad quotiented by weak bisimilarity.

import Partiality-monad.Coinductive

-- A partial order.

import Partiality-monad.Coinductive.Partial-order

-- An alternative definition of the partiality monad: a variant of the
-- delay monad quotiented by a notion of weak bisimilarity.

import Partiality-monad.Coinductive.Alternative

------------------------------------------------------------------------
-- A proof of equivalence

-- The partiality monads in Partiality-monad.Inductive and
-- Partiality-monad.Coinductive are pointwise equivalent, for sets,
-- assuming extensionality and countable choice.

import Partiality-monad.Equivalence

------------------------------------------------------------------------
-- ω-cpos

-- Pointed and non-pointed ω-cpos.

import Omega-cpo

-- The code in the following three modules is based on a suggestion
-- from Paolo Capriotti.

-- A quotient inductive-inductive definition of the lifting
-- construction on ω-cpos.

import Lifting

-- An alternative but equivalent definition of the partiality monad
-- (but only for sets), based on the lifting construction in Lifting.

import Lifting.Partiality-monad

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Lists
------------------------------------------------------------------------

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

module Data.List where

------------------------------------------------------------------------
-- Types and basic operations

open import Data.List.Base public

ext: agda


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

open import Categories.Category

module Categories.Object.Product.Indexed.Properties {o ℓ e} (C : Category o ℓ e) where

open import Level

open import Categories.Category.Discrete
open import Categories.Category.Complete
open import Categories.Category.Construction.Cones
open import Categories.Category.Lift
open import Categories.Object.Product.Indexed C
open import Categories.Diagram.Limit
open import Categories.Functor

import Relation.Binary.PropositionalEquality as ≡

private
  variable
    o′ ℓ′ e′ : Level
  open Category C

module _ {i} (Com : Complete (i ⊔ o′) (i ⊔ ℓ′) (i ⊔ e′) C) where

  module _ {I : Set i} (P : I → Obj) where
    private
      Z = liftC o′ ℓ′ e′ (Discrete I)
      F = lift-func C P ∘F unliftF o′ ℓ′ e′ (Discrete I)
      module L = Limit (Com F)

      K : ∀ {Y} → (∀ i → Y ⇒ P i) → Cone F
      K f = record
        { apex = record
          { ψ       = λ i → f (lower i)
          ; commute = λ { (lift ≡.refl) → identityˡ }
          }
        }

    Complete⇒IndexedProductOf : IndexedProductOf P
    Complete⇒IndexedProductOf = record
      { X       = L.apex
      ; π       = λ i → L.proj (lift i)
      ; ⟨_⟩     = λ f → L.rep (K f)
      ; commute = λ f _ → Cone⇒.commute (L.rep-cone (K f))
      ; unique  = λ f g eq → L.terminal.!-unique {A = K g} record
        { arr     = f
        ; commute = eq _
        }
      }

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
{-# OPTIONS --without-K #-}
module hott.truncation.equality where

open import sum
open import equality
open import function.extensionality
open import function.isomorphism
open import function.overloading
open import sets.nat
open import hott.equivalence
open import hott.level.core
open import hott.level.closure
open import hott.truncation.core

module _ {i}{X : Set i}(n-1 : ℕ) where
  private
    n : ℕ
    n = suc n-1

    Trunc-dep-iso₂ : ∀ {j} (Z : Trunc n X → Trunc n X → Set j)
                   → ((c c' : Trunc n X) → h n (Z c c'))
                   → ((c c' : Trunc n X) → Z c c')
                   ≅ ((x y : X) → Z [ x ] [ y ])
    Trunc-dep-iso₂ Z hZ = begin
        ((c c' : Trunc n X) → Z c c')
      ≅⟨ (Π-ap-iso refl≅ λ c → Trunc-dep-iso n (Z c) (hZ c)) ⟩
        ((c : Trunc n X)(y : X) → Z c [ y ])
      ≅⟨ Trunc-dep-iso n (λ c → (y : X) → Z c [ y ]) (λ c → Π-level λ y → hZ c [ y ]) ⟩
        ((x y : X) → Z [ x ] [ y ])
      ∎
      where open ≅-Reasoning

    P₀ : X → X → Type i (n-1)
    P₀ x y = Trunc (n-1) (x ≡ y) , Trunc-level n-1

    abstract
      r₀ : (x : X) → proj₁ (P₀ x x)
      r₀ x = [ refl ]

      abstract
        P-iso' : (Trunc n X → Trunc n X → Type i (n-1))
               ≅ (X → X → Type i (n-1))
        P-iso' = Trunc-dep-iso₂ (λ _ _ → Type i (n-1))
                               (λ _ _ → type-level)

        P-iso-we : weak-equiv (λ (Z : Trunc n X → Trunc n X → Type i (n-1)) x y → Z [ x ] [ y ])
        P-iso-we = proj₂ (≅⇒≈ P-iso')

      P-iso : (Trunc n X → Trunc n X → Type i (n-1))
            ≅ (X → X → Type i (n-1))
      P-iso = ≈⇒≅ ((λ Z x y → Z [ x ] [ y ]) , P-iso-we)

      module impl (P : Trunc n X → Trunc n X → Type i (n-1))
                  (P-β : (x y : X) → P [ x ] [ y ] ≡ P₀ x y) where

        r' : (P : Trunc n X → Trunc n X → Type i (n-1))
           → (∀ x y → P [ x ] [ y ] ≡ P₀ x y)
           → (c : Trunc n X) → proj₁ (P c c)
        r' P q = Trunc-dep-elim n (λ c → proj₁ (P c c))
                                  (λ c → h↑ (proj₂ (P c c)))
                                  λ x → subst proj₁ (sym (q x x)) (r₀ x)

        r : (c : Trunc n X) → proj₁ (P c c)
        r = r' P P-β

        abstract
          P-elim-iso : (Z : Trunc n X → Trunc n X → Type i (n-1))
                     → ((c c' : Trunc n X) → proj₁ (P c c') → proj₁ (Z c c'))
                     ≅ ((c : Trunc n X) → proj₁ (Z c c))
          P-elim-iso Z = begin
              ((c c' : Trunc n X) → proj₁ (P c c') → proj₁ (Z c c'))
           ≅⟨ Trunc-dep-iso₂ (λ c c' → proj₁ (P c c') → proj₁ (Z c c'))
                             (λ c c' → Π-level λ p → h↑ (proj₂ (Z c c'))) ⟩
              ((x y : X) → proj₁ (P [ x ] [ y ]) → proj₁ (Z [ x ] [ y ]))
            ≅⟨ ( Π-ap-iso refl≅ λ x
               → Π-ap-iso refl≅ λ y
               → Π-ap-iso (≡⇒≅ (ap proj₁ (P-β x y))) λ _
               → refl≅ ) ⟩
              ((x y : X) → Trunc (n-1) (x ≡ y) → proj₁ (Z [ x ] [ y ]))
            ≅⟨ ( Π-ap-iso refl≅ λ x
               → Π-ap-iso refl≅ λ y
               → Trunc-elim-iso (n-1) (x ≡ y) _ (proj₂ (Z [ x ] [ y ])) ) ⟩
              ((x y : X) → x ≡ y → proj₁ (Z [ x ] [ y ]))
            ≅⟨ ( Π-ap-iso refl≅ λ x → sym≅ J-iso ) ⟩
              ((x : X) → proj₁ (Z [ x ] [ x ]))
            ≅⟨ sym≅ (Trunc-dep-iso n (λ c → proj₁ (Z c c)) (λ c → h↑ (proj₂ (Z c c)))) ⟩
              ((c : Trunc n X) → proj₁ (Z c c))
            ∎
            where open ≅-Reasoning

        Eq : Trunc n X → Trunc n X → Type i (n-1)
        Eq c c' = (c ≡ c') , Trunc-level n c c'

        abstract
          f₀ : (c c' : Trunc n X) → proj₁ (P c c') → c ≡ c'
          f₀ = _≅_.from (P-elim-iso Eq) (λ _ → refl)

        abstract
          f : (c c' : Trunc n X) → proj₁ (P c c') → c ≡ c'
          f c c' p = f₀ c c' p · sym (f₀ c' c' (r c'))

          f-β : (c : Trunc n X) → f c c (r c) ≡ refl
          f-β c = left-inverse (f₀ c c (r c))

        g : (c c' : Trunc n X) → c ≡ c' → proj₁ (P c c')
        g c .c refl = r c

    --    α : (c c' : Trunc n X)(p : proj₁ (P c c')) → g c c' (f c c' p) ≡ p
    --    α = _≅_.from (P-elim-dep-iso Z) λ c → ap (g c c) (f-β c)
    --      where
    --        Z : (c c' : Trunc n X) → proj₁ (P c c') → Type i (n-1)
    --        Z c c' p = (g c c' (f c c' p) ≡ p) , h↑ (proj₂ (P c c')) _ _

        β : (c c' : Trunc n X)(q : c ≡ c') → f c c' (g c c' q) ≡ q
        β c .c refl = f-β c

        trunc-equality : {x y : X} → _≡_ {A = Trunc n X} [ x ] [ y ] → Trunc (n-1) (x ≡ y)
        trunc-equality {x}{y} p = subst (λ Z → Z) (ap proj₁ (P-β x y)) (g [ x ] [ y ] p)

      P : Trunc n X → Trunc n X → Type i (n-1)
      P = _≅_.from P-iso P₀

      P-β' : (λ x y → P [ x ] [ y ]) ≡ P₀
      P-β' = _≅_.iso₂ P-iso P₀

      P-β : (x y : X) → P [ x ] [ y ] ≡ P₀ x y
      P-β x y = funext-inv (funext-inv P-β' x) y

      open impl P P-β using (trunc-equality) public

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
-- Andreas, 2014-09-07
open import Common.Equality

data ⊥ : Set where
record ⊤ : Set where

-- Agda allows us to prove that A ≠ (A → B)
test : {A B : Set} → A ≡ (A → B) → ⊥
test ()

-- Agda allows us to prove that A ≠ (B → A)
test' : {A B : Set} → A ≡ (B → A) → ⊥
test' ()

-- But ⊤ is isomorphic to ⊤ → ⊤, which under univalence
-- isomorphism-as-equality contradicts both test and test'.

test'' : (⊤ ≡ (⊤ → ⊤)) → ⊥
test'' = test'

there : ⊤ → (⊤ → ⊤)
there _ _ = _

back : (⊤ → ⊤) → ⊤
back _ = _

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{- The following code gives the basic idea of division by repeated
   subtraction.  We have to ask Agda not to check termination of this
   function, because it is not structurally terminating.  The versions
   in nat-division.agda and nat-division-wf.agda correct this problem,
   and can be judged by Agda to be terminating. -}

module nat-division-basic where

open import bool
open import eq
open import nat
open import product
open import sum

{-# NON_TERMINATING #-}
div : (x d : ℕ) → d =ℕ 0 ≡ ff → ℕ × ℕ
div 0 _ _ = 0 , 0
div x d p with (x < d)
div x d p | tt = 0 , x
div x d p | ff with div (x ∸ d) d p
div x d p | ff | q , r = suc q , r

test-div : ℕ × ℕ
test-div = div 17 3 refl

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
module Miscellaneous.TFlipFlop where

open import Data.Boolean
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Logic
open import Data.Boolean.Numeral
open import Numeral.Natural
open import Syntax.Number

tFlipFlop : Bool → (ℕ → Bool) → (ℕ → Bool)
tFlipFlop init T(𝟎)    = init
tFlipFlop init T(𝐒(n)) = T(n) ⊕ tFlipFlop init T(n)

open import Data
open import Relator.Equals

module _ where
  postulate Q₀ : ℕ → Bool
  postulate Q₁ : ℕ → Bool

  postulate f : Bool → Bool
  postulate g : Bool → Bool

  postulate q₀0 : Q₀(0) ≡ 1
  postulate q₁0 : Q₁(0) ≡ 1

  postulate q₀1 : Q₀(1) ≡ 0
  postulate q₁1 : Q₁(1) ≡ 1

  postulate q₀2 : Q₀(2) ≡ 1
  postulate q₁2 : Q₁(2) ≡ 0

  postulate q₀3 : Q₀(3) ≡ 0
  postulate q₁3 : Q₁(3) ≡ 0

  postulate q₀4 : Q₀(4) ≡ Q₀(0)
  postulate q₁4 : Q₁(4) ≡ Q₁(0)

  {-# REWRITE q₀0 q₁0 q₀1 q₁1 q₀2 q₁2 q₀3 q₁3 q₀4 q₁4 #-}

  private variable n : ℕ

  postulate q₀step : Q₀(𝐒 n) ≡ f(Q₁(n)) ⊕ Q₀(n)
  postulate q₁step : Q₁(𝐒 n) ≡ g(Q₀(n)) ⊕ Q₁(n)

  open import Numeral.Natural.Oper
  open import Relator.Equals.Proofs
  open import Structure.Function
  open import Structure.Operator
  open import Syntax.Transitivity

  q₀cyclic : Q₀(n + 4) ≡ Q₀(n)
  q₁cyclic : Q₁(n + 4) ≡ Q₁(n)

  q₀cyclic {𝟎} = [≡]-intro
  q₀cyclic {𝐒 n} =
    Q₀ (𝐒 n + 4)                🝖[ _≡_ ]-[]
    Q₀ (𝐒(n + 4))               🝖[ _≡_ ]-[ q₀step{n + 4} ]
    f(Q₁(n + 4)) ⊕ Q₀(n + 4)    🝖[ _≡_ ]-[ congruence₂(_⊕_) (congruence₁(f) (q₁cyclic{n})) (q₀cyclic{n}) ]
    f(Q₁(n)) ⊕ Q₀(n)            🝖[ _≡_ ]-[ q₀step{n} ]-sym
    Q₀ (𝐒 n)                    🝖-end

  q₁cyclic {𝟎} = [≡]-intro
  q₁cyclic {𝐒 n} =
    Q₁ (𝐒 n + 4)                🝖[ _≡_ ]-[]
    Q₁ (𝐒(n + 4))               🝖[ _≡_ ]-[ q₁step{n + 4} ]
    g(Q₀(n + 4)) ⊕ Q₁(n + 4)    🝖[ _≡_ ]-[ congruence₂(_⊕_) (congruence₁(g) (q₀cyclic{n})) (q₁cyclic{n}) ]
    g(Q₀(n)) ⊕ Q₁(n)            🝖[ _≡_ ]-[ q₁step{n} ]-sym
    Q₁ (𝐒 n)                    🝖-end

  f0 : f(0) ≡ 1
  f0 with f(0) | q₀step{2}
  ... | 𝑇 | q = [≡]-intro

  f1 : f(1) ≡ 1
  f1 with f(1) | q₀step{0}
  ... | 𝑇 | q = [≡]-intro

  f1' : f(1) ≡ 1
  f1' with f(1) | q₀step{1}
  ... | 𝑇 | q = [≡]-intro

  f1'' : f(1) ≡ 1
  f1'' with f(1) | q₀step{0}
  ... | 𝑇 | q = [≡]-intro

  g1 : g(1) ≡ 0
  g1 with g(1) | q₁step{0}
  ... | 𝐹 | q = [≡]-intro

  g0 : g(0) ≡ 1
  g0 with g(0) | q₁step{1}
  ... | 𝑇 | q = [≡]-intro

  g1' : g(1) ≡ 0
  g1' with g(1) | q₁step{2}
  ... | 𝐹 | q = [≡]-intro

  g1'' : g(0) ≡ 1
  g1'' with g(0) | q₁step{3}
  ... | 𝑇 | q = [≡]-intro

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import progress
open import htype-decidable
open import lemmas-complete

module complete-progress where

  -- as in progress, we define a datatype for the possible outcomes of
  -- progress for readability.
  data okc : (d : ihexp) (Δ : hctx) → Set where
    V : ∀{d Δ} → d val → okc d Δ
    S : ∀{d Δ} → Σ[ d' ∈ ihexp ] (d ↦ d') → okc d Δ

  complete-progress : {Δ : hctx} {d : ihexp} {τ : htyp} →
                       Δ , ∅ ⊢ d :: τ →
                       d dcomplete →
                       okc d Δ
  complete-progress wt comp with progress wt
  complete-progress wt comp | I x = abort (lem-ind-comp comp x)
  complete-progress wt comp | S x = S x
  complete-progress wt comp | BV (BVVal x) = V x
  complete-progress wt (DCCast comp x₂ ()) | BV (BVHoleCast x x₁)
  complete-progress (TACast wt x) (DCCast comp x₃ x₄) | BV (BVArrCast x₁ x₂) = abort (x₁ (complete-consistency x x₃ x₄))
  complete-progress (TACast wt x) (DCCast comp x₃ x₄) | BV (BVSumCast x₁ x₂) = abort (x₁ (complete-consistency x x₃ x₄))
  complete-progress (TAInl wt) (DCInl x₁ comp) | BV (BVInl x)
    with complete-progress wt comp
  ... | V v = V (VInl v)
  ... | S (_ , Step x₂ x₃ x₄) = S (_ , Step (FHInl x₂) x₃ (FHInl x₄))
  complete-progress (TAInr wt) (DCInr x₁ comp) | BV (BVInr x)
    with complete-progress wt comp
  ... | V v = V (VInr v)
  ... | S (_ , Step x₂ x₃ x₄) = S (_ , Step (FHInr x₂) x₃ (FHInr x₄))
  complete-progress (TAPair wt wt₁) (DCPair comp comp₁) | BV (BVPair x x₁)
    with complete-progress wt comp | complete-progress wt₁ comp₁
  ... | V v | V v₁ = V (VPair v v₁)
  ... | V v | S (_ , Step x₁ x₂ x₃) = S (_ , Step (FHPair2 x₁) x₂ (FHPair2 x₃))
  ... | S (_ , Step x₁ x₂ x₃) | V v = S (_ , Step (FHPair1 x₁) x₂ (FHPair1 x₃))
  ... | S (_ , Step x₁ x₂ x₃) | S (_ , Step x₄ x₅ x₆) = S (_ , Step (FHPair1 x₁) x₂ (FHPair1 x₃))
  complete-progress (TACast wt x₁) (DCCast comp x₂ x₃) | BV (BVProdCast x x₄) = abort (x (complete-consistency x₁ x₂ x₃))

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module Whitespace where

-- The following definition contains several different whitespace
-- characters, and they are all treated as whitespace.

foo :  Set -> Set  ->  Set
foo x _ =  x

-- Tab characters are not treated as white space, but are still
-- allowed in character and string literals and non-pragma comments
-- (	).

{-# BUILTIN STRING  String #-}
{-# BUILTIN CHAR    Char   #-}

string : String
string = "	"

char : Char
char = '	'

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

module Loop where

open import Loop.Definitions public
open import Loop.Bundles public
open import Loop.Structures public


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Natural numbers, basic types and operations
------------------------------------------------------------------------

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

module Data.Nat.Base where

open import Level using (0ℓ)
open import Function using (_∘_; flip)
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality.Core
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (¬_)

------------------------------------------------------------------------
-- The types

open import Agda.Builtin.Nat public
  using (zero; suc) renaming (Nat to ℕ)

------------------------------------------------------------------------
-- Standard ordering relations

open import Agda.Builtin.Nat public
  using () renaming (_==_ to _≡ᵇ_; _<_ to _<ᵇ_)

infix 4 _≤_ _<_ _≥_ _>_ _≰_ _≮_ _≱_ _≯_

data _≤_ : Rel ℕ 0ℓ where
  z≤n : ∀ {n}                 → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

_<_ : Rel ℕ 0ℓ
m < n = suc m ≤ n

_≥_ : Rel ℕ 0ℓ
m ≥ n = n ≤ m

_>_ : Rel ℕ 0ℓ
m > n = n < m

_≰_ : Rel ℕ 0ℓ
a ≰ b = ¬ a ≤ b

_≮_ : Rel ℕ 0ℓ
a ≮ b = ¬ a < b

_≱_ : Rel ℕ 0ℓ
a ≱ b = ¬ a ≥ b

_≯_ : Rel ℕ 0ℓ
a ≯ b = ¬ a > b

------------------------------------------------------------------------
-- Arithmetic

open import Agda.Builtin.Nat public
  using (_+_; _*_) renaming (_-_ to _∸_)

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

infixl 7 _⊓_
infixl 6 _+⋎_ _⊔_

-- Argument-swapping addition. Used by Data.Vec._⋎_.

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

-- Max.

_⊔_ : ℕ → ℕ → ℕ
zero  ⊔ n     = n
suc m ⊔ zero  = suc m
suc m ⊔ suc n = suc (m ⊔ n)

-- Min.

_⊓_ : ℕ → ℕ → ℕ
zero  ⊓ n     = zero
suc m ⊓ zero  = zero
suc m ⊓ suc n = suc (m ⊓ n)

-- Division by 2, rounded downwards.

⌊_/2⌋ : ℕ → ℕ
⌊ 0 /2⌋           = 0
⌊ 1 /2⌋           = 0
⌊ suc (suc n) /2⌋ = suc ⌊ n /2⌋

-- Division by 2, rounded upwards.

⌈_/2⌉ : ℕ → ℕ
⌈ n /2⌉ = ⌊ suc n /2⌋

-- Naïve exponentiation

_^_ : ℕ → ℕ → ℕ
x ^ zero  = 1
x ^ suc n = x * x ^ n

-- Distance

∣_-_∣ : ℕ → ℕ → ℕ
∣ zero  - y     ∣ = y
∣ x     - zero  ∣ = x
∣ suc x - suc y ∣ = ∣ x - y ∣

------------------------------------------------------------------------
-- The following, alternative definition of _≤_ is more suitable for
-- well-founded induction (see Induction.Nat).

infix 4 _≤′_ _<′_ _≥′_ _>′_

data _≤′_ (m : ℕ) : ℕ → Set where
  ≤′-refl :                         m ≤′ m
  ≤′-step : ∀ {n} (m≤′n : m ≤′ n) → m ≤′ suc n

_<′_ : Rel ℕ 0ℓ
m <′ n = suc m ≤′ n

_≥′_ : Rel ℕ 0ℓ
m ≥′ n = n ≤′ m

_>′_ : Rel ℕ 0ℓ
m >′ n = n <′ m

------------------------------------------------------------------------
-- Another alternative definition of _≤_.

record _≤″_ (m n : ℕ) : Set where
  constructor less-than-or-equal
  field
    {k}   : ℕ
    proof : m + k ≡ n

infix 4 _≤″_ _<″_ _≥″_ _>″_

_<″_ : Rel ℕ 0ℓ
m <″ n = suc m ≤″ n

_≥″_ : Rel ℕ 0ℓ
m ≥″ n = n ≤″ m

_>″_ : Rel ℕ 0ℓ
m >″ n = n <″ m

------------------------------------------------------------------------
-- Useful for induction when you have an upper bound.

data _≤‴_ : ℕ → ℕ → Set where
  ≤‴-refl : ∀{m} → m ≤‴ m
  ≤‴-step : ∀{m n} → suc m ≤‴ n → m ≤‴ n

infix 4 _≤‴_ _<‴_ _≥‴_ _>‴_

_<‴_ : Rel ℕ 0ℓ
m <‴ n = suc m ≤‴ n

_≥‴_ : Rel ℕ 0ℓ
m ≥‴ n = n ≤‴ m

_>‴_ : Rel ℕ 0ℓ
m >‴ n = n <‴ m

------------------------------------------------------------------------
-- A comparison view. Taken from "View from the left"
-- (McBride/McKinna); details may differ.

data Ordering : Rel ℕ 0ℓ where
  less    : ∀ m k → Ordering m (suc (m + k))
  equal   : ∀ m   → Ordering m m
  greater : ∀ m k → Ordering (suc (m + k)) m

compare : ∀ m n → Ordering m n
compare zero    zero    = equal   zero
compare (suc m) zero    = greater zero m
compare zero    (suc n) = less    zero n
compare (suc m) (suc n) with compare m n
... | less    m k = less (suc m) k
... | equal   m   = equal (suc m)
... | greater n k = greater (suc n) k


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
module Network where

open import Data.Fin hiding (lift; _<_)
open import Function
open import Data.Nat
open import Data.Nat.Show
open import Data.String hiding (show)
open import Data.Vec hiding (_++_)
open import Foreign.Haskell
open import IO
import IO.Primitive as IOPrim
import Network.Primitive as NetPrim

withSocketsDo : ∀ {a} {A : Set a} → IO A → IO A
withSocketsDo io = lift (NetPrim.withSocketsDo (run io))

byteSize : ℕ
byteSize = 256

wordSize : ℕ
wordSize = byteSize * byteSize

data IPAddress : Set where
 IPv4 : Vec (Fin byteSize) 4 → IPAddress
 IPv6 : Vec (Fin wordSize) 8 → IPAddress

{-
private
  showIPVec : {m n : ℕ} → Vec (Fin m) n → String
  showIPVec ip = foldl₁ (λ x y → x ++ "." ++ y) (map (show ∘ toℕ) ip)
-}

showIP : IPAddress → String
showIP (IPv4 ip) = foldl₁ (λ x y → x ++ "." ++ y) (map (show ∘ toℕ) ip)
showIP (IPv6 ip) = foldl₁ (λ x y → x ++ ":" ++ y) (map ((showInBase 16) ∘ toℕ) ip)

data PortNumber : Set where
  portNum : Fin wordSize → PortNumber

showPort : PortNumber → String
showPort (portNum n) = show (toℕ n)

connectTo : IPAddress → PortNumber → IO IOPrim.Handle
connectTo ip (portNum n) = lift (NetPrim.connectTo (showIP ip) (toInteger (toℕ n)))

max_stars_repo_name: ilya-fiveisky/agda-network

max_issues_repo_name: ilya-fiveisky/agda-network

max_forks_repo_name: ilya-fiveisky/agda-network


text:
-- Andreas, 2019-11-10, issue #4185, reported and test case by nad.
--
-- Problem: no-eta-equality was ignored during Miller pattern unification
-- when turning meta-variable applied to constructed record expression
-- into meta-variable applied to record field(s).

-- {-# OPTIONS -v tc.meta.assign:30 #-}

open import Agda.Builtin.Equality

record Box (A : Set) : Set where
  no-eta-equality
  constructor box
  field
    unbox : A

open Box

postulate
  A : Set

AllBox All : (P : Box A → Set) → Set
AllBox P = (x : Box A) → P x
All    P = (a : A) → P (box a)

postulate
  to    : (P : Box A → Set) → AllBox P → All P

  from  : (P : Box A → Set) → All P → AllBox P

  test  : (P : Box A → Set)
        → (f : AllBox P) → from _ (to P f) ≡ f  -- Underscore should be solved.

-- Problem WAS:
--
-- Due to invalid η-expansion, the equation
--
--   _P (box a) = P (box a)
--
-- was solved as
--
--   _P x = P (box (unbox x))
--
-- resulting in a subsequent type error as Box has no η.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Definition.Typed.Consequences.SucCong where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Weakening
open import Definition.Typed.Properties
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Substitution

open import Tools.Product

-- Congurence of the type of the successor case in natrec.
sucCong : ∀ {F G Γ} → Γ ∙ ℕ ⊢ F ≡ G
        → Γ ⊢ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)
            ≡ Π ℕ ▹ (G ▹▹ G [ suc (var 0) ]↑)
sucCong F≡G with wfEq F≡G
sucCong F≡G | ⊢Γ ∙ ⊢ℕ =
  let ⊢F , _ = syntacticEq F≡G
  in  Π-cong ⊢ℕ (refl ⊢ℕ)
             (Π-cong ⊢F F≡G
                     (wkEq (step id) (⊢Γ ∙ ⊢ℕ ∙ ⊢F)
                           (subst↑TypeEq F≡G
                                         (refl (sucⱼ (var (⊢Γ ∙ ⊢ℕ) here))))))

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text: module Structure.Topology.Properties where


text:
{-# OPTIONS --without-K #-}
module sum-properties where

open import Type
import Level as L
open L using (Lift)
open import Data.Zero using (𝟘)
open import Data.Bool.NP
open Data.Bool.NP.Indexed
open import Data.Nat.NP
open import Data.Nat.Properties
open import Data.Product renaming (map to pmap)
open import Data.Sum
open import Relation.Binary.Product.Pointwise
open import Data.Maybe
open import Data.One using (𝟙)
open import Function.NP
import Function.Inverse as Inv
open Inv using (_↔_)
open import Function.Related
open import Function.Related.TypeIsomorphisms.NP
open import Function.Equality using (_⟨$⟩_)

--open import sum
open import Search.Type
open import Search.Sum
open import Search.Derived using (sum-swap)
open import Search.Searchable renaming (Searchable to SumProp)
open import Search.Searchable.Fin
open import Search.Searchable.Product
open import Search.Searchable.Sum
open import Relation.Binary.Sum
import Relation.Binary.PropositionalEquality.NP as ≡
open ≡ using (_≡_ ; _≗_ ; _≗₂_)

module _M2 {A : ★} (μA : SumProp A) (f g : A → Bool) where

sum-ext₂ : ∀ {A B}{f g : A → B → ℕ}(μA : SumProp A)(μB : SumProp B) → f ≗₂ g → sum μA (sum μB ∘ f) ≡ sum μA (sum μB ∘ g)
sum-ext₂ μA μB f≗g = sum-ext μA (sum-ext μB ∘ f≗g)

CountStableUnderInjection : ∀ {A} → SumProp A → Set
CountStableUnderInjection μ = ∀ p → Injective p → CountStableUnder (count μ) p

#-StableUnderInjection : ∀ {A}{μ : SumProp A} → SumStableUnderInjection (sum μ) → CountStableUnderInjection μ
#-StableUnderInjection sui p p-inj f = sui p p-inj (toℕ ∘ f)

𝟙SUI : SumStableUnderInjection (sum μ𝟙)
𝟙SUI f p x = ≡.refl

{-
stableMaybe : ∀ {A} (μA : SumProp A) → StableUnderInjection μA
                                     → StableUnderInjection (μMaybe μA)
stableMaybe {A} μA suiA f p p-inj with p nothing | ≡.inspect p nothing
... | nothing | ≡.[ eq ] = {!!}
  where h : ∀ x → p (just x) ≡ just {!!}
        h = {!!}
        p' : A → A
        p' x = {!p (just x)!}
        p'-inj : Injective p'
        p'-inj = {!!}
... | just pn | ≡.[ eq ] = ≡.trans (≡.cong (λ x → f nothing + x) (suiA (f ∘ just) p' p'-inj)) {!!}
  where p' : A → A
        p' x = maybe id pn (p (just x))
        p'-inj : Injective p'
        p'-inj = {!!}

SumsOk : ∀ {A B} → SumProp A → SumProp B → A ↔ B → ★
SumsOk μA μB iso = ∀ f → sum μA f ≡ sum μB (f ∘ from)
  where from = _⟨$⟩_ (Inv.Inverse.from iso)

module StableIso {A B}(μA : SumProp A)(μB : SumProp B)(iso : A ↔ B)
                 (sums-ok : SumsOk μA μB iso)
                 (suiB    : StableUnderInjection μB) where
  to : A → B
  to x = Inv.Inverse.to iso ⟨$⟩ x

  from : B → A
  from x = Inv.Inverse.from iso ⟨$⟩ x

  from-inj : Injective from
  from-inj = Inv.Inverse.injective (Inv.sym iso)

  to-inj : Injective to
  to-inj = Inv.Inverse.injective iso

  left-inv : from ∘ to ≗ id
  left-inv = Inv.Inverse.left-inverse-of iso

  stable : StableUnderInjection μA
  stable f p p-inj
    = sum μA f
    ≡⟨ sums-ok f ⟩
      sum μB (f ∘ from)
    ≡⟨ suiB (f ∘ from) (to ∘ p ∘ from) (from-inj ∘ p-inj ∘ to-inj) ⟩
      sum μB (f ∘ from ∘ to ∘ p ∘ from)
    ≡⟨ sum-ext μB (λ x → ≡.cong f (left-inv (p (from x)))) ⟩
      sum μB (f ∘ p ∘ from)
    ≡⟨ ≡.sym (sums-ok (f ∘ p)) ⟩
      sum μA (f ∘ p)
    ∎
    where open ≡.≡-Reasoning

record Iso1+ {A : Set}(μA : SumProp A) : ★₁ where
  constructor mk
  field
    B   : ★
    μB  : SumProp B
    iso : A ↔ Maybe B

  toMaybe : A → Maybe B
  toMaybe x = Inv.Inverse.to iso ⟨$⟩ x

  fromMaybe : Maybe B → A
  fromMaybe x = Inv.Inverse.from iso ⟨$⟩ x

  field
    sums-ok  : ∀ f → sum μA f ≡ sum (μMaybe μB) (f ∘ fromMaybe)

  from-inj : Injective fromMaybe
  from-inj = Inv.Inverse.injective (Inv.sym iso)

  to-inj : Injective toMaybe
  to-inj = Inv.Inverse.injective iso

  left-inv : fromMaybe ∘ toMaybe ≗ id
  left-inv = Inv.Inverse.left-inverse-of iso

  stable : StableUnderInjection (μMaybe μB) → StableUnderInjection μA
  stable suiMB = StableIso.stable μA (μMaybe μB) iso sums-ok suiMB

-- iso1+𝟙 : Iso1+ μ𝟙
-- iso1+𝟙 = {!mk !}

iso1+Maybe : ∀ {A} (μA : SumProp A) → Iso1+ μA → Iso1+ (μMaybe μA)
iso1+Maybe {A} μA A≅1+ = mk A μA Inv.id (λ f → ≡.refl)

iso1+FinSuc : ∀ n → Iso1+ (μFinSuc (suc n))
iso1+FinSuc n = mk (Fin (suc n)) (μFinSuc n) Fin∘suc↔Maybe∘Fin (λ f → ≡.refl)
-}

infix 4 _≈_

record _≈_ {A B} (μA : SumProp A)(μB : SumProp B) : Set where
  constructor mk
  field
    iso : A ↔ B
  from : B → A
  from x = Inv.Inverse.from iso ⟨$⟩ x

  to : A → B
  to x = Inv.Inverse.to iso ⟨$⟩ x

  from-inj : Injective from
  from-inj = Inv.Inverse.injective (Inv.sym iso)

  to-inj : Injective to
  to-inj = Inv.Inverse.injective iso

  field
    sums-ok : ∀ f → sum μA f ≡ sum μB (f ∘ from)

  sums-ok' : ∀ f → sum μB f ≡ sum μA (f ∘ to)
  sums-ok' f = sum μB f
             ≡⟨ sum-ext μB (≡.cong f ∘ ≡.sym ∘ Inv.Inverse.right-inverse-of iso) ⟩
               sum μB (f ∘ to ∘ from)
             ≡⟨ ≡.sym (sums-ok (f ∘ to)) ⟩
               sum μA (f ∘ to)
             ∎
    where open ≡.≡-Reasoning

  StableUnder≈ : SumStableUnderInjection (sum μA) → SumStableUnderInjection (sum μB)
  StableUnder≈ μA-SUI p p-inj f
    = sum μB f
    ≡⟨ sums-ok' f ⟩
      sum μA (f ∘ to)
    ≡⟨ μA-SUI (from ∘ p ∘ to) (to-inj ∘ p-inj ∘ from-inj) (f ∘ to) ⟩
      sum μA (f ∘ to ∘ from ∘ p ∘ to)
    ≡⟨ ≡.sym (sums-ok' (f ∘ to ∘ from ∘ p)) ⟩
      sum μB (f ∘ to ∘ from ∘ p)
    ≡⟨ sum-ext μB (≡.cong f ∘ Inv.Inverse.right-inverse-of iso ∘ p) ⟩
      sum μB (f ∘ p)
    ∎
    where open ≡.≡-Reasoning

≈-refl : ∀ {A} (μA : SumProp A) → μA ≈ μA
≈-refl μA = mk Inv.id (λ f → ≡.refl)

≈-id : ∀ {A} {μA : SumProp A} → μA ≈ μA
≈-id = ≈-refl _

≈-sym : ∀ {A B}{μA : SumProp A}{μB : SumProp B} → μA ≈ μB → μB ≈ μA
≈-sym A≈B = mk (Inv.sym iso) sums-ok'
  where open _≈_ A≈B

≈-trans : ∀ {A B C}{μA : SumProp A}{μB : SumProp B}{μC : SumProp C} → μA ≈ μB → μB ≈ μC → μA ≈ μC
≈-trans A≈B B≈C = mk (iso B≈C Inv.∘ iso A≈B) (λ f → ≡.trans (sums-ok A≈B f) (sums-ok B≈C (f ∘ from A≈B)))
  where open _≈_

infix 2 _≈∎
infixr 2 _≈⟨_⟩_

_≈∎ : ∀ {A} (μA : SumProp A) → μA ≈ μA
_≈∎ = ≈-refl

_≈⟨_⟩_ : ∀ {A B C} (μA : SumProp A){μB : SumProp B}{μC : SumProp C} → μA ≈ μB → μB ≈ μC → μA ≈ μC
_ ≈⟨ A≈B ⟩ B≈C = ≈-trans A≈B B≈C

{-
Fin1≈𝟙 : μFin 1 ≈ μ𝟙
Fin1≈𝟙 = mk iso sums-ok where
  open import Relation.Binary.Sum
  iso : _
  iso = (A⊎𝟘↔A Inv.∘ Inv.id ⊎-cong Fin0↔𝟘) Inv.∘ Fin∘suc↔𝟙⊎Fin

  sums-ok : (_ : _) → _
  sums-ok f = ≡.refl
-}

𝟙+Fin : ∀ {n pf} → μ𝟙 ⊎-μ μFinSuc n ≈ μFinSuc (suc n)
𝟙+Fin {zero} {()}
𝟙+Fin {suc n} = mk iso sums-ok where
  iso : _
  iso = Inv.sym Fin∘suc↔𝟙⊎Fin

  sums-ok : (_ : _) → _
  sums-ok f = ≡.refl

𝟙×A≈A : ∀ {A}{μA : SumProp A} → μ𝟙 ×-μ μA ≈ μA
𝟙×A≈A = mk iso sums-ok where
  iso : _
  iso = 𝟙×A↔A

  sums-ok : (_ : _) → _
  sums-ok f = ≡.refl

μFinSucPres : ∀ {m n} → m ≡ n → μFinSuc m ≈ μFinSuc n
μFinSucPres eq rewrite eq = ≈-refl _

μFinPres : ∀ {m n pfm pfn} → m ≡ n → μFinSuc m {pfm} ≈ μFinSuc n {pfn}
μFinPres eq rewrite eq = ≈-refl _

  {-
Maybe-Finable : ∀ {A} (μA : SumProp A) → Finable μA → Finable (μMaybe μA)
Maybe-Finable {A} μA finA = mk card iso sums-ok where
  module FinA = Finable finA
  card = suc FinA.FinCard

  |A| : ℕ
  |A| = suc (Finable.FinCard finA)

  iso : _
  iso = (𝟙 ⊎ A)       ↔⟨ Inv.id ⊎-cong FinA.iso ⟩
        (𝟙 ⊎ Fin |A|) ↔⟨ sym Fin∘suc↔𝟙⊎Fin ⟩
        Fin (suc |A|) ∎
    where open EquationalReasoning

  sums-ok : (_ : _) → _
  sums-ok f = ≡.cong (λ x → f (inj₁ _) + x) (FinA.sums-ok _)
-}

_+μ-cong_ : ∀ {A B C D}{μA : SumProp A}{μB : SumProp B}{μC : SumProp C}{μD : SumProp D}
          → μA ≈ μC → μB ≈ μD → μA ⊎-μ μB ≈ μC ⊎-μ μD
A≈C +μ-cong B≈D = mk iso sums-ok where
  open import Relation.Binary.Sum
  iso : _
  iso = (_≈_.iso A≈C) ⊎-cong (_≈_.iso B≈D)

  sums-ok : (_ : _) → _
  sums-ok f = ≡.cong₂ _+_ (_≈_.sums-ok A≈C (f ∘ inj₁)) (_≈_.sums-ok B≈D (f ∘ inj₂))

+μ-assoc : ∀ {A B C}(μA : SumProp A)(μB : SumProp B)(μC : SumProp C)
         → (μA ⊎-μ μB) ⊎-μ μC ≈ μA ⊎-μ (μB ⊎-μ μC)
+μ-assoc μA μB μC = mk iso sums-ok where
  iso : _
  iso = ⊎-CMon.assoc _ _ _

  sums-ok : (_ : _) → _
  sums-ok f = ℕ°.+-assoc (sum μA (f ∘ inj₁ ∘ inj₁)) (sum μB (f ∘ inj₁ ∘ inj₂)) (sum μC (f ∘ inj₂))

+μ-comm : ∀ {A B}(μA : SumProp A)(μB : SumProp B)
        → μA ⊎-μ μB ≈ μB ⊎-μ μA
+μ-comm μA μB = mk iso sums-ok where
  iso : _
  iso = ⊎-CMon.comm _ _

  sums-ok : (_ : _) → _
  sums-ok f = ℕ°.+-comm (sum μA (f ∘ inj₁)) (sum μB (f ∘ inj₂))

_×μ-cong_ :  ∀ {A B C D}{μA : SumProp A}{μB : SumProp B}{μC : SumProp C}{μD : SumProp D}
          → μA ≈ μC → μB ≈ μD → μA ×-μ μB ≈ μC ×-μ μD
_×μ-cong_ {μA = μA}{μD = μD} A≈C B≈D = mk iso sums-ok where
  open import Relation.Binary.Product.Pointwise
  iso : _
  iso = _≈_.iso A≈C ×-cong _≈_.iso B≈D

  sums-ok : (_ : _) → _
  sums-ok f = ≡.trans (sum-ext μA (_≈_.sums-ok B≈D ∘ curry f))
                      (_≈_.sums-ok A≈C (λ a → sum μD (curry f a ∘ (_≈_.from B≈D))))

×μ-assoc : ∀ {A B C}(μA : SumProp A)(μB : SumProp B)(μC : SumProp C)
         → (μA ×-μ μB) ×-μ μC ≈ μA ×-μ (μB ×-μ μC)
×μ-assoc μA μB μC = mk iso sums-ok where
  iso : _
  iso = ×-CMon.assoc _ _ _

  sums-ok : (_ : _) → _
  sums-ok f = ≡.refl

×μ-comm : ∀ {A B}(μA : SumProp A)(μB : SumProp B)
        → μA ×-μ μB ≈ μB ×-μ μA
×μ-comm μA μB = mk iso sums-ok where
  iso : _
  iso = ×-CMon.comm _ _

  sums-ok : (_ : _) → _
  sums-ok f = sum-swap μA μB (curry f)

×+-distrib : ∀ {A B C}(μA : SumProp A)(μB : SumProp B)(μC : SumProp C)
           → (μA ⊎-μ μB) ×-μ μC ≈ (μA ×-μ μC) ⊎-μ (μB ×-μ μC)
×+-distrib μA μB μC = mk iso sums-ok where
  iso : _
  iso = ×⊎°.distribʳ _ _ _

  sums-ok : (_ : _) → _
  sums-ok f = ≡.refl

{-
_Suc-+_ : ∀ {m} → Suc m → ∀ n → Suc (m + n)
_Suc-+_ {zero}  () _
_Suc-+_ {suc m} _  _ = _

+-≈ : ∀ m n {pfm pfn} → (μFin m {pfm}) +μ (μFin n {pfn}) ≈ μFin (m + n) {pfm Suc-+ n}
+-≈ zero _ {()}
+-≈ _ zero {_} {()}
+-≈ (suc m) (suc n) = μFin (suc m) +μ μFin (suc n)
                    ≈⟨ {!!} ⟩
                      μFin (suc m + suc n)
                    ≈∎
-}

{-
+-≈ (suc zero) (suc n) = μFin 1 +μ μFin (suc n)
               ≈⟨ Fin1≈𝟙 +μ-cong ≈-refl (μFin (suc n)) ⟩
                μ𝟙 +μ μFinSuc n
              ≈⟨ 𝟙+Fin ⟩
                μFinSuc (suc n)
              ≈∎
+-≈ (suc (suc m)) (suc n) = μFinSuc (suc m) +μ μFinSuc n
              ≈⟨ ≈-sym 𝟙+Fin +μ-cong ≈-refl (μFinSuc n) ⟩
                (μ𝟙 +μ μFinSuc m) +μ μFinSuc n
              ≈⟨ +μ-assoc μ𝟙 (μFinSuc m) (μFinSuc n) ⟩
                μ𝟙 +μ (μFinSuc m +μ μFinSuc n)
              ≈⟨ ≈-refl μ𝟙 +μ-cong +-≈ (suc m) (suc n) ⟩
                μ𝟙 +μ μFinSuc (m + suc n)
              ≈⟨ 𝟙+Fin ⟩
                μFinSuc (suc m + suc n)
              ≈∎
              -}

{-
+-≈ : ∀ m n → (μFinSuc m) +μ (μFinSuc n) ≈ μFinSuc (m + suc n)
+-≈ zero n    = μFinSuc zero +μ μFinSuc n
              ≈⟨ Fin1≈𝟙 +μ-cong ≈-refl (μFinSuc n) ⟩
                μ𝟙 +μ μFinSuc n
              ≈⟨ 𝟙+Fin ⟩
                μFinSuc (suc n)
              ≈∎
+-≈ (suc m) n = μFinSuc (suc m) +μ μFinSuc n
              ≈⟨ ≈-sym 𝟙+Fin +μ-cong ≈-refl (μFinSuc n) ⟩
                (μ𝟙 +μ μFinSuc m) +μ μFinSuc n
              ≈⟨ +μ-assoc μ𝟙 (μFinSuc m) (μFinSuc n) ⟩
                μ𝟙 +μ (μFinSuc m +μ μFinSuc n)
              ≈⟨ ≈-refl μ𝟙 +μ-cong +-≈ m n ⟩
                μ𝟙 +μ μFinSuc (m + suc n)
              ≈⟨ 𝟙+Fin ⟩
                μFinSuc (suc m + suc n)
              ≈∎

×-≈ : ∀ m n → μFinSuc m ×μ μFinSuc n ≈ μFinSuc (n + m * suc n)
×-≈ zero n    = μFinSuc 0 ×μ μFinSuc n
              ≈⟨ Fin1≈𝟙 ×μ-cong (≈-refl (μFinSuc n)) ⟩
                μ𝟙 ×μ μFinSuc n
              ≈⟨ 𝟙×A≈A ⟩
                μFinSuc n
              ≈⟨ μFinSucPres (ℕ°.+-comm 0 n) ⟩
                μFinSuc (n + 0)
              ≈∎
×-≈ (suc m) n = μFinSuc (suc m) ×μ μFinSuc n
              ≈⟨ ≈-sym 𝟙+Fin ×μ-cong ≈-refl (μFinSuc n) ⟩
                (μ𝟙 +μ μFinSuc m) ×μ μFinSuc n
              ≈⟨ ×+-distrib μ𝟙 (μFinSuc m) (μFinSuc n) ⟩
                (μ𝟙 ×μ μFinSuc n) +μ (μFinSuc m ×μ μFinSuc n)
              ≈⟨ 𝟙×A≈A {μA = μFinSuc n} +μ-cong ×-≈ m n ⟩
                μFinSuc n +μ μFinSuc (n + m * suc n)
              ≈⟨ +-≈ n (n + m * suc n) ⟩
                μFinSuc (n + suc m * suc n)
              ≈∎

-- μA→B ≈ μFinSuc (m ^ n)
-- μB   ≈ μFinSuc m
-- μMaybe→ μA→B μB ≈ μFinSuc (m * m ^ n)

open import Data.Fin using (Fin ; zero ; suc)

Finable : ∀ {A} → SumProp A → Set
Finable μA = Σ ℕ λ FinCard → μA ≈ μFinSuc FinCard

𝟙-Finable : Finable μ𝟙
𝟙-Finable = 0 , ≈-sym Fin1≈𝟙

Fin-Finable : ∀ {n} → Finable (μFinSuc n)
Fin-Finable {n} = n , ≈-refl (μFinSuc n)

+-Finable : ∀ {A B}(μA : SumProp A)(μB : SumProp B) → Finable μA → Finable μB → Finable (μA +μ μB)
+-Finable μA μB (|A| , A≈) (|B| , B≈) = (|A| + suc |B|) ,
  ( μA +μ μB
  ≈⟨ A≈ +μ-cong B≈ ⟩
    μFinSuc |A| +μ μFinSuc |B|
  ≈⟨ +-≈ |A| |B| ⟩
    μFinSuc (|A| + suc |B|) ≈∎)

×-Finable : ∀ {A B}(μA : SumProp A)(μB : SumProp B) → Finable μA → Finable μB → Finable (μA ×μ μB)
×-Finable μA μB (|A| , A≈) (|B| , B≈) = (|B| + |A| * suc |B|) ,
  ( μA ×μ μB
  ≈⟨ A≈ ×μ-cong B≈ ⟩
    μFinSuc |A| ×μ μFinSuc |B|
  ≈⟨ ×-≈ |A| |B| ⟩
    μFinSuc (|B| + |A| * suc |B|)
  ≈∎)

module _M3 where
  open import bijection-fin
  open import Data.Fin using (Fin; zero; suc)
  open import Data.Vec.NP renaming (sum to vsum)

  sumFin : ∀ n → Sum (Fin n)
  sumFin n f = vsum (tabulate f)

  sumFin-spec : ∀ n → sumFin (suc n) ≗ sum (μFinSuc n)
  sumFin-spec zero    f = ℕ°.+-comm (f zero) 0
  sumFin-spec (suc n) f = ≡.cong (_+_ (f zero)) (sumFin-spec n (f ∘ suc))

  sumFinSUI : ∀ n f p → Injective p → sumFin n f ≡ sumFin n (f ∘ p)
  sumFinSUI n f p p-inj = count-perm f p (λ _ _ → p-inj)

  μFinSUI : ∀ {n} → StableUnderInjection (μFinSuc n)
  μFinSUI {n} p p-inj f rewrite ≡.sym (sumFin-spec n f)
                              | ≡.sym (sumFin-spec n (f ∘ p))
                              = sumFinSUI (suc n) f p p-inj
open _M3 public

StableIfFinable : ∀ {A} (μA : SumProp A) → Finable μA → StableUnderInjection μA
StableIfFinable μA (_ , A≈Fin)
  = _≈_.StableUnder≈ (≈-sym A≈Fin) μFinSUI

Decomposable : ★ → ★₁
Decomposable A = (A ↔ 𝟙) ⊎ (∃ λ (B : ★) → A ↔ Maybe B)

open EquationalReasoning

dec-iso : ∀ {A B} → (A ↔ B) → Decomposable A → Decomposable B
dec-iso A↔B (inj₁ A↔𝟙) = inj₁ (A↔𝟙 Inv.∘ sym A↔B)
dec-iso A↔B (inj₂ (C , A↔MaybeC)) = inj₂ (C , A↔MaybeC Inv.∘ sym A↔B)

Maybe×⊎ : ∀ {A B : ★} → (Maybe A × B) ↔ (B ⊎ (A × B))
Maybe×⊎ {A} {B} = (Maybe A × B)   ↔⟨ Maybe↔𝟙⊎ ×-cong Inv.id ⟩
                  ((𝟙 ⊎ A) × B)   ↔⟨ ×⊎°.distribʳ B 𝟙 A ⟩
                  (𝟙 × B ⊎ A × B) ↔⟨ 𝟙×A↔A ⊎-cong Inv.id ⟩
                  (B ⊎ (A × B))   ∎

dec× : ∀ {A B} → Decomposable A → Decomposable B → Decomposable (A × B)
dec× {A} {B} (inj₁ A↔𝟙) dB = dec-iso (B      ↔⟨ sym 𝟙×A↔A ⟩
                                     (𝟙 × B) ↔⟨ sym A↔𝟙 ×-cong Inv.id ⟩
                                     (A × B) ∎) dB
dec× {A} {B} dA (inj₁ B↔𝟙) = dec-iso (A      ↔⟨ sym A×𝟙↔A ⟩
                                     (A × 𝟙) ↔⟨ Inv.id ×-cong sym B↔𝟙 ⟩
                                     (A × B) ∎) dA
dec× {A} {B} (inj₂ (C , A↔1+C)) (inj₂ (D , B↔1+D))
  = inj₂ (_ , Maybe-⊎ Inv.∘ Maybe×⊎ Inv.∘ A↔1+C ×-cong B↔1+D)

dec+ : ∀ {A B} → Decomposable A → Decomposable B → Decomposable (A ⊎ B)
dec+ {A} {B} (inj₁ A↔𝟙)         dB = inj₂ (B , sym Maybe↔𝟙⊎ Inv.∘ A↔𝟙 ⊎-cong Inv.id)
dec+ {A} {B} (inj₂ (C , A↔1+C)) dB = inj₂ ((C ⊎ B) , sym Maybe↔𝟙⊎
                                               Inv.∘ ⊎-CMon.assoc 𝟙 C B
                                               Inv.∘ (Maybe↔𝟙⊎ Inv.∘ A↔1+C) ⊎-cong Inv.id)

{-
dB = dec-iso {!!} dB
  where dec : Decomposable (A × B)
{-
 -- B     + C×B
 -- 1×B   + C×B
 -- (1+C) × B
 -- A     × B
 -}

Stable× : ∀ {A} (μA : SumProp A) {B} (μB : SumProp B)
                (suiA : StableUnderInjection μA)
                (suiB : StableUnderInjection μB)
              → StableUnderInjection (μA ×μ μB)
Stable× μA μB suiA suiB = {!!}

        -- -}
        -- -}
        -- -}
        -- -}

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
module Numeral.Finite.Proofs where

import Lvl
open import Data
open import Data.Boolean.Stmt
open import Functional
open import Logic.Classical
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Logic.Predicate
open import Numeral.Finite
import      Numeral.Finite.Oper.Comparisons as 𝕟
open import Numeral.Natural hiding (𝐏)
open import Numeral.Natural.Function
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.Comparisons
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Decidable
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function.Domain
open import Syntax.Number
open import Type.Properties.Decidable
open import Type.Properties.Decidable.Proofs

private variable N : ℕ

bounded : ∀{N : ℕ}{n : 𝕟(𝐒(N))} → (𝕟-to-ℕ(n) < 𝐒(N))
bounded{_}   {𝟎}    = [≤]-with-[𝐒] ⦃ [≤]-minimum ⦄
bounded{𝐒(N)}{𝐒(n)} = [≤]-with-[𝐒] ⦃ bounded{N}{n} ⦄

ℕ-to-𝕟-eq : ∀{M N n} ⦃ nM : IsTrue(n <? M) ⦄ ⦃ nN : IsTrue(n <? N) ⦄ → IsTrue(ℕ-to-𝕟 n {n = M} ⦃ nM ⦄ 𝕟.≡? ℕ-to-𝕟 n {n = N} ⦃ nN ⦄)
ℕ-to-𝕟-eq {𝐒 M} {𝐒 N} {𝟎}   = [⊤]-intro
ℕ-to-𝕟-eq {𝐒 M} {𝐒 N} {𝐒 n} = ℕ-to-𝕟-eq {M} {N} {n}

𝕟-to-ℕ-preserve-eq : ∀{M N}{m : 𝕟(M)}{n : 𝕟(N)} → IsTrue(m 𝕟.≡? n) → (𝕟-to-ℕ m ≡ 𝕟-to-ℕ n)
𝕟-to-ℕ-preserve-eq {𝐒 M} {𝐒 N} {𝟎}   {𝟎}   [⊤]-intro = [≡]-intro
𝕟-to-ℕ-preserve-eq {𝐒 M} {𝐒 N} {𝐒 m} {𝐒 n}           = [≡]-with(𝐒) ∘ 𝕟-to-ℕ-preserve-eq {M} {N} {m} {n}

𝕟-to-ℕ-preserve-gt : ∀{M N}{m : 𝕟(M)}{n : 𝕟(N)} → IsTrue(m 𝕟.>? n) → (𝕟-to-ℕ m > 𝕟-to-ℕ n)
𝕟-to-ℕ-preserve-gt {𝐒 M} {𝐒 N} {𝐒 m} {𝟎}   [⊤]-intro = [≤]-with-[𝐒] ⦃ [≤]-minimum ⦄
𝕟-to-ℕ-preserve-gt {𝐒 M} {𝐒 N} {𝐒 m} {𝐒 n} x         = [≤]-with-[𝐒] ⦃ 𝕟-to-ℕ-preserve-gt {M} {N} {m} {n} x ⦄

𝕟-to-ℕ-preserve-lt : ∀{M N}{m : 𝕟(M)}{n : 𝕟(N)} → IsTrue(m 𝕟.<? n) → (𝕟-to-ℕ m < 𝕟-to-ℕ n)
𝕟-to-ℕ-preserve-lt {𝐒 M} {𝐒 N} {𝟎}   {𝐒 n} [⊤]-intro = [≤]-with-[𝐒] ⦃ [≤]-minimum ⦄
𝕟-to-ℕ-preserve-lt {𝐒 M} {𝐒 N} {𝐒 m} {𝐒 n} x         = [≤]-with-[𝐒] ⦃ 𝕟-to-ℕ-preserve-lt {M} {N} {m} {n} x ⦄

𝕟-to-ℕ-preserve-ge : ∀{M N}{m : 𝕟(M)}{n : 𝕟(N)} → IsTrue(m 𝕟.≥? n) → (𝕟-to-ℕ m ≥ 𝕟-to-ℕ n)
𝕟-to-ℕ-preserve-ge {𝐒 M} {𝐒 N} {𝟎}   {𝟎}   [⊤]-intro = [≤]-minimum
𝕟-to-ℕ-preserve-ge {𝐒 M} {𝐒 N} {𝐒 n} {𝟎}   [⊤]-intro = [≤]-minimum
𝕟-to-ℕ-preserve-ge {𝐒 M} {𝐒 N} {𝐒 m} {𝐒 n} x         = [≤]-with-[𝐒] ⦃ 𝕟-to-ℕ-preserve-ge {M} {N} {m} {n} x ⦄

𝕟-to-ℕ-preserve-le : ∀{M N}{m : 𝕟(M)}{n : 𝕟(N)} → IsTrue(m 𝕟.≤? n) → (𝕟-to-ℕ m ≤ 𝕟-to-ℕ n)
𝕟-to-ℕ-preserve-le {𝐒 M} {𝐒 N} {𝟎}   {𝟎}   [⊤]-intro = [≤]-minimum
𝕟-to-ℕ-preserve-le {𝐒 M} {𝐒 N} {𝟎}   {𝐒 n} [⊤]-intro = [≤]-minimum
𝕟-to-ℕ-preserve-le {𝐒 M} {𝐒 N} {𝐒 m} {𝐒 n} x         = [≤]-with-[𝐒] ⦃ 𝕟-to-ℕ-preserve-le {M} {N} {m} {n} x ⦄

𝕟-to-ℕ-preserve-ne : ∀{M N}{m : 𝕟(M)}{n : 𝕟(N)} → IsTrue(m 𝕟.≢? n) → (𝕟-to-ℕ m ≢ 𝕟-to-ℕ n)
𝕟-to-ℕ-preserve-ne {𝐒 M} {𝐒 N} {𝟎}   {𝐒 n} _ ()
𝕟-to-ℕ-preserve-ne {𝐒 M} {𝐒 N} {𝐒 m} {𝟎}   _ ()
𝕟-to-ℕ-preserve-ne {𝐒 M} {𝐒 N} {𝐒 m} {𝐒 n} x p = 𝕟-to-ℕ-preserve-ne {M} {N} {m} {n} x (injective(𝐒) p)

congruence-ℕ-to-𝕟 : ∀ ⦃ pos : IsTrue(positive? N) ⦄ {x} ⦃ px : IsTrue(x <? N) ⦄ {y} ⦃ py : IsTrue(y <? N) ⦄ → (x ≡ y) → (ℕ-to-𝕟 x {N} ⦃ px ⦄ ≡ ℕ-to-𝕟 y ⦃ py ⦄)
congruence-ℕ-to-𝕟 [≡]-intro = [≡]-intro

𝕟-ℕ-inverse : ∀{N n} ⦃ nN : IsTrue(n <? N) ⦄ → (𝕟-to-ℕ {n = N}(ℕ-to-𝕟 n) ≡ n)
𝕟-ℕ-inverse {𝐒 N}{𝟎}   = [≡]-intro
𝕟-ℕ-inverse {𝐒 N}{𝐒 n} = [≡]-with(𝐒) (𝕟-ℕ-inverse {N}{n})

ℕ-𝕟-inverse : ∀{N}{n : 𝕟(𝐒(N))} → (ℕ-to-𝕟(𝕟-to-ℕ n) ⦃ [↔]-to-[→] decider-true (bounded{n = n}) ⦄ ≡ n)
ℕ-𝕟-inverse {𝟎}   {𝟎}   = [≡]-intro
ℕ-𝕟-inverse {𝐒 N} {𝟎}   = [≡]-intro
ℕ-𝕟-inverse {𝐒 N} {𝐒 n} = [≡]-with(𝐒) (ℕ-𝕟-inverse{N}{n})

instance
  [<]-of-𝕟-to-ℕ : ∀{N : ℕ}{n : 𝕟(N)} → (𝕟-to-ℕ (n) < N)
  [<]-of-𝕟-to-ℕ {𝟎} {()}
  [<]-of-𝕟-to-ℕ {𝐒 N} {𝟎}   = [≤]-with-[𝐒]
  [<]-of-𝕟-to-ℕ {𝐒 N} {𝐒 n} = [≤]-with-[𝐒] ⦃ [<]-of-𝕟-to-ℕ {N} {n} ⦄

instance
  [𝐒]-injective : ∀{N : ℕ} → Injective(𝕟.𝐒{N})
  Injective.proof [𝐒]-injective [≡]-intro = [≡]-intro

[≡][≡?]-equivalence : ∀{n}{i j : 𝕟(n)} → (i ≡ j) ↔ IsTrue(i 𝕟.≡? j)
[≡][≡?]-equivalence {𝐒 n} {𝟎}   {𝟎}   = [↔]-intro (const [≡]-intro) (const [⊤]-intro)
[≡][≡?]-equivalence {𝐒 n} {𝟎}   {𝐒 j} = [↔]-intro (\()) (\())
[≡][≡?]-equivalence {𝐒 n} {𝐒 i} {𝟎}   = [↔]-intro (\()) (\())
[≡][≡?]-equivalence {𝐒 n} {𝐒 i} {𝐒 j} = [∧]-map ([≡]-with(𝐒) ∘_) (_∘ injective(𝐒)) ([≡][≡?]-equivalence {n} {i} {j})

instance
  [≡][𝕟]-decider : ∀{n} → Decider(2)(_≡_ {T = 𝕟(n)})(𝕟._≡?_)
  [≡][𝕟]-decider {𝐒 n} {𝟎}   {𝟎}   = true [≡]-intro
  [≡][𝕟]-decider {𝐒 n} {𝟎}   {𝐒 y} = false \()
  [≡][𝕟]-decider {𝐒 n} {𝐒 x} {𝟎}   = false \()
  [≡][𝕟]-decider {𝐒 n} {𝐒 x} {𝐒 y} = step{f = id} (true ∘ [≡]-with(𝐒)) (false ∘ contrapositiveᵣ(injective(𝐒))) ([≡][𝕟]-decider {n} {x} {y})

maximum-0 : (maximum{N} ≡ 𝟎) → (N ≡ 𝟎)
maximum-0 {𝟎} _ = [≡]-intro


text:
open import Prelude
open import core

module grounding where
  grounding : ∀{ τ1 τ2} →
                             τ1 ▸gnd τ2 →
                             ((τ2 ground) × (τ1 ~ τ2) × (τ1 ≠ τ2))
  grounding (MGArr x) = GHole , TCArr TCHole1 TCHole1 , 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:
{-
Module in which the Grothendieck Group ("Groupification") of a commutative monoid is defined.
-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommMonoid.GrothendieckGroup where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.CommMonoid
open import Cubical.Algebra.CommMonoid.CommMonoidProd
open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.AbGroup

open import Cubical.HITs.SetQuotients.Base
open import Cubical.HITs.SetQuotients.Properties

open import Cubical.Relation.Binary.Base

private
  variable
    ℓ ℓ' : Level

module _ (M : CommMonoid ℓ) where
  open BinaryRelation

  M² : CommMonoid _
  M² = CommMonoidProd M M

  open CommMonoidStr ⦃...⦄
  private
    instance
      _ = snd M
      _ = snd M²

  R : ⟨ M² ⟩  → ⟨ M² ⟩ → Type _
  R (a₁ , b₁) (a₂ , b₂) =  Σ[ k ∈ ⟨ M ⟩ ] k · (a₁ · b₂) ≡ k · (b₁ · a₂)

  M²/R : Type _
  M²/R = ⟨ M² ⟩ / R

  0/R : M²/R
  0/R = [ ε , ε ]

  private
    _+/_ : M²/R → M²/R → M²/R
    x +/ y = setQuotBinOp isReflR isReflR _·_ isCongR x y
      where
      isReflR : isRefl R
      isReflR (a , b) = ε , cong (ε ·_) (·Comm a b)

      isCongR : ∀ u u' v v' → R u u' → R v v' → R (u · v) (u' · v')
      isCongR (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) (a₄ , b₄) (k , p) (s , q) = k · s , proof
        where
        proof =
          (k · s) · ((a₁ · a₃) · (b₂ · b₄)) ≡⟨ lemma ⟩
          (k · (a₁ · b₂)) · (s · (a₃ · b₄)) ≡⟨ cong₂ _·_ p q ⟩
          (k · (b₁ · a₂)) · (s · (b₃ · a₄)) ≡⟨ sym lemma ⟩
          (k · s) · ((b₁ · b₃) · (a₂ · a₄)) ∎
            where
            rExp : ∀ {x y z} → x ≡ y → x · z ≡ y · z
            rExp r = cong₂ _·_ r refl

            lExp : ∀ {x y z} → x ≡ y → z · x ≡ z · y
            lExp r = cong₂ _·_ refl r

            -- remove proof when MonoidSolver is done
            lemma : ∀ {k s a b c d} → (k · s) · ((a · b) · (c · d)) ≡ (k · (a · c)) · (s · (b · d))
            lemma = sym (·Assoc _ _ _) ∙ lExp (
                                   (·Assoc _ _ _) ∙ (·Assoc _ _ _) ∙ rExp (
                                       ·Comm _ _ ∙ (·Assoc _ _ _) ∙ (·Assoc _ _ _) ∙ rExp (
                                            ·Comm _ _ ∙ (·Assoc _ _ _)
                                       ) ∙ sym (·Assoc _ _ _)
                                   ) ∙ sym (·Assoc _ _ _) ∙ lExp (sym (·Assoc _ _ _))
                              ) ∙ (·Assoc _ _ _)

    -/_ : M²/R → M²/R
    -/_ = setQuotUnaryOp swap h
      where
      swap : ⟨ M² ⟩  → ⟨ M² ⟩
      swap = λ (a , b) → b , a

      h : ∀ u v → R u v → R (swap u) (swap v)
      h _ _ (k , p) = k , sym p

    assoc/R : (x y z : M²/R) → x +/ ( y +/ z) ≡ (x +/ y) +/ z
    assoc/R = elimProp3 (λ x y z → squash/ _ _) (λ u v w → cong [_] (·Assoc _ _ _))

    rid/R : (x : M²/R) → x +/ 0/R ≡ x
    rid/R = elimProp (λ x → squash/ _ _) (λ u → cong [_] (·IdR u))

    rinv/R : (x : M²/R) → x +/ (-/ x) ≡ 0/R
    rinv/R = elimProp (λ x → squash/ _ _)
                      (λ (a , b) →  eq/ _ _ (ε , cong (λ x → ε · (x · ε)) (·Comm _ _)))

    comm/R : (x y : M²/R) → x +/ y ≡ y +/ x
    comm/R = elimProp2 (λ x y → squash/ _ _) (λ u v → cong [_] (·Comm _ _))

  asAbGroup : AbGroup ℓ
  asAbGroup = makeAbGroup 0/R _+/_ -/_ squash/ assoc/R rid/R rinv/R comm/R

Groupification : CommMonoid ℓ → AbGroup ℓ
Groupification M = asAbGroup M

module UniversalProperty (M : CommMonoid ℓ) where
  open IsMonoidHom
  open CommMonoidStr ⦃...⦄

  private
    instance
      _ = snd M

{-
The "groupification" of a monoid comes with a universal morphism and a universal property:

            M ----- ∀φ -----> A
             \               Λ
              \             /
       universalHom    ∃! inducedHom
                \         /
                 V       /
             Groupification M
-}

  universalHom : CommMonoidHom M (AbGroup→CommMonoid (Groupification M))
  fst universalHom = λ m → [ m , ε ]
  pres· (snd universalHom) =
    λ _ _ → eq/ _ _ (ε , cong (ε ·_) (·Comm _ _ ∙ cong₂ _·_ (·IdR ε) refl))
  presε (snd universalHom) = refl

  private
    i = fst universalHom

  module _ {A : AbGroup ℓ} (φ : CommMonoidHom M (AbGroup→CommMonoid A)) where
    open IsGroupHom

    open GroupTheory (AbGroup→Group A)

    open AbGroupStr ⦃...⦄ using (-_; _-_; _+_; +InvR; +InvL)
    private
      instance
        AAsGroup  = snd A
        MAsGroup  = snd (Groupification M)
        AAsMonoid = snd (AbGroup→CommMonoid A)

    private
      module φ = IsMonoidHom (snd φ)
      f = fst φ

    inducedHom : AbGroupHom (Groupification M) A
    fst inducedHom = elim (λ x → isSetAbGroup A) g proof
        where
        g = λ (a , b) → f a - f b
        proof : (u v : ⟨ M² M ⟩) (r : R M u v) → g u ≡ g v
        proof _ _ (k , p) = lemma (lemma₂ p)
            where
            lemma₂ : ∀ {k a b c d} → k · (a · d) ≡ k · (b · c) → f a + f d ≡ f b + f c
            lemma₂ {k} {a} {b} {c} {d} p =
              f a + f d   ≡⟨ sym (φ.pres· _ _) ⟩
              f (a · d)   ≡⟨ ·CancelL _ (sym (φ.pres· _ _) ∙ (cong f p) ∙ φ.pres· _ _) ⟩
              f (b · c)   ≡⟨ φ.pres· _ _ ⟩
              f b + f c   ∎

            lemma : ∀ {a b c d} → f a + f d ≡ f b + f c → f a - f b ≡ f c - f d
            lemma {a} {b} {c} {d} p =
              f a - f b
                ≡⟨ cong (λ x → x - f b) (sym (·IdR _)) ⟩
              f a + ε - f b
                ≡⟨ cong (λ x → f a + x - f b) (sym (+InvR _)) ⟩
              f a + (f d - f d) - f b
                ≡⟨ cong (λ x → x - f b) (·Assoc _ _ _) ⟩
              f a + f d - f d - f b
                ≡⟨ cong (λ x → x - f d - f b) p ⟩
              f b + f c - f d - f b
                ≡⟨ ·Comm _ _ ∙ ·Assoc _ _ _ ⟩
              (- f b + (f b + f c)) - f d
                ≡⟨ cong (λ x → x - f d) (·Assoc _ _ _) ⟩
              ((- f b + f b) + f c) - f d
                ≡⟨ cong (λ x → (x + f c) - f d) (+InvL _) ∙ sym (·Assoc _ _ _) ∙ ·IdL _ ⟩
              f c - f d
                ∎

    pres· (snd inducedHom) = elimProp2 (λ _ _ → isSetAbGroup A _ _) proof
      where
        rExp : ∀ {x y z} → x ≡ y → x + z ≡ y + z
        rExp r = cong₂ _+_ r refl

        lExp : ∀ {x y z} → x ≡ y → z + x ≡ z + y
        lExp r = cong₂ _+_ refl r

        proof : ((a , b) (c , d) : ⟨ M² M ⟩) → (f (a · c)) - (f (b · d)) ≡ (f a - f b) + (f c - f d)
        proof (a , b) (c , d) =
          f (a · c) - f (b · d)     ≡⟨ cong₂ _-_ (φ.pres· _ _) (φ.pres· _ _) ⟩
          (f a + f c) - (f b + f d) ≡⟨ lExp (invDistr _ _ ∙ ·Comm _ _) ∙ ·Assoc _ _ _ ⟩
          ((f a + f c) - f b) - f d ≡⟨ lemma ⟩
          (f a - f b) + (f c - f d) ∎
          where
            lemma = rExp (sym (·Assoc _ _ _) ∙ lExp (·Comm _ _) ∙ ·Assoc _ _ _) ∙ sym (·Assoc _ _ _)

    pres1 (snd inducedHom)   = +InvR _
    presinv (snd inducedHom) = elimProp (λ _ → isSetAbGroup A _ _)
                                        (λ _ → sym (invDistr _ _ ∙ cong₂ _-_ (invInv _) refl))

    solution : (m : ⟨ M ⟩) → (fst inducedHom) (i m) ≡ f m
    solution m = cong ((f m)+_) ((cong (-_) φ.presε) ∙ inv1g) ∙ ·IdR _

    unique : (ψ : AbGroupHom (Groupification M) A)
             → (ψIsSolution : (m : ⟨ M ⟩) → ψ .fst (i m) ≡ f m)
             → (u : ⟨ M² M ⟩) → ψ .fst [ u ] ≡ inducedHom .fst [ u ]
    unique ψ ψIsSolution (a , b) =
       ψ .fst [ a , b ]                    ≡⟨ lemma ⟩
       ψ .fst ([ a , ε ] - [ b , ε ])      ≡⟨ (snd ψ).pres· _ _ ∙ cong₂ _+_ refl ((snd ψ).presinv _) ⟩
       ψ .fst [ a , ε ] - ψ .fst [ b , ε ] ≡⟨ cong₂ _-_ (ψIsSolution a) (ψIsSolution b) ⟩
       f a - f b                           ∎
       where
         lemma = cong (ψ .fst) (eq/ _ _ (ε , cong (ε ·_) (·Assoc _ _ _ ∙ ·Comm _ _)))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --with-K #-}

open import Level using (Level)

open import Axiom.UniquenessOfIdentityProofs.WithK using (uip)

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Data.Nat using (ℕ)
open import Data.Vec using (Vec)

open import FLA.Axiom.Extensionality.Propositional
open import FLA.Algebra.Structures
open import FLA.Algebra.LinearAlgebra
open import FLA.Algebra.LinearAlgebra.Properties
open import FLA.Algebra.LinearMap

module FLA.Algebra.LinearMap.Properties where

private
  variable
    ℓ : Level
    A : Set ℓ
    m n p q : ℕ
    ⦃ F ⦄ : Field A

-------------------------------------------------------------------------------
--                  LinearMap without the proofs: LinearMap↓                 --
-------------------------------------------------------------------------------

private
  data _⊸↓_ {A : Set ℓ} ⦃ F : Field A ⦄ (m n : ℕ) : Set ℓ where
    LM↓ : (Vec A m → Vec A n) → m ⊸↓ n

  _·ˡᵐ↓_ : ⦃ F : Field A ⦄ → m ⊸↓ n → Vec A m → Vec A n
  _·ˡᵐ↓_ (LM↓ f) = f

  -- Choose 20 since function application is assumed higher than almost anything
  infixr 20 _·ˡᵐ↓_

  L→L↓ : ⦃ F : Field A ⦄ → m ⊸ n → m ⊸↓ n
  L→L↓ record { f = f } = LM↓ f

  L↓→L : ⦃ F : Field A ⦄
        → (L↓ : m ⊸↓ n)
        → (f[u+v]≡f[u]+f[v] : (u v : Vec A m)
                             → L↓ ·ˡᵐ↓ (u +ⱽ v) ≡ L↓ ·ˡᵐ↓ u +ⱽ L↓ ·ˡᵐ↓ v)
        → (f[c*v]≡c*f[v] : (c : A) → (v : Vec A m)
                          → L↓ ·ˡᵐ↓ (c ∘ⱽ v) ≡ c ∘ⱽ (L↓ ·ˡᵐ↓ v))
        → m ⊸ n
  L↓→L (LM↓ f) f[u+v]≡f[u]+f[v] f[c*v]≡c*f[v] =
    record
      { f = f
      ; f[u+v]≡f[u]+f[v] = f[u+v]≡f[u]+f[v]
      ; f[c*v]≡c*f[v] = f[c*v]≡c*f[v]
      }

  f[u+v]≡f[u]+f[v]-UIP : {ℓ : Level} {A : Set ℓ} {m n : ℕ} → ⦃ F : Field A ⦄
    → (f : Vec A m → Vec A n)
    → (p q : (u v : Vec A m)
            → f (u +ⱽ v) ≡ f u +ⱽ f v)
    → p ≡ q
  f[u+v]≡f[u]+f[v]-UIP f p q =
    extensionality (λ u → extensionality (λ v → t f p q u v))
    where
      t : {ℓ : Level} {A : Set ℓ} {m n : ℕ} → ⦃ F : Field A ⦄
        → (f : Vec A m → Vec A n)
        → (p q : (u v : Vec A m)
                → f (u +ⱽ v) ≡ f u +ⱽ f v)
        → (u v : Vec A m) → p u v ≡ q u v
      t f p q u v = uip (p u v) (q u v)

  f[c*v]≡c*f[v]-UIP : {ℓ : Level} {A : Set ℓ} {m n : ℕ} → ⦃ F : Field A ⦄
                    → (f : Vec A m → Vec A n)
                    → (p q : (c : A) (v : Vec A m) → f (c ∘ⱽ v) ≡ c ∘ⱽ (f v))
                    → p ≡ q
  f[c*v]≡c*f[v]-UIP f p q =
    extensionality (λ c → extensionality (λ v → t f p q c v))
    where
      t : {ℓ : Level} {A : Set ℓ} {m n : ℕ} → ⦃ F : Field A ⦄
        → (f : Vec A m → Vec A n)
        → (p q : (c : A) (v : Vec A m) → f (c ∘ⱽ v) ≡ c ∘ⱽ (f v))
        → (c : A) (v : Vec A m) → p c v ≡ q c v
      t f p q c v = uip (p c v) (q c v)

  L↓≡→L≡ : ⦃ F : Field A ⦄ → (C D : m ⊸ n)
          → (L→L↓ C ≡ L→L↓ D) → C ≡ D
  L↓≡→L≡ record { f = f
                 ; f[u+v]≡f[u]+f[v] = f[u+v]≡f[u]+f[v]ᶜ
                 ; f[c*v]≡c*f[v] = f[c*v]≡c*f[v]ᶜ
                 }
          record { f = .f
                 ; f[u+v]≡f[u]+f[v] = f[u+v]≡f[u]+f[v]ᵈ
                 ; f[c*v]≡c*f[v] = f[c*v]≡c*f[v]ᵈ
                 }
          refl
    rewrite
      f[u+v]≡f[u]+f[v]-UIP f f[u+v]≡f[u]+f[v]ᶜ f[u+v]≡f[u]+f[v]ᵈ
    | f[c*v]≡c*f[v]-UIP f f[c*v]≡c*f[v]ᶜ f[c*v]≡c*f[v]ᵈ
    = refl

-------------------------------------------------------------------------------
--                   LinearMap Proofs via LinearMap↓ Proofs                  --
-------------------------------------------------------------------------------

module _ {ℓ : Level} {A : Set ℓ} ⦃ F : Field A ⦄ where
  open Field F
  open _⊸_

  +ˡᵐ-comm : (L R : m ⊸ n)
          → L +ˡᵐ R ≡ R +ˡᵐ L
  +ˡᵐ-comm L R = L↓≡→L≡ (L +ˡᵐ R) (R +ˡᵐ L) (+ˡᵐ-comm↓ L R)
    where
      +ⱽ-comm-ext : (f g : Vec A m → Vec A n)
        → (λ v → f v +ⱽ g v) ≡ (λ v → g v +ⱽ f v)
      +ⱽ-comm-ext f g = extensionality (λ v → +ⱽ-comm (f v) (g v))

      +ˡᵐ-comm↓ : (L R : m ⊸ n)
              → L→L↓ (L +ˡᵐ R) ≡ L→L↓ (R +ˡᵐ L)
      +ˡᵐ-comm↓ L R = cong LM↓ (+ⱽ-comm-ext (L ·ˡᵐ_) (R ·ˡᵐ_))

  *ˡᵐ-distr-+ˡᵐₗ : (X : n ⊸ m) → (Y Z : p ⊸ n)
                → (X *ˡᵐ (Y +ˡᵐ Z)) ≡ (X *ˡᵐ Y +ˡᵐ X *ˡᵐ Z)
  *ˡᵐ-distr-+ˡᵐₗ X Y Z = L↓≡→L≡ (X *ˡᵐ (Y +ˡᵐ Z)) ((X *ˡᵐ Y +ˡᵐ X *ˡᵐ Z))
                                (*ˡᵐ-distr-+ˡᵐₗ↓ X Y Z)
    where
      *-distr-+ⱽ : (X : n ⊸ m) → (Y Z : p ⊸ n)
        → (λ v → X ·ˡᵐ (Y ·ˡᵐ v +ⱽ Z ·ˡᵐ v)) ≡
          (λ v → X ·ˡᵐ (Y ·ˡᵐ v) +ⱽ X ·ˡᵐ (Z ·ˡᵐ v))
      *-distr-+ⱽ X Y Z = extensionality
        (λ v → f[u+v]≡f[u]+f[v] X (Y ·ˡᵐ v) (Z ·ˡᵐ v))

      *ˡᵐ-distr-+ˡᵐₗ↓ : (X : n ⊸ m) → (Y Z : p ⊸ n)
                      → L→L↓ (X *ˡᵐ (Y +ˡᵐ Z)) ≡ L→L↓ (X *ˡᵐ Y +ˡᵐ X *ˡᵐ Z)
      *ˡᵐ-distr-+ˡᵐₗ↓ X Y Z = cong LM↓ (*-distr-+ⱽ X Y Z)

  *ˡᵐ-distr-+ˡᵐᵣ : (X Y : n ⊸ m) → (Z : p ⊸ n)
                → (X +ˡᵐ Y) *ˡᵐ Z ≡ X *ˡᵐ Z +ˡᵐ Y *ˡᵐ Z
  *ˡᵐ-distr-+ˡᵐᵣ X Y Z = L↓≡→L≡ ((X +ˡᵐ Y) *ˡᵐ Z) (X *ˡᵐ Z +ˡᵐ Y *ˡᵐ Z)
                                (*ˡᵐ-distr-+ˡᵐᵣ↓ X Y Z)
    where
      *ˡᵐ-distr-+ˡᵐᵣ↓ : (X Y : n ⊸ m) → (Z : p ⊸ n)
                      → L→L↓ ((X +ˡᵐ Y) *ˡᵐ Z) ≡ L→L↓ (X *ˡᵐ Z +ˡᵐ Y *ˡᵐ Z)
      *ˡᵐ-distr-+ˡᵐᵣ↓ X Y Z = cong LM↓ refl

max_stars_repo_name: turion/functional-linear-algebra

max_issues_repo_name: turion/functional-linear-algebra

max_forks_repo_name: turion/functional-linear-algebra


text:
open import Proc

module Mission (param : Param) where

import Interp
import Hear
open import Basics

private
  open module P = Process param
  open module I = Interp param
  open module H = Hear param
    renaming ( sound    to hear-sound
             ; uniq     to hear-uniq
             ; complete to hear-complete
             )

open Tran

data IsRefuse {a : U}{p : Proc a} : Result p -> Set where
  isRefuse : {s : Silent p} -> IsRefuse (refuse s)

completeS : {a : U}{p : Proc a}(g : Guard p) ->
           Silent p -> (oracle : Oracle) -> IsRefuse (step g oracle)
completeS og           silent-o          oracle = isRefuse
completeS (>g f)       silent->          oracle = isRefuse
completeS (_ !g _)     ()                oracle
completeS (_ ! _ +g _) ()                oracle
completeS (g1 ||g g2)  (silent-|| s1 s2) oracle
  with step g1 (nextOracle oracle)
       | completeS g1 s1 (nextOracle oracle)
       | step g2 (nextOracle oracle)
       | completeS g2 s2 (nextOracle oracle)
       | prophecy oracle
... | refuse _ | _  | refuse _ | _  | _     = isRefuse
... | speak _  | () | speak _  | _  | _
... | refuse _ | _  | speak _  | () | _
... | speak _  | () | speak _  | _  | left
... | speak _  | _  | speak _  | () | right
... | speak _  | _  | refuse _ | () | _
completeS (φ /|g g)    (silent-/| s)  oracle with step g oracle
                                                | completeS g s oracle
... | speak _  | ()
... | refuse _ | _ = isRefuse
completeS (defg x g)   (silent-def s) oracle with step g oracle
                                                | completeS g s oracle
... | speak _  | ()
... | refuse _ | _ = isRefuse

theOracle : {a : U}{p : Proc a}{w : LT a}{q : Proc a} ->
            p -! w !-> q -> Oracle
theOracle tx-!        = anyOracle
theOracle tx-+        = anyOracle
theOracle (tx-!| s r) = ocons left  (theOracle s)
theOracle (tx-|! r s) = ocons right (theOracle s)
theOracle (tx-/| s)   = theOracle s
theOracle (tx-def s)  = theOracle s

data IsSpeak {a : U}{p : Proc a}(w : LT a)(q : Proc a) : Result p -> Set where
  isSpeak : {r : p -! w !-> q} -> IsSpeak w q (speak r)

completeT : {a : U}{p : Proc a}(g : Guard p){w : LT a}{q : Proc a} ->
            (r : p -! w !-> q) -> IsSpeak w q (step g (\x -> theOracle r x))
completeT og           ()
completeT (>g _)       ()
completeT (w !g p)     tx-!        = isSpeak
completeT (w ! p +g f) tx-+        = isSpeak
completeT (g1 ||g  g2) (tx-!| s r) with step g1 (\x -> theOracle s x)
                                      | step g2 (\x -> theOracle s x)
                                      | completeT g1 s
                                      | hear-complete g2 r
... | .(speak _) | refuse _ | isSpeak | refl = isSpeak
... | .(speak _) | speak _  | isSpeak | refl = isSpeak
completeT (g1 ||g  g2) (tx-|! r s) with step g1 (\x -> theOracle s x)
                                      | step g2 (\x -> theOracle s x)
                                      | hear-complete g1 r
                                      | completeT g2 s
... | refuse _ | .(speak _) | refl | isSpeak = isSpeak
... | speak _  | .(speak _) | refl | isSpeak = isSpeak
completeT (φ /|g g) (tx-/| s) with step g (\x -> theOracle s x)
                                 | completeT g s
... | ._ | isSpeak = isSpeak
completeT (defg x g)  (tx-def s) with step g (\x -> theOracle s x)
                                    | completeT g s
... | ._ | isSpeak = isSpeak

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
{-# OPTIONS --warning=error #-}

module UselessPrivatePrivate where

private
  private
    postulate
      A : Set


text:
module optics where

  open import Function
  open import Data.Nat
  open import Data.Vec
  open import Agda.Builtin.Sigma
  open import Data.Product
  import Relation.Binary.PropositionalEquality as Eq
  open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)

  record TraversalF (S T A B : Set) : Set where
    field
      extract : Σ[ f ∈ (S -> ℕ) ] ((s : S) -> Vec A (f s) × (Vec B (f s) -> T))

  record Traversal (S T A B : Set) : Set where
    field
      --extract : S -> ∃[ n ] (Vec A n × (Vec B n -> T))
      extract : S -> Σ[ n ∈ ℕ ] Vec A n × (Vec B n -> T)

    get : (s : S) -> Vec A (fst (extract s))
    get = fst ∘ snd ∘ extract

    put : (s : S) -> Vec B (fst (extract s)) -> T
    put = snd ∘ snd ∘ extract

  record TraversalLaws (S A : Set) (t : Traversal S S A A): Set where
    open Traversal t public
    field
      get-put-law : (s : S) -> (put s) (get s) ≡ s
      -- put-get-law : (s : S) -> (v : Vec A (fst (Traversal.extract t s))) ->
      --  (Traversal.get t (Traversal.put t s v)) ≡ {!!}

  record Traversal2 (S A B T : Set) : Set where
    field
      extract : (s : S) -> Σ[ f ∈ (S -> ℕ) ] Vec A (f s) × (Vec B (f s) -> T)

max_stars_repo_name: hablapps/safeoptics

max_issues_repo_name: hablapps/safeoptics

max_forks_repo_name: hablapps/safeoptics


text:
module Prologue where

open import Relation.Binary.Core

open IsEquivalence ⦃ … ⦄


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

open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.Definition

module Rings.Ideals.Principal.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where

open Setoid S
open Ring R
open Equivalence eq
open import Rings.Ideals.Principal.Definition R
open import Rings.Ideals.Definition R
open import Rings.Ideals.Lemmas R
open import Rings.Divisible.Definition R

generatorZeroImpliesAllZero : {c : _} {pred : A → Set c} → {i : Ideal pred} → (princ : PrincipalIdeal i) → PrincipalIdeal.generator princ ∼ 0R → {x : A} → pred x → x ∼ 0R
generatorZeroImpliesAllZero record { generator = gen ; genIsInIdeal = genIsInIdeal ; genGenerates = genGenerates } gen=0 {x} predX = generatorZeroImpliesMembersZero {x} (divisibleWellDefined gen=0 reflexive (genGenerates predX))


text:
-- WARNING: This file was generated automatically by Vehicle
-- and should not be modified manually!
-- Metadata
--  - Agda version: 2.6.2
--  - AISEC version: 0.1.0.1
--  - Time generated: ???

{-# OPTIONS --allow-exec #-}

open import Vehicle
open import Data.Integer as ℤ using (ℤ)
open import Data.Rational as ℚ using (ℚ)

module simple-arithmetic-temp-output where

precedence : ℚ → (ℚ → (ℚ → ℚ))
precedence x y z = (x ℚ.+ (ℤ.+ 2 ℚ./ 1) ℚ.* y) ℚ.- z ℚ.÷ y

max_stars_repo_name: vehicle-lang/vehicle

max_issues_repo_name: vehicle-lang/vehicle

max_forks_repo_name: vehicle-lang/vehicle


text:
-- Andreas, 2012-09-11
{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.meta:50 #-}
module Const where

import Common.Level

const : {A B : Set} → A → B → A
const a b = a
-- If this is analyzed as {A B : Set} → A → .B → A
-- then, due to constraint solving insensitive to subtyping,
-- the following will trigger an 'UnequalRelevance' error.

postulate
  F : Set → Set
  _<$>_ : {A B : Set} → (A → B) → F A → F B
  _<*>_ : {A B : Set} → F (A → B) → F A → F B

test : {A B : Set} → F A → F B → F A
test {A} {B} x y = (const <$> x) <*> y


text:
module PolyDepPrelude where

data Pi {X : Set} (Y : X -> Set) : Set where
  pi : ((x : X) -> Y x) -> Pi Y

apply : {a : Set} -> {f : a -> Set} -> Pi f -> (x : a) -> f x
apply (pi f) x = f x

data Forall {X : Set} (Y : X -> Set) : Set where
  forAll : ((x : X) -> Y x) -> Forall Y

data _=>_ (X Y : Set) : Set where
  lam : (X -> Y) -> X => Y

_$$_ : {X Y : Set} -> (X => Y) -> X -> Y
lam f $$ x = f x

infixr 0 _$$_

id : {a : Set} -> a -> a
id x = x

infixr 0 _$_

_$_ : {a b : Set} -> (a -> b) -> a -> b
f $ x = f x

data Bool : Set where
  true  : Bool
  false : Bool

_&&_ : Bool -> Bool -> Bool
true  && b = b
false && _ = false

data Pair (a b : Set) : Set where
  pair : a -> b -> Pair a b

fst : {a b : Set} -> Pair a b -> a
fst (pair x y) = x

snd : {a b : Set} -> Pair a b -> b
snd (pair x y) = y

cmp : {X Y Z : Set} -> (Y -> Z) -> (X -> Y) -> X -> Z
cmp f g = \x -> f (g x)

data Either (a b : Set) : Set where
  left  : a -> Either a b
  right : b -> Either a b

data Maybe (a : Set) : Set where
  Nothing : Maybe a
  Just    : a -> Maybe a

data Unit : Set where
  unit : Unit

Taut = Unit

data Absurd : Set where

postulate
  absurdElim : {whatever : Set} -> Absurd -> whatever

T : Bool -> Set
T true  = Unit
T false = Absurd

andT : {x y : Bool} -> T x -> T y -> T (x && y)
andT {true}  {true}  _  _ = unit
andT {false} {_}     () _
andT {true}  {false} _  ()

T' : {a : Set} -> (a -> a -> Bool) -> (a -> a -> Set)
T' f x y = T (f x y)

data Not (a : Set) : Set where
  not : (a -> Absurd) -> Not a

-- Not : Set -> Set
-- Not a = a -> Absurd

contrapositive : {a b : Set} -> (a -> b) -> Not b -> Not a
contrapositive p (not nb) = not (\a -> nb (p a))

private
  notDistribOut' : {a b : Set} -> Not a -> Not b -> Either a b -> Absurd
  notDistribOut' (not na) _        (left a)  = na a
  notDistribOut' _        (not nb) (right b) = nb b

notDistribOut : {a b : Set} -> Not a -> Not b -> Not (Either a b)
notDistribOut na nb = not (notDistribOut' na nb)

notDistribIn : {a b : Set} -> Not (Either a b) -> Pair (Not a) (Not b)
notDistribIn (not nab) = pair (not (\a -> nab (left a)))
                              (not (\b -> nab (right b)))

data _<->_ (a b : Set) : Set where
  iff : (a -> b) -> (b -> a) -> a <-> b

iffLeft : {a b : Set} -> (a <-> b) -> (a -> b)
iffLeft (iff l _) = l

iffRight : {a b : Set} -> (a <-> b) -> (b -> a)
iffRight (iff _ r) = r

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

one : Nat
one = suc zero

elimNat : (C : Nat -> Set)
         -> (C zero) -> ((m : Nat) -> C m -> C (suc m)) -> (n : Nat) -> C n
elimNat C c_z c_s zero = c_z
elimNat C c_z c_s (suc m') = c_s m' (elimNat C c_z c_s m')

data List (A : Set) : Set where
  nil  : List A
  _::_ : A -> List A -> List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  nil  #-}
{-# BUILTIN CONS _::_ #-}

elimList : {A : Set} ->
          (C : List A -> Set) ->
          (C nil) ->
          ((a : A) -> (as : List A) -> C as -> C (a :: as)) ->
          (as : List A) ->
          C as
elimList _ c_nil _ nil = c_nil
elimList C c_nil c_con (a :: as) = c_con a as (elimList C c_nil c_con as)

data Reflexive {X : Set} (_R_ : X -> X -> Set) : Set where
  reflexive : ((x : X) -> x R x) -> Reflexive _R_
data Symmetrical {X : Set} (_R_ : X -> X -> Set) : Set where
  symmetrical : ( {x1 x2 : X} -> x1 R x2 -> x2 R x1) -> Symmetrical _R_
data Substitutive {X : Set} (_R_ : X -> X -> Set) : Set1 where
  substitutive : ( (P : X -> Set) -> {x1 x2 : X} -> x1 R x2 -> P x1 -> P x2)
                 -> Substitutive _R_

True : Bool -> Set
True (true)  = Unit
True (false) = Absurd

data Datoid  : Set1 where
  datoid : (Elem : Set) ->
           (eq : Elem -> Elem -> Bool) ->
           (ref : (x : Elem) -> True (eq x x)) ->
           (subst : Substitutive  (\x1 -> \x2 -> True (eq x1 x2))) ->
           Datoid

pElem : Datoid -> Set
pElem (datoid Elem _ _ _) = Elem


text:
open import Oscar.Prelude
open import Oscar.Class.HasEquivalence
open import Oscar.Class.Smap
open import Oscar.Class.Symmetry
open import Oscar.Class.Symmetrical
open import Oscar.Data.Surjcollation
import Oscar.Class.HasEquivalence.Ṗroperty
import Oscar.Class.Surjection.⋆
import Oscar.Data.Proposequality

module Oscar.Class.Symmetrical.Unifies where

module _
  {𝔵} {𝔛 : Ø 𝔵}
  {𝔞} {𝔄 : 𝔛 → 𝔛 → Ø 𝔞}
  {𝔠} {ℭ : 𝔛 → Ø 𝔠}
  ⦃ _ : Smap!.class 𝔄 (Extension ℭ) ⦄
  {ℓ} {_≈'_ : ∀ {y} → ℭ y → ℭ y → Ø ℓ}
  ⦃ _ : ∀ {y} → Symmetry.class (_≈'_ {y}) ⦄
  where

  instance

    𝓢ymmetricalUnifies₀ : ∀ {m} → Symmetrical surjcollation⟦ _ / _≈'_ ⟧ (λ x y → x ≈[ LeftṖroperty ℓ 𝔄 m ] y)
    𝓢ymmetricalUnifies₀ .𝓢ymmetrical.symmetrical x y .π₀ = symmetry , symmetry


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Data.Fin.Arithmetic where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Mod
open import Cubical.Data.Nat.Order
open import Cubical.Data.Fin
open import Cubical.Data.Sigma

infixl 6 _+ₘ_ _-ₘ_ _·ₘ_
infix 7 -ₘ_

-- Addition, subtraction and multiplication
_+ₘ_ : {n : ℕ} → Fin (suc n) → Fin (suc n) → Fin (suc n)
fst (_+ₘ_ {n = n} x y) = ((fst x) + (fst y)) mod (suc n)
snd (_+ₘ_ {n = n} x y) = mod< _ ((fst x) + (fst y))

-ₘ_ : {n : ℕ} → (x : Fin (suc n)) → Fin (suc n)
fst (-ₘ_ {n = n} x) =
  (+induction n _ (λ x _ → ((suc n) ∸ x) mod (suc n)) λ _ x → x) (fst x)
snd (-ₘ_ {n = n} x) = lem (fst x)
  where
  ≡<-trans : {x y z : ℕ} → x < y → x ≡ z → z < y
  ≡<-trans (k , p) q = k , cong (λ x → k + suc x) (sym q) ∙ p

  lem : {n : ℕ} (x : ℕ)
     → (+induction n _ _ _) x < suc n
  lem {n = n} =
    +induction n _
      (λ x p → ≡<-trans (mod< n (suc n ∸ x))
                 (sym (+inductionBase n _ _ _ x p)))
       λ x p → ≡<-trans p
                 (sym (+inductionStep n _ _ _ x))

_-ₘ_ : {n : ℕ} → (x y : Fin (suc n)) → Fin (suc n)
_-ₘ_ x y = x +ₘ (-ₘ y)

_·ₘ_ : {n : ℕ} → (x y : Fin (suc n)) → Fin (suc n)
fst (_·ₘ_ {n = n} x y) = (fst x · fst y) mod (suc n)
snd (_·ₘ_ {n = n} x y) = mod< n (fst x · fst y)

-- Group laws
+ₘ-assoc : {n : ℕ} (x y z : Fin (suc n))
  → (x +ₘ y) +ₘ z ≡ (x +ₘ (y +ₘ z))
+ₘ-assoc {n = n} x y z =
  Σ≡Prop (λ _ → isProp≤)
       ((mod-rCancel (suc n) ((fst x + fst y) mod (suc n)) (fst z))
    ∙∙ sym (mod+mod≡mod (suc n) (fst x + fst y) (fst z))
    ∙∙ cong (_mod suc n) (sym (+-assoc (fst x) (fst y) (fst z)))
    ∙∙ mod+mod≡mod (suc n) (fst x) (fst y + fst z)
    ∙∙ sym (mod-lCancel (suc n) (fst x) ((fst y + fst z) mod suc n)))

+ₘ-comm : {n : ℕ} (x y : Fin (suc n)) → (x +ₘ y) ≡ (y +ₘ x)
+ₘ-comm {n = n} x y =
  Σ≡Prop (λ _ → isProp≤)
    (cong (_mod suc n) (+-comm (fst x) (fst y)))

+ₘ-lUnit : {n : ℕ} (x : Fin (suc n)) → 0 +ₘ x ≡ x
+ₘ-lUnit {n = n} (x , p) =
  Σ≡Prop (λ _ → isProp≤)
    (+inductionBase n _ _ _ x p)

+ₘ-rUnit : {n : ℕ} (x : Fin (suc n)) → x +ₘ 0 ≡ x
+ₘ-rUnit x = +ₘ-comm x 0 ∙ (+ₘ-lUnit x)

+ₘ-rCancel : {n : ℕ} (x : Fin (suc n)) → x -ₘ x ≡ 0
+ₘ-rCancel {n = n} x =
  Σ≡Prop (λ _ → isProp≤)
      (cong (λ z → (fst x + z) mod (suc n))
            (+inductionBase n _ _ _ (fst x) (snd x))
    ∙∙ sym (mod-rCancel (suc n) (fst x) ((suc n) ∸ (fst x)))
    ∙∙ cong (_mod (suc n)) (+-comm (fst x) ((suc n) ∸ (fst x)))
    ∙∙ cong (_mod (suc n)) (≤-∸-+-cancel (<-weaken (snd x)))
    ∙∙ zero-charac (suc n))

+ₘ-lCancel : {n : ℕ} (x : Fin (suc n)) → (-ₘ x) +ₘ x ≡ 0
+ₘ-lCancel {n = n} x = +ₘ-comm (-ₘ x) x ∙ +ₘ-rCancel x

-- TODO : Ring laws

private
  test₁ : Path (Fin 11) (5 +ₘ 10) 4
  test₁ = refl

  test₂ : Path (Fin 11) (-ₘ 7 +ₘ 5 +ₘ 10) 8
  test₂ = refl


text:
-- Operator example

module Operators where

data True : Set where
  tt : True

data False : Set where

data Bool : Set where
  false : Bool
  true  : Bool

-- An operator is declared with '_' where the arguments go
if_then_else_ : Bool -> {A : Set} -> A -> A -> A
if true  then x else y = x
if false then x else y = y

-- The actual name of the operator is obtained by removing all the spaces from
-- the declared version.
infix 1 if_then_else_

-- This name can be used in normal applications, for instance, if a hidden argument
-- needs to be supplied.
_&&_ : Bool -> Bool -> Bool
x && y = if_then_else_ x {Bool} y false

-- Operators can be prefix...
¬_ : Bool -> Bool
¬ true  = false
¬ false = true

-- ...or postfix...
_valid : Bool -> Set
true  valid = True
false valid = False

-- ...or roundfix
⟦_⟧ : Bool -> Set
⟦ x ⟧ = x valid


text:
-- Andreas, 2014-01-10
-- Code by Jesper Cockx and Conor McBride and folks from the Coq-club

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

-- An empty type.

data Zero : Set where

-- A unit type as W-type.

mutual
  data WOne : Set where wrap : FOne -> WOne
  FOne = Zero -> WOne

-- Type equality.

data _<->_ (X : Set) : Set -> Set₁ where
  Refl : X <-> X

-- This postulate is compatible with univalence:

postulate
  iso : WOne <-> FOne

-- But accepting that is incompatible with univalence:

auoo : WOne -> Zero
auoo (wrap f) = noo FOne iso f
  where
    noo : (X : Set) -> (WOne <-> X) -> X -> Zero
    noo .WOne Refl w = auoo w

-- Matching against Refl silently applies the conversion
-- FOne -> WOne to f.  But this conversion corresponds
-- to an application of wrap.  Thus, f, which is really
-- (wrap f), should not be considered a subterm of (wrap f)
-- by the termination checker.
-- At least, if we want to be compatible with univalence.

absurd : Zero
absurd = auoo (wrap \ ())

-- noo should fail termination check.


text:
module Data.QuadTree.Implementation.QuadrantLenses where

open import Haskell.Prelude renaming (zero to Z; suc to S)
open import Data.Lens.Lens
open import Data.Logic
open import Data.QuadTree.Implementation.PropDepthRelation
open import Data.QuadTree.Implementation.Definition
open import Data.QuadTree.Implementation.ValidTypes

{-# FOREIGN AGDA2HS
{-# LANGUAGE Safe #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Rank2Types #-}
import Data.Nat
import Data.Lens.Lens
import Data.Logic

import Data.QuadTree.Implementation.Definition
import Data.QuadTree.Implementation.ValidTypes
#-}

---- Lenses

-- Lenses into a leaf of a depth zero quadrant
lensLeaf : {t : Set} {{eqT : Eq t}}
  -> Lens (VQuadrant t {0}) t
lensLeaf f (CVQuadrant (Leaf v)) = fmap (λ x -> CVQuadrant (Leaf x) {IsTrue.itsTrue}) (f v)
{-# COMPILE AGDA2HS lensLeaf #-}

-- A proof of the depth relation of a node and its children
propDepthRelationLte : {t : Set} -> (a b c d : Quadrant t) -> (dep : Nat)
  -> ((depth a <= dep && depth b <= dep) && (depth c <= dep && depth d <= dep)) ≡ (depth (Node a b c d) <= (S dep))
propDepthRelationLte a b c d dep =
  begin
    ((depth a <= dep && depth b <= dep) && (depth c <= dep && depth d <= dep))
  =⟨ propMaxLte4 (depth a) (depth b) (depth c) (depth d) dep ⟩
    (max (max (depth a) (depth b)) (max (depth c) (depth d)) <= dep)
  =⟨⟩
    (depth (Node a b c d) <= S dep)
  end

-- A proof of the compressed relation of a node and its children
propCompressedRelation : {t : Set} {{eqT : Eq t}} -> {a b c d : Quadrant t}
  -> IsTrue (isCompressed (Node a b c d))
  -> IsTrue (isCompressed a && isCompressed b && isCompressed c && isCompressed d)
propCompressedRelation {_} {Leaf a} {Leaf b} {Leaf c} {Leaf d} p = IsTrue.itsTrue
propCompressedRelation {_} {Node _ _ _ _} {b} {c} {d} p = p
propCompressedRelation {_} {Leaf _} {Node _ _ _ _} {c} {d} p = p
propCompressedRelation {_} {Leaf _} {Leaf _} {Node _ _ _ _} {d} p = p
propCompressedRelation {_} {Leaf _} {Leaf _} {Leaf _} {Node _ _ _ _} p = p

-- Combine 4 valid quadrants to a new valid quadrant
combine : {t : Set} {{eqT : Eq t}}
  -> {dep : Nat}
  -> (a b c d : VQuadrant t {dep})
  -> VQuadrant t {S dep}
combine {t} {dep} (CVQuadrant a@(Leaf va) {pa}) (CVQuadrant b@(Leaf vb) {pb}) (CVQuadrant c@(Leaf vc) {pc}) (CVQuadrant d@(Leaf vd) {pd})
  = ifc (va == vb && vb == vc && vc == vd)
    then CVQuadrant a {IsTrue.itsTrue}
    else (λ {{pn}} -> CVQuadrant (Node a b c d) {andCombine (zeroLteAny dep) (falseToNotTrue $ pn)})
-- The next 4 cases are all identical, but I could not figure out another way to convince agda
combine {t} {dep} (CVQuadrant a@(Node v1 v2 v3 v4) {pa}) (CVQuadrant b {pb}) (CVQuadrant c {pc}) (CVQuadrant d {pd})
  = CVQuadrant (Node a b c d) {andCombine
    (useEq (propDepthRelationLte a b c d dep) ((propIsTrueCombine4 (andFst {depth a <= dep} pa) (andFst {depth b <= dep} pb) (andFst {depth c <= dep} pc) (andFst {depth d <= dep} pd))))
    (propIsTrueCombine4Alt (andSnd {depth a <= dep} pa) (andSnd {depth b <= dep} pb) (andSnd {depth c <= dep} pc) (andSnd {depth d <= dep} pd))
  }
combine {t} {dep} (CVQuadrant a@(Leaf va) {pa}) (CVQuadrant b@(Node v1 v2 v3 v4) {pb}) (CVQuadrant c {pc}) (CVQuadrant d {pd})
  = CVQuadrant (Node a b c d) {andCombine
    (useEq (propDepthRelationLte a b c d dep) ((propIsTrueCombine4 (andFst {depth a <= dep} pa) (andFst {depth b <= dep} pb) (andFst {depth c <= dep} pc) (andFst {depth d <= dep} pd))))
    (propIsTrueCombine4Alt (andSnd {depth a <= dep} pa) (andSnd {depth b <= dep} pb) (andSnd {depth c <= dep} pc) (andSnd {depth d <= dep} pd))
  }
combine {t} {dep} (CVQuadrant a@(Leaf va) {pa}) (CVQuadrant b@(Leaf vb) {pb}) (CVQuadrant c@(Node v1 v2 v3 v4) {pc}) (CVQuadrant d {pd})
  = CVQuadrant (Node a b c d) {andCombine
    (useEq (propDepthRelationLte a b c d dep) ((propIsTrueCombine4 (andFst {depth a <= dep} pa) (andFst {depth b <= dep} pb) (andFst {depth c <= dep} pc) (andFst {depth d <= dep} pd))))
    (propIsTrueCombine4Alt (andSnd {depth a <= dep} pa) (andSnd {depth b <= dep} pb) (andSnd {depth c <= dep} pc) (andSnd {depth d <= dep} pd))
  }
combine {t} {dep} (CVQuadrant a@(Leaf va) {pa}) (CVQuadrant b@(Leaf vb) {pb}) (CVQuadrant c@(Leaf vc) {pc}) (CVQuadrant d@(Node v1 v2 v3 v4) {pd})
  = CVQuadrant (Node a b c d) {andCombine
    (useEq (propDepthRelationLte a b c d dep) ((propIsTrueCombine4 (andFst {depth a <= dep} pa) (andFst {depth b <= dep} pb) (andFst {depth c <= dep} pc) (andFst {depth d <= dep} pd))))
    (propIsTrueCombine4Alt (andSnd {depth a <= dep} pa) (andSnd {depth b <= dep} pb) (andSnd {depth c <= dep} pc) (andSnd {depth d <= dep} pd))
  }
{-# COMPILE AGDA2HS combine #-}

-- Goes from a valid quadrant to its a subquadrant
aSub : {t : Set} {{eqT : Eq t}} -> {dep : Nat} -> (a b c d : Quadrant t)
  -> IsTrue (isValid (S dep) (Node a b c d)) -> IsTrue (isValid (dep) a)
aSub {_} {dep} a b c d p = andCombine
  -- Convert depth proof using propDepthRelationLte
  (andFst $ andFst {(depth a <= dep && depth b <= dep)} $ useEq (sym (propDepthRelationLte a b c d dep)) (andFst p))
  -- Convert compressed proof using propCompressedRelation
  (and1 {isCompressed a} {isCompressed b} {isCompressed c} {isCompressed d} (propCompressedRelation {_} {a} (andSnd p)))

-- Goes from a valid quadrant to its b subquadrant
bSub : {t : Set} {{eqT : Eq t}} -> {dep : Nat} -> (a b c d : Quadrant t)
  -> IsTrue (isValid (S dep) (Node a b c d)) -> IsTrue (isValid (dep) b)
bSub {_} {dep} a b c d p = andCombine
  -- Convert depth proof using propDepthRelationLte
  (andSnd $ andFst {(depth a <= dep && depth b <= dep)} $ useEq (sym (propDepthRelationLte a b c d dep)) (andFst p))
  -- Convert compressed proof using propCompressedRelation
  (and2 {isCompressed a} {isCompressed b} {isCompressed c} {isCompressed d} (propCompressedRelation {_} {a} (andSnd p)))

-- Goes from a valid quadrant to its c subquadrant
cSub : {t : Set} {{eqT : Eq t}} -> {dep : Nat} -> (a b c d : Quadrant t)
  -> IsTrue (isValid (S dep) (Node a b c d)) -> IsTrue (isValid (dep) c)
cSub {_} {dep} a b c d p = andCombine
  -- Convert depth proof using propDepthRelationLte
  (andFst $ andSnd {(depth a <= dep && depth b <= dep)} $ useEq (sym (propDepthRelationLte a b c d dep)) (andFst p))
  -- Convert compressed proof using propCompressedRelation
  (and3 {isCompressed a} {isCompressed b} {isCompressed c} {isCompressed d} (propCompressedRelation {_} {a} (andSnd p)))

-- Goes from a valid quadrant to its d subquadrant
dSub : {t : Set} {{eqT : Eq t}} -> {dep : Nat} -> (a b c d : Quadrant t)
  -> IsTrue (isValid (S dep) (Node a b c d)) -> IsTrue (isValid (dep) d)
dSub {_} {dep} a b c d p = andCombine
  -- Convert depth proof using propDepthRelationLte
  (andSnd $ andSnd {(depth a <= dep && depth b <= dep)} $ useEq (sym (propDepthRelationLte a b c d dep)) (andFst p))
  -- Convert compressed proof using propCompressedRelation
  (and4 {isCompressed a} {isCompressed b} {isCompressed c} {isCompressed d} (propCompressedRelation {_} {a} (andSnd p)))

-- Lens into the a subquadrant
lensA :
  {t : Set} {{eqT : Eq t}}
  -> {dep : Nat}
  -> Lens (VQuadrant t {S dep}) (VQuadrant t {dep})
lensA {_} {dep} f (CVQuadrant (Leaf v) {p}) =
  let sub = CVQuadrant (Leaf v) {andCombine (zeroLteAny dep) IsTrue.itsTrue}
  in fmap (λ x -> combine x sub sub sub ) (f sub)
lensA {_} {dep} f (CVQuadrant (Node a b c d) {p}) =
  let
    sA = CVQuadrant a {aSub a b c d p}
    sB = CVQuadrant b {bSub a b c d p}
    sC = CVQuadrant c {cSub a b c d p}
    sD = CVQuadrant d {dSub a b c d p}
  in fmap (λ x -> combine x sB sC sD ) (f sA)
{-# COMPILE AGDA2HS lensA #-}

-- Lens into the b subquadrant
lensB :
  {t : Set} {{eqT : Eq t}}
  -> {dep : Nat}
  -> Lens (VQuadrant t {S dep}) (VQuadrant t {dep})
lensB {_} {dep} f (CVQuadrant (Leaf v) {p}) =
  let sub = CVQuadrant (Leaf v) {andCombine (zeroLteAny dep) IsTrue.itsTrue}
  in fmap (λ x -> combine sub x sub sub ) (f sub)
lensB {_} {dep} f (CVQuadrant (Node a b c d) {p}) =
  let
    sA = CVQuadrant a {aSub a b c d p}
    sB = CVQuadrant b {bSub a b c d p}
    sC = CVQuadrant c {cSub a b c d p}
    sD = CVQuadrant d {dSub a b c d p}
  in fmap (λ x -> combine sA x sC sD ) (f sB)
{-# COMPILE AGDA2HS lensB #-}

-- Lens into the c subquadrant
lensC :
  {t : Set} {{eqT : Eq t}}
  -> {dep : Nat}
  -> Lens (VQuadrant t {S dep}) (VQuadrant t {dep})
lensC {_} {dep} f (CVQuadrant (Leaf v) {p}) =
  let sub = CVQuadrant (Leaf v) {andCombine (zeroLteAny dep) IsTrue.itsTrue}
  in fmap (λ x -> combine sub sub x sub ) (f sub)
lensC {_} {dep} f (CVQuadrant (Node a b c d) {p}) =
  let
    sA = CVQuadrant a {aSub a b c d p}
    sB = CVQuadrant b {bSub a b c d p}
    sC = CVQuadrant c {cSub a b c d p}
    sD = CVQuadrant d {dSub a b c d p}
  in fmap (λ x -> combine sA sB x sD ) (f sC)
{-# COMPILE AGDA2HS lensC #-}

-- Lens into the d subquadrant
lensD :
  {t : Set} {{eqT : Eq t}}
  -> {dep : Nat}
  -> Lens (VQuadrant t {S dep}) (VQuadrant t {dep})
lensD {_} {dep} f (CVQuadrant (Leaf v) {p}) =
  let sub = CVQuadrant (Leaf v) {andCombine (zeroLteAny dep) IsTrue.itsTrue}
  in fmap (λ x -> combine sub sub sub x ) (f sub)
lensD {_} {dep} f (CVQuadrant (Node a b c d) {p}) =
  let
    sA = CVQuadrant a {aSub a b c d p}
    sB = CVQuadrant b {bSub a b c d p}
    sC = CVQuadrant c {cSub a b c d p}
    sD = CVQuadrant d {dSub a b c d p}
  in fmap (λ x -> combine sA sB sC x ) (f sD)
{-# COMPILE AGDA2HS lensD #-}

max_stars_repo_name: JonathanBrouwer/research-project

max_issues_repo_name: JonathanBrouwer/research-project

max_forks_repo_name: JonathanBrouwer/research-project


text:
------------------------------------------------------------------------------
-- Proving properties without using pattern matching on refl
------------------------------------------------------------------------------

{-# OPTIONS --no-pattern-matching #-}
{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}

module FOT.DistributiveLaws.NoPatternMatchingOnRefl where

open import DistributiveLaws.Base

------------------------------------------------------------------------------
-- From DistributiveLaws.PropertiesI

-- Congruence properties

·-leftCong : ∀ {a b c} → a ≡ b → a · c ≡ b · c
·-leftCong {a} {c = c} h = subst (λ t → a · c ≡ t · c) h refl

·-rightCong : ∀ {a b c} → b ≡ c → a · b ≡ a · c
·-rightCong {a} {b} h = subst (λ t → a · b ≡ a · t) h refl

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
open import Agda.Builtin.Bool

data D : Set where
  c : Bool → D

f : @0 D → Bool
f (c true)  = true
f (c false) = false

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

postulate
  D   : Set
  _≡_ : D → D → Set
  a b : D

postulate p : a ≡ b
{-# ATP axiom p #-}

postulate foo : a ≡ b
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
{-# OPTIONS --without-K --safe #-}
module Categories.CoYoneda where

-- CoYoneda Lemma.  See Yoneda for more documentation

open import Level
open import Function.Base using (_$_)
open import Function.Bundles using (Inverse)
open import Function.Equality using (Π; _⟨$⟩_; cong)
open import Relation.Binary.Bundles using (module Setoid)
import Relation.Binary.Reasoning.Setoid as SetoidR
open import Data.Product using (_,_; Σ)

open import Categories.Category using (Category; _[_,_])
open import Categories.Category.Product using (πʳ; πˡ; _※_)
open import Categories.Category.Construction.Presheaves using (CoPresheaves)
open import Categories.Category.Construction.Functors using (eval)
open import Categories.Category.Construction.Functors
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Functor.Hom using (module Hom; Hom[_][_,-]; Hom[_][-,-])
open import Categories.Functor.Bifunctor using (Bifunctor)
-- open import Categories.Functor.Presheaf using (Presheaf)
open import Categories.Functor.Construction.LiftSetoids using (LiftSetoids)
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) renaming (id to idN)
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)

import Categories.Morphism as Mor
import Categories.Morphism.Reasoning as MR
import Categories.NaturalTransformation.Hom as NT-Hom

private
  variable
    o ℓ e : Level

module Yoneda (C : Category o ℓ e) where
  open Category C hiding (op) -- uses lots
  open HomReasoning using (_○_; ⟺)
  open MR C using (id-comm)
  open NaturalTransformation using (η; commute)
  open NT-Hom C using (Hom[C,A]⇒Hom[C,B])
  private
    module CE = Category.Equiv C using (refl)
    module C = Category C using (op)

  -- The CoYoneda embedding functor
  embed : Functor C.op (CoPresheaves C)
  embed = record
    { F₀           = Hom[ C ][_,-]
    ; F₁           = Hom[C,A]⇒Hom[C,B] -- B⇒A induces a NatTrans on the Homs.
    ; identity     = identityʳ ○_
    ; homomorphism = λ h₁≈h₂ → ∘-resp-≈ˡ h₁≈h₂ ○ sym-assoc
    ; F-resp-≈     = λ f≈g h≈i → ∘-resp-≈ h≈i f≈g
    }

  -- Using the adjunction between product and product, we get a kind of contravariant Bifunctor
  yoneda-inverse : (a : Obj) (F : Functor C (Setoids ℓ e)) →
    Inverse (Category.hom-setoid (CoPresheaves C) {Functor.F₀ embed a} {F}) (Functor.F₀ F a)
  yoneda-inverse a F = record
    { f = λ nat → η nat a ⟨$⟩ id
    ; f⁻¹ = λ x → ntHelper record
        { η       = λ X → record
          { _⟨$⟩_ = λ X⇒a → F.₁ X⇒a ⟨$⟩ x
          ; cong  = λ i≈j → F.F-resp-≈ i≈j SE.refl
          }
        ; commute = λ {X} {Y} X⇒Y {f} {g} f≈g →
          let module SR = SetoidR (F.₀ Y) in
          SR.begin
             F.₁ (X⇒Y ∘ f ∘ id) ⟨$⟩ x   SR.≈⟨ F.F-resp-≈ (∘-resp-≈ʳ (identityʳ ○ f≈g)) SE.refl ⟩
             F.₁ (X⇒Y ∘ g) ⟨$⟩ x        SR.≈⟨ F.homomorphism SE.refl ⟩
             F.₁ X⇒Y ⟨$⟩ (F.₁ g ⟨$⟩ x)
           SR.∎
        }
    ; cong₁ = λ i≈j → i≈j CE.refl
    ; cong₂ = λ i≈j y≈z → F.F-resp-≈ y≈z i≈j
    ; inverse = (λ Fa → F.identity SE.refl) , λ nat {x} {z} {y} z≈y →
        let module SR     = SetoidR (F.₀ x) in
        SR.begin
          F.₁ z ⟨$⟩ (η nat a ⟨$⟩ id) SR.≈˘⟨ commute nat z (CE.refl {a}) ⟩
          η nat x ⟨$⟩ z ∘ id ∘ id SR.≈⟨ cong (η nat x) (∘-resp-≈ʳ identity² ○ identityʳ ○ z≈y ) ⟩
          η nat x ⟨$⟩ y
        SR.∎
    }
    where
    module F = Functor F using (₀; ₁; F-resp-≈; homomorphism; identity)
    module SE = Setoid (F.₀ a) using (refl)

  private
    Nat[Hom[C][c,-],F] : Bifunctor (CoPresheaves C) C (Setoids (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e))
    Nat[Hom[C][c,-],F] = Hom[ CoPresheaves C ][-,-] ∘F (Functor.op embed ∘F πʳ ※ πˡ)

    FC : Bifunctor (CoPresheaves C) C (Setoids _ _)
    FC = LiftSetoids (o ⊔ ℓ ⊔ e) (o ⊔ ℓ) ∘F eval {C = C} {D = Setoids ℓ e}

    module yoneda-inverse {a} {F} = Inverse (yoneda-inverse a F)

  -- the two bifunctors above are naturally isomorphic.
  -- it is easy to show yoneda-inverse first then to yoneda.
  yoneda : NaturalIsomorphism Nat[Hom[C][c,-],F] FC
  yoneda = record
    { F⇒G = ntHelper record
      { η       = λ where
        (F , A) → record
          { _⟨$⟩_ = λ α → lift (yoneda-inverse.f α)
          ; cong  = λ i≈j → lift (i≈j CE.refl)
          }
      ; commute = λ where
        {_} {G , B} (α , f) {β} {γ} β≈γ → lift $ cong (η α B) (helper f β γ β≈γ)
      }
    ; F⇐G = ntHelper record
      { η       = λ (F , A) → record
          { _⟨$⟩_ = λ x → yoneda-inverse.f⁻¹ (lower x)
          ; cong  = λ i≈j y≈z → Functor.F-resp-≈ F y≈z (lower i≈j)
          }
      ; commute = λ { {F , A} {G , B} (α , f) {X} {Y} eq {Z} {h} {i} eq′ → helper′ α f (lower eq) eq′}
      }
    ; iso = λ (F , A) → record
        { isoˡ = λ {α β} i≈j {X} y≈z →
          Setoid.trans (Functor.F₀ F X) ( yoneda-inverse.inverseʳ α {x = X} y≈z) (i≈j CE.refl)
        ; isoʳ = λ eq → lift (Setoid.trans (Functor.F₀ F A) ( yoneda-inverse.inverseˡ {F = F} _) (lower eq))
        }
    }
    where helper : {F : Functor C (Setoids ℓ e)}
                   {A B : Obj} (f : A ⇒ B)
                   (β γ : NaturalTransformation Hom[ C ][ A ,-] F) →
                   Setoid._≈_ (Functor.F₀ Nat[Hom[C][c,-],F] (F , A)) β γ →
                   Setoid._≈_ (Functor.F₀ F B) (η β B ⟨$⟩ id ∘ f) (Functor.F₁ F f ⟨$⟩ (η γ A ⟨$⟩ id))
          helper {F} {A} {B} f β γ β≈γ = S.begin
            η β B ⟨$⟩ id ∘ f        S.≈⟨ cong (η β B) (MR.id-comm-sym C ○ ∘-resp-≈ʳ (⟺ identity²)) ⟩
            η β B ⟨$⟩ f ∘ id ∘ id   S.≈⟨ commute β f CE.refl ⟩
            F.₁ f ⟨$⟩ (η β A ⟨$⟩ id) S.≈⟨ cong (F.₁ f) (β≈γ CE.refl) ⟩
            F.₁ f ⟨$⟩ (η γ A ⟨$⟩ id) S.∎
            where
            module F = Functor F using (₀;₁)
            module S = SetoidR (F.₀ B)

          helper′ : ∀ {F G : Functor C (Setoids ℓ e)}
                      {A B Z : Obj}
                      {h i : B ⇒ Z}
                      {X Y : Setoid.Carrier (Functor.F₀ F A)}
                      (α : NaturalTransformation F G)
                      (f : A ⇒ B) →
                      Setoid._≈_ (Functor.F₀ F A) X Y →
                      h ≈ i →
                      Setoid._≈_ (Functor.F₀ G Z) (Functor.F₁ G h ⟨$⟩ (η α B ⟨$⟩ (Functor.F₁ F f ⟨$⟩ X)))
                                          (η α Z ⟨$⟩ (Functor.F₁ F (i ∘ f) ⟨$⟩ Y))
          helper′ {F} {G} {A} {B} {Z} {h} {i} {X} {Y} α f eq eq′ = S.begin
            G.₁ h ⟨$⟩ (η α B ⟨$⟩ (F.₁ f ⟨$⟩ X))  S.≈˘⟨ commute α h ((S′.sym (cong (F.₁ f) eq))) ⟩
            η α Z ⟨$⟩ (F.₁ h ⟨$⟩ (F.₁ f ⟨$⟩ Y))  S.≈⟨ cong (η α Z) ((F.F-resp-≈ eq′ S′.refl)) ⟩
            η α Z ⟨$⟩ (F.₁ i ⟨$⟩ (F.₁ f ⟨$⟩ Y))  S.≈˘⟨ cong (η α Z) ((F.homomorphism (Setoid.refl (F.₀ A)))) ⟩
            η α Z ⟨$⟩ (F.₁ (i ∘ f) ⟨$⟩ Y)        S.∎
            where
              module F = Functor F using (₀; ₁; homomorphism; F-resp-≈)
              module G = Functor G using (₀; ₁)
              module S = SetoidR (G.₀ Z)
              module S′ = Setoid (F.₀ B) using (refl; sym)

  module yoneda = NaturalIsomorphism yoneda

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


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

module HoTT.Sigma.Universal where

Σ-univ : ∀ {i j k} {X : 𝒰 i} {A : X → 𝒰 j} (P : (x : X) → A x → 𝒰 k) →
         ((x : X) → Σ (A x) λ a → P x a) ≃
         (Σ ((x : X) → A x) λ g → (x : X) → P x (g x))
Σ-univ _ = let open Iso in iso→eqv λ where
  .f h → pr₁ ∘ h , pr₂ ∘ h
  .g h x → pr₁ h x , pr₂ h x
  .η h → funext (Σ-uniq ∘ h)
  .ε h → Σ-uniq h

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott