text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Lattice.Properties where

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

open import Cubical.Data.Sigma

open import Cubical.Structures.Axioms
open import Cubical.Structures.Auto
open import Cubical.Structures.Macro
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.CommMonoid
open import Cubical.Algebra.Semilattice
open import Cubical.Algebra.Lattice.Base

open import Cubical.Relation.Binary.Poset

private
  variable
    ℓ : Level

module LatticeTheory (L' : Lattice ℓ) where
 private L = fst L'
 open LatticeStr (snd L')

 0lLeftAnnihilates∧l : ∀ (x : L) → 0l ∧l x ≡ 0l
 0lLeftAnnihilates∧l x = 0l ∧l x          ≡⟨ cong (0l ∧l_) (sym (∨lLid _)) ⟩
                          0l ∧l (0l ∨l x) ≡⟨ ∧lAbsorb∨l _ _ ⟩
                          0l ∎

 0lRightAnnihilates∧l : ∀ (x : L) → x ∧l 0l ≡ 0l
 0lRightAnnihilates∧l _ = ∧lComm _ _ ∙ 0lLeftAnnihilates∧l _

 1lLeftAnnihilates∨l : ∀ (x : L) → 1l ∨l x ≡ 1l
 1lLeftAnnihilates∨l x = 1l ∨l x          ≡⟨ cong (1l ∨l_) (sym (∧lLid _)) ⟩
                          1l ∨l (1l ∧l x) ≡⟨ ∨lAbsorb∧l _ _ ⟩
                          1l ∎

 1lRightAnnihilates∨l : ∀ (x : L) → x ∨l 1l ≡ 1l
 1lRightAnnihilates∨l _ = ∨lComm _ _ ∙ 1lLeftAnnihilates∨l _

module Order (L' : Lattice ℓ) where
 private L = fst L'
 open LatticeStr (snd L')
 open JoinSemilattice (Lattice→JoinSemilattice L') renaming (_≤_ to _≤j_ ; IndPoset to JoinPoset)
 open MeetSemilattice (Lattice→MeetSemilattice L') renaming (_≤_ to _≤m_ ; IndPoset to MeetPoset)

 ≤j→≤m : ∀ x y → x ≤j y → x ≤m y
 ≤j→≤m x y x∨ly≡y = x ∧l y         ≡⟨ cong (x ∧l_) (sym x∨ly≡y) ⟩
                    x ∧l (x ∨l y) ≡⟨ ∧lAbsorb∨l _ _ ⟩
                    x ∎

 ≤m→≤j : ∀ x y → x ≤m y → x ≤j y
 ≤m→≤j x y x∧ly≡x = x ∨l y ≡⟨ ∨lComm _ _ ⟩
                    y ∨l x ≡⟨ cong (y ∨l_) (sym x∧ly≡x) ⟩
                    y ∨l (x ∧l y) ≡⟨ cong (y ∨l_) (∧lComm _ _) ⟩
                    y ∨l (y ∧l x) ≡⟨ ∨lAbsorb∧l _ _ ⟩
                    y ∎

 ≤Equiv : ∀ (x y : L) → (x ≤j y) ≃ (x ≤m y)
 ≤Equiv x y = propBiimpl→Equiv (isSetLattice L' _ _) (isSetLattice L' _ _) (≤j→≤m x y) (≤m→≤j x y)

 IndPosetPath : JoinPoset ≡ MeetPoset
 IndPosetPath = PosetPath _ _ .fst ((idEquiv _) , isposetequiv ≤Equiv )

 -- transport inequalities from ≤m to ≤j
 ∧lIsMinJoin : ∀ x y z → z ≤j x → z ≤j y → z ≤j x ∧l y
 ∧lIsMinJoin _ _ _ z≤jx z≤jy = ≤m→≤j _ _ (∧lIsMin _ _ _ (≤j→≤m _ _ z≤jx) (≤j→≤m _ _ z≤jy))

 ∧≤LCancelJoin : ∀ x y → x ∧l y ≤j y
 ∧≤LCancelJoin x y = ≤m→≤j _ _ (∧≤LCancel x y)

module _ {L M : Lattice ℓ} (φ ψ : LatticeHom L M) where
 open LatticeStr ⦃...⦄
 open IsLatticeHom
 private
   instance
     _ = L
     _ = M
     _ = snd L
     _ = snd M

 LatticeHom≡f : fst φ ≡ fst ψ → φ ≡ ψ
 LatticeHom≡f = Σ≡Prop λ f → isPropIsLatticeHom _ f _

ext: agda

max_stars_repo_name: FernandoLarrain/cubical


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

open import LogicalFormulae
open import Groups.Cosets
open import Groups.Homomorphisms.Definition
open import Rings.Homomorphisms.Definition
open import Groups.Lemmas
open import Groups.Definition
open import Setoids.Setoids
open import Setoids.Functions.Lemmas
open import Rings.Definition
open import Sets.EquivalenceRelations
open import Rings.Ideals.Definition
open import Fields.Fields
open import Fields.Lemmas
open import Rings.Cosets
open import Rings.Ideals.Maximal.Definition
open import Rings.Ideals.Lemmas
open import Rings.Ideals.Prime.Definition
open import Rings.IntegralDomains.Definition
open import Rings.Ideals.Prime.Lemmas

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

module Rings.Ideals.Maximal.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {pred : A → Set c} (i : Ideal R pred)  where

open Ring R
open Group additiveGroup
open Setoid S
open Equivalence eq

idealMaximalImpliesQuotientField : ({d : Level} → MaximalIdeal i {d}) → Field (cosetRing R i)
Field.allInvertible (idealMaximalImpliesQuotientField max) cosetA cosetA!=0 = ans' , ans''
  where
    gen : Ideal (cosetRing R i) (generatedIdealPred (cosetRing R i) cosetA)
    gen = generatedIdeal (cosetRing R i) cosetA
    inv : Ideal R (inverseImagePred {S = S} {T = cosetSetoid additiveGroup (Ideal.isSubgroup i)} (GroupHom.wellDefined (RingHom.groupHom (cosetRingHom R i))) (Ideal.isSubset gen))
    inv = inverseImageIsIdeal (cosetRing R i) (cosetRingHom R i) gen
    containsOnce : {a : A} → (Ideal.predicate i a) → (Ideal.predicate inv a)
    containsOnce {x} ix = x , ((x , Ideal.closedUnderPlus i (Ideal.closedUnderInverse i ix) (Ideal.isSubset i *Commutative (Ideal.accumulatesTimes i ix))) ,, Ideal.isSubset i (symmetric invLeft) (Ideal.containsIdentity i))
    notInI : A
    notInI = cosetA
    notInIIsInInv : Ideal.predicate inv notInI
    notInIIsInInv = cosetA , ((1R , Ideal.isSubset i {0R} (symmetric (transitive (+WellDefined reflexive (transitive *Commutative identIsIdent)) (invLeft {cosetA}))) (Ideal.containsIdentity i)) ,, Ideal.isSubset i (symmetric invLeft) (Ideal.containsIdentity i))
    notInIPr : (Ideal.predicate i notInI) → False
    notInIPr iInI = cosetA!=0 (Ideal.isSubset i (transitive (symmetric identLeft) (+WellDefined (symmetric (invIdent additiveGroup)) reflexive)) iInI)
    ans : {a : A} → Ideal.predicate inv a
    ans = MaximalIdeal.isMaximal max inv containsOnce (notInI , (notInIIsInInv ,, notInIPr))
    ans' : A
    ans' with ans {1R}
    ... | _ , ((b , _) ,, _) = b
    ans'' : pred (inverse (Ring.1R (cosetRing R i)) + (ans' * cosetA))
    ans'' with ans {1R}
    ans'' | a , ((b , predCAb-a) ,, pred1-a) = Ideal.isSubset i (transitive (+WellDefined (invContravariant additiveGroup) reflexive) (transitive +Associative (+WellDefined (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight)) *Commutative))) (Ideal.closedUnderPlus i (Ideal.closedUnderInverse i pred1-a) predCAb-a)
Field.nontrivial (idealMaximalImpliesQuotientField max) 1=0 = MaximalIdeal.notContainedIsNotContained max (Ideal.isSubset i (identIsIdent {MaximalIdeal.notContained (max {lzero})}) (Ideal.accumulatesTimes i p))
  where
    have : pred (inverse 1R)
    have = Ideal.isSubset i identRight 1=0
    p : pred 1R
    p = Ideal.isSubset i (invTwice additiveGroup 1R) (Ideal.closedUnderInverse i have)

quotientFieldImpliesIdealMaximal : Field (cosetRing R i) → ({d : _} → MaximalIdeal i {d})
MaximalIdeal.notContained (quotientFieldImpliesIdealMaximal f) = Ring.1R (cosetRing R i)
MaximalIdeal.notContainedIsNotContained (quotientFieldImpliesIdealMaximal f) p1R = Field.nontrivial f (memberDividesImpliesMember R i p1R ((inverse 1R + 0R) , identIsIdent))
MaximalIdeal.isMaximal (quotientFieldImpliesIdealMaximal f) {bigger} biggerIdeal contained (a , (biggerA ,, notPredA)) = Ideal.isSubset biggerIdeal identIsIdent (Ideal.accumulatesTimes biggerIdeal v)
  where
    inv : Sg A (λ t → pred (inverse 1R + (t * a)))
    inv = Field.allInvertible f a λ r → notPredA (translate' R i r)
    r : A
    r = underlying inv
    s : pred (inverse 1R + (r * a))
    s with inv
    ... | _ , p = p
    t : bigger (inverse 1R + (r * a))
    t = contained s
    u : bigger (inverse (r * a))
    u = Ideal.closedUnderInverse biggerIdeal (Ideal.isSubset biggerIdeal *Commutative (Ideal.accumulatesTimes biggerIdeal biggerA))
    v : bigger 1R
    v = Ideal.isSubset biggerIdeal (invTwice additiveGroup 1R) (Ideal.closedUnderInverse biggerIdeal (Ideal.isSubset biggerIdeal (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight)) (Ideal.closedUnderPlus biggerIdeal t u)))

idealMaximalImpliesIdealPrime : ({d : _} → MaximalIdeal i {d}) → PrimeIdeal i
idealMaximalImpliesIdealPrime max = quotientIntDomImpliesIdealPrime i (fieldIsIntDom (idealMaximalImpliesQuotientField max))

maximalIdealWellDefined : {d : _} {pred2 : A → Set d} (i2 : Ideal R pred2) → ({x : A} → pred x → pred2 x) → ({x : A} → pred2 x → pred x) → {e : _} → MaximalIdeal i {e} → MaximalIdeal i2 {e}
MaximalIdeal.notContained (maximalIdealWellDefined i2 pToP2 p2ToP record { notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained ; isMaximal = isMaximal }) = notContained
MaximalIdeal.notContainedIsNotContained (maximalIdealWellDefined i2 pToP2 p2ToP record { notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained ; isMaximal = isMaximal }) p2Not = notContainedIsNotContained (p2ToP p2Not)
MaximalIdeal.isMaximal (maximalIdealWellDefined i2 pToP2 p2ToP record { notContained = notContained ; notContainedIsNotContained = notContainedIsNotContained ; isMaximal = isMaximal }) {biggerPred} bigger pred2InBigger (r , (biggerPredR ,, notP2r)) {x} = isMaximal bigger (λ p → pred2InBigger (pToP2 p)) (r , (biggerPredR ,, λ p → notP2r (pToP2 p)))


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

char : Char → Set
char 'A' with 'O'
char _ | _ = Char
char _ = Char

lit : Nat → Set
lit 5 with 0
lit _ | _ = Nat
lit _ = Nat

con : Nat → Set
con zero    with zero
con _       | _ = Nat
con (suc x) with zero
con _       | _ = Nat

record R : Set where
  coinductive -- disallow matching
  field f : Bool
        n : Nat

data P (r : R) : Nat → Set where
  fTrue  : R.f r ≡ true → P r zero
  nSuc   : P r (suc (R.n r))

data Q : (b : Bool) (n : Nat) →  Set where
  true! : Q true zero
  suc!  : ∀{b n} → Q b (suc n)

test : (r : R) {n : Nat} (p : P r n) → Q (R.f r) n
test r nSuc       = suc!
test r (fTrue p)  with R.f r
test _ (fTrue ()) | false
test _ _          | true = true!  -- underscore instead of (isTrue _)

-- -- Note that `with` first and then splitting on p does not work:
--
-- foo :  (r : R) {n : Nat} (p : P r n) → Q (R.f r) n
-- foo r p with R.f r
-- foo r (fTrue x) | false = {!x!}  -- cannot split on x
-- foo r (fTrue _) | true  = true!
-- foo r nSuc      | _     = suc!

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Agda.Builtin.List
open import Agda.Builtin.Reflection

macro

  print : (Set → Set) → Term → TC _
  print t _ = bindTC (quoteTC t) λ t →
              typeError (termErr t ∷ [])

-- Prints λ { X → X }.

Test₁ : Set
Test₁ = {!print (λ { X → X })!}

module _ (A : Set) where

  -- Prints λ { A₁ X → X }.

  Test₂ : Set
  Test₂ = {!print (λ { X → X })!}

  -- Prints λ { B₁ X → X } B.

  Test₃ : Set → Set
  Test₃ B = {!print (λ { X → X })!}

module _ (A : Set) where

  -- Prints λ { A₁ X → A₁ }. Note that A is not mentioned at all.

  Test₄ : Set
  Test₄ = {!print (λ { X → A })!}

  -- Prints λ { B₁ X → A } B.

  Test₅ : Set → Set
  Test₅ B = {!print (λ { X → A })!}

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Number.Instances.QuoInt where

open import Cubical.Foundations.Everything hiding (⋆) renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Foundations.Logic renaming (inl to inlᵖ; inr to inrᵖ)

open import Cubical.Relation.Nullary.Base renaming (¬_ to ¬ᵗ_)
open import Cubical.Relation.Binary.Base
open import Cubical.Data.Sum.Base renaming (_⊎_ to infixr 4 _⊎_)
open import Cubical.Data.Sigma.Base renaming (_×_ to infixr 4 _×_)
open import Cubical.Data.Sigma
open import Cubical.Data.Bool as Bool using (Bool; not; true; false)
open import Cubical.Data.Empty renaming (elim to ⊥-elim; ⊥ to ⊥⊥) -- `⊥` and `elim`
open import Cubical.Foundations.Logic renaming (¬_ to ¬ᵖ_; inl to inlᵖ; inr to inrᵖ)
open import Function.Base using (it; _∋_; _$_)
open import Cubical.Foundations.Isomorphism

open import Cubical.HITs.PropositionalTruncation --.Properties

open import Utils using (!_; !!_)
open import MoreLogic.Reasoning
open import MoreLogic.Definitions
open import MoreLogic.Properties
open import MorePropAlgebra.Definitions hiding (_≤''_)
open import MorePropAlgebra.Structures
open import MorePropAlgebra.Bundles
open import MorePropAlgebra.Consequences
open import Number.Structures2
open import Number.Bundles2

open import Cubical.Data.Nat.Literals
open import Cubical.Data.Nat using (suc; zero; ℕ; HasFromNat)
open import Number.Prelude.Nat using (¬-<ⁿ-zero; +ⁿ-comm; ¬suc<ⁿ0; _+ⁿ_; _·ⁿ_; ·ⁿ-reflects-≡ˡ')
open import Number.Instances.QuoIntFromInt public
open import Cubical.HITs.Ints.QuoInt as QuoInt using
  ( ℤ
  ; HasFromNat
  ; _+_
  ; Int≡ℤ
  ; signed
  ; posneg
  ; ℤ→Int
  ; sucℤ
  ; predℤ
  ; sign
  ; abs
  ; pos
  ; neg
  ; +-comm
  ; +-assoc
  ; sucℤ-+ʳ
  ; sucℤ-+ˡ
  ; spos
  ; sneg
  ; *-pos-suc
  ; negate-invol
  ) renaming
  ( isSetℤ to is-set
  ; _*_ to _·_
  ; -_ to infixl 6 -_
  ; *-comm to ·-comm
  )
open IsLinearlyOrderedCommRing is-LinearlyOrderedCommRing using
  ( _-_
  ; <-irrefl
  ; <-trans
  ; +-<-ext
  ; +-rinv
  ; +-identity
  ; ·-identity
  ; _≤_
  ; ·-preserves-<
  ; <-tricho
  ; <-asym
  ; _#_
  ; +-inverse
  ; ·-assoc
  )

0<1 : [ 0 < 1 ]
0<1 = 0 , refl

-- TODO: import these properties from somewhere else
+-reflects-<      : ∀ x y z → [ (x + z < y + z) ⇒ (    x < y    ) ]
+-preserves-<     : ∀ x y z → [ (    x < y    ) ⇒ (x + z < y + z) ]
+-creates-<       : ∀ x y z → [ (    x < y    ) ⇔ (x + z < y + z) ]

+-preserves-< a b x = snd (
  ( a            <  b           ) ⇒ᵖ⟨ transport (λ i → [ sym (fst (+-identity a)) i < sym (fst (+-identity b)) i ]) ⟩
  ( a +    0     <  b +    0    ) ⇒ᵖ⟨ transport (λ i → [ a + sym (+-rinv x) i < b + sym (+-rinv x) i ]) ⟩
  ( a + (x  - x) <  b + (x  - x)) ⇒ᵖ⟨ transport (λ i → [ +-assoc a x (- x) i < +-assoc b x (- x) i ]) ⟩
  ((a +  x) - x  < (b +  x) - x ) ⇒ᵖ⟨ +-<-ext (a + x) (- x) (b + x) (- x) ⟩
  ((a + x < b + x) ⊔ (- x < - x)) ⇒ᵖ⟨ (λ q → case q as (a + x < b + x) ⊔ (- x < - x) ⇒ a + x < b + x of λ
                                      { (inl a+x<b+x) → a+x<b+x -- somehow ⊥-elim needs a hint in the next line
                                      ; (inr  -x<-x ) → ⊥-elim {A = λ _ → [ a + x < b + x ]} (<-irrefl (- x) -x<-x)
                                      }) ⟩
   a + x < b + x ◼ᵖ)

+-reflects-< x y z = snd
  ( x + z < y + z              ⇒ᵖ⟨ +-preserves-< (x + z) (y + z) (- z) ⟩
    (x + z) - z  < (y + z) - z ⇒ᵖ⟨ transport (λ i → [ +-assoc x z (- z) (~ i) < +-assoc y z (- z) (~ i) ]) ⟩
    x + (z - z) < y + (z - z)  ⇒ᵖ⟨ transport (λ i → [ x + +-rinv z i < y + +-rinv z i ]) ⟩
    x + 0 < y + 0              ⇒ᵖ⟨ transport (λ i → [ fst (+-identity x) i < fst (+-identity y) i ]) ⟩
    x < y                      ◼ᵖ)

+-creates-< x y z .fst = +-preserves-< x y z
+-creates-< x y z .snd = +-reflects-<  x y z

suc-creates-< : ∀ x y → [ (x < y) ⇔ (sucℤ x < sucℤ y) ]
suc-creates-< x y .fst p = substₚ (λ p → sucℤ x < p) (∣ +-comm y (pos 1) ∣) $ substₚ (λ p → p < y + pos 1) (∣ +-comm x (pos 1) ∣) (+-preserves-< x y (pos 1) p)
suc-creates-< x y .snd p = +-reflects-< x y (pos 1) $ substₚ (λ p → p < y + pos 1) (∣ +-comm (pos 1) x ∣) $ substₚ (λ p → sucℤ x < p) (∣ +-comm (pos 1) y ∣) p

·-creates-< : ∀ a b x → [ 0 < x ] → [ (a < b) ⇔ ((a · x) < (b · x)) ]
·-creates-< a b x p .fst q = ·-preserves-< a b x p q
·-creates-< a b x p .snd q = ·-reflects-< a b x p q

·-creates-<ˡ : ∀ a b x → [ 0 < x ] → [ (a < b) ⇔ ((x · a) < (x · b)) ]
·-creates-<ˡ a b x p .fst q = transport (λ i → [ ·-comm a x i < ·-comm b x i ]) $ ·-preserves-< a b x p q
·-creates-<ˡ a b x p .snd q = ·-reflects-< a b x p (transport (λ i → [ ·-comm x a i < ·-comm x b i ]) q)

·-creates-<-≡ : ∀ a b x → [ 0 < x ] → (a < b) ≡ ((a · x) < (b · x))
·-creates-<-≡ a b x p = ⇔toPath' (·-creates-< a b x p)

·-creates-<ˡ-≡ : ∀ a b x → [ 0 < x ] → (a < b) ≡ ((x · a) < (x · b))
·-creates-<ˡ-≡ a b x p = ⇔toPath' (·-creates-<ˡ a b x p)

+-creates-≤ : ∀ a b x → [ (a ≤ b) ⇔ ((a + x) ≤ (b + x)) ]
+-creates-≤ a b x = {!   !}

·-creates-≤ : ∀ a b x → [ 0 ≤ x ] → [ (a ≤ b) ⇔ ((a · x) ≤ (b · x)) ]
·-creates-≤ a b x 0≤x .fst p = {!   !}
·-creates-≤ a b x 0≤x .snd p = {!   !}

·-creates-≤-≡ : ∀ a b x → [ 0 ≤ x ] → (a ≤ b) ≡ ((a · x) ≤ (b · x))
·-creates-≤-≡ a b x 0≤x = uncurry ⇔toPath $ ·-creates-≤ a b x 0≤x

≤-dicho : ∀ x y → [ (x ≤ y) ⊔ (y ≤ x) ]
≤-dicho x y with <-tricho x y
... | inl (inl x<y) = inlᵖ $ <-asym x y x<y
... | inl (inr y<x) = inrᵖ $ <-asym y x y<x
... | inr      x≡y  = inlᵖ $ subst (λ p → [ ¬(p < x) ]) x≡y (<-irrefl x)

ℤlattice : Lattice {ℓ-zero} {ℓ-zero}
ℤlattice = record { LinearlyOrderedCommRing bundle renaming (≤-Lattice to is-Lattice) }

open import MorePropAlgebra.Properties.Lattice ℤlattice
open OnSet is-set hiding (+-min-distribʳ; ·-min-distribʳ; +-max-distribʳ; ·-max-distribʳ)

≤-min-+ : ∀ a b c w → [ w ≤ (a + c) ] → [ w ≤ (b + c) ] → [ w ≤ (min a b + c) ]
≤-max-+ : ∀ a b c w → [ (a + c) ≤ w ] → [ (b + c) ≤ w ] → [ (max a b + c) ≤ w ]
≤-min-· : ∀ a b c w → [ w ≤ (a · c) ] → [ w ≤ (b · c) ] → [ w ≤ (min a b · c) ]
≤-max-· : ∀ a b c w → [ (a · c) ≤ w ] → [ (b · c) ≤ w ] → [ (max a b · c) ≤ w ]

≤-min-+ = OnType.≤-dicho⇒+.≤-min-+ _+_ ≤-dicho
≤-max-+ = OnType.≤-dicho⇒+.≤-max-+ _+_ ≤-dicho
≤-min-· = OnType.≤-dicho⇒·.≤-min-· _·_ ≤-dicho
≤-max-· = OnType.≤-dicho⇒·.≤-max-· _·_ ≤-dicho

+-min-distribʳ : ∀ x y z             → (min x y + z) ≡ min (x + z) (y + z)
·-min-distribʳ : ∀ x y z → [ 0 ≤ z ] → (min x y · z) ≡ min (x · z) (y · z)
+-max-distribʳ : ∀ x y z             → (max x y + z) ≡ max (x + z) (y + z)
·-max-distribʳ : ∀ x y z → [ 0 ≤ z ] → (max x y · z) ≡ max (x · z) (y · z)
+-min-distribˡ : ∀ x y z             → (z + min x y) ≡ min (z + x) (z + y)
·-min-distribˡ : ∀ x y z → [ 0 ≤ z ] → (z · min x y) ≡ min (z · x) (z · y)
+-max-distribˡ : ∀ x y z             → (z + max x y) ≡ max (z + x) (z + y)
·-max-distribˡ : ∀ x y z → [ 0 ≤ z ] → (z · max x y) ≡ max (z · x) (z · y)

+-min-distribʳ = OnSet.+-min-distribʳ is-set _+_ +-creates-≤ ≤-min-+
·-min-distribʳ = OnSet.·-min-distribʳ is-set 0 _·_ ·-creates-≤ ≤-min-·
+-max-distribʳ = OnSet.+-max-distribʳ is-set _+_ +-creates-≤ ≤-max-+
·-max-distribʳ = OnSet.·-max-distribʳ is-set 0 _·_ ·-creates-≤ ≤-max-·

+-min-distribˡ x y z   = +-comm z (min x y) ∙ +-min-distribʳ x y z   ∙ (λ i → min (+-comm x z i) (+-comm y z i))
·-min-distribˡ x y z p = ·-comm z (min x y) ∙ ·-min-distribʳ x y z p ∙ (λ i → min (·-comm x z i) (·-comm y z i))
+-max-distribˡ x y z   = +-comm z (max x y) ∙ +-max-distribʳ x y z   ∙ (λ i → max (+-comm x z i) (+-comm y z i))
·-max-distribˡ x y z p = ·-comm z (max x y) ∙ ·-max-distribʳ x y z p ∙ (λ i → max (·-comm x z i) (·-comm y z i))

pos<pos[suc] : ∀ x → [ pos x < pos (suc x) ]
pos<pos[suc] 0 = 0<1
pos<pos[suc] (suc x) = suc-creates-< (pos x) (pos (suc x)) .fst (pos<pos[suc] x)

0<ᶻpos[suc] : ∀ x → [ 0 < pos (suc x) ]
0<ᶻpos[suc]      0  = 0<1
0<ᶻpos[suc] (suc x) = <-trans 0 (pos (suc x)) (pos (suc (suc x))) (0<ᶻpos[suc] x) (suc-creates-< (pos x) (pos (suc x)) .fst (pos<pos[suc] x))

·-nullifiesˡ : ∀(x : ℤ) → 0 · x ≡ 0
·-nullifiesˡ (pos zero) = refl
·-nullifiesˡ (neg zero) = refl
·-nullifiesˡ (posneg i) = refl
·-nullifiesˡ (pos (suc n)) = refl
·-nullifiesˡ (neg (suc n)) = sym posneg

·-nullifiesʳ : ∀(x : ℤ) → x · 0 ≡ 0
·-nullifiesʳ x = ·-comm x 0 ∙ ·-nullifiesˡ x

·-preserves-0< : ∀ a b → [ 0 < a ] → [ 0 < b ] → [ 0 < a · b ]
·-preserves-0< a b p q = subst (λ p → [ p < a · b ]) (·-nullifiesˡ b) (·-preserves-< 0 a b q p)

private
  term : ∀ b x → Type ℓ-zero
  term b x = [ ((pos 0 < x) ⇒ (pos 0 < b)) ⊓ ((pos 0 < b) ⇒ (pos 0 < x)) ]

·-reflects-<ˡ : (x y z : ℤ) → [ pos 0 < z ] → [ z · x < z · y ] → [ x < y ]
·-reflects-<ˡ x y z p q = ·-reflects-< x y z p  (transport (λ i → [ ·-comm z x i < ·-comm z y i ]) q)

-flips-<0 : ∀ x → [ (x < 0) ⇔ (0 < (- x)) ]
-flips-<0 (signed spos zero) = (λ x → x) , (λ x → x)
-flips-<0 (signed sneg zero) = (λ x → x) , (λ x → x)
-flips-<0 (ℤ.posneg i)       = (λ x → x) , (λ x → x)
-flips-<0 (signed spos (suc n)) .fst p  = ¬-<ⁿ-zero p
-flips-<0 (signed sneg (suc n)) .fst tt = n , +ⁿ-comm n 1
-flips-<0 (signed sneg (suc n)) .snd p  = tt

-- NOTE: this could be a path, if we make `+-creates-<` into a path
-flips-< : ∀ x y → [ x < y ] → [ - y < - x ]
-flips-< x y p = (
  (    x            < y    ) ⇒ᵖ⟨ +-creates-< x y (- y) .fst ⟩
  (    x  - y       < y - y) ⇒ᵖ⟨ transport (λ i → [ +-comm x (- y) i < +-rinv y i ]) ⟩
  ( (- y) + x       < 0    ) ⇒ᵖ⟨ +-creates-< ((- y) + x) 0 (- x) .fst ⟩
  (((- y) + x) - x  < 0 - x) ⇒ᵖ⟨ transport (λ i → [ +-assoc (- y) x (- x) (~ i) < +-identity (- x) .snd i ]) ⟩
  ( (- y) + (x - x) < - x  ) ⇒ᵖ⟨ transport (λ i → [ (- y) + +-rinv x i < - x ]) ⟩
  ( (- y) +    0    < - x  ) ⇒ᵖ⟨ transport (λ i → [ +-identity (- y) .fst i < - x ]) ⟩
  (  - y            < - x  ) ◼ᵖ) .snd p

-flips-<-⇔ : ∀ x y → [ (x < y) ⇔ (- y < - x) ]
-flips-<-⇔ x y .fst = -flips-< x y
-flips-<-⇔ x y .snd p = transport (λ i → [ negate-invol x i < negate-invol y i ]) $ -flips-< (- y) (- x) p

-flips-<-≡ : ∀ x y → (x < y) ≡ (- y < - x)
-flips-<-≡ x y = ⇔toPath' (-flips-<-⇔ x y)

-identity-· : ∀ a → (- 1) · a ≡ - a
-identity-· (pos zero) j = posneg (~ i0 ∨ ~ j)
-identity-· (neg zero) j = posneg (~ i1 ∨ ~ j)
-identity-· (posneg i) j = posneg (~ i  ∨ ~ j)
-identity-· (pos (suc n)) i = neg (suc (+ⁿ-comm n 0 i))
-identity-· (neg (suc n)) i = pos (suc (+ⁿ-comm n 0 i))

-distˡ : ∀ a b → -(a · b) ≡ (- a) · b
-distˡ a b =
  -(a · b)        ≡⟨ sym $ -identity-· (a · b) ⟩
  (- 1) · (a · b) ≡⟨ ·-assoc (- 1) a b ⟩
  ((- 1) · a) · b ≡⟨ (λ i → -identity-· a i · b) ⟩
  (- a) · b       ∎

private
  lem : ∀ z → [ z < 0 ] → [ 0 < - z ]
  lem z p = subst (λ p → [ p < - z ]) (sym posneg) $ -flips-< z 0 p

·-creates-<-flippedˡ-≡ : (x y z : ℤ) → [ z < 0 ] → (z · x < z · y) ≡ (y < x)
·-creates-<-flippedˡ-≡ x y z p =
     z  · x  <    z ·  y  ≡⟨ -flips-<-≡ (z · x) (z · y) ⟩
  - (z  · y) < - (z ·  x) ≡⟨ (λ i → -distˡ z y i < -distˡ z x i) ⟩
  (- z) · y  < (- z) · x  ≡⟨ sym $ ·-creates-<ˡ-≡ y x (- z) (lem z p) ⟩
          y  <         x  ∎

·-creates-<-flippedʳ-≡ : (x y z : ℤ) → [ z < 0 ] → (x · z < y · z) ≡ (y < x)
·-creates-<-flippedʳ-≡ x y z p = (λ i → ·-comm x z i < ·-comm y z i) ∙ ·-creates-<-flippedˡ-≡ x y z p

·-reflects-<-flippedˡ : (x y z : ℤ) → [ z < 0 ] → [ z · x < z · y ] → [ y < x ]
·-reflects-<-flippedˡ x y z p q = pathTo⇒ (·-creates-<-flippedˡ-≡ x y z p) q
  --   (z  · x  <    z ·  y  ⇒ᵖ⟨ -flips-< (z · x) (z · y) ⟩
  -- - (z  · y) < - (z ·  x) ⇒ᵖ⟨ transport (λ i → [ -distˡ z y i < -distˡ z x i ]) ⟩
  -- (- z) · y  < (- z) · x  ⇒ᵖ⟨ ·-creates-<ˡ y x (- z) (lem z p) .snd ⟩
  --         y  <         x  ◼ᵖ) .snd q

·-reflects-<-flippedʳ : (x y z : ℤ) → [ z < 0 ] → [ x · z < y · z ] → [ y < x ]
·-reflects-<-flippedʳ x y z p q = ·-reflects-<-flippedˡ x y z p (transport (λ i → [ ·-comm x z i < ·-comm y z i ]) q)

-- ·-preserves-<-flippedˡ : (x y z : ℤ) → [ z < 0 ] → [ x < y ] → [ z · y < z · x ]
-- ·-preserves-<-flippedˡ x y z p q = {!   !}

·-reflects-0< : ∀ a b → [ 0 < a · b ] → [ ((0 < a) ⇔ (0 < b)) ⊓ ((a < 0) ⇔ (b < 0)) ]
·-reflects-0< a b p .fst .fst q = ·-reflects-<ˡ 0 b a q (transport (λ i → [ ·-nullifiesʳ a (~ i) < a · b ]) p)
·-reflects-0< a b p .fst .snd q = ·-reflects-<  0 a b q (transport (λ i → [ ·-nullifiesˡ b (~ i) < a · b ]) p)
·-reflects-0< a b p .snd .fst q = ·-reflects-<-flippedˡ 0 b a q (transport (λ i → [ ·-nullifiesʳ a (~ i) < a · b ]) p)
·-reflects-0< a b p .snd .snd q = ·-reflects-<-flippedʳ 0 a b q (transport (λ i → [ ·-nullifiesˡ b (~ i) < a · b ]) p)

#-dicho : ∀ x → [ x # 0 ] ⊎ (x ≡ 0)
#-dicho x = <-tricho x 0

⊕-identityʳ : ∀ s → (s Bool.⊕ spos) ≡ s
⊕-identityʳ spos = refl
⊕-identityʳ sneg = refl

·-preserves-signˡ : ∀ x y → [ 0 < y ] → sign (x · y) ≡ sign x
·-preserves-signˡ x (signed spos zero) p = ⊥-elim {A = λ _ → sign (x · ℤ.posneg i0) ≡ sign x} (¬-<ⁿ-zero p)
·-preserves-signˡ x (signed sneg  zero) p = ⊥-elim {A = λ _ → sign (x · ℤ.posneg i1) ≡ sign x} (¬-<ⁿ-zero p)
·-preserves-signˡ x (ℤ.posneg i)        p = ⊥-elim {A = λ _ → sign (x · ℤ.posneg i ) ≡ sign x} (¬-<ⁿ-zero p)
·-preserves-signˡ (signed spos zero) (signed spos (suc n)) p = refl
·-preserves-signˡ (signed sneg  zero) (signed spos (suc n)) p = refl
·-preserves-signˡ (ℤ.posneg i)        (signed spos (suc n)) p = refl
·-preserves-signˡ (signed s (suc n₁)) (signed spos (suc n)) p = ⊕-identityʳ s

#⇒≢ : ∀ x → [ x # 0 ] → ¬ᵗ(0 ≡ x)
#⇒≢ x (inl p) q = <-irrefl 0 $ subst (λ p → [ p < pos 0 ]) (sym q) p
#⇒≢ x (inr p) q = <-irrefl 0 $ subst (λ p → [ pos 0 < p ]) (sym q) p

<-split-pos : ∀ z → [ 0 < z ] → Σ[ n ∈ ℕ ] z ≡ pos (suc n)
<-split-pos (pos zero)    p = ⊥-elim {A = λ _ → Σ[ n ∈ ℕ ] posneg i0 ≡ pos (suc n)} (<-irrefl 0 p)
<-split-pos (neg zero)    p = ⊥-elim {A = λ _ → Σ[ n ∈ ℕ ] posneg i1 ≡ pos (suc n)} (<-irrefl 0 p)
<-split-pos (posneg i)    p = ⊥-elim {A = λ _ → Σ[ n ∈ ℕ ] posneg i  ≡ pos (suc n)} (<-irrefl 0 p)
<-split-pos (pos (suc n)) p = n , refl

<-split-neg : ∀ z → [ z < 0 ] → Σ[ n ∈ ℕ ] z ≡ neg (suc n)
<-split-neg (pos zero)    p = ⊥-elim {A = λ _ → Σ[ n ∈ ℕ ] posneg i0   ≡ neg (suc n)} (<-irrefl 0 p)
<-split-neg (neg zero)    p = ⊥-elim {A = λ _ → Σ[ n ∈ ℕ ] posneg i1   ≡ neg (suc n)} (<-irrefl 0 p)
<-split-neg (posneg i)    p = ⊥-elim {A = λ _ → Σ[ n ∈ ℕ ] posneg i    ≡ neg (suc n)} (<-irrefl 0 p)
<-split-neg (pos (suc m)) p = ⊥-elim {A = λ _ → Σ[ n ∈ ℕ ] pos (suc m) ≡ neg (suc n)} (¬suc<ⁿ0 m p)
<-split-neg (neg (suc m)) p = m , refl

#-split-abs : ∀ a → [ a # 0 ] → Σ[ x ∈ _ ] (abs a ≡ suc (abs x))
#-split-abs a (inl a<0) with <-split-neg a a<0; ... | (n , p) = neg n , λ i → abs (p i)
#-split-abs a (inr 0<a) with <-split-pos a 0<a; ... | (n , p) = pos n , λ i → abs (p i)

-- this is  QuoInt.signed-zero
signed0≡0 : ∀ s → signed s 0 ≡ 0
signed0≡0 spos   = refl
signed0≡0 sneg i = posneg (~ i)

·-sucIntʳ⁺ : ∀ m n → m · pos (suc n) ≡ m + m · pos n
·-sucIntʳ⁺ m n = ·-comm m (pos (suc n)) ∙ *-pos-suc n m ∙ (λ i → m + ·-comm (pos n) m i)

signed-respects-+ : ∀ s a b → signed s (a +ⁿ b) ≡ signed s a + signed s b
signed-respects-+ spos  zero   b   = refl
signed-respects-+ sneg  zero   b   = refl
signed-respects-+ spos (suc a) b i = sucℤ  $ signed-respects-+ spos a b i
signed-respects-+ sneg (suc a) b i = predℤ $ signed-respects-+ sneg a b i

-- this is QuoInt.signed-inv
sign-abs-identity : ∀ a → signed (sign a) (abs a) ≡ a
sign-abs-identity (pos zero) j  = posneg (i0 ∧ j)
sign-abs-identity (neg zero) j  = posneg (i1 ∧ j)
sign-abs-identity (posneg i) j  = posneg (i  ∧ j)
sign-abs-identity (pos (suc n)) = refl
sign-abs-identity (neg (suc n)) = refl

signed-reflects-≡₁ : ∀ s₁ s₂ n → signed s₁ (suc n) ≡ signed s₂ (suc n) → s₁ ≡ s₂
signed-reflects-≡₁ s₁ s₂ n p i = sign (p i)

signed-reflects-≡₂ : ∀ s₁ s₂ a b → signed s₁ a ≡ signed s₂ b → a ≡ b
signed-reflects-≡₂ s₁ s₂ a b p i = abs (p i)

-abs : ∀ a → abs (- a) ≡ abs a
-abs (signed s n) = refl
-abs (posneg i) = refl

-reflects-≡ : ∀ a b → - a ≡ - b → a ≡ b
-reflects-≡ a b p = sym (negate-invol a) ∙ (λ i → - p i) ∙ negate-invol b

abs-preserves-· : ∀ a b → abs (a · b) ≡ abs a ·ⁿ abs b
abs-preserves-· a b = refl

sign-abs-≡ : ∀ a b → sign a ≡ sign b → abs a ≡ abs b → a ≡ b
sign-abs-≡ a b p q = transport (λ i → sign-abs-identity a i ≡ sign-abs-identity b i) λ i → signed (p i) (q i)

0<-sign : ∀ z → [ 0 < z ] → sign z ≡ spos
0<-sign z p i = sign $ <-split-pos z p .snd i

<0-sign : ∀ z → [ z < 0 ] → sign z ≡ sneg
<0-sign z p i = sign $ <-split-neg z p .snd i

sign-pos : ∀ n → sign (pos n) ≡ spos
sign-pos zero = refl
sign-pos (suc n) = refl

-- inj-*sm : l * suc m ≡ n * suc m → l ≡ n
-- inj-*sm {zero} {m} {n} p = 0≡n*sm→0≡n p
-- inj-*sm {l} {m} {zero} p = sym (0≡n*sm→0≡n (sym p))
-- inj-*sm {suc l} {m} {suc n} p = cong suc (inj-*sm (inj-m+ {m = suc m} p))

private
  lem1 : ∀ a x → sign a ≡ sign (signed (sign a) (abs a +ⁿ x ·ⁿ abs a))
  lem1 (pos zero)    x = sym $ sign-pos (x ·ⁿ 0)
  lem1 (neg zero)    x = sym $ sign-pos (x ·ⁿ 0)
  lem1 (posneg i)    x = sym $ sign-pos (x ·ⁿ 0)
  lem1 (pos (suc n)) x = refl
  lem1 (neg (suc n)) x = refl

·-reflects-≡ˡ⁺ : ∀ a b x → (pos (suc x)) · a ≡ (pos (suc x)) · b → a ≡ b
·-reflects-≡ˡ⁺ a b x p = sym (sign-abs-identity a) ∙ (λ i → signed (κ i) (γ i)) ∙ sign-abs-identity b where
  φ : suc x ·ⁿ abs a ≡ suc x ·ⁿ abs b
  φ = signed-reflects-≡₂ _ _ _ _ p
  γ : abs a ≡ abs b
  γ = ·ⁿ-reflects-≡ˡ' {x} {abs a} {abs b} φ
  κ = transport ( sign (signed (sign a) (suc x ·ⁿ abs a))
                ≡ sign (signed (sign b) (suc x ·ⁿ abs b)) ≡⟨ (λ i → lem1 a x (~ i) ≡ lem1 b x (~ i)) ⟩
                  sign a ≡ sign b                         ∎) (λ i → sign (p i))

·-reflects-≡ˡ⁻ : ∀ a b x → (neg (suc x)) · a ≡ (neg (suc x)) · b → a ≡ b
·-reflects-≡ˡ⁻ a b x p = sym (sign-abs-identity a) ∙ γ ∙ sign-abs-identity b  where
  φ : suc x ·ⁿ abs a ≡ suc x ·ⁿ abs b
  φ = signed-reflects-≡₂ _ _ _ _ p
  κ : abs a ≡ abs b
  κ = ·ⁿ-reflects-≡ˡ' {x} {abs a} {abs b} φ
  γ : signed (sign a) (abs a) ≡ signed (sign b) (abs b)
  γ with #-dicho a
  ... | inl a#0 = -reflects-≡ _ _ (λ i → signed (θ i) (κ i)) where
    abstract
      c = #-split-abs a a#0 .fst
      q₁ : abs a ≡ suc (abs c)
      q₁ = #-split-abs a a#0 .snd
      q₂ : abs b ≡ suc (abs c)
      q₂ = sym κ ∙ q₁
    θ : not (sign a) ≡ not (sign b)
    θ = signed-reflects-≡₁ _ _ _ (transport (λ i → signed (not (sign a)) (suc x ·ⁿ q₁ i) ≡ signed (not (sign b)) (suc x ·ⁿ q₂ i)) p)
  ... | inr a≡0 = cong₂ signed refl (λ i → abs (a≡0 i)) ∙ signed0≡0 (sign a) ∙ sym (signed0≡0 (sign b)) ∙ cong₂ signed refl ((λ i → abs (a≡0 (~ i))) ∙ κ)

·-reflects-≡ˡ : ∀ a b x → [ x # 0 ] → x · a ≡ x · b → a ≡ b
·-reflects-≡ˡ a b x (inl x<0) q = let (y , r) = <-split-neg x x<0 in ·-reflects-≡ˡ⁻ a b y (transport (λ i → r i · a ≡ r i · b) q)
·-reflects-≡ˡ a b x (inr 0<x) q = let (y , r) = <-split-pos x 0<x in ·-reflects-≡ˡ⁺ a b y (transport (λ i → r i · a ≡ r i · b) q)

·-reflects-≡ʳ : ∀ a b x → [ x # 0 ] → a · x ≡ b · x → a ≡ b
·-reflects-≡ʳ a b x p q = ·-reflects-≡ˡ a b x p (·-comm x a ∙ q ∙ ·-comm b x)

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
------------------------------------------------------------------------------
-- We do not know how erase a proof term in the translation
------------------------------------------------------------------------------

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

module NotErasedProofTerm where

postulate
  D    : Set
  _≡_  : D → D → Set
  _≤_  : D → D → Set
  zero : D
  succ : D → D

data N : D → Set where
  zN :               N zero
  sN : ∀ {n} → N n → N (succ n)

thm : ∀ n → N n → (∀ k → k ≤ k) → n ≡ n
thm n Nn h = prf
  where
  -- The internal type of prf is

  --  ∀ (n : D) (Nn : N n) (h : ∀ k → k ≤ k) → ...

  -- Apia can erase the proof term Nn, but it cannot erase the proof
  -- term h.

  postulate prf : n ≡ n
  {-# ATP prove prf #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia


text:
open import Nat
open import Prelude
open import core
open import contexts
open import lemmas-disjointness
open import exchange
open import lemmas-freshG

-- this module contains all the proofs of different weakening structural
-- properties that we use for the hypothetical judgements
module weakening where
  mutual
    weaken-subst-Δ : ∀{Δ1 Δ2 Γ σ Γ'} → Δ1 ## Δ2
                                     → Δ1 , Γ ⊢ σ :s: Γ'
                                     → (Δ1 ∪ Δ2) , Γ ⊢ σ :s: Γ'
    weaken-subst-Δ disj (STAId x) = STAId x
    weaken-subst-Δ disj (STASubst subst x) = STASubst (weaken-subst-Δ disj subst) (weaken-ta-Δ1 disj x)

    weaken-ta-Δ1 : ∀{Δ1 Δ2 Γ d τ} → Δ1 ## Δ2
                                  → Δ1 , Γ ⊢ d :: τ
                                  → (Δ1 ∪ Δ2) , Γ ⊢ d :: τ
    weaken-ta-Δ1 disj TAConst = TAConst
    weaken-ta-Δ1 disj (TAVar x₁) = TAVar x₁
    weaken-ta-Δ1 disj (TALam x₁ wt) = TALam x₁ (weaken-ta-Δ1 disj wt)
    weaken-ta-Δ1 disj (TAAp wt wt₁) = TAAp (weaken-ta-Δ1 disj wt) (weaken-ta-Δ1 disj wt₁)
    weaken-ta-Δ1 {Δ1} {Δ2} {Γ} disj (TAEHole {u = u} {Γ' = Γ'} x x₁) = TAEHole (x∈∪l Δ1 Δ2 u _ x ) (weaken-subst-Δ disj x₁)
    weaken-ta-Δ1 {Δ1} {Δ2} {Γ} disj (TANEHole {Γ' = Γ'} {u = u} x wt x₁) = TANEHole (x∈∪l Δ1 Δ2 u _ x) (weaken-ta-Δ1 disj wt) (weaken-subst-Δ disj x₁)
    weaken-ta-Δ1 disj (TACast wt x) = TACast (weaken-ta-Δ1 disj wt) x
    weaken-ta-Δ1 disj (TAFailedCast wt x x₁ x₂) = TAFailedCast (weaken-ta-Δ1 disj wt) x x₁ x₂
    weaken-ta-Δ1 disj (TAFst wt) = TAFst (weaken-ta-Δ1 disj wt)
    weaken-ta-Δ1 disj (TASnd wt) = TASnd (weaken-ta-Δ1 disj wt)
    weaken-ta-Δ1 disj (TAPair wt wt₁) = TAPair (weaken-ta-Δ1 disj wt) (weaken-ta-Δ1 disj wt₁)

  -- this is a little bit of a time saver. since ∪ is commutative on
  -- disjoint contexts, and we need that premise anyway in both positions,
  -- there's no real reason to repeat the inductive argument above
  weaken-ta-Δ2 : ∀{Δ1 Δ2 Γ d τ} → Δ1 ## Δ2
                                → Δ2 , Γ ⊢ d :: τ
                                → (Δ1 ∪ Δ2) , Γ ⊢ d :: τ
  weaken-ta-Δ2 {Δ1} {Δ2} {Γ} {d} {τ} disj D = tr (λ q → q , Γ ⊢ d :: τ) (∪comm Δ2 Δ1 (##-comm disj)) (weaken-ta-Δ1 (##-comm disj) D)

  -- note that these statements are somewhat stronger than usual. this is
  -- because we don't have implcit α-conversion. this reifies the
  -- often-silent on paper assumption that if you collide with a bound
  -- variable you can just α-convert it away and not worry.

  -- used in both cases below, so factored into a lemma to save repeated code
  lem-reassoc : {A : Set} {Γ Γ' : A ctx} {x : Nat} {τ : A} → (x # Γ') → (Γ ,, (x , τ)) ∪ Γ' == (Γ ∪ Γ') ,, (x , τ)
  lem-reassoc {A} {Γ} {Γ'} {x} {τ} apt with lem-apart-sing-disj apt
  ... | disj = (∪assoc Γ (■ (x , τ)) Γ' disj) ·
                 (ap1 (λ qq → Γ ∪ qq) (∪comm (■ (x , τ)) (Γ') disj) ·
                   ! (∪assoc Γ Γ' (■ (x , τ)) (##-comm disj)))

  -- first we prove a general form of weakening, that you can add any
  -- context Γ as long as it's fresh with respect to e
  mutual
    weaken-synth-∪ : ∀{e τ Γ Γ'} → freshΓ Γ' e → Γ ⊢ e => τ → (Γ ∪ Γ')  ⊢ e => τ
    weaken-synth-∪ frsh SConst = SConst
    weaken-synth-∪ frsh (SAsc x) = SAsc (weaken-ana-∪ (freshΓ-asc frsh) x)
    weaken-synth-∪ {Γ = Γ} {Γ' = Γ'} frsh (SVar {x = x} x₁) = SVar (x∈∪l Γ Γ' x _ x₁)
    weaken-synth-∪ frsh (SAp x wt x₁ x₂) = SAp x (weaken-synth-∪ (freshΓ-ap1 frsh) wt)
                                                      x₁
                                                      (weaken-ana-∪ (freshΓ-ap2 frsh) x₂)
    weaken-synth-∪ frsh SEHole = SEHole
    weaken-synth-∪ frsh (SNEHole x wt) = SNEHole x (weaken-synth-∪ (freshΓ-nehole frsh) wt)
    weaken-synth-∪ {Γ = Γ} {Γ' = Γ'} frsh (SLam {e = e} {τ2 = τ2} {x = x}  x₁ wt)
      with ctxindirect Γ' x
    ... | Inl qq = abort (lem-fresh-lam2 (frsh x qq))
    ... | Inr qq = SLam (apart-parts Γ Γ' x x₁ qq)
                             (tr (λ qq → qq ⊢ e => τ2) (lem-reassoc {Γ = Γ} qq)
                                                       (weaken-synth-∪ (freshΓ-lam2 frsh) wt))
    weaken-synth-∪ frsh (SFst wt x) = SFst (weaken-synth-∪ (freshΓ-fst frsh) wt) x
    weaken-synth-∪ frsh (SSnd wt x) = SSnd (weaken-synth-∪ (freshΓ-snd frsh) wt) x
    weaken-synth-∪ frsh (SPair hd wt wt₁) = SPair hd (weaken-synth-∪ (freshΓ-pair1 frsh) wt) (weaken-synth-∪ (freshΓ-pair2 frsh) wt₁)

    weaken-ana-∪ : ∀{e τ Γ Γ'} → freshΓ Γ' e →  Γ ⊢ e <= τ → (Γ ∪ Γ') ⊢ e <= τ
    weaken-ana-∪ frsh (ASubsume x x₁) = ASubsume (weaken-synth-∪ frsh x) x₁
    weaken-ana-∪ {Γ = Γ} {Γ' = Γ'} frsh (ALam {e = e} {τ2 = τ2} {x = x} x₁ x₂ wt)
      with ctxindirect Γ' x
    ... | Inl qq = abort (lem-fresh-lam1 (frsh x qq))
    ... | Inr qq = ALam (apart-parts Γ Γ' x x₁ qq)
                        x₂
                        (tr (λ qq → qq ⊢ e <= τ2) (lem-reassoc {Γ = Γ} qq)
                                                  (weaken-ana-∪ (freshΓ-lam1 frsh) wt))

  -- it follows from this that if the term is closed, you can weaken with
  -- any context that's fresh in e
  weaken-synth-closed : ∀{e τ Γ} → freshΓ Γ e → ∅ ⊢ e => τ → Γ ⊢ e => τ
  weaken-synth-closed {e} {τ} {Γ} f wt = tr (λ qq → qq ⊢ e => τ) ∅∪1 (weaken-synth-∪ f wt)

  weaken-ana-closed : ∀{e τ Γ} → freshΓ Γ e → ∅ ⊢ e <= τ → Γ ⊢ e <= τ
  weaken-ana-closed {e} {τ} {Γ} f wt = tr (λ qq → qq ⊢ e <= τ) ∅∪1 (weaken-ana-∪ f wt)

  -- the very structural forms also follow from the union weakening, since
  -- ,, is defined by ∪
  weaken-synth : ∀{ x Γ e τ τ'} → freshe x e
                                  → Γ ⊢ e => τ
                                  → (Γ ,, (x , τ')) ⊢ e => τ
  weaken-synth f wt = weaken-synth-∪ (fresh-freshΓ f) wt

  weaken-ana : ∀{x Γ e τ τ'} → freshe x e
                               → Γ ⊢ e <= τ
                               → (Γ ,, (x , τ')) ⊢ e <= τ
  weaken-ana f wt = weaken-ana-∪ (fresh-freshΓ f) wt

  mutual
    weaken-subst-Γ : ∀{ x Γ Δ σ Γ' τ} →
                     envfresh x σ →
                     Δ , Γ ⊢ σ :s: Γ' →
                     Δ , (Γ ,, (x , τ)) ⊢ σ :s: Γ'
    weaken-subst-Γ {Γ = Γ} (EFId x₁) (STAId x₂) = STAId (λ x τ x₃ → x∈∪l Γ _ x τ (x₂ x τ x₃) )
    weaken-subst-Γ {x = x} {Γ = Γ} (EFSubst x₁ efrsh x₂) (STASubst {y = y} {τ = τ'} subst x₃) =
      STASubst (exchange-subst-Γ {Γ = Γ} (flip x₂) (weaken-subst-Γ {Γ = Γ ,, (y , τ')} efrsh subst))
               (weaken-ta x₁ x₃)

    weaken-ta : ∀{x Γ Δ d τ τ'} →
                fresh x d →
                Δ , Γ ⊢ d :: τ →
                Δ , Γ ,, (x , τ') ⊢ d :: τ
    weaken-ta _ TAConst = TAConst
    weaken-ta {x} {Γ} {_} {_} {τ} {τ'} (FVar x₂) (TAVar x₃) = TAVar (x∈∪l Γ (■ (x , τ')) _ _ x₃)
    weaken-ta {x = x} frsh (TALam {x = y} x₂ wt) with natEQ x y
    weaken-ta (FLam x₁ x₂) (TALam x₃ wt) | Inl refl = abort (x₁ refl)
    weaken-ta {Γ = Γ} {τ' = τ'} (FLam x₁ x₃) (TALam {x = y} x₄ wt) | Inr x₂ = TALam (apart-extend1 Γ (flip x₁) x₄) (exchange-ta-Γ {Γ = Γ} (flip x₁) (weaken-ta x₃ wt))
    weaken-ta (FAp frsh frsh₁) (TAAp wt wt₁) = TAAp (weaken-ta frsh wt) (weaken-ta frsh₁ wt₁)
    weaken-ta (FHole x₁) (TAEHole x₂ x₃) = TAEHole x₂ (weaken-subst-Γ x₁ x₃)
    weaken-ta (FNEHole x₁ frsh) (TANEHole x₂ wt x₃) = TANEHole x₂ (weaken-ta frsh wt) (weaken-subst-Γ x₁ x₃)
    weaken-ta (FCast frsh) (TACast wt x₁) = TACast (weaken-ta frsh wt) x₁
    weaken-ta (FFailedCast frsh) (TAFailedCast wt x₁ x₂ x₃) = TAFailedCast (weaken-ta frsh wt) x₁ x₂ x₃
    weaken-ta (FFst frsh) (TAFst wt) = TAFst (weaken-ta frsh wt)
    weaken-ta (FSnd frsh) (TASnd wt) = TASnd (weaken-ta frsh wt)
    weaken-ta (FPair frsh frsh₁) (TAPair wt wt₁) = TAPair (weaken-ta frsh wt) (weaken-ta frsh₁ wt₁)

max_stars_repo_name: hazelgrove/hazel-palette-agda

max_issues_repo_name: hazelgrove/hazel-palette-agda

max_forks_repo_name: hazelgrove/hazelnut-livelits-agda


text:
-- Bug: With abstraction depended on bound variable names!
module Issue233 where

postulate
  T   : (Set → Set) → Set
  mkT : (F : Set → Set) → T F

foo : T (λ A → A)
foo with λ (B : Set) → B
... | F = mkT F


text:
open import Data.List using ( List ; [] ; _∷_ )
open import Data.Nat using ( ℕ ; zero ; suc )
open import Data.Maybe using ( Maybe ; just ; nothing )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl ; subst )
open import Relation.Binary.PropositionalEquality.TrustMe using ( trustMe )

module AssocFree.Util where

≡-relevant : ∀ {α} {A : Set α} {a b : A} → .(a ≡ b) → (a ≡ b)
≡-relevant a≡b = trustMe

δsubst₂ : ∀ {a b p} {A : Set a} {B : A → Set b} (P : ∀ a → B a → Set p)
         {x₁ x₂ y₁ y₂} → (x₁≡x₂ : x₁ ≡ x₂) → (subst B x₁≡x₂ y₁ ≡ y₂) → P x₁ y₁ → P x₂ y₂
δsubst₂ P refl refl p = p

subst-natural : ∀ {α β γ} {A : Set α} {B : A → Set β} {C : A → Set γ} {a₁ a₂ : A}
  (p : a₁ ≡ a₂) (f : ∀ {a} → B a → C a) (b : B a₁) →
    subst C p (f b) ≡ f (subst B p b)
subst-natural refl f b = refl

lookup : ∀ {α} {A : Set α} → List A → ℕ → Maybe A
lookup [] n             = nothing
lookup (a ∷ as) zero    = just a
lookup (a ∷ as) (suc n) = lookup as n

max_stars_repo_name: agda/agda-assoc-free

max_issues_repo_name: agda/agda-assoc-free

max_forks_repo_name: agda/agda-assoc-free


text:
{-# OPTIONS --without-K #-}
module Util.HoTT.Univalence.Axiom where

open import Util.HoTT.Equiv
open import Util.HoTT.Univalence.Statement
open import Util.Prelude
open import Util.Relation.Binary.PropositionalEquality using (Σ-≡⁻)

private
  variable
    α β γ : Level
    A B C : Set α

postulate
  univalence : ∀ {α} → Univalence α

≃→≡ : A ≃ B → A ≡ B
≃→≡ A≃B = univalence A≃B .proj₁ .proj₁

≡→≃∘≃→≡ : (p : A ≃ B) → ≡→≃ (≃→≡ p) ≡ p
≡→≃∘≃→≡ p = univalence p .proj₁ .proj₂

≃→≡∘≡→≃ : (p : A ≡ B) → ≃→≡ (≡→≃ p) ≡ p
≃→≡∘≡→≃ p = Σ-≡⁻ (univalence (≡→≃ p) .proj₂ (p , refl)) .proj₁

≃→≡-≡→≃-coh : (p : A ≡ B)
  → subst (λ q → ≡→≃ q ≡ ≡→≃ p) (≃→≡∘≡→≃ p) (≡→≃∘≃→≡ (≡→≃ p)) ≡ refl
≃→≡-≡→≃-coh p = Σ-≡⁻ (univalence (≡→≃ p) .proj₂ (p , refl)) .proj₂

≅→≡ : A ≅ B → A ≡ B
≅→≡ = ≃→≡ ∘ ≅→≃

max_stars_repo_name: JLimperg/msc-thesis-code

max_issues_repo_name: JLimperg/msc-thesis-code

max_forks_repo_name: JLimperg/msc-thesis-code


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- IO
------------------------------------------------------------------------

module IO where

open import Coinduction
open import Data.Unit
open import Data.String
open import Data.Colist
open import Function
import IO.Primitive as Prim
open import Level

------------------------------------------------------------------------
-- The IO monad

-- One cannot write "infinitely large" computations with the
-- postulated IO monad in IO.Primitive without turning off the
-- termination checker (or going via the FFI, or perhaps abusing
-- something else). The following coinductive deep embedding is
-- introduced to avoid this problem. Possible non-termination is
-- isolated to the run function below.

infixl 1 _>>=_ _>>_

data IO {a} (A : Set a) : Set (suc a) where
  lift   : (m : Prim.IO A) → IO A
  return : (x : A) → IO A
  _>>=_  : {B : Set a} (m : ∞ (IO B)) (f : (x : B) → ∞ (IO A)) → IO A
  _>>_   : {B : Set a} (m₁ : ∞ (IO B)) (m₂ : ∞ (IO A)) → IO A

{-# NON_TERMINATING #-}

run : ∀ {a} {A : Set a} → IO A → Prim.IO A
run (lift m)   = m
run (return x) = Prim.return x
run (m  >>= f) = Prim._>>=_ (run (♭ m )) λ x → run (♭ (f x))
run (m₁ >> m₂) = Prim._>>=_ (run (♭ m₁)) λ _ → run (♭ m₂)

------------------------------------------------------------------------
-- Utilities

sequence : ∀ {a} {A : Set a} → Colist (IO A) → IO (Colist A)
sequence []       = return []
sequence (c ∷ cs) = ♯ c                  >>= λ x  →
                    ♯ (♯ sequence (♭ cs) >>= λ xs →
                    ♯ return (x ∷ ♯ xs))

-- The reason for not defining sequence′ in terms of sequence is
-- efficiency (the unused results could cause unnecessary memory use).

sequence′ : ∀ {a} {A : Set a} → Colist (IO A) → IO (Lift ⊤)
sequence′ []       = return _
sequence′ (c ∷ cs) = ♯ c                   >>
                     ♯ (♯ sequence′ (♭ cs) >>
                     ♯ return _)

mapM : ∀ {a b} {A : Set a} {B : Set b} →
       (A → IO B) → Colist A → IO (Colist B)
mapM f = sequence ∘ map f

mapM′ : {A B : Set} → (A → IO B) → Colist A → IO (Lift ⊤)
mapM′ f = sequence′ ∘ map f

------------------------------------------------------------------------
-- Simple lazy IO

-- Note that the functions below produce commands which, when
-- executed, may raise exceptions.

-- Note also that the semantics of these functions depends on the
-- version of the Haskell base library. If the version is 4.2.0.0 (or
-- later?), then the functions use the character encoding specified by
-- the locale. For older versions of the library (going back to at
-- least version 3) the functions use ISO-8859-1.

getContents : IO Costring
getContents = lift Prim.getContents

readFile : String → IO Costring
readFile f = lift (Prim.readFile f)

-- Reads a finite file. Raises an exception if the file path refers to
-- a non-physical file (like "/dev/zero").

readFiniteFile : String → IO String
readFiniteFile f = lift (Prim.readFiniteFile f)

writeFile∞ : String → Costring → IO ⊤
writeFile∞ f s =
  ♯ lift (Prim.writeFile f s) >>
  ♯ return _

writeFile : String → String → IO ⊤
writeFile f s = writeFile∞ f (toCostring s)

appendFile∞ : String → Costring → IO ⊤
appendFile∞ f s =
  ♯ lift (Prim.appendFile f s) >>
  ♯ return _

appendFile : String → String → IO ⊤
appendFile f s = appendFile∞ f (toCostring s)

putStr∞ : Costring → IO ⊤
putStr∞ s =
  ♯ lift (Prim.putStr s) >>
  ♯ return _

putStr : String → IO ⊤
putStr s = putStr∞ (toCostring s)

putStrLn∞ : Costring → IO ⊤
putStrLn∞ s =
  ♯ lift (Prim.putStrLn s) >>
  ♯ return _

putStrLn : String → IO ⊤
putStrLn s = putStrLn∞ (toCostring s)


text:
-- {-# OPTIONS -v tc.cover.cover:10 -v tc.cover.splittree:100 -v tc.cover.strategy:100 -v tc.cc:100 #-}
module Issue365 where

{- Basic data types -}

data Nat : Set where
 zero : Nat
 succ : Nat -> Nat

data Fin : Nat -> Set where
 fzero : {n : Nat} -> Fin (succ n)
 fsucc : {n : Nat} -> Fin n -> Fin (succ n)

data Vec (A : Set) : Nat -> Set where
 []   : Vec A zero
 _::_ : {n : Nat} -> A -> Vec A n -> Vec A (succ n)

data _==_ {A : Set} (x : A) : A -> Set where
 refl : x == x

{- Function composition -}

_◦_ : {A : Set} {B : A -> Set} {C : (x : A) -> B x -> Set}
     (f : {x : A} (y : B x) -> C x y) (g : (x : A) -> B x)
     (x : A) -> C x (g x)
(f ◦ g) x = f (g x)

{- Indexing and tabulating -}

_!_ : {n : Nat} {A : Set} -> Vec A n -> Fin n -> A
[]        ! ()
(x :: xs) ! fzero     = x
(x :: xs) ! (fsucc i) = xs ! i

tabulate : {n : Nat} {A : Set} -> (Fin n -> A) -> Vec A n
tabulate {zero}   f = []
tabulate {succ n} f = f fzero :: tabulate (f ◦ fsucc)

lem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs
lem-tab-! {A} {zero}   [] = refl
lem-tab-! {A} {succ n} (x :: xs) with tabulate (_!_ xs) | lem-tab-! xs
lem-tab-! {A} {succ _} (x :: xs) | .xs | refl = refl

max_stars_repo_name: np/agda-git-experiment

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
module Operator.Equals {ℓ} where

import      Lvl
open import Data.Boolean
open import Functional
open import Relator.Equals{ℓ}
open import Type{ℓ}

-- Type class for run-time checking of equality
record Equals(T : Type) : Type where
  infixl 100 _==_
  field
    _==_ : T → T → Bool
  field
    ⦃ completeness ⦄ : ∀{a b : T} → (a ≡ b) → (a == b ≡ 𝑇)
open Equals ⦃ ... ⦄ using (_==_) public

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:
open import Data.Product using ( ∃ ; _×_ ; _,_ ; proj₁ ; proj₂ )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.TBox.Interp using ( Δ ; _⊨_≈_ ) renaming
  ( Interp to Interp′ ; emp to emp′ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.Util using ( False ; id )

module Web.Semantic.DL.ABox.Interp where

infixr 4 _,_
infixr 5 _*_

{-
   An interpretation of a signature Σ (made of concept and role names)
   over a set X of individuals consists of
    - a Signature interpreation I
    - a mapping from X do Δ I, the domain of interpretation of I
   Note: In RDF the members of X are  sets of IRIs, BNodes or Literals, but
   IRIs can also refer to TBox elements.
-}
data Interp (Σ : Signature) (X : Set) : Set₁ where
  -- I is a full Interpreation (Interp')
  -- The function X → Δ {Σ} I interprets the variables in X
  _,_ : ∀ I → (X → Δ {Σ} I) → (Interp Σ X)

-- extract the Signature Interpretation, forgetting the interpretation of variables
⌊_⌋ : ∀ {Σ X} → Interp Σ X → Interp′ Σ
⌊ I , i ⌋ = I

-- return the individuals function for an interpretation
ind : ∀ {Σ X} → (I : Interp Σ X) → X → Δ ⌊ I ⌋
ind (I , i) = i

-- paired individuals function for an interpretation, useful for relations/roles
ind² : ∀ {Σ X} → (I : Interp Σ X) → (X × X) → (Δ ⌊ I ⌋ × Δ ⌊ I ⌋)
ind² I (x , y) = (ind I x , ind I y)

-- why * ?
_*_ : ∀ {Σ X Y} → (Y → X) → Interp Σ X → Interp Σ Y
f * I = (⌊ I ⌋ , λ y → ind I (f y))

-- Empty interpretation
emp : ∀ {Σ} → Interp Σ False
emp = (emp′ , id)

data Surjective {Σ X} (I : Interp Σ X) : Set where
  -- y is a variable i.e. y : X
  -- (ind I y), x : Δ
  -- all elements x of the domain Δ, have a variable y that it is an interpretation of
  surj : (∀ x → ∃ λ y → ⌊ I ⌋ ⊨ x ≈ ind I y) → (I ∈ Surjective)

ind⁻¹ : ∀ {Σ X} {I : Interp Σ X} → (I ∈ Surjective) → (Δ ⌊ I ⌋ → X)
ind⁻¹ (surj i) x = proj₁ (i x)

surj✓ : ∀ {Σ X} {I : Interp Σ X} (I∈Surj : I ∈ Surjective) → ∀ x → (⌊ I ⌋ ⊨ x ≈ ind I (ind⁻¹ I∈Surj x))
surj✓ (surj i) x = proj₂ (i x)

max_stars_repo_name: bblfish/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
{-# OPTIONS --cubical #-}
module Cubical.Categories.Everything where

import Cubical.Categories.Category
import Cubical.Categories.Functor
import Cubical.Categories.NaturalTransformation
import Cubical.Categories.Presheaves
import Cubical.Categories.Sets
import Cubical.Categories.Type

max_stars_repo_name: borsiemir/cubical

max_issues_repo_name: borsiemir/cubical

max_forks_repo_name: borsiemir/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Vectors defined by recursion
------------------------------------------------------------------------

-- What is the point of this module? The n-ary products below are intended
-- to be used with a fixed n, in which case the nil constructor can be
-- avoided: pairs are represented as pairs (x , y), not as triples
-- (x , y , unit).
-- Additionally, vectors defined by recursion enjoy η-rules. That is to say
-- that two vectors of known length are definitionally equal whenever their
-- elements are.

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

module Data.Vec.Recursive where

open import Level using (Level; Lift; lift)
open import Data.Nat.Base as Nat using (ℕ; zero; suc)
open import Data.Empty
open import Data.Fin.Base as Fin using (Fin; zero; suc)
open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂)
open import Data.Sum.Base as Sum using (_⊎_)
open import Data.Unit.Base
open import Data.Vec.Base as Vec using (Vec; _∷_)
open import Function
open import Relation.Unary
open import Agda.Builtin.Equality using (_≡_)

private
  variable
    a b c p : Level
    A : Set a
    B : Set b
    C : Set c

-- Types and patterns
------------------------------------------------------------------------

pattern 2+_ n = suc (suc n)

infix 8 _^_
_^_ : Set a → ℕ → Set a
A ^ 0    = Lift _ ⊤
A ^ 1    = A
A ^ 2+ n = A × A ^ suc n

pattern [] = lift tt

infix 3 _∈[_]_
_∈[_]_ : {A : Set a} → A → ∀ n → A ^ n → Set a
a ∈[ 0    ] as      = Lift _ ⊥
a ∈[ 1    ] a′      = a ≡ a′
a ∈[ 2+ n ] a′ , as = a ≡ a′ ⊎ a ∈[ suc n ] as

-- Basic operations
------------------------------------------------------------------------

cons : ∀ n → A → A ^ n → A ^ suc n
cons 0       a _  = a
cons (suc n) a as = a , as

uncons : ∀ n → A ^ suc n → A × A ^ n
uncons 0        a        = a , lift tt
uncons (suc n)  (a , as) = a , as

head : ∀ n → A ^ suc n → A
head n as = proj₁ (uncons n as)

tail : ∀ n → A ^ suc n → A ^ n
tail n as = proj₂ (uncons n as)

fromVec : ∀[ Vec A ⇒ (A ^_) ]
fromVec = Vec.foldr (_ ^_) (cons _) _

toVec : Π[ (A ^_) ⇒ Vec A ]
toVec 0       as = Vec.[]
toVec (suc n) as = head n as ∷ toVec n (tail n as)

lookup : ∀ {n} (k : Fin n) → A ^ n → A
lookup zero        = head _
lookup (suc {n} k) = lookup k ∘′ tail n

replicate : ∀ n → A → A ^ n
replicate n a = fromVec (Vec.replicate a)

tabulate : ∀ n → (Fin n → A) → A ^ n
tabulate n f = fromVec (Vec.tabulate f)

append : ∀ m n → A ^ m → A ^ n → A ^ (m Nat.+ n)
append 0      n xs       ys = ys
append 1      n x        ys = cons n x ys
append (2+ m) n (x , xs) ys = x , append (suc m) n xs ys

splitAt : ∀ m n → A ^ (m Nat.+ n) → A ^ m × A ^ n
splitAt 0       n xs = [] , xs
splitAt (suc m) n xs =
  let (ys , zs) = splitAt m n (tail (m Nat.+ n) xs) in
  cons m (head (m Nat.+ n) xs) ys , zs

-- Manipulating N-ary products
------------------------------------------------------------------------

map : (A → B) → ∀ n → A ^ n → B ^ n
map f 0      as       = lift tt
map f 1      a        = f a
map f (2+ n) (a , as) = f a , map f (suc n) as

ap : ∀ n → (A → B) ^ n → A ^ n → B ^ n
ap 0      fs       ts       = []
ap 1      f        t        = f t
ap (2+ n) (f , fs) (t , ts) = f t , ap (suc n) fs ts

module _ {P : ℕ → Set p} where

  foldr : P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (2+ n)) →
          ∀ n → A ^ n → P n
  foldr p0 p1 p2+ 0      as       = p0
  foldr p0 p1 p2+ 1      a        = p1 a
  foldr p0 p1 p2+ (2+ n) (a , as) = p2+ n a (foldr p0 p1 p2+ (suc n) as)

foldl : (P : ℕ → Set p) →
        P 0 → (A → P 1) → (∀ n → A → P (suc n) → P (2+ n)) →
        ∀ n → A ^ n → P n
foldl P p0 p1 p2+ 0      as       = p0
foldl P p0 p1 p2+ 1      a        = p1 a
foldl P p0 p1 p2+ (2+ n) (a , as) = let p1′ = p1 a in
  foldl (P ∘′ suc) p1′ (λ a → p2+ 0 a p1′) (p2+ ∘ suc) (suc n) as

reverse : ∀ n → A ^ n → A ^ n
reverse = foldl (_ ^_) [] id (λ n → _,_)

zipWith : (A → B → C) → ∀ n → A ^ n → B ^ n → C ^ n
zipWith f 0      as       bs       = []
zipWith f 1      a        b        = f a b
zipWith f (2+ n) (a , as) (b , bs) = f a b , zipWith f (suc n) as bs

unzipWith : (A → B × C) → ∀ n → A ^ n → B ^ n × C ^ n
unzipWith f 0      as       = [] , []
unzipWith f 1      a        = f a
unzipWith f (2+ n) (a , as) = Prod.zip _,_ _,_ (f a) (unzipWith f (suc n) as)

zip : ∀ n → A ^ n → B ^ n → (A × B) ^ n
zip = zipWith _,_

unzip : ∀ n → (A × B) ^ n → A ^ n × B ^ n
unzip = unzipWith id


text:
open import Prelude
open import RW.Utils.Monads

-- Some Error monad utilities, a là Haskell.
module RW.Utils.Error where

  open import Data.String

  open Monad {{...}}

  -- Error Typeclass
  record IsError {a}(A : Set a) : Set a where
    field
      showError : A → String

  open IsError {{...}}

  instance
    IsError-String : IsError String
    IsError-String = record { showError = λ s → s }

  -- Error Monad
  Err : ∀{a} → (E : Set a) ⦃ isErr : IsError E ⦄
             → Set a → Set a
  Err e a = e ⊎ a

  throwError : ∀{a}{E A : Set a} ⦃ isErr : IsError E ⦄
             → E → Err E A
  throwError = i1

  catchError : ∀{a}{E A : Set a} ⦃ isErr : IsError E ⦄
             → Err E A → (E → Err E A) → Err E A
  catchError (i2 a) _ = i2 a
  catchError (i1 e) f = f e

  instance
    MonadError : ∀{e}{E : Set e} ⦃ isErr : IsError E ⦄
               → Monad (Err E)
    MonadError = record
      { return = i2
      ; _>>=_  = λ { (i1 err) _ → i1 err
                   ; (i2 x  ) f → f x
                   }
      }

  runErr : ∀{a}{E A : Set a} ⦃ isErr : IsError E ⦄
         → Err E A → String ⊎ A
  runErr (i2 a) = i2 a
  runErr ⦃ s ⦄ (i1 e) = i1 (IsError.showError s e)

max_stars_repo_name: VictorCMiraldo/agda-rw

max_issues_repo_name: VictorCMiraldo/agda-rw

max_forks_repo_name: VictorCMiraldo/agda-rw


text:
-- Andreas, 2018-04-10, issue #3581, reported by 3abc, test case by Andrea

-- Regression in the termination checker introduced together
-- with collecting function calls also in the type signatures
-- (fix of #1556).

open import Agda.Builtin.Bool
open import Agda.Builtin.Nat

I = Bool
i0 = true
i1 = false

record PathP {l} (A : I → Set l) (x : A i0) (y : A i1) : Set l where
  field
    apply : ∀ i → A i

open PathP

_[_≡_] = PathP

_≡_ : ∀ {l} {A : Set l} → A → A → Set l
_≡_ {A = A} = PathP (\ _ → A)

refl : ∀ {l} {A : Set l} {x : A} → x ≡ x
refl {x = x} .apply _ = x

cong' : ∀ {l ℓ'} {A : Set l}{B : A → Set ℓ'} (f : (a : A) → B a) {x y} (p : x ≡ y)
     → PathP (λ i → B (p .apply i)) (f (p .apply i0)) (f (p .apply i1))
cong' f p .apply = λ i → f (p .apply i)

foo : Nat → Nat
foo zero = zero
foo (suc n) = Z .apply true .apply true
 where
 postulate
   Z : (\ _ → foo n ≡ foo n) [ (cong' foo (refl {x = n})) ≡ (\ { .apply i → cong' foo (refl {x = n}) .apply i }) ]

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
------------------------------------------------------------------------------
-- Testing Agda internal terms: @Var Nat Args@ when @Args = []@
------------------------------------------------------------------------------

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

module AgdaInternalTerms.VarEmptyArgumentsTerm where

postulate D : Set

postulate id : (P : D → Set)(x : D) → P x → P x
{-# ATP prove id #-}


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Groupoid where

open import Level

open import Categories.Category
import Categories.Morphisms

record Groupoid {o ℓ e} (C : Category o ℓ e) : Set (o ⊔ ℓ ⊔ e) where
  private module C = Category C
  open C using (_⇒_)

  open Categories.Morphisms C

  field
    _⁻¹  : ∀ {A B} → (A ⇒ B) → (B ⇒ A)
    iso : ∀ {A B} {f : A ⇒ B} → Iso f (f ⁻¹)

max_stars_repo_name: p-pavel/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
------------------------------------------------------------------------
-- Lemmas
------------------------------------------------------------------------

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

module Math.Combinatorics.ListFunction.Properties.Lemma where

open import Data.List hiding (_∷ʳ_)
import Data.List.Properties as Lₚ
open import Data.List.Relation.Binary.Sublist.Propositional using (_⊆_; []; _∷_; _∷ʳ_)
open import Data.Product as Prod using (proj₁; proj₂; _×_; _,_)
open import Function
open import Relation.Binary.PropositionalEquality

module _ {a} {A : Set a} where
  []⊆xs : ∀ (xs : List A) → [] ⊆ xs
  []⊆xs []       = []
  []⊆xs (x ∷ xs) = x ∷ʳ []⊆xs xs

module _ {a b} {A : Set a} {B : Set b} where
  lemma₁ : ∀ (f : A → B) (x : A) (xss : List (List A)) →
    map (λ ys → f x ∷ ys) (map (map f) xss) ≡ map (map f) (map (λ ys → x ∷ ys) xss)
  lemma₁ f x xss = begin
    map (λ ys → f x ∷ ys) (map (map f) xss) ≡⟨ sym $ Lₚ.map-compose xss ⟩
    map (λ ys → f x ∷ map f ys) xss         ≡⟨ Lₚ.map-compose xss ⟩
    map (map f) (map (λ ys → x ∷ ys) xss)   ∎
    where open ≡-Reasoning

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where
  proj₁-map₁ : ∀ (f : A → B) (t : A × C) → proj₁ (Prod.map₁ f t) ≡ f (Prod.proj₁ t)
  proj₁-map₁ _ _ = refl

module _ {a b} {A : Set a} {B : Set b} where
  proj₁-map₂ : ∀ (f : B → B) (t : A × B) → proj₁ (Prod.map₂ f t) ≡ proj₁ t
  proj₁-map₂ _ _ = refl

  proj₁′ : A × B → A
  proj₁′ = proj₁


text:
module _ where

open import Agda.Builtin.Equality using (_≡_; refl)

-- First example --

module M (A : Set) where

  record R : Set where
    data D : Set where

  open R (record {})

  postulate
    x : A

  F : D → Set₁
  F _ rewrite refl {x = x} = Set

-- Second example --

record ⊤ : Set where
  no-eta-equality
  constructor tt

data Box (A : Set) : Set where
  [_] : A → Box A

Unit : Set
Unit = Box ⊤

F : Unit → Set → Set
F [ _ ] x = x

G : {P : Unit → Set} → ((x : ⊤) → P [ x ]) → ((x : Unit) → P x)
G f [ x ] = f x

record R : Set₁ where
  no-eta-equality
  field
    f : (x : Unit) → Box (F x ⊤)

  data ⊥ : Set where

r : R
r = record { f = G [_] }

open R r

H : ⊥ → Set₁
H _ rewrite refl {x = tt} = Set


text:
{-# OPTIONS --sized-types #-}

open import FRP.JS.Bool using ( Bool ; true ; false ) renaming ( _≟_ to _≟b_ )
open import FRP.JS.Nat using ( ℕ )
open import FRP.JS.Float using ( ℝ ) renaming ( _≟_ to _≟n_ )
open import FRP.JS.String using ( String ) renaming ( _≟_ to _≟s_ )
open import FRP.JS.Array using ( Array ) renaming ( lookup? to alookup? ; _≟[_]_ to _≟a[_]_ )
open import FRP.JS.Object using ( Object ) renaming ( lookup? to olookup? ; _≟[_]_ to _≟o[_]_ )
open import FRP.JS.Maybe using ( Maybe ; just ; nothing )
open import FRP.JS.Size using ( Size ; ↑_ )

module FRP.JS.JSON where

data JSON : {σ : Size} → Set where
  null : ∀ {σ} → JSON {σ}
  string : ∀ {σ} → String → JSON {σ}
  float : ∀ {σ} → ℝ → JSON {σ}
  bool : ∀ {σ} → Bool → JSON {σ}
  array : ∀ {σ} → Array (JSON {σ}) → JSON {↑ σ}
  object : ∀ {σ} → Object (JSON {σ}) → JSON {↑ σ}

{-# COMPILED_JS JSON function(x,v) {
  if (x === null) { return v.null(null); }
  else if (x.constructor === String) { return v.string(null,x); }
  else if (x.constructor === Number) { return v.float(null,x); }
  else if (x.constructor === Boolean) { return v.bool(null,x); }
  else if (x.constructor === Array) { return v.array(null,x); }
  else { return v.object(null,x); }
} #-}
{-# COMPILED_JS null   function() { return null; } #-}
{-# COMPILED_JS string function() { return function(x) { return x; }; } #-}
{-# COMPILED_JS float  function() { return function(x) { return x; }; } #-}
{-# COMPILED_JS bool   function() { return function(x) { return x; }; } #-}
{-# COMPILED_JS array  function() { return function(x) { return x; }; } #-}
{-# COMPILED_JS object function() { return function(x) { return x; }; } #-}

postulate
  show  : JSON → String
  parse : String → Maybe JSON

{-# COMPILED_JS show  JSON.stringify #-}
{-# COMPILED_JS parse require("agda.box").handle(JSON.parse) #-}

Key : Bool → Set
Key true  = String
Key false = ℕ

lookup? : ∀ {σ} → Maybe (JSON {↑ σ}) → ∀ {b} → Key b → Maybe (JSON {σ})
lookup? (just (object js)) {true}  k = olookup? js k
lookup? (just (array js))  {false} i = alookup? js i
lookup? _                          _ = nothing

_≟_ : ∀ {σ τ} → JSON {σ} → JSON {τ} → Bool
null      ≟ null      = true
string s  ≟ string t  = s ≟s t
float m   ≟ float n   = m ≟n n
bool b    ≟ bool c    = b ≟b c
array js  ≟ array ks  = js ≟a[ _≟_ ] ks
object js ≟ object ks = js ≟o[ _≟_ ] ks
_         ≟ _         = false

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
-- Testing the version option on a file with errors.
--
-- N.B. It is necessary to change the Issue1244a.out file when using
-- different versions of Agda.

foo : Set → Set
foo a = b


text:
module Luau.Addr where

open import Agda.Builtin.Bool using (true; false)
open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Nat using (Nat; _==_)
open import Agda.Builtin.String using (String)
open import Agda.Builtin.TrustMe using (primTrustMe)
open import Properties.Dec using (Dec; yes; no)
open import Properties.Equality using (_≢_)

Addr : Set
Addr = Nat

_≡ᴬ_ : (a b : Addr) → Dec (a ≡ b)
a ≡ᴬ b with a == b
a ≡ᴬ b | false = no p where postulate p : (a ≢ b)
a ≡ᴬ b | true = yes primTrustMe

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


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

-- The Category of Presheaves over a Category C, i.e.
-- the Functor Category [ C.op , Setoids ]
-- Again, the levels are made explicit to show the generality and constraints.

-- CoPreasheaves are defined here as well, for convenience
-- The main reson to name them is that some things (like CoYoneda)
-- look more natural/symmetric then.

open import Level

open import Categories.Category
open import Categories.Category.Construction.Functors
open import Categories.Category.Instance.Setoids using (Setoids)

Presheaves′ : ∀ o′ ℓ′ {o ℓ e : Level} → Category o ℓ e →
  Category (o ⊔ ℓ ⊔ e ⊔ suc (o′ ⊔ ℓ′)) (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) (o ⊔ o′ ⊔ ℓ′)
Presheaves′ o′ ℓ′ C = Functors (Category.op C) (Setoids o′ ℓ′)

Presheaves : ∀ {o ℓ e o′ ℓ′ : Level} → Category o ℓ e →
  Category (o ⊔ ℓ ⊔ e ⊔ suc (o′ ⊔ ℓ′)) (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) (o ⊔ o′ ⊔ ℓ′)
Presheaves {o} {ℓ} {e} {o′} {ℓ′} C = Presheaves′ o′ ℓ′ C

CoPresheaves′ : ∀ o′ ℓ′ {o ℓ e : Level} → Category o ℓ e →
  Category (o ⊔ ℓ ⊔ e ⊔ suc (o′ ⊔ ℓ′)) (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) (o ⊔ o′ ⊔ ℓ′)
CoPresheaves′ o′ ℓ′ C = Functors C (Setoids o′ ℓ′)

CoPresheaves : ∀ {o ℓ e o′ ℓ′ : Level} → Category o ℓ e →
  Category (o ⊔ ℓ ⊔ e ⊔ suc (o′ ⊔ ℓ′)) (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) (o ⊔ o′ ⊔ ℓ′)
CoPresheaves {o} {ℓ} {e} {o′} {ℓ′} C = CoPresheaves′ o′ ℓ′ C

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module Monads.MonadMorphs where

open import Library
open import Functors
open import Categories
open import Monads

open Fun
open Monad

record MonadMorph {a b}{C : Cat {a}{b}}(M M' : Monad C) : Set (a ⊔ b) where
  constructor monadmorph
  open Cat C
  field morph    : ∀ {X} → Hom (T M X) (T M' X)
        lawη     : ∀ {X} → comp morph (η M {X}) ≅ η M' {X}
        lawbind  : ∀ {X Y}{k : Hom X (T M Y)} →
                   comp (morph {Y}) (bind M k)
                   ≅
                   comp (bind M' (comp (morph {Y}) k)) (morph {X})

max_stars_repo_name: jmchapman/Relative-Monads

max_issues_repo_name: jmchapman/Relative-Monads

max_forks_repo_name: jmchapman/Relative-Monads


text:
-- Occurs check when unifying indices in patterns
module OccursCheck where

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

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

f : {n : Nat} -> n == suc n -> Nat
f refl = zero

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Function.Base using (_∋_)
import Cubical.Algebra.Group as Std
-- import Cubical.Structures.Group.Properties
open import MorePropAlgebra.Bundles

module MorePropAlgebra.Properties.Group {ℓ} (assumptions : Group {ℓ}) where
open Group assumptions renaming (Carrier to G)

import MorePropAlgebra.Properties.Monoid
module Monoid'Properties = MorePropAlgebra.Properties.Monoid   (record { Group assumptions }) -- how does this even work without renaming?
module Monoid'           =                            Monoid   (record { Group assumptions })
(      Monoid')          =                            Monoid ∋ (record { Group assumptions })

stdIsGroup : Std.IsGroup 0g _+_ (-_)
stdIsGroup  .Std.IsGroup.isMonoid = Monoid'Properties.stdIsMonoid
stdIsGroup  .Std.IsGroup.inverse  = is-inverse

stdGroup : Std.Group {ℓ}
stdGroup = record { Group assumptions ; isGroup = stdIsGroup }

module GroupLemmas' = Std.GroupLemmas stdGroup

-- module GroupLemmas (G : Group {ℓ}) where
--   open Group G public
--   abstract
--     simplL : (a : Carrier) {b c : Carrier} → a + b ≡ a + c → b ≡ c
--     simplR : {a b : Carrier} (c : Carrier) → a + c ≡ b + c → a ≡ b
--     invInvo : (a : Carrier) → - (- a) ≡ a
--     invId : - 0g ≡ 0g
--     idUniqueL : {e : Carrier} (x : Carrier) → e + x ≡ x → e ≡ 0g
--     idUniqueR : (x : Carrier) {e : Carrier} → x + e ≡ x → e ≡ 0g
--     invUniqueL : {g h : Carrier} → g + h ≡ 0g → g ≡ - h
--     invUniqueR : {g h : Carrier} → g + h ≡ 0g → h ≡ - g
--     invDistr : (a b : Carrier) → - (a + b) ≡ - b - a

-- private
--   simplR = GroupLemmas.simplR G

abstract
  invUniqueL : {g h : G} → g + h ≡ 0g → g ≡ - h
  invUniqueL {g} {h} p = GroupLemmas'.simplR h (p ∙ sym (is-invl h))

  -- ported from `Algebra.Properties.Group`
  private
    right-helper : ∀ x y → y ≡ - x + (x + y)
  right-helper x y = (
    y               ≡⟨ sym (snd (is-identity y)) ⟩
    0g          + y ≡⟨ cong₂ _+_ (sym (snd (is-inverse x))) refl  ⟩
    ((- x) + x) + y ≡⟨ sym (is-assoc (- x) x y) ⟩
    (- x) + (x + y) ∎)

  -- alternative:
  --   follows from uniqueness of -
  --     (a + -a) ≡ 0
  --     ∃! b . a + b = 0
  --   show that a is an additive inverse of - a then it must be THE additive inverse of - a and has to be called - - a which is a by uniqueness
  -involutive : ∀ x → - - x ≡ x
  -involutive x = (
    (- (- x))             ≡⟨ sym (fst (is-identity _)) ⟩
    (- (- x)) + 0g        ≡⟨ cong₂ _+_ refl (sym (snd (is-inverse _))) ⟩
    (- (- x)) + (- x + x) ≡⟨ sym (right-helper (- x) x) ⟩
    x                     ∎)

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
module BSTree  {A : Set}(_≤_ : A → A → Set) where

open import BTree {A}

data _⊴*_ : A → BTree → Set where
  gelf : {x : A}
                   → x ⊴* leaf
  gend : {x y : A}{l r : BTree}
                   → x ≤ y
                   → x ⊴* l
                   → x ⊴* (node y l r)

data _*⊴_ : BTree → A → Set where
  lelf : {x : A}
                   → leaf *⊴ x
  lend : {x y : A}{l r : BTree}
                   → y ≤ x
                   → r *⊴ x
                   → (node y l r) *⊴ x

data BSTree : BTree → Set where
  slf : BSTree leaf
  snd : {x : A}{l r : BTree}
                   → BSTree l
                   → BSTree r
                   → l *⊴ x
                   → x ⊴* r
                   → BSTree (node x l r)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Issue1252 where

data Bool : Set where
  true false : Bool

{-# COMPILED_DATA Bool Bool True False #-}

foo : Bool → Bool
foo true  = false
foo false = true

{-# COMPILED_EXPORT foo foohs #-}


text:
module Hello where

open import IO using (run; putStrLn)
import IO.Primitive as Prim using (IO)
open import Data.Nat using (ℕ)
import Data.Nat.Show as Nat using (show)
open import Data.Unit using (⊤) -- This is no upper case 't'
open import Data.String using (_++_)

age : ℕ
age = 28

main : Prim.IO ⊤
main = run (putStrLn ("Hello World! I'm " ++ Nat.show age))

max_stars_repo_name: neosimsim/merkdas

max_issues_repo_name: neosimsim/merkdas

max_forks_repo_name: neosimsim/merkdas


text:
-- Based on an example due to Thorsten Altenkirch. See "Recursion with
-- boxes", http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=104.

module SubjectReduction where

open import Common.Coinduction

Eq : {A : Set} → A → A → Set1
Eq {A} x y = (P : A → Set) → P x → P y

refl : ∀ {A} (x : A) → Eq x x
refl x P Px = Px

data Stream : Set where
  tick : ∞ Stream → Stream

ticks : Stream
ticks = tick (♯ ticks)

l₁ : Eq ticks (tick _) -- Eq ticks (tick (♯ ticks))
l₁ = refl ticks

l₂ : ∀ {s t} → Eq s t → Eq (tick (♯ s)) (tick (♯ t))
l₂ eq = λ P Px → eq (λ s → P (tick (♯ s))) Px

Goal : Set1
Goal = Eq (tick (♯ ticks)) (tick (♯ tick (♯ ticks)))

_∶_ : (A : Set1) → A → A
_ ∶ x = x

l₃ : Goal
l₃ = ((_ → Eq (tick (♯ ticks)) (tick (♯ tick (♯ ticks)))) ∶ l₂) l₁

-- If l₃ is accepted, then it evaluates to λ P Px → Px, but the
-- following code is not accepted:

-- l₃′ : Goal
-- l₃′ = λ P Px → Px

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Data.List.Decidable where

import      Lvl
open import Data.Boolean
import      Data.Boolean.Operators
open        Data.Boolean.Operators.Programming
open import Data.Tuple
open import Data.List
open import Data.List.Functions
open import Data.List.Equiv
open import Functional
open import Logic.Propositional
open import Logic.Propositional.Theorems
open import Structure.Operator
open import Structure.Relator.Properties
open import Structure.Setoid
open import Type
open import Type.Properties.Decidable
open import Type.Properties.Decidable.Proofs

private variable ℓ ℓₑ ℓₑₗ : Lvl.Level
private variable T : Type{ℓ}

module _
  ⦃ equiv      : Equiv{ℓₑ}(T) ⦄
  ⦃ equiv-list : Equiv{ℓₑₗ}(List(T)) ⦄
  ⦃ ext        : Extensionality(equiv-list) ⦄
  {_≡?_ : T → T → Bool}
  where

  instance
    [≡]-decider : ⦃ dec : Decider(2)(_≡_ {T = T})(_≡?_) ⦄ → Decider(2)(_≡_ {T = List(T)})(satisfiesAll₂(_≡?_) (const 𝐹) (const 𝐹))
    [≡]-decider {x = ∅}      {∅}      = true (reflexivity(_≡_))
    [≡]-decider {x = ∅}      {y ⊰ ys} = false [∅][⊰]-unequal
    [≡]-decider {x = x ⊰ xs} {∅}      = false ([∅][⊰]-unequal ∘ symmetry(_≡_))
    [≡]-decider {x = x ⊰ xs} {y ⊰ ys} = step{f = id} (true ∘ uncurry (congruence₂(_⊰_))) (false ∘ contrapositiveᵣ [⊰]-generalized-cancellation) (tuple-decider ⦃ dec-Q = [≡]-decider {x = xs} {ys} ⦄)


text:
module Structure.Type.Identity.Proofs where

import      Lvl
open import Functional using (_→ᶠ_ ; id ; _on₂_ ; swap ; _$_ ; apply)
open import Logic
open import Logic.Propositional
open import Logic.Propositional.Proofs.Structures
open import Structure.Function
open import Structure.Setoid using (Equiv ; intro) renaming (_≡_ to _≡ₛ_)
open import Structure.Relator.Equivalence
import      Structure.Relator.Names as Names
open import Structure.Relator.Properties
open import Structure.Relator.Properties.Proofs
open import Structure.Relator
open import Structure.Type.Identity
open import Syntax.Function
open import Type

private variable ℓ ℓ₁ ℓ₂ ℓₑ₁ ℓₑ₂ ℓₑ ℓₘₑ ℓₚ ℓₒ : Lvl.Level
private variable T A B : Type{ℓ}
private variable x y : T
private variable Id _≡_ _▫_ : T → T → Stmt{ℓ}

module _ {_≡_ : Type{ℓ} → Type{ℓ} → Stmt{ℓₑ}} ⦃ minRefl : MinimalReflexiveRelation{ℓₚ = ℓ}(_≡_) ⦄ where
  minimal-reflection-coercion : ((_≡_) ⊆₂ (_→ᶠ_))
  minimal-reflection-coercion = minRefl{_→ᶠ_}

module _
  {_≡_ : A → A → Stmt{ℓₑ₁}} ⦃ minRefl : MinimalReflexiveRelation{ℓₚ = ℓₑ₂}(_≡_) ⦄
  {_▫_ : B → B → Stmt{ℓₑ₂}} ⦃ op-refl : Reflexivity(_▫_) ⦄
  {f : A → B}
  where

  minimal-reflection-transport : (_≡_) ⊆₂ ((_▫_) on₂ f)
  minimal-reflection-transport = intro (sub₂(_≡_)((_▫_) on₂ f) ⦃ minRefl ⦃ on₂-reflexivity ⦄ ⦄)

module _ ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ ⦃ minRefl : MinimalReflexiveRelation{ℓₚ = ℓₑ₂}(Equiv._≡_ equiv-A) ⦄ where
  minimal-reflection-to-function : ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ {f : A → B} → Function ⦃ equiv-A ⦄ ⦃ equiv-B ⦄ (f)
  minimal-reflection-to-function {f = f} = intro (sub₂(Equiv._≡_ equiv-A)((_≡ₛ_) on₂ f) ⦃ minimal-reflection-transport ⦄)

module _ ⦃ equiv-T : Equiv{ℓₑ}(T) ⦄ ⦃ minRefl : MinimalReflexiveRelation{ℓₚ = ℓ}(Equiv._≡_ equiv-T) ⦄ where
  minimal-reflection-to-relator : ∀{P : T → Stmt{ℓ}} → UnaryRelator(P)
  minimal-reflection-to-relator {P = P} = intro (sub₂(Equiv._≡_ equiv-T)((_→ᶠ_) on₂ P) ⦃ minimal-reflection-transport ⦄)

module _ ⦃ minRefl : MinimalReflexiveRelation(_≡_) ⦄ where
  minimal-reflection-to-flipped-transitivityᵣ : Names.FlippedTransitivityᵣ(_≡_)
  minimal-reflection-to-flipped-transitivityᵣ {z = z} = sub₂(_≡_)((_→ᶠ_) on₂ (_≡ z)) ⦃ minimal-reflection-transport ⦄

module _ ⦃ refl : Reflexivity(_≡_) ⦄ ⦃ minRefl : MinimalReflexiveRelation(_≡_) ⦄ where
  minimal-reflection-to-symmetry : Symmetry(_≡_)
  Symmetry.proof minimal-reflection-to-symmetry = sub₂(_≡_)(swap(_≡_)) ⦃ minRefl ⦃ swap-reflexivity ⦄ ⦄

  minimal-reflection-to-transitivity : Transitivity(_≡_)
  Transitivity.proof minimal-reflection-to-transitivity xy yz = minimal-reflection-to-flipped-transitivityᵣ (symmetry(_≡_) ⦃ minimal-reflection-to-symmetry ⦄ xy) yz

  minimal-reflection-to-equivalence : Equivalence(_≡_)
  Equivalence.reflexivity  minimal-reflection-to-equivalence = refl
  Equivalence.symmetry     minimal-reflection-to-equivalence = minimal-reflection-to-symmetry
  Equivalence.transitivity minimal-reflection-to-equivalence = minimal-reflection-to-transitivity

module _ ⦃ refl-Id : Reflexivity(Id) ⦄ ⦃ identElim : IdentityEliminator{ℓₚ = ℓₚ}(Id) ⦄ where
  identity-eliminator-to-reflexive-subrelation : MinimalReflexiveRelation(Id)
  identity-eliminator-to-reflexive-subrelation {_▫_ = _▫_} = intro(idElim(Id) (\{x y} _ → (x ▫ y)) (reflexivity(_▫_)))

module _ ⦃ refl : Reflexivity(Id) ⦄ ⦃ identElim : IdentityEliminator(Id) ⦄ where
  identity-eliminator-to-symmetry : Symmetry(Id)
  identity-eliminator-to-symmetry = minimal-reflection-to-symmetry ⦃ minRefl = identity-eliminator-to-reflexive-subrelation ⦄

  identity-eliminator-to-flipped-transitivityᵣ : Names.FlippedTransitivityᵣ(Id)
  identity-eliminator-to-flipped-transitivityᵣ = minimal-reflection-to-flipped-transitivityᵣ ⦃ minRefl = identity-eliminator-to-reflexive-subrelation ⦄

  identity-eliminator-to-transitivity : Transitivity(Id)
  identity-eliminator-to-transitivity = minimal-reflection-to-transitivity ⦃ minRefl = identity-eliminator-to-reflexive-subrelation ⦄

  identity-eliminator-to-equivalence : Equivalence(Id)
  Equivalence.reflexivity  identity-eliminator-to-equivalence = refl
  Equivalence.symmetry     identity-eliminator-to-equivalence = identity-eliminator-to-symmetry
  Equivalence.transitivity identity-eliminator-to-equivalence = identity-eliminator-to-transitivity


text:
-- Andreas, 2020-03-18, issue #4520, reported by Dylan Ede.
--
-- Make the error message concerning ambiguous names
-- in BUILTIN declarations more precise.

open import Agda.Primitive
open import Agda.Builtin.FromNat
open import Agda.Builtin.Nat renaming (Nat to ℕ)

private
  variable
    ℓ ℓ' : Level

record FromNat (A : Set ℓ) : Set (lsuc ℓ) where
  field
    Constraint : ℕ → Set ℓ
    fromNat : (n : ℕ) ⦃ _ : Constraint n ⦄ → A
open FromNat ⦃ ... ⦄ public using (fromNat)

{-# BUILTIN FROMNAT fromNat #-}

-- ERROR WAS:
-- The argument to BUILTIN FROMNAT must be an unambiguous defined name
-- when scope checking the declaration
--   {-# BUILTIN FROMNAT fromNat #-}

-- NEW ERROR:
-- Name  fromNat  is ambiguous
-- when scope checking the declaration
--   {-# BUILTIN FROMNAT fromNat #-}


text:
{-# OPTIONS --experimental-irrelevance #-}

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

data Box (A : Set) : ..(x : A) → Set where
  c : (x : A) → Box A x

unbox : {A : Set} → .(x : A) → Box A x → A
unbox a (c b) = b

.b : Bool
b = true

b' : Bool
b' = unbox b (c _)


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.Truncation.Properties where

open import Cubical.HITs.Truncation.Base
open import Cubical.Data.Nat
open import Cubical.Data.NatMinusOne
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.HITs.Sn
open import Cubical.Data.Empty
open import Cubical.HITs.Susp

open import Cubical.HITs.PropositionalTruncation renaming (∥_∥ to ∥_∥₋₁)
open import Cubical.HITs.SetTruncation
open import Cubical.HITs.GroupoidTruncation
open import Cubical.HITs.2GroupoidTruncation

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

sphereFill : (n : ℕ) (f : S n → A) → Type _
sphereFill {A = A} n f = Σ[ top ∈ A ] ((x : S n) → top ≡ f x)

isSphereFilled : ℕ → Type ℓ → Type ℓ
isSphereFilled n A = (f : S n → A) → sphereFill n f

isSphereFilled∥∥ : {n : ℕ₋₁} → isSphereFilled (1+ n) (∥ A ∥ n)
isSphereFilled∥∥ f = (hub f) , (spoke f)

isSphereFilled→isOfHLevel : (n : ℕ) → isSphereFilled n A → isOfHLevel (1 + n) A
isSphereFilled→isOfHLevel {A = A} 0 h x y = sym (snd (h f) north) ∙ snd (h f) south
  where
    f : Susp ⊥ → A
    f north = x
    f south = y
    f (merid () i)
isSphereFilled→isOfHLevel {A = A} (suc n) h x y = isSphereFilled→isOfHLevel n (helper h x y)
  where
    helper : {n : ℕ} → isSphereFilled (suc n) A → (x y : A) → isSphereFilled n (x ≡ y)
    helper {n = n} h x y f = l , r
      where
        f' : Susp (S n) → A
        f' north = x
        f' south = y
        f' (merid u i) = f u i

        u : sphereFill (suc n) f'
        u = h f'

        z : A
        z = fst u

        p : z ≡ x
        p = snd u north

        q : z ≡ y
        q = snd u south

        l : x ≡ y
        l = sym p ∙ q

        r : (s : S n) → l ≡ f s
        r s i j = hcomp
                    (λ k →
                       λ { (i = i0) → compPath-filler (sym p) q k j
                         ; (i = i1) → snd u (merid s j) k
                         ; (j = i0) → p (k ∨ (~ i))
                         ; (j = i1) → q k
                         })
                  (p ((~ i) ∧ (~ j)))

isOfHLevel→isSphereFilled : (n : ℕ) → isOfHLevel (1 + n) A → isSphereFilled n A
isOfHLevel→isSphereFilled 0 h f = (f north) , (λ _ → h _ _)
isOfHLevel→isSphereFilled {A = A} (suc n) h = helper λ x y → isOfHLevel→isSphereFilled n (h x y)
  where
    helper : {n : ℕ} → ((x y : A) → isSphereFilled n (x ≡ y)) → isSphereFilled (suc n) A
    helper {n = n} h f = l , r
      where
      l : A
      l = f north

      f' : S n → f north ≡ f south
      f' x i = f (merid x i)

      h' : sphereFill n f'
      h' = h (f north) (f south) f'

      r : (x : S (suc n)) → l ≡ f x
      r north = refl
      r south = h' .fst
      r (merid x i) j = hcomp (λ k → λ { (i = i0) → f north
                                        ; (i = i1) → h' .snd x (~ k) j
                                        ; (j = i0) → f north
                                        ; (j = i1) → f (merid x i) }) (f (merid x (i ∧ j)))

isOfHLevel∥∥ : (n : ℕ₋₁) → isOfHLevel (1 + 1+ n) (∥ A ∥ n)
isOfHLevel∥∥ n = isSphereFilled→isOfHLevel (1+ n) isSphereFilled∥∥

ind : {n : ℕ₋₁}
      {B : ∥ A ∥ n → Type ℓ'}
      (hB : (x : ∥ A ∥ n) → isOfHLevel (1 + 1+ n) (B x))
      (g : (a : A) → B (∣ a ∣))
      (x : ∥ A ∥ n) →
      B x
ind hB g (∣ a ∣ ) = g a
ind {B = B} hB g (hub f) =
  isOfHLevel→isSphereFilled _ (hB (hub f)) (λ x → subst B (sym (spoke f x)) (ind hB g (f x)) ) .fst
ind {B = B} hB g (spoke f x i) =
  toPathP {A = λ i → B (spoke f x (~ i))}
    (sym (isOfHLevel→isSphereFilled _ (hB (hub f)) (λ x → subst B (sym (spoke f x)) (ind hB g (f x))) .snd x))
    (~ i)

ind2 : {n : ℕ₋₁}
       {B : ∥ A ∥ n → ∥ A ∥ n → Type ℓ'}
       (hB : ((x y : ∥ A ∥ n) → isOfHLevel (1 + 1+ n) (B x y)))
       (g : (a b : A) → B ∣ a ∣ ∣ b ∣)
       (x y : ∥ A ∥ n) →
       B x y
ind2 {n = n} hB g = ind (λ _ → hLevelPi (1 + 1+ n) (λ _ → hB _ _)) λ a →
                    ind (λ _ → hB _ _) (λ b → g a b)

ind3 : {n : ℕ₋₁}
       {B : (x y z : ∥ A ∥ n) → Type ℓ'}
       (hB : ((x y z : ∥ A ∥ n) → isOfHLevel (1 + 1+ n) (B x y z)))
       (g : (a b c : A) → B (∣ a ∣) ∣ b ∣ ∣ c ∣)
       (x y z : ∥ A ∥ n) →
       B x y z
ind3 {n = n} hB g = ind2 (λ _ _ → hLevelPi (1 + 1+ n) (hB _ _)) λ a b →
                    ind (λ _ → hB _ _ _) (λ c → g a b c)

idemTrunc : (n : ℕ₋₁) → isOfHLevel (1 + 1+ n) A → (∥ A ∥ n) ≃ A
idemTrunc {A = A} n hA = isoToEquiv (iso f g f-g g-f)
  where
  f : ∥ A ∥ n → A
  f = ind (λ _ → hA) λ a → a

  g : A → ∥ A ∥ n
  g = ∣_∣

  f-g : ∀ a → f (g a) ≡ a
  f-g a = refl

  g-f : ∀ x → g (f x) ≡ x
  g-f = ind (λ _ → hLevelSuc (1+ n) _ (hLevelPath (1+ n) (isOfHLevel∥∥ n) _ _)) (λ _ → refl)

propTrunc≃Trunc-1 : ∥ A ∥₋₁ ≃ ∥ A ∥ neg1
propTrunc≃Trunc-1 =
  isoToEquiv
    (iso
      (elimPropTrunc (λ _ → isOfHLevel∥∥ neg1) ∣_∣)
      (ind (λ _ → propTruncIsProp) ∣_∣)
      (ind (λ _ → hLevelSuc 0 _ (hLevelPath 0 (isOfHLevel∥∥ neg1) _ _)) (λ _ → refl))
      (elimPropTrunc (λ _ → hLevelSuc 0 _ (hLevelPath 0 propTruncIsProp _ _)) (λ _ → refl)))

setTrunc≃Trunc0 : ∥ A ∥₀ ≃ ∥ A ∥ (suc neg1)
setTrunc≃Trunc0 =
  isoToEquiv
    (iso
      (elimSetTrunc (λ _ → isOfHLevel∥∥ (suc neg1)) ∣_∣)
      (ind (λ _ → squash₀) ∣_∣₀)
      (ind (λ _ → hLevelSuc 1 _ (hLevelPath 1 (isOfHLevel∥∥ (suc neg1)) _ _)) (λ _ → refl))
      (elimSetTrunc (λ _ → hLevelSuc 1 _ (hLevelPath 1 squash₀ _ _)) (λ _ → refl)))

groupoidTrunc≃Trunc1 : ∥ A ∥₁ ≃ ∥ A ∥ (ℕ→ℕ₋₁ 1)
groupoidTrunc≃Trunc1 =
  isoToEquiv
    (iso
      (groupoidTruncElim _ _ (λ _ → isOfHLevel∥∥ (ℕ→ℕ₋₁ 1)) ∣_∣)
      (ind (λ _ → squash₁) ∣_∣₁)
      (ind (λ _ → hLevelSuc 2 _ (hLevelPath 2 (isOfHLevel∥∥ (ℕ→ℕ₋₁ 1)) _ _)) (λ _ → refl))
      (groupoidTruncElim _ _ (λ _ → hLevelSuc 2 _ (hLevelPath 2 squash₁ _ _)) (λ _ → refl)))

2groupoidTrunc≃Trunc2 : ∥ A ∥₂ ≃ ∥ A ∥ (ℕ→ℕ₋₁ 2)
2groupoidTrunc≃Trunc2 =
  isoToEquiv
    (iso
      (g2TruncElim _ _ (λ _ → isOfHLevel∥∥ (ℕ→ℕ₋₁ 2)) ∣_∣)
      (ind (λ _ → squash₂) ∣_∣₂)
      (ind (λ _ → hLevelSuc 3 _ (hLevelPath 3 (isOfHLevel∥∥ (ℕ→ℕ₋₁ 2)) _ _)) (λ _ → refl))
      (g2TruncElim _ _ (λ _ → hLevelSuc 3 _ (hLevelPath 3 squash₂ _ _)) (λ _ → refl)))

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


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

open import Boolean.Definition
open import Sets.FinSet.Definition
open import LogicalFormulae
open import Groups.Abelian.Definition
open import Groups.Vector
open import Groups.Definition
open import Groups.Abelian.Definition
open import Numbers.Integers.Integers
open import Setoids.Setoids
open import Sets.EquivalenceRelations
open import Modules.Definition
open import Groups.Cyclic.Definition
open import Groups.Cyclic.DefinitionLemmas
open import Rings.Polynomial.Multiplication
open import Rings.Polynomial.Ring
open import Rings.Definition
open import Rings.Lemmas
open import Groups.Polynomials.Definition
open import Numbers.Naturals.Semiring
open import Vectors
open import Modules.Span
open import Numbers.Integers.Definition
open import Numbers.Integers.Addition
open import Rings.IntegralDomains.Definition
open import Numbers.Naturals.Order
open import Numbers.Modulo.Definition
open import Numbers.Modulo.Group

module Modules.Examples where

abGrpModule : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {G' : Group S _+_} (G : AbelianGroup G') → Module ℤRing G (λ x i → elementPower G' i x)
Module.dotWellDefined (abGrpModule {S = S} {G' = G'} G) {m} {n} {g} {h} m=n g=h = transitive (elementPowerWellDefinedG G' g h g=h {m}) (elementPowerWellDefinedZ' G' m n m=n {h})
  where
    open Setoid S
    open Equivalence eq
Module.dotDistributesLeft (abGrpModule {G' = G'} G) {n} {x} {y} = elementPowerHomAbelian G' (AbelianGroup.commutative G) x y n
Module.dotDistributesRight (abGrpModule {S = S} {G' = G'} G) {r} {s} {x} = symmetric (elementPowerCollapse G' x r s)
  where
    open Equivalence (Setoid.eq S)
Module.dotAssociative (abGrpModule {G' = G'} G) {r} {s} {x} = elementPowerMultiplies G' r s x
Module.dotIdentity (abGrpModule {G' = G'} G) = Group.identRight G'

zAndZ : Module ℤRing ℤAbGrp _*Z_
Module.dotWellDefined zAndZ refl refl = refl
Module.dotDistributesLeft zAndZ = Ring.*DistributesOver+ ℤRing
Module.dotDistributesRight zAndZ {x} {y} {z} = Ring.*DistributesOver+' ℤRing {x} {y} {z}
Module.dotAssociative zAndZ {x} {y} {z} = equalityCommutative (Ring.*Associative ℤRing {x} {y} {z})
Module.dotIdentity zAndZ = Ring.identIsIdent ℤRing

twoOrAnother : ℤ → Bool → ℤ
twoOrAnother _ BoolTrue = nonneg 2
twoOrAnother n BoolFalse = n

23Spans : Spans zAndZ (twoOrAnother (nonneg 3))
23Spans m = 2 , (((BoolTrue ,- (BoolFalse ,- [])) ,, (Group.inverse ℤGroup m ,- (m ,- []))) , t m)
  where
    open Group ℤGroup
    open Ring ℤRing
    t : (m : ℤ) → inverse m *Z nonneg 2 +Z (m *Z nonneg 3 +Z nonneg 0) ≡ m
    t m rewrite identRight {m *Z nonneg 3} | *DistributesOver+ {m} {nonneg 2} {nonneg 1} | +Associative {inverse m *Z nonneg 2} {m *Z nonneg 2} {m *Z nonneg 1} = transitivity (transitivity (+WellDefined {inverse m *Z nonneg 2 +Z m *Z nonneg 2} {m *Z nonneg 1} {nonneg 0} {_} (transitivity (equalityCommutative (*DistributesOver+' {inverse m} {m} {nonneg 2})) (*WellDefined (invLeft {m}) refl)) refl) *Commutative) identIsIdent

evenNotOdd : (i : ℤ) → nonneg 0 ≡ i *Z nonneg 2 +Z nonneg 1 → False
evenNotOdd (nonneg x) pr rewrite equalityCommutative (+Zinherits (x *N 2) 1) = evenNotOdd' x (nonnegInjective pr)
  where
    evenNotOdd' : (i : ℕ) → 0 ≡ i *N 2 +N 1 → False
    evenNotOdd' zero ()
    evenNotOdd' (succ i) ()
evenNotOdd (negSucc zero) ()
evenNotOdd (negSucc (succ zero)) ()
evenNotOdd (negSucc (succ (succ x))) ()

2NotSpan : Spans zAndZ {_} {True} (λ _ → nonneg 2) → False
2NotSpan f with f (nonneg 1)
2NotSpan f | n , (trues , b) = bad (_&&_.fst trues) (_&&_.snd trues) (nonneg 0) b
  where
    open Group ℤGroup
    open Ring ℤRing
    bad : {n : ℕ} → (t : Vec True n) (u : Vec ℤ n) (i : ℤ) → dot zAndZ (vecMap (λ _ → nonneg 2) t) u ≡ ((i *Z nonneg 2) +Z nonneg 1) → False
    bad [] [] i x = evenNotOdd i x
    bad (record {} ,- t) (u ,- us) i x = bad t us (i +Z inverse u) (transitivity (+WellDefined (equalityCommutative (invLeft {u *Z nonneg 2})) refl) (transitivity (equalityCommutative (+Associative {inverse (u *Z nonneg 2)} {u *Z nonneg 2})) (transitivity (+WellDefined (refl {x = inverse (u *Z nonneg 2)}) x) (transitivity (+Associative {inverse (u *Z nonneg 2)} {i *Z nonneg 2}) (+WellDefined {inverse (u *Z nonneg 2) +Z i *Z nonneg 2} {_} {(i +Z inverse u) *Z nonneg 2} (transitivity (transitivity (groupIsAbelian {inverse (u *Z nonneg 2)}) (applyEquality (i *Z nonneg 2 +Z_) (equalityCommutative (ringMinusExtracts' ℤRing)))) (equalityCommutative (*DistributesOver+' {i} {inverse u} {nonneg 2}))) (refl {x = nonneg 1}))))))

3NotSpan : Spans zAndZ {_} {True} (λ _ → nonneg 3) → False
3NotSpan f with f (nonneg 1)
... | n , ((trues ,, coeffs) , b) = bad trues coeffs (nonneg 0) b
  where
    open Group ℤGroup
    open Ring ℤRing
    bad : {n : ℕ} → (t : Vec True n) (u : Vec ℤ n) (i : ℤ) → dot zAndZ (vecMap (λ _ → nonneg 3) t) u ≡ ((i *Z nonneg 3) +Z nonneg 1) → False
    bad [] [] (nonneg zero) ()
    bad [] [] (nonneg (succ i)) ()
    bad [] [] (negSucc zero) ()
    bad [] [] (negSucc (succ i)) ()
    bad (record {} ,- ts) (u ,- us) i x = bad ts us (i +Z inverse u) (transitivity (+WellDefined (equalityCommutative (invLeft {u *Z nonneg 3})) (refl {x = dot zAndZ (vecMap (λ _ → nonneg 3) ts) us})) (transitivity (equalityCommutative (+Associative {inverse (u *Z nonneg 3)} {u *Z nonneg 3})) (transitivity (+WellDefined (equalityCommutative (ringMinusExtracts' ℤRing {u} {nonneg 3})) x) (transitivity (+Associative {inverse u *Z nonneg 3} {i *Z nonneg 3} {nonneg 1}) (+WellDefined (transitivity {x = (inverse u *Z nonneg 3 +Z i *Z nonneg 3)} (equalityCommutative (*DistributesOver+' {inverse u} {i})) (*WellDefined (groupIsAbelian {inverse u} {i}) (refl {x = nonneg 3}))) (refl {x = nonneg 1}))))))

nothingNotSpan : Spans zAndZ {_} {False} (λ ()) → False
nothingNotSpan f with f (nonneg 1)
nothingNotSpan f | zero , (([] ,, []) , ())
nothingNotSpan f | succ n , (((() ,- fst) ,, snd) , b)

1Basis : Basis zAndZ {_} {True} (λ _ → nonneg 1)
_&&_.fst 1Basis m = 1 , (((record {} ,- []) ,, (m ,- [])) , transitivity (Group.+WellDefined ℤGroup (transitivity (Ring.*Commutative ℤRing {m}) (Ring.identIsIdent ℤRing)) refl) (Group.identRight ℤGroup))
_&&_.snd 1Basis {zero} r x [] x₁ = record {}
_&&_.snd 1Basis {succ zero} (record {} ,- []) x (b ,- []) pr = equalityCommutative (transitivity (equalityCommutative (transitivity (Group.+WellDefined ℤGroup (transitivity (Ring.*Commutative ℤRing {b}) (Ring.identIsIdent ℤRing)) refl) (Group.identRight ℤGroup))) pr) ,, record {}
_&&_.snd 1Basis {succ (succ n)} (record {} ,- (record {} ,- r)) x b pr with x {0} {1} (succIsPositive _) (succPreservesInequality (succIsPositive _)) refl
_&&_.snd 1Basis {succ (succ n)} (record {} ,- (record {} ,- r)) x b pr | ()

2Independent : Independent zAndZ {_} {True} (λ _ → nonneg 2)
2Independent {zero} r x [] x₁ = record {}
2Independent {succ zero} (record {} ,- []) x (coeff ,- []) pr rewrite Group.identRight ℤGroup {coeff *Z nonneg 2} = equalityCommutative (IntegralDomain.intDom ℤIntDom (transitivity (Ring.*Commutative ℤRing) pr) λ ()) ,, record {}
2Independent {succ (succ n)} (record {} ,- (record {} ,- rest)) pr b x = exFalso (naughtE t)
  where
    t : 0 ≡ 1
    t = pr {0} {1} (succIsPositive (succ n)) (succPreservesInequality (succIsPositive n)) refl

2AndExtraNotIndependent : (n : ℤ) → Independent zAndZ (twoOrAnother n) → False
2AndExtraNotIndependent n indep = exFalso (naughtE (nonnegInjective ohNo))
  where
    r : {a b : ℕ} → (a<n : a <N 2) → (b<n : b <N 2) → vecIndex (BoolTrue ,- (BoolFalse ,- [])) a a<n ≡ vecIndex (BoolTrue ,- (BoolFalse ,- [])) b b<n → a ≡ b
    r {zero} {zero} a<n b<n x = refl
    r {zero} {succ (succ b)} a<n (le (succ zero) ()) x
    r {zero} {succ (succ b)} a<n (le (succ (succ y)) ()) x
    r {succ zero} {succ zero} a<n b<n x = refl
    r {succ zero} {succ (succ b)} a<n (le (succ zero) ()) x
    r {succ zero} {succ (succ b)} a<n (le (succ (succ i)) ()) x
    r {succ (succ a)} {b} (le (succ zero) ()) b<n x
    r {succ (succ a)} {b} (le (succ (succ i)) ()) b<n x
    s : dot zAndZ (vecMap (twoOrAnother n) (BoolTrue ,- (BoolFalse ,- []))) (Group.inverse ℤGroup n ,- (nonneg 2 ,- [])) ≡ nonneg 0
    s rewrite Group.identRight ℤGroup {nonneg 2 *Z n} | Ring.*Commutative ℤRing {nonneg 2} {n} | equalityCommutative (Ring.*DistributesOver+' ℤRing {additiveInverse n} {n} {nonneg 2}) | Group.invLeft ℤGroup {n} = refl
    t : _=V_ zAndZ (Ring.additiveGroup ℤRing) (nonneg 0 ,- (nonneg 0 ,- [])) (Group.inverse ℤGroup n ,- (nonneg 2 ,- []))
    t = indep (BoolTrue ,- (BoolFalse ,- [])) r (Group.inverse ℤGroup n ,- (nonneg 2 ,- [])) s

    ohNo : nonneg 0 ≡ nonneg 2
    ohNo with t
    ohNo | ()

oneLengthAlwaysInj : {a b : ℕ} → (a<n : a <N 1) → (b<n : b <N 1) → a ≡ b
oneLengthAlwaysInj {zero} {zero} a<n b<n = refl
oneLengthAlwaysInj {zero} {succ b} a<n (le zero ())
oneLengthAlwaysInj {zero} {succ b} a<n (le (succ x) ())
oneLengthAlwaysInj {succ a} {b} (le zero ()) b<n
oneLengthAlwaysInj {succ a} {b} (le (succ x) ()) b<n

noBasisExample : Independent (abGrpModule (ℤnAbGroup 5 (le 4 refl))) (λ (t : True) → record { x = 1 ; xLess = le 3 refl }) → False
noBasisExample ind with ind (record {} ,- []) (λ a<n b<n _ → oneLengthAlwaysInj a<n b<n) (nonneg 5 ,- []) refl
noBasisExample ind | ()


text:
module Data.Map
    (Key  : Set)
  where

import Data.Bool
import Data.Maybe

open   Data.Bool

infix 40 _<_ _>_

postulate
  _<_  : Key -> Key -> Bool

_>_ : Key -> Key -> Bool
x > y = y < x

private
  data Map' (a : Set) : Set where
    leaf : Map' a
    node : Key -> a -> Map' a -> Map' a -> Map' a

Map : Set -> Set
Map = Map'

empty : {a : Set} -> Map a
empty = leaf

insert : {a : Set} -> Key -> a -> Map a -> Map a
insert k v leaf = node k v leaf leaf
insert k v (node k' v' l r) =
  | k < k' => node k' v' (insert k v l) r
  | k > k' => node k' v' l (insert k v r)
  | otherwise node k' v l r

open Data.Maybe

lookup : {a : Set} -> Key -> Map a -> Maybe a
lookup k leaf = nothing
lookup k (node k' v l r) =
  | k < k' => lookup k l
  | k > k' => lookup k r
  | otherwise just v


text:
{-# OPTIONS --show-irrelevant #-}

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

postulate
  A : Set
  f : .(Bool → A) → Bool → A

mutual
  X : .A → Bool → A
  X = _

  test : (x : Bool → A) → X (x true) ≡ f x
  test x = refl

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K --safe #-}
module Experiment.Transitive where

open import Level
open import Relation.Binary
open import Relation.Binary.Construct.Closure.Transitive
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

insert-permutation : ∀ x xs → insert x xs ↭ x ∷ xs
insert-pres-Sorted : ∀ x {xs} → Sorted xs → Sorted (insert x xs)
sort-Sorted        : ∀ xs → Sorted (sort xs)
sort-permutation   : ∀ xs → sort xs ↭ xs

private
  variable
    a b r : Level
    A B : Set a
    R S : Rel A r

fold : Transitive R → A [ R ]⁺ B → R A B
fold R-trans [ x∼y ]         = x∼y
fold R-trans (x ∼⁺⟨ x₁ ⟩ x₂) = R-trans (fold R-trans x₁) (fold R-trans x₂)

reverse : Symmetric R → A [ R ]⁺ B → B [ R ]⁺ A
reverse R-sym [ x∼y ]         = [ R-sym x∼y ]
reverse R-sym (x ∼⁺⟨ x₁ ⟩ x₂) = _ ∼⁺⟨ reverse R-sym x₂ ⟩ reverse R-sym x₁

fold-reverse : (R-trans : Transitive R) (R-sym : Symmetric R) (xs : A [ R ]⁺ B) →
              (∀ {a b c} (x : R b c) (y : R a b) →
                R-trans (R-sym x) (R-sym y) ≡ R-sym (R-trans y x)) →
              fold R-trans (reverse R-sym xs) ≡ R-sym (fold R-trans xs)
fold-reverse R-trans R-sym [ x∼y ]           homo = ≡.refl
fold-reverse R-trans R-sym (x ∼⁺⟨ xs₁ ⟩ xs₂) homo = begin
  R-trans (fold R-trans (reverse R-sym xs₂)) (fold R-trans (reverse R-sym xs₁))
    ≡⟨ ≡.cong₂ R-trans (fold-reverse R-trans R-sym xs₂ homo) (fold-reverse R-trans R-sym xs₁ homo) ⟩
  R-trans (R-sym (fold R-trans xs₂)) (R-sym (fold R-trans xs₁))
    ≡⟨ homo (fold R-trans xs₂) (fold R-trans xs₁) ⟩
  R-sym (R-trans (fold R-trans xs₁) (fold R-trans xs₂))
    ∎
  where
  open ≡.≡-Reasoning

-- map :
-- Star⇔ReflexiveTransitive : Star R x y ↔ Reflexive (Transitive R x y)

-- map-reverse : (RS : R ⊆ S) (R-sym : Symmetric R) (S-sym : Symmetric S) xs → map RS (reverse R-sym xs) ≡ reverse S-sym (map RS xs)
-- map-reverse R-sym xs = ?

-- ∘ᵢ-tc (reverse f⁺) ∘ᵢ ∘ᵢ-tc f⁺ ≃ ≅.refl


text:
-- {-# OPTIONS -v tc.size.solve:60 #-}

module Issue300 where

open import Common.Size

data Nat : Size → Set where
  zero : (i : Size) → Nat (↑ i)
  suc  : (i : Size) → Nat i → Nat (↑ i)

-- Size meta used in a different context than the one created in

A : Set₁
A = (Id : (i : Size) → Nat _ → Set)
    (k : Size) (m : Nat (↑ k)) (p : Id k m) →
    (j : Size) (n : Nat j    ) → Id j n
-- should solve _ with ↑ i

-- 1) Id,k,m |- ↑ 1 ≤ X 1      ==> ↑ 4 ≤ X 4
-- 2) Id,k,m,p,j,n |- 1 ≤ X 1

-- Unfixed by fix for #1914 (Andreas, 2016-04-08).


text:
module Everything where

import Library
import NfCBPV

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
module Foreword where

open import Relation.Binary

--open Setoid ⦃ … ⦄
--open IsEquivalence ⦃ … ⦄

open import Level

record HasEquivalence (A : Set) ℓ : Set (suc ℓ) where
  field
    _≈_ : Rel A ℓ
    ⦃ isEquivalence ⦄ : IsEquivalence _≈_

  setoid : Setoid _ _
  Setoid.Carrier setoid = A
  Setoid._≈_ setoid = _≈_
  Setoid.isEquivalence setoid = isEquivalence

open HasEquivalence ⦃ … ⦄

module TestEquivalence (A : Set) (B : Set) ⦃ _ : HasEquivalence A zero ⦄ ⦃ _ : HasEquivalence B zero ⦄ where
  testA : (x : A) → x ≈ x
  testA = {!!}


text:
-- Andreas, 2019-07-09, issue #3900
-- Regression introduced by the fix of #3434

-- {-# OPTIONS -v tc.inj:100 #-}

data Bool : Set where
  true false : Bool

abstract

  data Unit : Set where
    unit : Unit

  f : Unit
  f with true
  ... | true  = unit
  ... | false = unit

-- Error WAS:
-- Not in Scope: unit

-- Should succeed.