text:
module stateDependentObjects where

open import Size renaming (Size to AgdaSize)
open import Agda.Builtin.Equality
open import Data.Nat.Base as N hiding (_⊔_)
open import Data.Product
open import Data.Vec as Vec using (Vec; []; _∷_; head; tail)
open import Function
open import NativeIO
open import Relation.Binary.PropositionalEquality
open import interactiveProgramsAgda
-- open import SizedIO.Base

{- State dependent interfaces, objects -}

record Interfaceˢ : Set₁ where
  field  Stateˢ  : Set
         Methodˢ : (s : Stateˢ) → Set
         Resultˢ : (s : Stateˢ) → (m : Methodˢ s) → Set
         nextˢ   : (s : Stateˢ) → (m : Methodˢ s) → (r : Resultˢ s m)
                   → Stateˢ

open Interfaceˢ public

{- State-Dependent Objects -}

record Objectˢ (I : Interfaceˢ) (s : Stateˢ I) : Set where
  coinductive
  field objectMethod :  (m : Methodˢ I s) →
                        Σ[ r ∈ Resultˢ I s m ] Objectˢ I (nextˢ I s m r)

open Objectˢ public

record IOObjectˢ (Iᵢₒ : IOInterface) (I : Interfaceˢ) (s : Stateˢ I) : Set where
  coinductive
  field method :  (m : Methodˢ I s) →
                  IO Iᵢₒ ∞ (Σ[ r ∈ Resultˢ I s m ] IOObjectˢ Iᵢₒ I (nextˢ I s m r))

{- Example of a Stack -}

StackStateˢ : Set
StackStateˢ = ℕ

data StackMethodˢ (A : Set) : (n : StackStateˢ) → Set where
  push  :  ∀ {n}  →  A  →  StackMethodˢ A n
  pop   :  ∀ {n}         →  StackMethodˢ A (suc n)

StackResultˢ : (A : Set) → (s : StackStateˢ) → StackMethodˢ A s → Set
StackResultˢ A _  (push _)  =  Unit
StackResultˢ A _  pop       =  A

stackNextˢ  :  ∀ A n (m : StackMethodˢ A n) (r : StackResultˢ A n m) →  StackStateˢ
stackNextˢ A  n        (push x)  r  =  suc n
stackNextˢ A  (suc n)  pop       r  =  n

StackInterfaceˢ : (A : Set)  →  Interfaceˢ
Stateˢ   (StackInterfaceˢ A)  =  StackStateˢ
Methodˢ  (StackInterfaceˢ A)  =  StackMethodˢ A
Resultˢ  (StackInterfaceˢ A)  =  StackResultˢ A
nextˢ    (StackInterfaceˢ A)  =  stackNextˢ A

stack  :  ∀{A}{n : ℕ} (as : Vec A n) →  Objectˢ (StackInterfaceˢ A) n
objectMethod (stack as)        (push a)  =  _  ,  stack (a ∷ as)
objectMethod (stack (a ∷ as))  pop       =  a  ,  stack as

{- Reasoning about Stateful Objects -}

{- Bisimiliarity -}

module Bisim (I : Interfaceˢ)
             (let S = Stateˢ I)   (let M = Methodˢ I) (let R = Resultˢ I)
             (let next = nextˢ I) (let O = Objectˢ I)
  where

  data  ΣR     {A : Set} {B : A → Set} (R : ∀{a} (b b' : B a) → Set)
               :  (p p' : Σ A B) → Set
        where
        eqΣ    :  ∀{a}{b b' : B a} → R b b' → ΣR R (a , b) (a , b')

  record _≅_ {s : S} (o o' : O s) : Set where
    coinductive
    field  bisimMethod  :  (m : M s) →
                           ΣR (_≅_) (objectMethod o m) (objectMethod o' m)

  open _≅_ public

  refl≅ :  ∀{s} (o : O s) → o ≅ o
  bisimMethod (refl≅ o) m  =  let  (r , o') =  objectMethod o m
                              in   eqΣ (refl≅ o')

module _ {E : Set} where
  private
    I = StackInterfaceˢ E
    S = Stateˢ I
    O = Objectˢ I
  open Bisim I

{-  Verifying Stack laws -}

  pop-after-push : ∀{n} {v : Vec E n} {e : E} →
    let  st          =  stack v
         (_ , st₁)   =  objectMethod  st   (push e)
         (e₂ , st₂)  =  objectMethod  st₁  pop

    in   (e ≡ e₂) × (st ≅ st₂)

  pop-after-push = refl , refl≅ _

  push-after-pop : ∀{n} {v : Vec E n} {e : E} →
    let  st            =  stack (e ∷ v)
         (e₁  ,  st₁)  =  objectMethod st   pop
         (_   ,  st₂)  =  objectMethod st₁  (push e₁)

    in   st ≅ st₂
  push-after-pop = refl≅ _

{- Bisimilarity of different stack implementations -}

  stackFState = ℕ → E

  pushStackF : E → stackFState → stackFState
  pushStackF e f = λ { 0       → e ;
                       (suc m) → f m}

  popStackFe : stackFState → E
  popStackFe f = f 0

  popStackFf  :  stackFState → stackFState
  popStackFf f = f ∘ suc

  tabulate  :  ∀ (n : ℕ) → stackFState → Vec E n
  tabulate  0        f  =  []
  tabulate  (suc n)  f  =  popStackFe f ∷ tabulate n (popStackFf f)

  stackF : ∀ (n : ℕ) (f : ℕ → E) → Objectˢ (StackInterfaceˢ E) n
  objectMethod (stackF n       f) (push e) = _ ,
                                             stackF (suc n) (pushStackF e f)
  objectMethod (stackF (suc n) f) pop      = popStackFe f ,
                                             stackF n (popStackFf f)

  impl-bisim : ∀{n f} v (p : tabulate n f ≡ v) → stackF n f ≅ stack v
  bisimMethod (impl-bisim v        p) (push e) =
    eqΣ (impl-bisim (e ∷ v)  (cong (_∷_ e)  p))

  bisimMethod (impl-bisim (e ∷ v)  p) pop rewrite cong head p =
    eqΣ (impl-bisim v        (cong tail     p))

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
{-# OPTIONS --without-K #-}
open import Data.Nat.Base using (ℕ)
open import Data.Product
open import HoTT
open import Function.Extensionality
open import Algebra.Group
open import Algebra.Group.Homomorphism
open import Algebra.Group.Isomorphism
open import Function using (id; _∘_ ; flip)
open import Relation.Binary.PropositionalEquality.NP

open import Explore.Core
open import Explore.Properties
import Explore.Explorable as E

open Equivalences

module Explore.Group where

module FromGroupHomomorphism
  {ℓ}{A B : Set ℓ}(𝔾+ : Group A)(𝔾* : Group B)
  (φ : A → B)(φ-hom : GroupHomomorphism 𝔾+ 𝔾* φ)
  where

 open Additive-Group 𝔾+
 open Multiplicative-Group 𝔾*

 module LiftGroupHomomorphism
  {i}{I : Set i}
  {explore : ∀ {ℓ} → Explore ℓ I}
  (explore-ind : ∀ {p ℓ} → ExploreInd {ℓ} p explore)
  (g : I → A)
  where
  open GroupHomomorphism φ-hom

  Σᴵ = explore 0# _+_
  Πᴵ = explore 1# _*_

  lift-hom : φ (Σᴵ g) ≡ Πᴵ (φ ∘ g)
  lift-hom = E.FromExploreInd.LiftHom.lift-hom explore-ind _≡_ refl trans 0# _+_ 1# _*_ *= φ g 0-hom-1 hom

 module FromExplore
   {ℓx} {X : Set ℓx}(z : X)(_⊕_ : X → X → X)
   (exploreᴬ  : Explore ℓx A)
   (exploreᴬ= : ExploreExt exploreᴬ)
   (let [⊕] = exploreᴬ z _⊕_)
   (O : B → X)
   (sui : ∀ {k} → [⊕] (O ∘ φ) ≡ [⊕] (O ∘ _*_ k ∘ φ))
   where

    +-stable : ∀ {k} → [⊕] (O ∘ φ) ≡ [⊕] (O ∘ φ ∘ _+_ k)
    +-stable = Algebra.Group.Homomorphism.Stability.+-stable 𝔾+ 𝔾* φ φ-hom
                  ([⊕] ∘ _∘_ O) (exploreᴬ= _ _ ∘ _∘_ (ap O)) sui

module FromGroupIsomorphism
         {ℓa}{ℓb}{A : Set ℓa}{B : Set ℓb}(𝔾+ : Group A)(𝔾* : Group B)
         (φ : A → B)(φ-iso : GroupIsomorphism 𝔾+ 𝔾* φ) where
 open GroupIsomorphism φ-iso

 open Additive-Group 𝔾+
 open Multiplicative-Group 𝔾*

 module FromBigOp
  {ℓx}{X : Set ℓx}(F : BigOp X A)
  (F= : ∀ {g₀ g₁ : A → X} → g₀ ≗ g₁ → F g₀ ≡ F g₁)
  (O : B → X)
  (sui : ∀ {k} → F (O ∘ φ) ≡ F (O ∘ φ ∘ _+_ k))
  where

  _≈_ : (g₀ g₁ : B → B) → Set ℓx
  g₀ ≈ g₁ = F (O ∘ g₀ ∘ φ) ≡ F (O ∘ g₁ ∘ φ)

  -- The core of the proof is there:
  open Algebra.Group.Isomorphism.Stability 𝔾+ 𝔾* φ φ-iso

  id≈k* : ∀ {k} → id ≈ _*_ k
  id≈k* = *-stable (F  ∘ _∘_ O)
                   (F= ∘ _∘_ (ap O))
                   sui

  k₀*≈k₁* : ∀ {k₀ k₁} → _*_ k₀ ≈ _*_ k₁
  k₀*≈k₁* = ! id≈k* ∙ id≈k*

 module FromExplore
  {ℓx}{X : Set ℓx}(z : X)(_⊕_ : X → X → X)
  (exploreᴬ  : Explore ℓx A)
  (exploreᴬ= : ExploreExt exploreᴬ)
  = FromBigOp (exploreᴬ z _⊕_) (exploreᴬ= z _⊕_)

module FromAdequate-sum
  {ℓb}{A : Set}{B : Set ℓb}(𝔾+ : Group A)(𝔾* : Group B)
  (φ : A → B)(φ-iso : GroupIsomorphism 𝔾+ 𝔾* φ)
  {sum : Sum A}
  (open Adequacy _≡_)
  (sum-adq : Adequate-sum sum)
  {{_ : UA}}{{_ : FunExt}}
  (open E.FromAdequate-sum sum-adq)
  (O : B → ℕ)
  (open Additive-Group 𝔾+)
  (open FromGroupIsomorphism 𝔾+ 𝔾* φ φ-iso)
  = FromBigOp sum sum-ext O (! (sumStableUnder (_ , +-is-equiv) (O ∘ φ)))

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

ext: agda

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The universe polymorphic unit type and the total relation on unit
------------------------------------------------------------------------

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

module Data.Unit.Polymorphic where

------------------------------------------------------------------------
-- Re-export contents of Base module

open import Data.Unit.Polymorphic.Base public

------------------------------------------------------------------------
-- Re-export query operations

open import Data.Unit.Polymorphic.Properties public using (_≟_)


text:
open import Relation.Binary using (Decidable; DecSetoid)
open import Level

module CP.Session2 {a} (ChanSetoid : DecSetoid zero a) (Type : Set) where

Chan : Set
Chan = DecSetoid.Carrier ChanSetoid

_≟Chan_ = DecSetoid._≟_ ChanSetoid
_≈Chan_ = DecSetoid._≈_ ChanSetoid
_≉Chan_ = DecSetoid._≉_ ChanSetoid

infixl 5 _,_∶_
data Session : Set a where
    _,_∶_ : Session → Chan → Type → Session
    _++_ : Session → Session → Session
    ∅ : Session

-- open import Data.Bool hiding (_≟_)

-- open import Data.Empty
-- open import Data.Unit
open import Relation.Nullary
open import Relation.Nullary.Decidable

-- open import Relation.Binary.PropositionalEquality

infix 4 _∋_
data _∋_ : (Γ : Session) → (x : Chan) → Set a where
  here  : ∀ {Γ x y A} → x ≈Chan y         → Γ , y ∶ A ∋ x
  there : ∀ {Γ x y A} →             Γ ∋ x → Γ , y ∶ A ∋ x
  left  : ∀ {Γ Δ x}               → Γ ∋ x → Γ ++ Δ    ∋ x
  right : ∀ {Γ Δ x}               → Δ ∋ x → Γ ++ Δ    ∋ x

infix 4 _∋?_
_∋?_ : (Γ : Session) → (x : Chan) → Dec (Γ ∋ x)
Γ , y ∶ A ∋? x with x ≟Chan y
... | yes x≈y = yes (here x≈y)
... | no ¬x≈y with Γ ∋? x
... | yes Γ∋x = yes (there Γ∋x)
... | no ¬Γ∋x = no (λ where (here x≈y) → ¬x≈y x≈y
                            (there Γ∋x) → ¬Γ∋x Γ∋x)
(Γ ++ Δ) ∋? x with Γ ∋? x
... | yes Γ∋x = yes (left Γ∋x)
... | no ¬Γ∋x with Δ ∋? x
... | yes Δ∋x = yes (right Δ∋x)
... | no ¬Δ∋x = no (λ where (left Γ∋x) → ¬Γ∋x Γ∋x
                            (right Δ∋x) → ¬Δ∋x Δ∋x)
∅ ∋? x = no (λ ())

open import Data.Product
open import Data.Empty using (⊥-elim)

infix 4 _≈_
_≈_ : Session → Session → Set a
Γ ≈ Δ = (∀ x → Γ ∋ x → Δ ∋ x) × (∀ x → Δ ∋ x → Γ ∋ x)

∅∌x : ∀ {x} → ¬ ∅ ∋ x
∅∌x ()

open DecSetoid ChanSetoid hiding (_≈_)

∅-empty : ∀ {Δ x A} → ¬ ∅ ≈ Δ , x ∶ A
∅-empty {Δ} {x} (P , Q) = ∅∌x (Q x (here refl))

<<<<<<< HEAD
swap : ∀ {Γ x y A B} → Γ , x ∶ A , y ∶ B ≈ Γ , y ∶ B , x ∶ A
swap {Γ} {x} {y} {A} {B} = to , from
  where
    to : ∀ v → Γ , x ∶ A , y ∶ B ∋ v → Γ , y ∶ B , x ∶ A ∋ v
    to v (here P) = there (here P)
    to v (there (here P)) = here P
    to v (there (there P)) = there (there P)

    from : ∀ v → Γ , y ∶ B , x ∶ A ∋ v → Γ , x ∶ A , y ∶ B ∋ v
    from v (here P) = there (here P)
    from v (there (here P)) = here P
    from v (there (there P)) = there (there P)

-- contract : ∀ {Γ x y A B} →  → Γ , x ∶ A ≈ Γ
-- contract
-- strengthen : ∀ {Γ x A v} → Γ , x ∶ A ∋ v → x ≉ v → Γ ∋ v
-- strengthen (here x≈v) x≉v = ⊥-elim (x≉v (sym x≈v))
-- strengthen (there P) x≉v = P
=======
>>>>>>> 40f82fd098a0c30c87ea0056baa48152aefae1f6

lookup : (Γ : Session) (x : Chan) → Dec (∃[ Δ ] ∃[ A ] (Γ ≈ (Δ , x ∶ A)))
lookup (Γ , y ∶ A) x with x ≟Chan y
... | yes x≈y = yes (Γ , A  , (λ where v (here v≈y) → here (trans v≈y (sym x≈y))
                                       v (there Γ∷y∋v) → there Γ∷y∋v)
                             , λ where v (here v≈x) → here (trans v≈x x≈y)
                                       v (there Γ∷x∋v) → there Γ∷x∋v)
... | no ¬x≈y with lookup Γ x
... | yes (Δ , B , Γ≈Δ,x∶B) = yes (Δ , y ∶ A , B  , (λ where v (here v≈y) → there (here v≈y)
<<<<<<< HEAD
                                                             v (there Γ∋v) → proj₁ swap v (there (proj₁ Γ≈Δ,x∶B v Γ∋v)))
                                                  , λ where v (here v≈x) → there (proj₂ Γ≈Δ,x∶B v (here v≈x))
                                                            v (there (here v≈y)) → here v≈y
                                                            v (there (there Δ∋v)) → there (proj₂ Γ≈Δ,x∶B v (there Δ∋v)))
... | no ¬P = no (λ (Δ , B , Q) → ¬P (Δ , B , {!   !}))
  -- (λ where v P → proj₁ Q v (there P))
  --                                           , (λ where v P → {! proj₂ Q v P   !})))
=======
                                                             v (there Γ∋v) → {!   !}) , {!   !})
... | no P = {!   !}
>>>>>>> 40f82fd098a0c30c87ea0056baa48152aefae1f6
lookup (Γ ++ Δ) x = {!   !}
lookup ∅ x = no (λ where (Δ , A , P) → ∅-empty P)

-- ... | yes x≈y = yes (Γ , A , λ v → (λ where (here v≈y) → here (trans v≈y (sym x≈y))
--                                             (there Γ∋v) → there Γ∋v) -- (λ v≈x → v≉y (trans v≈x x≈y))
--                                   , λ where (here v≈x) → here (trans v≈x x≈y)
--                                             (there Γ∋v) → there Γ∋v) -- (λ v≈y → v≉x (trans v≈y (sym x≈y)))
-- ... | no ¬x≈y with lookup Γ x
-- ... | yes (Δ , B , Γ≈Δ,x∶B) = yes (Δ , y ∶ A , B , λ v → (λ where (here v≈y) → there (here v≈y) -- (λ v≈x → ¬x≈y (trans (sym v≈x) v≈y))
--                                                                   (there Γ∋v) → lemma-1 (proj₁ (Γ≈Δ,x∶B v) Γ∋v))
--                                                         , λ where (here v≈x) → there (proj₂ (Γ≈Δ,x∶B v) (here v≈x)) -- (λ v≈y → ¬x≈y (trans (sym v≈x) v≈y))
--                                                                   (there Δ,y∶A∋y) → ,-weakening y A (proj₂ (Γ≈Δ,x∶B v)) (lemma-1 Δ,y∶A∋y))
--     where
--       lemma-1 : ∀ {Γ x y z A B} → Γ , x ∶ A ∋ z → Γ , y ∶ B , x ∶ A ∋ z
--       lemma-1 (here z≈x) = here z≈x
--       lemma-1 (there Γ∋z) = there (there Γ∋z)

--       ,-weakening : ∀ {Γ Δ v} x A → (Γ ∋ v → Δ ∋ v) → (Γ , x ∶ A ∋ v → Δ , x ∶ A ∋ v)
--       ,-weakening x A f (here v≈x) = here v≈x
--       ,-weakening x A f (there Γ∋v) = there (f Γ∋v)

-- ... | no ¬P = no λ Q → {!   !}

-- -- GOAL : Γ , y ∶ A ≉ CTX , x ∶ TYPE
-- -- ¬P     Γ         ≉ CTX , x : TYPE

--   -- no (λ (Δ , B , Q) → ¬P (Δ , B , {!  Q !}))
--   -- λ v → (λ Γ∋v → proj₁ (Q v) (there Γ∋v))
--   --                                                 , (λ Δ,x∶B∋v → {! proj₂ (Q v) Δ,x∶B∋v  !})))
--   --                       → (λ Γ∋v → proj₁ (Q v) (there Γ∋v))
--   --                       , λ Δ,x∶B∋v → {! (proj₂ (Q v) Δ,x∶B∋v)  !}))
--                           -- where
--                           --   (here P)  → strengthen (proj₂ (Q v) (here P)) (λ y≈v → ¬x≈y (sym (trans y≈v P)))
--                           --   (there P) → {!   !}))

--     where

--       -- GOAL : Δ , x ∶ B           →       Γ

--       -- Q v :  Δ , x ∶ B          <≈>      Γ , y ∶ A

--       -- -- ¬P Δ A =              Γ   <=>  Δ , x ∶ A
--       --        (x₁ : Carrier) →
--       --        Σ (Γ ∋ x₁ → Δ₁ , x ∶ A₁ ∋ x₁) (λ x₂ → Δ₁ , x ∶ A₁ ∋ x₁ → Γ ∋ x₁)))

--       strengthen : ∀ {Γ x A v} → Γ , x ∶ A ∋ v → x ≉ v → Γ ∋ v
--       strengthen (here x≈v) x≉v = ⊥-elim (x≉v (sym x≈v))
--       strengthen (there P) x≉v = P

--       temp : ∀ Δ B v → (Δ ∋ v) → (f : Δ , x ∶ B ∋ v → Γ , y ∶ A ∋ v) → Γ ∋ v
--       temp Δ B v Δ∋v f with v ≟Chan x
--       ... | yes v≈x = strengthen (f (here v≈x)) (λ y≈v → ¬x≈y (sym (trans y≈v v≈x)))
--       ... | no ¬v≈x with y ≟Chan v
--       ... | yes y≈v = {!   !}
--       ... | no ¬y≈v = strengthen (f (there Δ∋v)) ¬y≈v
--         -- strengthen (f (there Δ∈v)) λ y≈v → {!   !}

--       -- lemma : G

-- lookup (Γ ++ Δ) x = {!   !}
-- lookup ∅ x = no (λ where (Δ , A , P) → ∅-empty P)

-- -- _≈?_ : (Γ Δ : Session) → Dec (Γ ≈ Δ)
-- -- Γ ≈? Δ = {!   !}
-- -- empty : ∀ {Γ x A} → ¬ (∅ ≈ (Γ , x ∶ A))
-- -- empty {Γ} {x} {A} P with x ≟ x
-- -- ... | no ¬p = {!   !}
-- -- ... | yes p = {!   !}

-- -- lookup : (Γ : Session) (x : Chan) → Dec (∃[ Δ ] ∃[ A ] (Γ ≈ (Δ , x ∶ A)))
-- -- lookup (Γ , y ∶ A) x = {!   !}
-- -- lookup (Γ ++ Δ) x with lookup Γ x
-- -- ... | yes p = {!   !}
-- -- ... | no ¬p = {!   !}
-- -- lookup ∅ x = no (λ where (Γ , A , P) → {! P x  !})

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


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

open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (fromWitness; toWitness)
open import Function using (_∘_)
open import Data.Empty using (⊥-elim)

import Data.Fin as Fin
import Data.Unit as Unit
import Data.Product as Product
import Data.Vec as Vec
import Data.Vec.Relation.Unary.All as All
import Data.Nat as ℕ

open Fin using (Fin; zero; suc)
open Unit using (⊤; tt)
open ℕ using (ℕ)
open Product using (Σ-syntax; ∃-syntax; _,_; _×_; proj₁; proj₂)
open Vec using (Vec; []; _∷_)
open All using (All; []; _∷_)

module PiCalculus.LinearTypeSystem.Algebras where

private
  variable
    n : ℕ

infixr 100 _²

_² : ∀ {a} → Set a → Set a
A ² = A × A

record Algebra (Q : Set) : Set₁ where
  field
    0∙ 1∙       : Q

    _≔_∙_       : Q → Q → Q → Set

    -- Given two operands, we can decide whether a third one exists
    ∙-computeʳ  : ∀ x y         → Dec (∃[ z ] (x ≔ y ∙ z))

    -- If a third operand exists, it must be unique
    ∙-unique    : ∀ {x x' y z}  → x' ≔ y ∙ z → x ≔ y ∙ z → x' ≡ x
    ∙-uniqueˡ   : ∀ {x y y' z}  → x ≔ y' ∙ z → x ≔ y ∙ z → y' ≡ y

    -- 0 is the minimum
    0∙-minˡ     : ∀ {y z}       → 0∙ ≔ y ∙ z → y ≡ 0∙

    -- Neutral element, commutativity, associativity
    ∙-idˡ       : ∀ {x}         → x ≔ 0∙ ∙ x
    ∙-comm      : ∀ {x y z}     → x ≔ y ∙ z → x ≔ z ∙ y -- no need for right rules
    ∙-assoc     : ∀ {x y z u v} → x ≔ y ∙ z → y ≔ u ∙ v → ∃[ w ] (x ≔ u ∙ w × w ≔ v ∙ z)

  ℓ∅ : Q ²
  ℓ∅ = 0∙ , 0∙

  ℓᵢ : Q ²
  ℓᵢ = 1∙ , 0∙

  ℓₒ : Q ²
  ℓₒ = 0∙ , 1∙

  ℓ# : Q ²
  ℓ# = 1∙ , 1∙

  _≔_∙²_ : Q ² → Q ² → Q ² → Set
  (lx , rx) ≔ (ly , ry) ∙² (lz , rz) = (lx ≔ ly ∙ lz) × (rx ≔ ry ∙ rz)

  ∙-idʳ : ∀ {x} → x ≔ x ∙ 0∙
  ∙-idʳ = ∙-comm ∙-idˡ

  ∙-assoc⁻¹ : ∀ {x y z u v} → x ≔ y ∙ z → z ≔ u ∙ v → ∃[ ； ] (x ≔ ； ∙ v × ； ≔ y ∙ u)
  ∙-assoc⁻¹ a b = let _ , a' , b' = ∙-assoc (∙-comm a) (∙-comm b) in _ , ∙-comm a' , ∙-comm b'

  ∙-mut-cancel : ∀ {x y y' z} → x ≔ y ∙ z → z ≔ y' ∙ x → x ≡ z
  ∙-mut-cancel x≔y∙z z≔y'∙x with ∙-assoc⁻¹ x≔y∙z z≔y'∙x
  ∙-mut-cancel x≔y∙z z≔y'∙x | e , x≔e∙x , e≔y∙y' rewrite ∙-uniqueˡ x≔e∙x ∙-idˡ | 0∙-minˡ e≔y∙y' = ∙-unique x≔y∙z ∙-idˡ

  ∙²-computeʳ : ∀ x y → Dec (∃[ z ] (x ≔ y ∙² z))
  ∙²-computeʳ (lx , rx) (ly , ry) with ∙-computeʳ lx ly | ∙-computeʳ rx ry
  ∙²-computeʳ (lx , rx) (ly , ry) | yes (_ , p) | yes (_ , q) = yes (_ , p , q)
  ∙²-computeʳ (lx , rx) (ly , ry) | yes p | no ¬q = no λ {(_ , _ , r) → ¬q (_ , r)}
  ∙²-computeʳ (lx , rx) (ly , ry) | no ¬p | _     = no λ {(_ , l , _) → ¬p (_ , l)}

  ∙²-unique : ∀ {x x' y z} → x' ≔ y ∙² z → x ≔ y ∙² z → x' ≡ x
  ∙²-unique {x = _ , _} {x' = _ , _} (ll , rl) (lr , rr)
    rewrite ∙-unique ll lr | ∙-unique rl rr = refl

  ∙²-uniqueˡ : ∀ {x y y' z} → x ≔ y' ∙² z → x ≔ y ∙² z → y' ≡ y
  ∙²-uniqueˡ {y = _ , _} {y' = _ , _} (ll , lr) (rl , rr)
    rewrite ∙-uniqueˡ ll rl | ∙-uniqueˡ lr rr = refl

  ∙²-idˡ : ∀ {x} → x ≔ (0∙ , 0∙) ∙² x
  ∙²-idˡ = ∙-idˡ , ∙-idˡ

  ∙²-comm : ∀ {x y z} → x ≔ y ∙² z → x ≔ z ∙² y
  ∙²-comm (lx , rx) = ∙-comm lx , ∙-comm rx

  ∙²-idʳ : ∀ {x} → x ≔ x ∙² (0∙ , 0∙)
  ∙²-idʳ = ∙²-comm ∙²-idˡ

  ∙²-assoc : ∀ {x y z u v} → x ≔ y ∙² z → y ≔ u ∙² v → ∃[ w ] (x ≔ u ∙² w × w ≔ v ∙² z)
  ∙²-assoc (lx , rx) (ly , ry) with ∙-assoc lx ly | ∙-assoc rx ry
  ∙²-assoc (lx , rx) (ly , ry) | _ , ll , rl | _ , lr , rr = _ , ((ll , lr) , (rl , rr))

  ∙²-assoc⁻¹ : ∀ {x y z u v} → x ≔ y ∙² z → z ≔ u ∙² v → ∃[ ； ] (x ≔ ； ∙² v × ； ≔ y ∙² u)
  ∙²-assoc⁻¹ a b = let _ , a' , b' = ∙²-assoc (∙²-comm a) (∙²-comm b) in _ , ∙²-comm a' , ∙²-comm b'

  ∙²-mut-cancel : ∀ {x y y' z} → x ≔ y ∙² z → z ≔ y' ∙² x → x ≡ z
  ∙²-mut-cancel {_ , _} (lx , rx) (ly , ry) rewrite ∙-mut-cancel lx ly | ∙-mut-cancel rx ry = refl

record Algebras : Set₁ where
  field
    Idx          : Set
    ∃Idx         : Idx
    Usage        : Idx → Set
    UsageAlgebra : ∀ idx → Algebra (Usage idx)

  infixl 40 _-,_
  pattern _-,_ xs x = _∷_ x xs

  module _ {idx : Idx} where
    open Algebra (UsageAlgebra idx) public

max_stars_repo_name: guilhermehas/typing-linear-pi

max_issues_repo_name: guilhermehas/typing-linear-pi

max_forks_repo_name: guilhermehas/typing-linear-pi


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Conversion of _≤_ to _<_
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Construct.NonStrictToStrict
  {a ℓ₁ ℓ₂} {A : Set a} (_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) where

open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Sum using (inj₁; inj₂)
open import Function using (_∘_; flip)
open import Relation.Nullary using (¬_; yes; no)

------------------------------------------------------------------------
-- _≤_ can be turned into _<_ as follows:

_<_ : Rel A _
x < y = (x ≤ y) × ¬ (x ≈ y)

------------------------------------------------------------------------
-- The converted relations have certain properties
-- (if the original relations have certain other properties)

<⇒≤ : _<_ ⇒ _≤_
<⇒≤ = proj₁

<-irrefl : Irreflexive _≈_ _<_
<-irrefl x≈y (_ , x≉y) = x≉y x≈y

<-trans : IsPartialOrder _≈_ _≤_ → Transitive _<_
<-trans po (x≤y , x≉y) (y≤z , y≉z) =
  (trans x≤y y≤z , x≉y ∘ antisym x≤y ∘ trans y≤z ∘ reflexive ∘ Eq.sym)
  where open IsPartialOrder po

<-≤-trans : Symmetric _≈_ → Transitive _≤_ → Antisymmetric _≈_ _≤_ →
           _≤_ Respectsʳ _≈_ → Trans _<_ _≤_ _<_
<-≤-trans sym trans antisym respʳ (x≤y , x≉y) y≤z =
  trans x≤y y≤z , (λ x≈z → x≉y (antisym x≤y (respʳ (sym x≈z) y≤z)))

≤-<-trans : Transitive _≤_ → Antisymmetric _≈_ _≤_ →
           _≤_ Respectsˡ _≈_ → Trans _≤_ _<_ _<_
≤-<-trans trans antisym respʳ x≤y (y≤z , y≉z) =
  trans x≤y y≤z , (λ x≈z → y≉z (antisym y≤z (respʳ x≈z x≤y)))

<-asym : Antisymmetric _≈_ _≤_ → Asymmetric _<_
<-asym antisym (x≤y , x≉y) (y≤x , _) = x≉y (antisym x≤y y≤x)

<-respˡ-≈ : Transitive _≈_ → _≤_ Respectsˡ _≈_ → _<_ Respectsˡ _≈_
<-respˡ-≈ trans respˡ y≈z (y≤x , y≉x) =
  (respˡ y≈z y≤x) , (λ z≈x → y≉x (trans y≈z z≈x))

<-respʳ-≈ : Symmetric _≈_ → Transitive _≈_ →
            _≤_ Respectsʳ _≈_ → _<_ Respectsʳ _≈_
<-respʳ-≈ sym trans respʳ {x} {y} {z} y≈z (x≤y , x≉y) =
  (respʳ y≈z x≤y) , λ x≈z → x≉y (trans x≈z (sym y≈z))

<-resp-≈ : IsEquivalence _≈_ → _≤_ Respects₂ _≈_ → _<_ Respects₂ _≈_
<-resp-≈ eq (respʳ , respˡ) =
  <-respʳ-≈ sym trans respʳ , <-respˡ-≈ trans respˡ
  where open IsEquivalence eq

<-trichotomous : Symmetric _≈_ → Decidable _≈_ →
                 Antisymmetric _≈_ _≤_ → Total _≤_ →
                 Trichotomous _≈_ _<_
<-trichotomous ≈-sym _≟_ antisym total x y with x ≟ y
... | yes x≈y = tri≈ (<-irrefl x≈y) x≈y (<-irrefl (≈-sym x≈y))
... | no  x≉y with total x y
...   | inj₁ x≤y = tri< (x≤y , x≉y) x≉y
                        (x≉y ∘ antisym x≤y ∘ proj₁)
...   | inj₂ x≥y = tri> (x≉y ∘ flip antisym x≥y ∘ proj₁) x≉y
                        (x≥y , x≉y ∘ ≈-sym)

<-decidable : Decidable _≈_ → Decidable _≤_ → Decidable _<_
<-decidable _≟_ _≤?_ x y with x ≟ y | x ≤? y
... | yes x≈y | _       = no (flip proj₂ x≈y)
... | no  x≉y | yes x≤y = yes (x≤y , x≉y)
... | no  x≉y | no  x≰y = no (x≰y ∘ proj₁)

<-isStrictPartialOrder : IsPartialOrder _≈_ _≤_ →
                         IsStrictPartialOrder _≈_ _<_
<-isStrictPartialOrder po = record
  { isEquivalence = isEquivalence
  ; irrefl        = <-irrefl
  ; trans         = <-trans po
  ; <-resp-≈      = <-resp-≈ isEquivalence ≤-resp-≈
  } where open IsPartialOrder po

<-isStrictTotalOrder₁ : Decidable _≈_ → IsTotalOrder _≈_ _≤_ →
                        IsStrictTotalOrder _≈_ _<_
<-isStrictTotalOrder₁ ≟ tot = record
  { isEquivalence = isEquivalence
  ; trans         = <-trans isPartialOrder
  ; compare       = <-trichotomous Eq.sym ≟ antisym total
  } where open IsTotalOrder tot

<-isStrictTotalOrder₂ : IsDecTotalOrder _≈_ _≤_ →
                        IsStrictTotalOrder _≈_ _<_
<-isStrictTotalOrder₂ dtot = <-isStrictTotalOrder₁ _≟_ isTotalOrder
  where open IsDecTotalOrder dtot

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

-- Version 0.16

irrefl         = <-irrefl
{-# WARNING_ON_USAGE irrefl
"Warning: irrefl was deprecated in v0.16.
Please use <-irrefl instead."
#-}
trans          = <-trans
{-# WARNING_ON_USAGE trans
"Warning: trans was deprecated in v0.16.
Please use <-trans instead."
#-}
antisym⟶asym = <-asym
{-# WARNING_ON_USAGE antisym⟶asym
"Warning: antisym⟶asym was deprecated in v0.16.
Please use <-asym instead."
#-}
decidable      = <-decidable
{-# WARNING_ON_USAGE decidable
"Warning: decidable was deprecated in v0.16.
Please use <-decidable instead."
#-}
trichotomous   = <-trichotomous
{-# WARNING_ON_USAGE trichotomous
"Warning: trichotomous was deprecated in v0.16.
Please use <-trichotomous instead."
#-}
isPartialOrder⟶isStrictPartialOrder = <-isStrictPartialOrder
{-# WARNING_ON_USAGE isPartialOrder⟶isStrictPartialOrder
"Warning: isPartialOrder⟶isStrictPartialOrder was deprecated in v0.16.
Please use <-isStrictPartialOrder instead."
#-}
isTotalOrder⟶isStrictTotalOrder     = <-isStrictTotalOrder₁
{-# WARNING_ON_USAGE isTotalOrder⟶isStrictTotalOrder
"Warning: isTotalOrder⟶isStrictTotalOrder was deprecated in v0.16.
Please use <-isStrictTotalOrder₁ instead."
#-}
isDecTotalOrder⟶isStrictTotalOrder  = <-isStrictTotalOrder₂
{-# WARNING_ON_USAGE isDecTotalOrder⟶isStrictTotalOrder
"Warning: isDecTotalOrder⟶isStrictTotalOrder was deprecated in v0.16.
Please use <-isStrictTotalOrder₂ instead."
#-}


text:
-- Andreas 2012-09-27, reported by Fredrik Forsberg
{-# OPTIONS --sized-types #-}
module Issue701-c where

  open import Common.Size

{- If I understand correctly, unconstrained sizes should be resolved to \infty.
If I define -}

  data U : {i : Size} -> Set where
    c : {i : Size} -> U {↑ i}

  data V : {i : Size} -> Set where
    d : {i : Size} -> U {∞} -> V {↑ i}

  works-with-explicit-infty : {i : Size} -> V {i} -> V {↑ i}
  works-with-explicit-infty x = x

-- everything is fine. However, if I leave out {\infty}:

  data V' : {i : Size} -> Set where
    d : {i : Size} -> U -> V' {↑ i}

  fails-if-no-infty : {i : Size} -> V' {i} -> V' {↑ i}
  fails-if-no-infty x = x
  --.i != ↑ .i of type Size
  --when checking that the expression x has type V'

{- V' is not detected as a sized type anymore which seems to break the
promise about unconstrained sizes. Since U is just a non-inductive
argument to d, I wouldn't expect it to influence whether V is a sized
type or not? -}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Relation.Binary.Core using (Decidable ; _≡_)

module Precond (Carrier : Set) (deq : Decidable {A = Carrier} _≡_) where

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin ; zero ; suc)
open import Data.Fin.Properties using (_≟_)
open import Data.List using (List ; [] ; _∷_)
open import Level using () renaming (zero to ℓ₀)
import Category.Monad
import Category.Functor
open import Data.Maybe using (Maybe ; nothing ; just ; maybe′)
open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_)
open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_)
open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList)
open import Data.Vec.Properties using (map-cong ; map-∘ ; tabulate-∘)
import Data.List.All
open import Data.List.Any using (here ; there)
open Data.List.Any.Membership-≡ using (_∉_)
open import Data.Maybe using (just)
open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
open import Function using (flip ; _∘_ ; id)
open import Relation.Binary using (Setoid)
open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid)
open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
open import Relation.Nullary using (yes ; no)

open import Structures using (IsFunctor ; module Shaped ; Shaped)
open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete ; lemma-lookupM-fromFunc ; reshape ; lemma-reshape-id)
import CheckInsert
open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
import BFF
import Bidir
open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain)
import GetTypes
open GetTypes.PartialShapeShape using (Get ; module Get)
open BFF.PartialShapeBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff)

lemma-maybe-just : {A : Set} → (a : A) → (ma : Maybe A) → maybe′ Maybe.just (just a) ma ≡ Maybe.just (maybe′ id a ma)
lemma-maybe-just a (just x) = refl
lemma-maybe-just a nothing = refl

lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : FinMapMaybe n A} {g : Fin n → A} → is in-domain-of h → ∃ λ v → union h (delete-many is (fromFunc g)) ≡ fromFunc v
lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (lemma-tabulate-∘ (λ f → begin
      maybe′ just (lookupM f (fromFunc g)) (lookupM f h)
        ≡⟨ cong (flip (maybe′ just) (lookupM f h)) (lemma-lookupM-fromFunc g f) ⟩
      maybe′ just (just (g f)) (lookupM f h)
        ≡⟨ lemma-maybe-just (g f) (lookupM f h) ⟩
      just (maybe′ id (g f) (lookupM f h)) ∎))
lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.All._∷_ (x , px) ps) = _ , (begin
  union h (delete i (delete-many is (fromFunc g)))
    ≡⟨ lemma-tabulate-∘ inner ⟩
  union h (delete-many is (fromFunc g))
    ≡⟨ proj₂ (lemma-union-delete-fromFunc ps) ⟩
  _ ∎)
  where inner : (f : Fin n) → maybe′ just (lookupM f (delete i (delete-many is (fromFunc g)))) (lookup f h) ≡ maybe′ just (lookupM f (delete-many is (fromFunc g))) (lookup f h)
        inner f with f ≟ i
        inner .i | yes refl = begin
          maybe′ just (lookupM i (delete i (delete-many is (fromFunc g)))) (lookup i h)
            ≡⟨ cong (maybe′ just _) px ⟩
          just x
            ≡⟨ cong (maybe′ just _) (sym px) ⟩
          maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎
        inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i)

module _ (G : Get) where
  open Get G
  open Shaped ViewShapeT using () renaming (content to contentV)

  assoc-enough : {i : I} → (j : I) → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ j)) → ∃ (λ h → assoc (contentV (get (enumerate SourceShapeT (gl₁ j)))) (contentV v) ≡ just h) → ∃ λ u → bff G j s v ≡ just u
  assoc-enough {i} j s v (h , p) = _ , cong (_<$>_ ((λ f → fmapS f t) ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Shaped.arity SourceShapeT (gl₁ j))))) p
    where g′ = delete-many (contentV (get (enumerate SourceShapeT (gl₁ i)))) (fromFunc (denumerate SourceShapeT s))
          t  = enumerate SourceShapeT (gl₁ j)

module _ (G : Get) where
  open Get G
  open Shaped ViewShapeT using () renaming (content to contentV)

  assoc-enough′ : {i : I} → (s : SourceContainer Carrier (gl₁ i)) → (v : ViewContainer Carrier (gl₂ i)) → ∃ (λ h → assoc (contentV (get (enumerate SourceShapeT (gl₁ i)))) (contentV v) ≡ just h) → ∃ λ u → bff G i s v ≡ just (fmapS just u)
  assoc-enough′ {i} s v (h , p) = _ , (begin
    bff G i s v
      ≡⟨ proj₂ (assoc-enough G i s v (h , p)) ⟩
    just (fmapS (flip lookupM (union h (reshape g′ (Shaped.arity SourceShapeT (gl₁ i))))) t)
      ≡⟨ cong just (begin _
          ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩
        fmapS (flip lookupM (union h g′)) t
          ≡⟨ cong ((λ f → fmapS f t) ∘ flip lookupM) (proj₂ wp) ⟩
        fmapS (flip lookupM (fromFunc (proj₁ wp))) t
          ≡⟨ IsFunctor.cong (Shaped.isFunctor SourceShapeT (gl₁ i)) (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩
        fmapS (Maybe.just ∘ proj₁ wp) t
          ≡⟨ IsFunctor.composition (Shaped.isFunctor SourceShapeT (gl₁ i)) just (proj₁ wp) t ⟩
        fmapS Maybe.just (fmapS (proj₁ wp) t) ∎) ⟩ _ ∎)
    where s′ = enumerate SourceShapeT (gl₁ i)
          g  = fromFunc (denumerate SourceShapeT s)
          g′ = delete-many (contentV (get s′)) g
          t  = enumerate SourceShapeT (gl₁ i)
          wp = lemma-union-delete-fromFunc (lemma-assoc-domain (contentV (get t)) (contentV v) p)

data All-different {A : Set} : List A → Set where
  different-[] : All-different []
  different-∷  : {x : A} {xs : List A} → x ∉ xs → All-different xs → All-different (x ∷ xs)

lemma-∉-lookupM-assoc : {m n : ℕ} → (i : Fin n) → (is : Vec (Fin n) m) → (xs : Vec Carrier m) → {h : FinMapMaybe n Carrier} → assoc is xs ≡ just h → (i ∉ toList is) → lookupM i h ≡ nothing
lemma-∉-lookupM-assoc i []         []         refl i∉is = lemma-lookupM-empty i
lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') ph i∉is with assoc is' xs' | inspect (assoc is') xs'
lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') () i∉is | nothing | [ ph' ]
lemma-∉-lookupM-assoc i (i' ∷ is') (x' ∷ xs') {h} ph i∉is | just h' | [ ph' ] = begin
  lookupM i h
    ≡⟨ lemma-lookupM-checkInsert-other i i' (i∉is ∘ here) x' h' ph ⟩
  lookupM i h'
    ≡⟨ lemma-∉-lookupM-assoc i is' xs' ph' (i∉is ∘ there) ⟩
  nothing ∎

different-assoc : {m n : ℕ} → (u : Vec (Fin n) m) → (v : Vec Carrier m) → All-different (toList u) → ∃ λ h → assoc u v ≡ just h
different-assoc []       []       p = empty , refl
different-assoc (u ∷ us) (v ∷ vs) (different-∷ u∉us diff-us) with different-assoc us vs diff-us
different-assoc (u ∷ us) (v ∷ vs) (different-∷ u∉us diff-us) | h , p' = insert u v h , (begin
  assoc (u ∷ us) (v ∷ vs)
    ≡⟨ refl ⟩
  (assoc us vs >>= checkInsert u v)
    ≡⟨ cong (flip _>>=_ (checkInsert u v)) p' ⟩
  checkInsert u v h
    ≡⟨ lemma-checkInsert-new u v h (lemma-∉-lookupM-assoc u us vs p' u∉us) ⟩
  just (insert u v h) ∎)

max_stars_repo_name: jvoigtlaender/bidiragda

max_issues_repo_name: jvoigtlaender/bidiragda

max_forks_repo_name: jvoigtlaender/bidiragda


text:
module Data.Real.Properties where

open import Data.Real.Base as ℝ
open import Data.Real.Order
open import Data.Real.Abstract.Structures
  using (IsOrderedHeytingField; IsArchimedanHeytingField)
open import Assume
open import Algebra using (IsCommutativeRing; CommutativeRing)
open import Algebra.Module using (Module)
open import Algebra.Module.Construct.TensorUnit using (⟨module⟩)
open import Algebra.Module.Normed using (IsNormedModule; NormedModule)
open import Algebra.Apartness using (IsHeytingField; HeytingField)
open import Level using (0ℓ)
open import Data.Product using (_,_)

+-*-isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0.0 1.0
+-*-isCommutativeRing = assume

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

+-*-module : Module +-*-commutativeRing 0ℓ 0ℓ
+-*-module = ⟨module⟩

+-*-isHeytingField : IsHeytingField _≈_ _≉_ _+_ _*_ -_ 0.0 1.0
+-*-isHeytingField = assume

+-*-heytingField : HeytingField 0ℓ 0ℓ 0ℓ
+-*-heytingField = record { isHeytingField = +-*-isHeytingField  }

+-*-isOrderedHeytingField : IsOrderedHeytingField +-*-heytingField _<_
+-*-isOrderedHeytingField =
  record
  { isStrictTotalOrder = <-isStrictTotalOrder
  ; ordered = assume
  }

+-*-isArchimedanHeytingField : IsArchimedanHeytingField +-*-heytingField _<_
+-*-isArchimedanHeytingField =
  record
  { dense = λ a b a<b → ((a + b) ÷ 2.0) , assume
  ; archimedan = λ a b a<0 b<0 → ∣ unsafeM ⌈ b ÷ a ⌉ ∣ , assume
  }
  where
    open import Data.Integer using (∣_∣)
    open import Data.Maybe

    unsafeM : ∀ {a} {A : Set a} → Maybe A → A
    unsafeM (just x) = x
    unsafeM nothing = assume

abs-isNormedModule : IsNormedModule +-*-module _≤_ abs
abs-isNormedModule = assume

abs-normedModule : NormedModule +-*-commutativeRing _≤_ 0ℓ 0ℓ
abs-normedModule = record { isNormedModule = abs-isNormedModule  }

max_stars_repo_name: cspollard/reals

max_issues_repo_name: cspollard/reals

max_forks_repo_name: cspollard/reals


text:
module MalformedModuleNameInIMPORT where

{-# IMPORT m #-}

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Numeral.Natural.TotalOper where

import Lvl
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Natural hiding (𝐏)
open import Numeral.Natural.Relation.Divisibility
open import Numeral.Natural.Relation.Divisibility.Proofs
open import Numeral.Natural.Relation
open import Numeral.Natural.Relation.Order
open import Numeral.Natural.Relation.Order.Proofs
open import Relator.Equals
open import Relator.Equals.Proofs

-- Total predecessor function (Truncated predecessor)
𝐏 : (n : ℕ) → ⦃ _ : Positive(n) ⦄ → ℕ
𝐏(𝐒(n)) = n

-- Total subtraction (Truncated subtraction)
_−_ : (a : ℕ) → (b : ℕ) → ⦃ _ : a ≥ b ⦄ → ℕ
_−_ a 𝟎 = a
_−_ 𝟎 (𝐒(b)) ⦃ 0≥𝐒b ⦄ with ([<]-to-[≱] ([<]-minimum{b})) (0≥𝐒b)
... | ()
_−_ (𝐒(a)) (𝐒(b)) ⦃ 𝐒b≤𝐒a ⦄ = _−_ a b ⦃ [≤]-without-[𝐒] {b} (𝐒b≤𝐒a) ⦄

-- Total division (Whole number division)
_/₀_ : (a : ℕ) → (b : ℕ) → ⦃ _ : (b ∣ a) ⦄ → ℕ
_/₀_ _ _ ⦃ div ⦄ = divides-quotient div

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:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category.Groupoid

module Categories.Category.Groupoid.Properties {o ℓ e} (G : Groupoid o ℓ e) where

import Categories.Morphism as Morphism
import Categories.Morphism.Properties as MorphismProps
import Categories.Morphism.Reasoning as MR

open Groupoid G
open Morphism category
open MorphismProps category
open HomReasoning
open MR category

private
  variable
    A B C : Obj

mono : {f : A ⇒ B} → Mono f
mono = Iso⇒Mono iso

epi : {f : A ⇒ B} → Epi f
epi = Iso⇒Epi iso

id-inverse : id {A = A} ⁻¹ ≈ id
id-inverse = ⟺ identityˡ ○ iso.isoʳ

⁻¹-involutive : {f : A ⇒ B} → f ⁻¹ ⁻¹ ≈ f
⁻¹-involutive {f = f} = begin
  f ⁻¹ ⁻¹            ≈⟨ introʳ iso.isoˡ ⟩
  f ⁻¹ ⁻¹ ∘ f ⁻¹ ∘ f ≈⟨ sym-assoc ○ elimˡ iso.isoˡ ⟩
                   f ∎

⁻¹-commute : {f : A ⇒ B} {g : C ⇒ A} → (f ∘ g) ⁻¹ ≈ g ⁻¹ ∘ f ⁻¹
⁻¹-commute {f = f} {g} = epi _ _ ( begin
  (f ∘ g) ⁻¹ ∘ f ∘ g    ≈⟨ iso.isoˡ ⟩
  id                    ≈˘⟨ iso.isoˡ ⟩
  g ⁻¹ ∘ g              ≈˘⟨ cancelInner iso.isoˡ ⟩
  (g ⁻¹ ∘ f ⁻¹) ∘ f ∘ g ∎ )

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module examplesPaperJFP.Coalgebra where

open import Size

F     :  Set → Set
mapF  :  ∀{A B} (f : A → B) → (F A → F B)

--- Dummy implementation to satisfy Agda's positivity checker.
F X       =  X
mapF f x  =  f x

S  :  Set
t  :  S → F S

data S′ : Set where

S = S′
t x = x

record νF : Set where
  coinductive
  field force : F νF

open νF using (force)

{-# TERMINATING #-}
unfoldF : ∀{S} (t : S → F S) → (S → νF)
force (unfoldF t s) = mapF (unfoldF t) (t s)


text:
------------------------------------------------------------------------
-- Semantics
------------------------------------------------------------------------

module RecursiveTypes.Semantics where

open import Codata.Musical.Notation

open import RecursiveTypes.Syntax
open import RecursiveTypes.Substitution

-- The semantics of a recursive type, i.e. its possibly infinite
-- unfolding.

⟦_⟧ : ∀ {n} → Ty n → Tree n
⟦ ⊥ ⟧       = ⊥
⟦ ⊤ ⟧       = ⊤
⟦ var x ⟧   = var x
⟦ σ ⟶ τ ⟧   = ♯ ⟦ σ ⟧         ⟶ ♯ ⟦ τ ⟧
⟦ μ σ ⟶ τ ⟧ = ♯ ⟦ σ [0≔ χ ] ⟧ ⟶ ♯ ⟦ τ [0≔ χ ] ⟧
              where χ = μ σ ⟶ τ

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
module iff-erasure where

open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Empty using (⊥-elim)
-- open import plfa.part1.Isomorphism using (_⇔_)
open import decidable using (Dec; yes; no; Bool; true; false; ⌊_⌋)

-- 同値 (equivalence)
record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
open _⇔_

-- 必要十分条件 (if and only if)
_iff_ : Bool → Bool → Bool
true  iff true  = true
true  iff false = false
false iff true  = false
false iff false = true

-- 同値のdecidable
_⇔-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⇔ B)
yes a ⇔-dec yes b = yes record { to = λ _ → b ; from = λ _ → a }
yes a ⇔-dec no ¬b = no λ a⇔b → ¬b (to a⇔b a)
no ¬a ⇔-dec yes b = no λ a⇔b → ¬a (from a⇔b b)
no ¬a ⇔-dec no ¬b = yes record { to = λ a → ⊥-elim (¬a a) ; from = λ b → ⊥-elim (¬b b) }

-- erasureを使うことで真偽値の必要十分条件とdecidableの同値が等しくなることの証明
iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
iff-⇔ (yes a) (yes b) = refl
iff-⇔ (yes a) (no b)  = refl
iff-⇔ (no a)  (yes b) = refl
iff-⇔ (no a)  (no b)  = refl

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
{-

The Inductive Version of James Construction

This file contains:
  - An inductive family 𝕁, and its direct colimit is equivalence to James;
    (KANG Rongji, Feb. 2022)
  - The family 𝕁 can be iteratively constructed as pushouts;
  - Special cases of 𝕁 n for n = 0, 1 and 2;
  - Connectivity of inclusion maps.

This file is the summary of the main results.
The proof is divided into parts and put inside the fold Cubical.HITs.James.Inductive

-}
{-# OPTIONS --safe #-}
module Cubical.HITs.James.Inductive where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Pointed

open import Cubical.Data.Nat
open import Cubical.Data.Unit
open import Cubical.Data.Sigma

open import Cubical.HITs.Wedge
open import Cubical.HITs.Pushout
open import Cubical.HITs.Pushout.PushoutProduct
open import Cubical.HITs.SequentialColimit

open import Cubical.HITs.James.Base
open import Cubical.HITs.James.Inductive.Base
open import Cubical.HITs.James.Inductive.PushoutFormula
  renaming (isConnectedIncl to connIncl ; isConnectedInl to connInl)
open import Cubical.HITs.James.Inductive.Reduced
open import Cubical.HITs.James.Inductive.ColimitEquivalence

open import Cubical.Homotopy.Connected

private
  variable
    ℓ : Level

module JamesInd
  (X∙@(X , x₀) : Pointed ℓ) where

  -- The family 𝕁 n is equivalence to Brunerie's J n, as will be shown latter.
  -- Instead of his inductive procedure, 𝕁 is defined directly as an indexed HIT.

  𝕁 : ℕ → Type ℓ
  𝕁 = 𝕁ames (X , x₀)

  -- This family forms a direct system.

  𝕁Seq : Sequence ℓ
  𝕁Seq = 𝕁amesSeq (X , x₀)

  -- The inductive construction of James is called 𝕁∞.
  -- It is the direct colimit of 𝕁 n.

  𝕁∞ : Type ℓ
  𝕁∞ = Lim→ 𝕁Seq

  -- And of course it is equivalent to James.

  J≃𝕁∞ : James (X , x₀) ≃ 𝕁∞
  J≃𝕁∞ = compEquiv (James≃𝕁Red∞ _) (invEquiv (𝕁ames∞≃𝕁Red∞ _))

  -- Special cases of 𝕁 n for n = 0, 1 and 2:

  𝕁₀≃Unit : 𝕁 0 ≃ Unit
  𝕁₀≃Unit = 𝕁ames0≃ _

  𝕁₁≃X : 𝕁 1 ≃ X
  𝕁₁≃X = 𝕁ames1≃ _

  𝕁₂≃P[X×X←X⋁X→X] : 𝕁 2 ≃ Pushout ⋁↪ fold⋁
  𝕁₂≃P[X×X←X⋁X→X] = 𝕁ames2≃ _

  -- The following is defined as pushouts of 𝕁 n.

  𝕁Push : ℕ → Type ℓ
  𝕁Push = 𝕁amesPush (X , x₀)

  -- Brunerie uses f and g to denote the following maps, so do I.

  module _
    {n : ℕ} where

    f : 𝕁Push n → X × 𝕁 (1 + n)
    f = leftMap _

    g : 𝕁Push n → 𝕁 (1 + n)
    g = rightMap _

  -- Here we show that 𝕁 (n+2) can be made as double pushouts invoving only X, 𝕁 n and 𝕁 (n+1).
  -- In particular, our 𝕁 is exactly what Brunerie had defined.

  𝕁ₙ₊₂≃Pushout : (n : ℕ) → 𝕁 (2 + n) ≃ Pushout f g
  𝕁ₙ₊₂≃Pushout = 𝕁ames2+n≃ _

  -- Connectivity of inclusion maps:

  module _
    (d : ℕ)(conn : isConnected (1 + d) X) where

    -- Warning:
    -- The connectivity is shifted by 2 from the convention of usual homotopy theory.

    -- If X is (d+1)-connected, the transition incl : 𝕁 n → 𝕁 (n+1) will be (n+1)d-connected.

    isConnectedIncl : (n : ℕ) → isConnectedFun ((1 + n) · d) (incl {n = n})
    isConnectedIncl = connIncl X∙ d conn

    -- If X is (d+1)-connected, the inclusion inl : 𝕁 n → 𝕁∞ will be (n+1)d-connected.

    inl∞ : (n : ℕ) → 𝕁 n → 𝕁∞
    inl∞ _ = inl

    isConnectedInl : (n : ℕ) → isConnectedFun ((1 + n) · d) (inl∞ n)
    isConnectedInl = connInl X∙ d conn

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


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

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive
open import Agda.Primitive.Cubical

variable
  a p         : Level
  A           : Set a
  P           : A → Set p
  eq₁ u v x y : A

refl : x ≡ x
refl {x = x} = λ _ → x

subst : (P : A → Set p) → x ≡ y → P x → P y
subst P x≡y p = primTransp (λ i → P (x≡y i)) i0 p

hcong :
  (f : (x : A) → P x) (x≡y : x ≡ y) →
  PathP (λ i → P (x≡y i)) (f x) (f y)
hcong f x≡y = λ i → f (x≡y i)

dcong :
  (f : (x : A) → P x) (x≡y : x ≡ y) →
  subst P x≡y (f x) ≡ f y
dcong {P = P} f x≡y = λ i →
  primTransp (λ j → P (x≡y (primIMax i j))) i (f (x≡y i))

-- This lemma is due to Anders Mörtberg.

lemma₁ :
  {P : I → Set p} {p : P i0} {q : P i1} →
  PathP P p q ≡ (primTransp P i0 p ≡ q)
lemma₁ {P = P} {p = p} {q = q} = λ i →
  PathP
    (λ j → P (primIMax i j))
    (primTransp (λ j → P (primIMin i j)) (primINeg i) p)
    q

data 𝕊¹ : Set where
  base : 𝕊¹
  loop : base ≡ base

postulate

  Q : 𝕊¹ → Set
  b : Q base
  ℓ : subst Q loop b ≡ b

lemma₂ :
  {eq : x ≡ y} →
  subst Q eq u ≡ v →
  PathP (λ i → Q (eq i)) u v
lemma₂ = subst (λ A → A → PathP _ _ _) lemma₁ (λ x → x)

lemma₃ : (x : 𝕊¹) → Q x
lemma₃ base     = b
lemma₃ (loop i) = lemma₂ ℓ i

postulate

  lemma₄ :
    (eq₂ : subst Q eq₁ (lemma₃ x) ≡ lemma₃ y) →
    hcong lemma₃ eq₁ ≡ lemma₂ eq₂ →
    dcong lemma₃ eq₁ ≡ eq₂

works : dcong lemma₃ loop ≡ ℓ
works = lemma₄ ℓ refl

-- "injectivity" of lemma₃ was the problem
should-work-too : dcong lemma₃ loop ≡ ℓ
should-work-too = lemma₄ _ refl

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
module _ where

postulate
  C : Set → Set
  A : Set
  i : C A
  foo : {X : Set} {{_ : C X}} → X

bar : A
bar = let instance z = i in foo


text:
-- By default both sized types and constructor-based guardedness are
-- available.

open import Agda.Builtin.Size

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A

open Stream

repeat : ∀ {A} → A → Stream A
repeat x .head = x
repeat x .tail = repeat x

record Sized-stream (A : Set) (i : Size) : Set where
  coinductive
  field
    head : A
    tail : {j : Size< i} → Sized-stream A j

open Sized-stream

postulate
  destroy-guardedness : {A : Set} → A → A

repeat-sized : ∀ {A i} → A → Sized-stream A i
repeat-sized x .head = x
repeat-sized x .tail = destroy-guardedness (repeat-sized x)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.Polynomials.Multivariate.Equiv.Poly0-A where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism

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

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

open import Cubical.Algebra.Polynomials.Univariate.Base

open import Cubical.Algebra.Polynomials.Multivariate.Base
open import Cubical.Algebra.Polynomials.Multivariate.Properties
open import Cubical.Algebra.CommRing.Instances.MultivariatePoly

private variable
  ℓ : Level

module Equiv-Poly0-A (A' : CommRing ℓ) where
  A = fst A'
  cra = snd A'

  open CommRingStr cra renaming (is-set to isSetA)
  open Nth-Poly-structure A' 0

-----------------------------------------------------------------------------
-- Equivalence

  Poly0→A : Poly A' 0 → A
  Poly0→A = Poly-Rec-Set.f A' 0 A isSetA
             0r
             (λ v a → a)
             _+_
             +Assoc
             +Rid
             +Comm
             (λ _ → refl)
             λ _ a b → refl

  A→Poly0 : A → Poly A' 0
  A→Poly0 a = base [] a

  e-sect : (a : A) → Poly0→A (A→Poly0 a) ≡ a
  e-sect a = refl

  e-retr : (P : Poly A' 0) → A→Poly0 (Poly0→A P) ≡ P
  e-retr = Poly-Ind-Prop.f A' 0
           (λ P → A→Poly0 (Poly0→A P) ≡ P)
           (λ _ → trunc _ _)
           (base-0P [])
           (λ { [] a → refl })
           λ {U V} ind-U ind-V → (sym (base-Poly+ [] (Poly0→A U) (Poly0→A V))) ∙ (cong₂ _Poly+_ ind-U ind-V)

-----------------------------------------------------------------------------
-- Ring homomorphism

  map-0P : Poly0→A 0P ≡ 0r
  map-0P = refl

  Poly0→A-gmorph : (P Q : Poly A' 0) → Poly0→A ( P Poly+ Q) ≡ Poly0→A P + Poly0→A Q
  Poly0→A-gmorph P Q = refl

  map-1P : Poly0→A 1P ≡ 1r
  map-1P = refl

  Poly0→A-rmorph : (P Q : Poly A' 0) → Poly0→A ( P Poly* Q) ≡ Poly0→A P · Poly0→A Q
  Poly0→A-rmorph = Poly-Ind-Prop.f A' 0
                    (λ P → (Q : Poly A' 0) → Poly0→A (P Poly* Q) ≡ Poly0→A P · Poly0→A Q)
                    (λ P p q i Q j → isSetA (Poly0→A (P Poly* Q)) (Poly0→A P · Poly0→A Q) (p Q) (q Q) i j)
                    (λ Q → sym (RingTheory.0LeftAnnihilates (CommRing→Ring A') (Poly0→A Q)))
                    (λ v a → Poly-Ind-Prop.f A' 0
                              (λ P → Poly0→A (base v a Poly* P) ≡ Poly0→A (base v a) · Poly0→A P)
                              (λ _ → isSetA _ _)
                              (sym (RingTheory.0RightAnnihilates (CommRing→Ring A') (Poly0→A (base v a))))
                              (λ v' a' → refl)
                              λ {U V} ind-U ind-V → (cong₂ _+_ ind-U ind-V) ∙ (sym (·Rdist+ _ _ _)))
                    λ {U V} ind-U ind-V Q → (cong₂ _+_ (ind-U Q) (ind-V Q)) ∙ (sym (·Ldist+ _ _ _))

-----------------------------------------------------------------------------
-- Ring Equivalence

module _ (A' : CommRing ℓ) where

  open Equiv-Poly0-A A'

  CRE-Poly0-A : CommRingEquiv (PolyCommRing A' 0) A'
  fst CRE-Poly0-A = isoToEquiv is
    where
    is : Iso (Poly A' 0) (A' .fst)
    Iso.fun is = Poly0→A
    Iso.inv is = A→Poly0
    Iso.rightInv is = e-sect
    Iso.leftInv is = e-retr
  snd CRE-Poly0-A = makeIsRingHom map-1P Poly0→A-gmorph Poly0→A-rmorph

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.Relation.Everything where

open import Cubical.Relation.Nullary public
open import Cubical.Relation.Nullary.DecidableEq public
open import Cubical.Relation.Binary public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text: open import Issue2229Base public


text:
-- Andreas, 2019-08-08, issue #3962 reported (+ test case) by guillaumebrunerie

-- Don't lex "{{" as instance braces if followed by "-", as this will confuse Emacs.
-- Rather lex "{{-" as "{" "{-".

postulate
  A : Set
  f : {{_ : A}} → Set
  -x : A

B : Set
B = f {{-x}}

C : Set
C = ?

-- WAS: passes parser but confuses emacs, which treats everything following {- as comment.

-- Expected error: Unterminated '{-'


text:
module Numeral.Finite.Oper.Comparisons where

import      Lvl
open import Data.Boolean
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Programming
open import Functional
open import Numeral.Finite
open import Numeral.Sign

-- Compare
_⋚?_ : ∀{a b} → 𝕟(a) → 𝕟(b) → (−|0|+)
𝟎    ⋚? 𝟎    = 𝟎
𝟎    ⋚? 𝐒(b) = ➖
𝐒(a) ⋚? 𝟎    = ➕
𝐒(a) ⋚? 𝐒(b) = a ⋚? b

-- Equality check
_≡?_ : ∀{a b} → 𝕟(a) → 𝕟(b) → Bool
_≡?_ = elim₃ 𝐹 𝑇 𝐹 ∘₂ (_⋚?_)

-- Non-equality check
_≢?_ : ∀{a b} → 𝕟(a) → 𝕟(b) → Bool
_≢?_ = elim₃ 𝑇 𝐹 𝑇 ∘₂ (_⋚?_)

-- Lesser-than check
_<?_ : ∀{a b} → 𝕟(a) → 𝕟(b) → Bool
_<?_ = elim₃ 𝑇 𝐹 𝐹 ∘₂ (_⋚?_)

-- Lesser-than or equals check
_≤?_ : ∀{a b} → 𝕟(a) → 𝕟(b) → Bool
_≤?_ = elim₃ 𝑇 𝑇 𝐹 ∘₂ (_⋚?_)

-- Greater-than check
_>?_ : ∀{a b} → 𝕟(a) → 𝕟(b) → Bool
_>?_ = elim₃ 𝐹 𝐹 𝑇 ∘₂ (_⋚?_)

-- Greater-than or equals check
_≥?_ : ∀{a b} → 𝕟(a) → 𝕟(b) → Bool
_≥?_ = elim₃ 𝐹 𝑇 𝑇 ∘₂ (_⋚?_)


text:
{-# OPTIONS --without-K #-}
module Universe.Utility.General where

open import lib.Basics
open import lib.NType2

open import lib.types.Nat hiding (_+_)
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Unit

-- A readable notation for the join of universe levels.
infixr 8  _⊔_

_⊔_ : ULevel → ULevel → ULevel
_⊔_ = lmax

-- Important detail: addition operator adjustment.
_+_ : ℕ → ℕ → ℕ
a + b = b lib.types.Nat.+ a  -- n + 1 should mean S n (author preference)!

{- Since natural numbers and universe levels use
   different types, we require a translation operation. -}
｢_｣ : ℕ → ULevel
｢ 0   ｣ = lzero
｢ S n ｣ = lsucc ｢ n ｣

{- The (function) exponentiation operator. For convenience, we
   choose to define it via postcomposition in the recursion step. -}
infix 10 _^_

_^_ : ∀ {i} {A : Set i} → (A → A) → ℕ → A → A
f ^ 0   = idf _
f ^ S n = f ^ n ∘ f

{- The rest of this file contains the remainder of the library type material
   that could not yet be merged into the community's HoTT library due to
   organizational issues. -}

module _ {i j} {A : Type i} {B : A → Type j} where
  module _ (h : is-contr A) where
    Π₁-contr : Π A B ≃ B (fst h)
    Π₁-contr = Π₁-Unit ∘e equiv-Π-l _ (snd (contr-equiv-Unit h ⁻¹)) ⁻¹

    Σ₁-contr : Σ A B ≃ B (fst h)
    Σ₁-contr = Σ₁-Unit ∘e equiv-Σ-fst _ (snd (contr-equiv-Unit h ⁻¹)) ⁻¹

  module _ (h : (a : A) → is-contr (B a)) where
    Σ₂-contr : Σ A B ≃ A
    Σ₂-contr = Σ₂-Unit ∘e equiv-Σ-snd (λ _ → contr-equiv-Unit (h _))

    Π₂-contr : Π A B ≃ ⊤
    Π₂-contr = Π₂-Unit ∘e equiv-Π-r (λ _ → contr-equiv-Unit (h _))

×-comm : ∀ {i j} {A : Type i} {B : Type j} → (A × B) ≃ (B × A)
×-comm = equiv (λ {(a , b) → (b , a)})
               (λ {(b , a) → (a , b)})
               (λ _ → idp) (λ _ → idp)

Σ-comm-snd : ∀ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k}
           → Σ (Σ A B) (λ ab → C (fst ab)) ≃ Σ (Σ A C) (λ ac → B (fst ac))
Σ-comm-snd {A = A} {B} {C} =
  Σ (Σ A B) (λ ab → C (fst ab))  ≃⟨ Σ-assoc ⟩
  Σ A (λ a → B a × C a)          ≃⟨ equiv-Σ-snd (λ _ → ×-comm) ⟩
  Σ A (λ a → C a × B a)          ≃⟨ Σ-assoc ⁻¹ ⟩
  Σ (Σ A C) (λ ac → B (fst ac))  ≃∎

flip : ∀ {i j k} {A : Type i} {B : Type j} {C : A → B → Type k}
       → ((a : A) (b : B) → C a b) → ((b : B) (a : A) → C a b)
flip = –> (curry-equiv ∘e equiv-Π-l _ (snd ×-comm) ∘e curry-equiv ⁻¹)

module _ {i j k} {A : Type i} {B : Type j} {C : A → B → Type k} where
  ↓-cst→app-equiv : {x x' : A} {p : x == x'} {u : (b : B) → C x b} {u' : (b : B) → C x' b}
                  → ((b : B) → u b == u' b [ (λ x → C x b) ↓ p ]) ≃ (u == u' [ (λ x → (b : B) → C x b) ↓ p ])
  ↓-cst→app-equiv {p = idp} = equiv λ= app= (! ∘ λ=-η) (λ= ∘ app=-β)

module _ {i j k} {A : Type i} {B : A → Type j} {C : A → Type k} where
  ↓-cst2-equiv : {x y : A} (p : x == y) {b : C x} {c : C y}
    (q : b == c [ C ↓ p ]) {u : B x} {v : B y}
    → (u == v [ B ↓ p ]) ≃ (u == v [ (λ xy → B (fst xy)) ↓ (pair= p q) ])
  ↓-cst2-equiv idp idp = ide _

module _ {i} {A B : Type i} (e : A ≃ B) {u : A} {v : B} where
  ↓-idf-ua-equiv : (–> e u == v) ≃ (u == v [ (λ x → x) ↓ (ua e) ])
  ↓-idf-ua-equiv = to-transp-equiv _ _ ⁻¹ ∘e (_ , pre∙-is-equiv (ap (λ z → z u) (ap coe (ap-idf (ua e)) ∙ ap –> (coe-equiv-β e))))

-- On propositions, equivalence coincides with logical equivalence.
module _ {i j} {A : Type i} {B : Type j} where
  prop-equiv' : (B → is-prop A) → (A → is-prop B) → (A → B) → (B → A) → A ≃ B
  prop-equiv' h k f g = equiv f g (λ b → prop-has-all-paths (k (g b)) _ _)
                                  (λ a → prop-has-all-paths (h (f a)) _ _)

  prop-equiv : is-prop A → is-prop B → (A → B) → (B → A) → A ≃ B
  prop-equiv h k f g = prop-equiv' (cst h) (cst k) f g

-- Equivalent types have equivalent truncatedness propositions.
equiv-level : ∀ {i j} {A : Type i} {B : Type j} {n : ℕ₋₂}
            → A ≃ B → has-level n A ≃ has-level n B
equiv-level u = prop-equiv has-level-is-prop
                           has-level-is-prop
                           (equiv-preserves-level u)
                           (equiv-preserves-level (u ⁻¹))

prop-equiv-inhab-to-contr : ∀ {i} {A : Type i} → is-prop A ≃ (A → is-contr A)
prop-equiv-inhab-to-contr = prop-equiv is-prop-is-prop
                                       (Π-level (λ _ → is-contr-is-prop))
                                       (flip inhab-prop-is-contr)
                                       inhab-to-contr-is-prop

max_stars_repo_name: sattlerc/HoTT-Agda

max_issues_repo_name: sattlerc/HoTT-Agda

max_forks_repo_name: sattlerc/HoTT-Agda


text:
module Data.ByteString.Utf8 where

open import Data.ByteString.Primitive
open import Data.String using (String)

{-# FOREIGN GHC import qualified Data.ByteString #-}
{-# FOREIGN GHC import qualified Data.Text.Encoding #-}
postulate
  packStrict : String → ByteStringStrict
  unpackStrict : ByteStringStrict → String
{-# COMPILE GHC packStrict = (Data.Text.Encoding.encodeUtf8) #-}
{-# COMPILE GHC unpackStrict = (Data.Text.Encoding.decodeUtf8) #-}

max_stars_repo_name: semenov-vladyslav/bytes-agda

max_issues_repo_name: semenov-vladyslav/bytes-agda

max_forks_repo_name: semenov-vladyslav/bytes-agda


text:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

{-# OPTIONS --sized-types --guardedness #-}

open import Agda.Builtin.Equality
open import Data.Product
open import Data.Sum
open import Data.Empty
open import Data.Unit
open import Level
open import Size
open import Codata.Thunk
open import Relation.Unary using (_⊆_)
open import Data.Container.Indexed

module is-lib.InfSys.Container {𝓁}(U : Set 𝓁) where

    module ISCont {𝓁p} where

        ISCont : {𝓁c : Level} → Set _
        ISCont {𝓁c} = Container U U 𝓁c 𝓁p

        ISContClosed : ∀{𝓁c 𝓁'}(is : ISCont {𝓁c}) → (U → Set 𝓁') → Set _
        ISContClosed is P = (⟦ is ⟧ P ⊆ P)

        _↾_ : ∀{𝓁c 𝓁'} → ISCont {𝓁c} → (U → Set 𝓁') → ISCont {𝓁c ⊔ 𝓁'}
        (is ↾ P) .Command  u       = is .Command u × P u
        (is ↾ P) .Response (c , p) = is .Response c
        (is ↾ P) .next (c , p) r   = is .next c r

        _∪_ : ∀{𝓁c 𝓁c'} → ISCont {𝓁c} → ISCont {𝓁c'} → ISCont {𝓁c ⊔ 𝓁c'}
        (is ∪ is') .Command  u = is .Command u  ⊎ is' .Command u
        (is ∪ is') .Response   = [ is .Response , is' .Response ]
        (is ∪ is') .next       = [ is .next     , is' .next     ]

        Ind⟦_⟧ = μ

        -- Coinductive interpretation

        record CoInd⟦_⟧ {𝓁c : Level}(is : ISCont {𝓁c}) (u : U) : Set (𝓁c ⊔ 𝓁p) where
            coinductive
            constructor cofold_
            field
                unfold : ⟦ is ⟧ CoInd⟦ is ⟧ u

        -- Sized coinductive interpretation

        record CoInd⟦_⟧^ {𝓁c : Level}(is : ISCont {𝓁c}) (i : Size) (u : U) : Set (𝓁c ⊔ 𝓁p) where
            coinductive
            constructor cofold_
            field
                unfold : {j : Size< i} → ⟦ is ⟧ (CoInd⟦ is ⟧^ j) u

        -- Sized coinductive interpretation (using Thunk)

        data SCoInd⟦_⟧ {𝓁c : Level}(is : ISCont {𝓁c}) (u : U) (i : Size) : Set (𝓁c ⊔ 𝓁p) where
            sfold : ⟦ is ⟧ (λ u → Thunk (SCoInd⟦ is ⟧ u) i) u → SCoInd⟦ is ⟧ u i

        FCoInd⟦_,_⟧ : ∀{𝓁c 𝓁c'} → (I : ISCont {𝓁c}) (C : ISCont {𝓁c'}) → U → Set _
        FCoInd⟦ I , C ⟧ = CoInd⟦ I ↾ Ind⟦ I ∪ C ⟧ ⟧

        module _ {𝓁c 𝓁'} (is : ISCont {𝓁c}) (P : U → Set 𝓁') (closed : ISContClosed is P) where

            open import Data.W.Indexed using (iter)

            ind[_] : Ind⟦ is ⟧ ⊆ P
            ind[_] = iter is closed

        module _ {𝓁c 𝓁'} (is : ISCont {𝓁c}) (P : U → Set 𝓁') (consistent : P ⊆ ⟦ is ⟧ P) where

            open CoInd⟦_⟧

            coind[] : P ⊆ CoInd⟦ is ⟧
            coind[] p .unfold .proj₁ = consistent p .proj₁
            coind[] p .unfold .proj₂ r = coind[] (consistent p .proj₂ r)

        module _ {𝓁c 𝓁c' 𝓁'}(I : ISCont {𝓁c}) (C : ISCont {𝓁c'}) (P : U → Set 𝓁') (bounded : P ⊆ Ind⟦ I ∪ C ⟧) (consistent : P ⊆ ⟦ I ⟧ P) where

            open CoInd⟦_⟧

            bounded-coind[] : P ⊆ FCoInd⟦ I , C ⟧
            bounded-coind[] p .unfold .proj₁ .proj₁ = consistent p .proj₁
            bounded-coind[] p .unfold .proj₁ .proj₂ = bounded p
            bounded-coind[] p .unfold .proj₂ r      = bounded-coind[] (consistent p .proj₂ r)

    module Equivalence {𝓁p 𝓁P 𝓁P'} where

        open ISCont {𝓁p}
        open import is-lib.InfSys.Base {𝓁} as IS
        open IS.MetaRule
        open IS.IS

        {- Every IS is an EndoContainer -}

        C[_] : ∀{𝓁c 𝓁n} → IS {𝓁c} {𝓁p} {𝓁n} U → ISCont {𝓁 ⊔ 𝓁c ⊔ 𝓁n}
        C[ is ] .Command u = Σ[ rn ∈ is .Names ] Σ[ c ∈ is .rules rn .Ctx ] u ≡ is .rules rn .conclu c
        C[ is ] .Response (rn , c , refl) = is .rules rn .Pos c
        C[ is ] .next (rn , c , refl) r = is .rules rn .prems c r

        {- Every EndoContainer is an IS -}

        IS[_] : ∀{𝓁'} → ISCont {𝓁'} → IS {zero} {𝓁p} {𝓁 ⊔ 𝓁'} U
        IS[_] C .Names = Σ[ u ∈ U ] C .Command u
        IS[ C ] .rules (u , c) =
            record {
                Ctx = ⊤ ;
                Pos = λ _ → C .Response c ;
                prems = λ _ r → C .next c r ;
                conclu = λ _ → u }

        {- Equivalence -}

        isf-to-c : ∀{𝓁c 𝓁n} → {is : IS {𝓁c} {𝓁p} {𝓁n} U}{P : U → Set 𝓁P}
            → ISF[ is ] P ⊆ ⟦ C[ is ] ⟧ P
        isf-to-c (rn , c , refl , pr) = (rn , c , refl) , pr

        c-to-isf : ∀{𝓁'}{C : ISCont {𝓁'}}{P : U → Set 𝓁P}
            → ⟦ C ⟧ P ⊆ ISF[ IS[ C ] ] P
        c-to-isf (c , pr) = (_ , c) , tt , refl , pr

        ∪-IS-eq : ∀{𝓁c 𝓁n 𝓁n'}{is : IS {𝓁c} {𝓁p} {𝓁n} U}{is' : IS {𝓁c} {𝓁p} {𝓁n'} U}{P : U → Set 𝓁P}
            → ISF[ is IS.∪ is' ] P ⊆ ⟦ C[ is ] ISCont.∪ C[ is' ] ⟧ P
        ∪-IS-eq (inj₁ rn , c , refl , pr) = inj₁ (rn , c , refl) , pr
        ∪-IS-eq (inj₂ rn , c , refl , pr) = inj₂ (rn , c , refl) , pr

        ∪-C-eq : ∀{𝓁1 𝓁2}{c : ISCont {𝓁1}}{c' : ISCont {𝓁2}}{P : U → Set 𝓁P}
            → ⟦ c ISCont.∪ c' ⟧ P ⊆ ISF[ IS[ c ] IS.∪ IS[ c' ] ] P
        ∪-C-eq (inj₁ c , r) = inj₁ (_ , c) , tt , refl , r
        ∪-C-eq (inj₂ c , r) = inj₂ (_ , c) , tt , refl , r

        ⊓-IS-eq : ∀{𝓁c 𝓁n}{is : IS {𝓁c} {𝓁p} {𝓁n} U}{P : U → Set 𝓁P}{P' : U → Set 𝓁P'}
            → ISF[ is ⊓ P ] P' ⊆ ⟦ C[ is ] ↾ P ⟧ P'
        ⊓-IS-eq (rn , (c , Pu) , refl , pr) = ((rn , c , refl) , Pu) , pr

        ↾-C-eq : ∀{𝓁c}{c : ISCont {𝓁c}}{P : U → Set 𝓁P}{P' : U → Set 𝓁P'}
            → ⟦ c ↾ P ⟧ P' ⊆ ISF[ IS[ c ] ⊓ P ] P'
        ↾-C-eq ((c , Pu) , r) = (_ , c) , (tt , Pu) , refl , r

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
?bug : Set
?bug = ?

-- Andreas, 2014-04-16
-- Issue 1104 reported by Fabien Renaud.
-- Emacs mode got confused by identifiers containing --

-- Problem: {!!} is not turned into hole

bug-- : Set
bug-- = ?

another : Set
another = (-- Senfgurke ?
           {!!})-- Noch eine Senfgurke ?

_:--_ : Set → Set → Set
_:--_ = {!!}

bla = let x = Set ;-- bla ?
                   y = Set in  Set

bug? : Set
bug? = {!!}


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

module hott.topology.loopspace where

open import hott.core
open import hott.types
open import hott.functions

-- The pointed loop space

Ω∙ : ∀{ℓ} → Type● ℓ → Type● ℓ
Ω∙ (A , a) = (a ≡ a , refl)

-- The loops space. It is obtained by suppressing the base point of
-- the corresponding pointed loop space.
Ω : ∀{ℓ} → Type● ℓ → Type ℓ
Ω = space ∘ Ω∙

--

-- The iterated pointed loop space

Ω̂∙ : ∀{ℓ}  → ℕ → Type● ℓ → Type● ℓ
Ω̂∙ = iterate Ω∙

-- The iterated loop space. It is obtained by suppressing the base
-- point of the iterated pointed loop space.

Ω̂ : ∀{ℓ}  → ℕ → Type● ℓ → Type ℓ
Ω̂ n = space ∘ Ω̂∙ n

-- Some short hands

Ω²∙ : ∀{ℓ} → Type● ℓ → Type● ℓ; Ω²∙ = Ω̂∙ 2
Ω³∙ : ∀{ℓ} → Type● ℓ → Type● ℓ; Ω³∙ = Ω̂∙ 3
Ω⁴∙ : ∀{ℓ} → Type● ℓ → Type● ℓ; Ω⁴∙ = Ω̂∙ 4
Ω⁵∙ : ∀{ℓ} → Type● ℓ → Type● ℓ; Ω⁵∙ = Ω̂∙ 5
Ω⁶∙ : ∀{ℓ} → Type● ℓ → Type● ℓ; Ω⁶∙ = Ω̂∙ 6
Ω⁷∙ : ∀{ℓ} → Type● ℓ → Type● ℓ; Ω⁷∙ = Ω̂∙ 7
Ω⁸∙ : ∀{ℓ} → Type● ℓ → Type● ℓ; Ω⁸∙ = Ω̂∙ 8
Ω⁹∙ : ∀{ℓ} → Type● ℓ → Type● ℓ; Ω⁹∙ = Ω̂∙ 9

Ω² : ∀{ℓ} → Type● ℓ → Type ℓ; Ω² = Ω̂ 2
Ω³ : ∀{ℓ} → Type● ℓ → Type ℓ; Ω³ = Ω̂ 3
Ω⁴ : ∀{ℓ} → Type● ℓ → Type ℓ; Ω⁴ = Ω̂ 4
Ω⁵ : ∀{ℓ} → Type● ℓ → Type ℓ; Ω⁵ = Ω̂ 5
Ω⁶ : ∀{ℓ} → Type● ℓ → Type ℓ; Ω⁶ = Ω̂ 6
Ω⁷ : ∀{ℓ} → Type● ℓ → Type ℓ; Ω⁷ = Ω̂ 7
Ω⁸ : ∀{ℓ} → Type● ℓ → Type ℓ; Ω⁸ = Ω̂ 8
Ω⁹ : ∀{ℓ} → Type● ℓ → Type ℓ; Ω⁹ = Ω̂ 9

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}

open import Cubical.Core.Everything
open import Cubical.Foundations.HLevels

module Cubical.Algebra.Group.Construct.Free {ℓ} (Aˢ : hSet ℓ) where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Path
open import Cubical.Algebra.Group

open import Cubical.Data.Empty.Polymorphic
open import Cubical.Data.Prod

open import Cubical.Relation.Binary.Reasoning.Equality

A = ⟨ Aˢ ⟩
isSetA = Aˢ .snd

data FreeG : Type ℓ where
  inj : A → FreeG
  _•_ : Op₂ FreeG
  ε   : FreeG
  _⁻¹ : Op₁ FreeG

  •-assoc     : Associative _•_
  •-identityˡ : LeftIdentity ε _•_
  •-identityʳ : RightIdentity ε _•_
  •-inverseˡ  : LeftInverse ε _⁻¹ _•_
  •-inverseʳ  : RightInverse ε _⁻¹ _•_

  squash : isSet FreeG

•-identity : Identity ε _•_
•-identity = •-identityˡ , •-identityʳ

•-inverse : Inverse ε _⁻¹ _•_
•-inverse = •-inverseˡ , •-inverseʳ

elim : ∀ {ℓ′} {B : FreeG → Type ℓ′} →
        (∀ x → isSet (B x)) →
        (∀ x → B (inj x)) →
        (op : ∀ {x y} → B x → B y → B (x • y)) →
        (e : B ε) →
        (inv : ∀ {x} → B x → B (x ⁻¹)) →
        (∀ {x y z} (a : B x) (b : B y) (c : B z) → PathP (λ i → B (•-assoc x y z i)) (op (op a b) c) (op a (op b c))) →
        (∀ {x} (a : B x) → PathP (λ i → B (•-identityˡ x i)) (op e a) a) →
        (∀ {x} (a : B x) → PathP (λ i → B (•-identityʳ x i)) (op a e) a) →
        (∀ {x} (a : B x) → PathP (λ i → B (•-inverseˡ x i)) (op (inv a) a) e) →
        (∀ {x} (a : B x) → PathP (λ i → B (•-inverseʳ x i)) (op a (inv a)) e) →
        (x : FreeG) → B x
elim isSetB f op e inv assc idˡ idʳ invˡ invʳ (inj x) = f x
elim isSetB f op e inv assc idˡ idʳ invˡ invʳ (x • y) = op (elim isSetB f op e inv assc idˡ idʳ invˡ invʳ x)
                                                            (elim isSetB f op e inv assc idˡ idʳ invˡ invʳ y)
elim isSetB f op e inv assc idˡ idʳ invˡ invʳ ε = e
elim isSetB f op e inv assc idˡ idʳ invˡ invʳ (x ⁻¹) = inv (elim isSetB f op e inv assc idˡ idʳ invˡ invʳ x)
elim isSetB f op e inv assc idˡ idʳ invˡ invʳ (•-assoc x y z i) = assc (elim isSetB f op e inv assc idˡ idʳ invˡ invʳ x)
                                                                        (elim isSetB f op e inv assc idˡ idʳ invˡ invʳ y)
                                                                        (elim isSetB f op e inv assc idˡ idʳ invˡ invʳ z) i
elim isSetB f op e inv assc idˡ idʳ invˡ invʳ (•-identityˡ x i) = idˡ (elim isSetB f op e inv assc idˡ idʳ invˡ invʳ x) i
elim isSetB f op e inv assc idˡ idʳ invˡ invʳ (•-identityʳ x i) = idʳ (elim isSetB f op e inv assc idˡ idʳ invˡ invʳ x) i
elim isSetB f op e inv assc idˡ idʳ invˡ invʳ (•-inverseˡ x i) = invˡ (elim isSetB f op e inv assc idˡ idʳ invˡ invʳ x) i
elim isSetB f op e inv assc idˡ idʳ invˡ invʳ (•-inverseʳ x i) = invʳ (elim isSetB f op e inv assc idˡ idʳ invˡ invʳ x) i
elim isSetB f op e inv assc idˡ idʳ invˡ invʳ (squash x y p q i j) =
  isOfHLevel→isOfHLevelDep 2 isSetB
    (elim isSetB f op e inv assc idˡ idʳ invˡ invʳ x) (elim isSetB f op e inv assc idˡ idʳ invˡ invʳ y)
    (cong (elim isSetB f op e inv assc idˡ idʳ invˡ invʳ) p) (cong (elim isSetB f op e inv assc idˡ idʳ invˡ invʳ) q) (squash x y p q) i j

FreeG-isGroup : IsGroup FreeG _•_ ε _⁻¹
FreeG-isGroup = record
  { isMonoid = record
      { isSemigroup = record
          { isMagma = record { is-set = squash }
          ; assoc   = •-assoc
          }
      ; identity    = •-identity
      }
  ; inverse  = •-inverse
  }

FreeGroup : Group ℓ
FreeGroup = record { isGroup = FreeG-isGroup }


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

module n2o.Network.Http where


text:
{-
This second-order term syntax was created from the following second-order syntax description:

syntax PDiff | PD

type
  * : 0-ary

term
  zero  : * | 𝟘
  add   : *  *  ->  * | _⊕_ l20
  one   : * | 𝟙
  mult  : *  *  ->  * | _⊗_ l20
  neg   : *  ->  * | ⊖_ r50
  pd : *.*  *  ->  * | ∂_∣_

theory
  (𝟘U⊕ᴸ) a |> add (zero, a) = a
  (𝟘U⊕ᴿ) a |> add (a, zero) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊕C) a b |> add(a, b) = add(b, a)
  (𝟙U⊗ᴸ) a |> mult (one, a) = a
  (𝟙U⊗ᴿ) a |> mult (a, one) = a
  (⊗A) a b c |> mult (mult(a, b), c) = mult (a, mult(b, c))
  (⊗D⊕ᴸ) a b c |> mult (a, add (b, c)) = add (mult(a, b), mult(a, c))
  (⊗D⊕ᴿ) a b c |> mult (add (a, b), c) = add (mult(a, c), mult(b, c))
  (𝟘X⊗ᴸ) a |> mult (zero, a) = zero
  (𝟘X⊗ᴿ) a |> mult (a, zero) = zero
  (⊖N⊕ᴸ) a |> add (neg (a), a) = zero
  (⊖N⊕ᴿ) a |> add (a, neg (a)) = zero
  (⊗C) a b |> mult(a, b) = mult(b, a)
  (∂⊕) a : * |> x : * |- d0 (add (x, a)) = one
  (∂⊗) a : * |> x : * |- d0 (mult(a, x)) = a
  (∂C) f : (*,*).* |> x : *  y : * |- d1 (d0 (f[x,y])) = d0 (d1 (f[x,y]))
  (∂Ch₂) f : (*,*).*  g h : *.* |> x : * |- d0 (f[g[x], h[x]]) = add (mult(pd(z. f[z, h[x]], g[x]), d0(g[x])), mult(pd(z. f[g[x], z], h[x]), d0(h[x])))
  (∂Ch₁) f g : *.* |> x : * |- d0 (f[g[x]]) = mult (pd (z. f[z], g[x]), d0(g[x]))
-}

module PDiff.Syntax where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive

open import SOAS.Metatheory.Syntax

open import PDiff.Signature

private
  variable
    Γ Δ Π : Ctx
    α : *T
    𝔛 : Familyₛ

-- Inductive term declaration
module PD:Terms (𝔛 : Familyₛ) where

  data PD : Familyₛ where
    var  : ℐ ⇾̣ PD
    mvar : 𝔛 α Π → Sub PD Π Γ → PD α Γ

    𝟘    : PD * Γ
    _⊕_  : PD * Γ → PD * Γ → PD * Γ
    𝟙    : PD * Γ
    _⊗_  : PD * Γ → PD * Γ → PD * Γ
    ⊖_   : PD * Γ → PD * Γ
    ∂_∣_ : PD * (* ∙ Γ) → PD * Γ → PD * Γ

  infixl 20 _⊕_
  infixl 30 _⊗_
  infixr 50 ⊖_

  open import SOAS.Metatheory.MetaAlgebra ⅀F 𝔛

  PDᵃ : MetaAlg PD
  PDᵃ = record
    { 𝑎𝑙𝑔 = λ where
      (zeroₒ ⋮ _)     → 𝟘
      (addₒ  ⋮ a , b) → _⊕_  a b
      (oneₒ  ⋮ _)     → 𝟙
      (multₒ ⋮ a , b) → _⊗_  a b
      (negₒ  ⋮ a)     → ⊖_   a
      (pdₒ   ⋮ a , b) → ∂_∣_ a b
    ; 𝑣𝑎𝑟 = var ; 𝑚𝑣𝑎𝑟 = λ 𝔪 mε → mvar 𝔪 (tabulate mε) }

  module PDᵃ = MetaAlg PDᵃ

  module _ {𝒜 : Familyₛ}(𝒜ᵃ : MetaAlg 𝒜) where

    open MetaAlg 𝒜ᵃ

    𝕤𝕖𝕞 : PD ⇾̣ 𝒜
    𝕊 : Sub PD Π Γ → Π ~[ 𝒜 ]↝ Γ
    𝕊 (t ◂ σ) new = 𝕤𝕖𝕞 t
    𝕊 (t ◂ σ) (old v) = 𝕊 σ v
    𝕤𝕖𝕞 (mvar 𝔪 mε) = 𝑚𝑣𝑎𝑟 𝔪 (𝕊 mε)
    𝕤𝕖𝕞 (var v) = 𝑣𝑎𝑟 v

    𝕤𝕖𝕞  𝟘         = 𝑎𝑙𝑔 (zeroₒ ⋮ tt)
    𝕤𝕖𝕞 (_⊕_  a b) = 𝑎𝑙𝑔 (addₒ  ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞  𝟙         = 𝑎𝑙𝑔 (oneₒ  ⋮ tt)
    𝕤𝕖𝕞 (_⊗_  a b) = 𝑎𝑙𝑔 (multₒ ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)
    𝕤𝕖𝕞 (⊖_   a)   = 𝑎𝑙𝑔 (negₒ  ⋮ 𝕤𝕖𝕞 a)
    𝕤𝕖𝕞 (∂_∣_ a b) = 𝑎𝑙𝑔 (pdₒ   ⋮ 𝕤𝕖𝕞 a , 𝕤𝕖𝕞 b)

    𝕤𝕖𝕞ᵃ⇒ : MetaAlg⇒ PDᵃ 𝒜ᵃ 𝕤𝕖𝕞
    𝕤𝕖𝕞ᵃ⇒ = record
      { ⟨𝑎𝑙𝑔⟩ = λ{ {t = t} → ⟨𝑎𝑙𝑔⟩ t }
      ; ⟨𝑣𝑎𝑟⟩ = refl
      ; ⟨𝑚𝑣𝑎𝑟⟩ = λ{ {𝔪 = 𝔪}{mε} → cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-tab mε)) }  }
      where
      open ≡-Reasoning
      ⟨𝑎𝑙𝑔⟩ : (t : ⅀ PD α Γ) → 𝕤𝕖𝕞 (PDᵃ.𝑎𝑙𝑔 t) ≡ 𝑎𝑙𝑔 (⅀₁ 𝕤𝕖𝕞 t)
      ⟨𝑎𝑙𝑔⟩ (zeroₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (addₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (oneₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (multₒ ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (negₒ  ⋮ _) = refl
      ⟨𝑎𝑙𝑔⟩ (pdₒ   ⋮ _) = refl

      𝕊-tab : (mε : Π ~[ PD ]↝ Γ)(v : ℐ α Π) → 𝕊 (tabulate mε) v ≡ 𝕤𝕖𝕞 (mε v)
      𝕊-tab mε new = refl
      𝕊-tab mε (old v) = 𝕊-tab (mε ∘ old) v

    module _ (g : PD ⇾̣ 𝒜)(gᵃ⇒ : MetaAlg⇒ PDᵃ 𝒜ᵃ g) where

      open MetaAlg⇒ gᵃ⇒

      𝕤𝕖𝕞! : (t : PD α Γ) → 𝕤𝕖𝕞 t ≡ g t
      𝕊-ix : (mε : Sub PD Π Γ)(v : ℐ α Π) → 𝕊 mε v ≡ g (index mε v)
      𝕊-ix (x ◂ mε) new = 𝕤𝕖𝕞! x
      𝕊-ix (x ◂ mε) (old v) = 𝕊-ix mε v
      𝕤𝕖𝕞! (mvar 𝔪 mε) rewrite cong (𝑚𝑣𝑎𝑟 𝔪) (dext (𝕊-ix mε))
        = trans (sym ⟨𝑚𝑣𝑎𝑟⟩) (cong (g ∘ mvar 𝔪) (tab∘ix≈id mε))
      𝕤𝕖𝕞! (var v) = sym ⟨𝑣𝑎𝑟⟩

      𝕤𝕖𝕞! 𝟘 = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (_⊕_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! 𝟙 = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (_⊗_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (⊖_ a) rewrite 𝕤𝕖𝕞! a = sym ⟨𝑎𝑙𝑔⟩
      𝕤𝕖𝕞! (∂_∣_ a b) rewrite 𝕤𝕖𝕞! a | 𝕤𝕖𝕞! b = sym ⟨𝑎𝑙𝑔⟩

-- Syntax instance for the signature
PD:Syn : Syntax
PD:Syn = record
  { ⅀F = ⅀F
  ; ⅀:CS = ⅀:CompatStr
  ; mvarᵢ = PD:Terms.mvar
  ; 𝕋:Init = λ 𝔛 → let open PD:Terms 𝔛 in record
    { ⊥ = PD ⋉ PDᵃ
    ; ⊥-is-initial = record { ! = λ{ {𝒜 ⋉ 𝒜ᵃ} → 𝕤𝕖𝕞 𝒜ᵃ ⋉ 𝕤𝕖𝕞ᵃ⇒ 𝒜ᵃ }
    ; !-unique = λ{ {𝒜 ⋉ 𝒜ᵃ} (f ⋉ fᵃ⇒) {x = t} → 𝕤𝕖𝕞! 𝒜ᵃ f fᵃ⇒ t } } } }

-- Instantiation of the syntax and metatheory
open Syntax PD:Syn public
open PD:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands PDᵃ public
open import SOAS.Metatheory PD:Syn public

-- Derived operations
∂₀_ : {𝔛 : Familyₛ} → PD 𝔛 * (* ∙ Γ) → PD 𝔛 * (* ∙ Γ)
∂₀_ {𝔛 = 𝔛} e = ∂ Theory.𝕨𝕜 𝔛 e ∣ x₀
∂₁_ : {𝔛 : Familyₛ} → PD 𝔛 * (* ∙ * ∙ Γ) → PD 𝔛 * (* ∙ * ∙ Γ)
∂₁_ {𝔛 = 𝔛} e = ∂ Theory.𝕨𝕜 𝔛 e ∣ x₁
infix 10 ∂₀_ ∂₁_

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
module TruthValue where

open import OscarPrelude

record TruthValue : Set
 where
  constructor ⟨_⟩
  field
    truthValue : Bool

open TruthValue public


text:
module Base.Free.Instance.Identity.Properties where

open import Relation.Binary.PropositionalEquality using (refl; cong)

open import Base.Free                             using (Free; pure; impure)
open import Base.Free.Instance.Identity                                      renaming (Identity to IdentityF)

open import Base.Isomorphism                      using (_≃_)
open        _≃_

-- The usual `Identity` monad representation an the free version are isomorphic.
data Identity (A : Set) : Set where
  Ident : A → Identity A

Identity≃IdentityF : ∀ {A} → Identity A ≃ IdentityF A
to Identity≃IdentityF (Ident x)  = pure x
from Identity≃IdentityF (pure x) = Ident x
from∘to Identity≃IdentityF (Ident x) = refl
to∘from Identity≃IdentityF (pure x)  = refl

max_stars_repo_name: FreeProving/free-compiler

max_issues_repo_name: FreeProving/free-compiler

max_forks_repo_name: FreeProving/free-compiler


text:
module Nats.Multiply.Comm where

open import Nats
open import Equality
open import Function

open import Nats.Add.Comm
open import Nats.Add.Assoc

------------------------------------------------------------------------
-- internal stuffs

private

  a*0=0*a : ∀ a → a * 0 ≡ 0
  a*0=0*a  zero   = refl
  a*0=0*a (suc a) = a*0=0*a a

  a+a*b=a*++b : ∀ a b → a + a * b ≡ a * suc b
  a+a*b=a*++b  zero   _ = refl
  a+a*b=a*++b (suc a) b
    rewrite nat-add-comm b $ a * suc b
          | nat-add-comm b $ a * b
          | sym $ nat-add-assoc a (a * b) b
          | a+a*b=a*++b a b
            = refl

  a*b=b*a : ∀ a b → a * b ≡ b * a
  a*b=b*a  zero   b
    rewrite a*0=0*a b = refl
  a*b=b*a (suc a) b
    rewrite a*b=b*a a b
          | a+a*b=a*++b b a
            = refl

------------------------------------------------------------------------
-- public aliases

nat-multiply-comm : ∀ a b → a * b ≡ b * a
nat-multiply-comm = a*b=b*a


text:
postulate
  A : →.B

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda