text:
{-

The Existence of Smith Normal Form for Integer Matrices (KANG Rongji, Jan. 2022)

-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.IntegerMatrix.Smith.Normalization where

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

open import Cubical.Data.Nat
  hiding   (_·_)
  renaming (_+_ to _+ℕ_ ; +-assoc to +Assocℕ)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Nat.Divisibility
  using    (m∣n→m≤n)
  renaming (∣-trans to ∣ℕ-trans)
open import Cubical.Data.Int
  hiding   (_+_ ; _·_ ; _-_ ; -_ ; addEq)
open import Cubical.Data.Int.Divisibility
open import Cubical.Data.FinData
open import Cubical.Data.Empty as Empty
open import Cubical.Data.Sum

open import Cubical.Algebra.Matrix
open import Cubical.Algebra.Matrix.CommRingCoefficient
open import Cubical.Algebra.Matrix.Elementaries
open import Cubical.Algebra.IntegerMatrix.Base
open import Cubical.Algebra.IntegerMatrix.Elementaries
open import Cubical.Algebra.IntegerMatrix.Smith.NormalForm

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Instances.Int
  renaming (ℤ to ℤRing)

open import Cubical.Relation.Nullary
open import Cubical.Induction.WellFounded

private
  variable
    m n k : ℕ

open CommRingStr (ℤRing .snd)
open Coefficient  ℤRing
open Sim

-- The elementary transformations needed

open ElemTransformation ℤRing
open ElemTransformationℤ
open SwapFirstRow
open SwapPivot
open AddFirstRow
open RowsImproved
open ColsImproved

-- Operations used in the reduction step

record RowsImprovedTrick (M : Mat (suc m) (suc n)) : Type where
  field
    sim : Sim M

    div     : (i : Fin (suc m)) → sim .result zero zero ∣ M i zero
    const   : (i : Fin m) → sim .result (suc i) zero ≡ sim .result zero zero
    nonZero : ¬ sim .result zero zero ≡ 0

open RowsImprovedTrick

improveRowsTrick : (M : Mat (suc m) (suc n))(p : ¬ M zero zero ≡ 0) → RowsImprovedTrick M
improveRowsTrick M p =
  let improveM = improveRows M p
      trickM = addFirstRow (improveM .sim .result)
      inv₀₀ = (λ t → trickM .inv₀ t zero)
  in  record
        { sim = compSim (improveM .sim) (trickM .sim)
        ; div     = (λ i → subst (λ a → a ∣ M i zero) inv₀₀ (improveM .div i))
        ; const   =
              (λ i → sym (trickM .addEq i zero)
            ∙ (λ t → improveM .sim .result zero zero + improveM .vanish i t)
            ∙ +Rid _ ∙ inv₀₀)
        ; nonZero = (λ r → improveM .nonZero (inv₀₀ ∙ r)) }

-- Reduce the pivot

record PivotReduced (M : Mat (suc m) (suc n)) : Type where
  field
    sim : Sim M

    nonZero : ¬ sim .result zero zero ≡ 0
    div : (i : Fin (suc m))(j : Fin (suc n)) → sim .result zero zero ∣ sim .result i j

open PivotReduced

simPivotReduced : {M : Mat (suc m) (suc n)}
  (SimM : Sim M)(prSimM : PivotReduced (SimM .result)) → PivotReduced M
simPivotReduced simM prSimM .sim = compSim simM (prSimM .sim)
simPivotReduced _ prSimM .nonZero = prSimM .nonZero
simPivotReduced _ prSimM .div     = prSimM .div

-- Helpers to do structural recursion
record RowsImprovedTrickHelper (M : Mat (suc m) (suc n)) : Type where
  field
    sim : Sim M

    const   : (i : Fin m) → sim .result (suc i) zero ≡ sim .result zero zero
    nonZero : ¬ sim .result zero zero ≡ 0

open RowsImprovedTrickHelper

record InductionHelper (M : Mat (suc m) (suc n)) : Type where
  field
    improved : RowsImprovedTrickHelper M
    normIneq : abs (improved .sim .result zero zero) < abs (M zero zero)

open InductionHelper

private
  reducePivot-induction-helper :
      (M : Mat (suc m) (suc n))
    → (p : ¬ M zero zero ≡ 0)
    → (j : Fin n)(q : ¬ M zero zero ∣ M zero (suc j))
    → InductionHelper M
  reducePivot-induction-helper M p j q =
    let improveColsM = improveCols M p
        improveM = improveRowsTrick (improveColsM .sim .result) (improveColsM .nonZero)
    in  record
        { improved =
          record
          { sim = compSim (improveColsM .sim) (improveM .sim)
          ; const   = improveM .const
          ; nonZero = improveM .nonZero }
        ; normIneq =
          ≤<-trans
            (m∣n→m≤n (¬x≡0→¬abs≡0 (improveColsM .nonZero)) (∣→∣ℕ (improveM .div zero)))
            (stDivIneq p q (improveColsM .div zero) (improveColsM .div (suc j))) }

  reducePivot-helper :
      (M : Mat (suc m) (suc n))
    → (p : ¬ M zero zero ≡ 0)(h : Norm (M zero zero))
    → (cst : (i : Fin m) → M (suc i) zero ≡ M zero zero)
    → (pivot? : PivotOrNot (M zero zero) M)
    → PivotReduced M
  reducePivot-helper M _ _ _ (noPivot q) .sim     = idSim M
  reducePivot-helper _ p _ _ (noPivot q) .nonZero = p
  reducePivot-helper _ _ _ _ (noPivot q) .div     = q
  reducePivot-helper _ _ _ _ (pivot zero zero q) =
    Empty.rec (q (∣-refl refl))
  reducePivot-helper M _ _ cst (pivot (suc i) zero q) =
    Empty.rec (q (subst (λ a → (M zero zero) ∣ a) (sym (cst i)) (∣-refl refl)))
  reducePivot-helper M p (acc ind) _ (pivot zero (suc j) q) =
    let helperM = reducePivot-induction-helper M p j q
        reduceM =
          reducePivot-helper
            (helperM .improved .sim .result)
            (helperM .improved .nonZero)
            (ind _ (helperM .normIneq))
            (helperM .improved .const) (findPivot _ _)
    in  simPivotReduced (helperM .improved .sim) reduceM
  reducePivot-helper M p (acc ind) cst (pivot (suc i) (suc j) q) =
    let swapM = swapFirstRow i M
        swapNonZero = (λ r → p (sym (cst i) ∙ (swapM .swapEq zero) ∙ r))
        swapDiv =
          (transport ((λ t → ¬ cst i (~ t) ∣ M (suc i) (suc j))
                    ∙ (λ t → ¬ swapM .swapEq zero t ∣ swapM .swapEq (suc j) t)) q)
        helperM  = reducePivot-induction-helper _ swapNonZero j swapDiv
        swapNorm =
          subst (λ a → abs (helperM . improved .sim .result zero zero) < abs a)
                (sym (sym (cst i) ∙ (swapM .swapEq zero))) (helperM .normIneq)
        reduceM  =
          reducePivot-helper
            (helperM .improved .sim .result)
            (helperM .improved .nonZero)
            (ind _ swapNorm)
            (helperM .improved .const) (findPivot _ _)
    in  simPivotReduced (compSim (swapM .sim) (helperM .improved .sim)) reduceM

-- The reduction of pivot

reducePivot : (M : Mat (suc m) (suc n))(p : ¬ M zero zero ≡ 0) → PivotReduced M
reducePivot M p =
  let improveM = improveRowsTrick M p
      reduceM  =
        reducePivot-helper
          (improveM .sim .result)
          (improveM .nonZero)
          (<-wellfounded _)
          (improveM .const) (findPivot _ _)
  in  simPivotReduced (improveM .sim) reduceM

-- One induction step towards normal form

open isSmithNormal
open Smith

record SmithStep (M : Mat (suc m) (suc n)) : Type where
  field
    sim : Sim M

    firstColClean : (i : Fin m) → sim .result (suc i) zero ≡ 0
    firstRowClean : (j : Fin n) → sim .result zero (suc j) ≡ 0

    nonZero : ¬ sim .result zero zero ≡ 0
    div : (i : Fin m)(j : Fin n) → sim .result zero zero ∣ sim .result (suc i) (suc j)

open SmithStep

private
  smithStep-helper : (M : Mat (suc m) (suc n)) → NonZeroOrNot M → SmithStep M ⊎ (M ≡ 𝟘)
  smithStep-helper _ (allZero p) = inr p
  smithStep-helper M (hereIs i j p) =
    let swapM = swapPivot i j M
        swapNonZero = (λ r → p (swapM .swapEq ∙ r))
        reduceM = reducePivot (swapM .sim .result) swapNonZero
        improveColM = improveCols (reduceM .sim .result) (reduceM .nonZero)
        divCol = (λ i j → bézoutRows-commonDivInv _ (reduceM .nonZero) (λ i j → reduceM .div j i) j i)
        improveRowM = improveRows (improveColM .sim .result) (improveColM .nonZero)
        invCol = bézoutRows-inv _ (improveColM .nonZero) (λ i → divCol (suc i) zero)
    in  inl record
        { sim = compSim (swapM .sim) (compSim (reduceM .sim) (compSim (improveColM .sim) (improveRowM .sim)))
        ; firstColClean = improveRowM .vanish
        ; firstRowClean = (λ j → (λ t → invCol (~ t) (suc j)) ∙ improveColM .vanish j)
        ; nonZero = improveRowM .nonZero
        ; div     = (λ i j → bézoutRows-commonDivInv _ (improveColM .nonZero) divCol (suc i) (suc j)) }

smithStep : (M : Mat (suc m) (suc n)) → SmithStep M ⊎ (M ≡ 𝟘)
smithStep M = smithStep-helper M (findNonZero _)

-- The main procedure

private
  smithReduction-helper :
      (M : Mat (suc m) (suc n))(step : SmithStep M)
    → step .sim .result ≡ step .sim .result zero zero ⊕ sucMat (step .sim .result)
  smithReduction-helper M step t zero zero = step .sim .result zero zero
  smithReduction-helper M step t zero (suc j) = step .firstRowClean j t
  smithReduction-helper M step t (suc i) zero = step .firstColClean i t
  smithReduction-helper M step t (suc i) (suc j) = step .sim .result (suc i) (suc j)

consIsSmithNormal :
    (a : ℤ)(M : Mat m n)
  → (p : ¬ a ≡ 0)
  → (div : (i : Fin m)(j : Fin n) → a ∣ M i j)
  → isSmithNormal M → isSmithNormal (a ⊕ M)
consIsSmithNormal a _ p d isNorm .divs = cons a (isNorm .divs) (smith∣ a isNorm p d)
consIsSmithNormal _ _ _ _ isNorm .rowNull = isNorm .rowNull
consIsSmithNormal _ _ _ _ isNorm .colNull = isNorm .colNull
consIsSmithNormal _ _ _ _ isNorm .rowEq = (λ t → suc (isNorm .rowEq t))
consIsSmithNormal _ _ _ _ isNorm .colEq = (λ t → suc (isNorm .colEq t))
consIsSmithNormal a _ _ _ isNorm .matEq = (λ t → a ⊕ isNorm .matEq t)

smithReduction :
    (a : ℤ)(M : Mat m n)
  → (p : ¬ a ≡ 0)
  → (div : (i : Fin m)(j : Fin n) → a ∣ M i j)
  → Smith M → Smith (a ⊕ M)
smithReduction a _ _ _ smithnorm .sim = ⊕Sim a (smithnorm .sim)
smithReduction a _ p d smithnorm .isnormal =
  consIsSmithNormal a _ p (sim∣ _ _ (smithnorm .sim) d) (smithnorm .isnormal)

-- The Existence of Smith Normal Form

smith : (M : Mat m n) → Smith M
smith {m = 0} = smithEmpty
smith {m = suc m} {n = 0} = smithEmptyᵗ
smith {m = suc m} {n = suc n} M = helper (smithStep _)
  where
  helper : SmithStep M ⊎ (M ≡ 𝟘) → Smith M
  helper (inr p) = subst Smith (sym p) smith𝟘
  helper (inl stepM) =
    let sucM = sucMat (stepM .sim .result)
        smithM = smithReduction _ _ (stepM .nonZero) (stepM .div) (smith sucM)
    in  simSmith (compSim (stepM .sim) (≡Sim (smithReduction-helper _ stepM))) smithM

-- TODO: The uniqueness of Smith normal form up to unit multiplication.

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
{-# OPTIONS --cubical #-}
module SolutionsSession1 where

open import Part1 hiding (B)

variable
  B : A → Type ℓ

-- Solutions to ExerciseSession1

-- Exercise 1:
funExtDep : {f g : (x : A) → B x}
          → ((x : A) → f x ≡ g x)
          → f ≡ g
funExtDep p i x = p x i

-- Exercise 2:
congP : {x y : A} {B : A → Type ℓ'}
        (f : (a : A) → B a) (p : x ≡ y) →
        PathP (λ i → B (p i)) (f x) (f y)
congP f p i = f (p i)

-- Exercise 3:
isContrInhProp : isProp A → A → isContr A
isContrInhProp p x = x , p x

-- We could have stated isProp as follows:
isProp' : Type ℓ → Type ℓ
isProp' A = (x y : A) → isContr (x ≡ y)

-- Exercise 4:
isProp'→isProp : isProp' A → isProp A
isProp'→isProp h = λ x y → h x y .fst

-- Exercise 5:
isPropΠ : (h : (x : A) → isProp (B x)) → isProp ((x : A) → B x)
isPropΠ h p q i x = h x (p x) (q x) i

-- Exercise 6:
funExt⁻ : {f g : (x : A) → B x} → f ≡ g → ((x : A) → f x ≡ g x)
funExt⁻ eq x i = eq i x

-- Exercise 7:
isSetΠ : (h : (x : A) → isSet (B x)) → isSet ((x : A) → B x)
isSetΠ h f g p q i j x = h x (f x) (g x) (funExt⁻ p x) (funExt⁻ q x) i j

-- We could have defined the type of singletons as follows
singl' : {A : Type ℓ} (a : A) → Type ℓ
singl' {A = A} a = Σ[ x ∈ A ] x ≡ a

-- Exercise 8:
isContrSingl' : (x : A) → isContr (singl' x)
isContrSingl' x = ctr , prf
  where
  ctr : singl' x
  ctr = x , refl

  prf : (s : singl' x) → ctr ≡ s
  prf (y , pax) i = (pax (~ i)) , λ j → pax (~ i ∨ j)

ext: agda


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

module Cubical.Categories.TypesOfCategories.TypeCategory where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv
open import Cubical.Data.Sigma
import Cubical.Functions.Fibration as Fibration

open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.Presheaf
open import Cubical.Categories.Limits.Pullback
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Instances.Sets

open Fibration.ForSets

record isTypeCategory {ℓ ℓ' ℓ''} (C : Precategory ℓ ℓ')
       : Type (ℓ-max ℓ (ℓ-max ℓ' (ℓ-suc ℓ''))) where
  open Precategory C
  open Cospan
  open PullbackLegs
  open isPullback
  field
    -- a Type of types over a context
    Ty[_] : ob → Type ℓ''
    -- extend a context with a type
    cext : ∀ (Γ : _) → (A : Ty[ Γ ]) → Σ[ ΓA ∈ ob ] (C [ ΓA , Γ ])

  -- the new object from a context extension
  _⍮_ : (Γ : _) → (A : Ty[ Γ ]) → ob
  Γ ⍮ A = fst (cext Γ A)

  -- the projection from the extended context to the original
  π : (Γ : _) → (A : Ty[ Γ ]) → C [ Γ ⍮ A , Γ ]
  π Γ A = snd (cext Γ A)

  field
    -- pullback over context extentions
    reindex : ∀ {Γ' Γ}
            → C [ Γ' , Γ ]
            → (Ty[ Γ ] → Ty[ Γ' ])

    q⟨_,_⟩ : ∀ {Γ' Γ}
           → (f : C [ Γ' , Γ ])
           → (A : Ty[ Γ ])
           → C [ Γ' ⍮ (reindex f A) , Γ ⍮ A ]

    isPB : ∀ {Γ' Γ : ob} (f : C [ Γ' , Γ ]) (A : Ty[ Γ ])
         → isPullback {C = C} (cospan Γ' Γ (Γ ⍮ A) f (π Γ A))
                      (pblegs (π Γ' (reindex f A)) q⟨ f , A ⟩)

-- presheaves are type contexts
module _ {ℓ ℓ' ℓ'' : Level} (C : Precategory ℓ ℓ') where
  open isTypeCategory
  open Precategory
  open Functor
  open NatTrans
  open isPullback

  private
    -- types over Γ are types with a "projection" (aka surjection) to Γ
    PSTy[_] : PreShv C ℓ'' .ob → Type _
    PSTy[ Γ ] = Σ[ ΓA ∈ PreShv C ℓ'' .ob ]
                   Σ[ π ∈ ΓA ⇒ Γ ]
                     (∀ (c : C .ob)
                     → isSurjSET {A = ΓA ⟅ c ⟆} {Γ ⟅ c ⟆} (π ⟦ c ⟧))

    -- just directly use types from above as context extensions
    PSCext : (Γ : _) → PSTy[ Γ ] → Σ[ ΓA ∈ PreShv C ℓ'' .ob ] ΓA ⇒ Γ
    PSCext Γ (ΓA , π , _) = ΓA , π

    -- the pullback or reindexed set is the disjoint union of the fibers
    -- from the projection
    module _ {Δ Γ : PreShv C ℓ'' .ob} (γ : Δ ⇒ Γ)
             (A'@(ΓA , π , isSurjπ) : PSTy[ Γ ]) where
      ΔA : PreShv C ℓ'' .ob
      ΔA .F-ob c =  ΔATy , isSetΔA
        where
          ΔATy = (Σ[ x ∈ fst (Δ ⟅ c ⟆) ] fiber (π ⟦ c ⟧) ((γ ⟦ c ⟧) x))

          isSetΔA : isSet ΔATy
          isSetΔA = isOfHLevelΣ 2 (snd (Δ ⟅ c ⟆)) λ Γc → isOfHLevelΣ 2 (snd (ΓA ⟅ c ⟆)) λ ΓAc → isProp→isSet (snd (Γ ⟅ c ⟆) _ _)
      -- for morphisms, we apply Δ ⟪ f ⟫ to the first component
      -- and ΓA ⟪ f ⟫ to the second
      -- the fiber rule
      ΔA .F-hom {c} {d} f (δax , γax , eq)
        = ((Δ ⟪ f ⟫) δax)
        , (((ΓA ⟪ f ⟫) γax)
        , ((π ⟦ d ⟧) ((ΓA ⟪ f ⟫) γax)
        ≡[ i ]⟨ π .N-hom f i γax ⟩
          (Γ ⟪ f ⟫) ((π ⟦ c ⟧) γax)
        ≡[ i ]⟨ (Γ ⟪ f ⟫) (eq i) ⟩
          (Γ ⟪ f ⟫) ((γ ⟦ c ⟧) δax)
        ≡[ i ]⟨ γ .N-hom f (~ i) δax ⟩
          (γ ⟦ d ⟧) ((Δ ⟪ f ⟫) δax)
        ∎))
      ΔA .F-id {x = c}
        = funExt λ (δax , γax , eq)
                → ΣPathP ((λ i → Δ .F-id i δax)
                          , fibersEqIfRepsEq {isSetB = snd (Γ ⟅ c ⟆)} _
                                            (λ i → ΓA .F-id i γax))
      ΔA .F-seq {a} {b} {c} f g
        = funExt λ (δax , γax , eq)
                → ΣPathP ((λ i → Δ .F-seq f g i δax)
                  , fibersEqIfRepsEq {isSetB = snd (Γ ⟅ c ⟆)} _
                                      λ i → ΓA .F-seq f g i γax)
      π' : ΔA ⇒ Δ
      π' .N-ob c (x , snd) = x
      π' .N-hom f = refl
      PSReindex : PSTy[ Δ ]
      PSReindex = ΔA , (π' , isSurj)
        where

          isSurj : ∀ (c : C .ob) → isSurjSET {A = ΔA ⟅ c ⟆} {B = Δ ⟅ c ⟆} (π' ⟦ c ⟧)
          isSurj c δx = (δx , isSurjπ c ((γ ⟦ c ⟧) δx)) , refl

      PSq : ΔA ⇒ ΓA
      PSq .N-ob c (δax , γax , eq) = γax
      PSq .N-hom {c} {d} f = funExt λ (δax , γax , eq) → refl

      PSIsPB : isPullback {C = PreShv C ℓ''}
                 (cospan Δ Γ (fst (PSCext Γ A')) γ (snd (PSCext Γ A')))
                 (pblegs (snd (PSCext Δ PSReindex)) (PSq))
      PSIsPB .sq = makeNatTransPath (funExt sqExt)
        where
          sqExt : ∀ (c : C .ob) → _
          sqExt c = funExt λ (δax , γax , eq) → sym eq

      PSIsPB .up {Θ} (cone (pblegs p₁ p₂) sq)
        = ((α , eq)
          , unique)
        where
          α : Θ ⇒ ΔA
          α .N-ob c t = ((p₁ ⟦ c ⟧) t)
                      , (((p₂ ⟦ c ⟧) t)
                      , (λ i → (sq (~ i) ⟦ c ⟧) t))
          α .N-hom {d} {c} f = funExt αHomExt
            where
              αHomExt : ∀ (t : fst (Θ ⟅ d ⟆))
                      → ((p₁ ⟦ c ⟧) ((Θ ⟪ f ⟫) t) , (p₂ ⟦ c ⟧) ((Θ ⟪ f ⟫) t), _)
                      ≡ ((Δ ⟪ f ⟫) ((p₁ ⟦ d ⟧) t) , (ΓA ⟪ f ⟫) ((p₂ ⟦ d ⟧) t) , _)
              αHomExt t = ΣPathP ((λ i → p₁ .N-hom f i t)
                                 , fibersEqIfRepsEq {isSetB = snd (Γ ⟅ c ⟆)} _
                                                    (λ i → p₂ .N-hom f i t))

          eq : _
          eq = makeNatTransPath (funExt (λ _ → funExt λ _ → refl))
             , makeNatTransPath (funExt (λ _ → funExt λ _ → refl))

          unique : ∀ (βeq : Σ[ β ∈ Θ ⇒ ΔA ] _)
                 → (α , eq) ≡ βeq
          unique (β , eqβ) = ΣPathP (α≡β , eq≡eqβ)
            where
              α≡β : α ≡ β
              α≡β = makeNatTransPath (funExt λ c → funExt λ t → eqExt c t)
                where
                  eqβ1 = eqβ .fst
                  eqβ2 = eqβ .snd
                  eqExt : ∀ (c : C .ob)
                        → (t : fst (Θ ⟅ c ⟆))
                        → (α ⟦ c ⟧) t ≡ (β ⟦ c ⟧) t
                  eqExt c t = ΣPathP ((λ i → (eqβ1 i ⟦ c ⟧) t)
                            , fibersEqIfRepsEq {isSetB = snd (Γ ⟅ c ⟆)} _
                                               (λ i → (eqβ2 i ⟦ c ⟧) t))
              eq≡eqβ : PathP (λ i
                             → (p₁ ≡ (α≡β i) ●ᵛ π')
                             × (p₂ ≡ (α≡β i) ●ᵛ PSq)) eq eqβ
              eq≡eqβ = ΣPathP ( isPropNatP1 (eq .fst) (eqβ .fst) α≡β
                              , isPropNatP2 (eq .snd) (eqβ .snd) α≡β)
                where
                  isPropNatP1 : isOfHLevelDep 1 (λ γ → p₁ ≡ γ ●ᵛ π')
                  isPropNatP1 = isOfHLevel→isOfHLevelDep 1 (λ _ → isSetNat _ _)

                  isPropNatP2 : isOfHLevelDep 1 (λ γ → p₂ ≡ γ ●ᵛ PSq)
                  isPropNatP2 = isOfHLevel→isOfHLevelDep 1 (λ _ → isSetNat _ _)

  -- putting everything together
  isTypeCategoryPresheaf : isTypeCategory (PreShv C ℓ'')
  isTypeCategoryPresheaf .Ty[_] Γ = PSTy[ Γ ]
  isTypeCategoryPresheaf .cext = PSCext
  isTypeCategoryPresheaf .reindex = PSReindex
  isTypeCategoryPresheaf .q⟨_,_⟩ = PSq
  isTypeCategoryPresheaf .isPB = PSIsPB

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
-- This bug was reported by Christian Sattler. (I modified his example
-- slightly.)

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

module Issue903 where

record T : Set where
  constructor tt

postulate
  Id : (A : Set) → A → Set
  e  : (B : Set) (f : T → B) → Id B (f tt) → Id (T → B) f
  k  : (P : Set → Set) (u : P T) → Id (P T) u → T
  h  : Id T tt

q : T
q = k {!!} {!!} (e {!!} _ {!h!})

-- WAS: If one tries to give h:
--
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/MetaVars.hs:654

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2017-06-14, issue #2603
-- reported by rfindler, shrunk test case by Ulf

-- {-# OPTIONS -v tc.conv:40 -v tc.conv.atom:50 -v tc:80 -v tc.meta.assign:70 #-}

{-# OPTIONS --allow-unsolved-metas #-}

open import Agda.Builtin.Equality

data List (A : Set) : Set where
  [] : List A

postulate
  Signal : Set

data Any (xs : List Signal) : Set where
  no : Any xs

any : ∀ xs → Any xs
any [] = no

record Env : Set where
  field sig : List Signal
open Env

Can : (θ : Env) → Any (sig θ) → Set
Can θ no = Signal

postulate
  elephant : ∀ θ → Can θ (any (sig θ)) ≡ Signal

lemma2 : Set
lemma2 rewrite elephant _ = Signal

-- Should succeed.
-- This lead to an internal error when the conversion checker
-- tried to eta expand a meta variable but dontAssignMetas was on.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Prelude.Fin where

open import Prelude.Eq
open import Prelude.Nat

data Fin : Nat -> Set where
  fz : ∀{n} -> Fin (S n)
  fs : ∀{n} -> Fin n -> Fin (S n)

forget : {n : Nat} -> Fin n -> Nat
forget fz     = Z
forget (fs n) = S (forget n)

inject : (n : Nat) -> Fin (S n)
inject Z = fz
inject (S n) = fs (inject n)

inc : {n : Nat} -> Fin n -> Fin (S n)
inc fz     = fz
inc (fs n) = fs (inc n)


text:
module Thesis.Lang where

open import Thesis.Syntax public
open import Thesis.Environments public

⟦_⟧Const : ∀ {τ} → Const τ → ⟦ τ ⟧Type
⟦ unit ⟧Const = tt
⟦ lit n ⟧Const = n
⟦ plus ⟧Const = _+_
⟦ minus ⟧Const = _-_
⟦ cons ⟧Const v1 v2 = v1 , v2
⟦ fst ⟧Const (v1 , v2) = v1
⟦ snd ⟧Const (v1 , v2) = v2
⟦ linj ⟧Const v1 = inj₁ v1
⟦ rinj ⟧Const v2 = inj₂ v2
⟦ match ⟧Const (inj₁ x) f g = f x
⟦ match ⟧Const (inj₂ y) f g = g y

⟦_⟧Term : ∀ {Γ τ} → Term Γ τ → ⟦ Γ ⟧Context → ⟦ τ ⟧Type
⟦ const c ⟧Term ρ = ⟦ c ⟧Const
⟦ var x ⟧Term ρ = ⟦ x ⟧Var ρ
⟦ app s t ⟧Term ρ = ⟦ s ⟧Term ρ (⟦ t ⟧Term ρ)
⟦ abs t ⟧Term ρ = λ v → ⟦ t ⟧Term (v • ρ)

open import Theorem.CongApp
open import Postulate.Extensionality

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

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Ints.HAEquivInt.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HAEquiv

data HAEquivInt : Type₀ where
  zero : HAEquivInt
  suc : HAEquivInt -> HAEquivInt

  -- suc is a HAEquiv:
  pred : HAEquivInt -> HAEquivInt
  suc-pred : ∀ z -> suc (pred z) ≡ z
  pred-suc : ∀ z -> pred (suc z) ≡ z
  coh : ∀ z → (λ i → suc (pred-suc z i)) ≡ suc-pred (suc z)

suc-haequiv : HAEquiv HAEquivInt HAEquivInt
suc-haequiv = suc , record { g = pred ; sec = pred-suc ; ret = suc-pred ; com = coh }

-- OPEN: prove HAEquivInt ≃ Int! See Experiments/HInt.agda

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Strings: builtin type and basic operations
------------------------------------------------------------------------

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

module Data.String.Base where

open import Data.Nat.Base as Nat using (ℕ)
open import Data.List.Base as List using (List)
open import Data.List.NonEmpty as NE using (List⁺)
open import Agda.Builtin.Char using (Char)
open import Function

------------------------------------------------------------------------
-- From Agda.Builtin: type and renamed primitives

-- Note that we do not re-export primStringAppend because we want to
-- give it an infix definition and be able to assign it a level.

import Agda.Builtin.String as String

open String public using ( String )
  renaming
  ( primStringToList   to toList
  ; primStringFromList to fromList
  ; primShowString     to show
  )

------------------------------------------------------------------------
-- Operations

-- Additional conversion functions

fromList⁺ : List⁺ Char → String
fromList⁺ = fromList ∘ NE.toList

-- List-like functions

infixr 5 _++_
_++_ : String → String → String
_++_ = String.primStringAppend

length : String → ℕ
length = List.length ∘ toList

replicate : ℕ → Char → String
replicate n = fromList ∘ List.replicate n

concat : List String → String
concat = List.foldr _++_ ""

-- String-specific functions

unlines : List String → String
unlines = concat ∘ List.intersperse "\n"


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

open import Algebra.Bundles using (Semiring)

-- Credit: This definition is taken from the stdlib issue #1175
-- As given by @MatthewDaggitt and @mechvel

module Definitions.Semiring {α α≈} (R : Semiring α α≈)
  where
  open Semiring R

  record NonZero (x : Carrier) : Set α≈ where
     constructor mkNonZero
     field
        nonZero : x ≉ 0#


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

open import library.Basics hiding (Type ; Σ ; S)
open import library.types.Sigma

open import Sec2preliminaries
open import Sec3hedberg
open import Sec4hasConstToSplit
open import Sec5factorConst
open import Sec6hasConstToDecEq
open import Sec7populatedness

module Sec8taboos where

-- Subsection 8.1

all-hasConst : Type₁
all-hasConst = (X : Type) → hasConst X

-- Theorem 8.1
module functional-subrelation (ac : all-hasConst) (X : Type) (R : X × X → Type) where

  all-sets : (Y : Type) → is-set Y
  all-sets Y = pathHasConst→isSet (λ y₁ y₂ → ac _)

  R₋ : (x : X) → Type
  R₋ x = Σ X λ y → R(x , y)

  k : (x : X) → (R₋ x) → (R₋ x)
  k x = fst (ac _)

  kc : (x : X) → const (k x)
  kc x = snd (ac _)

  S : X × X → Type
  S (x , y) = Σ (R(x , y)) λ a →
                (y , a) == k x (y , a)

  -- the relation S
  S₋ : (x : X) → Type
  S₋ x = Σ X λ y → S(x , y)

  -- fix kₓ is equivalent to Sₓ
  -- This is just Σ-assoc. We try to make it more readable by adding some (trivial) steps.
  fixk-S : (x : X) → (fix (k x)) ≃ S₋ x
  fixk-S x =
      (fix (k x))                                           ≃⟨ ide _ ⟩
      (Σ (Σ X λ y → R(x , y)) λ a → a == k x a)             ≃⟨ Σ-assoc ⟩
      (Σ X λ y → Σ (R(x , y)) λ r → (y , r) == k x (y , r)) ≃⟨ ide _ ⟩
      (S₋ x)                                                ≃∎

  -- claim (0)
  subrelation : (x y : X) → S(x , y) →  R(x , y)
  subrelation x y (r , _) = r

   -- claim (1)
  prop-Sx : (x : X) → is-prop (S₋ x)
  prop-Sx x = equiv-preserves-level {A = fix (k x)} {B = (S₋ x)} (fixk-S x) (fixed-point _ (kc x))

  -- claim (2)
  same-domain : (x : X) → (R₋ x) ↔ (S₋ x)
  same-domain x = rs , sr where
    rs : (R₋ x) → (S₋ x)
    rs a = –> (fixk-S x) (to-fix (k x) (kc x) a)
    sr : (S₋ x) → (R₋ x)
    sr (y , r , _) = y , r

  -- claim (3)
  prop-S : (x y : X) → is-prop (S (x , y))
  prop-S x y = all-paths-is-prop all-paths where
    all-paths : (s₁ s₂ : S(x , y)) → s₁ == s₂
    all-paths s₁ s₂ = ss where

      yss : (y , s₁) == (y , s₂)
      yss = prop-has-all-paths (prop-Sx x) _ _

      ss : s₁ == s₂
      ss = set-lemma (all-sets _) y s₁ s₂ yss

-- intermediate definition
-- see the caveat about the notion 'epimorphism' in the article
is-split-epimorphism : {U V : Type} → (U → V) → Type
is-split-epimorphism {U} {V} e = Σ (V → U) λ s → (v : V) → e (s v) == v

is-epimorphism : {U V : Type} → (U → V) → Type₁
is-epimorphism {U} {V} e = (W : Type) → (f g : V → W) → ((u : U) → f (e u) == g (e u)) → (v : V) → f v == g v

-- Lemma 8.2
path-trunc-epi→set : {Y : Type} → ((y₁ y₂ : Y) → is-epimorphism (∣_∣ {X = y₁ == y₂})) → is-set Y
path-trunc-epi→set {Y} path-epi = reminder special-case where

  f : (y₁ y₂ : Y) → Trunc (y₁ == y₂) → Y
  f y₁ _ _ = y₁

  g : (y₁ y₂ : Y) → Trunc (y₁ == y₂) → Y
  g _ y₂ _ = y₂

  special-case : (y₁ y₂ : Y) → Trunc (y₁ == y₂) → y₁ == y₂
  special-case y₁ y₂ = path-epi y₁ y₂ Y (f y₁ y₂) (g y₁ y₂) (idf _)

  reminder : hseparated Y → is-set Y
  reminder = fst set-characterizations ∘ snd (snd set-characterizations)

-- Theorem 8.3 (1)
all-split→all-deceq : ((X : Type) → is-split-epimorphism (∣_∣ {X = X})) → (X : Type) → has-dec-eq X
all-split→all-deceq all-split = all-hasConst→dec-eq ac where
  ac : (X : Type) → hasConst X
  ac X = snd hasConst↔splitSup (fst (all-split X))

-- Theorem 8.3 (2)
all-epi→all-set : ((X : Type) → is-epimorphism (∣_∣ {X = X})) → (X : Type) → is-set X
all-epi→all-set all-epi X = path-trunc-epi→set (λ y₁ y₂ → all-epi (y₁ == y₂))

-- Subsection 8.2

-- Lemma 8.4, first proof
pop-splitSup-1 : {X : Type} → Pop (splitSup X)
pop-splitSup-1 {X} f c = to-fix f c (hasConst→splitSup (g , gc)) where

  g : X → X
  g x = f (λ _ → x) ∣ x ∣

  gc : const g
  gc x₁ x₂ =
    g x₁               =⟨ idp ⟩
    f (λ _ → x₁) ∣ x₁ ∣ =⟨ ap (λ k → k ∣ x₁ ∣) (c (λ _ → x₁) (λ _ → x₂)) ⟩
    f (λ _ → x₂) ∣ x₁ ∣ =⟨ ap (f (λ _ → x₂)) (prop-has-all-paths (h-tr X) ∣ x₁ ∣ ∣ x₂ ∣) ⟩
    f (λ _ → x₂) ∣ x₂ ∣ =⟨ idp ⟩
    g x₂               ∎

-- Lemma 8.4, second proof
pop-splitSup-2 : {X : Type} → Pop (splitSup X)
pop-splitSup-2 {X} = snd (pop-alt₂ {splitSup X}) get-P where
  get-P : (P : Type) → is-prop P → splitSup X ↔ P → P
  get-P P pp (hstp , phst) = hstp free-hst where

    xp : X → P
    xp x = hstp (λ _ → x)

    zp : Trunc X → P
    zp = rec pp xp

    free-hst : splitSup X
    free-hst z = phst (zp z) z

-- Lemma 8.5, third proof
pop-splitSup-3 : {X : Type} → Pop (splitSup X)
pop-splitSup-3 {X} = snd pop-alt translation where

  translation-aux : splitSup (splitSup X) → splitSup X
  translation-aux = λ hsthst z → hsthst (trunc-functorial {X = X} {Y = splitSup X} (λ x _ → x) z) z

  translation : Trunc (splitSup (splitSup X)) → Trunc (splitSup X)
  translation = trunc-functorial translation-aux

-- Theorem 8.5
module thm85 where

  One = (X : Type) → Pop X → Trunc X

  Two = (X : Type) → Trunc (splitSup X)

  Three = (P : Type) → is-prop P → (Y : P → Type) → ((p : P) → Trunc (Y p)) → Trunc ((p : P) → Y p)

  Four = (X Y : Type) → (X → Y) → (Pop X → Pop Y)

  One→Two : One → Two
  One→Two poptr X = poptr (splitSup X) pop-splitSup-1

  Two→One : Two → One
  Two→One trhst X pop = fst pop-alt pop (trhst X)

  One→Four : One → Four
  One→Four poptr X Y f = Trunc→Pop ∘ (trunc-functorial f) ∘ (poptr X)

  Four→One : Four → One
  Four→One funct X px = prop-pop (h-tr _) pz where
    pz : Pop (Trunc X)
    pz  =  funct X (Trunc X) ∣_∣ px

  -- only very slightly different to the proof in the article
  One→Three : One → Three
  One→Three poptr P pp Y = λ py → poptr _ (snd pop-alt' (λ hst p₀ → hst (contr-trick p₀ py) p₀)) where
    contr-trick : (p₀ : P) → ((p : P) → Trunc (Y p)) → Trunc ((p : P) → Y p)
    contr-trick p₀ py = rec {X = Y p₀}
                            {P = Trunc ((p : P) → Y p)}
                            (h-tr _)
                            (λ y₀ → ∣ <– (thm55aux.neutral-contr-exp {P = P} {Y = Y} pp p₀) y₀ ∣) (py p₀)

  Three→Two : Three → Two
  Three→Two proj X = proj (Trunc X) (h-tr _) (λ _ → X) (idf _)

-- Subsection 8.3

-- Some very simple lemmata

-- If P is a proposition, so is P + ¬ P
dec-is-prop : {P : Type} → (Funext {X = P} {Y = Empty}) → is-prop P → is-prop (P + ¬ P)
dec-is-prop {P} fext pp = all-paths-is-prop (λ { (inl p₁) (inl p₂) → ap inl (prop-has-all-paths pp _ _) ;
                                (inl p₁) (inr np₂) → Empty-elim {A = λ _ → inl p₁ == inr np₂} (np₂ p₁) ;
                                (inr np₁) (inl p₂) → Empty-elim {A = λ _ → inr np₁ == inl p₂} (np₁ p₂) ;
                                (inr np₁) (inr np₂) → ap inr (fext np₁ np₂ (λ p → prop-has-all-paths (λ ()) _ _)) })

-- Theorem 8.7
nonempty-pop→lem : ((X : Type) → Funext {X} {Empty})
                         → ((X : Type) → (¬(¬ X) → Pop X)) → LEM
nonempty-pop→lem fext nn-pop P pp = from-fix {X = dec} (idf _) (nn-pop dec nndec (idf _) idc) where
  dec : Type
  dec = P + ¬ P

  idc : const (idf dec)
  idc = λ _ _ → prop-has-all-paths (dec-is-prop {P} (fext P) pp) _ _

  nndec : ¬(¬ dec)
  nndec ndec = (λ np → ndec (inr np)) λ p → ndec (inl p)

-- Corollary 8.8
nonempty-pop↔lem : ((X : Type) → Funext {X} {Empty})
                         → ((X : Type) → (¬(¬ X) → Pop X)) ↔₁₁ LEM
nonempty-pop↔lem fext = nonempty-pop→lem fext , other where
  other : LEM → ((X : Type) → (¬(¬ X) → Pop X))
  other lem X nnX = p where
    pnp : Pop X + ¬ (Pop X)
    pnp = lem (Pop X) pop-property₂

    p : Pop X
    p = match pnp withl idf _ withr (λ np → Empty-elim {A = λ _ → Pop X} (nnX (λ x → np (pop-property₁ x))))

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Issue268 where

module Example₁ where
  open import Common.Coinduction

  module Record where

    record Stream : Set where
      constructor cons
      field
        tail : ∞ Stream

  module Data where

    data Stream : Set where
      cons : ∞ Stream → Stream

  -- open Data
  open Record

  id : Stream → Stream
  id (cons xs) = cons (♯ id (♭ xs))

  postulate
    P  : Stream → Set
    f  : ∀ xs → P (id xs) → Set
    xs : Stream
    p  : P (id xs)

  Foo : Set
  Foo = f _ p

  -- The code type checks when Data is opened, but not when Record is
  -- opened:
  --
  -- Bug.agda:34,11-12
  -- (Stream.tail (id xs)) != (.Bug.♯-0 _40) of type (∞ Stream)
  -- when checking that the expression p has type P (id (cons _40))

module Example₂ where

  data D : Set where
    d : D

  id : D → D
  id d = d

  module Record where

    record E : Set where
      constructor e
      field
        f : D

  module Data where

    data E : Set where
      e : D → E

  -- open Data
  open Record

  id′ : E → E
  id′ (e xs) = e (id xs)

  postulate
    P : E → Set
    f : (x : E) → P (id′ x) → Set
    x : E
    p : P (id′ x)

  Foo : Set
  Foo = f _ p

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: asr/agda-kanso

max_forks_repo_name: asr/agda-kanso


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Group.DirProd where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Semigroup

open GroupStr
open IsGroup hiding (·IdR ; ·IdL ; ·InvR ; ·InvL)
open IsMonoid hiding (·IdR ; ·IdL)
open IsSemigroup

DirProd : ∀ {ℓ ℓ'} → Group ℓ → Group ℓ' → Group (ℓ-max ℓ ℓ')
fst (DirProd G H) = (fst G) × (fst H)
1g (snd (DirProd G H)) = (1g (snd G)) , (1g (snd H))
_·_ (snd (DirProd G H)) (g , h) (g' , h') = _·_ (snd G) g g' , _·_ (snd H) h h'
inv (snd (DirProd G H)) (g , h) = (inv (snd G) g) , (inv (snd H) h)
isGroup (snd (DirProd G H)) = makeIsGroup
                              (isSet× (is-set (snd G)) (is-set (snd H)))
                              (λ x y z → ≡-× (·Assoc (snd G) _ _ _) (·Assoc (snd H) _ _ _))
                              (λ x → ≡-× (·IdR (snd G) _) (·IdR (snd H) _))
                              (λ x → ≡-× (·IdL (snd G) _) (·IdL (snd H) _))
                              (λ x → ≡-× (·InvR (snd G) _) (·InvR (snd H) _))
                              λ x → ≡-× (·InvL (snd G) _) (·InvL (snd H) _)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{-# OPTIONS --warning=error --allow-unsolved-metas #-}

-- This file contains everything that cannot be compiled in --safe mode.

--open import Lists.SortList

module Everything.Unsafe where


text:
module StrongArrows where

open import Library
open import Categories
open import Functors
open import MonoidalCat
open import WeakArrows

record SArrow {l m}(J : Monoidal {l}{m}) : Set (lsuc (l ⊔ m)) where
  constructor sarrow
  open Monoidal J
  open Cat C
  open Fun
  field A : Arrow C
  open Arrow A
  field fst' : ∀{X X' Y} -> R X' X -> R (OMap ⊗ (X' , Y)) (OMap ⊗ (X , Y))
  -- laws later

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
{-

Functions between structures S and T: X ↦ S X → T X

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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Path
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence

open import Cubical.Functions.FunExtEquiv

open import Cubical.Data.Nat
open import Cubical.Data.Vec

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

-- General function structure

FunctionStructure : (S : Type ℓ → Type ℓ₁) (T : Type ℓ → Type ℓ₂)
  → Type ℓ → Type (ℓ-max ℓ₁ ℓ₂)
FunctionStructure S T X = S X → T X

FunctionEquivStr : {S : Type ℓ → Type ℓ₁} {T : Type ℓ → Type ℓ₂}
  → StrEquiv S ℓ₁' → StrEquiv T ℓ₂'
  → StrEquiv (FunctionStructure S T) (ℓ-max ℓ₁ (ℓ-max ℓ₁' ℓ₂'))
FunctionEquivStr {S = S} {T} ι₁ ι₂ (X , f) (Y , g) e =
  {s : S X} {t : S Y} → ι₁ (X , s) (Y , t) e → ι₂ (X , f s) (Y , g t) e

functionUnivalentStr : {S : Type ℓ → Type ℓ₁} {T : Type ℓ → Type ℓ₂}
  (ι₁ : StrEquiv S ℓ₁') (θ₁ : UnivalentStr S ι₁)
  (ι₂ : StrEquiv T ℓ₂') (θ₂ : UnivalentStr T ι₂)
  → UnivalentStr (FunctionStructure S T) (FunctionEquivStr ι₁ ι₂)
functionUnivalentStr ι₁ θ₁ ι₂ θ₂ e =
  compEquiv
    (equivImplicitΠCod (equivImplicitΠCod (equiv→ (θ₁ e) (θ₂ e))))
    funExtDepEquiv

functionEquivAction : {S : Type ℓ → Type ℓ₁} {T : Type ℓ → Type ℓ₂}
  → EquivAction S → EquivAction T
  → EquivAction (FunctionStructure S T)
functionEquivAction α₁ α₂ e = equiv→ (α₁ e) (α₂ e)

functionTransportStr : {S : Type ℓ → Type ℓ₁} {T : Type ℓ → Type ℓ₂}
  (α₁ : EquivAction S) (τ₁ : TransportStr α₁)
  (α₂ : EquivAction T) (τ₂ : TransportStr α₂)
  → TransportStr (functionEquivAction α₁ α₂)
functionTransportStr {S = S} α₁ τ₁ α₂ τ₂ e f =
  funExt λ t →
  cong (equivFun (α₂ e) ∘ f) (invTransportStr α₁ τ₁ e t)
  ∙ τ₂ e (f (subst⁻ S (ua e) t))

-- Definition of structured equivalence using an action in the domain

FunctionEquivStr+ : {S : Type ℓ → Type ℓ₁} {T : Type ℓ → Type ℓ₂}
  → EquivAction S → StrEquiv T ℓ₂'
  → StrEquiv (FunctionStructure S T) (ℓ-max ℓ₁ ℓ₂')
FunctionEquivStr+ {S = S} {T} α₁ ι₂ (X , f) (Y , g) e =
  (s : S X) → ι₂ (X , f s) (Y , g (equivFun (α₁ e) s)) e

functionUnivalentStr+ : {S : Type ℓ → Type ℓ₁} {T : Type ℓ → Type ℓ₂}
  (α₁ : EquivAction S) (τ₁ : TransportStr α₁)
  (ι₂ : StrEquiv T ℓ₂') (θ₂ : UnivalentStr T ι₂)
  → UnivalentStr (FunctionStructure S T) (FunctionEquivStr+ α₁ ι₂)
functionUnivalentStr+ {S = S} {T} α₁ τ₁ ι₂ θ₂ {X , f} {Y , g} e =
  compEquiv
    (compEquiv
      (equivΠCod λ s →
        compEquiv
          (θ₂ e)
          (pathToEquiv (cong (PathP (λ i → T (ua e i)) (f s) ∘ g) (τ₁ e s))))
      (invEquiv heteroHomotopy≃Homotopy))
    funExtDepEquiv

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module examplesPaperJFP.triangleRightOperator where

_▹_    :  ∀{A B : Set} → A → (A → B) → B
a ▹ f  =  f a

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021 Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.PKCS
open import LibraBFT.Base.Types
open import LibraBFT.Prelude
import      LibraBFT.Yasm.Base   as LYB
import      LibraBFT.Yasm.System as LYS

-- This module provides a single import for all Yasm modules

module LibraBFT.Yasm.Yasm
   (ℓ-PeerState : Level)
   (ℓ-VSFP      : Level)
   (parms       : LYB.SystemTypeParameters ℓ-PeerState)
   (iiah  : LYB.SystemInitAndHandlers ℓ-PeerState parms)
   (ValidSenderForPK        : LYS.WithInitAndHandlers.ValidSenderForPK-type        ℓ-PeerState ℓ-VSFP parms iiah)
   (ValidSenderForPK-stable : LYS.WithInitAndHandlers.ValidSenderForPK-stable-type ℓ-PeerState ℓ-VSFP parms iiah ValidSenderForPK)
  where
 open LYB.SystemTypeParameters  parms
 open LYB.SystemInitAndHandlers iiah
 open import LibraBFT.Yasm.Base                                                                              public
 open import LibraBFT.Yasm.Types                                                                             public
 open import LibraBFT.Yasm.System     ℓ-PeerState ℓ-VSFP parms                                               public
 open import LibraBFT.Yasm.Properties ℓ-PeerState ℓ-VSFP parms iiah ValidSenderForPK ValidSenderForPK-stable public
 open        WithInitAndHandlers iiah                                                                        public
 open import Util.FunctionOverride    PeerId _≟PeerId_                                                       public

max_stars_repo_name: oracle/bft-consensus-agda

max_issues_repo_name: oracle/bft-consensus-agda

max_forks_repo_name: oracle/bft-consensus-agda


text:
{-# OPTIONS --cubical-compatible #-}
postulate
  A : Set
  B : A → Set

@0 T : Set
T = (@0 x : A) → B x

_ : Set₁
_ = (@0 A : Set) → @0 A → (@0 x : A) → Set

data D : Set₁ where
  @0 c : (@0 A : Set) → A → (x : A) → D


text:
------------------------------------------------------------------------------
-- Inductive Peano arithmetic base
------------------------------------------------------------------------------

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

module PA.Inductive.Base where

infixl 7 _*_
infixl 6 _+_

------------------------------------------------------------------------------
-- PA universe
open import PA.Inductive.Base.Core public

-- First-order logic (without equality)
--
open import Common.FOL.FOL public hiding ( _,_ ; ∃ )
-- 2012-04-24. Agda bug? Why it is necessary to use the modifier
-- @using@ in the following importation?
open import PA.Inductive.Existential public using ( _,_ ; ∃ )

-- The induction principle on the PA universe
ℕ-ind : (A : ℕ → Set) → A zero → (∀ n → A n → A (succ n)) → ∀ n → A n
ℕ-ind A A0 h zero     = A0
ℕ-ind A A0 h (succ n) = h n (ℕ-ind A A0 h n)

-- The identity type on the PA universe
open import PA.Inductive.Relation.Binary.PropositionalEquality public

-- PA primitive recursive functions
_+_ : ℕ → ℕ → ℕ
zero   + n = n
succ m + n = succ (m + n)

_*_ : ℕ → ℕ → ℕ
zero   * n = zero
succ m * n = n + m * n

------------------------------------------------------------------------------
-- ATPs helper
-- We don't traslate the body of functions, only the types. Therefore
-- we need to feed the ATPs with the functions' equations.

-- Addition axioms
+-0x : ∀ n → zero + n ≡ n
+-0x n = refl
-- {-# ATP hint +-0x #-}

+-Sx : ∀ m n → succ m + n ≡ succ (m + n)
+-Sx m n = refl
{-# ATP hint +-Sx #-}

-- Multiplication axioms
*-0x : ∀ n → zero * n ≡ zero
*-0x n = refl
-- {-# ATP hint *-0x #-}

*-Sx : ∀ m n → succ m * n ≡ n + m * n
*-Sx m n = refl
-- {-# ATP hint *-Sx #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

module Cubical.Algebra.MonoidSolver.Reflection where

open import Cubical.Foundations.Prelude hiding (Type)

open import Agda.Builtin.Reflection hiding (Type)
open import Agda.Builtin.String

open import Cubical.Reflection.Base

open import Cubical.Data.Maybe
open import Cubical.Data.Sigma
open import Cubical.Data.List
open import Cubical.Data.Nat
open import Cubical.Data.FinData using () renaming (zero to fzero; suc to fsuc)
open import Cubical.Data.Bool
open import Cubical.Data.Vec using (Vec) renaming ([] to emptyVec; _∷_ to _∷vec_) public

open import Cubical.Algebra.Monoid.Base
open import Cubical.Algebra.CommMonoid.Base
open import Cubical.Algebra.MonoidSolver.Solver renaming (solve to naiveSolve)
open import Cubical.Algebra.MonoidSolver.CommSolver renaming (solve to naiveCommSolve)
open import Cubical.Algebra.MonoidSolver.MonoidExpression

private
  variable
    ℓ : Level

module ReflectionSolver (op unit solver : Name) where

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

  record VarInfo : Type ℓ-zero where
    field
      varName : String
      varType : Arg Term
      index : ℕ

  {-
    `getLastTwoArgsOf` maps a term 'def n (z₁ ∷ … ∷ zₙ ∷ x ∷ y ∷ [])' to the pair '(x,y)'
    non-visible arguments are ignored.
  -}
  getLastTwoArgsOf : Name → Term → Maybe (Term × Term)
  getLastTwoArgsOf n' (def n xs) =
    if n == n'
    then go xs
    else nothing
      where
      go : List (Arg Term) → Maybe (Term × Term)
      go (varg x ∷ varg y ∷ []) = just (x , y)
      go (x ∷ xs)               = go xs
      go _                      = nothing
  getLastTwoArgsOf n' _ = nothing

  {-
    `getArgs` maps a term 'x ≡ y' to the pair '(x,y)'
  -}
  getArgs : Term → Maybe (Term × Term)
  getArgs = getLastTwoArgsOf (quote PathP)

  firstVisibleArg : List (Arg Term) → Maybe Term
  firstVisibleArg [] = nothing
  firstVisibleArg (varg x ∷ l) = just x
  firstVisibleArg (x ∷ l) = firstVisibleArg l

  {-
    If the solver needs to be applied during equational reasoning,
    the right hand side of the equation to solve cannot be given to
    the solver directly. The following function extracts this term y
    from a more complex expression as in:
      x ≡⟨ solve ... ⟩ (y ≡⟨ ... ⟩ z ∎)
  -}
  getRhs : Term → Maybe Term
  getRhs reasoningToTheRight@(def n xs) =
    if n == (quote _∎)
    then firstVisibleArg xs
    else (if n == (quote _≡⟨_⟩_)
         then firstVisibleArg xs
         else nothing)
  getRhs _ = nothing

  private
    solverCallAsTerm : Term → Arg Term → Term → Term → Term
    solverCallAsTerm M varList lhs rhs =
      def
         solver
         (varg M ∷ varg lhs ∷ varg rhs
           ∷ varList
           ∷ varg (def (quote refl) []) ∷ [])

  solverCallWithLambdas : ℕ → List VarInfo → Term → Term → Term → Term
  solverCallWithLambdas n varInfos M lhs rhs =
    encloseWithIteratedLambda
      (map VarInfo.varName varInfos)
      (solverCallAsTerm M (variableList (rev varInfos)) lhs rhs)
    where
      encloseWithIteratedLambda : List String → Term → Term
      encloseWithIteratedLambda (varName ∷ xs) t = lam visible (abs varName (encloseWithIteratedLambda xs t))
      encloseWithIteratedLambda [] t = t

      variableList : List VarInfo → Arg Term
      variableList [] = varg (con (quote emptyVec) [])
      variableList (varInfo ∷ varInfos)
        = varg (con (quote _∷vec_) (varg (var (VarInfo.index varInfo) []) ∷ (variableList varInfos) ∷ []))

  solverCallByVarIndices : ℕ → List ℕ → Term → Term → Term → Term
  solverCallByVarIndices n varIndices R lhs rhs =
      solverCallAsTerm R (variableList (rev varIndices)) lhs rhs
      where
        variableList : List ℕ → Arg Term
        variableList [] = varg (con (quote emptyVec) [])
        variableList (varIndex ∷ varIndices)
          = varg (con (quote _∷vec_) (varg (var (varIndex) []) ∷ (variableList varIndices) ∷ []))

  module _ (monoid : Term) where

    `ε⊗` : Term
    `ε⊗` = con (quote ε⊗) []

    mutual

      `_⊗_` : List (Arg Term) → Term
      `_⊗_` (harg _ ∷ xs) = `_⊗_` xs
      `_⊗_` (varg _ ∷ varg x ∷ varg y ∷ []) =
        con
          (quote _⊗_) (varg (buildExpression x) ∷ varg (buildExpression y) ∷ [])
      `_⊗_` _ = unknown

      finiteNumberAsTerm : ℕ → Term
      finiteNumberAsTerm ℕ.zero = con (quote fzero) []
      finiteNumberAsTerm (ℕ.suc n) = con (quote fsuc) (varg (finiteNumberAsTerm n) ∷ [])

      buildExpression : Term → Term
      buildExpression (var index _) = con (quote ∣) (varg (finiteNumberAsTerm index) ∷ [])
      buildExpression t@(def n xs) =
        if (n == op)
          then `_⊗_` xs
        else if (n == unit)
          then `ε⊗`
        else
          unknown
      buildExpression t = unknown

    toMonoidExpression : Maybe (Term × Term) → Maybe (Term × Term)
    toMonoidExpression nothing = nothing
    toMonoidExpression (just (lhs , rhs)) = just (buildExpression lhs , buildExpression rhs)

  adjustDeBruijnIndex : (n : ℕ) → Term → Term
  adjustDeBruijnIndex n (var k args) = var (k + n) args
  adjustDeBruijnIndex n _ = unknown

  extractVarIndices : Maybe (List Term) → Maybe (List ℕ)
  extractVarIndices (just ((var index _) ∷ l)) with extractVarIndices (just l)
  ... | just indices = just (index ∷ indices)
  ... | nothing = nothing
  extractVarIndices (just []) = just []
  extractVarIndices _ = nothing

  getVarsAndEquation : Term → Maybe (List VarInfo × Term)
  getVarsAndEquation t =
    let
      (rawVars , equationTerm) = extractVars t
      maybeVars = addIndices (length rawVars) rawVars
    in map-Maybe (_, equationTerm) maybeVars
    where
          extractVars : Term → List (String × Arg Term) × Term
          extractVars (pi argType (abs varName t)) with extractVars t
          ...                                         | xs , equation
                                                        = (varName , argType) ∷ xs , equation
          extractVars equation = [] , equation

          addIndices : ℕ → List (String × Arg Term) → Maybe (List VarInfo)
          addIndices ℕ.zero         []        = just []
          addIndices (ℕ.suc countVar) ((varName , argType) ∷ list) =
            map-Maybe (λ varList → record { varName = varName ; varType = argType ; index = countVar }
                                   ∷ varList)
                      (addIndices countVar list)
          addIndices _ _ = nothing

  toListOfTerms : Term → Maybe (List Term)
  toListOfTerms (con c []) = if (c == (quote [])) then just [] else nothing
  toListOfTerms (con c (varg t ∷ varg s ∷ args)) with toListOfTerms s
  ... | just terms = if (c == (quote _∷_)) then just (t ∷ terms) else nothing
  ... | nothing = nothing
  toListOfTerms (con c (harg t ∷ args)) = toListOfTerms (con c args)
  toListOfTerms _ = nothing

  solve-macro : Term → Term → TC Unit
  solve-macro monoid hole =
    do
      hole′ ← inferType hole >>= normalise
      just (varInfos , equation) ← returnTC (getVarsAndEquation hole′)
        where
          nothing
            → typeError (strErr "Something went wrong when getting the variable names in "
                           ∷ termErr hole′ ∷ [])
      {-
        The call to the monoid solver will be inside a lamba-expression.
        That means, that we have to adjust the deBruijn-indices of the variables in 'monoid'
      -}
      adjustedMonoid ← returnTC (adjustDeBruijnIndex (length varInfos) monoid)
      just (lhs , rhs) ← returnTC (toMonoidExpression adjustedMonoid (getArgs equation))
        where
          nothing
            → typeError(
                strErr "Error while trying to build ASTs for the equation " ∷
                termErr equation ∷ [])
      let solution = solverCallWithLambdas (length varInfos) varInfos adjustedMonoid lhs rhs
      unify hole solution

macro
  solveMonoid : Term → Term → TC _
  solveMonoid = ReflectionSolver.solve-macro (quote MonoidStr._·_) (quote MonoidStr.ε) (quote naiveSolve)

  solveCommMonoid : Term → Term → TC _
  solveCommMonoid = ReflectionSolver.solve-macro (quote CommMonoidStr._·_) (quote CommMonoidStr.ε) (quote naiveCommSolve)


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

open import Categories.Category using (Category; module Commutation)

-- The "four middle interchange" for monoidal categories.
--
-- Aka the "interchange law" or "exchange law" (though those terms are
-- more comonly used in the more general context of composition in
-- 2-categories).

-- Section 5.3 of the PhD thesis of Geoff Cruttwell states most (all?)
-- the properties in the module, starting on p. 57 (starting with Prop. 5.3.4).
-- It also has nice string-diagrammatic proofs.
--    See also further comments in https://github.com/agda/agda-categories/pull/294#issuecomment-897697009

module Categories.Category.Monoidal.Interchange
  {o ℓ e} {C : Category o ℓ e} where

open import Level using (_⊔_)

import Categories.Category.Monoidal.Construction.Product as MonoidalProduct
open import Categories.Category.Monoidal.Core using (Monoidal)
import Categories.Category.Monoidal.Utilities as MonoidalUtilities
open import Categories.Category.Product using (_⁂_)
open import Categories.Functor using (_∘F_)
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
open import Categories.Morphism C using (_≅_; module ≅)

open Category C using (Obj; id; _⇒_; _∘_; _≈_)
open Commutation C

private
  variable
    W W₁ W₂ X X₁ X₂ Y Y₁ Y₂ Z Z₁ Z₂ : Obj
    f g h i : X ⇒ Y

-- An abstract definition of an interchange map with the minimal set
-- of coherence laws required to make the tensor product ⊗ of C a
-- monoidal functor.  (See also Categories.Functor.Monoidal.Tensor.)

record HasInterchange (M : Monoidal C) : Set (o ⊔ ℓ ⊔ e) where
  open Monoidal M using (_⊗₀_; _⊗₁_; unit; ⊗)
  open MonoidalUtilities.Shorthands M using (α⇒; λ⇐; λ⇒; ρ⇒)

  -- The "four middle interchange" for tensor products.

  field swapInner : ∀ {W X Y Z} → (W ⊗₀ X) ⊗₀ (Y ⊗₀ Z) ≅ (W ⊗₀ Y) ⊗₀ (X ⊗₀ Z)

  module swapInner {W X Y Z} = _≅_ (swapInner {W} {X} {Y} {Z})
  private
    i⇒ = swapInner.from
    i⇐ = swapInner.to

  -- Naturality and coherence laws of the interchange.

  field
    natural : i⇒ ∘ (f ⊗₁ g) ⊗₁ (h ⊗₁ i) ≈ (f ⊗₁ h) ⊗₁ (g ⊗₁ i) ∘ i⇒

    assoc : [ ((X₁ ⊗₀ X₂) ⊗₀ (Y₁ ⊗₀ Y₂)) ⊗₀ (Z₁ ⊗₀ Z₂) ⇒
              (X₁ ⊗₀ (Y₁ ⊗₀ Z₁)) ⊗₀ (X₂ ⊗₀ (Y₂ ⊗₀ Z₂)) ]⟨
              i⇒ ⊗₁ id   ⇒⟨ ((X₁ ⊗₀ Y₁) ⊗₀ (X₂ ⊗₀ Y₂)) ⊗₀ (Z₁ ⊗₀ Z₂) ⟩
              i⇒         ⇒⟨ ((X₁ ⊗₀ Y₁) ⊗₀ Z₁) ⊗₀ ((X₂ ⊗₀ Y₂) ⊗₀ Z₂) ⟩
              α⇒ ⊗₁ α⇒
            ≈ α⇒         ⇒⟨ (X₁ ⊗₀ X₂) ⊗₀ ((Y₁ ⊗₀ Y₂) ⊗₀ (Z₁ ⊗₀ Z₂)) ⟩
              id ⊗₁ i⇒   ⇒⟨ (X₁ ⊗₀ X₂) ⊗₀ ((Y₁ ⊗₀ Z₁) ⊗₀ (Y₂ ⊗₀ Z₂)) ⟩
              i⇒
            ⟩

    unitˡ : [ unit ⊗₀ (X ⊗₀ Y) ⇒ (X ⊗₀ Y) ]⟨
              λ⇐ ⊗₁ id   ⇒⟨ (unit ⊗₀ unit) ⊗₀ (X ⊗₀ Y) ⟩
              i⇒         ⇒⟨ (unit ⊗₀ X) ⊗₀ (unit ⊗₀ Y) ⟩
              λ⇒ ⊗₁ λ⇒
            ≈ λ⇒
            ⟩

    unitʳ : [ (X ⊗₀ Y) ⊗₀ unit ⇒ (X ⊗₀ Y) ]⟨
              id ⊗₁ λ⇐   ⇒⟨ (X ⊗₀ Y) ⊗₀ (unit ⊗₀ unit) ⟩
              i⇒         ⇒⟨ (X ⊗₀ unit) ⊗₀ (Y ⊗₀ unit) ⟩
              ρ⇒ ⊗₁ ρ⇒
            ≈ ρ⇒
            ⟩

  -- The interchange is a natural isomorphism.

  naturalIso : ⊗ ∘F (⊗ ⁂ ⊗) ≃ ⊗ ∘F MonoidalProduct.⊗ M M
  naturalIso = niHelper (record
    { η       = λ _ → i⇒
    ; η⁻¹     = λ _ → i⇐
    ; commute = λ _ → natural
    ; iso     = λ _ → swapInner.iso
    })

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:
postulate A : Set

data D : Set where
  c : A → D

data P : D → Set where
  d : (x : A) → P (c x)

g : (x : D) → P x → D
g blargh (d y) with Set
g glurph (d y) | w = {!!}
  -- Expected: glurph = c y : D, y : A, w : Set₁

h : D → D
h x@(c y) with Set
h (c z) | w = {!!}
  -- Expected: z : A, w : Set₁

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
-- 2018-05-25, Reported by Sergei Meshveliani on the Agda list

open import Common.Prelude

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B

f : List (Nat × Nat) → List (Nat × Nat)
f ps =
     map (\p → let (x , y) = p in (x , suc y))  ps


text:
module Esterel.CompletionCode where

open import Data.Nat
  using (ℕ ; zero ; suc) renaming (_≟_ to _≟ℕ_ ; _⊔_ to _⊔ℕ_ ; _≤_ to _≤N_ ; _≤?_ to _≤?N_)
open import Data.Nat.Properties
  using (⊔-⊓-isCommutativeSemiringWithoutOne)
open import Function
  using (_∘_)
open import Relation.Nullary
  using (Dec ; yes ; no)
open import Relation.Binary
  using (Decidable)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; cong)
import Level
import Relation.Binary
open import Data.List using (List ; _∷_ ; [] ; _++_)
open import Data.List.Any.Properties using (++⁻)
  renaming (++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ)
open import Data.Sum using (_⊎_ ; inj₁ ; inj₂)
open import Data.Empty using (⊥-elim)
import Data.Bool
open import Algebra.Structures
  using (IsCommutativeSemiringWithoutOne ; IsCommutativeMonoid)

open import utility

data CompletionCode : Set where
  nothin : CompletionCode
  pause  : CompletionCode
  exit   : ℕ → CompletionCode

↓* : CompletionCode → CompletionCode
↓* nothin         = nothin
↓* pause          = pause
↓* (exit zero)    = nothin
↓* (exit (suc n)) = exit n

exit-injective : ∀{n m} → exit n ≡ exit m → n ≡ m
exit-injective refl = refl

_≟_ : Decidable {A = CompletionCode} _≡_
nothin ≟ nothin = yes refl
nothin ≟ pause  = no λ()
nothin ≟ exit _ = no λ()
pause  ≟ nothin = no λ()
pause  ≟ pause  = yes refl
pause  ≟ exit _ = no λ()
exit _ ≟ nothin = no λ()
exit _ ≟ pause  = no λ()
exit n ≟ exit m with n ≟ℕ m
... | yes n≡m = yes (cong exit n≡m)
... | no ¬n≡m = no (¬n≡m ∘ exit-injective)

open ListSet _≟_

_⊔_ : CompletionCode → CompletionCode → CompletionCode
nothin ⊔ r      = r
pause  ⊔ nothin = pause
pause  ⊔ r      = r
exit n ⊔ nothin = exit n
exit n ⊔ pause  = exit n
exit n ⊔ exit m = exit (n ⊔ℕ m)

⊔-comm : ∀ c₁ c₂ → c₁ ⊔ c₂ ≡ c₂ ⊔ c₁
⊔-comm nothin   nothin   = refl
⊔-comm nothin   pause    = refl
⊔-comm nothin   (exit m) = refl
⊔-comm pause    nothin   = refl
⊔-comm pause    pause    = refl
⊔-comm pause    (exit m) = refl
⊔-comm (exit n) nothin   = refl
⊔-comm (exit n) pause    = refl
⊔-comm (exit n) (exit m)
  rewrite IsCommutativeMonoid.comm
            (IsCommutativeSemiringWithoutOne.+-isCommutativeMonoid
              ⊔-⊓-isCommutativeSemiringWithoutOne) n m
  = refl

data _≤_ : Relation.Binary.Rel CompletionCode Level.zero where
  nothin≤c     : ∀ {c}                 -> nothin ≤ c
  pause≤pause  :                          pause  ≤ pause
  pause≤exit   : ∀ {n}                 -> pause  ≤ exit n
  exit≤exit    : ∀ {n} {m} -> (n ≤N m) -> exit n ≤ exit m

_≤?_ : Decidable _≤_
nothin ≤? c2 = yes nothin≤c
pause ≤? nothin = no (λ ())
pause ≤? pause = yes pause≤pause
pause ≤? exit x = yes pause≤exit
exit n ≤? nothin = no (λ ())
exit n ≤? pause = no (λ ())
exit n ≤? exit m with n ≤?N m
exit n ≤? exit m | yes n≤m = yes (exit≤exit n≤m)
exit n ≤? exit m | no ¬n≤m = no ¬≤ where
  ¬≤ : Relation.Nullary.¬ (exit n ≤ exit m)
  ¬≤ (exit≤exit n) = ¬n≤m n

codessub : (List CompletionCode) → (List CompletionCode) → Set
codessub codes' codes = (∀ a → a ∈ codes' → a ∈ codes)
codesub++ll : ∀{a b c} →  codessub a b → codessub a (b ++ c)
codesub++ll sub a a∈ = ++ˡ (sub a a∈)

codesub++both : ∀{a b c d} →  codessub a c → codessub b d → codessub (a ++ b) (c ++ d)
codesub++both{a}{b}{c}{d} a⊂c b⊂d z z∈ with ++⁻ a z∈
... | inj₁ z∈1 = ++ˡ (a⊂c z z∈1)
... | inj₂ z∈2 = ++ʳ c (b⊂d z z∈2)

codesub- : ∀{a b} z → codessub a b → codessub (set-remove a z) (set-remove b z)
codesub-{a}{b} z a⊂b x x∈ with z ≟ x
... | yes refl = ⊥-elim (set-remove-removed{x}{a} x∈)
... | no ¬refl = set-remove-not-removed ¬refl (a⊂b x (set-remove-mono-∈ z x∈))

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text: mmodule silly1 where

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Values where

open import Data.Bool
open import Data.List
open import Data.List.All
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality

open import Typing
open import Syntax
open import Global
open import Channel

mutual
-- a value indexed by a *relevant* session context, which is "used up" by the value
  data Val (G : SCtx) : Type → Set where
    VUnit : (inaG : Inactive G)
      → Val G TUnit
    VInt  : (i : ℕ)
      → (inaG : Inactive G)
      → Val G TInt
    VPair : ∀ {t₁ t₂ G₁ G₂}
      → (ss-GG₁G₂ : SSplit G G₁ G₂)
      → (v₁ : Val G₁ t₁)
      → (v₂ : Val G₂ t₂)
      → Val G (TPair t₁ t₂)
    VChan : ∀ {s}
      → (ce : ChannelEnd)
      → (cr : ChannelRef G ce s)
      → Val G (TChan s)
    VFun : ∀ {φ lu t₁ t₂}
      → (lu ≡ LL ⊎ All Unr φ)
      → (ϱ : VEnv G φ)
      → (e : Expr (t₁ ∷ φ) t₂)
      → Val G (TFun lu t₁ t₂)

  -- type environment-indexed value environment
  -- session context G describes the entire environment, it splits over all (channel) values
  data VEnv (G : SCtx) : TCtx → Set where
    vnil : (ina : Inactive G) → VEnv G []
    vcons : ∀{t φ G₁ G₂} → (ssp : SSplit G G₁ G₂) → (v : Val G₁ t) → (ϱ : VEnv G₂ φ) → VEnv G (t ∷ φ)

unrestricted-val :  ∀ {t G} → Unr t → Val G t → Inactive G
unrestricted-venv : ∀ {φ G} → All Unr φ → VEnv G φ → Inactive G

unrestricted-val UUnit (VUnit x) = x
unrestricted-val UInt (VInt i x) = x
unrestricted-val (UPair unrt unrt₁) (VPair x v v₁) =
  ssplit-inactive x (unrestricted-val unrt v) (unrestricted-val unrt₁ v₁)
unrestricted-val {TFun UU t₁ t₂} UFun (VFun (inj₁ ()) ϱ e)
unrestricted-val {TFun UU t₁ t₂} UFun (VFun (inj₂ unr-φ) ϱ e) = unrestricted-venv unr-φ ϱ

unrestricted-venv unr-φ (vnil ina) = ina
unrestricted-venv (px ∷ unr-φ) (vcons ssp v ϱ) =
  ssplit-inactive ssp (unrestricted-val px v) (unrestricted-venv unr-φ ϱ)

-- access a value in an indexed environment
access : ∀ {φ t} {G : SCtx} → VEnv G φ → t ∈ φ → ∃ λ G₁ → ∃ λ G₂ → Inactive G₂ × SSplit G G₁ G₂ × Val G₁ t
access (vcons ssp v ϱ) (here allUnr) =  _ , _ , unrestricted-venv allUnr ϱ , ssp , v
access (vcons ssp x₀ ϱ) (there unrX₀ x) with access ϱ x
access (vcons ssp x₀ ϱ) (there unrX₀ x) | G₁ , G₂ , inaG₂ , ssp12 , v with ssplit-compose4 ssp ssp12
... | Gi , ssp1 , ssp2 = G₁ , Gi , ssplit-inactive ssp2 (unrestricted-val unrX₀ x₀) inaG₂ , ssp1 , v

-- coerce a value to a supertype
coerce : ∀ {G t t'} → Val G t → SubT t t' → Val G t'
coerce (VUnit inaG) sub-unit = VUnit inaG
coerce (VInt i inaG) sub-int = VInt i inaG
coerce (VPair ss-GG₁G₂ v v₁) (sub-pair t≤t' t≤t'') = VPair ss-GG₁G₂ (coerce v t≤t') (coerce v₁ t≤t'')
coerce (VChan b vcr) (sub-chan s≲s') = VChan b (vcr-coerce vcr s≲s')
coerce (VFun lu ϱ e) (sub-fun t≤t' t≤t'') = VFun lu ϱ (expr-coerce e t≤t'' t≤t')

rewrite-ssplit : ∀ {G G' G₁ G₂} → G ≡ G' → SSplit G G₁ G₂ → SSplit G' G₁ G₂
rewrite-ssplit p ssp rewrite p = ssp

rewrite-ssplit1 : ∀ {G G₁ G₁' G₂} → G₁ ≡ G₁' → SSplit G G₁ G₂ → SSplit G G₁' G₂
rewrite-ssplit1 p ssp rewrite p = ssp

-- split environment according to type context split
split-env : ∀ {Φ Φ₁ Φ₂} {G : SCtx}
  → Split Φ Φ₁ Φ₂
  → VEnv G Φ
  → Σ (SCtx × SCtx) λ { (G₁ , G₂) → SSplit G G₁ G₂ × VEnv G₁ Φ₁ × VEnv G₂ Φ₂ }
split-env{G = G} [] (vnil ina) =  (G , G) , inactive-ssplit-trivial ina , vnil ina , vnil ina
split-env (dupl unrt sp) (vcons ssp v ϱ) with split-env sp ϱ | unrestricted-val unrt v
split-env (dupl unrt sp) (vcons ssp v ϱ) | (G₁' , G₂') , ssp12 , ϱ₁' , ϱ₂' | unr-v rewrite inactive-left-ssplit ssp unr-v with ssplit-compose4 ssp ssp12 | ssplit-compose3 ssp ssp12
... | Gi , ssp-GG1Gi , ssp-GiG1G2' | Gi-1 , ssp-GGiG2' , ssp-GiG1G1' =
  let p₁ = (inactive-left-ssplit ssp-GiG1G1' unr-v) in
  let p₂ = (inactive-left-ssplit ssp-GiG1G2' unr-v) in
  (G₁' , G₂') ,  ssp12 , vcons (rewrite-ssplit p₁ ssp-GiG1G1') v ϱ₁' , vcons (rewrite-ssplit p₂ ssp-GiG1G2') v ϱ₂'
split-env (drop px sp) (vcons ssp v ϱ)
  rewrite inactive-left-ssplit ssp (unrestricted-val px v)
  = split-env sp ϱ
split-env (left sp) (vcons ssp v ϱ) with split-env sp ϱ
split-env{G = G} (left sp) (vcons ssp v ϱ) | (G₁' , G₂') , ssp12 , ϱ₁' , ϱ₂' with ssplit-compose3 ssp ssp12
... | Gi , ssp-GiG2' , ssp-GiG1G1' = (Gi , G₂') , ssp-GiG2' , vcons ssp-GiG1G1' v ϱ₁' , ϱ₂'
split-env (rght sp) (vcons ssp v ϱ) with split-env sp ϱ
split-env (rght sp) (vcons ssp v ϱ) | (G₁' , G₂') , ssp12 , ϱ₁' , ϱ₂' with ssplit-compose4 ssp ssp12
...| Gi , ssp-GG1'Gi , ssp-GiG1G2' = (G₁' , Gi) , ssp-GG1'Gi , ϱ₁' , vcons ssp-GiG1G2' v ϱ₂'

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.IsEquivalence
open import Oscar.Data.𝟙

module Oscar.Class.HasEquivalence where

module _
  {𝔬} (𝔒 : Ø 𝔬) ℓ
  where
  𝔥asEquivalence : Rℭlass 𝟙
  𝔥asEquivalence = ∁ (𝔒 → 𝔒 → Ø ℓ) IsEquivalence
  open Rℭlass 𝔥asEquivalence using () renaming (GET-CLASS to HasEquivalence) public

module _
  {𝔬} (𝔒 : Ø 𝔬) {ℓ}
  where
  open Rℭlass (𝔥asEquivalence 𝔒 ℓ) using () renaming (GET-METHOD to Equivalence[_]) public

infix 4 ≈-syntax
≈-syntax = Equivalence[_]
syntax ≈-syntax 𝔒 x y = x ≈[ 𝔒 ] y

module _
  {𝔬} {𝔒 : Ø 𝔬} {ℓ}
  where
  open Rℭlass (𝔥asEquivalence 𝔒 ℓ) using () renaming (GET-METHOD to Equivalence) public

infix 4 _≈_
_≈_ = Equivalence


text:
  module _ where

  module A where

    postulate C : Set → Set → Set

    syntax C X Y = X , Y

  module B where

    postulate C : Set

  open A
  open B

  Foo : Set → Set
  Foo X = X , X


text:
open import Type
open import Structure.Relator
open import Structure.Setoid renaming (_≡_ to _≡ₑ_)

module Structure.Sets.Quantifiers.Proofs {ℓₛ ℓₗ ℓₑ} {S : Type{ℓₛ}} ⦃ equiv : Equiv{ℓₑ}(S) ⦄ (_∈_ : S → S → Type{ℓₗ}) ⦃ [∈]-binaryRelator : BinaryRelator(_∈_) ⦄ where

import      Lvl
open import Structure.Relator.Proofs renaming ([≡]-binaryRelator to [≡ₑ]-binaryRelator)
open import Structure.Sets.Quantifiers(_∈_)
open import Syntax.Function

private variable ℓ : Lvl.Level
private variable A : S

[∃ₛ]-unaryRelator : ∀{P : S → S → Type{ℓ}} → ⦃ rel-P : ∀{x} → UnaryRelator(P(x)) ⦄ → UnaryRelator(\y → ∃ₛ(A)(x ↦ P(x)(y)))
[∃ₛ]-unaryRelator = [∃]-unaryRelator ⦃ rel-P = [∧]-unaryRelator ⦄

[∀ₛ]-unaryRelator : ∀{P : S → S → Type{ℓ}} → ⦃ rel-P : ∀{x} → UnaryRelator(P(x)) ⦄ → UnaryRelator(\y → ∀ₛ(A)(x ↦ P(x)(y)))
[∀ₛ]-unaryRelator = [∀]-unaryRelator ⦃ rel-P = [→]-unaryRelator ⦄

[∃ₛ]-binaryRelator : ∀{P : S → S → S → Type{ℓ}} → ⦃ rel-P : ∀{x} → BinaryRelator(P(x)) ⦄ → BinaryRelator(\A y → ∃ₛ(A)(x ↦ P(x)(A)(y)))
[∃ₛ]-binaryRelator = binaryRelator-from-unaryRelator
  ⦃ relₗ = [∃]-unaryRelator ⦃ rel-P = [∧]-unaryRelator ⦃ rel-P = binary-unaryRelatorₗ ⦄ ⦃ rel-Q = binary-unaryRelatorᵣ ⦄ ⦄ ⦄
  ⦃ relᵣ = [∃]-unaryRelator ⦃ rel-P = [∧]-unaryRelator ⦃ rel-Q = binary-unaryRelatorₗ ⦄ ⦄ ⦄

[∀ₛ]-binaryRelator : ∀{P : S → S → S → Type{ℓ}} → ⦃ rel-P : ∀{x} → BinaryRelator(P(x)) ⦄ → BinaryRelator(\A y → ∀ₛ(A)(x ↦ P(x)(A)(y)))
[∀ₛ]-binaryRelator = binaryRelator-from-unaryRelator
  ⦃ relₗ = [∀]-unaryRelator ⦃ rel-P = [→]-unaryRelator ⦃ rel-P = binary-unaryRelatorₗ ⦄ ⦃ rel-Q = binary-unaryRelatorᵣ ⦄ ⦄ ⦄
  ⦃ relᵣ = [∀]-unaryRelator ⦃ rel-P = [→]-unaryRelator ⦃ rel-Q = binary-unaryRelatorₗ ⦄ ⦄ ⦄

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 --erased-cubical #-}

module Midi where

open import Agda.Builtin.String using (String)
open import Data.Fin using (toℕ)
open import Data.Nat using (ℕ)
open import Data.List using (List; []; _∷_; concatMap)
open import Data.Product using (_,_)
open import Data.Unit using (⊤)

open import MidiEvent using (Tick; MidiEvent; midiEvent; MidiTrack; track)

{-# FOREIGN GHC
  import System.Environment (getArgs)
  import Codec.Midi
  import Data.Text (Text, unpack, pack)
  import Data.List (sort, map)
  import Text.Read (readMaybe)

  type HsTicksPerBeat = Integer
  type HsTicks        = Integer
  type HsKey          = Integer
  type HsVelocity     = Integer
  type HsPreset       = Integer
  type HsChannel      = Integer
  type HsTempo        = Integer

  type HsAbsTime      = Integer

  type HsTrackName    = Text

  -- convert beats per minute to microseconds per beat
  bpmToTempo :: Int -> Tempo
  bpmToTempo bpm = round $ 1000000 * 60 / fromIntegral bpm

  data HsMidiMessage = HsNoteOn HsVelocity HsTicks HsKey | HsNoteOff HsVelocity HsTicks HsKey
    deriving Eq

  getTicks :: HsMidiMessage -> HsTicks
  getTicks (HsNoteOn  _ t _) = t
  getTicks (HsNoteOff _ t _) = t

  instance Ord HsMidiMessage where
    a <= b = getTicks a <= getTicks b

  data HsMidiTrack = HsMidiTrack HsTrackName HsPreset HsChannel HsTempo [HsMidiMessage]

  fi = fromInteger

  makeTrack :: Channel -> HsAbsTime -> [HsMidiMessage] -> (Track Ticks , HsAbsTime)
  makeTrack c t []                      = ([(0, TrackEnd)], t)
  makeTrack c t (HsNoteOn  v t' k : ms) = let (rest, t'') = makeTrack c t' ms
                                          in ((fi (t' - t), NoteOn  c (fi k) (fi v)) : rest, t'')
  makeTrack c t (HsNoteOff v t' k : ms) = let (rest, t'') = makeTrack c t' ms
                                          in ((fi (t' - t), NoteOff c (fi k) (fi v)) : rest, t'')

  toTrack :: HsMidiTrack -> Track Ticks
  toTrack (HsMidiTrack name preset channel tempo messages) =
    (0, TrackName (unpack name)) :
    (0, ProgramChange (fi channel) (fi preset)) :
    (0, TempoChange (bpmToTempo (fi tempo))) :
    fst (makeTrack (fi channel) 0 (sort messages))

  toMidi :: HsTicksPerBeat -> [HsMidiTrack] -> Midi
  toMidi ticks tracks = let mtracks = map toTrack tracks
                        in Midi MultiTrack (TicksPerBeat (fi ticks)) mtracks

  exportTracks :: Text -> HsTicksPerBeat -> [HsMidiTrack] -> IO ()
  exportTracks filePath ticksPerBeat tracks = do
    let path = unpack filePath
    --putStrLn $ "Writing file " ++ path
    --putStrLn $ show $ toMidi ticksPerBeat tracks
    exportFile path (toMidi ticksPerBeat tracks)

  -- Returns n+1 if s parses as natural number n, or 0 for any failure
  readNat :: Text -> Integer
  readNat s = case (readMaybe (unpack s) :: Maybe Integer) of
    Just n  -> if n >= 0 then n+1 else 0
    Nothing -> 0
#-}

postulate
  IO       : Set → Set
  putStrLn : String -> IO ⊤
  getArgs  : IO (List String)
  _>>=_    : {A B : Set} -> IO A -> (A -> IO B) -> IO B

{-# BUILTIN IO IO #-}
{-# COMPILE GHC IO = type IO #-}

{-# COMPILE GHC putStrLn = putStrLn . unpack #-}
{-# COMPILE GHC getArgs = fmap (fmap pack) getArgs #-}
{-# COMPILE GHC _>>=_ = \_ _ -> (>>=) :: IO a -> (a -> IO b) -> IO b #-}

FilePath = String

data Pair (A : Set) (B : Set) : Set where
  pair : A → B → Pair A B

{-# COMPILE GHC Pair = data (,) ((,)) #-}

HInstrument HPitch HVelocity : Set
HInstrument = ℕ
HPitch      = ℕ
HVelocity   = ℕ
HChannel    = ℕ
HTempo      = ℕ

data MidiMessage : Set where
  noteOn  : HVelocity → Tick → HPitch → MidiMessage
  noteOff : HVelocity → Tick → HPitch → MidiMessage

{-# COMPILE GHC MidiMessage = data HsMidiMessage (HsNoteOn | HsNoteOff) #-}

event→messages : MidiEvent → List MidiMessage
event→messages (midiEvent p start stop v) =
  let v' = toℕ v
  in noteOn v' start p ∷ noteOff v' stop p ∷ []

data HMidiTrack : Set where
  htrack : String → HInstrument → HChannel → HTempo → List MidiMessage → HMidiTrack

{-# COMPILE GHC HMidiTrack = data HsMidiTrack (HsMidiTrack) #-}

track→htrack : MidiTrack → HMidiTrack
track→htrack (track n i c t m) = htrack n (toℕ i) (toℕ c) t (concatMap event→messages m)

postulate
  exportTracks : FilePath        → -- path to the file to save the MIDI data to
                 ℕ               → -- number of ticks per beat (by default a beat is a quarter note)
                 List HMidiTrack → -- tracks, one per instrument
                 IO ⊤

{-# COMPILE GHC exportTracks = exportTracks #-}

postulate
  readNat : String → ℕ

{-# COMPILE GHC readNat = readNat #-}

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
module ParseTree where
open import Data.String
open import Data.Nat
open import Data.Bool
open import Data.List
{-# FOREIGN GHC import ParseTree #-}

data ParseTree : Set
data TypeSignature : Set
data Expr : Set
data Range : Set
data Identifier : Set
data RangePosition : Set
data Pragma : Set
data Comment : Set

data ParseTree where
  signature : (signature : TypeSignature) -> (range : Range) -> ParseTree
  functionDefinition : (definitionOf : Identifier) -> (params : List Expr) -> (body : Expr) -> (range : Range) -> ParseTree
  dataStructure : (dataName : Identifier) -> (parameters : List TypeSignature) -> (indexInfo : Expr) -> (constructors : List TypeSignature) -> (range : Range) -> {comments : List (List Comment)} -> ParseTree
  pragma : (pragma : Pragma) -> (range : Range) -> ParseTree
  openImport : (opened : Bool) -> (imported : Bool) -> (moduleName : Identifier) -> (range : Range) -> {comments : List (List Comment)} -> ParseTree
  moduleName : (moduleName : Identifier) -> (range : Range) -> ParseTree

{-# COMPILE GHC ParseTree = data ParseTree
( Signature
| FunctionDefinition
| DataStructure
| Pragma
| OpenImport
| ModuleName
) #-}

data TypeSignature where
  typeSignature : (funcName : Identifier) -> (funcType : Expr) -> TypeSignature

{-# COMPILE GHC TypeSignature = data TypeSignature
( TypeSignature
) #-}

data Expr where
  numLit : {value : ℕ} -> {position : Range} -> {commentsBef : List Comment} -> {commentsAf : List Comment} -> Expr
  ident : (identifier : Identifier) -> Expr
  hole : {textInside : String} -> {position : Range} -> {commentsBef : List Comment} -> {commentsAf : List Comment} -> Expr
  functionApp : (firstPart : Expr) -> (secondPart : Expr) -> {isType : Bool} -> Expr
  implicit : (expr : Expr) -> Expr
  underscore : {position : Range} -> {commentsBef : List Comment} -> {commentsAf : List Comment} -> Expr
  namedArgument : (arg : TypeSignature) -> {explicit : Bool} -> {commentsBef : List Comment} -> {commentsAf : List Comment} -> Expr

{-# COMPILE GHC Expr = data Expr
( NumLit
| Ident
| Hole
| FunctionApp
| Implicit
| Underscore
| NamedArgument
) #-}

data Range where
  range : (lastUnaffected : ℕ) -> (lastAffected : ℕ) -> Range

{-# COMPILE GHC Range = data Range
( Range
) #-}

data Identifier where
  identifier : (name : String) -> (isInRange : (ℕ -> RangePosition)) -> (scope : ℕ) -> (declaration : ℕ) -> {inScope : Bool} -> {commentsBefore : List Comment} -> {commentsAfter : List Comment} -> Identifier

{-# COMPILE GHC Identifier = data Identifier
( Identifier
) #-}

data RangePosition where
  before : RangePosition
  inside : RangePosition
  after : RangePosition

{-# COMPILE GHC RangePosition = data RangePosition
( Before
| Inside
| After
) #-}

data Pragma where
  builtin : (concept : String) -> (definition : Identifier) -> Pragma
  option : (opts : List String) -> Pragma

{-# COMPILE GHC Pragma = data Pragma
( Builtin
| Option
) #-}

data Comment where
  comment : {content : String} -> {codePos : Range} -> {isMultiLine : Bool} -> Comment

{-# COMPILE GHC Comment = data Comment
( Comment
) #-}


text:
module Web.Semantic.DL.Category.Properties.Tensor where

open import Web.Semantic.DL.Category.Properties.Tensor.RespectsEquiv public using
  ( tensor-resp-≣ )

open import Web.Semantic.DL.Category.Properties.Tensor.Functor public using
  ( tensor-resp-id ; tensor-resp-compose )

open import Web.Semantic.DL.Category.Properties.Tensor.Isomorphisms public using
  ( symm-iso ; assoc-iso ; assoc⁻¹-iso
  ; unit₁-iso ; unit₁⁻¹-iso ; unit₂-iso ; unit₂⁻¹-iso )

open import Web.Semantic.DL.Category.Properties.Tensor.Coherence public using
  ( assoc-unit ; assoc-assoc ; assoc-symm )

open import Web.Semantic.DL.Category.Properties.Tensor.UnitNatural public using
  ( unit₁-natural ; unit₂-natural )

open import Web.Semantic.DL.Category.Properties.Tensor.SymmNatural public using
  ( symm-natural )

open import Web.Semantic.DL.Category.Properties.Tensor.AssocNatural public using
  ( assoc-natural )

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic