text:
-- Andreas, 2016-10-11, AIM XXIV, issue #2248
-- COMPILED_TYPE should only work on postulates

data Unit : Set where
  unit : Unit

postulate
  IO : Set → Set

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

abstract
  IO' : Set → Set
  IO' A = A

  doNothing : IO' Unit
  doNothing = unit

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

postulate
  toIO : {A : Set} → IO' A → IO A

{-# COMPILE GHC toIO = \ _ x -> x #-}

main : IO Unit
main = toIO doNothing

max_stars_repo_name: Blaisorblade/Agda

max_issues_repo_name: Blaisorblade/Agda

max_forks_repo_name: Blaisorblade/Agda


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

open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Naturals
open import Numbers.Naturals.EuclideanAlgorithm
open import Semirings.Definition
open import Orders.Total.Definition

module Numbers.Modulo.ModuloFunction where

open TotalOrder ℕTotalOrder

private
  notBigger : (a : ℕ) {n : ℕ} → succ a +N n ≡ a → False
  notBigger (succ a) {n} pr = notBigger a {n} (succInjective pr)

  notBigger' : (a : ℕ) {n : ℕ} → succ a +N n ≡ n → False
  notBigger' (succ a) {succ n} pr rewrite Semiring.commutative ℕSemiring a (succ n) | Semiring.commutative ℕSemiring n a = notBigger' _ (succInjective pr)

mod : (n : ℕ) → .(pr : 0 <N n) → (a : ℕ) → ℕ
mod (succ n) 0<n a = divisionAlgResult.rem (divisionAlg (succ n) a)

abstract
  modIsMod : {n : ℕ} → .(pr : 0 <N n) → (a : ℕ) → a <N n → mod n pr a ≡ a
  modIsMod {succ n} 0<n a a<n with divisionAlg (succ n) a
  modIsMod {succ n} 0<n a a<n | record { quot = zero ; rem = rem ; pr = pr ; remIsSmall = remIsSmall ; quotSmall = quotSmall } rewrite multiplicationNIsCommutative n 0 = pr
  modIsMod {succ n} 0<n a (le x proof) | record { quot = succ quot ; rem = rem ; pr = pr ; remIsSmall = inl rem<sn ; quotSmall = quotSmall } = exFalso (notBigger a v)
    where
      t : ((succ (a +N x)) *N succ quot) +N rem ≡ a
      t rewrite Semiring.commutative ℕSemiring a x = transitivity (applyEquality (λ i → (i *N succ quot) +N rem) proof) pr
      u : (succ quot *N succ (a +N x)) +N rem ≡ a
      u = transitivity (applyEquality (_+N rem) (multiplicationNIsCommutative (succ quot) _)) t
      v : succ a +N ((x +N quot *N succ (a +N x)) +N rem) ≡ a
      v = transitivity (applyEquality succ (transitivity (Semiring.+Associative ℕSemiring a _ rem) (applyEquality (_+N rem) (Semiring.+Associative ℕSemiring a x _)))) u

  mod<N : {n : ℕ} → .(pr : 0 <N n) → (a : ℕ) → (mod n pr a) <N n
  mod<N {succ n} pr a with divisionAlg (succ n) a
  mod<N {succ n} 0<n a | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl x ; quotSmall = quotSmall } = x

  modIdempotent : {n : ℕ} → .(pr : 0 <N n) → (a : ℕ) → mod n pr (mod n pr a) ≡ mod n pr a
  modIdempotent 0<n a = modIsMod 0<n (mod _ 0<n a) (mod<N 0<n a)

  modAnd+n : {n : ℕ} → .(pr : 0 <N n) → (a : ℕ) → mod n pr (n +N a) ≡ mod n pr a
  modAnd+n {succ n} 0<sn a with divisionAlg (succ n) (succ n +N a)
  modAnd+n {succ n} 0<sn a | record { quot = 0 ; rem = rem ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = inl q } rewrite multiplicationNIsCommutative n 0 | pr = exFalso (notBigger (succ n) (transitivity (applyEquality succ (transitivity (applyEquality succ (Semiring.+Associative ℕSemiring n a _)) (Semiring.commutative ℕSemiring (succ (n +N a)) _))) (_<N_.proof remIsSmall)))
  modAnd+n {succ n} 0<sn a | record { quot = succ quot ; rem = rem ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = inl q } = modIsUnique (record { quot = quot ; rem = rem ; pr = t ; remIsSmall = inl remIsSmall ; quotSmall = inl q }) (divisionAlg (succ n) a)
    where
      g : succ n +N ((quot *N succ n) +N rem) ≡ succ n +N a
      g = transitivity (Semiring.+Associative ℕSemiring (succ n) _ rem) (transitivity (applyEquality (_+N rem) (multiplicationNIsCommutative (succ quot) _)) pr)
      h : (quot *N succ n) +N rem ≡ a
      h = canSubtractFromEqualityLeft g
      t : (succ n *N quot) +N rem ≡ a
      t = transitivity (applyEquality (_+N rem) (multiplicationNIsCommutative (succ n) quot)) h

  modExtracts : {n : ℕ} → .(pr : 0 <N n) → (a b : ℕ) → mod n pr (a +N b) ≡ mod n pr (mod n pr a +N mod n pr b)
  modExtracts {succ n} 0<sn a b with divisionAlg (succ n) a
  modExtracts {succ n} 0<sn a b | record { quot = sn/a ; rem = sn%a ; pr = prA ; remIsSmall = remIsSmallA ; quotSmall = quotSmallA } with divisionAlg (succ n) b
  modExtracts {succ n} 0<sn a b | record { quot = sn/a ; rem = sn%a ; pr = prA ; remIsSmall = remIsSmallA ; quotSmall = quotSmallA } | record { quot = sn/b ; rem = sn%b ; pr = prB ; remIsSmall = remIsSmallB ; quotSmall = quotSmallB } with divisionAlg (succ n) (a +N b)
  modExtracts {succ n} 0<sn a b | record { quot = sn/a ; rem = sn%a ; pr = prA ; remIsSmall = remIsSmallA ; quotSmall = quotSmallA } | record { quot = sn/b ; rem = sn%b ; pr = prB ; remIsSmall = remIsSmallB ; quotSmall = quotSmallB } | record { quot = sn/a+b ; rem = sn%a+b ; pr = prA+B ; remIsSmall = remIsSmallA+B ; quotSmall = quotSmallA+B } with divisionAlg (succ n) (sn%a +N sn%b)
  modExtracts {succ n} 0<sn a b | record { quot = sn/a ; rem = sn%a ; pr = prA ; remIsSmall = inl sn%a<sn ; quotSmall = inl _ } | record { quot = sn/b ; rem = sn%b ; pr = prB ; remIsSmall = inl sn%b<sn ; quotSmall = inl _ } | record { quot = sn/a+b ; rem = sn%a+b ; pr = prA+B ; remIsSmall = inl sn%a+b<sn ; quotSmall = inl _ } | record { quot = quot ; rem = rem ; pr = pr ; remIsSmall = inl remIsSmall ; quotSmall = inl _ } = equalityCommutative whoa
    where
      t : ((succ n *N sn/a) +N sn%a) +N ((succ n *N sn/b) +N sn%b) ≡ a +N b
      t = +NWellDefined prA prB
      t' : (succ n *N (sn/a +N sn/b)) +N (sn%a +N sn%b) ≡ a +N b
      t' = transitivity (transitivity (Semiring.+Associative ℕSemiring (succ n *N (sn/a +N sn/b)) sn%a sn%b) (transitivity (applyEquality (_+N sn%b) (transitivity (transitivity (applyEquality (_+N sn%a) (transitivity (applyEquality (succ n *N_) (Semiring.commutative ℕSemiring sn/a sn/b)) (Semiring.+DistributesOver* ℕSemiring (succ n) sn/b sn/a))) (equalityCommutative (Semiring.+Associative ℕSemiring (succ n *N sn/b) (succ n *N sn/a) sn%a))) (Semiring.commutative ℕSemiring (succ n *N sn/b) ((succ n *N sn/a) +N sn%a)))) (equalityCommutative (Semiring.+Associative ℕSemiring ((succ n *N sn/a) +N sn%a) (succ n *N sn/b) sn%b)))) t
      thing : ((succ n) *N quot) +N rem ≡ sn%a +N sn%b
      thing = pr
      t'' : (succ n *N ((sn/a +N sn/b) +N quot)) +N rem ≡ a +N b
      t'' rewrite Semiring.+DistributesOver* ℕSemiring (succ n) (sn/a +N sn/b) quot | equalityCommutative (Semiring.+Associative ℕSemiring (succ n *N (sn/a +N sn/b)) (succ n *N quot) rem) | thing = t'
      whoa : rem ≡ sn%a+b
      whoa = modUniqueLemma _ _ remIsSmall sn%a+b<sn (transitivity t'' (equalityCommutative prA+B))

  modAddition : {n : ℕ} → .(pr : 0 <N n) → {a b : ℕ} → (a <N n) → (b <N n) → (a +N b ≡ mod n pr (a +N b)) || (a +N b ≡ n +N mod n pr (a +N b))
  modAddition {succ n} 0<sn {a} {b} a<n b<n with divisionAlg (succ n) (a +N b)
  modAddition {succ n} 0<sn {a} {b} a<n b<n | record { quot = zero ; rem = rem ; pr = pr ; remIsSmall = inl rem<sn ; quotSmall = inl _ } = inl (equalityCommutative (transitivity (applyEquality (_+N rem) (multiplicationNIsCommutative 0 n)) pr))
  modAddition {succ n} 0<sn {a} {b} a<n b<n | record { quot = succ zero ; rem = rem ; pr = pr ; remIsSmall = inl rem<sn ; quotSmall = inl _ } = inr (transitivity (equalityCommutative pr) (applyEquality (λ i → succ i +N rem) (transitivity (multiplicationNIsCommutative n 1) (Semiring.sumZeroRight ℕSemiring n))))
  modAddition {succ n} 0<sn {a} {b} (le x prA) (le y prB) | record { quot = succ (succ quot) ; rem = 0 ; pr = pr ; remIsSmall = inl rem<sn ; quotSmall = inl _ } rewrite Semiring.sumZeroRight ℕSemiring (succ n *N succ (succ quot)) | multiplicationNIsCommutative (succ n) (succ (succ quot)) = exFalso (notBigger' ((x +N succ y) +N (quot *N succ n)) u)
    where
      t : ((succ x +N a) +N succ (y +N b)) +N (quot *N succ n) ≡ a +N b
      t = transitivity (transitivity (applyEquality (_+N quot *N succ n) (+NWellDefined prA prB)) (equalityCommutative (Semiring.+Associative ℕSemiring (succ n) (succ n) (quot *N succ n)))) pr
      u : ((succ x +N succ y) +N (quot *N succ n)) +N (a +N b) ≡ a +N b
      u rewrite Semiring.commutative ℕSemiring ((x +N succ y) +N quot *N succ n) (a +N b) | Semiring.+Associative ℕSemiring (succ a +N b) (x +N succ y) (quot *N succ n) = transitivity (applyEquality (λ i → succ i +N quot *N succ n) (transitivity (Semiring.commutative ℕSemiring (a +N b) _) (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring x (succ y) _)) (transitivity (applyEquality (x +N_) (transitivity (Semiring.+Associative ℕSemiring (succ y) a b) (transitivity (applyEquality (_+N b) (Semiring.commutative ℕSemiring _ a)) (equalityCommutative (Semiring.+Associative ℕSemiring a (succ y) b))))) (Semiring.+Associative ℕSemiring x a _))))) t
  modAddition {succ n} 0<sn {a} {b} a<n b<n | record { quot = succ (succ quot) ; rem = succ rem ; pr = pr ; remIsSmall = inl rem<sn ; quotSmall = inl _ } = exFalso (irreflexive (<Transitive u t))
    where
      t : (succ n *N succ (succ quot) +N succ rem) <N succ n +N succ n
      t = identityOfIndiscernablesLeft _<N_ (addStrongInequalities a<n b<n) (equalityCommutative pr)
      lemm : {a c d : ℕ} → (a +N a) <N (a *N succ (succ c)) +N succ d
      lemm {a} {c} {d} = le (a *N c +N d) f
        where
          f : succ ((a *N c +N d) +N (a +N a)) ≡ a *N succ (succ c) +N succ d
          f rewrite multiplicationNIsCommutative a (succ (succ c)) | Semiring.+Associative ℕSemiring a a (c *N a) | multiplicationNIsCommutative c a | Semiring.commutative ℕSemiring (a *N c +N d) (a +N a) | Semiring.+Associative ℕSemiring (a +N a) (a *N c) d | Semiring.commutative ℕSemiring ((a +N a) +N a *N c) (succ d) = applyEquality succ (Semiring.commutative ℕSemiring _ d)
      u : (succ n +N succ n) <N (succ n *N succ (succ quot) +N succ rem)
      u = lemm {succ n}

  modN : {n : ℕ} → .(0<n : 0 <N n) → mod n 0<n n ≡ 0
  modN {succ n} 0<n = modIsUnique (divisionAlg (succ n) (succ n)) record { quot = 1 ; rem = zero ; pr = ans ; remIsSmall = inl (le n (Semiring.sumZeroRight ℕSemiring (succ n))) ; quotSmall = inl (le n (Semiring.sumZeroRight ℕSemiring (succ n))) }
    where
      ans : succ (n *N 1 +N 0) ≡ succ n
      ans rewrite multiplicationNIsCommutative n 1 | Semiring.sumZeroRight ℕSemiring n | Semiring.sumZeroRight ℕSemiring n = refl

ext: agda


text:
-- 2011-09-15 by Nisse
-- {-# OPTIONS -v tc.lhs.unify:15 #-}
module Issue292-17 where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ

postulate
  I  : Set
  U  : I → Set
  El : ∀ {i} → U i → Set

mutual

  infixl 5 _▻_

  data Ctxt : Set where
    _▻_ : (Γ : Ctxt) (σ : Type Γ) → Ctxt

  Type : Ctxt → Set
  Type Γ = Σ I (λ i → Env Γ → U i)

  Env : Ctxt → Set
  Env (Γ ▻ σ) = Σ (Env Γ) λ γ → El (proj₂ σ γ)

postulate
  Γ : Ctxt
  σ : Type Γ

data D : Type (Γ ▻ σ) → Set where
  d : (τ : Type Γ) → D (proj₁ τ , λ γ → proj₂ τ (proj₁ γ))

record [D] : Set where
  constructor [d]
  field
    τ : Type (Γ ▻ σ)
    x : D τ

Foo : {τ₁ τ₂ : Type Γ} →
      [d] (proj₁ τ₁ , λ γ → proj₂ τ₁ (proj₁ γ)) (d τ₁) ≡
      [d] (proj₁ τ₂ , λ γ → proj₂ τ₂ (proj₁ γ)) (d τ₂) →
      Set₁
Foo refl = Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Prelude where

open import Level public
open import Data.Sigma public
open import Function.Fiber public
open import Data.Empty public
open import Data.Unit public
open import Data.Nat public
  using (ℕ; suc; zero)
open import Data.Bool public
  using (Bool; true; false; bool; if_then_else_; T; _and_; _or_; not)
open import Data.Maybe public
  using (Maybe; just; nothing)
open import HITs.PropositionalTruncation public
  using (∥_∥; ∣_∣)
open import Function.Surjective public
  using (Surjective; SplitSurjective; _↠!_; _↠_)
open import Data.Pi public
open import Function.Isomorphism public
open import Path public
open import Function public
open import Relation.Nullary.Decidable public
open import Relation.Nullary.Discrete public using (Discrete)
open import Relation.Nullary.Discrete.Properties public using (Discrete→isSet)
open import HLevels public
open import Data.Sum public
open import Equiv public
open import Data.Lift public
open import Function.Biconditional public
open import Relation.Unary public
open import Strict public
open import Instance public

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Various forms of induction for natural numbers
------------------------------------------------------------------------

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

module Data.Nat.Induction where

open import Function
open import Data.Nat.Base
open import Data.Nat.Properties using (≤⇒≤′)
open import Data.Product
open import Data.Unit
open import Induction
open import Induction.WellFounded as WF
open import Level using (Lift)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary

------------------------------------------------------------------------
-- Re-export accessability

open WF public using (Acc; acc)

------------------------------------------------------------------------
-- Ordinary induction

Rec : ∀ ℓ → RecStruct ℕ ℓ ℓ
Rec ℓ P zero    = Lift ℓ ⊤
Rec ℓ P (suc n) = P n

recBuilder : ∀ {ℓ} → RecursorBuilder (Rec ℓ)
recBuilder P f zero    = _
recBuilder P f (suc n) = f n (recBuilder P f n)

rec : ∀ {ℓ} → Recursor (Rec ℓ)
rec = build recBuilder

------------------------------------------------------------------------
-- Complete induction

CRec : ∀ ℓ → RecStruct ℕ ℓ ℓ
CRec ℓ P zero    = Lift ℓ ⊤
CRec ℓ P (suc n) = P n × CRec ℓ P n

cRecBuilder : ∀ {ℓ} → RecursorBuilder (CRec ℓ)
cRecBuilder P f zero    = _
cRecBuilder P f (suc n) = f n ih , ih
  where ih = cRecBuilder P f n

cRec : ∀ {ℓ} → Recursor (CRec ℓ)
cRec = build cRecBuilder

------------------------------------------------------------------------
-- Complete induction based on _<′_

<′-Rec : ∀ {ℓ} → RecStruct ℕ ℓ ℓ
<′-Rec = WfRec _<′_

mutual

  <′-wellFounded : WellFounded _<′_
  <′-wellFounded n = acc (<′-wellFounded′ n)

  <′-wellFounded′ : ∀ n → <′-Rec (Acc _<′_) n
  <′-wellFounded′ (suc n) .n ≤′-refl       = <′-wellFounded n
  <′-wellFounded′ (suc n)  m (≤′-step m<n) = <′-wellFounded′ n m m<n

module _ {ℓ} where
  open WF.All <′-wellFounded ℓ public
    renaming ( wfRecBuilder to <′-recBuilder
             ; wfRec        to <′-rec
             )
    hiding (wfRec-builder)

------------------------------------------------------------------------
-- Complete induction based on _<_

<-Rec : ∀ {ℓ} → RecStruct ℕ ℓ ℓ
<-Rec = WfRec _<_

<-wellFounded : WellFounded _<_
<-wellFounded = Subrelation.wellFounded ≤⇒≤′ <′-wellFounded

module _ {ℓ} where
  open WF.All <-wellFounded ℓ public
    renaming ( wfRecBuilder to <-recBuilder
             ; wfRec        to <-rec
             )
    hiding (wfRec-builder)

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

-- Version 0.15

rec-builder      = recBuilder
{-# WARNING_ON_USAGE rec-builder
"Warning: rec-builder was deprecated in v0.15.
Please use recBuilder instead."
#-}
cRec-builder     = cRecBuilder
{-# WARNING_ON_USAGE cRec-builder
"Warning: cRec-builder was deprecated in v0.15.
Please use cRecBuilder instead."
#-}
<′-rec-builder   = <′-recBuilder
{-# WARNING_ON_USAGE <′-rec-builder
"Warning: <′-rec-builder was deprecated in v0.15.
Please use <′-recBuilder instead."
#-}
<-rec-builder    = <-recBuilder
{-# WARNING_ON_USAGE <-rec-builder
"Warning: <-rec-builder was deprecated in v0.15.
Please use <-recBuilder instead."
#-}
<′-well-founded  = <′-wellFounded
{-# WARNING_ON_USAGE <′-well-founded
"Warning: <′-well-founded was deprecated in v0.15.
Please use <′-wellFounded instead."
#-}
<′-well-founded′ = <′-wellFounded′
{-# WARNING_ON_USAGE <′-well-founded′
"Warning: <′-well-founded′ was deprecated in v0.15.
Please use <′-wellFounded′ instead."
#-}
<-well-founded   = <-wellFounded
{-# WARNING_ON_USAGE <-well-founded
"Warning: <-well-founded was deprecated in v0.15.
Please use <-wellFounded instead."
#-}


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category
import Categories.Category.Monoidal as M

-- Properties of Monoidal Categories

module Categories.Category.Monoidal.Properties
  {o ℓ e} {C : Category o ℓ e} (MC : M.Monoidal C) where

open import Data.Product using (_,_; Σ; uncurry′)

open Category C
open M.Monoidal MC
open import Categories.Category.Monoidal.Utilities MC
import Categories.Category.Monoidal.Reasoning as MonR
open import Categories.Category.Construction.Core C
open import Categories.Category.Product using (Product)
open import Categories.Functor using (Functor)
open import Categories.Functor.Bifunctor
open import Categories.Functor.Properties
open import Categories.Category.Groupoid using (IsGroupoid)
open import Categories.Morphism C
open import Categories.Morphism.IsoEquiv C using (_≃_; ⌞_⌟)
open import Categories.Morphism.Isomorphism C
import Categories.Morphism.Reasoning as MR
open import Categories.NaturalTransformation.NaturalIsomorphism.Properties
  using (push-eq)

private
  module C = Category C
  variable
    A B : Obj

⊗-iso : Bifunctor Core Core Core
⊗-iso = record
  { F₀           = uncurry′ _⊗₀_
  ; F₁           =  λ where (f , g) → f ⊗ᵢ g
  ; identity     = refl⊗refl≃refl
  ; homomorphism = ⌞ homomorphism ⌟
  ; F-resp-≈     = λ where (⌞ eq₁ ⌟ , ⌞ eq₂ ⌟) → ⌞ F-resp-≈ (eq₁ , eq₂) ⌟
  }
  where open Functor ⊗
        open _≃_

_⊗ᵢ- : Obj → Functor Core Core
X ⊗ᵢ- = appˡ ⊗-iso X

-⊗ᵢ_ : Obj → Functor Core Core
-⊗ᵢ X = appʳ ⊗-iso X

-- Coherence laws due to Mac Lane (1963) the were subsequently proven
-- admissible by Max Kelly (1964).  See
-- https://ncatlab.org/nlab/show/monoidal+category#other_coherence_conditions
-- for more details.

module Kelly's where
  open Functor
  open IsGroupoid.Commutation Core-isGroupoid

  private
    assoc′ = IsGroupoid.assoc Core-isGroupoid
    variable
          f f′ g h h′ i i′ j k : A ≅ B

  module _ {X Y : Obj} where
    open IsGroupoid.HomReasoning Core-isGroupoid

    -- TS: following three isos commute

    ua : unit ⊗₀ (unit ⊗₀ X) ⊗₀ Y ≅ unit ⊗₀ unit ⊗₀ X ⊗₀ Y
    ua = ≅.refl ⊗ᵢ associator

    u[λY] : unit ⊗₀ (unit ⊗₀ X) ⊗₀ Y ≅ unit ⊗₀ X ⊗₀ Y
    u[λY] = ≅.refl ⊗ᵢ unitorˡ ⊗ᵢ ≅.refl

    uλ : unit ⊗₀ unit ⊗₀ X ⊗₀ Y ≅ unit ⊗₀ X ⊗₀ Y
    uλ = ≅.refl ⊗ᵢ unitorˡ

    -- setups

    perimeter : [ ((unit ⊗₀ unit) ⊗₀ X) ⊗₀ Y ⇒ unit ⊗₀ X ⊗₀ Y ]⟨
                  (unitorʳ ⊗ᵢ ≅.refl) ⊗ᵢ ≅.refl               ⇒⟨ (unit ⊗₀ X) ⊗₀ Y ⟩
                  associator
                ≈ associator                                  ⇒⟨ (unit ⊗₀ unit) ⊗₀ X ⊗₀ Y ⟩
                  associator                                  ⇒⟨ unit ⊗₀ unit ⊗₀ X ⊗₀ Y ⟩
                  uλ
                ⟩
    perimeter = ⟺ (glue◃◽′ triangle-iso
                             (sym (lift-square′ (Equiv.trans assoc-commute-from
                                                             (∘-resp-≈ˡ (F-resp-≈ ⊗ (Equiv.refl , identity ⊗)))))))
      where open MR Core

    [uλ]Y : (unit ⊗₀ (unit ⊗₀ X)) ⊗₀ Y ≅ (unit ⊗₀ X) ⊗₀ Y
    [uλ]Y = (≅.refl ⊗ᵢ unitorˡ) ⊗ᵢ ≅.refl

    aY : ((unit ⊗₀ unit) ⊗₀ X) ⊗₀ Y ≅ (unit ⊗₀ unit ⊗₀ X) ⊗₀ Y
    aY = associator ⊗ᵢ ≅.refl

    [ρX]Y : ((unit ⊗₀ unit) ⊗₀ X) ⊗₀ Y ≅ (unit ⊗₀ X) ⊗₀ Y
    [ρX]Y = (unitorʳ ⊗ᵢ ≅.refl) ⊗ᵢ ≅.refl

    tri : [uλ]Y ∘ᵢ aY ≃ [ρX]Y
    tri = lift-triangle′ ([ appʳ ⊗ Y ]-resp-∘ triangle)

    sq : associator ∘ᵢ [uλ]Y ≃ u[λY] ∘ᵢ associator
    sq = lift-square′ assoc-commute-from

    -- proofs

    perimeter′ : [ ((unit ⊗₀ unit) ⊗₀ X) ⊗₀ Y ⇒ unit ⊗₀ X ⊗₀ Y ]⟨
                   (unitorʳ ⊗ᵢ ≅.refl) ⊗ᵢ ≅.refl     ⇒⟨ (unit ⊗₀ X) ⊗₀ Y ⟩
                   associator
                 ≈ aY                                 ⇒⟨ (unit ⊗₀ (unit ⊗₀ X)) ⊗₀ Y ⟩
                   associator                         ⇒⟨ unit ⊗₀ (unit ⊗₀ X) ⊗₀ Y ⟩
                   ua                                 ⇒⟨ unit ⊗₀ unit ⊗₀ X ⊗₀ Y ⟩
                   uλ
                 ⟩
    perimeter′ = begin
      associator ∘ᵢ (unitorʳ ⊗ᵢ ≅.refl) ⊗ᵢ ≅.refl    ≈⟨ perimeter ⟩
      uλ ∘ᵢ associator ∘ᵢ associator                  ≈˘⟨ refl⟩∘⟨ pentagon-iso ⟩
      uλ ∘ᵢ ua ∘ᵢ associator ∘ᵢ aY                    ∎

    top-face : uλ ∘ᵢ ua ≃ u[λY]
    top-face = elim-triangleˡ′ (sym perimeter′) (glue◽◃ (sym sq) tri)
      where open MR Core

    coherence-iso₁ : [ (unit ⊗₀ X) ⊗₀ Y ⇒ X ⊗₀ Y ]⟨
                    associator                ⇒⟨ unit ⊗₀ X ⊗₀ Y ⟩
                    unitorˡ
                  ≈ unitorˡ ⊗ᵢ ≅.refl
                  ⟩
    coherence-iso₁ = triangle-prism top-face square₁ square₂ square₃
      where square₁ : [ unit ⊗₀ X ⊗₀ Y ⇒ unit ⊗₀ X ⊗₀ Y ]⟨
                        ≅.sym unitorˡ ∘ᵢ unitorˡ
                      ≈ ≅.refl ⊗ᵢ unitorˡ ∘ᵢ ≅.sym unitorˡ
                      ⟩
            square₁ = lift-square′ unitorˡ-commute-to

            square₂ : [ (unit ⊗₀ X) ⊗₀ Y ⇒ unit ⊗₀ unit ⊗₀ X ⊗₀ Y ]⟨
                        ≅.sym unitorˡ ∘ᵢ associator
                      ≈ ≅.refl ⊗ᵢ associator ∘ᵢ ≅.sym unitorˡ
                      ⟩
            square₂ = lift-square′ unitorˡ-commute-to

            square₃ : [ (unit ⊗₀ X) ⊗₀ Y ⇒ unit ⊗₀ X ⊗₀ Y ]⟨
                        ≅.sym unitorˡ ∘ᵢ unitorˡ ⊗ᵢ ≅.refl
                      ≈ ≅.refl ⊗ᵢ unitorˡ ⊗ᵢ ≅.refl ∘ᵢ ≅.sym unitorˡ
                      ⟩
            square₃ = lift-square′ unitorˡ-commute-to

    coherence₁ : unitorˡ.from ∘ associator.from ≈ unitorˡ.from {X} ⊗₁ C.id {Y}
    coherence₁ = project-triangle coherence-iso₁

    -- another coherence property

    -- TS : the following three commute

    ρu : ((X ⊗₀ Y) ⊗₀ unit) ⊗₀ unit ≅ (X ⊗₀ Y) ⊗₀ unit
    ρu = unitorʳ ⊗ᵢ ≅.refl

    au : ((X ⊗₀ Y) ⊗₀ unit) ⊗₀ unit ≅ (X ⊗₀ Y ⊗₀ unit) ⊗₀ unit
    au = associator ⊗ᵢ ≅.refl

    [Xρ]u : (X ⊗₀ Y ⊗₀ unit) ⊗₀ unit ≅ (X ⊗₀ Y) ⊗₀ unit
    [Xρ]u = (≅.refl ⊗ᵢ unitorʳ) ⊗ᵢ ≅.refl

    perimeter″ : [ ((X ⊗₀ Y) ⊗₀ unit) ⊗₀ unit ⇒ X ⊗₀ Y ⊗₀ unit ]⟨
                   associator                        ⇒⟨ (X ⊗₀ Y) ⊗₀ unit ⊗₀ unit ⟩
                   associator                        ⇒⟨ X ⊗₀ Y ⊗₀ unit ⊗₀ unit ⟩
                   ≅.refl ⊗ᵢ ≅.refl ⊗ᵢ unitorˡ
                 ≈ ρu                                ⇒⟨ (X ⊗₀ Y) ⊗₀ unit ⟩
                   associator
                 ⟩
    perimeter″ = glue▹◽ triangle-iso (sym (lift-square′
        (Equiv.trans (∘-resp-≈ʳ (F-resp-≈ ⊗ (Equiv.sym (identity ⊗) , Equiv.refl)))
                      assoc-commute-from)))
      where open MR Core

    perimeter‴ : [ ((X ⊗₀ Y) ⊗₀ unit) ⊗₀ unit ⇒ X ⊗₀ Y ⊗₀ unit  ]⟨
                   associator ⊗ᵢ ≅.refl                           ⇒⟨ (X ⊗₀ (Y ⊗₀ unit)) ⊗₀ unit ⟩
                   (associator                                    ⇒⟨ X ⊗₀ (Y ⊗₀ unit) ⊗₀ unit ⟩
                   ≅.refl ⊗ᵢ associator                           ⇒⟨ X ⊗₀ Y ⊗₀ unit ⊗₀ unit ⟩
                   ≅.refl ⊗ᵢ ≅.refl ⊗ᵢ unitorˡ)
                 ≈ ρu                                             ⇒⟨ (X ⊗₀ Y) ⊗₀ unit ⟩
                   associator
                 ⟩
    perimeter‴ = let α = associator in let λλ = unitorˡ in begin
      (≅.refl ⊗ᵢ ≅.refl ⊗ᵢ λλ ∘ᵢ ≅.refl ⊗ᵢ α ∘ᵢ α) ∘ᵢ α ⊗ᵢ ≅.refl  ≈⟨ assoc′ ⟩
       ≅.refl ⊗ᵢ ≅.refl ⊗ᵢ λλ ∘ᵢ (≅.refl ⊗ᵢ α ∘ᵢ α) ∘ᵢ α ⊗ᵢ ≅.refl ≈⟨ refl⟩∘⟨ assoc′ ⟩
       ≅.refl ⊗ᵢ ≅.refl ⊗ᵢ λλ ∘ᵢ ≅.refl ⊗ᵢ α ∘ᵢ α ∘ᵢ α ⊗ᵢ ≅.refl   ≈⟨ refl⟩∘⟨ pentagon-iso ⟩
       ≅.refl ⊗ᵢ ≅.refl ⊗ᵢ λλ ∘ᵢ α ∘ᵢ α                             ≈⟨ perimeter″ ⟩
       α ∘ᵢ ρu                                                       ∎

    top-face′ : [Xρ]u ∘ᵢ au ≃ ρu
    top-face′ = cut-squareʳ perimeter‴ (sym (glue◃◽′ tri′ (sym (lift-square′ assoc-commute-from))))
      where open MR Core
            tri′ : [ X ⊗₀ (Y ⊗₀ unit) ⊗₀ unit ⇒ X ⊗₀ Y ⊗₀ unit ]⟨
                   (≅.refl ⊗ᵢ ≅.refl ⊗ᵢ unitorˡ ∘ᵢ ≅.refl ⊗ᵢ associator)
                 ≈ ≅.refl ⊗ᵢ unitorʳ ⊗ᵢ ≅.refl
                 ⟩
            tri′ = lift-triangle′ ([ X ⊗- ]-resp-∘ triangle)

    coherence-iso₂ : [ (X ⊗₀ Y) ⊗₀ unit ⇒ X ⊗₀ Y ]⟨
                       ≅.refl ⊗ᵢ unitorʳ ∘ᵢ associator
                     ≈ unitorʳ
                     ⟩
    coherence-iso₂ = triangle-prism top-face′ square₁ square₂ (lift-square′ unitorʳ-commute-to)
      where square₁ : [ X ⊗₀ Y ⊗₀ unit ⇒ (X ⊗₀ Y) ⊗₀ unit ]⟨
                        ≅.sym unitorʳ ∘ᵢ ≅.refl ⊗ᵢ unitorʳ
                      ≈ (≅.refl ⊗ᵢ unitorʳ) ⊗ᵢ ≅.refl ∘ᵢ ≅.sym unitorʳ
                      ⟩
            square₁ = lift-square′ unitorʳ-commute-to

            square₂ : [ (X ⊗₀ Y) ⊗₀ unit ⇒ (X ⊗₀ Y ⊗₀ unit) ⊗₀ unit ]⟨
                        ≅.sym unitorʳ ∘ᵢ associator
                      ≈ associator ⊗ᵢ ≅.refl ∘ᵢ ≅.sym unitorʳ
                      ⟩
            square₂ = lift-square′ unitorʳ-commute-to

    coherence₂ : C.id {X} ⊗₁ unitorʳ.from {Y} ∘ associator.from ≈ unitorʳ.from
    coherence₂ = project-triangle coherence-iso₂

  -- A third coherence condition (Lemma 2.3)

  coherence₃ : unitorˡ.from {unit} ≈ unitorʳ.from
  coherence₃ = push-eq unitorˡ-naturalIsomorphism (begin
      C.id ⊗₁ unitorˡ.from
    ≈˘⟨ cancelʳ associator.isoʳ ⟩
      (C.id ⊗₁ unitorˡ.from ∘ associator.from) ∘ associator.to
    ≈⟨ triangle ⟩∘⟨refl ⟩
      unitorʳ.from ⊗₁ C.id ∘ associator.to
    ≈⟨ unitor-coherenceʳ ⟩∘⟨refl ⟩
      unitorʳ.from ∘ associator.to
    ≈˘⟨ coherence₂ ⟩∘⟨refl ⟩
      (C.id ⊗₁ unitorʳ.from ∘ associator.from) ∘ associator.to
    ≈⟨ cancelʳ associator.isoʳ ⟩
      C.id ⊗₁ unitorʳ.from
    ∎)
    where
      open MR C hiding (push-eq)
      open C.HomReasoning

  coherence-iso₃ : [ unit ⊗₀ unit ⇒ unit ]⟨ unitorˡ ≈ unitorʳ ⟩
  coherence-iso₃ = ⌞ coherence₃ ⌟

open Kelly's using (coherence₁; coherence-iso₁; coherence₂; coherence-iso₂) public

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module NoSuchBuiltinName where

postulate X : Set

{-# BUILTIN FOOBAR X #-}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2020-06-24, issue #4775 reported by JakobBruenker
-- Non-record patterns in lets and lambdas lead to internal error

-- {-# OPTIONS -v tc.term.lambda:30 #-}
-- {-# OPTIONS -v tc.lhs:15 #-}
-- {-# OPTIONS -v tc.term.let.pattern:30 #-}
-- -- {-# OPTIONS -v tc.term.let.pattern:80 #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Sigma

data IsSuc : Nat → Set where
  isSuc : ∀ y → IsSuc (suc y)

test : Σ Nat IsSuc → Set
test = λ (y1 , isSuc y2) → Nat

-- ERROR NOW:
-- Expected record pattern
-- when checking the let binding y1 , isSuc y2 = .patternInTele0

-- (Talks about desugaring; could still be improved.)


text:
-- This file defines the Euclidean Domain structure.

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

module EuclideanDomain where
-- We comply to the definition format in stdlib, i.e. define an
-- IsSomething predicate then define the bundle.

  open import Relation.Binary using (Rel; Setoid; IsEquivalence)

  module Structures
    {a ℓ} {A : Set a}  -- The underlying set
    (_≈_ : Rel A ℓ)    -- The underlying equality relation
    where

    open import Algebra.Structures _≈_
    open import Algebra.Core
    open import Algebra.Definitions _≈_
    import Algebra.Consequences.Setoid as Consequences
    open import Data.Product using (_,_; proj₁; proj₂)
    open import Level using (_⊔_)

    open import Data.Nat using (ℕ ; _<_)
    open import Data.Product using (∃ ; _×_)
    open import Relation.Nullary using (¬_)

    -- We only require leftcancellative since we have required the
    -- domain to be commutative. An Euclidean domain is a commutative
    -- domain with a div, mod, and rank function satisfy euc-eq and
    -- euc-rank.
    record IsEuclideanDomain
             (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
      field
        isCommutativeRing : IsCommutativeRing + * - 0# 1#
        *-alc : AlmostLeftCancellative 0# *
        div : ∀ (n d : A) -> ¬ d ≈ 0# -> A
        mod : ∀ (n d : A) -> ¬ d ≈ 0# -> A
        rank : A → ℕ
        euc-eq : ∀ (n d : A) -> (n0 : ¬ d ≈ 0#) ->
                   let r = mod n d n0 in let q = div n d n0 in
                   n ≈ + r (* q d)
        euc-rank : ∀ (n d : A) -> (n0 : ¬ d ≈ 0#) ->
                   let r = mod n d n0 in let q = div n d n0 in
                   rank r < rank d

  module Bundles where

    open Structures
    open import Algebra.Core
    open import Algebra.Structures
    open import Relation.Binary
    open import Function.Base
    import Relation.Nullary as N
    open import Level

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

      open IsEuclideanDomain isEuclideanDomain public

max_stars_repo_name: onestruggler/EucDomain

max_issues_repo_name: onestruggler/EucDomain

max_forks_repo_name: onestruggler/EucDomain


text:
------------------------------------------------------------------------
-- Some results related to an LTS from Section 6.2.5 of "Enhancements
-- of the bisimulation proof method" by Pous and Sangiorgi,
-- implemented using the coinductive definition of bisimilarity
------------------------------------------------------------------------

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

open import Prelude

module Bisimilarity.6-2-5 {Name : Type} where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude.Size

open import Function-universe equality-with-J hiding (id; _∘_)

import Bisimilarity.Equational-reasoning-instances
open import Equational-reasoning
open import Indexed-container using (⟦_⟧)
open import Labelled-transition-system.6-2-5 Name
open import Relation

open import Bisimilarity 6-2-5
open import Bisimilarity.Up-to 6-2-5

-- Some simple lemmas. The first two are stated by Pous and Sangiorgi,
-- and the third one is a generalisation of a result stated by Pous
-- and Sangiorgi.

op·∅ : ∀ {a} → op (a · ∅) ∼ ∅
op·∅ {a} = ⟨ lr , (λ ()) ⟩
  where
  lr : ∀ {P′ μ} →
       op (a · ∅) [ μ ]⟶ P′ →
       ∃ λ Q′ → ∅ [ μ ]⟶ Q′ × P′ ∼′ Q′
  lr (op action ())

op··∅ : ∀ {a} → op (a · a · ∅) ∼ a · ∅
op··∅ {a} = ⟨ lr , rl ⟩
  where
  lr : ∀ {P′ μ b} →
       op (a · b · ∅) [ μ ]⟶ P′ →
       ∃ λ Q′ → b · ∅ [ μ ]⟶ Q′ × P′ ∼′ Q′
  lr (op action action) = _ , action , reflexive

  rl : ∀ {Q′ μ} →
       a · ∅ [ μ ]⟶ Q′ →
       ∃ λ P′ → op (a · a · ∅) [ μ ]⟶ P′ × P′ ∼′ Q′
  rl action = _ , op action action , reflexive

a≁b·c : ∀ {a b c} → ¬ (a · ∅ ∼ b · c · ∅)
a≁b·c a∼b·c with right-to-left a∼b·c action
... | .∅ , action , ∅∼a with right-to-left (force ∅∼a) action
...   | _ , () , _

-- Pous and Sangiorgi note that every context preserves bisimilarity.
-- One can prove that a ·_ preserves bisimilarity in a size-preserving
-- way.

·-cong : ∀ {i a P Q} → [ i ] P ∼ Q → [ i ] a · P ∼ a · Q
·-cong {i} {a} P∼Q =
  ⟨ lr P∼Q
  , Σ-map id (Σ-map id symmetric) ∘ lr (symmetric P∼Q)
  ⟩
  where
  lr : ∀ {P P′ Q μ} →
       [ i ] P ∼ Q → a · P [ μ ]⟶ P′ →
       ∃ λ Q′ → a · Q [ μ ]⟶ Q′ × [ i ] P′ ∼′ Q′
  lr P∼Q action = _ , action , convert P∼Q

-- The operator op also preserves bisimilarity, but this lemma is not
-- claimed to be size-preserving.

op-cong : ∀ {i} {j : Size< i} {P Q} →
          [ i ] P ∼ Q → [ j ] op P ∼ op Q
op-cong {i} {j} P∼Q =
  ⟨ lr P∼Q
  , Σ-map id (Σ-map id symmetric) ∘ lr (symmetric P∼Q)
  ⟩
  where
  lr : ∀ {P P′ Q μ} →
       [ i ] P ∼ Q → op P [ μ ]⟶ P′ →
       ∃ λ Q′ → op Q [ μ ]⟶ Q′ × [ j ] P′ ∼′ Q′
  lr P∼Q (op P⟶P′ P′⟶P″) =
    let Q′ , Q⟶Q′  , P′∼Q′ = left-to-right        P∼Q    P⟶P′
        Q″ , Q′⟶Q″ , P″∼Q″ = left-to-right (force P′∼Q′) P′⟶P″
    in Q″ , op Q⟶Q′ Q′⟶Q″ , P″∼Q″

-- Let us assume that the Name type is inhabited. In that case op-cong
-- /cannot/ preserve the size of its argument.
--
-- The proof is based on an argument presented by Pous and Sangiorgi.

op-cong-cannot-preserve-size :
  Name →
  ¬ (∀ {i P Q} → [ i ] P ∼ Q → [ i ] op P ∼ op Q)
op-cong-cannot-preserve-size a op-cong = a≁b·c a∼a·a
  where
  op-cong′ : ∀ {i P Q} → [ i ] P ∼′ Q → [ i ] op P ∼′ op Q
  force (op-cong′ P∼′Q) = op-cong (force P∼′Q)

  a∼a·a : ∀ {i} → [ i ] a · ∅ ∼ a · a · ∅
  a∼a·a {i} = ⟨ lr , rl ⟩
    where
    a∼′a·a : ∀ {i} → [ i ] a · ∅ ∼′ a · a · ∅
    force a∼′a·a = a∼a·a

    lemma =
      ∅               ∼⟨ symmetric op·∅ ⟩
      op (a · ∅)      ∼⟨ op-cong′ (a∼′a·a {i = i}) ⟩
      op (a · a · ∅)  ∼⟨ op··∅ ⟩■
      a · ∅

    lr : ∀ {P′ μ} →
         a · ∅ [ μ ]⟶ P′ →
         ∃ λ Q′ → a · a · ∅ [ μ ]⟶ Q′ × [ i ] P′ ∼′ Q′
    lr action = a · ∅ , action , lemma

    rl : ∀ {Q′ μ} →
         a · a · ∅ [ μ ]⟶ Q′ →
         ∃ λ P′ → a · ∅ [ μ ]⟶ P′ × [ i ] P′ ∼′ Q′
    rl action = ∅ , action , lemma

-- Up to context (for monadic contexts).

Up-to-context : Trans₂ (# 0) Proc
Up-to-context R (P , Q) =
  ∃ λ (C : Context 1) →
  ∃ λ P′ →
  ∃ λ Q′ →
  P ≡ C [ (λ _ → P′) ]
    ×
  Q ≡ C [ (λ _ → Q′) ]
    ×
  R (P′ , Q′)

-- Up to context is monotone.

up-to-context-monotone : Monotone Up-to-context
up-to-context-monotone R⊆S =
  Σ-map id $ Σ-map id $ Σ-map id $ Σ-map id $ Σ-map id R⊆S

-- Up to bisimilarity and context.

Up-to-bisimilarity-and-context : Trans₂ (# 0) Proc
Up-to-bisimilarity-and-context =
  Up-to-bisimilarity ∘ Up-to-context

-- Up to bisimilarity and context is monotone.

up-to-bisimilarity-and-context-monotone :
  Monotone Up-to-bisimilarity-and-context
up-to-bisimilarity-and-context-monotone =
  up-to-bisimilarity-monotone ∘ up-to-context-monotone

-- Up to bisimilarity and context is not sound (assuming that Name is
-- inhabited).
--
-- This result is due to Pous and Sangiorgi.

¬-up-to-bisimilarity-and-context :
  Name →
  ¬ Up-to-technique Up-to-bisimilarity-and-context
¬-up-to-bisimilarity-and-context a =
  Up-to-technique Up-to-bisimilarity-and-context  ↝⟨ _$ R⊆ ⟩
  R ⊆ Bisimilarity ∞                              ↝⟨ R⊈∼ ⟩□
  ⊥                                               □
  where
  data R : Rel₂ (# 0) Proc where
    base : R (a · ∅ , a · a · ∅)

  lemma : Up-to-bisimilarity-and-context R (∅ , a · ∅)
  lemma =
    op (a · ∅) ,
    symmetric op·∅ ,
    op (a · a · ∅) ,
    (op (hole fzero) , a · ∅ , a · a · ∅ , refl , refl , base) ,
    op··∅

  R⊆ : R ⊆ ⟦ StepC ⟧ (Up-to-bisimilarity-and-context R)
  R⊆ base =
    ⟨ (λ { action → a · ∅ , action , lemma })
    , (λ { action → ∅     , action , lemma })
    ⟩

  R⊈∼ : ¬ R ⊆ Bisimilarity ∞
  R⊈∼ =
    R ⊆ Bisimilarity ∞  ↝⟨ (λ R⊆∼ → R⊆∼ base) ⟩
    a · ∅ ∼ a · a · ∅   ↝⟨ a≁b·c ⟩□
    ⊥                   □

-- The last result above can be used to give another proof showing
-- that op-cong cannot preserve the size of its argument (assuming
-- that Name is inhabited).

op-cong-cannot-preserve-size′ :
  Name →
  ¬ (∀ {i P Q} → [ i ] P ∼ Q → [ i ] op P ∼ op Q)
op-cong-cannot-preserve-size′ a =
  (∀ {i P Q} → [ i ] P ∼ Q → [ i ] op P ∼ op Q)               ↝⟨ (λ op-cong C P∼Q → []-cong op-cong C (λ _ → P∼Q)) ⟩

  (∀ {i P Q} (C : Context 1) → [ i ] P ∼ Q →
   [ i ] C [ (λ _ → P) ] ∼ C [ (λ _ → Q) ])                   ↝⟨ (λ []-cong → λ where
                                                                    {x = P , Q} (_ , P∼C[R₁] , _ ,
                                                                                (C , R₁ , R₂ , refl , refl , R₁∼R₂) , C[R₂]∼Q) →

                                                                      P                 ∼⟨ P∼C[R₁] ⟩
                                                                      C [ (λ _ → R₁) ]  ∼⟨ []-cong C R₁∼R₂ ⟩
                                                                      C [ (λ _ → R₂) ]  ∼⟨ C[R₂]∼Q ⟩■
                                                                      Q) ⟩
  (∀ {i} → Up-to-bisimilarity-and-context (Bisimilarity i) ⊆
           Bisimilarity i)                                    ↝⟨ _⇔_.from (monotone→⇔ up-to-bisimilarity-and-context-monotone) ⟩

  Size-preserving Up-to-bisimilarity-and-context              ↝⟨ size-preserving→up-to ⟩

  Up-to-technique Up-to-bisimilarity-and-context              ↝⟨ ¬-up-to-bisimilarity-and-context a ⟩□

  ⊥                                                           □
  where
  []-cong :
    (∀ {i P Q} → [ i ] P ∼ Q → [ i ] op P ∼ op Q) →
    ∀ {i n Ps Qs}
    (C : Context n) → (∀ x → [ i ] Ps x ∼ Qs x) →
    [ i ] C [ Ps ] ∼ C [ Qs ]
  []-cong op-cong (hole x) Ps∼Qs = Ps∼Qs x
  []-cong op-cong (op C)   Ps∼Qs = op-cong ([]-cong op-cong C Ps∼Qs)
  []-cong op-cong (a · C)  Ps∼Qs = ·-cong ([]-cong op-cong C Ps∼Qs)
  []-cong op-cong ∅        Ps∼Qs = reflexive

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
open import Relation.Binary.Core

module SelectSort.Everything {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)
                  (trans≤ : Transitive _≤_) where

open import SelectSort.Correctness.Order _≤_ tot≤ trans≤
open import SelectSort.Correctness.Permutation _≤_ tot≤

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
------------------------------------------------------------------------
-- Trees
------------------------------------------------------------------------

-- This example is based on one in Wadler's "A prettier printer".

{-# OPTIONS --guardedness #-}

module Examples.Tree where

open import Codata.Musical.Notation
open import Data.List
open import Data.List.NonEmpty as List⁺
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Examples.Identifier
import Grammar.Infinite
import Pretty
open import Renderer
open import Utilities

data Tree : Set where
  node : Identifier → List Tree → Tree

module _ where

  open Grammar.Infinite

  mutual

    tree : Grammar Tree
    tree = node <$> identifier-w ⊛ brackets

    brackets : Grammar (List Tree)
    brackets = return []
             ∣ List⁺.toList <$> (symbol′ "[" ⊛> ♯ trees <⊛ symbol′ "]")

    trees : Grammar (List⁺ Tree)
    trees = _∷_ <$> tree ⊛ commas-and-trees

    commas-and-trees : Grammar (List Tree)
    commas-and-trees = (symbol′ "," ⊛> tree) ⋆

open Pretty

-- Wadler presents two pretty-printers for trees in his final code
-- listing (§11.7). I've included corresponding, but not quite
-- identical, implementations here.
--
-- (One of Wadler's implementations is buggy: recursive calls to
-- showTree/showTrees should most likely have referred to
-- showTree'/showTrees'. The code below is intended to match a
-- corrected version of Wadler's.)

module Printer₁ where

  mutual

    tree-printer : Pretty-printer tree
    tree-printer (node s ts) =
      group (<$> identifier-w-printer s ⊛
             nest (List⁺.length s) (brackets-printer ts))

    brackets-printer : Pretty-printer brackets
    brackets-printer []       = left nil
    brackets-printer (t ∷ ts) =
      right (<$> (symbol ⊛> nest 1 (trees-printer (t ∷ ts)) <⊛ symbol))

    trees-printer : Pretty-printer trees
    trees-printer (t ∷ ts) =
      <$> tree-printer t ⊛ commas-and-trees-printer ts

    commas-and-trees-printer : Pretty-printer commas-and-trees
    commas-and-trees-printer []       = nil-⋆
    commas-and-trees-printer (t ∷ ts) =
      cons-⋆ (symbol-line ⊛> tree-printer t)
             (commas-and-trees-printer ts)

module Printer₂ where

  mutual

    tree-printer : Pretty-printer tree
    tree-printer (node s ts) =
      <$> identifier-w-printer s ⊛ brackets-printer ts

    brackets-printer : Pretty-printer brackets
    brackets-printer []       = left nil
    brackets-printer (t ∷ ts) =
      right (<$> bracket 7 (trees-printer (t ∷ ts)))

    trees-printer : Pretty-printer trees
    trees-printer (t ∷ ts) =
      <$> tree-printer t ⊛ commas-and-trees-printer ts

    commas-and-trees-printer : Pretty-printer commas-and-trees
    commas-and-trees-printer []       = nil-⋆
    commas-and-trees-printer (t ∷ ts) =
      cons-⋆ (symbol-line ⊛> tree-printer t)
             (commas-and-trees-printer ts)

t : Tree
t = node (str⁺ "aaa")
      (node (str⁺ "bbbbb")
         (node (str⁺ "ccc") [] ∷
          node (str⁺ "dd") [] ∷
          []) ∷
       node (str⁺ "eee") [] ∷
       node (str⁺ "ffff")
         (node (str⁺ "gg") [] ∷
          node (str⁺ "hhh") [] ∷
          node (str⁺ "ii") [] ∷
          []) ∷
       [])

test₁ : render 0 (Printer₁.tree-printer t) ≡
        "aaa[bbbbb[ccc,\n          dd],\n    eee,\n    ffff[gg,\n         hhh,\n         ii]]"
test₁ = refl

test₂ : render 30 (Printer₁.tree-printer t) ≡
        "aaa[bbbbb[ccc, dd],\n    eee,\n    ffff[gg, hhh, ii]]"
test₂ = refl

test₃ : render 0 (Printer₂.tree-printer t) ≡
        "aaa[\n  bbbbb[\n    ccc,\n    dd\n  ],\n  eee,\n  ffff[\n    gg,\n    hhh,\n    ii\n  ]\n]"
test₃ = refl

test₄ : render 80 (Printer₂.tree-printer t) ≡
        "aaa[ bbbbb[ ccc, dd ], eee, ffff[ gg, hhh, ii ] ]"
test₄ = refl

max_stars_repo_name: nad/pretty

max_issues_repo_name: nad/pretty

max_forks_repo_name: nad/pretty


text:
open import Agda.Primitive
open import Agda.Builtin.Equality   renaming (_≡_ to _==_) --(( If I want to rename the built-in equality ))

-- What follows is an attempt to formalize multicategories. For this purpose, we also need to define lists, since the source of a multimap in a multicategory is a list.
-- For the moment, I do not try to prove that the lists an the associated concatenation form a monoid (because I do not know if this is useful or not).

module MultiCategories where

  -- ** Function extensionality **
  postulate
    funext : ∀ {X : Set} {Y : X → Set} {f g : ∀ (x : X) → (Y x)} → (∀ (x : X) → ((f x) == (g x))) → (f == g)

  -- ** Lists **

  -- We first define lists
  data List {l : Level} (A : Set l) : Set l where
    [] : List A
    _::_ : A → List A → List A

  infixr 30 _::_

  open List

  -- We define equality on lists, that extends the built-in equality (since for the moment, we dont need other definitions of equality → but maybe we could do something more general by asking the "equality" as a parameter ?)
  data _≡ᴸ_ {l : Level} {A : Set l} : (u v : List {l} A) → Set (lsuc l) where
    eq-nil : [] ≡ᴸ []
    eq-cons : ∀ (x y : A) (su sv : List A) → (x == y) → (su ≡ᴸ sv) → ( (x :: su) ≡ᴸ (y :: sv))

  -- We define the mapping of lists
  list-map : ∀ {l : Level} {A B : Set l} → (f : A → B) → List A → List B
  list-map f [] = []
  list-map f (x :: u) = ((f x) :: (list-map f u))

  -- We define the concatenation of lists
  _++_ : ∀ {l}{A : Set l} → List A → List A → List A
  [] ++ ys = ys
  (x :: xs) ++ ys = x :: (xs ++ ys)

  -- We define a fold function
  fold : ∀ {l : Level} {A B : Set l} → (A → B → B) → B → List A → B
  fold _⊗_ e [] =  e
  fold _⊗_ e (x :: xs)  =  x ⊗ (fold _⊗_ e xs)

  -- We define a flatten function
  flatten : ∀ {l : Level} {A : Set l} → (u : List ( List A)) → (List A)
  flatten [] = []
  flatten (x :: xs) = x ++ (flatten xs)
  --  (I wanted to do this with the above fold function, which would be more elegant, but I don't know why, I miserably failed at it - must be tired)

  -- We define a function that takes a list of functions and a list of arguments and apply the functions point to point
  list-apply : ∀ {l : Level} {A B : Set l} → (list-f : List (A → B)) → (list-arg : List A) → List B
  list-apply [] [] = []
  list-apply (f :: fs) [] = []
  list-apply [] (x :: xs) = []
  list-apply (f :: fs) (x :: xs) = (f x) :: (list-apply fs xs)
  -- The two cases in the middle should be forbidden, but I don't know how to do this

  -- ** Multicategories **

  -- -- We first define the multimaps on a set
  -- data Multimap {l : Level} {O : Setl l} : Set l where
  --   map : ()

  record MultiCategory {l : Level} : Set (lsuc l) where
    field
      -- Objects and maps
      object : Set l
      multimap : Set l
      sources : ∀ (m : multimap) → List object
      target : ∀ (m : multimap) → object
      -- Composition and associated equations / conditions
      _∘_ : ∀ (f : multimap) → (list : List multimap) → multimap
      plug : ∀ {g : multimap} → {f : multimap} → {list : List multimap} → {g == (f ∘ list)} →  (sources f) ≡ᴸ (list-map target list)
      dom-comp : ∀ {f : multimap} → {list : List multimap} → ((flatten (list-map sources list)) ≡ᴸ (sources (f ∘ list)))
      comp-codom : ∀ (f : multimap) → (list : List multimap) → (target f == target (f ∘ list))
      -- Identities and associated equations / conditions
      id : ∀ (o : object) → multimap
      id-dom-codom : ∀ (o : object) → (sources (id o) == o :: [] )
      id-codom :  ∀ (o : object) → (target (id o) == o)
      id-left : ∀ {o : object} {f : multimap} → {f == id o} → (list : List multimap) → ( (f ∘ list) == f)
      id-rigth : ∀ {f : multimap} {list : List multimap} → {list ≡ᴸ (list-map id (sources f))} → ((f ∘ list) == f)
      -- Associativity
      assoc : ∀ {f : multimap} {list-g : List multimap} {list-h : List (List multimap)} → (f ∘ (list-apply (list-map _∘_ list-g) list-h)) == ( (f ∘ list-g) ∘ (flatten list-h))

  open MultiCategory

  -- List over a list
  data ListOver {l : Level} {A : Set l} (B : A → Set l) : List A → Set l where
    [[]] : ListOver B []
    _:::_ : ∀ {x xs} → (y : B x) → (ys : ListOver B xs) → ListOver B (x :: xs)

  infixr 25 _:::_

  over-map : ∀ {l : Level} {A : Set l} {B : A → Set l} {xs} {C : Set l} → (∀ {x} → B x → C) → ListOver B xs → List C
  over-map f [[]] = []
  over-map f (y ::: ys) = f y :: over-map f ys

  over-over-map : ∀ {l : Level} {A : Set l} {B : A → Set l} {xs} {C : A → Set l} → (∀ {x} → B x → C x) → ListOver B xs → ListOver C xs
  over-over-map f [[]] = [[]]
  over-over-map f (y ::: ys) = f y ::: over-over-map f ys

  over-lift : ∀ {l : Level} {A : Set l} (list : List A) → ListOver (λ x → A) list
  over-lift [] = [[]]
  over-lift (y :: ys) = y ::: (over-lift ys)

  over-flatten : ∀ {l : Level} {A B : Set l} {list : List A} (list-ov : ListOver (λ x → List B) list) → List B
  over-flatten [[]] = []
  over-flatten (x ::: xs) = x ++ (over-flatten xs)

  -- Dependent sum
  record Σ {l} (A : Set l) (B : A → Set l) : Set l where
    constructor ⟨_,_⟩
    field
      π₁ : A
      π₂ : B π₁

  open Σ

  -- Shortcuts to map the projections on lists when the dependent sum is a "product"
  list-π₁ : ∀ {l : Level} {A : Set l} {B} (list : List ( Σ {l} A B)) → List A
  list-π₁ list = list-map π₁ list

  list-π₂ : ∀ {l : Level} {A C : Set l} (list : List ( Σ {l} A ( λ x → C))) → List C
  list-π₂ list = list-map π₂ list

  -- A more dependent attempt at multicategories
  record MultiCategory2 {l : Level} : Set (lsuc l) where
    field
      object : Set l
      multimap : List object → object → Set l
      𝟙 : ∀ {x} → multimap (x :: []) x
      _•_ : ∀ {ys x} → multimap ys x → ∀ (gs : ListOver (λ y → Σ (List object) (λ zs → multimap zs y)) ys) →
            multimap (flatten (over-map π₁ gs)) x
      -- Another attempt to define multimaps, "putting the dependance elsewhere"
      _●_ : ∀ {x : object} {ys : List (Σ (List object) (λ x → object))} → multimap (list-π₂ ys) x → ListOver (λ y → multimap (π₁ y) (π₂ y)) ys → multimap (flatten (list-π₁ ys)) x
      -- here complications start
      -- 𝟙-left : ∀ {ys x} → (f : multimap ys x) → 𝟙 • (⟨ ys , f ⟩ ::: [[]]) == f
      -- 𝟙-right : ∀ {ys x} → (f : multimap ys x) → f • (over-over-map ? (over-lift ys)) == f
      --(ListOver ( λ y → ⟨ x ::: [[]] , 𝟙 ⟩ ) ys) == f
      -- Attempt with the alternative composition
      𝟙-left-● : ∀ {x ys} → (f : multimap ys x) → 𝟙 ● (f ::: [[]]) == f -- Here it seems that we have a lemma to prove to say that ys = (ys ++ flatten (list-map π₁ [])). Do we do it locally or would it be useful to have a more genral lemma ?

-- Here I tried to fix 𝟙-left and to define 𝟙-right, but I did not manage to do it, it both cases. Maybe we should revise the definition of _•_ ?
-- Agda seems to struggle with the fact that thnigs that should be equal are not equal by definition (conversion/reduction problems). Maybe there are some lemmas to prove here.
-- Also, I do not understand why we use the "over-map" : it would feel more natural to me if, once we lift a list to a dependent one, and use dependant lists, we only use dependeant lists, that's why I defined over-lift and over-over-map. (I also defined an "over-flatten" but don't know if it's useful)

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
module NotLinearPat where

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

bad : Nat -> Nat -> Nat
bad x x = zero
bad x y = succ zero

max_stars_repo_name: andreasabel/miniagda

max_issues_repo_name: andreasabel/miniagda

max_forks_repo_name: andreasabel/miniagda


text:
------------------------------------------------------------------------
-- agda-misc
-- All modules
------------------------------------------------------------------------

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

module AgdaMiscEverything where

------------------------------------------------------------------------
-- Algorithms

-- Insertion sort
import Algorithms.List.Sort.Insertion

import Algorithms.List.Sort.Insertion.Properties

-- Quicksort
import Algorithms.List.Sort.Quick

import Algorithms.List.Sort.Quick.Properties

------------------------------------------------------------------------
-- Constructive mathematics

-- Definitions of Axioms that are nonconstructive
import Constructive.Axiom

import Constructive.Axiom.Properties

import Constructive.Axiom.Properties.Base

import Constructive.Axiom.Properties.Base.Lemma

import Constructive.Axiom.Properties.Bool

import Constructive.Axiom.Properties.Transport

-- Alternative proof of LLPO => MP∨
import Constructive.Axiom.Properties.Alternative

-- Combinators for reasoning
import Constructive.Combinators

import Constructive.Common

-- Searchable set
import Constructive.Searchable

-- Experiment

-- Category theory
import Experiment.Categories.Solver.Category

import Experiment.Categories.Solver.Category.Example

import Experiment.Categories.Solver.Category.Cartesian

import Experiment.Categories.Solver.Category.Cartesian.Example

import Experiment.Categories.Solver.Functor

import Experiment.Categories.Solver.Functor.Example

import Experiment.Categories.Solver.MultiFunctor

import Experiment.Categories.Solver.MultiFunctor.Example

------------------------------------------------------------------------
-- Formal language

import Math.FormalLanguage

------------------------------------------------------------------------
-- Googology

import Math.Googology.Function

import Math.Googology.Function.Properties

------------------------------------------------------------------------
-- Number theory

-- Fibonacci number
import Math.NumberTheory.Fibonacci.Generic

import Math.NumberTheory.Fibonacci.Nat

import Math.NumberTheory.Fibonacci.Nat.Properties

-- Summation
import Math.NumberTheory.Summation.Generic

import Math.NumberTheory.Summation.Generic.Properties

import Math.NumberTheory.Summation.Nat

import Math.NumberTheory.Summation.Nat.Properties

-- Product
import Math.NumberTheory.Product.Generic

import Math.NumberTheory.Product.Generic.Properties

import Math.NumberTheory.Product.Nat

import Math.NumberTheory.Product.Nat.Properties

------------------------------------------------------------------------
-- Type theory

-- Natural number
import TypeTheory.Nat.Operations

import TypeTheory.Nat.Properties

import TypeTheory.Nat.Instance

-- Homotopy Type Theory
import TypeTheory.HoTT.Base

import TypeTheory.HoTT.Data.Empty.Properties

import TypeTheory.HoTT.Data.Sum.Properties

import TypeTheory.HoTT.Function.Properties

import TypeTheory.HoTT.Relation.Nullary.Negation.Properties

-- Identity type
import TypeTheory.Identity


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra.Ideal where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Powerset

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Ideal renaming (IdealsIn to IdealsInCommRing;
                                                     makeIdeal to makeIdealCommRing)
open import Cubical.Algebra.CommAlgebra

private
  variable
    ℓ : Level

module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
  IdealsIn : Type _
  IdealsIn = IdealsInCommRing (CommAlgebra→CommRing A)

  open CommAlgebraStr (snd A)

  makeIdeal : (I : fst A → hProp ℓ)
              → (+-closed : {x y : fst A} → x ∈ I → y ∈ I → (x + y) ∈ I)
              → (0-closed : 0a ∈ I)
              → (·-closedLeft : {x : fst A} → (r : fst A) → x ∈ I → r · x ∈ I)
              → IdealsIn
  makeIdeal = makeIdealCommRing {R = CommAlgebra→CommRing A}

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
-- Copyright:  (c) 2016 Ertugrul Söylemez
-- License:    BSD3
-- Maintainer: Ertugrul Söylemez <esz@posteo.de>

module Algebra.Group.Monoid where

open import Algebra.Category
open import Algebra.Group.Semigroup
open import Core

-- A monoid is a semigroup with an identity element.

record IsMonoid {a r} (S : Semigroup {a} {r}) : Set (a ⊔ r) where
  open Semigroup S

  field
    id : A
    left-id  : ∀ x → id ⋄ x ≈ x
    right-id : ∀ x → x ⋄ id ≈ x

  category : Category
  category =
    record {
      semigroupoid = semigroupoid;
      id = id;
      left-id = left-id;
      right-id = right-id
    }

  open Category category public
    using (id-unique; Iso)

record Monoid {a r} : Set (lsuc (a ⊔ r)) where
  field
    semigroup : Semigroup {a} {r}
    isMonoid  : IsMonoid semigroup

  open Semigroup semigroup public
  open IsMonoid isMonoid public

-- A monoid morphism is a function that maps the elements of one monoid
-- to another while preserving the compositional structure as well as
-- identity.

record MonoidMorphism
           {ma mr na nr}
           (M : Monoid {ma} {mr})
           (N : Monoid {na} {nr})
           : Set (ma ⊔ mr ⊔ na ⊔ nr)
       where

  private
    module M = Monoid M
    module N = Monoid N

  field semigroupMorphism : SemigroupMorphism M.semigroup N.semigroup
  open SemigroupMorphism semigroupMorphism public

  field
    id-preserving : map M.id N.≈ N.id

  functor : Functor M.category N.category
  functor =
    record {
      semifunctor = semifunctor;
      id-preserving = id-preserving
    }

  open Functor functor public
    using (Iso-preserving)

-- An equivalence relation on monoid morphisms that considers monoid
-- morphisms to be equal iff they map every element in the domain to the
-- same element in the codomain.

MonoidMorphismEq :
  ∀ {ma mr na nr}
    {M : Monoid {ma} {mr}} {N : Monoid {na} {nr}}
  → Equiv (MonoidMorphism M N)
MonoidMorphismEq {N = N} =
  record {
    _≈_ = λ F G →
            let module F = MonoidMorphism F
                module G = MonoidMorphism G
            in ∀ x → F.map x ≈ G.map x;
    refl = λ _ → refl;
    sym = λ x≈y x → sym (x≈y x);
    trans = λ x≈y y≈z x → trans (x≈y x) (y≈z x)
  }

  where
  module N = Monoid N
  open Equiv N.Eq

-- Category of monoids.

Monoids : ∀ {a r} → Category
Monoids {a} {r} =
  record {
    semigroupoid = record {
      Ob = Monoid {a} {r};
      Hom = MonoidMorphism;
      Eq = MonoidMorphismEq;
      _∘_ = _∘_;
      ∘-cong = λ {_} {_} {_} {f1} {f2} {g1} {g2} → ∘-cong {f1 = f1} {f2} {g1} {g2};
      assoc = assoc
    };
    id = id;
    left-id = left-id;
    right-id = right-id
  }

  where
  open module MyEquiv {M : Monoid} {N : Monoid} = Equiv (MonoidMorphismEq {M = M} {N})

  id : ∀ {M} → MonoidMorphism M M
  id {M} =
    record {
      semigroupMorphism = record {
        map = Sets.id;
        map-cong = Sets.id;
        ⋄-preserving = λ x y → M.refl
      };
      id-preserving = M.refl
    }

    where
    module M = Monoid M

  _∘_ : ∀ {M N O} → MonoidMorphism N O → MonoidMorphism M N → MonoidMorphism M O
  _∘_ {M} {N} {O} f g =
    record {
      semigroupMorphism = f.semigroupMorphism Semigroups.∘ g.semigroupMorphism;
      id-preserving =
        O.begin
          f.map (g.map M.id) O.≈[ f.map-cong g.id-preserving ]
          f.map N.id         O.≈[ f.id-preserving ]
          O.id
        O.qed
    }

    where
    module f = MonoidMorphism f
    module g = MonoidMorphism g
    module M = Monoid M
    module N = Monoid N
    module O = Monoid O

  ∘-cong :
    ∀ {M N O}
      {f1 f2 : MonoidMorphism N O}
      {g1 g2 : MonoidMorphism M N}
    → f1 ≈ f2
    → g1 ≈ g2
    → f1 ∘ g1 ≈ f2 ∘ g2
  ∘-cong {O = O} {f1} {f2} {g1} {g2} f1≈f2 g1≈g2 x =
    O.begin
      f1.map (g1.map x) O.≈[ f1.map-cong (g1≈g2 x) ]
      f1.map (g2.map x) O.≈[ f1≈f2 (g2.map x) ]
      f2.map (g2.map x)
    O.qed

    where
    module O = Monoid O
    module f1 = MonoidMorphism f1
    module f2 = MonoidMorphism f2
    module g1 = MonoidMorphism g1
    module g2 = MonoidMorphism g2

  assoc :
    ∀ {M N O P}
      (f : MonoidMorphism O P)
      (g : MonoidMorphism N O)
      (h : MonoidMorphism M N)
    → (f ∘ g) ∘ h ≈ f ∘ (g ∘ h)
  assoc {P = P} _ _ _ _ = P.refl
    where
    module P = Monoid P

  left-id : ∀ {M N} (f : MonoidMorphism M N) → id ∘ f ≈ f
  left-id {N = N} _ _ = N.refl
    where
    module N = Monoid N

  right-id : ∀ {M N} (f : MonoidMorphism M N) → f ∘ id ≈ f
  right-id {N = N} _ _ = N.refl
    where
    module N = Monoid N

max_stars_repo_name: esoeylemez/agda-simple

max_issues_repo_name: esoeylemez/agda-simple

max_forks_repo_name: esoeylemez/agda-simple


text:
open import Agda.Primitive
open import Semigroup

module Monoid where

  record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
    constructor _,_
    field
      proj₁ : A
      proj₂ : B proj₁

  Σ-syntax : ∀ {a b} (A : Set a) → (A → Set b) → Set (a ⊔ b)
  Σ-syntax = Σ

  syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

  _×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
  A × B = Σ[ x ∈ A ] B

  record Monoid {A : Set} (_∙_ : A → A → A) (ε : A) : Set where
    field
      semigroup : Semigroup _∙_
      identity : (∀ x → ε ∙ x ≡ x) × (∀ x → x ∙ ε ≡ x)

max_stars_repo_name: cantsin/agda-experiments

max_issues_repo_name: cantsin/agda-experiments

max_forks_repo_name: cantsin/agda-experiments


text:
{-# OPTIONS --cubical-compatible --rewriting --confluence-check #-}

open import Issue1719.Common
open import Issue1719.Spans
open import Issue1719.Pushouts

module _ {d : Span} {l} {P : Pushout d → Set l}
  (left* : (a : Span.A d) → P (left a))
  (right* : (b : Span.B d) → P (right b))
  (glue* : (c : Span.C d) → left* (Span.f d c) == right* (Span.g d c) [ P ↓ glue c ]) where

  test : (a : Span.A d) → Pushout-elim {P = P} left* right* glue* (left a) ↦ left* a
  test a = idr


text:
-- Andreas, 2017-05-17, issue #2574 reported by G. Allais

-- This module is intentionally without name.

module _ where

private
  postulate A : Set


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Instantiates the ring solver with two copies of the same ring with
-- decidable equality
------------------------------------------------------------------------

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

open import Algebra.Solver.Ring.AlmostCommutativeRing
open import Relation.Binary
open import Relation.Binary.Consequences using (dec⟶weaklyDec)

module Algebra.Solver.Ring.Simple
         {r₁ r₂} (R : AlmostCommutativeRing r₁ r₂)
         (_≟_ : Decidable (AlmostCommutativeRing._≈_ R))
         where

open AlmostCommutativeRing R
import Algebra.Solver.Ring as RS
open RS rawRing R (-raw-almostCommutative⟶ R) (dec⟶weaklyDec _≟_) public


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

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

open VectorSpace(vectorSpace)

open import Data.Tuple as Tuple using (_,_)
open import Logic.Propositional
open import Logic.Predicate
import      Lvl
open import Sets.ExtensionalPredicateSet as PredSet using (PredSet ; _∈_ ; [∋]-binaryRelator)
open import Structure.Container.SetLike using (SetElement)
private open module SetLikeFunctionProperties{ℓ} = Structure.Container.SetLike.FunctionProperties{C = PredSet{ℓ}(V)}{E = V}(_∈_)
open import Structure.Operator
open import Structure.Operator.Proofs.Util
open import Structure.Operator.Properties
open import Structure.Operator.Vector
open import Structure.Operator.Vector.Subspace ⦃ vectorSpace = vectorSpace ⦄
open import Syntax.Transitivity

private variable ℓ ℓ₁ ℓ₂ ℓₗ : Lvl.Level

module _ where
  module _ where
    -- TODO: This operator can also be constructed for vector spaces, not just subspaces
    _+ˢᵘᵇ_ : SubspaceObject{ℓ₁} → SubspaceObject{ℓ₂} → SubspaceObject
    ([∃]-intro V₁ ⦃ p₁ ⦄) +ˢᵘᵇ ([∃]-intro V₂ ⦃ p₂ ⦄) = [∃]-intro (PredSet.map₂(_+ᵥ_) V₁ V₂) ⦃ p ⦄ where
      p : Subspace(PredSet.map₂(_+ᵥ_) V₁ V₂)
      ∃.witness (Structure.Container.SetLike.FunctionProperties._closed-under₂_.proof (Subspace.add-closure p) ([∃]-intro(a₁ , a₂)) ([∃]-intro(b₁ , b₂))) = ((a₁ +ᵥ b₁) , (a₂ +ᵥ b₂))
      ∃.proof (Structure.Container.SetLike.FunctionProperties._closed-under₂_.proof (Subspace.add-closure p) {a}{b} ([∃]-intro ([∧]-intro a₁ a₂) ⦃ [∧]-intro ([∧]-intro a₁V₁ a₂V₂) a₁a₂a ⦄) ([∃]-intro (b₁ , b₂) ⦃ [∧]-intro ([∧]-intro b₁V₁ b₂V₂) b₁b₂b ⦄)) = [∧]-intro ([∧]-intro l₁ l₂) r where
        l₁ : (a₁ +ᵥ b₁) ∈ V₁
        l₁ = (V₁ closureUnder₂(_+ᵥ_)) a₁V₁ b₁V₁
        l₂ : (a₂ +ᵥ b₂) ∈ V₂
        l₂ = (V₂ closureUnder₂(_+ᵥ_)) a₂V₂ b₂V₂
        r : (a₁ +ᵥ b₁) +ᵥ (a₂ +ᵥ b₂) ≡ a +ᵥ b
        r =
          (a₁ +ᵥ b₁) +ᵥ (a₂ +ᵥ b₂) 🝖[ _≡_ ]-[ One.associate-commute4-c {_▫_ = _+ᵥ_} ⦃ op = [+ᵥ]-binary-operator ⦄ ⦃ assoc = [+ᵥ]-associativity ⦄ ⦃ comm = [+ᵥ]-commutativity ⦄ ] -- TODO: Why are the instances not inferred?
          (a₁ +ᵥ a₂) +ᵥ (b₁ +ᵥ b₂) 🝖[ _≡_ ]-[ congruence₂(_+ᵥ_) ⦃ [+ᵥ]-binary-operator ⦄ a₁a₂a b₁b₂b ]
          a +ᵥ b                   🝖-end
      ∃.witness (Structure.Container.SetLike.FunctionProperties._closed-under₁_.proof (Subspace.mul-closure p {s}) ([∃]-intro(v₁ , v₂))) = ((s ⋅ₛᵥ v₁) , (s ⋅ₛᵥ v₂))
      ∃.proof (Structure.Container.SetLike.FunctionProperties._closed-under₁_.proof (Subspace.mul-closure p {s}) {v} ([∃]-intro(v₁ , v₂) ⦃ [∧]-intro ([∧]-intro v₁V₁ v₂V₂) v₁v₂v ⦄)) = [∧]-intro ([∧]-intro l₁ l₂) r where
        l₁ : (s ⋅ₛᵥ v₁) ∈ V₁
        l₁ = (V₁ closureUnder₁(s ⋅ₛᵥ_)) v₁V₁
        l₂ : (s ⋅ₛᵥ v₂) ∈ V₂
        l₂ = (V₂ closureUnder₁(s ⋅ₛᵥ_)) v₂V₂
        r : (s ⋅ₛᵥ v₁) +ᵥ (s ⋅ₛᵥ v₂) ≡ (s ⋅ₛᵥ v)
        r =
          (s ⋅ₛᵥ v₁) +ᵥ (s ⋅ₛᵥ v₂) 🝖[ _≡_ ]-[ distributivityₗ(_⋅ₛᵥ_)(_+ᵥ_) ]-sym
          s ⋅ₛᵥ (v₁ +ᵥ v₂)         🝖[ _≡_ ]-[ congruence₂ᵣ(_⋅ₛᵥ_)(s) v₁v₂v ]
          s ⋅ₛᵥ v                  🝖-end

  -- TODO: Formulate
  -- [⊕ˢᵘᵇ]-span-vectorSpace : (V₁ ⊕ V₂ ⊕ … ≡ₛ 𝐔) ↔ (∀{v₁}{v₂}{…} → (v₁ ∈ V₁) → (v₂ ∈ V₂) → … → (v₁ + v₂ + … ≡ 𝟎ᵥ) → ((v₁ ≡ 𝟎ᵥ) ∧ (v₂ ≡ 𝟎ᵥ) ∧ …))
  -- [⊕ˢᵘᵇ]-span-existence-finite-space : Finite → ∃(\{(V₁ , V₂ , …) → V₁ ⊕ V₂ ⊕ … ≡ₛ 𝐔}) -- TODO: Just take the "standard" "axis aligned" subspaces

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 -v tc.with:100 #-}
module Issue818 where

data ⊤ : Set where
  tt : ⊤

Foo : {x : ⊤} → Set₁
Foo with tt
Foo {x = _} | tt = Set

-- Panic: wrong number of arguments in with clause: given 1, expected
-- 0
-- when checking that the clause
-- Foo with tt
-- Foo {x = _} | tt = Set
-- has type {⊤} → Set₁

-- The code above type-checks using Agda 2.3.0.1, but not with Agda
-- 2.3.2.

-- Andreas, 2013-03-08: same error thrown by

-- foo : ⊤ → Set₁
-- foo with tt
-- foo x | tt = Set

-- Implicit arguments are no longer eagerly introduced (see release notes
-- for 2.3.2, text for issue 679).

-- Should now throw a proper error message (not a panic).

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import Algebra.Apartness using (HeytingField)

module Data.Real.Abstract.Structures {c ℓ₁ ℓ₂} (f : HeytingField c ℓ₁ ℓ₂) where

open HeytingField f

open import Relation.Binary using (Rel; IsStrictTotalOrder)
open import Level using (_⊔_)
open import Data.Product using (_×_; ∃-syntax)

import Data.Nat as ℕ
open ℕ using (ℕ; zero; suc)

record IsOrderedHeytingField
  {r} (_<_ : Rel Carrier r) : Set (c ⊔ ℓ₁ ⊔ r)
  where

  field
    isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_
    ordered : ∀ a b c → a < b → (a + c) < (b + c) × (c + a) < (c + b)

_ℕ*_ : ℕ → Carrier → Carrier
zero ℕ* x = 1#
suc n ℕ* x = x * (n ℕ* x)

record IsArchimedanHeytingField
  {r} (_<_ : Rel Carrier r) : Set (c ⊔ ℓ₁ ⊔ r)
  where

  field
    dense : ∀ a b → a < b → ∃[ c ] (a < c) × (c < b)
    archimedan : ∀ a b → 0# < a → 0# < b → ∃[ n ] (b < (n ℕ* a))

max_stars_repo_name: cspollard/reals

max_issues_repo_name: cspollard/reals

max_forks_repo_name: cspollard/reals


text:
-- Proof of: ∀ (x : ND ℕ) → always (even (double (eo x))) ≡ tt

module even-double-eo where

open import bool
open import nat
open import eq
open import nat-thms
open import nondet
open import nondet-thms
open import functions

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

-- A definition of double with addition.
double : ℕ → ℕ
double x = x + x

-- even is a deterministic predicate:
even : ℕ → 𝔹
even zero = tt
even (suc 0) = ff
even (suc (suc x)) = even x

-- eo yields an even and odd number close to the input value:
eo : ℕ → ND ℕ
eo n = Val n ?? Val (suc n)

-- auxiliary property for x+x instead of double:
even-x+x : (x : ℕ) → even (x + x) ≡ tt
even-x+x zero = refl
even-x+x (suc x) rewrite +suc x x | even-x+x x = refl

-- (even (double x)) is always true:
even-double-is-true : ∀ (x : ℕ) → even (double x) ≡ tt
even-double-is-true x rewrite even-x+x x = refl

-- Proof of main result:
even-double-eo-true : (n : ℕ) → always ((even ∘ double) $* (eo n)) ≡ tt
even-double-eo-true n = always-$* (even ∘ double) (eo n) even-double-is-true

-- Alternative statement and proof:
double-eo-satisfy-even : ∀ (n : ℕ) → (double $* (eo n)) satisfy even ≡ tt
double-eo-satisfy-even n
  rewrite even-double-is-true n | +suc n n | even-double-is-true n = refl

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

max_stars_repo_name: mihanus/curry-agda

max_issues_repo_name: mihanus/curry-agda

max_forks_repo_name: mihanus/curry-agda


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

open import Polynomial.Parameters

module Polynomial.Solver
  {c r₁ r₂ r₃}
  (homo : Homomorphism c r₁ r₂ r₃)
  where

open import Data.Vec as Vec using (Vec)
open import Polynomial.Expr public
open import Algebra.Solver.Ring.AlmostCommutativeRing

open Homomorphism homo
open Eval homo

open import Polynomial.NormalForm.Definition coeffs
  using (Poly)
open import Polynomial.NormalForm.Operations coeffs
  using (_⊞_; _⊠_; ⊟_; _⊡_; κ; ι)

norm : ∀ {n} → Expr Raw.Carrier n → Poly n
norm (Κ x) = κ x
norm (Ι x) = ι x
norm (x ⊕ y) = norm x ⊞ norm y
norm (x ⊗ y) = norm x ⊠ norm y
norm (x ⊛ i) = norm x ⊡ i
norm (⊝ x) = ⊟ norm x

open import Polynomial.NormalForm.Semantics homo
  renaming (⟦_⟧ to ⟦_⟧ₚ)

⟦_⇓⟧ : ∀ {n} → Expr Raw.Carrier n → Vec Carrier n → Carrier
⟦ x ⇓⟧ = ⟦ norm x ⟧ₚ

import Polynomial.Homomorphism homo
  as Hom
open import Function

correct : ∀ {n} (e : Expr Raw.Carrier n) ρ → ⟦ e ⇓⟧ ρ ≈ ⟦ e ⟧ ρ
correct (Κ x) ρ = Hom.κ-hom x ρ
correct (Ι x) ρ = Hom.ι-hom x ρ
correct (x ⊕ y) ρ = Hom.⊞-hom (norm x) (norm y) ρ ⟨ trans ⟩ (correct x ρ ⟨ +-cong ⟩ correct y ρ)
correct (x ⊗ y) ρ = Hom.⊠-hom (norm x) (norm y) ρ ⟨ trans ⟩ (correct x ρ ⟨ *-cong ⟩ correct y ρ)
correct (x ⊛ i) ρ = Hom.⊡-hom (norm x) i ρ ⟨ trans ⟩ (Hom.pow-cong i (correct x ρ))
correct (⊝ x) ρ = Hom.⊟-hom (norm x) ρ ⟨ trans ⟩ -‿cong (correct x ρ)

open import Relation.Binary.Reflection setoid Ι ⟦_⟧ ⟦_⇓⟧ correct public

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Product.Relation.Binary.Pointwise.Dependent directly.
------------------------------------------------------------------------

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

module Data.Product.Relation.Pointwise.Dependent where

open import Data.Product.Relation.Binary.Pointwise.Dependent public


text:
module WellScopedTerms where

open import Library
open import Categories
open import Functors
open import Categories.Sets
open import Functors.Fin hiding (lift)
open import RMonads
open import Relation.Binary.HeterogeneousEquality
open Cat
open Fun

data Tm : ℕ → Set where
  var : ∀{n} → Fin n → Tm n
  lam : ∀{n} → Tm (suc n) → Tm n
  app : ∀{n} → Tm n → Tm n → Tm n

Ren : ℕ → ℕ → Set
Ren m n = Fin m → Fin n

-- Weakening a renaming (to push it under a lambda)

wk : ∀{m n} → Ren m n → Ren (suc m) (suc n)
wk f zero     = zero
wk f (suc i) = suc (f i)

-- Performing a renaming on an expression

ren : ∀{m n} → Ren m n → Tm m → Tm n
ren f (var i)   = var (f i)
ren f (app t u) = app (ren f t) (ren f u)
ren f (lam t)   = lam (ren (wk f) t)

-- Identity renaming

renId : ∀{n} → Ren n n
renId = id

-- Composition of renamings

renComp : ∀{m n o} → Ren n o → Ren m n → Ren m o
renComp f g = f ∘ g

-- we prove that wk is an endofunctor

wkid : ∀{n}(i : Fin (suc n)) → wk renId i ≅ id i
wkid zero    = refl
wkid (suc i) = refl

wkcomp : ∀{m n o}(f : Ren n o)(g : Ren m n)(i : Fin (suc m)) →
            wk (renComp f g) i ≅ renComp (wk f) (wk g) i
wkcomp f g zero    = refl
wkcomp f g (suc i) = refl

-- we prove that renamings is a functor

renid : ∀{n}(t : Tm n) → ren renId t ≅ t
renid (var i)   = refl
renid (app t u) = cong₂ app (renid t) (renid u)
renid (lam t)   =
  proof
  lam (ren (wk renId) t)
  ≅⟨ cong (λ f → lam (ren f t)) (ext wkid) ⟩
  lam (ren renId t)
  ≅⟨ cong lam (renid t) ⟩
  lam t
  ∎

rencomp : ∀{m n o}(f : Ren n o)(g : Ren m n)(t : Tm m) →
          ren (renComp f g) t ≅ ren f (ren g t)
rencomp f g (var i)   = refl
rencomp f g (app t u) = cong₂ app (rencomp f g t) (rencomp f g u)
rencomp f g (lam t)   =
  proof
  lam (ren (wk (renComp f g)) t)
  ≅⟨ cong (λ f → lam (ren f t)) (ext (wkcomp f g)) ⟩
  lam (ren (renComp (wk f) (wk g)) t)
  ≅⟨ cong lam (rencomp (wk f) (wk g) t) ⟩
  lam (ren (wk f) (ren (wk g) t))
  ∎

-- Substitutions

Sub : ℕ → ℕ → Set
Sub m n = Fin m → Tm n

-- Weaken a substitution to push it under a lambda

lift : ∀{m n} → Sub m n → Sub (suc m) (suc n)
lift f zero     = var zero
lift f (suc i) = ren suc (f i)

-- Perform substitution on an expression

sub : ∀{m n} → Sub m n → Tm m → Tm n
sub f (var i)   = f i
sub f (app t u) = app (sub f t) (sub f u)
sub f (lam t)   = lam (sub (lift f) t)

-- Identity substitution

subId : ∀{n} → Sub n n
subId = var

-- Composition of substitutions

subComp : ∀{m n o} → Sub n o → Sub m n → Sub m o
subComp f g = sub f ∘ g

-- lift is an endofunctor on substitutions and sub is a functor, we
-- need some auxilary lemmas for the composition cases

-- the conditions for identity are easy

liftid : ∀{n}(i : Fin (suc n)) → lift subId i ≅ subId i
liftid zero    = refl
liftid (suc i) = refl

subid : ∀{n}(t : Tm n) → sub subId t ≅ id t
subid (var i)   = refl
subid (app t u) =
  proof
  app (sub subId t) (sub subId u)
  ≅⟨ cong₂ app (subid t) (subid u) ⟩
  app t u
  ∎
subid (lam t)   =
  proof
  lam (sub (lift subId) t)
  ≅⟨ cong lam (cong (λ f → sub f t) (ext liftid)) ⟩
  lam (sub subId t)
  ≅⟨ cong lam (subid t) ⟩
  lam t
  ∎

-- for composition of subs (subcomp) and lifts (liftcomp) we need two
-- lemmas about how renaming and subs interact for these two lemmas we
-- need two lemmas about how lift and wk interact.

liftwk : ∀{m n o}(f : Sub n o)(g : Ren m n)(i : Fin (suc m)) →
            (lift f ∘ wk g) i ≅ lift (f ∘ g) i
liftwk f g zero    = refl
liftwk f g (suc i) = refl

subren : ∀{m n o}(f : Sub n o)(g : Ren m n)(t : Tm m) →
         (sub f ∘ ren g) t ≅ sub (f ∘ g) t
subren f g (var i)   = refl
subren f g (app t u) =
  proof
  app (sub f (ren g t)) (sub f (ren g u))
  ≅⟨ cong₂ app (subren f g t) (subren f g u) ⟩
  app (sub (f ∘ g) t) (sub (f ∘ g) u)
  ∎
subren f g (lam t)   =
  proof
  lam (sub (lift f) (ren (wk g) t))
  ≅⟨ cong lam (subren (lift f) (wk g) t) ⟩
  lam (sub (lift f ∘ wk g) t)
  ≅⟨ cong lam (cong (λ f₁ → sub f₁ t) (ext (liftwk f g))) ⟩
  lam (sub (lift (f ∘ g)) t)
  ∎

renwklift : ∀{m n o}(f : Ren n o)(g : Sub m n)(i : Fin (suc m)) →
               (ren (wk f) ∘ lift g) i ≅ lift (ren f ∘ g) i
renwklift f g zero    = refl
renwklift f g (suc i) =
  proof
  ren (wk f) (ren suc (g i))
  ≅⟨ sym (rencomp (wk f) suc (g i)) ⟩
  ren (wk f ∘ suc) (g i)
  ≡⟨⟩
  ren (suc ∘ f) (g i)
  ≅⟨ rencomp suc f (g i) ⟩
  ren suc (ren f (g i))
  ∎

rensub : ∀{m n o}(f : Ren n o)(g : Sub m n)(t : Tm m) →
         (ren f ∘ sub g) t ≅ sub (ren f ∘ g) t
rensub f g (var i)   = refl
rensub f g (app t u) =
  proof
  app (ren f (sub g t)) (ren f (sub g u))
  ≅⟨ cong₂ app (rensub f g t) (rensub f g u) ⟩
  app (sub (ren f ∘ g) t) (sub (ren f ∘ g) u)
  ∎
rensub f g (lam t)   =
  proof
  lam (ren (wk f) (sub (lift g) t))
  ≅⟨ cong lam (rensub (wk f) (lift g) t) ⟩
  lam (sub (ren (wk f) ∘ (lift g)) t)
  ≅⟨ cong (λ f → lam (sub f t)) (ext (renwklift f g)) ⟩
  lam (sub (lift (ren f ∘ g)) t)
  ∎

liftcomp : ∀{m n o}(f : Sub n o)(g : Sub m n)(i : Fin (suc m)) →
           lift (subComp f g) i ≅ subComp (lift f) (lift g) i
liftcomp f g zero    = refl
liftcomp f g (suc i) =
  proof
  ren suc (sub f (g i))
  ≅⟨ rensub suc f (g i) ⟩
  sub (ren suc ∘ f) (g i)
  ≅⟨ sym (subren (lift f) suc (g i)) ⟩
  sub (lift f) (ren suc (g i))
  ∎

subcomp : ∀{m n o}(f : Sub n o)(g : Sub m n)(t : Tm m) →
          sub (subComp f g) t ≅ (sub f ∘ sub g) t
subcomp f g (var i)   = refl
subcomp f g (app t u) =
  proof
  app (sub (subComp f g) t) (sub (subComp f g) u)
  ≅⟨ cong₂ app (subcomp f g t) (subcomp f g u) ⟩
  app (sub f (sub g t)) (sub f (sub g u))
  ∎
subcomp f g (lam t)   =
  proof
  lam (sub (lift (subComp f g)) t)
  ≅⟨ cong (λ f → lam (sub f t)) (ext (liftcomp f g)) ⟩
  lam (sub (subComp (lift f)(lift g)) t)
  ≅⟨ cong lam (subcomp (lift f) (lift g) t) ⟩
  lam (sub (lift f) (sub (lift g) t))
  ∎

TmRMonad : RMonad FinF
TmRMonad = record {
  T    = Tm;
  η    = var;
  bind = sub;
  law1 = ext subid;
  law2 = refl;
  law3 = ext (subcomp _ _)}

-- module

open import RMonads.Modules

-- any functor is a relative monad over itself (including FinF)
FinMonad : RMonad FinF
FinMonad = trivRM FinF

-- TM is module for Fin Monad This is not exactly the same as the
TmModFin : Mod FinMonad
TmModFin = mod Tm ren (ext renid) (ext (rencomp _ _))

-- in fact, any suitable functor is a module over FinMonad
FModFin' : (F : Fun Nats Sets) →  Mod FinMonad
FModFin' F = ModF (\ h → h , refl) id F

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


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

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

record R : Set where
  eta-equality
  constructor c

R' = R

postulate
  D : Set
  d : D
  f : R' → D -- = R → D
  x : R
  r : f x ≡ d

{-# REWRITE r #-}

-- SUCCEEDS:
_ : f c ≡ d
_ = refl

-- FAILS:
_ : f x ≡ d
_ = refl -- (*)

cong : (y : R') → x ≡ y → f x ≡ f y
cong _ refl = refl

-- SUCCEEDS:
_ : f x ≡ f c
_ = cong c refl

-- FAILS:
_ : f x ≡ f c
_ = refl -- = cong c refl

max_forks_repo_name: shlevy/agda


text:
------------------------------------------------------------------------
-- "Lenses" defined using bijections
------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}

import Equality.Path as P

module Lens.Non-dependent.Bijection
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Prelude

open import Bijection equality-with-J using (_↔_)
open import Equality.Path.Isomorphisms eq hiding (univ)
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J as F
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq
open import Surjection equality-with-J using (_↠_)
open import Univalence-axiom equality-with-J

open import Lens.Non-dependent eq
import Lens.Non-dependent.Higher      eq as Higher
import Lens.Non-dependent.Traditional eq as Traditional

private
  variable
    a b : Level

-- A "naive" definition of lenses using a bijection.
--
-- This definition is not in general isomorphic to Higher.Lens A B,
-- not even if A and B are sets (consider the case in which A and B
-- are empty; see ¬Higher-lens↠Lens below).

Lens : Set a → Set b → Set (lsuc (a ⊔ b))
Lens {a = a} {b = b} A B =
  ∃ λ (R : Set (a ⊔ b)) → A ↔ (R × B)

instance

  -- The lenses defined above have getters and setters.

  has-getter-and-setter :
    Has-getter-and-setter (Lens {a = a} {b = b})
  has-getter-and-setter = record
    { get = λ (_ , bij) a → proj₂ (_↔_.to bij a)
    ; set = λ (_ , bij) a b → _↔_.from bij (proj₁ (_↔_.to bij a) , b)
    }

-- Lens ⊥ ⊥ is isomorphic to Set something.

Lens-⊥-⊥↔Set :
  Lens (⊥ {ℓ = a}) (⊥ {ℓ = b}) ↔ Set (a ⊔ b)
Lens-⊥-⊥↔Set =
  Lens ⊥ ⊥               ↔⟨ (∃-cong λ _ → Eq.↔↔≃ ext (mono₁ 1 ⊥-propositional)) ⟩
  (∃ λ R → ⊥ ≃ (R × ⊥))  ↔⟨ (∃-cong λ _ → Eq.≃-preserves-bijections ext F.id ×-right-zero) ⟩
  (∃ λ R → ⊥ ≃ ⊥₀)       ↔⟨ (∃-cong λ _ → ≃⊥≃¬ ext) ⟩
  (∃ λ R → ¬ ⊥)          ↔⟨ drop-⊤-right (λ _ → ¬⊥↔⊤ {k = bijection} ext) ⟩□
  Set _                  □

-- There is a split surjection from Lens A B to Higher.Lens A B
-- (assuming univalence).

Lens↠Higher-lens :
  {A : Set a} {B : Set b} →
  Univalence (a ⊔ b) →
  Lens A B ↠ Higher.Lens A B
Lens↠Higher-lens {A = A} {B} univ = record
  { logical-equivalence = record
    { to   = λ { (R , A↔R×B) → Higher.isomorphism-to-lens A↔R×B }
    ; from = λ { l → R l , _≃_.bijection (equiv l) }
    }
  ; right-inverse-of = λ { l →
      _↔_.from (Higher.equality-characterisation₂ univ)
        ( (R l × ∥ B ∥  ↔⟨ drop-⊤-right (λ r → inhabited⇒∥∥↔⊤ (inhabited l r)) ⟩□
           R l          □)
        , λ _ → refl _
        ) }
  }
  where
  open Higher.Lens

-- However, there is in general no split surjection in the other
-- direction, not even for sets (assuming univalence).

¬Higher-lens↠Lens :
  Univalence (a ⊔ b) →
  ¬ ({A : Set a} {B : Set b} →
     Is-set A → Is-set B →
     Higher.Lens A B ↠ Lens A B)
¬Higher-lens↠Lens univ surj =
  ⊥-elim (subst F.id ⊤≡⊥ _)
  where
  ⊥-is-set : ∀ {ℓ} → Is-set (⊥ {ℓ = ℓ})
  ⊥-is-set = mono₁ 1 ⊥-propositional

  ⊤↠Set =
    ⊤                ↔⟨ inverse $ Higher.lens-from-⊥↔⊤ univ ⟩
    Higher.Lens ⊥ ⊥  ↝⟨ surj ⊥-is-set ⊥-is-set ⟩
    Lens ⊥ ⊥         ↔⟨ Lens-⊥-⊥↔Set ⟩□
    Set _            □

  ⊤≡⊥ : ↑ _ ⊤ ≡ ⊥
  ⊤≡⊥ =
    ↑ _ ⊤              ≡⟨ sym $ right-inverse-of _ ⟩
    to (from (↑ _ ⊤))  ≡⟨⟩
    to (from ⊥)        ≡⟨ right-inverse-of _ ⟩∎
    ⊥                  ∎
    where
    open _↠_ ⊤↠Set

-- The split surjection Lens↠Higher-lens preserves getters and
-- setters.

Lens↠Higher-lens-preserves-getters-and-setters :
  {A : Set a} {B : Set b}
  (univ : Univalence (a ⊔ b)) →
  Preserves-getters-and-setters-⇔ A B
    (_↠_.logical-equivalence (Lens↠Higher-lens univ))
Lens↠Higher-lens-preserves-getters-and-setters univ =
    (λ _ → refl _ , refl _)
  , (λ _ → refl _ , refl _)

max_stars_repo_name: Saizan/dependent-lenses

max_issues_repo_name: Saizan/dependent-lenses

max_forks_repo_name: Saizan/dependent-lenses


text:
module STLCRef.Semantics where

-- This file contains the definitional interpreter for STLC+Ref
-- described in Section 3 of the paper.

open import Agda.Primitive
open import Data.Unit
open import Data.Nat hiding (_⊔_ ; _^_)
open import Data.Integer hiding (_⊔_)
open import Data.List
open import Data.List.Properties.Extra
open import Data.List.All.Properties.Extra
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All as All
open import Data.List.Prefix
open import Data.Product
open import Data.Maybe hiding (_>>=_)
open import Function
open import Common.Weakening

------------
-- SYNTAX --
------------

-- These definitions correspond to Section 3.1, except we have
-- included numbers (integers) and integer operations in the language.

data Ty : Set

Ctx = List Ty

data Ty where
  _⇒_  : (a b : Ty) → Ty
  unit : Ty
  int  : Ty
  ref  : Ty -> Ty

data Expr (Γ : List Ty) : Ty → Set where
  unit  : Expr Γ unit
  var   : ∀ {t} → t ∈ Γ → Expr Γ t
  ƛ     : ∀ {a b} → Expr (a ∷ Γ) b → Expr Γ (a ⇒ b)
  _·_   : ∀ {a b} → Expr Γ (a ⇒ b) → Expr Γ a → Expr Γ b
  num   : ℤ → Expr Γ int
  iop   : (ℤ → ℤ → ℤ) → (l r : Expr Γ int) → Expr Γ int
  ifz   : ∀ {t} → Expr Γ int → Expr Γ t → Expr Γ t → Expr Γ t
  ref   : ∀ {t} → Expr Γ t → Expr Γ (ref t)
  !_    : ∀ {t} → Expr Γ (ref t) → Expr Γ t
  _≔_   : ∀ {t} → Expr Γ (ref t) → Expr Γ t → Expr Γ unit

-----------------------
-- STORES AND VALUES --
-----------------------

StoreTy = List Ty

mutual
  data Val : Ty → (Σ : StoreTy) → Set where
    loc    : ∀ {Σ t} → t ∈ Σ → Val (ref t) Σ
    unit   : ∀ {Σ} → Val unit Σ
    ⟨_,_⟩  : ∀ {Σ Γ a b} → Expr (a ∷ Γ) b → Env Γ Σ → Val (a ⇒ b) Σ
    num   : ∀ {Σ} → ℤ → Val int Σ

  Env : (Γ : Ctx)(Σ : StoreTy) → Set
  Env Γ Σ = All (λ t → Val t Σ) Γ

Store : (Σ : StoreTy) → Set
Store Σ = All (λ t → Val t Σ) Σ

-- The `lookup-store` function is defined in terms of the `lookup`
-- function from `Data.List.All` in the Agda Standard Library.
lookup-store : ∀ {Σ t} → t ∈ Σ → Store Σ → Val t Σ
lookup-store x μ = All.lookup μ x

-- The `update-store` function is defined in terms of the update
-- function for the `All` type: `_All[_]≔'_` from the Standard Library
-- extension (contained in the `lib/*` folder of this artifact).
update-store : ∀ {Σ t} → t ∈ Σ → Val t Σ → Store Σ → Store Σ
update-store ptr v μ = μ All.[ ptr ]≔ v

-----------
-- MONAD --
-----------

-- These definitions correspond to Section 3.3.

M : ∀ {i}(Γ : Ctx) → (p : StoreTy → Set i) → (Σ : StoreTy) → Set i
M Γ p Σ = Env Γ Σ → Store Σ → Maybe (∃ λ Σ' → Store Σ' × p Σ' × Σ ⊑ Σ')

mutual
  weaken-val  : ∀ {a}{Σ Σ' : StoreTy} → Σ ⊑ Σ' → Val a Σ → Val a Σ'
  weaken-val ext unit      = unit
  weaken-val ext (loc l)   = loc (∈-⊒ l ext)
  weaken-val ext ⟨ e , E ⟩ = ⟨ e , weaken-env ext E ⟩
  weaken-val ext (num z)   = num z

  weaken-env  : ∀ {Γ}{Σ Σ' : StoreTy} → Σ ⊑ Σ' → Env Γ Σ → Env Γ Σ'
  weaken-env ext (v ∷ vs)  = weaken-val ext v ∷ weaken-env ext vs
  weaken-env ext []        = []

-- The definition below asserts that values can be weakened, by adding
-- an instance argument of `Weakenable (Val t)`.
--
-- Here, `Weakenable` is defined as in the paper Section 3.4; see
-- `Common.Weakening` in this artifact.

instance
  weaken-val' : ∀ {t} → Weakenable (Val t)
  weaken-val' = record { wk = weaken-val }

return   :    ∀ {Σ Γ}{p : List Ty → Set} → p Σ → M Γ p Σ
return x E μ = just (_ , μ , x , ⊑-refl)

_>>=_ : ∀ {Σ Γ}{p q : StoreTy → Set} →
        (f : M Γ p Σ) → (g : ∀ {Σ'} → p Σ' → M Γ q Σ') → M Γ q Σ
(f >>= c) E μ = case (f E μ) of λ{
  nothing → nothing ;
  (just (_ , μ' , x , ext)) → case (c x (weaken-env ext E) μ') of λ{
    nothing → nothing ;
    (just (_ , μ'' , y , ext')) → just (_ , μ'' , y , ext ⊚ ext')
  }}

getEnv   :    ∀ {Σ Γ} → M Γ (Env Γ) Σ
getEnv E = return E E

usingEnv   :    ∀ {Σ Γ Γ'}{p : List Ty → Set} → Env Γ Σ → M Γ p Σ → M Γ' p Σ
usingEnv E f  _ = f E

timeout  :    ∀ {Σ Γ}{p : List Ty → Set} → M Γ p Σ
timeout _ _ = nothing

store    :    ∀ {Σ t Γ} → Val t Σ → M Γ (Val (ref t)) Σ
store {Σ} {t} v _ μ
  = let ext = ∷ʳ-⊒ t Σ
        v'  = loc (∈-∷ʳ Σ t)
        μ'  = (All.map (weaken-val ext) μ) all-∷ʳ (weaken-val ext v)
    in just (_ , μ' , v' , ext)

deref    :    ∀ {Σ Γ t} → t ∈ Σ → M Γ (Val t) Σ
deref x E μ = return (All.lookup μ x) E μ

update   :    ∀ {Σ Γ t} → t ∈ Σ → Val t Σ → M Γ (λ _ → ⊤) Σ
update x v E μ = return tt E (update-store x v μ)

weaken : ∀ {i}{p : List Ty → Set i}⦃ w : Weakenable p ⦄ → ∀ {Σ Σ'} → Σ ⊑ Σ' → p Σ → p Σ'
weaken ⦃ w ⦄ ext v = Weakenable.wk w ext v

--------------------------------
-- STRONG MONADIC INTERPRETER --
--------------------------------

-- These definitions correspond to Section 3.4.
--
-- The definition of `_^_` below is defined in terms of the `_⊗_`
-- type, which is defined in `Common.Weakening` in this artifact.

_^_  : ∀ {Σ Γ}{p q : StoreTy → Set} → ⦃ w : Weakenable q ⦄ → M Γ p Σ → q Σ → M Γ (p ⊗ q) Σ
(f ^ x) E μ = case (f E μ) of λ {
  nothing → nothing ;
  (just (Σ , μ' , y , ext)) → just (Σ , μ' , (y , weaken ext x) , ext) }

eval : ℕ → ∀ {Σ Γ t} → Expr Γ t → M Γ (Val t) Σ
eval zero     _           =
  timeout
eval (suc k)  unit        =
  return unit
eval (suc k)  (var x)     =
  getEnv >>= λ E →
  return (All.lookup E x)
eval (suc k)  (ƛ e)       =
  getEnv >>= λ E →
  return ⟨ e , E ⟩
eval (suc k)  (l · r)     =
  eval k l >>= λ{ ⟨ e , E ⟩ →
  (eval k r ^ E) >>= λ{ (v , E) →
  usingEnv (v ∷ E) (eval k e) }}
eval (suc k)  (num x)     =
  return (num x)
eval (suc k)  (iop f l r) =
  eval k l >>= λ{ (num vₗ) →
  eval k r >>= λ{ (num vᵣ) →
  return (num (f vₗ vᵣ)) }}
eval (suc k) (ifz c t e) =
  eval k c >>= λ{ (num z) →
  case z of λ{ (+ zero) →
    eval k t
  ; _ →
    eval k e }}
eval (suc k)  (ref e)     =
  eval k e >>= λ v →
  store v
eval (suc k)  (! e)       =
  eval k e >>= λ{ (loc l) →
  deref l }
eval (suc k)  (r ≔ e)     =
  eval k r >>= λ{ (loc l) →
  (eval k e ^ l) >>= λ{ (v , l) →
  update l v >>= λ _ →
  return unit }}


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

open import Setoids.Setoids
open import Functions.Definition
open import Groups.Definition
open import Sets.EquivalenceRelations
open import Groups.Homomorphisms.Definition

module Groups.Homomorphisms.Examples where

identityHom : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+A_ : A → A → A} (G : Group S _+A_) → GroupHom G G id
GroupHom.groupHom (identityHom {S = S} G) = Equivalence.reflexive (Setoid.eq S)
GroupHom.wellDefined (identityHom G) = id


text:
module RMonads.Restriction where

open import Library
open import Categories
open import Functors
open import Naturals
open import Monads
open import RMonads

open Cat
open Fun

restrictM : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}(J : Fun C D) →
            Monad D → RMonad J
restrictM J M = record {
  T    = T ∘ OMap J;
  η    = η;
  bind = bind;
  law1 = law1;
  law2 = law2;
  law3 = law3}
  where open Monad M

open import Monads.MonadMorphs
open import RMonads.RMonadMorphs

restrictMM : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{M M' : Monad D}
             (J : Fun C D) → MonadMorph M M' →
             RMonadMorph (restrictM J M) (restrictM J M')
restrictMM J MM = record {
  morph   = λ{X} → morph {OMap J X};
  lawη    = lawη;
  lawbind = lawbind}
  where open MonadMorph MM
open import Adjunctions
open import RAdjunctions

restrictA : ∀{a b c d e f}{C : Cat {a}{b}}{D : Cat {c}{d}}{E : Cat {e}{f}}
            (J : Fun C D) → Adj D E → RAdj J E
restrictA J A = record{
  L        = L ○ J;
  R        = R;
  left     = left;
  right    = right;
  lawa     = lawa;
  lawb     = lawb;
  natleft  = natleft ∘ HMap J;
  natright = natright ∘ HMap J}
  where open Adj A


text:
------------------------------------------------------------------------
-- Pure type systems (PTS)
------------------------------------------------------------------------

-- This file contains some core definitions which are reexported by
-- Pts.Typing

module Pts.Core where

open import Data.Fin.Substitution.Typed
open import Data.Product using (∃)

import Pts.Syntax

-- Instances of pure type systems.
record PTS : Set₁ where

  -- The following predicates represent the set of sorts, axioms and
  -- rules, respectively.
  field
    Sort  : Set                        -- sorts
    Axiom : Sort → Sort → Set          -- axioms
    Rule  : Sort → Sort → Sort → Set   -- rules

  -- Convenience aliases of modules in Pts.Syntax.
  module Syntax       = Pts.Syntax.Syntax       Sort
  module Substitution = Pts.Syntax.Substitution Sort
  module Ctx          = Pts.Syntax.Ctx          Sort

  open Syntax
  open Ctx

  -- Abstract well-formed typing contexts.
  module WfCtx (_⊢_∈_ : Typing Term Term Term) where

    -- Well-formedness of terms/types.
    _⊢_wf : Wf Term
    Γ ⊢ a wf = ∃ λ s → Γ ⊢ a ∈ sort s

    -- FIXME: the following definition should not be necessary.
    --
    -- Instead, it should be sufficient to directly open the module
    -- WellFormedContext like so:
    --
    --   open WellFormedContext _⊢_wf public
    --
    -- but there is currently a bug that prevents us from doing so.
    -- See https://github.com/agda/agda/issues/2901

    _wf : ∀ {n} → Ctx n → Set
    _wf = WellFormedContext._wf  _⊢_wf

    open WellFormedContext _⊢_wf public hiding (_wf)

max_stars_repo_name: asr/pts-agda

max_issues_repo_name: asr/pts-agda

max_forks_repo_name: asr/pts-agda


text:
-- Andreas, 2016-02-09, issue reported by Anton Setzer
-- {-# OPTIONS -v tc.conv.infer:30 -v tc.deftype:30 #-}

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

data ⊥ : Set where

data MaybeSet : Set₁ where
  nothing : MaybeSet
  just : Set → MaybeSet

-- not injective
FromJust : MaybeSet → Set
FromJust nothing = ⊥
FromJust (just A) = A

R0 : ⊥ → Set
R0 ()

data C1 (A :  Set) : Set where
  c1 : ⊥ → C1 A

-- R1 is projection-like
R1 : (A : Set) → C1 A → Set
R1 A (c1 c) = R0 c
-- R1 A (c1 ()) -- no int. err.

record Iface  : Set₁ where
  field
    Command   : Set
    Response  : Command → Set

I1 : (A : Set) → Iface
Iface.Command   (I1 A) = C1 A
Iface.Response  (I1 A) = R1 A
-- Iface.Response  (I1 A) (c1 c) = R0 c -- no int.err.
-- I1 A = record { Command = C1 A; Response = R1 A } -- no. int. err

postulate
  IO : Iface → Set

data C2 (s : MaybeSet) : Set₁ where
  c2  : (FromJust s → IO (I1 (FromJust s))) → C2 s

data IOˢ : MaybeSet → Set₁ where
  do : {s : MaybeSet} (c : C2 s) → IOˢ s

postulate
  bla : Set → ⊥ → IO (I1  ⊥)

test : IOˢ nothing
test = do (c2 (bla {!!}))


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Cocones where

open import Level

open import Categories.Category
open import Categories.Functor hiding (_∘_; _≡_; equiv; id; assoc; identityˡ; identityʳ; ∘-resp-≡)
open import Categories.Cocone

record CoconeMorphism {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} {F : Functor J C} (c₁ c₂ : Cocone F) : Set (ℓ ⊔ e ⊔ o′ ⊔ ℓ′) where
  module c₁ = Cocone c₁
  module c₂ = Cocone c₂
  module C = Category C
  module J = Category J
  open C
  field
    f : C [ c₁.N , c₂.N ]
    .commute : ∀ {X} → f ∘ c₁.ψ X ≡ c₂.ψ X

Cocones : ∀ {o ℓ e} {o′ ℓ′ e′} {C : Category o ℓ e} {J : Category o′ ℓ′ e′} (F : Functor J C) → Category (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′) (ℓ ⊔ e ⊔ o′ ⊔ ℓ′) e
Cocones {C = C} F = record
  { Obj = Obj′
  ; _⇒_ = Hom′
  ; _≡_ = _≡′_
  ; _∘_ = _∘′_
  ; id = record { f = id; commute = identityˡ }
  ; assoc = assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; equiv = record
    { refl = Equiv.refl
    ; sym = Equiv.sym
    ; trans = Equiv.trans
    }
  ; ∘-resp-≡ = ∘-resp-≡
  }
  where
  open Category C
  open Cocone
  open CoconeMorphism
  open Functor F

  infixr 9 _∘′_
  infix  4 _≡′_

  Obj′ = Cocone F

  Hom′ : Obj′ → Obj′ → Set _
  Hom′ = CoconeMorphism

  _≡′_ : ∀ {A B} → Hom′ A B → Hom′ A B → Set _
  F ≡′ G = f F ≡ f G

  _∘′_ : ∀ {A B C} → Hom′ B C → Hom′ A B → Hom′ A C
  _∘′_ {A} {B} {C} F G = record
    { f = f F ∘ f G
    ; commute = commute′
    }
    where
    .commute′ : ∀ {X} → (f F ∘ f G) ∘ ψ A X ≡ ψ C X
    commute′ {X} =
        begin
          (f F ∘ f G) ∘ ψ A X
        ↓⟨ assoc ⟩
          f F ∘ (f G ∘ ψ A X)
        ↓⟨ ∘-resp-≡ʳ (CoconeMorphism.commute G) ⟩
          f F ∘ ψ B X
        ↓⟨ CoconeMorphism.commute F ⟩
          ψ C X
        ∎
      where
      open HomReasoning

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

record R : Set₁ where
  field
    fun  : (A : Set) → A → Bool → A ≡ Bool → Bool
    rule : ∀ x → fun Bool false x refl ≡ false
open R

test : R
fun test .Bool true true refl = true
fun test _     _    _    _    = false
rule test x = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Data.Vec.Any.Membership.Properties where

open import Relation.Binary
open import Data.Vec

module SingleSetoid {a ℓ} (S : Setoid a ℓ) where
    open Setoid S renaming (Carrier to A)
    open import Data.Vec.Any
    open import Data.Vec.Any.Membership S
    open import Function using (flip)
    open import Data.Vec.Equality using (module Equality)
    open Equality S renaming (_≈_ to _≋_; trans to ≋-trans)
    ⊆-reflexive : ∀ {n m} {xs : Vec A n} {ys : Vec A m} →
      xs ≋ ys → xs ⊆ ys
    ⊆-reflexive []-cong ()
    ⊆-reflexive (x₁≈x₂ ∷-cong eq) (here x≈x₁) = here (trans x≈x₁ x₁≈x₂)
    ⊆-reflexive (_ ∷-cong eq) (there p) = there (⊆-reflexive eq p)

    ∈′-resp-≈ : ∀ {x} → (x ≈_) Respects _≈_
    ∈′-resp-≈ = flip trans

    ∈′-resp-≋ : ∀ {n₁ n₂ x}{xs₁ : Vec A n₁}{xs₂ : Vec A n₂} →
      xs₁ ≋ xs₂ → x ∈′ xs₁ → x ∈′ xs₂
    ∈′-resp-≋ {xs₁ = .[]} {.[]} []-cong ()
    ∈′-resp-≋ {xs₁ = .(_ ∷ _)} {.(_ ∷ _)} (x¹≈x² ∷-cong eq) (here x≈x₁) = here (trans x≈x₁ x¹≈x²)
    ∈′-resp-≋ {xs₁ = .(_ ∷ _)} {.(_ ∷ _)} (x¹≈x² ∷-cong eq) (there p) =
       there (∈′-resp-≋ eq p)

open SingleSetoid public

module DoubleSetoid {a₁ a₂ ℓ₁ ℓ₂}
  (S₁ : Setoid a₁ ℓ₁) (S₂ : Setoid a₂ ℓ₂) where
      open import Data.Vec.Any.Properties
      import Data.Vec.Any as Any
      open import Data.Product hiding (map)
      open Setoid S₁ renaming (Carrier to A₁; _≈_ to _≈₁_; refl to refl₁)
      open Setoid S₂ renaming (Carrier to A₂; _≈_ to _≈₂_)

      open import Data.Vec.Any.Membership S₁ renaming (_∈′_ to _∈′₁_) using (find′)
      open import Data.Vec.Any.Membership S₂ renaming (_∈′_ to _∈′₂_) using ()

      ∈′-map⁺  : ∀ {n x}{xs : Vec A₁ n} {f} →
        f Preserves _≈₁_ ⟶ _≈₂_ →
          x ∈′₁ xs → f x ∈′₂ map f xs
      ∈′-map⁺ pres x∈′xs = map⁺ (Any.map pres x∈′xs)

      ∈′-map⁻  : ∀ {n y}{xs : Vec A₁ n} {f} → y ∈′₂ map f xs →
        ∃ λ x → x ∈′₁ xs × y ≈₂ f x
      ∈′-map⁻ y∈′map with find′ (map⁻ y∈′map)
      ... | _ , x∈xs , px = , x∈xs , px
open DoubleSetoid public

max_stars_repo_name: tizmd/agda-vector-any

max_issues_repo_name: tizmd/agda-vector-any

max_forks_repo_name: tizmd/agda-vector-any


text:
open import MLib.Algebra.PropertyCode
open import MLib.Algebra.PropertyCode.Structures

module MLib.Matrix.Pow {c ℓ} (struct : Struct bimonoidCode c ℓ) where

open import MLib.Prelude
open import MLib.Matrix.Core
open import MLib.Matrix.Equality struct
open import MLib.Matrix.Mul struct
open import MLib.Matrix.Plus struct
open import MLib.Matrix.Bimonoid struct

open FunctionProperties

module _ {n} where
  open import MLib.Algebra.Operations (matrixStruct n)

  pow : Matrix S n n → ℕ → Matrix S n n
  pow M zero = 1●
  pow M (suc p) = M ⊗ pow M p

  pstar : Matrix S n n → ℕ → Matrix S n n
  pstar M zero = 0●
  pstar M (suc p) = 1● ⊕ M ⊗ pstar M p

  pstar′ : Matrix S n n → ℕ → Matrix S n n
  pstar′ M p = ∑[ q < p ] pow M (Fin.toℕ q)

  pstar′-unfold : ∀ {M : Matrix S n n} {p} → pstar′ M (suc p) ≈ 1● ⊕ M ⊗ pstar′ M p
  pstar′-unfold {M} {p} =
    begin
      pstar′ M (suc p)                                                  ≡⟨⟩
      pow M (Fin.toℕ (zero {p})) ⊕ ∑[ q < p ] pow M (Fin.toℕ (suc q))  ≡⟨⟩
      1● ⊕ ∑[ q < p ] pow M (suc (Fin.toℕ q))                          ≡⟨⟩
      1● ⊕ ∑[ q < p ] (M ⊗ pow M (Fin.toℕ q))                          ≈⟨ ⊕-cong refl (sym (sumDistribˡ ⦃ {!!} ⦄ {p} M _)) ⟩
      1● ⊕ M ⊗ ∑[ q < p ] pow M (Fin.toℕ q)                            ≡⟨⟩
      1● ⊕ M ⊗ pstar′ M p                                               ∎
    where open EqReasoning setoid

  -- pstar-pstar′ : ∀ {M : Matrix S n n} {p} → pstar M p ≈ pstar′ M p
  -- pstar-pstar′ {p = zero} _ _ = S.refl
  -- pstar-pstar′ {M = M} {suc p} =
  --   begin
  --     ((1● ⊕ M) ⊗ pstar M p)  ≈⟨ {!!} ⟩
  --     pow M (Fin.toℕ (zero {p})) ⊕ (Table.foldr {n = p} _⊕_ 0● (tabulate (pow M ∘ Fin.toℕ ∘ suc))) ≡⟨⟩
  --     pstar′ M (suc p)        ∎
  --   where open EqReasoning setoid


text:
------------------------------------------------------------------------------
-- Common stuff used by the gcd example
------------------------------------------------------------------------------

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

module FOTC.Program.GCD.Total.Definitions where

open import FOTC.Base
open import FOTC.Data.Nat.Divisibility.By0
open import FOTC.Data.Nat.Inequalities
open import FOTC.Data.Nat.Type

------------------------------------------------------------------------------
-- Common divisor.
CD : D → D → D → Set
CD m n cd = cd ∣ m ∧ cd ∣ n
{-# ATP definition CD #-}

-- Divisible for any common divisor.
Divisible : D → D → D → Set
Divisible m n gcd = ∀ cd → N cd → CD m n cd → cd ∣ gcd
{-# ATP definition Divisible #-}

-- Greatest common divisor specification.

-- The gcd is a common divisor and the gcd is divided by any common
-- divisor, thefore the gcd is the greatest common divisor
-- according to the partial order _∣_.
gcdSpec : D → D → D → Set
gcdSpec m n gcd = CD m n gcd ∧ Divisible m n gcd
{-# ATP definition gcdSpec #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc