text:
module ProcessSyntax where

open import Data.List

open import Typing
open import Syntax

-- processes
data Proc (Φ : TCtx) : Set where
  exp : (e : Expr Φ TUnit)
    → Proc Φ

  par : ∀ {Φ₁ Φ₂}
    → (sp : Split Φ Φ₁ Φ₂)
    → (P₁ : Proc Φ₁)
    → (P₂ : Proc Φ₂)
    → Proc Φ

  res : (s : SType)
    → (P : Proc (TChan (SType.force s) ∷ TChan (SType.force (dual s)) ∷ Φ))
    → Proc Φ

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text:
------------------------------------------------------------------------------
-- Distributive laws on a binary operation: Task B
------------------------------------------------------------------------------

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

module DistributiveLaws.TaskB-TopDownATP where

open import DistributiveLaws.Base

open import Common.FOL.Relation.Binary.EqReasoning

------------------------------------------------------------------------------
-- We found the longest chains of equalities from
-- DistributiveLaws.TaskB-I which are prove by the ATPs, following a
-- top-down approach.

prop₂ : ∀ u x y z → (x · y · (z · u)) ·
                    (( x · y · ( z · u)) · (x · z · (y · u))) ≡
                    x · z · (y · u)
prop₂ u x y z =

-- The numbering of the proof step justifications are associated with
-- the numbers used in DistributiveLaws.TaskB-I.

   xy·zu · (xy·zu · xz·yu)                                         ≡⟨ j₁₋₅ ⟩
   xy·zu · (xz · xu·yu · (y·zu · xz·yu))                           ≡⟨ j₅₋₉ ⟩
   xy·zu · (xz · xyu · (yxz · yu))                                 ≡⟨ j₉₋₁₄ ⟩
   xz · xyu · (yz · xyu) · (xz · xyu · (y·xu · z·yu))              ≡⟨ j₁₄₋₂₀ ⟩
   xz · xyu · (y·xu · (y·yu · z·yu) · (z · xu·yu · (y·xu · z·yu))) ≡⟨ j₂₀₋₂₃ ⟩
   xz · xyu · (y · xu·zu · (z · xu·yu · (y·xu · z·yu)))            ≡⟨ j₂₃₋₂₅ ⟩
   (xz · xyu) · (y · xu·zu · (z·xu · y·xu · z·yu))                 ≡⟨ j₂₅₋₃₀ ⟩
   xz · xyu · (y·zy · xzu)                                         ≡⟨ j₃₀₋₃₅ ⟩
   xz·yu                                                           ∎
  where
  -- Two variables abbreviations

  xz = x · z
  yu = y · u
  yz = y · z
  {-# ATP definitions xz yu yz #-}

  -- Three variables abbreviations

  xyu = x · y · u
  xyz = x · y · z
  xzu = x · z · u
  yxz = y · x · z
  {-# ATP definitions xyu xyz xzu yxz #-}

  y·xu = y · (x · u)
  y·yu = y · (y · u)
  y·zu = y · (z · u)
  y·zy = y · (z · y)
  {-# ATP definitions y·xu y·yu y·zu y·zy #-}

  z·xu = z · (x · u)
  z·yu = z · (y · u)
  {-# ATP definitions z·xu z·yu #-}

  -- Four variables abbreviations

  xu·yu = x · u · (y · u)
  xu·zu = x · u · (z · u)
  {-# ATP definitions xu·yu xu·zu #-}

  xy·zu = x · y · (z · u)
  {-# ATP definition xy·zu #-}

  xz·yu = x · z · (y · u)
  {-# ATP definition xz·yu #-}

  -- Steps justifications

  postulate j₁₋₅ : xy·zu · (xy·zu · xz·yu) ≡
                   xy·zu · (xz · xu·yu · (y·zu · xz·yu))
  {-# ATP prove j₁₋₅ #-}

  postulate j₅₋₉ : xy·zu · (xz · xu·yu · (y·zu · xz·yu)) ≡
                   xy·zu · (xz · xyu · (yxz · yu))
  {-# ATP prove j₅₋₉ #-}

  postulate j₉₋₁₄ : xy·zu · (xz · xyu · (yxz · yu)) ≡
                    xz · xyu · (yz · xyu) · (xz · xyu · (y·xu · z·yu))
  {-# ATP prove j₉₋₁₄ #-}

  postulate
    j₁₄₋₂₀ : xz · xyu · (yz · xyu) · (xz · xyu · (y·xu · z·yu)) ≡
             xz · xyu · (y·xu · (y·yu · z·yu) · (z · xu·yu · (y·xu · z·yu)))
  {-# ATP prove j₁₄₋₂₀ #-}

  postulate
    j₂₀₋₂₃ : xz · xyu · (y·xu · (y·yu · z·yu) · (z · xu·yu · (y·xu · z·yu))) ≡
             xz · xyu · (y · xu·zu · (z · xu·yu · (y·xu · z·yu)))
  {-# ATP prove j₂₀₋₂₃ #-}

  postulate j₂₃₋₂₅ : xz · xyu · (y · xu·zu · (z · xu·yu · (y·xu · z·yu))) ≡
                     (xz · xyu) · (y · xu·zu · (z·xu · y·xu · z·yu))
  {-# ATP prove j₂₃₋₂₅ #-}

  postulate j₂₅₋₃₀ : (xz · xyu) · (y · xu·zu · (z·xu · y·xu · z·yu)) ≡
                     xz · xyu · (y·zy · xzu)
  {-# ATP prove j₂₅₋₃₀ #-}

  postulate j₃₀₋₃₅ : xz · xyu · (y·zy · xzu) ≡ xz·yu
  {-# ATP prove j₃₀₋₃₅ #-}

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Sandbox.IndRec where
-- Ornamental Algebras, Algebraic Ornaments, CONOR McBRIDE
-- https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/Ornament.pdf
-- A Finite Axiomtization of Inductive-Recursion definitions, Peter Dybjer, Anton Setzer
-- http://www.cse.chalmers.se/~peterd/papers/Finite_IR.pdf

open import Data.Product using (_×_; Σ; _,_)
open import Data.Bool
open import Data.Unit
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

data Desc : Set₁ where
    arg : (A : Set)             -- a bag of tags to choose constructors with
        → (A → Desc)            -- given a tag, return the description of the constructor it corresponds to
        → Desc
    rec : Desc → Desc           -- recursive subnode
    ret : Desc                  -- stop

-- the "decoder", "interpreter"
⟦_⟧ : Desc → Set → Set
⟦ arg A D ⟧ R = Σ A (λ a → ⟦ D a ⟧ R)
⟦ rec D   ⟧ R = R × ⟦ D ⟧ R
⟦ ret     ⟧ R = ⊤

-- "μ" in some other literature
data Data (D : Desc) : Set where
    ⟨_⟩ : ⟦ D ⟧ (Data D) → Data D   -- or "in"

out : ∀ {D} → Data D → ⟦ D ⟧ (Data D)
out ⟨ x ⟩ = x

map : ∀ {A B} → (d : Desc) → (A → B) → ⟦ d ⟧ A → ⟦ d ⟧ B
map (arg A  d) f (a , y) = a , (map (d a) f y)
map (rec desc) f (a , x) = (f a) , (map desc f x)
map (ret) f tt = tt

-- fold : ∀ {A} → (F : Desc) → (⟦ F ⟧ A → A) → Data F → A
-- fold F alg ⟨ x ⟩ = alg (map F (fold F alg) x)

-- mapFold F alg x = map F (fold F alg) x
-- fold F alg x = alg (mapFold F alg (out x))
-- mapFold F alg x = map F (λ y → alg (mapFold F alg (out y))) x

mapFold : ∀ {A} (F G : Desc) → (⟦ G ⟧ A → A) → ⟦ F ⟧ (Data G) → ⟦ F ⟧ A
mapFold (arg T decoder) G alg (t , cnstrctr) = t , (mapFold (decoder t) G alg cnstrctr)
mapFold (rec F) G alg (⟨ x ⟩ , xs) = alg (mapFold G G alg x) , mapFold F G alg xs
mapFold ret G alg x = tt

fold : ∀ {A} → (F : Desc) → (⟦ F ⟧ A → A) → Data F → A
fold F alg ⟨ x ⟩ = alg (mapFold F F alg x)

-- ℕ
ℕDesc : Desc
ℕDesc = arg Bool λ { false → ret
                    ; true → rec ret }

ℕ : Set
ℕ = Data ℕDesc

zero : ℕ
zero = ⟨ (false , tt) ⟩

suc : ℕ → ℕ
suc n = ⟨ (true , (n , tt)) ⟩

-- induction principle on ℕ
indℕ : (P : ℕ → Set)
     → (P zero)
     → ((n : ℕ) → (P n) → (P (suc n)))
     → (x : ℕ)
     → P x
indℕ P base step ⟨ true , n-1 , _ ⟩ = step n-1 (indℕ P base step n-1)
indℕ P base step ⟨ false , _ ⟩ = base

_+_ : ℕ → ℕ → ℕ
x + y = indℕ (λ _ → ℕ) y (λ n x → suc x) x

-- Maybe
MaybeDesc : Set → Desc
MaybeDesc A = arg Bool (λ { false → ret ; true → arg A (λ x → ret) })

Maybe : Set → Set
Maybe A = Data (MaybeDesc A)

nothing : ∀ {A} → Maybe A
nothing = ⟨ (false , tt) ⟩

just : ∀ {A} → A → Maybe A
just a = ⟨ (true , (a , tt)) ⟩

mapMaybe : ∀ {A B} → (A → B) → Maybe A → Maybe B
mapMaybe f ⟨ true , a , tt ⟩ = ⟨ (true , ((f a) , tt)) ⟩
mapMaybe f ⟨ false , tt ⟩ = ⟨ false , tt ⟩

-- List
ListDesc : Set → Desc
ListDesc A = arg Bool (λ { false → ret ; true → arg A (λ _ → rec ret )})

List : Set → Set
List A = Data (ListDesc A)

nil : ∀ {A} → List A
nil = ⟨ (false , tt) ⟩

cons : ∀ {A} → A → List A → List A
cons x xs = ⟨ (true , (x , (xs , tt))) ⟩

foldList : ∀ {A B} (f : A → B → B) → B → List A → B
foldList {A} {B} f e xs = fold (ListDesc A) alg xs
    where   alg : ⟦ ListDesc A ⟧ B → B
            alg (true , n , acc , tt) = f n acc
            alg (false , tt) = e

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


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

module Categories.Category.Finite where

open import Level
open import Data.Nat using (ℕ)
open import Data.Fin

open import Categories.Adjoint.Equivalence
open import Categories.Category
open import Categories.Functor
open import Categories.Category.Finite.Fin

-- definition of a finite category
--
-- the idea is to require a functor from C to a category generated from a finite shape
-- is the right adjoint.
--
-- Question: it seems to me right adjoint is enough, though the original plan is to
-- use adjoint equivalence. intuitively, the shape category is an "overapproximation"
-- of C, which is a very strong constraint. so requiring adjoint equivalence sounds an
-- unnecessarily stronger constraint. is adjoint equivalence necessary?
--
-- Answer: probably yes. adjoint equivalence seems necessary as the notion needs to
-- show that shapes are preserved.
--
-- c.f. Categories.Adjoint.Equivalence.Properties.⊣equiv-preserves-diagram
record Finite {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  field
    shape : FinCatShape

  open FinCatShape public renaming (size to ∣Obj∣)

  shapeCat : Category _ _ _
  shapeCat = FinCategory shape

  --
  --   /------------\
  --  <      -       \
  -- C       |        S
  --  \      -       ^
  --   \------------/
  --
  field
    ⊣equiv : ⊣Equivalence shapeCat C

  module ⊣equiv = ⊣Equivalence ⊣equiv
  open ⊣equiv public

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
module Generic.Lib.Data.Maybe where

open import Data.Maybe.Base using (Maybe; just; nothing; maybe; maybe′; from-just; fromMaybe) public

open import Generic.Lib.Intro
open import Generic.Lib.Category

infixr 0 _?>_

instance
  MaybeMonad : ∀ {α} -> RawMonad {α} Maybe
  MaybeMonad = record
    { return = just
    ; _>>=_  = Data.Maybe.Base._>>=_
    }

  MaybeApplicative : ∀ {α} -> RawApplicative {α} Maybe
  MaybeApplicative = rawIApplicative

  MaybeFunctor : ∀ {α} -> RawFunctor {α} Maybe
  MaybeFunctor = rawFunctor

_?>_ : ∀ {α} {A : Set α} -> Bool -> A -> Maybe A
true  ?> x = just x
false ?> x = nothing

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
open import Type

module Relator.Sets {ℓ ℓₑ ℓₛ} {E : Type{ℓₑ}} {S : Type{ℓₛ}} (_∈_ : E → S → Type{ℓ}) where

open import Functional
open import Logic.Propositional
open import Logic.Predicate

_∉_ : E → S → Type
_∉_ = (¬_) ∘₂ (_∈_)

_∋_ : S → E → Type
_∋_ = swap(_∈_)

_∌_ : S → E → Type
_∌_ = (¬_) ∘₂ (_∋_)

_⊆_ : S → S → Type
_⊆_ L₁ L₂ = ∀ₗ(x ↦ ((_→ᶠ_) on₂ (x ∈_)) L₁ L₂)

_⊇_ : S → S → Type
_⊇_ L₁ L₂ = ∀ₗ(x ↦ ((_←_) on₂ (x ∈_)) L₁ L₂)

_≡_ : S → S → Type
_≡_ L₁ L₂ = ∀ₗ(x ↦ ((_↔_) on₂ (x ∈_)) L₁ L₂)

_⊈_ : S → S → Type
_⊈_ = (¬_) ∘₂ (_⊆_)

_⊉_ : S → S → Type
_⊉_ = (¬_) ∘₂ (_⊇_)

_≢_ : S → S → Type
_≢_ = (¬_) ∘₂ (_≡_)

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:
module Issue804 where

mutual

  {-# NO_TERMINATION_CHECK #-}

  Foo : Set
  Foo = Foo

-- WAS: The pragma above doesn't apply to Foo. An informative error message
-- could be helpful.

-- NOW: The pragma does apply to Foo.

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- A type used to index a combined definition of strong and weak
-- bisimilarity and expansion
------------------------------------------------------------------------

{-# OPTIONS --safe #-}

module Delay-monad.Bisimilarity.Kind where

open import Equality.Propositional
open import Prelude

-- The three different relations are defined as a single relation,
-- indexed by the Kind type.

data Not-strong-kind : Type where
  weak expansion : Not-strong-kind

data Kind : Type where
  strong : Kind
  other  : Not-strong-kind → Kind

-- Kind equality is decidable.

infix 4 _≟-Kind_ _≟-Not-strong-kind_

_≟-Not-strong-kind_ : Decidable-equality Not-strong-kind
weak      ≟-Not-strong-kind weak      = yes refl
weak      ≟-Not-strong-kind expansion = no λ ()
expansion ≟-Not-strong-kind weak      = no λ ()
expansion ≟-Not-strong-kind expansion = yes refl

_≟-Kind_ : Decidable-equality Kind
_≟-Kind_ strong     strong     = yes refl
_≟-Kind_ strong     (other _)  = no λ()
_≟-Kind_ (other _)  strong     = no λ()
_≟-Kind_ (other k₁) (other k₂) =
  ⊎-map (cong other)
        (λ { hyp refl → hyp refl })
        (k₁ ≟-Not-strong-kind k₂)

max_stars_repo_name: nad/delay-monad

max_issues_repo_name: nad/delay-monad

max_forks_repo_name: nad/delay-monad


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.CommRing.BinomialThm where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

open import Cubical.Data.Nat renaming ( _+_ to _+ℕ_ ; _·_ to _·ℕ_ ; _^_ to _^ℕ_
                                      ; +-comm to +ℕ-comm
                                      ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm
                                      ; _choose_ to _ℕchoose_ ; snotz to ℕsnotz)
open import Cubical.Data.Nat.Order
open import Cubical.Data.FinData
open import Cubical.Data.Empty as ⊥

open import Cubical.Algebra.Monoid.BigOp
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.RingSolver.Reflection

private
  variable
    ℓ : Level

module BinomialThm (R' : CommRing ℓ) where
 open CommRingStr (snd R')
 open Exponentiation R'
 open CommRingTheory R'
 open Sum (CommRing→Ring R')
 private R = fst R'

 _choose_ : ℕ → ℕ → R
 n choose zero = 1r
 zero choose suc k = 0r
 suc n choose suc k = n choose (suc k) + n choose k

 n<k→nChooseK≡0 : ∀ n k → n < k → n choose k ≡ 0r
 n<k→nChooseK≡0 zero zero (m , p) = ⊥.rec (ℕsnotz (sym (+ℕ-comm m 1) ∙ p))
 n<k→nChooseK≡0 zero (suc k) (m , p) = refl
 n<k→nChooseK≡0 (suc n) zero (m , p) = ⊥.rec (ℕsnotz {n = m +ℕ (suc n)} (sym (+-suc _ _) ∙ p))
 n<k→nChooseK≡0 (suc n) (suc k) (m , p) = cong₂ (_+_) p1 p2 ∙ +Lid 0r
  where
  p1 : n choose suc k ≡ 0r
  p1 = n<k→nChooseK≡0 n (suc k) (suc m , sym (+-suc _ _) ∙ p)
  p2 : n choose k ≡ 0r
  p2 =  n<k→nChooseK≡0 n k (m , injSuc (sym (+-suc _ _) ∙ p))

 nChooseN+1 : ∀ n → n choose (suc n) ≡ 0r
 nChooseN+1 n = n<k→nChooseK≡0 n (suc n) (0 , refl)

 BinomialVec : (n : ℕ) → R → R → FinVec R (suc n)
 BinomialVec n x y i = (n choose (toℕ i)) · x ^ (toℕ i) · y ^ (n ∸ toℕ i)

 BinomialThm : ∀ (n : ℕ) (x y : R) → (x + y) ^ n ≡ ∑ (BinomialVec n x y)
 BinomialThm zero x y = solve R'
 BinomialThm (suc n) x y =
     (x + y) ^ suc n
  ≡⟨ refl ⟩
     (x + y) · (x + y) ^ n
  ≡⟨ cong ((x + y) ·_) (BinomialThm n x y) ⟩
     (x + y) · ∑ (BinomialVec n x y)
  ≡⟨ ·Ldist+ _ _ _ ⟩
     x · ∑ (BinomialVec n x y) + y · ∑ (BinomialVec n x y)
  ≡⟨ cong₂ (_+_) (∑Mulrdist _ (BinomialVec n x y)) (∑Mulrdist _ (BinomialVec n x y)) ⟩
     ∑ (λ i → x · BinomialVec n x y i)
   + ∑ (λ i → y · BinomialVec n x y i)
  ≡⟨ refl ⟩
     ∑ {n = suc n} (λ i → x · ((n choose (toℕ i)) · x ^ (toℕ i) · y ^ (n ∸ toℕ i)))
   + ∑ {n = suc n} (λ i → y · ((n choose (toℕ i)) · x ^ (toℕ i) · y ^ (n ∸ toℕ i)))
  ≡⟨ cong₂ (_+_) (∑Ext xVecPath) (∑Ext yVecPath) ⟩
     ∑ xVec + ∑ yVec
  ≡⟨ cong (_+ ∑ yVec) (∑Last xVec) ⟩
     ∑ (xVec ∘ weakenFin) + xⁿ⁺¹ + (yⁿ⁺¹ + ∑ (yVec ∘ suc))
  ≡⟨ solve3 _ _ _ _ ⟩
     yⁿ⁺¹  + (∑ (xVec ∘ weakenFin) + ∑ (yVec ∘ suc)) + xⁿ⁺¹
  ≡⟨ cong (λ s → yⁿ⁺¹  + s + xⁿ⁺¹) (sym (∑Split _ _))  ⟩
     yⁿ⁺¹  + (∑ middleVec) + xⁿ⁺¹
  ≡⟨ cong (λ s → yⁿ⁺¹  + s + xⁿ⁺¹) (∑Ext middlePath) ⟩
     yⁿ⁺¹ + ∑ ((BinomialVec (suc n) x y) ∘ weakenFin ∘ suc) + xⁿ⁺¹
  ≡⟨ refl ⟩
     ∑ ((BinomialVec (suc n) x y) ∘ weakenFin) + xⁿ⁺¹
  ≡⟨ cong (∑ ((BinomialVec (suc n) x y) ∘ weakenFin) +_) xⁿ⁺¹Path
   ∙ sym (∑Last (BinomialVec (suc n) x y)) ⟩
     ∑ (BinomialVec (suc n) x y) ∎
  where
  xVec : FinVec R (suc n)
  xVec i = (n choose (toℕ i)) · x ^ (suc (toℕ i)) · y ^ (n ∸ toℕ i)

  solve1 : ∀ x nci xⁱ yⁿ⁻ⁱ → x · (nci · xⁱ · yⁿ⁻ⁱ) ≡ nci · (x · xⁱ) · yⁿ⁻ⁱ
  solve1 = solve R'

  xVecPath : ∀ (i : Fin (suc n)) → x · ((n choose (toℕ i)) · x ^ (toℕ i) · y ^ (n ∸ toℕ i)) ≡ xVec i
  xVecPath i = solve1 _ _ _ _

  yVec : FinVec R (suc n)
  yVec i = (n choose (toℕ i)) · x ^ (toℕ i) · y ^ (suc (n ∸ toℕ i))

  solve2 : ∀ y nci xⁱ yⁿ⁻ⁱ → y · (nci · xⁱ · yⁿ⁻ⁱ) ≡ nci · xⁱ · (y · yⁿ⁻ⁱ)
  solve2 = solve R'

  yVecPath : ∀ (i : Fin (suc n)) → y · ((n choose (toℕ i)) · x ^ (toℕ i) · y ^ (n ∸ toℕ i)) ≡ yVec i
  yVecPath i = solve2 _ _ _ _

  xⁿ⁺¹ : R
  xⁿ⁺¹ = xVec (fromℕ n)
  yⁿ⁺¹ : R
  yⁿ⁺¹ = yVec zero

  xⁿ⁺¹Path : xⁿ⁺¹ ≡ BinomialVec (suc n) x y (fromℕ (suc n))
  xⁿ⁺¹Path = cong (λ m → m · (x · x ^ toℕ (fromℕ n)) · y ^ (n ∸ toℕ (fromℕ n)))
                  (sym (+Lid _) ∙ cong (_+ (n choose toℕ (fromℕ n)))
                  (sym (subst (λ m → (n choose suc m) ≡ 0r) (sym (toFromId n)) (nChooseN+1 n))))

  solve3 : ∀ sx sy xⁿ⁺¹ yⁿ⁺¹ → sx + xⁿ⁺¹ + (yⁿ⁺¹ + sy) ≡ yⁿ⁺¹ + (sx + sy) + xⁿ⁺¹
  solve3 = solve R'

  middleVec : FinVec R n
  middleVec i = xVec (weakenFin i) + yVec (suc i)

  middlePath : ∀ (i : Fin n) → middleVec i ≡ BinomialVec (suc n) x y (weakenFin (suc i))
  middlePath i = transport (λ j →
     (n choose toℕ (weakenFin i)) · (x · x ^ toℕ (weakenFin i)) · y ^ (n ∸ toℕ (weakenFin i))
   + (n choose suc (weakenRespToℕ i j)) · (x · x ^ (weakenRespToℕ i j)) · sym yHelper j
   ≡ ((n choose suc (toℕ (weakenFin i))) + (n choose toℕ (weakenFin i)))
   · (x · x ^ toℕ (weakenFin i)) · y ^ (n ∸ toℕ (weakenFin i)))
   (solve4 _ _ _ _)
   where
   yHelper : (y · y ^ (n ∸ suc (toℕ i))) ≡ y ^ (n ∸ toℕ (weakenFin i))
   yHelper = cong (λ m → y · y ^ (n ∸ suc m)) (sym (weakenRespToℕ i))
           ∙ cong (y ^_) (≤-∸-suc (subst (λ m → suc m ≤ n) (sym (weakenRespToℕ _)) (toℕ<n i)))

   solve4 : ∀ nci ncsi xxⁱ yⁿ⁻ⁱ → nci · xxⁱ · yⁿ⁻ⁱ + ncsi · xxⁱ · yⁿ⁻ⁱ ≡ (ncsi + nci) · xxⁱ · yⁿ⁻ⁱ
   solve4 = solve R'

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
postulate
  Bool : Set
  D    : Bool → Set
  f    : (a : Bool) → D a
  ⟦_⟧  : ∀ {a} → D a → Bool

record State : Set where
  field bool : Bool

open State {{...}}

postulate
  guard : {S : Set} → ({{_ : S}} → Bool) → S

test : State
test = guard ⟦ f bool ⟧ -- doesn't work, used to work in agda 2.4

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

-- This is basically identical to Category, except that the
-- Obj type is a parameter rather than a field.

open import Level
open import Function.Base using (flip)

open import Relation.Binary using (Rel; IsEquivalence)

record Category {o : Level} (Obj : Set o) (ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  eta-equality
  infix  4 _≈_ _⇒_
  infixr 9 _∘_

  field
    _⇒_ : Rel Obj ℓ
    _≈_ : ∀ {A B} → Rel (A ⇒ B) e

    id  : ∀ {A} → (A ⇒ A)
    _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)

  field
    assoc     : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f)
    -- We add a symmetric proof of associativity so that the opposite category of the
    -- opposite category is definitionally equal to the original category. See how
    -- `op` is implemented.
    sym-assoc : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} → h ∘ (g ∘ f) ≈ (h ∘ g) ∘ f
    identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f
    identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f
    -- We add a proof of "neutral" identity proof, in order to ensure the opposite of
    -- constant functor is definitionally equal to itself.
    identity² : ∀ {A} → id ∘ id {A} ≈ id {A}
    equiv     : ∀ {A B} → IsEquivalence (_≈_ {A} {B})
    ∘-resp-≈  : ∀ {A B C} {f h : B ⇒ C} {g i : A ⇒ B} → f ≈ h → g ≈ i → f ∘ g ≈ h ∘ i

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
open import Agda.Builtin.Unit
open import Agda.Builtin.Sigma
open import Agda.Builtin.List
open import Agda.Builtin.Equality
open import Agda.Builtin.Reflection renaming (bindTC to infixl 4 _>>=_)

macro
  quoteDef : Name → Term → TC ⊤
  quoteDef f hole = (getDefinition f >>= quoteTC) >>= unify hole

postulate
  A : Set
  B : A → Set

-- foo is projection-like
foo : (x : A) → B x → B x
foo x y = y

pattern vArg x = arg (arg-info visible relevant) x

test : quoteDef foo ≡
  function
    (clause
     (("x" , vArg (def (quote A) [])) ∷
      ("y" , vArg (def (quote B) (vArg (var 0 []) ∷ [])))
      ∷ [])
     (vArg (var 1) ∷ vArg (var 0) ∷ [])
     (var 0 [])
     ∷ [])
test = refl

max_stars_repo_name: guilhermehas/agda

max_issues_repo_name: guilhermehas/agda

max_forks_repo_name: guilhermehas/agda


text:
-- Andreas, 2012-09-17 documenting an internal error in InternalToAbstract.hs
-- {-# OPTIONS -v syntax.reify.con:30 -v tc.with.type:30 #-}
module NameFirstIfHidden where

Total : (D : (A : Set) → A → Set)(A : Set) → Set
Total D A = forall a → D A a

data D (A : Set) : (a : A) → Set where
  c : Total D A

postulate P : {A : Set}{a : A} → D A a → Set

f : (A : Set)(a : A) → P (c a) → D A a
f A a p with Total
... | _ = c a
-- should succeed, triggered an internal error before

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

open import Groups.Definition
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Groups.Homomorphisms.Definition
open import Groups.Homomorphisms.Lemmas
open import Groups.Subgroups.Definition
open import Groups.Subgroups.Normal.Definition
open import Groups.Lemmas

module Groups.Homomorphisms.Kernel {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+G_ : A → A → A} {_+H_ : B → B → B} {G : Group S _+G_} {H : Group T _+H_} {f : A → B} (fHom : GroupHom G H f) where

open Setoid T
open Equivalence eq

groupKernelPred : A → Set d
groupKernelPred a = Setoid._∼_ T (f a) (Group.0G H)

groupKernelPredWd : {x y : A} → (Setoid._∼_ S x y) → groupKernelPred x → groupKernelPred y
groupKernelPredWd x=y fx=0 = transitive (GroupHom.wellDefined fHom (Equivalence.symmetric (Setoid.eq S) x=y)) fx=0

groupKernelIsSubgroup : Subgroup G groupKernelPred
Subgroup.closedUnderPlus groupKernelIsSubgroup fg=0 fh=0 = transitive (transitive (GroupHom.groupHom fHom) (Group.+WellDefined H fg=0 fh=0)) (Group.identLeft H)
Subgroup.containsIdentity groupKernelIsSubgroup = imageOfIdentityIsIdentity fHom
Subgroup.closedUnderInverse groupKernelIsSubgroup fg=0 = transitive (homRespectsInverse fHom) (transitive (inverseWellDefined H fg=0) (invIdent H))
Subgroup.isSubset groupKernelIsSubgroup = groupKernelPredWd

groupKernelIsNormalSubgroup : normalSubgroup G groupKernelIsSubgroup
groupKernelIsNormalSubgroup {g} fk=0 = transitive (transitive (transitive (GroupHom.groupHom fHom) (transitive (Group.+WellDefined H reflexive (transitive (GroupHom.groupHom fHom) (transitive (Group.+WellDefined H fk=0 reflexive) (Group.identLeft H)))) (symmetric (GroupHom.groupHom fHom)))) (GroupHom.wellDefined fHom (Group.invRight G {g}))) (imageOfIdentityIsIdentity fHom)


text:
open import Categories
open import Functors
open import RMonads

module RMonads.CatofRAdj {a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{J : Fun C D}
                         (M : RMonad J) where

open import Library

open import RAdjunctions

open Fun
open Cat

record ObjAdj {e f} : Set ((a ⊔ b ⊔ c ⊔ d ⊔ lsuc e ⊔ lsuc f)) where
  open RMonad M
  field E   : Cat {e}{f}
        adj : RAdj J E
  open RAdj adj
  field law : R ○ L ≅ TFun M
        ηlaw : ∀{X} → left (iden E {OMap L X}) ≅ η {X}
        bindlaw : ∀{X Y}{f : Hom D (OMap J X) (T Y)} →
          HMap R (right (subst (Hom D (OMap J X))
                               (fcong Y (cong OMap (sym law))) f))
          ≅ bind f
open ObjAdj

record HomAdj {e f}(A B : ObjAdj {e}{f}) : Set (a ⊔ b ⊔ c ⊔ d ⊔ lsuc (e ⊔ f))
  where
  constructor homadj
  open RAdj
  field K : Fun (E A) (E B)
        Llaw : K ○ L (adj A) ≅ L (adj B)
        Rlaw : R (adj A) ≅ R (adj B) ○ K
        rightlaw : {X : Obj C}{Y : Obj (E A)}
                   {f : Hom D (OMap J X) (OMap (R (adj A)) Y)} →
                   HMap K (right (adj A) {X}{Y} f)
                   ≅
                   right (adj B)
                         {X}
                         {OMap K Y}
                         (subst (Hom D (OMap J X))
                                (fcong Y (cong OMap Rlaw))
                                f)

open HomAdj

HomAdjEq : ∀{a b}{A B : ObjAdj {a}{b}}
           (f g : HomAdj A B) → K f ≅ K g → f ≅ g
HomAdjEq {A = A}{B} (homadj K _ _ _) (homadj .K _ _ _) refl =
  cong₃ (homadj K)
        (ir _ _)
        (ir _ _)
        (iext λ _ → iext λ _ → iext λ _ → hir refl)

rightlawlem : ∀{e f}{E : Cat {e}{f}}(R : Fun E D)(L : Fun C E) →
  (p : OMap R ≅ OMap (R ○ (IdF E))) →
  (right : {X : Obj C} {Y : Obj E} →
           Hom D (OMap J X) (OMap R Y) → Hom E (OMap L X) Y) →
  {X : Obj C}{Y : Obj E}{f : Hom D (OMap J X) (OMap R Y)} →
  right f ≅ right (subst (Hom D (OMap J X)) (fcong Y p) f)
rightlawlem R L refl right = refl

idLlaw : ∀{e f}(X : ObjAdj {e}{f}) →
         IdF (E X) ○ RAdj.L (adj X) ≅ RAdj.L (adj X)
idLlaw X = FunctorEq _ _ refl refl

idRlaw : ∀{e f}(X : ObjAdj {e}{f}) →
         RAdj.R (adj X) ≅ RAdj.R (adj X) ○ IdF (E X)
idRlaw X  = FunctorEq _ _ refl refl

idrightlaw : ∀{e f}
             (X : ObjAdj {e}{f}) →
             {X₁ : Obj C} {Y : Obj (E X)}
             {f : Hom D (OMap J X₁) (OMap (RAdj.R (adj X)) Y)} →
             HMap (IdF (E X)) (RAdj.right (adj X) f)
             ≅
             RAdj.right (adj X)
                        (subst (Hom D (OMap J X₁))
                               (fcong Y (cong OMap (idRlaw X)))
                               f)
idrightlaw X =
  rightlawlem (R (adj X))
              (L (adj X))
              (cong OMap
                    (FunctorEq (R (adj X))
                               (R (adj X) ○ IdF (E X))
                               refl
                               refl))
              (right (adj X))
  where open RAdj

idHomAdj : ∀{e f}{X : ObjAdj {e}{f}} → HomAdj X X
idHomAdj {X = X} = record {
  K        = IdF (E X);
  Llaw     = idLlaw X;
  Rlaw     = idRlaw X;
  rightlaw = idrightlaw X }

HMaplem : ∀{a b c d}{C : Cat {a}{b}}{D : Cat {c}{d}}{X X' Y Y' : Obj C} →
          X ≅ X' → Y ≅ Y' →
          {f : Hom C X Y}{f' : Hom C X' Y'} → f ≅ f' → (F : Fun C D) →
          HMap F {X}{Y} f ≅ HMap F {X'}{Y'} f'
HMaplem refl refl refl F = refl

rightlawlem2 : ∀{e f g h i j}{E : Cat {e}{f}}{F : Cat {g}{h}}{G : Cat {i}{j}}
  (J : Fun C D)
  (RX : Fun E D)(LX : Fun C E)
  (RY : Fun F D)(LY : Fun C F)
  (RZ : Fun G D)(LZ : Fun C G)
  (KA : Fun E F)(KB : Fun F G) →
  (rightX : {X : Obj C}{Y : Obj E} →
            Hom D (OMap J X) (OMap RX Y) → Hom E (OMap LX X) Y)
  (rightY : {X : Obj C}{Y : Obj F} →
            Hom D (OMap J X) (OMap RY Y) → Hom F (OMap LY X) Y)
  (rightZ : {X : Obj C}{Y : Obj G} →
            Hom D (OMap J X) (OMap RZ Y) → Hom G (OMap LZ X) Y) →
  (p : RY ≅ RZ ○ KB)(q : RX ≅ RY ○ KA) →
  (p' : KA ○ LX ≅ LY) →
  (r : {X : Obj C}{Y : Obj F}{f : Hom D (OMap J X) (OMap RY Y)} →
       HMap KB (rightY f)
       ≅
       rightZ (subst (Hom D (OMap J X))
                     (fcong Y (cong OMap p))
                     f)) →
  (s : {X : Obj C}{Y : Obj E}{f : Hom D (OMap J X) (OMap RX Y)} →
       HMap KA (rightX f)
       ≅
       rightY (subst (Hom D (OMap J X))
                     (fcong Y (cong OMap q))
                     f)) →
  ∀{A B}(h : Hom D (OMap J A) (OMap RX B)) →
  HMap (KB ○ KA) (rightX h) ≅
  rightZ
  (subst (Hom D (OMap J A))
         (fcong B (cong OMap (trans q (cong (λ F₁ → F₁ ○ KA) p))))
         h)
rightlawlem2 J .((RZ ○ KB) ○ KA) LX .(RZ ○ KB) .(KA ○ LX) RZ LZ KA KB
  rightX rightY rightZ refl refl refl r s h = trans (cong (HMap KB) s) r

compLlaw : ∀{e f}{X Y Z : ObjAdj {e}{f}} →
            (f : HomAdj Y Z)(g : HomAdj X Y) →
            (K f ○ K g) ○ RAdj.L (adj X) ≅ RAdj.L (adj Z)
compLlaw f g = FunctorEq
  _
  _
  (ext (λ A → trans
    (cong (OMap (K f)) (cong (λ F → OMap F A) (Llaw g)))
    (cong (λ F → OMap F A) (Llaw f))))
  (iext λ A → iext λ B → ext λ h → trans
    (HMaplem
      (cong (λ F → OMap F A) (Llaw g))
      (cong (λ F → OMap F B) (Llaw g))
      (cong (λ F → HMap F h) (Llaw g))
      (K f))
    (cong (λ F → HMap F h) (Llaw f)))

compRlaw : ∀{e f}{X Y Z : ObjAdj {e}{f}} →
            (f : HomAdj Y Z)(g : HomAdj X Y) →
            RAdj.R (adj X) ≅ RAdj.R (adj Z) ○ (K f ○ K g)
compRlaw f g = FunctorEq
  _
  _
  (ext (λ A → trans
    (cong (λ F → OMap F A) (Rlaw g))
    (cong (λ F → OMap F (OMap (K g) A)) (Rlaw f))))
  (iext λ A → iext λ B → ext λ h → trans
    (cong (λ F → HMap F h) (Rlaw g))
    (cong (λ F → HMap F (HMap (K g) h)) (Rlaw f)))

comprightlaw : ∀{e f}{X Y Z : ObjAdj {e}{f}} →
            (f : HomAdj Y Z)(g : HomAdj X Y) →
            {A : Obj C} {B : Obj (E X)}
            {h : Hom D (OMap J A) (OMap (RAdj.R (adj X)) B)} →
            HMap (K f ○ K g) (RAdj.right (adj X) h)
            ≅
            RAdj.right (adj Z)
                       (subst (Hom D (OMap J A))
                              (fcong B (cong OMap (compRlaw f g)))
                              h)
comprightlaw {X = X}{Y}{Z} f g {A}{B}{h} = trans
  (rightlawlem2 J (R (adj X)) (L (adj X)) (R (adj Y)) (L (adj Y))
   (R (adj Z)) (L (adj Z)) (K g) (K f) (right (adj X)) (right (adj Y))
   (right (adj Z)) (Rlaw f) (Rlaw g) (Llaw g) (rightlaw f)
   (rightlaw g) h) (cong (right (adj Z)) (trans (stripsubst (Hom D (OMap J A)) h (fcong B (cong OMap (trans (Rlaw g) (cong (λ F → F ○ K g) (Rlaw f)))))) (sym (stripsubst (Hom D (OMap J A)) h (fcong B (cong OMap (compRlaw f g))))))) where open RAdj

compHomAdj : ∀{e f}{X Y Z : ObjAdj {e}{f}} →
             HomAdj Y Z → HomAdj X Y → HomAdj X Z
compHomAdj f g = record {
  K        = K f ○ K g;
  Llaw     = compLlaw f g;
  Rlaw     = compRlaw f g;
  rightlaw = comprightlaw f g }

idlHomAdj : ∀{e f}{X Y : ObjAdj {e}{f}}
            {f : HomAdj X Y} → compHomAdj idHomAdj f ≅ f
idlHomAdj = HomAdjEq _ _ (FunctorEq _ _ refl refl)

idrHomAdj : ∀{e f}{X Y : ObjAdj {e}{f}}
            {f : HomAdj X Y} → compHomAdj f idHomAdj ≅ f
idrHomAdj  = HomAdjEq _ _ (FunctorEq _ _ refl refl)

assHomAdj : ∀{a b}{W X Y Z : ObjAdj {a}{b}}
            {f : HomAdj Y Z} {g : HomAdj X Y} {h : HomAdj W X} →
            compHomAdj (compHomAdj f g) h ≅ compHomAdj f (compHomAdj g h)
assHomAdj = HomAdjEq _ _ (FunctorEq _ _ refl refl)

CatofAdj : ∀{a b} → Cat
CatofAdj {a}{b} = record{
  Obj  = ObjAdj {a}{b};
  Hom  = HomAdj;
  iden = idHomAdj;
  comp = compHomAdj;
  idl  = idlHomAdj;
  idr  = idrHomAdj;
  ass  = λ{_ _ _ _ f g h} →
    assHomAdj {f = f}{g}{h}}

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


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

open import Categories.Category

module Categories.Functor.Core where

open import Level
open import Categories.Support.EqReasoning

record Functor {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) (D : Category o′ ℓ′ e′) : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
  eta-equality
  private module C = Category C
  private module D = Category D

  field
    F₀ : C.Obj → D.Obj
    {F₁} : ∀ {A B} → C [ A , B ] → D [ F₀ A , F₀ B ]

    .{identity} : ∀ {A} → D [ F₁ (C.id {A}) ≡ D.id ]
    .{homomorphism} : ∀ {X Y Z} {f : C [ X , Y ]} {g : C [ Y , Z ]}
                  → D [ F₁ (C [ g ∘ f ]) ≡ D [ F₁ g ∘ F₁ f ] ]
    .{F-resp-≡} : ∀ {A B} {F G : C [ A , B ]} → C [ F ≡ G ] → D [ F₁ F ≡ F₁ G ]

  op : Functor C.op D.op
  op = record
    { F₀ = F₀
    ; F₁ = F₁
    ; identity = identity
    ; homomorphism = homomorphism
    ; F-resp-≡ = F-resp-≡
    }

Endofunctor : ∀ {o ℓ e} → Category o ℓ e → Set _
Endofunctor C = Functor C C

Contravariant : ∀ {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) (D : Category o′ ℓ′ e′) → Set _
Contravariant C D = Functor C.op D
  where module C = Category C

id : ∀ {o ℓ e} {C : Category o ℓ e} → Endofunctor C
id {C = C} = record
  { F₀ = λ x → x
  ; F₁ = λ x → x
  ; identity = refl
  ; homomorphism = refl
  ; F-resp-≡ = λ x → x
  }
  where open Category.Equiv C

infixr 9 _∘_

_∘_ : ∀ {o ℓ e} {o′ ℓ′ e′} {o′′ ℓ′′ e′′} {C : Category o ℓ e} {D : Category o′ ℓ′ e′} {E : Category o′′ ℓ′′ e′′}
    → Functor D E → Functor C D → Functor C E
_∘_ {C = C} {D = D} {E = E} F G = record
  { F₀ = λ x → F₀ (G₀ x)
  ; F₁ = λ f → F₁ (G₁ f)
  ; identity = identity′
  ; homomorphism = homomorphism′
  ; F-resp-≡ = ∘-resp-≡′
  }
  where
  module C = Category C
  module D = Category D
  module E = Category E
  module F = Functor F
  module G = Functor G
  open F
  open G renaming (F₀ to G₀; F₁ to G₁; F-resp-≡ to G-resp-≡)

  .identity′ : ∀ {A} → E [ F₁ (G₁ (C.id {A})) ≡ E.id ]
  identity′ = begin
                F₁ (G₁ C.id)
              ≈⟨ F-resp-≡ G.identity ⟩
                F₁ D.id
              ≈⟨ F.identity ⟩
                E.id
              ∎
    where
    open SetoidReasoning E.hom-setoid

  .homomorphism′ : ∀ {X Y Z} {f : C [ X , Y ]} {g : C [ Y , Z ]}
                 → E [ F₁ (G₁ (C [ g ∘ f ])) ≡ E [ F₁ (G₁ g) ∘ F₁ (G₁ f) ] ]
  homomorphism′ {f = f} {g = g} = begin
                                    F₁ (G₁ (C [ g ∘ f ]))
                                  ≈⟨ F-resp-≡ G.homomorphism ⟩
                                    F₁ (D [ G₁ g ∘ G₁ f ])
                                  ≈⟨ F.homomorphism ⟩
                                    (E [ F₁ (G₁ g) ∘ F₁ (G₁ f) ])
                                  ∎
    where
    open SetoidReasoning E.hom-setoid

  .∘-resp-≡′ : ∀ {A B} {F G : C [ A , B ]}
            → C [ F ≡ G ] → E [ F₁ (G₁ F) ≡ F₁ (G₁ G) ]
  ∘-resp-≡′ = λ x → F-resp-≡ (G-resp-≡ x)

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module FunClause where

f
  : {A : Set}
  → A
  → A
f x
  = y
  where
    y = x
    z = x

data List
  (A : Set)
  : Set
  where

  nil
    : List A

  cons
    : A
    → List A
    → List A

snoc
  : {A : Set}
  → List A
  → A
  → List A
snoc nil y
  = cons y nil
snoc (cons x xs) y
  = cons x (snoc xs y)

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
------------------------------------------------------------------------
-- Brandt and Henglein's subterm relation
------------------------------------------------------------------------

module RecursiveTypes.Subterm where

open import Algebra
open import Data.Fin using (Fin; zero; suc; lift)
open import Data.Nat
open import Data.List using (List; []; _∷_; [_]; _++_)
open import Data.List.Properties
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.List.Relation.Unary.Any.Properties
  using (++↔; map-with-∈↔)
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
open import Data.List.Relation.Binary.BagAndSetEquality as BSEq
open import Data.List.Relation.Binary.Subset.Propositional
open import Data.List.Relation.Binary.Subset.Propositional.Properties
open import Data.Product
open import Data.Sum
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse using (module Inverse)
open import Relation.Binary
import Relation.Binary.Reasoning.Preorder as PreR
import Relation.Binary.Reasoning.Setoid as EqR
import Relation.Binary.PropositionalEquality as P
open import Data.Fin.Substitution

private
  open module SetM {A : Set} =
    CommutativeMonoid (BSEq.commutativeMonoid set A)
      using (_≈_)

open import RecursiveTypes.Syntax
open import RecursiveTypes.Substitution
  hiding (subst) renaming (id to idˢ)
open // using (_//_)

------------------------------------------------------------------------
-- Subterms

-- The subterm relation.

infix 4 _⊑_

data _⊑_ {n} : Ty n → Ty n → Set where
  refl   : ∀ {τ} → τ ⊑ τ
  unfold : ∀ {σ τ₁ τ₂} (σ⊑ : σ ⊑ unfold[μ τ₁ ⟶ τ₂ ]) → σ ⊑ μ τ₁ ⟶ τ₂
  ⟶ˡ     : ∀ {σ τ₁ τ₂} (σ⊑τ₁ : σ ⊑ τ₁) → σ ⊑ τ₁ ⟶ τ₂
  ⟶ʳ     : ∀ {σ τ₁ τ₂} (σ⊑τ₂ : σ ⊑ τ₂) → σ ⊑ τ₁ ⟶ τ₂

-- Some simple consequences.

unfold′ : ∀ {n} {τ₁ τ₂ : Ty (suc n)} →
          unfold[μ τ₁ ⟶ τ₂ ] ⊑ μ τ₁ ⟶ τ₂
unfold′ = unfold refl

⟶ˡ′ : ∀ {n} {τ₁ τ₂ : Ty n} → τ₁ ⊑ τ₁ ⟶ τ₂
⟶ˡ′ = ⟶ˡ refl

⟶ʳ′ : ∀ {n} {τ₁ τ₂ : Ty n} → τ₂ ⊑ τ₁ ⟶ τ₂
⟶ʳ′ = ⟶ʳ refl

-- The subterm relation is transitive.

trans : ∀ {n} {σ τ χ : Ty n} →
        σ ⊑ τ → τ ⊑ χ → σ ⊑ χ
trans σ⊑τ refl        = σ⊑τ
trans σ⊑τ (unfold τ⊑) = unfold (trans σ⊑τ τ⊑)
trans σ⊑τ (⟶ˡ τ⊑δ₁)   = ⟶ˡ (trans σ⊑τ τ⊑δ₁)
trans σ⊑τ (⟶ʳ τ⊑δ₂)   = ⟶ʳ (trans σ⊑τ τ⊑δ₂)

------------------------------------------------------------------------
-- Subterm closure

-- The list τ_∗ contains exactly the subterms of τ (possibly with
-- duplicates).
--
-- The important property is completeness, which ensures that the
-- number of distinct subterms of a given type is always finite.

mutual

  infix 7 _∗ _∗′

  _∗ : ∀ {n} → Ty n → List (Ty n)
  τ ∗ = τ ∷ τ ∗′

  _∗′ : ∀ {n} → Ty n → List (Ty n)
  (τ₁ ⟶ τ₂)   ∗′ = τ₁ ∗ ++ τ₂ ∗
  (μ τ₁ ⟶ τ₂) ∗′ = (τ₁ ⟶ τ₂ ∷ τ₁ ∗ ++ τ₂ ∗) // sub (μ τ₁ ⟶ τ₂)
  τ           ∗′ = []

------------------------------------------------------------------------
-- Soundness

-- _/_ is monotonous in its left argument.

/-monoˡ : ∀ {m n σ τ} {ρ : Sub Ty m n} →
          σ ⊑ τ → σ / ρ ⊑ τ / ρ
/-monoˡ refl                              = refl
/-monoˡ (⟶ˡ σ⊑τ₁)                         = ⟶ˡ (/-monoˡ σ⊑τ₁)
/-monoˡ (⟶ʳ σ⊑τ₂)                         = ⟶ʳ (/-monoˡ σ⊑τ₂)
/-monoˡ {ρ = ρ} (unfold {σ} {τ₁} {τ₂} σ⊑) =
  unfold $ P.subst (λ χ → σ / ρ ⊑ χ)
                   (sub-commutes (τ₁ ⟶ τ₂))
                   (/-monoˡ σ⊑)

sub-⊑-μ : ∀ {n} {σ : Ty (suc n)} {τ₁ τ₂} →
          σ ⊑ τ₁ ⟶ τ₂ → σ / sub (μ τ₁ ⟶ τ₂) ⊑ μ τ₁ ⟶ τ₂
sub-⊑-μ σ⊑τ₁⟶τ₂ = unfold (/-monoˡ σ⊑τ₁⟶τ₂)

-- All list elements are subterms.

sound : ∀ {n σ} (τ : Ty n) → σ ∈ τ ∗ → σ ⊑ τ
sound τ         (here P.refl) = refl
sound (τ₁ ⟶ τ₂) (there σ∈)    =
  [ ⟶ˡ ∘ sound τ₁ , ⟶ʳ ∘ sound τ₂ ]′
    (Inverse.from (++↔ {xs = τ₁ ∗}) ⟨$⟩ σ∈)
sound (μ τ₁ ⟶ τ₂) (there (here P.refl)) = unfold refl
sound (μ τ₁ ⟶ τ₂) (there (there σ∈))
  with Inverse.from (map-∈↔ (λ σ → σ / sub (μ τ₁ ⟶ τ₂))
                            {xs = τ₁ ∗ ++ τ₂ ∗}) ⟨$⟩ σ∈
... | (χ , χ∈ , P.refl) =
  sub-⊑-μ $ [ ⟶ˡ ∘ sound τ₁ , ⟶ʳ ∘ sound τ₂ ]′
              (Inverse.from (++↔ {xs = τ₁ ∗}) ⟨$⟩ χ∈)
sound ⊥       (there ())
sound ⊤       (there ())
sound (var x) (there ())

------------------------------------------------------------------------
-- Completeness

++-lemma : ∀ {A} xs ys {zs : List A} →
           (xs ++ zs) ++ (ys ++ zs) ≈ (xs ++ ys) ++ zs
++-lemma xs ys {zs} = begin
  (xs ++ zs) ++ (ys ++ zs)  ≈⟨ SetM.assoc xs zs (ys ++ zs) ⟩
  xs ++ (zs ++ (ys ++ zs))  ≈⟨ SetM.∙-cong (SetM.refl {x = xs}) (begin
    zs ++ (ys ++ zs)             ≈⟨ SetM.∙-cong (SetM.refl {x = zs}) (SetM.comm ys zs) ⟩
    zs ++ (zs ++ ys)             ≈⟨ SetM.sym $ SetM.assoc zs zs ys ⟩
    (zs ++ zs) ++ ys             ≈⟨ SetM.∙-cong (++-idempotent zs) SetM.refl ⟩
    zs ++ ys                     ≈⟨ SetM.comm zs ys ⟩
    ys ++ zs                     ∎) ⟩
  xs ++ (ys ++ zs)          ≈⟨ SetM.sym $ SetM.assoc xs ys zs ⟩
  (xs ++ ys) ++ zs          ∎
  where open EqR ([ set ]-Equality _)

open BSEq.⊆-Reasoning

mutual

  -- Weakening "commutes" with _∗.

  wk-∗-commute : ∀ k {n} (σ : Ty (k + n)) →
                 σ / wk ↑⋆ k ∗ ⊆ σ ∗ // wk ↑⋆ k
  wk-∗-commute k σ (here P.refl) = here P.refl
  wk-∗-commute k σ (there •∈•)   = there $ wk-∗′-commute k σ •∈•

  wk-∗′-commute : ∀ k {n} (σ : Ty (k + n)) →
                  σ / wk ↑⋆ k ∗′ ⊆ σ ∗′ // wk ↑⋆ k
  wk-∗′-commute k (σ₁ ⟶ σ₂) = begin
    σ₁ ⟶ σ₂ / wk ↑⋆ k ∗′                ≡⟨ P.refl ⟩
    σ₁ / wk ↑⋆ k ∗ ++ σ₂ / wk ↑⋆ k ∗    ⊆⟨ ++⁺ (wk-∗-commute k σ₁)
                                               (wk-∗-commute k σ₂) ⟩
    σ₁ ∗ // wk ↑⋆ k ++ σ₂ ∗ // wk ↑⋆ k  ≡⟨ P.sym $ map-++-commute
                                             (λ σ → σ / wk ↑⋆ k) (σ₁ ∗) (σ₂ ∗) ⟩
    (σ₁ ∗ ++ σ₂ ∗) // wk ↑⋆ k           ≡⟨ P.refl ⟩
    σ₁ ⟶ σ₂ ∗′ // wk ↑⋆ k               ∎
  wk-∗′-commute k (μ σ₁ ⟶ σ₂) = begin
    (μ σ₁ ⟶ σ₂) / wk ↑⋆ k ∗′                          ≡⟨ P.refl ⟩
    σ₁ ⟶ σ₂ / wk ↑⋆ (suc k) / sub (σ / wk ↑⋆ k) ∷
      (σ₁ / wk ↑⋆ (suc k) ∗ ++ σ₂ / wk ↑⋆ (suc k) ∗)
        // sub (σ / wk ↑⋆ k)                          ⊆⟨ ++⁺ lem₁ lem₂ ⟩
    σ₁ ⟶ σ₂ / sub σ / wk ↑⋆ k ∷
      (σ₁ ∗ ++ σ₂ ∗) // sub σ // wk ↑⋆ k              ≡⟨ P.refl ⟩
    μ σ₁ ⟶ σ₂ ∗′ // wk ↑⋆ k                           ∎
    where
    σ = μ σ₁ ⟶ σ₂

    lem₁ : _ ⊆ _
    lem₁ = begin
      [ σ₁ ⟶ σ₂ / wk ↑⋆ (suc k) / sub (σ / wk ↑⋆ k) ]  ≡⟨ P.cong [_] $ P.sym $
                                                            sub-commutes (σ₁ ⟶ σ₂) ⟩
      [ σ₁ ⟶ σ₂ / sub σ / wk ↑⋆ k                   ]  ∎

    lem₂ : _ ⊆ _
    lem₂ = begin
      (σ₁ / wk ↑⋆ (suc k) ∗ ++
       σ₂ / wk ↑⋆ (suc k) ∗) // sub (σ / wk ↑⋆ k)           ⊆⟨ map⁺ _ (++⁺ (wk-∗-commute (suc k) σ₁)
                                                                           (wk-∗-commute (suc k) σ₂)) ⟩
      (σ₁ ∗ // wk ↑⋆ (suc k) ++
       σ₂ ∗ // wk ↑⋆ (suc k)) // sub (σ / wk ↑⋆ k)          ≡⟨ P.cong (λ σs → σs // sub (σ / wk ↑⋆ k)) $
                                                                 P.sym $ map-++-commute
                                                                   (λ σ → σ / wk ↑⋆ suc k) (σ₁ ∗) (σ₂ ∗) ⟩
      (σ₁ ∗ ++ σ₂ ∗) // wk ↑⋆ (suc k) // sub (σ / wk ↑⋆ k)  ≡⟨ P.sym $ //.sub-commutes (σ₁ ∗ ++ σ₂ ∗) ⟩
      (σ₁ ∗ ++ σ₂ ∗) // sub σ // wk ↑⋆ k                    ∎
  wk-∗′-commute k (var x) = begin
    var x / wk ↑⋆ k ∗′     ≡⟨ P.cong _∗′ (var-/-wk-↑⋆ k x) ⟩
    var (lift k suc x) ∗′  ≡⟨ P.refl ⟩
    []                     ⊆⟨ (λ ()) ⟩
    var x ∗′ // wk ↑⋆ k    ∎
  wk-∗′-commute k ⊥ = λ ()
  wk-∗′-commute k ⊤ = λ ()

-- Substitution "commutes" with _∗.

sub-∗′-commute-var : ∀ k {n} x (τ : Ty n) →
                     var x / sub τ ↑⋆ k ∗′ ⊆ τ ∗ // wk⋆ k
sub-∗′-commute-var zero zero τ = begin
  τ ∗′             ⊆⟨ there ⟩
  τ ∗              ≡⟨ P.sym $ //.id-vanishes (τ ∗) ⟩
  τ ∗ // wk⋆ zero  ∎
sub-∗′-commute-var zero (suc x) τ = begin
  var x / idˢ ∗′   ≡⟨ P.cong _∗′ (id-vanishes (var x)) ⟩
  var x ∗′         ≡⟨ P.refl ⟩
  []               ⊆⟨ (λ ()) ⟩
  τ ∗ // wk⋆ zero  ∎
sub-∗′-commute-var (suc k) zero τ = begin
  []                  ⊆⟨ (λ ()) ⟩
  τ ∗ // wk⋆ (suc k)  ∎
sub-∗′-commute-var (suc k) (suc x) τ = begin
  var (suc x) / sub τ ↑⋆ suc k ∗′         ≡⟨ P.cong _∗′ (suc-/-↑ {ρ = sub τ ↑⋆ k} x) ⟩
  var x / sub τ ↑⋆ k / wk ∗′              ⊆⟨ wk-∗′-commute zero (var x / sub τ ↑⋆ k) ⟩
  var x / sub τ ↑⋆ k ∗′ // wk             ⊆⟨ map⁺ _ (sub-∗′-commute-var k x τ) ⟩
  τ ∗ // wk⋆ k // wk                      ≡⟨ P.sym $ //./-weaken (τ ∗) ⟩
  τ ∗ // wk⋆ (suc k)                      ∎

sub-∗-commute : ∀ k {n} σ (τ : Ty n) →
                σ / sub τ ↑⋆ k ∗ ⊆ σ ∗ // sub τ ↑⋆ k ++ τ ∗ // wk⋆ k
sub-∗-commute k σ         τ     (here P.refl) = here P.refl
sub-∗-commute k ⊥         τ     •∈•           = Inverse.to ++↔ ⟨$⟩ inj₁ •∈•
sub-∗-commute k ⊤         τ     •∈•           = Inverse.to ++↔ ⟨$⟩ inj₁ •∈•
sub-∗-commute k (var x)   τ     (there •∈•)   = there $ sub-∗′-commute-var k x τ •∈•
sub-∗-commute k (σ₁ ⟶ σ₂) τ {χ} (there •∈•)   = there $
  χ                                    ∈⟨ •∈• ⟩
  (σ₁ / ρ) ∗ ++ (σ₂ / ρ) ∗             ⊆⟨ ++⁺ (sub-∗-commute k σ₁ τ)
                                              (sub-∗-commute k σ₂ τ) ⟩
  (σ₁ ∗ // ρ ++ τ ∗ // wk⋆ k) ++
  (σ₂ ∗ // ρ ++ τ ∗ // wk⋆ k)          ∼⟨ ++-lemma (σ₁ ∗ // ρ) (σ₂ ∗ // ρ) ⟩
  (σ₁ ∗ // ρ ++ σ₂ ∗ // ρ) ++
  τ ∗ // wk⋆ k                         ≡⟨ P.cong₂ _++_
                                            (P.sym $ map-++-commute (λ σ → σ / ρ) (σ₁ ∗) (σ₂ ∗))
                                            P.refl ⟩
  (σ₁ ∗ ++ σ₂ ∗) // ρ ++ τ ∗ // wk⋆ k  ∎
  where ρ = sub τ ↑⋆ k
sub-∗-commute k (μ σ₁ ⟶ σ₂) τ (there (here P.refl)) =
  there $ here $ P.sym $ sub-commutes (σ₁ ⟶ σ₂)
sub-∗-commute k (μ σ₁ ⟶ σ₂) τ {χ} (there (there •∈•)) = there $ there $
  χ                                              ∈⟨ •∈• ⟩
  ((σ₁ / ρ ↑) ∗ ++ (σ₂ / ρ ↑) ∗) // sub (σ / ρ)  ⊆⟨ map⁺ _ (begin
      (σ₁ / ρ ↑) ∗ ++ (σ₂ / ρ ↑) ∗                    ⊆⟨ ++⁺ (sub-∗-commute (suc k) σ₁ τ)
                                                             (sub-∗-commute (suc k) σ₂ τ) ⟩
      (σ₁ ∗ // ρ ↑ ++ τ ∗ // wk⋆ (suc k)) ++
      (σ₂ ∗ // ρ ↑ ++ τ ∗ // wk⋆ (suc k))             ∼⟨ ++-lemma (σ₁ ∗ // ρ ↑) (σ₂ ∗ // ρ ↑) ⟩
      (σ₁ ∗ // ρ ↑ ++ σ₂ ∗ // ρ ↑) ++
      τ ∗ // wk⋆ (suc k)                              ≡⟨ P.cong₂ _++_
                                                           (P.sym $ map-++-commute
                                                                      (λ σ → σ / ρ ↑) (σ₁ ∗) (σ₂ ∗))
                                                           P.refl ⟩
      (σ₁ ∗ ++ σ₂ ∗) // ρ ↑ ++
      τ ∗ // wk⋆ (suc k)                              ∎) ⟩
  ((σ₁ ∗ ++ σ₂ ∗) // ρ ↑ ++
   τ ∗ // wk⋆ (suc k)) // sub (σ / ρ)            ≡⟨ map-++-commute (λ χ → χ / sub (σ / ρ))
                                                                   ((σ₁ ∗ ++ σ₂ ∗) // ρ ↑) _ ⟩
  (σ₁ ∗ ++ σ₂ ∗) // ρ ↑ // sub (σ / ρ) ++
  τ ∗ // wk⋆ (suc k) // sub (σ / ρ)              ≡⟨ P.cong₂ _++_
                                                      (P.sym $ //.sub-commutes (σ₁ ∗ ++ σ₂ ∗))
                                                      lem ⟩
  (σ₁ ∗ ++ σ₂ ∗) // sub σ // ρ ++
  τ ∗ // wk⋆ k                                   ∎
  where
  ρ = sub τ ↑⋆ k
  σ = μ σ₁ ⟶ σ₂

  lem = ≡R.begin
    τ ∗ // wk⋆ (suc k) // sub (σ / ρ)  ≡R.≡⟨ P.cong₂ _//_ (//./-weaken (τ ∗)) P.refl ⟩
    τ ∗ // wk⋆ k // wk // sub (σ / ρ)  ≡R.≡⟨ //.wk-sub-vanishes (τ ∗ // wk⋆ k) ⟩
    τ ∗ // wk⋆ k                       ≡R.∎
    where
    module ≡R = P.≡-Reasoning

-- The list contains all subterms.

complete : ∀ {n} {σ τ : Ty n} → σ ⊑ τ → σ ∈ τ ∗
complete refl                      = here P.refl
complete (⟶ˡ σ⊑τ₁)                 = there (Inverse.to ++↔                            ⟨$⟩ inj₁ (complete σ⊑τ₁))
complete (⟶ʳ σ⊑τ₂)                 = there (Inverse.to (++↔ {P = P._≡_ _} {xs = _ ∗}) ⟨$⟩ inj₂ (complete σ⊑τ₂))
complete (unfold {σ} {τ₁} {τ₂} σ⊑) =
  σ                                 ∈⟨ complete σ⊑ ⟩
  unfold[μ τ₁ ⟶ τ₂ ] ∗              ⊆⟨ sub-∗-commute zero (τ₁ ⟶ τ₂) τ ⟩
  τ₁ ⟶ τ₂ ∗ // sub τ ++ τ ∗ // idˢ  ≡⟨ P.cong (_++_ (τ₁ ⟶ τ₂ ∗ // sub τ))
                                              (//.id-vanishes (τ ∗)) ⟩
  τ ∗′ ++ τ ∗                       ⊆⟨ ++⁺ (there {x = τ} {xs = τ ∗′}) id ⟩
  τ ∗  ++ τ ∗                       ∼⟨ ++-idempotent (τ ∗) ⟩
  τ ∗                               ∎
  where τ = μ τ₁ ⟶ τ₂

------------------------------------------------------------------------
-- A wrapper function

-- Pairs up subterms with proofs.

subtermsOf : ∀ {n} (τ : Ty n) → List (∃ λ σ → σ ⊑ τ)
subtermsOf τ = map-with-∈ (τ ∗) (-,_ ∘′ sound τ)

-- subtermsOf is complete.

subtermsOf-complete : ∀ {n} {σ τ : Ty n} →
                      σ ⊑ τ → ∃ λ σ⊑τ → (σ , σ⊑τ) ∈ subtermsOf τ
subtermsOf-complete {σ = σ} {τ} σ⊑τ =
  (-, Inverse.to (map-with-∈↔ {f = -,_ ∘′ sound τ}) ⟨$⟩
        (σ , complete σ⊑τ , P.refl))

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
-- {-# OPTIONS -v reify:80 #-}

open import Common.Prelude
open import Common.Reflection
open import Common.Equality

module Issue1345 (A : Set) where

unquoteDecl idNat = define (vArg idNat)
  (funDef (pi (vArg (def (quote Nat) [])) (abs "" (def (quote Nat) [])))
          (clause (vArg (var "") ∷ []) (var 0 []) ∷ []))

thm : ∀ n → idNat n ≡ n
thm n = refl


text:
------------------------------------------------------------------------------
-- Testing the erasing of the duplicate definitions required by a conjecture
------------------------------------------------------------------------------

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

module DuplicateAgdaDefinitions1 where

infix 7 _≈_

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

postulate
  D   : Set
  _≈_ : D → D → Set

Eq : D → D → Set
Eq x y = x ≈ y
{-# ATP definition Eq #-}

postulate Eq-trans : ∀ {x y z} → Eq x y → Eq y z → Eq x z

postulate Eq-trans₂ : ∀ {w x y z} → Eq w x → Eq x y → Eq y z → Eq w z
{-# ATP prove Eq-trans₂ Eq-trans #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


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

module Cardinality.Infinite.ManifestEnumerable where

open import Prelude
open import Data.List.Kleene
open import Data.Fin
import Data.Nat as ℕ
open import Data.Nat using (_+_)
open import Cubical.Data.Sigma.Properties
open import Cubical.Foundations.Prelude using (J)
import Data.List.Kleene.Membership as Kleene
open import Codata.Stream
open import Cardinality.Infinite.Split

open import HITs.PropositionalTruncation.Sugar

private
  variable
    u : Level
    U : A → Type u
    s : Level
    S : ℕ → Type s

-- ℰ : Type a → Type a
-- ℰ A = Σ[ xs ⦂ Stream A ] Π[ x ⦂ A ] ∥ x ∈ xs ∥

-- ℰ≡ℕ↠ : ℰ A ≡ (ℕ ↠ A)
-- ℰ≡ℕ↠ = refl

-- _∥Σ∥_ : ℰ A → (∀ x → ℰ (U x)) → ℰ (Σ A U)
-- (xs ∥Σ∥ ys) .fst = cantor (xs .fst) (fst ∘ ys)
-- (xs ∥Σ∥ ys) .snd (x , y) =
--   concat-∈
--     (x , y)
--     (xs .fst * (fst ∘ ys)) ∥$∥
--     ⦇ (*-cover x (xs .fst) y (fst ∘ ys)) (xs .snd x) (ys x .snd y) ⦈

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

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

variable
  ℓ ℓ' : Level
  A : Set ℓ
  B : Set ℓ'
  x y z : A

sym : x ≡ y → y ≡ x
sym refl = refl

_∙_ : x ≡ y → y ≡ z → x ≡ z
refl ∙ refl = refl

leftId : (p : x ≡ y) → refl ∙ p ≡ p
leftId refl = refl

rightId : (p : x ≡ y) → p ∙ refl ≡ p
rightId refl = refl

transport : (P : A → Set ℓ') → x ≡ y → P x → P y
transport _ refl px = px

ap : (f : A → B) → x ≡ y → f x ≡ f y
ap _ refl = refl

apd : (P : A → Set ℓ') → (f : (a : A) → P a) → (p : x ≡ y) → transport P p (f x) ≡ f y
apd _ _ refl = refl

postulate
  Size : Set
  base : Size
  next : Size → Size
  inf : Size
  lim : next inf ≡ inf

postulate
  elim : (P : Size → Set ℓ) →
    (pb : P base) →
    (pn : (s : Size) → P s → P (next s)) →
    (pi : P inf) →
    -- (elim P pb pn pi pl (next inf)) = (elim P pb pn pi pl inf)
    (pl : transport P lim (pn inf pi) ≡ pi) →
    (s : Size) → P s
  elim-base : (P : Size → Set ℓ) →
    (pb : P base) →
    (pn : (s : Size) → P s → P (next s)) →
    (pi : P inf) →
    (pl : transport P lim (pn inf pi) ≡ pi) →
    elim P pb pn pi pl base ≡ pb
  elim-next : (P : Size → Set ℓ) →
    (pb : P base) →
    (pn : (s : Size) → P s → P (next s)) →
    (pi : P inf) →
    (pl : transport P lim (pn inf pi) ≡ pi) →
    (s : Size) →
    elim P pb pn pi pl (next s) ≡ pn s (elim P pb pn pi pl s)
  elim-inf : (P : Size → Set ℓ) →
    (pb : P base) →
    (pn : (s : Size) → P s → P (next s)) →
    (pi : P inf) →
    (pl : transport P lim (pn inf pi) ≡ pi) →
    elim P pb pn pi pl inf ≡ pi

{-# REWRITE elim-base elim-next elim-inf #-}

postulate
  elim-lim : (P : Size → Set ℓ) →
    (pb : P base) →
    (pn : (s : Size) → P s → P (next s)) →
    (pi : P inf) →
    (pl : transport P lim (pn inf pi) ≡ pi) →
    apd P (elim P pb pn pi pl) lim ≡ pl

{-# REWRITE elim-lim #-}

-- postulate lim-refl : transport (λ s → s ≡ inf) lim lim ≡ refl

absurd : ∀ {A s} → base ≡ next s → A
absurd {A} p =
  let discr : Size → Set
      discr = elim (λ _ → Set) Size (λ _ _ → A) A (apd (λ _ → Set) (λ _ → A) lim)
  in transport discr p base

inj : ∀ {s t} → next s ≡ next t → s ≡ t
inj {s} {t} p =
  let pred : Size → Size
      pred = elim (λ _ → Size) base (λ s _ → s) inf (apd (λ _ → Size) (λ s → inf) lim)
  in ap pred p

data Nat : Size → Set where
  zero : (s : Size) → Nat (next s)
  succ : (s : Size) → Nat s → Nat (next s)

prev : (P : Size → Set ℓ') → P (next inf) → P inf
prev P pni = transport P lim pni

double' : ∀ s → Nat s → Nat inf
double' _ (zero _) = prev Nat (zero inf)
double' _ (succ s n) = prev Nat (succ inf (prev Nat (succ inf (double' s n))))

-- pn inf pi ≡ pi
-- zero: zero = ?pi
-- next: succ _ (succ _ ?pi) = ?pi

double : ∀ s → Nat s → Nat inf
double = elim (λ s → Nat s → Nat inf) {!   !} {!   !} {!   !} {!   !}

max_stars_repo_name: ionathanch/msc-thesis

max_issues_repo_name: ionathanch/msc-thesis

max_forks_repo_name: ionathanch/msc-thesis


text:
----------------------------------------------------------------------------
-- Well-founded induction on the relation _◁_
----------------------------------------------------------------------------

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

-- N.B This module does not contain combined proofs, but it imports
-- modules which contain combined proofs.

module FOT.FOTC.Program.McCarthy91.WF-Relation.Induction.NonAcc.WellFoundedATP
  where

open import FOTC.Base

open import FOTC.Data.Nat

open import FOTC.Program.McCarthy91.McCarthy91
open import FOTC.Program.McCarthy91.WF-Relation
open import FOTC.Program.McCarthy91.WF-Relation.PropertiesATP

----------------------------------------------------------------------------
-- Adapted from FOTC.Data.Nat.Induction.WellFoundedI.wfInd-LT₁.

{-# TERMINATING #-}
◁-wfind : (P : D → Set) →
          (∀ {n} → N n → (∀ {m} → N m → m ◁ n → P m) → P n) →
          ∀ {n} → N n → P n
◁-wfind P h Nn = h Nn (helper Nn)
  where
    helper : ∀ {n m} → N n → N m → m ◁ n → P m
    helper Nn nzero 0◁n = ⊥-elim (0◁x→⊥ Nn 0◁n)

    -- This equation does not pass the termination check.
    helper nzero (nsucc Nm) Sm◁0 = h (nsucc Nm)
      (λ {m'} Nm' m'◁Sm →
        let m'◁0 : m' ◁ zero
            m'◁0 = ◁-trans Nm' (nsucc Nm) nzero m'◁Sm Sm◁0

        in helper nzero Nm' m'◁0
      )

    -- Other version of the previous equation (this version neither
    -- pass the termination check).
    -- helper nzero (nsucc {m} Nm) Sm◁0 = h (nsucc Nm)
    --   (λ {m'} Nm' m'◁Sm →
    --     let m'◁m : MCR m' m
    --         m'◁m = x◁Sy→x◁y Nm' Nm m'◁Sm

    --     in helper Nm Nm' m'◁m
    --   )

    -- Other version of the previous equation (this version neither
    -- pass the termination check).
    -- helper nzero Nm m◁0 = h Nm
    --   (λ {m'} Nm' m'◁m →
    --     let m'◁0 : MCR m' zero
    --         m'◁0 = ◁-trans Nm' Nm nzero m'◁m m◁0

    --     in helper nzero Nm' m'◁0
    --   )

    -- Other version of the previous equation (this version neither
    -- pass the termination check).
    -- helper {m = m} nzero Nm m◁0 =
    --   h Nm (λ {m'} Nm' m'◁m → helper Nm Nm' m'◁m)

    helper (nsucc {n} Nn) (nsucc {m} Nm) Sm◁Sn = helper Nn (nsucc Nm) Sm◁n
      where
        Sm◁n : succ₁ m ◁ n
        Sm◁n = x◁Sy→x◁y (nsucc Nm) Nn Sm◁Sn

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --no-qualified-instances #-}

module NoQualifiedInstances-ParameterizedImport where

postulate
  T : Set

open import NoQualifiedInstances.ParameterizedImport.A T as A

postulate
  f : {{A.I}} → A.I

test : A.I
test = f


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

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

module LibraBFT.ImplShared.Util.Dijkstra.All where

open import Dijkstra.All public
open import LibraBFT.ImplShared.LBFT public


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

module lambda.system-d where

open import Data.Nat
open import Data.Fin hiding (lift)

open import lambda.vec
open import lambda.untyped

infixr 21 _∧_
infixr 22 _⇒_

data type : Set where
  base : ℕ → type
  _⇒_ _∧_ : type → type → type

context : ℕ → Set
context = vec type

infix 10 _⊢_∶_

data _⊢_∶_ {n : ℕ} (Γ : context n) : term n → type → Set where
  ax : ∀ {i} → Γ ⊢ var i ∶ lookup i Γ
  lam : ∀ {A B x} → Γ ▸ A ⊢ x ∶ B → Γ ⊢ lam x ∶ A ⇒ B
  app : ∀ {A B x y} → Γ ⊢ x ∶ (A ⇒ B) → Γ ⊢ y ∶ A → Γ ⊢ app x y ∶ B
  ∧ⁱ : ∀ {A B x} → Γ ⊢ x ∶ A → Γ ⊢ x ∶ B → Γ ⊢ x ∶ A ∧ B
  ∧ᵉˡ : ∀ {A B x} → Γ ⊢ x ∶ A ∧ B → Γ ⊢ x ∶ A
  ∧ᵉʳ : ∀ {A B x} → Γ ⊢ x ∶ A ∧ B → Γ ⊢ x ∶ B

⊢_∶_ : term 0 → type → Set
⊢ x ∶ t = ε ⊢ x ∶ t

-- This lemma is actually false, because i did not setup the context
-- inclusions properly. It's not really complicated to fix: just
-- transpose the whole machinery from lambda.stack to lambda.vec. The
-- only thing is that it's a bit long and boring to get the same job
-- done on an indexed datatype. Substitution is hard to get right...
lift-p : ∀ {n A X Γ} {x : term n} → Γ ⊢ x ∶ A → Γ ▸ X ⊢ lift x ∶ A
lift-p ax = ax
lift-p (lam x) = {!!}
lift-p (app x y) = app (lift-p x) (lift-p y)
lift-p (∧ⁱ x₁ x₂) = ∧ⁱ (lift-p x₁) (lift-p x₂)
lift-p (∧ᵉˡ x) = ∧ᵉˡ (lift-p x)
lift-p (∧ᵉʳ x) = ∧ᵉʳ (lift-p x)

↑-p : ∀ {n m X Γ Δ} {ρ : Fin n → term m} →
      ((i : Fin n) → Δ ⊢ ρ i ∶ lookup i Γ) →
      (i : Fin (suc n)) → (Δ ▸ X) ⊢ ↑ ρ i ∶ lookup i (Γ ▸ X)
↑-p ρT zero = ax
↑-p ρT (suc i) = lift-p (ρT i)

subst-p : ∀ {n m A} {x : term n} {Γ : context n} {Δ : context m} {ρ : Fin n → term m} →
        Γ ⊢ x ∶ A → ((i : Fin n) → Δ ⊢ ρ i ∶ lookup i Γ) → Δ ⊢ subst x ρ ∶ A
subst-p (ax {i}) ρT = ρT i
subst-p (lam x) ρT = lam (subst-p x (↑-p ρT))
subst-p (app x y) ρT = app (subst-p x ρT) (subst-p y ρT)
subst-p (∧ⁱ x₁ x₂) ρT = ∧ⁱ (subst-p x₁ ρT) (subst-p x₂ ρT)
subst-p (∧ᵉˡ x) ρT = ∧ᵉˡ (subst-p x ρT)
subst-p (∧ᵉʳ x) ρT = ∧ᵉʳ (subst-p x ρT)


text:
module README where

------------------------------------------------------------------------
-- The Agda "standard" library, version 0.2
--
-- Author: Nils Anders Danielsson, with contributions from
-- Jean-Philippe Bernardy, Samuel Bronson, Liang-Ting Chen, Dan Doel,
-- Patrik Jansson, Shin-Cheng Mu, and Ulf Norell
------------------------------------------------------------------------

-- This version of the library has been tested using Agda 2.2.4.

-- Note that no guarantees are currently made about forwards or
-- backwards compatibility, the library is still at an experimental
-- stage.

-- To make use of the library, add the path to the library’s root
-- directory (src) to the Agda search path, either using the
-- --include-path flag or by customising the Emacs mode variable
-- agda2-include-dirs (M-x customize-group RET agda2 RET).

-- To compile programs using some of the IO functions you need to
-- install the Haskell package utf8-string (available from Hackage).

-- Contributions to this library are welcome. Please send
-- contributions in the form of darcs patches (run
-- darcs send --output <patch file> and attach the patch file to an
-- email), and include a statement saying that you agree to release
-- your library patches under the library's licence.

------------------------------------------------------------------------
-- Module hierarchy
------------------------------------------------------------------------

-- The top-level module names of the library are currently allocated
-- as follows:
--
-- • Algebra
--     Abstract algebra (monoids, groups, rings etc.), along with
--     properties needed to specify these structures (associativity,
--     commutativity, etc.), and operations on and proofs about the
--     structures.
-- • Category
--     Category theory-inspired idioms used to structure functional
--     programs (functors and monads, for instance).
-- • Coinduction
--     Support for coinduction.
-- • Data
--     Data types and properties about data types. (Also some
--     combinators working solely on and with functions; see
--     Data.Function.)
-- • Foreign
--     Related to the foreign function interface.
-- • Induction
--     A general framework for induction (includes lexicographic and
--     well-founded induction).
-- • IO
--     Input/output-related functions.
-- • Relation
--     Properties of and proofs about relations (mostly homogeneous
--     binary relations).
-- • Size
--     Sizes used by the sized types mechanism.

------------------------------------------------------------------------
-- A selection of useful library modules
------------------------------------------------------------------------

-- Note that module names in source code are often hyperlinked to the
-- corresponding module. In the Emacs mode you can follow these
-- hyperlinks by typing M-. or clicking with the middle mouse button.

-- • Some data types

import Data.Bool     -- Booleans.
import Data.Char     -- Characters.
import Data.Empty    -- The empty type.
import Data.Fin      -- Finite sets.
import Data.List     -- Lists.
import Data.Maybe    -- The maybe type.
import Data.Nat      -- Natural numbers.
import Data.Product  -- Products.
import Data.Stream   -- Streams.
import Data.String   -- Strings.
import Data.Sum      -- Disjoint sums.
import Data.Unit     -- The unit type.
import Data.Vec      -- Fixed-length vectors.

-- • Some types used to structure computations

import Category.Functor      -- Functors.
import Category.Applicative  -- Applicative functors.
import Category.Monad        -- Monads.

-- • Equality

-- Propositional equality:
import Relation.Binary.PropositionalEquality

-- Convenient syntax for "equational reasoning" using a preorder:
import Relation.Binary.PreorderReasoning

-- Solver for commutative ring or semiring equalities:
import Algebra.RingSolver

-- • Properties of functions, sets and relations

-- Monoids, rings and similar algebraic structures:
import Algebra

-- Negation, decidability, and similar operations on sets:
import Relation.Nullary

-- Properties of homogeneous binary relations:
import Relation.Binary

-- • Induction

-- An abstraction of various forms of recursion/induction:
import Induction

-- Well-founded induction:
import Induction.WellFounded

-- Various forms of induction for natural numbers:
import Induction.Nat

-- • Support for coinduction

import Coinduction

-- • IO

import IO

------------------------------------------------------------------------
-- Record hierarchies
------------------------------------------------------------------------

-- When an abstract hierarchy of some sort (for instance semigroup →
-- monoid → group) is included in the library the basic approach is to
-- specify the properties of every concept in terms of a record
-- containing just properties, parameterised on the underlying
-- operations, sets etc.:
--
--   record IsSemigroup {A} (≈ : Rel A) (∙ : Op₂ A) : Set where
--     open FunctionProperties ≈
--     field
--       isEquivalence : IsEquivalence ≈
--       assoc         : Associative ∙
--       ∙-pres-≈      : ∙ Preserves₂ ≈ ⟶ ≈ ⟶ ≈
--
-- More specific concepts are then specified in terms of the simpler
-- ones:
--
--     record IsMonoid {A} (≈ : Rel A) (∙ : Op₂ A) (ε : A) : Set where
--       open FunctionProperties ≈
--       field
--         isSemigroup : IsSemigroup ≈ ∙
--         identity    : Identity ε ∙
--
--     open IsSemigroup isSemigroup public
--
-- Note here that open IsSemigroup isSemigroup public ensures that the
-- fields of the isSemigroup record can be accessed directly; this
-- technique enables the user of an IsMonoid record to use underlying
-- records without having to manually open an entire record hierarchy.
-- This is not always possible, though. Consider the following definition
-- of preorders:
--
--   record IsPreorder {A : Set}
--                     (_≈_ : Rel A) -- The underlying equality.
--                     (_∼_ : Rel A) -- The relation.
--                     : Set where
--     field
--       isEquivalence : IsEquivalence _≈_
--       -- Reflexivity is expressed in terms of an underlying equality:
--       reflexive     : _≈_ ⇒ _∼_
--       trans         : Transitive _∼_
--       ∼-resp-≈      : _∼_ Respects₂ _≈_
--
--     module Eq = IsEquivalence isEquivalence
--
--     refl : Reflexive _∼_
--     refl = reflexive Eq.refl
--
-- The Eq module in IsPreorder is not opened publicly, because it
-- contains some fields which clash with fields or other definitions
-- in IsPreorder.

-- Records packing up properties with the corresponding operations,
-- sets, etc. are sometimes also defined:
--
--   record Semigroup : Set₁ where
--     infixl 7 _∙_
--     infix  4 _≈_
--     field
--       carrier     : Set
--       _≈_         : Rel carrier
--       _∙_         : Op₂ carrier
--       isSemigroup : IsSemigroup _≈_ _∙_
--
--     open IsSemigroup isSemigroup public
--
--     setoid : Setoid
--     setoid = record { isEquivalence = isEquivalence }
--
--   record Monoid : Set₁ where
--     infixl 7 _∙_
--     infix  4 _≈_
--     field
--       carrier  : Set
--       _≈_      : Rel carrier
--       _∙_      : Op₂ carrier
--       ε        : carrier
--       isMonoid : IsMonoid _≈_ _∙_ ε
--
--     open IsMonoid isMonoid public
--
--     semigroup : Semigroup
--     semigroup = record { isSemigroup = isSemigroup }
--
--     open Semigroup semigroup public using (setoid)
--
-- Note that the Monoid record does not include a Semigroup field.
-- Instead the Monoid /module/ includes a "repackaging function"
-- semigroup which converts a Monoid to a Semigroup.

-- The above setup may seem a bit complicated, but we think it makes the
-- library quite easy to work with, while also providing enough
-- flexibility.

------------------------------------------------------------------------
-- More documentation
------------------------------------------------------------------------

-- Some examples showing where the natural numbers and some related
-- operations and properties are defined, and how they can be used:

import README.Nat

------------------------------------------------------------------------
-- Core modules
------------------------------------------------------------------------

-- Some modules have names ending in ".Core". These modules are
-- internal, and have (mostly) been created to avoid mutual recursion
-- between modules. They should not be imported directly; their
-- contents are reexported by other modules.

------------------------------------------------------------------------
-- All library modules
------------------------------------------------------------------------

-- For short descriptions of every library module, see Everything:

import Everything

max_issues_repo_name: larrytheliquid/Lemmachine


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Functors
------------------------------------------------------------------------

-- Note that currently the functor laws are not included here.

module Category.Functor where

open import Function
open import Level

record RawFunctor {ℓ} (F : Set ℓ → Set ℓ) : Set (suc ℓ) where
  infixl 4 _<$>_ _<$_

  field
    _<$>_ : ∀ {A B} → (A → B) → F A → F B

  _<$_ : ∀ {A B} → A → F B → F A
  x <$ y = const x <$> y


text:
------------------------------------------------------------------------------
-- Testing variable names clash
------------------------------------------------------------------------------

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

module VariableNamesClash where

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

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

foo : (n : D) → a ≡ b
foo n = prf n
  where
  -- The translation of this postulate must use two diferents
  -- quantified variables names e.g. ∀ x. ∀ y. a ≡ b.
  postulate prf : (n : D) → a ≡ b
  {-# ATP prove prf #-}


text:
-- Solver for Functor

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

open import Categories.Category
open import Categories.Functor renaming (id to idF)

module Experiment.Categories.Solver.Functor
  {o ℓ e o′ ℓ′ e′} {𝒞 : Category o ℓ e} {𝒟 : Category o′ ℓ′ e′}
  (F : Functor 𝒞 𝒟)
  where

open import Level
open import Relation.Binary using (Rel)

import Categories.Morphism.Reasoning as MR

import Experiment.Categories.Solver.Category

module 𝒞 = Category 𝒞
module CS = Experiment.Categories.Solver.Category 𝒞
open CS using (:id; _:∘_; ∥_∥) renaming (∥-∥ to ∥-∥′) public

open Category 𝒟
open HomReasoning
open MR 𝒟

open Functor F

private
  variable
    A B C D E : Obj

infixr 9 _:∘_

data Expr : Rel Obj (o ⊔ o′ ⊔ ℓ ⊔ ℓ′) where
  :id  : Expr A A
  _:∘_ : Expr B C → Expr A B → Expr A C
  :F₁  : ∀ {A B} → CS.Expr A B → Expr (F₀ A) (F₀ B)
  ∥_∥  : A ⇒ B → Expr A B

-- Semantics
⟦_⟧ : Expr A B → A ⇒ B
⟦ :id      ⟧ = id
⟦ e₁ :∘ e₂ ⟧ = ⟦ e₁ ⟧ ∘ ⟦ e₂ ⟧
⟦ :F₁ e    ⟧ = F₁ CS.⟦ e ⟧
⟦ ∥ f ∥    ⟧ = f

F₁⟦_⟧N∘_ : ∀ {B C} → CS.Expr B C → A ⇒ F₀ B → A ⇒ F₀ C
F₁⟦ :id      ⟧N∘ g = g
F₁⟦ e₁ :∘ e₂ ⟧N∘ g = F₁⟦ e₁ ⟧N∘ (F₁⟦ e₂ ⟧N∘ g)
F₁⟦ ∥ f ∥    ⟧N∘ g = F₁ f ∘ g

⟦_⟧N∘_ : Expr B C → A ⇒ B → A ⇒ C
⟦ :id      ⟧N∘ g = g
⟦ e₁ :∘ e₂ ⟧N∘ g = ⟦ e₁ ⟧N∘ (⟦ e₂ ⟧N∘ g)
⟦ :F₁ e    ⟧N∘ g = F₁⟦ e ⟧N∘ g
⟦ ∥ f ∥    ⟧N∘ g = f ∘ g

⟦_⟧N : Expr A B → A ⇒ B
⟦ e ⟧N = ⟦ e ⟧N∘ id

F₁⟦e⟧N∘f≈F₁⟦e⟧∘f : ∀ {B C} (e : CS.Expr B C) (g : A ⇒ F₀ B) →
                   F₁⟦ e ⟧N∘ g ≈ F₁ CS.⟦ e ⟧ ∘ g
F₁⟦e⟧N∘f≈F₁⟦e⟧∘f :id        g = begin
  g           ≈˘⟨ identityˡ ⟩
  id ∘ g      ≈˘⟨ identity ⟩∘⟨refl ⟩
  F₁ 𝒞.id ∘ g ∎
F₁⟦e⟧N∘f≈F₁⟦e⟧∘f (e₁ :∘ e₂) g = begin
  F₁⟦ e₁ ⟧N∘ (F₁⟦ e₂ ⟧N∘ g)         ≈⟨ F₁⟦e⟧N∘f≈F₁⟦e⟧∘f e₁ (F₁⟦ e₂ ⟧N∘ g) ⟩
  F₁ CS.⟦ e₁ ⟧ ∘ (F₁⟦ e₂ ⟧N∘ g)     ≈⟨ pushʳ (F₁⟦e⟧N∘f≈F₁⟦e⟧∘f e₂ g) ⟩
  (F₁ CS.⟦ e₁ ⟧ ∘ F₁ CS.⟦ e₂ ⟧) ∘ g ≈˘⟨ homomorphism ⟩∘⟨refl ⟩
  F₁ (CS.⟦ e₁ ⟧ 𝒞.∘ CS.⟦ e₂ ⟧) ∘ g ∎
F₁⟦e⟧N∘f≈F₁⟦e⟧∘f ∥ x ∥      g = refl

⟦e⟧N∘f≈⟦e⟧∘f : (e : Expr B C) (g : A ⇒ B) → ⟦ e ⟧N∘ g ≈ ⟦ e ⟧ ∘ g
⟦e⟧N∘f≈⟦e⟧∘f :id        g = ⟺ identityˡ
⟦e⟧N∘f≈⟦e⟧∘f (e₁ :∘ e₂) g = begin
  ⟦ e₁ ⟧N∘ (⟦ e₂ ⟧N∘ g) ≈⟨ ⟦e⟧N∘f≈⟦e⟧∘f e₁ (⟦ e₂ ⟧N∘ g) ⟩
  ⟦ e₁ ⟧ ∘ (⟦ e₂ ⟧N∘ g) ≈⟨ pushʳ (⟦e⟧N∘f≈⟦e⟧∘f e₂ g) ⟩
  (⟦ e₁ ⟧ ∘ ⟦ e₂ ⟧) ∘ g ∎
⟦e⟧N∘f≈⟦e⟧∘f (:F₁ e)    g = F₁⟦e⟧N∘f≈F₁⟦e⟧∘f e g
⟦e⟧N∘f≈⟦e⟧∘f ∥ f ∥      g = refl

⟦e⟧N≈⟦e⟧ : (e : Expr A B) → ⟦ e ⟧N ≈ ⟦ e ⟧
⟦e⟧N≈⟦e⟧ e = ⟦e⟧N∘f≈⟦e⟧∘f e id ○ identityʳ

solve : (e₁ e₂ : Expr A B) → ⟦ e₁ ⟧N ≈ ⟦ e₂ ⟧N → ⟦ e₁ ⟧ ≈ ⟦ e₂ ⟧
solve e₁ e₂ eq = begin
  ⟦ e₁ ⟧  ≈˘⟨ ⟦e⟧N≈⟦e⟧ e₁ ⟩
  ⟦ e₁ ⟧N ≈⟨ eq ⟩
  ⟦ e₂ ⟧N ≈⟨ ⟦e⟧N≈⟦e⟧ e₂ ⟩
  ⟦ e₂ ⟧  ∎

∥-∥ : ∀ {f : A ⇒ B} → Expr A B
∥-∥ {f = f} = ∥ f ∥


text:
module Thesis.LangChanges where

open import Thesis.Changes
open import Thesis.IntChanges
open import Thesis.Types
open import Thesis.Contexts
open import Thesis.Environments
open import Relation.Binary.PropositionalEquality

Chτ : (τ : Type) → Set
Chτ τ = ⟦ Δt τ ⟧Type

ΔΓ : Context → Context
ΔΓ ∅ = ∅
ΔΓ (τ • Γ) = Δt τ • τ • ΔΓ Γ

ChΓ : ∀ (Γ : Context) → Set
ChΓ Γ = ⟦ ΔΓ Γ ⟧Context

[_]τ_from_to_ : ∀ (τ : Type) → (dv : Chτ τ) → (v1 v2 : ⟦ τ ⟧Type) → Set

isCompChangeStructureτ : ∀ τ → IsCompChangeStructure ⟦ τ ⟧Type ⟦ Δt τ ⟧Type [ τ ]τ_from_to_

changeStructureτ : ∀ τ → ChangeStructure ⟦ τ ⟧Type
changeStructureτ τ = record { isCompChangeStructure = isCompChangeStructureτ τ }

instance
  ichangeStructureτ : ∀ {τ} → ChangeStructure ⟦ τ ⟧Type
  ichangeStructureτ {τ} = changeStructureτ τ

[ σ ⇒ τ ]τ df from f1 to f2 =
  ∀ (da : Chτ σ) (a1 a2 : ⟦ σ ⟧Type) →
  [ σ ]τ da from a1 to a2 → [ τ ]τ df a1 da from f1 a1 to f2 a2
[ unit ]τ tt from tt to tt = ⊤
[ int ]τ dv from v1 to v2 = v1 + dv ≡ v2
[ pair σ τ ]τ (da , db) from (a1 , b1) to (a2 , b2) = [ σ ]τ da from a1 to a2 × [ τ ]τ db from b1 to b2
[ sum σ τ ]τ dv from v1 to v2 = sch_from_to_ dv v1 v2

isCompChangeStructureτ (σ ⇒ τ) = ChangeStructure.isCompChangeStructure (funCS {{changeStructureτ σ}} {{changeStructureτ τ}})
isCompChangeStructureτ unit = ChangeStructure.isCompChangeStructure unitCS
isCompChangeStructureτ int = ChangeStructure.isCompChangeStructure intCS
isCompChangeStructureτ (pair σ τ) = ChangeStructure.isCompChangeStructure (pairCS {{changeStructureτ σ}} {{changeStructureτ τ}})
isCompChangeStructureτ (sum σ τ) = ChangeStructure.isCompChangeStructure (sumCS {{changeStructureτ σ}} {{changeStructureτ τ}})

open import Data.Unit
-- We can define an alternative semantics for contexts, that defines environments as nested products:
⟦_⟧Context-prod : Context → Set
⟦ ∅ ⟧Context-prod = ⊤
⟦ τ • Γ ⟧Context-prod = ⟦ τ ⟧Type × ⟦ Γ ⟧Context-prod

-- And define a change structure for such environments, reusing the change
-- structure constructor for pairs. However, this change structure does not
-- duplicate base values in the environment. We probably *could* define a
-- different change structure for pairs that gives the right result.
changeStructureΓ-old : ∀ Γ → ChangeStructure ⟦ Γ ⟧Context-prod
changeStructureΓ-old ∅ = unitCS
changeStructureΓ-old (τ • Γ) = pairCS {{changeStructureτ τ}}  {{changeStructureΓ-old Γ}}

data [_]Γ_from_to_ : ∀ Γ → ChΓ Γ → (ρ1 ρ2 : ⟦ Γ ⟧Context) → Set where
  v∅ : [ ∅ ]Γ ∅ from ∅ to ∅
  _v•_ : ∀ {τ Γ dv v1 v2 dρ ρ1 ρ2} →
    (dvv : [ τ ]τ dv from v1 to v2) →
    (dρρ : [ Γ ]Γ dρ from ρ1 to ρ2) →
    [ τ • Γ ]Γ (dv • v1 • dρ) from (v1 • ρ1) to (v2 • ρ2)

module _ where
  _e⊕_ : ∀ {Γ} → ⟦ Γ ⟧Context → ChΓ Γ → ⟦ Γ ⟧Context
  _e⊕_ ∅ ∅ = ∅
  _e⊕_ (v • ρ) (dv • _ • dρ) = v ⊕ dv • ρ e⊕ dρ
  _e⊝_ : ∀ {Γ} → ⟦ Γ ⟧Context → ⟦ Γ ⟧Context → ChΓ Γ
  _e⊝_ ∅ ∅ = ∅
  _e⊝_ (v₂ • ρ₂) (v₁ • ρ₁) = v₂ ⊝ v₁ • v₁ • ρ₂ e⊝ ρ₁

  isEnvCompCS : ∀ Γ → IsCompChangeStructure ⟦ Γ ⟧Context (ChΓ Γ) [ Γ ]Γ_from_to_

  efromto→⊕ : ∀ {Γ} (dρ : ChΓ Γ) (ρ1 ρ2 : ⟦ Γ ⟧Context) →
      [ Γ ]Γ dρ from ρ1 to ρ2 → (ρ1 e⊕ dρ) ≡ ρ2
  efromto→⊕ .∅ .∅ .∅ v∅ = refl
  efromto→⊕ .(_ • _ • _) .(_ • _) .(_ • _) (dvv v• dρρ) =
    cong₂ _•_ (fromto→⊕ _ _ _ dvv) (efromto→⊕ _ _ _ dρρ)

  e⊝-fromto : ∀ {Γ} → (ρ1 ρ2 : ⟦ Γ ⟧Context) → [ Γ ]Γ ρ2 e⊝ ρ1 from ρ1 to ρ2
  e⊝-fromto ∅ ∅ = v∅
  e⊝-fromto (v1 • ρ1) (v2 • ρ2) = ⊝-fromto v1 v2 v• e⊝-fromto ρ1 ρ2

  _e⊚_ : ∀ {Γ} → ChΓ Γ → ChΓ Γ → ChΓ Γ
  _e⊚_ {∅} ∅ ∅ = ∅
  _e⊚_ {τ • Γ} (dv1 • v1 • dρ1) (dv2 • _ • dρ2) = dv1 ⊚[ ⟦ τ ⟧Type ] dv2 • v1 • dρ1 e⊚ dρ2

  e⊚-fromto : ∀ Γ → (ρ1 ρ2 ρ3 : ⟦ Γ ⟧Context) (dρ1 dρ2 : ChΓ Γ) →
    [ Γ ]Γ dρ1 from ρ1 to ρ2 →
    [ Γ ]Γ dρ2 from ρ2 to ρ3 → [ Γ ]Γ (dρ1 e⊚ dρ2) from ρ1 to ρ3
  e⊚-fromto ∅ ∅ ∅ ∅ ∅ ∅ v∅ v∅ = v∅
  e⊚-fromto (τ • Γ) (v1 • ρ1) (v2 • ρ2) (v3 • ρ3)
    (dv1 • (.v1 • dρ1)) (dv2 • (.v2 • dρ2))
    (dvv1 v• dρρ1) (dvv2 v• dρρ2) =
        ⊚-fromto v1 v2 v3 dv1 dv2 dvv1 dvv2
      v•
        e⊚-fromto Γ ρ1 ρ2 ρ3 dρ1 dρ2 dρρ1 dρρ2

  isEnvCompCS Γ = record
    { isChangeStructure = record
      { _⊕_ = _e⊕_
      ; fromto→⊕ = efromto→⊕
      ; _⊝_ = _e⊝_
      ; ⊝-fromto = e⊝-fromto
      }
    ; _⊚_ = _e⊚_
    ; ⊚-fromto = e⊚-fromto Γ
    }

changeStructureΓ : ∀ Γ → ChangeStructure ⟦ Γ ⟧Context
changeStructureΓ Γ = record { isCompChangeStructure = isEnvCompCS Γ }

instance
  ichangeStructureΓ : ∀ {Γ} → ChangeStructure ⟦ Γ ⟧Context
  ichangeStructureΓ {Γ} = changeStructureΓ Γ

changeStructureΓτ : ∀ Γ τ → ChangeStructure (⟦ Γ ⟧Context → ⟦ τ ⟧Type)
changeStructureΓτ Γ τ = funCS

instance
  ichangeStructureΓτ : ∀ {Γ τ} → ChangeStructure (⟦ Γ ⟧Context → ⟦ τ ⟧Type)
  ichangeStructureΓτ {Γ} {τ} = changeStructureΓτ Γ τ

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

module Data.PolyP.Universe where

open import Prelude hiding (_⟨_⟩_)
open import Data.Vec.Iterated
open import Data.Fin.Indexed

--------------------------------------------------------------------------------
--
--  The Universe of functors we're interested in.
--
--------------------------------------------------------------------------------
data Functor (n : ℕ) : Type where
  !     : Fin n → Functor n
  _⊕_   : (F G : Functor n) → Functor n
  _⊗_   : (F G : Functor n) → Functor n
  μ⟨_⟩  : Functor (suc n) → Functor n
  ⓪     : Functor n
  ①     : Functor n

infixl 6 _⊕_
infixl 7 _⊗_

Params : ℕ → Type₁
Params = Vec Type

variable
  n m k : ℕ
  F G : Functor n
  As Bs : Params n

---------------------------------------------------------------------------------
--
-- Interpretation
--
---------------------------------------------------------------------------------

mutual
  ⟦_⟧ : Functor n → Params n → Type
  ⟦ ! i     ⟧ xs = xs [ i ]
  ⟦ F ⊕  G  ⟧ xs = ⟦ F ⟧ xs ⊎  ⟦ G ⟧ xs
  ⟦ F ⊗  G  ⟧ xs = ⟦ F ⟧ xs ×  ⟦ G ⟧ xs
  ⟦ μ⟨ F ⟩  ⟧ xs = μ F xs
  ⟦ ⓪       ⟧ xs = ⊥
  ⟦ ①       ⟧ xs = ⊤

  record μ (F : Functor (suc n)) (As : Params n) : Type where
    pattern; inductive; constructor ⟨_⟩
    field unwrap : ⟦ F ⟧ (μ F As ∷ As)
open μ public

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------------
-- The alternating bit protocol (ABP) is correct
------------------------------------------------------------------------------

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

-- This module proves the correctness of the ABP by simplifing the
-- formalization in Dybjer and Sander (1989) using a stronger (maybe
-- invalid) co-induction principle.

module FOT.FOTC.Program.ABP.StrongerInductionPrinciple.CorrectnessProofI where

open import FOT.FOTC.Relation.Binary.Bisimilarity.Type
open import FOT.FOTC.Program.ABP.StrongerInductionPrinciple.LemmaI

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Stream.Type
open import FOTC.Data.Stream.Equality.PropertiesI
open import FOTC.Program.ABP.ABP hiding ( B )
open import FOTC.Program.ABP.Fair.Type
open import FOTC.Program.ABP.Terms
open import FOTC.Relation.Binary.Bisimilarity.Type

------------------------------------------------------------------------------
-- Main theorem.
abpCorrect : ∀ {b is os₁ os₂} → Bit b → Stream is → Fair os₁ → Fair os₂ →
             is ≈ abpTransfer b os₁ os₂ is
abpCorrect {b} {is} {os₁} {os₂} Bb Sis Fos₁ Fos₂ = ≈-stronger-coind B h refl
  where
  B : D → D → Set
  B xs ys = xs ≡ xs

  h : B is (abpTransfer b os₁ os₂ is) →
      ∃[ i' ] ∃[ is' ] ∃[ js' ]
        is ≡ i' ∷ is' ∧ abpTransfer b os₁ os₂ is ≡ i' ∷ js' ∧ B is' js'
  h _ with Stream-out Sis
  ... | i' , is' , prf₁ , Sis' with lemma Bb Fos₁ Fos₂ prf₂
    where
    aux₁ aux₂ aux₃ aux₄ aux₅ : D
    aux₁ = send b
    aux₂ = ack b
    aux₃ = out b
    aux₄ = corrupt os₁
    aux₅ = corrupt os₂

    prf₂ : S b (i' ∷ is') os₁ os₂
            (has aux₁ aux₂ aux₃ aux₄ aux₅ (i' ∷ is'))
            (hbs aux₁ aux₂ aux₃ aux₄ aux₅ (i' ∷ is'))
            (hcs aux₁ aux₂ aux₃ aux₄ aux₅ (i' ∷ is'))
            (hds aux₁ aux₂ aux₃ aux₄ aux₅ (i' ∷ is'))
            (abpTransfer b os₁ os₂ (i' ∷ is'))
    prf₂ = has-eq aux₁ aux₂ aux₃ aux₄ aux₅ (i' ∷ is')
           , hbs-eq aux₁ aux₂ aux₃ aux₄ aux₅ (i' ∷ is')
           , hcs-eq aux₁ aux₂ aux₃ aux₄ aux₅ (i' ∷ is')
           , hds-eq aux₁ aux₂ aux₃ aux₄ aux₅ (i' ∷ is')
           , trans (abpTransfer-eq b os₁ os₂ (i' ∷ is'))
               (transfer-eq aux₁ aux₂ aux₃ aux₄ aux₅ (i' ∷ is'))

  ... | js' , prf₃ = i'
                     , is'
                     , js'
                     , prf₁
                     , subst (λ t → abpTransfer b os₁ os₂ t ≡ i' ∷ js' )
                             (sym prf₁)
                             prf₃
                     , refl

------------------------------------------------------------------------------
-- abpTransfer produces a Stream.
abpTransfer-Stream : ∀ {b is os₁ os₂} →
                     Bit b →
                     Stream is →
                     Fair os₁ →
                     Fair os₂ →
                     Stream (abpTransfer b os₁ os₂ is)
abpTransfer-Stream Bb Sis Fos₁ Fos₂ = ≈→Stream₂ (abpCorrect Bb Sis Fos₁ Fos₂)

------------------------------------------------------------------------------
-- References
--
-- Dybjer, Peter and Sander, Herbert P. (1989). A Functional
-- Programming Approach to the Specification and Verification of
-- Concurrent Systems. Formal Aspects of Computing 1, pp. 303–319.


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Instances.Rings where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

open import Cubical.Algebra.Ring

open import Cubical.Categories.Category

open Category
open RingHoms

RingsCategory : ∀ {ℓ} → Category (ℓ-suc ℓ) ℓ
ob RingsCategory       = Ring _
Hom[_,_] RingsCategory = RingHom
id RingsCategory {R}   = idRingHom R
_⋆_ RingsCategory      = compRingHom
⋆IdL RingsCategory     = compIdRingHom
⋆IdR RingsCategory     = idCompRingHom
⋆Assoc RingsCategory   = compAssocRingHom
isSetHom RingsCategory = isSetRingHom _ _

max_stars_repo_name: FernandoLarrain/cubical


text:
-- Algorithmic equality.

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

module Definition.Conversion where

open import Definition.Untyped
open import Definition.Typed

open import Tools.Nat
open import Tools.Product
import Tools.PropositionalEquality as PE

infix 10 _⊢_~_↑_
infix 10 _⊢_~_↓_
infix 10 _⊢_[conv↑]_
infix 10 _⊢_[conv↓]_
infix 10 _⊢_[conv↑]_∷_
infix 10 _⊢_[conv↓]_∷_

mutual
  -- Neutral equality.
  data _⊢_~_↑_ (Γ : Con Term) : (k l A : Term) → Set where
    var-refl      : ∀ {x y A}
                  → Γ ⊢ var x ∷ A
                  → x PE.≡ y
                  → Γ ⊢ var x ~ var y ↑ A
    app-cong      : ∀ {k l t v F G}
                  → Γ ⊢ k ~ l ↓ Π F ▹ G
                  → Γ ⊢ t [conv↑] v ∷ F
                  → Γ ⊢ k ∘ t ~ l ∘ v ↑ G [ t ]
    fst-cong      : ∀ {p r F G}
                  → Γ ⊢ p ~ r ↓ Σ F ▹ G
                  → Γ ⊢ fst p ~ fst r ↑ F
    snd-cong      : ∀ {p r F G}
                  → Γ ⊢ p ~ r ↓ Σ F ▹ G
                  → Γ ⊢ snd p ~ snd r ↑ G [ fst p ]
    natrec-cong   : ∀ {k l h g a₀ b₀ F G}
                  → Γ ∙ ℕ ⊢ F [conv↑] G
                  → Γ ⊢ a₀ [conv↑] b₀ ∷ F [ zero ]
                  → Γ ⊢ h [conv↑] g ∷ Π ℕ ▹ (F ▹▹ F [ suc (var 0) ]↑)
                  → Γ ⊢ k ~ l ↓ ℕ
                  → Γ ⊢ natrec F a₀ h k ~ natrec G b₀ g l ↑ F [ k ]
    Emptyrec-cong : ∀ {k l F G}
                  → Γ ⊢ F [conv↑] G
                  → Γ ⊢ k ~ l ↓ Empty
                  → Γ ⊢ Emptyrec F k ~ Emptyrec G l ↑ F

  -- Neutral equality with types in WHNF.
  record _⊢_~_↓_ (Γ : Con Term) (k l B : Term) : Set where
    inductive
    constructor [~]
    field
      A     : Term
      D     : Γ ⊢ A ⇒* B
      whnfB : Whnf B
      k~l   : Γ ⊢ k ~ l ↑ A

  -- Type equality.
  record _⊢_[conv↑]_ (Γ : Con Term) (A B : Term) : Set where
    inductive
    constructor [↑]
    field
      A′ B′  : Term
      D      : Γ ⊢ A ⇒* A′
      D′     : Γ ⊢ B ⇒* B′
      whnfA′ : Whnf A′
      whnfB′ : Whnf B′
      A′<>B′ : Γ ⊢ A′ [conv↓] B′

  -- Type equality with types in WHNF.
  data _⊢_[conv↓]_ (Γ : Con Term) : (A B : Term) → Set where
    U-refl     : ⊢ Γ → Γ ⊢ U [conv↓] U
    ℕ-refl     : ⊢ Γ → Γ ⊢ ℕ [conv↓] ℕ
    Empty-refl : ⊢ Γ → Γ ⊢ Empty [conv↓] Empty
    Unit-refl  : ⊢ Γ → Γ ⊢ Unit [conv↓] Unit
    ne         : ∀ {K L}
               → Γ ⊢ K ~ L ↓ U
               → Γ ⊢ K [conv↓] L
    Π-cong     : ∀ {F G H E}
               → Γ ⊢ F
               → Γ ⊢ F [conv↑] H
               → Γ ∙ F ⊢ G [conv↑] E
               → Γ ⊢ Π F ▹ G [conv↓] Π H ▹ E
    Σ-cong     : ∀ {F G H E}
               → Γ ⊢ F
               → Γ ⊢ F [conv↑] H
               → Γ ∙ F ⊢ G [conv↑] E
               → Γ ⊢ Σ F ▹ G [conv↓] Σ H ▹ E

  -- Term equality.
  record _⊢_[conv↑]_∷_ (Γ : Con Term) (t u A : Term) : Set where
    inductive
    constructor [↑]ₜ
    field
      B t′ u′ : Term
      D       : Γ ⊢ A ⇒* B
      d       : Γ ⊢ t ⇒* t′ ∷ B
      d′      : Γ ⊢ u ⇒* u′ ∷ B
      whnfB   : Whnf B
      whnft′  : Whnf t′
      whnfu′  : Whnf u′
      t<>u    : Γ ⊢ t′ [conv↓] u′ ∷ B

  -- Term equality with types and terms in WHNF.
  data _⊢_[conv↓]_∷_ (Γ : Con Term) : (t u A : Term) → Set where
    ℕ-ins     : ∀ {k l}
              → Γ ⊢ k ~ l ↓ ℕ
              → Γ ⊢ k [conv↓] l ∷ ℕ
    Empty-ins : ∀ {k l}
              → Γ ⊢ k ~ l ↓ Empty
              → Γ ⊢ k [conv↓] l ∷ Empty
    Unit-ins  : ∀ {k l}
              → Γ ⊢ k ~ l ↓ Unit
              → Γ ⊢ k [conv↓] l ∷ Unit
    ne-ins    : ∀ {k l M N}
              → Γ ⊢ k ∷ N
              → Γ ⊢ l ∷ N
              → Neutral N
              → Γ ⊢ k ~ l ↓ M
              → Γ ⊢ k [conv↓] l ∷ N
    univ      : ∀ {A B}
              → Γ ⊢ A ∷ U
              → Γ ⊢ B ∷ U
              → Γ ⊢ A [conv↓] B
              → Γ ⊢ A [conv↓] B ∷ U
    zero-refl : ⊢ Γ → Γ ⊢ zero [conv↓] zero ∷ ℕ
    suc-cong  : ∀ {m n}
              → Γ ⊢ m [conv↑] n ∷ ℕ
              → Γ ⊢ suc m [conv↓] suc n ∷ ℕ
    η-eq      : ∀ {f g F G}
              → Γ ⊢ f ∷ Π F ▹ G
              → Γ ⊢ g ∷ Π F ▹ G
              → Function f
              → Function g
              → Γ ∙ F ⊢ wk1 f ∘ var 0 [conv↑] wk1 g ∘ var 0 ∷ G
              → Γ ⊢ f [conv↓] g ∷ Π F ▹ G
    Σ-η       : ∀ {p r F G}
              → Γ ⊢ p ∷ Σ F ▹ G
              → Γ ⊢ r ∷ Σ F ▹ G
              → Product p
              → Product r
              → Γ ⊢ fst p [conv↑] fst r ∷ F
              → Γ ⊢ snd p [conv↑] snd r ∷ G [ fst p ]
              → Γ ⊢ p [conv↓] r ∷ Σ F ▹ G
    η-unit    : ∀ {k l}
              → Γ ⊢ k ∷ Unit
              → Γ ⊢ l ∷ Unit
              → Whnf k
              → Whnf l
              → Γ ⊢ k [conv↓] l ∷ Unit

star-refl : ∀ {Γ} → ⊢ Γ → Γ ⊢ star [conv↓] star ∷ Unit
star-refl ⊢Γ = η-unit (starⱼ ⊢Γ) (starⱼ ⊢Γ) starₙ starₙ


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

open import HoTT
open import cohomology.Theory

{- Ordinary cohomology groups of the n-torus Tⁿ = (S¹)ⁿ.
 - We have Cᵏ(Tⁿ) == C⁰(S⁰)^(n choose' k) where _choose'_ defined as below.
 - This argument could give Cᵏ((Sᵐ)ⁿ) with a little more work. -}

module cohomology.Torus {i} (OT : OrdinaryTheory i) where

open OrdinaryTheory OT
open import cohomology.Sn OT
open import cohomology.SphereProduct cohomology-theory
open import cohomology.Unit cohomology-theory

{- Almost n choose k, but with n choose' O = 0 for any n. -}
_choose'_ : ℕ → ℤ → ℕ
n choose' negsucc _ = 0
n choose' pos O = 0
n choose' pos (S O) = n
O choose' pos (S (S k)) = 0
S n choose' pos (S (S k)) = (n choose' (pos (S (S k)))) + (n choose' (pos (S k)))

_-⊙Torus : ℕ → Ptd i
O -⊙Torus = ⊙Lift ⊙Unit
(S n) -⊙Torus = ⊙Lift {j = i} ⊙S¹ ⊙× (n -⊙Torus)

C-nTorus : (k : ℤ) (n : ℕ)
  → C k (n -⊙Torus) == C 0 (⊙Lift ⊙S⁰) ^ᴳ (n choose' k)

C-nTorus (negsucc k) O = C-Unit (negsucc k)

C-nTorus (negsucc k) (S n) =
  C-Sphere× (negsucc k) 1 (n -⊙Torus)
  ∙ ap (λ K → K ×ᴳ (C (negsucc k) (n -⊙Torus)
                    ×ᴳ C (negsucc k) (⊙Susp^ 1 (n -⊙Torus))))
       (C-Sphere-≠ (negsucc k) 1 (ℤ-negsucc≠pos _ _))
  ∙ ×ᴳ-unit-l {G = C (negsucc k) (n -⊙Torus)
                   ×ᴳ C (negsucc k) (⊙Susp (n -⊙Torus))}
  ∙ ap (λ K → K ×ᴳ C (negsucc k) (⊙Susp (n -⊙Torus)))
       (C-nTorus (negsucc k) n)
  ∙ ×ᴳ-unit-l {G = C (negsucc k) (⊙Susp (n -⊙Torus))}
  ∙ group-ua (C-Susp (negsucc (S k)) (n -⊙Torus))
  ∙ C-nTorus (negsucc (S k)) n

C-nTorus (pos O) O = C-Unit (pos O)

C-nTorus (pos O) (S n) =
  C-Sphere× (pos O) 1 (n -⊙Torus)
  ∙ ap (λ K → K ×ᴳ (C 0 (n -⊙Torus) ×ᴳ C 0 (⊙Susp (n -⊙Torus))))
       (C-Sphere-≠ (pos O) 1 (pos-≠ (ℕ-O≠S _)))
  ∙ ×ᴳ-unit-l {G = C 0 (n -⊙Torus) ×ᴳ C 0 (⊙Susp (n -⊙Torus))}
  ∙ ap (λ K → K ×ᴳ C 0 (⊙Susp (n -⊙Torus)))
       (C-nTorus 0 n)
  ∙ ×ᴳ-unit-l {G = C 0 (⊙Susp (n -⊙Torus))}
  ∙ group-ua (C-Susp (negsucc O) (n -⊙Torus))
  ∙ C-nTorus (negsucc O) n

C-nTorus (pos (S O)) O = C-Unit 1

C-nTorus (pos (S O)) (S n) =
  C-Sphere× 1 1 (n -⊙Torus)
  ∙ ap (λ K → K ×ᴳ (C 1 (n -⊙Torus)
                    ×ᴳ C 1 (⊙Susp (n -⊙Torus))))
       (C-Sphere-diag 1)
  ∙ ap (λ K → C 0 (⊙Lift ⊙S⁰) ×ᴳ K)
       (ap2 _×ᴳ_
         (C-nTorus 1 n)
         (group-ua (C-Susp 0 (n -⊙Torus)) ∙ C-nTorus 0 n)
        ∙ ×ᴳ-unit-r {G = C 0 (⊙Lift ⊙S⁰) ^ᴳ (n choose' 1)})

C-nTorus (pos (S (S k))) O =
  C-Unit (pos (S (S k)))

C-nTorus (pos (S (S k))) (S n) =
  C-Sphere× (pos (S (S k))) 1 (n -⊙Torus)
  ∙ ap (λ K → K ×ᴳ (C (pos (S (S k))) (n -⊙Torus)
                    ×ᴳ C (pos (S (S k))) (⊙Susp (n -⊙Torus))))
       (C-Sphere-≠ (pos (S (S k))) 1 (pos-≠ (ℕ-S-≠ (ℕ-S≠O k))))
  ∙ ×ᴳ-unit-l {G = (C (pos (S (S k))) (n -⊙Torus))
                   ×ᴳ (C (pos (S (S k))) (⊙Susp (n -⊙Torus)))}
  ∙ ap2 _×ᴳ_ (C-nTorus (pos (S (S k))) n)
             (group-ua (C-Susp (pos (S k)) (n -⊙Torus)) ∙ C-nTorus (pos (S k)) n)
  ∙ ^ᴳ-sum (C 0 (⊙Lift ⊙S⁰)) (n choose' pos (S (S k))) (n choose' pos (S k))

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module Languages.ILL.TypeCheck where

open import bool
open import maybe

open import Languages.ILL.TypeSyntax
open import Languages.ILL.Syntax
open import Utils.HaskellTypes
open import Utils.HaskellFunctions
open import Utils.Exception

data StateT (s : Set) (m : Set → Set) (a : Set) : Set where
  stateT : (s → m (Prod a s)) → StateT s m a

runStateT : ∀{s m a} → StateT s m a → (s → m (Prod a s))
runStateT (stateT f) = f

returnSTE : ∀{s A} → A → StateT s (Either Exception) A
returnSTE x = stateT (λ y → right (x , y))

infixl 20 _>>=STE_
_>>=STE_ : ∀{s A B} → StateT s (Either Exception) A → (A → StateT s (Either Exception) B) → StateT s (Either Exception) B
(stateT st) >>=STE f = stateT (λ y → st y >>=E (λ p → runStateT (f (fst p)) (snd p)))

infixl 20 _>>STE_
_>>STE_ : ∀{s A B} → StateT s (Either Exception) A → StateT s (Either Exception) B → StateT s (Either Exception) B
c₁ >>STE c₂ = c₁ >>=STE (λ _ → c₂)

throw : ∀{s A} → Exception → StateT s (Either Exception) A
throw x = stateT (λ _ → error x)

lift : ∀{s A} → Either Exception A → StateT s (Either Exception) A
lift (Left x) = stateT (λ _ → error x)
lift (Right x) = stateT (λ y → right (x , y))

get : ∀{S} → StateT S (Either Exception) S
get = stateT (λ x → right (x , x))

put : ∀{S} → S → StateT S (Either Exception) Unit
put s = stateT (λ x → Right (triv , s))

CTXEl : Set
CTXEl = Prod String Type

CTX : Set
CTX = List CTXEl

CTXV-eq : CTXEl → CTXEl → 𝔹
CTXV-eq (x , ty) (y , ty') = x str-eq y

TC : Set → Set
TC = StateT CTX (Either Exception)

_isDisjointWith_ : CTX → CTX → TC Unit
ctx₁ isDisjointWith ctx₂ with disjoint CTXV-eq ctx₁ ctx₂
... | tt = returnSTE triv
... | ff = throw TypeErrorDuplicatedFreeVar

getTypeCTX : String → CTX → maybe Type
getTypeCTX x ctx = lookup _str-eq_ x ctx

{-# TERMINATING #-}
subctxFV : CTX → Term → Either Exception CTX
subctxFV ctx Triv = right []
subctxFV ctx t@(FVar x) with getTypeCTX x ctx
... | just ty = right ((x , ty) :: [])
... | nothing = error VarNotInCtx
subctxFV ctx (BVar _ _ _) = right []
subctxFV ctx (Let t₁ _ _ t₂) =
  (subctxFV ctx t₁) >>=E
    (λ l₁ → (subctxFV ctx t₂) >>=E
       λ l₂ → right (l₁ ++ l₂))
subctxFV ctx (Lam _ _ t) = subctxFV ctx t
subctxFV ctx (App t₁ t₂) =
  (subctxFV ctx t₁) >>=E
    (λ l₁ → (subctxFV ctx t₂) >>=E
       λ l₂ → right (l₁ ++ l₂))
subctxFV ctx (Tensor t₁ t₂) =
  (subctxFV ctx t₁) >>=E
    (λ l₁ → (subctxFV ctx t₂) >>=E
       λ l₂ → right (l₁ ++ l₂))
subctxFV ctx (Promote ms t) =
  mctx₁ >>=E
    (λ ctx₁ → (subctxFV ctx t) >>=E
      (λ ctx₂ → right (ctx₁ ++ ctx₂)))
 where
  aux = (λ m r →
    (subctxFV ctx (fstT m)) >>=E
      (λ l₁ → r >>=E
        (λ l₂ → right (l₁ ++ l₂))))
  mctx₁ = foldr aux (right []) ms
subctxFV ctx (Discard t₁ t₂) =
  (subctxFV ctx t₁) >>=E
    (λ l₁ → (subctxFV ctx t₂) >>=E
       λ l₂ → right (l₁ ++ l₂))
subctxFV ctx (Copy t₁ _ t₂) =
  (subctxFV ctx t₁) >>=E
    (λ l₁ → (subctxFV ctx t₂) >>=E
       λ l₂ → right (l₁ ++ l₂))
subctxFV ctx (Derelict t) = subctxFV ctx t

isTop : Type → TC Type
isTop Top = returnSTE Top
isTop _ = throw TypeErrorLetNotTop

isTensor : Type → TC (Prod Type Type)
isTensor (Tensor x y) = returnSTE (x , y)
isTensor _ = throw TypeErrorLetNotTensor

isBang : Type → TC Type
isBang (Bang ty) = returnSTE ty
isBang _ = throw TypeErrorPromoteNotBang

isImp : Type → TC (Prod Type Type)
isImp (Imp A B) = returnSTE (A , B)
isImp _ = throw TypeErrorAppNotImp

_tyEq_ : Type → Type → TC Unit
_tyEq_ ty₁ ty₂ with ty₁ eq-type ty₂
... | tt = returnSTE triv
... | ff = throw TypeErrorTypesNotEqual

{-# TERMINATING #-}
typeCheck' : Term → TC Type
typeCheck' Triv = get >>=STE checkCTX
 where
   checkCTX : CTX → TC Type
   checkCTX [] = returnSTE Top
   checkCTX _ = throw NonEmptyCtx
typeCheck' (FVar x) = get >>=STE checkCtx
 where
   checkCtx : CTX → TC Type
   checkCtx ((y , ty) :: []) with x str-eq y
   ... | tt = returnSTE ty
   ... | ff = throw VarNotInCtx
   checkCtx _ = throw NonLinearCtx
typeCheck' (BVar _ _ _) = throw NonlocallyClosed
typeCheck' (Let t₁ ty PTriv t₂) =
 get >>=STE
   (λ ctx → lift (subctxFV ctx t₁) >>=STE
     (λ ctx₁ → lift (subctxFV ctx t₂) >>=STE
       λ ctx₂ → (ctx₁ isDisjointWith ctx₂) >>STE
         ((put ctx₁) >>STE typeCheck' t₁) >>=STE
           (λ ty₁ → isTop ty₁ >>STE
             (put ctx₂ >>STE typeCheck' t₂))))
typeCheck' (Let t₁ ty (PTensor x y) t₂) =
  get >>=STE
    (λ ctx → lift (subctxFV ctx t₁) >>=STE
     (λ ctx₁ → lift (subctxFV ctx t₂) >>=STE
      (λ ctx₂ → (ctx₁ isDisjointWith ctx₂) >>STE
        ((put ctx₁) >>STE
          typeCheck' t₁) >>=STE
            (λ ty₁ → (isTensor ty₁) >>=STE
              (λ tys → let A = fst tys
                           B = snd tys
                           t₂' = open-t 0 y RLPV (FVar y) (open-t 0 x LLPV (FVar x) t₂)
                        in put ((x , A) :: (y , B) :: ctx₂) >>STE typeCheck' t₂')))))
typeCheck' (Lam x ty t) =
  get >>=STE
    (λ ctx → (put ((x , ty) :: ctx)) >>STE
      typeCheck' (open-t 0 x BV (FVar x) t) >>=STE
        (λ ty₂ → returnSTE (Imp ty ty₂)))
typeCheck' (App t₁ t₂) =
  get >>=STE
    (λ ctx → lift (subctxFV ctx t₁) >>=STE
      (λ ctx₁ → lift (subctxFV ctx t₂) >>=STE
        (λ ctx₂ → (ctx₁ isDisjointWith ctx₂) >>STE
          (put ctx₁) >>STE (typeCheck' t₁) >>=STE
            (λ ty₁ → isImp ty₁ >>=STE
              (λ tys → (put ctx₂) >>STE (typeCheck' t₂) >>=STE
                (λ ty₂ → ((fst tys) tyEq ty₂) >>STE returnSTE (snd tys)))))))
typeCheck' (Tensor t₁ t₂) =
  get >>=STE
    (λ ctx → lift (subctxFV ctx t₁) >>=STE
      (λ ctx₁ → lift (subctxFV ctx t₂) >>=STE
        (λ ctx₂ → (ctx₁ isDisjointWith ctx₂) >>STE
          (put ctx₁) >>STE typeCheck' t₁ >>=STE
            (λ ty₁ → (put ctx₂) >>STE typeCheck' t₂ >>=STE
              (λ ty₂ → returnSTE (Tensor ty₁ ty₂))))))
typeCheck' (Promote ms t) =
  put [] >>STE getSubctxs ms
         >>=STE areDisjointCtxs
         >>STE checkVectorOpenTerm ms t
         >>=STE typeCheck'
         >>=STE (λ ty → returnSTE (Bang ty))
 where
   getSubctxs : List (Triple Term String Type) → TC (List CTX)
   getSubctxs ((triple t _ _) :: rest) =
     get >>=STE
       (λ ctx → (lift (subctxFV ctx t)) >>=STE
         (λ ctx' → (getSubctxs rest) >>=STE
           (λ r → returnSTE (ctx' :: r))))
   getSubctxs l = returnSTE []

   areDisjointCtxs : List CTX → TC Unit
   areDisjointCtxs [] = returnSTE triv
   areDisjointCtxs (ctx₁ :: rest) = aux ctx₁ rest >>STE areDisjointCtxs rest
     where
       aux : CTX → List CTX → TC Unit
       aux ctx₁ (ctx₂ :: rest) = (ctx₁ isDisjointWith ctx₂) >>STE aux ctx₁ rest
       aux _ [] = returnSTE triv

   checkVectorTerm : Term → TC Type
   checkVectorTerm t =
     get >>=STE
       (λ ctx → lift (subctxFV ctx t) >>=STE
         (λ ctx₁ → (put ctx₁) >>STE
           typeCheck' t))

   checkVectorOpenTerm : List (Triple Term String Type) → Term → TC Term
   checkVectorOpenTerm [] t = throw IllformedPromote
   checkVectorOpenTerm (triple t₁ x₁ ty₁ :: rest) t =
     get >>=STE
       (λ ctx → checkVectorTerm t₁ >>=STE
         (λ ty₁' → (isBang ty₁' >>STE (ty₁ tyEq ty₁')) >>STE
           (put ((x₁ , ty₁) :: ctx) >>STE
             ((checkVectorOpenTerm rest t) >>=STE
               (λ t' → returnSTE (open-t 0 x₁ PBV (FVar x₁) t'))))))
typeCheck' (Discard t₁ t₂) = get >>=STE
   (λ ctx → lift (subctxFV ctx t₁) >>=STE
     (λ ctx₁ → lift (subctxFV ctx t₂) >>=STE
       (λ ctx₂ → (ctx₁ isDisjointWith ctx₂) >>STE
         (put ctx₁) >>STE typeCheck' t₁
                    >>=STE isBang
                    >>STE (put ctx₂)
                    >>STE typeCheck' t₂)))
typeCheck' (Copy t₁ (x , y) t₂) =
  get >>=STE
       (λ ctx → lift (subctxFV ctx t₁) >>=STE
         (λ ctx₁ → lift (subctxFV ctx t₂) >>=STE
           (λ ctx₂ → (ctx₁ isDisjointWith ctx₂) >>STE
             (put ctx₁) >>STE typeCheck' t₁ >>=STE
               (λ ty₁ → isBang ty₁ >>STE
                 (put ((x , ty₁) :: (y , ty₁) :: ctx₂) >>STE typeCheck' t₂')))))
 where
   t₂' = open-t 0 y RCPV (FVar y) (open-t 0 x LCPV (FVar x) t₂)
typeCheck' (Derelict t) = typeCheck' t >>=STE isBang

typeCheck : Term → Either Exception Type
typeCheck t with runStateT (typeCheck' t) []
... | Left e = Left e
... | Right (ty , _) = right ty

max_stars_repo_name: heades/Agda-LLS

max_issues_repo_name: heades/Agda-LLS

max_forks_repo_name: heades/Agda-LLS


text:
module Examples.Resolution where

open import Prelude
open import Implicits.Syntax
open import Implicits.Syntax.Type.Constructors
open import Implicits.WellTyped
open import Implicits.Substitutions
open import Extensions.ListFirst
open Rules

unit = 0

-- simple implicit resolution by implication
module ex₁ where
  r : Type zero
  r = ∀' (tp-weaken tnat ⇒ (TVar zero))

  -- proof that the above type is a rule
  r-isrule : IsRule r
  r-isrule = ∀'-rule (rule (tp-weaken tnat) (TVar zero))

  -- the context used
  K = tnat ∷K nil

-- partial implicit resolution
-- as described by Oliveira et al
module ex₂ where
  r : Type zero
  r = (tnat ⇒ TC unit ⇒ TC unit)

  -- proof that the above type is a rule
  r-isrule : IsRule r
  r-isrule = rule tnat (TC unit ⇒ TC unit)

  K : Ktx 0 1
  K = TC unit ∷K nil

-- higher order resolution
module ex₃ where
  r : Type zero
  r = ∀' ((TC unit ⇒ TVar zero) ⇒ (TVar zero ×' TVar zero))

  r' : Type zero
  r' = (TC unit ⇒ tnat) ⇒ (tnat ×' tnat)

  r-isrule : IsRule r
  r-isrule = ∀'-rule (rule (TC unit ⇒ TVar zero) (TVar zero ×' TVar zero))

  r'-isrule : IsRule r'
  r'-isrule = rule (TC unit ⇒ tnat) (tnat ×' tnat)

  K : Ktx 0 1
  K = (TC unit ⇒ tnat) ∷K nil