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

data _==_ {i} {A : Set i} : (x y : A) → Set i where
  refl : {a : A} → a == a

{-# BUILTIN REWRITE _==_ #-}

data ⊥ : Set where

record ⊤ : Set where
  constructor tt

module Test (p : ⊥ == ⊤) where
  abstract
    A : Set
    A = ⊥

    q : A == ⊤
    q = p

    {-# REWRITE q #-}

  f : A
  f = tt

  abstract
    g : ⊥
    g = f
    -- g reduces to tt, which does not have type ⊥.

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module interfaceExtensionAndDelegation where

open import Data.Product
open import Data.Nat.Base
open import Data.Nat.Show
open import Data.String.Base using (String; _++_)
open import Size
open import NativeIO
open import interactiveProgramsAgda using (ConsoleInterface; _>>=_; do;
                                           IO; return; putStrLn;
                                           translateIOConsole )
open import objectsInAgda using (Interface; Method; Result; CellMethod;
                                 get; put; CellResult; cellI; IOObject;
                                 CellC; method; simpleCell )

data CounterMethod A : Set where
  super  :  (m : CellMethod A) → CounterMethod A
  stats  :  CounterMethod A

statsCellI : (A : Set) → Interface
Method  (statsCellI A)            =  CounterMethod A
Result  (statsCellI A) (super m)  =  Result (cellI A) m
Result  (statsCellI A) stats      =  Unit

CounterC : (i : Size) → Set
CounterC = IOObject ConsoleInterface (statsCellI String)

pattern getᶜ    = super get
pattern putᶜ x  = super (put x)

{- Methods of CounterC are now
   getᶜ  (putᶜ x)   stats
-}

counterCell : ∀{i} (c : CellC i) (ngets nputs : ℕ) → CounterC i
method (counterCell c ngets nputs) getᶜ =
  method c get                                >>= λ { (s , c') →
  return (s , counterCell c' (1 + ngets) nputs)  }

method (counterCell c ngets nputs) (putᶜ x) =
  method c (put x)                            >>= λ { (_ , c') →
  return (_ , counterCell c' ngets (1 + nputs))  }

method (counterCell c ngets nputs) stats =
  do (putStrLn ("Counted "
    ++ show ngets ++ " calls to get and "
    ++ show nputs ++ " calls to put."))       λ _ →
  return (_ , counterCell c ngets nputs)

program : String → IO ConsoleInterface ∞ Unit
program arg =
  let c₀ = counterCell (simpleCell "Start") 0 0 in
  method c₀ getᶜ               >>= λ{ (s   , c₁) →
  do (putStrLn s)              λ _ →
  method c₁ (putᶜ arg)         >>= λ{ (_        , c₂) →
  method c₂ getᶜ               >>= λ{ (s'  , c₃) →
  do (putStrLn s')             λ _ →
  method c₃ (putᶜ "Over!")     >>= λ{ (_ , c₄) →
  method c₄ stats              >>= λ{ (_ , c₅) →
  return _                     }}}}}

main : NativeIO Unit
main = translateIOConsole (program "Hello")

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


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

module Integer.Univalence where

open import Cubical.Foundations.NTypes
open import Data.Empty
open import Data.Product as Σ
open import Data.Product.Relation.Pointwise.NonDependent
open import Data.Unit
open import Equality
open import Function
open import Integer.Difference as D
open import Integer.Signed as S
open import Natural as ℕ
open import Quotient as /
open import Syntax
open import Relation.Nullary

zero≢suc : ∀ {m} → ¬ (zero ≡ suc m)
zero≢suc p = case ⟪ p ⟫ of λ ()

⟦D→S⟧ : D.⟦ℤ⟧ → S.⟦ℤ⟧
⟦D→S⟧ (a – zero) = +1* a
⟦D→S⟧ (zero – b) = -1* b
⟦D→S⟧ (suc a – suc b) = ⟦D→S⟧ (a – b)

D→S : D.ℤ → S.ℤ
D→S = ⟦D→S⟧ // line
  where
    line : ∀ x y → x D.≈ y → ⟦D→S⟧ x S.≈ ⟦D→S⟧ y
    line (zero – zero) (zero – zero) p = refl
    line (zero – zero) (zero – suc d) p = refl , p
    line (zero – zero) (suc c – zero) p = compPath p (cong suc ⟨ +-identityʳ c ⟩)
    line (zero – b) (suc c – suc d) p = line (zero – b) (c – d) ⟨ suc-injective ⟪ p ⟫ ⟩
    line (suc a – suc b) (zero – d) p = line (a – b) (zero – d) ⟨ suc-injective ⟪ p ⟫ ⟩
    line (zero – suc b) (zero – zero) p = sym p , refl
    line (zero – suc b) (zero – suc d) p = sym p
    line (zero – suc b) (suc c – zero) p = case ⟪ p ⟫ of λ ()
    line (suc a – zero) (zero – d) p = case ⟪ p ⟫ of λ ()
    line (suc a – zero) (suc c – zero) p =
        suc a
      ≡⟨ cong suc (sym ⟨ +-identityʳ a ⟩) ⟩
        suc (a + 0)
      ≡⟨ p ⟩
        suc (c + 0)
      ≡⟨ cong suc ⟨ +-identityʳ c ⟩ ⟩
        suc c
      ∎
    line (suc a – b) (suc c – suc d) p =
      line (suc a – b) (c – d)
        ⟨ suc-injective ⟪ compPath (cong suc (sym (+-suc a d))) p ⟫ ⟩
    line (suc a – suc b) (suc c – d) p =
      line (a – b) (suc c – d)
        ⟨ suc-injective ⟪ compPath p (cong suc (+-suc c b)) ⟫ ⟩

⟦S→D⟧ : S.⟦ℤ⟧ → D.⟦ℤ⟧
⟦S→D⟧ (+1* a) = a – zero
⟦S→D⟧ (-1* a) = zero – a

⟦D→S→D⟧ : ∀ x → ⟦S→D⟧ (⟦D→S⟧ x) D.≈ x
⟦D→S→D⟧ (zero – zero) = refl
⟦D→S→D⟧ (zero – suc b) = refl
⟦D→S→D⟧ (suc a – zero) = refl
⟦D→S→D⟧ (suc a – suc b) =
  let m , n = ⟦S→D⟧ (⟦D→S⟧ (a – b)) in
      m + suc b
    ≡⟨ +-suc m b ⟩
      suc (m + b)
    ≡⟨ cong suc (⟦D→S→D⟧ (a – b)) ⟩
      suc (a + n)
    ∎

⟦S→D→S⟧ : ∀ x → ⟦D→S⟧ (⟦S→D⟧ x) S.≈ x
⟦S→D→S⟧ (+1* x) = refl
⟦S→D→S⟧ (-1* zero) = refl , refl
⟦S→D→S⟧ (-1* suc x) = refl

cong-⟦S→D⟧ : ∀ x y → x S.≈ y → ⟦S→D⟧ x D.≈ ⟦S→D⟧ y
cong-⟦S→D⟧ (+1* x) (+1* y) = cong (_+ zero)
cong-⟦S→D⟧ (-1* x) (-1* y) = sym
cong-⟦S→D⟧ (+1* x) (-1* y) = Σ.uncurry (cong₂ _+_)
cong-⟦S→D⟧ (-1* x) (+1* y) (p , q) = compPath (sym (cong₂ _+_ p q)) ⟨ +-comm x y ⟩

cong-⟦D→S⟧ : ∀ x y → x D.≈ y → ⟦D→S⟧ x S.≈ ⟦D→S⟧ y
cong-⟦D→S⟧ (zero – zero) (zero – zero) p = refl
cong-⟦D→S⟧ (zero – zero) (zero – suc d) p = refl , p
cong-⟦D→S⟧ (zero – zero) (suc c – zero) p = compPath p (cong suc ⟨ +-identityʳ c ⟩)
cong-⟦D→S⟧ (zero – b) (suc c – suc d) p = cong-⟦D→S⟧ (zero – b) (c – d) ⟨ suc-injective ⟪ p ⟫ ⟩
cong-⟦D→S⟧ (suc a – suc b) (zero – d) p = cong-⟦D→S⟧ (a – b) (zero – d) ⟨ suc-injective ⟪ p ⟫ ⟩
cong-⟦D→S⟧ (zero – suc b) (zero – zero) p = sym p , refl
cong-⟦D→S⟧ (zero – suc b) (zero – suc d) p = sym p
cong-⟦D→S⟧ (zero – suc b) (suc c – zero) p = case ⟪ p ⟫ of λ ()
cong-⟦D→S⟧ (suc a – zero) (zero – d) p = case ⟪ p ⟫ of λ ()
cong-⟦D→S⟧ (suc a – zero) (suc c – zero) p =
    suc a
  ≡⟨ cong suc (sym ⟨ +-identityʳ a ⟩) ⟩
    suc (a + 0)
  ≡⟨ p ⟩
    suc (c + 0)
  ≡⟨ cong suc ⟨ +-identityʳ c ⟩ ⟩
    suc c
  ∎
cong-⟦D→S⟧ (suc a – b) (suc c – suc d) p =
  cong-⟦D→S⟧ (suc a – b) (c – d)
    ⟨ suc-injective ⟪ compPath (cong suc (sym (+-suc a d))) p ⟫ ⟩
cong-⟦D→S⟧ (suc a – suc b) (suc c – d) p =
  cong-⟦D→S⟧ (a – b) (suc c – d)
    ⟨ suc-injective ⟪ compPath p (cong suc (+-suc c b)) ⟫ ⟩

Signed≡Difference : S.ℤ ≡ D.ℤ
Signed≡Difference = ua (isoToEquiv ⟦S→D⟧ ⟦D→S⟧ cong-⟦S→D⟧ cong-⟦D→S⟧ ⟦S→D→S⟧ ⟦D→S→D⟧)


text:
postulate anything : ∀{a}{A : Set a} → A

data N : Set where
  suc : (n : N) → N

data Val : (n : N) → Set where
  valSuc : (n : N) → Val (suc n)
--  valSuc : (n : N) → Val n -- internal error disappears

Pred : Set₁
Pred = (n : N) → Set

postulate
  Any  : (P : Pred) → Set
  F    : (P : Pred) → Pred
  anyF : {P : Pred} (S : Any P) → Any (F P)

Evaluate : ∀ (n : N) (P : (w : Val n) → Set) → Set
Evaluate n P = P anything

LR : (n : N) → Pred
LR n m = Evaluate n λ { (valSuc _) → anything}

anyLR : {n : N} → Any (LR n)
anyLR = anyF anything

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

-- The 'Identity' instance, with all of Setoids as models

module Categories.Theory.Lawvere.Instance.Identity where

open import Data.Fin using (splitAt)
open import Data.Sum using ([_,_]′)
open import Data.Unit.Polymorphic using (⊤; tt)
open import Level
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; isEquivalence)

open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
open import Categories.Category.Core using (Category)
open import Categories.Category.Instance.Nat
open import Categories.Category.Unbundled.Properties using (unpack′)
open import Categories.Functor.IdentityOnObjects using (id-IOO)
open import Categories.Object.Product using (Product)
open import Categories.Theory.Lawvere using (LawvereTheory)

Identity : LawvereTheory 0ℓ 0ℓ
Identity = record
  { L = unpack′ (Category.op Nat)
  ; T = CartesianCategory.cartesian Natop-Cartesian
  ; I = id-IOO
  ; CartF = record
    { F-resp-⊤ = record { ! = λ () ; !-unique = λ _ () }
    ; F-resp-× = λ {m} {n} → record { P m n }
    }
  }
  where
  module P m n = Product Natop (Natop-Product m n)

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
-- Andreas, 2016-11-02, issue #2285
-- double check for record types

record Big : _ where
  field any : ∀{a} → Set a


text:
{-# OPTIONS --allow-unsolved-metas
            --no-positivity-check
            --no-termination-check
            --type-in-type
            --sized-types
            --injective-type-constructors
            --guardedness-preserving-type-constructors
            --experimental-irrelevance #-}
module SafeFlagPragmas where


text:
-- Andreas, 2020-09-26, issue #4944.
-- Size solver got stuck on projected variables which are left over
-- in some size constraints by the generalization feature.

-- {-# OPTIONS --sized-types #-}
-- {-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.conv.size:60 -v tc.size:30 -v tc.meta.assign:10 #-}

open import Agda.Builtin.Size

variable
  i : Size

postulate
  A : Set

data ListA (i : Size) : Set where
  nil   : ListA i
  cons  : (j : Size< i) (t : A) (as : ListA j) → ListA i

postulate
  node : A → ListA ∞ → A
  R    : (i : Size) (as as′ : ListA i) → Set

  test : -- {i : Size} -- made error vanish
         (t u : A) (as : ListA i) →
         R (↑ (↑ i)) (cons (↑ i) t (cons i u as)) (cons _ (node t (cons _ u nil)) as)

variable
  t u : A
  as : ListA i

postulate
  tst2 : R _ (cons _ t (cons _ u as)) (cons _ (node t (cons _ u nil)) as)

-- Should pass.

max_forks_repo_name: shlevy/agda


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

module ConcretePermutation where

import Level using (zero)

open import Data.Nat using (ℕ; _+_; _*_)
open import Data.Fin using (Fin)
open import Data.Product using (proj₁; proj₂)
open import Data.Vec using (tabulate)

open import Algebra using (CommutativeSemiring)
open import Algebra.Structures using
  (IsSemigroup; IsCommutativeMonoid; IsCommutativeSemiring)

open import Relation.Binary using (IsEquivalence)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; cong; cong₂; module ≡-Reasoning)

open import Equiv using (_≃_; sym≃;p∘!p≡id)
--

open import FinVec
  using (FinVec; 1C; _∘̂_; _⊎c_; _×c_;
         unite+; uniti+;
         unite+r; uniti+r;
         assocl+; assocr+;
         swap+cauchy;
         unite*; uniti*;
         unite*r; uniti*r;
         assocl*; assocr*;
         swap⋆cauchy;
         dist*+; factor*+;
         distl*+; factorl*+;
         right-zero*l; right-zero*r)

open import FinVecProperties
  using (∘̂-assoc; ∘̂-lid; ∘̂-rid;
         ~⇒≡;
         1C⊎1C≡1C; 1C×1C≡1C; 1C₀⊎x≡x;
         ⊎c-distrib; ×c-distrib;
         unite+∘̂uniti+~id; uniti+∘̂unite+~id;
         unite+r∘̂uniti+r~id; uniti+r∘̂unite+r~id;
         assocl+∘̂assocr+~id; assocr+∘̂assocl+~id;
         swap+-inv;
         unite*∘̂uniti*~id; uniti*∘̂unite*~id;
         unite*r∘̂uniti*r~id; uniti*r∘̂unite*r~id;
         assocl*∘̂assocr*~id; assocr*∘̂assocl*~id;
         swap*-inv;
         dist*+∘̂factor*+~id; factor*+∘̂dist*+~id;
         distl*+∘̂factorl*+~id; factorl*+∘̂distl*+~id;
         right-zero*l∘̂right-zero*r~id; right-zero*r∘̂right-zero*l~id)

------------------------------------------------------------------------------
-- A concrete permutation has 4 components:
-- - the one-line notation for a permutation
-- - the one-line notation for the inverse permutation
-- - and 2 proofs that these are indeed inverses

record CPerm (values : ℕ) (size : ℕ) : Set where
  constructor cp
  field
    π  : FinVec values size
    πᵒ : FinVec size values
    αp : π ∘̂ πᵒ ≡ 1C
    βp : πᵒ ∘̂ π ≡ 1C

------------------------------------------------------------------------------
-- Now the goal is to prove that CPerm m n is a commutative semiring
-- (including symmetry now)

-- First it is an equivalence relation

idp : ∀ {n} → CPerm n n
idp {n} = cp 1C 1C (∘̂-rid _) (∘̂-lid _)

symp : ∀ {m n} → CPerm m n → CPerm n m
symp (cp p₁ p₂ α β) = cp p₂ p₁ β α

transp : ∀ {m₁ m₂ m₃} → CPerm m₂ m₁ → CPerm m₃ m₂ → CPerm m₃ m₁
transp {n} (cp π πᵒ αp βp) (cp π₁ πᵒ₁ αp₁ βp₁) = cp (π ∘̂ π₁) (πᵒ₁ ∘̂ πᵒ) pf₁ pf₂
  where
    open ≡-Reasoning
    pf₁ : (π ∘̂ π₁) ∘̂ (πᵒ₁ ∘̂ πᵒ) ≡ 1C
    pf₁ =
      begin (
        (π ∘̂ π₁) ∘̂ (πᵒ₁ ∘̂ πᵒ) ≡⟨ ∘̂-assoc _ _ _ ⟩
        ((π ∘̂ π₁) ∘̂ πᵒ₁) ∘̂ πᵒ ≡⟨ cong (λ x → x ∘̂ πᵒ) (sym (∘̂-assoc _ _ _)) ⟩
        (π ∘̂ (π₁ ∘̂ πᵒ₁)) ∘̂ πᵒ ≡⟨ cong (λ x → (π ∘̂ x) ∘̂ πᵒ) (αp₁) ⟩
        (π ∘̂ 1C) ∘̂ πᵒ         ≡⟨ cong (λ x → x ∘̂ πᵒ) (∘̂-rid _) ⟩
        π ∘̂ πᵒ                ≡⟨ αp ⟩
        1C ∎)
    pf₂ : (πᵒ₁ ∘̂ πᵒ) ∘̂ (π ∘̂ π₁) ≡ 1C
    pf₂ =
      begin (
        (πᵒ₁ ∘̂ πᵒ) ∘̂ (π ∘̂ π₁) ≡⟨ ∘̂-assoc _ _ _ ⟩
        ((πᵒ₁ ∘̂ πᵒ) ∘̂ π) ∘̂ π₁ ≡⟨ cong (λ x → x ∘̂ π₁) (sym (∘̂-assoc _ _ _)) ⟩
        (πᵒ₁ ∘̂ (πᵒ ∘̂ π)) ∘̂ π₁ ≡⟨ cong (λ x → (πᵒ₁ ∘̂ x) ∘̂ π₁) βp ⟩
        (πᵒ₁ ∘̂ 1C) ∘̂ π₁       ≡⟨ cong (λ x → x ∘̂ π₁) (∘̂-rid _) ⟩
         πᵒ₁ ∘̂ π₁             ≡⟨ βp₁ ⟩
        1C ∎)

-- units
-- zero permutation

0p : CPerm 0 0
0p = idp {0}

-- Additive monoid

_⊎p_ : ∀ {m₁ m₂ n₁ n₂} → CPerm m₁ m₂ → CPerm n₁ n₂ → CPerm (m₁ + n₁) (m₂ + n₂)
_⊎p_ {m₁} {m₂} {n₁} {n₂} π₀ π₁ =
  cp ((π π₀) ⊎c (π π₁)) ((πᵒ π₀) ⊎c (πᵒ π₁)) pf₁ pf₂
  where
    open CPerm
    open ≡-Reasoning
    pf₁ : (π π₀ ⊎c π π₁) ∘̂ (πᵒ π₀ ⊎c πᵒ π₁) ≡ 1C
    pf₁ =
      begin (
        (π π₀ ⊎c π π₁) ∘̂ (πᵒ π₀ ⊎c πᵒ π₁)
          ≡⟨ ⊎c-distrib {p₁ = π π₀} ⟩
       (π π₀ ∘̂ πᵒ π₀) ⊎c (π π₁ ∘̂ πᵒ π₁)
          ≡⟨ cong₂ _⊎c_ (αp π₀) (αp π₁) ⟩
        1C {m₂} ⊎c 1C {n₂}
          ≡⟨ 1C⊎1C≡1C {m₂} ⟩
        1C ∎)
    pf₂ : (πᵒ π₀ ⊎c πᵒ π₁) ∘̂ (π π₀ ⊎c π π₁) ≡ 1C
    pf₂ =
      begin (
        (πᵒ π₀ ⊎c πᵒ π₁) ∘̂ (π π₀ ⊎c π π₁)
          ≡⟨ ⊎c-distrib {p₁ = πᵒ π₀} ⟩
        (πᵒ π₀ ∘̂ π π₀) ⊎c (πᵒ π₁ ∘̂ π π₁)
          ≡⟨ cong₂ _⊎c_ (βp π₀) (βp π₁) ⟩
        1C {m₁} ⊎c 1C {n₁}
          ≡⟨ 1C⊎1C≡1C {m₁} ⟩
        1C ∎ )

-- For the rest of the permutations, it is convenient to lift things from
-- FinVec in one go
mkPerm : {m n : ℕ} → (Fin m ≃ Fin n) → CPerm m n
mkPerm {m} {n} eq = cp p q p∘̂q≡1 q∘̂p≡1
  where
    f = proj₁ eq
    g = proj₁ (sym≃ eq)
    p = tabulate g -- note the flip!
    q = tabulate f
    q∘̂p≡1 = ~⇒≡ {f = g} {g = f} (p∘!p≡id {p = eq})
    p∘̂q≡1 = ~⇒≡ {f = f} {g = g} (p∘!p≡id {p = sym≃ eq})

-- units

unite+p : {m : ℕ} → CPerm m (0 + m)
unite+p {m} =
  cp (unite+ {m}) (uniti+ {m}) (unite+∘̂uniti+~id {m}) (uniti+∘̂unite+~id {m})

uniti+p : {m : ℕ} → CPerm (0 + m) m
uniti+p {m} = symp (unite+p {m})

unite+rp : {m : ℕ} → CPerm m (m + 0)
unite+rp {m} =
  cp (unite+r {m}) (uniti+r) (unite+r∘̂uniti+r~id) (uniti+r∘̂unite+r~id)

uniti+rp : {m : ℕ} → CPerm (m + 0) m
uniti+rp {m} = symp (unite+rp {m})

-- commutativity

swap+p : {m n : ℕ} → CPerm (n + m) (m + n)
swap+p {m} {n} =
  cp (swap+cauchy m n) (swap+cauchy n m) (swap+-inv {m}) (swap+-inv {n})

-- associativity

assocl+p : {m n o : ℕ} → CPerm ((m + n) + o) (m + (n + o))
assocl+p {m} =
  cp
    (assocl+ {m}) (assocr+ {m})
    (assocl+∘̂assocr+~id {m}) (assocr+∘̂assocl+~id {m})

assocr+p : {m n o : ℕ} → CPerm (m + (n + o)) ((m + n) + o)
assocr+p {m} = symp (assocl+p {m})

-- Multiplicative monoid

_×p_ : ∀ {m₁ m₂ n₁ n₂} → CPerm m₁ m₂ → CPerm n₁ n₂ → CPerm (m₁ * n₁) (m₂ * n₂)
_×p_ {m₁} {m₂} {n₁} {n₂} π₀ π₁ =
  cp ((π π₀) ×c (π π₁)) ((πᵒ π₀) ×c (πᵒ π₁)) pf₁ pf₂
  where
    open CPerm
    open ≡-Reasoning
    pf₁ : (π π₀ ×c π π₁) ∘̂ (πᵒ π₀ ×c πᵒ π₁) ≡ 1C
    pf₁ =
      begin (
        (π π₀ ×c π π₁) ∘̂ (πᵒ π₀ ×c πᵒ π₁) ≡⟨ ×c-distrib {p₁ = π π₀} ⟩
        (π π₀ ∘̂ πᵒ π₀) ×c (π π₁ ∘̂ πᵒ π₁)  ≡⟨ cong₂ _×c_ (αp π₀) (αp π₁) ⟩
        1C ×c 1C                          ≡⟨ 1C×1C≡1C ⟩
        1C ∎)
    pf₂ : (πᵒ π₀ ×c πᵒ π₁) ∘̂ (π π₀ ×c π π₁) ≡ 1C
    pf₂ =
      begin (
        (πᵒ π₀ ×c πᵒ π₁) ∘̂ (π π₀ ×c π π₁) ≡⟨ ×c-distrib {p₁ = πᵒ π₀} ⟩
        (πᵒ π₀ ∘̂ π π₀) ×c (πᵒ π₁ ∘̂ π π₁) ≡⟨ cong₂ _×c_ (βp π₀) (βp π₁) ⟩
        1C ×c 1C                          ≡⟨ 1C×1C≡1C ⟩
        1C ∎)

-- units

unite*p : {m : ℕ} → CPerm m (1 * m)
unite*p {m} =
  cp (unite* {m}) (uniti* {m}) (unite*∘̂uniti*~id {m}) (uniti*∘̂unite*~id {m})

uniti*p : {m : ℕ} → CPerm (1 * m) m
uniti*p {m} = symp (unite*p {m})

unite*rp : {m : ℕ} → CPerm m (m * 1)
unite*rp {m} =
  cp
    (unite*r {m}) (uniti*r {m})
    (unite*r∘̂uniti*r~id {m}) (uniti*r∘̂unite*r~id {m})

uniti*rp : {m : ℕ} → CPerm (m * 1) m
uniti*rp {m} = symp (unite*rp {m})

-- commutativity

swap*p : {m n : ℕ} → CPerm (n * m) (m * n)
swap*p {m} {n} =
  cp (swap⋆cauchy m n) (swap⋆cauchy n m) (swap*-inv {m}) (swap*-inv {n})

-- associativity

assocl*p : {m n o : ℕ} → CPerm ((m * n) * o) (m * (n * o))
assocl*p {m} =
  cp
    (assocl* {m}) (assocr* {m})
    (assocl*∘̂assocr*~id {m}) (assocr*∘̂assocl*~id {m})

assocr*p : {m n o : ℕ} → CPerm (m * (n * o)) ((m * n) * o)
assocr*p {m} = symp (assocl*p {m})

-- Distributivity

-- right-zero absorbing permutation

0pr : ∀ {n} → CPerm 0 (n * 0)
0pr {n} =
  cp
    (right-zero*l {n}) (right-zero*r {n})
    (right-zero*l∘̂right-zero*r~id {n}) (right-zero*r∘̂right-zero*l~id {n})

-- and its symmetric version

0pl : ∀ {n} → CPerm (n * 0) 0
0pl {n} = symp (0pr {n})

distp : {m n o : ℕ} → CPerm (m * o + n * o) ((m + n) * o)
distp {m} {n} {o} =
  cp
    (dist*+ {m}) (factor*+ {m})
    (dist*+∘̂factor*+~id {m}) (factor*+∘̂dist*+~id {m})

factorp : {m n o : ℕ} → CPerm ((m + n) * o) (m * o + n * o)
factorp {m} = symp (distp {m})

distlp : {m n o : ℕ} → CPerm (m * n + m * o) (m * (n + o))
distlp {m} {n} {o} =
  cp
    (distl*+ {m}) (factorl*+ {m})
    (distl*+∘̂factorl*+~id {m}) (factorl*+∘̂distl*+~id {m})

factorlp : {m n o : ℕ} → CPerm (m * (n + o)) (m * n + m * o)
factorlp {m} = symp (distlp {m})

------------------------------------------------------------------------------
-- Commutative semiring structure

cpermIsEquiv : IsEquivalence {Level.zero} {Level.zero} {ℕ} CPerm
cpermIsEquiv = record {
  refl = idp;
  sym = symp;
  trans = λ p q → transp q p
  }

cpermPlusIsSG : IsSemigroup {Level.zero} {Level.zero} {ℕ} CPerm _+_
cpermPlusIsSG = record {
  isEquivalence = cpermIsEquiv ;
  assoc = λ m n o → assocl+p {m} {n} {o} ;
  ∙-cong = _⊎p_
  }

cpermTimesIsSG : IsSemigroup {Level.zero} {Level.zero} {ℕ} CPerm _*_
cpermTimesIsSG = record {
  isEquivalence = cpermIsEquiv ;
  assoc = λ m n o → assocl*p {m} {n} {o} ;
  ∙-cong = _×p_
  }

cpermPlusIsCM : IsCommutativeMonoid CPerm _+_ 0
cpermPlusIsCM = record {
  isSemigroup = cpermPlusIsSG ;
  identityˡ = λ m → idp ;
  comm = λ m n → swap+p {n} {m}
  }

cpermTimesIsCM : IsCommutativeMonoid CPerm _*_ 1
cpermTimesIsCM = record {
  isSemigroup = cpermTimesIsSG ;
  identityˡ = λ m → uniti*p {m} ;
  comm = λ m n → swap*p {n} {m}
  }

cpermIsCSR : IsCommutativeSemiring CPerm _+_ _*_ 0 1
cpermIsCSR = record {
  +-isCommutativeMonoid = cpermPlusIsCM ;
  *-isCommutativeMonoid = cpermTimesIsCM ;
  distribʳ = λ o m n → factorp {m} {n} {o} ;
  zeroˡ = λ m → 0p
  }

cpermCSR : CommutativeSemiring Level.zero Level.zero
cpermCSR = record {
  Carrier = ℕ ;
  _≈_ = CPerm;
  _+_ = _+_ ;
  _*_ = _*_ ;
  0# = 0 ;
  1# = 1 ;
  isCommutativeSemiring = cpermIsCSR
  }

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

open import Light.Library.Data.Natural as ℕ using (ℕ)
open import Light.Package using (Package)

module Light.Literals.Natural ⦃ package : Package record { ℕ } ⦄ where

open import Light.Literals.Definition.Natural using (FromNatural)
open FromNatural using (convert)

instance from‐natural : FromNatural ℕ
convert from‐natural n = n

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Decorated star-lists
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module Data.Star.Decoration where

open import Data.Unit
open import Function
open import Level
open import Relation.Binary
open import Relation.Binary.Construct.Closure.ReflexiveTransitive

-- A predicate on relation "edges" (think of the relation as a graph).

EdgePred : {ℓ r : Level} (p : Level) {I : Set ℓ} → Rel I r → Set (suc p ⊔ ℓ ⊔ r)
EdgePred p T = ∀ {i j} → T i j → Set p

data NonEmptyEdgePred {ℓ r p : Level} {I : Set ℓ} (T : Rel I r)
                      (P : EdgePred p T) : Set (ℓ ⊔ r ⊔ p) where
  nonEmptyEdgePred : ∀ {i j} {x : T i j}
                     (p : P x) → NonEmptyEdgePred T P

-- Decorating an edge with more information.

data DecoratedWith {ℓ r p : Level} {I : Set ℓ} {T : Rel I r} (P : EdgePred p T)
       : Rel (NonEmpty (Star T)) p where
  ↦ : ∀ {i j k} {x : T i j} {xs : Star T j k}
      (p : P x) → DecoratedWith P (nonEmpty (x ◅ xs)) (nonEmpty xs)

module _ {ℓ r p : Level} {I : Set ℓ} {T : Rel I r} {P : EdgePred p T} where

  edge : ∀ {i j} → DecoratedWith {T = T} P i j → NonEmpty T
  edge (↦ {x = x} p) = nonEmpty x

  decoration : ∀ {i j} → (d : DecoratedWith {T = T} P i j) →
               P (NonEmpty.proof (edge d))
  decoration (↦ p) = p

-- Star-lists decorated with extra information. All P xs means that
-- all edges in xs satisfy P.

All : ∀ {ℓ r p} {I : Set ℓ} {T : Rel I r} → EdgePred p T → EdgePred (ℓ ⊔ (r ⊔ p)) (Star T)
All P {j = j} xs =
  Star (DecoratedWith P) (nonEmpty xs) (nonEmpty {y = j} ε)

-- We can map over decorated vectors.

gmapAll : ∀ {ℓ ℓ′ r p q} {I : Set ℓ} {T : Rel I r} {P : EdgePred p T}
                {J : Set ℓ′} {U : Rel J r} {Q : EdgePred q U}
                {i j} {xs : Star T i j}
          (f : I → J) (g : T =[ f ]⇒ U) →
          (∀ {i j} {x : T i j} → P x → Q (g x)) →
          All P xs → All {T = U} Q (gmap f g xs)
gmapAll f g h ε          = ε
gmapAll f g h (↦ x ◅ xs) = ↦ (h x) ◅ gmapAll f g h xs

-- Since we don't automatically have gmap id id xs ≡ xs it is easier
-- to implement mapAll in terms of map than in terms of gmapAll.

mapAll : ∀ {ℓ r p q} {I : Set ℓ} {T : Rel I r}
         {P : EdgePred p T} {Q : EdgePred q T} {i j} {xs : Star T i j} →
         (∀ {i j} {x : T i j} → P x → Q x) →
         All P xs → All Q xs
mapAll {P = P} {Q} f ps = map F ps
  where
  F : DecoratedWith P ⇒ DecoratedWith Q
  F (↦ x) = ↦ (f x)

-- We can decorate star-lists with universally true predicates.

decorate : ∀ {ℓ r p} {I : Set ℓ} {T : Rel I r} {P : EdgePred p T} {i j} →
           (∀ {i j} (x : T i j) → P x) →
           (xs : Star T i j) → All P xs
decorate f ε        = ε
decorate f (x ◅ xs) = ↦ (f x) ◅ decorate f xs

-- We can append Alls. Unfortunately _◅◅_ does not quite work.

infixr 5 _◅◅◅_ _▻▻▻_

_◅◅◅_ : ∀ {ℓ r p} {I : Set ℓ} {T : Rel I r} {P : EdgePred p T}
              {i j k} {xs : Star T i j} {ys : Star T j k} →
        All P xs → All P ys → All P (xs ◅◅ ys)
ε          ◅◅◅ ys = ys
(↦ x ◅ xs) ◅◅◅ ys = ↦ x ◅ xs ◅◅◅ ys

_▻▻▻_ : ∀ {ℓ r p} {I : Set ℓ} {T : Rel I r} {P : EdgePred p T}
              {i j k} {xs : Star T j k} {ys : Star T i j} →
        All P xs → All P ys → All P (xs ▻▻ ys)
_▻▻▻_ = flip _◅◅◅_


text:
module Category.Fibration where

open import Data.Product

open import Category.Category
open import Category.Subcategory
open import Category.Funct

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
-- 2010-10-04
-- termination checker no longer counts stripping off a record constructor
-- as decrease
module Issue334 where

data Unit : Set where
  unit : Unit

record E : Set where
  inductive
  constructor mkE
  field
    fromE : E
    spam  : Unit

f : E -> Set
f (mkE e unit) = f e
-- the record pattern translation does not apply to f
-- still, should not termination check, because
--   f (mkE e u) = f e
-- also does not!

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
open import Relation.Binary.PropositionalEquality
open import Data.Unit using (⊤ ; tt)
open import Data.Product renaming (_×_ to _∧_ ; proj₁ to fst ; proj₂ to snd)
open import Data.Sum renaming (_⊎_ to _∨_ ; inj₁ to left ; inj₂ to right)
open import Data.Nat using (ℕ ; zero ; suc)
open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
open import Data.List hiding (length ; head)

{- --- 1. Order on natural numbers --- -}
data _≤_ : ℕ → ℕ → Set where
  z≤n : {n : ℕ}                 → zero  ≤ n
  s≤s : {m n : ℕ} (m≤n : m ≤ n) → suc m ≤ suc n

{- 1.1 Compatibility with successor -}
≤-pred : {m n : ℕ} → (suc m ≤ suc n) → m ≤ n
≤-pred (s≤s i) = i

≤-suc : {m n : ℕ} → (m ≤ n) → suc m ≤ suc n
≤-suc i = s≤s i

{- 1.2 Reflexivity -}
≤-refl : (n : ℕ) → n ≤ n
≤-refl zero = z≤n
≤-refl (suc n) = s≤s (≤-refl n)

{- 1.3 Transitivity -}
≤-trans : {m n p : ℕ} → (m ≤ n) → (n ≤ p) → (m ≤ p)
≤-trans z≤n i2 = z≤n
≤-trans (s≤s i1) (s≤s i2) = ≤-suc (≤-trans i1 i2)

{- 1.4 Totality -}
_≤?_ : (m n : ℕ) → (m ≤ n) ∨ (n ≤ m)
zero ≤? n = left z≤n
suc m ≤? zero = right z≤n
suc m ≤? suc n with m ≤? n
... | left e = left (≤-suc e)
... | right e = right (≤-suc e)

{- --- 2. Insertion sort --- -}

{- 2.1 Insertion -}
insert : (x : ℕ) → (l : List ℕ) → List ℕ
insert x [] = x ∷ []
insert x (x₁ ∷ l) with x ≤? x₁
... | left e = x ∷ (x₁ ∷ l)
... | right e = x₁ ∷ (insert x l)

{- 2.2 Sorting -}
sort : List ℕ → List ℕ
sort [] = []
sort (x ∷ l) = insert x (sort l)

test : List ℕ
test = sort (4 ∷ 1 ∷ 45 ∷ 8 ∷ 32 ∷ 12 ∷ 1 ∷ [])

{- 2.3 The bounded below predicate -}
data _≤*_ : ℕ → List ℕ → Set where
  [] : {x : ℕ} → x ≤* []
  _∷_ : {x y : ℕ} → {l : List ℕ} → (x ≤ y) → (x ≤* l) → (x ≤* (y ∷ l))

{- 2.4 The sorted predicate -}
data sorted : (l : List ℕ) → Set where
  [] : sorted []
  _∷_ : {x : ℕ} → {l : List ℕ} → (x ≤* l) → sorted l → (sorted (x ∷ l))

{- 2.5 Insert is sorting -}

≤*-trans : {x y : ℕ} → (l : List ℕ) → x ≤ y → y ≤* l → x ≤* l
≤*-trans [] x≤y y≤*l = []
≤*-trans (x₁ ∷ l) x≤y (y≤x₁ ∷ y≤*l) = ≤-trans x≤y y≤x₁ ∷ ≤*-trans l x≤y y≤*l

sorted-lemma : {x y : ℕ} → (l : List ℕ) → x ≤ y → sorted (y ∷ l) → x ≤* (y ∷ l)
sorted-lemma l x≤y (y≤*l ∷ s) = x≤y ∷ (≤*-trans l x≤y y≤*l)

insert-lemma : (x y : ℕ) → (l : List ℕ) → y ≤ x → y ≤* l → y ≤* insert x l
insert-lemma x y [] y≤x y≤*l = y≤x ∷ []
insert-lemma x y (x₁ ∷ l) y≤x (y≤x₁ ∷ y≤*l) with x ≤? x₁
... | right x₁≤x = y≤x₁ ∷ insert-lemma x y l y≤x y≤*l
... | left x≤x₁ = y≤x ∷ (y≤x₁ ∷ y≤*l)

insert-sorting : (x : ℕ) → (l : List ℕ) → sorted l → sorted (insert x l)
insert-sorting x [] s = [] ∷ []
insert-sorting x (y ∷ l) (y≤*l ∷ s) with x ≤? y
... | left x≤y = (x≤y ∷ (≤*-trans l x≤y y≤*l)) ∷ (y≤*l ∷ s)
... | right y≤x = insert-lemma x y l y≤x y≤*l ∷ (insert-sorting x l s)

{- 2.6 Sort is sorting -}
sort-sorting : (l : List ℕ) → sorted (sort l)
sort-sorting [] = []
sort-sorting (x ∷ l) = insert-sorting x (sort l) (sort-sorting l)

{- 2.7 The problem of specification -}

{- Empty lists are always sorted, so always return an empty list -}
f : List ℕ → List ℕ
f l = []

f-sorting : (l : List ℕ) → sorted (f l)
f-sorting _ = []

{- 2.8 Intrinsic approach -}
mutual
  data Sorted : Set where
    nil : Sorted
    cons : (x : ℕ) → (l : Sorted) → x ≤ (head x l) → Sorted

  head : ℕ → Sorted → ℕ
  head d nil = d
  head d (cons x l x₁) = x

mutual
  insert' : (x : ℕ) → Sorted → Sorted
  insert' x nil = nil
  insert' x (cons x₁ l x₁≤hd) with x ≤? x₁
  ... | left x≤x₁ = cons x (cons x₁ l x₁≤hd) x≤x₁
  ... | right x₁≤x = cons x₁ (insert' x l) (ins-lemma x x₁ l x₁≤x x₁≤hd)

  {- In other words, y ≤ x and y ≤* l gives us y ≤* (insert x l) -}
  ins-lemma : (x y : ℕ) → (l : Sorted) → y ≤ x → y ≤ head y l → y ≤ head y (insert' x l)
  ins-lemma x y nil y≤x y≤hd = ≤-refl y
  ins-lemma x y (cons x₁ l x₁≤hd) y≤x y≤hd with x ≤? x₁
  ... | left x≤x₁ = y≤x
  ... | right x₁≤x = y≤hd

sort' : (l : List ℕ) → Sorted
sort' [] = nil
sort' (x ∷ l) = insert' x (sort' l)

{- --- 4. Merge sort --- -}

{- 4.1 Splitting -}
split : {A : Set} → List A → List A × List A
split [] = [] , []
split (x ∷ []) = (x ∷ []) , []
split (x ∷ y ∷ l) =
  let (l₁ , l₂) = split l in
  x ∷ l₁ , y ∷ l₂

test-split : List ℕ × List ℕ
test-split = split (4 ∷ 1 ∷ 45 ∷ 8 ∷ 32 ∷ 12 ∷ 1 ∷ [])

{- 4.2 Merging -}
merge : (l m : List ℕ) → List ℕ
merge [] m = m
merge l [] = l
merge (x ∷ l) (y ∷ m) with x ≤? y
... | left x≤y = x ∷ (merge l (y ∷ m))
... | right y≤x = y ∷ (merge (x ∷ l) m)

{- 4.3 Sorting -}

{-# TERMINATING #-}
mergesort-v1 : List ℕ → List ℕ
mergesort-v1 [] = []
mergesort-v1 (x ∷ []) = x ∷ []
mergesort-v1 l =
  let (l₁ , l₂) = split l in
  merge (mergesort-v1 l₁) (mergesort-v1 l₂)

test-merge-v1 : List ℕ
test-merge-v1 = mergesort-v1 (4 ∷ 1 ∷ 45 ∷ 8 ∷ 32 ∷ 12 ∷ 1 ∷ [])

{- 4.4 Splitting is decreasing -}
data _<_ : ℕ → ℕ → Set where
  s<s : {m n : ℕ} (m<n : suc m ≤ n) → m < n

length : {A : Set} (l : List A) → ℕ
length [] = zero
length (x ∷ l) = suc (length l)

test-length : ℕ
test-length = length (4 ∷ [])

{- Surprisingly we need this lemma to have a compact proof that splitting is decreasing -}
≤-to-suc : (m : ℕ) → m ≤ suc m
≤-to-suc zero = z≤n
≤-to-suc (suc m) = s≤s (≤-to-suc m)

{- Splitting is strictly decreasing only for lists with at least two elements
   Another approach would be to add `2 ≤ length l` as an argument, but it
   complicates the proof and Agda's pattern matching shows problematic behavior in that case
   [see at the end] -}
<-split₁ : {A : Set} → (x y : A) → (l : List A)
                    → length (fst (split (x ∷ y ∷ l))) < length (x ∷ y ∷ l)
<-split₁ x y [] = s<s (≤-refl 2)
<-split₁ x y (x₁ ∷ []) = s<s (s≤s (s≤s (≤-refl 1)))
<-split₁ x y (x₁ ∷ x₂ ∷ l) with <-split₁ x y l
... | s<s h = s<s (s≤s (s≤s (≤-trans (≤-to-suc (suc (length (fst (split l))))) h)))

<-split₂ : {A : Set} → (x y : A) → (l : List A)
                    → length (snd (split (x ∷ y ∷ l))) < length (x ∷ y ∷ l)
<-split₂ x y [] = s<s (≤-refl 2)
<-split₂ x y (x₁ ∷ []) = s<s (s≤s (s≤s z≤n))
<-split₂ x y (x₁ ∷ x₂ ∷ l) with <-split₂ x y l
... | s<s h = s<s (s≤s (s≤s (≤-trans (≤-to-suc (suc (length (snd (split l))))) h)))

{- 4.5 The fuel definition of merge -}

{- Convenience function -}
<-to-≤ : {m n : ℕ} → m < n → suc m ≤ n
<-to-≤ (s<s m<n) = m<n

{- The key part of this definition is proving that the recursive calls are decreasing -}
mergesort-fuel : (n : ℕ) → (l : List ℕ) → (length l ≤ n) → List ℕ
mergesort-fuel n [] l≤n = []
mergesort-fuel n (x ∷ []) l≤n = x ∷ []
mergesort-fuel (suc n) (x ∷ y ∷ l) l≤n =
  let (l₁ , l₂) = split (x ∷ y ∷ l) in
  merge
    (mergesort-fuel n l₁ (≤-trans (≤-pred (<-to-≤ (<-split₁ x y l))) (≤-pred l≤n)))
    (mergesort-fuel n l₂ (≤-trans (≤-pred (<-to-≤ (<-split₂ x y l))) (≤-pred l≤n)))

mergesort : (l : List ℕ) → List ℕ
mergesort l = mergesort-fuel (length l) l (≤-refl (length l))

test-merge : List ℕ
test-merge = mergesort (4 ∷ 1 ∷ 45 ∷ 8 ∷ 32 ∷ 12 ∷ 1 ∷ [])

{- 4.6 Merge sort is sorting -}

{- Intrinsic approach: using the Sorted type -}

{- Step 1: merging two sorted lists produces a sorted list -}
mutual
  merge' : (l m : Sorted) → Sorted
  merge' nil m = m
  merge' l nil = l
  merge' (cons x l x≤l) (cons y m y≤m) with x ≤? y
  ... | left x≤y = cons x (merge' l (cons y m y≤m)) (merge-lemma x l (cons y m y≤m) x≤l x≤y)
  ... | right y≤x = cons y (merge' (cons x l x≤l) m) (merge-lemma y (cons x l x≤l) m y≤x y≤m)

  {- Lemma: if x is a lower bound on both l and m, it's also a lower bound on the merged list -}
  merge-lemma : (x : ℕ) → (l m : Sorted) → x ≤ head x l → x ≤ head x m
                → x ≤ head x (merge' l m)
  merge-lemma x nil m x≤l x≤m = x≤m
  merge-lemma x (cons y l y≤l) nil x≤l x≤m = x≤l
  merge-lemma x (cons y l y≤l) (cons z m z≤m) x≤l x≤m with y ≤? z
  ... | left y≤z = x≤l
  ... | right z≤y = x≤m

{- Step 2: same-approach to mergesort-fuel -}
mergesort-fuel-v2 : (n : ℕ) → (l : List ℕ) → (length l ≤ n) → Sorted
mergesort-fuel-v2 _ [] _ = nil
mergesort-fuel-v2 _ (x ∷ []) _ = cons x nil (≤-refl x)
mergesort-fuel-v2 (suc n) (x ∷ y ∷ l) l≤n =
  let (l₁ , l₂) = split (x ∷ y ∷ l) in
  merge'
    (mergesort-fuel-v2 n l₁ (≤-trans (≤-pred (<-to-≤ (<-split₁ x y l))) (≤-pred l≤n)))
    (mergesort-fuel-v2 n l₂ (≤-trans (≤-pred (<-to-≤ (<-split₂ x y l))) (≤-pred l≤n)))

{- Step 3: mergesort-v3 comes to life -}
mergesort-v3 : List ℕ → Sorted
mergesort-v3 l = mergesort-fuel-v2 (length l) l (≤-refl (length l))

{- --- APPENDIX --- -}

{- Showcase: Agda's pattern matching forces us to consider a case where 2 ≤ 1 -}
<-split₁-x : {A : Set} → (l : List A) → 2 ≤ length l
                                    → length (fst (split l)) < length l
<-split₁-x (x ∷ []) (s≤s ())
<-split₁-x (x ∷ y ∷ l) 2≤l' with 2 ≤? length l
... | left 2≤l = s<s (s≤s (≤-trans (<-to-≤ (<-split₁-x l 2≤l)) (≤-to-suc (length l))))
... | right l≤2 = {!!} {- would need to refine l here -}

max_stars_repo_name: erwinkn/program-eq-proof

max_issues_repo_name: erwinkn/program-eq-proof

max_forks_repo_name: erwinkn/program-eq-proof


text:
record R : Set₁ where
  X = Y  -- should get error here
  field A : Set


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Simple combinators working solely on and with functions
------------------------------------------------------------------------

-- The contents of this file can be accessed from `Function`.

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

module Function.Base where

open import Level
open import Strict

private
  variable
    a b c d e : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d
    E : Set e

------------------------------------------------------------------------
-- Some simple functions

id : A → A
id x = x

const : A → B → A
const x = λ _ → x

------------------------------------------------------------------------
-- Operations on dependent functions

-- These are functions whose output has a type that depends on the
-- value of the input to the function.

infixr 9 _∘_
infixl 8 _ˢ_
infixl 0 _|>_
infix  0 case_return_of_
infixr -1 _$_ _$!_

-- Composition

_∘_ : ∀ {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
      (∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
      ((x : A) → C (g x))
f ∘ g = λ x → f (g x)

-- Flipping order of arguments

flip : ∀ {A : Set a} {B : Set b} {C : A → B → Set c} →
       ((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ y x → f x y

-- Application - note that _$_ is right associative, as in Haskell.
-- If you want a left associative infix application operator, use
-- Category.Functor._<$>_ from Category.Monad.Identity.IdentityMonad.

_$_ : ∀ {A : Set a} {B : A → Set b} →
      ((x : A) → B x) → ((x : A) → B x)
f $ x = f x

-- Strict (call-by-value) application

_$!_ : ∀ {A : Set a} {B : A → Set b} →
       ((x : A) → B x) → ((x : A) → B x)
_$!_ = flip force

-- Flipped application (aka pipe-forward)

_|>_ : ∀ {A : Set a} {B : A → Set b} →
       (a : A) → (∀ a → B a) → B a
_|>_ = flip _$_

-- The S combinator - written infix as in Conor McBride's paper
-- "Outrageous but Meaningful Coincidences: Dependent type-safe syntax
-- and evaluation".

_ˢ_ : ∀ {A : Set a} {B : A → Set b} {C : (x : A) → B x → Set c} →
      ((x : A) (y : B x) → C x y) →
      (g : (x : A) → B x) →
      ((x : A) → C x (g x))
f ˢ g = λ x → f x (g x)

-- Converting between implicit and explicit function spaces.

_$- : ∀ {A : Set a} {B : A → Set b} → ((x : A) → B x) → ({x : A} → B x)
f $- = f _

λ- : ∀ {A : Set a} {B : A → Set b} → ({x : A} → B x) → ((x : A) → B x)
λ- f = λ x → f

-- Case expressions (to be used with pattern-matching lambdas, see
-- README.Case).

case_return_of_ : ∀ {A : Set a} (x : A) (B : A → Set b) →
                  ((x : A) → B x) → B x
case x return B of f = f x

------------------------------------------------------------------------
-- Non-dependent versions of dependent operations

-- Any of the above operations for dependent functions will also work
-- for non-dependent functions but sometimes Agda has difficulty
-- inferring the non-dependency. Primed (′ = \prime) versions of the
-- operations are therefore provided below that sometimes have better
-- inference properties.

infixr 9 _∘′_
infixl 0 _|>′_
infix  0 case_of_
infixr -1 _$′_ _$!′_

-- Composition

_∘′_ : (B → C) → (A → B) → (A → C)
f ∘′ g = _∘_ f g

-- Application

_$′_ : (A → B) → (A → B)
_$′_ = _$_

-- Strict (call-by-value) application

_$!′_ : (A → B) → (A → B)
_$!′_ = _$!_

-- Flipped application (aka pipe-forward)

_|>′_ : A → (A → B) → B
_|>′_ = _|>_

-- Case expressions (to be used with pattern-matching lambdas, see
-- README.Case).

case_of_ : A → (A → B) → B
case x of f = case x return _ of f

------------------------------------------------------------------------
-- Operations that are only defined for non-dependent functions

infixr 0 _-[_]-_
infixl 1 _on_
infixl 1 _⟨_⟩_
infixl 0 _∋_

-- Binary application

_⟨_⟩_ : A → (A → B → C) → B → C
x ⟨ f ⟩ y = f x y

-- Composition of a binary function with a unary function

_on_ : (B → B → C) → (A → B) → (A → A → C)
_*_ on f = λ x y → f x * f y

-- Composition of three binary functions

_-[_]-_ : (A → B → C) → (C → D → E) → (A → B → D) → (A → B → E)
f -[ _*_ ]- g = λ x y → f x y * g x y

-- In Agda you cannot annotate every subexpression with a type
-- signature. This function can be used instead.

_∋_ : (A : Set a) → A → A
A ∋ x = x

-- Conversely it is sometimes useful to be able to extract the
-- type of a given expression.

typeOf : {A : Set a} → A → Set a
typeOf {A = A} _ = A

-- Construct an element of the given type by instance search.

it : {A : Set a} → {{A}} → A
it {{x}} = x


text:
open import Relation.Binary.Core

module PLRTree.Insert {A : Set}
                     (_≤_ : A → A → Set)
                     (tot≤ : Total _≤_) where

open import Data.Sum
open import PLRTree {A}

insert : A → PLRTree → PLRTree
insert x leaf = node perfect x leaf leaf
insert x (node perfect y l r)
    with tot≤ x y | l | r
... | inj₁ x≤y | leaf | leaf = node right x (node perfect y leaf leaf) leaf
... | inj₁ x≤y | _ | _ = node left x (insert y l) r
... | inj₂ y≤x | leaf | leaf = node right y (node perfect x leaf leaf) leaf
... | inj₂ y≤x | _ | _ = node left y (insert x l) r
insert x (node left y l r)
    with tot≤ x y
... | inj₁ x≤y
    with insert y l
... | node perfect y' l' r' = node right x (node perfect y' l' r') r
... | t = node left x t r
insert x (node left y l r) | inj₂ y≤x
    with insert x l
... | node perfect y' l' r' = node right y (node perfect y' l' r') r
... | t = node left y t r
insert x (node right y l r)
    with tot≤ x y
... | inj₁ x≤y
    with insert y r
... | node perfect y' l' r' = node perfect x l (node perfect y' l' r')
... | t = node right x l t
insert x (node right y l r) | inj₂ y≤x
    with insert x r
... | node perfect y' l' r' = node perfect y l (node perfect y' l' r')
... | t = node right y l t

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
open import Common.Prelude
open import Common.Equality

infixr 5 _∷_

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

record Eq (A : Set) : Set where
  field
    _==_ : (x y : A) → Maybe (x ≡ y)

open Eq {{...}}

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (x : A) → B x → Σ A B

eqNat : ∀ n m → Maybe (n ≡ m)
eqNat zero zero = just refl
eqNat zero (suc m) = nothing
eqNat (suc n) zero = nothing
eqNat (suc n) (suc m) with eqNat n m
eqNat (suc n) (suc m) | nothing = nothing
eqNat (suc n) (suc .n) | just refl = just refl

eqVec : ∀ {A n} {{EqA : Eq A}} (xs ys : Vec A n) → Maybe (xs ≡ ys)
eqVec [] [] = just refl
eqVec (x ∷ xs) ( y ∷  ys) with x == y    | eqVec xs ys
eqVec (x ∷ xs) ( y ∷  ys)    | nothing   | _         = nothing
eqVec (x ∷ xs) ( y ∷  ys)    | _         | nothing   = nothing
eqVec (x ∷ xs) (.x ∷ .xs)    | just refl | just refl = just refl

eqSigma : ∀ {A B} {{EqA : Eq A}} {{EqB : ∀ {x} → Eq (B x)}} (x y : Σ A B) → Maybe (x ≡ y)
eqSigma (x , y) (x₁ , y₁) with x == x₁
eqSigma (x , y) (x₁ , y₁) | nothing = nothing
eqSigma (x , y) (.x , y₁) | just refl with y == y₁
eqSigma (x , y) (.x , y₁) | just refl | nothing = nothing
eqSigma (x , y) (.x , .y) | just refl | just refl = just refl

instance
  EqNat : Eq Nat
  EqNat = record { _==_ = eqNat }

  EqVec : ∀ {A n} {{_ : Eq A}} → Eq (Vec A n)
  EqVec = record { _==_ = eqVec }

  EqSigma : ∀ {A B} {{_ : Eq A}} {{_ : ∀ {x} → Eq (B x)}} → Eq (Σ A B)
  EqSigma = record { _==_ = eqSigma }

cmpSigma : (xs ys : Σ Nat (Vec Nat)) → Maybe (xs ≡ ys)
cmpSigma xs ys = xs == ys


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

module Cubical.Categories.Constructions.Quotient where

open import Cubical.Categories.Category.Base
open import Cubical.Categories.Functor.Base
open import Cubical.Categories.Limits.Terminal
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.HITs.SetQuotients renaming ([_] to ⟦_⟧)

private
  variable
    ℓ ℓ' ℓq : Level

module _ (C : Category ℓ ℓ') where
  open Category C

  module _ (_~_ : {x y : ob} (f g : Hom[ x , y ] ) → Type ℓq)
           (~refl : {x y : ob} (f : Hom[ x , y ] ) → f ~ f)
           (~cong : {x y z : ob}
                    (f f' : Hom[ x , y ]) → f ~ f'
                  → (g g' : Hom[ y , z ]) → g ~ g'
                  → (f ⋆ g) ~ (f' ⋆ g')) where

    private
      Hom[_,_]/~ = λ (x y : ob) → Hom[ x , y ] / _~_

      module _ {x y z : ob} where
        _⋆/~_ : Hom[ x , y ]/~ → Hom[ y , z ]/~ → Hom[ x , z ]/~
        _⋆/~_ = rec2 squash/ (λ f g → ⟦ f ⋆ g ⟧)
                    (λ f f' g f~f' → eq/ _ _ (~cong _ _ f~f' _ _ (~refl _)))
                    (λ f g g' g~g' → eq/ _ _ (~cong _ _ (~refl _) _ _ g~g'))

    module _ {x y : ob} where
      ⋆/~IdL : (f : Hom[ x , y ]/~) → (⟦ id ⟧ ⋆/~ f) ≡ f
      ⋆/~IdL = elimProp (λ _ → squash/ _ _) (λ _ → cong ⟦_⟧ (⋆IdL _))

      ⋆/~IdR : (f : Hom[ x , y ]/~) → (f ⋆/~ ⟦ id ⟧) ≡ f
      ⋆/~IdR = elimProp (λ _ → squash/ _ _) (λ _ → cong ⟦_⟧ (⋆IdR _))

    module _ {x y z w : ob} where
      ⋆/~Assoc : (f : Hom[ x , y ]/~)
                (g : Hom[ y , z ]/~)
                (h : Hom[ z , w ]/~)
        → ((f ⋆/~ g) ⋆/~ h) ≡ (f ⋆/~ (g ⋆/~ h))

      ⋆/~Assoc = elimProp3 (λ _ _ _ → squash/ _ _) (λ _ _ _ → cong ⟦_⟧ (⋆Assoc _ _ _))

    open Category
    QuotientCategory : Category ℓ (ℓ-max ℓ' ℓq)
    QuotientCategory .ob = ob C
    QuotientCategory .Hom[_,_] x y = (C [ x , y ]) / _~_
    QuotientCategory .id = ⟦ id C ⟧
    QuotientCategory ._⋆_ = _⋆/~_
    QuotientCategory .⋆IdL = ⋆/~IdL
    QuotientCategory .⋆IdR = ⋆/~IdR
    QuotientCategory .⋆Assoc = ⋆/~Assoc
    QuotientCategory .isSetHom = squash/

    private
      C/~ = QuotientCategory

    -- Quotient map
    open Functor
    QuoFunctor : Functor C C/~
    QuoFunctor .F-ob x = x
    QuoFunctor .F-hom = ⟦_⟧
    QuoFunctor .F-id = refl
    QuoFunctor .F-seq f g = refl

    -- Quotients preserve initial / terminal objects
    isInitial/~ : {z : ob C} → isInitial C z → isInitial C/~ z
    isInitial/~ zInit x = ⟦ zInit x .fst ⟧ , elimProp (λ _ → squash/ _ _)
        λ f → eq/ _ _ (subst (_~ f) (sym (zInit x .snd f)) (~refl _))

    isFinal/~ : {z : ob C} → isFinal C z → isFinal C/~ z
    isFinal/~ zFinal x = ⟦ zFinal x .fst ⟧ , elimProp (λ _ → squash/ _ _)
        λ f → eq/ _ _ (subst (_~ f) (sym (zFinal x .snd f)) (~refl _))


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Pointed.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed.Base
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Sigma

private
  variable
    ℓ ℓ' ℓA ℓB ℓC ℓD : Level

-- the default pointed Π-type: A is pointed, and B has a base point in the chosen fiber
Π∙ : (A : Pointed ℓ) (B : typ A → Type ℓ') (ptB : B (pt A)) → Type (ℓ-max ℓ ℓ')
Π∙ A B ptB = Σ[ f ∈ ((a : typ A) → B a) ] f (pt A) ≡ ptB

-- the unpointed Π-type becomes a pointed type if the fibers are all pointed
Πᵘ∙ : (A : Type ℓ) (B : A → Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
Πᵘ∙ A B .fst = ∀ a → typ (B a)
Πᵘ∙ A B .snd a = pt (B a)

-- if the base and all fibers are pointed, we have the pointed pointed Π-type
Πᵖ∙ : (A : Pointed ℓ) (B : typ A → Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
Πᵖ∙ A B .fst = Π∙ A (typ ∘ B) (pt (B (pt A)))
Πᵖ∙ A B  .snd .fst a = pt (B a)
Πᵖ∙ A B  .snd .snd = refl

-- the default pointed Σ-type is just the Σ-type, but as a pointed type
Σ∙ : (A : Pointed ℓ) (B : typ A → Type ℓ') (ptB : B (pt A)) → Pointed (ℓ-max ℓ ℓ')
Σ∙ A B ptB .fst = Σ[ a ∈ typ A ] B a
Σ∙ A B ptB .snd .fst = pt A
Σ∙ A B ptB .snd .snd = ptB

-- version if B is a family of pointed types
Σᵖ∙ : (A : Pointed ℓ) (B : typ A → Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
Σᵖ∙ A B = Σ∙ A (typ ∘ B) (pt (B (pt A)))

_×∙_ : (A∙ : Pointed ℓ) (B∙ : Pointed ℓ') → Pointed (ℓ-max ℓ ℓ')
(A∙ ×∙ B∙) .fst = (typ A∙) × (typ B∙)
(A∙ ×∙ B∙) .snd .fst = pt A∙
(A∙ ×∙ B∙) .snd .snd = pt B∙

-- composition of pointed maps
_∘∙_ : {A : Pointed ℓA} {B : Pointed ℓB} {C : Pointed ℓC}
       (g : B →∙ C) (f : A →∙ B) → (A →∙ C)
((g , g∙) ∘∙ (f , f∙)) .fst x = g (f  x)
((g , g∙) ∘∙ (f , f∙)) .snd = (cong g f∙) ∙ g∙

-- pointed identity
id∙ : (A : Pointed ℓA) → (A →∙ A)
id∙ A .fst x = x
id∙ A .snd = refl

-- constant pointed map
const∙ : (A : Pointed ℓA) (B : Pointed ℓB) → (A →∙ B)
const∙ _ B .fst _ = B .snd
const∙ _ B .snd = refl

-- left identity law for pointed maps
∘∙-idˡ : {A : Pointed ℓA} {B : Pointed ℓB} (f : A →∙ B) → f ∘∙ id∙ A ≡ f
∘∙-idˡ f = ΣPathP ( refl , (lUnit (f .snd)) ⁻¹ )

-- right identity law for pointed maps
∘∙-idʳ : {A : Pointed ℓA} {B : Pointed ℓB} (f : A →∙ B) → id∙ B ∘∙ f ≡ f
∘∙-idʳ f = ΣPathP ( refl , (rUnit (f .snd)) ⁻¹ )

-- associativity for composition of pointed maps
∘∙-assoc : {A : Pointed ℓA} {B : Pointed ℓB} {C : Pointed ℓC} {D : Pointed ℓD}
           (h : C →∙ D) (g : B →∙ C) (f : A →∙ B)
           → (h ∘∙ g) ∘∙ f ≡ h ∘∙ (g ∘∙ f)
∘∙-assoc (h , h∙) (g , g∙) (f , f∙) = ΣPathP (refl , q)
  where
    q : (cong (h ∘ g) f∙) ∙ (cong h g∙ ∙ h∙) ≡ cong h (cong g f∙ ∙ g∙) ∙ h∙
    q = ( (cong (h ∘ g) f∙) ∙ (cong h g∙ ∙ h∙)
        ≡⟨ refl ⟩
        (cong h (cong g f∙)) ∙ (cong h g∙ ∙ h∙)
        ≡⟨ assoc (cong h (cong g f∙)) (cong h g∙) h∙ ⟩
        (cong h (cong g f∙) ∙ cong h g∙) ∙ h∙
        ≡⟨ cong (λ p → p ∙ h∙) ((cong-∙ h (cong g f∙) g∙) ⁻¹) ⟩
        (cong h (cong g f∙ ∙ g∙) ∙ h∙) ∎ )

max_stars_repo_name: L-TChen/cubical

max_issues_repo_name: L-TChen/cubical

max_forks_repo_name: L-TChen/cubical


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

module Definition.Typed.EqRelInstance where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening
open import Definition.Typed.Properties
open import Definition.Typed.Reduction
open import Definition.Typed.EqualityRelation

open import Tools.Function

Urefl   : ∀ {r l Γ} → ⊢ Γ → Γ ⊢ (Univ r l) ≡ (Univ r l) ^ [ ! , next l ]
Urefl {l = ⁰} ⊢Γ = refl (univ (univ 0<1 ⊢Γ))
Urefl {l = ¹} ⊢Γ = refl (Uⱼ ⊢Γ)

instance eqRelInstance : EqRelSet
eqRelInstance = eqRel _⊢_≡_^_ _⊢_≡_∷_^_ _⊢_≡_∷_^_
                      idᶠ idᶠ idᶠ univ un-univ≡
                      sym genSym genSym trans genTrans genTrans
                      conv conv wkEq wkEqTerm wkEqTerm
                      reduction reductionₜ
                      Urefl (refl ∘ᶠ univ 0<1) (refl ∘ᶠ ℕⱼ) (refl ∘ᶠ Emptyⱼ)
                      Π-cong ∃-cong (refl ∘ᶠ zeroⱼ) suc-cong
                      (λ lF lG x x₁ x₂ x₃ x₄ x₅ → η-eq lF lG x x₁ x₂ x₅)
                      genVar app-cong natrec-cong Emptyrec-cong
                      Id-cong
                      (λ ⊢Γ → Id-cong (refl (ℕⱼ ⊢Γ)))
                      (λ ⊢Γ → Id-cong (refl (ℕⱼ ⊢Γ)) (refl (zeroⱼ ⊢Γ)))
                      (λ ⊢Γ t → Id-cong (refl (ℕⱼ ⊢Γ)) (suc-cong t))
                      (λ ⊢Γ → Id-cong (refl (univ 0<1 ⊢Γ)))
                      (λ ⊢Γ → Id-cong (refl (univ 0<1 ⊢Γ)) (refl (ℕⱼ ⊢Γ)))
                      (λ ⊢A B → Id-cong (refl (univ 0<1 (wfEq (univ ⊢A)))) ⊢A B)
                      cast-cong
                      (λ ⊢Γ → cast-cong (refl (ℕⱼ ⊢Γ)))
                      (λ ⊢Γ → cast-cong (refl (ℕⱼ ⊢Γ)) (refl (ℕⱼ ⊢Γ)))
                      cast-cong
                      (λ ⊢A ⊢P P → cast-cong (refl (ℕⱼ (wf (univ ⊢A)))) P)
                      (λ ⊢A ⊢P P → cast-cong P (refl (ℕⱼ (wf (univ ⊢A)))))
                      (λ ⊢A ⊢P P ⊢A' ⊢P' P' → cast-cong P P')
                      (λ ⊢A ⊢P P ⊢A' ⊢P' P' → cast-cong P P')
                      proof-irrelevance

max_stars_repo_name: CoqHott/logrel-mltt

max_issues_repo_name: CoqHott/logrel-mltt

max_forks_repo_name: CoqHott/logrel-mltt


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

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

open import LibraBFT.Abstract.Types
open import LibraBFT.Abstract.Types.EpochConfig
open import Util.Lemmas
open import Util.Prelude
open        WithAbsVote

-- For each desired property (VotesOnce and PreferredRoundRule), we have a
-- module containing a Type that defines a property that an implementation
-- should prove, and a proof that it implies the corresponding rule used by
-- the abstract proofs.  Then, we use those proofs to instantiate thmS5,
-- and the use thmS5 to prove a number of correctness conditions.
--
-- TODO-1: refactor this file to separate the definitions and proofs of
-- VotesOnce and PreferredRoundRule from their use in proving the correctness
-- properties.

module LibraBFT.Abstract.Properties
  (UID    : Set)
  (_≟UID_ : (u₀ u₁ : UID) → Dec (u₀ ≡ u₁))
  (NodeId : Set)
  (𝓔  : EpochConfig UID NodeId)
  (𝓥  : VoteEvidence UID NodeId 𝓔)
  where

 open import LibraBFT.Abstract.Records                 UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.Records.Extends         UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.RecordChain             UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.RecordChain.Assumptions UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.System                  UID _≟UID_ NodeId 𝓔 𝓥
 open import LibraBFT.Abstract.RecordChain.Properties  UID _≟UID_ NodeId 𝓔 𝓥
 open        EpochConfig 𝓔

 module WithAssumptions {ℓ}
   (InSys               : Record → Set ℓ)
   (no-collisions-InSys : NoCollisions InSys)
   (votes-once          : VotesOnlyOnceRule InSys)
   (preferred-round     : PreferredRoundRule InSys)
  where

   open All-InSys-props InSys

   CommitsDoNotConflict : ∀{q q'}
        → {rc  : RecordChain (Q q)}  → All-InSys rc
        → {rc' : RecordChain (Q q')} → All-InSys rc'
        → {b b' : Block}
        → CommitRule rc  b
        → CommitRule rc' b'
        → (B b) ∈RC rc' ⊎ (B b') ∈RC rc
   CommitsDoNotConflict ais ais' cr cr'
      with WithInvariants.thmS5 InSys votes-once preferred-round ais ais' cr cr'
       -- We use the implementation-provided evidence that Block ids are injective among
       -- Block actually in the system to dismiss the first possibility
   ...| inj₁ ((_ , neq , h≡) , (is1 , is2)) = ⊥-elim (neq (no-collisions-InSys is1 is2 h≡))
   ...| inj₂ corr = corr

   -- When we are dealing with a /Complete/ InSys predicate, we can go a few steps
   -- further and prove that commits do not conflict even if we have only partial
   -- knowledge about Records represented in the system.
   module _ (∈QC⇒AllSent : Complete InSys) where

    -- For a /complete/ system (i.e., one in which peers vote for a Block only if
    -- they know of a RecordChain up to that Block whose Records are all InSys), we
    -- can prove that CommitRules based on RecordChainFroms similarly do not
    -- conflict, provided all of the Records in the RecordChainFroms are InSys.
    -- This enables peers not participating in consensus to confirm commits even if
    -- they are sent only a "commit certificate" that contains enough of a
    -- RecordChain to confirm the CommitRule.  Note that it is this "sending" that
    -- justfies the assumption that the RecordChainFroms on which the CommitRules
    -- are based are All-InSys.
    CommitsDoNotConflict'
      : ∀{o o' q q'}
      → {rcf  : RecordChainFrom o  (Q q)}  → All-InSys rcf
      → {rcf' : RecordChainFrom o' (Q q')} → All-InSys rcf'
      → {b b' : Block}
      → CommitRuleFrom rcf  b
      → CommitRuleFrom rcf' b'
      → Σ (RecordChain (Q q')) ((B b)  ∈RC_)
      ⊎ Σ (RecordChain (Q q))  ((B b') ∈RC_)
    CommitsDoNotConflict' {cb} {q = q} {q'} {rcf} rcfAll∈sys {rcf'} rcf'All∈sys crf crf'
       with bft-property (qVotes-C1 q) (qVotes-C1 q')
    ...| α , α∈qmem , α∈q'mem , hα
       with Any-sym (Any-map⁻ α∈qmem) | Any-sym (Any-map⁻ α∈q'mem)
    ...| α∈q | α∈q'
       with ∈QC⇒AllSent {q = q} hα α∈q (rcfAll∈sys here) | ∈QC⇒AllSent {q = q'} hα α∈q' (rcf'All∈sys here)
    ...| ab , (arc , ais) , ab←q | ab' , (arc' , ais') , ab←q'
      with crf⇒cr rcf (step arc ab←q) crf | crf⇒cr rcf' (step arc' ab←q') crf'
    ...| inj₁ ((_ , neq , h≡) , (is1 , is2)) | _                     = ⊥-elim (neq (no-collisions-InSys (rcfAll∈sys  is1) (ais  (∈RC-simple-¬here arc  ab←q  (λ ()) is2)) h≡))
    ...| inj₂ _                | inj₁ ((_ , neq , h≡) , (is1 , is2)) = ⊥-elim (neq (no-collisions-InSys (rcf'All∈sys is1) (ais' (∈RC-simple-¬here arc' ab←q' (λ ()) is2)) h≡))
    ...| inj₂ cr               | inj₂ cr'
      with CommitsDoNotConflict (All-InSys-step ais ab←q (rcfAll∈sys here)) (All-InSys-step ais' ab←q' (rcf'All∈sys here)) cr cr'
    ...| inj₁ b∈arc' = inj₁ (step arc' ab←q' , b∈arc')
    ...| inj₂ b'∈arc = inj₂ (step arc  ab←q  , b'∈arc)


text:
module Data.List.First.Properties {ℓ}{A : Set ℓ} where

open import Data.Product
open import Data.List
open import Data.List.Any
open import Relation.Binary.PropositionalEquality
open import Function
open import Data.Empty
open import Data.List.First
open import Data.List.Membership.Propositional

first⟶∈ : ∀ {B : A → Set} {x l} → First B x l → (x ∈ l × B x)
first⟶∈ (here {x = x} p) = here refl , p
first⟶∈ (there x' ¬px f) with (first⟶∈ f)
first⟶∈ (there x' ¬px f) | x∈l , p = there x∈l , p

first-unique : ∀ {P : A → Set}{x y v} → First P x v → First P y v → x ≡ y
first-unique (here x) (here y) = refl
first-unique (here {x = x} px) (there .x ¬px r) = ⊥-elim (¬px px)
first-unique (there x ¬px l) (here {x = .x} px) = ⊥-elim (¬px px)
first-unique (there x' _ l) (there .x' _ r) = first-unique l r


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

open import Categories.Category

module Categories.Category.Construction.Spans {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level

open import Categories.Category.Diagram.Span 𝒞
open import Categories.Morphism.Reasoning 𝒞

open Category 𝒞
open HomReasoning
open Equiv

open Span
open Span⇒

Spans : Obj → Obj → Category (o ⊔ ℓ) (o ⊔ ℓ ⊔ e) e
Spans X Y = record
  { Obj = Span X Y
  ; _⇒_ = Span⇒
  ; _≈_ = λ f g → arr f ≈ arr g
  ; id = id-span⇒
  ; _∘_ = _∘ₛ_
  ; assoc = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv = record
    { refl = refl
    ; sym = sym
    ; trans = trans
    }
  ; ∘-resp-≈ = ∘-resp-≈
  }


text:
{- Definition of join for ◇ and associated lemmas. -}
module TemporalOps.Diamond.JoinLemmas where

open import CategoryTheory.Categories
open import CategoryTheory.Instances.Reactive
open import CategoryTheory.Functor
open import CategoryTheory.NatTrans
open import CategoryTheory.Monad
open import TemporalOps.Common
open import TemporalOps.Next
open import TemporalOps.Delay
open import TemporalOps.Diamond.Functor
open import TemporalOps.Diamond.Join

import Relation.Binary.PropositionalEquality as ≡
open import Data.Product
open import Relation.Binary.HeterogeneousEquality as ≅
            using (_≅_ ; ≅-to-≡ ; ≡-to-≅ ; cong₂)
open import Data.Nat.Properties
            using (+-identityʳ ; +-comm ; +-suc ; +-assoc)

open import Holes.Term using (⌞_⌟)
open import Holes.Cong.Propositional

-- | Auxiliary lemmas

-- Equality of two delayed values
◇-≅ : ∀{A : τ}{n n′ k k′ : ℕ}
          -> {v : delay A by k at n} {v′ : delay A by k′ at n′}
          -> (pk : k ≡ k′) (pn : n ≡ n′)
          -> v ≅ v′
          -> _≅_ {A = ◇ A at n} (k , v)
                 {B = ◇ A at n′} (k′ , v′)
◇-≅ refl refl ≅.refl = ≅.refl

-- | Lemmas involving μ

-- Two consecutive shifts can be composed
μ-shift-comp : ∀{A} {n k l : ℕ} {a : ◇ A at n}
            -> μ-shift l (k + n) (μ-shift {A} k n a)
             ≅ μ-shift {A} (l + k) n a
μ-shift-comp {A} {n} {k} {l} {j , v} =
    begin
        μ-shift l (k + n) (μ-shift k n (j , v))
    ≡⟨⟩
        μ-shift l (k + n) (k + j , v′)
    ≡⟨⟩
        l + (k + j) , rew (sym (delay-+ l (k + j) (k + n))) v′
    ≅⟨ ◇-≅ (sym (+-assoc l k j)) ((sym (+-assoc l k n))) pr ⟩
        (l + k) + j , rew (sym (delay-+ (l + k) j n)) v
    ≡⟨⟩
        μ-shift (l + k) n (j , v)
    ∎
    where
    open ≅.≅-Reasoning
    v′ : delay A by (k + j) at (k + n)
    v′ = rew (sym (delay-+ k j n)) v
    v≅v′ : v ≅ v′
    v≅v′ = rew-to-≅ (sym (delay-+ k j n))
    pr : rew (sym (delay-+ l (k + j) (k + n))) v′
        ≅ rew (sym (delay-+ (l + k) j n)) v
    pr = delay-assoc-sym l k j n v′ v (≅.sym v≅v′)

private module μ = _⟹_ μ-◇
open ≅.≅-Reasoning

-- Shift and multiplication can be interchanged
μ-interchange : ∀{A}{n k : ℕ}{a : ◇ ◇ A at n}
             -> μ.at A (k + n) (μ-shift k n a)
              ≅ μ-shift k n (μ.at A n a)
μ-interchange {A} {n} {k} {l , y} with inspect (compareLeq l n)
μ-interchange {A} {.(l + m)} {k} {l , v} | snd==[ .l + m ] with≡ pf =
    begin
        μ.at A (k + (l + m)) (μ-shift k (l + m) (l , v))
    ≡⟨⟩
        μ.at A (k + (l + m)) (k + l , rew (sym (delay-+ k l (l + m))) v)
    ≡⟨⟩
        μ-compare A (k + (l + m)) (k + l) v′ (compareLeq (k + l) (k + (l + m)))
    ≅⟨
        ≅-cong₃ (λ x y z → μ-compare A x (k + l) y z)
            (≡-to-≅ (sym (+-assoc k l m))) v′≅v″ (compare-snd-+-assoc l m k pf)
     ⟩
        μ-compare A ((k + l) + m) (k + l) v″ (snd==[ (k + l) + m ])
    ≡⟨⟩
        μ-shift (k + l) m ⌞ rew (delay-+-left0 (k + l) m) v″ ⌟
    ≡⟨ cong! (pr k l m v″ v v″≅v) ⟩
        μ-shift (k + l) m (rew (delay-+-left0 l m) v)
    ≅⟨ ≅.sym ( μ-shift-comp {A} {m} {l} {k} {(rew (delay-+-left0 l m) v)} ) ⟩
        μ-shift k (l + m) (μ-shift l m (rew (delay-+-left0 l m) v))
    ≡⟨⟩
        μ-shift k (l + m) (μ-compare A (l + m) l v ⌞ snd==[ l + m ] ⌟)
    ≡⟨ cong! (sym pf) ⟩
        μ-shift k (l + m) (μ-compare A (l + m) l v (compareLeq l (l + m)))
    ≡⟨⟩
        μ-shift k (l + m) (μ.at A (l + m) (l , v))
    ∎
    where
    v′ : delay ◇ A by (k + l) at (k + (l + m))
    v′ = rew (sym (delay-+ k l (l + m))) v
    v≅v′ : v ≅ v′
    v≅v′ = rew-to-≅ (sym (delay-+ k l (l + m)))
    lemma-assoc : ∀{A : τ} -> (a b c : ℕ)
              -> delay ◇ A by (a + b) at (a + (b + c))
               ≡ delay ◇ A by (a + b) at ((a + b) + c)
    lemma-assoc a b c rewrite sym (+-assoc a b c) = refl
    v″ : delay ◇ A by (k + l) at ((k + l) + m)
    v″ = (rew (lemma-assoc k l m) v′)
    v′≅v″ : v′ ≅ v″
    v′≅v″ = rew-to-≅ (lemma-assoc k l m)
    v″≅v : v″ ≅ v
    v″≅v = ≅.trans (≅.sym v′≅v″) (≅.sym v≅v′)
    pr : ∀{A} (k l m : ℕ) -> Proof-≡ (delay-+-left0 {A} (k + l) m)
                                     (delay-+-left0 {A} l m)
    pr zero l m v .v ≅.refl = refl
    pr (suc k) l m = pr k l m

-- l = n + suc j
μ-interchange {A} {.n} {k} {.(n + suc l) , v} | fst==suc[ n + l ] with≡ pf =
    begin
        μ.at A (k + n) (μ-shift k n (n + suc l , v))
    ≡⟨⟩
        μ.at A (k + n) (k + (n + suc l) , rew (sym (delay-+ k (n + suc l) n)) v)
    ≡⟨⟩
        μ-compare A (k + n) (k + (n + suc l)) v′ (compareLeq (k + (n + suc l)) (k + n))
    ≅⟨ ≅-cong₃ ((λ x y z → μ-compare A (k + n) x y z))
            (≡-to-≅ (sym (+-assoc k n (suc l)))) v′≅v″ (compare-fst-+-assoc n l k pf) ⟩
        μ-compare A (k + n) ((k + n) + suc l) v″ fst==suc[ (k + n) + l ]
    ≡⟨⟩
        (k + n) + suc l , rew (delay-⊤ (k + n) l) top.tt
    ≅⟨ ◇-≅ (+-assoc k n (suc l)) refl (pr n k l) ⟩
        k + (n + suc l) , rew (sym (delay-+ k (n + suc l) n)) (rew (delay-⊤ n l) top.tt)
    ≡⟨⟩
        μ-shift k n (n + suc l , rew (delay-⊤ n l) top.tt)
    ≡⟨⟩
        μ-shift k n (μ-compare A n (n + suc l) v ⌞ fst==suc[ n + l ] ⌟)
    ≡⟨ cong! (sym pf) ⟩
        μ-shift k n (μ-compare A n (n + suc l) v (compareLeq (n + suc l) n))
    ≡⟨⟩
        μ-shift k n (μ.at A n (n + suc l , v))
    ∎
    where
    v′ : delay ◇ A by (k + (n + suc l)) at (k + n)
    v′ = (rew (sym (delay-+ k (n + suc l) n)) v)
    lemma-assoc : ∀{A : τ} -> (a b c : ℕ)
              -> delay ◇ A by (a + (b + c)) at (a + b)
               ≡ delay ◇ A by ((a + b) + c) at (a + b)
    lemma-assoc {A} a b c rewrite sym (+-assoc a b c) = refl
    v″ : delay ◇ A by ((k + n) + suc l) at (k + n)
    v″ = (rew (lemma-assoc k n (suc l)) v′)
    v′≅v″ : v′ ≅ v″
    v′≅v″ = rew-to-≅ (lemma-assoc k n (suc l))
    pr : ∀{A} (n k l : ℕ)
      -> rew (delay-⊤ {A} (k + n) l) top.tt
       ≅ rew (sym (delay-+ {A} k (n + suc l) n)) (rew (delay-⊤ n l) top.tt)
    pr n zero l = ≅.refl
    pr n (suc k) l = pr n k l

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Subtyping where

open import Light.Level using (_⊔_ ; ++_)
open import Light.Variable.Levels
open import Light.Variable.Sets

record DirectSubtyping (𝕒 : Set aℓ) (𝕓 : Set bℓ) : Set (aℓ ⊔ bℓ) where
      constructor #_
      field cast₁ : 𝕒 → 𝕓
open DirectSubtyping ⦃ ... ⦄ public

record StrictSubtyping (𝕒 : Set aℓ) (𝕓 : Set aℓ) : Set (++ aℓ)
data Subtyping {aℓ} : ∀ (𝕒 : Set aℓ) (𝕓 : Set aℓ) → Set (++ aℓ)

record StrictSubtyping {aℓ} 𝕒 𝕓 where
      inductive
      instance constructor transitivity′
      field {Thing} : Set aℓ
      field ⦃ direct ⦄ : DirectSubtyping 𝕒 Thing
      field ⦃ indirect ⦄ : Subtyping Thing 𝕓

data Subtyping where
      instance reflexivity : Subtyping 𝕒 𝕒
      instance from‐strict : ∀ ⦃ strict : StrictSubtyping 𝕒 𝕓 ⦄ → Subtyping 𝕒 𝕓

cast : ∀ ⦃ subtyping : Subtyping 𝕒 𝕓 ⦄ → 𝕒 → 𝕓
cast ⦃ subtyping = reflexivity ⦄ a = a
cast ⦃ subtyping = from‐strict ⦄ a = cast (cast₁ a)

-- Note: These cannot be instances, they must be written explicitly.
transitivity′′ : ∀ ⦃ a‐to‐b : Subtyping 𝕒 𝕓 ⦄ ⦃ b‐to‐c : Subtyping 𝕓 𝕔 ⦄ → DirectSubtyping 𝕒 𝕔
transitivity′′ ⦃ a‐to‐b = a‐to‐b ⦄ ⦃ b‐to‐c = b‐to‐c ⦄ = # λ a → cast ⦃ subtyping = b‐to‐c ⦄ (cast ⦃ subtyping = a‐to‐b ⦄ a)
transitivity : ∀ ⦃ a‐to‐b : Subtyping 𝕒 𝕓 ⦄ ⦃ b‐to‐c : Subtyping 𝕓 𝕔 ⦄ → Subtyping 𝕒 𝕔
transitivity ⦃ a‐to‐b = a‐to‐b ⦄ ⦃ b‐to‐c = b‐to‐c ⦄ = from‐strict where instance _ = transitivity′′ ⦃ a‐to‐b = a‐to‐b ⦄ ⦃ b‐to‐c = b‐to‐c ⦄

module _ ⦃ c‐to‐a : Subtyping 𝕔 𝕒 ⦄ ⦃ b‐to‐d : Subtyping 𝕓 𝕕 ⦄ where
      instance
            explicit‐variance : DirectSubtyping (𝕒 → 𝕓) (𝕔 → 𝕕)
            implicit‐variance : DirectSubtyping (∀ {a : 𝕒} → 𝕓) (∀ {c : 𝕔} → 𝕕)
            instance‐variance : DirectSubtyping (∀ ⦃ a : 𝕒 ⦄ → 𝕓) (∀ ⦃ c : 𝕔 ⦄ → 𝕕)
      explicit‐variance = # λ f c → cast ⦃ subtyping = b‐to‐d ⦄ (f (cast c))
      implicit‐variance = # λ f {c = c} → cast ⦃ subtyping = b‐to‐d ⦄ (f {a = cast c})
      instance‐variance = # λ f ⦃ c = c ⦄ → cast ⦃ subtyping = b‐to‐d ⦄ (f ⦃ a = cast c ⦄)


text:
module Issue561 where

open import Common.Char
open import Common.Prelude

primitive
  primIsDigit : Char → Bool

postulate
  IO : Set → Set
  return : ∀ {A} → A → IO A

{-# BUILTIN IO IO #-}

main : IO Bool
main = return true

max_stars_repo_name: dagit/agda

max_issues_repo_name: dagit/agda

max_forks_repo_name: dagit/agda


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

module library.types.Types where

open import library.Basics
open import library.types.Empty public
open import library.types.Unit public
open import library.types.Bool public
open import library.types.Nat public
open import library.types.Int public
open import library.types.TLevel public
open import library.types.Paths public
open import library.types.Sigma public
open import library.types.Pi public
open import library.types.Coproduct public
open import library.types.Lift public
open import library.types.Circle public
open import library.types.Span public
open import library.types.Pushout public
open import library.types.PushoutFlattening public
open import library.types.Suspension public
open import library.types.Join public
open import library.types.Torus public
open import library.types.Truncation public
open import library.types.Cospan public
open import library.types.Pullback public
open import library.types.Group public
open import library.types.Groupoid public
open import library.types.GroupSet public
open import library.types.KG1 public
open import library.types.Pointed public
open import library.types.LoopSpace public
open import library.types.HomotopyGroup public
open import library.types.PathSet public
open import library.types.FundamentalGroupoid public
open import library.types.Cover public
open import library.types.OneSkeleton public

open import library.types.PathSeq public

-- This should probably not be exported
-- module Generic1HIT {i j} (A : Type i) (B : Type j) (f g : B → A) where
--   open import library.types.Generic1HIT A B f g public

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
record Unit : Set where
  constructor tt

postulate
  C : Set
  c : C

g : C

f : Unit → C
f tt = c

record R : Set where
  constructor r

g = c


text:
-- A variant of code reported by Andreas Abel (who suggested that this
-- way to trigger the bug might have been due to NAD).

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

open import Agda.Builtin.Sigma
open import Agda.Builtin.Size

data ⊥ : Set where

record Delay (A : Set) : Set where
  coinductive
  constructor ♯
  field ♭   : Σ A λ _ → ⊥ → Delay A
  -- Recursive in order to please the termination checker.

open Delay

data D : Size → Set where
  inn : ∀ i → Delay (D i) → D (↑ i)

iter : ∀{i} → D i → ⊥
iter (inn i t) = iter (fst (♭ t))

-- Should be rejected by the termination checker.

bla : Delay (D ∞)
♭ bla = inn ∞ bla , λ()

false : ⊥
false = iter (fst (♭ bla))


text: test = forall _let_ → Set


text:
module SystemF.BigStep.Types where

open import Prelude

-- types are indexed by the number of open tvars
infixl 10 _⇒_
data Type (n : ℕ) : Set where
  Unit : Type n
  ν    : (i : Fin n) → Type n
  _⇒_  : Type n → Type n → Type n
  ∀'   : Type (suc n) → Type n

open import Data.Fin.Substitution
open import Data.Vec

module App {T} (l : Lift T Type )where
  open Lift l hiding (var)
  _/_  : ∀ {m n} → Type m → Sub T m n → Type n
  Unit / s = Unit
  ν i / s = lift (lookup i s)
  (a ⇒ b) / s = (a / s) ⇒ (b / s)
  ∀' x / s = ∀' (x / (s ↑))

  open Application (record { _/_ = _/_ }) using (_/✶_)

  open import Data.Star

  Unit-/✶-↑✶ : ∀ k {m n} (ρs : Subs T m n) → Unit /✶ ρs ↑✶ k ≡ Unit
  Unit-/✶-↑✶ k ε = refl
  Unit-/✶-↑✶ k (x ◅ ρs) = cong₂ _/_ (Unit-/✶-↑✶ k ρs) refl

  ∀-/✶-↑✶ : ∀ k {m n t} (ρs : Subs T m n) →
            ∀' t /✶ ρs ↑✶ k ≡ ∀' (t /✶ ρs ↑✶ suc k)
  ∀-/✶-↑✶ k ε        = refl
  ∀-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (∀-/✶-↑✶ k ρs) refl

  ⇒-/✶-↑✶ : ∀ k {m n t₁ t₂} (ρs : Subs T m n) →
            t₁ ⇒ t₂ /✶ ρs ↑✶ k ≡ (t₁ /✶ ρs ↑✶ k) ⇒ (t₂ /✶ ρs ↑✶ k)
  ⇒-/✶-↑✶ k ε        = refl
  ⇒-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (⇒-/✶-↑✶ k ρs) refl

tmSubst : TermSubst Type
tmSubst = record { var = ν; app = App._/_ }

open TermSubst tmSubst hiding (var; subst) public

module Lemmas where

  open import Data.Fin.Substitution.Lemmas

  tyLemmas : TermLemmas Type
  tyLemmas = record
    { termSubst = tmSubst
    ; app-var   = refl
    ; /✶-↑✶     = Lemma./✶-↑✶
    }
    where
    module Lemma {T₁ T₂} {lift₁ : Lift T₁ Type} {lift₂ : Lift T₂ Type} where

      open Lifted lift₁ using () renaming (_↑✶_ to _↑✶₁_; _/✶_ to _/✶₁_)
      open Lifted lift₂ using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂_)

      /✶-↑✶ : ∀ {m n} (ρs₁ : Subs T₁ m n) (ρs₂ : Subs T₂ m n) →
              (∀ k x → ν x /✶₁ ρs₁ ↑✶₁ k ≡ ν x /✶₂ ρs₂ ↑✶₂ k) →
              ∀ k t → t /✶₁ ρs₁ ↑✶₁ k ≡ t /✶₂ ρs₂ ↑✶₂ k
      /✶-↑✶ ρs₁ ρs₂ hyp k Unit =
        begin _ ≡⟨ App.Unit-/✶-↑✶ _ k ρs₁ ⟩ Unit ≡⟨ sym $ App.Unit-/✶-↑✶ _ k ρs₂ ⟩ _ ∎
      /✶-↑✶ ρs₁ ρs₂ hyp k (ν i) = hyp k i
      /✶-↑✶ ρs₁ ρs₂ hyp k (a ⇒ b) = begin
        _ ≡⟨ App.⇒-/✶-↑✶ _ k ρs₁ ⟩
        (a /✶₁ ρs₁ ↑✶₁ k) ⇒ (b /✶₁ ρs₁ ↑✶₁ k) ≡⟨ cong₂ _⇒_ (/✶-↑✶ ρs₁ ρs₂ hyp k a)
                                                           ((/✶-↑✶ ρs₁ ρs₂ hyp k b)) ⟩
        (a /✶₂ ρs₂ ↑✶₂ k) ⇒ (b /✶₂ ρs₂ ↑✶₂ k) ≡⟨ sym $ App.⇒-/✶-↑✶ _ k ρs₂ ⟩
        _ ∎
      /✶-↑✶ ρs₁ ρs₂ hyp k (∀' x) = begin
        _ ≡⟨ App.∀-/✶-↑✶ _ k ρs₁ ⟩
          ∀' (x /✶₁ ρs₁ ↑✶₁ (suc k)) ≡⟨ cong ∀' (/✶-↑✶ ρs₁ ρs₂ hyp (suc k) x) ⟩
        ∀' (x /✶₂ ρs₂ ↑✶₂ (suc k)) ≡⟨ sym $ App.∀-/✶-↑✶ _ k ρs₂ ⟩
        _ ∎

  open TermLemmas tyLemmas public hiding (var)


text:
record R (A : Set) : Set where
  constructor c₂
  field
    f : A → A

open module R′ (A : Set) (r : R A) = R {A = A} r
  renaming (f to f′)

_ : (@0 A : Set) → R A → A → A
_ = λ A → f′ {A = A}

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Magma.Properties where

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

open import Cubical.Algebra
open import Cubical.Algebra.Magma.Morphism

open import Cubical.Algebra.Magma.MorphismProperties public
  using (MagmaPath; uaMagma; carac-uaMagma; Magma≡; caracMagma≡)

private
  variable
    ℓ : Level

isPropIsMagma : {M : Type ℓ} {_•_ : Op₂ M} → isProp (IsMagma M _•_)
isPropIsMagma (ismagma x) (ismagma y) = cong ismagma (isPropIsSet x y)


text:
module Numeral.Natural.Oper.Summation.Range where

import      Lvl
open import Data.List
open import Data.List.Functions
open import Numeral.Natural
open import Type

_‥_ : ℕ → ℕ → List(ℕ)
_   ‥ 𝟎   = ∅
𝟎   ‥ 𝐒 b = 𝟎 ⊰ map 𝐒(𝟎 ‥ b)
𝐒 a ‥ 𝐒 b = map 𝐒(a ‥ b)

‥_ : ℕ → List(ℕ)
‥ b = 𝟎 ‥ b

_‥₌_ : ℕ → ℕ → List(ℕ)
a ‥₌ b = a ‥ 𝐒(b)

‥₌_ : ℕ → List(ℕ)
‥₌ b = 𝟎 ‥₌ b

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module Dodo.Unary.Equality where

-- Stdlib imports
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Level using (Level; _⊔_)
open import Function using (_∘_)
open import Relation.Unary using (Pred)

-- # Definitions

infix 4 _⊆₁'_ _⊆₁_ _⇔₁_

-- Binary relation subset helper. Generally, use `_⊆₁_` (below).
_⊆₁'_ : {a ℓ₁ ℓ₂ : Level} {A : Set a}
  → (P : Pred A ℓ₁)
  → (R : Pred A ℓ₂)
  → Set (a ⊔ ℓ₁ ⊔ ℓ₂)
_⊆₁'_ {A = A} P R = ∀ (x : A) → P x → R x

-- Somehow, Agda cannot infer P and R from `P ⇒ R`, and requires them explicitly passed.
-- For proof convenience, wrap the proof in this structure, which explicitly conveys P and R
-- to the type-checker.
data _⊆₁_ {a ℓ₁ ℓ₂ : Level} {A : Set a} (P : Pred A ℓ₁) (R : Pred A ℓ₂) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  ⊆: : P ⊆₁' R → P ⊆₁ R

data _⇔₁_ {a ℓ₁ ℓ₂ : Level} {A : Set a} (P : Pred A ℓ₁) (R : Pred A ℓ₂) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
  ⇔: : P ⊆₁' R → R ⊆₁' P → P ⇔₁ R

-- # Helpers

⇔₁-intro : {a ℓ₁ ℓ₂ : Level} {A : Set a}
  → {P : Pred A ℓ₁} {R : Pred A ℓ₂}
  → P ⊆₁ R
  → R ⊆₁ P
  → P ⇔₁ R
⇔₁-intro (⊆: P⊆R) (⊆: R⊆P) = ⇔: P⊆R R⊆P

⇔₁-compose : ∀ {a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Set a} {B : Set b}
    {P : Pred A ℓ₁} {Q : Pred A ℓ₂} {R : Pred B ℓ₃} {S : Pred B ℓ₄}
  → ( P ⊆₁ Q → R ⊆₁ S )
  → ( Q ⊆₁ P → S ⊆₁ R )
  → P ⇔₁ Q
  → R ⇔₁ S
⇔₁-compose ⊆-proof ⊇-proof (⇔: P⊆Q R⊆S) = ⇔₁-intro (⊆-proof (⊆: P⊆Q)) (⊇-proof (⊆: R⊆S))

-- # Properties

-- ## Properties: ⊆₁

module _ {a ℓ : Level} {A : Set a} {R : Pred A ℓ} where

  ⊆₁-refl : R ⊆₁ R
  ⊆₁-refl = ⊆: (λ _ Rx → Rx)

module _ {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a} {P : Pred A ℓ₁} {Q : Pred A ℓ₂} {R : Pred A ℓ₃} where

  ⊆₁-trans : P ⊆₁ Q → Q ⊆₁ R → P ⊆₁ R
  ⊆₁-trans (⊆: P⊆Q) (⊆: Q⊆R) = ⊆: (λ x Qx → Q⊆R x (P⊆Q x Qx))

-- ## Properties: ⇔₁

module _ {a ℓ : Level} {A : Set a} {R : Pred A ℓ} where

  ⇔₁-refl : R ⇔₁ R
  ⇔₁-refl = ⇔₁-intro ⊆₁-refl ⊆₁-refl

module _ {a ℓ₁ ℓ₂ : Level} {A : Set a} {Q : Pred A ℓ₁} {R : Pred A ℓ₂} where

  ⇔₁-sym : Q ⇔₁ R → R ⇔₁ Q
  -- WARNING: Do *NOT* use `Symmetric _⇔_`. It messes up the universe levels.
  ⇔₁-sym (⇔: Q⊆R R⊆Q) = ⇔: R⊆Q Q⊆R

module _ {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a}
    {P : Pred A ℓ₁} {Q : Pred A ℓ₂} {R : Pred A ℓ₃} where

  ⇔₁-trans : P ⇔₁ Q → Q ⇔₁ R → P ⇔₁ R
  ⇔₁-trans (⇔: P⊆Q Q⊆P) (⇔: Q⊆R R⊆Q) = ⇔₁-intro (⊆₁-trans (⊆: P⊆Q) (⊆: Q⊆R)) (⊆₁-trans (⊆: R⊆Q) (⊆: Q⊆P))

-- # Operations

-- ## Operations: ⇔₁ and ⊆₁ conversion

un-⊆₁ : ∀ {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} {R : Pred A ℓ₂}
  → P ⊆₁ R
  → P ⊆₁' R
un-⊆₁ (⊆: P⊆R) = P⊆R

unlift-⊆₁ : ∀ {a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Set a} {B : Set b}
    {P : Pred A ℓ₁} {Q : Pred A ℓ₂} {R : Pred B ℓ₃} {S : Pred B ℓ₄}
  → ( P ⊆₁ Q → R ⊆₁ S )
  → ( P ⊆₁' Q → R ⊆₁' S )
unlift-⊆₁ f P⊆Q = un-⊆₁ (f (⊆: P⊆Q))

lift-⊆₁ : ∀ {a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level} {A : Set a} {B : Set b}
    {P : Pred A ℓ₁} {Q : Pred A ℓ₂} {R : Pred B ℓ₃} {S : Pred B ℓ₄}
  → ( P ⊆₁' Q → R ⊆₁' S )
  → ( P ⊆₁ Q → R ⊆₁ S )
lift-⊆₁ f (⊆: P⊆Q) = ⊆: (f P⊆Q)

⇔₁-to-⊆₁ : {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} {Q : Pred A ℓ₂}
  → P ⇔₁ Q
    ------
  → P ⊆₁ Q
⇔₁-to-⊆₁ (⇔: P⊆Q _) = ⊆: P⊆Q

⇔₁-to-⊇₁ : {a ℓ₁ ℓ₂ : Level} {A : Set a} {P : Pred A ℓ₁} {Q : Pred A ℓ₂}
  → P ⇔₁ Q
    ------
  → Q ⊆₁ P
⇔₁-to-⊇₁ (⇔: _ Q⊆P) = ⊆: Q⊆P

-- ## Operations: ⊆₁

⊆₁-apply : ∀ {a ℓ₁ ℓ₂ : Level} {A : Set a}
    {P : Pred A ℓ₁} {Q : Pred A ℓ₂}
  → P ⊆₁ Q
  → {x : A}
  → P x
    -------
  → Q x
⊆₁-apply (⊆: P⊆Q) {x} = P⊆Q x

⊆₁-substˡ : ∀ {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a}
    {P : Pred A ℓ₁} {Q : Pred A ℓ₂} {R : Pred A ℓ₃} {x : A}
  → P ⇔₁ Q
  → P ⊆₁ R
    ------
  → Q ⊆₁ R
⊆₁-substˡ (⇔: _ Q⊆P) P⊆R = ⊆₁-trans (⊆: Q⊆P) P⊆R

⊆₁-substʳ : ∀ {a ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set a}
    {P : Pred A ℓ₁} {Q : Pred A ℓ₂} {R : Pred A ℓ₃}
  → Q ⇔₁ R
  → P ⊆₁ Q
    ------
  → P ⊆₁ R
⊆₁-substʳ (⇔: Q⊆R _) P⊆Q = ⊆₁-trans P⊆Q (⊆: Q⊆R)

≡-to-⊆₁ : {a b ℓ : Level} {A : Set a}
    {P : Pred A ℓ} {Q : Pred A ℓ}
  → P ≡ Q
    ------
  → P ⊆₁ Q
≡-to-⊆₁ refl = ⊆: (λ _ Px → Px)

-- ## Operations: ⇔₁

⇔₁-apply-⊆₁ : {a ℓ₁ ℓ₂ : Level} {A : Set a}
    {P : Pred A ℓ₁} {Q : Pred A ℓ₂}
  → P ⇔₁ Q
  → {x : A}
  → P x
    -------
  → Q x
⇔₁-apply-⊆₁ = ⊆₁-apply ∘ ⇔₁-to-⊆₁

⇔₁-apply-⊇₁ : {a ℓ₁ ℓ₂ : Level} {A : Set a}
    {P : Pred A ℓ₁} {Q : Pred A ℓ₂}
  → P ⇔₁ Q
  → {x : A}
  → Q x
    -------
  → P x
⇔₁-apply-⊇₁ = ⊆₁-apply ∘ ⇔₁-to-⊇₁

≡-to-⇔₁ : {a ℓ : Level} {A : Set a}
    {P : Pred A ℓ} {Q : Pred A ℓ}
  → P ≡ Q
    ------
  → P ⇔₁ Q
≡-to-⇔₁ refl = ⇔₁-intro ⊆₁-refl ⊆₁-refl

-- # Reasoning

-- ## Reasoning: ⊆₁

module ⊆₁-Reasoning {a ℓ₁ : Level} {A : Set a} where

  infix  3 _⊆₁∎
  infixr 2 step-⊆₁
  infix  1 begin⊆₁_

  begin⊆₁_ : {ℓ₂ : Level} {P : Pred A ℓ₁} {Q : Pred A ℓ₂}
    → P ⊆₁ Q
      ------
    → P ⊆₁ Q
  begin⊆₁_ P⊆Q = P⊆Q

  step-⊆₁ : ∀ {ℓ₂ ℓ₃ : Level}
    → (P : Pred A ℓ₁)
    → {Q : Pred A ℓ₂}
    → {R : Pred A ℓ₃}
    → Q ⊆₁ R
    → P ⊆₁ Q
      ------
    → P ⊆₁ R
  step-⊆₁ P Q⊆R P⊆Q = ⊆₁-trans P⊆Q Q⊆R

  _⊆₁∎ : ∀ (P : Pred A ℓ₁) → P ⊆₁ P
  _⊆₁∎ _ = ⊆₁-refl

  syntax step-⊆₁ P Q⊆R P⊆Q = P ⊆₁⟨ P⊆Q ⟩ Q⊆R

-- ## Reasoning: ⇔₁

module ⇔₁-Reasoning {a ℓ₁ : Level} {A : Set a} where

  infix  3 _⇔₁∎
  infixr 2 _⇔₁⟨⟩_ step-⇔₁
  infix  1 begin⇔₁_

  begin⇔₁_ : {ℓ₂ : Level} {P : Pred A ℓ₁} {Q : Pred A ℓ₂}
    → P ⇔₁ Q
      ------
    → P ⇔₁ Q
  begin⇔₁_ P⇔Q = P⇔Q

  _⇔₁⟨⟩_ : {ℓ₂ : Level}
      (P : Pred A ℓ₁)
    → {Q : Pred A ℓ₂}
    → P ⇔₁ Q
      ---------------
    → P ⇔₁ Q
  _ ⇔₁⟨⟩ x≡y = x≡y

  step-⇔₁ : ∀ {ℓ₂ ℓ₃ : Level}
    → (P : Pred A ℓ₁)
    → {Q : Pred A ℓ₂}
    → {R : Pred A ℓ₃}
    → Q ⇔₁ R
    → P ⇔₁ Q
      ---------------
    → P ⇔₁ R
  step-⇔₁ _ Q⇔R P⇔Q = ⇔₁-trans P⇔Q Q⇔R

  _⇔₁∎ : ∀ (P : Pred A ℓ₁) → P ⇔₁ P
  _⇔₁∎ _ = ⇔₁-refl

  syntax step-⇔₁ P Q⇔R P⇔Q = P ⇔₁⟨ P⇔Q ⟩ Q⇔R

max_stars_repo_name: sourcedennis/agda-dodo

max_issues_repo_name: sourcedennis/agda-dodo

max_forks_repo_name: sourcedennis/agda-dodo


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

module Data.Bool.Properties where

open import Prelude
open import Data.Bool
open import Data.Unit.Properties

T? : ∀ x → Dec (T x)
T? x .does = x
T? false .why = ofⁿ id
T? true  .why = ofʸ tt

isPropT : ∀ x → isProp (T x)
isPropT false = isProp⊥
isPropT true  = isProp⊤

discreteBool : Discrete Bool
discreteBool false y .does = not y
discreteBool true y .does = y
discreteBool false false .why = ofʸ refl
discreteBool false true .why = ofⁿ λ p → subst (bool ⊤ ⊥) p tt
discreteBool true false .why = ofⁿ λ p → subst (bool ⊥ ⊤) p tt
discreteBool true true .why = ofʸ refl

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

module P where

open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality

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

-- For now, a groupoid is just a set

Groupoid : Set₁
Groupoid = Set

mutual

-- types
  data B : Set where
    ZERO : B
    ONE : B
    _+_ : B → B → B
    _*_ : B → B → B
    _~_ : {b : B} → ⟦ b ⟧ → ⟦ b ⟧ → B

-- values
  ⟦_⟧ : B → Groupoid
  ⟦ ZERO ⟧ = ⊥
  ⟦ ONE ⟧ = ⊤
  ⟦ b₁ + b₂ ⟧ = ⟦ b₁ ⟧ ⊎ ⟦ b₂ ⟧
  ⟦ b₁ * b₂ ⟧ = ⟦ b₁ ⟧ × ⟦ b₂ ⟧
  ⟦ v₁ ~ v₂ ⟧ = v₁ ≡ v₂

-- pointed types
data PB : Set where
  POINTED : Σ B (λ b → ⟦ b ⟧) → PB
  RECIP : PB → PB

-- lift B type constructors to pointed types

_++_ : PB → PB → PB
(POINTED (b₁ , v₁)) ++ (POINTED (b₂ , v₂)) = POINTED (b₁ + b₂ , inj₁ v₁)
_ ++ _ = {!!}

_**_ : PB → PB → PB
(POINTED (b₁ , v₁)) ** (POINTED (b₂ , v₂)) = POINTED (b₁ * b₂ , (v₁ , v₂))
_ ** _ = {!!}

-- All the pi combinators now work on pointed types

data _⟷_ : PB → PB → Set₁ where
  swap⋆ : {pb₁ pb₂ : PB} → (pb₁ ** pb₂) ⟷ (pb₂ ** pb₁)
  eta : {pb : PB} → POINTED (ONE , tt) ⟷ RECIP pb

-- induction principle to reason about identities; needed ???

ind : {b : B} →
      (C : (v₁ v₂ : ⟦ b ⟧) → (p : ⟦ _~_ {b} v₁ v₂ ⟧) → Set) →
      (c : (v : ⟦ b ⟧) → C v v refl) →
      (v₁ v₂ : ⟦ b ⟧) → (p : ⟦ _~_ {b} v₁ v₂ ⟧) → C v₁ v₂ p
ind C c v .v refl = c v

-- Examples

Bool : B
Bool = ONE + ONE

false : ⟦ Bool ⟧
false = inj₁ tt

true : ⟦ Bool ⟧
true = inj₂ tt

pb1 : PB
pb1 = POINTED (Bool , false)

pb2 : PB
pb2 = POINTED (Bool , true)

FalseID : B
FalseID = _~_ {Bool} false false

pb3 : PB
pb3 = POINTED (FalseID , refl)

FalseID^2 : B
FalseID^2 = _~_ {FalseID} refl refl

pb4 : PB
pb4 = POINTED (FalseID^2 , refl)

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


text:
-- Basic intuitionistic logic of proofs, without ∨, ⊥, or +.
-- Gentzen-style formalisation of syntax with context pairs.
-- Normal forms and neutrals.

module BasicILP.Syntax.DyadicGentzenNormalForm where

open import BasicILP.Syntax.DyadicGentzen public

-- Derivations.

mutual
  -- Normal forms, or introductions.
  infix 3 _⊢ⁿᶠ_
  data _⊢ⁿᶠ_ : Cx² Ty Box → Ty → Set where
    neⁿᶠ   : ∀ {A Γ Δ}     → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ ⊢ⁿᶠ A
    lamⁿᶠ  : ∀ {A B Γ Δ}   → Γ , A ⁏ Δ ⊢ⁿᶠ B → Γ ⁏ Δ ⊢ⁿᶠ A ▻ B

    boxⁿᶠ  : ∀ {Ψ Ω A Γ Δ} → (x : Ψ ⁏ Ω ⊢ A)
                           → Γ ⁏ Δ ⊢ⁿᶠ [ Ψ ⁏ Ω ⊢ x ] A

    pairⁿᶠ : ∀ {A B Γ Δ}   → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ⁿᶠ B → Γ ⁏ Δ ⊢ⁿᶠ A ∧ B
    unitⁿᶠ : ∀ {Γ Δ}       → Γ ⁏ Δ ⊢ⁿᶠ ⊤

  -- Neutrals, or eliminations.
  infix 3 _⊢ⁿᵉ_
  data _⊢ⁿᵉ_ : Cx² Ty Box → Ty → Set where
    varⁿᵉ   : ∀ {A Γ Δ}         → A ∈ Γ → Γ ⁏ Δ ⊢ⁿᵉ A
    appⁿᵉ   : ∀ {A B Γ Δ}       → Γ ⁏ Δ ⊢ⁿᵉ A ▻ B → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ⁿᵉ B

    mvarⁿᵉ  : ∀ {Ψ Ω A x Γ Δ}   → [ Ψ ⁏ Ω ⊢ x ] A ∈ Δ
                                → {{_ : Γ ⁏ Δ ⊢⋆ⁿᶠ Ψ}}
                                → {{_ : Γ ⁏ Δ ⊢⍟ⁿᶠ Ω}}
                                → Γ ⁏ Δ ⊢ⁿᵉ A

    unboxⁿᵉ : ∀ {Ψ Ω A C x Γ Δ} → Γ ⁏ Δ ⊢ⁿᵉ [ Ψ ⁏ Ω ⊢ x ] A
                                → Γ ⁏ Δ , [ Ψ ⁏ Ω ⊢ x ] A ⊢ⁿᶠ C
                                → Γ ⁏ Δ ⊢ⁿᵉ C

    fstⁿᵉ   : ∀ {A B Γ Δ}       → Γ ⁏ Δ ⊢ⁿᵉ A ∧ B → Γ ⁏ Δ ⊢ⁿᵉ A
    sndⁿᵉ   : ∀ {A B Γ Δ}       → Γ ⁏ Δ ⊢ⁿᵉ A ∧ B → Γ ⁏ Δ ⊢ⁿᵉ B

  infix 3 _⊢⋆ⁿᶠ_
  _⊢⋆ⁿᶠ_ : Cx² Ty Box → Cx Ty → Set
  Γ ⁏ Δ ⊢⋆ⁿᶠ ∅     = 𝟙
  Γ ⁏ Δ ⊢⋆ⁿᶠ Ξ , A = Γ ⁏ Δ ⊢⋆ⁿᶠ Ξ × Γ ⁏ Δ ⊢ⁿᶠ A

  infix 3 _⊢⍟ⁿᶠ_
  _⊢⍟ⁿᶠ_ : Cx² Ty Box → Cx Box → Set
  Γ ⁏ Δ ⊢⍟ⁿᶠ ∅                    = 𝟙
  Γ ⁏ Δ ⊢⍟ⁿᶠ Ξ , [ Ψ ⁏ Ω ⊢ x ] A = Γ ⁏ Δ ⊢⍟ⁿᶠ Ξ × Γ ⁏ Δ ⊢ⁿᶠ [ Ψ ⁏ Ω ⊢ x ] A

infix 3 _⊢⋆ⁿᵉ_
_⊢⋆ⁿᵉ_ : Cx² Ty Box → Cx Ty → Set
Γ ⁏ Δ ⊢⋆ⁿᵉ ∅     = 𝟙
Γ ⁏ Δ ⊢⋆ⁿᵉ Ξ , A = Γ ⁏ Δ ⊢⋆ⁿᵉ Ξ × Γ ⁏ Δ ⊢ⁿᵉ A

infix 3 _⊢⍟ⁿᵉ_
_⊢⍟ⁿᵉ_ : Cx² Ty Box → Cx Box → Set
Γ ⁏ Δ ⊢⍟ⁿᵉ ∅                    = 𝟙
Γ ⁏ Δ ⊢⍟ⁿᵉ Ξ , [ Ψ ⁏ Ω ⊢ x ] A = Γ ⁏ Δ ⊢⍟ⁿᵉ Ξ × Γ ⁏ Δ ⊢ⁿᵉ [ Ψ ⁏ Ω ⊢ x ] A

-- Translation to simple terms.

mutual
  nf→tm : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ ⊢ A
  nf→tm (neⁿᶠ t)     = ne→tm t
  nf→tm (lamⁿᶠ t)    = lam (nf→tm t)
  nf→tm (boxⁿᶠ t)    = box t
  nf→tm (pairⁿᶠ t u) = pair (nf→tm t) (nf→tm u)
  nf→tm unitⁿᶠ       = unit

  ne→tm : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ ⊢ A
  ne→tm (varⁿᵉ i)                = var i
  ne→tm (appⁿᵉ t u)              = app (ne→tm t) (nf→tm u)
  ne→tm (mvarⁿᵉ i {{ts}} {{us}}) = mvar i {{nf→tm⋆ ts}} {{nf→tm⍟ us}}
  ne→tm (unboxⁿᵉ t u)            = unbox (ne→tm t) (nf→tm u)
  ne→tm (fstⁿᵉ t)                = fst (ne→tm t)
  ne→tm (sndⁿᵉ t)                = snd (ne→tm t)

  nf→tm⋆ : ∀ {Ξ Γ Δ} → Γ ⁏ Δ ⊢⋆ⁿᶠ Ξ → Γ ⁏ Δ ⊢⋆ Ξ
  nf→tm⋆ {∅}     ∙        = ∙
  nf→tm⋆ {Ξ , A} (ts , t) = nf→tm⋆ ts , nf→tm t

  nf→tm⍟ : ∀ {Ξ Γ Δ} → Γ ⁏ Δ ⊢⍟ⁿᶠ Ξ → Γ ⁏ Δ ⊢⍟ Ξ
  nf→tm⍟ {∅}     ∙        = ∙
  nf→tm⍟ {Ξ , _} (ts , t) = nf→tm⍟ ts , nf→tm t

ne→tm⋆ : ∀ {Ξ Γ Δ} → Γ ⁏ Δ ⊢⋆ⁿᵉ Ξ → Γ ⁏ Δ ⊢⋆ Ξ
ne→tm⋆ {∅}     ∙        = ∙
ne→tm⋆ {Ξ , A} (ts , t) = ne→tm⋆ ts , ne→tm t

ne→tm⍟ : ∀ {Ξ Γ Δ} → Γ ⁏ Δ ⊢⍟ⁿᵉ Ξ → Γ ⁏ Δ ⊢⍟ Ξ
ne→tm⍟ {∅}     ∙        = ∙
ne→tm⍟ {Ξ , _} (ts , t) = ne→tm⍟ ts , ne→tm t

-- Monotonicity with respect to context inclusion.

mutual
  mono⊢ⁿᶠ : ∀ {A Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢ⁿᶠ A → Γ′ ⁏ Δ ⊢ⁿᶠ A
  mono⊢ⁿᶠ η (neⁿᶠ t)     = neⁿᶠ (mono⊢ⁿᵉ η t)
  mono⊢ⁿᶠ η (lamⁿᶠ t)    = lamⁿᶠ (mono⊢ⁿᶠ (keep η) t)
  mono⊢ⁿᶠ η (boxⁿᶠ t)    = boxⁿᶠ t
  mono⊢ⁿᶠ η (pairⁿᶠ t u) = pairⁿᶠ (mono⊢ⁿᶠ η t) (mono⊢ⁿᶠ η u)
  mono⊢ⁿᶠ η unitⁿᶠ       = unitⁿᶠ

  mono⊢ⁿᵉ : ∀ {A Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢ⁿᵉ A → Γ′ ⁏ Δ ⊢ⁿᵉ A
  mono⊢ⁿᵉ η (varⁿᵉ i)                = varⁿᵉ (mono∈ η i)
  mono⊢ⁿᵉ η (appⁿᵉ t u)              = appⁿᵉ (mono⊢ⁿᵉ η t) (mono⊢ⁿᶠ η u)
  mono⊢ⁿᵉ η (mvarⁿᵉ i {{ts}} {{us}}) = mvarⁿᵉ i {{mono⊢⋆ⁿᶠ η ts}} {{mono⊢⍟ⁿᶠ η us}}
  mono⊢ⁿᵉ η (unboxⁿᵉ t u)            = unboxⁿᵉ (mono⊢ⁿᵉ η t) (mono⊢ⁿᶠ η u)
  mono⊢ⁿᵉ η (fstⁿᵉ t)                = fstⁿᵉ (mono⊢ⁿᵉ η t)
  mono⊢ⁿᵉ η (sndⁿᵉ t)                = sndⁿᵉ (mono⊢ⁿᵉ η t)

  mono⊢⋆ⁿᶠ : ∀ {Ξ Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢⋆ⁿᶠ Ξ → Γ′ ⁏ Δ ⊢⋆ⁿᶠ Ξ
  mono⊢⋆ⁿᶠ {∅}     η ∙        = ∙
  mono⊢⋆ⁿᶠ {Ξ , A} η (ts , t) = mono⊢⋆ⁿᶠ η ts , mono⊢ⁿᶠ η t

  mono⊢⍟ⁿᶠ : ∀ {Ξ Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢⍟ⁿᶠ Ξ → Γ′ ⁏ Δ ⊢⍟ⁿᶠ Ξ
  mono⊢⍟ⁿᶠ {∅}     η ∙        = ∙
  mono⊢⍟ⁿᶠ {Ξ , _} η (ts , t) = mono⊢⍟ⁿᶠ η ts , mono⊢ⁿᶠ η t

mono⊢⋆ⁿᵉ : ∀ {Ξ Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢⋆ⁿᵉ Ξ → Γ′ ⁏ Δ ⊢⋆ⁿᵉ Ξ
mono⊢⋆ⁿᵉ {∅}     η ∙        = ∙
mono⊢⋆ⁿᵉ {Ξ , A} η (ts , t) = mono⊢⋆ⁿᵉ η ts , mono⊢ⁿᵉ η t

mono⊢⍟ⁿᵉ : ∀ {Ξ Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢⍟ⁿᵉ Ξ → Γ′ ⁏ Δ ⊢⍟ⁿᵉ Ξ
mono⊢⍟ⁿᵉ {∅}     η ∙        = ∙
mono⊢⍟ⁿᵉ {Ξ , _} η (ts , t) = mono⊢⍟ⁿᵉ η ts , mono⊢ⁿᵉ η t

-- Monotonicity with respect to modal context inclusion.

mutual
  mmono⊢ⁿᶠ : ∀ {A Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ⁿᶠ A → Γ ⁏ Δ′ ⊢ⁿᶠ A
  mmono⊢ⁿᶠ θ (neⁿᶠ t)     = neⁿᶠ (mmono⊢ⁿᵉ θ t)
  mmono⊢ⁿᶠ θ (lamⁿᶠ t)    = lamⁿᶠ (mmono⊢ⁿᶠ θ t)
  mmono⊢ⁿᶠ θ (boxⁿᶠ t)    = boxⁿᶠ t
  mmono⊢ⁿᶠ θ (pairⁿᶠ t u) = pairⁿᶠ (mmono⊢ⁿᶠ θ t) (mmono⊢ⁿᶠ θ u)
  mmono⊢ⁿᶠ θ unitⁿᶠ       = unitⁿᶠ

  mmono⊢ⁿᵉ : ∀ {A Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ⁿᵉ A → Γ ⁏ Δ′ ⊢ⁿᵉ A
  mmono⊢ⁿᵉ θ (varⁿᵉ i)                = varⁿᵉ i
  mmono⊢ⁿᵉ θ (appⁿᵉ t u)              = appⁿᵉ (mmono⊢ⁿᵉ θ t) (mmono⊢ⁿᶠ θ u)
  mmono⊢ⁿᵉ θ (mvarⁿᵉ i {{ts}} {{us}}) = mvarⁿᵉ (mono∈ θ i) {{mmono⊢⋆ⁿᶠ θ ts}} {{mmono⊢⍟ⁿᶠ θ us}}
  mmono⊢ⁿᵉ θ (unboxⁿᵉ t u)            = unboxⁿᵉ (mmono⊢ⁿᵉ θ t) (mmono⊢ⁿᶠ (keep θ) u)
  mmono⊢ⁿᵉ θ (fstⁿᵉ t)                = fstⁿᵉ (mmono⊢ⁿᵉ θ t)
  mmono⊢ⁿᵉ θ (sndⁿᵉ t)                = sndⁿᵉ (mmono⊢ⁿᵉ θ t)

  mmono⊢⋆ⁿᶠ : ∀ {Ξ Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢⋆ⁿᶠ Ξ → Γ ⁏ Δ′ ⊢⋆ⁿᶠ Ξ
  mmono⊢⋆ⁿᶠ {∅}     θ ∙        = ∙
  mmono⊢⋆ⁿᶠ {Ξ , A} θ (ts , t) = mmono⊢⋆ⁿᶠ θ ts , mmono⊢ⁿᶠ θ t

  mmono⊢⍟ⁿᶠ : ∀ {Ξ Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢⍟ⁿᶠ Ξ → Γ ⁏ Δ′ ⊢⍟ⁿᶠ Ξ
  mmono⊢⍟ⁿᶠ {∅}     θ ∙        = ∙
  mmono⊢⍟ⁿᶠ {Ξ , _} θ (ts , t) = mmono⊢⍟ⁿᶠ θ ts , mmono⊢ⁿᶠ θ t

mmono⊢⋆ⁿᵉ : ∀ {Ξ Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢⋆ⁿᵉ Ξ → Γ ⁏ Δ′ ⊢⋆ⁿᵉ Ξ
mmono⊢⋆ⁿᵉ {∅}     θ ∙        = ∙
mmono⊢⋆ⁿᵉ {Ξ , A} θ (ts , t) = mmono⊢⋆ⁿᵉ θ ts , mmono⊢ⁿᵉ θ t

mmono⊢⍟ⁿᵉ : ∀ {Ξ Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢⍟ⁿᵉ Ξ → Γ ⁏ Δ′ ⊢⍟ⁿᵉ Ξ
mmono⊢⍟ⁿᵉ {∅}     θ ∙        = ∙
mmono⊢⍟ⁿᵉ {Ξ , _} θ (ts , t) = mmono⊢⍟ⁿᵉ θ ts , mmono⊢ⁿᵉ θ t

-- Monotonicity using context pairs.

mono²⊢ⁿᶠ : ∀ {A Π Π′} → Π ⊆² Π′ → Π ⊢ⁿᶠ A → Π′ ⊢ⁿᶠ A
mono²⊢ⁿᶠ (η , θ) = mono⊢ⁿᶠ η ∘ mmono⊢ⁿᶠ θ

mono²⊢ⁿᵉ : ∀ {A Π Π′} → Π ⊆² Π′ → Π ⊢ⁿᵉ A → Π′ ⊢ⁿᵉ A
mono²⊢ⁿᵉ (η , θ) = mono⊢ⁿᵉ η ∘ mmono⊢ⁿᵉ θ

-- Generalised reflexivity.

refl⊢⋆ⁿᵉ : ∀ {Γ Ψ Δ} → {{_ : Ψ ⊆ Γ}} → Γ ⁏ Δ ⊢⋆ⁿᵉ Ψ
refl⊢⋆ⁿᵉ {∅}     {{done}}   = ∙
refl⊢⋆ⁿᵉ {Γ , A} {{skip η}} = mono⊢⋆ⁿᵉ weak⊆ (refl⊢⋆ⁿᵉ {{η}})
refl⊢⋆ⁿᵉ {Γ , A} {{keep η}} = mono⊢⋆ⁿᵉ weak⊆ (refl⊢⋆ⁿᵉ {{η}}) , varⁿᵉ top

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module EquationalTheory where

open import Library
open import Syntax
open import RenamingAndSubstitution

-- Single collapsing substitution.

sub1 : ∀{Γ σ τ} → Tm Γ σ → Tm (Γ , σ) τ → Tm Γ τ
sub1 {Γ}{σ}{τ} u t = sub (subId , u) t

-- Typed β-η-equality.

data _≡βη_ {Γ : Cxt} : ∀{σ} → Tm Γ σ → Tm Γ σ → Set where

  -- Axioms.

  beta≡  : ∀{σ τ} {t : Tm (Γ , σ) τ} {u : Tm Γ σ} →

           --------------------------
           app (abs t) u ≡βη sub1 u t

  eta≡   : ∀{σ τ} (t : Tm Γ (σ ⇒ τ)) →

           -------------------------------------
           abs (app (weak _ t) (var zero)) ≡βη t

  -- Congruence rules.

  var≡   : ∀{σ} (x : Var Γ σ) →

           ---------------
           var x ≡βη var x

  abs≡   : ∀{σ τ}{t t' : Tm (Γ , σ) τ} →

           t ≡βη t' →
           ----------------
           abs t ≡βη abs t'

  app≡   : ∀{σ τ}{t t' : Tm Γ (σ ⇒ τ)}{u u' : Tm Γ σ} →

          t ≡βη t' → u ≡βη u' →
          ---------------------
          app t u ≡βη app t' u'

  -- Equivalence rules.

  refl≡  : ∀{a} (t {t'} : Tm Γ a) →

           t ≡ t' →
           -------
           t ≡βη t'

  sym≡   : ∀{a}{t t' : Tm Γ a}

           (t'≡t : t' ≡βη t) →
           -----------------
           t ≡βη t'

  trans≡ : ∀{a}{t₁ t₂ t₃ : Tm Γ a}

           (t₁≡t₂ : t₁ ≡βη t₂) (t₂≡t₃ : t₂ ≡βη t₃) →
           ----------------------------------
           t₁ ≡βη t₃

-- A calculation on renamings needed for renaming of eta≡.

ren-eta≡ : ∀ {Γ Δ a b} (t : Tm Γ (a ⇒ b)) (ρ : Ren Δ Γ) →
        ren (wkr ρ , zero) (ren (wkr renId) t) ≡ ren (wkr {σ = a} renId) (ren ρ t)
ren-eta≡ t ρ = begin
  ren (wkr ρ , zero) (ren (wkr renId) t)     ≡⟨ sym (rencomp _ _ _) ⟩
  ren (renComp (wkr ρ , zero) (wkr renId)) t ≡⟨ cong (λ ρ₁ → ren ρ₁ t) (lemrr _ _ _) ⟩
  ren (renComp (wkr ρ) renId) t              ≡⟨ cong (λ ρ₁ → ren ρ₁ t) (ridr _) ⟩
  ren (wkr ρ) t                              ≡⟨ cong (λ ρ₁ → ren ρ₁ t) (cong wkr (sym (lidr _))) ⟩
  ren (wkr (renComp renId ρ)) t              ≡⟨ cong (λ ρ₁ → ren ρ₁ t) (sym (wkrcomp _ _)) ⟩
  ren (renComp (wkr renId) ρ) t              ≡⟨ rencomp _ _ _ ⟩
  ren (wkr renId) (ren ρ t)                  ∎ where open ≡-Reasoning

-- Definitional equality is closed under renaming.

ren≡βη : ∀{Γ a} {t : Tm Γ a}{t' : Tm Γ a} → t ≡βη t' → ∀{Δ}(ρ : Ren Δ Γ) →
        ren ρ t ≡βη ren ρ t'

ren≡βη (beta≡ {t = t}{u = u}) ρ = trans≡ beta≡ $ refl≡ _ $
  trans (subren (subId , ren ρ u) (liftr ρ) t)
        (trans (cong (λ xs → sub xs t)
                     (cong₂ Sub._,_
                            (trans (lemsr subId (ren ρ u) ρ)
                            (trans (sidl (ren2sub ρ)) (sym $ sidr (ren2sub ρ))))
                            (ren2subren ρ u)))
               (sym $ rensub ρ (subId , u) t))
  -- TODO: factor out reasoning about renamings and substitutions

ren≡βη (eta≡ {a} t) ρ rewrite ren-eta≡ t ρ = eta≡ (ren ρ t)

-- OLD:
-- ren≡βη (eta≡ t) ρ = trans≡
--   (abs≡ (app≡ (refl≡ _
--     (trans (sym $ rencomp (liftr ρ) (wkr renId) t)
--            (trans (cong (λ xs → ren xs t)
--                         (trans (lemrr (wkr ρ) zero renId)
--                                (trans (ridr (wkr ρ))
--                                       (trans (cong wkr (sym (lidr ρ)))
--                                              (sym (wkrcomp renId ρ))))))
--                   (rencomp (wkr renId) ρ t))))
--     (refl≡ _)))
--   (eta≡ _)

ren≡βη (var≡ x)       ρ = var≡ (lookr ρ x)
ren≡βη (abs≡ p)       ρ = abs≡ (ren≡βη p (liftr ρ))
ren≡βη (app≡ p q)     ρ = app≡ (ren≡βη p ρ) (ren≡βη q ρ)

ren≡βη (refl≡ _ refl) ρ = refl≡ _ refl
ren≡βη (sym≡ p)       ρ = sym≡ (ren≡βη p ρ)
ren≡βη (trans≡ p q)   ρ = trans≡ (ren≡βη p ρ) (ren≡βη q ρ)

max_stars_repo_name: ryanakca/strong-normalization

max_issues_repo_name: ryanakca/strong-normalization

max_forks_repo_name: ryanakca/strong-normalization


text:
open import Relation.Binary.Core

module InsertSort.Impl2.Correctness.Order {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)  where

open import Data.List
open import Function using (_∘_)
open import InsertSort.Impl2 _≤_ tot≤
open import List.Sorted _≤_
open import OList _≤_
open import OList.Properties _≤_

theorem-insertSort-sorted : (xs : List A) → Sorted (forget (insertSort xs))
theorem-insertSort-sorted = lemma-olist-sorted ∘ insertSort


text:
{-# OPTIONS --prop #-}

open import Agda.Builtin.Nat

data T : Nat → Prop where
  To : T zero
  Tn : ∀ n → T n

ummm : ∀ n → T n → {!   !}
ummm n t = {! t  !}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- A variant of code reported by Andreas Abel.

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

open import Common.Coinduction renaming (∞ to Delay)
open import Common.Size
open import Common.Product

data ⊥ : Set where

record Stream (A : Set) : Set where
  inductive
  constructor delay
  field
    force : Delay (A × Stream A)
open Stream

head : ∀{A} → Stream A → A
head s = proj₁ (♭ (force s))

-- This type should be empty, as Stream A is isomorphic to ℕ → A.
data D : (i : Size) → Set where
  lim : ∀ i → Stream (D i) → D (↑ i)

-- Emptiness witness for D.
empty : ∀ i → D i → ⊥
empty .(↑ i) (lim i s) = empty i (head s)

-- BAD: But we can construct an inhabitant.
inh : Stream (D ∞)
inh = delay (♯ (lim ∞ inh , inh)) -- Should be rejected by termination checker.

absurd : ⊥
absurd = empty ∞ (lim ∞ inh)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Oscar.Prelude
open import Oscar.Class
open import Oscar.Class.IsPrecategory
open import Oscar.Class.IsCategory
open import Oscar.Class.HasEquivalence
open import Oscar.Class.Reflexivity
open import Oscar.Class.Symmetry
open import Oscar.Class.Transextensionality
open import Oscar.Class.Transassociativity
open import Oscar.Class.Transleftidentity
open import Oscar.Class.Transrightidentity
open import Oscar.Class.Transitivity
open import Oscar.Class.Precategory
open import Oscar.Class.Category
open import Oscar.Property.Setoid.Proposequality
open import Oscar.Property.Setoid.Proposextensequality
open import Oscar.Data.Proposequality
import Oscar.Class.Reflexivity.Function
import Oscar.Class.Transextensionality.Proposequality

module Oscar.Property.Category.Function where

module _ {𝔬 : Ł} where

  instance

    TransitivityFunction : Transitivity.class Function⟦ 𝔬 ⟧
    TransitivityFunction .⋆ f g = g ∘ f

module _ {𝔬 : Ł} where

  instance

    HasEquivalenceFunction : ∀ {A B : Ø 𝔬} → HasEquivalence (Function⟦ 𝔬 ⟧ A B) 𝔬
    HasEquivalenceFunction .⋆ = _≡̇_
    HasEquivalenceFunction .Rℭlass.⋆⋆ = !

  instance

    TransassociativityFunction : Transassociativity.class Function⟦ 𝔬 ⟧ _≡̇_ transitivity
    TransassociativityFunction .⋆ _ _ _ _ = ∅

  instance

    𝓣ransextensionalityFunctionProposextensequality : Transextensionality.class Function⟦ 𝔬 ⟧ Proposextensequality transitivity
    𝓣ransextensionalityFunctionProposextensequality .⋆ {f₂ = f₂} f₁≡̇f₂ g₁≡̇g₂ x rewrite f₁≡̇f₂ x = g₁≡̇g₂ (f₂ x)

  instance

    IsPrecategoryFunction : IsPrecategory Function⟦ 𝔬 ⟧ _≡̇_ transitivity
    IsPrecategoryFunction = ∁

  instance

    TransleftidentityFunction : Transleftidentity.class Function⟦ 𝔬 ⟧ _≡̇_ ε transitivity
    TransleftidentityFunction .⋆ _ = ∅

    TransrightidentityFunction : Transrightidentity.class Function⟦ 𝔬 ⟧ _≡̇_ ε transitivity
    TransrightidentityFunction .⋆ _ = ∅

  instance

    IsCategoryFunction : IsCategory Function⟦ 𝔬 ⟧ _≡̇_ ε transitivity
    IsCategoryFunction = ∁

  PrecategoryFunction : Precategory _ _ _
  PrecategoryFunction = ∁ Function⟦ 𝔬 ⟧ Proposextensequality transitivity

  CategoryFunction : Category _ _ _
  CategoryFunction = ∁ Function⟦ 𝔬 ⟧ Proposextensequality ε transitivity


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Floats
------------------------------------------------------------------------

module Data.Float where

open import Data.Bool hiding (_≟_)
open import Relation.Nullary.Decidable
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
open import Relation.Binary.PropositionalEquality.TrustMe
open import Data.String using (String)

postulate
  Float : Set

{-# BUILTIN FLOAT Float #-}

primitive
  primFloatEquality : Float → Float → Bool
  primShowFloat     : Float → String

show : Float → String
show = primShowFloat

_≟_ : (x y : Float) → Dec (x ≡ y)
x ≟ y with primFloatEquality x y
... | true  = yes trustMe
... | false = no whatever
  where postulate whatever : _


text:
module Issue2447.Type-error where

import Issue2447.M

Rejected : Set
Rejected = Set


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

open import Groups.Homomorphisms.Definition
open import Groups.Definition
open import Setoids.Setoids
open import Rings.Definition

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Rings.Homomorphisms.Definition where

record RingHom {m n o p : _} {A : Set m} {B : Set n} {SA : Setoid {m} {o} A} {SB : Setoid {n} {p} B} {_+A_ : A → A → A} {_*A_ : A → A → A} (R : Ring SA _+A_ _*A_) {_+B_ : B → B → B} {_*B_ : B → B → B} (S : Ring SB _+B_ _*B_) (f : A → B) : Set (m ⊔ n ⊔ o ⊔ p) where
  open Ring S
  open Group additiveGroup
  open Setoid SB
  field
    preserves1 : f (Ring.1R R) ∼ 1R
    ringHom : {r s : A} → f (r *A s) ∼ (f r) *B (f s)
    groupHom : GroupHom (Ring.additiveGroup R) additiveGroup f