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

module PiTracedLevel0 where

open import Data.Empty   using (⊥; ⊥-elim)
open import Data.Unit    using (⊤; tt)
open import Data.Sum     using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂)

------------------------------------------------------------------------------
-- Level 0 of Pi (with trace)
--
-- ZERO is a type with no elements
-- ONE is a type with one element 'tt'
-- PLUS ONE ONE is a type with elements 'false' and 'true'
-- and so on for all finite types built from ZERO, ONE, PLUS, and TIMES
--
-- We also have that U is a type with elements ZERO, ONE, PLUS ONE ONE,
--   TIMES BOOL BOOL, etc.

data U : Set where
  ZERO  : U
  ONE   : U
  PLUS  : U → U → U
  TIMES : U → U → U

⟦_⟧ : U → Set
⟦ ZERO ⟧        = ⊥
⟦ ONE ⟧         = ⊤
⟦ PLUS t₁ t₂ ⟧  = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
⟦ TIMES t₁ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧

infix  30 _⟷_
infixr 50 _◎_

-- Combinators, permutations, or paths depending on the perspective

data _⟷_ : U → U → Set where
  unite₊  : {t : U} → PLUS ZERO t ⟷ t
  uniti₊  : {t : U} → t ⟷ PLUS ZERO t
  swap₊   : {t₁ t₂ : U} → PLUS t₁ t₂ ⟷ PLUS t₂ t₁
  assocl₊ : {t₁ t₂ t₃ : U} → PLUS t₁ (PLUS t₂ t₃) ⟷ PLUS (PLUS t₁ t₂) t₃
  assocr₊ : {t₁ t₂ t₃ : U} → PLUS (PLUS t₁ t₂) t₃ ⟷ PLUS t₁ (PLUS t₂ t₃)
  unite⋆  : {t : U} → TIMES ONE t ⟷ t
  uniti⋆  : {t : U} → t ⟷ TIMES ONE t
  swap⋆   : {t₁ t₂ : U} → TIMES t₁ t₂ ⟷ TIMES t₂ t₁
  assocl⋆ : {t₁ t₂ t₃ : U} → TIMES t₁ (TIMES t₂ t₃) ⟷ TIMES (TIMES t₁ t₂) t₃
  assocr⋆ : {t₁ t₂ t₃ : U} → TIMES (TIMES t₁ t₂) t₃ ⟷ TIMES t₁ (TIMES t₂ t₃)
  absorbr  : {t : U} → TIMES ZERO t ⟷ ZERO
  absorbl : {t : U} → TIMES t ZERO ⟷ ZERO
  factorzr : {t : U} → ZERO ⟷ TIMES t ZERO
  factorzl : {t : U} → ZERO ⟷ TIMES ZERO t
  dist    : {t₁ t₂ t₃ : U} →
            TIMES (PLUS t₁ t₂) t₃ ⟷ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃)
  factor  : {t₁ t₂ t₃ : U} →
            PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) ⟷ TIMES (PLUS t₁ t₂) t₃
  id⟷    : {t : U} → t ⟷ t
  _◎_     : {t₁ t₂ t₃ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
  _⊕_     : {t₁ t₂ t₃ t₄ : U} →
            (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (PLUS t₁ t₂ ⟷ PLUS t₃ t₄)
  _⊗_     : {t₁ t₂ t₃ t₄ : U} →
            (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (TIMES t₁ t₂ ⟷ TIMES t₃ t₄)
  trace   : {t t₁ t₂ : U} → (PLUS t₁ t ⟷ PLUS t₂ t) → (t₁ ⟷ t₂)

! : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
! unite₊    = uniti₊
! uniti₊    = unite₊
! swap₊     = swap₊
! assocl₊   = assocr₊
! assocr₊   = assocl₊
! unite⋆    = uniti⋆
! uniti⋆    = unite⋆
! swap⋆     = swap⋆
! assocl⋆   = assocr⋆
! assocr⋆   = assocl⋆
! absorbl     = factorzr
! absorbr     = factorzl
! factorzl  = absorbr
! factorzr = absorbl
! dist      = factor
! factor    = dist
! id⟷      = id⟷
! (c₁ ◎ c₂) = ! c₂ ◎ ! c₁
! (c₁ ⊕ c₂) = (! c₁) ⊕ (! c₂)
! (c₁ ⊗ c₂) = (! c₁) ⊗ (! c₂)
! (trace c) = trace (! c)

------------------------------------------------------------------------------
-- Cat

open import Level using () renaming (zero to lzero)
open import Data.Unit
open import Relation.Binary.Core using (IsEquivalence)
open import Data.Product using (_,_)

open import Categories.Category
open import Categories.Groupoid
open import Categories.Monoidal
open import Categories.Monoidal.Helpers
open import Categories.Bifunctor
open import Categories.NaturalIsomorphism
open import Categories.Monoidal.Braided
open import Categories.Monoidal.Symmetric
open import Categories.RigCategory
open import Categories.Monoidal.Traced

triv≡ : {t₁ t₂ : U} → (f g : t₁ ⟷ t₂) → Set
triv≡ _ _ = ⊤

triv≡Equiv : {t₁ t₂ : U} → IsEquivalence (triv≡ {t₁} {t₂})
triv≡Equiv = record
  { refl = tt
  ; sym = λ _ → tt
  ; trans = λ _ _ → tt
  }

PiCat : Category lzero lzero lzero
PiCat = record
  { Obj = U
  ; _⇒_ = _⟷_
  ; _≡_ = triv≡
  ; id = id⟷
  ; _∘_ = λ y⟷z x⟷y → x⟷y ◎ y⟷z
  ; assoc = tt
  ; identityˡ = tt
  ; identityʳ = tt
  ; equiv = triv≡Equiv
  ; ∘-resp-≡ = λ _ _ → tt
  }

-- and a groupoid

PiGroupoid : Groupoid PiCat
PiGroupoid = record
  { _⁻¹ = !
  ; iso = record { isoˡ = tt ; isoʳ = tt }
  }

-- additive bifunctor and monoidal structure
⊕-bifunctor : Bifunctor PiCat PiCat PiCat
⊕-bifunctor = record
  { F₀ = λ {(u , v) → PLUS u v}
  ; F₁ = λ {(x⟷y , z⟷w) → x⟷y ⊕ z⟷w }
  ; identity = tt
  ; homomorphism = tt
  ; F-resp-≡ = λ _ → tt
  }

module ⊎h = MonoidalHelperFunctors PiCat ⊕-bifunctor ZERO

0⊕x≡x : NaturalIsomorphism ⊎h.id⊗x ⊎h.x
0⊕x≡x = record
  { F⇒G = record
    { η = λ X → unite₊
    ; commute = λ _ → tt }
  ; F⇐G = record
    { η = λ X → uniti₊
    ; commute = λ _ → tt }
  ; iso = λ X → record { isoˡ = tt; isoʳ = tt }
  }

x⊕0≡x : NaturalIsomorphism ⊎h.x⊗id ⊎h.x
x⊕0≡x = record
  { F⇒G = record
    { η = λ X → swap₊ ◎ unite₊  -- !!!
    ; commute = λ _ → tt
    }
  ; F⇐G = record
    { η = λ X → uniti₊ ◎ swap₊
    ; commute = λ _ → tt
    }
  ; iso = λ X → record
    { isoˡ = tt
    ; isoʳ = tt
    }
  }

[x⊕y]⊕z≡x⊕[y⊕z] : NaturalIsomorphism ⊎h.[x⊗y]⊗z ⊎h.x⊗[y⊗z]
[x⊕y]⊕z≡x⊕[y⊕z] = record
  { F⇒G = record
    { η = λ X → assocr₊
    ; commute = λ f → tt
    }
  ; F⇐G = record
    { η = λ X → assocl₊
    ; commute = λ _ → tt
    }
  ; iso = λ X → record
    { isoˡ = tt
    ; isoʳ = tt
    }
  }

M⊕ : Monoidal PiCat
M⊕ = record
  { ⊗ = ⊕-bifunctor
  ; id = ZERO
  ; identityˡ = 0⊕x≡x
  ; identityʳ = x⊕0≡x
  ; assoc = [x⊕y]⊕z≡x⊕[y⊕z]
  ; triangle = tt
  ; pentagon = tt
  }

-- multiplicative bifunctor and monoidal structure
⊗-bifunctor : Bifunctor PiCat PiCat PiCat
⊗-bifunctor =  record
  { F₀ = λ {(u , v) → TIMES u v}
  ; F₁ = λ {(x⟷y , z⟷w) → x⟷y ⊗ z⟷w }
  ; identity = tt
  ; homomorphism = tt
  ; F-resp-≡ = λ _ → tt
  }

module ⊗h = MonoidalHelperFunctors PiCat ⊗-bifunctor ONE

1⊗x≡x : NaturalIsomorphism ⊗h.id⊗x ⊗h.x
1⊗x≡x = record
  { F⇒G = record
    { η = λ X → unite⋆
    ; commute = λ _ → tt }
  ; F⇐G = record
    { η = λ X → uniti⋆
    ; commute = λ _ → tt }
  ; iso = λ X → record { isoˡ = tt; isoʳ = tt }
  }

x⊗1≡x : NaturalIsomorphism ⊗h.x⊗id ⊗h.x
x⊗1≡x = record
  { F⇒G = record
    { η = λ X → swap⋆ ◎ unite⋆  -- !!!
    ; commute = λ _ → tt
    }
  ; F⇐G = record
    { η = λ X → uniti⋆ ◎ swap⋆
    ; commute = λ _ → tt
    }
  ; iso = λ X → record
    { isoˡ = tt
    ; isoʳ = tt
    }
  }

[x⊗y]⊗z≡x⊗[y⊗z] : NaturalIsomorphism ⊗h.[x⊗y]⊗z ⊗h.x⊗[y⊗z]
[x⊗y]⊗z≡x⊗[y⊗z] = record
  { F⇒G = record
    { η = λ X → assocr⋆
    ; commute = λ f → tt
    }
  ; F⇐G = record
    { η = λ X → assocl⋆
    ; commute = λ _ → tt
    }
  ; iso = λ X → record
    { isoˡ = tt
    ; isoʳ = tt
    }
  }

M⊗ : Monoidal PiCat
M⊗ = record
  { ⊗ = ⊗-bifunctor
  ; id = ONE
  ; identityˡ = 1⊗x≡x
  ; identityʳ = x⊗1≡x
  ; assoc = [x⊗y]⊗z≡x⊗[y⊗z]
  ; triangle = tt
  ; pentagon = tt
  }

x⊕y≡y⊕x : NaturalIsomorphism ⊎h.x⊗y ⊎h.y⊗x
x⊕y≡y⊕x = record
  { F⇒G = record { η = λ X → swap₊ ; commute = λ f → tt }
  ; F⇐G = record { η = λ X → swap₊ ; commute = λ f → tt }
  ; iso = λ X → record { isoˡ = tt ; isoʳ = tt } }

BM⊕ : Braided M⊕
BM⊕ = record { braid = x⊕y≡y⊕x ; hexagon₁ = tt ; hexagon₂ = tt }

x⊗y≡y⊗x : NaturalIsomorphism ⊗h.x⊗y ⊗h.y⊗x
x⊗y≡y⊗x = record
  { F⇒G = record { η = λ X → swap⋆ ; commute = λ f → tt }
  ; F⇐G = record { η = λ X → swap⋆ ; commute = λ f → tt }
  ; iso = λ X → record { isoˡ = tt ; isoʳ = tt } }

BM⊗ : Braided M⊗
BM⊗ = record { braid = x⊗y≡y⊗x ; hexagon₁ = tt ; hexagon₂ = tt }

SBM⊕ : Symmetric BM⊕
SBM⊕ = record { symmetry = tt }

-- trace

Pi0Traced : Traced SBM⊕
Pi0Traced = record {
    trace = trace
  ; vanish_id = tt
  ; vanish_⊗ = tt
  ; superpose = tt
  ; yank = tt
  }

--

SBM⊗ : Symmetric BM⊗
SBM⊗ = record { symmetry = tt }

module r = BimonoidalHelperFunctors SBM⊕ BM⊗

x⊗0≡0 : NaturalIsomorphism r.x⊗0 r.0↑
x⊗0≡0 = record
  { F⇒G = record { η = λ X → absorbl ; commute = λ f → tt }
  ; F⇐G = record { η = λ X → factorzr ; commute = λ f → tt }
  ; iso = λ X → record { isoˡ = tt ; isoʳ = tt }
  }

0⊗x≡0 : NaturalIsomorphism r.0⊗x r.0↑
0⊗x≡0 = record
  { F⇒G = record { η = λ X → absorbr ; commute = λ f → tt }
  ; F⇐G = record { η = λ X → factorzl ; commute = λ f → tt }
  ; iso = λ X → record { isoˡ = tt ; isoʳ = tt }
  }

x⊗[y⊕z]≡[x⊗y]⊕[x⊗z] : NaturalIsomorphism r.x⊗[y⊕z] r.[x⊗y]⊕[x⊗z]
x⊗[y⊕z]≡[x⊗y]⊕[x⊗z] = record -- this probably says we need distl/distr
  { F⇒G = record { η = λ X → swap⋆ ◎ dist ◎ (swap⋆ ⊕ swap⋆) ; commute = λ f → tt }
  ; F⇐G = record { η = λ X → (swap⋆ ⊕ swap⋆) ◎ factor ◎ swap⋆ ; commute = λ f → tt }
  ; iso = λ X → record { isoˡ = tt ; isoʳ = tt }
  }

[x⊕y]⊗z≡[x⊗z]⊕[y⊗z] : NaturalIsomorphism r.[x⊕y]⊗z r.[x⊗z]⊕[y⊗z]
[x⊕y]⊗z≡[x⊗z]⊕[y⊗z] = record
  { F⇒G = record { η = λ X → dist ; commute = λ f → tt }
  ; F⇐G = record { η = λ X → factor ; commute = λ f → tt }
  ; iso = λ X → record { isoˡ = tt ; isoʳ = tt }
  }

Pi0Rig : RigCategory SBM⊕ BM⊗
Pi0Rig = record
  { distribₗ = x⊗[y⊕z]≡[x⊗y]⊕[x⊗z]
  ; distribᵣ = [x⊕y]⊗z≡[x⊗z]⊕[y⊗z]
  ; annₗ = x⊗0≡0
  ; annᵣ = 0⊗x≡0
  }

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

open import Prelude
open import GSeTT.Syntax
open import GSeTT.Rules
open import GSeTT.Disks
open import GSeTT.Uniqueness-Derivations
open import GSeTT.Dec-Type-Checking
open import CaTT.Ps-contexts
open import CaTT.Relation
open import CaTT.Uniqueness-Derivations-Ps

module CaTT.Decidability-ps where
  ∅-is-not-ps : ∀ x A → ¬ (nil ⊢ps x # A)
  ∅-is-not-ps x A ∅⊢psx with psvar ∅⊢psx
  ... | var _ ()

  ps-carrier : ∀{Γ A B C x y z} → ((Γ :: (x , A)) :: (y , B)) ⊢ps z # C → ((Σ Pre-Tm λ a → (⇒ A a (Var x) == B)) × (x == length Γ)) × (y == S (length Γ))
  ps-carrier (psd Γ⊢ps) = ps-carrier Γ⊢ps
  ps-carrier (pse _ idp idp idp idp idp) = ((_ , idp) , idp) , idp

  Γ+⊢ps→Γ⊢ps : ∀ {Γ x A a y B z} → ((Γ :: (y , B)) :: (z , ⇒ B (Var a) (Var y))) ⊢ps x # A → Γ ⊢ps a # B
  Γ+⊢ps→Γ⊢ps (psd Γ⊢ps) = Γ+⊢ps→Γ⊢ps Γ⊢ps
  Γ+⊢ps→Γ⊢ps (pse Γ⊢ps idp idp p idp idp) = transport ((=Var (snd (fst (=⇒ p)))) ^) Γ⊢ps

  𝔻0-var : ∀ x A → Pre-𝔻 0 ⊢t (Var x) # A → x == 0
  𝔻0-var x A (var _ (inr (idp , _))) = idp

  𝔻0-type : ∀ x A → Pre-𝔻 0 ⊢t (Var x) # A → A == ∗
  𝔻0-type x A (var _ (inr (idp , idp))) = idp

  ⊢psx→⊢ps : ∀ {Γ x A} → Γ ⊢ps x # A → Γ ⊢ps
  ⊢psx→⊢ps {A = ∗} Γ⊢psx = ps Γ⊢psx
  ⊢psx→⊢ps {A = ⇒ A (Var _) (Var _)} Γ⊢psx = ⊢psx→⊢ps (psd Γ⊢psx)

  dec-⊢-dim : ∀ {Γ} → Γ ⊢C → (n : ℕ) → dec (Σ (ℕ × Pre-Ty) (λ (x , A) → (Γ ⊢t (Var x) # A) × (dim A == n)))
  dec-⊢-dim {nil} _ n = inr λ{((x , A) , ((var _ ())  , _))}
  dec-⊢-dim {Γ :: (x , A)} Γ+⊢@(cc Γ⊢ _ _) n with eqdecℕ (dim A) n
  ... | inl idp = inl ((x , A) , (var Γ+⊢ (inr (idp , idp)) , idp))
  ... | inr dimA≠n with dec-⊢-dim Γ⊢ n
  ... | inl ((y , B) , ((var _ y∈Γ) , dimB=n)) = inl ((y , B ), (var Γ+⊢ (inl y∈Γ) , dimB=n))
  ... | inr ¬∃y = inr λ{((z , C) , ((var _ (inl z∈Γ)) , idp)) → ¬∃y ((z , C) , (var Γ⊢ z∈Γ , idp));
                        ((z , C) , ((var _ (inr (idp , idp))) , idp)) → dimA≠n idp}

  dim-pse : ∀ {Γ x A y B} → ((Γ :: (x , A)) :: (y , B)) ⊢ps y # B → (∀ z C → ((Γ :: (x , A)) :: (y , B)) ⊢ps z # C → dim C ≤ dim B)
  dim-pse Γ⊢psy z C (psd Γ⊢psf) = Sn≤m→n≤m (dim-pse Γ⊢psy _ _ Γ⊢psf)
  dim-pse Γ⊢psy z C (pse Γ⊢psz idp idp idp idp idp) = n≤n _

  private
    tgt-⟿ : ∀ {Γ x A y z a} → Γ ⊢t Var x # ⇒ A (Var y) (Var z) → Γ , x ⟿ a → z ≠ a → Γ , z ⟿ a
    tgt-⟿ Γ⊢x (∂⁺⟿ Γ⊢'x) z≠a with unique-type Γ⊢x Γ⊢'x idp
    ... | idp = ⊥-elim (z≠a idp)
    tgt-⟿ Γ⊢x (x⟿∂⁺ Γ⊢'x x⟿a) z≠a with unique-type Γ⊢x Γ⊢'x idp
    ... | idp = x⟿a

  ⇒≠∗ : ∀ {A t u} → ⇒ A t u ≠ ∗
  ⇒≠∗ ()

  dec-Σ⊢T : ∀ {Γ t} → dec (Σ Pre-Ty λ A → Γ ⊢t t # A)
  dec-Σ⊢T {nil} {Var x} = inr λ{(_ , var _ ())}
  dec-Σ⊢T {Γ+@(Γ :: (y , B))} {Var x} with dec-⊢C Γ+ | eqdecℕ x y
  ... | inr Γ+⊬ | _ = inr λ (A , Γ+⊢x) → Γ+⊬ (Γ⊢t:A→Γ⊢ Γ+⊢x)
  ... | inl Γ+⊢ | inl idp = inl (B , var Γ+⊢ (inr (idp , idp)))
  ... | inl Γ+⊢ | inr x≠y with dec-Σ⊢T {Γ} {Var x}
  ... | inl (A , Γ⊢x)= inl (A , wkt Γ⊢x Γ+⊢)
  ... | inr Γ⊬x = inr λ{ (B , var _ (inr (idp , idp))) → x≠y idp;
                         (B , var (cc Γ⊢ _ _) (inl x#B∈Γ)) → Γ⊬x (B , var Γ⊢ x#B∈Γ)}

  dec-⟿ : ∀ Γ x y → dec (Γ , x ⟿ y)
  dec-⟿-aux : ∀ Γ x A y → Γ ⊢t (Var x) # A → dec (Γ , x ⟿ y)
  dec-⟿-aux Γ x ∗ y Γ⊢x = inr λ{(∂⁺⟿ Γ⊢'x) → ⇒≠∗ (unique-type Γ⊢'x Γ⊢x idp) ; (x⟿∂⁺ Γ⊢'x _) → ⇒≠∗ (unique-type Γ⊢'x Γ⊢x idp)}
  dec-⟿-aux Γ x (⇒ A (Var _) (Var z)) y Γ⊢x with eqdecℕ z y | dec-⟿-aux Γ z A y (Γ⊢tgt (Γ⊢t:A→Γ⊢A Γ⊢x))
  ... | inl idp | _ = inl (∂⁺⟿ Γ⊢x)
  ... | inr _ | inl x⟿z = inl (x⟿∂⁺ Γ⊢x x⟿z)
  ... | inr z≠y | inr ¬x⟿z = inr λ x⟿y → ¬x⟿z (tgt-⟿ Γ⊢x x⟿y z≠y)
  dec-⟿ Γ x y with dec-Σ⊢T {Γ} {Var x}
  ... | inr Γ⊬x = inr λ{(∂⁺⟿ Γ⊢x) → Γ⊬x (_ , Γ⊢x) ; (x⟿∂⁺ Γ⊢x _) → Γ⊬x (_ , Γ⊢x)}
  ... | inl (A , Γ⊢x) = dec-⟿-aux Γ x A y Γ⊢x

  Γ⊢psx-dim-⟿ : ∀ {Γ x A y B} → Γ ⊢ps x # A → Γ ⊢ps y # B → dim B < dim A → Γ , x ⟿ y
  Γ⊢psx-dim-⟿ Γ⊢psx pss dB<dA with 𝔻0-type _ _ (psvar Γ⊢psx)
  ... | idp = ⊥-elim (Sn≰n _ dB<dA)
  Γ⊢psx-dim-⟿ {Γ} {x} {A} {y} {B} Γ⊢psx (psd Γ⊢psf) dB<dA with eqdecℕ (S (dim B)) (dim A)
  ... | inl SdB=dA = transport {B = λ a → Γ , a ⟿ y} (Γ⊢psx-dim Γ⊢psf Γ⊢psx SdB=dA) (∂⁺⟿ (psvar Γ⊢psf))
  ... | inr SdB≠dA = T⟿ (Γ⊢psx-dim-⟿ Γ⊢psx Γ⊢psf (≤×≠→< dB<dA SdB≠dA)) (∂⁺⟿ (psvar Γ⊢psf))
  Γ⊢psx-dim-⟿ Γ⊢psx Γ⊢psy@(pse _ idp idp idp idp idp) dB<dA = ⊥-elim (Sn≰n _ (≤T dB<dA (dim-pse Γ⊢psy _ _ Γ⊢psx)))

  ⟿→psx : ∀ {Γ x A y} → Γ ⊢ps x # A → Γ , x ⟿ y → Σ Pre-Ty λ B → Γ ⊢ps y # B
  ⟿→psx Γ⊢psx (∂⁺⟿ Γ⊢x) with unique-type (psvar Γ⊢psx) Γ⊢x idp
  ... | idp = _ , (psd Γ⊢psx)
  ⟿→psx Γ⊢psx (x⟿∂⁺ Γ⊢x z⟿y) with unique-type (psvar Γ⊢psx) Γ⊢x idp
  ... | idp = ⟿→psx (psd Γ⊢psx) z⟿y

  pse-max : ∀ {Γ x A y B} → ((Γ :: (x , A)) :: (y , B)) ⊢ps y # B → (∀ z C → ((Γ :: (x , A)) :: (y , B)) ⊢ps z # C → (y == z) + (((Γ :: (x , A)) :: (y , B)) , y ⟿ z))
  pse-max {B = B} Γ⊢psy z C Γ⊢psz with ℕ-trichotomy (dim B) (dim C)
  ... | inl (inl dimB<dimC) = ⊥-elim (Sn≰n _ (≤T dimB<dimC (dim-pse Γ⊢psy _ _ Γ⊢psz)) )
  ... | inl (inr dimC<dimB) = inr (Γ⊢psx-dim-⟿ Γ⊢psy Γ⊢psz dimC<dimB)
  ... | inr dimB=dimC = inl (Γ⊢psx-dim Γ⊢psy Γ⊢psz dimB=dimC)

  ⊢psx→max : ∀ {Γ x A} → Γ ⊢ps x # A → (Σ (ℕ × Pre-Ty) λ (y , B) → (Γ ⊢ps y # B) × (∀ z C → Γ ⊢ps z # C → (y == z) + (Γ , y ⟿ z)))
  ⊢psx→max pss = (0 , ∗) , (pss , λ z C 𝔻0⊢psx → inl (𝔻0-var z C (psvar 𝔻0⊢psx) ^))
  ⊢psx→max (psd Γ⊢psx) = ⊢psx→max Γ⊢psx
  ⊢psx→max {((Γ :: (_ , B)) :: (_ , C))} {x} {A} Γ+⊢ps@(pse Γ⊢psx idp idp idp idp idp) = (S (length Γ) , C) , (Γ+⊢ps , pse-max Γ+⊢ps)

  -- TODO : move case_of_ in Prelude
  case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
  case x of f = f x

  ill-formed-1st-var : ∀ {y A} → ¬ ((nil :: (S y , A)) ⊢C)
  ill-formed-1st-var (cc _ _ ())

  ill-formed-1st-type : ∀ {y A a b} → ¬ ((nil :: (y , ⇒ A a b)) ⊢C)
  ill-formed-1st-type (cc _ (ar (var _ ()) _) _)

  dec-⊢psx-max : ∀ {Γ} → dec (Σ (ℕ × Pre-Ty) λ (x , A) → (Γ ⊢ps x # A) × (∀ y B → Γ ⊢ps y # B → (x == y) + (Γ , x ⟿ y)))
  dec-⊢psx-max {nil} = inr λ ((x , A) , (nil⊢psx , _ )) → ∅-is-not-ps _ _ nil⊢psx
  dec-⊢psx-max {nil :: (O , ∗)} = inl ((0 , ∗) , (pss , λ y B  𝔻0⊢psy → inl (𝔻0-var _ _ (psvar 𝔻0⊢psy) ^)))
  dec-⊢psx-max {nil :: (O , ⇒ _ _ _)} = inr λ ((x , A) , (Γ⊢psx , _ )) → ill-formed-1st-type (psv Γ⊢psx)
  dec-⊢psx-max {nil :: (S z , C)} = inr λ ((x , A) , (Γ⊢psx , _ )) → ill-formed-1st-var (psv Γ⊢psx)
  dec-⊢psx-max {(Γ :: (z , C)) :: (f , ∗)} = inr λ ((x , A) , (Γ+⊢psx , _)) → ⇒≠∗ (snd (fst (fst (ps-carrier Γ+⊢psx))))
  dec-⊢psx-max {(Γ :: (z , C)) :: (f , ⇒ D (Var a) (Var b))} with eqdec-PreTy C D | eqdecℕ z (length Γ) | eqdecℕ (length Γ) b | eqdecℕ f (S (length Γ))
  ... | inr C≠D | _ | _ | _  = inr λ ((x , A) , (Γ+⊢psx , _)) → C≠D (fst (fst (=⇒ (snd (fst (fst (ps-carrier Γ+⊢psx)))))))
  ... | inl idp | inr z≠l | _ | _  = inr λ ((x , A) , (Γ+⊢psx , _)) → z≠l (snd (fst (ps-carrier Γ+⊢psx)))
  ... | inl idp | inl idp | inr l≠b | _  = inr λ ((x , A) , (Γ+⊢psx , _)) → l≠b (=Var (snd (=⇒ (snd (fst (fst (ps-carrier Γ+⊢psx)))))))
  ... | inl idp | inl idp | inl idp | inr f≠Sl  = inr λ ((x , A) , (Γ+⊢psx , _)) → f≠Sl (snd (ps-carrier Γ+⊢psx))
  ... | inl idp | inl idp | inl idp | inl idp with dec-⊢psx-max {Γ}
  ... | inr ¬Γ⊢ps = inr λ ((x , A) , (Γ+⊢psx , _)) → ¬Γ⊢ps (⊢psx→max (Γ+⊢ps→Γ⊢ps Γ+⊢psx))
  ... | inl ((c , E) , (Γ⊢psc , cmax)) with eqdecℕ c a | eqdec-PreTy E C
  ... | inl idp | inl idp = let Γ+⊢ps = pse Γ⊢psc idp idp idp idp idp in inl ((S (length Γ) , ⇒ C (Var a) (Var (length Γ))) , (Γ+⊢ps , pse-max Γ+⊢ps))
  ... | inl idp | inr E≠C = inr λ ((x , A) , (Γ+⊢psx , _)) → E≠C (unique-type (psvar Γ⊢psc) (psvar (Γ+⊢ps→Γ⊢ps Γ+⊢psx)) idp)
  ... | inr c≠a | _ with dec-⟿ Γ c a
  ... | inr ¬c⟿a = inr λ ((x , A) , (Γ+⊢psx , _)) → case cmax _ _ (Γ+⊢ps→Γ⊢ps Γ+⊢psx) of λ{(inl c=a) → c≠a c=a; (inr c⟿a) → ¬c⟿a c⟿a }
  ... | inl c⟿a with (⟿→psx Γ⊢psc c⟿a)
  ... | (F , Γ⊢psa) with eqdec-PreTy F C
  ... | inl idp = let Γ+⊢ps = pse Γ⊢psa idp idp idp idp idp in inl ((S (length Γ) , ⇒ C (Var a) (Var (length Γ))) , (Γ+⊢ps  , pse-max Γ+⊢ps))
  ... | inr F≠C = inr λ ((x , A) , (Γ+⊢psx , _)) → F≠C (unique-type (psvar Γ⊢psa) (psvar (Γ+⊢ps→Γ⊢ps Γ+⊢psx)) idp)

  dec-⊢ps : ∀ Γ → dec(Γ ⊢ps)
  dec-⊢ps Γ with dec-⊢psx-max {Γ}
  ... | inl ((x , A) , (Γ⊢psx , _)) = inl (⊢psx→⊢ps Γ⊢psx)
  ... | inr ¬Γ⊢psx = inr λ {(ps Γ⊢psy) → ¬Γ⊢psx (⊢psx→max Γ⊢psy)}

ext: agda

max_stars_repo_name: thibautbenjamin/catt-formalization

max_issues_repo_name: thibautbenjamin/catt-formalization

max_forks_repo_name: thibautbenjamin/catt-formalization


text:
open import FRP.JS.String using ( _<_ )
open import FRP.JS.True using ( True )

module FRP.JS.String.Properties where

postulate
  <-trans : ∀ {k l m} → True (k < l) → True (l < m) → True (k < m)

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


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

open import Categories.Category using () renaming (Category to Setoid-Category)
open import Categories.Category.Monoidal using (Monoidal)

module Categories.Enriched.Functor {o ℓ e} {V : Setoid-Category o ℓ e}
                                   (M : Monoidal V) where

open import Level

open import Categories.Enriched.Category M
open import Categories.Functor using () renaming (Functor to Setoid-Functor)
open import Categories.Morphism.Reasoning V
open import Categories.Category.Monoidal.Reasoning M using (⊗-distrib-over-∘)

open Setoid-Category V renaming (Obj to ObjV; id to idV)
open Commutation
open HomReasoning
open Monoidal M

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

  field
    map₀ : C.Obj → D.Obj
    map₁ : ∀ {X Y} → C [ X , Y ] ⇒ D [ map₀ X , map₀ Y ]

    identity     : ∀ {X} → map₁ ∘ C.id ≈ D.id {map₀ X}
    homomorphism : ∀ {X Y Z} →
      [ C [ Y , Z ] ⊗₀ C [ X , Y ] ⇒ D [ map₀ X , map₀ Z ] ]⟨
        C.⊚           ⇒⟨ C [ X , Z ]                ⟩  map₁
      ≈ map₁ ⊗₁ map₁  ⇒⟨ D [ _ , _ ] ⊗₀ D [ _ , _ ] ⟩  D.⊚
      ⟩

    -- We don't need an analogue of F-resp-≈ because |hom A B| is not
    -- a hom-Setoid but a hom-object (in V) and the functorial action
    -- is not a Setoid-map but a V-morphism.  Whether V-objects have a
    -- notion of equality, and whether such equalities are preserved
    -- by V-morphisms, depends entirely on V.

  -- Shorthands for the functorial actions that work well as
  -- post-projections.

  ₀ = map₀
  ₁ = map₁

Endofunctor : ∀ {c} → Category c → Set (ℓ ⊔ e ⊔ c)
Endofunctor C = Functor C C

id : ∀ {c} {C : Category c} → Endofunctor C
id {_} {C} = record
  { map₀         = λ X → X
  ; map₁         = idV
  ; identity     = identityˡ
  ; homomorphism = id-comm-sym ○ ∘-resp-≈ʳ (⟺ ⊗.identity)
  }
  where
  open Category C
  module ⊗ = Setoid-Functor ⊗

infixr 9 _∘F_

_∘F_ : ∀ {c d e} {C : Category c} {D : Category d} {E : Category e} →
       Functor D E → Functor C D → Functor C E
_∘F_ {_} {_} {_} {C} {D} {E} G F = record
  { map₀     = λ X → G.₀ (F.₀ X)
  ; map₁     = G.₁ ∘ F.₁
  ; identity = begin
      (G.₁ ∘ F.₁) ∘ C.id   ≈⟨ pullʳ F.identity ⟩
      G.₁ ∘ D.id           ≈⟨ G.identity ⟩
      E.id                 ∎
  ; homomorphism = begin
      (G.₁ ∘ F.₁) ∘ C.⊚                  ≈⟨ pullʳ F.homomorphism ⟩
      G.₁ ∘ (D.⊚ ∘ F.₁ ⊗₁ F.₁)           ≈⟨ pullˡ G.homomorphism ⟩
      (E.⊚ ∘ G.₁ ⊗₁ G.₁) ∘ F.₁ ⊗₁ F.₁    ≈˘⟨ pushʳ ⊗-distrib-over-∘ ⟩
      E.⊚ ∘ (G.₁ ∘ F.₁) ⊗₁ (G.₁ ∘ F.₁)   ∎
  }
  where
    module C = Category C
    module D = Category D
    module E = Category E
    module F = Functor F
    module G = Functor G

-- A V-enriched functor induces an ordinary functor on the underlying
-- categories.

module _ {c d} {C : Category c} {D : Category d} where

  UnderlyingFunctor : Functor C D → Setoid-Functor (Underlying C) (Underlying D)
  UnderlyingFunctor F = record
    { F₀           = F.₀
    ; F₁           = F.₁ ∘_
    ; identity     = F.identity
    ; homomorphism = λ {_} {_} {_} {f} {g} → begin
        F.₁ ∘ C.⊚ ∘ g ⊗₁ f ∘ λ⇐             ≈⟨ pullˡ F.homomorphism ⟩
        (D.⊚ ∘ F.₁ ⊗₁ F.₁) ∘ g ⊗₁ f ∘ λ⇐    ≈˘⟨ pushʳ (pushˡ ⊗-distrib-over-∘) ⟩
        D.⊚ ∘ (F.₁ ∘ g) ⊗₁ (F.₁ ∘ f) ∘ λ⇐   ∎
    ; F-resp-≈     = ∘-resp-≈ʳ
    }
    where
      module C = Category C
      module D = Category D
      module F = Functor F

      λ⇐ = unitorˡ.to

  module UnderlyingFunctor F = Setoid-Functor (UnderlyingFunctor F)

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Unsafe machine word operations
------------------------------------------------------------------------

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

module Data.Word.Unsafe where

import Data.Nat as ℕ
open import Data.Word using (Word64; toℕ)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Binary.PropositionalEquality.TrustMe

------------------------------------------------------------------------
-- An informative equality test.

_≟_ : (a b : Word64) → Dec (a ≡ b)
a ≟ b with toℕ a ℕ.≟ toℕ b
... | yes _ = yes trustMe
... | no  _ = no whatever
  where postulate whatever : _


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

open import HoTT
open import cohomology.Theory
open import groups.Exactness
open import groups.ExactSequence

open import cw.CW

module cw.cohomology.HigherCoboundaryGrid {i} (OT : OrdinaryTheory i)
  {n} (⊙skel : ⊙Skeleton {i} (S (S n))) (ac : ⊙has-cells-with-choice 0 ⊙skel i) where

open OrdinaryTheory OT
open import cw.cohomology.WedgeOfCells OT
open import cw.cohomology.HigherCoboundary OT ⊙skel
open import cw.cohomology.GridPtdMap (⊙cw-incl-last (⊙cw-init ⊙skel)) (⊙cw-incl-last ⊙skel)
import cw.cohomology.GridLongExactSequence
private
  module GLES n = cw.cohomology.GridLongExactSequence
    cohomology-theory n (⊙cw-incl-last (⊙cw-init ⊙skel)) (⊙cw-incl-last ⊙skel)

{-
  Xn --> X(n+1) -----> X(n+2)
   |       |             |
   v       v             v
   1 -> X(n+1)/n ---> X(n+2)/n
           |    this     |
           v      one    v
           1 -----> X(n+2)/(n+1)
-}

private
  n≤SSn : n ≤ S (S n)
  n≤SSn = inr (ltSR ltS)

private
  -- separate lemmas to speed up the type checking
  abstract
    lemma₀-exact₀ : is-exact
      (C-fmap (ℕ-to-ℤ (S n)) Z/X-to-Z/Y)
      (C-fmap (ℕ-to-ℤ (S n)) Y/X-to-Z/X)
    lemma₀-exact₀ = exact-seq-index 2 $ GLES.C-grid-cofiber-exact-seq (ℕ-to-ℤ n)

    lemma₀-exact₁ : is-exact (C-fmap (ℕ-to-ℤ (S n)) Y/X-to-Z/X) cw-co∂-last
    lemma₀-exact₁ = exact-seq-index 0 $ GLES.C-grid-cofiber-exact-seq (ℕ-to-ℤ (S n))

    lemma₀-trivial : is-trivialᴳ (C (ℕ-to-ℤ (S n)) Z/Y)
    lemma₀-trivial = CXₙ/Xₙ₋₁-<-is-trivial ⊙skel ltS ac

Ker-cw-co∂-last : C (ℕ-to-ℤ (S n)) (⊙Cofiber (⊙cw-incl-tail n≤SSn ⊙skel))
               ≃ᴳ Ker.grp cw-co∂-last
Ker-cw-co∂-last = Exact2.G-trivial-implies-H-iso-ker
  lemma₀-exact₀ lemma₀-exact₁ lemma₀-trivial

private
  -- separate lemmas to speed up the type checking
  abstract
    lemma₁-exact₀ : is-exact cw-co∂-last (C-fmap (ℕ-to-ℤ (S (S n))) Z/X-to-Z/Y)
    lemma₁-exact₀ = exact-seq-index 1 $ GLES.C-grid-cofiber-exact-seq (ℕ-to-ℤ (S n))

    lemma₁-exact₁ : is-exact
      (C-fmap (ℕ-to-ℤ (S (S n))) Z/X-to-Z/Y)
      (C-fmap (ℕ-to-ℤ (S (S n))) Y/X-to-Z/X)
    lemma₁-exact₁ = exact-seq-index 2 $ GLES.C-grid-cofiber-exact-seq (ℕ-to-ℤ (S n))

    lemma₁-trivial : is-trivialᴳ (C (ℕ-to-ℤ (S (S n))) Y/X)
    lemma₁-trivial = CXₙ/Xₙ₋₁->-is-trivial (⊙cw-init ⊙skel) ltS
      (⊙init-has-cells-with-choice ⊙skel ac)

Coker-cw-co∂-last : CokerCo∂ ≃ᴳ C (ℕ-to-ℤ (S (S n))) (⊙Cofiber (⊙cw-incl-tail n≤SSn ⊙skel))
Coker-cw-co∂-last = Exact2.L-trivial-implies-coker-iso-K
  lemma₁-exact₀ lemma₁-exact₁ (CXₙ/Xₙ₋₁-is-abelian ⊙skel (ℕ-to-ℤ (S (S n)))) lemma₁-trivial

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
-- Andreas, 2019-04-10, re #3687, better test case for #1926

-- {-# OPTIONS -v interaction.contents.record:20 #-}

module _ (Foo : Set) where

open import Agda.Builtin.Sigma

test : {A : Set} {B : A → Set} (r : Σ A B) → Set
test r = {!r!}  -- C-c C-o

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{- Conatural numbers (Tesla Ice Zhang, Feb. 2019)

This file defines:

- A coinductive natural number representation which is dual to
  the inductive version (zero | suc Nat → Nat) of natural numbers.

- Trivial operations (succ, pred) and the pattern synonyms on conaturals.

While this definition can be seen as a coinductive wrapper of an inductive
datatype, another way of definition is to define an inductive datatype that
wraps a coinductive thunk of Nat.
The standard library uses the second approach:

https://github.com/agda/agda-stdlib/blob/master/src/Codata/Conat.agda

The first approach is chosen to exploit guarded recursion and to avoid the use
of Sized Types.
-}

{-# OPTIONS --cubical --no-import-sorts --safe --guardedness #-}
module Cubical.Codata.Conat.Base where

open import Cubical.Data.Unit
open import Cubical.Data.Sum

open import Cubical.Core.Everything

record Conat : Type₀
Conat′ = Unit ⊎ Conat
record Conat where
  coinductive
  constructor conat′
  field force : Conat′
open Conat public

pattern zero  = inl tt
pattern suc n = inr n

conat : Conat′ → Conat
force (conat a) = a

succ : Conat → Conat
force (succ a) = suc a

succ′ : Conat′ → Conat′
succ′ n = suc λ where .force → n

pred′ : Conat′ → Conat′
pred′  zero   = zero
pred′ (suc x) = force x

pred′′ : Conat′ → Conat
force (pred′′ zero) = zero
pred′′ (suc x) = x

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
-- Andreas, 2016-06-21, issue #2054
-- Size solver should not default to ∞ in where block signatures

-- {-# OPTIONS --v tc.size:20 #-}

-- {-# BUILTIN SIZEUNIV SizeU #-}
-- {-# BUILTIN SIZE     Size   #-}
-- {-# BUILTIN SIZESUC  ↑_     #-}
-- {-# BUILTIN SIZEINF  ∞     #-}

open import Common.Size

data N : Size → Set where
  suc : ∀{i} (a : N i) → N (↑ i)

record R (j : Size) : Set where
  field num : N j

postulate
  W : ∀ {j} (ft : R j) → Set
  E : ∀ {j} (ft : R j) (P : (w : W ft) → Set) → Set

test : ∀ {j} (ft : R j) → Set
test {j} ft = E {j} ft testw
  where
    postulate
      testw : ∀ {ft : R _} (w : W ft) → Set

-- Should work
-- _ should not set to ∞, but to j

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Agda.Builtin.Nat

data Vec (A : Set) : Nat → Set where
  [] : Vec A 0
  cons : (n : Nat) → A → Vec A n → Vec A (suc n)

tail : {A : Set} (n : Nat) → Vec A (suc n) → Vec A n
tail n (cons n x xs) = xs

tail' : {A : Set} (n : Nat) → Vec A (suc n) → Vec A n
tail' 0 (cons 0 x []) = []
tail' (suc n) (cons (suc n) x (cons n x₁ xs)) = (cons n x₁ xs)


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Properties.Successor {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Irrelevance
open import Definition.LogicalRelation.ShapeView

open import Tools.Embedding
open import Tools.Product

-- Helper function for successors for specific reducible derivations.
sucTerm′ : ∀ {l Γ n}
           ([ℕ] : Γ ⊩⟨ l ⟩ℕ ℕ)
         → Γ ⊩⟨ l ⟩ n ∷ ℕ / ℕ-intr [ℕ]
         → Γ ⊩⟨ l ⟩ suc n ∷ ℕ / ℕ-intr [ℕ]
sucTerm′ (noemb D) (ιx (ℕₜ n [ ⊢t , ⊢u , d ] n≡n prop)) =
  let natN = natural prop
  in  ιx (ℕₜ _ [ sucⱼ ⊢t , sucⱼ ⊢t , id (sucⱼ ⊢t) ]
         (≅-suc-cong (≅ₜ-red (red D) d d ℕₙ
                             (naturalWhnf natN) (naturalWhnf natN) n≡n))
         (sucᵣ (ℕₜ n [ ⊢t , ⊢u , d ] n≡n prop)))
sucTerm′ (emb 0<1 x) (ιx [n]) = ιx (sucTerm′ x [n])

-- Reducible natural numbers can be used to construct reducible successors.
sucTerm : ∀ {l Γ n} ([ℕ] : Γ ⊩⟨ l ⟩ ℕ)
        → Γ ⊩⟨ l ⟩ n ∷ ℕ / [ℕ]
        → Γ ⊩⟨ l ⟩ suc n ∷ ℕ / [ℕ]
sucTerm [ℕ] [n] =
  let [n]′ = irrelevanceTerm [ℕ] (ℕ-intr (ℕ-elim [ℕ])) [n]
  in  irrelevanceTerm (ℕ-intr (ℕ-elim [ℕ]))
                      [ℕ]
                      (sucTerm′ (ℕ-elim [ℕ]) [n]′)

-- Helper function for successor equality for specific reducible derivations.
sucEqTerm′ : ∀ {l Γ n n′}
             ([ℕ] : Γ ⊩⟨ l ⟩ℕ ℕ)
           → Γ ⊩⟨ l ⟩ n ≡ n′ ∷ ℕ / ℕ-intr [ℕ]
           → Γ ⊩⟨ l ⟩ suc n ≡ suc n′ ∷ ℕ / ℕ-intr [ℕ]
sucEqTerm′ (noemb D) (ιx (ℕₜ₌ k k′ [ ⊢t , ⊢u , d ]
                              [ ⊢t₁ , ⊢u₁ , d₁ ] t≡u prop)) =
  let natK , natK′ = split prop
  in  ιx (ℕₜ₌ _ _ (idRedTerm:*: (sucⱼ ⊢t)) (idRedTerm:*: (sucⱼ ⊢t₁))
        (≅-suc-cong (≅ₜ-red (red D) d d₁ ℕₙ (naturalWhnf natK) (naturalWhnf natK′) t≡u))
        (sucᵣ (ℕₜ₌ k k′ [ ⊢t , ⊢u , d ] [ ⊢t₁ , ⊢u₁ , d₁ ] t≡u prop)))
sucEqTerm′ (emb 0<1 x) (ιx [n≡n′]) = ιx (sucEqTerm′ x [n≡n′])

-- Reducible natural number equality can be used to construct reducible equality
-- of the successors of the numbers.
sucEqTerm : ∀ {l Γ n n′} ([ℕ] : Γ ⊩⟨ l ⟩ ℕ)
          → Γ ⊩⟨ l ⟩ n ≡ n′ ∷ ℕ / [ℕ]
          → Γ ⊩⟨ l ⟩ suc n ≡ suc n′ ∷ ℕ / [ℕ]
sucEqTerm [ℕ] [n≡n′] =
  let [n≡n′]′ = irrelevanceEqTerm [ℕ] (ℕ-intr (ℕ-elim [ℕ])) [n≡n′]
  in  irrelevanceEqTerm (ℕ-intr (ℕ-elim [ℕ])) [ℕ]
                        (sucEqTerm′ (ℕ-elim [ℕ]) [n≡n′]′)

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
open import Nat
open import Prelude
open import core
open import contexts
open import typed-elaboration
open import lemmas-gcomplete
open import lemmas-complete

module complete-elaboration where
  mutual
    complete-elaboration-synth : ∀{e τ Γ Δ d} →
                               Γ gcomplete →
                               e ecomplete →
                               Γ ⊢ e ⇒ τ ~> d ⊣ Δ →
                               (d dcomplete × τ tcomplete × Δ == ∅)
    complete-elaboration-synth gc ec ESConst = DCConst , TCBase , refl
    complete-elaboration-synth gc ec (ESVar x₁) = DCVar , gc _ _ x₁ , refl
    complete-elaboration-synth gc (ECLam2 ec x₁) (ESLam x₂ exp)
      with complete-elaboration-synth (gcomp-extend gc x₁ x₂) ec exp
    ... | ih1 , ih2 , ih3 = DCLam ih1 x₁ , TCArr x₁ ih2 , ih3
    complete-elaboration-synth gc (ECAp ec ec₁) (ESAp _ _ x MAHole x₂ x₃)
      with comp-synth gc ec x
    ... | ()
    complete-elaboration-synth gc (ECAp ec ec₁) (ESAp {Δ1 = Δ1} {Δ2 = Δ2} _ _ x MAArr x₂ x₃)
      with comp-synth gc ec x
    ... | TCArr t1 t2
      with complete-elaboration-ana gc ec (TCArr t1 t2) x₂ | complete-elaboration-ana gc ec₁ t1 x₃
    ... | ih1 , _ ,  ih4 | ih2 , _ , ih3 = DCAp (DCCast ih1 (comp-ana gc x₂ ih1) (TCArr t1 t2)) (DCCast ih2 (comp-ana gc x₃ ih2) t1) ,
                                  t2 ,
                                  tr (λ qq → (qq ∪ Δ2) == ∅) (! ih4) (tr (λ qq → (∅ ∪ qq) == ∅) (! ih3) refl)
    complete-elaboration-synth gc () ESEHole
    complete-elaboration-synth gc () (ESNEHole _ exp)
    complete-elaboration-synth gc (ECAsc x ec) (ESAsc x₁)
      with complete-elaboration-ana gc ec x x₁
    ... | ih1 , _ , ih2 = DCCast ih1 (comp-ana gc x₁ ih1) x , x , ih2

    complete-elaboration-ana : ∀{e τ τ' Γ Δ d} →
                             Γ gcomplete →
                             e ecomplete →
                             τ tcomplete →
                             Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
                             (d dcomplete × τ' tcomplete × Δ == ∅)
    complete-elaboration-ana gc (ECLam1 ec) () (EALam x₁ MAHole exp)
    complete-elaboration-ana gc (ECLam1 ec) (TCArr t1 t2)  (EALam x₁ MAArr exp)
      with complete-elaboration-ana (gcomp-extend gc t1 x₁) ec t2 exp
    ... | ih , ih3 , ih2 = DCLam ih t1 , TCArr t1 ih3 , ih2
    complete-elaboration-ana gc ec tc (EASubsume x x₁ x₂ x₃)
      with complete-elaboration-synth gc ec x₂
    ... | ih1 , ih2 , ih3 = ih1 , ih2 , ih3

    -- this is just a convenience since it shows up a few times above
    comp-ana : ∀{Γ e τ d τ' Δ} →
       Γ gcomplete →
       Γ ⊢ e ⇐ τ ~> d :: τ' ⊣ Δ →
       d dcomplete →
       τ' tcomplete
    comp-ana gc ex dc = complete-ta gc (π2 (typed-elaboration-ana ex)) dc

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
------------------------------------------------------------------------
-- Universe levels
------------------------------------------------------------------------

module Common.Level where

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

{-# IMPORT Common.FFI #-}
{-# COMPILED_TYPE Level Common.FFI.Level #-}
{-# COMPILED lzero Common.FFI.Zero #-}
{-# COMPILED lsuc Common.FFI.Suc #-}

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

infixl 6 _⊔_

-- Lifting.

record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where
  constructor lift
  field lower : A

open Lift public

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Forcing4 where

open import Common.Nat renaming (zero to Z; suc to S)
open import Lib.Fin
open import Common.Equality
open import Common.String
open import Common.IO
open import Common.Unit

{-
toNat : {n : Nat} → Fin n → Nat
toNat (zero _)    = 0
toNat (suc _ i) = suc (toNat i)
-}

Rel : (X : Set) -> Set1
Rel X = X -> X -> Set

data _<=_ : Rel Nat where
  z<=n : ∀ n                 → Z  <= n
  s<=s : ∀ m n (m<=n : m <= n) → S m <= S n

_ℕ<_ : Rel Nat
m ℕ< n = S m <= n

fromℕ≤ : ∀ {m n} → m ℕ< n → Fin n
fromℕ≤ (s<=s .0 n (z<=n .n)) = fz {n}
fromℕ≤ (s<=s .(S m) .(S n) (s<=s m n m<=n)) = fs {S n} (fromℕ≤ (s<=s m n m<=n))

fromℕ≤-toℕ : ∀ m (i : Fin m) (i<m : forget i ℕ< m) → fromℕ≤ i<m ≡ i
fromℕ≤-toℕ .(S n) (fz {n}) (s<=s .0 .n (z<=n .n)) = refl
fromℕ≤-toℕ .(S (S n)) (fs .{S n} y) (s<=s .(S (forget y)) .(S n) (s<=s .(forget y) n m≤n)) = cong (\ n -> fs n) (fromℕ≤-toℕ (S n) y (s<=s (forget y) n m≤n))

[_/2] : Nat -> Nat
[ 0 /2] = 0
[ 1 /2] = 0
[ S (S n) /2] = S [ n /2]

[1/2]-mono : (m n : Nat) -> m <= n -> [ m /2] <= [ n /2]
[1/2]-mono .0 .n (z<=n n) = z<=n [ n /2]
[1/2]-mono .1 .(S n) (s<=s .0 .n (z<=n n)) = z<=n [ S n /2]
[1/2]-mono .(S (S m)) .(S (S n)) (s<=s .(S m) .(S n) (s<=s m n m<=n)) = s<=s [ m /2] [ n /2] ([1/2]-mono m n m<=n)

showEq : {X : Set}{A : X}  -> A ≡ A -> String
showEq refl = "refl"

show<= : {m n : Nat} -> m <= n -> String
show<= (z<=n n) = "0 <= " +S+ natToString n
show<= (s<=s m n m<=n) = natToString (S m) +S+ " <= " +S+ natToString (S n)

data Bot : Set where
-- Only to check that it compiles..
foo : (n : Nat) -> S n <= n -> Bot
foo .(S n) (s<=s .(S n) n le) = foo n le

main : IO Unit
main = putStrLn (showEq (fromℕ≤-toℕ 3 (inc (inject 1)) le)) ,,
       putStrLn (show<= ([1/2]-mono 4 6 le'))
  where
    le : 2 <= 3
    le = s<=s _ _ (s<=s _ _ (z<=n _))
    le' : 4 <= 6
    le' = s<=s _ _ (s<=s _ _ (s<=s _ _ (s<=s _ _ (z<=n _))))

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module NatIf3 where

open import Data.Nat
open import Data.Vec

natIf3 : (a : Set) -> a -> a -> a -> ℕ -> a
natIf3 a x y z zero = x
natIf3 a x y z (suc zero) = y
natIf3 a x y z (suc (suc n)) = z

nilNat : Vec ℕ 0
nilNat = []

--test1 = natIf3 _ 1 nilNat 3 0

test2 = natIf3 _ nilNat 2 3 0

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint


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

module FOT.Common.FOL.Existential.Syntax where

-- We add 3 to the fixities of the Agda standard library 0.8.1 (see
-- Relation.Binary.Core).
infix 7 _≡_

postulate
  D    : Set
  _≡_  : D → D → Set
  refl : ∀ {d} → d ≡ d
  d    : D

module ∃₁ where

  -- We add 3 to the fixities of the Agda standard library 0.8.1 (see
  -- Data/Product.agda, Data/Sum.agda and Relation/Nullary/Core.agda).
  infixr 7 _,_
  infix  5 ∃

  data ∃ (P : D → Set) : Set where
    _,_ : (x : D) → P x → ∃ P

  syntax ∃ (λ x → e)  = ∃[ x ] e

  t₁ : ∃ λ x → x ≡ x
  t₁ = d , refl

  t₂ : ∃[ x ] x ≡ x
  t₂ = d , refl

  t₃ : ∃ λ x → ∃ λ y → x ≡ y
  t₃ = d , d , refl

  t₄ : ∃[ x ] ∃[ y ] x ≡ y
  t₄ = d , d ,  refl

module ∃₂ where
  infixr 7 _,_,_

  data ∃₂ (P : D → D → Set) : Set where
    _,_,_ : (x y : D) → P x y → ∃₂ P

  -- Agda issue: 536
  -- syntax ∃₂ (λ x y → e) = ∃₂[ x , y ] e

  t₁ : ∃₂ λ x y → x ≡ y
  t₁ = d , d , refl

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module prelude.int where
open import Data.Nat as Nat renaming (suc to s; zero to z)
open import Agda.Builtin.Int public

⁺1 : Int → Int
⁺1 (pos n) = pos (s n)
⁺1 (negsuc z) = pos z
⁺1 (negsuc (s n)) = negsuc n

⁻1 : Int → Int
⁻1 (pos Nat.zero) = negsuc Nat.zero
⁻1 (pos (Nat.suc n)) = pos n
⁻1 (negsuc n) = negsuc (Nat.suc n)

max_stars_repo_name: mstone/poly

max_issues_repo_name: dspivak/poly

max_forks_repo_name: dspivak/poly


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

open import Categories.Category

module Categories.Category.Cartesian.Properties {o ℓ e} (C : Category o ℓ e) where

open import Function using (_$_)

open import Categories.Category.Cartesian C

open import Categories.Diagram.Pullback C
open import Categories.Diagram.Equalizer C
open import Categories.Morphism.Reasoning C

private
  open Category C
  variable
    A B X Y : Obj
    f g : A ⇒ B

-- all binary products and pullbacks implies equalizers
module _ (prods : BinaryProducts) (pullbacks : ∀ {A B X} (f : A ⇒ X) (g : B ⇒ X) → Pullback f g) where
  open BinaryProducts prods
  open HomReasoning

  prods×pullbacks⇒equalizers : Equalizer f g
  prods×pullbacks⇒equalizers {f = f} {g = g} = record
    { arr       = pb′.p₁
    ; equality  = begin
      f ∘ pb′.p₁           ≈⟨ refl⟩∘⟨ helper₁ ⟩
      f ∘ pb.p₁ ∘ pb′.p₂   ≈⟨ pullˡ pb.commute ⟩
      (g ∘ pb.p₂) ∘ pb′.p₂ ≈˘⟨ pushʳ helper₂ ⟩
      g ∘ pb′.p₁           ∎
    ; equalize  = λ {_ i} eq → pb′.universal $ begin
      ⟨ id , id ⟩ ∘ i                                       ≈⟨ ⟨⟩∘ ⟩
      ⟨ id ∘ i , id ∘ i ⟩                                   ≈⟨ ⟨⟩-cong₂ identityˡ identityˡ ⟩
      ⟨ i ,  i ⟩                                            ≈˘⟨ ⟨⟩-cong₂ pb.p₁∘universal≈h₁ pb.p₂∘universal≈h₂ ⟩
      ⟨ pb.p₁ ∘ pb.universal eq , pb.p₂ ∘ pb.universal eq ⟩ ≈˘⟨ ⟨⟩∘ ⟩
      h ∘ pb.universal eq                                   ∎
    ; universal = ⟺ pb′.p₁∘universal≈h₁
    ; unique    = λ eq → pb′.unique (⟺ eq) (pb.unique (pullˡ (⟺ helper₁) ○ ⟺ eq) (pullˡ (⟺ helper₂) ○ ⟺ eq))
    }
    where pb : Pullback f g
          pb         = pullbacks _ _
          module pb  = Pullback pb
          h          = ⟨ pb.p₁ , pb.p₂ ⟩
          pb′ : Pullback ⟨ id , id ⟩ h
          pb′        = pullbacks _ _
          module pb′ = Pullback pb′
          helper₁ : pb′.p₁ ≈ pb.p₁ ∘ pb′.p₂
          helper₁    = begin
            pb′.p₁                    ≈˘⟨ cancelˡ project₁ ⟩
            π₁ ∘ ⟨ id , id ⟩ ∘ pb′.p₁ ≈⟨ refl⟩∘⟨ pb′.commute ⟩
            π₁ ∘ h ∘ pb′.p₂           ≈⟨ pullˡ project₁ ⟩
            pb.p₁ ∘ pb′.p₂            ∎
          helper₂ : pb′.p₁ ≈ pb.p₂ ∘ pb′.p₂
          helper₂    = begin
            pb′.p₁                    ≈˘⟨ cancelˡ project₂ ⟩
            π₂ ∘ ⟨ id , id ⟩ ∘ pb′.p₁ ≈⟨ refl⟩∘⟨ pb′.commute ⟩
            π₂ ∘ h ∘ pb′.p₂           ≈⟨ pullˡ project₂ ⟩
            pb.p₂ ∘ pb′.p₂            ∎

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
-- Andreas, 2012-11-06 this has been fixed with issue 655
module Issue378 where

infix  7 _≡_
infixl 9 _+_

postulate
  ℕ    : Set
  _≡_  : ℕ → ℕ → Set
  zero : ℕ
  _+_  : ℕ → ℕ → ℕ

postulate
  S₁ : ∀ {m n o} → m ≡ n → m ≡ o → n ≡ o
  S₅ : ∀ n → zero + n ≡ n

-- Calling Auto on the hole generates the invalid expression
-- S₁ (S₅ .n) (S₅ .n).
refl : ∀ {n} → n ≡ n
refl = {!-m!}
-- C-c C-a should work now


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Creates trivially indexed records from their non-indexed counterpart.
------------------------------------------------------------------------

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

module Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
  {i} {I : Set i} where

open import Relation.Binary
open import Relation.Binary.Indexed.Heterogeneous hiding (Rel)
  hiding (IsEquivalence; Setoid)

------------------------------------------------------------------------
-- Structures

module _ {a} {A : Set a} where

  private
    Aᵢ : I → Set a
    Aᵢ i = A

  isIndexedEquivalence : ∀ {ℓ} {_≈_ : Rel A ℓ} → IsEquivalence _≈_ →
                         IsIndexedEquivalence Aᵢ _≈_
  isIndexedEquivalence isEq = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
    where open IsEquivalence isEq

  isIndexedPreorder : ∀ {ℓ₁ ℓ₂} {_≈_ : Rel A ℓ₁} {_∼_ : Rel A ℓ₂} →
                      IsPreorder _≈_ _∼_ →
                      IsIndexedPreorder Aᵢ _≈_ _∼_
  isIndexedPreorder isPreorder = record
    { isEquivalence = isIndexedEquivalence isEquivalence
    ; reflexive     = reflexive
    ; trans         = trans
    }
    where open IsPreorder isPreorder

------------------------------------------------------------------------
-- Packages

indexedSetoid : ∀ {a ℓ} → Setoid a ℓ → IndexedSetoid I a ℓ
indexedSetoid S = record
  { isEquivalence = isIndexedEquivalence isEquivalence
  }
  where open Setoid S

indexedPreorder : ∀ {a ℓ₁ ℓ₂} → Preorder a ℓ₁ ℓ₂ →
                  IndexedPreorder I a ℓ₁ ℓ₂
indexedPreorder O = record
  { isPreorder = isIndexedPreorder isPreorder
  }
  where open Preorder O


text:
open import Oscar.Prelude
open import Oscar.Class.Reflexivity
open import Oscar.Class.Transitivity
open import Oscar.Class.Transextensionality
open import Oscar.Class.Transassociativity

module Oscar.Class.IsPrecategory where

module _
  {𝔬} {𝔒 : Ø 𝔬}
  {𝔯} (_∼_ : 𝔒 → 𝔒 → Ø 𝔯)
  {ℓ} (_∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ) (let infix 4 _∼̇_ ; _∼̇_ = _∼̇_)
  (_↦_ : Transitivity.type _∼_)
  where
  record IsPrecategory : Ø 𝔬 ∙̂ 𝔯 ∙̂ ℓ where
    constructor ∁
    field
      ⦃ `𝓣ransextensionality ⦄ : Transextensionality.class _∼_ _∼̇_ _↦_
      ⦃ `𝓣ransassociativity ⦄ : Transassociativity.class _∼_ _∼̇_ _↦_


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.Prelude

module LibraBFT.ImplShared.Util.Dijkstra.EitherD where

data EitherD (E : Set) : Set → Set₁ where
  -- Primitive combinators
  EitherD-return : ∀ {A} → A → EitherD E A
  EitherD-bind   : ∀ {A B} → EitherD E A → (A → EitherD E B) → EitherD E B
  EitherD-bail   : ∀ {A} → E → EitherD E A
  -- Branching conditionals (used for creating more convenient contracts)
  EitherD-if     : ∀ {A} → Guards (EitherD E A) → EitherD E A
  EitherD-either : ∀ {A B C} → Either B C
                   → (B → EitherD E A) → (C → EitherD E A) → EitherD E A
  EitherD-maybe  : ∀ {A B} → Maybe A → EitherD E B → (A → EitherD E B) → EitherD E B

pattern LeftD  x = EitherD-bail   x
pattern RightD x = EitherD-return x

private
  variable
    E : Set
    A B C : Set

EitherD-run : EitherD E A → Either E A
EitherD-run (EitherD-return x) = Right x
EitherD-run (EitherD-bind m f)
  with EitherD-run m
... | Left x = Left x
... | Right y = EitherD-run (f y)
EitherD-run (EitherD-bail x) = Left x
EitherD-run (EitherD-if (clause (b ≔ c) gs)) =
  if toBool b then EitherD-run c else EitherD-run (EitherD-if gs)
EitherD-run (EitherD-if (otherwise≔ c)) =
  EitherD-run c
EitherD-run (EitherD-either (Left x) f₁ f₂) = EitherD-run (f₁ x)
EitherD-run (EitherD-either (Right y) f₁ f₂) = EitherD-run (f₂ y)
EitherD-run (EitherD-maybe nothing n s) = EitherD-run n
EitherD-run (EitherD-maybe (just x) n s) = EitherD-run (s x)

EitherD-Pre : (E A : Set) → Set₁
EitherD-Pre E A = Set

EitherD-Post : (E A : Set) → Set₁
EitherD-Post E A = Either E A → Set

EitherD-PredTrans : (E A : Set) → Set₁
EitherD-PredTrans E A = EitherD-Post E A → EitherD-Pre E A

EitherD-weakestPre-bindPost : (f : A → EitherD E B) → EitherD-Post E B → EitherD-Post E A

EitherD-weakestPre : (m : EitherD E A) → EitherD-PredTrans E A
EitherD-weakestPre (EitherD-return x) P = P (Right x)
EitherD-weakestPre (EitherD-bind m f) P =
  EitherD-weakestPre m (EitherD-weakestPre-bindPost f P)
EitherD-weakestPre (EitherD-bail x) P = P (Left x)
EitherD-weakestPre (EitherD-if (clause (b ≔ c) gs)) P =
  (toBool b ≡ true → EitherD-weakestPre c P)
  × (toBool b ≡ false → EitherD-weakestPre (EitherD-if gs) P)
EitherD-weakestPre (EitherD-if (otherwise≔ x)) P =
  EitherD-weakestPre x P
EitherD-weakestPre (EitherD-either e f₁ f₂) P =
  (∀ x → e ≡ Left x → EitherD-weakestPre (f₁ x) P)
  × (∀ y → e ≡ Right y → EitherD-weakestPre (f₂ y) P)
EitherD-weakestPre (EitherD-maybe m n s) P =
  (m ≡ nothing → EitherD-weakestPre n P)
  × (∀ j → m ≡ just j → EitherD-weakestPre (s j) P)

EitherD-weakestPre-bindPost f P (Left x) =
  P (Left x)
EitherD-weakestPre-bindPost f P (Right y) =
  ∀ c → c ≡ y → EitherD-weakestPre (f c) P

EitherD-Contract : (m : EitherD E A) → Set₁
EitherD-Contract{E}{A} m =
  (P : EitherD-Post E A)
  → EitherD-weakestPre m P → P (EitherD-run m)

EitherD-contract : (m : EitherD E A) → EitherD-Contract m
EitherD-contract (EitherD-return x) P wp = wp
EitherD-contract (EitherD-bind m f) P wp
   with EitherD-contract m _ wp
...| wp'
   with EitherD-run m
... | Left x = wp'
... | Right y = EitherD-contract (f y) P (wp' y refl)
EitherD-contract (EitherD-bail x) P wp = wp
EitherD-contract{E}{A} (EitherD-if gs) P wp =
  EitherD-contract-if gs P wp
  where
  EitherD-contract-if : (gs : Guards (EitherD E A)) → EitherD-Contract (EitherD-if gs)
  EitherD-contract-if (clause (b ≔ c) gs) P wp
     with toBool b
  ... | false = EitherD-contract-if gs P (proj₂ wp refl)
  ... | true = EitherD-contract c P (proj₁ wp refl)
  EitherD-contract-if (otherwise≔ x) P wp = EitherD-contract x P wp
EitherD-contract (EitherD-either (Left x) f₁ f₂) P wp =
  EitherD-contract (f₁ x) P (proj₁ wp x refl)
EitherD-contract (EitherD-either (Right y) f₁ f₂) P wp =
  EitherD-contract (f₂ y) P (proj₂ wp y refl)
EitherD-contract (EitherD-maybe nothing f₁ f₂) P wp =
  EitherD-contract f₁ P (proj₁ wp refl)
EitherD-contract (EitherD-maybe (just x) f₁ f₂) P wp =
  EitherD-contract (f₂ x) P (proj₂ wp x refl)

max_stars_repo_name: oracle/bft-consensus-agda

max_issues_repo_name: oracle/bft-consensus-agda

max_forks_repo_name: oracle/bft-consensus-agda


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommMonoid.Base where

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

open import Cubical.Data.Sigma

open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid.Base

open import Cubical.Displayed.Base
open import Cubical.Displayed.Auto
open import Cubical.Displayed.Record
open import Cubical.Displayed.Universe

open import Cubical.Reflection.RecordEquiv

open Iso

private
  variable
    ℓ ℓ' : Level

record IsCommMonoid {A : Type ℓ} (ε : A) (_·_ : A → A → A) : Type ℓ where
  constructor iscommmonoid

  field
   isMonoid : IsMonoid ε _·_
   comm :  (x y : A) → x · y ≡ y · x

  open IsMonoid isMonoid public

unquoteDecl IsCommMonoidIsoΣ = declareRecordIsoΣ IsCommMonoidIsoΣ (quote IsCommMonoid)

record CommMonoidStr (A : Type ℓ) : Type ℓ where
  constructor commmonoidstr

  field
    ε        : A
    _·_      : A → A → A
    isCommMonoid : IsCommMonoid ε _·_

  infixl 7 _·_

  open IsCommMonoid isCommMonoid public

CommMonoid : ∀ ℓ → Type (ℓ-suc ℓ)
CommMonoid ℓ = TypeWithStr ℓ CommMonoidStr

commmonoid : (A : Type ℓ) (ε : A) (_·_ : A → A → A) (h : IsCommMonoid ε _·_) → CommMonoid ℓ
commmonoid A ε _·_ h = A , commmonoidstr ε _·_ h

-- Easier to use constructors
makeIsCommMonoid : {M : Type ℓ} {ε : M} {_·_ : M → M → M}
               (is-setM : isSet M)
               (assoc : (x y z : M) → x · (y · z) ≡ (x · y) · z)
               (rid : (x : M) → x · ε ≡ x)
               (lid : (x : M) → ε · x ≡ x)
               (comm : (x y : M) → x · y ≡ y · x)
             → IsCommMonoid ε _·_
IsCommMonoid.isMonoid (makeIsCommMonoid is-setM assoc rid lid comm) =
                                        makeIsMonoid is-setM assoc rid lid
IsCommMonoid.comm (makeIsCommMonoid is-setM assoc rid lid comm) = comm

makeCommMonoid : {M : Type ℓ} (ε : M) (_·_ : M → M → M)
             (is-setM : isSet M)
             (assoc : (x y z : M) → x · (y · z) ≡ (x · y) · z)
             (rid : (x : M) → x · ε ≡ x)
             (lid : (x : M) → ε · x ≡ x)
             (comm : (x y : M) → x · y ≡ y · x)
           → CommMonoid ℓ
makeCommMonoid ε _·_ is-setM assoc rid lid comm =
  commmonoid _ ε _·_ (makeIsCommMonoid is-setM assoc rid lid comm)

CommMonoidStr→MonoidStr : {A : Type ℓ} → CommMonoidStr A → MonoidStr A
CommMonoidStr→MonoidStr (commmonoidstr _ _ H) = monoidstr _ _ (IsCommMonoid.isMonoid H)

CommMonoid→Monoid : CommMonoid ℓ → Monoid ℓ
CommMonoid→Monoid (_ , commmonoidstr _ _ H) = _ , monoidstr _ _ (IsCommMonoid.isMonoid H)

CommMonoidHom : (L : CommMonoid ℓ) (M : CommMonoid ℓ') → Type (ℓ-max ℓ ℓ')
CommMonoidHom L M = MonoidHom (CommMonoid→Monoid L) (CommMonoid→Monoid M)

IsCommMonoidEquiv : {A : Type ℓ} {B : Type ℓ'}
  (M : CommMonoidStr A) (e : A ≃ B) (N : CommMonoidStr B) → Type (ℓ-max ℓ ℓ')
IsCommMonoidEquiv M e N = IsMonoidHom (CommMonoidStr→MonoidStr M) (e .fst) (CommMonoidStr→MonoidStr N)

CommMonoidEquiv : (M : CommMonoid ℓ) (N : CommMonoid ℓ') → Type (ℓ-max ℓ ℓ')
CommMonoidEquiv M N = Σ[ e ∈ (M .fst ≃ N .fst) ] IsCommMonoidEquiv (M .snd) e (N .snd)

isPropIsCommMonoid : {M : Type ℓ} (ε : M) (_·_ : M → M → M)
             → isProp (IsCommMonoid ε _·_)
isPropIsCommMonoid ε _·_ (iscommmonoid MM MC) (iscommmonoid SM SC) =
  λ i → iscommmonoid (isPropIsMonoid _ _ MM SM i) (isPropComm MC SC i)
  where
  isSetM : isSet _
  isSetM = MM .IsMonoid.isSemigroup .IsSemigroup.is-set

  isPropComm : isProp ((x y : _) → x · y ≡ y · x)
  isPropComm = isPropΠ2 λ _ _ → isSetM _ _

𝒮ᴰ-CommMonoid : DUARel (𝒮-Univ ℓ) CommMonoidStr ℓ
𝒮ᴰ-CommMonoid =
  𝒮ᴰ-Record (𝒮-Univ _) IsCommMonoidEquiv
    (fields:
      data[ ε ∣ autoDUARel _ _ ∣ presε ]
      data[ _·_ ∣ autoDUARel _ _ ∣ isHom ]
      prop[ isCommMonoid ∣ (λ _ _ → isPropIsCommMonoid _ _) ])
  where
  open CommMonoidStr
  open IsMonoidHom

CommMonoidPath : (M N : CommMonoid ℓ) → CommMonoidEquiv M N ≃ (M ≡ N)
CommMonoidPath = ∫ 𝒮ᴰ-CommMonoid .UARel.ua

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
module Common where

open import Agda.Builtin.Size public
  using (Size ; Size<_)
  renaming (ω to ∞)

open import Agda.Primitive public
  using ()
  renaming (_⊔_ to _⊔ᴸ_ ; lsuc to sucᴸ)

open import Data.Bool public
  using (true ; false)
  renaming (Bool to 𝔹 ; _∧_ to _∧ᴮ_ ; _∨_ to _∨ᴮ_ ; not to ¬ᴮ_ ; if_then_else_ to ifᴮ)

open import Data.Empty public
  using ()
  renaming (⊥ to 𝟘 ; ⊥-elim to elim𝟘)

open import Data.Fin public
  using (Fin ; zero ; suc)

open import Data.List public
  using (List ; [] ; _∷_)

open import Data.Nat public
  using (ℕ ; zero ; suc)
  renaming (_≟_ to _≟ᴺ_)

open import Data.Sum public
  using (_⊎_)
  renaming (inj₁ to ι₁ ; inj₂ to ι₂)

open import Data.Unit public
  using ()
  renaming (⊤ to 𝟙 ; tt to ∙)

open import Function public
  using (_∘_ ; _$_)
  renaming (id to I ; const to K ; _ˢ_ to S)

open import Relation.Binary.PropositionalEquality public
  using (_≡_ ; _≢_ ; refl ; trans ; sym ; cong ; subst)
  renaming (cong₂ to cong²)

open import Relation.Nullary public
  using (Dec ; yes ; no)
  renaming (¬_ to Not)

open import Relation.Nullary.Decidable public
  using ()
  renaming (map′ to mapDec)

open import Relation.Nullary.Negation public
  using ()
  renaming (contradiction to _↯_)

-- Abstract symbols, or atoms.

abstract
  Atom : Set
  Atom = ℕ

  _≟ᵅ_ : (P P′ : Atom) → Dec (P ≡ P′)
  _≟ᵅ_ = _≟ᴺ_

-- Products, with custom fixities.

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

open Σ public

∃ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ᴸ b)
∃ = Σ _

infix 2 _×_
_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ᴸ b)
A × B = Σ A (λ _ → B)

-- Elimination for disjoint unions.

elim⊎ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
        → A ⊎ B → (A → C) → (B → C) → C
elim⊎ (ι₁ x) f g = f x
elim⊎ (ι₂ y) f g = g y

-- Double-argument K combinator.

K² : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
     → A → B → C → A
K² x _ _ = x

-- Triple-argument congruence.

cong³ : ∀ {a b c d} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
        (f : A → B → C → D) {x x′ y y′ z z′}
        → x ≡ x′ → y ≡ y′ → z ≡ z′ → f x y z ≡ f x′ y′ z′
cong³ f refl refl refl = refl

-- Iteration and recursion for naturals.

itᴺ : ∀ {a} {A : Set a} → ℕ → (A → A) → A → A
itᴺ zero    f x = x
itᴺ (suc n) f x = f (itᴺ n f x)

recᴺ : ∀ {a} {A : Set a} → ℕ → (ℕ → A → A) → A → A
recᴺ zero    f x = x
recᴺ (suc n) f x = f n (recᴺ n f x)

-- Iteration and recursion for lists.

itᴸ : ∀ {a b} {A : Set a} {B : Set b} → List A → (A → B → B) → B → B
itᴸ []       f x = x
itᴸ (k ∷ ks) f x = f k (itᴸ ks f x)

recᴸ : ∀ {a b} {A : Set a} {B : Set b} → List A → (A → List A → B → B) → B → B
recᴸ []       f x = x
recᴸ (k ∷ ks) f x = f k ks (recᴸ ks f x)

-- Composition, supremum, and infimum for relations.

module _ {W : Set} where
  _⨾_ : (W → W → Set) → (W → W → Set) → (W → W → Set)
  _R_ ⨾ _Q_ = λ w w′ → ∃ (λ v → w R v × v Q w′)

  _⊔_ : (W → W → Set) → (W → W → Set) → (W → W → Set)
  _R_ ⊔ _Q_ = λ w w′ → ∃ (λ v → w R v × w′ Q v)

  _⊓_ : (W → W → Set) → (W → W → Set) → (W → W → Set)
  _R_ ⊓ _Q_ = λ w w′ → ∃ (λ v → v R w × v Q w′)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
------------------------------------------------------------------------
-- Lists where at least one element satisfies a given property
------------------------------------------------------------------------

module Data.List.Any where

open import Data.Empty
open import Data.Fin
open import Data.Function
open import Data.List as List using (List; []; _∷_)
import Data.List.Equality as ListEq
open import Data.Product as Prod using (∃; _×_; _,_)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Unary using (Pred) renaming (_⊆_ to _⋐_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_)

-- Any P xs means that at least one element in xs satisfies P.

data Any {A} (P : A → Set) : List A → Set where
  here  : ∀ {x xs} (px  : P x)      → Any P (x ∷ xs)
  there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)

-- Map.

map : ∀ {A} {P Q : Pred A} → P ⋐ Q → Any P ⋐ Any Q
map g (here px)   = here (g px)
map g (there pxs) = there (map g pxs)

-- If the head does not satisfy the predicate, then the tail will.

tail : ∀ {A x xs} {P : A → Set} → ¬ P x → Any P (x ∷ xs) → Any P xs
tail ¬px (here  px)  = ⊥-elim (¬px px)
tail ¬px (there pxs) = pxs

-- Decides Any.

any : ∀ {A} {P : A → Set} →
      (∀ x → Dec (P x)) → (xs : List A) → Dec (Any P xs)
any p []       = no λ()
any p (x ∷ xs) with p x
any p (x ∷ xs) | yes px = yes (here px)
any p (x ∷ xs) | no ¬px = Dec.map (there , tail ¬px) (any p xs)

-- index x∈xs is the list position (zero-based) which x∈xs points to.

index : ∀ {A} {P : A → Set} {xs} → Any P xs → Fin (List.length xs)
index (here  px)  = zero
index (there pxs) = suc (index pxs)

------------------------------------------------------------------------
-- List membership and some related definitions

module Membership (S : Setoid) where

  private
    open module S = Setoid S using (_≈_) renaming (carrier to A)
    open module L = ListEq.Equality S
      using ([]; _∷_) renaming (_≈_ to _≋_)

  -- If a predicate P respects the underlying equality then Any P
  -- respects the list equality.

  lift-resp : ∀ {P} → P Respects _≈_ → Any P Respects _≋_
  lift-resp resp []            ()
  lift-resp resp (x≈y ∷ xs≈ys) (here px)   = here (resp x≈y px)
  lift-resp resp (x≈y ∷ xs≈ys) (there pxs) =
    there (lift-resp resp xs≈ys pxs)

  -- List membership.

  infix 4 _∈_ _∉_

  _∈_ : A → List A → Set
  x ∈ xs = Any (_≈_ x) xs

  _∉_ : A → List A → Set
  x ∉ xs = ¬ x ∈ xs

  -- Subsets.

  infix 4 _⊆_ _⊈_

  _⊆_ : List A → List A → Set
  xs ⊆ ys = ∀ {x} → x ∈ xs → x ∈ ys

  _⊈_ : List A → List A → Set
  xs ⊈ ys = ¬ xs ⊆ ys

  -- Equality is respected by the predicate which is used to define
  -- _∈_.

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

  -- List equality is respected by _∈_.

  ∈-resp-list-≈ : ∀ {x} → _∈_ x Respects _≋_
  ∈-resp-list-≈ = lift-resp ∈-resp-≈

  -- _⊆_ is a preorder.

  ⊆-preorder : Preorder
  ⊆-preorder = record
    { carrier    = List A
    ; _≈_        = _≋_
    ; _∼_        = _⊆_
    ; isPreorder = record
      { isEquivalence = Setoid.isEquivalence L.setoid
      ; reflexive     = reflexive
      ; trans         = λ ys⊆zs xs⊆ys → xs⊆ys ∘ ys⊆zs
      ; ∼-resp-≈      =
          (λ ys₁≋ys₂ xs⊆ys₁ → reflexive ys₁≋ys₂ ∘ xs⊆ys₁)
        , (λ xs₁≋xs₂ xs₁⊆ys → xs₁⊆ys ∘ reflexive (L.sym xs₁≋xs₂))
      }
    }
    where
    reflexive : _≋_ ⇒ _⊆_
    reflexive eq = ∈-resp-list-≈ eq

  module ⊆-Reasoning where
    import Relation.Binary.PreorderReasoning as PreR
    open PreR ⊆-preorder public
      renaming (_∼⟨_⟩_ to _⊆⟨_⟩_)

    infix 1 _∈⟨_⟩_

    _∈⟨_⟩_ : ∀ x {xs ys} → x ∈ xs → xs IsRelatedTo ys → x ∈ ys
    x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs

  -- A variant of List.map.

  map-with-∈ : ∀ {B} (xs : List A) → (∀ {x} → x ∈ xs → B) → List B
  map-with-∈ []       f = []
  map-with-∈ (x ∷ xs) f = f (here S.refl) ∷ map-with-∈ xs (f ∘ there)

  -- Finds an element satisfying the predicate.

  find : ∀ {P : A → Set} {xs} → Any P xs → ∃ λ x → x ∈ xs × P x
  find (here px)   = (_ , here S.refl , px)
  find (there pxs) = Prod.map id (Prod.map there id) (find pxs)

  lose : ∀ {P x xs} → P Respects _≈_ → x ∈ xs → P x → Any P xs
  lose resp x∈xs px = map (flip resp px) x∈xs

-- The code above instantiated (and slightly changed) for
-- propositional equality.

module Membership-≡ {A : Set} where

  private
    open module M = Membership (PropEq.setoid A) public
      hiding (lift-resp; lose; ⊆-preorder; module ⊆-Reasoning)

  lose : ∀ {P x xs} → x ∈ xs → P x → Any P xs
  lose {P} = M.lose (PropEq.subst P)

  -- _⊆_ is a preorder.

  ⊆-preorder : Preorder
  ⊆-preorder = record
    { carrier    = List A
    ; _≈_        = _≡_
    ; _∼_        = _⊆_
    ; isPreorder = record
      { isEquivalence = PropEq.isEquivalence
      ; reflexive     = λ eq → PropEq.subst (_∈_ _) eq
      ; trans         = λ ys⊆zs xs⊆ys → xs⊆ys ∘ ys⊆zs
      ; ∼-resp-≈      = PropEq.resp₂ _⊆_
      }
    }

  module ⊆-Reasoning where
    import Relation.Binary.PreorderReasoning as PreR
    open PreR ⊆-preorder public
      renaming (_∼⟨_⟩_ to _⊆⟨_⟩_; _≈⟨_⟩_ to _≡⟨_⟩_)

    infix 1 _∈⟨_⟩_

    _∈⟨_⟩_ : ∀ x {xs ys} → x ∈ xs → xs IsRelatedTo ys → x ∈ ys
    x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs

------------------------------------------------------------------------
-- Another function

-- If any element satisfies P, then P is satisfied.

satisfied : ∀ {A} {P : A → Set} {xs} → Any P xs → ∃ P
satisfied = Prod.map id Prod.proj₂ ∘ Membership-≡.find

max_issues_repo_name: larrytheliquid/Lemmachine


text:
-- The category of monadic functions.

open import Level

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Axiom.FunctionExtensionality

open import Control.Monad
open import Control.Category

module Control.Kleisli where

-- The type of monadic functions.

Kleisli : (M : Set → Set) (A : Set) (B : Set) → Set
Kleisli M A B = A → M B

KleisliHom : (M : Set → Set) (A : Set) (B : Set) → Setoid zero zero
KleisliHom M A B = setoid (Kleisli M A B)

-- The laws of a Kleisli category correspond to the Monad laws,
-- modulo function extensionality.

kleisliIsCategory : {M : Set → Set} (monad : IsMonad M) → IsCategory (KleisliHom M)
kleisliIsCategory monad = record
  { ops = record
    { id  = return
    ; _⟫_ = _⟫_
    }
  ; laws = record
    { id-first = fun-ext (bind-β _)
    ; id-last  = fun-ext (λ a → bind-η _)
    ; ∘-assoc  = λ f → fun-ext (λ a → bind-assoc (f a))
    ; ∘-cong   = cong₂ _⟫_
    }
  }
  where
    open IsMonad monad
    open T-CategoryOps (KleisliHom _)
    _⟫_ : T-⟫
    f ⟫ g = λ a → f a >>= g

-- The Kleisli category over a Monad on Set

KLEISLI : {M : Set → Set} (monad : IsMonad M) → Category _ _ _
KLEISLI monad = record { Hom = KleisliHom _; isCategory = kleisliIsCategory monad }

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
------------------------------------------------------------------------------
-- The FOTC types without using data, i.e. using Agda as a logical framework
------------------------------------------------------------------------------

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

module Predicates where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Base.List.PropertiesI
open import FOTC.Base.PropertiesI

------------------------------------------------------------------------------
-- The existential proyections.

∃-proj₁ : ∀ {A} → ∃ A → D
∃-proj₁ (x , _) = x

∃-proj₂ : ∀ {A} → (h : ∃ A) → A (∃-proj₁ h)
∃-proj₂ (_ , Ax) = Ax

------------------------------------------------------------------------------
-- The inductive FOTC types using postulates.

module Pure where

  -- The FOTC natural numbers type.
  postulate
    N     : D → Set
    nzero : N zero
    nsucc : ∀ {n} → N n → N (succ₁ n)

  -- Example.
  [1] : D
  [1] = succ₁ zero

  1-N : N [1]
  1-N = nsucc nzero

  -- The FOTC lists type.
  postulate
    List  : D → Set
    lnil  : List []
    lcons : ∀ x {xs} → List xs → List (x ∷ xs)

  -- Example.
  l : List (zero ∷ true ∷ [])
  l = lcons zero (lcons true lnil)

  -- The FOTC list of natural numbers type.
  postulate
    ListN  : D → Set
    lnnil  : ListN []
    lncons : ∀ {n ns} → N n → ListN ns → ListN (n ∷ ns)

  -- Example.
  ln : ListN (zero ∷ [1] ∷ [])
  ln = lncons nzero (lncons 1-N lnnil)

------------------------------------------------------------------------------
-- The inductive FOTC types using data.

module Inductive where

  -- The FOTC natural numbers type.
  data N : D → Set where
    nzero : N zero
    nsucc : ∀ {n} → N n → N (succ₁ n)

  -- Example.
  [1] : D
  [1] = succ₁ zero

  1-N : N [1]
  1-N = nsucc nzero

  -- The FOTC lists type.
  data List : D → Set where
    lnil  : List []
    lcons : ∀ x {xs} → List xs → List (x ∷ xs)

  -- Example.
  l : List (zero ∷ true ∷ [])
  l = lcons zero (lcons true lnil)

  -- The FOTC list of natural numbers type.
  data ListN : D → Set where
    lnnil  : ListN []
    lncons : ∀ {n ns} → N n → ListN ns → ListN (n ∷ ns)

  -- Example.
  ln : ListN (zero ∷ [1] ∷ [])
  ln = lncons nzero (lncons 1-N lnnil)

------------------------------------------------------------------------------
-- The least fixed-point operator.

module LFP where

  postulate
    -- Least fixed-points correspond to inductively defined types.
    --
    -- N.B. We cannot write μ in first-order logic. We should use an
    -- instance instead.
    μ : ((D → Set) → D → Set) → D → Set

    -- In FOTC, we cannot use the equality on predicates, i.e. we
    -- cannot write
    --
    -- (f : (D → Set) → D → Set) → f (μ f) ≡ μ f  (1)
    --
    -- because the type of the equality is
    --
    -- _≡_ : D → D → Set,
    --
    -- therefore we postulate both directions of the conversion rule (1).

    -- LFP₁ : (f : (D → Set) → D → Set)(d : D) → μ f d → f (μ f) d
    μ-in : (f : (D → Set) → D → Set)(d : D) → f (μ f) d → μ f d

------------------------------------------------------------------------------
-- The greatest fixed-point operator.

-- N.B. At the moment, the definitions of μ and ν are the same.

module GFP where

  postulate
    -- Greatest fixed-points correspond to co-inductively defined
    -- types.

    ν : ((D → Set) → D → Set) → D → Set

    ν-out : (f : (D → Set) → D → Set)(d : D) → ν f d → f (ν f) d
    GFP₂  : (f : (D → Set) → D → Set)(d : D) → f (ν f) d → ν f d

------------------------------------------------------------------------------
-- The FOTC natural numbers type as the least fixed-point of a
-- functor.

module NLFP where

  open LFP

  -- Functor for the FOTC natural numbers type.

  -- From Peter: NatF if D was an inductive type.
  --
  -- NatF : (D → Set) → D → Set
  -- NatF X zero      = ⊤
  -- NatF X (succ₁ n) = X n

  -- From Peter: NatF in pure predicate logic.
  NatF : (D → Set) → D → Set
  NatF X n = n ≡ zero ∨ (∃[ n' ] n ≡ succ₁ n' ∧ X n')

  -- The FOTC natural numbers type using μ.
  N : D → Set
  N = μ NatF

  -- The data constructors of N.
  nzero : N zero
  nzero = μ-in NatF zero (inj₁ refl)

  nsucc : {n : D} → N n → N (succ₁ n)
  nsucc {n} Nn = μ-in NatF (succ₁ n) (inj₂ (n , refl , Nn))

  -- Example.
  [1] : D
  [1] = succ₁ zero

  1-N : N [1]
  1-N = nsucc nzero

------------------------------------------------------------------------------
-- The FOTC list type as the least fixed-point of a functor.

module ListLFT where

  open LFP

  -- Functor for the FOTC lists type.
  ListF : (D → Set) → D → Set
  ListF X xs = xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ X xs')

  -- The FOTC list type using μ.
  List : D → Set
  List = μ ListF

  -- The data constructors of List.
  lnil : List []
  lnil = μ-in ListF [] (inj₁ refl)

  lcons : ∀ x {xs} → List xs → List (x ∷ xs)
  lcons x {xs} Lxs = μ-in ListF (x ∷ xs) (inj₂ (x , xs , refl , Lxs))

  -- Example.
  l : List (zero ∷ true ∷ [])
  l = lcons zero (lcons true lnil)

------------------------------------------------------------------------------
-- The FOTC list of natural numbers type as the least fixed-point of a
-- functor.

module ListNLFT where

  open LFP
  open NLFP

  -- Functor for the FOTC list of natural numbers type.
  ListNF : (D → Set) → D → Set
  ListNF X ns = ns ≡ [] ∨ (∃[ n' ] ∃[ ns' ] ns ≡ n' ∷ ns' ∧ N n' ∧ X ns')

  -- The FOTC list type using μ.
  ListN : D → Set
  ListN = μ ListNF

  -- The data constructors of ListN.
  lnnil : ListN []
  lnnil = μ-in ListNF [] (inj₁ refl)

  lncons : ∀ {n ns} → N n → ListN ns → ListN (n ∷ ns)
  lncons {n} {ns} Nn LNns =
    μ-in ListNF (n ∷ ns) (inj₂ (n , ns , refl , Nn , LNns))

  -- Example.
  ln : ListN (zero ∷ [1] ∷ [])
  ln = lncons nzero (lncons 1-N lnnil)

------------------------------------------------------------------------------
-- The FOTC Colist type as the greatest fixed-point of a functor.

module CoList where

  open GFP

  -- Functor for the FOTC Colists type (the same functor that for the
  -- List type).
  ColistF : (D → Set) → D → Set
  ColistF X xs = xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ X xs')

  -- The FOTC Colist type using ν.
  Colist : D → Set
  Colist = ν ColistF

  -- The data constructors of Colist.
  nilCL : Colist []
  nilCL = GFP₂ ColistF [] (inj₁ refl)

  consCL : ∀ x xs → Colist xs → Colist (x ∷ xs)
  consCL x xs CLxs = GFP₂ ColistF (x ∷ xs) (inj₂ (x , xs , refl , CLxs))

  -- Example (finite colist).
  l : Colist (zero ∷ true ∷ [])
  l = consCL zero (true ∷ []) (consCL true [] nilCL)

  -- TODO: Example (infinite colist).
  -- zerosCL : Colist {!!}
  -- zerosCL = consCL zero {!!} zerosCL

------------------------------------------------------------------------------
-- The FOTC Stream type as the greatest fixed-point of a functor.

module Stream where

  open GFP

  -- Functor for the FOTC Stream type.
  StreamF : (D → Set) → D → Set
  StreamF X xs = ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ X xs'

  -- The FOTC Stream type using ν.
  Stream : D → Set
  Stream = ν StreamF

  -- The data constructor of Stream.
  consS : ∀ x {xs} → Stream xs → Stream (x ∷ xs)
  consS x {xs} Sxs = GFP₂ StreamF (x ∷ xs) (x , xs , refl , Sxs)

  -- TODO: Example
  -- zerosS : Stream {!!}
  -- zerosS = consS zero {!!} zerosS

  headS : ∀ {x xs} → Stream (x ∷ xs) → D
  headS {x} _ = x

  tailS : ∀ {x xs} → Stream (x ∷ xs) → Stream xs
  tailS {x} {xs} Sx∷xs = Sxs
    where
    unfoldS : StreamF (ν StreamF) (x ∷ xs)
    unfoldS = ν-out StreamF (x ∷ xs) Sx∷xs

    e : D
    e = ∃-proj₁ unfoldS

    Pe : ∃ λ es → x ∷ xs ≡ e ∷ es ∧ ν StreamF es
    Pe = ∃-proj₂ unfoldS

    es : D
    es = ∃-proj₁ Pe

    Pes : x ∷ xs ≡ e ∷ es ∧ ν StreamF es
    Pes = ∃-proj₂ Pe

    xs≡es : xs ≡ es
    xs≡es = ∧-proj₂ (∷-injective (∧-proj₁ Pes))

    Sxs : ν StreamF xs
    Sxs = subst (ν StreamF) (sym xs≡es) (∧-proj₂ Pes)


text:
{-# OPTIONS --safe #-}
module Issue639-2 where

postulate A : Set


text:
module Trees where

open import Data.Unit using (⊤)

data BinTree {a} (A : Set a) : Set a where
  Empty : A → BinTree A
  Node  : A → BinTree A → BinTree A → BinTree A

BareBinTree : Set
BareBinTree = BinTree ⊤


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to list membership
------------------------------------------------------------------------

-- List membership is defined in Data.List.Any. This module does not
-- treat the general variant of list membership, parametrised on a
-- setoid, only the variant where the equality is fixed to be
-- propositional equality.

module Data.List.Any.Membership where

open import Algebra
open import Category.Monad
open import Data.Bool
open import Data.Empty
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (module Equivalence)
import Function.Injection as Inj
open import Function.Inverse as Inv using (_↔_; module Inverse)
import Function.Related as Related
open import Function.Related.TypeIsomorphisms
open import Data.List as List
open import Data.List.Any as Any using (Any; here; there)
open import Data.List.Any.Properties
open import Data.Nat as Nat
import Data.Nat.Properties as NatProp
open import Data.Product as Prod
open import Data.Sum as Sum
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P
  using (_≡_; refl; _≗_)
import Relation.Binary.Properties.DecTotalOrder as DTOProperties
import Relation.Binary.Sigma.Pointwise as Σ
open import Relation.Unary using (_⟨×⟩_)
open import Relation.Nullary
open import Relation.Nullary.Negation

open Any.Membership-≡
private
  module ×⊎ {k ℓ} = CommutativeSemiring (×⊎-CommutativeSemiring k ℓ)
  open module ListMonad {ℓ} = RawMonad (List.monad {ℓ = ℓ})

------------------------------------------------------------------------
-- Properties relating _∈_ to various list functions

-- Isomorphisms.

map-∈↔ : ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y xs} →
         (∃ λ x → x ∈ xs × y ≡ f x) ↔ y ∈ List.map f xs
map-∈↔ {a} {b} {f = f} {y} {xs} =
  (∃ λ x → x ∈ xs × y ≡ f x)  ↔⟨ Any↔ {a = a} {p = b} ⟩
  Any (λ x → y ≡ f x) xs      ↔⟨ map↔ {a = a} {b = b} {p = b} ⟩
  y ∈ List.map f xs           ∎
  where open Related.EquationalReasoning

concat-∈↔ : ∀ {a} {A : Set a} {x : A} {xss} →
            (∃ λ xs → x ∈ xs × xs ∈ xss) ↔ x ∈ concat xss
concat-∈↔ {a} {x = x} {xss} =
  (∃ λ xs → x ∈ xs × xs ∈ xss)  ↔⟨ Σ.cong {a₁ = a} {b₁ = a} {b₂ = a} Inv.id $ ×⊎.*-comm _ _ ⟩
  (∃ λ xs → xs ∈ xss × x ∈ xs)  ↔⟨ Any↔ {a = a} {p = a} ⟩
  Any (Any (_≡_ x)) xss         ↔⟨ concat↔ {a = a} {p = a} ⟩
  x ∈ concat xss                ∎
  where open Related.EquationalReasoning

>>=-∈↔ : ∀ {ℓ} {A B : Set ℓ} {xs} {f : A → List B} {y} →
         (∃ λ x → x ∈ xs × y ∈ f x) ↔ y ∈ (xs >>= f)
>>=-∈↔ {ℓ} {xs = xs} {f} {y} =
  (∃ λ x → x ∈ xs × y ∈ f x)  ↔⟨ Any↔ {a = ℓ} {p = ℓ} ⟩
  Any (Any (_≡_ y) ∘ f) xs    ↔⟨ >>=↔ {ℓ = ℓ} {p = ℓ} ⟩
  y ∈ (xs >>= f)              ∎
  where open Related.EquationalReasoning

⊛-∈↔ : ∀ {ℓ} {A B : Set ℓ} (fs : List (A → B)) {xs y} →
       (∃₂ λ f x → f ∈ fs × x ∈ xs × y ≡ f x) ↔ y ∈ fs ⊛ xs
⊛-∈↔ {ℓ} fs {xs} {y} =
  (∃₂ λ f x → f ∈ fs × x ∈ xs × y ≡ f x)       ↔⟨ Σ.cong {a₁ = ℓ} {b₁ = ℓ} {b₂ = ℓ} Inv.id (∃∃↔∃∃ {a = ℓ} {b = ℓ} {p = ℓ} _) ⟩
  (∃ λ f → f ∈ fs × ∃ λ x → x ∈ xs × y ≡ f x)  ↔⟨ Σ.cong {a₁ = ℓ} {b₁ = ℓ} {b₂ = ℓ}
                                                         Inv.id ((_ ∎) ⟨ ×⊎.*-cong {ℓ = ℓ} ⟩ Any↔ {a = ℓ} {p = ℓ}) ⟩
  (∃ λ f → f ∈ fs × Any (_≡_ y ∘ f) xs)        ↔⟨ Any↔ {a = ℓ} {p = ℓ} ⟩
  Any (λ f → Any (_≡_ y ∘ f) xs) fs            ↔⟨ ⊛↔ ⟩
  y ∈ fs ⊛ xs                                  ∎
  where open Related.EquationalReasoning

⊗-∈↔ : ∀ {A B : Set} {xs ys} {x : A} {y : B} →
       (x ∈ xs × y ∈ ys) ↔ (x , y) ∈ (xs ⊗ ys)
⊗-∈↔ {A} {B} {xs} {ys} {x} {y} =
  (x ∈ xs × y ∈ ys)                ↔⟨ ⊗↔′ ⟩
  Any (_≡_ x ⟨×⟩ _≡_ y) (xs ⊗ ys)  ↔⟨ Any-cong helper (_ ∎) ⟩
  (x , y) ∈ (xs ⊗ ys)              ∎
  where
  open Related.EquationalReasoning

  helper : (p : A × B) → (x ≡ proj₁ p × y ≡ proj₂ p) ↔ (x , y) ≡ p
  helper (x′ , y′) = record
    { to         = P.→-to-⟶ (uncurry $ P.cong₂ _,_)
    ; from       = P.→-to-⟶ < P.cong proj₁ , P.cong proj₂ >
    ; inverse-of = record
      { left-inverse-of  = λ _ → P.cong₂ _,_ (P.proof-irrelevance _ _)
                                             (P.proof-irrelevance _ _)
      ; right-inverse-of = λ _ → P.proof-irrelevance _ _
      }
    }

-- Other properties.

filter-∈ : ∀ {a} {A : Set a} (p : A → Bool) (xs : List A) {x} →
           x ∈ xs → p x ≡ true → x ∈ filter p xs
filter-∈ p []       ()          _
filter-∈ p (x ∷ xs) (here refl) px≡true rewrite px≡true = here refl
filter-∈ p (y ∷ xs) (there pxs) px≡true with p y
... | true  = there (filter-∈ p xs pxs px≡true)
... | false =        filter-∈ p xs pxs px≡true

------------------------------------------------------------------------
-- Properties relating _∈_ to various list functions

-- Various functions are monotone.

mono : ∀ {a p} {A : Set a} {P : A → Set p} {xs ys} →
       xs ⊆ ys → Any P xs → Any P ys
mono xs⊆ys =
  _⟨$⟩_ (Inverse.to Any↔) ∘′
  Prod.map id (Prod.map xs⊆ys id) ∘
  _⟨$⟩_ (Inverse.from Any↔)

map-mono : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {xs ys} →
           xs ⊆ ys → List.map f xs ⊆ List.map f ys
map-mono f xs⊆ys =
  _⟨$⟩_ (Inverse.to map-∈↔) ∘
  Prod.map id (Prod.map xs⊆ys id) ∘
  _⟨$⟩_ (Inverse.from map-∈↔)

_++-mono_ : ∀ {a} {A : Set a} {xs₁ xs₂ ys₁ ys₂ : List A} →
            xs₁ ⊆ ys₁ → xs₂ ⊆ ys₂ → xs₁ ++ xs₂ ⊆ ys₁ ++ ys₂
_++-mono_ xs₁⊆ys₁ xs₂⊆ys₂ =
  _⟨$⟩_ (Inverse.to ++↔) ∘
  Sum.map xs₁⊆ys₁ xs₂⊆ys₂ ∘
  _⟨$⟩_ (Inverse.from ++↔)

concat-mono : ∀ {a} {A : Set a} {xss yss : List (List A)} →
              xss ⊆ yss → concat xss ⊆ concat yss
concat-mono {a} xss⊆yss =
  _⟨$⟩_ (Inverse.to $ concat-∈↔ {a = a}) ∘
  Prod.map id (Prod.map id xss⊆yss) ∘
  _⟨$⟩_ (Inverse.from $ concat-∈↔ {a = a})

>>=-mono : ∀ {ℓ} {A B : Set ℓ} (f g : A → List B) {xs ys} →
           xs ⊆ ys → (∀ {x} → f x ⊆ g x) →
           (xs >>= f) ⊆ (ys >>= g)
>>=-mono {ℓ} f g xs⊆ys f⊆g =
  _⟨$⟩_ (Inverse.to $ >>=-∈↔ {ℓ = ℓ}) ∘
  Prod.map id (Prod.map xs⊆ys f⊆g) ∘
  _⟨$⟩_ (Inverse.from $ >>=-∈↔ {ℓ = ℓ})

_⊛-mono_ : ∀ {ℓ} {A B : Set ℓ}
             {fs gs : List (A → B)} {xs ys : List A} →
           fs ⊆ gs → xs ⊆ ys → (fs ⊛ xs) ⊆ (gs ⊛ ys)
_⊛-mono_ {fs = fs} {gs} fs⊆gs xs⊆ys =
  _⟨$⟩_ (Inverse.to $ ⊛-∈↔ gs) ∘
  Prod.map id (Prod.map id (Prod.map fs⊆gs (Prod.map xs⊆ys id))) ∘
  _⟨$⟩_ (Inverse.from $ ⊛-∈↔ fs)

_⊗-mono_ : {A B : Set} {xs₁ ys₁ : List A} {xs₂ ys₂ : List B} →
           xs₁ ⊆ ys₁ → xs₂ ⊆ ys₂ → (xs₁ ⊗ xs₂) ⊆ (ys₁ ⊗ ys₂)
xs₁⊆ys₁ ⊗-mono xs₂⊆ys₂ =
  _⟨$⟩_ (Inverse.to ⊗-∈↔) ∘
  Prod.map xs₁⊆ys₁ xs₂⊆ys₂ ∘
  _⟨$⟩_ (Inverse.from ⊗-∈↔)

any-mono : ∀ {a} {A : Set a} (p : A → Bool) →
           ∀ {xs ys} → xs ⊆ ys → T (any p xs) → T (any p ys)
any-mono {a} p xs⊆ys =
  _⟨$⟩_ (Equivalence.to $ any⇔ {a = a}) ∘
  mono xs⊆ys ∘
  _⟨$⟩_ (Equivalence.from $ any⇔ {a = a})

map-with-∈-mono :
  ∀ {a b} {A : Set a} {B : Set b}
    {xs : List A} {f : ∀ {x} → x ∈ xs → B}
    {ys : List A} {g : ∀ {x} → x ∈ ys → B}
  (xs⊆ys : xs ⊆ ys) → (∀ {x} → f {x} ≗ g ∘ xs⊆ys) →
  map-with-∈ xs f ⊆ map-with-∈ ys g
map-with-∈-mono {f = f} {g = g} xs⊆ys f≈g {x} =
  _⟨$⟩_ (Inverse.to map-with-∈↔) ∘
  Prod.map id (Prod.map xs⊆ys (λ {x∈xs} x≡fx∈xs → begin
    x               ≡⟨ x≡fx∈xs ⟩
    f x∈xs          ≡⟨ f≈g x∈xs ⟩
    g (xs⊆ys x∈xs)  ∎)) ∘
  _⟨$⟩_ (Inverse.from map-with-∈↔)
  where open P.≡-Reasoning

-- Other properties.

filter-⊆ : ∀ {a} {A : Set a} (p : A → Bool) →
           (xs : List A) → filter p xs ⊆ xs
filter-⊆ _ []       = λ ()
filter-⊆ p (x ∷ xs) with p x | filter-⊆ p xs
... | false | hyp = there ∘ hyp
... | true  | hyp =
  λ { (here  eq)      → here eq
    ; (there ∈filter) → there (hyp ∈filter)
    }

------------------------------------------------------------------------
-- Other properties

-- Only a finite number of distinct elements can be members of a
-- given list.

finite : ∀ {a} {A : Set a}
         (f : Inj.Injection (P.setoid ℕ) (P.setoid A)) →
         ∀ xs → ¬ (∀ i → Inj.Injection.to f ⟨$⟩ i ∈ xs)
finite         inj []       ∈[]   with ∈[] zero
... | ()
finite {A = A} inj (x ∷ xs) ∈x∷xs = excluded-middle helper
  where
  open Inj.Injection inj

  module DTO = DecTotalOrder Nat.decTotalOrder
  module STO = StrictTotalOrder
                 (DTOProperties.strictTotalOrder Nat.decTotalOrder)
  module CS  = CommutativeSemiring NatProp.commutativeSemiring

  not-x : ∀ {i} → ¬ (to ⟨$⟩ i ≡ x) → to ⟨$⟩ i ∈ xs
  not-x {i} ≢x with ∈x∷xs i
  ... | here  ≡x  = ⊥-elim (≢x ≡x)
  ... | there ∈xs = ∈xs

  helper : ¬ Dec (∃ λ i → to ⟨$⟩ i ≡ x)
  helper (no ≢x)        = finite inj  xs (λ i → not-x (≢x ∘ _,_ i))
  helper (yes (i , ≡x)) = finite inj′ xs ∈xs
    where
    open P

    f : ℕ → A
    f j with STO.compare i j
    f j | tri< _ _ _ = to ⟨$⟩ suc j
    f j | tri≈ _ _ _ = to ⟨$⟩ suc j
    f j | tri> _ _ _ = to ⟨$⟩ j

    ∈-if-not-i : ∀ {j} → i ≢ j → to ⟨$⟩ j ∈ xs
    ∈-if-not-i i≢j = not-x (i≢j ∘ injective ∘ trans ≡x ∘ sym)

    lemma : ∀ {k j} → k ≤ j → suc j ≢ k
    lemma 1+j≤j refl = NatProp.1+n≰n 1+j≤j

    ∈xs : ∀ j → f j ∈ xs
    ∈xs j with STO.compare i j
    ∈xs j  | tri< (i≤j , _) _ _ = ∈-if-not-i (lemma i≤j ∘ sym)
    ∈xs j  | tri> _ i≢j _       = ∈-if-not-i i≢j
    ∈xs .i | tri≈ _ refl _      =
      ∈-if-not-i (NatProp.m≢1+m+n i ∘
                  subst (_≡_ i ∘ suc) (sym $ proj₂ CS.+-identity i))

    injective′ : Inj.Injective {B = P.setoid A} (→-to-⟶ f)
    injective′ {j} {k} eq with STO.compare i j | STO.compare i k
    ... | tri< _ _ _         | tri< _ _ _         = cong pred                                   $ injective eq
    ... | tri< _ _ _         | tri≈ _ _ _         = cong pred                                   $ injective eq
    ... | tri< (i≤j , _) _ _ | tri> _ _ (k≤i , _) = ⊥-elim (lemma (DTO.trans k≤i i≤j)           $ injective eq)
    ... | tri≈ _ _ _         | tri< _ _ _         = cong pred                                   $ injective eq
    ... | tri≈ _ _ _         | tri≈ _ _ _         = cong pred                                   $ injective eq
    ... | tri≈ _ i≡j _       | tri> _ _ (k≤i , _) = ⊥-elim (lemma (subst (_≤_ k) i≡j k≤i)       $ injective eq)
    ... | tri> _ _ (j≤i , _) | tri< (i≤k , _) _ _ = ⊥-elim (lemma (DTO.trans j≤i i≤k)     $ sym $ injective eq)
    ... | tri> _ _ (j≤i , _) | tri≈ _ i≡k _       = ⊥-elim (lemma (subst (_≤_ j) i≡k j≤i) $ sym $ injective eq)
    ... | tri> _ _ (j≤i , _) | tri> _ _ (k≤i , _) =                                               injective eq

    inj′ = record
      { to        = →-to-⟶ {B = P.setoid A} f
      ; injective = injective′
      }


text:
{-# OPTIONS --without-K --safe #-}
module Cats.Util.SetoidReasoning where

open import Relation.Binary.Reasoning.MultiSetoid public

open import Relation.Binary using (Setoid)

module _ {c ℓ} (S : Setoid c ℓ) where

  open Setoid S

  triangle :
    ∀ m {x y}
    → x ≈ m
    → y ≈ m
    → x ≈ y
  triangle m x≈m y≈m = trans x≈m (sym y≈m)

max_stars_repo_name: JLimperg/cats

max_issues_repo_name: JLimperg/cats

max_forks_repo_name: JLimperg/cats


text:
-- {-# OPTIONS -v tc.meta:30 #-}

module GiveSize where

{-# BUILTIN SIZE Size #-}

postulate
  A : Size → Set
  c : ∀ i → A i

k : ∀ i → A i
k i = c {!i!}


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

-- This file documents a bug caused by one of the fixes for issue 153.

module Issue153 where

open import Common.Coinduction

record R : Set₁ where
  field
    S : Set
    T : S → Set

module D (r : R) (s : R.S r) where
  open R r

  data D (t : T s) : Set where

module M (r : R) (s : R.S r) where
  open R r
  open D _ s

  postulate
    t : T s
    d : D t

  foo : ∞ (D t)
  foo = ♯ d

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/Interaction/Highlighting/Generate.hs:383


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

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

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

-- Following Part IB's course Groups, Rings, and Modules, we take rings to be commutative with one.
module Rings.Definition where

record Ring {n m} {A : Set n} (S : Setoid {n} {m} A) (_+_ : A → A → A) (_*_ : A → A → A) : Set (lsuc n ⊔ m) where
  field
    additiveGroup : Group S _+_
  open Group additiveGroup
  open Setoid S
  open Equivalence eq
  0R : A
  0R = 0G
  _-R_ : A → A → A
  a -R b = a + (inverse b)
  field
    *WellDefined : {r s t u : A} → (r ∼ t) → (s ∼ u) → r * s ∼ t * u
    1R : A
    groupIsAbelian : {a b : A} → a + b ∼ b + a
    *Associative : {a b c : A} → (a * (b * c)) ∼ (a * b) * c
    *Commutative : {a b : A} → a * b ∼ b * a
    *DistributesOver+ : {a b c : A} → a * (b + c) ∼ (a * b) + (a * c)
    identIsIdent : {a : A} → 1R * a ∼ a
  timesZero : {a : A} → a * 0R ∼ 0R
  timesZero {a} = symmetric (transitive (transitive (symmetric invLeft) (+WellDefined reflexive (transitive (*WellDefined {a} {a} reflexive (symmetric identRight)) *DistributesOver+))) (transitive +Associative (transitive (+WellDefined invLeft reflexive) identLeft)))
  timesZero' : {a : A} → 0R * a ∼ 0R
  timesZero' {a} = transitive *Commutative timesZero
  *DistributesOver+' : {a b c : A} → (a + b) * c ∼ (a * c) + (b * c)
  *DistributesOver+' = transitive *Commutative (transitive *DistributesOver+ (+WellDefined *Commutative *Commutative))
  *Associative' : {a b c : A} → ((a * b) * c) ∼ (a * (b * c))
  *Associative' = symmetric *Associative
  identIsIdent' : {a : A} → a * 1R ∼ a
  identIsIdent' = transitive *Commutative identIsIdent


text:
module MLib.Matrix.Core where

open import MLib.Prelude
open import MLib.Algebra.PropertyCode
open import MLib.Algebra.PropertyCode.Structures

import Relation.Binary.Indexed as I

Matrix : ∀ {a} → Set a → ℕ → ℕ → Set a
Matrix A m n = Fin m → Fin n → A

module _ {a} (A : Set a) where
  row : ∀ {m n} → Fin m → Matrix A m n → Table A n
  row i M .lookup j = M i j

  col : ∀ {m n} → Fin n → Matrix A m n → Table A m
  col j M .lookup i = M i j


text:
module to-string-tests where

open import lib
open import cedille-types
open import syntax-util
open import to-string

t = mapp (mapp (mvar "plus") (mvar "Z")) (mvar "Z")
s = term-to-string t

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

{-# OPTIONS --guardedness #-}

open import Level

open import Data.Empty
open import Data.Unit
open import Data.Product
open import Data.Sum
open import Data.Bool
open import Data.List using (List)

open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Relation.Unary using (Pred; _∈_; _⊆_; Empty; Satisfiable)
open import Relation.Binary.PropositionalEquality using (_≡_; refl ; subst ; cong)

open import Common

module SessionType {ℙ : Set} (message : Message ℙ)
  where

data    SessionType : Set
record ∞SessionType : Set where
  constructor box_
  coinductive
  field force : SessionType
open ∞SessionType public

Continuation : Set
Continuation = ℙ -> ∞SessionType

data SessionType where
  nil : SessionType
  inp : (f : Continuation) -> SessionType
  out : (f : Continuation) -> SessionType

data Defined : SessionType -> Set where
  inp : ∀{f} -> Defined (inp f)
  out : ∀{f} -> Defined (out f)

Defined? : (T : SessionType) -> Dec (Defined T)
Defined? nil     = no λ ()
Defined? (inp _) = yes inp
Defined? (out _) = yes out

Defined-eq : ∀{T : SessionType} (p : Defined T) (q : Defined T) -> p ≡ q
Defined-eq inp inp = refl
Defined-eq out out = refl

dom : Continuation -> Pred ℙ Level.zero
dom f x = Defined (f x .force)

_∈?_ : (x : ℙ) (f : Continuation) -> Dec (x ∈ dom f)
x ∈? f with f x .force
... | nil   = no λ ()
... | inp _ = yes inp
... | out _ = yes out

EmptyContinuation : Continuation -> Set
EmptyContinuation f = Empty (dom f)

Witness : Continuation -> Set
Witness f = Satisfiable (dom f)

Empty? : (f : Continuation) -> EmptyContinuation f ⊎ Witness f
Empty? f with excluded-middle {Witness f}
... | yes w = inj₂ w
... | no nw = inj₁ λ x def -> nw (x , def)

-- WARNING: Win and End must be different predicates, because
-- client-wise they are different, whereas Server-wise they are
-- equivalent. inp cannot be End or else an ended client may receive
-- a message and fail!

data Win : SessionType -> Set where
  out : ∀{f} (U : EmptyContinuation f) -> Win (out f)

data End : SessionType -> Set where
  inp : ∀{f} (U : EmptyContinuation f) -> End (inp f)
  out : ∀{f} (U : EmptyContinuation f) -> End (out f)

win : SessionType
win = out λ _ -> λ where .force -> nil

Win-win : Win win
Win-win = out λ { _ () }

win->defined : ∀{T} -> Win T -> Defined T
win->defined (out _) = out

-- if T is not Defined, then it is nil
not-def->nil : ∀{T} → ¬ (Defined T) → T ≡ nil
not-def->nil {nil} nd = refl
not-def->nil {inp f} nd = ⊥-elim (nd inp)
not-def->nil {out f} nd = ⊥-elim (nd out)

not-nil-defined : Defined nil → ⊥
not-nil-defined ()

open Message message

if-≡-ch : (x y : ℙ) → SessionType → SessionType → SessionType
if-≡-ch x y S T with x ?= y
... | no ¬p = T
... | yes refl = S

sample-cont : ℙ → SessionType → SessionType → Continuation
force (sample-cont t S T x) = if-≡-ch x t S T

cont-not-def : ∀{t} → ¬ (Defined (sample-cont t nil win t .force))
cont-not-def {t} ok with t ?= t
cont-not-def {t} () | yes refl
... | no ¬eq = ⊥-elim (¬eq refl)

force-eq : ∀{t S T} → S ≡ (sample-cont t S T) t .force
force-eq {t} with t ?= t
... | no ¬p = ⊥-elim (¬p refl)
... | yes refl = refl

wit-cont : ∀{t S T} → Defined S → Witness (sample-cont t S T)
wit-cont {t} def = t , subst Defined force-eq def

sample-in : (t : ℙ) → SessionType → SessionType
sample-in t S = inp (sample-cont t S nil)

sample-out : (t : ℙ) → SessionType → SessionType
sample-out t S = out (sample-cont t S nil)

full-cont : SessionType → Continuation
force (full-cont S _) = S

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution {{eqrel : EqRelSet}} where

open import Agda.Primitive

open import Definition.Untyped
open import Definition.Typed
open import Definition.LogicalRelation

open import Tools.Embedding
open import Tools.Product
open import Tools.Unit

-- The validity judgements:
-- We consider expressions that satisfy these judgments valid

ValRel : Setω₂
ValRel = (Γ : Con Term) → (⊩Subst : (Δ : Con Term) → Subst → ⊢ Δ → Setω)
    → (⊩EqSubst : (Δ : Con Term) → (σ σ′ : Subst) → (⊢Δ : ⊢ Δ) → (⊩Subst Δ σ ⊢Δ) → Setω)
    → Setω₁

record ⊩ᵛ⁰_/_ (Γ : Con Term) (_⊩_▸_ : ValRel) : Setω₁ where
  inductive
  eta-equality
  constructor VPack
  field
    ⊩Subst : (Δ : Con Term) → Subst → ⊢ Δ → Setω
    ⊩EqSubst : (Δ : Con Term) → (σ σ′ : Subst) → (⊢Δ : ⊢ Δ) → (⊩Subst Δ σ ⊢Δ) → Setω
    ⊩V : Γ ⊩ ⊩Subst ▸ ⊩EqSubst

_⊩ˢ⁰_∷_/_/_ : {R : ValRel} (Δ : Con Term) (σ : Subst) (Γ : Con Term) ([Γ] : ⊩ᵛ⁰ Γ / R) (⊢Δ : ⊢ Δ)
           → Setω
Δ ⊩ˢ⁰ σ ∷ Γ / VPack ⊩Subst ⊩EqSubst ⊩V / ⊢Δ = ⊩Subst Δ σ ⊢Δ

_⊩ˢ⁰_≡_∷_/_/_/_ : {R : ValRel} (Δ : Con Term) (σ σ′ : Subst) (Γ : Con Term) ([Γ] : ⊩ᵛ⁰ Γ / R)
                 (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ⁰ σ ∷ Γ / [Γ] / ⊢Δ) → Setω
Δ ⊩ˢ⁰ σ ≡ σ′ ∷ Γ / VPack ⊩Subst ⊩EqSubst ⊩V / ⊢Δ / [σ] = ⊩EqSubst Δ σ σ′ ⊢Δ [σ]

-- Validity of types
_⊩ᵛ⁰⟨_⟩_/_ : {R : ValRel} (Γ : Con Term) (l : TypeLevel) (A : Term) → ⊩ᵛ⁰ Γ / R → Setω
_⊩ᵛ⁰⟨_⟩_/_ Γ l A [Γ] =
  ∀ {Δ σ} (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ⁰ σ ∷ Γ / [Γ] / ⊢Δ)
  → Σω₀ (Δ ⊩⟨ l ⟩ subst σ A) (λ [Aσ]
    → ∀ {σ′} ([σ′] : Δ ⊩ˢ⁰ σ′ ∷ Γ / [Γ] / ⊢Δ)
      ([σ≡σ′] : Δ ⊩ˢ⁰ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ])
    → Δ ⊩⟨ l ⟩ subst σ A ≡ subst σ′ A / [Aσ])

data _⊩V_▸_ : ValRel where
  Vε : ε
    ⊩V (λ Δ σ ⊢Δ → ⊤′)
    ▸ (λ Δ σ σ′ ⊢Δ [σ] → ⊤′)
  V∙ : ∀ {Γ A l}
    → ([Γ] : ⊩ᵛ⁰ Γ / _⊩V_▸_)
    → ([A] : Γ ⊩ᵛ⁰⟨ l ⟩ A / [Γ])
    → Γ ∙ A
        ⊩V (λ Δ σ ⊢Δ → Σω₂ (Δ ⊩ˢ⁰ tail σ ∷ Γ / [Γ] / ⊢Δ)
                         (λ [tailσ] → (Δ ⊩⟨ l ⟩ head σ ∷ subst (tail σ) A / proj₁ ([A] ⊢Δ [tailσ]))))
        ▸ (λ Δ σ σ′ ⊢Δ [σ] → (Δ ⊩ˢ⁰ tail σ ≡ tail σ′ ∷ Γ / [Γ] / ⊢Δ / proj₁ [σ]) ×ω₂
             (Δ ⊩⟨ l ⟩ head σ ≡ head σ′ ∷ subst (tail σ) A / proj₁ ([A] ⊢Δ (proj₁ [σ]))))

⊩ᵛ : Con Term → Setω₁
⊩ᵛ Γ = ⊩ᵛ⁰ Γ / _⊩V_▸_

_⊩ˢ_∷_/_/_ : (Δ : Con Term) (σ : Subst) (Γ : Con Term) ([Γ] : ⊩ᵛ Γ) (⊢Δ : ⊢ Δ)
           → Setω
Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ = Δ ⊩ˢ⁰ σ ∷ Γ / [Γ] / ⊢Δ

_⊩ˢ_≡_∷_/_/_/_ : (Δ : Con Term) (σ σ′ : Subst) (Γ : Con Term) ([Γ] : ⊩ᵛ Γ)
                 (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ) → Setω
Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ] = Δ ⊩ˢ⁰ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ]

-- Validity of types
_⊩ᵛ⟨_⟩_/_ : (Γ : Con Term) (l : TypeLevel) (A : Term) → ⊩ᵛ Γ → Setω
Γ ⊩ᵛ⟨ l ⟩ A / [Γ] = Γ ⊩ᵛ⁰⟨ l ⟩ A / [Γ]

-- Validity of terms
_⊩ᵛ⟨_⟩_∷_/_/_ : (Γ : Con Term) (l : TypeLevel) (t A : Term) ([Γ] : ⊩ᵛ Γ)
                 ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ]) → Setω
Γ ⊩ᵛ⟨ l ⟩ t ∷ A / [Γ] / [A] =
  ∀ {Δ σ} (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ) →
  Σω₀ (Δ ⊩⟨ l ⟩ subst σ t ∷ subst σ A / proj₁ ([A] ⊢Δ [σ])) λ [tσ] →
  ∀ {σ′} → Δ ⊩ˢ σ′ ∷ Γ / [Γ] / ⊢Δ → Δ ⊩ˢ σ ≡ σ′ ∷ Γ / [Γ] / ⊢Δ / [σ]
    → Δ ⊩⟨ l ⟩ subst σ t ≡ subst σ′ t ∷ subst σ A / proj₁ ([A] ⊢Δ [σ])

-- Validity of type equality
_⊩ᵛ⟨_⟩_≡_/_/_ : (Γ : Con Term) (l : TypeLevel) (A B : Term) ([Γ] : ⊩ᵛ Γ)
                ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ]) → Setω
Γ ⊩ᵛ⟨ l ⟩ A ≡ B / [Γ] / [A] =
  ∀ {Δ σ} (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
  → Δ ⊩⟨ l ⟩ subst σ A ≡ subst σ B / proj₁ ([A] ⊢Δ [σ])

-- Validity of term equality
_⊩ᵛ⟨_⟩_≡_∷_/_/_ : (Γ : Con Term) (l : TypeLevel) (t u A : Term) ([Γ] : ⊩ᵛ Γ)
                    ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ]) → Setω
Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ A / [Γ] / [A] =
  ∀ {Δ σ} → (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
          → Δ ⊩⟨ l ⟩ subst σ t ≡ subst σ u ∷ subst σ A / proj₁ ([A] ⊢Δ [σ])

-- Valid term equality with validity of its type and terms
record [_⊩ᵛ⟨_⟩_≡_∷_/_] (Γ : Con Term) (l : TypeLevel)
                       (t u A : Term) ([Γ] : ⊩ᵛ Γ) : Setω where
  constructor modelsTermEq
  field
    [A]   : Γ ⊩ᵛ⟨ l ⟩ A / [Γ]
    [t]   : Γ ⊩ᵛ⟨ l ⟩ t ∷ A / [Γ] / [A]
    [u]   : Γ ⊩ᵛ⟨ l ⟩ u ∷ A / [Γ] / [A]
    [t≡u] : Γ ⊩ᵛ⟨ l ⟩ t ≡ u ∷ A / [Γ] / [A]

-- Validity of reduction of terms
_⊩ᵛ_⇒_∷_/_ : (Γ : Con Term) (t u A : Term) ([Γ] : ⊩ᵛ Γ) → Setω
Γ ⊩ᵛ t ⇒ u ∷ A / [Γ] = ∀ {Δ σ} (⊢Δ : ⊢ Δ) ([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ)
                       → Δ ⊢ subst σ t ⇒ subst σ u ∷ subst σ A

_∙″_ : ∀ {Γ A l} → ([Γ] : ⊩ᵛ Γ) → Γ ⊩ᵛ⟨ l ⟩ A / [Γ] → ⊩ᵛ (Γ ∙ A)
[Γ] ∙″ [A] = (VPack _ _ (V∙ [Γ] [A]))

pattern ε′ = (VPack _ _ Vε)
pattern _∙′_ [Γ] [A] = (VPack _ _ (V∙ [Γ] [A]))