text:
module Prelude.Applicative where

open import Agda.Primitive
open import Prelude.Unit
open import Prelude.Functor
open import Prelude.Function
open import Prelude.Equality
open import Prelude.Number
open import Prelude.Semiring
open import Prelude.Fractional

open import Prelude.Applicative.Indexed {I = ⊤} as Indexed

Applicative : ∀ {a b} (F : Set a → Set b) → Set (lsuc a ⊔ b)
Applicative F = Indexed.IApplicative (λ _ _ → F)

Applicative′ : ∀ {a b} (F : ∀ {a} → Set a → Set a) → Set (lsuc (a ⊔ b))
Applicative′ {a} {b} F = Indexed.IApplicative′ {a = a} {b = b} (λ _ _ → F)

open Indexed public hiding (IApplicative; IApplicative′)

fmapApplicative : ∀ {a b} {F : Set a → Set b} →
                    (∀ {A} → A → F A) → (∀ {A B} → F (A → B) → F A → F B) →
                    ∀ {A B} → (A → B) → F A → F B
fmapApplicative pure _<*>_ f m = pure f <*> m

module _ {a b} {F : Set a → Set b} {{AppF : Applicative F}} where

  defaultApplicativeNumber : {A : Set a} {{NumA : Number A}} -- levels get in the way of having constraints
                             {{_ : NoNumConstraint NumA}} →
                             Number (F A)
  Number.Constraint defaultApplicativeNumber n = ⊤′
  fromNat {{defaultApplicativeNumber}} n = pure (fromNat n)

  defaultApplicativeNegative : {A : Set a} {{NegA : Negative A}} -- levels get in the way of having constraints
                             {{_ : NoNegConstraint NegA}} →
                             Negative (F A)
  Negative.Constraint defaultApplicativeNegative _ = ⊤′
  fromNeg {{defaultApplicativeNegative}} n = pure (fromNeg n)

  defaultApplicativeSemiring : {A : Set a} {{_ : Semiring A}} → Semiring (F A)
  zro {{defaultApplicativeSemiring}} = pure zro
  one {{defaultApplicativeSemiring}} = pure one
  _+_ {{defaultApplicativeSemiring}} x y = _+_ <$> x <*> y
  _*_ {{defaultApplicativeSemiring}} x y = _*_ <$> x <*> y

  defaultApplicativeSubtractive : {A : Set a} {{_ : Subtractive A}} → Subtractive (F A)
  _-_    {{defaultApplicativeSubtractive}} x y = _-_ <$> x <*> y
  negate {{defaultApplicativeSubtractive}} x   = negate <$> x

  defaultApplicativeFractional : {A : Set a} {{FracA : Fractional A}}  -- only if no constraints
                                 {{_ : Fractional.NoConstraint FracA}} →
                                 Fractional (F A)
  Fractional.Constraint defaultApplicativeFractional _ _ = ⊤′
  Fractional._/_ defaultApplicativeFractional x y = (λ x y → x / y) <$> x <*> y

-- Congruence for _<*>_ and friends

module _ {a b} {A B : Set a} {F : Set a → Set b} {{_ : Applicative F}} where

  infixl 4 _=*=_
  _=*=_ : {f g : F (A → B)} {x y : F A} → f ≡ g → x ≡ y → (f <*> x) ≡ (g <*> y)
  refl =*= refl = refl

  _=*_ : {a₁ a₂ : F A} {b₁ b₂ : F B} → a₁ ≡ a₂ → b₁ ≡ b₂ → (a₁ <* b₁) ≡ (a₂ <* b₂)
  refl =* refl = refl

  _*=_ : {a₁ a₂ : F A} {b₁ b₂ : F B} → a₁ ≡ a₂ → b₁ ≡ b₂ → (a₁ *> b₁) ≡ (a₂ *> b₂)
  refl *= refl = refl

module _ {F  : ∀ {a}   → Set a → Set a}
         {{_ : ∀ {a b} → Applicative′ {a} {b} F}}
         {{_ : ∀ {a}   → Applicative {a} F}}
         {a b} {A : Set a} {B : Set b} where

  infixl 4 _=*=′_
  _=*=′_ : {f g : F (A → B)} {x y : F A} → f ≡ g → x ≡ y → (f <*>′ x) ≡ (g <*>′ y)
  refl =*=′ refl = refl

  _=*′_ : {a₁ a₂ : F A} {b₁ b₂ : F B} → a₁ ≡ a₂ → b₁ ≡ b₂ → (a₁ <*′ b₁) ≡ (a₂ <*′ b₂)
  refl =*′ refl = refl

  _*=′_ : {a₁ a₂ : F A} {b₁ b₂ : F B} → a₁ ≡ a₂ → b₁ ≡ b₂ → (a₁ *>′ b₁) ≡ (a₂ *>′ b₂)
  refl *=′ refl = refl


text:
module Issue308b where

data D : Set where
  d : D → D

syntax d x = e x x

g : D → D
g (d x) = e x

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Level
open import Data.Product
open import Relation.Binary using (Setoid; _Preserves₂_⟶_⟶_)
open import Algebra.Structures
module CommAssocLemmas (A : Set) (_≈_ : A -> A -> Set) (_+_ : A -> A -> A) (zer : A)
         (isCommMon : IsCommutativeMonoid _≈_ _+_ zer) where

  SA : Setoid _ _
  SA = record {Carrier = A; _≈_ = _≈_; isEquivalence = IsCommutativeMonoid.isEquivalence isCommMon}

  --  open Relation.Binary.Setoid SA
  open import Algebra.FunctionProperties public
  open IsCommutativeMonoid isCommMon public renaming (∙-cong to _<+>_)

  open import Relation.Binary.EqReasoning SA
  lemmaCommAssoc00 : ∀ a b c d ->  (a + ((b + c) + (d + zer))) ≈ ((a + c) + (b + d))
  lemmaCommAssoc00 a b c d =
    begin
      (a     + ((b + c)    + (d + zer)))
    ≈⟨ refl <+> (refl     <+> proj₂ identity d) ⟩
      (a     + ((b + c)    + d))
    ≈⟨ refl <+> (comm b c <+> refl) ⟩
      (a     + ((c + b)    + d))
    ≈⟨ refl <+> assoc c b d ⟩
      (a     + (c + (b + d)))
    ≈⟨ sym (assoc a c (b + d)) ⟩
      ((a + c) + (b + d))
    ∎

--  lemmaCommAssoc00 : ∀ a b c d ->  (a + ((b + c) + d)) ≈ ((a + c) + (b + d))

  lemmaCommAssoc01 : ∀ {a} {b} {c} {d} {e} -> (a + ((b + c)  + (d + e))) ≈ (((a + c) + d) + (b + e))
  lemmaCommAssoc01 {a} {b} {c} {d} {e} =
    begin
      (a     +  ((b + c)  + (d + e)))
    ≈⟨ refl <+> assoc b c (d + e) ⟩
      (a     +  (b     + (c + (d + e))))
    ≈⟨ refl <+> (refl <+> sym (assoc c d e)) ⟩
      (a     +  (b     + ((c + d) + e)))
    ≈⟨ refl <+> (sym (assoc b (c + d) e)) ⟩
      (a     +  ((b + (c + d))   +  e))
    ≈⟨ refl <+> (comm b (c + d) <+> refl) ⟩
      (a     +  (((c + d) + b) + e))
    ≈⟨ refl <+> (assoc (c + d) b e) ⟩
      (a     +  ((c + d) + (b + e)))
    ≈⟨ sym (assoc a (c + d) (b + e))⟩
      ((a + (c + d)) + (b + e))
    ≈⟨ sym (assoc a c d) <+> refl ⟩
      (((a + c) + d) + (b + e))
    ∎

{-
  lemmaCommAssoc11 : ∀ a b c d ->  (a + (b + (c + d))) ≈ ((a + c) + (b + d))
  lemmaCommAssoc11 a b c d =
    begin
      (a     + (b + (c    + d)))
    ≈⟨ refl <+> (sym (assoc b c d)) ⟩
      (a     + ((b + c)    + d))
    ≈⟨ lemmaCommAssoc00 a b c d ⟩
      ((a + c) + (b + d))
    ∎
-}

--  open Lemmas public

max_stars_repo_name: DSLsofMath/ValiantAgda

max_issues_repo_name: DSLsofMath/ValiantAgda

max_forks_repo_name: DSLsofMath/ValiantAgda


text:
module Human.Bool where

data Bool : Set where
  false true : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN FALSE false #-}
{-# BUILTIN TRUE  true  #-}

{-# COMPILE JS Bool  = function (x,v) { return ((x) ? v["true"]() : v["false"]()); } #-}
{-# COMPILE JS false = false #-}
{-# COMPILE JS true  = true  #-}

max_stars_repo_name: MaisaMilena/JuiceMaker

max_issues_repo_name: MaisaMilena/JuiceMaker

max_forks_repo_name: MaisaMilena/JuiceMaker


text:
{-# OPTIONS --overlapping-instances #-}

module Succeed.RecursiveInstanceSearchLevel where

open import Common.Prelude
open import Common.Product
open import Common.Equality

-- Definition of truncation levels. We wrap the definition into a datatype in
-- order to be able to use instance search.
data has-level (n : Nat) (A : Set) : Set
has-level' : (n : Nat) (A : Set) → Set

data has-level n A where
  c : has-level' n A → has-level n A

has-level' zero A = Σ A (λ a → (b : A) → a ≡ b)
has-level' (suc n) A = (a b : A) → has-level n (a ≡ b)

-- This one should not be declared as eligible by instance search or else we
-- will get unsolvable loops
postulate
  higher-level : {n : Nat} {A : Set} {{_ : has-level n A}} → has-level (suc n) A

postulate
  Trunc : Nat → Set → Set

instance
  =-level : {n : Nat} {A : Set} {{_ : has-level (suc n) A}} {a b : A} → has-level n (a ≡ b)
  =-level {{c f}} = f _ _

  postulate
    =-level-same : {n : Nat} {A : Set} {{_ : has-level n A}} {a b : A} → has-level n (a ≡ b)

  postulate
    Nat-level : has-level 2 Nat
    Π-level : {n : Nat} {A : Set} {B : A → Set} {{_ : (a : A) → has-level n (B a)}} → has-level n ((a : A) → B a)
    Πimp-level : {n : Nat} {A : Set} {B : A → Set} {{_ : (a : A) → has-level n (B a)}} → has-level n ({a : A} → B a)
    Σ-level : {n : Nat} {A : Set} {B : A → Set} {{_ : has-level n A}} {{_ : (a : A) → has-level n (B a)}} → has-level n (Σ A B)
    Trunc-level : {n : Nat} {A : Set} → has-level n (Trunc n A)

-- Used to check, using instance search, if some type has a given level
postulate
  check-level : (n : Nat) (A : Set) {{_ : has-level n A}} → Set

test₁ : (A : Set) → Set
test₁ A = check-level 1 ((a b : Trunc 2 A) → (a , (b , 3)) ≡ (b , (a , 4)))

test₂ : (A : Set) → Set
test₂ A = check-level 2 ((a b : Trunc 2 A) → (a , (b , 3)) ≡ (b , (a , 4)))

-- -- To be fixed
-- test₃ : {n : Nat} {A : Set} {B : A → Set} {_ : {a : A} → has-level n (B a)} → Nat → has-level n ((a : A) → B a)
-- test₃ r = Π-level ⟨⟩

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by bounded join semilattices
------------------------------------------------------------------------

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

open import Relation.Binary.Lattice

module Relation.Binary.Properties.BoundedJoinSemilattice
  {c ℓ₁ ℓ₂} (J : BoundedJoinSemilattice c ℓ₁ ℓ₂) where

open BoundedJoinSemilattice J

import Algebra.FunctionProperties as P; open P _≈_
open import Data.Product
open import Function using (_∘_; flip)
open import Relation.Binary
open import Relation.Binary.Properties.Poset poset

-- Bottom is an identity of the meet operation.

identityˡ : LeftIdentity ⊥ _∨_
identityˡ x =
  let _ , x≤⊥∨x , least = supremum ⊥ x
  in antisym (least x (minimum x) refl) x≤⊥∨x

identityʳ : RightIdentity ⊥ _∨_
identityʳ x =
  let x≤x∨⊥ , _ , least = supremum x ⊥
  in antisym (least x refl (minimum x)) x≤x∨⊥

identity : Identity ⊥ _∨_
identity = identityˡ , identityʳ

-- The dual construction is a bounded meet semilattice.

dualIsBoundedMeetSemilattice : IsBoundedMeetSemilattice _≈_ (flip _≤_) _∨_ ⊥
dualIsBoundedMeetSemilattice = record
  { isMeetSemilattice = record
    { isPartialOrder  = invIsPartialOrder
    ; infimum         = supremum
    }
  ; maximum           = minimum
  }

dualBoundedMeetSemilattice : BoundedMeetSemilattice c ℓ₁ ℓ₂
dualBoundedMeetSemilattice = record
  { ⊤                        = ⊥
  ; isBoundedMeetSemilattice = dualIsBoundedMeetSemilattice
  }


text:
-- Andrea(s), 2016-07-06, issue #2076 reported by Andrea
-- This is to test printing of extended lambdas

-- {-# OPTIONS -v tc.cc:60 -v tc.term.exlam:100 -v reify.clause:60 #-}

postulate
  A : Set
  _,_ : A → A → A

data Unit : Set where
  true : Unit

bar : (p : A) (q : A) → Unit → A
bar p q = aux
  where
  aux : Unit → A
  aux true = p , q

foo : (p : A) (q : A) → Unit → A
foo p q = \ { true → p , q}

test : (a : A) → Unit → A
test a = foo a a
-- Normalize me! Expected:
-- λ a → λ { true → a , a }

-- From test/interaction/ExtendedLambdaCase.agda

data Bool : Set where
  true false : Bool

data Void : Set where

module M {A : Set}(B : A → Set) where
  postulate
    Bar : (Bool → Bool) → Set

Test : Set
Test = (y : Bool) → M.Bar {Bool} (λ _ → Void) (λ { true → true ; false → false })
-- Normalize me! Expected:
-- (y : Bool) → M.Bar (λ _ → Void) (λ { true → true ; false → false })

-- .extendedlambda1 y true  = true
-- .extendedlambda1 y false = false
-- dropped args:  []
-- hidden  args:  []
-- visible args:  [y]

-- Extended lambda inside parameterized module

module PM (X : Set) where
  extlam : (p : A) (q : A) → Unit → A
  extlam p q = \ { true -> p , q}

-- ConcreteDef extended lambda's implementation ".extendedlambda1" has type:
-- Unit → A
-- dropped args:  [X]
-- hidden  args:  []
-- visible args:  [p, q]

-- clauses before compilation .extendedlambda1 p₁ q₁ true = p₁ , q₁

  -- , clauseTel =
  --   ExtendTel r(El {_getSort = Type (Max [ClosedLevel 1]), unEl = Sort (Type (Max []))}) (Abs "X"
  --   ExtendTel r(El {_getSort = Type (Max []), unEl = Def Issue2076.A []}) (Abs "p"
  --   ExtendTel r(El {_getSort = Type (Max []), unEl = Def Issue2076.A []}) (Abs "q"
  --   EmptyTel)))
  -- , namedClausePats =
  --   [r(X = VarP (DBPatVar {dbPatVarName = "X", dbPatVarIndex = 2}))
  --   ,r(p = VarP (DBPatVar {dbPatVarName = "p", dbPatVarIndex = 1}))
  --   ,r(q = VarP (DBPatVar {dbPatVarName = "q", dbPatVarIndex = 0}))
  --   ,r(x = ConP Issue2076.Unit.true(inductive)[] (ConPatternInfo {conPRecord = Nothing, conPType = Just r(El {_getSort = Type (Max []), unEl = Def Issue2076.Unit []})}) [])
  --   ]
  -- , clauseBody = Bind (Abs "h0" Bind (Abs "h1" Bind (Abs "h2" Body (Def Issue2076._,_ [Apply r(Var 1 []),Apply r(Var 0 [])]))))

-- clauses before compilation
--   , clauseTel =
--     ExtendTel r(El {_getSort = Type (Max [ClosedLevel 1]), unEl = Sort (Type (Max []))}) (Abs "X"
--     ExtendTel r(El {_getSort = Type (Max []), unEl = Def Issue2076.A []}) (Abs "p"
--     ExtendTel r(El {_getSort = Type (Max []), unEl = Def Issue2076.A []}) (Abs "q"
--     EmptyTel)))

--   , namedClausePats =
--     [r(X = VarP (DBPatVar {dbPatVarName = "X", dbPatVarIndex = 2}))
--     ,r(p = VarP (DBPatVar {dbPatVarName = "p", dbPatVarIndex = 1}))
--     ,r(q = VarP (DBPatVar {dbPatVarName = "q", dbPatVarIndex = 0}))]

--   , clauseBody = Bind (Abs "h0" Bind (Abs "h1" Bind (Abs "h2"
--       Body (Def Issue2076.PM..extendedlambda1
--         [Apply r(Var 2 []),Apply r(Var 1 []),Apply r(Var 0 [])]))))

  -- wrong printing
  -- clauses before compilation extlam p q = λ { q₁ true → p₁ , q₁ }

  inside : (a : A) → Unit → A
  inside a = extlam a a

  bla : (a : A) → {!!}
  bla a = {!inside a!}
  -- Normalization of `inside a` here should yield
  -- λ { true → a , a }

ptest : (a : A) → Unit → A
ptest a = PM.extlam Unit a a
-- ptest should normalize to λ a → λ { true → a , a }

module MM (Y : Set) where
  open PM Y public

-- Normalizing MM.extlam should yield
-- λ Y p q → λ { true → p , q }

open MM Unit

opentest : (a : A) → Unit → A
opentest a = extlam a a
-- opentest should normalize to λ a → λ { true → a , a }

module Parent (Y : Set) where
  module Child (X : Set) where
    extlam2 : (p : A) (q : A) → Unit → A
    extlam2 p q = \ { true -> p , q}

-- Normalizing Parent.Child.extlam2 should yield
-- λ Y X p q → λ { true → p , q }

open import Agda.Builtin.Nat

data Vec (A : Set) : Nat → Set where
  [] : Vec A 0
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

postulate
  h : (∀ {n} → Vec Nat n → Nat) → Nat

f : Nat → Nat
f n = h λ where []       → 0
                (x ∷ xs) → n

-- Normalising f should yield
-- λ n → h (λ { [] → 0 ; (x ∷ xs) → n })

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- Lemmas related to application of substitutions
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Substitution.Data.Application.Application22
  {i u e} {Uni : IndexedUniverse i u e}
  where

import deBruijn.Context; open deBruijn.Context Uni
open import deBruijn.Substitution.Data.Application.Application21
open import deBruijn.Substitution.Data.Application.Application222
open import deBruijn.Substitution.Data.Basics
open import deBruijn.Substitution.Data.Simple
open import Level using (_⊔_)

-- Lemmas related to application.
--
-- In order to lessen the performance problems which—at the time of
-- writing—plague Agda this module has been split into two,
-- Application221 and Application222.

record Application₂₂
  {t₁} {T₁ : Term-like t₁}
  {t₂} {T₂ : Term-like t₂}

  -- Simple substitutions for the first kind of terms.
  (simple₁ : Simple T₁)

  -- Simple substitutions for the second kind of terms.
  (simple₂ : Simple T₂)

  -- A translation from the first to the second kind of terms.
  (trans : [ T₁ ⟶⁼ T₂ ])
  : Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where

  open Term-like T₂ renaming (_⊢_ to _⊢₂_; _≅-⊢_ to _≅-⊢₂_)
  open Simple simple₁
    using () renaming (wk[_] to wk₁[_]; _↑⁺⋆_ to _↑⁺⋆₁_)
  open Simple simple₂
    using () renaming (var to var₂; weaken[_] to weaken₂[_])

  field
    application₂₁ : Application₂₁ simple₁ simple₂ trans

  open Application₂₁ application₂₁

  field
    -- Lifts equalities valid for all variables and liftings to
    -- arbitrary terms.
    var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆ :
      ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρs₁ : Subs T₁ ρ̂) (ρs₂ : Subs T₁ ρ̂) →
      (∀ Γ⁺ {σ} (x : Γ ++⁺ Γ⁺ ∋ σ) →
         var₂ · x /⊢⋆ ρs₁ ↑⁺⋆₁ Γ⁺ ≅-⊢₂ var₂ · x /⊢⋆ ρs₂ ↑⁺⋆₁ Γ⁺) →
      ∀ Γ⁺ {σ} (t : Γ ++⁺ Γ⁺ ⊢₂ σ) →
      t /⊢⋆ ρs₁ ↑⁺⋆₁ Γ⁺ ≅-⊢₂ t /⊢⋆ ρs₂ ↑⁺⋆₁ Γ⁺

    -- The wk substitution and the weaken function are equivalent.
    /⊢-wk : ∀ {Γ σ τ} (t : Γ ⊢₂ τ) →
            t /⊢ wk₁[ σ ] ≅-⊢₂ weaken₂[ σ ] · t

  open Application₂₂₂
    (record { application₂₂₁ = record
              { application₂₁         = application₂₁
              ; var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆ = var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆
              ; /⊢-wk                 = /⊢-wk
              }
            }) public
    hiding (application₂₁; var-/⊢⋆-↑⁺⋆-⇒-/⊢⋆-↑⁺⋆; /⊢-wk)

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax


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

test : lzero ≡ lsuc lzero
test = refl

-- WAS: Set != Set₁
-- SHOULD BE: lzero != lsuc lzero

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans)
open Eq.≡-Reasoning

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

lift : ∀ {m n : ℕ} → m ≡ n → suc m ≡ suc n
lift refl = refl

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
  begin
    (zero + n) + p
  ≡⟨⟩
    zero + (n + p)
  ∎
+-assoc (suc m) n p =
  begin
    (suc m + n) + p
  ≡⟨⟩
    suc ((m + n) + p)
  ≡⟨ lift (+-assoc m n p) ⟩
    suc (m + (n + p))
  ≡⟨⟩
    suc m + (n + p)
  ∎

+-identity : ∀ (m : ℕ) → m + zero ≡ m
+-identity zero =
  begin
    zero + zero
  ≡⟨⟩
    zero
  ∎
+-identity (suc m) =
  begin
    suc m + zero
  ≡⟨⟩
    suc (m + zero)
  ≡⟨ lift (+-identity m) ⟩
    suc m
  ∎

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc zero n =
  begin
    zero + suc n
  ≡⟨⟩
    suc n
  ≡⟨⟩
    suc (zero + n)
  ∎
+-suc (suc m) n =
  begin
    suc m + suc n
  ≡⟨⟩
    suc (m + suc n)
  ≡⟨ lift (+-suc m n) ⟩
    suc (suc (m + n))
  ≡⟨⟩
    suc (suc m + n)
  ∎

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
  begin
    m + zero
  ≡⟨ +-identity m ⟩
    m
  ≡⟨⟩
    zero + m
  ∎
+-comm m (suc n) =
  begin
    m + suc n
  ≡⟨ +-suc m n ⟩
    suc (m + n)
  ≡⟨ lift (+-comm m n) ⟩
    suc (n + m)
  ≡⟨⟩
    suc n + m
  ∎


text:
open import Agda.Primitive

record Relation {a b} (A : Set a) (B : Set b) c : Set (a ⊔ b ⊔ lsuc c) where
  constructor mk
  field
    _∼_ : A → B → Set c

record Setoid a c : Set (lsuc (a ⊔ c)) where
  constructor mk
  field
    carrier  : Set a
    relation : Relation carrier carrier c

  open Relation relation public renaming (_∼_ to _≈_)

record HeytingAlgebra {a c}
         (setoid : Setoid a c)
         (_∧_ _∨_ : let open Setoid setoid in
                    carrier → carrier → carrier) :
         Set (a ⊔ c) where
  constructor laws
  open Setoid setoid

  field
    ∧-cong : ∀ {x₁ x₂ y₁ y₂} → x₁ ≈ x₂ → y₁ ≈ y₂ → (x₁ ∧ y₁) ≈ (x₂ ∧ y₂)
    ∨-cong : ∀ {x₁ x₂ y₁ y₂} → x₁ ≈ x₂ → y₁ ≈ y₂ → (x₁ ∨ y₁) ≈ (x₂ ∨ y₂)

infix 0 _⇒_

record _⇒_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor mk
  field
    ⇒-fst : A → B

open _⇒_ public

infix 0 _⇔_
infixr 0 _,_

record _⇔_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    ⇔-fst : A ⇒ B
    ⇔-snd : B ⇒ A

open _⇔_ public

⇔-relation : ∀ {a b} → Relation (Set a) (Set b) (a ⊔ b)
⇔-relation = mk _⇔_

⇔-setoid : ∀ c → Setoid (lsuc c) c
⇔-setoid c = mk (Set c) ⇔-relation

infix 0 _∧_

record _∧_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    ∧-fst : A
    ∧-snd : B

open _∧_ public

infix 0 _∨_

data _∨_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  ∨-inl : A → (A ∨ B)
  ∨-inr : B → (A ∨ B)

heyting-algebra : ∀ {a} → HeytingAlgebra (⇔-setoid a) _∧_ (_∨_ {a})
heyting-algebra {a} = laws ∧-cong ∨-cong
  where
  open Setoid (⇔-setoid _) -- much faster if _ is replaced by a

  ∧-cong : ∀ {x₁ x₂ y₁ y₂} → x₁ ≈ x₂ → y₁ ≈ y₂ → (x₁ ∧ y₁) ≈ (x₂ ∧ y₂)
  ∧-cong x₁≈x₂ y₁≈y₂ =
    mk (λ x₁∧y₁ → ⇒-fst (⇔-fst x₁≈x₂) (∧-fst x₁∧y₁) , ⇒-fst (⇔-fst y₁≈y₂) (∧-snd x₁∧y₁)) ,
    mk (λ x₂∧y₂ → ⇒-fst (⇔-snd x₁≈x₂) (∧-fst x₂∧y₂) , ⇒-fst (⇔-snd y₁≈y₂) (∧-snd x₂∧y₂))

  ∨-cong : ∀ {x₁ x₂ y₁ y₂} → x₁ ≈ x₂ → y₁ ≈ y₂ → (x₁ ∨ y₁) ≈ (x₂ ∨ y₂)

  -- 1.1s
  ∨-cong {x₁} {x₂} {y₁} {y₂} x₁≈x₂ y₁≈y₂ =
    mk lemma₁ , mk lemma₂
    where
    lemma₁ : x₁ ∨ y₁ →  x₂ ∨ y₂
    lemma₁ (∨-inl x₁) = ∨-inl (⇒-fst (⇔-fst x₁≈x₂) x₁)
    lemma₁ (∨-inr y₁) = ∨-inr (⇒-fst (⇔-fst y₁≈y₂) y₁)
    lemma₂ : x₂ ∨ y₂ →  x₁ ∨ y₁
    lemma₂ (∨-inl x₂) = ∨-inl (⇒-fst (⇔-snd x₁≈x₂) x₂)
    lemma₂ (∨-inr y₂) = ∨-inr (⇒-fst (⇔-snd y₁≈y₂) y₂)

  -- -- 3.0s
  -- ∨-cong {x₁} {x₂} {y₁} {y₂} (x₁⇒x₂ , x₂⇒x₁) (y₁⇒y₂ , y₂⇒y₁) =
  --   mk lemma₁ , mk lemma₂
  --   where
  --   lemma₁ : x₁ ∨ y₁ →  x₂ ∨ y₂
  --   lemma₁ (∨-inl x₁) = ∨-inl (⇒-fst x₁⇒x₂ x₁)
  --   lemma₁ (∨-inr y₁) = ∨-inr (⇒-fst y₁⇒y₂ y₁)
  --   lemma₂ : x₂ ∨ y₂ →  x₁ ∨ y₁
  --   lemma₂ (∨-inl x₂) = ∨-inl (⇒-fst x₂⇒x₁ x₂)
  --   lemma₂ (∨-inr y₂) = ∨-inr (⇒-fst y₂⇒y₁ y₂)

  -- -- 0.4s
  -- ∨-cong {x₁} {x₂} {y₁} {y₂} (mk x₁→x₂ , mk x₂→x₁) (mk y₁→y₂ , mk y₂→y₁) =
  --   mk lemma₁ , mk lemma₂
  --   where
  --   lemma₁ : x₁ ∨ y₁ →  x₂ ∨ y₂
  --   lemma₁ (∨-inl x₁) = ∨-inl (x₁→x₂ x₁)
  --   lemma₁ (∨-inr y₁) = ∨-inr (y₁→y₂ y₁)
  --   lemma₂ : x₂ ∨ y₂ →  x₁ ∨ y₁
  --   lemma₂ (∨-inl x₂) = ∨-inl (x₂→x₁ x₂)
  --   lemma₂ (∨-inr y₂) = ∨-inr (y₂→y₁ y₂)


text:
-- Hilbert-style formalisation of closed syntax.
-- Nested terms.

module OldBasicILP.Syntax.ClosedHilbert where

open import OldBasicILP.Syntax.Common public

-- Types parametrised by closed derivations.

mutual
  infixr 10 _⦂_
  infixl 9 _∧_
  infixr 7 _▻_
  data Ty : Set where
    α_  : Atom → Ty
    _▻_ : Ty → Ty → Ty
    _⦂_ : ∀ {A} → Proof A → Ty → Ty
    _∧_ : Ty → Ty → Ty
    ⊤  : Ty

  -- Anti-bug wrappers.

  record Proof (A : Ty) : Set where
    inductive
    constructor [_]
    field
      der : ⊢ A

  -- Derivations.

  infix 3 ⊢_
  data ⊢_ : Ty → Set where
    app   : ∀ {A B}   → ⊢ A ▻ B → ⊢ A → ⊢ B
    ci    : ∀ {A}     → ⊢ A ▻ A
    ck    : ∀ {A B}   → ⊢ A ▻ B ▻ A
    cs    : ∀ {A B C} → ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C

    box   : ∀ {A}     → (d : ⊢ A)
                      → ⊢ [ d ] ⦂ A

    cdist : ∀ {A B}   → {d₁ : ⊢ A ▻ B} {d₂ : ⊢ A}
                      → ⊢ [ d₁ ] ⦂ (A ▻ B) ▻ [ d₂ ] ⦂ A ▻ [ app d₁ d₂ ] ⦂ B

    cup   : ∀ {A}     → {d : ⊢ A}
                      → ⊢ [ d ] ⦂ A ▻ [ box d ] ⦂ [ d ] ⦂ A

    cdown : ∀ {A}     → {d : ⊢ A}
                      → ⊢ [ d ] ⦂ A ▻ A

    cpair : ∀ {A B}   → ⊢ A ▻ B ▻ A ∧ B
    cfst  : ∀ {A B}   → ⊢ A ∧ B ▻ A
    csnd  : ∀ {A B}   → ⊢ A ∧ B ▻ B
    unit  : ⊢ ⊤

infix 3 ⊢⋆_
⊢⋆_ : Cx Ty → Set
⊢⋆ ∅     = 𝟙
⊢⋆ Ξ , A = ⊢⋆ Ξ × ⊢ A

-- Additional useful types.

infixr 7 _▻⋯▻_
_▻⋯▻_ : Cx Ty → Ty → Ty
∅       ▻⋯▻ B = B
(Ξ , A) ▻⋯▻ B = Ξ ▻⋯▻ (A ▻ B)

-- Cut and multicut.

cut : ∀ {A B} → ⊢ A → ⊢ A ▻ B → ⊢ B
cut d₁ d₂ = app d₂ d₁

multicut : ∀ {Ξ A} → ⊢⋆ Ξ → ⊢ Ξ ▻⋯▻ A → ⊢ A
multicut {∅}     ∙         d₂ = d₂
multicut {Ξ , B} (ds , d₁) d₂ = app (multicut ds d₂) d₁

-- Contraction.

ccont : ∀ {A B} → ⊢ (A ▻ A ▻ B) ▻ A ▻ B
ccont = app (app cs cs) (app ck ci)

cont : ∀ {A B} → ⊢ A ▻ A ▻ B → ⊢ A ▻ B
cont d = app ccont d

-- Exchange, or Schönfinkel’s C combinator.

cexch : ∀ {A B C} → ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C
cexch = app (app cs (app (app cs (app ck cs))
                         (app (app cs (app ck ck)) cs)))
            (app ck ck)

exch : ∀ {A B C} → ⊢ A ▻ B ▻ C → ⊢ B ▻ A ▻ C
exch d = app cexch d

-- Composition, or Schönfinkel’s B combinator.

ccomp : ∀ {A B C} → ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
ccomp = app (app cs (app ck cs)) ck

comp : ∀ {A B C} → ⊢ B ▻ C → ⊢ A ▻ B → ⊢ A ▻ C
comp d₁ d₂ = app (app ccomp d₁) d₂

-- Useful theorems in functional form.

dist : ∀ {A B r₁ r₂} → ⊢ [ r₁ ] ⦂ (A ▻ B) → ⊢ [ r₂ ] ⦂ A → ⊢ [ app r₁ r₂ ] ⦂ B
dist d₁ d₂ = app (app cdist d₁) d₂

up : ∀ {A r} → ⊢ [ r ] ⦂ A → ⊢ [ box r ] ⦂ [ r ] ⦂ A
up d = app cup d

down : ∀ {A r} → ⊢ [ r ] ⦂ A → ⊢ A
down d = app cdown d

distup : ∀ {A B} → {r₀ : ⊢ A} {r₁ : ⊢ [ r₀ ] ⦂ A ▻ B}
         → ⊢ [ r₁ ] ⦂ ([ r₀ ] ⦂ A ▻ B) → ⊢ [ r₀ ] ⦂ A → ⊢ [ app r₁ (box r₀) ] ⦂ B
distup d₁ d₂ = dist d₁ (up d₂)

pair : ∀ {A B} → ⊢ A → ⊢ B → ⊢ A ∧ B
pair d₁ d₂ = app (app cpair d₁) d₂

fst : ∀ {A B} → ⊢ A ∧ B → ⊢ A
fst d = app cfst d

snd : ∀ {A B} → ⊢ A ∧ B → ⊢ B
snd d = app csnd d

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Ints.BiInvInt.Properties where

open import Cubical.Core.Everything

open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Equiv.Properties
open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Prelude

open import Cubical.Data.Nat using (ℕ)
import Cubical.Data.Int as Int
open import Cubical.Data.Bool

open import Cubical.HITs.Ints.BiInvInt.Base

infixl 6 _+_ _-_
infixl 7 _·_

-- To prove a property P about BiInvInt, we need to show:
-- * P zero
-- * If P n, then P (suc n)
-- * If P n, then P (pred n)
BiInvInt-ind-prop :
  ∀ {ℓ} {P : BiInvInt → Type ℓ} → (∀ n → isProp (P n)) →
  P zero → (∀ n → P n → P (suc n)) → (∀ n → P n → P (pred n)) →
  (n : BiInvInt) → P n
BiInvInt-ind-prop {P = P} P-isProp P-zero P-suc P-pred = φ
  where
  P-predr : ∀ n → P n → P (predr n)
  P-predr n x = subst P (predl≡predr n) (P-pred n x)

  P-predl : ∀ n → P n → P (predl n)
  P-predl = P-pred

  P-isProp' : {a b : BiInvInt} (p : a ≡ b) (x : P a) (y : P b) → PathP (λ i → P (p i)) x y
  P-isProp' _ _ _ = toPathP (P-isProp _ _ _)

  φ : (n : BiInvInt) → P n
  φ zero = P-zero
  φ (suc n) = P-suc n (φ n)
  φ (predr n) = P-predr n (φ n)
  φ (suc-predr n i) = P-isProp' (suc-predr n) (P-suc (predr n) (P-predr n (φ n))) (φ n) i
  φ (predl n) = P-predl n (φ n)
  φ (predl-suc n i) = P-isProp' (predl-suc n) (P-predl (suc n) (P-suc n (φ n))) (φ n) i

-- To define a function BiInvInt → A, we need:
-- · a point z : A for zero
-- · an equivalence s : A ≃ A for suc/pred
BiInvInt-rec : ∀ {ℓ} {A : Type ℓ} → A → A ≃ A → BiInvInt → A
BiInvInt-rec {A = A} z e = φ
  where
  e-Iso : Iso A A
  e-Iso = equivToIso e

  φ : BiInvInt → A
  φ zero = z
  φ (suc n) = Iso.fun e-Iso (φ n)
  φ (predr n) = Iso.inv e-Iso (φ n)
  φ (suc-predr n i) = Iso.rightInv e-Iso (φ n) i
  φ (predl n) = Iso.inv e-Iso (φ n)
  φ (predl-suc n i) = Iso.leftInv e-Iso (φ n) i

sucIso : Iso BiInvInt BiInvInt
Iso.fun sucIso = suc
Iso.inv sucIso = pred
Iso.rightInv sucIso = suc-predl
Iso.leftInv sucIso = predl-suc

sucEquiv : BiInvInt ≃ BiInvInt
sucEquiv = isoToEquiv sucIso

-- addition

-- the following equalities hold definitionally:
--   zero   + n ≡ n
--   suc m  + n ≡ suc (m + n)
--   pred m + n ≡ pred (m + n)
_+_ : BiInvInt → BiInvInt → BiInvInt
_+_ = BiInvInt-rec (idfun BiInvInt) (postCompEquiv sucEquiv)

-- properties of addition

+-zero : ∀ n → n + zero ≡ n
+-zero = BiInvInt-ind-prop (λ _ → isSetBiInvInt _ _) refl (λ n p → cong suc p) (λ n p → cong pred p)

+-suc : ∀ m n → m + suc n ≡ suc (m + n)
+-suc = BiInvInt-ind-prop (λ _ → isPropΠ λ _ → isSetBiInvInt _ _)
  (λ m → refl)
  (λ m p n → cong suc (p n))
  (λ m p n → cong pred (p n) ∙ predl-suc (m + n) ∙ sym (suc-predl (m + n)))

+-pred : ∀ m n → m + pred n ≡ pred (m + n)
+-pred = BiInvInt-ind-prop (λ _ → isPropΠ λ _ → isSetBiInvInt _ _)
  (λ m → refl)
  (λ m p n → cong suc (p n) ∙ suc-predl (m + n) ∙ sym (predl-suc (m + n)))
  (λ m p n → cong pred (p n))

+-comm : ∀ m n → m + n ≡ n + m
+-comm m n = +-comm' n m
  where
  +-comm' : ∀ n m → m + n ≡ n + m
  +-comm' = BiInvInt-ind-prop (λ _ → isPropΠ λ _ → isSetBiInvInt _ _)
    +-zero
    (λ n p m → +-suc m n ∙ cong suc (p m))
    (λ n p m → +-pred m n ∙ cong pred (p m))

+-assoc : ∀ m n o → m + (n + o) ≡ (m + n) + o
+-assoc = BiInvInt-ind-prop (λ _ → isPropΠ2 λ _ _ → isSetBiInvInt _ _)
  (λ n o → refl)
  (λ m p n o → cong suc (p n o))
  (λ m p n o → cong pred (p n o))

-- negation / subtraction

-- the following equalities hold definitionally:
--   - zero     ≡ zero
--   - (suc m)  ≡ pred m
--   - (pred m) ≡ suc m
-_ : BiInvInt → BiInvInt
-_ = BiInvInt-rec zero (invEquiv sucEquiv)

_-_ : BiInvInt → BiInvInt → BiInvInt
m - n = m + (- n)

+-invˡ : ∀ n → (- n) + n ≡ zero
+-invˡ = BiInvInt-ind-prop (λ _ → isSetBiInvInt _ _)
  refl
  (λ n p → cong pred (+-suc (- n) n) ∙ predl-suc _ ∙ p)
  (λ n p → cong suc (+-pred (- n) n) ∙ suc-predl _ ∙ p)

+-invʳ : ∀ n → n + (- n) ≡ zero
+-invʳ = BiInvInt-ind-prop (λ _ → isSetBiInvInt _ _)
  refl
  (λ n p → cong suc (+-pred n (- n)) ∙ suc-predl _ ∙ p)
  (λ n p → cong pred (+-suc n (- n)) ∙ predl-suc _ ∙ p)

inv-hom : ∀ m n → - (m + n) ≡ (- m) + (- n)
inv-hom = BiInvInt-ind-prop (λ _ → isPropΠ λ _ → isSetBiInvInt _ _)
  (λ n → refl)
  (λ m p n → cong pred (p n))
  (λ m p n → cong suc (p n))

-- natural injections from ℕ

pos : ℕ → BiInvInt
pos ℕ.zero = zero
pos (ℕ.suc n) = suc (pos n)

neg : ℕ → BiInvInt
neg ℕ.zero = zero
neg (ℕ.suc n) = pred (neg n)

-- absolute value and sign
-- (Note that there doesn't appear to be any way around using
--  bwd here! Any direct proof ends up doing the same work...)

abs : BiInvInt → ℕ
abs n = Int.abs (bwd n)

sgn : BiInvInt → Bool
sgn n = Int.sgn (bwd n)

Iso-n+ : (n : BiInvInt) → Iso BiInvInt BiInvInt
Iso.fun (Iso-n+ n) = n +_
Iso.inv (Iso-n+ n) = - n +_
Iso.rightInv (Iso-n+ n) m = +-assoc n (- n) m ∙ cong (_+ m) (+-invʳ n)
Iso.leftInv (Iso-n+ n) m = +-assoc (- n) n m ∙ cong (_+ m) (+-invˡ n)

isEquiv-n+ : ∀ n → isEquiv (n +_)
isEquiv-n+ n = isoToIsEquiv (Iso-n+ n)

-- multiplication

-- the following equalities hold definitionally:
--   zero   · n ≡ zero
--   suc m  · n ≡ n + m · n
--   pred m · n ≡ (- n) + m · n
_·_ : BiInvInt → BiInvInt → BiInvInt
m · n = BiInvInt-rec zero (n +_ , isEquiv-n+ n) m

-- properties of multiplication

·-zero : ∀ n → n · zero ≡ zero
·-zero = BiInvInt-ind-prop (λ _ → isSetBiInvInt _ _) refl (λ n p → p) (λ n p → p)

·-suc : ∀ m n → m · suc n ≡ m + m · n
·-suc = BiInvInt-ind-prop (λ _ → isPropΠ λ _ → isSetBiInvInt _ _)
  (λ n → refl)
  (λ m p n → cong suc
    (cong (n +_) (p n) ∙ +-assoc n m (m · n) ∙
     cong (_+ m · n) (+-comm n m) ∙ sym (+-assoc m n (m · n))))
  (λ m p n → cong pred
    (cong (- n +_) (p n) ∙ +-assoc (- n) m (m · n) ∙
     cong (_+ m · n) (+-comm (- n) m) ∙ sym (+-assoc m (- n) (m · n))))

·-pred : ∀ m n → m · pred n ≡ (- m) + m · n
·-pred = BiInvInt-ind-prop (λ _ → isPropΠ λ _ → isSetBiInvInt _ _)
  (λ n → refl)
  (λ m p n → cong pred
    (cong (n +_) (p n) ∙ +-assoc n (- m) (m · n) ∙
     cong (_+ m · n) (+-comm n (- m)) ∙ sym (+-assoc (- m) n (m · n))))
  (λ m p n → cong suc
    (cong (- n +_) (p n) ∙ +-assoc (- n) (- m) (m · n) ∙
     cong (_+ m · n) (+-comm (- n) (- m)) ∙ sym (+-assoc (- m) (- n) (m · n))))

·-comm : ∀ m n → m · n ≡ n · m
·-comm = BiInvInt-ind-prop (λ _ → isPropΠ λ _ → isSetBiInvInt _ _)
  (λ n → sym (·-zero n))
  (λ m p n → cong (n +_) (p n) ∙ sym (·-suc n m))
  (λ m p n → cong (- n +_) (p n) ∙ sym (·-pred n m))

·-identityˡ : ∀ m → suc zero · m ≡ m
·-identityˡ = +-zero

·-identityʳ : ∀ m → m · suc zero ≡ m
·-identityʳ m = ·-comm m (suc zero) ∙ ·-identityˡ m

·-distribʳ : ∀ m n o → (m · o) + (n · o) ≡ (m + n) · o
·-distribʳ = BiInvInt-ind-prop (λ _ → isPropΠ2 λ _ _ → isSetBiInvInt _ _)
  (λ n o → refl)
  (λ m p n o → sym (+-assoc o (m · o) (n · o)) ∙ cong (o +_) (p n o))
  (λ m p n o → sym (+-assoc (- o) (m · o) (n · o)) ∙ cong (- o +_) (p n o))

·-distribˡ : ∀ o m n → (o · m) + (o · n) ≡ o · (m + n)
·-distribˡ o m n =
  cong (_+ o · n) (·-comm o m) ∙ cong (m · o +_) (·-comm o n) ∙
  ·-distribʳ m n o ∙ ·-comm (m + n) o

·-inv : ∀ m n → m · (- n) ≡ - (m · n)
·-inv = BiInvInt-ind-prop (λ _ → isPropΠ λ _ → isSetBiInvInt _ _)
  (λ n → refl)
  (λ m p n → cong (- n +_) (p n) ∙ sym (inv-hom n (m · n)))
  (λ m p n → cong (- (- n) +_) (p n) ∙ sym (inv-hom (- n) (m · n)))

inv-· : ∀ m n → (- m) · n ≡ - (m · n)
inv-· m n = ·-comm (- m) n ∙ ·-inv n m ∙ cong (-_) (·-comm n m)

·-assoc : ∀ m n o → m · (n · o) ≡ (m · n) · o
·-assoc = BiInvInt-ind-prop (λ _ → isPropΠ2 λ _ _ → isSetBiInvInt _ _)
  (λ n o → refl)
  (λ m p n o →
    cong (n · o +_) (p n o) ∙ ·-distribʳ n (m · n) o)
  (λ m p n o →
    cong (- (n · o) +_) (p n o) ∙ cong (_+ m · n · o) (sym (inv-· n o)) ∙
    ·-distribʳ (- n) (m · n) o)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Issue326 where

open import Common.Prelude

postulate
  QName : Set

{-# BUILTIN QNAME QName #-}

primitive primQNameEquality : QName → QName → Bool

main : IO Unit
main = printBool (primQNameEquality (quote Unit) (quote IO))


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

-- The Category of "Families of Sets"
open import Level
open import Relation.Binary using (Rel)
open import Data.Product
open import Relation.Binary.PropositionalEquality as ≡
open import Function renaming (id to idf; _∘_ to _⊚_)
import Relation.Binary.Reasoning.Setoid as SetoidR

open import Categories.Category

module _ {a b : Level} where
  record Fam : Set (suc a ⊔ suc b) where
      field
        U : Set a
        T : U → Set b
  open Fam

  record Hom (A B : Fam) : Set (a ⊔ b) where
    field
      f : U A → U B
      φ : (x : U A) → T A x → T B (f x)

  -- it is more convenient if we have g≡f than f≡g
  record _≡Fam_ {X Y} (f g : (Hom X Y)) : Set (a ⊔ b) where
    field
      g≡f : {x : U X} → Hom.f g x ≡ Hom.f f x
      φ≡γ : {x : U X} {bx : T X x} → Hom.φ f x bx ≡ subst (T Y) (g≡f {x}) (Hom.φ g x bx)

  module Eq = _≡Fam_

  Cat : Category (suc a ⊔ suc b) (a ⊔ b) (a ⊔ b)
  Cat = record
    { Obj       = Fam
    ; _⇒_       = Hom
    ; _≈_       = _≡Fam_
    ; id        = record { f = idf ; φ = λ _ → idf }
    ; _∘_       = λ H I → record { f = Hom.f H ⊚ Hom.f I ; φ = λ ua → Hom.φ H (Hom.f I ua) ⊚ Hom.φ I ua }
    ; assoc     = record { g≡f = refl ; φ≡γ = refl }
    ; sym-assoc = record { g≡f = refl ; φ≡γ = refl }
    ; identityˡ = record { g≡f = refl ; φ≡γ = refl }
    ; identityʳ = record { g≡f = refl ; φ≡γ = refl }
    ; identity² = record { g≡f = refl ; φ≡γ = refl }
    ; equiv     = λ {A} {B} → record
      { refl  = record { g≡f = refl ; φ≡γ = refl }
      ; sym   = λ {i} {j} i≡j → record
        { g≡f = sym (Eq.g≡f i≡j)
        ; φ≡γ = λ {x} {bx} →
          let open SetoidR (setoid (T B (Hom.f j x) )) in
          let eq = Eq.g≡f i≡j in begin
          Hom.φ j x bx                                          ≈⟨ sym (subst-sym-subst eq) ⟩
          subst (T B) (sym eq) (subst (T B) eq (Hom.φ j x bx))  ≈⟨ cong (subst (T B) (sym eq)) (sym (Eq.φ≡γ i≡j)) ⟩
          subst (T B) (sym eq) (Hom.φ i x bx) ∎
        }
      ; trans = λ {i} {j} {k} i≡j j≡k → record
        { g≡f = trans (Eq.g≡f j≡k) (Eq.g≡f i≡j)
        ; φ≡γ = λ {x} {bx} →
          let eq₁ = Eq.g≡f i≡j in
          let eq₂ = Eq.g≡f j≡k in
          let eq₃ = Eq.φ≡γ i≡j in
          let y = Hom.φ i x bx in
          let z = Hom.φ j x bx in
          let w = Hom.φ k x bx in
          let open SetoidR (setoid (T B (Hom.f i _))) in
          begin
          y                                   ≈⟨ eq₃ ⟩
          subst (T B) eq₁ z                   ≈⟨ cong (subst (T B) eq₁) (Eq.φ≡γ j≡k) ⟩
          subst (T B) eq₁ (subst (T B) eq₂ w) ≈⟨ subst-subst eq₂ ⟩
          subst (T B) ((trans eq₂ eq₁)) w  ∎
        }
      }
    ; ∘-resp-≈ = λ {A} {B} {C} {ff} {hh} {g} {i} f≡h g≡i → record
      { g≡f = λ {x} → trans (cong (Hom.f hh) (Eq.g≡f g≡i)) (Eq.g≡f f≡h)
      ; φ≡γ = λ {x} {bx} →
        let eq₁ = Eq.g≡f f≡h in
        let eq₂ = Eq.g≡f g≡i in
        let eq₃ = Eq.φ≡γ f≡h in
        let eq₄ = Eq.φ≡γ g≡i in
        let y = Hom.φ i x bx in
        let z = Hom.φ g x bx in
        let ix = Hom.f i x in
        let gx = Hom.f g x in
        let φgx = Hom.φ g x bx in
        let φhy = Hom.φ hh ix y in
        let ST₁ {z} x = subst (T C) (eq₁ {z}) x in
        let ST₂ {z} x = subst (T B) (eq₂ {z}) x in
        let open SetoidR (setoid (T C _)) in
        begin
        Hom.φ ff (Hom.f g x) z                            ≈⟨ eq₃ ⟩
        ST₁ (Hom.φ hh gx φgx)                             ≈⟨ cong (λ q → ST₁ (Hom.φ hh gx q)) eq₄ ⟩
        ST₁ (Hom.φ hh gx (ST₂ y))                          ≈⟨ cong ST₁ (subst-app (T B) (Hom.φ hh) eq₂) ⟩
        ST₁ (subst (T C) (cong (Hom.f hh) eq₂) φhy)        ≈⟨ subst-subst (cong (Hom.f hh) eq₂) ⟩
        subst (T C) (trans (cong (Hom.f hh) eq₂) eq₁) φhy  ∎

      }
    }
    where
      -- this is almost like subst-application from stdlib
      subst-app : ∀ {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
                    (B₁ : A₁ → Set b₁) {B₂ : A₂ → Set b₂}
                    {f : A₁ → A₂} {x₁ x₂ : A₁} {y : B₁ x₁}
                    (g : ∀ x → B₁ x → B₂ (f x)) (eq : x₁ ≡ x₂) →
                    g x₂ (subst B₁ eq y) ≡ subst B₂ (cong f eq) (g x₁ y)
      subst-app _ _ refl = refl

  open Category Cat public

FamilyOfSets : ∀ a b → Category (suc a ⊔ suc b) (a ⊔ b) (a ⊔ b)
FamilyOfSets a b = Cat {a} {b}

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
module Extensions.Substitution where

open import Prelude hiding (id)

open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
open import Data.Vec.Properties
open import Data.Vec
open import Function hiding (id)

module AdditionalLemmas {T} (lemmas : TermLemmas T) where

  open TermLemmas lemmas
  module Var = VarSubst

  -- Weakening commutes with single-variable substitution
  weaken-sub : ∀ {n} (a : T (1 + n)) (b : T n) →
                weaken (a / sub b) ≡ a / wk ↑ / sub (weaken b)
  weaken-sub a b = begin
    weaken (a / sub b)        ≡⟨ sym (/-wk′ (a / sub b)) ⟩
    a / sub b / wk            ≡⟨ sub-commutes a ⟩
    a / wk ↑ / sub (b / wk)   ≡⟨ cong (λ c → a / wk ↑ / sub c) (/-wk′ b) ⟩
    a / wk ↑ / sub (weaken b) ∎
    where /-wk′ : ∀ {n} (a : T n) → a / wk ≡ weaken a
          /-wk′ a = /-wk {t = a}

  -- Weakening commutes with reverse composition of substitutions.
  map-weaken-⊙ : ∀ {m n k} (σ₁ : Sub T m n) (σ₂ : Sub T n k) →
                  map weaken (σ₁ ⊙ σ₂) ≡ (map weaken σ₁) ⊙ (σ₂ ↑)
  map-weaken-⊙ σ₁ σ₂ = begin
    map weaken (σ₁ ⊙ σ₂)     ≡⟨ map-weaken ⟩
    (σ₁ ⊙ σ₂) ⊙ wk           ≡⟨ sym ⊙-assoc ⟩
    σ₁ ⊙ (σ₂ ⊙ wk)           ≡⟨ cong (λ σ₂ → σ₁ ⊙ σ₂) ⊙-wk ⟩
    σ₁ ⊙ (wk ⊙ (σ₂ ↑))       ≡⟨ ⊙-assoc ⟩
    (σ₁ ⊙ wk) ⊙ (σ₂ ↑)       ≡⟨ cong (λ σ₁ → σ₁ ⊙ (σ₂ ↑)) (sym map-weaken) ⟩
    (map weaken σ₁) ⊙ (σ₂ ↑) ∎

  weaken⋆↑ : ∀ {ν μ} (x : T ν) (s : Sub T ν μ) → (weaken x) / (s ↑) ≡ weaken (x / s)
  weaken⋆↑ x s = begin
    (weaken x) / (s ↑) ≡⟨ cong (λ u → u / (s ↑)) (sym /-wk) ⟩
    x / wk / (s ↑) ≡⟨ sym (/-⊙ x) ⟩
    x / (wk ⊙ (s ↑)) ≡⟨ cong (_/_ x) (sym ⊙-wk) ⟩
    x / (s ⊙ wk) ≡⟨ /-⊙ x ⟩
    x / s / wk ≡⟨ /-wk ⟩
    weaken (x / s) ∎

  weaken-sub-vanishes : ∀ {ν} {a b : T ν} → (weaken a) / (sub b) ≡ a
  weaken-sub-vanishes {ν} {a} {b} = begin
    (weaken a) / (sub b) ≡⟨ cong (flip _/_ (sub b)) (sym $ /-wk {t = a}) ⟩
    a / wk / (sub b) ≡⟨ wk-sub-vanishes a ⟩
    a ∎

  -- make /Var usable from lemmas
  open TermSubst termSubst using (_/Var_) public

  private
    var⋆weaken : ∀ {n} → _≗_ {A = Fin n} (var ∘ suc) (weaken ∘ var)
    var⋆weaken n = begin
      var (suc n) ≡⟨ sym $ lookup-wk n ⟩
      lookup n wk ≡⟨ sym $ var-/ ⟩
      (var n) / wk ≡⟨ /-wk ⟩
      weaken (var n) ∎

    map-var⋆weaken : ∀ {n m} {v : Vec (Fin n) m} → map var (map suc v) ≡ map weaken (map var v)
    map-var⋆weaken {v = v} = begin
      map var (map suc v) ≡⟨ sym $ map-∘ var suc v ⟩
      map (var ∘ suc) v ≡⟨ map-cong var⋆weaken v ⟩
      map (weaken ∘ var) v ≡⟨ map-∘ weaken var v ⟩
      map weaken (map var v) ∎

  map-var-varid≡id : ∀ {n} → map var (Var.id {n}) ≡ id {n}
  map-var-varid≡id {zero} = refl
  map-var-varid≡id {suc n} = begin
    var zero ∷ (map var $ map suc Var.id)
      ≡⟨ cong (_∷_ (var zero)) map-var⋆weaken ⟩
    var zero ∷ (map weaken $ map var Var.id)
      ≡⟨ cong (λ u → var zero ∷ (map weaken u)) map-var-varid≡id ⟩
    id ↑ ∎

  map-var-varwk≡wk : ∀ {n} → map var (Var.wk {n}) ≡ wk {n}
  map-var-varwk≡wk {zero} = refl
  map-var-varwk≡wk {suc n} = begin
    map var (map suc Var.id) ≡⟨ map-var⋆weaken ⟩
    map weaken (map var Var.id) ≡⟨ cong (map weaken) map-var-varid≡id ⟩
    wk ∎

  map-var-↑ : ∀ {n m} {s : Vec (Fin n) m} {s'} → map var s ≡ s' → map var (s Var.↑) ≡ s' ↑
  map-var-↑ {s = s} {s' = s'} eq = begin
    var zero ∷ (map var $ map suc s)
      ≡⟨ cong (_∷_ $ var zero) map-var⋆weaken ⟩
    var zero ∷ (map weaken $ map var s)
      ≡⟨ cong (λ u → var zero ∷ (map weaken u)) eq ⟩
    s' ↑ ∎

  a/wk↑/sub0≡a : ∀ {ν} (a : T (suc ν)) → a / wk ↑ / (sub $ var zero) ≡ a
  a/wk↑/sub0≡a a = begin
    a / wk ↑ / (sub $ var zero)
      ≡⟨ sym $ /-⊙ a ⟩
    a / (var zero / (sub $ var zero) ∷ map /-var-zero (map weaken wk))
      ≡⟨ cong (λ u → a / (u ∷ map /-var-zero (map weaken wk))) var-/ ⟩
    a / (var zero ∷ map /-var-zero (map weaken wk))
      ≡⟨ cong' (sym $ map-∘ /-var-zero weaken wk) ⟩
    a / (var zero ∷ map (λ t → (weaken t) / (sub $ var zero)) wk)
      ≡⟨ cong' (map-cong (λ t → weaken-sub-vanishes) wk) ⟩
    a / (var zero ∷ map Prelude.id wk)
      ≡⟨ cong' (map-id wk) ⟩
    a / ((var zero ∷ wk))
      ≡⟨ id-vanishes a ⟩
    a ∎
    where
      /-var-zero = (λ t → t / (sub $ var zero))
      cong' : ∀ {x y} → x ≡ y → a / (var zero ∷ x) ≡ a / (var zero ∷ y)
      cong' = λ rest → cong (λ u → a / (var zero ∷ u)) rest


text:
module Imports.Issue1913-I where

open import Imports.Issue1913-M

instance
  x : D
  x = d


text:
-- Andreas, 2022-03-10, issue #5823, reported by oisdk
-- It was possible to make the check for singleton records loop.
-- This has never worked (not a regression).

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

isProp : ∀{a} (A : Set a) → Set a
isProp A = ∀ (x y : A) → x ≡ y

cong : ∀{a b} {A : Set a} {B : Set b} (f : A → B) {x y : A} (eq : x ≡ y) → f x ≡ f y
cong f refl = refl

postulate
  funExt : ∀{a b}{A : Set a} {B : (x : A) → Set b} {f g : (x : A) → B x} → (∀ (x : A) → f x ≡ g x) → f ≡ g

record Acc {a} {A : Set a} {r} (R : A → A → Set r) (x : A) : Set (a ⊔ r) where
  inductive; eta-equality
  constructor acc
  field step : ∀ y → R y x → Acc R y
open Acc public

-- Naively testing Acc R x for being a singleton will infinitely unfold its definition.
-- We need to keep track of which record types we already unfolded!

isPropAcc : ∀ {a r} {A : Set a} {R : A → A → Set r} {x : A} → isProp (Acc R x)
isPropAcc (acc x) (acc y) = cong acc (funExt λ n → funExt λ p → isPropAcc (x n p) (y n p))

-- Agda used to loop when trying determine whether Acc is a singleton type.
-- Now it gives a termination error, as expected.


text:
{-# OPTIONS --postfix-projections #-}
module PresheavesAndSheaves where

open import Library hiding (refl; trans; _∈_)

open import Level
import Relation.Binary.Core as Eq
import Relation.Binary.PropositionalEquality as Eq
import Relation.Binary.PropositionalEquality.Core as Eq
open import Function.Inverse using (_↔_; module Inverse)
open import Function.Equality using (_⟨$⟩_)

module _ {A : Set} {B : Set} (e : A ↔ B) where
  open Inverse e

  –> : A → B
  –> a = to ⟨$⟩ a

  <– : B → A
  <– b = from ⟨$⟩ b

record Poset : Set₁ where
  field
    A : Set
    _≤_ : (x y : A) → Set
    refl : {x : A} → x ≤ x
    trans : {x y z : A} (p : x ≤ y) (q : y ≤ z) → x ≤ z

record Poset₁ : Set₂ where
  field
    A : Set₁
    _≤_ : (x y : A) → Set
    refl : {x : A} → x ≤ x
    trans : {x y z : A} (p : x ≤ y) (q : y ≤ z) → x ≤ z

module _ {P : Poset} where
  open Poset P

  record IsMeet (x y z : A) : Set where
    field
      π₁ : z ≤ x
      π₂ : z ≤ y
      univ : (a : A) (e₁ : a ≤ x) (e₂ : a ≤ y) → a ≤ z

record Coverage (P : Poset) : Set₁ where
  open Poset P

  field
    Cover : A → Set
    _∈_ : {a : A} (b : A) (C : Cover a) → Set
    ∈-≤ : {a b : A} {C : Cover a} → b ∈ C → b ≤ a

    weaken : {a b : A} (σ : b ≤ a) (C : Cover a) → Cover b
    weaken-ext : {a b : A} {σ : b ≤ a} {C : Cover a} → Σ A (λ x → x ∈ C) ↔ Σ A (λ y → y ∈ weaken σ C)
    weaken-ext-meet : {a b : A} {σ : b ≤ a} {C : Cover a} {x : A} {e : x ∈ C} → IsMeet {P} a x (proj₁ (–> (weaken-ext {σ = σ}) (x , e)))

    singleton : {a : A} → Cover a
    singleton-ext : {a b : A} → b ∈ singleton {a} ↔ b Eq.≡ a

    paste : {a : A} (C : Cover a) (D : (b : A) → b ∈ C → Cover b) → Cover a
    paste-ext : {a : A} {C : Cover a} {D : (b : A) → b ∈ C → Cover b} {c : A} → c ∈ paste C D ↔ ∃ λ b → Σ (b ∈ C) (λ e → c ∈ D b e)

record Presheaf (P : Poset) : Set₁ where
  open Poset P

  field
    ⟦_⟧ : A → Set
    ⟦_⟧-hom : {a b : A} (p : b ≤ a) → ⟦ a ⟧ → ⟦ b ⟧

module _ {P : Poset} where
  open Poset P

  PresheafPoset : Poset₁
  PresheafPoset .Poset₁.A = Presheaf P
  PresheafPoset .Poset₁._≤_ F G = {a : A} → F.⟦ a ⟧ → G.⟦ a ⟧ where
    module F = Presheaf F
    module G = Presheaf G
  PresheafPoset .Poset₁.refl = Library.id
  PresheafPoset .Poset₁.trans f g = g ∘ f

  open Poset₁ PresheafPoset using () renaming (refl to reflᵖ; trans to transᵖ) public
  infix 4 _≤ᵖ_
  _≤ᵖ_ = Poset₁._≤_ PresheafPoset

module PresheafFormers {P : Poset} where
  open Poset P
  open Presheaf

  True : Presheaf P
  True .⟦_⟧ a = ⊤
  ⟦ True ⟧-hom p ⊤.tt = ⊤.tt

  True-in : {H : Presheaf P} → H ≤ᵖ True
  True-in _ = ⊤.tt

  False : Presheaf P
  False .⟦_⟧ a = ⊥
  ⟦ False ⟧-hom p ()

  False-out : {H : Presheaf P} → False ≤ᵖ H
  False-out = ⊥-elim

  module _ (F G : Presheaf P) where
    private module F = Presheaf F
    private module G = Presheaf G

    infix 10 _∧_

    _∧_ : Presheaf P
    _∧_ .⟦_⟧ a = F.⟦ a ⟧ × G.⟦ a ⟧
    _∧_ .⟦_⟧-hom p = map-× (F.⟦_⟧-hom p) (G.⟦_⟧-hom p)

  ∧-in : ∀ {F G H} → H ≤ᵖ F → H ≤ᵖ G → H ≤ᵖ F ∧ G
  ∧-in u v x = (u x , v x)

  ∧-out₁ : ∀ {F G} → F ∧ G ≤ᵖ F
  ∧-out₁ = proj₁

  ∧-out₂ : ∀ {F G} → F ∧ G ≤ᵖ G
  ∧-out₂ = proj₂

  module _ (F G : Presheaf P) where
    private module F = Presheaf F
    private module G = Presheaf G

    infix 9 _∨_

    _∨_ : Presheaf P
    _∨_ .⟦_⟧ a = F.⟦ a ⟧ ⊎ G.⟦ a ⟧
    _∨_ .⟦_⟧-hom p = map-⊎ (F.⟦_⟧-hom p) (G.⟦_⟧-hom p)

  ∨-in₁ : ∀ {F G} → F ≤ᵖ F ∨ G
  ∨-in₁ = inj₁

  ∨-in₂ : ∀ {F G} → G ≤ᵖ F ∨ G
  ∨-in₂ = inj₂

  ∨-out : ∀ {F G H} → F ≤ᵖ H → G ≤ᵖ H → F ∨ G  ≤ᵖ H
  ∨-out u v = [ u , v ]

  module _ (F G : Presheaf P) where
    private module F = Presheaf F
    private module G = Presheaf G

    infix 8 _⇒_

    _⇒_ : Presheaf P
    _⇒_ .⟦_⟧ a = (a' : A) (p : a' ≤ a) (x : F.⟦ a' ⟧) → G.⟦ a' ⟧
    _⇒_ .⟦_⟧-hom {a} {b} p fa b' q y = fa b' (trans q p) y

  ⇒-in : ∀ {F G H} → H ∧ F ≤ᵖ G → H ≤ᵖ F ⇒ G
  ⇒-in {H = H} u x a' p y = u (H.⟦ p ⟧-hom x , y) where
    module H = Presheaf H

  ⇒-out : ∀ {F G H} → H ≤ᵖ F ⇒ G → H ∧ F ≤ᵖ G
  ⇒-out f (x , y) = f x _ refl y

  module Fund (H : Presheaf P) where
    private module H = Presheaf H

    trueI : H ≤ᵖ True
    trueI x = ⊤.tt

    falseE : ∀ {M} → False ≤ᵖ M
    falseE = ⊥-elim

    andE₁ : ∀ {F G} → H ≤ᵖ F ∧ G → H ≤ᵖ F
    andE₁ t x = proj₁ (t x)

    andE₂ : ∀ {F G} → H ≤ᵖ F ∧ G → H ≤ᵖ G
    andE₂ t x = proj₂ (t x)

    orI₁ : ∀ {F G} → H ≤ᵖ F → H ≤ᵖ F ∨ G
    orI₁ t x = inj₁ (t x)

    orI₂ : ∀ {F G} → H ≤ᵖ G → H ≤ᵖ F ∨ G
    orI₂ t x = inj₂ (t x)

    impI : ∀ {F G} → H ∧ F ≤ᵖ G → H ≤ᵖ F ⇒ G
    impI u x a' p y = u (H.⟦ p ⟧-hom x , y)

    impE : ∀ {F G} → H ≤ᵖ F ⇒ G → H ≤ᵖ F → H ≤ᵖ G
    impE f u x = f x _ refl (u x)

module _ {P : Poset} where
  open Poset P

  module _ where
    open Presheaf

    yoneda : A → Presheaf P
    yoneda a .⟦_⟧ b = b ≤ a
    yoneda a .⟦_⟧-hom = trans

  record Sheaf (coverage : Coverage P) : Set₁ where
    open Coverage coverage

    field
      presheaf : Presheaf P
    open Presheaf presheaf public
    field
      glue : {a : A} (C : Cover a) → ({b : A} → b ∈ C → ⟦ b ⟧) → ⟦ a ⟧

  infix 20 _ᵖ

  _ᵖ : {coverage : Coverage P} → Sheaf coverage → Presheaf P
  _ᵖ = Sheaf.presheaf

  module _ {coverage : Coverage P} where
    open Coverage coverage

    SheafPoset : Poset₁
    SheafPoset .Poset₁.A = Sheaf coverage
    SheafPoset .Poset₁._≤_ F G = F ᵖ ≤ᵖ G ᵖ
    SheafPoset .Poset₁.refl {F} = reflᵖ {P} {F ᵖ}
    SheafPoset .Poset₁.trans {F} {G} {H} = transᵖ {P} {F ᵖ} {G ᵖ} {H ᵖ}

    open Poset₁ SheafPoset using () renaming (refl to reflˢ; trans to transˢ) public
    infix 4 _≤ˢ_
    _≤ˢ_ = Poset₁._≤_ SheafPoset

  module Sheafification {coverage : Coverage P} where
    open Coverage coverage

    module _ where
      open Sheaf

      sheafify : Presheaf P → Sheaf coverage
      sheafify F = G where
        private module F = Presheaf F
        open Presheaf

        G : Sheaf coverage
        G .presheaf .⟦_⟧ a = Σ (Cover a) λ C → {x : A} (e : x ∈ C) → F.⟦ x ⟧
        -- I don't like to use 'with'
        G .presheaf .⟦_⟧-hom p (C , h) = (weaken p C , help) where
          help : {x' : A} (e' : x' ∈ weaken p C) → F.⟦ x' ⟧
          help {x'} e' = F.⟦ q ⟧-hom (h e) where
            open Σ (<– weaken-ext (x' , e')) renaming (proj₁ to x; proj₂ to e)

            q : x' ≤ x
            q = Eq.subst (λ z → z .proj₁ ≤ x) (Inverse.right-inverse-of weaken-ext (x' , e')) (weaken-ext-meet {e = e} .IsMeet.π₂)
        G .glue C h .proj₁ = paste C λ b e → h e .proj₁
        -- I don't like to use 'with'
        G .glue C h .proj₂ e = h e' .proj₂ q where
          open Σ (–> paste-ext e) renaming (proj₁ to b; proj₂ to e',q)
          open Σ e',q renaming (proj₁ to e'; proj₂ to q)

    η : {F : Presheaf P} → F ≤ᵖ sheafify F ᵖ
    η x .proj₁ = singleton
    η {F} x .proj₂ e = Eq.subst ⟦_⟧ (Eq.sym (–> singleton-ext e)) x where
      open Presheaf F

    univ-prop : {F : Presheaf P} {G : Sheaf coverage} (u : F ≤ᵖ G ᵖ) → sheafify F ᵖ ≤ᵖ G ᵖ
    univ-prop {F} {G} u (C , h) = glue C (u ∘ h) where
      open Sheaf G
      module F = Presheaf F
      module G = Presheaf presheaf

  module SheafFormers {coverage : Coverage P} where
    open Coverage coverage
    open Sheaf

    module PF = PresheafFormers
    open Sheafification {coverage = coverage}

    True : Sheaf coverage
    True .presheaf = PF.True
    True .glue _ _ = ⊤.tt

    True-in : {H : Sheaf coverage} → H ≤ˢ True
    True-in _ = ⊤.tt

    False : Sheaf coverage
    False = sheafify PF.False

    False-out : {H : Sheaf coverage} → False ≤ˢ H
    False-out {H} = univ-prop {F = PF.False} {G = H} (PF.False-out {H = H ᵖ})

    module _ (F G : Sheaf coverage) where
      private module F = Sheaf F
      private module G = Sheaf G

      infix 10 _∧_

      _∧_ : Sheaf coverage
      _∧_ .presheaf = F.presheaf PF.∧ G.presheaf
      _∧_ .glue C h = (F.glue C (proj₁ ∘ h) , G.glue C (proj₂ ∘ h))

    ∧-in : ∀ {F G H} → H ≤ˢ F → H ≤ˢ G → H ≤ˢ F ∧ G
    ∧-in {F} {G} {H} = PF.∧-in {F = F ᵖ} {G = G ᵖ} {H = H ᵖ}

    ∧-out₁ : ∀ {F G} → F ∧ G ≤ˢ F
    ∧-out₁ {F} {G} = PF.∧-out₁ {F = F ᵖ} {G = G ᵖ}

    ∧-out₂ : ∀ {F G} → F ∧ G ≤ˢ G
    ∧-out₂ {F} {G} = PF.∧-out₂ {F = F ᵖ} {G = G ᵖ}

    module _ (F G : Sheaf coverage) where
      private module F = Sheaf F
      private module G = Sheaf G

      infix 9 _∨_

      _∨_ : Sheaf coverage
      _∨_ = sheafify (F.presheaf PF.∨ G.presheaf)

    ∨-in₁ : ∀ {F G} → F ≤ˢ F ∨ G
    ∨-in₁ {F} {G} = transᵖ {x = F ᵖ} {y = F ᵖ PF.∨ G ᵖ} {z = (F ∨ G) ᵖ} (PF.∨-in₁ {F = F ᵖ} {G = G ᵖ}) (η {F = F ᵖ PF.∨ G ᵖ})

    ∨-in₂ : ∀ {F G} → G ≤ˢ F ∨ G
    ∨-in₂ {F} {G} = transᵖ {x = G ᵖ} {y = F ᵖ PF.∨ G ᵖ} {z = (F ∨ G) ᵖ} (PF.∨-in₂ {F = F ᵖ} {G = G ᵖ}) (η {F = F ᵖ PF.∨ G ᵖ})

    ∨-out : ∀ {F G H} → F ≤ˢ H → G ≤ˢ H → F ∨ G ≤ˢ H
    ∨-out {F} {G} {H} u v = univ-prop {F = F ᵖ PF.∨ G ᵖ} {G = H} (PF.∨-out {F = F ᵖ} {G = G ᵖ} {H = H ᵖ} u v)

    module _ (F G : Sheaf coverage) where
      private module F = Sheaf F
      private module G = Sheaf G

      infix 8 _⇒_

      _⇒_ : Sheaf coverage
      _⇒_ .presheaf = F.presheaf PF.⇒ G.presheaf
      _⇒_ .glue {a} C h a' p x = let
          help : {b' : A} → b' ∈ weaken p C → G.⟦ b' ⟧
          help {b'} e' = let
              open Σ (<– weaken-ext (b' , e')) renaming (proj₁ to b; proj₂ to e)
              k : F.⟦ b' ⟧ → G.⟦ b' ⟧
              k = h e b' (Eq.subst (λ z → z .proj₁ ≤ b)
                            (Inverse.right-inverse-of weaken-ext (b' , e'))
                            (weaken-ext-meet {σ = p} {C = C} {x = b} {e = e} .IsMeet.π₂))
            in k (F.⟦ ∈-≤ e' ⟧-hom x)
        in G.glue (weaken p C) help

      -- _⇒_ : Sheaf coverage
      -- _⇒_ .presheaf = F.presheaf PF.⇒ G.presheaf
      -- _⇒_ .glue {a} C h a' p x = G.glue (weaken p C) help where
      --   help : {b' : A} → b' ∈ weaken p C → G.⟦ b' ⟧
      --   help {b'} e' = k (F.⟦ ∈-≤ e' ⟧-hom x) where
      --     open Σ (<– weaken-ext (b' , e')) renaming (proj₁ to b; proj₂ to e)

      --     k : F.⟦ b' ⟧ → G.⟦ b' ⟧
      --     k = h e b' (Eq.subst (λ z → z .proj₁ ≤ b) (Inverse.right-inverse-of weaken-ext (b' , e')) (weaken-ext-meet {σ = p} {C = C} {x = b} {e = e} .IsMeet.π₂))

    ⇒-in : ∀ {F G H} → H ∧ F ≤ˢ G → H ≤ˢ F ⇒ G
    ⇒-in {F} {G} {H} = PF.⇒-in {F = F ᵖ} {G = G ᵖ} {H = H ᵖ}

    ⇒-out : ∀ {F G H} → H ≤ˢ F ⇒ G → H ∧ F ≤ˢ G
    ⇒-out {F} {G} {H} = PF.⇒-out {F = F ᵖ} {G = G ᵖ} {H = H ᵖ}

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
module _ where

-- This is all standard library stuff, inspect on steroids:

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

data Unit : Set where
  unit : Unit

Hidden : Set → Set
Hidden A = Unit → A

hide : {A : Set} {B : A → Set} →
       ((x : A) → B x) → ((x : A) → Hidden (B x))
hide f x unit = f x

reveal : {A : Set} → Hidden A → A
reveal f = f unit

data Reveal_is_ {A : Set} (x : Hidden A) (y : A) : Set where
  [_] : (eq : reveal x ≡ y) → Reveal x is y

inspect : {A : Set} {B : A → Set}
          (f : (x : A) → B x) (x : A) → Reveal (hide f x) is (f x)
inspect f x = [ refl ]

data ℕ : Set where
  zero : ℕ
  suc : ℕ -> ℕ

-- New stuff starts here:

data Wrap : ℕ -> Set where
  con : (n : ℕ) -> Wrap n

wrap : (n : ℕ) -> Wrap n
wrap zero    = con zero
wrap (suc x) = con (suc x)

bar-with : (n : ℕ)(v : Wrap n) -> Reveal (hide wrap n) is (wrap n) -> ℕ
bar-with n (con .n) r = zero

bar : (n : ℕ) -> ℕ
bar zero = zero
bar (suc n) = bar-with n (wrap n) (inspect wrap n)

-- I've manually desugared `bar' to make the error clearer, but the
-- following definition works correctly:
{-
bar : (n : ℕ) -> ℕ
bar zero = zero
bar (suc n) with wrap n | inspect wrap n
bar (suc ._) | con _    | r = zero
-}

foo : (n : ℕ) -> Wrap (bar n) -> ℕ
foo zero p = zero
foo (suc x) p with inspect bar x
foo (suc x) p | r = zero

-- The previous line gives the error:

-- ℕ != Wrap x of type Set
-- when checking that the type
-- (x : ℕ) (w : Reveal_is_ {ℕ} (hide {ℕ} {λ _ → ℕ} bar x) (bar x))
-- (p : Wrap (bar-with x (wrap x) w)) →
-- ℕ
-- of the generated with function is well-formed

-- In particular, notice that the type of `p' is incorrect, because an
-- occurrence of `inspect wrap x` has been turned into the variable w
-- (which corresponds to `inspect bar x`).

-- I think the correct desugaring of the with is as follows:

good-foo-with : (x : ℕ) -> Wrap (bar (suc x)) -> Reveal (hide bar x) is bar x -> ℕ
good-foo-with x w r = zero

good-foo : (n : ℕ) -> Wrap (bar n) -> ℕ
good-foo zero p = zero
good-foo (suc x) p = good-foo-with x p (inspect bar x)


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

module RewriteAndUniversePolymorphism where

postulate
  Level : Set
  lzero : Level
  lsuc  : (i : Level) → Level
  _⊔_   : Level -> Level -> Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO lzero  #-}
{-# BUILTIN LEVELSUC  lsuc   #-}
{-# BUILTIN LEVELMAX _⊔_ #-}

infixl 6 _⊔_

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

infix 4 _≡_

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

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

test : (a b : ℕ) → a ≡ b → b ≡ a
test a b eq rewrite eq = refl

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module ObsEq where

data Zero : Set where

record One : Set where

data Two : Set where
  tt : Two
  ff : Two

Π : (S : Set)(T : S -> Set) -> Set
Π S T = (x : S) -> T x

record Σ (S : Set)(T : S -> Set) : Set where
  field
    fst : S
    snd : T fst

_,_ : {S : Set}{T : S -> Set}(s : S) -> T s -> Σ S T
s , t = record {fst = s; snd = t}

open module Σ' {S : Set}{T : S -> Set} = Σ {S} {T}

data W (S : Set)(T : S -> Set) : Set where
  _<|_ : (s : S) -> (T s -> W S T) -> W S T

mutual

  data ∗ : Set where
    /0/ : ∗
    /1/ : ∗
    /2/ : ∗
    /Π/ : (S : ∗)(T : [ S ] -> ∗) -> ∗
    /Σ/ : (S : ∗)(T : [ S ] -> ∗) -> ∗
    /W/ : (S : ∗)(T : [ S ] -> ∗) -> ∗

  [_] : ∗ -> Set
  [ /0/ ]      = Zero
  [ /1/ ]      = One
  [ /2/ ]      = Two
  [ /Π/ S T ]  = Π [ S ] \s -> [ T s ]
  [ /Σ/ S T ]  = Σ [ S ] \s -> [ T s ]
  [ /W/ S T ]  = W [ S ] \s -> [ T s ]

infixr 40 _⟶_

_⟶_ : ∗ -> ∗ -> ∗
S ⟶ T = /Π/ S \_ -> T

{-
_Ψ_ : Zero -> (S : ∗) -> [ S ]
() Ψ S   -- magic as there's no such thing
-}

_Ψ : Zero -> {S : Set} -> S
() Ψ

Case : Two -> ∗ -> ∗ -> ∗
Case tt St Sf = St
Case ff St Sf = Sf

case : (P : Two -> ∗)(b : Two) -> [ P tt ] -> [ P ff ] -> [ P b ]
case P tt ptt pff = ptt
case P ff ptt pff = pff

rec : {S : Set}{T : S -> Set}(P : W S T -> ∗)(x : W S T) ->
      ((s : S)(f : T s -> W S T) ->
       ((t : T s) -> [ P (f t) ]) -> [ P (s <| f) ]) ->
      [ P x ]
rec P (s <| f) p = p s f \t -> rec P (f t) p

/Nat/ : ∗
/Nat/ = /W/ /2/ \b -> Case b /0/ /1/

zero : [ /Nat/ ]
zero = tt <| \z -> z Ψ

suc : [ /Nat/ ⟶ /Nat/ ]
suc n = ff <| \_ -> n

{-
elimNatSet : (P : [ /Nat/ ] -> Set) ->
          P zero ->
          ((k : [ /Nat/ ]) -> P k -> P (suc k)) ->
          (n : [ /Nat/ ]) -> P n
elimNatSet P pz ps (tt <| g) = {! !}
elimNatSet P pz ps (ff <| g) = {! !}
-}

infixr 60 _∧_

data † : Set where
  ⊥   : †
  TT  : †
  _∧_ : † -> † -> †
  ∏   : (S : ∗) -> ([ S ] -> †) -> †

|- : † -> ∗
|- ⊥       = /0/
|- TT      = /1/
|- (P ∧ Q) = /Σ/ (|- P) \_ -> |- Q
|- (∏ S P) = /Π/ S \s -> |- (P s)

Prf : † -> Set
Prf P = [ |- P ]

infixr 40 _⇒_

_⇒_ : † -> † -> †
P ⇒ Q = ∏ (|- P) \_ -> Q

infix 80 _⇔_

mutual

  _⇔_ : ∗ -> ∗ -> †
  /0/        ⇔  /0/        =  TT
  /1/        ⇔  /1/        =  TT
  /2/        ⇔  /2/        =  TT
  /Π/ S0 T0  ⇔  /Π/ S1 T1  =
    S1 ⇔ S0  ∧
    ∏ S1 \s1 -> ∏ S0 \s0 -> (S1 > s1 ≅ S0 > s0) ⇒ (T0 s0 ⇔ T1 s1)
  /Σ/ S0 T0  ⇔  /Σ/ S1 T1  =
    S0 ⇔ S1  ∧
    ∏ S0 \s0 -> ∏ S1 \s1 -> (S0 > s0 ≅ S1 > s1) ⇒ (T0 s0 ⇔ T1 s1)
  /W/ S0 T0  ⇔  /W/ S1 T1  =
    S0 ⇔ S1  ∧
    ∏ S0 \s0 -> ∏ S1 \s1 -> (S0 > s0 ≅ S1 > s1) ⇒ (T1 s1 ⇔ T0 s0)
  _          ⇔  _ = ⊥

  _>_≅_>_ : (S : ∗) -> [ S ] -> (T : ∗) -> [ T ] -> †
  /0/ > _  ≅ /0/ > _  = TT
  /1/ > _  ≅ /1/ > _  = TT
  /2/ > tt ≅ /2/ > tt = TT
  /2/ > ff ≅ /2/ > ff = TT

  /Π/ S0 T0 > f0 ≅ /Π/ S1 T1 > f1 =
    ∏ S0 \s0 -> ∏ S1 \s1 -> (S0 > s0 ≅ S1 > s1) ⇒
      (T0 s0 > f0 s0 ≅ T1 s1 > f1 s1)

  /Σ/ S0 T0 > p0 ≅ /Σ/ S1 T1 > p1 =
    (S0          > fst p0 ≅ S1          > fst p1) ∧
    (T0 (fst p0) > snd p0 ≅ T1 (fst p1) > snd p1)

  /W/ S0 T0 > (s0 <| f0) ≅ /W/ S1 T1 > (s1 <| f1) =
    (S0 > s0 ≅ S1 > s1)  ∧
    ∏ (T0 s0) \t0 -> ∏ (T1 s1) \t1 ->
       (T0 s0 > t0 ≅ T1 s1 > t1) ⇒
       (/W/ S0 T0 > f0 t0 ≅ /W/ S1 T1 > f1 t1)

  _ > _ ≅ _ > _ = ⊥

mutual

  _>_<_!_ : (S : ∗) -> [ S ] -> (T : ∗) -> Prf (S ⇔ T) -> [ T ]

  /0/ > z < /0/ ! _  = z
  /1/ > u < /1/ ! _  = u
  /2/ > b < /2/ ! _  = b

  /Π/ S0 T0 > f0 < /Π/ S1 T1 ! Q =
    let S1S0 : Prf (S1 ⇔ S0)
        S1S0 = fst Q
        T0T1 : Prf (∏ S1 \s1 -> ∏ S0 \s0 -> (S1 > s1 ≅ S0 > s0) ⇒
                      (T0 s0 ⇔ T1 s1))
        T0T1 = snd Q
    in  \s1 ->
        let s0   : [ S0 ]
            s0   = S1 > s1 < S0 ! S1S0
            s1s0 : Prf (S1 > s1 ≅ S0 > s0)
            s1s0 = [| S1 > s1 < S0 ! S1S0 |]
        in  T0 s0 > f0 s0 < T1 s1 ! T0T1 s1 s0 s1s0

  /Σ/ S0 T0 > p0 < /Σ/ S1 T1 ! Q =
    let S0S1 : Prf (S0 ⇔ S1)
        S0S1 = fst Q
        T0T1 : Prf (∏ S0 \s0 -> ∏ S1 \s1 -> (S0 > s0 ≅ S1 > s1) ⇒
                      (T0 s0 ⇔ T1 s1))
        T0T1 = snd Q
        s0   : [ S0 ]
        s0   = fst p0
        s1   : [ S1 ]
        s1   = S0 > s0 < S1 ! S0S1
        s0s1 : Prf (S0 > s0 ≅ S1 > s1)
        s0s1 = [| S0 > s0 < S1 ! S0S1 |]
        t0   : [ T0 s0 ]
        t0   = snd p0
        t1   : [ T1 s1 ]
        t1   = T0 s0 > t0 < T1 s1 ! T0T1 s0 s1 s0s1
    in  s1 , t1

  /W/ S0 T0 > (s0 <| f0) < /W/ S1 T1 ! Q =
    let S0S1 : Prf (S0 ⇔ S1)
        S0S1 = fst Q
        T1T0 : Prf (∏ S0 \s0 -> ∏ S1 \s1 -> (S0 > s0 ≅ S1 > s1) ⇒
                      (T1 s1 ⇔ T0 s0))
        T1T0 = snd Q
        s1   : [ S1 ]
        s1   = S0 > s0 < S1 ! S0S1
        s0s1 : Prf (S0 > s0 ≅ S1 > s1)
        s0s1 = [| S0 > s0 < S1 ! S0S1 |]
    in  s1 <| \t1 ->
        let t0   : [ T0 s0 ]
            t0   = T1 s1 > t1 < T0 s0 ! T1T0 s0 s1 s0s1
        in  /W/ S0 T0 > f0 t0 < /W/ S1 T1 ! Q

  /0/     > _ < /1/     ! ()
  /0/     > _ < /2/     ! ()
  /0/     > _ < /Π/ _ _ ! ()
  /0/     > _ < /Σ/ _ _ ! ()
  /0/     > _ < /W/ _ _ ! ()
  /1/     > _ < /0/     ! ()
  /1/     > _ < /2/     ! ()
  /1/     > _ < /Π/ _ _ ! ()
  /1/     > _ < /Σ/ _ _ ! ()
  /1/     > _ < /W/ _ _ ! ()
  /2/     > _ < /0/     ! ()
  /2/     > _ < /1/     ! ()
  /2/     > _ < /Π/ _ _ ! ()
  /2/     > _ < /Σ/ _ _ ! ()
  /2/     > _ < /W/ _ _ ! ()
  /Π/ _ _ > _ < /0/     ! ()
  /Π/ _ _ > _ < /1/     ! ()
  /Π/ _ _ > _ < /2/     ! ()
  /Π/ _ _ > _ < /Σ/ _ _ ! ()
  /Π/ _ _ > _ < /W/ _ _ ! ()
  /Σ/ _ _ > _ < /0/     ! ()
  /Σ/ _ _ > _ < /1/     ! ()
  /Σ/ _ _ > _ < /2/     ! ()
  /Σ/ _ _ > _ < /Π/ _ _ ! ()
  /Σ/ _ _ > _ < /W/ _ _ ! ()
  /W/ _ _ > _ < /0/     ! ()
  /W/ _ _ > _ < /1/     ! ()
  /W/ _ _ > _ < /2/     ! ()
  /W/ _ _ > _ < /Π/ _ _ ! ()
  /W/ _ _ > _ < /Σ/ _ _ ! ()

  [|_>_<_!_|] : (S : ∗)(s : [ S ])(T : ∗)(q : Prf (S ⇔ T)) ->
    Prf (S > s ≅ T > (S > s < T ! q))
  [| S > s < T ! q |] = {! !}

Resp : (S : ∗)(P : [ S ] -> ∗)
       {s0 s1 : [ S ]} -> Prf ((S > s0 ≅ S > s1) ⇒ (P s0 ⇔ P s1))
Resp = {! !}

[|_>_|] : (S : ∗)(s : [ S ]) -> Prf (S > s ≅ S > s)
[| S > s |] = {! !}

Sym : (S0 S1 : ∗) -> Prf ((S0 ⇔ S1) ⇒ (S1 ⇔ S0))
Sym = {! !}

sym : (S0 : ∗)(s0 : [ S0 ])(S1 : ∗)(s1 : [ S1 ]) ->
      Prf ((S0 > s0 ≅ S1 > s1) ⇒ (S1 > s1 ≅ S0 > s0))
sym = {! !}

elimNat∗ : (P : [ /Nat/ ] -> ∗) ->
           [( P zero ⟶ (/Π/ /Nat/ \k -> P k ⟶ P (suc k)) ⟶
              /Π/ /Nat/ \n -> P n )]
{-
elimNat∗ P pz ps (tt <| g) = P zero > pz < P (tt <| g) !
  Resp /Nat/ P (_ , \z0 -> z0 Ψ)
elimNat∗ P pz ps (ff <| g) =
  let n = g _
  in  P (suc n) > ps n (elimNat∗ P pz ps n) < P (ff <| g) !
         Resp /Nat/ P
           (_ , \u0 u1 u0u1 -> [| (/1/ ⟶ /Nat/) > g |] _ u1 _)
-}
elimNat∗ P pz ps n = rec P n
  \b -> case (\ b -> /Π/ ((Case b /0/ /1/) ⟶ /Nat/) \g ->
                        (/Π/ (Case b /0/ /1/) \t -> P (g t)) ⟶
                        P (b <| g)) b
    (\g _ -> P zero > pz < P (tt <| g) ! Resp /Nat/ P (_ , \z0 -> z0 Ψ))
    (\g h ->
       let n = g _
       in  P (suc n) > ps n (h _) < P (ff <| g) !
             Resp /Nat/ P
               (_ , \u0 u1 u0u1 -> [| (/1/ ⟶ /Nat/) > g |] _ u1 _))

plus : [ /Nat/ ⟶ /Nat/ ⟶ /Nat/ ]
plus x y = elimNat∗ (\_ -> /Nat/) y (\_ -> suc) x

irr : (P0 P1 : †) -> Prf ((|- P0 ⇔ |- P1) ⇒
      ∏ (|- P0) \p0 -> ∏ (|- P1) \p1 -> |- P0 > p0 ≅ |- P1 > p1)

irr ⊥  ⊥  _ _ _ = _

irr TT TT _ _ _ = _

irr (P0 ∧ Q0) (P1 ∧ Q1) PQ01 pq0 pq1 =
  let p01 : Prf (|- P0 > fst pq0 ≅ |- P1 > fst pq1)
      p01 = irr P0 P1 (fst PQ01) (fst pq0) (fst pq1)
  in  p01 , irr Q0 Q1 (snd PQ01 (fst pq0) (fst pq1) p01) (snd pq0) (snd pq1)

irr (∏ S0 P0) (∏ S1 P1) SP01 f0 f1 = \s0 s1 s0s1 ->
  irr (P0 s0) (P1 s1) (snd SP01 s1 s0 (sym S0 s0 S1 s1 s0s1)) (f0 s0) (f1 s1)

irr        ⊥  TT       () _ _
irr        ⊥  (_ ∧ _)  () _ _
irr        ⊥  (∏ _ _)  () _ _
irr       TT  ⊥        () _ _
irr       TT  (_ ∧ _)  () _ _
irr       TT  (∏ _ _)  () _ _
irr  (_ ∧ _)  TT       () _ _
irr  (_ ∧ _)  ⊥        () _ _
irr  (_ ∧ _)  (∏ _ _)  () _ _
irr  (∏ _ _)  TT       () _ _
irr  (∏ _ _)  ⊥        () _ _
irr  (∏ _ _)  (_ ∧ _)  () _ _

{---------------------------------------------------------------------------

	      The News from Nottingham (with subtitles)

			    Conor McBride

			   joint work with
	 Thorsten Altenkirch, Wouter Swierstra, Peter Hancock,
            Nicolas Oury, James Chapman and Peter Morris

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

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Tests for the compiler itself

open import FRP.JS.Bool using ( Bool ; true ; false ; not )
open import FRP.JS.QUnit using ( TestSuite ; test ; ok ; _,_ )

module FRP.JS.Test.Compiler where

module A where
  module B where
    x = true

f : Bool → Bool
f x = y where
  y = true

f′ : Bool → Bool
f′ x = not y where
  y = false

g : Bool → Bool → Bool
g x = h where
  h : Bool → Bool
  h y = z where
    z = true

mutual
  m1 = m2
  m2 = true
  m3 = m1

tests : TestSuite
tests =
  ( test "nested modules"
    ( ok "A.B.x" A.B.x)
  , test "where clauses"
    ( ok "f false" (f false)
    , ok "f′ false" (f′ false)
    , ok "g false false" (g false false) )
  , test "mutual clauses"
    ( ok "m1" m1
    , ok "m2" m2
    , ok "m3" m3 ) )

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


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

open import LogicalFormulae
open import Groups.Abelian.Definition
open import Groups.Definition
open import Setoids.Setoids
open import Functions.Definition
open import Sets.EquivalenceRelations
open import Lists.Lists

module Groups.Polynomials.Addition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) where

open import Groups.Polynomials.Definition G
open Setoid S
open Equivalence eq
open Group G

_+P_ : NaivePoly → NaivePoly → NaivePoly
_+P_ = listZip _+_ id id

inverse' : NaivePoly → NaivePoly
inverse' = map (Group.inverse G)

abstract
  PidentRight : {m : NaivePoly} → polysEqual (m +P []) m
  PidentRight {[]} = record {}
  PidentRight {x :: m} = reflexive ,, identityOfIndiscernablesLeft polysEqual (Equivalence.reflexive (Setoid.eq naivePolySetoid)) (equalityCommutative (mapId m))

  +PwellDefined : {m n x y : NaivePoly} → polysEqual m x → polysEqual n y → polysEqual (m +P n) (x +P y)
  +PwellDefined {[]} {[]} {[]} {[]} m=x n=y = record {}
  +PwellDefined {[]} {[]} {[]} {x :: y} m=x (fst ,, snd) = fst ,, identityOfIndiscernablesRight polysEqual snd (equalityCommutative (mapId y))
  +PwellDefined {[]} {[]} {x :: xs} {[]} (fst ,, snd) n=y = fst ,, identityOfIndiscernablesRight polysEqual snd (equalityCommutative (mapId xs))
  +PwellDefined {[]} {[]} {x :: xs} {y :: ys} (fst ,, snd) (fst2 ,, snd2) = transitive (+WellDefined fst fst2) identRight ,, +PwellDefined {[]} {[]} {xs} {ys} snd snd2
  +PwellDefined {[]} {n :: ns} {[]} {[]} m=x (fst ,, snd) = fst ,, identityOfIndiscernablesLeft polysEqual snd (equalityCommutative (mapId ns))
  +PwellDefined {[]} {n :: ns} {[]} {y :: ys} m=x (fst ,, snd) = fst ,, +PwellDefined m=x snd
  +PwellDefined {[]} {n :: ns} {x :: xs} {[]} (fst ,, snd) (fst2 ,, snd2) = transitive fst2 (symmetric fst) ,, ans
    where
      ans : polysEqual (map (λ z → z) ns) (map (λ z → z) xs)
      ans rewrite mapId ns | mapId xs = Equivalence.transitive (Setoid.eq naivePolySetoid) snd2 snd
  +PwellDefined {[]} {n :: ns} {x :: xs} {y :: ys} (fst ,, snd) (fst2 ,, snd2) = transitive (symmetric identLeft) (+WellDefined (symmetric fst) fst2) ,, (+PwellDefined snd snd2)
  +PwellDefined {m :: ms} {[]} {[]} {[]} (fst ,, snd) _ = fst ,, identityOfIndiscernablesLeft polysEqual snd (equalityCommutative (mapId ms))
  +PwellDefined {m :: ms} {[]} {[]} {x :: ys} (fst ,, snd) (fst2 ,, snd2) = transitive fst (symmetric fst2) ,, ans
    where
      ans : polysEqual (map (λ z → z) ms) (map (λ z → z) ys)
      ans rewrite mapId ms | mapId ys = Equivalence.transitive (Setoid.eq naivePolySetoid) snd snd2
  +PwellDefined {m :: ms} {[]} {x :: xs} {[]} (fst ,, snd) n=y = fst ,, ans
    where
      ans : polysEqual (map (λ z → z) ms) (map (λ z → z) xs)
      ans rewrite mapId ms | mapId xs = snd
  +PwellDefined {m :: ms} {[]} {x :: xs} {y :: ys} (fst ,, snd) (fst2 ,, snd2) = transitive (symmetric identRight) (+WellDefined fst (symmetric fst2)) ,, identityOfIndiscernablesLeft polysEqual (Equivalence.transitive (Setoid.eq naivePolySetoid) (Equivalence.symmetric (Setoid.eq naivePolySetoid) PidentRight) (+PwellDefined snd snd2)) (equalityCommutative (mapId ms))
  +PwellDefined {m :: ms} {n :: ns} {[]} {[]} (fst ,, snd) (fst2 ,, snd2) = transitive (+WellDefined fst fst2) identLeft ,, +PwellDefined snd snd2
  +PwellDefined {m :: ms} {n :: ns} {[]} {y :: ys} (fst ,, snd) (fst2 ,, snd2) = transitive (+WellDefined fst fst2) identLeft ,, +PwellDefined snd snd2
  +PwellDefined {m :: ms} {n :: ns} {x :: xs} {[]} (fst ,, snd) (fst2 ,, snd2) = transitive (+WellDefined fst fst2) identRight ,, identityOfIndiscernablesRight polysEqual (Equivalence.transitive (Setoid.eq naivePolySetoid) (+PwellDefined snd snd2) PidentRight) (equalityCommutative (mapId xs))
  +PwellDefined {m :: ms} {n :: ns} {x :: xs} {y :: ys} (fst ,, snd) (fst2 ,, snd2) = +WellDefined fst fst2 ,, +PwellDefined snd snd2

  PidentLeft : {m : NaivePoly} → polysEqual ([] +P m) m
  PidentLeft {[]} = record {}
  PidentLeft {x :: m} = reflexive ,, identityOfIndiscernablesLeft polysEqual (Equivalence.reflexive (Setoid.eq naivePolySetoid)) (equalityCommutative (mapId m))

  invLeft' : {a : NaivePoly} → polysEqual ((inverse' a) +P a) []
  invLeft' {[]} = record {}
  invLeft' {x :: a} = Group.invLeft G ,, invLeft' {a}

  invRight' : {a : NaivePoly} → polysEqual (a +P (inverse' a)) []
  invRight' {[]} = record {}
  invRight' {x :: a} = Group.invRight G ,, invRight' {a}

  assoc : {a b c : NaivePoly} → polysEqual (a +P (b +P c)) ((a +P b) +P c)
  assoc {[]} {[]} {[]} = record {}
  assoc {[]} {[]} {x :: c} = reflexive ,, ans
    where
      ans : polysEqual (map (λ z → z) (map (λ z → z) c)) (map (λ z → z) c)
      ans rewrite mapId c | mapId c = Equivalence.reflexive (Setoid.eq naivePolySetoid)
  assoc {[]} {b :: bs} {[]} = reflexive ,, ans
    where
      ans : polysEqual (map (λ z → z) (map (λ z → z) bs)) (map (λ z → z) (map (λ z → z) bs))
      ans rewrite mapId bs | mapId bs = Equivalence.reflexive (Setoid.eq naivePolySetoid)
  assoc {[]} {b :: bs} {c :: cs} = reflexive ,, ans
    where
      ans : polysEqual (map (λ z → z) (listZip _+_ (λ z → z) (λ z → z) bs cs)) (listZip _+_ (λ z → z) (λ z → z) (map (λ z → z) bs) cs)
      ans rewrite mapId bs | mapId (listZip _+_ id id bs cs) = Equivalence.reflexive (Setoid.eq naivePolySetoid)
  assoc {a :: as} {[]} {[]} = reflexive ,, ans
    where
      ans : polysEqual (map (λ z → z) as) (map (λ z → z) (map (λ z → z) as))
      ans rewrite mapId as | mapId as = Equivalence.reflexive (Setoid.eq naivePolySetoid)
  assoc {a :: as} {[]} {c :: cs} = reflexive ,, ans
    where
      ans : polysEqual (listZip _+_ (λ z → z) (λ z → z) as (map (λ z → z) cs)) (listZip _+_ (λ z → z) (λ z → z) (map (λ z → z) as) cs)
      ans rewrite mapId cs | mapId as = Equivalence.reflexive (Setoid.eq naivePolySetoid)
  assoc {a :: as} {b :: bs} {[]} = reflexive ,, ans
    where
      ans : polysEqual (listZip _+_ (λ z → z) (λ z → z) as (map (λ z → z) bs)) (map (λ z → z) (listZip _+_ (λ z → z) (λ z → z) as bs))
      ans rewrite mapId (listZip _+_ id id as bs) | mapId bs = Equivalence.reflexive (Setoid.eq naivePolySetoid)
  assoc {a :: as} {b :: bs} {c :: cs} = Group.+Associative G ,, assoc {as} {bs} {cs}

  comm : AbelianGroup G → {x y : NaivePoly} → polysEqual (x +P y) (y +P x)
  comm com {[]} {y} = Equivalence.transitive (Setoid.eq naivePolySetoid) PidentLeft (Equivalence.symmetric (Setoid.eq naivePolySetoid) PidentRight)
  comm com {x :: xs} {[]} = reflexive ,, Equivalence.reflexive (Setoid.eq naivePolySetoid)
  comm com {x :: xs} {y :: ys} = AbelianGroup.commutative com ,, comm com {xs} {ys}

  mapDist : (f : A → A) (fDist : {x y : A} → f (x + y) ∼ (f x) + (f y)) (xs ys : NaivePoly) → polysEqual (map f (xs +P ys)) ((map f xs) +P (map f ys))
  mapDist f fDist [] [] = record {}
  mapDist f fDist [] (x :: ys) rewrite mapId ys | mapId (map f ys) = reflexive ,, Equivalence.reflexive (Setoid.eq naivePolySetoid)
  mapDist f fDist (x :: xs) [] rewrite mapId xs | mapId (map f xs) = reflexive ,, Equivalence.reflexive (Setoid.eq naivePolySetoid)
  mapDist f fDist (x :: xs) (y :: ys) = fDist {x} {y} ,, mapDist f fDist xs ys


text:
open import Agda.Builtin.Nat

record R : Set where
  field
    r₁ : Nat
    r₂ : Nat
open R

h : (n : Nat) → R
r₁ (h zero) = {!!}
r₂ (h zero) = {!!}
h = {!!}


text:
module Formalization.ClassicalPropositionalLogic.Syntax.Proofs where

import      Lvl
open import Formalization.ClassicalPropositionalLogic.Syntax
open import Relator.Equals.Proofs.Equiv
open import Type.Size.Countable
open import Type

private variable ℓₚ ℓ : Lvl.Level
private variable P : Type{ℓₚ}

-- TODO: How would a proof of this look like?
instance
  postulate Formula-is-countably-infinite : ⦃ _ : CountablyInfinite(P) ⦄ → CountablyInfinite(Formula(P))

{-
open import Type.WellOrdering
Formula-W-bijectivity : Bijective(W{A = 𝕟(8)}())
Formula-W-bijectivity = {!!
-}

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 Data.Star.Properties.Extra where

open import Relation.Binary.Core
open import Data.Star

module _ {i}{I : Set i}{r}{R : Rel I r} where
  _◅◅-ε : ∀ {i j} → (xs : Star R i j) → xs ◅◅ ε ≡ xs
  ε ◅◅-ε = refl
  (x ◅ xs) ◅◅-ε rewrite xs ◅◅-ε = refl


text:
module my-termination where

open import bool
open import eq
open import level
open import list
open import nat
open import nat-thms
open import product
open import sum

----------------------------------------------------------------------
-- types
----------------------------------------------------------------------

{- ↓ _>_ a means that the _>_ relation is well-founded below a.  That
   is, there are no infinite chains a > a1 > ... starting with a.
   One can also say that _>_ terminates from a. -}
data ↓ {ℓ ℓ'} {A : Set ℓ} (_>_ : A → A → Set ℓ') : A → Set (ℓ ⊔ ℓ') where
  pf↓ : ∀ {x : A} → (∀ {y : A} → x > y → ↓ _>_ y) → ↓ _>_ x

↓𝔹 : ∀ {ℓ}{A : Set ℓ} (_>_ : A → A → 𝔹) → A → Set ℓ
↓𝔹{ℓ}{A} _>_ x = ↓{ℓ}{lzero} (λ (x y : A) → (x > y) ≡ tt) x

----------------------------------------------------------------------
-- theorems
----------------------------------------------------------------------

-----------------------------------
-- natural number > is terminating
-----------------------------------
↓-> : ∀ (x : ℕ) → ↓𝔹 _>_ x
↓-> x = pf↓ (h x)
  where h : ∀ x → ∀ {y} → x > y ≡ tt → ↓𝔹 _>_ y
        h 0 {0} ()
        h 0 {suc y} ()
        h (suc x) {y} p with <-drop {y} p
        h (suc x) {y} p | inj₁ u rewrite u = ↓-> x
        h (suc x) {y} p | inj₂ u = h x u

{-
↓-> : ∀ (n : ℕ) → ↓𝔹 _>_ n
↓-> n = pf↓ (lem n)
  where lem : ∀ y → ∀ {x} → y > x ≡ tt → ↓𝔹 _>_ x
        lem 0 {0} ()
        lem 0 {suc y} ()
        lem (suc x) {y} p with <-drop {y} p
        lem (suc x) {y} p | inj₁ u rewrite u = ↓-> x
        lem (suc x) {y} p | inj₂ u = lem x u
-}

------------------------------
-- lexicographic combination
------------------------------
module lexcomb {ℓ ℓ' ℓ1 ℓ2 : level}{A : Set ℓ}{B : Set ℓ'}(_>A_ : A → A → Set ℓ1)(_>B_ : B → B → Set ℓ2) where

  _>lex_ : A × B → A × B → Set (ℓ ⊔ ℓ1 ⊔ ℓ2)
  (a , b) >lex (a' , b') = a >A a' ∨ (a ≡ a' ∧ b >B b')

  {- If _>A_ is well-founded below a and if _>B_ is well-founded below every b, then
     _>lex_ is well-founded below (a , b) -}
  ↓-lex : {a : A} → ↓ _>A_ a → ((b : B) → ↓ _>B_ b) → {b : B} → ↓ _>lex_ (a , b)
  ↓-lex {a} (pf↓ fA) tB {b} = pf↓ (helper fA (tB b))
     where helper : {a : A} → (∀{y : A} → a >A y → ↓ _>A_ y) → {b : B} → ↓ _>B_ b → {y : A × B} → (a , b) >lex y → ↓ _>lex_ y
           helper fA _ {a' , b'} (inj₁ u) = ↓-lex (fA u) tB
           helper fA (pf↓ fB) {a' , b'} (inj₂ (u , u')) rewrite u = pf↓ (helper fA (fB u'))

------------------------------
-- measure functions
------------------------------

{- Suppose we want to prove that _>A_ is terminating starting from a, and we have a function m,
   called a measure function, that maps A to another type B, where we know an
   ordering _>B_ is terminating starting from (m a).

   Then as long as m is preserved by _>A_ -- meaning that a >A a' implies m a >B m a' -- then we
   can derive termination starting from a from termination starting from b. -}
module measure {ℓ ℓ' ℓ1 ℓ2 : level}{A : Set ℓ}{B : Set ℓ'}(_>A_ : A → A → Set ℓ1)(_>B_ : B → B → Set ℓ2)
               (m : A → B)
               (decreasem : ∀{a a' : A} → a >A a' → m a >B m a') where

  measure-↓ : ∀ {a : A} → ↓ _>B_ (m a) → ↓ _>A_ a
  measure-↓{a} (pf↓ fM) = pf↓ h
    where h : {y : A} → a >A y → ↓ _>A_ y
          h{y} p = measure-↓ (fM (decreasem p))

------------------------------
-- Newman's Lemma
------------------------------

{-
{- Newman's Lemma says that local confluence implies confluence for
   terminating elements of the relation (the usual formulation speaks
   about these properties for the whole relation, not just elements,
   but this is an obvious refinement). -}

module newman {ℓ ℓ' : level}{A : Set ℓ}(_>A_ : A → A → Set ℓ')
              (lc : ∀{a b c : A} → a >A b → a >A c → ∃ A (λ d → b >A d ∧ c >A d)) where

  open import relations _>A_ using (_tc_ ; tc-step ; tc-trans)

{-  In progress...

  the_lemma : ∀{a b c : A} → ↓ _>A_ a → a tc b → a tc c → ∃ A (λ d → b tc d ∧ c tc d)
  the_lemma w (tc-step u) (tc-step v) with lc u v
  the_lemma w (tc-step u) (tc-step v) | d , u' , v' = d , tc-step u' , tc-step v'
  the_lemma w (tc-step u) (tc-trans v1 v2) = {!!}
  the_lemma w (tc-trans u1 u2) (tc-step v) = {!!}
  the_lemma w (tc-trans u1 u2) (tc-trans v1 v2) = {!!}
-}-}

max_stars_repo_name: logicshan/IAL

max_issues_repo_name: logicshan/IAL

max_forks_repo_name: logicshan/IAL


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

module Hanon where

open import Data.Fin     using (#_)
open import Data.Integer using (+_)
open import Data.List    using (List; _∷_; []; map; concat; _++_)
open import Data.Nat     using (ℕ; zero; suc)
open import Data.Product using (_,_; map₁)
open import Data.Vec     using (fromList)
open import Function     using (_∘_)

open import Pitch        using (Pitch; octave; relativeToAbsolute; majorScale)
open import Note         using (8th)
open import Music        using (Melody; Counterpoint; cp; pitches→melody; transposeMelody)
open import MidiEvent    using (Channel-1; InstrumentNumber-1; MidiTrack; track; counterpoint→events; defaultVelocity)
open import ScaleDegree  using (ScaleDegreeOctave; scaleDegree; transposeScaleDegree; scaleDegreeToPitchClass)

cell : List (ScaleDegreeOctave 7)
cell = map (_, octave 3) (map (scaleDegree) (# 0 ∷ # 2 ∷ # 3 ∷ # 4 ∷ # 5 ∷ # 4 ∷ # 3 ∷ # 2 ∷ []))

0toN : ℕ → List ℕ
0toN zero    = 0 ∷ []
0toN (suc n) = 0toN n ++ (suc n) ∷ []

tcell : ℕ → List (ScaleDegreeOctave 7)
tcell n = map (transposeScaleDegree n) cell

half1scale : List (ScaleDegreeOctave 7)
half1scale = concat (map tcell (0toN 13))

half1pitches : List Pitch
half1pitches = map (relativeToAbsolute ∘ map₁ (scaleDegreeToPitchClass majorScale)) half1scale

half1bot half1top : Melody 224
half1bot = pitches→melody 8th (fromList half1pitches)
half1top = transposeMelody (+ 12) half1bot

hanon1 : Counterpoint 2 224
hanon1 = cp (fromList (half1bot ∷ half1top ∷ []))

----

instrument : InstrumentNumber-1
instrument = # 0 -- piano

channel : Channel-1
channel = # 0

tempo : ℕ
tempo = 180

hanonTrack : List MidiTrack
hanonTrack = track "Piano" instrument channel tempo (counterpoint→events defaultVelocity hanon1) ∷ []

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
open import Functional using (id)
import      Structure.Logic.Classical.NaturalDeduction

module Structure.Logic.Classical.SetTheory.Function {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} ⦃ classicLogic : _ ⦄ (_∈_ : Domain → Domain → Formula) where
open Structure.Logic.Classical.NaturalDeduction.ClassicalLogic {ℓₗ} {Formula} {ℓₘₗ} {Proof} {ℓₒ} {Domain} (classicLogic)

open import Syntax.Function
open import Structure.Logic.Classical.SetTheory.SetBoundedQuantification ⦃ classicLogic ⦄ (_∈_)
open import Structure.Logic.Constructive.Functions(Domain)
open import Structure.Logic.Constructive.Functions.Properties ⦃ constructiveLogicSignature ⦄

-- States whether the function f is defined for all elements in the set X.
Map : Function → Domain → Formula
Map f(X) = ∀ₛ(X) (x ↦ Defined f(x))


text:
module Pi.Category where
open import Categories.Category
open import Categories.Category.Groupoid
open import Categories.Category.Product
open import Categories.Functor.Bifunctor
open import Categories.Category.Monoidal
open import Categories.Category.Monoidal.Braided
open import Categories.Category.Monoidal.Symmetric
open import Categories.Category.RigCategory
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Sum
open import Data.Product
open import Data.Maybe
open import Relation.Binary.Core
open import Relation.Binary hiding (Symmetric)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_)
open import Base
open import Pi.Syntax
open import Pi.Opsem
open import Pi.Interp
open import Pi.Properties

Pi : Category _ _ _
Pi = record {
       Obj = 𝕌
     ; _⇒_ = _↔_
     ; _≈_ = λ c₁ c₂ → interp c₁ ∼ interp c₂
     ; id = id↔
     ; _∘_ = λ f g → g ⨾ f
     ; assoc = λ _ → refl
     ; sym-assoc = λ _ → refl
     ; identityˡ = λ _ → refl
     ; identityʳ = λ _ → refl
     ; identity² = λ _ → refl
     ; equiv = record { refl = λ _ → refl ;
                        sym = λ f~g x → sym (f~g x) ;
                        trans = λ f~g g~h x → trans (f~g x) (g~h x) }
     ; ∘-resp-≈ = λ {A} {B} {C} {f} {h} {g} {i} f~h g~i x → trans (cong (interp f) (g~i x))
                                                                  (f~h (interp i x))}

PiGroupoid : Groupoid _ _ _
PiGroupoid = record {
               category = Pi
             ; isGroupoid = record { _⁻¹ = !_
                                   ; iso = λ {A} {B} {c} →
                                             record { isoˡ = c⨾!c≡id↔ c
                                                    ; isoʳ = !c⨾c≡id↔ c}}}

Pi+Monoidal : Monoidal Pi
Pi+Monoidal = record {
                ⊗ = record {
                      F₀ = λ {(A , B) → A +ᵤ B}
                    ; F₁ = λ {(c₁ , c₂) → c₁ ⊕ c₂ }
                    ; identity = λ {(inj₁ x) → refl ; (inj₂ y) → refl}
                    ; homomorphism = λ {(inj₁ x) → refl ; (inj₂ y) → refl}
                    ; F-resp-≈ = λ { (f~h , g~i) (inj₁ x) → cong inj₁ (f~h x)
                                   ; (f~h , g~i) (inj₂ y) → cong inj₂ (g~i y)}}
              ; unit = 𝟘
              ; unitorˡ = record {
                            from = unite₊l
                          ; to = uniti₊l
                          ; iso = record { isoˡ = λ {(inj₂ y) → refl} ; isoʳ = λ x → refl}}
              ; unitorʳ = record {
                            from = unite₊r
                          ; to = uniti₊r
                          ; iso = record { isoˡ = λ {(inj₁ x) → refl} ; isoʳ = λ x → refl}}
              ; associator = record {
                               from = assocr₊
                             ; to = assocl₊
                             ; iso = record { isoˡ = λ {(inj₁ (inj₁ x)) → refl ; (inj₁ (inj₂ y)) → refl ; (inj₂ z) → refl}
                                            ; isoʳ = λ {(inj₁ x) → refl ; (inj₂ (inj₁ y)) → refl ; (inj₂ (inj₂ z)) → refl}}}
              ; unitorˡ-commute-from = λ {(inj₂ y) → refl}
              ; unitorˡ-commute-to = λ x → refl
              ; unitorʳ-commute-from = λ {(inj₁ x) → refl}
              ; unitorʳ-commute-to = λ x → refl
              ; assoc-commute-from = λ {(inj₁ (inj₁ x)) → refl ; (inj₁ (inj₂ y)) → refl ; (inj₂ z) → refl}
              ; assoc-commute-to = λ {(inj₁ x) → refl ; (inj₂ (inj₁ y)) → refl ; (inj₂ (inj₂ z)) → refl}
              ; triangle = λ {(inj₁ (inj₁ x)) → refl ; (inj₂ z) → refl}
              ; pentagon = λ {(inj₁ (inj₁ (inj₁ x))) → refl ;
                              (inj₁ (inj₁ (inj₂ y))) → refl ;
                              (inj₁ (inj₂ z)) → refl ;
                              (inj₂ w) → refl}}

Pi×Monoidal : Monoidal Pi
Pi×Monoidal = record {
                ⊗ = record {
                      F₀ = λ {(A , B) → A ×ᵤ B}
                    ; F₁ = λ {(c₁ , c₂) → c₁ ⊗ c₂ }
                    ; identity = λ {(x , y) → refl}
                    ; homomorphism = λ {(x , y) → refl}
                    ; F-resp-≈ = λ { {(A , B)} {(C , D)} {(f , g)} {(h , i)} (f~h , g~i) (x , y) →
                                     trans (cong ((interp f x ,_)) (g~i y)) (cong (_, (interp i y)) (f~h x))}}
              ; unit = 𝟙
              ; unitorˡ = record {
                            from = unite⋆l
                          ; to = uniti⋆l
                          ; iso = record { isoˡ = λ {(tt , x) → refl} ; isoʳ = λ x → refl}}
              ; unitorʳ = record {
                            from = unite⋆r
                          ; to = uniti⋆r
                          ; iso = record { isoˡ = λ {(x , tt) → refl} ; isoʳ = λ x → refl}}
              ; associator = record {
                               from = assocr⋆
                             ; to = assocl⋆
                             ; iso = record { isoˡ = λ {((x , y) , z) → refl} ; isoʳ = λ {(x , (y , z)) → refl}}}
              ; unitorˡ-commute-from = λ {(tt , x) → refl}
              ; unitorˡ-commute-to = λ x → refl
              ; unitorʳ-commute-from = λ {(x , tt) → refl}
              ; unitorʳ-commute-to = λ x → refl
              ; assoc-commute-from = λ {((x , y) , z) → refl}
              ; assoc-commute-to = λ {(x , (y , z)) → refl}
              ; triangle = λ {((x , tt) , y) → refl}
              ; pentagon = λ {(((x , y) , z) , w) → refl}}

Pi+Braided : Braided Pi+Monoidal
Pi+Braided = record {
               braiding = record { F⇒G = record { η = λ _ → swap₊
                                                ; commute = λ {(f , g) (inj₁ x) → refl;
                                                               (f , g) (inj₂ y) → refl}
                                                ; sym-commute = λ {(f , g) (inj₁ x) → refl;
                                                                   (f , g) (inj₂ y) → refl}}
                                 ; F⇐G = record { η = λ _ → swap₊
                                                ; commute = λ {(f , g) (inj₁ x) → refl;
                                                               (f , g) (inj₂ y) → refl}
                                                ; sym-commute = λ {(f , g) (inj₁ x) → refl;
                                                                   (f , g) (inj₂ y) → refl}}
                                 ; iso = λ (A , B) → record { isoˡ = λ {(inj₁ x) → refl ; (inj₂ y) → refl}
                                                            ; isoʳ = λ {(inj₁ x) → refl ; (inj₂ y) → refl}}}
             ; hexagon₁ = λ {(inj₁ (inj₁ x)) → refl ; (inj₁ (inj₂ y)) → refl ; (inj₂ z) → refl}
             ; hexagon₂ = λ {(inj₁ x) → refl ; (inj₂ (inj₁ y)) → refl ; (inj₂ (inj₂ z)) → refl}}

Pi×Braided : Braided Pi×Monoidal
Pi×Braided = record {
               braiding = record { F⇒G = record { η = λ _ → swap⋆
                                                ; commute = λ {(f , g) (x , y) → refl}
                                                ; sym-commute = λ {(f , g) (x , y) → refl}}
                                 ; F⇐G = record { η = λ _ → swap⋆
                                                ; commute = λ {(f , g) (x , y) → refl}
                                                ; sym-commute = λ {(f , g) (x , y) → refl}}
                                 ; iso = λ (A , B) → record { isoˡ = λ {(x , y) → refl}
                                                            ; isoʳ = λ {(x , y) → refl}}}
             ; hexagon₁ = λ {((x , y) , z) → refl}
             ; hexagon₂ = λ {(x , (y , z)) → refl}}

Pi+Symmetric : Symmetric Pi+Monoidal
Pi+Symmetric = record {
                 braided = Pi+Braided
               ; commutative = λ {(inj₁ x) → refl ; (inj₂ y) → refl}}

Pi×Symmetric : Symmetric Pi×Monoidal
Pi×Symmetric = record {
                 braided = Pi×Braided
               ; commutative = λ {(x , y) → refl}}

PiRig : RigCategory Pi Pi+Symmetric Pi×Symmetric
PiRig = record {
          annₗ = record { from = absorbr
                        ; to = factorzl
                        ; iso = record { isoˡ = λ () ; isoʳ = λ ()}}
        ; annᵣ = record { from = absorbl
                        ; to = factorzr
                        ; iso = record { isoˡ = λ () ; isoʳ = λ ()}}
        ; distribₗ = record { from = distl
                            ; to = factorl
                            ; iso = record { isoˡ = λ {(x , inj₁ y) → refl ; (x , inj₂ z) → refl}
                                           ; isoʳ = λ {(inj₁ (x , y)) → refl ; (inj₂ (x , z)) → refl}}}
        ; distribᵣ = record { from = dist
                            ; to = factor
                            ; iso = record { isoˡ = λ {(inj₁ x , z) → refl ; (inj₂ y , z) → refl}
                                           ; isoʳ = λ {(inj₁ (x , z)) → refl ; (inj₂ (y , z)) → refl}}}
        ; laplazaI = λ {(x , inj₁ y) → refl ; (x , inj₂ z) → refl}
        ; laplazaII = λ {(inj₁ x , z) → refl ; (inj₂ y , z) → refl}
        ; laplazaIV = λ {(inj₁ x , w) → refl ; (inj₂ (inj₁ y) , w) → refl ; (inj₂ (inj₂ z) , w) → refl}
        ; laplazaVI = λ {(x , (y , inj₁ z)) → refl ; (x , (y , inj₂ w)) → refl}
        ; laplazaIX = λ {(inj₁ x , inj₁ z) → refl ;
                         (inj₁ x , inj₂ w) → refl ;
                         (inj₂ y , inj₁ z) → refl ;
                         (inj₂ y , inj₂ w) → refl}
        ; laplazaX = λ ()
        ; laplazaXI = λ ()
        ; laplazaXIII = λ ()
        ; laplazaXV = λ ()
        ; laplazaXVI = λ ()
        ; laplazaXVII = λ ()
        ; laplazaXIX = λ {(x , inj₂ y) → refl}
        ; laplazaXXIII = λ {(tt , inj₁ x) → refl ; (tt , inj₂ y) → refl}}


text:
module type-util where
open import cedille-types
open import general-util
open import syntax-util

tmtp-to-arg : erased? → tmtp → arg
tmtp-to-arg ff (inj₁ t) = Arg t
tmtp-to-arg me = ArgE

tmtps-to-args : erased? → 𝕃 tmtp → args
tmtps-to-args = map ∘ tmtp-to-arg

tmtps-to-args-for-params : (keep-extra : maybe erased?) → params → 𝕃 tmtp → args
tmtps-to-args-for-params b (ParamTm _ _ :: ps) (inj₁ t :: as) =
   Arg t :: tmtps-to-args-for-params b ps as
tmtps-to-args-for-params b (_ :: ps) (tT :: as) =
  ArgE tT :: tmtps-to-args-for-params b ps as
tmtps-to-args-for-params nothing _ _ = []
tmtps-to-args-for-params (just me) _ as = tmtps-to-args me as

arg-to-tmtp : arg → tmtp
arg-to-tmtp a = a >>= id

args-to-tmtps : args → 𝕃 tmtp
args-to-tmtps = map arg-to-tmtp

params-to-args : params → args
params-to-args = map λ where
  (ParamTm v _) → Arg (Var v)
  (ParamEr v _) → ArgEr (Var v)
  (ParamTp v _) → ArgTp (TpVar v)

decompose-lams : term → (𝕃 var) × term
decompose-lams (Lam _ x _ t) with decompose-lams t
decompose-lams (Lam _ x _ t) | vs , body = (x :: vs) , body
decompose-lams t = [] , t

decompose-apps : term → term × args
decompose-apps = h [] where
  h : args → term → term × args
  h acc (App t t') = h (Arg t' :: acc) t
  h acc (AppE t tT) = h (ArgE tT :: acc) t
  h acc t = t , acc

decompose-tpapps : type → type × 𝕃 tmtp
decompose-tpapps = h [] where
  h : 𝕃 tmtp → type → type × 𝕃 tmtp
  h acc (TpApp T tT) = h (tT :: acc) T
  h acc T = T , acc

decompose-var-headed : term → maybe (var × args)
decompose-var-headed t with decompose-apps t
decompose-var-headed t | Var x , as = just (x , as)
decompose-var-headed t | _ = nothing

decompose-tpvar-headed : type → maybe (var × 𝕃 tmtp)
decompose-tpvar-headed T with decompose-tpapps T
decompose-tpvar-headed T | TpVar x , as = just (x , as)
decompose-tpvar-headed T | _ = nothing

recompose-apps : args → term → term
recompose-apps = flip $ foldl λ a t → either-else' a (App t) (AppE t)

recompose-tpapps : 𝕃 tmtp → type → type
recompose-tpapps = flip $ foldl $ flip TpApp

apps-term : term → args → term
apps-term = flip recompose-apps

apps-type : type → args → type
apps-type = foldl $ flip TpApp ∘ arg-to-tmtp

lam-expand-term : params → term → term
lam-expand-term = flip $ foldr λ where
  (Param me x atk) → Lam me x (just atk)

lam-expand-type : params → type → type
lam-expand-type = flip $ foldr λ where
  (Param me x atk) → TpLam x atk

abs-expand-type : params → type → type
abs-expand-type = flip $ foldr λ where
  (Param me x atk) → TpAbs me x atk

abs-expand-kind : params → kind → kind
abs-expand-kind = flip $ foldr λ where
  (Param me x atk) → KdAbs x atk

case-args-to-lams : case-args → term → term
case-args-to-lams = flip $ foldr λ where
  (CaseArg me x atk) → Lam me x atk

expand-case : case → term
expand-case (Case x xs t T) = case-args-to-lams xs t

is-eq-tp? : {ed : exprd} → ⟦ ed ⟧ → maybe (term × term)
is-eq-tp? {TYPE} (TpEq t₁ t₂) = just $ t₁ , t₂
is-eq-tp? _ = nothing

arg-set-erased : erased? → arg → arg
arg-set-erased tt (Arg t) = ArgEr t
arg-set-erased ff (ArgEr t) = Arg t
arg-set-erased e a = a

is-var : tmtp → maybe var
is-var (Ttm (Var x)) = just x
is-var (Ttp (TpVar x)) = just x
is-var _ = nothing

arg-var : arg → maybe var
arg-var = either-else (is-var ∘ Ttm) is-var

is-var-unqual : tmtp → maybe var
is-var-unqual = maybe-map (λ x → maybe-else (unqual-local x) id (var-suffix x)) ∘ is-var

unerased-arrows : type → ℕ
unerased-arrows (TpAbs ff x atk T) = suc (unerased-arrows T)
unerased-arrows (TpAbs tt x atk T) = unerased-arrows T
unerased-arrows _ = zero

lterms-to-term : theta → ex-tm → 𝕃 lterm → ex-tm
lterms-to-term AbstractEq t [] = ExApp t Erased (ExBeta (term-end-pos t) nothing nothing)
lterms-to-term _ t [] = t
lterms-to-term θ t (Lterm e t' :: ls) = lterms-to-term θ (ExApp t e t') ls

is-hole : ∀ {ed} → ⟦ ed ⟧ → 𝔹
is-hole {TERM} (Hole pi) = tt
is-hole {TYPE} (TpHole pi) = tt
is-hole {KIND} (KdHole pi) = tt
is-hole _ = ff

data datatype : Set where
  Data : var → params → indices → ctrs → datatype

tk-erased : tpkd → erased? → erased?
tk-erased (Tkk _) me = Erased
tk-erased (Tkt _) me = me

params-set-erased : erased? → params → params
params-set-erased me = map λ where
  (Param me' x atk) → Param me x atk

args-set-erased : erased? → args → args
args-set-erased = map ∘ arg-set-erased

indices-to-params : indices → params
indices-to-params = map λ where
  (Index x tk) → Param ff x tk

params-to-indices : params → indices
params-to-indices = map λ where
  (Param me x tk) → Index x tk

indices-to-tmtps : indices → 𝕃 tmtp
indices-to-tmtps = map λ where
  (Index x (Tkt T)) → Ttm (Var x)
  (Index x (Tkk k)) → Ttp (TpVar x)

indices-to-kind : indices → kind → kind
indices-to-kind = flip $ foldr λ {(Index x atk) → KdAbs x atk}

params-to-kind : params → kind → kind
params-to-kind = flip $ foldr λ {(Param me x atk) → KdAbs x atk}

indices-to-tplams : indices → (body : type) → type
indices-to-tplams = flip $ foldr λ where
  (Index x atk) → TpLam x atk

params-to-tplams : params → (body : type) → type
params-to-tplams = flip $ foldr λ where
  (Param me x atk) → TpLam x atk

indices-to-alls : indices → (body : type) → type
indices-to-alls = flip $ foldr λ where
  (Index x atk) → TpAbs Erased x atk

params-to-alls : params → (body : type) → type
params-to-alls = flip $ foldr λ where
  (Param me x atk) → TpAbs (tk-erased atk me) x atk

indices-to-lams : indices → (body : term) → term
indices-to-lams = flip $ foldr λ where
  (Index x atk) → Lam Erased x (just atk)

params-to-lams : params → (body : term) → term
params-to-lams = flip $ foldr λ where
  (Param me x atk) → Lam (tk-erased atk me) x (just atk)

indices-to-apps : indices → (body : term) → term
indices-to-apps = flip $ foldl λ where
  (Index x (Tkt T)) t → AppEr t (Var x)
  (Index x (Tkk k)) t → AppTp t (TpVar x)

params-to-apps : params → (body : term) → term
params-to-apps = recompose-apps ∘ params-to-args

indices-to-tpapps : indices → (body : type) → type
indices-to-tpapps = flip $ foldl λ where
  (Index x (Tkt _)) T → TpAppTm T (Var x)
  (Index x (Tkk _)) T → TpAppTp T (TpVar x)

params-to-tpapps : params → (body : type) → type
params-to-tpapps = flip apps-type ∘ params-to-args

params-to-case-args : params → case-args
params-to-case-args = map λ where
  (Param me x tk) → CaseArg me x (just tk)

ctrs-to-lams : ctrs → term → term
ctrs-to-lams = flip $ foldr λ {(Ctr x T) → Lam NotErased x (just (Tkt T))}

max_stars_repo_name: zmthy/cedille

max_issues_repo_name: zmthy/cedille

max_forks_repo_name: zmthy/cedille