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

record Eq (A : Set) : Set₁ where
  field
    _≈_ : A → A → Set

open Eq {{...}} public

record Setoid : Set₁ where
  field
    ∣_∣    : Set
    {{eq}} : Eq ∣_∣

open Setoid public

instance
  EqNat : Eq Nat
  _≈_ {{EqNat}} = _≡_

NatSetoid : Setoid
∣ NatSetoid ∣ = Nat

thm : (x : ∣ NatSetoid ∣) → x ≈ x
thm x = refl

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Numeral.Integer.Function where

open import Numeral.Integer
open import Numeral.Integer.Oper
open import Numeral.Natural as ℕ using (ℕ)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module AgdaIssue2557 where

record Superclass : Set₁ where field super : Set

open Superclass ⦃ … ⦄ public

record Subclass : Set₁ where
  field
    ⦃ iSuperclass ⦄ : Superclass
    sub : super

open Subclass

postulate A : Set

instance

  SuperclassA : Superclass
  Superclass.super SuperclassA = A → A

postulate function-A : A → A

test-1 : Subclass
Subclass.sub test-1 = {!!} -- Goal: A → A

test-2 : Subclass
test-2 = record { sub = function-A } -- works

test-3 : Subclass
Subclass.iSuperclass test-3 = SuperclassA -- (could also put "it" here)
Subclass.sub test-3 = function-A -- works

test-4 : Subclass
Subclass.sub test-4 = {!function-A!} -- fails

-- test-5 : Subclass
-- Subclass.sub test-5 x = {!!} -- fails

test-6 : Subclass
Subclass.sub test-6 = {!λ x → {!!}!} -- fails


text:
{-# OPTIONS --cubical --no-import-sorts --allow-unsolved-metas #-}

module Test.Number where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)

private
  variable
    ℓ ℓ' ℓ'' : Level

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Relation.Nullary.Base -- ¬_
open import Cubical.Relation.Binary.Base -- Rel
open import Cubical.Data.Unit.Base -- Unit
open import Cubical.Data.Empty -- ⊥
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Empty renaming (elim to ⊥-elim) -- `⊥` and `elim`
open import Function.Base using (it; _∋_; _$_)

-- open import Data.Nat.Base using (ℕ) renaming (_≤_ to _≤ₙ_)
-- open import Cubical.Data.Nat using (ℕ; zero; suc) renaming (_+_ to _+ₙ_)
-- open import Cubical.Data.Nat.Order renaming (zero-≤ to z≤n; suc-≤-suc to s≤s; _≤_ to _≤ₙ_; _<_ to _<ₙ_)
-- open import Cubical.Data.Fin.Base
-- import Cubical.Data.Fin.Properties
-- open import Cubical.Data.Nat using (ℕ; zero; suc) renaming (_+_ to _+ₙ_)
-- open import Cubical.Data.Nat.Properties using (+-suc; injSuc; snotz; +-comm; +-assoc; +-zero; inj-m+)
-- open import Cubical.Data.Nat.Order renaming (zero-≤ to z≤n; suc-≤-suc to s≤s; _≤_ to _≤ₙ_; _<_ to _<ₙ_; _≟_ to _≟ₙ_)
-- open import Data.Nat.Base using (ℕ; z≤n; s≤s; zero; suc) renaming (_≤_ to _≤ₙ_; _<_ to _<ₙ_; _+_ to _+ₙ_)
-- open import Agda.Builtin.Bool renaming (true to TT; false to FF)
-- import Cubical.Data.Fin.Properties
-- open import Data.Nat.Properties using (+-mono-<)

-- open import Bundles

open import Number.Postulates
open import Number.Structures
open import Number.Bundles
open import Number.Inclusions
open import Number.Base
open import Number.Coercions
open import Number.Operations

open ℕⁿ
open ℤᶻ
open ℚᶠ
open ℝʳ
open ℂᶜ

import Data.Nat.Properties

-- NOTE: well, for 15 allowed coercions, we might just enumerate them
--   unfortunately with overlapping patterns a style as in `Cl` is not possible
--   we need to explicitly write out all the 5×5 combinations
--   or, we implement a min operator which might work even with overlapping patterns

-- num {isNat     ,, p} (x ,, q) = x
-- num {isInt     ,, p} (x ,, q) = x
-- num {isRat     ,, p} (x ,, q) = x
-- num {isReal    ,, p} (x ,, q) = x
-- num {isComplex ,, p} (x ,, q) = x

-- TODO: name this "inject" instead of "coerce"
-- TODO: make the module ℤ and the Carrier ℤ.ℤ
-- TODO: for a binary relation `a # b` it would be nice to have a way to compose ≡-pathes to the left and the right
--       similar to how ∙ can be used for pathes
--       this reasoning might extend to transitive relations
--       `cong₂ _#_ refl x` and `cong₂ _#_ x refl` to this (together with `transport`)
-- NOTE: maybe ℕ↪ℤ should be a postfix operation

-- module _ where
-- module ℕ' = ROrderedCommSemiring ℕ.Bundle
-- module ℤ' = ROrderedCommRing     ℤ.Bundle
-- module ℚ' = ROrderedField        ℚ.Bundle
-- module ℝ' = ROrderedField        ℝ.Bundle
-- module ℂ' = RField               ℂ.Bundle--

-- coerce-OCSR : ∀{l p} {ll : NumberKind} {𝕏OCSR 𝕐OCSR : ROrderedCommSemiring {ℝℓ} {ℝℓ'}}
--             → (x : Number (l ,, p))
--             → {f : Il l → Il ll}
--             → IsROrderedCommSemiringInclusion 𝕏OCSR 𝕐OCSR f
--             → Ip ll p (f (num x))
-- coerce-OCSR {l} {ll} {p} {𝕏OCSR} {𝕐OCSR} {f} (x ,, q) = ?

{-
private
  instance
    z≤n' : ∀ {n}                 → zero  ≤ₙ n
    z≤n' {n} = z≤n
    s≤s' : ∀ {m n} {{m≤n : m ≤ₙ n}} → suc m ≤ₙ suc n
    s≤s' {m} {n} {{m≤n}} = s≤s m≤n
-}

{-
-- TODO: why does `it` not work here?
⁻¹-Levels : (a : NumberKind) → Σ[ b ∈ NumberKind ] a ≤ₙₗ b
⁻¹-Levels isNat     = isRat     , z≤n -- it
⁻¹-Levels isInt     = isRat     , s≤s z≤n -- s≤s' {{z≤n'}}
⁻¹-Levels isRat     = isRat     , s≤s (s≤s z≤n)
⁻¹-Levels isReal    = isReal    , s≤s (s≤s (s≤s z≤n)) -- it
⁻¹-Levels isComplex = isComplex , s≤s (s≤s (s≤s (s≤s z≤n)))

⁻¹-Levels' : (a : NumberKind) → NumberKind
⁻¹-Levels' x = maxₙₗ x isRat
-}

open PatternsType

{-
private
  pattern X   = anyPositivity
  pattern X⁺⁻ = isNonzero
  pattern X₀⁺ = isNonnegative
  pattern X⁺  = isPositive
  pattern X⁻  = isNegative
  pattern X₀⁻ = isNonpositive
-}

{-
⁻¹-Types : NumberProp → Maybe NumberProp
⁻¹-Types (level ,, X  ) = nothing
⁻¹-Types (level ,, X₀⁺) = nothing
⁻¹-Types (level ,, X₀⁻) = nothing
⁻¹-Types (level ,, p  ) = just (fst (⁻¹-Levels level) ,, p)
-}

-- ∀{{ q : Unit }} → Number (level ,, X⁺⁻)
-- ∀{{ q : Unit }} → Number (level ,, X⁺ )
-- ∀{{ q : Unit }} → Number (level ,, X⁻ )

-- pattern [ℝ₀⁺] = (isReal , X₀⁺)
-- [ℝ₀⁺] = Number (isReal , isNonnegativeᵒʳ)
-- [ℝ⁺]  = Number (isReal , isPositiveᵒʳ)
-- [ℕ⁺]  = Number (isNat  , isPositiveᵒʳ)
-- [ℝ]   = Number (isReal , anyPositivityᵒʳ)

open import Number.Prettyprint

-- {-# DISPLAY maxₙₗ' isReal isReal = isReal #-}
-- {-# DISPLAY Number (isReal , isNonnegative) = [ℝ₀⁺] #-}
-- {-# DISPLAY Number (isReal , isPositive)    = [ℝ⁺]  #-}

[1ʳ] : [ℝ⁺]
[1ʳ] = 1ʳ ,, ℝ.0<1

[1]-Type : (l : NumberKind) → Type (NumberLevel l)
[1]-Type isNat     = [ℕ⁺]
[1]-Type isInt     = [ℤ⁺]
[1]-Type isRat     = [ℚ⁺]
[1]-Type isReal    = [ℝ⁺]
[1]-Type isComplex = [ℂ⁺⁻]

-- NOTE: this is ambiguous with generic operations such as _+_
[1] : ∀{l} → [1]-Type l
[1] {isNat}     = 1ⁿ ,, ℕ.0<1
[1] {isInt}     = 1ᶻ ,, ℤ.0<1
[1] {isRat}     = 1ᶠ ,, ℚ.0<1
[1] {isReal}    = 1ʳ ,, ℝ.0<1
[1] {isComplex} = 1ᶜ ,, ℂ.1#0

-- test101 : Number (isNat , isPositiveᵒʳ) → Number (isReal ,  isNonnegativeᵒʳ) → {!!}

open import Function.Base using (typeOf)

test201 : [ℕ⁺] → [ℝ₀⁺] → [ℝ]
-- As-patterns (or @-patterns) go well with resolving things in our approach
test201 n@(nn ,, np) r@(rn ,, rp) = let
-- generic operations are provided
-- q : [ℕ⁺]
-- z : [ℝ₀⁺]
   q = n + n
   z = r + r

-- we can project-out the underlying number of a `Number` with `num`
-- zʳ : ℝ
   zʳ = num z

-- and we can project-out the property of a `Number` with `prp`
-- zp : 0ʳ ≤ʳ (rn +ʳ rn)
   zp = prp z

-- since the generic `_+_` makes use of `_+ʳ_` on ℝ, we get definitional equality
   _ : zʳ ≡ rn +ʳ rn
   _ = refl

-- we can turn a generic number into a Σ pair with `pop`
-- qʳ   : ℕ₀
-- qʳ   = nn +ⁿ nn
-- qp   : 0ⁿ <ⁿ (nn +ⁿ nn)
-- qp   = +-<-<-implies-<ʳ nn nn np np
   (qʳ , qp) = pop q

-- and we can create a number with `_,,_`
-- this needs some type annotation for help
   q' : typeOf q
   q' = qʳ ,, qp

-- if the two parts of q and q' are in scope, then we get definitional equality
   _ : q ≡ q'
   _ = refl

-- r is nonnegative from [ℝ₀⁺], [1ʳ] is positive from [ℝ⁺]
-- and _+_ makes use of the fact that "positive + nonnegative = positive"
-- y : [ℝ⁺]
-- y = (rn +ʳ 1ʳ) ,, +-≤-<-implies-<ʳ rn 1ʳ rp 0<1
   y =  r + [1ʳ]

-- _+_ automatically coerces n from ℕ⁺ to ℝ⁺
-- and uses the fact that "positive + nonnegative = positive"
-- n+r : [ℝ⁺]
-- n+r = (ℕ↪ℝ nn +ʳ rn) ,, +-<-≤-implies-<ʳ (ℕ↪ℝ nn) rn (coerce-ℕ↪ℝ (nn ,, np)) rp
   n+r = n + r

-- generic relations like _<_ also make use of their underlying relations
-- and therefore we also get definitional equality, no matter how the relation is stated
   pp   : [1ʳ] <      (r  + [1ʳ])
   pp   = {!!}
   pp'  :  1ʳ  <ʳ num (r  + [1ʳ])
   pp'  = {!!}
   pp'' :  1ʳ  <ʳ     (rn +ʳ 1ʳ )
   pp'' = {!!}
   _ : (pp ≡ pp') × (pp ≡ pp'')
   _ = refl , refl
   in {! - [1ʳ]!}

_ = {! ℕ!}

{-

distance : ∀(x y : [ℝ]) → [ℝ]
distance x y = max (x + (- y)) (- (x + (- y)))

IsCauchy : (x : ℕ → ℝ) → Type (ℓ-max ℓ' ℚℓ)
IsCauchy x = ∀(ε : [ℚ⁺]) → ∃[ N ∈ ℕ ] ∀(m n : ℕ) → N ≤ⁿ m → N ≤ⁿ n → distance (x m) (x n) < ε

-}

test : [ℕ⁺] → [ℝ₀⁺] → [ℝ]
test n@(nn ,, np) r@(rn ,, rp) = let
  q : [ℕ⁺]
  q = n + n
  z : [ℝ₀⁺]
  z = r + r
  k : [ℝ⁺]
  k = n + r
  in {!!}

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
open import Prelude
open import core
open import contexts
open import lemmas-matching

module synth-unicity where
  -- synthesis only produces equal types. note that there is no need for an
  -- analagous theorem for analytic positions because we think of
  -- the type as an input
  synthunicity : {Γ : tctx} {e : hexp} {t t' : htyp} →
                 Γ ⊢ e => t →
                 Γ ⊢ e => t' →
                 t == t'
  synthunicity (SAsc _) (SAsc _) = refl
  synthunicity {Γ = G} (SVar in1) (SVar in2) = ctxunicity {Γ = G} in1 in2
  synthunicity (SAp  D1 MAHole _) (SAp D2 MAHole y) = refl
  synthunicity (SAp D1 MAHole _) (SAp D2 MAArr y) with synthunicity D1 D2
  ... | ()
  synthunicity (SAp D1 MAArr _) (SAp D2 MAHole y) with synthunicity D1 D2
  ... | ()
  synthunicity (SAp D1 MAArr _) (SAp D2 MAArr y) with synthunicity D1 D2
  ... | refl = refl
  synthunicity SEHole SEHole = refl
  synthunicity (SNEHole _) (SNEHole _) = refl
  synthunicity SNum SNum = refl
  synthunicity (SPlus _ _) (SPlus _ _) = refl
  synthunicity (SLam _ D1) (SLam _ D2) with synthunicity D1 D2
  synthunicity (SLam x₁ D1) (SLam x₂ D2) | refl = refl
  synthunicity (SPair D1 D2) (SPair D3 D4)
    with synthunicity D1 D3 | synthunicity D2 D4
  ... | refl | refl = refl
  synthunicity (SFst D1 x) (SFst D2 x₁) with synthunicity D1 D2
  ... | refl with ▸prod-unicity x x₁
  ... | refl = refl
  synthunicity (SSnd D1 x) (SSnd D2 x₁) with synthunicity D1 D2
  ... | refl with ▸prod-unicity x x₁
  ... | refl = refl

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
-- Minimal logic, PHOAS approach, initial encoding

module Pi.M (Indiv : Set) where

-- Types

data Ty : Set

Pred : Set
Pred = Indiv -> Ty

infixl 2 _&&_
infixl 1 _||_
infixr 0 _=>_
data Ty where
  UNIT   :             Ty
  _=>_   : Ty -> Ty -> Ty
  _&&_   : Ty -> Ty -> Ty
  _||_   : Ty -> Ty -> Ty
  FALSE  :             Ty
  FORALL : Pred     -> Ty
  EXISTS : Pred     -> Ty

infixr 0 _<=>_
_<=>_ : Ty -> Ty -> Ty
a <=> b = (a => b) && (b => a)

NOT : Ty -> Ty
NOT a = a => FALSE

TRUE : Ty
TRUE = FALSE => FALSE

-- Context and truth/individual judgement

data El : Set where
  mkTrue  : Ty    -> El
  mkIndiv : Indiv -> El

Cx : Set1
Cx = El -> Set

isTrue : Ty -> Cx -> Set
isTrue a tc = tc (mkTrue a)

isIndiv : Indiv -> Cx -> Set
isIndiv x tc = tc (mkIndiv x)

-- Terms

module M where
  infixl 2 _$$_
  infixl 1 _$_
  data Tm (tc : Cx) : Ty -> Set where
    var    : forall {a}     -> isTrue a tc                      -> Tm tc a
    lam'   : forall {a b}   -> (isTrue a tc -> Tm tc b)         -> Tm tc (a => b)
    _$_    : forall {a b}   -> Tm tc (a => b)   -> Tm tc a      -> Tm tc b
    pair'  : forall {a b}   -> Tm tc a          -> Tm tc b      -> Tm tc (a && b)
    fst    : forall {a b}   -> Tm tc (a && b)                   -> Tm tc a
    snd    : forall {a b}   -> Tm tc (a && b)                   -> Tm tc b
    left   : forall {a b}   -> Tm tc a                          -> Tm tc (a || b)
    right  : forall {a b}   -> Tm tc b                          -> Tm tc (a || b)
    case'  : forall {a b c} -> Tm tc (a || b)   -> (isTrue a tc -> Tm tc c) -> (isTrue b tc -> Tm tc c) -> Tm tc c
    pi'    : forall {p}     -> (forall {x} -> isIndiv x tc -> Tm tc (p x)) -> Tm tc (FORALL p)
    _$$_   : forall {p x}   -> Tm tc (FORALL p) -> isIndiv x tc -> Tm tc (p x)
    sig'   : forall {p x}   -> isIndiv x tc     -> Tm tc (p x)  -> Tm tc (EXISTS p)
    split' : forall {p x a} -> Tm tc (EXISTS p) -> (isTrue (p x) tc -> Tm tc a) -> Tm tc a

  lam'' : forall {tc a b} -> (Tm tc a -> Tm tc b) -> Tm tc (a => b)
  lam'' f = lam' \x -> f (var x)

  case'' : forall {tc a b c} -> Tm tc (a || b) -> (Tm tc a -> Tm tc c) -> (Tm tc b -> Tm tc c) -> Tm tc c
  case'' xy f g = case' xy (\x -> f (var x)) (\y -> g (var y))

  split'' : forall {tc p x a} -> Tm tc (EXISTS p) -> (Tm tc (p x) -> Tm tc a) -> Tm tc a
  split'' x f = split' x \y -> f (var y)

  syntax lam''   (\a -> b)   = lam a => b
  syntax pair'   x y         = [ x , y ]
  syntax case''  xy (\x -> z1) (\y -> z2) = case xy of x => z1 or y => z2
  syntax pi'     (\x -> px)  = pi x => px
  syntax sig'    x px        = [ x ,, px ]
  syntax split'' x (\y -> z) = split x as y => z

  Thm : Ty -> Set1
  Thm a = forall {tc} -> Tm tc a
open M public

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
module _ where

open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

record R : Set₁ where
  field
    _≡_  : {A : Set} → A → A → Set
    refl : {A : Set} (x : A) → x ≡ x

record R′ (_ : Set) : Set where

module _ (r : R) (_ : {A : Set} → R′ A) where

  open R r

  macro

    m : Term → TC ⊤
    m goal =
      bindTC (unify (def (quote refl)
                         (arg (arg-info visible relevant) unknown ∷ []))
                    goal) λ _ →
      bindTC solveConstraints λ _ →
      bindTC (reduce goal) λ where
        (meta m _) → typeError (strErr "Meta" ∷ [])
        _          → returnTC _

  test : true ≡ true
  test = m

  macro

    m′ : Term → TC ⊤
    m′ goal =
      bindTC (unify (def (quote refl)
                         (arg (arg-info visible relevant) unknown ∷ []))
                    goal) λ _ →
      bindTC (reduce goal) λ where
        goal@(meta m _) →
          bindTC (solveConstraintsMentioning (m ∷ [])) λ _ →
          bindTC (reduce goal) λ where
            (meta _ _) → typeError (strErr "Meta" ∷ [])
            _          → returnTC _
        _ → returnTC _

  test′ : true ≡ true
  test′ = m′

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


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

open import lib.Basics
open import lib.Relation
open import lib.NType2
open import lib.types.Pi

module lib.types.SetQuotient {i} {A : Type i} {j} where

postulate  -- HIT
  SetQuot : (R : Rel A j) → Type (lmax i j)

module _ {R : Rel A j} where

  postulate  -- HIT
    q[_] : (a : A) → SetQuot R
    quot-rel : {a₁ a₂ : A} → R a₁ a₂ → q[ a₁ ] == q[ a₂ ]
    SetQuot-level : is-set (SetQuot R)

  SetQuot-is-set = SetQuot-level

  module SetQuotElim {k} {P : SetQuot R → Type k}
    (p : (x : SetQuot R) → is-set (P x)) (q[_]* : (a : A) → P q[ a ])
    (rel* : ∀ {a₁ a₂} (r : R a₁ a₂) → q[ a₁ ]* == q[ a₂ ]* [ P ↓ quot-rel r ]) where

    postulate  -- HIT
      f : Π (SetQuot R) P
      q[_]-β : (a : A) → f q[ a ] ↦ q[ a ]*
    {-# REWRITE q[_]-β #-}

    postulate  -- HIT
      quot-rel-β : ∀ {a₁ a₂} (r : R a₁ a₂) → apd f (quot-rel r) == rel* r

  open SetQuotElim public using () renaming (f to SetQuot-elim)

  module SetQuotRec {k} {B : Type k} (p : is-set B)
    (q[_]* : A → B) (rel* : ∀ {a₁ a₂} (r : R a₁ a₂) → q[ a₁ ]* == q[ a₂ ]*) where

    private
      module M = SetQuotElim (λ x → p) q[_]* (λ {a₁ a₂} r → ↓-cst-in (rel* r))

    f : SetQuot R → B
    f = M.f

  open SetQuotRec public using () renaming (f to SetQuot-rec)

  -- If [R] is an equivalence relation, then [quot-rel] is an equivalence.

module _ {R : Rel A j}
  (R-is-prop : ∀ {a b} → is-prop (R a b))
  (R-is-refl : is-refl R) (R-is-sym : is-sym R)
  (R-is-trans : is-trans R) where

  private
    Q : Type (lmax i j)
    Q = SetQuot R

    R'-over-quot : Q → Q → hProp j
    R'-over-quot = SetQuot-rec (→-is-set $ hProp-is-set j)
      (λ a → SetQuot-rec (hProp-is-set j)
        (λ b → R a b , R-is-prop)
        (nType=-out ∘ lemma-a))
      (λ ra₁a₂ → λ= $ SetQuot-elim
        (λ _ → raise-level -1 $ hProp-is-set j _ _)
        (λ _ → nType=-out $ lemma-b ra₁a₂)
        (λ _ → prop-has-all-paths-↓ $ hProp-is-set j _ _))
      where
        abstract
          lemma-a : ∀ {a b₁ b₂} → R b₁ b₂ → R a b₁ == R a b₂
          lemma-a rb₁b₂ = ua $ equiv
            (λ rab₁ → R-is-trans rab₁ rb₁b₂)
            (λ rab₂ → R-is-trans rab₂ (R-is-sym rb₁b₂))
            (λ _ → prop-has-all-paths R-is-prop _ _)
            (λ _ → prop-has-all-paths R-is-prop _ _)

          lemma-b : ∀ {a₁ a₂ b} → R a₁ a₂ → R a₁ b == R a₂ b
          lemma-b ra₁a₂ = ua $ equiv
            (λ ra₁b → R-is-trans (R-is-sym ra₁a₂) ra₁b)
            (λ ra₂b → R-is-trans ra₁a₂ ra₂b)
            (λ _ → prop-has-all-paths R-is-prop _ _)
            (λ _ → prop-has-all-paths R-is-prop _ _)

    R-over-quot : Q → Q → Type j
    R-over-quot q₁ q₂ = fst (R'-over-quot q₁ q₂)

    abstract
      R-over-quot-is-prop : {q₁ q₂ : Q} → is-prop (R-over-quot q₁ q₂)
      R-over-quot-is-prop {q₁} {q₂} = snd (R'-over-quot q₁ q₂)

      R-over-quot-is-refl : (q : Q) → R-over-quot q q
      R-over-quot-is-refl = SetQuot-elim
        (λ q → raise-level -1 (R-over-quot-is-prop {q} {q}))
        (λ a → R-is-refl a)
        (λ _ → prop-has-all-paths-↓ R-is-prop)

      path-to-R-over-quot : {q₁ q₂ : Q} → q₁ == q₂ → R-over-quot q₁ q₂
      path-to-R-over-quot {q} idp = R-over-quot-is-refl q

  quot-rel-equiv : ∀ {a₁ a₂ : A} → R a₁ a₂ ≃ (q[ a₁ ] == q[ a₂ ])
  quot-rel-equiv {a₁} {a₂} = equiv
    quot-rel (path-to-R-over-quot {q[ a₁ ]} {q[ a₂ ]})
    (λ _ → prop-has-all-paths (SetQuot-is-set _ _) _ _)
    (λ _ → prop-has-all-paths R-is-prop _ _)

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module Issue4022 where

open import Common.Prelude
open import Agda.Builtin.Equality
open import Agda.Builtin.Char.Properties
open import Agda.Builtin.String.Properties
open import Agda.Builtin.Float.Properties

open import Issue4022.Import


text:
{-# OPTIONS --cubical --no-import-sorts --guardedness --safe #-}

module Cubical.Codata.M.AsLimit.M where

open import Cubical.Codata.M.AsLimit.M.Base public
open import Cubical.Codata.M.AsLimit.M.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Main where

import Proof


text:
{-# OPTIONS --copatterns --sized-types #-}
-- {-# OPTIONS -v tc.size.solve:30 #-}
-- {-# OPTIONS -v term:40 -v term.proj:60 --show-implicit #-}
-- Andreas, 2013-10-01 Make sure trailing implicit insertion
-- works with copatterns
module CopatternTrailingImplicit where

import Common.Level
open import Common.Size
open import Common.Prelude

-- Sized streams

record Stream (A : Set) {i : Size} : Set where
  coinductive
  field
    head : A
    tail : {j : Size< i} → Stream A {j}
open Stream

-- Mapping over streams

map : {A B : Set} (f : A → B) {i : Size} → Stream A {i} → Stream B {i}
tail (map f {i} s) {j} = map f (tail s)
head (map f s) = f (head s)

-- Nats defined using map
nats : {i : Size} → Stream Nat {i}
head nats = 0
tail nats = map suc nats
-- Before this patch, Agda would insert a {_} also in the `head' clause
-- leading to a type error.

-- 2013-10-12 works now also without manual {_} insertion
-- (See TermCheck.introHiddenLambdas.)
nats' : {i : Size} → Stream Nat {i}
head nats' = 0
tail nats' = map suc nats'
-- Before this latest patch, the termination checker would complain
-- since it would not see the type of the hidden {j : Size< i}
-- which is the argument to the recursive call.

-- All this would not be an issue if Agda still eagerly introduced
-- trailing hidden arguments on the LHS, but this has other
-- drawbacks (Q: even with varying arity?): cannot have
-- hidden lambdas on rhs (used to name trailing hiddens in with-clauses).

max_stars_repo_name: larrytheliquid/agda

max_issues_repo_name: larrytheliquid/agda

max_forks_repo_name: larrytheliquid/agda


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

-- The universe of all types
module hott.core.universe where

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

-- We give an new name for Set
Type : (ℓ : Level) → Set (lsuc ℓ)
Type ℓ = Set ℓ

lone   : Level; lone   = lsuc lzero
ltwo   : Level; ltwo   = lsuc lone
lthree : Level; lthree = lsuc ltwo
lfour  : Level; lfour  = lsuc lthree
lfive  : Level; lfive  = lsuc lfour
lsix   : Level; lsix   = lsuc lfive
lseven : Level; lseven = lsuc lsix
leight : Level; leight = lsuc lseven
lnine  : Level; lnine  = lsuc leight

Type₀ = Type lzero
Type₁ = Type lone
Type₂ = Type ltwo
Type₃ = Type lthree
Type₄ = Type lfour
Type₅ = Type lfive
Type₆ = Type lsix
Type₇ = Type lseven
Type₈ = Type leight
Type₉ = Type lnine

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


text:
{-# OPTIONS --no-positivity-check #-}

module STLC.Coquand.Normalisation where

open import STLC.Coquand.Substitution public

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

record 𝔐 : Set₁ where
  field
    𝒲      : Set

    𝒢      : 𝒲 → Set

    _⊒_    : 𝒲 → 𝒲 → Set

    idₐ    : ∀ {w} → w ⊒ w

    _◇_    : ∀ {w w′ w″} → w″ ⊒ w′ → w′ ⊒ w → w″ ⊒ w

    lid◇   : ∀ {w w′} → (ξ : w′ ⊒ w)
                      → idₐ ◇ ξ ≡ ξ

    rid◇   : ∀ {w w′} → (ξ : w′ ⊒ w)
                      → ξ ◇ idₐ ≡ ξ

    assoc◇ : ∀ {w w′ w″ w‴} → (ξ₁ : w‴ ⊒ w″) (ξ₂ : w″ ⊒ w′) (ξ₃ : w′ ⊒ w)
                            → ξ₁ ◇ (ξ₂ ◇ ξ₃) ≡ (ξ₁ ◇ ξ₂) ◇ ξ₃

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  infix 3 _⊩_
  data _⊩_ : 𝒲 → 𝒯 → Set
    where
      ⟦G⟧ : ∀ {w} → (h : ∀ {w′} → (ξ : w′ ⊒ w)
                                 → 𝒢 w′)
                  → w ⊩ ⎵

      ⟦ƛ⟧ : ∀ {A B w} → (h : ∀ {w′} → (ξ : w′ ⊒ w) (a : w′ ⊩ A)
                                     → w′ ⊩ B)
                      → w ⊩ A ⇒ B

  ⟦g⟧⟨_⟩ : ∀ {w w′} → w′ ⊒ w → w ⊩ ⎵ → 𝒢 w′
  ⟦g⟧⟨ ξ ⟩ (⟦G⟧ f) = f ξ

  _⟦∙⟧⟨_⟩_ : ∀ {A B w w′} → w ⊩ A ⇒ B → w′ ⊒ w → w′ ⊩ A → w′ ⊩ B
  (⟦ƛ⟧ f) ⟦∙⟧⟨ ξ ⟩ a = f ξ a

  -- ⟦putᵣ⟧ can’t be stated here
  -- ⟦getᵣ⟧ can’t be stated here
  -- ⟦wkᵣ⟧ can’t be stated here
  -- ⟦liftᵣ⟧ can’t be stated here
  -- idₐ = ⟦idᵣ⟧

  -- acc = ⟦ren⟧
  acc : ∀ {A w w′} → w′ ⊒ w → w ⊩ A → w′ ⊩ A
  acc {⎵}      ξ f = ⟦G⟧ (λ ξ′   → ⟦g⟧⟨ ξ′ ◇ ξ ⟩ f)
  acc {A ⇒ B} ξ f = ⟦ƛ⟧ (λ ξ′ a → f ⟦∙⟧⟨ ξ′ ◇ ξ ⟩ a)

  -- ⟦wk⟧ can’t be stated here
  -- _◇_ = _⟦○⟧_

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

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  mutual
    data Eq : ∀ {A w} → w ⊩ A → w ⊩ A → Set
      where
        eq⎵ : ∀ {w} → {f₁ f₂ : w ⊩ ⎵}
                    → (h : ∀ {w′} → (ξ : w′ ⊒ w)
                                   → ⟦g⟧⟨ ξ ⟩ f₁ ≡ ⟦g⟧⟨ ξ ⟩ f₂)
                    → Eq f₁ f₂

        eq⊃ : ∀ {A B w} → {f₁ f₂ : w ⊩ A ⇒ B}
                        → (h : ∀ {w′} → (ξ : w′ ⊒ w) {a : w′ ⊩ A} (u : Un a)
                                       → Eq (f₁ ⟦∙⟧⟨ ξ ⟩ a) (f₂ ⟦∙⟧⟨ ξ ⟩ a))
                        → Eq f₁ f₂

    data Un : ∀ {A w} → w ⊩ A → Set
      where
        un⎵ : ∀ {w} → {f : w ⊩ ⎵}
                    → Un f

        un⊃ : ∀ {A B w} → {f : w ⊩ A ⇒ B}
                        → (h₁ : ∀ {w′} → (ξ : w′ ⊒ w)
                                           {a : w′ ⊩ A}
                                           (u : Un a)
                                        → Un (f ⟦∙⟧⟨ ξ ⟩ a))
                        → (h₂ : ∀ {w′} → (ξ : w′ ⊒ w)
                                           {a₁ a₂ : w′ ⊩ A}
                                           (p : Eq a₁ a₂)
                                           (u₁ : Un a₁)
                                           (u₂ : Un a₂)
                                        → Eq (f ⟦∙⟧⟨ ξ ⟩ a₁) (f ⟦∙⟧⟨ ξ ⟩ a₂))
                        → (h₃ : ∀ {w′ w″} → (ξ₁ : w″ ⊒ w′)
                                              (ξ₂ : w′ ⊒ w)
                                              {a : w′ ⊩ A}
                                              (u : Un a)
                                           → Eq (acc ξ₁ (f ⟦∙⟧⟨ ξ₂ ⟩ a))
                                                 (f ⟦∙⟧⟨ ξ₁ ◇ ξ₂ ⟩ (acc ξ₁ a)))
                        → Un f

  reflEq : ∀ {A w} → {a : w ⊩ A}
                   → Un a
                   → Eq a a
  reflEq un⎵            = eq⎵ (λ ξ → refl)
  reflEq (un⊃ h₁ h₂ h₃) = eq⊃ (λ ξ u → reflEq (h₁ ξ u))

  _⁻¹Eq : ∀ {A w} → {a₁ a₂ : w ⊩ A}
                  → Eq a₁ a₂
                  → Eq a₂ a₁
  _⁻¹Eq {⎵}      (eq⎵ h) = eq⎵ (λ ξ → h ξ ⁻¹)
  _⁻¹Eq {A ⇒ B} (eq⊃ h) = eq⊃ (λ ξ u → h ξ u ⁻¹Eq)

  _⦙Eq_ : ∀ {A w} → {a₁ a₂ a₃ : w ⊩ A}
                  → Eq a₁ a₂ → Eq a₂ a₃
                  → Eq a₁ a₃
  _⦙Eq_ {⎵}      (eq⎵ h₁) (eq⎵ h₂) = eq⎵ (λ ξ → h₁ ξ ⦙ h₂ ξ)
  _⦙Eq_ {A ⇒ B} (eq⊃ h₁) (eq⊃ h₂) = eq⊃ (λ ξ u → h₁ ξ u ⦙Eq h₂ ξ u)

  ≡→Eq : ∀ {A w} → {a₁ a₂ : w ⊩ A}
                  → a₁ ≡ a₂ → Un a₁
                  → Eq a₁ a₂
  ≡→Eq refl u = reflEq u

  instance
    perEq : ∀ {A w} → PER (w ⊩ A) Eq
    perEq =
      record
        { _⁻¹ = _⁻¹Eq
        ; _⦙_ = _⦙Eq_
        }

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

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  -- (cong⟦∙⟧⟨_⟩Eq)
  postulate
    cong⟦∙⟧Eq : ∀ {A B w w′} → {f₁ f₂ : w ⊩ A ⇒ B} {a₁ a₂ : w′ ⊩ A}
                             → (ξ : w′ ⊒ w)
                             → Eq f₁ f₂ → Un f₁ → Un f₂
                             → Eq a₁ a₂ → Un a₁ → Un a₂
                             → Eq (f₁ ⟦∙⟧⟨ ξ ⟩ a₁)
                                   (f₂ ⟦∙⟧⟨ ξ ⟩ a₂)

  cong⟦∙⟧Un : ∀ {A B w w′} → {f : w ⊩ A ⇒ B} {a : w′ ⊩ A}
                           → (ξ : w′ ⊒ w) → Un f → Un a
                           → Un (f ⟦∙⟧⟨ ξ ⟩ a)
  cong⟦∙⟧Un ξ (un⊃ h₁ h₂ h₃) u = h₁ ξ u

  -- (cong↑⟨_⟩Eq)
  postulate
    congaccEq : ∀ {A w w′} → {a₁ a₂ : w ⊩ A}
                           → (ξ : w′ ⊒ w) → Eq a₁ a₂
                           → Eq (acc ξ a₁) (acc ξ a₂)

  -- (cong↑⟨_⟩𝒰)
  postulate
    congaccUn : ∀ {A w w′} → {a : w ⊩ A}
                           → (ξ : w′ ⊒ w) → Un a
                           → Un (acc ξ a)

  -- (aux₄₁₁)
  postulate
    lidaccEq : ∀ {A w} → {a : w ⊩ A}
                       → Un a
                       → Eq (acc idₐ a) a

  -- (aux₄₁₂)
  postulate
    acc◇Eq : ∀ {A w w′ w″} → {a : w ⊩ A}
                           → (ξ₁ : w″ ⊒ w′) (ξ₂ : w′ ⊒ w) → Un a
                           → Eq (acc (ξ₁ ◇ ξ₂) a)
                                 ((acc ξ₁ ∘ acc ξ₂) a)

  -- (aux₄₁₃)
  postulate
    acc⟦∙⟧idEq : ∀ {A B w w′} → {f : w ⊩ A ⇒ B} {a : w′ ⊩ A}
                              → (ξ : w′ ⊒ w) → Un f → Un a
                              → Eq (acc ξ f ⟦∙⟧⟨ idₐ ⟩ a)
                                    (f ⟦∙⟧⟨ ξ ⟩ a)

  acc⟦∙⟧Eq : ∀ {A B w w′ w″} → {f : w ⊩ A ⇒ B} {a : w′ ⊩ A}
                             → (ξ₁ : w′ ⊒ w) (ξ₂ : w″ ⊒ w′) → Un f → Un a
                             → Eq (acc ξ₁ f ⟦∙⟧⟨ ξ₂ ⟩ acc ξ₂ a)
                                   (acc ξ₂ (f ⟦∙⟧⟨ ξ₁ ⟩ a))
  acc⟦∙⟧Eq ξ₁ ξ₂ (un⊃ h₁ h₂ h₃) u = h₃ ξ₂ ξ₁ u ⁻¹

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

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  infix 3 _⊩⋆_
  data _⊩⋆_ : 𝒲 → 𝒞 → Set
    where
      ∅   : ∀ {w} → w ⊩⋆ ∅

      _,_ : ∀ {Ξ A w} → (ρ : w ⊩⋆ Ξ) (a : w ⊩ A) →
                         w ⊩⋆ Ξ , A

  -- ⟦putₛ⟧ can’t be stated here

  -- getᵥ = ⟦getₛ⟧ (lookup)
  getᵥ : ∀ {Ξ A w} → w ⊩⋆ Ξ → Ξ ∋ A → w ⊩ A
  getᵥ (ρ , a) zero    = a
  getᵥ (ρ , a) (suc i) = getᵥ ρ i

  -- unwkᵥ ≡ ⟦unwkₛ⟧
  unwkᵥ : ∀ {Ξ A w} → w ⊩⋆ Ξ , A → w ⊩⋆ Ξ
  unwkᵥ (ρ , a) = ρ

  -- ⟦wkₛ⟧ can’t be stated here
  -- ⟦liftₛ⟧ can’t be stated here
  -- ⟦idₛ⟧ can’t be stated here
  -- ⟦sub⟧ can’t be stated here
  -- ⟦cut⟧ can’t be stated here
  -- _◆_ can’t be stated here

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

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  -- (⟦_◑_⟧ / ↑⟨_⟩⊩⋆)
  _⬗_ : ∀ {Ξ w w′} → w′ ⊒ w → w ⊩⋆ Ξ → w′ ⊩⋆ Ξ
  ξ ⬗ ∅       = ∅
  ξ ⬗ (ρ , a) = ξ ⬗ ρ , acc ξ a

  -- (⟦_◐_⟧ / ↓⟨_⟩⊩⋆)
  _⬖_ : ∀ {Ξ Ξ′ w} → w ⊩⋆ Ξ′ → Ξ′ ∋⋆ Ξ → w ⊩⋆ Ξ
  ρ ⬖ ∅       = ∅
  ρ ⬖ (η , i) = ρ ⬖ η , getᵥ ρ i

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

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  zap⬖ : ∀ {Ξ Ξ′ A w} → (ρ : w ⊩⋆ Ξ′) (η : Ξ′ ∋⋆ Ξ) (a : w ⊩ A)
                      → (ρ , a) ⬖ wkᵣ η ≡ ρ ⬖ η
  zap⬖ ρ ∅       a = refl
  zap⬖ ρ (η , i) a = (_, getᵥ ρ i) & zap⬖ ρ η a

  rid⬖ : ∀ {Ξ w} → (ρ : w ⊩⋆ Ξ)
                 → ρ ⬖ idᵣ ≡ ρ
  rid⬖ ∅       = refl
  rid⬖ (ρ , a) = (_, a) & ( zap⬖ ρ idᵣ a
                          ⦙ rid⬖ ρ
                          )

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

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  get⬖ : ∀ {Ξ Ξ′ A w} → (ρ : w ⊩⋆ Ξ′) (η : Ξ′ ∋⋆ Ξ) (i : Ξ ∋ A)
                      → getᵥ (ρ ⬖ η) i ≡ (getᵥ ρ ∘ getᵣ η) i
  get⬖ ρ (η , j) zero    = refl
  get⬖ ρ (η , j) (suc i) = get⬖ ρ η i

  comp⬖○ : ∀ {Ξ Ξ′ Ξ″ w} → (ρ : w ⊩⋆ Ξ″) (η₁ : Ξ″ ∋⋆ Ξ′) (η₂ : Ξ′ ∋⋆ Ξ)
                         → ρ ⬖ (η₁ ○ η₂) ≡ (ρ ⬖ η₁) ⬖ η₂
  comp⬖○ σ η₁ ∅        = refl
  comp⬖○ σ η₁ (η₂ , i) = _,_ & comp⬖○ σ η₁ η₂
                             ⊗ (get⬖ σ η₁ i ⁻¹)

  -- wk⬖ can’t be stated here
  -- lift⬖ can’t be stated here
  -- wkrid⬖ can’t be stated here
  -- liftwkrid⬖ can’t be stated here
  -- sub⬖ can’t be stated here
  -- subwk⬖ can’t be stated here
  -- sublift⬖ can’t be stated here
  -- subliftwk⬖ can’t be stated here

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

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  data Eq⋆ : ∀ {Ξ w} → w ⊩⋆ Ξ → w ⊩⋆ Ξ → Set
    where
      ∅   : ∀ {w} → Eq⋆ (∅ {w}) ∅

      _,_ : ∀ {Ξ A w} → {ρ₁ ρ₂ : w ⊩⋆ Ξ} {a₁ a₂ : w ⊩ A}
                      → (χ : Eq⋆ ρ₁ ρ₂) (p : Eq a₁ a₂)
                      → Eq⋆ (ρ₁ , a₁) (ρ₂ , a₂)

  data Un⋆ : ∀ {Ξ w} → w ⊩⋆ Ξ → Set
    where
      ∅   : ∀ {w} → Un⋆ (∅ {w})

      _,_ : ∀ {Ξ A w} → {ρ : w ⊩⋆ Ξ} {a : w ⊩ A}
                      → (υ : Un⋆ ρ) (u : Un a)
                      → Un⋆ (ρ , a)

  reflEq⋆ : ∀ {Ξ w} → {ρ : w ⊩⋆ Ξ}
                    → Un⋆ ρ
                    → Eq⋆ ρ ρ
  reflEq⋆ ∅       = ∅
  reflEq⋆ (υ , u) = reflEq⋆ υ , reflEq u

  _⁻¹Eq⋆ : ∀ {Ξ w} → {ρ₁ ρ₂ : w ⊩⋆ Ξ}
                   → Eq⋆ ρ₁ ρ₂
                   → Eq⋆ ρ₂ ρ₁
  ∅       ⁻¹Eq⋆ = ∅
  (χ , p) ⁻¹Eq⋆ = χ ⁻¹Eq⋆ , p ⁻¹Eq

  _⦙Eq⋆_ : ∀ {Ξ w} → {ρ₁ ρ₂ ρ₃ : w ⊩⋆ Ξ}
                   → Eq⋆ ρ₁ ρ₂ → Eq⋆ ρ₂ ρ₃
                   → Eq⋆ ρ₁ ρ₃
  ∅        ⦙Eq⋆ ∅        = ∅
  (χ₁ , p) ⦙Eq⋆ (χ₂ , q) = χ₁ ⦙Eq⋆ χ₂ , p ⦙Eq q

  ≡→Eq⋆ : ∀ {Ξ w} → {ρ₁ ρ₂ : w ⊩⋆ Ξ}
                   → ρ₁ ≡ ρ₂ → Un⋆ ρ₁
                   → Eq⋆ ρ₁ ρ₂
  ≡→Eq⋆ refl υ = reflEq⋆ υ

  instance
    perEq⋆ : ∀ {Ξ w} → PER (w ⊩⋆ Ξ) Eq⋆
    perEq⋆ =
      record
        { _⁻¹ = _⁻¹Eq⋆
        ; _⦙_ = _⦙Eq⋆_
        }

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

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  -- (conglookupEq)
  postulate
    conggetEq : ∀ {Ξ A w} → {ρ₁ ρ₂ : w ⊩⋆ Ξ}
                          → (i : Ξ ∋ A) → Eq⋆ ρ₁ ρ₂
                          → Eq (getᵥ ρ₁ i) (getᵥ ρ₂ i)

  -- (cong↑⟨_⟩Eq⋆)
  postulate
    cong⬗Eq⋆ : ∀ {Ξ w w′} → {ρ₁ ρ₂ : w ⊩⋆ Ξ}
                          → (ξ : w′ ⊒ w) → Eq⋆ ρ₁ ρ₂
                          → Eq⋆ (ξ ⬗ ρ₁) (ξ ⬗ ρ₂)

  -- (cong↓⟨_⟩Eq⋆)
  postulate
    cong⬖Eq⋆ : ∀ {Ξ Ξ′ w} → {ρ₁ ρ₂ : w ⊩⋆ Ξ′}
                          → Eq⋆ ρ₁ ρ₂ → (η : Ξ′ ∋⋆ Ξ)
                          → Eq⋆ (ρ₁ ⬖ η) (ρ₂ ⬖ η)

  -- (conglookup𝒰)
  postulate
    conggetUn : ∀ {Ξ A w} → {ρ : w ⊩⋆ Ξ}
                          → (i : Ξ ∋ A) → Un⋆ ρ
                          → Un (getᵥ ρ i)

  -- (cong↑⟨_⟩𝒰⋆)
  postulate
    cong⬗Un⋆ : ∀ {Ξ w w′} → {ρ : w ⊩⋆ Ξ}
                          → (ξ : w′ ⊒ w) → Un⋆ ρ
                          → Un⋆ (ξ ⬗ ρ)

  -- (cong↓⟨_⟩𝒰⋆)
  postulate
    cong⬖Un⋆ : ∀ {Ξ Ξ′ w} → {ρ : w ⊩⋆ Ξ′}
                          → (η : Ξ′ ∋⋆ Ξ) → Un⋆ ρ
                          → Un⋆ (ρ ⬖ η)

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

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  -- (aux₄₂₁)
  postulate
    get⬖Eq : ∀ {Ξ Ξ′ A w} → {ρ : w ⊩⋆ Ξ′}
                          → (η : Ξ′ ∋⋆ Ξ) (i : Ξ′ ∋ A) (j : Ξ ∋ A) → Un⋆ ρ
                          → Eq (getᵥ (ρ ⬖ η) j)
                                (getᵥ ρ i)

  -- (conglookup↑⟨_⟩Eq)
  postulate
    get⬗Eq : ∀ {Ξ A w w′} → {ρ : w ⊩⋆ Ξ}
                          → (ξ : w′ ⊒ w) (i : Ξ ∋ A) → Un⋆ ρ
                          → Eq (getᵥ (ξ ⬗ ρ) i)
                                (acc ξ (getᵥ ρ i))

  -- (aux₄₂₃)
  postulate
    zap⬖Eq⋆ : ∀ {Ξ Ξ′ A w} → {ρ : w ⊩⋆ Ξ′} {a : w ⊩ A}
                           → (η₁ : Ξ′ , A ∋⋆ Ξ) (η₂ : Ξ′ ∋⋆ Ξ) → Un⋆ ρ
                           → Eq⋆ ((ρ , a) ⬖ η₁)
                                  (ρ ⬖ η₂)

  -- (aux₄₂₄)
  postulate
    rid⬖Eq⋆ : ∀ {Ξ w} → {ρ : w ⊩⋆ Ξ}
                      → Un⋆ ρ
                      → Eq⋆ (ρ ⬖ idᵣ) ρ

  -- (aux₄₂₅)
  postulate
    lid⬗Eq⋆ : ∀ {Ξ w} → {ρ : w ⊩⋆ Ξ}
                      → Un⋆ ρ
                      → Eq⋆ (idₐ ⬗ ρ) ρ

  -- (aux₄₂₆)
  postulate
    comp⬖○Eq⋆ : ∀ {Ξ Ξ′ Ξ″ w} → {ρ : w ⊩⋆ Ξ″}
                              → (η₁ : Ξ″ ∋⋆ Ξ′) (η₂ : Ξ′ ∋⋆ Ξ) → Un⋆ ρ
                              → Eq⋆ (ρ ⬖ (η₁ ○ η₂))
                                     ((ρ ⬖ η₁) ⬖ η₂)

  -- (aux₄₂₇)
  postulate
    comp⬗◇Eq⋆ : ∀ {Ξ w w′ w″} → {ρ : w ⊩⋆ Ξ}
                              → (ξ₁ : w″ ⊒ w′) (ξ₂ : w′ ⊒ w) → Un⋆ ρ
                              → Eq⋆ (ξ₁ ⬗ (ξ₂ ⬗ ρ))
                                     ((ξ₁ ◇ ξ₂) ⬗ ρ)

  -- (aux₄₂₈)
  postulate
    comp⬗⬖Eq⋆ : ∀ {Ξ Ξ′ w w′} → {ρ : w ⊩⋆ Ξ′}
                              → (ξ : w′ ⊒ w) (η : Ξ′ ∋⋆ Ξ) → Un⋆ ρ
                              → Eq⋆ (ξ ⬗ (ρ ⬖ η))
                                     ((ξ ⬗ ρ) ⬖ η)

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

module _ {{𝔪 : 𝔐}} where
  open 𝔐 𝔪

  ⟦_⟧ : ∀ {Ξ A w} → Ξ ⊢ A → w ⊩⋆ Ξ → w ⊩ A
  ⟦ 𝓋 i ⟧   ρ = getᵥ ρ i
  ⟦ ƛ M ⟧   ρ = ⟦ƛ⟧ (λ ξ a → ⟦ M ⟧ (ξ ⬗ ρ , a))
  ⟦ M ∙ N ⟧ ρ = ⟦ M ⟧ ρ ⟦∙⟧⟨ idₐ ⟩ ⟦ N ⟧ ρ

  ⟦_⟧⋆ : ∀ {Ξ Φ w} → Ξ ⊢⋆ Φ → w ⊩⋆ Ξ → w ⊩⋆ Φ
  ⟦ ∅ ⟧⋆     ρ = ∅
  ⟦ σ , M ⟧⋆ ρ = ⟦ σ ⟧⋆ ρ , ⟦ M ⟧ ρ

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

instance
  canon : 𝔐
  canon = record
    { 𝒲      = 𝒞
    ; 𝒢      = _⊢ ⎵
    ; _⊒_    = _∋⋆_
    ; idₐ    = idᵣ
    ; _◇_    = _○_
    ; lid◇   = lid○
    ; rid◇   = rid○
    ; assoc◇ = assoc○
    }

mutual
  reify : ∀ {A Γ} → Γ ⊩ A → Γ ⊢ A
  reify {⎵}      f = ⟦g⟧⟨ idᵣ ⟩ f
  reify {A ⇒ B} f = ƛ (reify (f ⟦∙⟧⟨ wkᵣ idᵣ ⟩ ⟪𝓋 0 ⟫))

  ⟪_⟫ : ∀ {A Γ} → (∀ {Γ′} → Γ′ ∋⋆ Γ → Γ′ ⊢ A) → Γ ⊩ A
  ⟪_⟫ {⎵}      f = ⟦G⟧ (λ η   → f η)
  ⟪_⟫ {A ⇒ B} f = ⟦ƛ⟧ (λ η a → ⟪ (λ η′ → f (η′ ○ η) ∙ reify (acc η′ a)) ⟫)

  ⟪𝓋_⟫ : ∀ {Γ A} → Γ ∋ A → Γ ⊩ A
  ⟪𝓋 i ⟫ = ⟪ (λ η → ren η (𝓋 i)) ⟫

aux₄₄₁ : ∀ {A Γ} → (f₁ f₂ : ∀ {Γ′} → Γ′ ∋⋆ Γ → Γ′ ⊢ A)
                 → (∀ {Γ′} → (η : Γ′ ∋⋆ Γ) → f₁ η ≡ f₂ η)
                 → Eq (⟪ f₁ ⟫) (⟪ f₂ ⟫)
aux₄₄₁ {⎵}      f₁ f₂ h = eq⎵ (λ η → h η)
aux₄₄₁ {A ⇒ B} f₁ f₂ h =
  eq⊃ (λ η′ {a} u →
    aux₄₄₁ (λ η″ → f₁ (η″ ○ η′) ∙ reify (acc η″ a))
           (λ η″ → f₂ (η″ ○ η′) ∙ reify (acc η″ a))
           (λ η″ → (_∙ reify (acc η″ a)) & h (η″ ○ η′)))

aux₄₄₂ : ∀ {A Γ Γ′} → (η : Γ′ ∋⋆ Γ) (f : (∀ {Γ′} → Γ′ ∋⋆ Γ → Γ′ ⊢ A))
                    → Eq (acc η ⟪ f ⟫) (⟪ (λ η′ → f (η′ ○ η)) ⟫)
aux₄₄₂ {⎵}      η f = eq⎵ (λ η′ → f & refl)
aux₄₄₂ {A ⇒ B} η f =
  eq⊃ (λ η′ {a} u →
    aux₄₄₁ (λ η″ → f (η″ ○ (η′ ○ η)) ∙ reify (acc η″ a))
           (λ η″ → f ((η″ ○ η′) ○ η) ∙ reify (acc η″ a))
           (λ η″ → (_∙ reify (acc η″ a)) & (f & assoc○ η″ η′ η)))

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

-- Theorem 1.
mutual
  thm₁ : ∀ {Γ A} → {a₁ a₂ : Γ ⊩ A}
                 → Eq a₁ a₂
                 → reify a₁ ≡ reify a₂
  thm₁ (eq⎵ h) = h idᵣ
  thm₁ (eq⊃ h) = ƛ & thm₁ (h (wkᵣ idᵣ) ⟪𝓋 0 ⟫ᵤ)

  ⟪𝓋_⟫ᵤ : ∀ {Γ A} → (i : Γ ∋ A)
                  → Un (⟪𝓋 i ⟫)
  ⟪𝓋 i ⟫ᵤ = aux₄₄₃ (λ η → 𝓋 (getᵣ η i))

  aux₄₄₃ : ∀ {A Γ} → (f : ∀ {Γ′} → Γ′ ∋⋆ Γ → Γ′ ⊢ A)
                   → Un (⟪ f ⟫)
  aux₄₄₃ {⎵}      f = un⎵
  aux₄₄₃ {A ⇒ B} f =
    un⊃ (λ η {a} u →
          aux₄₄₃ (λ η′ → f (η′ ○ η) ∙ reify (acc η′ a)))
        (λ η {a₁} {a₂} p u₁ u₂ →
          aux₄₄₁ (λ η′ → f (η′ ○ η) ∙ reify (acc η′ a₁))
                 (λ η′ → f (η′ ○ η) ∙ reify (acc η′ a₂))
                 (λ η′ → (f (η′ ○ η) ∙_) & thm₁ (congaccEq η′ p)))
        (λ η₁ η₂ {a} u →
          aux₄₄₂ η₁ (λ η′ → f (η′ ○ η₂) ∙ reify (acc η′ a))
        ⦙ aux₄₄₁ (λ η′ → f ((η′ ○ η₁) ○ η₂) ∙ reify (acc (η′ ○ η₁) a))
                 (λ η′ → f (η′ ○ (η₁ ○ η₂)) ∙ reify (acc η′ (acc η₁ a)))
                 (λ η′ → _∙_ & (f & assoc○ η′ η₁ η₂ ⁻¹)
                              ⊗ thm₁ (acc◇Eq η′ η₁ u)))

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

⌊_⌋ᵥ : ∀ {Γ Γ′} → Γ′ ∋⋆ Γ → Γ′ ⊩⋆ Γ
⌊ ∅ ⌋ᵥ     = ∅
⌊ η , i ⌋ᵥ = ⌊ η ⌋ᵥ , ⟪𝓋 i ⟫

idᵥ : ∀ {Γ} → Γ ⊩⋆ Γ
idᵥ = ⌊ idᵣ ⌋ᵥ

nf : ∀ {Γ A} → Γ ⊢ A → Γ ⊢ A
nf M = reify (⟦ M ⟧ idᵥ)

-- Corollary 1.
cor₁ : ∀ {Γ A} → (M₁ M₂ : Γ ⊢ A) → Eq (⟦ M₁ ⟧ idᵥ) (⟦ M₂ ⟧ idᵥ)
               → nf M₁ ≡ nf M₂
cor₁ M₁ M₂ = thm₁

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

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
module Haskell.RangedSets.Boundaries where

open import Agda.Builtin.Nat as Nat hiding (_==_; _<_; _+_; _-_)
open import Agda.Builtin.Char
open import Agda.Builtin.Int using (pos; negsuc)

open import Haskell.Prim
open import Haskell.Prim.Ord
open import Haskell.Prim.Bool
open import Haskell.Prim.Char
open import Haskell.Prim.Maybe
open import Haskell.Prim.Enum
open import Haskell.Prim.Num
open import Haskell.Prim.Eq
open import Haskell.Prim.Functor
open import Haskell.Prim.Monoid
open import Haskell.Prim.Monad
open import Haskell.Prim.Applicative
open import Haskell.Prim.Int
open import Haskell.Prim.List
open import Haskell.Prim.Integer
open import Haskell.Prim.Real
open import Haskell.Prim.Tuple
open import Haskell.Prim.Double
open import Haskell.Prim.Bounded

open import Agda.Builtin.Char

{-# FOREIGN AGDA2HS
import Data.Ratio
#-}

record DiscreteOrdered (a : Set) ⦃ _ : Ord a ⦄ : Set where
    field
        adjacent : a → a → Bool
        adjacentBelow : a → Maybe a

open DiscreteOrdered ⦃ ... ⦄ public
{-# COMPILE AGDA2HS DiscreteOrdered class #-}

orderingFromInt : Int → Ordering
orderingFromInt n = if_then_else_ (n == 0) LT (if_then_else_ (n == 1) EQ GT)
{-# COMPILE AGDA2HS orderingFromInt #-}

boundedAdjacentBool : (x y : Bool) → Bool
boundedAdjacentBool x y = if_then_else_ (x < y) true false
{-# COMPILE AGDA2HS boundedAdjacentBool #-}

boundedBelowBool : (x : Bool) → Maybe Bool
boundedBelowBool x = if_then_else_ (x == false) Nothing (Just false)
{-# COMPILE AGDA2HS boundedBelowBool #-}

boundedAdjacentOrdering : (x y : Ordering) → Bool
boundedAdjacentOrdering x y = if_then_else_ (x < y && x < GT) ((fromEnum x) + 1 == (fromEnum y)) false
{-# COMPILE AGDA2HS boundedAdjacentOrdering #-}

boundedBelowOrdering : (x : Ordering) → Maybe Ordering
boundedBelowOrdering x = if_then_else_ (x == LT) Nothing (Just (orderingFromInt ((fromEnum x) - 1)))
{-# COMPILE AGDA2HS boundedBelowOrdering #-}

boundedAdjacentChar : (x y : Char) → Bool
boundedAdjacentChar x y = if_then_else_ (x < y && x /= '\1114111') (((fromEnum x) + 1) == fromEnum y) false
{-# COMPILE AGDA2HS boundedAdjacentChar #-}

boundedBelowChar : (x : Char) → Maybe Char
boundedBelowChar x = if_then_else_ (x == '\0') Nothing (Just (chr ((ord x) - 1)))
{-# COMPILE AGDA2HS boundedBelowChar #-}

boundedAdjacentInt : (x y : Int) → Bool
boundedAdjacentInt x y = if_then_else_ (x < y && x /= 9223372036854775807) (x + 1 == y) false
{-# COMPILE AGDA2HS boundedAdjacentInt #-}

boundedBelowInt : (x : Int) → Maybe Int
boundedBelowInt x = if_then_else_ (x == -9223372036854775808) Nothing (Just (x - 1))
{-# COMPILE AGDA2HS boundedBelowInt #-}

boundedAdjacentInteger : (x y : Integer) → Bool
boundedAdjacentInteger x y = ((fromEnum x) + 1 == (fromEnum y))
{-# COMPILE AGDA2HS boundedAdjacentInteger #-}

boundedBelowInteger : (x : Integer) → Maybe Integer
boundedBelowInteger x = Just (x - (toInteger 1))
{-# COMPILE AGDA2HS boundedBelowInteger #-}

constructTuple : ⦃ o : Ord a ⦄ → ⦃ o2 : Ord b ⦄ → ⦃ DiscreteOrdered b ⦃ o2 ⦄ ⦄ → a → Maybe b → Maybe (a × b)
constructTuple _ Nothing = Nothing
constructTuple a (Just value) = Just (a , value)
{-# COMPILE AGDA2HS constructTuple #-}

constructTriple : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ o : Ord c ⦄ → ⦃ DiscreteOrdered c ⦃ o ⦄ ⦄ → a → b → Maybe c → Maybe (a × b × c)
constructTriple _ _ Nothing = Nothing
constructTriple a b (Just value) = Just (a , b , value)
{-# COMPILE AGDA2HS constructTriple #-}

constructQuadtruple : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄ → ⦃ o : Ord d ⦄ → ⦃ DiscreteOrdered d ⦃ o ⦄ ⦄
                        → a → b → c → Maybe d → Maybe (Tuple (a ∷ b ∷ c ∷ d ∷ []))
constructQuadtruple _ _ _ Nothing = Nothing
constructQuadtruple a b c (Just value) = Just (a ∷ b ∷ c ∷ value ∷ [])
{-# COMPILE AGDA2HS constructQuadtruple #-}

instance
    isDiscreteOrderedBool : DiscreteOrdered Bool
    isDiscreteOrderedBool . adjacent = boundedAdjacentBool
    isDiscreteOrderedBool . adjacentBelow = boundedBelowBool
{-# COMPILE AGDA2HS isDiscreteOrderedBool #-}

instance
    isDiscreteOrderedOrdering : DiscreteOrdered Ordering
    isDiscreteOrderedOrdering . adjacent = boundedAdjacentOrdering
    isDiscreteOrderedOrdering . adjacentBelow = boundedBelowOrdering
{-# COMPILE AGDA2HS isDiscreteOrderedOrdering #-}

instance
    isDiscreteOrderedChar : DiscreteOrdered Char
    isDiscreteOrderedChar . adjacent = boundedAdjacentChar
    isDiscreteOrderedChar . adjacentBelow = boundedBelowChar
{-# COMPILE AGDA2HS isDiscreteOrderedChar #-}

instance
    isDiscreteOrderedInt : DiscreteOrdered Int
    isDiscreteOrderedInt . adjacent = boundedAdjacentInt
    isDiscreteOrderedInt . adjacentBelow = boundedBelowInt
{-# COMPILE AGDA2HS isDiscreteOrderedInt #-}

instance
    isDiscreteOrderedInteger : DiscreteOrdered Integer
    isDiscreteOrderedInteger . adjacent = boundedAdjacentInteger
    isDiscreteOrderedInteger . adjacentBelow = boundedBelowInteger
{-# COMPILE AGDA2HS isDiscreteOrderedInteger #-}

instance
    isDiscreteOrderedDouble : DiscreteOrdered Double
    isDiscreteOrderedDouble . adjacent x y = false
    isDiscreteOrderedDouble . adjacentBelow x = Nothing
{-# COMPILE AGDA2HS isDiscreteOrderedDouble #-}

instance
    isDiscreteOrderedList : ⦃ o : Ord a ⦄ → ⦃ ol : Ord (List a) ⦄ → DiscreteOrdered (List a) ⦃ ol ⦄
    isDiscreteOrderedList . adjacent x y = false
    isDiscreteOrderedList . adjacentBelow x = Nothing
{-# COMPILE AGDA2HS isDiscreteOrderedList #-}

instance
    isDiscreteOrderedRatio : ⦃ o : Ord a ⦄ → ⦃ Integral a ⦄ → ⦃ or : Ord (Ratio a )⦄ → DiscreteOrdered (Ratio a) ⦃ or ⦄
    isDiscreteOrderedRatio . adjacent x y = false
    isDiscreteOrderedRatio . adjacentBelow x = Nothing
{-# COMPILE AGDA2HS isDiscreteOrderedRatio #-}

instance
    isDiscreteOrderedTuple : ⦃ Ord a ⦄ → ⦃ o : Ord b ⦄ → ⦃ DiscreteOrdered b ⦃ o ⦄ ⦄
                            →  ⦃ ot : Ord (a × b) ⦄ → DiscreteOrdered (a × b) ⦃ ot ⦄
    isDiscreteOrderedTuple . adjacent (x1 , x2) (y1 , y2) = (x1 == y1) && (adjacent x2 y2)
    isDiscreteOrderedTuple . adjacentBelow (x1 , x2) = constructTuple x1 (adjacentBelow x2)
{-# COMPILE AGDA2HS isDiscreteOrderedTuple #-}

instance
    isDiscreteOrderedTriple : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ o : Ord c ⦄ → ⦃ DiscreteOrdered c ⦃ o ⦄ ⦄
                                → ⦃ ot : Ord (a × b × c) ⦄ → DiscreteOrdered (a × b × c) ⦃ ot ⦄
    isDiscreteOrderedTriple . adjacent (x1 , x2 , x3) (y1 , y2 , y3) = (x1 == y1) && (x2 == y2) && (adjacent x3 y3)
    isDiscreteOrderedTriple . adjacentBelow (x1 , x2 , x3) = constructTriple x1 x2 (adjacentBelow x3)
{-# COMPILE AGDA2HS isDiscreteOrderedTriple #-}

instance
    isDiscreteOrderedQuadtruple : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄
                            → ⦃ o : Ord d ⦄ → ⦃ DiscreteOrdered d ⦃ o ⦄ ⦄
                            → ⦃ ot : Ord (Tuple (a ∷ b ∷ c ∷ d ∷ [])) ⦄ → DiscreteOrdered (Tuple (a ∷ b ∷ c ∷ d ∷ [])) ⦃ ot ⦄
    isDiscreteOrderedQuadtruple . adjacent (x1 ∷ x2 ∷ x3 ∷ x4 ∷ []) (y1 ∷ y2 ∷ y3 ∷ y4 ∷ []) = (x1 == y1) && (x2 == y2) && (x3 == y3) && (adjacent x4 y4)
    isDiscreteOrderedQuadtruple . adjacentBelow (x1 ∷ x2 ∷ x3 ∷ x4 ∷ []) = constructQuadtruple x1 x2 x3 (adjacentBelow x4)
{-# COMPILE AGDA2HS isDiscreteOrderedQuadtruple #-}

data Boundary (a : Set) ⦃ b : Ord a ⦄ ⦃ _ : DiscreteOrdered a ⦃ b ⦄ ⦄ : Set where
    BoundaryAbove    : a → Boundary a
    BoundaryBelow    : a → Boundary a
    BoundaryAboveAll : Boundary a
    BoundaryBelowAll : Boundary a

{-# COMPILE AGDA2HS Boundary #-}

above : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
        → Boundary a ⦃ o ⦄ → a → Bool
above (BoundaryAbove b) a    = a > b
above (BoundaryBelow b) a    = a >= b
above BoundaryAboveAll _     = false
above BoundaryBelowAll _     = true
{-# COMPILE AGDA2HS above #-}

infixr 4 _/>/_
_/>/_ : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
    → a → Boundary a ⦃ o ⦄ → Bool
_/>/_ x (BoundaryAbove b) = x > b
_/>/_ x (BoundaryBelow b) = x >= b
_/>/_ _ BoundaryAboveAll = false
_/>/_ _ BoundaryBelowAll = true
{-# COMPILE AGDA2HS _/>/_ #-}

instance
    isBoundaryEq : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → Eq (Boundary a)
    isBoundaryEq . _==_ (BoundaryAbove b1) (BoundaryAbove b2) = (b1 == b2)
    isBoundaryEq . _==_ (BoundaryAbove b1) (BoundaryBelow b2) = if_then_else_ (b1 < b2 && (adjacent b1 b2)) true false
    isBoundaryEq . _==_ (BoundaryBelow b1) (BoundaryBelow b2) = (b1 == b2)
    isBoundaryEq . _==_ (BoundaryBelow b1) (BoundaryAbove b2) = if_then_else_ (b1 > b2 && (adjacent b2 b1)) true false
    isBoundaryEq . _==_ BoundaryAboveAll BoundaryAboveAll = true
    isBoundaryEq . _==_ BoundaryBelowAll BoundaryBelowAll = true
    isBoundaryEq . _==_ _ _ = false
{-# COMPILE AGDA2HS isBoundaryEq #-}

instance
    isBoundaryOrd : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → Ord (Boundary a)
    isBoundaryOrd . compare (BoundaryAbove b1) (BoundaryAbove b2) = compare b1 b2
    isBoundaryOrd . compare (BoundaryAbove b1) (BoundaryBelow b2) = if_then_else_ (b1 < b2) (if_then_else_ (adjacent b1 b2) EQ LT) GT
    isBoundaryOrd . compare (BoundaryAbove b1) BoundaryAboveAll = LT
    isBoundaryOrd . compare (BoundaryAbove b1) BoundaryBelowAll = GT
    isBoundaryOrd . compare (BoundaryBelow b1) (BoundaryBelow b2) = compare b1 b2
    isBoundaryOrd . compare (BoundaryBelow b1) (BoundaryAbove b2) = if_then_else_ (b1 > b2) (if_then_else_ (adjacent b2 b1) EQ GT) LT
    isBoundaryOrd . compare (BoundaryBelow b1) BoundaryAboveAll = LT
    isBoundaryOrd . compare (BoundaryBelow b1) BoundaryBelowAll = GT
    isBoundaryOrd . compare BoundaryAboveAll BoundaryAboveAll = EQ
    isBoundaryOrd . compare BoundaryAboveAll _ = GT
    isBoundaryOrd . compare BoundaryBelowAll BoundaryBelowAll = EQ
    isBoundaryOrd . compare BoundaryBelowAll _ = LT
    isBoundaryOrd ._<_ x y = compare x y == LT
    isBoundaryOrd ._>_ x y = compare x y == GT
    isBoundaryOrd ._<=_ x BoundaryAboveAll = true
    isBoundaryOrd ._<=_ BoundaryBelowAll y = true
    isBoundaryOrd ._<=_ x y = (compare x y == LT) || (compare x y == EQ)
    isBoundaryOrd ._>=_ x y = (compare x y == GT) || (compare x y == EQ)
    isBoundaryOrd .max x y = if (compare x y == GT) then x else y
    isBoundaryOrd .min x y = if (compare x y == LT) then x else y
{-# COMPILE AGDA2HS isBoundaryOrd #-}


text:
open import Prelude

module Implicits.Resolution.Termination.Lemmas.Stack
  where

open import Induction.WellFounded
open import Induction.Nat
open import Data.Fin.Substitution
open import Implicits.Syntax
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas
open import Data.Nat hiding (_<_)
open import Data.Nat.Properties

open import Implicits.Resolution.Termination.SizeMeasures
open import Implicits.Resolution.Termination.Stack

open import Data.Nat.Base
+k<+k : ∀ {n m} k → n N< m → k N+ n N< k N+ m
+k<+k zero p = p
+k<+k (suc k) p = s≤s (+k<+k k p)

+k<+k' : ∀ {n m} k → n N< m → n N+ k N< m N+ k
+k<+k' {n} {m} k p = subst₂ (λ u v → u N< v) (+-comm k n) (+-comm k m) (+k<+k k p)
  where open import Data.Nat.Properties.Simple

-k<-k : ∀ {n m} k → k N+ n N< k N+ m → n < m
-k<-k zero x = x
-k<-k (suc k) (s≤s x) = -k<-k k x

-k<-k' : ∀ {n m} k → n N+ k N< m N+ k → n < m
-k<-k' {n} {m} k p = -k<-k k (subst₂ _N<_ (+-comm n k) (+-comm m k) p)
  where open import Data.Nat.Properties.Simple

----------------------------------------------------------------
-- stack properties

push< : ∀ {ν r a} {Δ : ICtx ν} (s : Stack Δ) (r∈Δ : r List.∈ Δ) →
        (, a) ρ< (, s get r∈Δ) → (s push a for r∈Δ) s< s
push< (b All.∷ s) (here _) a<b = +k<+k' (ssum s) a<b
push< (b All.∷ s) (there r∈Δ) p = +k<+k h|| b || (push< s r∈Δ p)

push≮ : ∀ {ν r a} {Δ : ICtx ν} (s : Stack Δ) (r∈Δ : r List.∈ Δ) →
        ¬ ((, a) ρ< (, s get r∈Δ)) → ¬ (s push a for r∈Δ) s< s
push≮ (b All.∷ s) (here _) ¬a<b = λ x → ¬a<b (-k<-k' (ssum s) x)
push≮ (b All.∷ s) (there r∈Δ) ¬a<b = λ x → push≮ s r∈Δ ¬a<b (-k<-k h|| b || x)

----------------------------------------------------------------
-- a type dominates a stack if pushing it to the stack makes the stack bigger

_for_?⊬dom_ : ∀ {ν r} {Δ : ICtx ν} → (a : Type ν) → (r∈Δ : r List.∈ Δ) → (s : Stack Δ) →
               Dec (a for r∈Δ ⊬dom s)
a for r∈Δ ?⊬dom s with (, a) ρ<? (, s get r∈Δ)
a for r∈Δ ?⊬dom s | yes p = yes (push< s r∈Δ p)
a for r∈Δ ?⊬dom s | no ¬p = no (push≮ s r∈Δ ¬p)

-- we also show that the ordering on stacks is well founded
s<-well-founded : ∀ {ν} {Δ : ICtx ν} → Well-founded (_s<_ {ν} {Δ})
s<-well-founded = sub.well-founded (image.well-founded <-well-founded)
  where
    open import Data.Nat.Base
    open import Data.Nat.Properties
    module sub = Inverse-image (λ{ s → ssum s})
    module image = Subrelation {A = ℕ} {_N<_} {_<′_} ≤⇒≤′

{-}
-- we can show that our strict size measure a ρ< b is well founded
-- by relating it to the well-foundedness proof of _<'_
sρ<-well-founded : Well-founded _sρ<_
sρ<-well-founded = sub.well-founded (image.well-founded <-well-founded)
  where
    module sub = Inverse-image (λ{ (_ , a) → || a ||})
    module image = Subrelation {A = ℕ} {_N<_} {_<′_} ≤⇒≤′
-}


text:
module Issue555c where

import Common.Level

record R {a} (A : Set a) : Set

record R A where
  field f : A

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------------
-- Inductive PA properties using the induction principle
------------------------------------------------------------------------------

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

module PA.Inductive.PropertiesByInductionATP where

open import PA.Inductive.Base
open import PA.Inductive.PropertiesByInduction

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

+-comm : ∀ m n → m + n ≡ n + m
+-comm m n = ℕ-ind A A0 is m
  where
  A : ℕ → Set
  A i = i + n ≡ n + i
  {-# ATP definition A #-}

  A0 : A zero
  A0 = sym (+-rightIdentity n)

  postulate is : ∀ i → A i → A (succ i)
  -- TODO (21 November 2014). See Apia issue 16
  -- {-# ATP prove is x+Sy≡S[x+y] #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise sum
------------------------------------------------------------------------

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

module Data.Sum.Relation.Binary.Pointwise where

open import Data.Product using (_,_)
open import Data.Sum as Sum
open import Data.Sum.Properties
open import Level using (_⊔_)
open import Function using (_∘_; id)
open import Function.Inverse using (Inverse)
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

----------------------------------------------------------------------
-- Definition

data Pointwise {a b c d r s}
               {A : Set a} {B : Set b} {C : Set c} {D : Set d}
               (R : REL A C r) (S : REL B D s)
               : REL (A ⊎ B) (C ⊎ D) (a ⊔ b ⊔ c ⊔ d ⊔ r ⊔ s) where
  inj₁ : ∀ {a c} → R a c → Pointwise R S (inj₁ a) (inj₁ c)
  inj₂ : ∀ {b d} → S b d → Pointwise R S (inj₂ b) (inj₂ d)

----------------------------------------------------------------------
-- Relational properties

module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂}
         {∼₁ : Rel A₁ ℓ₁} {∼₂ : Rel A₂ ℓ₂}
         where

  drop-inj₁ : ∀ {x y} → Pointwise ∼₁ ∼₂ (inj₁ x) (inj₁ y) → ∼₁ x y
  drop-inj₁ (inj₁ x) = x

  drop-inj₂ : ∀ {x y} → Pointwise ∼₁ ∼₂ (inj₂ x) (inj₂ y) → ∼₂ x y
  drop-inj₂ (inj₂ x) = x

  ⊎-refl : Reflexive ∼₁ → Reflexive ∼₂ →
           Reflexive (Pointwise ∼₁ ∼₂)
  ⊎-refl refl₁ refl₂ {inj₁ x} = inj₁ refl₁
  ⊎-refl refl₁ refl₂ {inj₂ y} = inj₂ refl₂

  ⊎-symmetric : Symmetric ∼₁ → Symmetric ∼₂ →
                Symmetric (Pointwise ∼₁ ∼₂)
  ⊎-symmetric sym₁ sym₂ (inj₁ x) = inj₁ (sym₁ x)
  ⊎-symmetric sym₁ sym₂ (inj₂ x) = inj₂ (sym₂ x)

  ⊎-transitive : Transitive ∼₁ → Transitive ∼₂ →
                 Transitive (Pointwise ∼₁ ∼₂)
  ⊎-transitive trans₁ trans₂ (inj₁ x) (inj₁ y) = inj₁ (trans₁ x y)
  ⊎-transitive trans₁ trans₂ (inj₂ x) (inj₂ y) = inj₂ (trans₂ x y)

  ⊎-asymmetric : Asymmetric ∼₁ → Asymmetric ∼₂ →
                 Asymmetric (Pointwise ∼₁ ∼₂)
  ⊎-asymmetric asym₁ asym₂ (inj₁ x) = λ { (inj₁ y) → asym₁ x y }
  ⊎-asymmetric asym₁ asym₂ (inj₂ x) = λ { (inj₂ y) → asym₂ x y }

  ⊎-substitutive : ∀ {ℓ₃} → Substitutive ∼₁ ℓ₃ → Substitutive ∼₂ ℓ₃ →
                   Substitutive (Pointwise ∼₁ ∼₂) ℓ₃
  ⊎-substitutive subst₁ subst₂ P (inj₁ x) = subst₁ (P ∘ inj₁) x
  ⊎-substitutive subst₁ subst₂ P (inj₂ x) = subst₂ (P ∘ inj₂) x

  ⊎-decidable : Decidable ∼₁ → Decidable ∼₂ →
                Decidable (Pointwise ∼₁ ∼₂)
  ⊎-decidable _≟₁_ _≟₂_ (inj₁ x) (inj₁ y) = Dec.map′ inj₁ drop-inj₁ (x ≟₁ y)
  ⊎-decidable _≟₁_ _≟₂_ (inj₁ x) (inj₂ y) = no λ()
  ⊎-decidable _≟₁_ _≟₂_ (inj₂ x) (inj₁ y) = no λ()
  ⊎-decidable _≟₁_ _≟₂_ (inj₂ x) (inj₂ y) = Dec.map′ inj₂ drop-inj₂ (x ≟₂ y)

module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
         {ℓ₁ ℓ₂} {∼₁ : Rel A₁ ℓ₁} {≈₁ : Rel A₁ ℓ₂}
         {ℓ₃ ℓ₄} {∼₂ : Rel A₂ ℓ₃} {≈₂ : Rel A₂ ℓ₄} where

  ⊎-reflexive : ≈₁ ⇒ ∼₁ → ≈₂ ⇒ ∼₂ →
                (Pointwise ≈₁ ≈₂) ⇒ (Pointwise ∼₁ ∼₂)
  ⊎-reflexive refl₁ refl₂ (inj₁ x) = inj₁ (refl₁ x)
  ⊎-reflexive refl₁ refl₂ (inj₂ x) = inj₂ (refl₂ x)

  ⊎-irreflexive : Irreflexive ≈₁ ∼₁ → Irreflexive ≈₂ ∼₂ →
                  Irreflexive (Pointwise ≈₁ ≈₂) (Pointwise ∼₁ ∼₂)
  ⊎-irreflexive irrefl₁ irrefl₂ (inj₁ x) (inj₁ y) = irrefl₁ x y
  ⊎-irreflexive irrefl₁ irrefl₂ (inj₂ x) (inj₂ y) = irrefl₂ x y

  ⊎-antisymmetric : Antisymmetric ≈₁ ∼₁ → Antisymmetric ≈₂ ∼₂ →
                    Antisymmetric (Pointwise ≈₁ ≈₂) (Pointwise ∼₁ ∼₂)
  ⊎-antisymmetric antisym₁ antisym₂ (inj₁ x) (inj₁ y) = inj₁ (antisym₁ x y)
  ⊎-antisymmetric antisym₁ antisym₂ (inj₂ x) (inj₂ y) = inj₂ (antisym₂ x y)

  ⊎-respectsˡ : ∼₁ Respectsˡ ≈₁ → ∼₂ Respectsˡ ≈₂ →
                (Pointwise ∼₁ ∼₂) Respectsˡ (Pointwise ≈₁ ≈₂)
  ⊎-respectsˡ resp₁ resp₂ (inj₁ x) (inj₁ y) = inj₁ (resp₁ x y)
  ⊎-respectsˡ resp₁ resp₂ (inj₂ x) (inj₂ y) = inj₂ (resp₂ x y)

  ⊎-respectsʳ : ∼₁ Respectsʳ ≈₁ → ∼₂ Respectsʳ ≈₂ →
                (Pointwise ∼₁ ∼₂) Respectsʳ (Pointwise ≈₁ ≈₂)
  ⊎-respectsʳ resp₁ resp₂ (inj₁ x) (inj₁ y) = inj₁ (resp₁ x y)
  ⊎-respectsʳ resp₁ resp₂ (inj₂ x) (inj₂ y) = inj₂ (resp₂ x y)

  ⊎-respects₂ : ∼₁ Respects₂ ≈₁ → ∼₂ Respects₂ ≈₂ →
                (Pointwise ∼₁ ∼₂) Respects₂ (Pointwise ≈₁ ≈₂)
  ⊎-respects₂ (r₁ , l₁) (r₂ , l₂) = ⊎-respectsʳ r₁ r₂ , ⊎-respectsˡ l₁ l₂

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

module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
         {ℓ₁ ℓ₂} {≈₁ : Rel A₁ ℓ₁} {≈₂ : Rel A₂ ℓ₂}
         where

  ⊎-isEquivalence : IsEquivalence ≈₁ → IsEquivalence ≈₂ →
                    IsEquivalence (Pointwise ≈₁ ≈₂)
  ⊎-isEquivalence eq₁ eq₂ = record
    { refl  = ⊎-refl       (refl  eq₁) (refl  eq₂)
    ; sym   = ⊎-symmetric  (sym   eq₁) (sym   eq₂)
    ; trans = ⊎-transitive (trans eq₁) (trans eq₂)
    }
    where open IsEquivalence

  ⊎-isDecEquivalence : IsDecEquivalence ≈₁ → IsDecEquivalence ≈₂ →
                       IsDecEquivalence (Pointwise ≈₁ ≈₂)
  ⊎-isDecEquivalence eq₁ eq₂ = record
    { isEquivalence =
        ⊎-isEquivalence (isEquivalence eq₁) (isEquivalence eq₂)
    ; _≟_           = ⊎-decidable (_≟_ eq₁) (_≟_ eq₂)
    }
    where open IsDecEquivalence

module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
         {ℓ₁ ℓ₂} {≈₁ : Rel A₁ ℓ₁} {∼₁ : Rel A₁ ℓ₂}
         {ℓ₃ ℓ₄} {≈₂ : Rel A₂ ℓ₃} {∼₂ : Rel A₂ ℓ₄} where

  ⊎-isPreorder : IsPreorder ≈₁ ∼₁ → IsPreorder ≈₂ ∼₂ →
                 IsPreorder (Pointwise ≈₁ ≈₂) (Pointwise ∼₁ ∼₂)
  ⊎-isPreorder pre₁ pre₂ = record
    { isEquivalence =
        ⊎-isEquivalence (isEquivalence pre₁) (isEquivalence pre₂)
    ; reflexive     = ⊎-reflexive (reflexive pre₁) (reflexive pre₂)
    ; trans         = ⊎-transitive (trans pre₁) (trans pre₂)
    }
    where open IsPreorder

  ⊎-isPartialOrder : IsPartialOrder ≈₁ ∼₁ →
                     IsPartialOrder ≈₂ ∼₂ →
                     IsPartialOrder
                       (Pointwise ≈₁ ≈₂) (Pointwise ∼₁ ∼₂)
  ⊎-isPartialOrder po₁ po₂ = record
    { isPreorder = ⊎-isPreorder (isPreorder po₁) (isPreorder po₂)
    ; antisym    = ⊎-antisymmetric (antisym po₁) (antisym    po₂)
    }
    where open IsPartialOrder

  ⊎-isStrictPartialOrder : IsStrictPartialOrder ≈₁ ∼₁ →
                           IsStrictPartialOrder ≈₂ ∼₂ →
                           IsStrictPartialOrder
                             (Pointwise ≈₁ ≈₂) (Pointwise ∼₁ ∼₂)
  ⊎-isStrictPartialOrder spo₁ spo₂ = record
    { isEquivalence =
        ⊎-isEquivalence (isEquivalence spo₁) (isEquivalence spo₂)
    ; irrefl        = ⊎-irreflexive (irrefl   spo₁) (irrefl   spo₂)
    ; trans         = ⊎-transitive  (trans    spo₁) (trans    spo₂)
    ; <-resp-≈      = ⊎-respects₂   (<-resp-≈ spo₁) (<-resp-≈ spo₂)
    }
    where open IsStrictPartialOrder

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

module _ {a b c d} where

  ⊎-setoid : Setoid a b → Setoid c d → Setoid _ _
  ⊎-setoid s₁ s₂ = record
    { isEquivalence =
        ⊎-isEquivalence (isEquivalence s₁) (isEquivalence s₂)
    } where open Setoid

  ⊎-decSetoid : DecSetoid a b → DecSetoid c d → DecSetoid _ _
  ⊎-decSetoid ds₁ ds₂ = record
    { isDecEquivalence =
        ⊎-isDecEquivalence (isDecEquivalence ds₁) (isDecEquivalence ds₂)
    } where open DecSetoid

  -- Some additional notation for combining setoids
  infix 4 _⊎ₛ_
  _⊎ₛ_ : Setoid a b → Setoid c d → Setoid _ _
  _⊎ₛ_ = ⊎-setoid

module _ {a b c d e f} where

  ⊎-preorder : Preorder a b c → Preorder d e f → Preorder _ _ _
  ⊎-preorder p₁ p₂ = record
    { isPreorder   =
        ⊎-isPreorder (isPreorder p₁) (isPreorder p₂)
    } where open Preorder

  ⊎-poset : Poset a b c → Poset a b c → Poset _ _ _
  ⊎-poset po₁ po₂ = record
    { isPartialOrder =
        ⊎-isPartialOrder (isPartialOrder po₁) (isPartialOrder po₂)
    } where open Poset

------------------------------------------------------------------------
-- The propositional equality setoid over products can be
-- decomposed using Pointwise

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

  Pointwise-≡⇒≡ : (Pointwise _≡_ _≡_) ⇒ _≡_ {A = A ⊎ B}
  Pointwise-≡⇒≡ (inj₁ x) = P.cong inj₁ x
  Pointwise-≡⇒≡ (inj₂ x) = P.cong inj₂ x

  ≡⇒Pointwise-≡ : _≡_ {A = A ⊎ B} ⇒ (Pointwise _≡_ _≡_)
  ≡⇒Pointwise-≡ P.refl = ⊎-refl P.refl P.refl

Pointwise-≡↔≡ : ∀ {a b} (A : Set a) (B : Set b) →
                Inverse (P.setoid A ⊎ₛ P.setoid B)
                        (P.setoid (A ⊎ B))
Pointwise-≡↔≡ _ _ = record
  { to         = record { _⟨$⟩_ = id; cong = Pointwise-≡⇒≡ }
  ; from       = record { _⟨$⟩_ = id; cong = ≡⇒Pointwise-≡ }
  ; inverse-of = record
    { left-inverse-of  = λ _ → ⊎-refl P.refl P.refl
    ; right-inverse-of = λ _ → P.refl
    }
  }

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

-- Version 1.0

module _ {a b c d r s}
         {A : Set a} {B : Set b} {C : Set c} {D : Set d}
         {R : REL A C r} {S : REL B D s}
         where

  ₁∼₁ : ∀ {a c} → R a c → Pointwise R S (inj₁ a) (inj₁ c)
  ₁∼₁ = inj₁
  {-# WARNING_ON_USAGE ₁∼₁
  "Warning: ₁∼₁ was deprecated in v1.0.
  Please use inj₁ in `Data.Sum.Properties` instead."
  #-}

  ₂∼₂ : ∀ {b d} → S b d → Pointwise R S (inj₂ b) (inj₂ d)
  ₂∼₂ = inj₂
  {-# WARNING_ON_USAGE ₂∼₂
  "Warning: ₂∼₂ was deprecated in v1.0.
  Please use inj₂ in `Data.Sum.Properties` instead."
  #-}

_⊎-≟_ : ∀ {a b} {A : Set a} {B : Set b} →
        Decidable {A = A} _≡_ → Decidable {A = B} _≡_ →
        Decidable {A = A ⊎ B} _≡_
(dec₁ ⊎-≟ dec₂) s₁ s₂ = Dec.map′ Pointwise-≡⇒≡ ≡⇒Pointwise-≡ (s₁ ≟ s₂)
  where
  open DecSetoid (⊎-decSetoid (P.decSetoid dec₁) (P.decSetoid dec₂))
{-# WARNING_ON_USAGE _⊎-≟_
"Warning: _⊎-≟_ was deprecated in v1.0.
Please use ≡-dec in `Data.Sum.Properties` instead."
#-}


text:
module Human.IO where

postulate IO : ∀ {a} → Set a → Set a
{-# BUILTIN IO IO #-}

max_stars_repo_name: MaisaMilena/JuiceMaker

max_issues_repo_name: MaisaMilena/JuiceMaker

max_forks_repo_name: MaisaMilena/JuiceMaker


text:
module Data.Fin.Subset.Disjoint where

open import Data.Nat
open import Data.Vec hiding (_∈_)
open import Data.Fin
open import Data.List as List hiding (zipWith)
open import Data.Fin.Subset

-- disjointness and relational specifiation of disjoint union
module _ {n} where

  _◆_ : Subset n → Subset n → Set
  l ◆ r = Empty (l ∩ r)

  data _⨄_ : List (Subset n) → Subset n → Set where
    []  : [] ⨄ ⊥
    _∷_ : ∀ {xs x y} → x ◆ y → xs ⨄ y → (x ∷ xs) ⨄ (x ∪ y)

-- picking from support
module _ {n} where
  _⊇⟨_⟩_ : Subset n → (l : ℕ) → Vec (Fin n) l → Set
  xs ⊇⟨ l ⟩ ys = All (λ y → y ∈ xs) ys
    where open import Data.Vec.All

-- removing from support
module _ {n} where
  _\\_ : ∀ {l} → Subset n → Vec (Fin n) l → Subset n
  xs \\ [] = xs
  xs \\ (x ∷ ys) = (xs [ x ]≔ outside) \\ ys


text:
module natThms where

open import lib

-- this function divides a natural number by 2, dropping any remainder
div2 : ℕ → ℕ
div2 0 = 0
div2 1 = 0
div2 (suc (suc x)) = suc (div2 x)

div2-double : ∀(x : ℕ) → (div2 (x * 2)) ≡ x
div2-double zero = refl
div2-double (suc x) rewrite div2-double (x)  = refl

{- Hint: consider the same cases as in the definition of div2: 0, 1, (suc (suc x)).
   The case for 1 is impossible, so you can just drop that case or use the
   absurd pattern for the proof of is-even 1 ≡ tt. -}
div2-even : ∀(x : ℕ) → is-even x ≡ tt → div2 x ≡ div2 (suc x)
div2-even zero x = refl
div2-even (suc (suc x))y rewrite div2-even x y = refl

-- same hint as for div2-even, except now the 0 case is impossible
div2-odd : ∀(x : ℕ) → is-odd x ≡ tt → div2 (suc x) ≡ suc (div2 x)
div2-odd (suc(suc x))y rewrite div2-odd x y = refl
div2-odd (suc zero) y  = refl

{- hint: do *not* do induction on x.  Look at the definitions of square and pow.
   There are lemmas about multiplication in the IAL that will help you (nat-thms.agda). -}
square-square : ∀(x : ℕ) → square (square x) ≡ x pow 4
square-square x rewrite *1{x} | *assoc x x ( x * x )  = refl


text:
-- Reported by nad 2018-01-23
{-# OPTIONS --sized-types #-}

module Issue3517 where

import Issue3517.S
import Issue3517.M

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Lang.Vars.Structure.Operator where

import Lvl
open import Data
open import Logic.Predicate
open import Structure.Setoid
open import Structure.Function.Domain
open import Structure.Operator.Properties
open import Structure.Operator
open import Type

-- TODO: These are to make the generalized variables work when they depend on each other. Are there any better ways?
module Select where
  module _ {ℓ ℓₑ} {T : Type{ℓ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ where
    select-invol : ∀(f : T → T) → Involution(f) → Type{Lvl.𝟎}
    select-invol _ _ = Data.Unit

  module _ {ℓ ℓₑ} {T : Type{ℓ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ {_▫_ : T → T → T} where
    select-id : ∀(id) → Identity(_▫_)(id) → Type{Lvl.𝟎}
    select-id _ _ = Data.Unit

    select-idₗ : ∀(id) → Identityₗ(_▫_)(id) → Type{Lvl.𝟎}
    select-idₗ _ _ = Data.Unit

    select-idᵣ : ∀(id) → Identityᵣ(_▫_)(id) → Type{Lvl.𝟎}
    select-idᵣ _ _ = Data.Unit

    select-inv : ∀(id)(ident)(inv) → InverseFunction(_▫_) ⦃ [∃]-intro(id) ⦃ ident ⦄ ⦄ (inv) → Type{Lvl.𝟎}
    select-inv _ _ _ _ = Data.Unit

    select-invₗ : ∀(id)(ident)(inv) → InverseFunctionₗ(_▫_) ⦃ [∃]-intro(id) ⦃ ident ⦄ ⦄ (inv) → Type{Lvl.𝟎}
    select-invₗ _ _ _ _ = Data.Unit

    select-invᵣ : ∀(id)(ident)(inv) → InverseFunctionᵣ(_▫_) ⦃ [∃]-intro(id) ⦃ ident ⦄ ⦄ (inv) → Type{Lvl.𝟎}
    select-invᵣ _ _ _ _ = Data.Unit

    select-invPropₗ : ∀(inv) → InversePropertyₗ(_▫_)(inv) → Type{Lvl.𝟎}
    select-invPropₗ _ _ = Data.Unit

    select-invPropᵣ : ∀(inv) → InversePropertyᵣ(_▫_)(inv) → Type{Lvl.𝟎}
    select-invPropᵣ _ _ = Data.Unit

    select-abs : ∀(id) → Absorber(_▫_)(id) → Type{Lvl.𝟎}
    select-abs _ _ = Data.Unit

    select-absₗ : ∀(id) → Absorberₗ(_▫_)(id) → Type{Lvl.𝟎}
    select-absₗ _ _ = Data.Unit

    select-absᵣ : ∀(id) → Absorberᵣ(_▫_)(id) → Type{Lvl.𝟎}
    select-absᵣ _ _ = Data.Unit

module One {ℓ ℓₑ} {T : Type{ℓ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ {_▫_ : T → T → T} where
  variable {id idₗ idᵣ ab abₗ abᵣ} : T
  variable {inv invₗ invᵣ} : T → T
  variable ⦃ op ⦄ : BinaryOperator ⦃ equiv ⦄ ⦃ equiv ⦄ ⦃ equiv ⦄ (_▫_)
  variable ⦃ comm ⦄ : Commutativity ⦃ equiv ⦄ (_▫_)
  variable ⦃ cancₗ ⦄ : Cancellationₗ ⦃ equiv ⦄ ⦃ equiv ⦄ (_▫_)
  variable ⦃ cancᵣ ⦄ : Cancellationᵣ ⦃ equiv ⦄ ⦃ equiv ⦄ (_▫_)
  variable ⦃ assoc ⦄ : Associativity ⦃ equiv ⦄ (_▫_)
  variable ⦃ ident  ⦄ : Identity ⦃ equiv ⦄ (_▫_)(id)
  variable ⦃ identₗ ⦄ : Identityₗ ⦃ equiv ⦄ (_▫_)(id)
  variable ⦃ identᵣ ⦄ : Identityᵣ ⦃ equiv ⦄ (_▫_)(id)
  variable ⦃ inver  ⦄ : InverseFunction ⦃ equiv ⦄ (_▫_) ⦃ [∃]-intro(id) ⦃ ident ⦄ ⦄ (inv)
  variable ⦃ inverₗ ⦄ : InverseFunctionₗ ⦃ equiv ⦄ (_▫_) ⦃ [∃]-intro(idₗ) ⦃ identₗ ⦄ ⦄ (invₗ)
  variable ⦃ inverᵣ ⦄ : InverseFunctionᵣ ⦃ equiv ⦄ (_▫_) ⦃ [∃]-intro(idᵣ) ⦃ identᵣ ⦄ ⦄ (invᵣ)
  variable ⦃ inverPropₗ ⦄ : InversePropertyₗ ⦃ equiv ⦄ (_▫_) (invₗ)
  variable ⦃ inverPropᵣ ⦄ : InversePropertyᵣ ⦃ equiv ⦄ (_▫_) (invᵣ)
  variable ⦃ invol ⦄ : Involution ⦃ equiv ⦄ (inv)
  variable ⦃ absorb  ⦄ : Absorber ⦃ equiv ⦄ (_▫_)(ab)
  variable ⦃ absorbₗ ⦄ : Absorberₗ ⦃ equiv ⦄ (_▫_)(ab)
  variable ⦃ absorbᵣ ⦄ : Absorberᵣ ⦃ equiv ⦄ (_▫_)(ab)

module OneTypeTwoOp {ℓ ℓₑ} {T : Type{ℓ}} ⦃ equiv : Equiv{ℓₑ}(T) ⦄ {_▫₁_ _▫₂_ : T → T → T} where
  variable {id} : T
  variable {inv} : T → T

  variable ⦃ op₁ ⦄ : BinaryOperator ⦃ equiv ⦄ ⦃ equiv ⦄ ⦃ equiv ⦄ (_▫₁_)
  variable ⦃ comm₁ ⦄ : Commutativity ⦃ equiv ⦄ (_▫₁_)
  variable ⦃ cancₗ₁ ⦄ : Cancellationₗ ⦃ equiv ⦄ ⦃ equiv ⦄ (_▫₁_)
  variable ⦃ cancᵣ₁ ⦄ : Cancellationᵣ ⦃ equiv ⦄ ⦃ equiv ⦄ (_▫₁_)
  variable ⦃ assoc₁ ⦄ : Associativity ⦃ equiv ⦄ (_▫₁_)
  variable ⦃ ident₁  ⦄ : Identity ⦃ equiv ⦄ (_▫₁_)(id)
  variable ⦃ identₗ₁ ⦄ : Identityₗ ⦃ equiv ⦄ (_▫₁_)(id)
  variable ⦃ identᵣ₁ ⦄ : Identityᵣ ⦃ equiv ⦄ (_▫₁_)(id)
  variable ⦃ inver₁  ⦄ : InverseFunction ⦃ equiv ⦄ (_▫₁_) ⦃ [∃]-intro(id) ⦃ ident₁ ⦄ ⦄ (inv)
  variable ⦃ inverₗ₁ ⦄ : InverseFunctionₗ ⦃ equiv ⦄ (_▫₁_) ⦃ [∃]-intro(id) ⦃ identₗ₁ ⦄ ⦄ (inv)
  variable ⦃ inverᵣ₁ ⦄ : InverseFunctionᵣ ⦃ equiv ⦄ (_▫₁_) ⦃ [∃]-intro(id) ⦃ identᵣ₁ ⦄ ⦄ (inv)
  variable ⦃ absorbₗ₁ ⦄ : Absorberₗ ⦃ equiv ⦄ (_▫₁_)(id)
  variable ⦃ absorbᵣ₁ ⦄ : Absorberᵣ ⦃ equiv ⦄ (_▫₁_)(id)

  variable ⦃ op₂ ⦄ : BinaryOperator ⦃ equiv ⦄ ⦃ equiv ⦄ ⦃ equiv ⦄ (_▫₂_)
  variable ⦃ comm₂ ⦄ : Commutativity ⦃ equiv ⦄ (_▫₂_)
  variable ⦃ cancₗ₂ ⦄ : Cancellationₗ ⦃ equiv ⦄ ⦃ equiv ⦄ (_▫₂_)
  variable ⦃ cancᵣ₂ ⦄ : Cancellationᵣ ⦃ equiv ⦄ ⦃ equiv ⦄ (_▫₂_)
  variable ⦃ assoc₂ ⦄ : Associativity ⦃ equiv ⦄ (_▫₂_)
  variable ⦃ ident₂  ⦄ : Identity ⦃ equiv ⦄ (_▫₂_)(id)
  variable ⦃ identₗ₂ ⦄ : Identityₗ ⦃ equiv ⦄ (_▫₂_)(id)
  variable ⦃ identᵣ₂ ⦄ : Identityᵣ ⦃ equiv ⦄ (_▫₂_)(id)
  variable ⦃ inver₂  ⦄ : InverseFunction ⦃ equiv ⦄ (_▫₂_) ⦃ [∃]-intro(id) ⦃ ident₂ ⦄ ⦄ (inv)
  variable ⦃ inverₗ₂ ⦄ : InverseFunctionₗ ⦃ equiv ⦄ (_▫₂_) ⦃ [∃]-intro(id) ⦃ identₗ₂ ⦄ ⦄ (inv)
  variable ⦃ inverᵣ₂ ⦄ : InverseFunctionᵣ ⦃ equiv ⦄ (_▫₂_) ⦃ [∃]-intro(id) ⦃ identᵣ₂ ⦄ ⦄ (inv)
  variable ⦃ absorbₗ₂ ⦄ : Absorberₗ ⦃ equiv ⦄ (_▫₂_)(id)
  variable ⦃ absorbᵣ₂ ⦄ : Absorberᵣ ⦃ equiv ⦄ (_▫₂_)(id)

  variable ⦃ distriₗ ⦄ : Distributivityₗ ⦃ equiv ⦄ (_▫₁_)(_▫₂_)
  variable ⦃ distriᵣ ⦄ : Distributivityᵣ ⦃ equiv ⦄ (_▫₁_)(_▫₂_)
  variable ⦃ absorpₗ ⦄ : Absorptionₗ ⦃ equiv ⦄ (_▫₁_)(_▫₂_)
  variable ⦃ absorpᵣ ⦄ : Absorptionᵣ ⦃ equiv ⦄ (_▫₁_)(_▫₂_)
  variable ⦃ inverOpₗ ⦄ : InverseOperatorₗ ⦃ equiv ⦄ (_▫₁_)(_▫₂_)
  variable ⦃ inverOpᵣ ⦄ : InverseOperatorᵣ ⦃ equiv ⦄ (_▫₁_)(_▫₂_)

module Two {ℓ₁ ℓ₂ ℓₑ₁ ℓₑ₂} {A : Type{ℓ₁}} ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ {_▫₁_ : A → A → A} {B : Type{ℓ₂}} ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ {_▫₂_ : B → B → B} where
  variable {id₁} : A
  variable {inv₁} : A → A
  variable {id₂} : B
  variable {inv₂} : B → B

  variable ⦃ op₁ ⦄ : BinaryOperator ⦃ equiv-A ⦄ ⦃ equiv-A ⦄ ⦃ equiv-A ⦄ (_▫₁_)
  variable ⦃ comm₁ ⦄ : Commutativity ⦃ equiv-A ⦄ (_▫₁_)
  variable ⦃ cancₗ₁ ⦄ : Cancellationₗ ⦃ equiv-A ⦄ ⦃ equiv-A ⦄ (_▫₁_)
  variable ⦃ cancᵣ₁ ⦄ : Cancellationᵣ ⦃ equiv-A ⦄ ⦃ equiv-A ⦄ (_▫₁_)
  variable ⦃ assoc₁ ⦄ : Associativity ⦃ equiv-A ⦄ (_▫₁_)
  variable ⦃ ident₁  ⦄ : Identity ⦃ equiv-A ⦄ (_▫₁_)(id₁)
  variable ⦃ identₗ₁ ⦄ : Identityₗ ⦃ equiv-A ⦄ (_▫₁_)(id₁)
  variable ⦃ identᵣ₁ ⦄ : Identityᵣ ⦃ equiv-A ⦄ (_▫₁_)(id₁)
  variable ⦃ inver₁  ⦄ : InverseFunction ⦃ equiv-A ⦄ (_▫₁_) ⦃ [∃]-intro(id₁) ⦃ ident₁ ⦄ ⦄ (inv₁)
  variable ⦃ inverₗ₁ ⦄ : InverseFunctionₗ ⦃ equiv-A ⦄ (_▫₁_) ⦃ [∃]-intro(id₁) ⦃ identₗ₁ ⦄ ⦄ (inv₁)
  variable ⦃ inverᵣ₁ ⦄ : InverseFunctionᵣ ⦃ equiv-A ⦄ (_▫₁_) ⦃ [∃]-intro(id₁) ⦃ identᵣ₁ ⦄ ⦄ (inv₁)

  variable ⦃ op₂ ⦄ : BinaryOperator ⦃ equiv-B ⦄ ⦃ equiv-B ⦄ ⦃ equiv-B ⦄ (_▫₂_)
  variable ⦃ comm₂ ⦄ : Commutativity ⦃ equiv-B ⦄ (_▫₂_)
  variable ⦃ cancₗ₂ ⦄ : Cancellationₗ ⦃ equiv-B ⦄ ⦃ equiv-B ⦄ (_▫₂_)
  variable ⦃ cancᵣ₂ ⦄ : Cancellationᵣ ⦃ equiv-B ⦄ ⦃ equiv-B ⦄ (_▫₂_)
  variable ⦃ assoc₂ ⦄ : Associativity ⦃ equiv-B ⦄ (_▫₂_)
  variable ⦃ ident₂  ⦄ : Identity ⦃ equiv-B ⦄ (_▫₂_)(id₂)
  variable ⦃ identₗ₂ ⦄ : Identityₗ ⦃ equiv-B ⦄ (_▫₂_)(id₂)
  variable ⦃ identᵣ₂ ⦄ : Identityᵣ ⦃ equiv-B ⦄ (_▫₂_)(id₂)
  variable ⦃ inver₂  ⦄ : InverseFunction ⦃ equiv-B ⦄ (_▫₂_) ⦃ [∃]-intro(id₂) ⦃ ident₂ ⦄ ⦄ (inv₂)
  variable ⦃ inverₗ₂ ⦄ : InverseFunctionₗ ⦃ equiv-B ⦄ (_▫₂_) ⦃ [∃]-intro(id₂) ⦃ identₗ₂ ⦄ ⦄ (inv₂)
  variable ⦃ inverᵣ₂ ⦄ : InverseFunctionᵣ ⦃ equiv-B ⦄ (_▫₂_) ⦃ [∃]-intro(id₂) ⦃ identᵣ₂ ⦄ ⦄ (inv₂)


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

open import HoTT
open import homotopy.elims.Lemmas

{- Given a span [A ←f– C –g→ B] and a map [h : A ⊔_C B → D] where
 - [g] has a left inverse:

 - To define a fundction  [Π (Cof h) P], one can give only the [cfbase],
 - [cfcod], [cfglue∘left], and [cfglue∘right] cases, and construct a map
 - which has the right behavior on [cfbase], [cfcod], [cfglue∘left],
 - with [cfglue∘right] edited to achieve the highest coherence.

 - This is useful for for proving equivalences where (at least) one side
 - involves one of these iterated pushouts. It could be generalized
 - further by loosening from cofiber to some more general class of pushouts,
 - but this is sufficient for the current applications. -}

module homotopy.elims.CofPushoutSection where

module _ {i j k l} {s : Span {i} {j} {k}} {D : Type l}
  {h : Pushout s → D} where

  open Span s

  module CofPushoutSection (r : B → C) (inv : ∀ c → r (g c) == c) where

    elim : ∀ {m} {P : Cofiber h → Type m}
      (cfbase* : P cfbase) (cfcod* : (d : D) → P (cfcod d))
      (cfglue-left* : (a : A) →
        cfbase* == cfcod* (h (left a)) [ P ↓ cfglue (left a) ])
      (cfglue-right* : (b : B) →
        cfbase* == cfcod* (h (right b)) [ P ↓ cfglue (right b) ])
      → Π (Cofiber h) P
    elim {P = P} cfbase* cfcod* cfglue-left* cfglue-right* =
      Cofiber-elim
        cfbase*
        cfcod*
        (Pushout-elim
          cfglue-left*
          (λ b → (fst (fill (r b))) ◃ cfglue-right* b)
          (λ c → ↓↓-from-squareover $
            transport
              (λ c' → SquareOver P (natural-square cfglue (glue c))
                  (cfglue-left* (f c))
                  (↓-ap-in P (λ _ → cfbase) (apd (λ _ → cfbase*) (glue c)))
                  (↓-ap-in P (cfcod ∘ h) (apd (cfcod* ∘ h) (glue c)))
                  (fst (fill c') ◃ cfglue-right* (g c)))
              (! (inv c))
              (snd (fill c))))
      where
      fill : (c : C)
        → Σ (cfbase* == cfbase*)
            (λ q → SquareOver P (natural-square cfglue (glue c))
                     (cfglue-left* (f c)) _ _ (q ◃ cfglue-right* (g c)))
      fill c = fill-upper-right _ _ _ _ _

    rec : ∀ {m} {E : Type m}
      (cfbase* : E) (cfcod* : D → E)
      (cfglue-left* : (a : A) → cfbase* == cfcod* (h (left a)))
      (cfglue-right* : (b : B) → cfbase* == cfcod* (h (right b)))
      → (Cofiber h → E)
    rec cfbase* cfcod* cfglue-left* cfglue-right* =
      elim cfbase* cfcod* (↓-cst-in ∘ cfglue-left*) (↓-cst-in ∘ cfglue-right*)

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


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

open import Definition.Typed.EqualityRelation

module Definition.LogicalRelation.Substitution.Introductions.Universe {{eqrel : EqRelSet}} where
open EqRelSet {{...}}

open import Definition.Untyped
open import Definition.LogicalRelation
open import Definition.LogicalRelation.Properties
open import Definition.LogicalRelation.Substitution

open import Tools.Product
import Tools.PropositionalEquality as PE

-- Validity of the universe type.
Uᵛ : ∀ {Γ} ([Γ] : ⊩ᵛ Γ) → Γ ⊩ᵛ⟨ ¹ ⟩ U / [Γ]
Uᵛ [Γ] ⊢Δ [σ] = Uᵣ′ ⁰ 0<1 ⊢Δ , λ _ x₂ → U₌ PE.refl

-- Valid terms of type U are valid types.
univᵛ : ∀ {A Γ l l′} ([Γ] : ⊩ᵛ Γ)
        ([U] : Γ ⊩ᵛ⟨ l ⟩ U / [Γ])
      → Γ ⊩ᵛ⟨ l ⟩ A ∷ U / [Γ] / [U]
      → Γ ⊩ᵛ⟨ l′ ⟩ A / [Γ]
univᵛ {l′ = l′} [Γ] [U] [A] ⊢Δ [σ] =
  let [A]₁ = maybeEmb′ {l′} (univEq (proj₁ ([U] ⊢Δ [σ])) (proj₁ ([A] ⊢Δ [σ])))
  in  [A]₁ , (λ [σ′] [σ≡σ′] → univEqEq (proj₁ ([U] ⊢Δ [σ])) [A]₁
                                       ((proj₂ ([A] ⊢Δ [σ])) [σ′] [σ≡σ′]))

-- Valid term equality of type U is valid type equality.
univEqᵛ : ∀ {A B Γ l l′} ([Γ] : ⊩ᵛ Γ)
          ([U] : Γ ⊩ᵛ⟨ l′ ⟩ U / [Γ])
          ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
        → Γ ⊩ᵛ⟨ l′ ⟩ A ≡ B ∷ U / [Γ] / [U]
        → Γ ⊩ᵛ⟨ l ⟩ A ≡ B / [Γ] / [A]
univEqᵛ {A} [Γ] [U] [A] [t≡u] ⊢Δ [σ] =
  univEqEq (proj₁ ([U] ⊢Δ [σ])) (proj₁ ([A] ⊢Δ [σ])) ([t≡u] ⊢Δ [σ])

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:
-- Andreas, 2018-06-09, issue #2513, parsing attributes

postulate
  @0 @ω A : Set

-- Should fail with error:
-- Conflicting attributes: 0 ω


text:
module Data.FixedTree where

import      Lvl
open import Data hiding (empty)
open import Data.List
open import Data.Tuple using (_⨯_ ; _,_)
open import Data.Tuple.Raise
open import Functional as Fn
open import Numeral.Natural
open import Type

private variable ℓ ℓᵢ ℓₗ ℓₙ ℓₒ : Lvl.Level
private variable n : ℕ
private variable N N₁ N₂ L T A B : Type{ℓ}

module _ {I : Type{ℓᵢ}} (children : I → ℕ) (step : I → I) (L : Type{ℓₗ}) (N : Type{ℓₙ}) where
  data Tree₊ : I → Type{ℓₗ Lvl.⊔ ℓₙ Lvl.⊔ ℓᵢ} where
    Leaf : ∀{i} → L → Tree₊(i)
    Node : ∀{i} → N → (Tree₊(step i) ^ children(step i)) → Tree₊(i)

  data Tree₋ : I → Type{ℓₗ Lvl.⊔ ℓₙ Lvl.⊔ ℓᵢ} where
    Leaf : ∀{i} → L → Tree₋(i)
    Node : ∀{i} → N → (Tree₋(i) ^ children(i)) → Tree₋(step i)

-- Alternative definition:
--   data FixedTree (n : ℕ) (L : Type{ℓₗ}) (N : Type{ℓₙ}) : Type{ℓₗ Lvl.⊔ ℓₙ} where
--     Leaf : L → FixedTree(n) L N
--     Node : N → ((FixedTree(n) L N) ^ n) → FixedTree(n) L N
FixedTree : ℕ → Type{ℓₗ} → Type{ℓₙ} → Type{ℓₗ Lvl.⊔ ℓₙ}
FixedTree(n) L N = Tree₊ id id L N n

open import Data using (Unit ; <>)
open import Data.Boolean
open import Data.Boolean.Operators
open        Data.Boolean.Operators.Programming
open import Data.Option
import      Data.Tuple.Raiseᵣ.Functions as Raise
open import Logic.Propositional
open import Logic.Predicate
open import Numeral.Finite
open import Numeral.Finite.Oper.Comparisons
open import Numeral.Natural.Function
open import Numeral.Natural.Oper hiding (_^_)

emptyTree : FixedTree{ℓₗ}(n) Unit N
emptyTree{n = n} = Leaf <>

singleton : N → FixedTree{ℓₗ}(n) Unit N
singleton{n = n} a = Node a (Raise.repeat n emptyTree)

isLeaf : FixedTree(n) L N → Bool
isLeaf (Leaf _)   = 𝑇
isLeaf (Node _ _) = 𝐹

isNode : FixedTree(n) L N → Bool
isNode (Leaf _)   = 𝐹
isNode (Node _ _) = 𝑇

root : FixedTree(n) L N → Option(N)
root (Leaf _)   = None
root (Node a _) = Some a

foldChildNodesᵣ : (((FixedTree(n) L N) ^ n) → N → T → T) → T → FixedTree(n) L N → T
foldChildNodesᵣ        join id (Leaf _)   = id
foldChildNodesᵣ{n = n} join id (Node _ c) = Raise.foldᵣ{n} (\{(Leaf _) → Fn.id ; (Node a c) → join c a}) id c

-- TODO: Is it correct? Also termination checker
{-
testfoldᵣ : ∀{n : ℕ}{ℓ₁ ℓ₂}{A : Type{ℓ₁}}{B : Type{ℓ₂}} → (A → B → B) → B → (FixedTree(n)(A) ^ n) → B
testfoldᵣ {0}       (_▫_) id _              = id
testfoldᵣ {1}       (_▫_) id Leaf           = id
testfoldᵣ {1}       (_▫_) id (Node a c)     = a ▫ testfoldᵣ {1} (_▫_) id c
-- x ▫ def
testfoldᵣ {𝐒(𝐒(n))} (_▫_) def (x , xs) = {!!}
-- x ▫ testfoldᵣ {𝐒(n)} (_▫_) def xs

fold : (A → B → B) → B → FixedTree(n)(A) → B
fold        (_▫_) id Leaf       = id
fold{n = n} (_▫_) id (Node a c) = a ▫ Raise.foldᵣ{n} (\{Leaf -> Fn.id ; node@(Node _ _) acc → fold{n = n} (_▫_) acc node}) id c

fold : (A → B → B) → B → FixedTree(n)(A) → B
fold{A = A}{B = B}{n = n} (_▫_) id tree = foldChildNodesᵣ ({!swap(fold{n = n} (_▫_))!}) id tree where
  f : ∀{n₁ n₂} → FixedTree(n₁)(A) ^ n₂ → A → B → B
  f {n₂ = 0}        <>           a acc = a ▫ acc
  f {n₂ = 1}        Leaf         a acc = a ▫ acc
  f {n₂ = 1}        (Node ca cc) a acc = f cc a (ca ▫ acc)
  -- ca ▫ (a ▫ acc)
  f {n₂ = 𝐒(𝐒(n₂))} c a acc = {!!}

testfoldDepthFirst : (A → B → B) → B → FixedTree(n)(A) → B
testfoldᵣ : ∀{n₁ n₂ : ℕ}{ℓ₁ ℓ₂}{A : Type{ℓ₁}}{B : Type{ℓ₂}} → (A → B → B) → B → (FixedTree(n₁)(A) ^ n₂) → B

testfoldDepthFirst        (_▫_) id Leaf       = id
testfoldDepthFirst{n = n} (_▫_) id (Node a c) = a ▫ testfoldᵣ{n} (_▫_) id c

testfoldᵣ          {n₂ = 0}        (_▫_) def _        = def
testfoldᵣ {n₁ = n₁}{n₂ = 1}        (_▫_) def x        = testfoldDepthFirst{n = n₁} (_▫_) def x
-- testfoldᵣ {n₂ = 𝐒(𝐒(n₂))} (_▫_) def (x , xs) = swap(testfoldDepthFirst{n = _} (_▫_)) x (testfoldᵣ {n₂ = 𝐒(n₂)} (_▫_) def xs)

testfoldᵣ : ∀{n₁ n₂ : ℕ}{ℓ₁ ℓ₂}{A : Type{ℓ₁}}{B : Type{ℓ₂}} → (A → B → B) → B → (FixedTree(n₁)(A) ^ n₂) → B
testfoldᵣ {n₂ = 0}       (_▫_) id <>              = id
testfoldᵣ {n₂ = 1}       (_▫_) id Leaf            = id
testfoldᵣ {n₂ = 1}       (_▫_) id (Node a c)      = a ▫ testfoldᵣ(_▫_) id c
testfoldᵣ {n₂ = 𝐒(𝐒(n))} (_▫_) id (Leaf     , xs) = testfoldᵣ(_▫_) id xs
testfoldᵣ {n₂ = 𝐒(𝐒(n))} (_▫_) id (Node a c , xs) = testfoldᵣ(_▫_) (a ▫ testfoldᵣ(_▫_) id xs) c
-}

{-# TERMINATING #-}
foldDepthFirst : (N → T → T) → T → FixedTree(n) L N → T
foldDepthFirst        (_▫_) id (Leaf _)   = id
foldDepthFirst{n = n} (_▫_) id (Node a c) = a ▫ Raise.foldᵣ{n} (swap(foldDepthFirst{n = n} (_▫_))) id c

import      Data.Tuple.RaiseTypeᵣ.Functions as RaiseType
open import Function.Multi
import      Function.Multi.Functions as Multi

{-# TERMINATING #-}
FixedTree-induction : ∀{P : FixedTree{ℓₗ}{ℓₙ}(n) L N → Type{ℓ}} → (∀{l} → P(Leaf l)) → ((a : N) → (c : (FixedTree(n) L N) ^ n) → (RaiseType.from-[^] (Raise.map P(c)) ⇉ P(Node a c))) → ((tree : FixedTree(n) L N) → P(tree))
FixedTree-induction                       base _    (Leaf l)   = base{l}
FixedTree-induction {n = 0}               _    step (Node a c) = step a c
FixedTree-induction {n = 1}               base step (Node a c) = step a c (FixedTree-induction{n = 1} base step c)
FixedTree-induction {n = 𝐒(𝐒(n))} {P = P} base step (Node a c) = recurseChildren{𝐒(𝐒(n))}(step a c) where
  recurseChildren : ∀{L}{l : _ ^ L} → (RaiseType.from-[^] (Raise.map P(l)) ⇉ P(Node a c)) → P(Node a c)
  recurseChildren {0}                 = id
  recurseChildren {1}       {l}     p = p(FixedTree-induction{n = 𝐒(𝐒(n))} base step l)
  recurseChildren {𝐒(𝐒(L))} {x , l} p = recurseChildren{𝐒(L)}{l} (p(FixedTree-induction{n = 𝐒(𝐒(n))} base step x))

-- The size is the number of nodes in the tree.
-- Alternative implementation:
--   size{n = n}{L = L}{N = N} = FixedTree-induction 𝟎 (rec{w = n}) where
--     rec : ∀{w} → (a : N) → (c : (FixedTree(n) L N) ^ w) → RaiseType.from-[^] (Raise.map{w} (const ℕ)(c)) ⇉ ℕ
--     rec {w = 0}       _  _         = 1
--     rec {w = 1}       _  _       n = 𝐒(n)
--     rec {w = 𝐒(𝐒(w))} a  (_ , c) n = Multi.compose(𝐒(w)) (n +_) (rec{w = 𝐒(w)} a c)
{-# TERMINATING #-}
size : FixedTree(n) L N → ℕ
size (Leaf _)   = 𝟎
size (Node _ c) = 𝐒(Raise.foldᵣ((_+_) ∘ size) 𝟎 c)

-- The height is the length of the longest path from the root node.
-- Alternative implementation:
--   height{n = n}{L = L}{N = N} = FixedTree-induction 𝟎 (rec{w = n}) where
--     -- Note: The return type is equal to `RaiseType.repeat(L) ℕ ⇉ ℕ`
--     rec : ∀{w} → (a : N) → (c : (FixedTree(n) L N) ^ w) → RaiseType.from-[^] (Raise.map{w} (const ℕ)(c)) ⇉ ℕ
--     rec {w = 0}       _  _         = 1
--     rec {w = 1}       _  _       n = 𝐒(n)
--     rec {w = 𝐒(𝐒(w))} a  (_ , c) n = Multi.compose(𝐒(w)) (max n) (rec{w = 𝐒(w)} a c)
{-# TERMINATING #-}
height : FixedTree(n) L N → ℕ
height (Leaf _)   = 𝟎
height (Node _ c) = 𝐒(Raise.foldᵣ(max ∘ height) 𝟎 c)

import Data.Tuple.Raiseᵣ.Functions as TupleRaiseᵣ
import Data.List.Functions as List

treesOfDepth : ℕ → FixedTree(n) L N → List(FixedTree(n) L N)
treesOfDepth 𝟎      tree       = tree ⊰ ∅
treesOfDepth (𝐒(_)) (Leaf _)   = ∅
treesOfDepth (𝐒(n)) (Node _ c) = TupleRaiseᵣ.foldᵣ((List._++_) ∘ treesOfDepth n) ∅ c


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

module HITs.PropositionalTruncation.Sugar where

open import Cubical.HITs.PropositionalTruncation
open import Level

_=<<_ : ∀ {a} {A : Type a} {b} {B : ∥ A ∥ → Type b}
      → ((x : A) → ∥ B ∣ x ∣ ∥) → (xs : ∥ A ∥) → ∥ B xs ∥
_=<<_ = elimPropTrunc (λ _ → squash)

_>>=_ : ∀ {a} {A : Type a} {b} {B : Type b}
      → (xs : ∥ A ∥) → (A → ∥ B ∥) → ∥ B ∥
_>>=_ {a} {A} {b} {B} xs f = elimPropTrunc (λ _ → squash) f xs

_>>_ : ∥ A ∥ → ∥ B ∥ → ∥ B ∥
_ >> ys = ys

pure : A → ∥ A ∥
pure = ∣_∣

_<*>_ : ∥ (A → B) ∥ → ∥ A ∥ → ∥ B ∥
fs <*> xs = do
  f ← fs
  x ← xs
  ∣ f x ∣

infixr 1 _∥$∥_
_∥$∥_ : (A → B)→ ∥ A ∥ → ∥ B ∥
f ∥$∥ xs = recPropTrunc squash (λ x → ∣ f x ∣) xs

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
{-

Part 3: Univalence and the SIP

• Univalence from ua and uaβ
• Transporting with ua
• The SIP as a consequence of ua

-}
{-# OPTIONS --cubical #-}
module Part3 where

open import Cubical.Core.Glue public
  using ( Glue ; glue ; unglue ; lineToEquiv )

open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism

open import Part1
open import Part2

-- A key concept in HoTT/UF is univalence. As we have seen earlier in
-- the week this is assumed as an axiom in HoTT. In Cubical Agda it is
-- instead provable and has computational content. This means that
-- transporting with paths constructed using univalence reduces as
-- opposed to HoTT where they would be stuck. This simplifies some
-- proofs and make it possible to actually do concrete computations
-- using univalence.

-- The part of univalence which is most useful for our applications is
-- to be able to turn equivalences (written _≃_ and defined as a Σ-type
-- of a function and a proof that it has contractible fibers) into
-- paths:
ua : {A B : Type ℓ} → A ≃ B → A ≡ B
ua {A = A} {B = B} e i = Glue B (λ { (i = i0) → (A , e)
                                   ; (i = i1) → (B , idEquiv B) })

-- This term is defined using "Glue types" which were introduced in
-- the CCHM paper. We won't have time to go into details about them
-- today, but for practical applications one can usually forget about
-- them and use ua as a black box. There are multiple useful lemmas in
-- Cubical.Foundations.Univalence and Cubical.Foundations.Transport
-- which are helpful when reasoning about ua which don't require
-- knowing what Glue types are.

-- The important point is that transporting along the path constructed
-- using ua applies the function underlying the equivalence. This is
-- easily proved using transportRefl:
uaβ : (e : A ≃ B) (x : A) → transport (ua e) x ≡ fst e x
uaβ e x = transportRefl (equivFun e x)

-- Note that for concrete types this typically hold definitionally,
-- but for an arbitrary equivalence e we have to prove it.

-- The fact that we have both ua and uaβ suffices to be able to prove
-- the standard formulation of univalence. For details see:
--
--   Cubical.Foundations.Univalence

-- The standard way of constructing equivalences is to start with an
-- isomorphism and then improve it into an equivalence. The lemma in
-- the library which does this is
--
--   isoToEquiv : {A B : Type ℓ} → Iso A B → A ≃ B

-- Composing this with ua lets us directly turn isomorphisms into paths:
--
--   isoToPath : {A B : Type ℓ} → Iso A B → A ≡ B

-- Time for an example!

-- Booleans
data Bool : Type₀ where
  false true : Bool

not : Bool → Bool
not false = true
not true  = false

notPath : Bool ≡ Bool
notPath = isoToPath (iso not not rem rem)
  where
  rem : (b : Bool) → not (not b) ≡ b
  rem false = refl
  rem true  = refl

_ : transport notPath true ≡ false
_ = refl

-- Another example, integers:

open import Cubical.Data.Int hiding (_+_ ; +-assoc)

sucPath : Int ≡ Int
sucPath = isoToPath (iso sucInt predInt sucPred predSuc)

_ : transport sucPath (pos 0) ≡ pos 1
_ = refl

_ : transport (sucPath ∙ sucPath) (pos 0) ≡ pos 2
_ = refl

_ : transport (sym sucPath) (pos 0) ≡ negsuc 0
_ = refl

-------------------------------------------------------------------------
-- The structure identity principle

-- Combining subst and ua lets us transport any structure on A to get
-- a structure on an equivalent type B
substEquiv : (S : Type ℓ → Type ℓ') (e : A ≃ B) → S A → S B
substEquiv S e = subst S (ua e)

-- Example with binary numbers:

open import Cubical.Data.BinNat.BinNat renaming (ℕ≃binnat to ℕ≃Bin ; binnat to Bin)
open import Cubical.Data.Nat

T : Set → Set
T X = Σ[ _+_ ∈ (X → X → X) ] ((x y z : X) → x + (y + z) ≡ (x + y) + z)

TBin : T Bin
TBin = substEquiv T ℕ≃Bin (_+_ , +-assoc)

_+Bin_ : Bin → Bin → Bin
_+Bin_  = fst TBin

+Bin-assoc : (m n o : Bin) → m +Bin (n +Bin o) ≡ (m +Bin n) +Bin o
+Bin-assoc = snd TBin

-- This is however not always what we want as _+Bin_ will translate
-- its input to unary numbers, add, and then translate back. Instead
-- we want to use efficient addition on binary numbers, but get the
-- associativity proof for free. So what we really want is to
-- characterize the equality of T-structured types, i.e. we want a
-- proof that two types equipped with T-structures are equal if there
-- is a T-structure preserving equivalence between them. This is the
-- usual meaning of the *structure identity principle* (SIP). This
-- implies in particular that the type of paths of
-- monoids/groups/rings/R-modules/... is equivalent to the type of
-- monoid/group/ring/R-module/... preserving equivalences.

-- We formalize this and much more using a cubical version of the SIP in:
--
-- Internalizing Representation Independence with Univalence
-- Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner
-- https://arxiv.org/abs/2009.05547
--
-- The binary numbers example with efficient addition is spelled out
-- in detail in Section 2.1.1 of:
--
-- https://www.doi.org/10.1017/S0956796821000034
-- (Can be downloaded from: https://staff.math.su.se/anders.mortberg/papers/cubicalagda2.pdf)


text:
{-# OPTIONS --copatterns #-}

open import Common.Prelude

record R : Set where
  field
    f1 : Nat
    f2 : String

r : R
R.f1 r = 5
R.f2 r = "yes"

main = putStrLn (R.f2 r)


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

   Copyright (c) 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.Base.Types
import      LibraBFT.Impl.OBM.ECP-LBFT-OBM-Diff.ECP-LBFT-OBM-Diff-0 as ECP-LBFT-OBM-Diff-0
open import Util.Prelude

module LibraBFT.Impl.OBM.ECP-LBFT-OBM-Diff.ECP-LBFT-OBM-Diff-2 where

-- This is a separate file to avoid a cyclic dependency.

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

e_DiemDB_getEpochEndingLedgerInfosImpl_limit : Epoch → Epoch → Epoch → (Epoch × Bool)
e_DiemDB_getEpochEndingLedgerInfosImpl_limit startEpoch endEpoch limit =
  if not ECP-LBFT-OBM-Diff-0.enabled
  then
    if-dec endEpoch >? startEpoch + limit
    then (startEpoch + limit , true)
    else (endEpoch           , false)
  else   (endEpoch           , false)


text:
-- Andreas, 2012-10-18 wish granted
module Issue481 where

-- Use case:

open import Common.Issue481ParametrizedModule Set using () renaming (id to idSet)
open import Common.Issue481ParametrizedModule (Set → Set) using () renaming (id to idSetToSet)

open import Common.Issue481ParametrizedModule

-- With 'as' clause:

open import Common.Issue481ParametrizedModule Set as PSet using (id)

{- MEANS:
import Common.Issue481ParametrizedModule
private open module PSet = Common.Issue481ParametrizedModule Set using (id)
-}

-- Abuse case:

as = Set

open import Common.Issue481ParametrizedModule as as as
module M = as

-- Test case:

module Test where

  -- should succeed:
  open import Issue481Record as Rec

  open Issue481Record

{- Note: this is NOT equivalent to the following, failing sequence

import Issue481Record
open module Rec = Issue481Record

open Issue481Record
-- Ambiguous module name Issue481Record. It could refer to any one of
--   Rec.Issue481Record
--   Issue481Record

It is equivalent to:
-}

module Test2 where

  import Issue481Record
  private
    open module Rec = Issue481Record

max_stars_repo_name: np/agda-git-experiment


text:
module Haskell.Prim.Word where

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Char
open import Agda.Builtin.String
open import Agda.Builtin.Unit
open import Agda.Builtin.Int using (pos; negsuc)

import Agda.Builtin.Word renaming (Word64 to Word; primWord64ToNat to w2n; primWord64FromNat to n2w)
open Agda.Builtin.Word
open Agda.Builtin.Word public using (Word)

open import Haskell.Prim
open import Haskell.Prim.Integer

--------------------------------------------------
-- Literals

private
  2⁶⁴ : Nat
  2⁶⁴ = 18446744073709551616

instance
  iNumberWord : Number Word
  iNumberWord .Number.Constraint n = IsTrue (n < 2⁶⁴)
  iNumberWord .fromNat n = n2w n

--------------------------------------------------
-- Arithmetic

negateWord : Word → Word
negateWord a = n2w (2⁶⁴ - w2n a)

addWord : Word → Word → Word
addWord a b = n2w (w2n a + w2n b)

subWord : Word → Word → Word
subWord a b = addWord a (negateWord b)

mulWord : Word → Word → Word
mulWord a b = n2w (w2n a * w2n b)

eqWord : Word → Word → Bool
eqWord a b = w2n a == w2n b

ltWord : Word → Word → Bool
ltWord a b = w2n a < w2n b

showWord : Word → List Char
showWord a = primStringToList (primShowNat (w2n a))

integerToWord : Integer → Word
integerToWord (pos n)    = n2w n
integerToWord (negsuc n) = negateWord (n2w (suc n))

wordToInteger : Word → Integer
wordToInteger n = pos (w2n n)


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

module Issue232 where

open import Common.Level

data T {ℓ} : {α : Set ℓ} → α → Set (lsuc ℓ) where
  c : {α : Set ℓ} {x : α} → T x


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

module Reader where

-- The reader monad (mainly used for nice syntax with idiom brackets)

open import Level

Reader : ∀ {r a} → Set r → Set a → Set (a ⊔ r)
Reader R A = R → A

module _ {r} {R′ : Set r} where
  R : ∀ {a} → Set a → Set (a ⊔ r)
  R = Reader R′

  pure : ∀ {a} {A : Set a} → A → R A
  pure x = λ _ → x
  {-# INLINE pure #-}

  _<*>_ : ∀ {a b} {A : Set a} {B : Set b}
        → R (A → B) → R A → R B
  f <*> g = λ x → f x (g x)
  {-# INLINE _<*>_ #-}

  _>>=_ : ∀ {a b} {A : Set a} {B : Set b}
        → R A → (A → R B) → R B
  f >>= k = λ x → k (f x) x
  {-# INLINE _>>=_ #-}

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
module AbstractTermination where

data Nat : Set where
  zero : Nat
  suc : Nat → Nat

mutual

  f : Nat → Nat
  f n = g n
    where
      abstract
        g : Nat → Nat
        g n = f n

-- Andreas, 2016-10-03 re issue #2231.
-- Should give termination error.
-- Wrong behavior with Agda-2.3.2.
-- Correct behavior from at least Agda-2.4.2.2.


text:
module TypesMore where

open import Basics
open import Types4

module DESC (I : Set) where

  data Desc : Set1 where
    inx : I -> Desc
    sg  : (A : Set)(D : A -> Desc) -> Desc
    _!_ : I -> Desc -> Desc

  Node : Desc -> (I -> Set) -> I -> Set
  Node (inx x) R i = x == i
  Node (sg A D) R i = Sg A \ a -> Node (D a) R i
  Node (x ! D) R i = R x * Node D R i

  data Mu (D : Desc)(i : I) : Set where
    [_] : Node D (Mu D) i -> Mu D i

  cata : forall D {X} -> ({i : I} -> Node D X i -> X i) ->
           forall {i} -> Mu D i -> X i
  mapCata : forall {D} E {X} -> ({i : I} -> Node D X i -> X i) ->
           forall {i} -> Node E (Mu D) i -> Node E X i
  cata D f [ x ] = f (mapCata D f x)
  mapCata (inx x) f q = q
  mapCata (sg A E) f (a , e) = a , mapCata (E a) f e
  mapCata (i ! E) f (x , e) = cata _ f x , mapCata E f e

  module ORN (J : Set)(ji : J -> I) where

    Hits : I -> Set
    Hits i = Sg J \ j -> ji j == i

    data Orn : Desc -> Set1 where
      inx : forall {i} -> Hits i -> Orn (inx i)
      sg  : forall A {D} -> ((a : A) -> Orn (D a)) -> Orn (sg A D)
      _!_ : forall {i D} -> Hits i -> Orn D -> Orn (i ! D)
      ins : forall (X : Set) {D} -> (X -> Orn D) -> Orn D
      del : forall {A D} a -> Orn (D a) -> Orn (sg A D)

open DESC

NatDesc : Desc One
NatDesc = sg Two \ { tt -> inx <> ; ff -> <> ! inx <> }

NAT : Set
NAT = Mu One NatDesc <>
pattern ZE = [ tt , refl ]
pattern SU n = [ ff , n , refl ]
PLUS : NAT -> NAT -> NAT
PLUS ZE y = y
PLUS (SU x) y = SU (PLUS x y)

open ORN

orned : forall {I D J ji} -> Orn I J ji D -> Desc J
orned (inx (j , q)) = inx j
orned (sg A D) = sg A \ a -> orned (D a)
orned ((j , q) ! O) = j ! orned O
orned (ins X O) = sg X \ x -> orned (O x)
orned (del a O) = orned O

ListOrn : Set -> Orn One One _ NatDesc
ListOrn X = sg Two \
  { tt -> inx (<> , refl)
  ; ff -> ins X \ _ -> (<> , refl) ! (inx (<> , refl))
  }

forget : forall {I D J ji} (O : Orn I J ji D) {P : I -> Set} ->
         {j : J} -> Node J (orned O) (\ j -> P (ji j)) j ->
                    Node I D P (ji j)
forget (inx (j , refl)) refl = refl
forget (sg A O) (a , o) = a , forget (O a) o
forget ((j , refl) ! O) (p , o) = p , forget O o
forget (ins X O) (x , o) = forget (O x) o
forget (del a O) o = a , forget O o

plain : forall {I D J ji} (O : Orn I J ji D)
        {j : J} -> Mu J (orned O) j -> Mu I D (ji j)
plain O = cata _ (orned O) (\ x -> [ forget O {Mu _ _} x ])


text:
-- Andreas, 2016-07-17 issue 2101

-- It should be possible to place a single function with a where block
-- inside `abstract`.

-- This will work if type signatures inside a where-block
-- are considered private, since in private type signatures,
-- abstract definitions are transparent.
-- (Unlike in public type signatures.)

record Wrap (A : Set) : Set where
  field unwrap : A

postulate
  P : ∀{A : Set} → A → Set

module AbstractPrivate (A : Set) where
  abstract
    B : Set
    B = Wrap A

    postulate
      b : B

    private -- this no longer (since #418) make abstract defs transparent in type signatures
      postulate
        test : P (Wrap.unwrap b) -- should no longer succeed

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2015-03-10, issue reported by Andrea Vezzosi

postulate
  X : Set

data D p : X → Set p where
  c : ∀ i → D _ i

-- WAS: internal error in Substitute.hs due to negative De Bruijn index

-- should work now