text:
module IID-Proof where

import Logic.ChainReasoning as Chain

open import LF
open import Identity
open import IID
open import IIDr
open import IID-Proof-Setup
open import DefinitionalEquality

Ug : {I : Set} -> OPg I -> I -> Set
Ug γ i = Ur (ε γ) i

introg : {I : Set}(γ : OPg I)(a : Args γ (Ug γ)) -> Ug γ (index γ (Ug γ) a)
introg γ a = intror (g→rArgs γ (Ug γ) a)

-- The elimination rule.
elim-Ug : {I : Set}(γ : OPg I)(C : (i : I) -> Ug γ i -> Set) ->
          ((a : Args γ (Ug γ)) -> IndHyp γ (Ug γ) C a -> C (index γ (Ug γ) a) (introg γ a)) ->
          (i : I)(u : Ug γ i) -> C i u
elim-Ug {I} γ C m = elim-Ur (ε γ) C step    -- eliminate the restricted type
  where
    U = Ug γ

    -- we've got a method to take care of inductive occurrences for general families (m),
    -- but we need something to handle the restricted encoding.
    step : (i : I)(a : rArgs (ε γ) U i) -> IndHyp (ε γ i) U C a -> C i (intror a)
    step i a h = conclusion
      where
        -- First convert the argument to a general argument
        a' : Args γ U
        a' = r→gArgs γ U i a

        -- Next convert our induction hypothesis to an hypothesis for a general family
        h' : IndHyp γ U C a'
        h' = r→gIndHyp γ U C i a h

        -- Our method m can be applied to the converted argument and induction
        -- hypothesis. This gets us almost all the way.
        lem₁ : C (index γ U a') (intror (g→rArgs γ U a'))
        lem₁ = m a' h'

        -- Now we just have to use the fact that the computed index is the same
        -- as our input index, and that g→rArgs ∘ r→gArgs is the identity.
        -- r←→gArgs-subst will perform the elimination of the identity proof.
        conclusion : C i (intror a)
        conclusion = r←→gArgs-subst γ U (\i a -> C i (intror a)) i a lem₁

open module Chain-≡ = Chain.Poly.Heterogenous _≡_ (\x -> refl-≡) trans-≡

-- What remains is to prove that the reduction behaviour of the elimination
-- rule is the correct one. I.e that
--  elim-Ug C m (index a) (introg a) ≡ m a (induction C (elim-Ug C m) a)
elim-Ug-reduction :
    {I : Set}(γ : OPg I)(C : (i : I) -> Ug γ i -> Set)
    (m : (a : Args γ (Ug γ)) -> IndHyp γ (Ug γ) C a -> C (index γ (Ug γ) a) (introg γ a))
    (a : Args γ (Ug γ)) ->
    elim-Ug γ C m (index γ (Ug γ) a) (introg γ a)
    ≡ m a (induction γ (Ug γ) C (elim-Ug γ C m) a)
elim-Ug-reduction γ C m a =

 chain> elim-Ug γ C m (index γ (Ug γ) a) (introg γ a)

      -- Unfolding the definition of elim-Ug we get
    === r←→gArgs-subst γ U C' i ra
          (m gra (r→gih \hyp -> elim-Ug γ C m (r-ind-index hyp) (r-ind-value hyp)))
    by  refl-≡

     -- Now (and this is the key step), since we started with a value in the
     -- generalised type we know that the identity proof is refl, so
     -- r←→gArgs-subst is the identity.
    === m gra (r→gih \hyp -> elim-Ug γ C m (r-ind-index hyp) (r-ind-value hyp))
    by  r←→gArgs-subst-identity γ U C' a _

    -- We use congruence to prove separately that gra ≡ a and that the computed
    -- induction hypothesis is the one we need.
    === m a (\hyp -> elim-Ug γ C m (g-ind-index hyp) (g-ind-value hyp))
    by  cong₂-≡' m (g←→rArgs-identity γ U a)

        -- The induction hypotheses match
        (η-≡ \hyp₀ hyp₁ hyp₀=hyp₁ ->
         chain> r→gih (\hyp -> elim-Ug γ C m (r-ind-index hyp) (r-ind-value hyp)) hyp₀

            -- Unfolding the definition of r→gih we get
            === g→rIndArg-subst γ U C i ra hyp₀
                  (elim-Ug γ C m (r-ind-index (g→rIndArg γ U i ra hyp₀))
                                 (r-ind-value (g→rIndArg γ U i ra hyp₀))
                  )
            by  refl-≡

            -- g→rIndArg-subst is definitionally the identity.
            === elim-Ug γ C m (r-ind-index (g→rIndArg γ U i ra hyp₀))
                              (r-ind-value (g→rIndArg γ U i ra hyp₀))

            by  g→rIndArg-subst-identity γ U C i ra hyp₀ _

            -- We can turn the restricted inductive occurrence into a
            -- generalised occurrence.
            === elim-Ug γ C m (IndIndex γ U gra hyp₀) (Ind γ U gra hyp₀)

            by  g→rIndArg-subst γ U
                  (\j b -> elim-Ug γ C m (r-ind-index (g→rIndArg γ U i ra hyp₀))
                                         (r-ind-value (g→rIndArg γ U i ra hyp₀))
                           ≡ elim-Ug γ C m j b
                  ) i ra hyp₀ refl-≡

            -- Finally we have gra ≡ a and hyp₀ ≡ hyp₁ so we're done.
            === elim-Ug γ C m (IndIndex γ U a hyp₁) (Ind γ U a hyp₁)

            by  cong₂-≡' (\a hyp -> elim-Ug γ C m (IndIndex γ U a hyp)
                                                  (Ind      γ U a hyp)
                         ) (g←→rArgs-identity γ U a) hyp₀=hyp₁
        )

    -- Writing it in a nicer way:
    === m a (induction γ (Ug γ) C (elim-Ug γ C m) a)
    by  refl-≡

  where
    U   = Ug γ
    i   = index γ U a
    ra  = g→rArgs γ U a
    gra = r→gArgs γ U i ra

    r→gih = r→gIndHyp γ U C i ra

    r-ind-index = IndIndex (ε γ i) (Ur (ε γ)) ra
    r-ind-value = Ind      (ε γ i) (Ur (ε γ)) ra

    g-ind-index = IndIndex γ U a
    g-ind-value = Ind      γ U a

    C'  = \i a -> C i (intror a)


text:
module CTL.Proof.AG where

open import CTL.Modalities.AG
open import FStream.Core
open import FStream.FVec
open import Library

-- TODO Maybe beautify syntax here and elsewhere
data proofAG' {ℓ₁ ℓ₂} {C : Container ℓ₁} : {n : ℕ} →
     (props : FVec' C (Set ℓ₂) n) → Set (ℓ₁ ⊔ ℓ₂) where
  []AG'  : proofAG' FNil'
  _▻AG'_ : ∀ {prop : Set ℓ₂} {n} {props : ⟦ C ⟧ (FVec' C (Set ℓ₂) n)} →
           prop → A (fmap proofAG' props) → proofAG' (FCons' prop props)

_pre⟨_▻AG' : ∀ {i ℓ₁ ℓ₂} {C : Container ℓ₁} {m n}
               {props : FVec' C (Set ℓ₂) m} {props' : FVec' C (Set ℓ₂) (suc n)}
            → proofAG' props → proofAG' props'
            → AG' {i} (props pre⟨ props' ▻⋯')
nowA ([]AG' pre⟨ (proof ▻AG' _) ▻AG') = proof
laterA ([]AG' pre⟨ (proof ▻AG' proofs) ▻AG') p =
  (proofs p) pre⟨ (proof ▻AG' proofs) ▻AG'
nowA ((proof ▻AG' _) pre⟨ _ ▻AG') = proof
laterA ((_ ▻AG' proofs) pre⟨ proofs' ▻AG') p =
  (proofs p) pre⟨ proofs' ▻AG'

⟨_▻AG' : ∀ {i} {ℓ₁ ℓ₂} {C : Container ℓ₁} {n}
           {props : FVec' C (Set ℓ₂) (suc n)}
       → proofAG' props → AG' {i} (FNil' pre⟨ props ▻⋯')
⟨ proofs ▻AG' = []AG' pre⟨ proofs ▻AG'

data proofAG {ℓ₁ ℓ₂} {C : Container ℓ₁} : {n : ℕ} →
     (props : FVec C (Set ℓ₂) n) → Set (ℓ₁ ⊔ ℓ₂) where
  []AG : proofAG FNil
  ConsAG : ∀ {n} {props : ⟦ C ⟧ (Set ℓ₂ × FVec C (Set ℓ₂) n)} →
    A (fmap (λ x → (proj₁ x) × (proofAG (proj₂ x))) props) → proofAG (FCons props)
  -- TODO This constructor type signature is an abomination and should be somehow rewritten with proofAG, but how??
  -- TODO props should be of type FVec C (Set ℓ₂) (suc n) maybe? Or is it easier this way?

mapAGlemma : ∀ {i} {ℓ₁ ℓ₂ ℓ₃} {C : Container ℓ₁}
             {A : Set ℓ₂} {f : A → Set ℓ₃} {m n} →
             (v : FVec C A m) →
             (v' : FVec C A (suc n)) →
             AG {i} ((vmap f v pre⟨ vmap f v' ▻⋯)) →
             AG {i} (map f (v pre⟨ v' ▻⋯))
nowA (mapAGlemma FNil (FCons x) proofs p) = nowA (proofs p) -- TODO Why can't I join this with the next line?
nowA (mapAGlemma (FCons x) v proofs p) = nowA (proofs p)
laterA (mapAGlemma FNil (FCons (shape , vals)) proofs p) p₁ =
  mapAGlemma (proj₂ (vals p)) (FCons (shape , vals)) (laterA (proofs p)) p₁
laterA (mapAGlemma (FCons (shape , vals)) v' proofs p) p₁ =
  mapAGlemma (proj₂ (vals p)) v' (laterA (proofs p)) p₁

mapAG : ∀ {i} {ℓ₁ ℓ₂ ℓ₃} {C : Container ℓ₁}
          {A : Set ℓ₂} {f : A → Set ℓ₃} {m n} →
        {v : FVec C A m} →
        {v' : FVec C A (suc n)} →
        AG {i} ((vmap f v pre⟨ vmap f v' ▻⋯)) →
        AG {i} (map f (v pre⟨ v' ▻⋯))
mapAG {v = v} {v' = v'} = mapAGlemma v v'

_pre⟨_▻AG : ∀ {i} {ℓ₁ ℓ₂} {C : Container ℓ₁} {m n}
              {props : FVec C (Set ℓ₂) m} {props' : FVec C (Set ℓ₂) (suc n)}
          → proofAG props
          → proofAG props'
          → AG {i} (props pre⟨ props' ▻⋯)
nowA ( ([]AG pre⟨ (ConsAG proofs) ▻AG) p) = proj₁ (proofs p)
laterA ( ([]AG pre⟨ (ConsAG proofs) ▻AG) p) p₁ =
  (proj₂ (proofs p) pre⟨ ConsAG proofs ▻AG) p₁
nowA ( ((ConsAG proofs) pre⟨ _ ▻AG) p) = proj₁ (proofs p)
laterA ( ((ConsAG proofs) pre⟨ proofs' ▻AG) p) p₁ =
  (proj₂ (proofs p) pre⟨ proofs' ▻AG) p₁
-- The p are the inputs (positions) from the side effects.

mapPreCycle : ∀ {i} {ℓ₁ ℓ₂ ℓ₃} {C : Container ℓ₁} {A : Set ℓ₂}
                {f : A → Set ℓ₃} {m n}
            → (v : FVec C A m) → (v' : FVec C A (suc n))
            → proofAG (vmap f v) → proofAG (vmap f v')
            → AG {i} (map f (v pre⟨ v' ▻⋯))
nowA (mapPreCycle FNil (FCons x) []AG (ConsAG proofs) p)
      with proofs p
...   | proof , proofs' = proof
laterA (mapPreCycle FNil (FCons (shape , vals)) []AG (ConsAG proofs) p) p'
      with proofs p
...   | proof , proofs'
      with vals p
...   | a , v = mapPreCycle v (FCons (shape , vals)) proofs' (ConsAG proofs) p'
nowA (mapPreCycle (FCons x) v' (ConsAG proofs) proofs' p) = proj₁ (proofs p)
laterA (mapPreCycle (FCons (shape , vals)) (FCons x) (ConsAG proofs) proofs' p) p₁
      with proofs p
...   | proof , proofs''
      with vals p
...   | a , v = mapPreCycle v (FCons x) proofs'' proofs' p₁

infixr 5 _▻AG_
infix 6 ⟨_▻AG
infix 7 _⟩AG

⟨_▻AG : ∀ {i} {ℓ₁ ℓ₂} {C : Container ℓ₁} {n}
      → {props : FVec C (Set ℓ₂) (suc n)}
      → proofAG props
      → AG {i} (FNil pre⟨ props ▻⋯)
⟨_▻AG = []AG pre⟨_▻AG

_⟩AG : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁} {prop : ⟦ C ⟧ (Set ℓ₂)}
     → A prop
     → proofAG (FCons (fmap (_, FNil) prop))
x ⟩AG = ConsAG (λ p → x p , []AG)

_▻AG_ : ∀ {ℓ₁ ℓ₂} {C : Container ℓ₁}
          {prop : ⟦ C ⟧ (Set ℓ₂)} {n} {props : FVec C (Set ℓ₂) n}
      → A prop → proofAG props
      → proofAG (FCons (fmap (_, props) prop))
x ▻AG v = ConsAG (λ p → (x p) , v)

ext: agda

max_stars_repo_name: Aerate/condatis

max_issues_repo_name: zimbatm/condatis

max_forks_repo_name: zimbatm/condatis


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

module LogicalFramework.Equality where

module LF where
  postulate
    D     : Set
    _≡_   : D → D → Set
    refl  : ∀ {x} → x ≡ x
    subst : (A : D → Set) → ∀ {x y} → x ≡ y → A x → A y

  sym : ∀ {x y} → x ≡ y → y ≡ x
  sym {x} h = subst (λ t → t ≡ x) h refl

  trans : ∀ {x y z} → x ≡ y → y ≡ z → x ≡ z
  trans {x} h₁ h₂ = subst (_≡_ x) h₂ h₁

module Inductive where

  open import Common.FOL.FOL-Eq
  open import Common.FOL.Relation.Binary.EqReasoning

  sym-er : ∀ {x y} → x ≡ y → y ≡ x
  sym-er {x} h = subst (λ t → t ≡ x) h refl

  trans-er : ∀ {x y z} → x ≡ y → y ≡ z → x ≡ z
  trans-er {x} h₁ h₂ = subst (_≡_ x) h₂ h₁

  -- NB. The proofs of sym and trans by pattern matching are in the
  -- module Common.FOL.Relation.Binary.PropositionalEquality.

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------------
-- Properties for the relation LTC
------------------------------------------------------------------------------

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

module FOTC.Data.List.WF-Relation.LT-Cons.PropertiesI where

open import FOTC.Base
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.List
open import FOTC.Data.List.PropertiesI
open import FOTC.Data.List.WF-Relation.LT-Cons
open import FOTC.Data.List.WF-Relation.LT-Length

------------------------------------------------------------------------------
-- LTC ⊆ LTL.
LTC→LTL : ∀ {xs ys} → List xs → LTC xs ys → LTL xs ys
LTC→LTL Lxs (x , refl) = lg-x<lg-x∷xs x Lxs


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Subset.Setoid.Properties directly.
------------------------------------------------------------------------

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

module Data.List.Relation.Subset.Setoid.Properties where

open import Data.List.Relation.Binary.Subset.Setoid.Properties public

{-# WARNING_ON_IMPORT
"Data.List.Relation.Subset.Setoid.Properties was deprecated in v1.0.
Use Data.List.Relation.Binary.Subset.Setoid.Properties instead."
#-}


text:
module _ where

module M₁ (_ : Set) where

  postulate
    A : Set

record R : Set₁ where
  field
    A : Set

module M₂ (r : R) where

  open M₁ (R.A r) public

module Unused (A : Set) (_ : Set) where

  open M₁ A public

postulate
  r : R

open M₂ r

postulate
  P : A → Set

data D : Set where
  c : D

F : D → Set
F c = A

_ : ∀ x → F x → Set
_ = λ _ r → P r

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


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

module PropsAsTypes where

data Σ {I : Set} (X : I → Set) : Set where
  _,_ : (i : I) → X i → Σ X

drec-Σ :  {I : Set} {X : I → Set} {A : Σ X → Set} →
          ((i : I) → (x : X i) → A (i , x)) →
          (u : Σ X) → A u
drec-Σ f (i , x) = f i x

π₁ : {I : Set} {X : I → Set} → Σ X → I
π₁ = drec-Σ (λ i x → i)

π₂ : {I : Set} {X : I → Set} → (u : Σ X) → X (π₁ u)
π₂ = drec-Σ (λ i x → x)

_×_ : Set → Set → Set
A × B = Σ {A} λ _ → B

Prop = Set

Pred : Set → Set₁
Pred A = A → Prop

Rel : Set → Set₁
Rel A = A → A → Prop

_⊆_ : {A : Set} → Pred A → Pred A → Prop
P ⊆ Q = ∀ x → P x → Q x

_⊑_ : {A : Set} → Rel A → Rel A → Prop
R ⊑ S = ∀ {x y} → R x y → S x y

_∧_ : Prop → Prop → Prop
A ∧ B = A × B

∧-elim₁ : {A₁ A₂ : Prop} → A₁ ∧ A₂ → A₁
∧-elim₁ = π₁

∧-elim₂ : {A₁ A₂ : Prop} → A₁ ∧ A₂ → A₂
∧-elim₂ = π₂

∧-intro : {A₁ A₂ : Prop} → A₁ → A₂ → A₁ ∧ A₂
∧-intro a₁ a₂ = (a₁ , a₂)

∃ : {X : Set} → (A : X → Prop) → Prop
∃ = Σ

∃-syntax : ∀ X → (X → Prop) → Prop
∃-syntax X A = ∃ A

syntax ∃-syntax X (λ x → A) = ∃[ x ∈ X ] A

∃-intro : {X : Set} {A : X → Prop} → (x : X) → A x → ∃[ x ∈ X ] (A x)
∃-intro x a = (x , a)

∃-elim :  {X : Set} {A : X → Prop} {B : Prop} →
          ((x : X) → A x → B) → ∃[ x ∈ X ] (A x) → B
∃-elim = drec-Σ

∃₂-elim :  {X Y : Set} {A : X → Prop} {B : Y → Prop} {C : Prop} →
           ((x : X) (y : Y) → A x → B y → C) →
           ∃[ x ∈ X ] (A x) → ∃[ x ∈ Y ] (B x) → C
∃₂-elim f p q = ∃-elim (λ x p' → ∃-elim (λ y q' → f x y p' q') q) p

infix 3 _⇔_

_⇔_ : Prop → Prop → Prop
A ⇔ B = (A → B) ∧ (B → A)

equivalence : {A B : Prop} → (A → B) → (B → A) → A ⇔ B
equivalence = ∧-intro

data ⊥ : Prop where
  absurd : ⊥ → ⊥

⊥-elim : {A : Prop} → ⊥ → A
⊥-elim (absurd p) = ⊥-elim p

¬ : Prop → Prop
¬ A = A → ⊥

data ⊤ : Prop where
  ∗ : ⊤

open import Data.Nat
open import Relation.Binary.PropositionalEquality as PE

IsSuc : ℕ → Set
IsSuc zero    = ⊥
IsSuc (suc _) = ⊤

zero-not-suc : ∀ n → ¬ (suc n ≡ 0)
zero-not-suc n p = subst IsSuc p ∗

-- Easier in Agda with absurd elimination
-- suc-injective : ∀ n → ¬ (suc n ≡ n)
-- suc-injective n ()

drec-≡ : {X : Set} → {C : (x y : X) → x ≡ y → Set} →
         ((x : X) → C x x refl) →
         ∀ x y → (p : x ≡ y) → C x y p
drec-≡ f x .x refl = f x

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


text:
module RecordUpdateSyntax where

data ⊤ : Set where
  tt : ⊤

record R : Set where
  field
    a b : ⊤

test : R
test = record {!!} { a = tt }

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------------
-- Distributive laws on a binary operation: Lemma 4
------------------------------------------------------------------------------

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

module DistributiveLaws.Lemma4-ATP where

open import DistributiveLaws.Base

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

postulate lemma-4a : ∀ x y z → ((x · x ) · y) · z ≡ (x · y) · z
{-# ATP prove lemma-4a #-}

postulate lemma-4b : ∀ x y z → (x · (y · (z · z))) ≡ x · (y · z)
{-# ATP prove lemma-4b #-}


text:
module Container.Bag where

open import Prelude

Bag : Set → Set
Bag A = List (Nat × A)

FunctorBag : Functor Bag
fmap {{FunctorBag}} f b = map (second f) b

union : {A : Set} {{OrdA : Ord A}} → Bag A → Bag A → Bag A
union a [] = a
union [] b = b
union ((i , x) ∷ a) ((j , y) ∷ b) with compare x y
... | less    _ = (i , x) ∷ union a ((j , y) ∷ b)
... | equal   _ = (i + j , x) ∷ union a b
... | greater _ = (j , y) ∷ union ((i , x) ∷ a) b

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


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

data _==_ {A : Set} (a : A) : A → Set where
  idp : a == a
{-# BUILTIN REWRITE _==_ #-}

ap : {A B : Set} (f : A → B) {x y : A} →
  x == y → f x == f y
ap f idp = idp

{- Circle -}
postulate
  Circle : Set
  base : Circle
  loop : base == base

module _ (P : Set) (base* : P) (loop* : base* == base*) where

  postulate
    Circle-rec : Circle → P
    Circle-base-recβ : Circle-rec base == base*
  {-# REWRITE Circle-base-recβ #-}

f : Circle → Circle
f = Circle-rec Circle base loop

postulate
  rewr : ap (λ z → f (f z)) loop == loop
{-# REWRITE rewr #-}

test : ap (λ z → f (f z)) loop == loop
test = idp

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
-- Alternating addition (Also called the Calkin-Wilf tree representation of the rationals).
-- One bijective representation of ℚ. That is, every rational number is appearing exactly once in this representation (TODO: Some proof would be nice).
module Numeral.Rational.AlterAdd where

import      Lvl
open import Data
open import Data.Boolean
open import Logic.Propositional
open import Numeral.Natural             as ℕ
import      Numeral.Natural.Oper        as ℕ
import      Numeral.Natural.Oper.Comparisons as ℕ
open import Numeral.PositiveInteger      as ℕ₊
open import Numeral.PositiveInteger.Oper as ℕ₊
open import Numeral.Integer using (ℤ)
open import Syntax.Number
open import Type

module Test1 where
  data Tree : ℕ₊ → ℕ₊ → Type{Lvl.𝟎} where
    intro : Tree(1)(1)
    left  : ∀{x y} → Tree(x)(y) → Tree(x) (y ℕ₊.+ x)
    right : ∀{x y} → Tree(x)(y) → Tree(x ℕ₊.+ y) (y)

  -- Tree-cancellationₗ : ∀{x₁ x₂ y} → (Tree x₁ y ≡ Tree x₂ y) → (x₁ ≡ x₂)

  {- TODO: Is there an algorithm that determines the path to every rational in this tree? Maybe the division algorithm:
  R6 (14928,2395)
  L4 (558,2395) 14928−2395⋅6 = 558
  R3 (558,163) 2395−558⋅4 = 163
  L2 (69,163) 558−163⋅3 = 69
  R2 (69,25) 163−69⋅2 = 25
  L1 (19,25) 69−25⋅2 = 19
  R3 (19,6) 25-19 = 6
  L5 (1,6) 19-6⋅3 = 1
  In (1,1) 6−1⋅5 = 1
  f(R$R$R$R$R$R $ L$L$L$L $ R$R$R $ L$L $ R$R $ L $ R$R$R $ L$L$L$L$L $ Init)
  If this is the case, then just represent the tree by: (Tree = List(Bool)) or (Tree = List(Either ℕ ℕ)) or (Tree = List(ℕ)) ?-}

  {-
  open import Data.Option
  Tree-construct : (x : ℕ₊) → (y : ℕ₊) → Tree(x)(y)
  Tree-construct ℕ₊.𝟏        ℕ₊.𝟏         = intro
  Tree-construct ℕ₊.𝟏        (𝐒 y)        = left(Tree-construct ℕ₊.𝟏 y)
  Tree-construct (𝐒 x)       ℕ₊.𝟏         = right(Tree-construct x ℕ₊.𝟏)
  Tree-construct(x@(ℕ₊.𝐒 _)) (y@(ℕ₊.𝐒 _)) with (x −₀ y)
  ... | Some z = {!right(Tree-construct(z)(y))!}
  ... | None   = {!left (Tree-construct(x)(y ℕ.−₀ x))!}
  -}

  -- _+_ : Tree(a₁)(b₁) → Tree(a₂)(b₂) →
  -- _⋅_ : Tree(a₁)(b₁) → Tree(a₂)(b₂) →

  data ℚ : Type{Lvl.𝟎} where
    𝟎  : ℚ
    _/₋_ : (x : ℕ₊) → (y : ℕ₊) → ⦃ _ : Tree(x)(y) ⦄ → ℚ
    _/₊_ : (x : ℕ₊) → (y : ℕ₊) → ⦃ _ : Tree(x)(y) ⦄ → ℚ

  {-
  _/_ : (x : ℤ) → (y : ℤ) → ℚ
  _/_ 𝟎 _ = 𝟎
  _/_ _ 𝟎 = 𝟎
  _/_ (𝐒(x)) (𝐒(y)) with sign(x) ⋅ sign(y)
  ... | [−] = (x /₋ y) ⦃ Tree-construction-algorithm(x)(y) ⦄
  ... | [+] = (x /₊ y) ⦃ Tree-construction-algorithm(x)(y) ⦄
  -}

  {-
  a₁/(a₁+b₁)
  (a₂+b₂)/b₂
  -}

  {-
  from-ℕ : ℕ → ℚ
  from-ℕ(𝟎)    = 𝟎
  from-ℕ(𝐒(n)) = (𝐒(n) /₊ 1) where
    instance
      f : (n : ℕ) → Tree(𝐒(n))(1)
      f(𝟎)    = Tree-intro
      f(𝐒(n)) = Tree-right(f(n))
  -}

  {-
  floor : ℚ → ℕ
  floor(x / y) = x ℕ.⌊/⌋ y

  ceil : ℚ → ℕ
  ceil(x / y) = x ℕ.⌈/⌉ y
  -}

{-
module Test2 where
  open import Data.Tuple as Tuple using (_⨯_ ; _,_)
  open import Functional

  data Tree : Type{Lvl.𝟎} where
    intro : Tree
    left  : Tree → Tree
    right : Tree → Tree

  Tree-quotient : Tree → (ℕ ⨯ ℕ)
  Tree-quotient intro                                    = (1       , 1      )
  Tree-quotient (left  t) with (x , y) ← Tree-quotient t = (x       , x ℕ.+ y)
  Tree-quotient (right t) with (x , y) ← Tree-quotient t = (x ℕ.+ y , y      )

  Tree-denominator : Tree → ℕ
  Tree-denominator = Tuple.right ∘ Tree-quotient

  Tree-numerator : Tree → ℕ
  Tree-numerator = Tuple.left ∘ Tree-quotient
-}

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:
------------------------------------------------------------------------
-- The values that are used by the NBE algorithm
------------------------------------------------------------------------

import Level
open import Data.Universe

module README.DependentlyTyped.NBE.Value
  (Uni₀ : Universe Level.zero Level.zero)
  where

import Axiom.Extensionality.Propositional as E
open import Data.Product renaming (curry to c; uncurry to uc)
open import deBruijn.Substitution.Data
open import Function using (id; _ˢ_; _$_) renaming (const to k)
import README.DependentlyTyped.NormalForm as NF; open NF Uni₀
import README.DependentlyTyped.NormalForm.Substitution as NFS
open NFS Uni₀
import README.DependentlyTyped.Term as Term; open Term Uni₀
open import Relation.Binary.PropositionalEquality as P using (_≡_)
import Relation.Binary.PropositionalEquality.WithK as P

open P.≡-Reasoning

-- A wrapper which is used to make V̌alue "constructor-headed", which
-- in turn makes Agda infer more types for us.

infix 3 _⊢_⟨ne⟩

record _⊢_⟨ne⟩ (Γ : Ctxt) (σ : Type Γ) : Set where
  constructor [_]el
  field t : Γ ⊢ σ ⟨ ne ⟩

mutual

  -- The values.

  V̌alue′ : ∀ Γ sp (σ : IType Γ sp) → Set
  V̌alue′ Γ ⋆           σ = Γ ⊢ ⋆  , σ ⟨ ne ⟩
  V̌alue′ Γ el          σ = Γ ⊢ el , σ ⟨ne⟩
  V̌alue′ Γ (π sp₁ sp₂) σ =
    Σ (V̌alue-π Γ sp₁ sp₂ σ) (W̌ell-behaved sp₁ sp₂ σ)

  V̌alue : (Γ : Ctxt) (σ : Type Γ) → Set
  V̌alue Γ (sp , σ) = V̌alue′ Γ sp σ

  V̌alue-π : ∀ Γ sp₁ sp₂ → IType Γ (π sp₁ sp₂) → Set
  V̌alue-π Γ sp₁ sp₂ σ =
    (Γ₊ : Ctxt₊ Γ)
    (v : V̌alue′ (Γ ++₊ Γ₊) sp₁ (ifst σ /̂I ŵk₊ Γ₊)) →
    V̌alue′ (Γ ++₊ Γ₊) sp₂ (isnd σ /̂I ŵk₊ Γ₊ ↑̂ ∘̂ ŝub ⟦̌ v ⟧)

    -- The use of Ctxt₊ rather than Ctxt⁺ in V̌alue-π is important: it
    -- seems to make it much easier to define weakening for V̌alue.

  W̌ell-behaved :
    ∀ {Γ} sp₁ sp₂ σ → V̌alue-π Γ sp₁ sp₂ σ → Set
  W̌ell-behaved {Γ} sp₁ sp₂ σ f =
    ∀ Γ₊ v → (⟦̌ σ ∣ f ⟧-π /̂Val ŵk₊ Γ₊) ˢ ⟦̌ v ⟧ ≅-Value ⟦̌ f Γ₊ v ⟧

  -- The semantics of a value.

  ⟦̌_⟧ : ∀ {Γ sp σ} → V̌alue′ Γ sp σ → Value Γ (sp , σ)
  ⟦̌ v ⟧ = ⟦ řeify _ v ⟧n

  ⟦̌_∣_⟧-π : ∀ {Γ sp₁ sp₂} σ →
            V̌alue-π Γ sp₁ sp₂ σ → Value Γ (π sp₁ sp₂ , σ)
  ⟦̌ _ ∣ f ⟧-π = ⟦ řeify-π _ _ _ f ⟧n

  -- Neutral terms can be turned into normal terms using reflection
  -- followed by reification.

  ňeutral-to-normal :
    ∀ {Γ} sp {σ} → Γ ⊢ sp , σ ⟨ ne ⟩ → Γ ⊢ sp , σ ⟨ no ⟩
  ňeutral-to-normal sp t = řeify sp (řeflect sp t)

  -- A normal term corresponding to variable zero.

  žero : ∀ {Γ} sp σ → Γ ▻ (sp , σ) ⊢ sp , σ /̂I ŵk ⟨ no ⟩
  žero sp σ = ňeutral-to-normal sp (var zero[ -, σ ])

  -- Reification.

  řeify : ∀ {Γ} sp {σ} → V̌alue′ Γ sp σ → Γ ⊢ sp , σ ⟨ no ⟩
  řeify ⋆           t       = ne ⋆  t
  řeify el          [ t ]el = ne el t
  řeify (π sp₁ sp₂) f       = řeify-π sp₁ sp₂ _ (proj₁ f)

  řeify-π : ∀ {Γ} sp₁ sp₂ σ →
            V̌alue-π Γ sp₁ sp₂ σ → Γ ⊢ π sp₁ sp₂ , σ ⟨ no ⟩
  řeify-π {Γ} sp₁ sp₂ σ f = čast sp₁ σ $
    ƛ (řeify sp₂ (f (fst σ ◅ ε) (řeflect sp₁ (var zero))))

  čast : ∀ {Γ} sp₁ {sp₂} (σ : IType Γ (π sp₁ sp₂)) →
         let ρ̂ = ŵk ↑̂ ∘̂ ŝub ⟦ žero sp₁ (ifst σ) ⟧n in
         Γ ⊢ Type-π (fst σ) (snd σ /̂ ρ̂) ⟨ no ⟩ →
         Γ ⊢ -, σ ⟨ no ⟩
  čast {Γ} sp₁ σ =
    P.subst (λ σ → Γ ⊢ σ ⟨ no ⟩)
            (≅-Type-⇒-≡ $ π-fst-snd-ŵk-ŝub-žero sp₁ σ)

  -- Reflection.

  řeflect : ∀ {Γ} sp {σ} → Γ ⊢ sp , σ ⟨ ne ⟩ → V̌alue Γ (sp , σ)
  řeflect ⋆           t = t
  řeflect el          t = [ t ]el
  řeflect (π sp₁ sp₂) t =
    (λ Γ₊ v → řeflect sp₂ ((t /⊢n Renaming.wk₊ Γ₊) · řeify sp₁ v)) ,
    řeflect-π-well-behaved sp₁ sp₂ t

  abstract

    řeflect-π-well-behaved :
      ∀ {Γ} sp₁ sp₂ {σ} (t : Γ ⊢ π sp₁ sp₂ , σ ⟨ ne ⟩) Γ₊ v →
      let t′ = ňeutral-to-normal sp₂
                 ((t /⊢n Renaming.wk) · žero sp₁ (ifst σ)) in
      (⟦ čast sp₁ σ (ƛ t′) ⟧n /̂Val ŵk₊ Γ₊) ˢ ⟦̌ v ⟧
        ≅-Value
      ⟦ ňeutral-to-normal sp₂ ((t /⊢n Renaming.wk₊ Γ₊) · řeify sp₁ v) ⟧n
    řeflect-π-well-behaved sp₁ sp₂ {σ} t Γ₊ v =
      let t′ = ňeutral-to-normal sp₂
                 ((t /⊢n Renaming.wk) · žero sp₁ (ifst σ))
          v′ = řeify sp₁ v

          lemma′ = begin
            [ ⟦ čast sp₁ σ (ƛ t′) ⟧n /̂Val ŵk₊ Γ₊ ]  ≡⟨ /̂Val-cong (ňeutral-to-normal-identity-π sp₁ sp₂ t) P.refl ⟩
            [ ⟦ t ⟧n                 /̂Val ŵk₊ Γ₊ ]  ≡⟨ t /⊢n-lemma Renaming.wk₊ Γ₊ ⟩
            [ ⟦ t /⊢n Renaming.wk₊ Γ₊ ⟧n         ]  ∎

      in begin
      [ (⟦ čast sp₁ σ (ƛ t′) ⟧n /̂Val ŵk₊ Γ₊) ˢ ⟦ v′ ⟧n            ]  ≡⟨ ˢ-cong lemma′ P.refl ⟩
      [ ⟦ t /⊢n Renaming.wk₊ Γ₊ ⟧n           ˢ ⟦ v′ ⟧n            ]  ≡⟨ P.refl ⟩
      [ ⟦ (t /⊢n Renaming.wk₊ Γ₊) · v′ ⟧n                         ]  ≡⟨ P.sym $ ňeutral-to-normal-identity sp₂ _ ⟩
      [ ⟦ ňeutral-to-normal sp₂ ((t /⊢n Renaming.wk₊ Γ₊) · v′) ⟧n ]  ∎

    -- A given context morphism is equal to the identity.

    ŵk-ŝub-žero :
      ∀ {Γ} sp₁ {sp₂} (σ : IType Γ (π sp₁ sp₂)) →
      ŵk ↑̂ fst σ ∘̂ ŝub ⟦ žero sp₁ (ifst σ) ⟧n ≅-⇨̂ îd[ Γ ▻ fst σ ]
    ŵk-ŝub-žero sp₁ σ = begin
      [ ŵk ↑̂ ∘̂ ŝub ⟦ žero sp₁ (ifst σ) ⟧n ]  ≡⟨ ∘̂-cong (P.refl {x = [ ŵk ↑̂ ]})
                                                       (ŝub-cong (ňeutral-to-normal-identity sp₁ (var zero))) ⟩
      [ ŵk ↑̂ ∘̂ ŝub ⟦ var zero          ⟧n ]  ≡⟨ P.refl ⟩
      [ îd                                ]  ∎

    -- A corollary of the lemma above.

    π-fst-snd-ŵk-ŝub-žero :
      ∀ {Γ} sp₁ {sp₂} (σ : IType Γ (π sp₁ sp₂)) →
      Type-π (fst σ) (snd σ /̂ ŵk ↑̂ ∘̂ ŝub ⟦ žero sp₁ (ifst σ) ⟧n) ≅-Type
      (-, σ)
    π-fst-snd-ŵk-ŝub-žero sp₁ σ = begin
      [ Type-π (fst σ) (snd σ /̂ ŵk ↑̂ ∘̂ ŝub ⟦ žero sp₁ (ifst σ) ⟧n) ]  ≡⟨ Type-π-cong $ /̂-cong (P.refl {x = [ snd σ ]})
                                                                                (ŵk-ŝub-žero sp₁ σ) ⟩
      [ Type-π (fst σ) (snd σ)                                     ]  ≡⟨ P.refl ⟩
      [ -, σ                                                       ]  ∎

    -- In the semantics řeify is a left inverse of řeflect.

    ňeutral-to-normal-identity :
      ∀ {Γ} sp {σ} (t : Γ ⊢ sp , σ ⟨ ne ⟩) →
      ⟦ ňeutral-to-normal sp t ⟧n ≅-Value ⟦ t ⟧n
    ňeutral-to-normal-identity ⋆           t = P.refl
    ňeutral-to-normal-identity el          t = P.refl
    ňeutral-to-normal-identity (π sp₁ sp₂) t =
      ňeutral-to-normal-identity-π sp₁ sp₂ t

    ňeutral-to-normal-identity-π :
      ∀ {Γ} sp₁ sp₂ {σ} (t : Γ ⊢ π sp₁ sp₂ , σ ⟨ ne ⟩) →
      let t′ = ňeutral-to-normal sp₂
                 ((t /⊢n Renaming.wk) · žero sp₁ (ifst σ)) in
      ⟦ čast sp₁ σ (ƛ t′) ⟧n ≅-Value ⟦ t ⟧n
    ňeutral-to-normal-identity-π sp₁ sp₂ {σ} t =
      let t′ = (t /⊢n Renaming.wk) · žero sp₁ (ifst σ)

          lemma = begin
            [ ⟦ ňeutral-to-normal sp₂ t′ ⟧n                   ]  ≡⟨ ňeutral-to-normal-identity sp₂ t′ ⟩
            [ ⟦ t′ ⟧n                                         ]  ≡⟨ P.refl ⟩
            [ ⟦ t /⊢n Renaming.wk ⟧n ˢ ⟦ žero sp₁ (ifst σ) ⟧n ]  ≡⟨ ˢ-cong (P.sym $ t /⊢n-lemma Renaming.wk)
                                                                           (ňeutral-to-normal-identity sp₁ (var zero)) ⟩
            [ (⟦ t ⟧n /̂Val ŵk)       ˢ lookup zero            ]  ≡⟨ P.refl ⟩
            [ uc ⟦ t ⟧n                                       ]  ∎

      in begin
      [ ⟦ čast sp₁ σ (ƛ (ňeutral-to-normal sp₂ t′)) ⟧n ]  ≡⟨ ⟦⟧n-cong $ drop-subst-⊢n id (≅-Type-⇒-≡ $ π-fst-snd-ŵk-ŝub-žero sp₁ σ) ⟩
      [ c ⟦ ňeutral-to-normal sp₂ t′ ⟧n                ]  ≡⟨ curry-cong lemma ⟩
      [ c {C = k El ˢ isnd σ} (uc ⟦ t ⟧n)              ]  ≡⟨ P.refl ⟩
      [ ⟦ t ⟧n                                         ]  ∎

-- An immediate consequence of the somewhat roundabout definition
-- above.

w̌ell-behaved :
  ∀ {Γ sp₁ sp₂ σ} (f : V̌alue Γ (π sp₁ sp₂ , σ)) →
  ∀ Γ₊ v → (⟦̌_⟧ {σ = σ} f /̂Val ŵk₊ Γ₊) ˢ ⟦̌ v ⟧ ≅-Value ⟦̌ proj₁ f Γ₊ v ⟧
w̌ell-behaved = proj₂

-- Values are term-like.

V̌al : Term-like _
V̌al = record
  { _⊢_ = V̌alue
  ; ⟦_⟧ = ⟦̌_⟧
  }

open Term-like V̌al public
  using ([_])
  renaming ( _≅-⊢_ to _≅-V̌alue_
           ; drop-subst-⊢ to drop-subst-V̌alue; ⟦⟧-cong to ⟦̌⟧-cong
           )

abstract

  -- Unfolding lemma for ⟦̌_∣_⟧-π.

  unfold-⟦̌∣⟧-π :
    ∀ {Γ sp₁ sp₂} σ (f : V̌alue-π Γ sp₁ sp₂ σ) →
    ⟦̌ σ ∣ f ⟧-π ≅-Value c ⟦̌ f (fst σ ◅ ε) (řeflect sp₁ (var zero)) ⟧
  unfold-⟦̌∣⟧-π σ _ = ⟦⟧n-cong $
    drop-subst-⊢n id (≅-Type-⇒-≡ $ π-fst-snd-ŵk-ŝub-žero _ σ)

-- Some congruence/conversion lemmas.

≅-⊢n-⇒-≅-Value-⋆ : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ ⋆ , σ₁ ⟨ ne ⟩}
                     {Γ₂ σ₂} {t₂ : Γ₂ ⊢ ⋆ , σ₂ ⟨ ne ⟩} →
                   t₁ ≅-⊢n t₂ → t₁ ≅-V̌alue t₂
≅-⊢n-⇒-≅-Value-⋆ P.refl = P.refl

≅-Value-⋆-⇒-≅-⊢n : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ ⋆ , σ₁ ⟨ ne ⟩}
                     {Γ₂ σ₂} {t₂ : Γ₂ ⊢ ⋆ , σ₂ ⟨ ne ⟩} →
                   t₁ ≅-V̌alue t₂ → t₁ ≅-⊢n t₂
≅-Value-⋆-⇒-≅-⊢n P.refl = P.refl

≅-⊢n-⇒-≅-Value-el : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ el , σ₁ ⟨ ne ⟩}
                      {Γ₂ σ₂} {t₂ : Γ₂ ⊢ el , σ₂ ⟨ ne ⟩} →
                    t₁ ≅-⊢n t₂ → [ t₁ ]el ≅-V̌alue [ t₂ ]el
≅-⊢n-⇒-≅-Value-el P.refl = P.refl

≅-Value-el-⇒-≅-⊢n : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ el , σ₁ ⟨ ne ⟩}
                      {Γ₂ σ₂} {t₂ : Γ₂ ⊢ el , σ₂ ⟨ ne ⟩} →
                    [ t₁ ]el ≅-V̌alue [ t₂ ]el → t₁ ≅-⊢n t₂
≅-Value-el-⇒-≅-⊢n P.refl = P.refl

abstract

  ,-cong : E.Extensionality Level.zero Level.zero →
           ∀ {Γ sp₁ sp₂ σ} {f₁ f₂ : V̌alue Γ (π sp₁ sp₂ , σ)} →
           (∀ Γ₊ v → proj₁ f₁ Γ₊ v ≅-V̌alue proj₁ f₂ Γ₊ v) →
           _≅-V̌alue_ {σ₁ = (π sp₁ sp₂ , σ)} f₁
                     {σ₂ = (π sp₁ sp₂ , σ)} f₂
  ,-cong ext hyp = P.cong (Term-like.[_] {_} {V̌al}) $
    ,-cong′ (ext λ Γ₊ → ext λ v → Term-like.≅-⊢-⇒-≡ V̌al $ hyp Γ₊ v)
            (ext λ _  → ext λ _ → P.≡-irrelevant _ _)
    where
    ,-cong′ : {A : Set} {B : A → Set}
              {x₁ x₂ : A} {y₁ : B x₁} {y₂ : B x₂} →
              (eq : x₁ ≡ x₂) → P.subst B eq y₁ ≡ y₂ →
              _≡_ {A = Σ A B} (x₁ , y₁) (x₂ , y₂)
    ,-cong′ P.refl P.refl = P.refl

ňeutral-to-normal-cong :
  ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁ ⟨ ne ⟩}
    {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂ ⟨ ne ⟩} →
  t₁ ≅-⊢n t₂ → ňeutral-to-normal _ t₁ ≅-⊢n ňeutral-to-normal _ t₂
ňeutral-to-normal-cong P.refl = P.refl

žero-cong : ∀ {Γ₁} {σ₁ : Type Γ₁}
              {Γ₂} {σ₂ : Type Γ₂} →
            σ₁ ≅-Type σ₂ → žero _ (proj₂ σ₁) ≅-⊢n žero _ (proj₂ σ₂)
žero-cong P.refl = P.refl

řeify-cong : ∀ {Γ₁ σ₁} {v₁ : V̌alue Γ₁ σ₁}
               {Γ₂ σ₂} {v₂ : V̌alue Γ₂ σ₂} →
             v₁ ≅-V̌alue v₂ → řeify _ v₁ ≅-⊢n řeify _ v₂
řeify-cong P.refl = P.refl

řeflect-cong : ∀ {Γ₁ σ₁} {t₁ : Γ₁ ⊢ σ₁ ⟨ ne ⟩}
                 {Γ₂ σ₂} {t₂ : Γ₂ ⊢ σ₂ ⟨ ne ⟩} →
               t₁ ≅-⊢n t₂ → řeflect _ t₁ ≅-V̌alue řeflect _ t₂
řeflect-cong P.refl = P.refl

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Bags of integers, for Nehemiah plugin.
--
-- This module imports postulates about bags of integers
-- with negative multiplicities as a group under additive union.
------------------------------------------------------------------------

module Structure.Bag.Nehemiah where

open import Postulate.Bag-Nehemiah public

open import Relation.Binary.PropositionalEquality
open import Algebra using (CommutativeRing)
open import Algebra.Structures
open import Data.Integer
open import Data.Integer.Properties
  using ()
  renaming (+-*-commutativeRing to ℤ-is-commutativeRing)
open import Data.Product

infixl 9 _\\_ -- same as Data.Map.(\\)
_\\_ : Bag → Bag → Bag
d \\ b = d ++ (negateBag b)

-- Useful properties of abelian groups
commutative : ∀ {A : Set} {f : A → A → A} {z} →
  IsCommutativeMonoid _≡_ f z → (m n : A) → f m n ≡ f n m
commutative = IsCommutativeMonoid.comm

associative : ∀ {A : Set} {f : A → A → A} {z} →
  IsCommutativeMonoid _≡_ f z → (k m n : A) → f (f k m) n ≡ f k (f m n)
associative abelian = IsCommutativeMonoid.assoc abelian

left-inverse : ∀ {A : Set} {f : A → A → A} {z neg} →
  IsAbelianGroup _≡_ f z neg → (n : A) → f (neg n) n ≡ z
left-inverse abelian = proj₁ (IsAbelianGroup.inverse abelian)
right-inverse : ∀ {A : Set} {f : A → A → A} {z neg} →
  IsAbelianGroup _≡_ f z neg → (n : A) → f n (neg n) ≡ z
right-inverse abelian = proj₂ (IsAbelianGroup.inverse abelian)

left-identity : ∀ {A : Set} {f : A → A → A} {z neg} →
  IsAbelianGroup _≡_ f z neg → (n : A) → f z n ≡ n
left-identity abelian = proj₁ (IsMonoid.identity
  (IsGroup.isMonoid (IsAbelianGroup.isGroup abelian)))
right-identity : ∀ {A : Set} {f : A → A → A} {z neg} →
  IsAbelianGroup _≡_ f z neg → (n : A) → f n z ≡ n
right-identity abelian = proj₂ (IsMonoid.identity
  (IsGroup.isMonoid (IsAbelianGroup.isGroup abelian)))

instance
  abelian-int : IsAbelianGroup _≡_ _+_ (+ 0) (-_)
  abelian-int =
    CommutativeRing.+-isAbelianGroup ℤ-is-commutativeRing

  abelian→comm-monoid :
   ∀ {A : Set} {f : A → A → A} {z neg} →
   {{abel : IsAbelianGroup _≡_ f z neg}} → IsCommutativeMonoid _≡_ f z
  abelian→comm-monoid {{abel}} = IsAbelianGroup.isCommutativeMonoid abel

  comm-monoid-int : IsCommutativeMonoid _≡_ _+_ (+ 0)
  comm-monoid-int = IsAbelianGroup.isCommutativeMonoid abelian-int
  comm-monoid-bag : IsCommutativeMonoid _≡_ _++_ emptyBag
  comm-monoid-bag = IsAbelianGroup.isCommutativeMonoid abelian-bag

  import Data.Nat as N
  import Data.Nat.Properties as NP
  comm-monoid-nat : IsCommutativeMonoid _≡_ N._+_ 0
  comm-monoid-nat = IsCommutativeSemiring.+-isCommutativeMonoid NP.isCommutativeSemiring

commutative-int : (m n : ℤ) → m + n ≡ n + m
commutative-int = commutative comm-monoid-int
associative-int : (k m n : ℤ) → (k + m) + n ≡ k + (m + n)
associative-int = associative comm-monoid-int
right-inv-int : (n : ℤ) → n - n ≡ + 0
right-inv-int = right-inverse abelian-int
left-id-int : (n : ℤ) → (+ 0) + n ≡ n
left-id-int = left-identity abelian-int
right-id-int : (n : ℤ) → n + (+ 0) ≡ n
right-id-int = right-identity abelian-int

commutative-bag : (a b : Bag) → a ++ b ≡ b ++ a
commutative-bag = commutative comm-monoid-bag
associative-bag : (a b c : Bag) → (a ++ b) ++ c ≡ a ++ (b ++ c)
associative-bag = associative comm-monoid-bag
right-inv-bag : (b : Bag) → b \\ b ≡ emptyBag
right-inv-bag = right-inverse abelian-bag
left-id-bag : (b : Bag) → emptyBag ++ b ≡ b
left-id-bag = left-identity abelian-bag
right-id-bag : (b : Bag) → b ++ emptyBag ≡ b
right-id-bag = right-identity abelian-bag

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

open import Categories.Category

module Categories.Category.Construction.Properties.Presheaves.Cartesian {o ℓ e} (C : Category o ℓ e) where

open import Level
open import Data.Unit
open import Data.Product using (_,_)
open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Function.Equality using (Π) renaming (_∘_ to _∙_)
open import Relation.Binary

open import Categories.Category.Cartesian
open import Categories.Category.Construction.Presheaves
open import Categories.Category.Instance.Setoids
open import Categories.Functor
open import Categories.Functor.Properties
open import Categories.Functor.Presheaf
open import Categories.NaturalTransformation

import Categories.Object.Product as Prod
import Categories.Morphism.Reasoning as MR

open Π using (_⟨$⟩_)

module _ {o′ ℓ′ o″ ℓ″} where

  Presheaves× : ∀ (A : Presheaf C (Setoids o′ ℓ′)) (A : Presheaf C (Setoids o″ ℓ″)) → Presheaf C (Setoids (o′ ⊔ o″) (ℓ′ ⊔ ℓ″))
  Presheaves× A B = record
    { F₀           = λ X → ×-setoid (A.₀ X) (B.₀ X)
    ; F₁           = λ f → record
      { _⟨$⟩_ = λ { (a , b) → A.₁ f ⟨$⟩ a , B.₁ f ⟨$⟩ b }
      ; cong  = λ { (eq₁ , eq₂) → Π.cong (A.₁ f) eq₁ , Π.cong (B.₁ f) eq₂ }
      }
    ; identity     = λ { (eq₁ , eq₂)    → A.identity eq₁ , B.identity eq₂ }
    ; homomorphism = λ { (eq₁ , eq₂)    → A.homomorphism eq₁ , B.homomorphism eq₂ }
    ; F-resp-≈     = λ { eq (eq₁ , eq₂) → A.F-resp-≈ eq eq₁ , B.F-resp-≈ eq eq₂ }
    }
    where module A = Functor A
          module B = Functor B

module IsCartesian o′ ℓ′ where
  private
    module C = Category C
    open C
    P = Presheaves′ o′ ℓ′ C
    module P = Category P
    S = Setoids o′ ℓ′
    module S = Category S

  Presheaves-Cartesian : Cartesian P
  Presheaves-Cartesian = record
    { terminal = record
      { ⊤        = record
        { F₀           = λ x → record
          { Carrier       = Lift o′ ⊤
          ; _≈_           = λ _ _ → Lift ℓ′ ⊤
          ; isEquivalence = _
          }
        }
      ; !        = _
      ; !-unique = _
      }
    ; products = record
      { product = λ {A B} →
        let module A = Functor A
            module B = Functor B
        in record
        { A×B      = Presheaves× A B
        ; π₁       = ntHelper record
          { η       = λ X → record
            { _⟨$⟩_ = λ { (fst , _) → fst }
            ; cong  = λ { (eq , _)  → eq }
            }
          ; commute = λ { f (eq , _) → Π.cong (A.F₁ f) eq }
          }
        ; π₂       = ntHelper record
          { η       = λ X → record
            { _⟨$⟩_ = λ { (_ , snd) → snd }
            ; cong  = λ { (_ , eq)  → eq }
            }
          ; commute = λ { f (_ , eq) → Π.cong (B.F₁ f) eq }
          }
        ; ⟨_,_⟩    = λ {F} α β →
          let module F = Functor F
              module α = NaturalTransformation α
              module β = NaturalTransformation β
          in ntHelper record
          { η       = λ Y → record
            { _⟨$⟩_ = λ S → α.η Y ⟨$⟩ S , β.η Y ⟨$⟩ S
            ; cong  = λ eq → Π.cong (α.η Y) eq , Π.cong (β.η Y) eq
            }
          ; commute = λ f eq → α.commute f eq , β.commute f eq
          }
        ; project₁ = λ {F α β x} eq →
          let module F = Functor F
              module α = NaturalTransformation α
              module β = NaturalTransformation β
          in Π.cong (α.η x) eq
        ; project₂ = λ {F α β x} eq →
          let module F = Functor F
              module α = NaturalTransformation α
              module β = NaturalTransformation β
          in Π.cong (β.η x) eq
        ; unique   = λ {F α β δ} eq₁ eq₂ {x} eq →
          let module F = Functor F
              module α = NaturalTransformation α
              module β = NaturalTransformation β
              module δ = NaturalTransformation δ
          in Setoid.sym (A.₀ x) (eq₁ (Setoid.sym (F.₀ x) eq))
           , Setoid.sym (B.₀ x) (eq₂ (Setoid.sym (F.₀ x) eq))
        }
      }
    }

  module Presheaves-Cartesian = Cartesian Presheaves-Cartesian

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Definitions of algebraic structures like monoids and rings
-- (packed in records together with sets, operations, etc.)
------------------------------------------------------------------------

-- The contents of this module should be accessed via `Algebra`.

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

module Algebra.Bundles where

open import Algebra.Core
open import Algebra.Structures
open import Relation.Binary
open import Function.Base
open import Level

------------------------------------------------------------------------
-- Bundles with 1 binary operation
------------------------------------------------------------------------

record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier

record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    isMagma : IsMagma _≈_ _∙_

  open IsMagma isMagma public

  rawMagma : RawMagma _ _
  rawMagma = record { _≈_ = _≈_; _∙_ = _∙_ }

record Semigroup c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier     : Set c
    _≈_         : Rel Carrier ℓ
    _∙_         : Op₂ Carrier
    isSemigroup : IsSemigroup _≈_ _∙_

  open IsSemigroup isSemigroup public

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

  open Magma magma public using (rawMagma)

record Band c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    isBand  : IsBand _≈_ _∙_

  open IsBand isBand public

  semigroup : Semigroup c ℓ
  semigroup = record { isSemigroup = isSemigroup }

  open Semigroup semigroup public using (magma; rawMagma)

record CommutativeSemigroup c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier                 : Set c
    _≈_                     : Rel Carrier ℓ
    _∙_                     : Op₂ Carrier
    isCommutativeSemigroup  : IsCommutativeSemigroup _≈_ _∙_

  open IsCommutativeSemigroup isCommutativeSemigroup public

  semigroup : Semigroup c ℓ
  semigroup = record { isSemigroup = isSemigroup }

  open Semigroup semigroup public using (magma; rawMagma)

record Semilattice c ℓ : Set (suc (c ⊔ ℓ)) where
  infixr 7 _∧_
  infix  4 _≈_
  field
    Carrier       : Set c
    _≈_           : Rel Carrier ℓ
    _∧_           : Op₂ Carrier
    isSemilattice : IsSemilattice _≈_ _∧_

  open IsSemilattice isSemilattice public

  band : Band c ℓ
  band = record { isBand = isBand }

  open Band band public using (rawMagma; magma; semigroup)

record SelectiveMagma c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier          : Set c
    _≈_              : Rel Carrier ℓ
    _∙_              : Op₂ Carrier
    isSelectiveMagma : IsSelectiveMagma _≈_ _∙_

  open IsSelectiveMagma isSelectiveMagma public

  magma : Magma c ℓ
  magma = record { isMagma = isMagma }

  open Magma magma public using (rawMagma)

------------------------------------------------------------------------
-- Bundles with 1 binary operation & 1 element
------------------------------------------------------------------------

-- A raw monoid is a monoid without any laws.

record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    ε       : Carrier

  rawMagma : RawMagma c ℓ
  rawMagma = record
    { _≈_ = _≈_
    ; _∙_ = _∙_
    }

record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier  : Set c
    _≈_      : Rel Carrier ℓ
    _∙_      : Op₂ Carrier
    ε        : Carrier
    isMonoid : IsMonoid _≈_ _∙_ ε

  open IsMonoid isMonoid public

  semigroup : Semigroup _ _
  semigroup = record { isSemigroup = isSemigroup }

  rawMonoid : RawMonoid _ _
  rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε}

  open Semigroup semigroup public using (rawMagma; magma)

record CommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier             : Set c
    _≈_                 : Rel Carrier ℓ
    _∙_                 : Op₂ Carrier
    ε                   : Carrier
    isCommutativeMonoid : IsCommutativeMonoid _≈_ _∙_ ε

  open IsCommutativeMonoid isCommutativeMonoid public

  monoid : Monoid _ _
  monoid = record { isMonoid = isMonoid }

  commutativeSemigroup : CommutativeSemigroup _ _
  commutativeSemigroup = record { isCommutativeSemigroup = isCommutativeSemigroup }

  open Monoid monoid public using (rawMagma; magma; semigroup; rawMonoid)

record IdempotentCommutativeMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier                       : Set c
    _≈_                           : Rel Carrier ℓ
    _∙_                           : Op₂ Carrier
    ε                             : Carrier
    isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _≈_ _∙_ ε

  open IsIdempotentCommutativeMonoid isIdempotentCommutativeMonoid public

  commutativeMonoid : CommutativeMonoid _ _
  commutativeMonoid = record { isCommutativeMonoid = isCommutativeMonoid }

  open CommutativeMonoid commutativeMonoid public
    using (rawMagma; magma; semigroup; rawMonoid; monoid)

-- Idempotent commutative monoids are also known as bounded lattices.
-- Note that the BoundedLattice necessarily uses the notation inherited
-- from monoids rather than lattices.

BoundedLattice = IdempotentCommutativeMonoid

module BoundedLattice {c ℓ} (idemCommMonoid : IdempotentCommutativeMonoid c ℓ) =
       IdempotentCommutativeMonoid idemCommMonoid

------------------------------------------------------------------------
-- Bundles with 1 binary operation, 1 unary operation & 1 element
------------------------------------------------------------------------

record RawGroup c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 _⁻¹
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    ε       : Carrier
    _⁻¹     : Op₁ Carrier

  rawMonoid : RawMonoid c ℓ
  rawMonoid = record
    { _≈_ = _≈_
    ; _∙_ = _∙_
    ; ε   = ε
    }

  open RawMonoid rawMonoid public
    using (rawMagma)

record Group c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 _⁻¹
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    ε       : Carrier
    _⁻¹     : Op₁ Carrier
    isGroup : IsGroup _≈_ _∙_ ε _⁻¹

  open IsGroup isGroup public

  rawGroup : RawGroup _ _
  rawGroup = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹}

  monoid : Monoid _ _
  monoid = record { isMonoid = isMonoid }

  open Monoid monoid public using (rawMagma; magma; semigroup; rawMonoid)

record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 _⁻¹
  infixl 7 _∙_
  infix  4 _≈_
  field
    Carrier        : Set c
    _≈_            : Rel Carrier ℓ
    _∙_            : Op₂ Carrier
    ε              : Carrier
    _⁻¹            : Op₁ Carrier
    isAbelianGroup : IsAbelianGroup _≈_ _∙_ ε _⁻¹

  open IsAbelianGroup isAbelianGroup public

  group : Group _ _
  group = record { isGroup = isGroup }

  open Group group public
    using (rawMagma; magma; semigroup; monoid; rawMonoid; rawGroup)

  commutativeMonoid : CommutativeMonoid _ _
  commutativeMonoid =
    record { isCommutativeMonoid = isCommutativeMonoid }

------------------------------------------------------------------------
-- Bundles with 2 binary operations
------------------------------------------------------------------------

record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
  infixr 7 _∧_
  infixr 6 _∨_
  infix  4 _≈_
  field
    Carrier   : Set c
    _≈_       : Rel Carrier ℓ
    _∨_       : Op₂ Carrier
    _∧_       : Op₂ Carrier
    isLattice : IsLattice _≈_ _∨_ _∧_

  open IsLattice isLattice public

  setoid : Setoid _ _
  setoid = record { isEquivalence = isEquivalence }

record DistributiveLattice c ℓ : Set (suc (c ⊔ ℓ)) where
  infixr 7 _∧_
  infixr 6 _∨_
  infix  4 _≈_
  field
    Carrier               : Set c
    _≈_                   : Rel Carrier ℓ
    _∨_                   : Op₂ Carrier
    _∧_                   : Op₂ Carrier
    isDistributiveLattice : IsDistributiveLattice _≈_ _∨_ _∧_

  open IsDistributiveLattice isDistributiveLattice public

  lattice : Lattice _ _
  lattice = record { isLattice = isLattice }

  open Lattice lattice public using (setoid)

------------------------------------------------------------------------
-- Bundles with 2 binary operations & 1 element
------------------------------------------------------------------------

record NearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier        : Set c
    _≈_            : Rel Carrier ℓ
    _+_            : Op₂ Carrier
    _*_            : Op₂ Carrier
    0#             : Carrier
    isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0#

  open IsNearSemiring isNearSemiring public

  +-monoid : Monoid _ _
  +-monoid = record { isMonoid = +-isMonoid }

  open Monoid +-monoid public
    using ()
    renaming
    ( rawMagma  to +-rawMagma
    ; magma     to +-magma
    ; semigroup to +-semigroup
    ; rawMonoid to +-rawMonoid
    )

  *-semigroup : Semigroup _ _
  *-semigroup = record { isSemigroup = *-isSemigroup }

  open Semigroup *-semigroup public
    using ()
    renaming
    ( rawMagma to *-rawMagma
    ; magma    to *-magma
    )

record SemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier              : Set c
    _≈_                  : Rel Carrier ℓ
    _+_                  : Op₂ Carrier
    _*_                  : Op₂ Carrier
    0#                   : Carrier
    isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0#

  open IsSemiringWithoutOne isSemiringWithoutOne public

  nearSemiring : NearSemiring _ _
  nearSemiring = record { isNearSemiring = isNearSemiring }

  open NearSemiring nearSemiring public
    using
    ( +-rawMagma; +-magma; +-semigroup; +-rawMonoid; +-monoid
    ; *-rawMagma; *-magma; *-semigroup
    )

  +-commutativeMonoid : CommutativeMonoid _ _
  +-commutativeMonoid =
    record { isCommutativeMonoid = +-isCommutativeMonoid }

record CommutativeSemiringWithoutOne c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier                         : Set c
    _≈_                             : Rel Carrier ℓ
    _+_                             : Op₂ Carrier
    _*_                             : Op₂ Carrier
    0#                              : Carrier
    isCommutativeSemiringWithoutOne :
      IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0#

  open IsCommutativeSemiringWithoutOne
         isCommutativeSemiringWithoutOne public

  semiringWithoutOne : SemiringWithoutOne _ _
  semiringWithoutOne =
    record { isSemiringWithoutOne = isSemiringWithoutOne }

  open SemiringWithoutOne semiringWithoutOne public
    using
    ( +-rawMagma; +-magma; +-semigroup
    ; *-rawMagma; *-magma; *-semigroup
    ; +-rawMonoid; +-monoid; +-commutativeMonoid
    ; nearSemiring
    )

------------------------------------------------------------------------
-- Bundles with 2 binary operations & 2 elements
------------------------------------------------------------------------

record RawSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier    : Set c
    _≈_        : Rel Carrier ℓ
    _+_        : Op₂ Carrier
    _*_        : Op₂ Carrier
    0#         : Carrier
    1#         : Carrier

record SemiringWithoutAnnihilatingZero c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier                           : Set c
    _≈_                               : Rel Carrier ℓ
    _+_                               : Op₂ Carrier
    _*_                               : Op₂ Carrier
    0#                                : Carrier
    1#                                : Carrier
    isSemiringWithoutAnnihilatingZero :
      IsSemiringWithoutAnnihilatingZero _≈_ _+_ _*_ 0# 1#

  open IsSemiringWithoutAnnihilatingZero
         isSemiringWithoutAnnihilatingZero public

  +-commutativeMonoid : CommutativeMonoid _ _
  +-commutativeMonoid =
    record { isCommutativeMonoid = +-isCommutativeMonoid }

  open CommutativeMonoid +-commutativeMonoid public
    using ()
    renaming
    ( rawMagma  to +-rawMagma
    ; magma     to +-magma
    ; semigroup to +-semigroup
    ; rawMonoid to +-rawMonoid
    ; monoid    to +-monoid
    )

  *-monoid : Monoid _ _
  *-monoid = record { isMonoid = *-isMonoid }

  open Monoid *-monoid public
    using ()
    renaming
    ( rawMagma  to *-rawMagma
    ; magma     to *-magma
    ; semigroup to *-semigroup
    ; rawMonoid to *-rawMonoid
    )

record Semiring c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier    : Set c
    _≈_        : Rel Carrier ℓ
    _+_        : Op₂ Carrier
    _*_        : Op₂ Carrier
    0#         : Carrier
    1#         : Carrier
    isSemiring : IsSemiring _≈_ _+_ _*_ 0# 1#

  open IsSemiring isSemiring public

  rawSemiring : RawSemiring _ _
  rawSemiring = record
    { _≈_ = _≈_
    ; _+_ = _+_
    ; _*_ = _*_
    ; 0#  = 0#
    ; 1#  = 1#
    }

  semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero _ _
  semiringWithoutAnnihilatingZero = record
    { isSemiringWithoutAnnihilatingZero =
        isSemiringWithoutAnnihilatingZero
    }

  open SemiringWithoutAnnihilatingZero
         semiringWithoutAnnihilatingZero public
    using
    ( +-rawMagma;  +-magma;  +-semigroup
    ; *-rawMagma;  *-magma;  *-semigroup
    ; +-rawMonoid; +-monoid; +-commutativeMonoid
    ; *-rawMonoid; *-monoid
    )

  semiringWithoutOne : SemiringWithoutOne _ _
  semiringWithoutOne =
    record { isSemiringWithoutOne = isSemiringWithoutOne }

  open SemiringWithoutOne semiringWithoutOne public
    using (nearSemiring)

record CommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier               : Set c
    _≈_                   : Rel Carrier ℓ
    _+_                   : Op₂ Carrier
    _*_                   : Op₂ Carrier
    0#                    : Carrier
    1#                    : Carrier
    isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#

  open IsCommutativeSemiring isCommutativeSemiring public

  semiring : Semiring _ _
  semiring = record { isSemiring = isSemiring }

  open Semiring semiring public
    using
    ( +-rawMagma; +-magma; +-semigroup
    ; *-rawMagma; *-magma; *-semigroup
    ; +-rawMonoid; +-monoid; +-commutativeMonoid
    ; *-rawMonoid; *-monoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero
    ; rawSemiring
    )

  *-commutativeSemigroup : CommutativeSemigroup _ _
  *-commutativeSemigroup = record
    { isCommutativeSemigroup = *-isCommutativeSemigroup
    }

  *-commutativeMonoid : CommutativeMonoid _ _
  *-commutativeMonoid = record
    { isCommutativeMonoid = *-isCommutativeMonoid
    }

  commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne _ _
  commutativeSemiringWithoutOne = record
    { isCommutativeSemiringWithoutOne = isCommutativeSemiringWithoutOne
    }

------------------------------------------------------------------------
-- Bundles with 2 binary operations, 1 unary operation & 2 elements
------------------------------------------------------------------------

-- A raw ring is a ring without any laws.

record RawRing c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier

  +-rawGroup : RawGroup c ℓ
  +-rawGroup = record
    { _≈_ = _≈_
    ; _∙_ = _+_
    ; ε   = 0#
    ; _⁻¹ = -_
    }

  *-rawMonoid : RawMonoid c ℓ
  *-rawMonoid = record
    { _≈_     = _≈_
    ; _∙_     = _*_
    ; ε       = 1#
    }

record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _+_     : Op₂ Carrier
    _*_     : Op₂ Carrier
    -_      : Op₁ Carrier
    0#      : Carrier
    1#      : Carrier
    isRing  : IsRing _≈_ _+_ _*_ -_ 0# 1#

  open IsRing isRing public

  +-abelianGroup : AbelianGroup _ _
  +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup }

  semiring : Semiring _ _
  semiring = record { isSemiring = isSemiring }

  open Semiring semiring public
    using
    ( +-rawMagma; +-magma; +-semigroup
    ; *-rawMagma; *-magma; *-semigroup
    ; +-rawMonoid; +-monoid ; +-commutativeMonoid
    ; *-rawMonoid; *-monoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero
    )

  open AbelianGroup +-abelianGroup public
    using () renaming (group to +-group)

  rawRing : RawRing _ _
  rawRing = record
    { _≈_ = _≈_
    ; _+_ = _+_
    ; _*_ = _*_
    ; -_  = -_
    ; 0#  = 0#
    ; 1#  = 1#
    }

record CommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier           : Set c
    _≈_               : Rel Carrier ℓ
    _+_               : Op₂ Carrier
    _*_               : Op₂ Carrier
    -_                : Op₁ Carrier
    0#                : Carrier
    1#                : Carrier
    isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1#

  open IsCommutativeRing isCommutativeRing public

  ring : Ring _ _
  ring = record { isRing = isRing }

  commutativeSemiring : CommutativeSemiring _ _
  commutativeSemiring =
    record { isCommutativeSemiring = isCommutativeSemiring }

  open Ring ring public using (rawRing; +-group; +-abelianGroup)
  open CommutativeSemiring commutativeSemiring public
    using
    ( +-rawMagma; +-magma; +-semigroup
    ; *-rawMagma; *-magma; *-semigroup
    ; +-rawMonoid; +-monoid; +-commutativeMonoid
    ; *-rawMonoid; *-monoid; *-commutativeMonoid
    ; nearSemiring; semiringWithoutOne
    ; semiringWithoutAnnihilatingZero; semiring
    ; commutativeSemiringWithoutOne
    )

record BooleanAlgebra c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 ¬_
  infixr 7 _∧_
  infixr 6 _∨_
  infix  4 _≈_
  field
    Carrier          : Set c
    _≈_              : Rel Carrier ℓ
    _∨_              : Op₂ Carrier
    _∧_              : Op₂ Carrier
    ¬_               : Op₁ Carrier
    ⊤                : Carrier
    ⊥                : Carrier
    isBooleanAlgebra : IsBooleanAlgebra _≈_ _∨_ _∧_ ¬_ ⊤ ⊥

  open IsBooleanAlgebra isBooleanAlgebra public

  distributiveLattice : DistributiveLattice _ _
  distributiveLattice = record { isDistributiveLattice = isDistributiveLattice }

  open DistributiveLattice distributiveLattice public
    using (setoid; lattice)

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.0

RawSemigroup = RawMagma
{-# WARNING_ON_USAGE RawSemigroup
"Warning: RawSemigroup was deprecated in v1.0.
Please use RawMagma instead."
#-}


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

open import LogicalFormulae
open import Groups.Abelian.Definition
open import Groups.Homomorphisms.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Rings.Definition
open import Lists.Lists
open import Rings.Homomorphisms.Definition

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

open Ring R
open Setoid S
open Equivalence eq
open import Groups.Polynomials.Group additiveGroup
open import Groups.Polynomials.Definition additiveGroup
open import Rings.Polynomial.Multiplication R

polyRing : Ring naivePolySetoid _+P_ _*P_
Ring.additiveGroup polyRing = polyGroup
Ring.*WellDefined polyRing {a} {b} {c} {d} = *PwellDefined {a} {b} {c} {d}
Ring.1R polyRing = 1R :: []
Ring.groupIsAbelian polyRing {x} {y} = AbelianGroup.commutative (abelian (record { commutative = Ring.groupIsAbelian R })) {x} {y}
Ring.*Associative polyRing {a} {b} {c} = *Passoc {a} {b} {c}
Ring.*Commutative polyRing {a} {b} = p*Commutative {a} {b}
Ring.*DistributesOver+ polyRing {a} {b} {c} = *Pdistrib {a} {b} {c}
Ring.identIsIdent polyRing {a} = *Pident {a}

polyInjectionIsHom : RingHom R polyRing polyInjection
RingHom.preserves1 polyInjectionIsHom = reflexive ,, record {}
RingHom.ringHom polyInjectionIsHom = reflexive ,, (reflexive ,, record {})
GroupHom.groupHom (RingHom.groupHom polyInjectionIsHom) = reflexive ,, record {}
GroupHom.wellDefined (RingHom.groupHom polyInjectionIsHom) = SetoidInjection.wellDefined polyInjectionIsInj


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

module Cubical.HITs.FreeGroupoid where

open import Cubical.HITs.FreeGroupoid.Base public
open import Cubical.HITs.FreeGroupoid.GroupoidActions public
open import Cubical.HITs.FreeGroupoid.Properties public

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --cubical #-}
module _ where
open import Agda.Primitive.Cubical renaming (primINeg to ~_; primIMax to _∨_; primIMin to _∧_)
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Sub
open import Agda.Builtin.Cubical.Sub using () renaming (Sub to _[_↦_]; primSubOut to ouc)
open import Agda.Primitive renaming (_⊔_ to ℓ-max)
open import Agda.Builtin.Sigma

transpFill : ∀ {ℓ} {A' : Set ℓ} (φ : I)
               (A : (i : I) → Set ℓ [ φ ↦ (\ _ → A') ]) →
               (u0 : ouc (A i0)) →
               PathP (λ i → ouc (A i)) u0 (primTransp (λ i → ouc (A i)) φ u0)
transpFill φ A u0 i = primTransp (\ j → ouc (A (i ∧ j))) (~ i ∨ φ) u0

-- private
--   internalFiber : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} (f : A → B) (y : B) → Set (ℓ-max ℓ ℓ')
--   internalFiber {A = A} f y = Σ A \ x → y ≡ f x

-- infix 4 _≃_

-- postulate
--   _≃_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ-max ℓ ℓ')
--   equivFun : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'} → A ≃ B → A → B
--   equivProof : ∀ {la lt} (T : Set la) (A : Set lt) → (w : T ≃ A) → (a : A)
--                → ∀ ψ → (Partial ψ (internalFiber (equivFun w) a)) → internalFiber (equivFun w) a

-- {-# BUILTIN EQUIV _≃_ #-}
-- {-# BUILTIN EQUIVFUN  equivFun #-}
-- {-# BUILTIN EQUIVPROOF equivProof #-}

-- -- This is a module so we can easily rename the primitives.
-- module GluePrims where
--   primitive
--     primGlue    : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
--       → (T : Partial φ (Set ℓ')) → (e : PartialP φ (λ o → T o ≃ A))
--       → Set ℓ'
--     prim^glue   : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
--       → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
--       → PartialP φ T → A → primGlue A T e
--     prim^unglue : ∀ {ℓ ℓ'} {A : Set ℓ} {φ : I}
--       → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
--       → primGlue A T e → A

--     -- Needed for transp in Glue.
--     primFaceForall : (I → I) → I

open import Agda.Builtin.Cubical.Glue public
  renaming ( prim^glue to glue
           ; prim^unglue to unglue)

-- We uncurry Glue to make it a bit more pleasant to use
Glue : ∀ {ℓ ℓ'} (A : Set ℓ) {φ : I}
       → (Te : Partial φ (Σ (Set ℓ') \ T →  T ≃ A))
       → Set ℓ'
Glue A Te = primGlue A (λ x → Te x .fst) (λ x → Te x .snd)

module TestHComp {ℓ ℓ'} (A : Set ℓ) {φ : I} (Te : Partial φ (Σ (Set ℓ') \ T →  T ≃ A))
         (ψ : I) (u : I → Partial ψ (Glue A Te)) (u0 : Sub (Glue A Te) ψ (u i0) ) where
  result : Glue A Te
  result = glue {φ = φ} (\ { (φ = i1) → primHComp {A = Te itIsOne .fst} u (primSubOut u0) })
                        (primHComp {A = A} (\ i → \ { (ψ = i1) → unglue {φ = φ} (u i itIsOne)
                                                    ; (φ = i1) → equivFun (Te itIsOne .snd)
                                                                          (primHComp (\ j → \ { (ψ = i1) → u (i ∧ j) itIsOne
                                                                                ; (i = i0) → primSubOut u0 })
                                                                                (primSubOut u0)) })
                                           (unglue {φ = φ} (primSubOut u0)))

  test : primHComp {A = Glue A Te} {ψ} u (primSubOut u0) ≡ result
  test i = primHComp {A = Glue A Te} {ψ} u (primSubOut u0)

module TestTransp {ℓ ℓ'} (A : Set ℓ) {φ : I} (Te : Partial φ (Σ (Set ℓ') \ T →  T ≃ A))
         (u0 : (Glue A Te)) where
  ψ = i0

  a0 = unglue {φ = φ} u0
  a1 = primComp (\ _ → A)
         φ
         (\ { i (φ = i1) → equivFun (Te itIsOne .snd) (transpFill {A' = Te itIsOne .fst} ψ (\ i → inc (Te itIsOne .fst)) u0 i) })
         a0

  pair : PartialP φ λ o → Helpers.fiber (Te o .snd .fst) a1
  pair o = equivProof (Te o .fst) A (Te o .snd) a1 φ \ { (φ = i1) → _ , Helpers.refl }

  result : Glue A Te
  result = glue {φ = φ} (λ o → pair o .fst) (primHComp (\ { j (φ = i1) → pair itIsOne .snd j}) a1)

  test : primTransp (\ _ → Glue A Te) ψ u0 ≡ result
  test = Helpers.refl

max_stars_repo_name: caryoscelus/agda

max_issues_repo_name: caryoscelus/agda

max_forks_repo_name: caryoscelus/agda


text:
module #2 where

open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality

{-
Exercise 1.2. Derive the recursion principle for products recA×B using only the projections, and
verify that the definitional equalities are valid. Do the same for Σ-types.
-}

module Products { a b c }{A : Set a}{B : Set b}{C : Set c}(g : A → B → C) where

  recₓ :  A × B → C
  recₓ x = g (proj₁ x) (proj₂ x)

  rec-β : (x : A)(y : B) → recₓ (x , y) ≡ g x y
  rec-β x y = refl

module Sums { a b c }{A : Set a}{B : A → Set b}{C : Set c}(g : (x : A) → B x → C) where

  rec-Σ : Σ A B → C
  rec-Σ x = g (proj₁ x) (proj₂ x)

  rec-Σ-β : (x : A)(y : B x) → rec-Σ (x , y) ≡ g x y
  rec-Σ-β x y = refl

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
module kiss where

open import string
open import list
open import bool
open import relations
open import product
open import unit

data formula : Set where
  $ : string → formula
  True : formula
  Implies : formula → formula → formula
  And : formula → formula → formula

ctxt : Set
ctxt = 𝕃 formula

data _⊢_ : ctxt → formula → Set where
  Assume : ∀{Γ f} → (f :: Γ) ⊢ f
  Weaken : ∀{Γ f f'} → Γ ⊢ f → (f' :: Γ) ⊢ f
  ImpliesI : ∀{Γ f1 f2} → (f1 :: Γ) ⊢ f2 → Γ ⊢ (Implies f1 f2)
  ImpliesE : ∀{Γ f1 f2} → Γ ⊢ (Implies f1 f2) → Γ ⊢ f1 → Γ ⊢ f2
  TrueI : ∀{Γ} → Γ ⊢ True
  AndI : ∀{Γ f1 f2} → Γ ⊢ f1 → Γ ⊢ f2 → Γ ⊢ (And f1 f2)
  AndE : ∀(b : 𝔹){Γ f1 f2} → Γ ⊢ (And f1 f2) → Γ ⊢ (if b then f1 else f2)
{-
p : formula
p = $ "p"

f1 : (p :: []) ⊢ p
f1 = assume {[]}{p}

f2 : (p :: []) ⊢ (And p p)
f2 = AndI f1 f1

f3 : [] ⊢ (Implies p (And p p))
f3 = ImpliesI f2
-}
record struct : Set1 where
  field W         : Set
        R         : W → W → Set
        preorderR : preorder R
        V         : W → string → Set
        monoV     : ∀{w w'} → R w w' → ∀{i} →
                    V w i → V w' i
  reflR : reflexive R
  reflR = fst preorderR
  transR : transitive R
  transR = snd preorderR

data world : Set where
  w0 : world
  w1 : world
  w2 : world

data rel : world → world → Set where
  r00 : rel w0 w0
  r11 : rel w1 w1
  r22 : rel w2 w2
  r01 : rel w0 w1
  r02 : rel w0 w2

rel-refl : reflexive rel
rel-refl {w0} = r00
rel-refl {w1} = r11
rel-refl {w2} = r22

rel-trans : transitive rel
rel-trans r00 r00 = r00
rel-trans r00 r01 = r01
rel-trans r00 r02 = r02
rel-trans r11 r11 = r11
rel-trans r22 r22 = r22
rel-trans r01 r11 = r01
rel-trans r02 r22 = r02

data val : world → string → Set where
  v1p : val w1 "p"
  v1q : val w1 "q"
  v2p : val w2 "p"
  v2q : val w2 "q"

mono-val : ∀{w w'} → rel w w' →
           ∀{i} → val w i → val w' i
mono-val r00 p = p
mono-val r11 p = p
mono-val r22 p = p
mono-val r01 ()
mono-val r02 ()

k : struct
k = record { W         = world ;
             R         = rel ;
             preorderR = (rel-refl , rel-trans) ;
             V         = val ;
             monoV     = mono-val }

open struct

_,_⊨_ : ∀(k : struct) → W k → formula → Set
k , w ⊨ ($ x) = V k w x
k , w ⊨ True = ⊤
k , w ⊨ Implies f1 f2 = ∀ {w' : W k} → R k w w' →
                        k , w' ⊨ f1 → k , w' ⊨ f2
k , w ⊨ And f1 f2 = k , w ⊨ f1 ∧ k , w ⊨ f2

pf-test-sem : k , w0 ⊨ Implies ($ "p") ($ "q")
pf-test-sem r00 ()
pf-test-sem r01 p = v1q
pf-test-sem r02 p = v2q

_,_⊨ctxt_ : ∀(k : struct) → W k → ctxt → Set
k , w ⊨ctxt [] = ⊤
k , w ⊨ctxt (f :: Γ) = (k , w ⊨ f) ∧ (k , w ⊨ctxt Γ)

mono⊨ : ∀{k : struct}{w1 w2 : W k}{f : formula} →
         R k w1 w2 →
         k , w1 ⊨ f →
         k , w2 ⊨ f
mono⊨{k} {f = $ x} r p = monoV k r p
mono⊨{k} {f = True} r p = triv
mono⊨{k} {f = Implies f1 f2} r p r' p' = p (transR k r r') p'
mono⊨{k} {f = And f1 f2} r (p1 , p2) = mono⊨{f = f1} r p1 , mono⊨{f = f2} r p2

mono⊨ctxt : ∀{k : struct}{Γ : ctxt}{w1 w2 : W k} →
            R k w1 w2 →
            k , w1 ⊨ctxt Γ →
            k , w2 ⊨ctxt Γ
mono⊨ctxt{k}{[]} _ _ = triv
mono⊨ctxt{k}{f :: Γ} r (u , v) = mono⊨{k}{f = f} r u , mono⊨ctxt{k}{Γ} r v

_⊩_ : ctxt → formula → Set1
Γ ⊩ f = ∀{k : struct}{w : W k} → k , w ⊨ctxt Γ → k , w ⊨ f

Soundness : ∀{Γ : ctxt}{f : formula} → Γ ⊢ f → Γ ⊩ f
Soundness Assume g = fst g
Soundness (Weaken p) g = Soundness p (snd g)
Soundness (ImpliesI p) g r u' = Soundness p (u' , mono⊨ctxt r g)
Soundness (ImpliesE p p') {k} g = (Soundness p g) (reflR k) (Soundness p' g)
Soundness TrueI g = triv
Soundness (AndI p p') g = (Soundness p g , Soundness p' g)
Soundness (AndE tt p) g = fst (Soundness p g)
Soundness (AndE ff p) g = snd (Soundness p g)

data _≼_ : 𝕃 formula → 𝕃 formula → Set where
  ≼-refl : ∀{Γ} → Γ ≼ Γ
  ≼-cons : ∀{Γ Γ' f} → Γ ≼ Γ' → Γ ≼ (f :: Γ')

≼-trans : ∀ {Γ Γ' Γ''} → Γ ≼ Γ' → Γ' ≼ Γ'' → Γ ≼ Γ''
≼-trans u ≼-refl = u
≼-trans u (≼-cons u') = ≼-cons (≼-trans u u')

Weaken≼ : ∀ {Γ Γ'}{f : formula} → Γ ≼ Γ' → Γ ⊢ f → Γ' ⊢ f
Weaken≼ ≼-refl p = p
Weaken≼ (≼-cons d) p = Weaken (Weaken≼ d p)

U : struct
U = record { W = ctxt ;
             R = _≼_ ;
             preorderR = ≼-refl , ≼-trans ;
             V = λ Γ n → Γ ⊢ $ n ;
             monoV = λ d p → Weaken≼ d p }

CompletenessU : ∀{f : formula}{Γ : W U} → U , Γ ⊨ f → Γ ⊢ f
SoundnessU : ∀{f : formula}{Γ : W U} → Γ ⊢ f → U , Γ ⊨ f
CompletenessU {$ x} u = u
CompletenessU {True} u = TrueI
CompletenessU {And f f'} u = AndI (CompletenessU{f} (fst u)) (CompletenessU{f'} (snd u))
CompletenessU {Implies f f'}{Γ} u =
  ImpliesI
    (CompletenessU {f'}
      (u (≼-cons ≼-refl) (SoundnessU {f} (Assume {Γ}))))
SoundnessU {$ x} p = p
SoundnessU {True} p = triv
SoundnessU {And f f'} p = SoundnessU{f} (AndE tt p) , SoundnessU{f'} (AndE ff p)
SoundnessU {Implies f f'} p r u = SoundnessU (ImpliesE (Weaken≼ r p) (CompletenessU {f} u))

ctxt-id : ∀{Γ : ctxt} → U , Γ ⊨ctxt Γ
ctxt-id{[]} = triv
ctxt-id{f :: Γ} = SoundnessU{f} Assume , mono⊨ctxt (≼-cons ≼-refl) (ctxt-id {Γ})

Completeness : ∀{Γ : ctxt}{f : formula} → Γ ⊩ f → Γ ⊢ f
Completeness{Γ} p = CompletenessU (p{U}{Γ} (ctxt-id{Γ}))

Universality1 : ∀{Γ : ctxt}{f : formula} → Γ ⊩ f → U , Γ ⊨ f
Universality1{Γ}{f} p = SoundnessU (Completeness{Γ}{f} p)

Universality2 : ∀{Γ : ctxt}{f : formula} → U , Γ ⊨ f → Γ ⊩ f
Universality2{Γ}{f} p = Soundness (CompletenessU{f}{Γ} p)

nbe : ∀ {Γ f} → Γ ⊢ f → Γ ⊢ f
nbe {Γ} p = Completeness (Soundness p)

max_stars_repo_name: logicshan/IAL

max_issues_repo_name: logicshan/IAL

max_forks_repo_name: logicshan/IAL


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

module Main where

open import Data.List

open import Midi
open import Note

open import Frog
open import Piston

main : IO Unit
main =
  let channel      = 0
      ticksPerBeat = 4 -- 16th notes
      file         = "/tmp/test.mid"
-- counterpoint
      song         = cfcpTracks1
--      song         = cfcpTracks2
-- harmony
--      song         = testHTracks
  in exportTracks file ticksPerBeat (map track→htrack song)

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
module x1-Base where

data List (X : Set) : Set where
  []  :              List X
  _∷_ : X → List X → List X
infixr 5 _∷_

foldr : ∀ {A} {B : Set} → (A → B → B) → B → List A → B
foldr f b      []  = b
foldr f b (a ∷ as) = f a (foldr f b as)

data Either (A : Set) (B : Set) : Set where
  left  : A → Either A B
  right : B → Either A B

[_,_] : ∀ {A B} {C : Set} → (A → C) → (B → C) → Either A B → C
[ f , g ] (left  x) = f x
[ f , g ] (right x) = g x

-- Unhabited type
data Empty : Set where

absurd : {X : Set} → Empty → X
absurd ()

-- use Empty to define something close to negation in logic:
-- e.g., terms of type ¬ (3 > 4)
infix 3 ¬_
¬_ : Set → Set
¬ X = X → Empty

-- binary relation on a type X
Rel : Set → Set₁
Rel X = X → X → Set

-- decidable relations
Decidable : ∀ {X} → Rel X → Set
Decidable R = ∀ x y → Either (R x y) (¬ (R x y))

-- To sort a list, need two relations on elements of list:

-- equality
record Equivalence {X} (_≈_ : Rel X) : Set₁ where
  field
    refl  : ∀ {x}     → x ≈ x
    sym   : ∀ {x y}   → x ≈ y → y ≈ x
    trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z

-- and ordering
record TotalOrder {X} (_≈_ : Rel X) (_≤_ : Rel X) : Set₁ where
  field
    antisym     : ∀ {x y}   → x ≤ y → y ≤ x → x ≈ y
    trans       : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
    total       : ∀  x y    → Either (x ≤ y) (y ≤ x)
    reflexive   : ∀ {x y}   → x ≈ y → x ≤ y
    equivalence : Equivalence _≈_

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
import      Lvl
open import Structure.Operator.Vector
open import Structure.Setoid
open import Type

module Structure.Operator.Vector.Subspaces.Span
  {ℓᵥ ℓₛ ℓᵥₑ ℓₛₑ}
  {V : Type{ℓᵥ}} ⦃ equiv-V : Equiv{ℓᵥₑ}(V) ⦄
  {S : Type{ℓₛ}} ⦃ equiv-S : Equiv{ℓₛₑ}(S) ⦄
  {_+ᵥ_ : V → V → V}
  {_⋅ₛᵥ_ : S → V → V}
  {_+ₛ_ _⋅ₛ_ : S → S → S}
  ⦃ vectorSpace : VectorSpace(_+ᵥ_)(_⋅ₛᵥ_)(_+ₛ_)(_⋅ₛ_) ⦄
  where

open VectorSpace(vectorSpace)

open import Logic.Predicate
open import Numeral.CoordinateVector as Vec using () renaming (Vector to Vec)
open import Numeral.Finite
open import Numeral.Natural
open import Sets.ExtensionalPredicateSet as PredSet using (PredSet ; _∈_ ; [∋]-binaryRelator)
open import Structure.Container.SetLike using (SetElement)
private open module SetLikeFunctionProperties{ℓ} = Structure.Container.SetLike.FunctionProperties{C = PredSet{ℓ}(V)}{E = V}(_∈_)
open import Structure.Function.Multi
open import Structure.Operator
open import Structure.Operator.Vector.LinearCombination        ⦃ vectorSpace = vectorSpace ⦄
open import Structure.Operator.Vector.LinearCombination.Proofs
open import Structure.Operator.Vector.Subspace                 ⦃ vectorSpace = vectorSpace ⦄
open import Structure.Relator.Properties
open import Syntax.Function
open import Syntax.Transitivity

private variable n : ℕ
private variable vf : Vec(n)(V)
private variable sf : Vec(n)(S)

Span : Vec(n)(V) → PredSet(V)
Span(vf) = PredSet.⊶(linearCombination(vf))

Span-subspace : ∀{vf} → Subspace(Span{n}(vf))
∃.witness (_closed-under₂_.proof (Subspace.add-closure (Span-subspace {vf = vf})) ([∃]-intro sf₁) ([∃]-intro sf₂)) = Vec.map₂(_+ₛ_) sf₁ sf₂
∃.proof (_closed-under₂_.proof (Subspace.add-closure (Span-subspace {vf = vf})) {v₁} {v₂} ([∃]-intro sf₁ ⦃ p₁ ⦄) ([∃]-intro sf₂ ⦃ p₂ ⦄)) =
  linearCombination vf (Vec.map₂(_+ₛ_) sf₁ sf₂)            🝖[ _≡_ ]-[ preserving₂(linearCombination vf) (Vec.map₂(_+ₛ_)) (_+ᵥ_) ]
  (linearCombination vf sf₁) +ᵥ (linearCombination vf sf₂) 🝖[ _≡_ ]-[ congruence₂(_+ᵥ_) ⦃ [+ᵥ]-binary-operator ⦄ p₁ p₂ ]
  v₁ +ᵥ v₂                                                 🝖-end
∃.witness (_closed-under₁_.proof (Subspace.mul-closure Span-subspace {s}) ([∃]-intro sf)) = Vec.map(s ⋅ₛ_) sf
∃.proof (_closed-under₁_.proof (Subspace.mul-closure (Span-subspace {vf = vf}) {s}) {v} ([∃]-intro sf ⦃ p ⦄)) =
  linearCombination vf (i ↦ s ⋅ₛ sf(i)) 🝖[ _≡_ ]-[ preserving₁(linearCombination vf) (Vec.map(s ⋅ₛ_)) (s ⋅ₛᵥ_) ]
  s ⋅ₛᵥ (linearCombination vf sf)       🝖[ _≡_ ]-[ congruence₂ᵣ(_⋅ₛᵥ_)(s) p ]
  s ⋅ₛᵥ v                               🝖-end


text:
module Examples.Effects where

open import Prelude

open import Effects.Denotational
open import Effects.WellTyped EC _ec≟_
open import Effects.Substitutions EC _ec≟_
open import Implicits.Calculus.Types

-- value abstraction
module ex₁ where

  f : Term 0 0 0
  f = λ' unit (does io)

  -- a lazy print is pure, but has a latent effect IO
  ⊢f : [] ⊢ f ∈ unit →[ has io & pure ] unit + pure
  ⊢f = λ' unit (does io)

  -- when we apply the above term
  -- the latent effect pops up
  f·t : Term 0 0 0
  f·t = f · tt

  ⊢f·t : [] ⊢ f·t ∈ unit + has io & pure
  ⊢f·t = ⊢f · tt

-- effect abstraction
module ex₂ where
  f : Term 0 0 0
  f = H (Λ (Λ (
    λ'
      (tvar zero →[ evar zero & pure ] tvar (suc zero))
      (λ' (tvar zero) ((var (suc zero)) · (var zero)))
    )))

  wt-f : [] ⊢ f ∈
    H (∀' (∀' ((
      tvar zero →[ evar zero & pure ] tvar (suc zero)) →[ pure ]
      (tvar zero →[ evar zero & pure ] (tvar (suc zero)))
    )))
    + pure
  wt-f = H (Λ (Λ (λ' (tvar zero →[ evar zero & pure ] tvar (suc zero))
    (λ' (tvar zero) (var (suc zero) · var zero)))))

module ex₃ where
  eff : Effects 0
  eff = (has io) & (has read) & pure

  -- lists of effects transtlate to tuples of Can*
  test : ⟦ eff , ([] , []) ⟧efs ≡ C.rec (tc CanIO ∷ tc CanRead ∷ [])
  test = refl

module ex₄ where
  f : Term 0 0 0
  f = Λ (λ' unit (does io))

  wt-f : [] ⊢ f ∈ (∀' (unit →[ has io & pure ] unit)) + pure
  wt-f = Λ (λ' unit (does io))

  test : ⟦ wt-f , ([] , []) ⟧ ≡
    C.Λ (C.λ' (tc unit) ((C.ρ (tc CanIO) ((C.ρ (tc CanIO) (C.new unit)) C.⟨⟩))))
  test = refl

module ex₅ where
  open ex₄

  tapp : Term 0 0 0
  tapp = f [ unit ]

  wt-tapp : [] ⊢ tapp ∈ (unit →[ has io & pure ] unit) + pure
  wt-tapp = wt-f [ unit ]

  app : Term 0 0 0
  app = tapp · tt

  wt-app : [] ⊢ app ∈ unit + has io & pure
  wt-app = wt-tapp · tt


text:
{-# OPTIONS --allow-unsolved-metas #-}
open import Agda.Builtin.Size

mutual

  data Nat (i : Size) : Set where
    zero : Nat i
    suc  : Nat′ i → Nat i

  data Nat′ (i : Size) : Set where
    [_] : {j : Size< i} → Nat j → Nat′ i

size : ∀ {i} → Nat′ i → Size
size ([_] {j} _) = {!j!}

unbox : ∀ {i} (n : Nat′ i) → Nat (size n)
unbox [ n ] = n

postulate
  _ _ _ _ _ _ : Set


text:
{-# OPTIONS --universe-polymorphism #-}

module InstanceArguments.09-higherOrderClasses where

open import Effect.Applicative
open import Effect.Monad
open import Effect.Monad.Indexed
open import Function

lift : ∀ {a b c} {A : Set a} {C : Set c} {B : A → Set b} →
       ({{x : A}} → B x) → (f : C → A) → {{x : C}} → B (f x)
lift m f {{x}} = m {{f x}}

monadToApplicative : ∀ {l} {M : Set l → Set l} → RawMonad M → RawApplicative M
monadToApplicative = RawIMonad.rawIApplicative

liftAToM : ∀ {l} {V : Set l} {M : Set l → Set l} → ({{appM : RawApplicative M}} → M V) →
           {{monadM : RawMonad M}} → M V
liftAToM app {{x}} = lift (λ {{appM}} → app {{appM}}) monadToApplicative {{x}}


text:
module Data.Dyck.Sized where

open import Prelude
open import Data.Nat using (_+_)
open import Data.Vec.Iterated using (Vec; _∷_; []; foldlN; head; foldl′)

open import Cubical.Foundations.Prelude using (substRefl)
open import Cubical.Data.Sigma.Properties using (Σ≡Prop)
open import Data.Nat.Properties using (isSetℕ)

private variable
    n m k : ℕ
    n⊙ m⊙ k⊙ : ℕ → ℕ

--------------------------------------------------------------------------------
-- Tree
--------------------------------------------------------------------------------

data Tree : Type where
  ⟨⟩ : Tree
  _*_ : Tree → Tree → Tree

size⊙ : Tree → ℕ → ℕ
size⊙ ⟨⟩ = suc
size⊙ (xs * ys) = size⊙ xs ∘ size⊙ ys

size : Tree → ℕ
size t = size⊙ t zero

--------------------------------------------------------------------------------
-- Dyck Word
--------------------------------------------------------------------------------

infixr 6 ⟨_ ⟩_
data Dyck : ℕ → ℕ → Type where
  ⟩! : Dyck 1 0
  ⟨_ : Dyck (1 + n) m → Dyck n (1 + m)
  ⟩_ : Dyck (1 + n) m → Dyck (2 + n) m

--------------------------------------------------------------------------------
-- Tree to Stack
--------------------------------------------------------------------------------

tree→stack⊙ : (t : Tree) → Dyck (suc m) k → Dyck m (size⊙ t k)
tree→stack⊙ ⟨⟩         = ⟨_
tree→stack⊙ (xs * ys) = tree→stack⊙ xs ∘ tree→stack⊙ ys ∘ ⟩_

tree→stack : (t : Tree) → Dyck 0 (size t)
tree→stack tr = tree→stack⊙ tr ⟩!

--------------------------------------------------------------------------------
-- Stack to Tree
--------------------------------------------------------------------------------

stack→tree⊙ : Dyck n m → Vec Tree n → Tree
stack→tree⊙ ⟩!     (v ∷ [])       = v
stack→tree⊙ (⟨ is) st             = stack→tree⊙ is (⟨⟩ ∷ st)
stack→tree⊙ (⟩ is) (t₁ ∷ t₂ ∷ st) = stack→tree⊙ is (t₂ * t₁ ∷ st)

stack→tree : Dyck 0 n → Tree
stack→tree ds = stack→tree⊙ ds []

--------------------------------------------------------------------------------
-- Size lemma
--------------------------------------------------------------------------------

stack→tree-size⊙ :  {st : Vec Tree n} (is : Dyck n m) →
 size (stack→tree⊙ is st) ≡ foldl′ size⊙ m st
stack→tree-size⊙ ⟩!     = refl
stack→tree-size⊙ (⟨ is) = stack→tree-size⊙ is
stack→tree-size⊙ (⟩ is) = stack→tree-size⊙ is

--------------------------------------------------------------------------------
-- Roundtrip
--------------------------------------------------------------------------------

tree→stack→tree⊙ :  {is : Dyck (1 + n) m} {st : Vec Tree n} (e : Tree) →
  stack→tree⊙ (tree→stack⊙ e is) st ≡ stack→tree⊙ is (e ∷ st)
tree→stack→tree⊙ ⟨⟩         = refl
tree→stack→tree⊙ (xs * ys) = tree→stack→tree⊙ xs ; tree→stack→tree⊙ ys

foldlNN : ∀ {A : Type a} {p} (P : ℕ → ℕ → Type p) →
          (f : A → ℕ → ℕ) →
          (∀ {n m} → (x : A) → P (suc n) m → P n (f x m)) →
          P n m →
          (xs : Vec A n) → P zero (foldl′ f m xs)
foldlNN {n = zero} P f s b xs = b
foldlNN {n = suc n} P f s b (x ∷ xs) = foldlNN P f s (s x b) xs

stack→tree→stack⊙ :  {st : Vec Tree n} (is : Dyck n m) →
 subst (Dyck 0) (stack→tree-size⊙ is) (tree→stack (stack→tree⊙ is st))
   ≡ foldlNN Dyck size⊙ tree→stack⊙ is st
stack→tree→stack⊙  ⟩!       = substRefl {B = Dyck 0} _
stack→tree→stack⊙ (⟨ is) = stack→tree→stack⊙ is
stack→tree→stack⊙ (⟩ is) = stack→tree→stack⊙ is

--------------------------------------------------------------------------------
-- Isomorphism
--------------------------------------------------------------------------------

STree : ℕ → Type
STree = fiber size

tree-stack : STree n ⇔ Dyck 0 n
tree-stack .fun (t , n) = subst (Dyck 0) n (tree→stack t)
tree-stack .inv st .fst = stack→tree st
tree-stack .inv st .snd = stack→tree-size⊙ st
tree-stack .leftInv  (t , sz≡) =
  Σ≡Prop
  (λ _ → isSetℕ _ _)
  (J
    (λ n sz≡ → stack→tree (subst (Dyck 0) sz≡ (tree→stack t)) ≡ t)
    (cong stack→tree (substRefl {B = Dyck 0} (tree→stack t)) ; tree→stack→tree⊙ t) sz≡)
tree-stack .rightInv st = stack→tree→stack⊙ st

--------------------------------------------------------------------------------
-- Finite
--------------------------------------------------------------------------------

open import Data.List

support-dyck : ∀ n m → List (Dyck n m)
support-dyck = λ n m → sup-k n m id []
  module ListDyck where
  Diff : Type → Type₁
  Diff A = ∀ {B : Type} → (A → B) → List B → List B

  infixr 5 _++′_
  _++′_ : Diff A → Diff A → Diff A
  xs ++′ ys = λ k → xs k ∘ ys k

  mutual
    sup-k : ∀ n m → Diff (Dyck n m)
    sup-k n m = end n m ++′ lefts n m  ++′ rights n m

    lefts : ∀ n m → Diff (Dyck n m)
    lefts n zero    k = id
    lefts n (suc m) k = sup-k (suc n) m (k ∘ ⟨_)

    rights : ∀ n m → Diff (Dyck n m)
    rights (suc (suc n)) m k = sup-k (suc n) m (k ∘ ⟩_)
    rights _             m k = id

    end : ∀ n m → Diff (Dyck n m)
    end 1 0 k xs = k ⟩! ∷ xs
    end _ _ k = id

open import Data.List.Membership
open import Data.Fin

cover-dyck : (x : Dyck n m) → x ∈ support-dyck n m
cover-dyck x = go _ _ x id []
  where
  open ListDyck

  mutual
    pushLefts : ∀ n m (k : Dyck n m → B) x xs → x ∈ xs → x ∈ lefts n m k xs
    pushLefts n (suc m) k = pushSup (suc n) m (λ z → k (⟨ z))
    pushLefts _ zero    k x xs p = p

    pushEnd : ∀ n m (k : Dyck n m → B) x xs → x ∈ xs → x ∈ end n m k xs
    pushEnd 0 m k x xs p = p
    pushEnd 1 0 k x xs (i , p) = fs i , p
    pushEnd 1 (suc m) k x xs p = p
    pushEnd (suc (suc n)) m k x xs p = p

    pushRights : ∀ n m (k : Dyck n m → B) x xs → x ∈ xs → x ∈ rights n m k xs
    pushRights (suc (suc n)) m k = pushSup (suc n) m λ z → k (⟩ z)
    pushRights 1 _ _ _ _ p = p
    pushRights 0 _ _ _ _ p = p

    pushSup : ∀ n m (k : Dyck n m → B) x xs → x ∈ xs → x ∈ sup-k n m k xs
    pushSup n m k x xs p = pushEnd n m k x (lefts n m k (rights n m k xs)) (pushLefts n m k x (rights n m k xs) (pushRights n m k x xs p))

  go : ∀ n m → (x : Dyck n m) → (k : Dyck n m → A) → (xs : List A) → k x ∈ sup-k n m k xs
  go .1 .0 ⟩! k xs = f0 , refl
  go 0 (suc m) (⟨ x) k xs = go 1 m x (k ∘ ⟨_) xs
  go 1 (suc m) (⟨ x) k xs = go 2 m x (k ∘ ⟨_) xs
  go (suc n@(suc _)) (suc m) (⟨ x) k xs = go (suc (suc n)) m x (k ∘ ⟨_) (rights (suc n) (suc m) k xs)
  go (suc n) m (⟩ x) k xs =
    let p = go n m x (k ∘ ⟩_) xs
    in pushEnd (suc n) m k (k (⟩ x)) (lefts (suc n) m k _) (pushLefts (suc n) m k (k (⟩ x)) (rights (suc n) m k xs) p)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground