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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence

open import Cubical.Reflection.StrictEquiv

private
  variable
    ℓ ℓ' : Level
    A : Type ℓ

-- Less polymorphic version of `cong`, to avoid some unresolved metas
cong′ : ∀ {B : Type ℓ'} (f : A → B) {x y : A} (p : x ≡ y)
      → Path B (f x) (f y)
cong′ f = cong f
{-# INLINE cong′ #-}

PathP≡Path : ∀ (P : I → Type ℓ) (p : P i0) (q : P i1) →
             PathP P p q ≡ Path (P i1) (transport (λ i → P i) p) q
PathP≡Path P p q i = PathP (λ j → P (i ∨ j)) (transport-filler (λ j → P j) p i) q

PathP≡Path⁻ : ∀ (P : I → Type ℓ) (p : P i0) (q : P i1) →
             PathP P p q ≡ Path (P i0) p (transport⁻ (λ i → P i) q)
PathP≡Path⁻ P p q i = PathP (λ j → P (~ i ∧ j)) p (transport⁻-filler (λ j → P j) q i)

PathP≃Path : ∀ (P : I → Type ℓ) (p : P i0) (q : P i1) →
             PathP P p q ≃ Path (P i1) (transport (λ i → P i) p) q
PathP≃Path P p q = transportEquiv (PathP≡Path P p q)

-- Alternative more unfolded proof
toPathP-isEquiv : ∀ (A : I → Type ℓ) {x y} → isEquiv (toPathP {A = A} {x} {y})
toPathP-isEquiv A {x} {y} = isoToIsEquiv (iso toPathP fromPathP to-from from-to)
 where
   to-from : ∀ (p : PathP A x y) → toPathP (fromPathP p) ≡ p
   to-from p h i = outS (hcomp-unique (λ { j (i = i0) → x ; j (i = i1) → fromPathP p j })
                                  (inS (transp (λ j → A (i ∧ j)) (~ i) x))
                                  \ h → inS (sq1 h i))
                        h
      where
        sq1 : (\ h → A [ x ≡ transp (\ j → A (h ∨ j)) h (p h) ]) [ (\ i → transp (λ j → A (i ∧ j)) (~ i) x) ≡ p ]
        sq1 = \ h i → comp (\ z → (hcomp (\ w →
                                                    \ { (z = i1) → A (i ∧ (w ∨ h))
                                                      ; (z = i0) → A (i ∧ h)
                                                      ; (i = i0) → A i0
                                                      ; (i = i1) → A (h ∨ (w ∧ z))
                                                      ; (h = i0) → A (i ∧ (w ∧ z))
                                                      ; (h = i1) → A i})
                                                   ((A (i ∧ h)))))
                                          (\ z → \ { (i = i0) → x
                                                   ; (i = i1) → transp (\ j → A (h ∨ (z ∧ j))) (h ∨ ~ z) (p h)
                                                   ; (h = i0) → transp (λ j → A ((i ∧ z) ∧ j)) (~ (i ∧ z)) x
                                                   ; (h = i1) → p i })
                                (p (i ∧ h))
   from-to : ∀ (q : transp (\ i → A i) i0 x ≡ y) → fromPathP (toPathP {A = A} q) ≡ q
   from-to q = (\ h i → outS (transp-hcomp i {A' = A i1} (\ j → inS (A (i ∨ j)))
                                           ((λ { j (i = i0) → x ; j (i = i1) → q j }))
                                           (inS ((transp (λ j → A (i ∧ j)) (~ i) x))))
                             h)
             ∙ (\ h i → outS (hcomp-unique {A = A i1} ((λ { j (i = i0) → transp (\ i → A i) i0 x ; j (i = i1) → q j }))
                                      (inS ((transp (λ j → A (i ∨ j)) i (transp (λ j → A (i ∧ j)) (~ i) x))))
                                      \ h → inS (sq2 h i))
                             h)
             ∙ sym (lUnit q)
     where
       sq2 : (\ h → transp (\ i → A i) i0 x ≡ q h) [ (\ i → transp (\ j → A (i ∨ j)) i (transp (\ j → A (i ∧ j)) (~ i) x)) ≡ refl ∙ q ]
       sq2 = \ h i → comp (\ z → hcomp (\ w → \ { (i = i1) → A i1
                                              ; (i = i0) → A (h ∨ (w ∧ z))
                                              ; (h = i0) → A (i ∨ (w ∧ z))
                                              ; (h = i1) → A i1
                                              ; (z = i0) → A (i ∨ h)
                                              ; (z = i1) → A ((i ∨ h) ∨ w) })
                                             (A (i ∨ h)))
                 (\ z → \ { (i = i0) → transp (λ j → A ((z ∨ h) ∧ j)) (~ z ∧ ~ h) x
                          ; (i = i1) → q (z ∧ h)
                          ; (h = i1) → compPath-filler refl q z i
                          ; (h = i0) → transp (\ j → A (i ∨ (z ∧ j))) (i ∨ ~ z) (transp (\ j → A (i ∧ j)) (~ i) x)
                          })
                          (transp (\ j → A ((i ∨ h) ∧ j)) (~ (i ∨ h)) x)

PathP≡compPath : ∀ {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z) (r : x ≡ z)
                 → (PathP (λ i → x ≡ q i) p r) ≡ (p ∙ q ≡ r)
PathP≡compPath p q r k = PathP (λ i → p i0 ≡ q (i ∨ k)) (λ j → compPath-filler p q k j) r

PathP≡doubleCompPathˡ : ∀ {A : Type ℓ} {w x y z : A} (p : w ≡ y) (q : w ≡ x) (r : y ≡ z) (s : x ≡ z)
                        → (PathP (λ i → p i ≡ s i) q r) ≡ (p ⁻¹ ∙∙ q ∙∙ s ≡ r)
PathP≡doubleCompPathˡ p q r s k = PathP (λ i → p (i ∨ k) ≡ s (i ∨ k))
                                        (λ j → doubleCompPath-filler (p ⁻¹) q s k j) r

PathP≡doubleCompPathʳ : ∀ {A : Type ℓ} {w x y z : A} (p : w ≡ y) (q : w ≡ x) (r : y ≡ z) (s : x ≡ z)
                        → (PathP (λ i → p i ≡ s i) q r) ≡ (q ≡ p ∙∙ r ∙∙ s ⁻¹)
PathP≡doubleCompPathʳ p q r s k  = PathP (λ i → p (i ∧ (~ k)) ≡ s (i ∧ (~ k)))
                                         q (λ j → doubleCompPath-filler p r (s ⁻¹) k j)

compPathl-cancel : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : x ≡ z) → p ∙ (sym p ∙ q) ≡ q
compPathl-cancel p q = p ∙ (sym p ∙ q) ≡⟨ assoc p (sym p) q ⟩
                       (p ∙ sym p) ∙ q ≡⟨ cong (_∙ q) (rCancel p) ⟩
                              refl ∙ q ≡⟨ sym (lUnit q) ⟩
                                     q ∎

compPathr-cancel : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : z ≡ y) (q : x ≡ y) → (q ∙ sym p) ∙ p ≡ q
compPathr-cancel {x = x} p q i j =
  hcomp-equivFiller (doubleComp-faces (λ _ → x) (sym p) j) (inS (q j)) (~ i)

compPathl-isEquiv : {x y z : A} (p : x ≡ y) → isEquiv (λ (q : y ≡ z) → p ∙ q)
compPathl-isEquiv p = isoToIsEquiv (iso (p ∙_) (sym p ∙_) (compPathl-cancel p) (compPathl-cancel (sym p)))

compPathlEquiv : {x y z : A} (p : x ≡ y) → (y ≡ z) ≃ (x ≡ z)
compPathlEquiv p = (p ∙_) , compPathl-isEquiv p

compPathr-isEquiv : {x y z : A} (p : y ≡ z) → isEquiv (λ (q : x ≡ y) → q ∙ p)
compPathr-isEquiv p = isoToIsEquiv (iso (_∙ p) (_∙ sym p) (compPathr-cancel p) (compPathr-cancel (sym p)))

compPathrEquiv : {x y z : A} (p : y ≡ z) → (x ≡ y) ≃ (x ≡ z)
compPathrEquiv p = (_∙ p) , compPathr-isEquiv p

-- Variations of isProp→isSet for PathP
isProp→SquareP : ∀ {B : I → I → Type ℓ} → ((i j : I) → isProp (B i j))
             → {a : B i0 i0} {b : B i0 i1} {c : B i1 i0} {d : B i1 i1}
             → (r : PathP (λ j → B j i0) a c) (s : PathP (λ j → B j i1) b d)
             → (t : PathP (λ j → B i0 j) a b) (u : PathP (λ j → B i1 j) c d)
             → SquareP B t u r s
isProp→SquareP {B = B} isPropB {a = a} r s t u i j =
  hcomp (λ { k (i = i0) → isPropB i0 j (base i0 j) (t j) k
           ; k (i = i1) → isPropB i1 j (base i1 j) (u j) k
           ; k (j = i0) → isPropB i i0 (base i i0) (r i) k
           ; k (j = i1) → isPropB i i1 (base i i1) (s i) k
        }) (base i j) where
    base : (i j : I) → B i j
    base i j = transport (λ k → B (i ∧ k) (j ∧ k)) a

isProp→isPropPathP : ∀ {ℓ} {B : I → Type ℓ} → ((i : I) → isProp (B i))
                   → (b0 : B i0) (b1 : B i1)
                   → isProp (PathP (λ i → B i) b0 b1)
isProp→isPropPathP {B = B} hB b0 b1 = isProp→SquareP (λ _ → hB) refl refl

isProp→isContrPathP : {A : I → Type ℓ} → (∀ i → isProp (A i))
                    → (x : A i0) (y : A i1)
                    → isContr (PathP A x y)
isProp→isContrPathP h x y = isProp→PathP h x y , isProp→isPropPathP h x y _

-- Flipping a square along its diagonal

flipSquare : {a₀₀ a₀₁ : A} {a₀₋ : a₀₀ ≡ a₀₁}
  {a₁₀ a₁₁ : A} {a₁₋ : a₁₀ ≡ a₁₁}
  {a₋₀ : a₀₀ ≡ a₁₀} {a₋₁ : a₀₁ ≡ a₁₁}
  → Square a₀₋ a₁₋ a₋₀ a₋₁ → Square a₋₀ a₋₁ a₀₋ a₁₋
flipSquare sq i j = sq j i

module _ {a₀₀ a₀₁ : A} {a₀₋ : a₀₀ ≡ a₀₁} {a₁₀ a₁₁ : A} {a₁₋ : a₁₀ ≡ a₁₁}
  {a₋₀ : a₀₀ ≡ a₁₀} {a₋₁ : a₀₁ ≡ a₁₁}
  where

  flipSquareEquiv : Square a₀₋ a₁₋ a₋₀ a₋₁ ≃ Square a₋₀ a₋₁ a₀₋ a₁₋
  unquoteDef flipSquareEquiv = defStrictEquiv flipSquareEquiv flipSquare flipSquare

  flipSquarePath : Square a₀₋ a₁₋ a₋₀ a₋₁ ≡ Square a₋₀ a₋₁ a₀₋ a₁₋
  flipSquarePath = ua flipSquareEquiv

module _ {a₀₀ a₁₁ : A} {a₋ : a₀₀ ≡ a₁₁}
  {a₁₀ : A} {a₁₋ : a₁₀ ≡ a₁₁} {a₋₀ : a₀₀ ≡ a₁₀} where

  slideSquareFaces : (i j k : I) → Partial (i ∨ ~ i ∨ j ∨ ~ j) A
  slideSquareFaces i j k (i = i0) = a₋ (j ∧ ~ k)
  slideSquareFaces i j k (i = i1) = a₁₋ j
  slideSquareFaces i j k (j = i0) = a₋₀ i
  slideSquareFaces i j k (j = i1) = a₋ (i ∨ ~ k)

  slideSquare : Square a₋ a₁₋ a₋₀ refl → Square refl a₁₋ a₋₀ a₋
  slideSquare sq i j = hcomp (slideSquareFaces i j) (sq i j)

  slideSquareEquiv : (Square a₋ a₁₋ a₋₀ refl) ≃ (Square refl a₁₋ a₋₀ a₋)
  slideSquareEquiv = isoToEquiv (iso slideSquare slideSquareInv fillerTo fillerFrom) where
    slideSquareInv : Square refl a₁₋ a₋₀ a₋ → Square a₋ a₁₋ a₋₀ refl
    slideSquareInv sq i j = hcomp (λ k → slideSquareFaces i j (~ k)) (sq i j)
    fillerTo : ∀ p → slideSquare (slideSquareInv p) ≡ p
    fillerTo p k i j = hcomp-equivFiller (λ k → slideSquareFaces i j (~ k)) (inS (p i j)) (~ k)
    fillerFrom : ∀ p → slideSquareInv (slideSquare p) ≡ p
    fillerFrom p k i j = hcomp-equivFiller (slideSquareFaces i j) (inS (p i j)) (~ k)

-- The type of fillers of a square is equivalent to the double composition identites
Square≃doubleComp : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
                    (a₀₋ : a₀₀ ≡ a₀₁) (a₁₋ : a₁₀ ≡ a₁₁)
                    (a₋₀ : a₀₀ ≡ a₁₀) (a₋₁ : a₀₁ ≡ a₁₁)
                    → Square a₀₋ a₁₋ a₋₀ a₋₁ ≃ (a₋₀ ⁻¹ ∙∙ a₀₋ ∙∙ a₋₁ ≡ a₁₋)
Square≃doubleComp a₀₋ a₁₋ a₋₀ a₋₁ = transportEquiv (PathP≡doubleCompPathˡ a₋₀ a₀₋ a₁₋ a₋₁)

-- sym induces an equivalence on identity types of paths
symIso : {a b : A} (p q : a ≡ b) → Iso (p ≡ q) (q ≡ p)
symIso p q = iso sym sym (λ _ → refl) λ _ → refl

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
-- Andreas, 2019-09-10, issue #4065, reported by nad

-- If the set of filtered unsolved constraints is empty, Agda
-- should print at least something like "Unsolved constraints"

postulate
  A : Set

record R (F : A → Set) : Set where

module M (r : (F : A → Set) → R F) where

  module T (F : _) = R (r (λ ℓ → F ℓ))

-- WAS (master after 2.6.0):
-- <no error> when checking the module application ...

-- Expected:
-- Unsolved constraints when checking the module application ...

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module _ (A : Set) where

id : A → A
id x = x

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Constructive.Axiom.Properties where

open import Constructive.Axiom.Properties.Base public
open import Constructive.Axiom.Properties.Transport public
open import Constructive.Axiom.Properties.Bool public


text:
module TemporalOps.OtherOps where

open import CategoryTheory.Instances.Reactive
open import CategoryTheory.Functor
open import CategoryTheory.Monad
open import CategoryTheory.Comonad
open import CategoryTheory.NatTrans
open import CategoryTheory.BCCCs
open import CategoryTheory.CartesianStrength

open import TemporalOps.Next
open import TemporalOps.Delay
open import TemporalOps.Diamond
open import TemporalOps.Box
open import TemporalOps.Common.Other

open import Relation.Binary.PropositionalEquality as ≡
open import Data.Product
open import Data.Sum
open import Data.Nat hiding (_*_)
open import Data.Nat.Properties
            using (+-identityʳ ; +-comm ; +-suc ; +-assoc)

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

open Monad M-◇
open Comonad W-□
private module F-◇ = Functor F-◇
private module F-□ = Functor F-□
open ≡.≡-Reasoning

-- | Natural transformations between modalities

-- delay A by 1 is the same as ▹ A
▹¹-to-▹ : F-delay 1 ⟺ F-▹
▹¹-to-▹ = record
    { to   = record { at = λ A n x → x ; nat-cond = refl }
    ; from = record { at = λ A n x → x ; nat-cond = refl }
    ; iso1 = refl
    ; iso2 = refl
    }

-- □ A is always available, in particular, after a delay by k
□-to-▹ᵏ : ∀(k : ℕ) -> F-□ ⟹ F-delay k
□-to-▹ᵏ k = record
    { at = at-□-▹ᵏ k
    ; nat-cond = nat-cond-□-▹ᵏ k
    }
    where
    at-□-▹ᵏ : ∀(k : ℕ)(A : τ) -> □ A ⇴ delay A by k
    at-□-▹ᵏ zero A n a = a n
    at-□-▹ᵏ (suc k) A zero a = top.tt
    at-□-▹ᵏ (suc k) A (suc n) a = at-□-▹ᵏ k A n a

    nat-cond-□-▹ᵏ : ∀(k : ℕ){A B : τ} {f : A ⇴ B} →
      Functor.fmap (F-delay k) f ∘ at-□-▹ᵏ k A ≈
      at-□-▹ᵏ k B ∘ Functor.fmap F-□ f
    nat-cond-□-▹ᵏ zero {A} {B} {f} {n} {a} = refl
    nat-cond-□-▹ᵏ (suc k) {A} {B} {f} {zero} {a} = refl
    nat-cond-□-▹ᵏ (suc k) {A} {B} {f} {suc n} {a} = nat-cond-□-▹ᵏ k

-- If A is delayed by k, then it is delayed
▹ᵏ-to-◇ : ∀(k : ℕ) -> F-delay k ⟹ F-◇
▹ᵏ-to-◇ k = record
    { at = λ A n a → k , a
    ; nat-cond = refl
    }

-- □ A is always available, in particular, after any delay
□-to-◇ : ∀{k} -> F-□ ⟹ F-◇
□-to-◇ {k} = ▹ᵏ-to-◇ k ⊚ □-to-▹ᵏ k

-- | Monadic operations for ◇

return : ∀{A : τ} -> A ⇴ ◇ A
return {A} = η.at A

-- Monadic extension
_⋆ : ∀{A B : τ} -> (A ⇴ ◇ B) -> (◇ A ⇴ ◇ B)
_⋆ {A} {B} f = μ.at B ∘ F-◇.fmap f
infixl 55 _⋆

-- Bind operator
_>>=_ : ∀{A B : τ}{n : ℕ} -> (◇ A) n -> (A ⇴ (◇ B)) -> (◇ B) n
_>>=_ {n = n} a f = (f ⋆) n a

-- Bind is associative
>>=-assoc : ∀{A B C : τ}{n : ℕ} -> (a : (◇ A) n) -> (f : (A ⇴ (◇ B))) -> (g : (B ⇴ (◇ C)))
         -> (a >>= f) >>= g ≡ a >>= (λ k x → (f k x) >>= g)
>>=-assoc {A}{B}{C} {n} a f g =
    begin
        ((a >>= f) >>= g)
    ≡⟨⟩
        μ.at C n ⌞ (((fmap g ∘ μ.at B) ∘ fmap f) n a) ⌟
    ≡⟨ cong! (≈-cong-left {f = fmap g} (μ.nat-cond {B} {◇ C} {g} {n} {fmap f n a}) {n} {a >>= f}) ⟩
        (((μ.at C ∘ μ.at (◇ C)) ∘ fmap (fmap g)) ∘ fmap f) n a
    ≡⟨ lemma ⟩
        (((μ.at C ∘ fmap (μ.at C)) ∘ fmap (fmap g)) ∘ fmap f) n a
    ≡⟨ cong (μ.at C n) (≈-cong-left {f = fmap g} (sym (fmap-∘ {a = fmap f n a})) {n} {a >>= f}) ⟩
        μ.at C n ((fmap (μ.at C ∘ fmap g) ∘ fmap f) n a)
    ≡⟨ cong (μ.at C n) (sym (fmap-∘ {a = a})) ⟩
        μ.at C n (fmap ((μ.at C ∘ fmap g) ∘ f) n a)
    ≡⟨⟩
        (a >>= (λ k x → f k x >>= g))
    ∎
    where
    open Functor F-◇
    lemma : (((μ.at C ∘ μ.at (◇ C)) ∘ fmap (fmap g)) ∘ fmap f) n a
          ≡ (((μ.at C ∘ fmap (μ.at C)) ∘ fmap (fmap g)) ∘ fmap f) n a
    lemma rewrite μ-assoc {C} {n} {((fmap (fmap g)) ∘ fmap f) n a} = refl

-- Return is left unit to bind
>>=-unit-left : ∀{A B : τ}{n : ℕ} -> (a : A n)(f : A ⇴ ◇ B)
             -> (η.at A n a) >>= f ≡ f n a
>>=-unit-left a f = η-unit1

-- Return is right unit to bind
>>=-unit-right : ∀{A : τ}{n : ℕ} -> (a : (◇ A) n)
              -> a >>= η.at A ≡ a
>>=-unit-right a = η-unit2

max_stars_repo_name: DimaSamoz/temporal-type-systems

max_issues_repo_name: DimaSamoz/temporal-type-systems

max_forks_repo_name: DimaSamoz/temporal-type-systems


text:
primitive
  primSetOmega : _


text:
-- Basic intuitionistic propositional calculus, without ∨ or ⊥.
-- Gentzen-style formalisation of syntax.
-- Normal forms, neutrals, and spines.

module BasicIPC.Syntax.GentzenSpinalNormalForm where

open import BasicIPC.Syntax.Gentzen public

-- Derivations.

mutual
  -- Normal forms, or introductions.
  infix 3 _⊢ⁿᶠ_
  data _⊢ⁿᶠ_ (Γ : Cx Ty) : Ty → Set where
    neⁿᶠ   : ∀ {P}   → Γ ⊢ⁿᵉ α P → Γ ⊢ⁿᶠ α P
    lamⁿᶠ  : ∀ {A B} → Γ , A ⊢ⁿᶠ B → Γ ⊢ⁿᶠ A ▻ B
    pairⁿᶠ : ∀ {A B} → Γ ⊢ⁿᶠ A → Γ ⊢ⁿᶠ B → Γ ⊢ⁿᶠ A ∧ B
    unitⁿᶠ : Γ ⊢ⁿᶠ ⊤

  -- Neutrals, or eliminations.
  infix 3 _⊢ⁿᵉ_
  data _⊢ⁿᵉ_ (Γ : Cx Ty) : Ty → Set where
    spⁿᵉ : ∀ {A C} → A ∈ Γ → Γ ⊢ˢᵖ A ⦙ C → Γ ⊢ⁿᵉ C

  -- Spines.
  infix 3 _⊢ˢᵖ_⦙_
  data _⊢ˢᵖ_⦙_ (Γ : Cx Ty) : Ty → Ty → Set where
    nilˢᵖ : ∀ {C}     → Γ ⊢ˢᵖ C ⦙ C
    appˢᵖ : ∀ {A B C} → Γ ⊢ˢᵖ B ⦙ C → Γ ⊢ⁿᶠ A → Γ ⊢ˢᵖ A ▻ B ⦙ C
    fstˢᵖ : ∀ {A B C} → Γ ⊢ˢᵖ A ⦙ C → Γ ⊢ˢᵖ A ∧ B ⦙ C
    sndˢᵖ : ∀ {A B C} → Γ ⊢ˢᵖ B ⦙ C → Γ ⊢ˢᵖ A ∧ B ⦙ C

-- Translation from normal forms to simple terms.

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

  ne→tm : ∀ {A Γ} → Γ ⊢ⁿᵉ A → Γ ⊢ A
  ne→tm (spⁿᵉ i xs) = sp→tm (var i) xs

  sp→tm : ∀ {A C Γ} → Γ ⊢ A → Γ ⊢ˢᵖ A ⦙ C → Γ ⊢ C
  sp→tm t nilˢᵖ        = t
  sp→tm t (appˢᵖ xs u) = sp→tm (app t (nf→tm u)) xs
  sp→tm t (fstˢᵖ xs)   = sp→tm (fst t) xs
  sp→tm t (sndˢᵖ xs)   = sp→tm (snd t) xs

-- Monotonicity with respect to context inclusion.

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

  mono⊢ⁿᵉ : ∀ {A Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ⁿᵉ A → Γ′ ⊢ⁿᵉ A
  mono⊢ⁿᵉ η (spⁿᵉ i xs) = spⁿᵉ (mono∈ η i) (mono⊢ˢᵖ η xs)

  mono⊢ˢᵖ : ∀ {A C Γ Γ′} → Γ ⊆ Γ′ → Γ ⊢ˢᵖ A ⦙ C → Γ′ ⊢ˢᵖ A ⦙ C
  mono⊢ˢᵖ η nilˢᵖ        = nilˢᵖ
  mono⊢ˢᵖ η (appˢᵖ xs u) = appˢᵖ (mono⊢ˢᵖ η xs) (mono⊢ⁿᶠ η u)
  mono⊢ˢᵖ η (fstˢᵖ xs)   = fstˢᵖ (mono⊢ˢᵖ η xs)
  mono⊢ˢᵖ η (sndˢᵖ xs)   = sndˢᵖ (mono⊢ˢᵖ η xs)

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
module Agda.Builtin.FromNat where

open import Agda.Primitive
open import Agda.Builtin.Nat

record Number {a} (A : Set a) : Set (lsuc a) where
  field
    Constraint : Nat → Set a
    fromNat : ∀ n → {{_ : Constraint n}} → A

open Number {{...}} public using (fromNat)

{-# BUILTIN FROMNAT fromNat #-}
{-# DISPLAY Number.fromNat _ n = fromNat n #-}


text:
open import Everything

module Test.Factsurj3 where

module Test0
  {𝔵 𝔭 𝔯 ℓ} {𝔛 : Ø 𝔵}
  (𝔓 : π̂ 𝔭 𝔛)
  (_≈_ : ∀̇ π̂² ℓ 𝔓)
  (_≈'_ : ∀̇ π̂² ℓ 𝔓)
  (ℜ : π̂² 𝔯 𝔛)
  (ε : Reflexivity.type ℜ)
  (_◃_ : Smaphomarrow!.type ℜ 𝔓)
  (_◃'_ : Smaphomarrow!.type ℜ 𝔓)
  where
  test-class' : ⦃ _ : Leftunit,smaphomarrow.class ℜ 𝔓 ε surjection _◃_ _≈_ ⦄ → Leftunit,smaphomarrow.class ℜ 𝔓 ε surjection _◃_ _≈_
  test-class' = !
  test-method' : ⦃ _ : Leftunit,smaphomarrow.class ℜ 𝔓 ε surjection _◃_ _≈_ ⦄ → Leftunit,smaphomarrow.type ℜ 𝔓 ε surjection _◃_ _≈_
  test-method' = leftunit

test-class : ∀
  {𝔵 𝔭 𝔯 ℓ} {𝔛 : Ø 𝔵}
  {𝔓 : π̂ 𝔭 𝔛}
  ⦃ _ : ∀ {x} → HasEquivalence (𝔓 x) ℓ ⦄
  {ℜ : π̂² 𝔯 𝔛}
  ⦃ _ : Reflexivity.class ℜ ⦄
  ⦃ _ : Smaphomarrow!.class ℜ 𝔓 ⦄
  → ⦃ _ : Leftunit,equivalence,smaphomarrow!.class ℜ 𝔓 ⦄
  → Leftunit,equivalence,smaphomarrow!.class ℜ 𝔓
test-class = !


text:
module Haskell.Prim.Foldable where

open import Haskell.Prim
open import Haskell.Prim.Num
open import Haskell.Prim.Eq
open import Haskell.Prim.List
open import Haskell.Prim.Int
open import Haskell.Prim.Bool
open import Haskell.Prim.Maybe
open import Haskell.Prim.Either
open import Haskell.Prim.Tuple
open import Haskell.Prim.Monoid

--------------------------------------------------
-- Foldable

record Foldable (t : Set → Set) : Set₁ where
  field
    foldMap : ⦃ Monoid b ⦄ → (a → b) → t a → b

  foldr : (a → b → b) → b → t a → b
  foldr f z t = foldMap ⦃ MonoidEndo ⦄ f t z

  foldl : (b → a → b) → b → t a → b
  foldl f z t = foldMap ⦃ MonoidEndoᵒᵖ ⦄ (flip f) t z

  any : (a → Bool) → t a → Bool
  any = foldMap ⦃ MonoidDisj ⦄

  all : (a → Bool) → t a → Bool
  all = foldMap ⦃ MonoidConj ⦄

  and : t Bool → Bool
  and = all id

  or : t Bool → Bool
  or = any id

  null : t a → Bool
  null = all (const false)

  concat : t (List a) → List a
  concat = foldMap id

  concatMap : (a → List b) → t a → List b
  concatMap = foldMap

  elem : ⦃ Eq a ⦄ → a → t a → Bool
  elem x = foldMap ⦃ MonoidDisj ⦄ (x ==_)

  notElem : ⦃ Eq a ⦄ → a → t a → Bool
  notElem x t = not (elem x t)

  toList : t a → List a
  toList = foldr _∷_ []

  sum : ⦃ iNum : Num a ⦄ → t a → a
  sum = foldMap ⦃ MonoidSum ⦄ id

  product : ⦃ iNum : Num a ⦄ → t a → a
  product = foldMap ⦃ MonoidProduct ⦄ id

  length : t a → Int
  length = foldMap ⦃ MonoidSum ⦄ (const 1)

open Foldable ⦃ ... ⦄ public

instance
  iFoldableList : Foldable List
  iFoldableList .foldMap f []       = mempty
  iFoldableList .foldMap f (x ∷ xs) = f x <> foldMap f xs

  iFoldableMaybe : Foldable Maybe
  iFoldableMaybe .foldMap _ Nothing  = mempty
  iFoldableMaybe .foldMap f (Just x) = f x

  iFoldableEither : Foldable (Either a)
  iFoldableEither .foldMap _ (Left _) = mempty
  iFoldableEither .foldMap f (Right x) = f x

  iFoldablePair : Foldable (a ×_)
  iFoldablePair .foldMap f (_ , x) = f x


text:
{-
  This file defines cohomology of a type with
  coefficients in a dependent spectrum over it.
  * Cohom and Cohom' are two versions of the cohomology groups
    - the only difference is the carrier type.
  * 'commDegreeΩ' commutes Ωs with degree shifts of the spectrum
  * 'cohomMap' implement the application of the cohomology functors
    to maps between types

  This general cohomology coincides with ZCohomology when the coefficients
  are constantly the Eilenberg-MacLane spectrum for ℤ (not proven here/yet)
-}
{-# OPTIONS --safe #-}
module Cubical.Cohomology.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed.Base
open import Cubical.Foundations.Pointed.Properties
open import Cubical.Foundations.Isomorphism using (isoToEquiv)
open import Cubical.Foundations.Function    using (_∘_)
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Univalence  using (ua)

open import Cubical.Functions.FunExtEquiv using (funExtEquiv)

open import Cubical.Algebra.Group.Base using (Group; GroupStr)
open import Cubical.Algebra.AbGroup.Base
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties

open import Cubical.Data.Int.Base hiding (_·_)
open import Cubical.Data.Nat.Base using (ℕ)
open import Cubical.Data.Sigma
open import Cubical.Homotopy.Group.Base
open import Cubical.HITs.SetTruncation hiding (map)

open import Cubical.Homotopy.Spectrum
open import Cubical.Homotopy.Loopspace renaming (EH to isCommΩ)
open import Cubical.Structures.Successor

private
  variable
    ℓ : Level

open Spectrum

module _ (X : Type ℓ) (A : (x : X) → Spectrum ℓ) where
  CohomClasses : ℤ → Pointed ℓ
  CohomClasses k = Πᵘ∙ X (λ x → space (A x) k)

  CohomType : ℤ → Type ℓ
  CohomType k = ∥  (fst (CohomClasses k)) ∥₂

  private
    commDegreeΩOnce : (k : ℤ) → (CohomClasses k) ≃∙ Πᵘ∙ X (λ x → Ω (space (A x) (sucℤ k)))
    commDegreeΩOnce k =
      (equivΠCod (λ x → fst (equivΩAt x))) ,
       λ i x → snd (equivΩAt x) i
      where equivΩAt : (x : X) → space (A x) k ≃∙ Ω (space (A x) (sucℤ k))
            equivΩAt x = (fst (map (A x) k) , equiv (A x) k) , snd (map (A x) k)

    commDegreeΩOnce' : (k : ℤ) → (CohomClasses k) ≃∙ Ω (CohomClasses (sucℤ k))
    commDegreeΩOnce' k =
      compEquiv∙ (commDegreeΩOnce k)
                 (funExtEquiv , refl)

  commDegreeΩ : (k : ℤ) (n : ℕ) → (CohomClasses k) ≃∙ (Ω^ n) (CohomClasses (k + (pos n)))
  commDegreeΩ k ℕ.zero = idEquiv∙ _
  commDegreeΩ k (ℕ.suc n) =
    CohomClasses k                                     ≃∙⟨ commDegreeΩ k n ⟩
    (Ω^ n) (CohomClasses (k + (pos n)))                ≃∙⟨ Ω^≃∙ n (commDegreeΩOnce' (k + pos n)) ⟩
    (Ω^ n) (Ω (CohomClasses (sucℤ (k + (pos n)))))     ≃∙⟨ invEquiv∙ (e n) ⟩
    (Ω^ (ℕ.suc n)) (CohomClasses (sucℤ (k + (pos n)))) ∎≃∙
    where e : {A : Pointed ℓ} (n : ℕ) → (Ω^ (ℕ.suc n)) A ≃∙ (Ω^ n) (Ω A)
          e ℕ.zero = isoToEquiv (flipΩIso ℕ.zero) , transportRefl refl
          e (ℕ.suc n) = isoToEquiv (flipΩIso (ℕ.suc n)) , flipΩrefl n

  {-
    Abelian group structure
  -}
  module abGroupStr (k : ℤ) where
    {-
      Use an equivalent type, where the group structure is just
      given by the homotopy group functor
      (index of homotopy groups is off by one below, we actually take π₂,
      to get an abelian group)
    -}
    CohomAsGroup : Group ℓ
    CohomAsGroup = (πGr 1) (Πᵘ∙ X  (λ x → (space (A x) (k + 2))))

    open GroupStr (snd CohomAsGroup)

    isComm :  (a b : fst CohomAsGroup) → a · b ≡ b · a
    isComm = elim2 (λ _ _ → isSetPathImplicit)
                   λ a b → ∣ a ∙ b ∣₂ ≡⟨ cong ∣_∣₂ (isCommΩ 0 a b) ⟩
                           ∣ b ∙ a ∣₂ ∎

    π₂AbGroup : AbGroup ℓ
    π₂AbGroup = Group→AbGroup CohomAsGroup isComm

  module _ (k : ℤ) where
    Cohom' : AbGroup ℓ
    Cohom' = abGroupStr.π₂AbGroup k

    CohomType' : Type ℓ
    CohomType' = fst (abGroupStr.π₂AbGroup k)

    private
      shiftΩTwicePath : fst (abGroupStr.π₂AbGroup k) ≡ CohomType k
      shiftΩTwicePath = sym (cong ∥_∥₂ (ua (fst (commDegreeΩ k 2))))

    Cohom : AbGroup ℓ
    Cohom = CohomType k , subst AbGroupStr shiftΩTwicePath (snd (abGroupStr.π₂AbGroup k))

    CohomPath : Cohom' ≡ Cohom
    CohomPath = ΣPathTransport→PathΣ Cohom' Cohom (shiftΩTwicePath , refl)

    CohomEquiv : AbGroupEquiv Cohom' Cohom
    CohomEquiv = fst (invEquiv (AbGroupPath Cohom' Cohom)) CohomPath

{-
  Functoriality in the type argument
-}
module _ {Y X : Type ℓ} (f : Y → X) (A : (x : X) → Spectrum ℓ) where
  {-
    The following will be used as coefficients for the
    cohomology of Y
  -}
  fA : (y : Y) → Spectrum ℓ
  fA y = A (f y)

  cohomMap' : (k : ℤ) → AbGroupHom (Cohom' X A k) (Cohom' Y fA k)
  cohomMap' k = πHom 1 mapOnClasses  -- apply π₂ to a map on cohomology classes
            where
             mapOnClasses : CohomClasses X A (k + 2) →∙ CohomClasses Y fA (k + 2)
             mapOnClasses = (λ l → (λ y → l (f y))) ,
                            refl

  cohomMap : (k : ℤ) → AbGroupHom (Cohom X A k) (Cohom Y fA k)
  cohomMap k = compGroupHom
                 (compGroupHom (GroupEquiv→GroupHom (invGroupEquiv (CohomEquiv X A k)))
                               (cohomMap' k))
                 (GroupEquiv→GroupHom (CohomEquiv Y fA k))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
open import Agda.Primitive using (lzero; lsuc; _⊔_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import SingleSorted.Substitution
open import Data.Nat using (ℕ; zero; suc)
import MultiSorted.Context as Context

module MultiSorted.Group where

data 𝒜 : Set₀ where
  A : 𝒜

single-sort : ∀ (X : 𝒜) → X ≡ A
single-sort A = refl

open import MultiSorted.AlgebraicTheory

open import MultiSorted.AlgebraicTheory
data GroupOp : Set where
  e : GroupOp
  inv : GroupOp
  mul : GroupOp

ctx : ∀ (n : ℕ) → Context.Context 𝒜
ctx zero = Context.ctx-empty
ctx (suc n) = Context.ctx-concat (ctx n) (Context.ctx-slot A)

-- the signature of the theory of small groups
-- has one constant, one unary operation, one binary operation
Σ : Signature {lzero} {lzero}
Σ = record { sort = 𝒜
           ; oper = GroupOp
           ; oper-arity = λ{ e → ctx 0 ; inv → ctx 1 ; mul → ctx 2}
           ; oper-sort = λ{ e → A ; inv → A ; mul → A}
           }

open Signature Σ

singleton-context : (var (ctx-slot A)) → var (ctx-concat ctx-empty (ctx-slot A))
singleton-context (var-var {A}) = var-inr (var-var {A})

single-sort-context : ∀ {Γ : Context} (x : var Γ) → sort-of Γ x ≡ A
single-sort-context {Γ} x = single-sort (Context.sort-of 𝒜  Γ x)

single-sort-terms : ∀ {X : 𝒜} {Γ : Context} → Term Γ X ≡ Term Γ A
single-sort-terms {A} = refl

σ : ∀ {Γ : Context} {t : Term Γ A} →  Γ ⇒s (ctx 1)
σ {Γ} {t} = λ{ (var-inr var-var) → t}

δ : ∀ {Γ : Context} {t : Term Γ A} {s : Term Γ A} → Γ ⇒s (ctx 2)
δ {Γ} {t} {s} = sub
  where
  sub : Γ ⇒s (ctx 2)
  sub (var-inl x) rewrite (single-sort-terms {(sort-of (ctx 2) (var-inl x))} {Γ}) = t
  sub (var-inr y) rewrite (single-sort-terms {(sort-of (ctx 2) (var-inr y))} {Γ}) = s

-- helper functions for creating terms
e' : ∀ {Γ : Context} → Term Γ A
e' {Γ} = tm-oper e λ()

_∗_ : ∀ {Γ} → Term Γ A → Term Γ A → Term Γ A
t ∗ s =  tm-oper mul λ{ xs → δ {t = t} {s = s} xs}

_ⁱ : ∀ {Γ : Context} →  Term Γ A → Term Γ A
t ⁱ =  tm-oper inv λ{ x → σ {t = t} x}

-- _∗_ : ∀ {Γ} → Term Γ A → Term Γ A → Term Γ A
-- _∗_ {Γ} t s  =  tm-oper mul λ{ (var-inl i) → {!!} ; (var-inr i) → {!!}}

-- _ⁱ : ∀ {Γ : Context} →  Term Γ A → Term Γ A
-- t ⁱ =  tm-oper inv λ{ x → t }

infixl 5 _∗_
infix 6 _ⁱ

_ : Term (ctx 2) A
_ = tm-var (var-inl (var-inr var-var)) ∗ tm-var (var-inr var-var)

-- group equations
data GroupEq : Set where
  mul-assoc e-left e-right inv-left inv-right : GroupEq

mul-assoc-eq : Equation Σ
e-left-eq : Equation Σ
e-right-eq : Equation Σ
inv-left-eq : Equation Σ
inv-right-eq : Equation Σ

mul-assoc-eq = record { eq-ctx = ctx 3
                      ; eq-lhs = x ∗ y ∗ z
                      ; eq-rhs = x ∗ (y ∗ z)
                      }
             where
             x : Term (ctx 3) A
             y : Term (ctx 3) A
             z : Term (ctx 3) A
             x = tm-var (var-inl (var-inl (var-inr var-var)))
             y = tm-var (var-inl (var-inr var-var))
             z = tm-var (var-inr var-var)

e-left-eq = record { eq-ctx = ctx 1 ; eq-lhs = e' ∗ x ; eq-rhs = x }
  where
  x : Term (ctx 1) A
  x = tm-var (var-inr var-var)

e-right-eq = record { eq-ctx = ctx 1 ; eq-lhs = x ∗ e' ; eq-rhs = x }
  where
  x : Term (ctx 1) A
  x = tm-var (var-inr var-var)

inv-left-eq = record { eq-ctx = ctx 1 ; eq-lhs = x ⁱ ∗ x ; eq-rhs = e' }
  where
  x : Term (ctx 1) A
  x = tm-var (var-inr var-var)

inv-right-eq = record { eq-ctx = ctx 1 ; eq-lhs = x ∗ x ⁱ ; eq-rhs = e' }
  where
  x : Term (ctx 1) A
  x = tm-var (var-inr var-var)

𝒢 : Theory lzero Σ
𝒢 = record { ax = GroupEq
            ; ax-eq = λ{ mul-assoc → mul-assoc-eq
                       ; e-left → e-left-eq
                       ; e-right → e-right-eq
                       ; inv-left → inv-left-eq
                       ; inv-right → inv-right-eq
                       }
            }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Induction over _<_ for ℕᵇ.
------------------------------------------------------------------------

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

module Data.Nat.Binary.Induction where

open import Data.Nat.Binary.Base
open import Data.Nat.Binary.Properties
open import Data.Nat.Base as ℕ using (ℕ)
import Data.Nat.Induction as ℕ
open import Induction.WellFounded

------------------------------------------------------------------------
-- _<_ is wellFounded

<-wellFounded : WellFounded _<_
<-wellFounded x = Subrelation.accessible <⇒<ℕ toℕ[x]-acc
  where
  toℕ[x]-acc = InverseImage.accessible toℕ (ℕ.<-wellFounded (toℕ x))


text:
-- Andreas, 2018-05-28, issue #3095, cannot make hidden shadowing variable visible

data Nat : Set where
  suc : {n : Nat} → Nat

data IsSuc : Nat → Set where
  isSuc : ∀{n} → IsSuc (suc {n})

test : ∀{n} → IsSuc n → Set
test p = aux p
  where
  aux : ∀{n} → IsSuc n → Set
  aux isSuc = {!n!}  -- Split on n here

-- Context:
-- p  : IsSuc n
-- n : Nat  (not in scope)
-- n₁ : Nat  (not in scope)

-- WAS: ERROR
-- Ambiguous variable n
-- when checking that the expression ? has type Set

max_stars_repo_name: phadej/agda

max_issues_repo_name: phadej/agda

max_forks_repo_name: phadej/agda


text:
{-# OPTIONS --cubical #-}
module PathWith where

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive.Cubical
open import Agda.Builtin.Nat

pred : Nat → Nat
pred (suc n) = n
pred 0 = 0

f : Nat → Nat
f n with pred n
... | zero = zero
... | suc m = suc m

module _ (qqq : Nat) where

  test1 : f ≡ pred
  test1 i n with pred n
  ... | zero = zero
  ... | suc q = suc q

test2 : test1 ≡ test1
test2 i n j x with pred x
... | zero = zero
... | suc q = suc q


text:
-- a few random examples
module Test where
import Agda.Builtin.Bool

data Nat : Set where zero : Nat -- Comment which gets eaten
                     suc  : Nat -> Nat --Comment which is preserved

plus {- preserved comment  {- which may be nested -} -} :
{- comment after Colon, also preserved-}
{-comments are essentially whitespace, even through they get parsed-} Nat -> {-comment,     preserved-} Nat -> Nat
{-# BUILTIN NATURAL
Nat #-}

plus  zero   m = m
plus (suc n) m = suc (plus n m)

{-# BUILTIN NATPLUS plus #-}

--excess brackets are not preserved
minus : ((Nat)) -> Nat
-- We can nest holes correctly
minus a = {! ? {! Hole inside hole !}  !}

-- Seriously long and complicated function type
func : {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)
func f g x = f (g x)

-- Holes can go here as well
id : {a : Set} -> a -> {!   !}
id x = x

-- and the code from the planning report, rewritten in Baby-Agda

data List (A : Set) : Set where
      empty : List A
      cons : A -> List A -> List A

append : {A : Set} -> List A -> List A -> List A
append empty ys = ys
append (cons x xs) ys = cons x (append xs ys)

-- proposed code after refactoring

data List2 (A : Set) : Nat -> Set where
      empty2 : List2 A 0
      cons2 : {n : Nat} -> A -> List2 A n -> List2 A (plus 1 n)

append2 : {n : Nat} -> {m : Nat} -> {A : Set} ->
            List2 A m -> List2 A n -> List2 A (plus m n)
append2 empty2 ys = ys
append2 (cons2 x xs) ys = cons2 x (append2 xs ys)


text:
module Structure.Category.NaturalTransformation.Equiv where

import      Function.Equals
open        Function.Equals.Dependent
import      Lvl
open import Logic
open import Logic.Predicate
open import Structure.Category
open import Structure.Category.Functor
open import Structure.Category.NaturalTransformation
open import Structure.Setoid
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Type

module _
  {ℓₗₒ ℓₗₘ ℓₗₑ ℓᵣₒ ℓᵣₘ ℓᵣₑ}
  {catₗ : CategoryObject{ℓₗₒ}{ℓₗₘ}{ℓₗₑ}}
  {catᵣ : CategoryObject{ℓᵣₒ}{ℓᵣₘ}{ℓᵣₑ}}
  {F₁ : catₗ →ᶠᵘⁿᶜᵗᵒʳ catᵣ}
  {F₂ : catₗ →ᶠᵘⁿᶜᵗᵒʳ catᵣ}
  where

  _≡ᴺᵀ_ : (F₁ →ᴺᵀ F₂) → (F₁ →ᴺᵀ F₂) → Stmt
  [∃]-intro N₁ ≡ᴺᵀ [∃]-intro N₂ = N₁ ⊜ N₂

  instance
    [≡ᴺᵀ]-reflexivity : Reflexivity(_≡ᴺᵀ_)
    Reflexivity.proof [≡ᴺᵀ]-reflexivity = reflexivity(_⊜_)

  instance
    [≡ᴺᵀ]-symmetry : Symmetry(_≡ᴺᵀ_)
    Symmetry.proof [≡ᴺᵀ]-symmetry = symmetry(_⊜_)

  instance
    [≡ᴺᵀ]-transitivity : Transitivity(_≡ᴺᵀ_)
    Transitivity.proof [≡ᴺᵀ]-transitivity = transitivity(_⊜_)

  instance
    [≡ᴺᵀ]-equivalence : Equivalence(_≡ᴺᵀ_)
    [≡ᴺᵀ]-equivalence = intro

  instance
    [→ᴺᵀ]-equiv : Equiv(F₁ →ᴺᵀ F₂)
    [→ᴺᵀ]-equiv = intro(_≡ᴺᵀ_) ⦃ [≡ᴺᵀ]-equivalence ⦄

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

open import Functions.Definition
open import Sets.CantorBijection.Proofs

module Sets.CantorBijection.CantorBijection where

open Sets.CantorBijection.Proofs using (cantorInverse ; cantorInverseLemma) public

cantorBijection : Bijection cantorInverse
Bijection.inj cantorBijection {x} {y} = cantorInverseInjective x y
Bijection.surj cantorBijection = cantorInverseSurjective


text:
module UniDB.Basic where

open import UniDB.Spec
open import UniDB.Subst
open import Function

module _
  {T : STX} {{vrT : Vr T}} {{wkT : Wk T}} {{apTT : Ap T T}} {{apVrT : ApVr T}} {{apWkTT : ApWk T T}}
  {Ξ : MOR} {{upΞ : Up Ξ}} {{compΞ : Comp Ξ}} {{lkTΞ : Lk T Ξ}} {{lkUpTΞ : LkUp T Ξ}}
    {{lkCompTΞ : LkCompAp T Ξ}} where

  ⊙-↑₁-pointwise : {γ₁ γ₂ γ₃ : Dom} (ξ₁ : Ξ γ₁ γ₂) (ξ₂ : Ξ γ₂ γ₃) →
    [ T ] ((ξ₁ ⊙ ξ₂) ↑₁) ≃ (ξ₁ ↑₁ ⊙ ξ₂ ↑₁)
  lk≃ (⊙-↑₁-pointwise ξ₁ ξ₂) zero = begin
    lk {T} ((ξ₁ ⊙ ξ₂) ↑₁) zero          ≡⟨ lk-↑₁-zero (ξ₁ ⊙ ξ₂) ⟩
    vr zero                             ≡⟨ sym (lk-↑₁-zero ξ₂) ⟩
    lk (ξ₂ ↑₁) zero                     ≡⟨ sym (ap-vr {T} (ξ₂ ↑₁) zero) ⟩
    ap {T} (ξ₂ ↑₁) (vr zero)            ≡⟨ cong (ap {T} (ξ₂ ↑₁)) (sym (lk-↑₁-zero ξ₁)) ⟩
    ap {T} (ξ₂ ↑₁) (lk (ξ₁ ↑₁) zero)    ≡⟨ sym (lk-⊙-ap {T} (ξ₁ ↑₁) (ξ₂ ↑₁) zero) ⟩
    lk (ξ₁ ↑₁ ⊙ ξ₂ ↑₁) zero             ∎
  lk≃ (⊙-↑₁-pointwise ξ₁ ξ₂) (suc i) = begin
    lk ((ξ₁ ⊙ ξ₂) ↑₁) (wk₁ i)           ≡⟨ lk-↑₁-suc (ξ₁ ⊙ ξ₂) i ⟩
    wk₁ (lk (ξ₁ ⊙ ξ₂) i)                ≡⟨ cong wk₁ (lk-⊙-ap {T} ξ₁ ξ₂ i) ⟩
    wk₁ (ap {T} ξ₂ (lk ξ₁ i))           ≡⟨ sym (ap-wk₁ {T} ξ₂ (lk ξ₁ i)) ⟩
    ap {T} (ξ₂ ↑₁) (wk₁ (lk ξ₁ i))      ≡⟨ cong (ap {T} (ξ₂ ↑₁)) (sym (lk-↑₁-suc ξ₁ i)) ⟩
    ap {T} (ξ₂ ↑₁) (lk (ξ₁ ↑₁) (wk₁ i)) ≡⟨ sym (lk-⊙-ap {T} (ξ₁ ↑₁) (ξ₂ ↑₁) (wk₁ i) ) ⟩
    lk (ξ₁ ↑₁ ⊙ ξ₂ ↑₁) (wk₁ i)          ∎

max_stars_repo_name: skeuchel/unidb-agda

max_issues_repo_name: skeuchel/unidb-agda

max_forks_repo_name: skeuchel/unidb-agda


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

open import Algebra
open import Relation.Unary
open import Relation.Binary hiding (Decidable)

module Data.FingerTree.Split
  {r m}
  (ℳ : Monoid r m)
  {s}
  {ℙ : Pred (Monoid.Carrier ℳ) s}
  (ℙ-resp : ℙ Respects (Monoid._≈_ ℳ))
  (ℙ? : Decidable ℙ)
  where

open import Relation.Nullary using (¬_; yes; no; Dec)
open import Level using (_⊔_)
open import Data.Product
open import Function
open import Data.List as List using (List; _∷_; [])

open import Data.FingerTree.Measures ℳ
open import Data.FingerTree.Structures ℳ
open import Data.FingerTree.Reasoning ℳ
open import Data.FingerTree.View ℳ using (deepₗ; deepᵣ)
open import Data.FingerTree.Cons ℳ using (listToTree)

open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (True; toWitness; False; toWitnessFalse)

open σ ⦃ ... ⦄

open Monoid ℳ renaming (Carrier to 𝓡)

open import Data.FingerTree.Relation.Binary.Reasoning.FasterInference.Setoid setoid

open import Data.FingerTree.Split.Point ℳ ℙ-resp ℙ?
open import Data.FingerTree.Split.StoredPredicate ℳ ℙ-resp ℙ?
open import Data.FingerTree.Split.Intermediate ℳ ℙ-resp ℙ?
open import Data.FingerTree.Split.Structures ℳ ℙ-resp ℙ?

record Split {a} (Σ : Set a) ⦃ _ : σ Σ ⦄ : Set (a ⊔ r ⊔ m ⊔ s) where
  constructor _∷⟨_⟩∷_[_]
  field
    left : Tree Σ
    focus : Σ
    right : Tree Σ
    is-split : μ left ∣ μ focus
open Split public

instance
  σ-Split : ∀  {a} {Σ : Set a} ⦃ _ : σ Σ ⦄ → σ (Split Σ)
  μ ⦃ σ-Split ⦄ (l ∷⟨ x ⟩∷ r [ _ ]) = μ l ∙ (μ x ∙ μ r)

split : ∀ {a} {Σ : Set a} ⦃ _ : σ Σ ⦄
      → {¬ℙ⟨ε⟩ : False (ℙ? ε)}
      → (xs : Tree Σ)
      → {ℙ⟨xs⟩ : True (ℙ? (μ xs))}
      → μ⟨ Split Σ ⟩≈ μ xs
split {¬ℙ⟨ε⟩ = ¬ℙ⟨ε⟩} xs {ℙ⟨xs⟩} with splitTree ε xs (init-ℙ ¬ℙ⟨ε⟩ ℙ⟨xs⟩) ≈[ identityˡ _ ]
... | xs′ ∷⟨ x ⟩∷ ys [ p ] ⇑[ p₂ ] = xs′ ∷⟨ x ⟩∷ ys [ Relation.Nullary.recompute (_ ∣? _) p ≈◄⟅ identityˡ _ ⟆ ] ⇑[  sym (identityˡ _) ⍮ p₂ ]

max_stars_repo_name: oisdk/agda-indexed-fingertree

max_issues_repo_name: oisdk/agda-indexed-fingertree

max_forks_repo_name: oisdk/agda-indexed-fingertree


text:
open import prelude renaming (_≟Nat_ to _≟_)

infixl 5 _$_

-- Copied pretty much verbatim

Var = Nat

data Term : Set where
  var : Var → Term
  fun : Term → Term
  _$_ : Term → Term → Term

-- Doing full reduction, so values are either of the form
-- (fun v) or (x v1 ... vN)

data VarHeaded : Term → Set
data Value : Term → Set

data VarHeaded where
  var : (x : Var) → VarHeaded(var x)
  _$_ : ∀ {t u} → VarHeaded(t) → Value(u) → VarHeaded(t $ u)

data Value where
  var : (x : Var) → Value(var x)
  fun : ∀ {t} → Value(t) → Value(fun t)
  _$_ : ∀ {t u} → VarHeaded(t) → Value(u) → Value(t $ u)

-- Substitution is now total!

shift : Var → Var → Term → Term
shift c d (var x) = if (c ≤? x) (var (d + x)) (var x)
shift c d (fun t) = fun (shift (1 + c) d t)
shift c d (t₁ $ t₂) = (shift c d t₁) $ (shift c d t₂)

[_↦_]_ : Var → Term → Term → Term
[ x ↦ s ] var y = if (x ≟ y) (shift x 0 s) (if (x ≤? y) (var (y - 1)) (var y))
[ x ↦ s ] fun t = fun ([ (1 + x) ↦ s ] t)
[ x ↦ s ] (t₁ $ t₂) = ([ x ↦ s ] t₁) $ ([ x ↦ s ] t₂)

-- Reduction is as per TAPL

data _⟶_ : Term → Term → Set where

  E─App1 : ∀ {t₁ t₁′ t₂} →

     (t₁ ⟶ t₁′) →
     ------------------------
     (t₁ $ t₂) ⟶ (t₁′ $ t₂)

  E─App2 : ∀ {t₁ t₂ t₂′} →

     (t₂ ⟶ t₂′) →
     ------------------------
     (t₁ $ t₂) ⟶ (t₁ $ t₂′)

  E─AppAbs : ∀ {t₁ t₂} →

     ---------------------------------
     (fun t₁ $ t₂) ⟶ ([ 0 ↦ t₂ ] t₁)

  -- Needed for full reduction!
  E─FunCong : ∀ {t t′} →

    (t ⟶ t′) →
    ----------------
    fun t ⟶ fun t′

-- A redex is a term which can reduce

data Redex  : Term → Set where

  redex : ∀ {t t′} →

    t ⟶ t′ →
    --------
    Redex(t)

-- Proving that every closed term is a value or a redex

data ValueOrRedex : Term → Set where

  value : ∀ {t} →

    (Value(t)) →
    ---------------
    ValueOrRedex(t)

  redex : ∀ {t t′} →

    t ⟶ t′ →
    ---------------
    ValueOrRedex(t)

valueOrRedex : (t : Term) → ValueOrRedex(t)
valueOrRedex (var x) = value (var x)
valueOrRedex (fun t) = helper (valueOrRedex t) where

  helper : ValueOrRedex(t) → ValueOrRedex(fun t)
  helper (value v) = value (fun v)
  helper (redex r) = redex (E─FunCong r)

valueOrRedex (t₁ $ t₂) = helper₁ (valueOrRedex t₁) where

  helper₃ : ∀ {t₁} → Value(t₁) → Value(t₂) → ValueOrRedex(t₁ $ t₂)
  helper₃ (var x) v = value (var x $ v)
  helper₃ (fun t) v = redex E─AppAbs
  helper₃ (t $ u) v = value (t $ u $ v)

  helper₂ : Value(t₁) → ValueOrRedex(t₂) → ValueOrRedex(t₁ $ t₂)
  helper₂ v₁ (value v₂) = helper₃ v₁ v₂
  helper₂ v₁ (redex r) = redex (E─App2 r)

  helper₁ : ValueOrRedex(t₁) → ValueOrRedex(t₁ $ t₂)
  helper₁ (value v₁) = helper₂ v₁ (valueOrRedex t₂)
  helper₁ (redex r) = redex (E─App1 r)

-- Interpreter!

data _⟶*_ : Term → Term → Set where

  done : ∀ {t} →

    --------
    t ⟶* t

  redex : ∀ {t t′ t″} →

    t ⟶ t′ →
    t′ ⟶* t″ →
    ----------
    t ⟶* t″

-- An interpreter result

data Result  : Term → Set where

  result : ∀ {t t′} →

    t ⟶* t′ →
    Value(t′) →
    ---------
    Result(t)

-- The interpreter just calls `valueOrRedex` until it is a value.
-- This might not terminate!

{-# NON_TERMINATING #-}
interp : (t : Term) → Result(t)
interp t = helper₂ (valueOrRedex t) where

  helper₁ : ∀ {t′} → (t ⟶ t′) → Result(t′) → Result(t)
  helper₁ r (result s v) = result (redex r s) v

  helper₂ : ValueOrRedex(t) → Result(t)
  helper₂ (value v)           = result done v
  helper₂ (redex {t′ = t′} r) = helper₁ r (interp t′)

-- Examples

zer : Term
zer = fun (fun (var 1))

succ : Term
succ = fun (fun (fun (var 0 $ var 2)))

add : Term
add = fun (fun (var 1 $ var 0 $ succ))

two : Term
two = succ $ (succ $ zer)

four : Term
four = add $ two $ two

-- DANGER! Do not run interp loop
loop : Term
loop = (fun (var 0 $ var 0)) $ (fun (var 0 $ var 0))

max_stars_repo_name: asajeffrey/tapl

max_issues_repo_name: asajeffrey/tapl

max_forks_repo_name: asajeffrey/tapl


text:
module Data.Graph where

open import Data.List as List using (List; []; _∷_)
open import Data.Nat hiding (_⊔_)
open import Data.Product
open import Data.Vec as Vec using (Vec; []; _∷_)
open import Data.Vec.Properties
open import Level as ℓ using (Level; _⊔_)
open import Finite
open import Finite.Pigeonhole
open import Function
open import Relation.Binary
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.HeterogeneousEquality as ≅
open import Relation.Binary.PropositionalEquality as ≡
open import Relation.Nullary

open IsFinite

module Path {ℓᵥ ℓₑ} {V : Set ℓᵥ} (_↦_ : V → V → Set ℓₑ) where
  data Path a : V → ℕ → Set (ℓᵥ ⊔ ℓₑ) where
    [] : Path a a zero
    _∷_ : ∀ {b c n} → a ↦ b → Path b c n → Path a c (suc n)

  Path≤ = λ a b n → ∃ λ m → m ≤ n × Path a b m
  Path< = λ a b n → ∃ λ m → m < n × Path a b m

  infixr 5 _∷ʳ_
  _∷ʳ_ : ∀ {a b c n} → Path a b n → b ↦ c → Path a c (suc n)
  [] ∷ʳ e = e ∷ []
  (e ∷ p) ∷ʳ e′ = e ∷ p ∷ʳ e′

  unsnoc : ∀ {n a c}
    (p : Path a c (suc n)) →
    ∃ λ b →
      ∃₂ λ (p′ : Path a b n) (e : b ↦ c) →
        p ≡ p′ ∷ʳ e
  unsnoc (e ∷ []) = -, [] , e , refl
  unsnoc (e ∷ d ∷ p) with unsnoc (d ∷ p)
  … | b , p′ , e′ , eq rewrite eq = b , e ∷ p′ , e′ , refl

  infixl 5 _++_
  _++_ : ∀ {a b c m n} → Path a b m → Path b c n → Path a c (m + n)
  [] ++ q = q
  (e ∷ p) ++ q = e ∷ (p ++ q)

  trail : ∀ {a b n} → Path a b n → Vec V n
  trail [] = []
  trail {a} (e ∷ p) = a ∷ trail p

  toStar : ∀ {a b n} → Path a b n → Star _↦_ a b
  toStar [] = ε
  toStar (e ∷ p) = e ◅ toStar p

  starLength : ∀ {a b} → Star _↦_ a b → ℕ
  starLength = fold _ (const suc) zero

  fromStar : ∀ {a b} (p : Star _↦_ a b) → Path a b (starLength p)
  fromStar ε = []
  fromStar (e ◅ p) = e ∷ fromStar p

  toStar-fromStar : ∀ {a b} (p : Star _↦_ a b) → p ≡ toStar (fromStar p)
  toStar-fromStar ε = refl
  toStar-fromStar (e ◅ p) = ≡.cong (e ◅_) (toStar-fromStar p)

  starLength-toStar : ∀ {a b n} (p : Path a b n) → n ≡ starLength (toStar p)
  starLength-toStar [] = refl
  starLength-toStar (e ∷ p) = ≡.cong suc (starLength-toStar p)

  fromStar-toStar : ∀ {a b n} (p : Path a b n) → p ≅ fromStar (toStar p)
  fromStar-toStar [] = refl
  fromStar-toStar (e ∷ p) =
    ≅.icong (Path _ _) {B = λ {x} _ → Path _ _ (suc x)}
      (starLength-toStar p)
      (e ∷_)
      (fromStar-toStar p)

  starTrail : ∀ {a b} (p : Star _↦_ a b) → Vec V (starLength p)
  starTrail ε = []
  starTrail {a} (e ◅ p) = a ∷ starTrail p

  trail-fromStar : ∀ {a b} (p : Star _↦_ a b) → starTrail p ≡ trail (fromStar p)
  trail-fromStar ε = refl
  trail-fromStar (e ◅ p) = ≡.cong (_ ∷_) (trail-fromStar p)

  starTrail-toStar : ∀ {a b n} (p : Path a b n) → trail p ≅ starTrail (toStar p)
  starTrail-toStar [] = refl
  starTrail-toStar {a} {b} {suc n} (e ∷ p) =
    ≅.icong (λ i → Vec V i) {B = λ {i} _ → Vec V (suc i)}
      (starLength-toStar p) (λ as → a ∷ as) (starTrail-toStar p)

module Embed {ℓᵥ ℓᵥ′ ℓₑ ℓₑ′}
  {V : Set ℓᵥ} {V′ : Set ℓᵥ′} {_↦_ : V → V → Set ℓₑ} {_↦′_ : V′ → V′ → Set ℓₑ′} {f}
  (r : _↦_ =[ f ]⇒ _↦′_) where

  open Path

  embedPath : ∀ {a b n} → Path _↦_ a b n → Path _↦′_ (f a) (f b) n
  embedPath [] = []
  embedPath (e ∷ es) = r e ∷ embedPath es

record FiniteGraph ℓᵥ ℓₑ : Set (ℓ.suc ℓᵥ ⊔ ℓ.suc ℓₑ) where
  field
    {Vertex} : Set ℓᵥ
    {Edge} : Vertex → Vertex → Set ℓₑ
    {{vertexFinite}} : IsFinite Vertex
    {{edgeFinite}} : ∀ a → IsFinite (∃ (Edge a))
    decEqVertex : (a b : Vertex) → Dec (a ≡ b)

  open Path Edge public


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommAlgebra.Instances.Unit where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Unit

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Instances.Unit
open import Cubical.Algebra.CommAlgebra

private
  variable
    ℓ ℓ' : Level

open CommAlgebraStr

module _ (R : CommRing ℓ) where

  UnitCommAlgebra : CommAlgebra R ℓ'
  UnitCommAlgebra = commAlgebraFromCommRing
      UnitCommRing
      (λ _ _ → tt*) (λ _ _ _ → refl) (λ _ _ _ → refl)
      (λ _ _ _ → refl) (λ _ → refl) (λ _ _ _ → refl)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
factorial : ℕ → ℕ
factorial zero = 1
factorial (suc n) = suc n * factorial n

max_issues_repo_name: seanwallawalla-forks/RosettaCodeData

max_forks_repo_name: seanwallawalla-forks/RosettaCodeData


text:
{-# OPTIONS --cubical --no-import-sorts --no-exact-split --safe #-}
module Cubical.Data.Queue.Truncated2List where

open import Cubical.Foundations.Everything

open import Cubical.Foundations.SIP
open import Cubical.Structures.Queue

open import Cubical.Data.Maybe
open import Cubical.Data.List
open import Cubical.Data.Sigma

open import Cubical.Data.Queue.1List

module Truncated2List {ℓ} (A : Type ℓ) (Aset : isSet A) where
 open Queues-on A Aset

 data Q : Type ℓ where
   Q⟨_,_⟩ : (xs ys : List A) → Q
   tilt : ∀ xs ys z → Q⟨ xs ++ [ z ] , ys ⟩ ≡ Q⟨ xs , ys ++ [ z ] ⟩
   trunc : (q q' : Q) (α β : q ≡ q') → α ≡ β

 multitilt : (xs ys zs : List A) → Q⟨ xs ++ rev zs , ys ⟩ ≡ Q⟨ xs , ys ++ zs ⟩
 multitilt xs ys [] = cong₂ Q⟨_,_⟩ (++-unit-r xs) (sym (++-unit-r ys))
 multitilt xs ys (z ∷ zs) =
   cong (λ ws → Q⟨ ws , ys ⟩) (sym (++-assoc xs (rev zs) [ z ]))
   ∙ tilt (xs ++ rev zs) ys z
   ∙ multitilt xs (ys ++ [ z ]) zs
   ∙ cong (λ ws → Q⟨ xs , ws ⟩) (++-assoc ys [ z ] zs)

  -- enq into the first list, deq from the second if possible

 emp : Q
 emp = Q⟨ [] , [] ⟩

 enq : A → Q → Q
 enq a Q⟨ xs , ys ⟩ = Q⟨ a ∷ xs , ys ⟩
 enq a (tilt xs ys z i) = tilt (a ∷ xs) ys z i
 enq a (trunc q q' α β i j) =
   trunc _ _ (cong (enq a) α) (cong (enq a) β) i j

 deqFlush : List A → Maybe (Q × A)
 deqFlush [] = nothing
 deqFlush (x ∷ xs) = just (Q⟨ [] , xs ⟩ , x)

 deq : Q → Maybe (Q × A)
 deq Q⟨ xs , [] ⟩ = deqFlush (rev xs)
 deq Q⟨ xs , y ∷ ys ⟩ = just (Q⟨ xs , ys ⟩ , y)
 deq (tilt xs [] z i) = path i
   where
   path : deqFlush (rev (xs ++ [ z ])) ≡ just (Q⟨ xs , [] ⟩ , z)
   path =
     cong deqFlush (rev-++ xs [ z ])
     ∙ cong (λ q → just (q , z)) (sym (multitilt [] [] (rev xs)))
     ∙ cong (λ ys → just (Q⟨ ys , [] ⟩ , z)) (rev-rev xs)
 deq (tilt xs (y ∷ ys) z i) = just (tilt xs ys z i , y)
 deq (trunc q q' α β i j) =
   isOfHLevelMaybe 0
     (isSetΣ trunc λ _ → Aset)
     (deq q) (deq q') (cong deq α) (cong deq β)
    i j

 Raw : RawQueue
 Raw = (Q , emp , enq , deq)

 -- We construct an equivalence to 1Lists and prove this is an equivalence of queue structures

 private
   module One = 1List A Aset
   open One renaming (Q to Q₁; emp to emp₁; enq to enq₁; deq to deq₁) using ()

 quot : Q₁ → Q
 quot xs = Q⟨ xs , [] ⟩

 eval : Q → Q₁
 eval Q⟨ xs , ys ⟩ = xs ++ rev ys
 eval (tilt xs ys z i) = path i
   where
   path : (xs ++ [ z ]) ++ rev ys ≡ xs ++ rev (ys ++ [ z ])
   path =
     ++-assoc xs [ z ] (rev ys)
     ∙ cong (_++_ xs) (sym (rev-++ ys [ z ]))
 eval (trunc q q' α β i j) = -- truncated case
   isOfHLevelList 0 Aset (eval q) (eval q') (cong eval α) (cong eval β) i j

 quot∘eval : ∀ q → quot (eval q) ≡ q
 quot∘eval Q⟨ xs , ys ⟩ = multitilt xs [] ys
 quot∘eval (tilt xs ys z i) = -- truncated case
   isOfHLevelPathP'
     {A = λ i → quot (eval (tilt xs ys z i)) ≡ tilt xs ys z i}
     0
     (trunc _ _)
     (multitilt (xs ++ [ z ]) [] ys) (multitilt xs [] (ys ++ [ z ]))
     .fst i
 quot∘eval (trunc q q' α β i j) = -- truncated case
   isOfHLevelPathP'
     {A = λ i →
       PathP (λ j → quot (eval (trunc q q' α β i j)) ≡ trunc q q' α β i j)
         (quot∘eval q) (quot∘eval q')}
     0
     (isOfHLevelPathP' 1 (isOfHLevelSuc 2 trunc _ _) _ _)
     (cong quot∘eval α) (cong quot∘eval β)
     .fst i j

 eval∘quot : ∀ xs → eval (quot xs) ≡ xs
 eval∘quot = ++-unit-r

 -- We get our desired equivalence
 quotEquiv : Q₁ ≃ Q
 quotEquiv = isoToEquiv (iso quot eval quot∘eval eval∘quot)

 -- Now it only remains to prove that this is an equivalence of queue structures
 quot∘emp : quot emp₁ ≡ emp
 quot∘emp = refl

 quot∘enq : ∀ x xs → quot (enq₁ x xs) ≡ enq x (quot xs)
 quot∘enq x xs = refl

 quot∘deq : ∀ xs → deqMap quot (deq₁ xs) ≡ deq (quot xs)
 quot∘deq [] = refl
 quot∘deq (x ∷ []) = refl
 quot∘deq (x ∷ x' ∷ xs) =
   deqMap-∘ quot (enq₁ x) (deq₁ (x' ∷ xs))
   ∙ sym (deqMap-∘ (enq x) quot (deq₁ (x' ∷ xs)))
   ∙ cong (deqMap (enq x)) (quot∘deq (x' ∷ xs))
   ∙ lemma x x' (rev xs)
   where
   lemma : ∀ x x' ys
     → deqMap (enq x) (deqFlush (ys ++ [ x' ]))
       ≡ deqFlush ((ys ++ [ x' ]) ++ [ x ])
   lemma x x' [] i = just (tilt [] [] x i , x')
   lemma x x' (y ∷ ys) i = just (tilt [] (ys ++ [ x' ]) x i , y)

 quotEquivHasQueueEquivStr : RawQueueEquivStr One.Raw Raw quotEquiv
 quotEquivHasQueueEquivStr = quot∘emp , quot∘enq , quot∘deq

 -- And we get a path between the raw 1Lists and 2Lists
 Raw-1≡2 : One.Raw ≡ Raw
 Raw-1≡2 = sip rawQueueUnivalentStr _ _ (quotEquiv , quotEquivHasQueueEquivStr)

 -- We derive the axioms for 2List from those for 1List
 WithLaws : Queue
 WithLaws = Q , str Raw , subst (uncurry QueueAxioms) Raw-1≡2 (snd (str One.WithLaws))

 WithLaws-1≡2 : One.WithLaws ≡ WithLaws
 WithLaws-1≡2 = sip queueUnivalentStr _ _ (quotEquiv , quotEquivHasQueueEquivStr)

 Finite : FiniteQueue
 Finite = Q , str WithLaws , subst (uncurry FiniteQueueAxioms) WithLaws-1≡2 (snd (str One.Finite))

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Soundness where

{-
open import Relation.Binary.PropositionalEquality
open import Data.Nat hiding (_>_)
-}

open import StdLibStuff

open import Syntax
open import STT
open import FSC
open import DerivedProps
open import HelpDefs

mutual
 sound : {n : ℕ} {Γ-t : Ctx n} (Γ : FSC-Ctx n Γ-t) (F : Form Γ-t $o) →
         Γ ⊢ F →
         ⊢ (hypos Γ F)
 sound Γ .(F || G) (||-I-l {F} {G} p) = inf-V (traverse-hypos F (F || G) Γ ax-2-s) (sound Γ F p)
 sound Γ .(F || G) (||-I-r {F} {G} p) = inf-V (traverse-hypos G (F || G) Γ (inf-V (inf-V ax-4-s ax-3-s) ax-2-s)) (sound Γ G p)
 sound Γ .(F & G) (&-I {F} {G} pF pG) = inf-V (inf-V (traverse-hypos-pair-I F G Γ) (sound Γ F pF)) (sound Γ G pG)
 sound Γ .(F => G) (=>-I {F} {G} p) = sound (F ∷h Γ) G p
 sound Γ .(~ F) (~-I {F} p) = inf-V (traverse-hypos (F => $false) (~ F) Γ (lem10 F)) (sound (F ∷h Γ) $false p)
 sound Γ .(![ t ] F) (!-I {t} {F} p) = traverse-=>-I-dep t F Γ (inf-VI-s (sound (t ∷ Γ) F p))
 sound Γ .(!'[ t ] F) (!'-I {t} {F} p) = traverse-=>-I-dep' t F Γ (sound (t ∷ Γ) (weak F · $ this {refl}) p)
 sound Γ F (elim x p) = inf-V (traverse-hypos-elim F Γ x) (sound-elim Γ (lookup-hyp Γ x) F p)
 sound Γ F (ac {t} p) = inf-V (traverse-hypos ((![ t > $o ] ((?[ t ] (var (next this) refl · var this refl)) => (var this refl · (ι t (var (next this) refl · var this refl))))) => F) F Γ (inf-V (lemb3 (![ t > $o ] ((?[ t ] (var (next this) refl · var this refl)) => (var this refl · ι t (var (next this) refl · var this refl)))) F) (inf-VI-s (ax-11-s {_} {(t > $o) ∷ _} {t} {var (next this) refl · var this refl})))) (sound-elim Γ (![ t > $o ] ((?[ t ] (var (next this) refl · var this refl)) => (var this refl · (ι t (var (next this) refl · var this refl))))) F p)
 sound Γ F (ac' {t} p) = inf-V (traverse-hypos ((![ t > $o ] ((?[ t ] ($ (next this) {refl} · $ this {refl})) => ($ this {refl} · ι' t ($ this {refl})))) => F) F Γ (inf-V (lemb3 (![ t > $o ] ((?[ t ] ($ (next this) {refl} · $ this {refl})) => ($ this {refl} · ι' t ($ this {refl})))) F) (inf-VI-s (ax-11-s2 ($ this {refl}))))) (sound-elim Γ (![ t > $o ] ((?[ t ] ($ (next this) {refl} · $ this {refl})) => ($ this {refl} · ι' t ($ this {refl})))) F p)
 sound Γ .(?[ t ] F) (?-I {t} {F} G p) = inf-V (traverse-hypos (sub G F) (?[ t ] F) Γ (inf-V ax-3-s (ax-5-s (~ F) G))) (sound Γ (sub G F) p)
 sound Γ .(?'[ t ] F) (?'-I {t} {F} G p) = inf-V (traverse-hypos (app F G) (?'[ t ] F) Γ (inf-V ax-3-s (ax-5-s2 F G))) (sound Γ (app F G) p)
 sound Γ .$true $true-I = traverse-hypos-use $true Γ (inf-VI-s (inf-V (inf-V ax-4-s ax-1-s) ax-2-s))
 sound Γ .(F == G) (==-I {t} {F} {G} p) = sound-== Γ t F G p
 sound Γ .(F ((^[ t ] G) · H)) (reduce {t} {u} {F} {G} {H} p) = inf-V (traverse-hypos (F (sub H G)) (F ((^[ t ] G) · H)) Γ (inf-III-samectx (λ x → (F x)) G H)) (sound Γ (F (sub H G)) p)
 sound Γ F (raa p) = inf-V (traverse-hypos (~ (~ F)) F Γ (lemb2 F)) (sound _ _ p)

 sound-elim : ∀ {n Γ-t} → (Γ : FSC-Ctx n Γ-t) (F G : Form Γ-t $o) →
  Γ , F ⊢ G →
  ⊢ (hypos Γ (F => G))
 sound-elim Γ F G (use p) = inf-V (traverse-hypos (G == F) (F => G) Γ (lem13 F G)) (sound-↔ Γ $o G F p)
 sound-elim Γ .(F & G) H (&-E-l {F} {G} p) = inf-V (traverse-hypos (F => H) ((F & G) => H) Γ (lem6 F G H)) (sound-elim Γ F H p)
 sound-elim Γ .(F & G) H (&-E-r {F} {G} p) = inf-V (traverse-hypos (G => H) ((F & G) => H) Γ (lem6b F G H)) (sound-elim Γ G H p)
 sound-elim Γ .(F => G) H (=>-E {F} {G} p₁ p₂) = inf-V (inf-V (traverse-hypos2 F (G => H) ((F => G) => H) Γ (lem7 F G H)) (sound Γ F p₁)) (sound-elim Γ G H p₂)
 sound-elim Γ .(~ F) H (~-E {F} p) = inf-V (traverse-hypos F (~ F => H) Γ (lemb4 F H)) (sound Γ F p)
 sound-elim Γ .(![ t ] F) H (!-E {t} {F} G p) = inf-V (traverse-hypos (sub G F => H) (![ t ] F => H) Γ (inf-V (lem9 (![ t ] F) (sub G F) H) (ax-5-s F G))) (sound-elim Γ (sub G F) H p)
 sound-elim Γ .(!'[ t ] F) H (!'-E {t} {F} G p) = inf-V (traverse-hypos ((F · G) => H) (!'[ t ] F => H) Γ (inf-V (lem9 (!'[ t ] F) (F · G) H) (ax-5-s3 F G))) (sound-elim Γ (F · G) H p)
 sound-elim Γ .$false H $false-E = traverse-hypos-use ($false => H) Γ (lem11 H)
 sound-elim Γ .(F || G) H (||-E {F} {G} p₁ p₂) = inf-V (inf-V (traverse-hypos2 (F => H) (G => H) ((F || G) => H) Γ (lemb5 F G H)) (sound _ _ p₁)) (sound _ _ p₂)
 sound-elim Γ .(?[ t ] F) H (?-E {t} {F} p) = inf-V (traverse-hypos (sub (ι t F) F => H) (?[ t ] F => H) Γ (inf-V (lem9 (?[ t ] F) (sub (ι t F) F) H) (ax-11-s {_} {_} {_} {F}))) (sound-elim Γ (sub (ι t F) F) H p)
 sound-elim Γ .(?'[ t ] F) H (?'-E {t} {F} p) = inf-V (traverse-hypos ((F · ι' _ F) => H) (?'[ t ] F => H) Γ (inf-V (lem9 (?'[ t ] F) (F · ι' t F) H) (ax-11-s2 F))) (sound-elim Γ (F · ι' _ F) H p)
 sound-elim Γ .(F ((^[ t ] G) · H)) I (reduce {t} {u} {F} {G} {H} p) = inf-V (traverse-hypos (F (sub H G) => I) (F ((^[ t ] G) · H) => I) Γ (inf-V (lem9 (F ((^[ t ] G) · H)) (F (sub H G)) I) (inf-II-samectx (λ x → (F x)) G H))) (sound-elim Γ (F (sub H G)) I p)
 sound-elim Γ .(F == G) H (r-bool-ext {F} {G} p) = inf-V (traverse-hypos (((F => G) & (G => F)) => H) ((F == G) => H) Γ (inf-V (lem9 (F == G) ((F => G) & (G => F)) H) (inf-V (lem2 (F == G) (F => G) (G => F)) (inf-V (inf-V (lemb1 ((F == G) => (F => G)) ((F == G) => (G => F))) (inf-V ax-3-s (inf-V (inf-V ax-4-s (inf-V (lem5 (F == G) (G == F)) (lem15 F G))) (inf-V ax-3-s (lem13 F G))))) (lem13 G F))))) (sound-elim Γ ((F => G) & (G => F)) H p)
 sound-elim Γ .(F == G) H (r-fun-ext {t} {u} {F} {G} I p) = inf-V (traverse-hypos (((F · I) == (G · I)) => H) ((F == G) => H) Γ (inf-V (lem9 (F == G) ((F · I) == (G · I)) H) (inf-V (inf-V (lem4 (F == G) (I == I) ((F · I) == (G · I))) (lem16 F G I I)) (lem12 I)))) (sound-elim Γ ((F · I) == (G · I)) H p)

 sound-== : ∀ {n Γ-t} → (Γ : FSC-Ctx n Γ-t) (t : Type n) (F G : Form Γ-t t) →
  Γ ⊢ t ∋ F == G →
  ⊢ (hypos Γ (F == G))
 sound-== Γ t F G (simp p) = sound-↔ Γ t F G p
 sound-== Γ t F G (step F' G' x p₁ p₂ p₃) = inf-V (inf-V (inf-V (traverse-hypos3 (F == F') (F' == G') (G' == G) (F == G) Γ (lem14 F F' G' G)) (sound-↔ Γ t F F' p₂)) (inf-V (traverse-hypos-elim (F' == G') Γ x) (sound-==-elim Γ (lookup-hyp Γ x) t F' G' p₁))) (sound-== Γ t G' G p₃)
 sound-== Γ .$o F G (bool-ext p) = inf-V (traverse-hypos ((F => G) & (G => F)) (F == G) Γ ax-10-a-s) (sound _ _ p)
 sound-== Γ .(t > u) F G (fun-ext {t} {u} p) = inf-V (traverse-hypos (![ t ] (((weak F) · $ this {refl}) == ((weak G) · $ this {refl}))) (F == G) Γ ax-10-b-s2) (traverse-=>-I-dep t ((weak F · $ this {refl}) == (weak G · $ this {refl})) Γ (inf-VI-s (sound-== (t ∷ Γ) u (weak F · $ this {refl}) (weak G · $ this {refl}) p)))

 sound-↔ : ∀ {n Γ-t} → (Γ : FSC-Ctx n Γ-t) (t : Type n) (F G : Form Γ-t t) →
  Γ ⊢ t ∋ F ↔ G →
  ⊢ (hypos Γ (F == G))
 sound-↔ Γ t .(var x p) .(var x p) (head-var ._ x p) = traverse-hypos-use (var x p == var x p) Γ (lem12 (var x p))
 sound-↔ Γ .t .c .c (head-const t c) = traverse-hypos-use (c == c) Γ (lem12 c)
 sound-↔ Γ .t₂ .(F₁ · G₁) .(F₂ · G₂) (head-app t₁ t₂ F₁ F₂ G₁ G₂ p₁ p₂) = inf-V (inf-V (traverse-hypos2 (F₁ == F₂) (G₁ == G₂) ((F₁ · G₁) == (F₂ · G₂)) Γ (lem16 F₁ F₂ G₁ G₂)) (sound-== Γ _ F₁ F₂ p₁)) (sound-== Γ _ G₁ G₂ p₂)
 sound-↔ Γ .(t₁ > t₂) .(lam t₁ F₁) .(lam t₁ F₂) (head-lam t₁ t₂ F₁ F₂ p) = traverse-hypos-eq-=>-I F₁ F₂ Γ (sound-== (t₁ ∷ Γ) t₂ F₁ F₂ p)
 sound-↔ Γ .(t₁ > t₂) .F₁ .(lam t₁ F₂) (head-lam-eta-left t₁ t₂ F₁ F₂ p) = inf-V (traverse-hypos (![ t₁ ] ((weak F₁ · $ this {refl}) == F₂)) (F₁ == lam t₁ F₂) Γ (inf-V (inf-V ax-4-s ax-10-b-s2) (subst (λ z → ⊢ ((![ t₁ ] ((weak F₁ · $ this {refl}) == z)) => (![ t₁ ] ((weak F₁ · $ this {refl}) == (weak (^[ t₁ ] F₂) · $ this {refl}))))) (sub-sub-weak-weak-p-3 F₂) (inf-III _ (t₁ ∷ ε) (λ z → ![ t₁ ] ((weak F₁ · $ this {refl}) == z)) (weak-i (t₁ ∷ ε) _ F₂) ($ this {refl}))))) (tst3' {_} {_} {ε} ((weak F₁ · $ this {refl}) == F₂) Γ refl (sound-== (t₁ ∷ Γ) t₂ (weak F₁ · $ this {refl}) F₂ p))
 sound-↔ Γ .(t₁ > t₂) .(lam t₁ F₂) .F₁ (head-lam-eta-right t₁ t₂ F₁ F₂ p) = inf-V (traverse-hypos (![ t₁ ] (F₂ == (weak F₁ · $ this {refl}))) (lam t₁ F₂ == F₁) Γ (inf-V (inf-V ax-4-s ax-10-b-s2) (subst (λ z → ⊢ ((![ t₁ ] (z == (weak F₁ · $ this {refl}))) => (![ t₁ ] ((weak (^[ t₁ ] F₂) · $ this {refl}) == (weak F₁ · $ this {refl}))))) (sub-sub-weak-weak-p-3 F₂) (inf-III _ (t₁ ∷ ε) (λ z → ![ t₁ ] (z == (weak F₁ · $ this {refl}))) (weak-i (t₁ ∷ ε) _ F₂) ($ this {refl}))))) (tst3' {_} {_} {ε} (F₂ == (weak F₁ · $ this {refl})) Γ refl (sound-== (t₁ ∷ Γ) t₂ F₂ (weak F₁ · $ this {refl}) p))
 sound-↔ Γ t .(F₁ ((^[ u ] G') · H)) G (reduce-l {.t} {u} {v} {F₁} {G'} {H} p) = inf-V (traverse-hypos (F₁ (sub H G') == G) (F₁ ((^[ u ] G') · H) == G) Γ (inf-III-samectx (λ x → (F₁ x == G)) G' H)) (sound-↔ Γ t (F₁ (sub H G')) G p)
 sound-↔ Γ t F .(F₂ ((^[ u ] G) · H)) (reduce-r {.t} {u} {v} {F₂} {G} {H} p) = inf-V (traverse-hypos (F == F₂ (sub H G)) (F == F₂ ((^[ u ] G) · H)) Γ (inf-III-samectx (λ x → (F == F₂ x)) G H)) (sound-↔ Γ t F (F₂ (sub H G)) p)

 sound-==-elim : ∀ {n Γ-t} → (Γ : FSC-Ctx n Γ-t) (F : Form Γ-t $o) (t : Type n) (G H : Form Γ-t t) →
  Γ , F ⊢ G == H →
  ⊢ (hypos Γ (F => (G == H)))
 sound-==-elim Γ .(G == H) t G H use = traverse-hypos-use ((G == H) => (G == H)) Γ (inf-V (inf-V ax-4-s ax-1-s) ax-2-s)
 sound-==-elim Γ F t G H (use' p) = traverse-hypos-use (F => (G == H)) Γ (hn-form (λ z → z => (G == H)) _ 2 (subst (λ z → ⊢ (z => (G == H))) p (hn-form (λ z → headNorm 2 (G == H) => z) _ 2 (inf-V (inf-V ax-4-s ax-1-s) ax-2-s))))
 sound-==-elim Γ .(H == G) t G H use-sym = traverse-hypos-use ((H == G) => (G == H)) Γ (lem15 H G)
 sound-==-elim Γ .(F & G') t G H (&-E-l {F} {G'} p) = inf-V (traverse-hypos (F => (G == H)) ((F & G') => (G == H)) Γ (lem6 F G' (G == H))) (sound-==-elim Γ F t G H p)
 sound-==-elim Γ .(F & G') t G H (&-E-r {F} {G'} p) = inf-V (traverse-hypos (G' => (G == H)) ((F & G') => (G == H)) Γ (lem6b F G' (G == H))) (sound-==-elim Γ G' t G H p)
 sound-==-elim Γ .(F => G') t G H (=>-E {F} {G'} p₁ p₂) = inf-V (inf-V (traverse-hypos2 F (G' => (G == H)) ((F => G') => (G == H)) Γ (lem7 F G' (G == H))) (sound Γ F p₁)) (sound-==-elim Γ G' t G H p₂)
 sound-==-elim Γ .(![ u ] F) t G H (!-E {u} {F} G' p) = inf-V (traverse-hypos (sub G' F => (G == H)) (![ u ] F => (G == H)) Γ (inf-V (lem9 (![ u ] F) (sub G' F) (G == H)) (ax-5-s F G'))) (sound-==-elim Γ (sub G' F) t G H p)
 sound-==-elim Γ .(!'[ u ] F) t G H (!'-E {u} {F} G' p) = inf-V (traverse-hypos ((F · G') => (G == H)) (!'[ u ] F => (G == H)) Γ (inf-V (lem9 (!'[ u ] F) (F · G') (G == H)) (ax-5-s3 F G'))) (sound-==-elim Γ (F · G') t G H p)
 sound-==-elim Γ .(?[ u ] F) t G H (?-E {u} {F} p) = inf-V (traverse-hypos (sub (ι u F) F => (G == H)) (?[ u ] F => (G == H)) Γ (inf-V (lem9 (?[ u ] F) (sub (ι u F) F) (G == H)) (ax-11-s {_} {_} {_} {F}))) (sound-==-elim Γ (sub (ι u F) F) t G H p)
 sound-==-elim Γ .(?'[ u ] F) t G H (?'-E {u} {F} p) = inf-V (traverse-hypos ((F · ι' u F) => (G == H)) (?'[ u ] F => (G == H)) Γ (inf-V (lem9 (?'[ u ] F) (F · ι' u F) (G == H)) (ax-11-s2 F))) (sound-==-elim Γ (F · ι' u F) t G H p)
 sound-==-elim Γ .(F ((^[ u ] G') · H')) t G H (reduce {u} {v} {F} {G'} {H'} p) = inf-V (traverse-hypos (F (sub H' G') => (G == H)) (F ((^[ u ] G') · H') => (G == H)) Γ (inf-V (lem9 (F ((^[ u ] G') · H')) (F (sub H' G')) (G == H)) (inf-II-samectx (λ x → (F x)) G' H'))) (sound-==-elim Γ (F (sub H' G')) t G H p)
 sound-==-elim Γ .(F == G) t H I (r-bool-ext {F} {G} p) = inf-V (traverse-hypos (((F => G) & (G => F)) => (H == I)) ((F == G) => (H == I)) Γ (inf-V (lem9 (F == G) ((F => G) & (G => F)) (H == I)) (inf-V (lem2 (F == G) (F => G) (G => F)) (inf-V (inf-V (lemb1 ((F == G) => (F => G)) ((F == G) => (G => F))) (inf-V ax-3-s (inf-V (inf-V ax-4-s (inf-V (lem5 (F == G) (G == F)) (lem15 F G))) (inf-V ax-3-s (lem13 F G))))) (lem13 G F))))) (sound-==-elim Γ ((F => G) & (G => F)) t H I p)
 sound-==-elim Γ .(F == G) t H I (r-fun-ext {u} {v} {F} {G} J p) = inf-V (traverse-hypos (((F · J) == (G · J)) => (H == I)) ((F == G) => (H == I)) Γ (inf-V (lem9 (F == G) ((F · J) == (G · J)) (H == I)) (inf-V (inf-V (lem4 (F == G) (J == J) ((F · J) == (G · J))) (lem16 F G J J)) (lem12 J)))) (sound-==-elim Γ ((F · J) == (G · J)) t H I p)

sound-top : {n : ℕ} (F : Form {n} ε $o) →
            ε ⊢ F →
            ⊢ F
sound-top = sound ε

max_stars_repo_name: frelindb/agsyHOL

max_issues_repo_name: frelindb/agsyHOL

max_forks_repo_name: frelindb/agsyHOL


text:
{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.polarity:10 #-}
module Issue44 where

data Ty : Set where
  ι : Ty
  _⇒_ : Ty -> Ty -> Ty

data Con : Set where
  ε : Con
  _<_ : Con -> Ty -> Con

data Var : Con -> Ty -> Set where
  vZ : forall {Γ σ} -> Var (Γ < σ) σ
  vS : forall {Γ σ}{τ : Ty} -> Var Γ σ -> Var (Γ < τ) σ

{-
stren : forall {Γ σ} -> Var Γ σ -> Con
stren (vZ {Γ}) = Γ
stren (vS {τ = τ} v) = stren v < τ

_/_ : forall Γ {σ} -> Var Γ σ -> Con
Γ / v = stren v
-}

-- However if I make stren a local function:

_/_ : forall Γ {σ} -> Var Γ σ -> Con
Γ / v = stren v where
  stren : forall {Γ σ} -> Var Γ σ -> Con
  stren (vZ {Γ}) = Γ
  stren (vS {τ = τ} v) = stren v < τ

thin : forall {Γ σ τ}(v : Var Γ σ) -> Var (Γ / v) τ -> Var Γ τ
thin vZ v' = vS v'
thin (vS v) vZ = vZ
thin (vS v) (vS v') = vS (thin v v')


text:
open import Agda.Builtin.Nat
open import Agda.Builtin.FromNat
open import Data.Unit using (⊤)
open import Function using (const)

module Data.Nat.FromNat where

instance
  NumberNat : Number Nat
  NumberNat = record { Constraint = const ⊤ ; fromNat = λ n → n }

max_stars_repo_name: wenkokke/nodcap

max_issues_repo_name: pepijnkokke/nodcap

max_forks_repo_name: pepijnkokke/nodcap


text:
module _ where

open import Agda.Builtin.IO
open import Agda.Builtin.String
open import Agda.Builtin.Unit

data D (A : Set) : Set where
  L : A → D A
  R : A → D A

data T : Set where
  Var : (s : D String) → T

test : T → String
test (Var (L "abc")) = ""
test (Var (L s)) = ""
test (Var (R s)) = ""


text:
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc)
open import Relation.Nullary using (Dec; yes; no)

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n : ℕ} → zero ≤ n
  s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n

_≤?_ : ∀ (m n : ℕ) → Dec (m ≤ n)
zero ≤? n = yes z≤n
suc m ≤? zero = no λ()
suc m ≤? suc n with m ≤? n
... | yes m≤n = yes (s≤s m≤n)
... | no ¬m≤n = no λ{ (s≤s m≤n) → ¬m≤n m≤n }

_ : 2 ≤? 4 ≡ yes (s≤s (s≤s z≤n))
_ = refl

_ : 4 ≤? 2 ≡ no {!!}
_ = refl

{-
Using ^C ^N, the term
  4 ≤? 2
evaluates to
  no (λ { (s≤s m≤n) → (λ { (s≤s m≤n) → (λ ()) 1 m≤n }) m≤n })
The 1 is spurious.
-}


text:
module Matrix where

open import Data.Nat
open import Data.Vec

Matrix : (A : Set) → ℕ → ℕ → Set
Matrix A m n = Vec (Vec A m) n

transpose : ∀ {A m n} → Matrix A m n → Matrix A n m
transpose [] = replicate []
transpose (xs ∷ xss) = zipWith _∷_ xs (transpose xss)

a = (1 ∷ 2 ∷ 3 ∷ []) ∷ (4 ∷ 5 ∷ 6 ∷ []) ∷ []
b = transpose a


text:
-- Andreas, 2015-07-01, Issue 1599:
-- abstract data needs to be positivity checked!

-- {-# OPTIONS -v tc.pos:80 #-}

data ⊥ : Set where

abstract

  T : Set → Set
  T X = X → ⊥

  data D : Set where
    lam : T D → D

  app : D → D → ⊥
  app (lam f) = f

  omega : D
  omega = lam λ x → app x x

  Omega : ⊥
  Omega = app omega omega

absurd : ⊥
absurd = Omega


text:
-- submitted by Nisse, 2011-06-21

-- {-# OPTIONS -v tc.lhs.unify:15 --show-implicit #-}

module Issue423 where

-- import Common.Level

------------------------------------------------------------------------
-- Prelude

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

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

curry : {A C : Set} {B : A → Set} →
        (Σ A B → C) → ((x : A) → B x → C)
curry f x y = f (x , y)

uncurry : {A C : Set} {B : A → Set} →
          ((x : A) → (y : B x) → C) → (Σ A B → C)
uncurry f (x , y) = f x y

------------------------------------------------------------------------
-- Preliminaries

postulate
  U  : Set
  El : U → Set

mutual

  data Ctxt : Set where
    _▻_ : (Γ : Ctxt) (σ : Type Γ) → Ctxt

  Type : Ctxt → Set
  Type Γ = Env Γ → U

  Env : Ctxt → Set
  Env (Γ ▻ σ) = Σ (Env Γ) λ γ → El (σ γ)

postulate
  Γ : Ctxt
  σ : Type Γ

------------------------------------------------------------------------
-- Problem

-- The following equalites hold definitionally.

curry∘uncurry : (τ : (γ : Env Γ) → El (σ γ) → U) →
                curry (uncurry τ) ≡ τ
curry∘uncurry τ = refl

uncurry∘curry : (τ : Env (Γ ▻ σ) → U) →
                uncurry (curry τ) ≡ τ
uncurry∘curry τ = refl

-- Bug was:
-- However, the two sides of curry∘uncurry behave differently.

works : (τ₁ τ₂ : (γ : Env Γ) → El (σ γ) → U) →
        τ₁ ≡ τ₂ → Set₁
works τ .τ refl = Set

works′ : (τ₁ τ₂ : (γ : Env Γ) → El (σ γ) → U) →
         curry (uncurry τ₁) ≡ τ₂ → Set₁
works′ τ .τ refl = Set

fails : (τ₁ τ₂ : (γ : Env Γ) → El (σ γ) → U) →
        τ₁ ≡ curry (uncurry τ₂) → Set₁
fails τ .τ refl = Set

fails′ : (τ₁ τ₂ : (γ : Env Γ) → El (σ γ) → U) →
         curry (uncurry τ₁) ≡ curry (uncurry τ₂) → Set₁
fails′ τ .τ refl = Set

-- Bug was:
-- I find it interesting that works′ works, whereas the symmetric
-- variant fails fails.


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

module Relation.Nullary.Decidable.Base where

open import Level
open import Data.Bool
open import Data.Empty

data Reflects {a} (A : Type a) : Bool → Type a where
  ofʸ  : (p   :    A) → Reflects A true
  ofⁿ  : (¬p  : ¬  A) → Reflects A false

record Dec {a} (A : Type a) : Type a where
  constructor _because_
  field
    does  : Bool
    why   : Reflects A does
open Dec public

pattern yes p  = true   because ofʸ p
pattern no ¬p  = false  because ofⁿ ¬p

map-reflects : ∀ {d} → (A → B) → (¬ A → ¬ B) → Reflects A d → Reflects B d
map-reflects to fro (ofʸ p) = ofʸ (to p)
map-reflects to fro (ofⁿ ¬p) = ofⁿ (fro ¬p)

map-dec : (A → B) → (¬ A → ¬ B) → Dec A → Dec B
map-dec to fro dec .does = dec .does
map-dec to fro dec .why = map-reflects to fro (dec .why)

⟦yes_,no_⟧ : (A → B) → (B → A) → Dec A → Dec B
⟦yes to ,no fro ⟧ = map-dec to λ ¬A ¬B → ¬A (fro ¬B)

∣_∣yes⇒_∣no⇒_ : Dec A → (A → B) → (¬ A → ¬ B) → Dec B
∣ d ∣yes⇒ y ∣no⇒ n = map-dec y n d

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


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

open import LogicalFormulae
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Order
open import Numbers.Naturals.Naturals -- for length
open import Lists.Lists
open import Orders.Partial.Definition
open import Orders.Total.Definition
open import Functions.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import Groups.FinitePermutations
open import Boolean.Definition

module Lists.SortList where
  isSorted : {a b : _} {A : Set a} (ord : TotalOrder A) (l : List A) → Set (a ⊔ b)
  isSorted ord [] = True'
  isSorted ord (x :: []) = True'
  isSorted ord (x :: (y :: l)) = (TotalOrder._≤_ ord x y) && (isSorted ord (y :: l))

  sortedTailIsSorted : {a b : _} {A : Set a} (ord : TotalOrder A) → (x : A) → (l : List A) → (isSorted ord (x :: l)) → isSorted ord l
  sortedTailIsSorted ord x [] pr = record {}
  sortedTailIsSorted ord x (y :: l) (fst ,, snd) = snd

  insert : {a b : _} {A : Set a} (ord : TotalOrder A) → (l : List A) → (isSorted ord l) → (x : A) → List A
  insert ord [] pr x = [ x ]
  insert ord (y :: l) pr x with TotalOrder.totality ord x y
  insert ord (y :: l) pr x | inl (inl x<y) = x :: (y :: l)
  insert ord (y :: l) pr x | inl (inr y<x) = y :: insert ord l (sortedTailIsSorted ord y l pr) x
  insert ord (y :: l) pr x | inr x=y = x :: (y :: l)

  insertionIncreasesLength : {a b : _} {A : Set a} (ord : TotalOrder A) → (l : List A) → (x : A) → (pr : isSorted ord l) → length (insert ord l pr x) ≡ succ (length l)
  insertionIncreasesLength ord [] x pr = refl
  insertionIncreasesLength ord (y :: l) x pr with TotalOrder.totality ord x y
  insertionIncreasesLength ord (y :: l) x pr | inl (inl x<y) = refl
  insertionIncreasesLength ord (y :: l) x pr | inl (inr y<x) = applyEquality succ (insertionIncreasesLength ord l x (sortedTailIsSorted ord y l pr))
  insertionIncreasesLength ord (y :: l) x pr | inr x=y = refl

  isEmpty : {a : _} {A : Set a} (l : List A) → Bool
  isEmpty [] = BoolTrue
  isEmpty (x :: l) = BoolFalse

  minList : {a b : _} {A : Set a} (ord : TotalOrder A) → (l : List A) → (isEmpty l ≡ BoolFalse) → A
  minList ord [] ()
  minList ord (x :: []) pr = x
  minList ord (x :: (y :: l)) refl with minList ord (y :: l) refl
  minList ord (x :: (y :: l)) refl | minSoFar with TotalOrder.totality ord x minSoFar
  minList ord (x :: (y :: l)) refl | minSoFar | inl (inl x<m) = x
  minList ord (x :: (y :: l)) refl | minSoFar | inl (inr m<x) = minSoFar
  minList ord (x :: (y :: l)) refl | minSoFar | inr x=m = x

  insertionSorts : {a b : _} {A : Set a} (ord : TotalOrder  A) → (l : List A) → (pr : isSorted ord l) → (x : A) → isSorted ord (insert ord l pr x)
  insertionSorts ord [] _ _ = record {}
  insertionSorts ord (y :: l) pr x with TotalOrder.totality ord x y
  insertionSorts ord (y :: l) pr x | inl (inl x<y) = inl x<y ,, pr
  insertionSorts ord (y :: l) pr x | inl (inr y<x) with insertionSorts ord l (sortedTailIsSorted ord y l pr) x
  ... | bl = {!!}
  insertionSorts ord (y :: l) pr x | inr x=y = inr x=y ,, pr

  orderNotLessThanAndEqual : {a b : _} {A : Set a} (ord : TotalOrder A) → {x y : A} → (x ≡ y) → TotalOrder._<_ ord x y → False
  orderNotLessThanAndEqual ord {x} {y} x=y x<y rewrite x=y = PartialOrder.irreflexive (TotalOrder.order ord) x<y

  orderToDecidableEquality : {a b : _} {A : Set a} (ord : TotalOrder A) → {x y : A} → (x ≡ y) || ((x ≡ y) → False)
  orderToDecidableEquality ord {x} {y} with TotalOrder.totality ord x y
  orderToDecidableEquality ord {x} {y} | inl (inl x<y) = inr λ x=y → orderNotLessThanAndEqual ord x=y x<y
  orderToDecidableEquality ord {x} {y} | inl (inr y<x) = inr λ x=y → orderNotLessThanAndEqual ord (equalityCommutative x=y) y<x
  orderToDecidableEquality ord {x} {y} | inr x=y = inl x=y

  --SortingAlgorithm : {a b : _} → Set (lsuc a ⊔ lsuc b)
  --SortingAlgorithm {a} {b} = {A : Set a} → (ord : TotalOrder {a} {b} A) → (input : List A) → Sg (List A) (λ l → isSorted ord l && isPermutation (orderToDecidableEquality ord) l input)

  insertionSort : {a b : _} {A : Set a} (ord : TotalOrder A) (l : List A) → List A
  insertionSortIsSorted : {a b : _} {A : Set a} (ord : TotalOrder A) (l : List A) → isSorted ord (insertionSort ord l)

  insertionSort ord [] = []
  insertionSort ord (x :: l) = insert ord (insertionSort ord l) (insertionSortIsSorted ord l) x
  insertionSortIsSorted ord [] = record {}
  insertionSortIsSorted ord (x :: l) = insertionSorts ord (insertionSort ord l) (insertionSortIsSorted ord l) x

  insertionSortLength : {a b : _} {A : Set a} (ord : TotalOrder A) (l : List A) → length l ≡ length (insertionSort ord l)
  insertionSortLength ord [] = refl
  insertionSortLength ord (x :: l) rewrite insertionIncreasesLength ord (insertionSort ord l) x (insertionSortIsSorted ord l) = {!!} --applyEquality succ (insertionSortLength ord l)

  isPermutation : {a b : _} {A : Set a} (ord : TotalOrder A) → (l m : List A) → Set a
  isPermutation ord l m = insertionSort ord l ≡ insertionSort ord m

  --insertionSort : {a b : _} → SortingAlgorithm {a} {b}
  --insertionSort {A = A} ord l = {!!}
  --  where
  --    lemma : Sg (List A) (isSorted ord) → (x : A) → Sg (List A) (isSorted ord)
  --    lemma (l , b) x = insert ord l b x , insertionSorts ord l b x

  --InsertionSort : {a b : _} → SortingAlgorithm {a} {b}
  --InsertionSort ord l = insertionSort ord l

  lexicographicOrderRel : {a b : _} {A : Set a} → (TotalOrder A) → Rel {a} {a ⊔ b} (List A)
  lexicographicOrderRel _ [] [] = False'
  lexicographicOrderRel _ [] (x :: l2) = True'
  lexicographicOrderRel _ (x :: l1) [] = False'
  lexicographicOrderRel order (x :: l1) (y :: l2) = (TotalOrder._<_ order x y) || ((x ≡ y) && lexicographicOrderRel order l1 l2)

  lexIrrefl : {a b : _} {A : Set a} (o : TotalOrder A) → {x : List A} → lexicographicOrderRel o x x → False
  lexIrrefl o {[]} ()
  lexIrrefl o {x :: l} (inl x<x) = PartialOrder.irreflexive (TotalOrder.order o) x<x
  lexIrrefl o {x :: l} (inr (pr ,, l=l)) = lexIrrefl o {l} l=l

  lexTransitive : {a b : _} {A : Set a} (o : TotalOrder A) → {x y z : List A} → lexicographicOrderRel o x y → lexicographicOrderRel o y z → lexicographicOrderRel o x z
  lexTransitive o {[]} {[]} {z} x<y y<z = y<z
  lexTransitive o {[]} {x :: y} {[]} record {} y<z = y<z
  lexTransitive o {[]} {x :: y} {x₁ :: z} record {} y<z = record {}
  lexTransitive o {x :: xs} {[]} {z} () y<z
  lexTransitive o {x :: xs} {y :: ys} {[]} (inl x<y) ()
  lexTransitive o {x :: xs} {y :: ys} {z :: zs} (inl x<y) (inl y<z) = inl (PartialOrder.<Transitive (TotalOrder.order o) x<y y<z)
  lexTransitive o {x :: xs} {y :: ys} {.y :: zs} (inl x<y) (inr (refl ,, ys<zs)) = inl x<y
  lexTransitive o {x :: xs} {.x :: ys} {[]} (inr (refl ,, xs<ys)) ()
  lexTransitive o {x :: xs} {.x :: ys} {z :: zs} (inr (refl ,, xs<ys)) (inl y<z) = inl y<z
  lexTransitive o {x :: xs} {.x :: ys} {.x :: zs} (inr (refl ,, xs<ys)) (inr (refl ,, u)) = inr (refl ,, lexTransitive o xs<ys u)

  lexTotal : {a b : _} {A : Set a} (o : TotalOrder A) → (x y : List A) → ((lexicographicOrderRel o x y) || (lexicographicOrderRel o y x)) || (x ≡ y)
  lexTotal o [] [] = inr refl
  lexTotal o [] (x :: y) = inl (inl (record {}))
  lexTotal o (x :: xs) [] = inl (inr (record {}))
  lexTotal o (x :: xs) (y :: ys) with TotalOrder.totality o x y
  lexTotal o (x :: xs) (y :: ys) | inl (inl x<y) = inl (inl (inl x<y))
  lexTotal o (x :: xs) (y :: ys) | inl (inr y<x) = inl (inr (inl y<x))
  lexTotal o (x :: xs) (y :: ys) | inr x=y with lexTotal o xs ys
  lexTotal o (x :: xs) (y :: ys) | inr x=y | inl (inl xs<ys) = inl (inl (inr (x=y ,, xs<ys)))
  lexTotal o (x :: xs) (y :: ys) | inr x=y | inl (inr ys<xs) = inl (inr (inr (equalityCommutative x=y ,, ys<xs)))
  lexTotal o (x :: xs) (y :: ys) | inr x=y | inr xs=ys rewrite x=y | xs=ys = inr refl

  lexicographicOrder : {a b : _} {A : Set a} → (TotalOrder A) → TotalOrder (List A)
  PartialOrder._<_ (TotalOrder.order (lexicographicOrder order)) = lexicographicOrderRel order
  PartialOrder.irreflexive (TotalOrder.order (lexicographicOrder order)) = lexIrrefl order
  PartialOrder.<Transitive (TotalOrder.order (lexicographicOrder order)) = lexTransitive order
  TotalOrder.totality (lexicographicOrder order) = lexTotal order

  badSort : {a b : _} {A : Set a} (order : TotalOrder A) → ℕ → List A → List A
  badSortLength : {a b : _} {A : Set a} (order : TotalOrder A) → (n : ℕ) → (l : List A) → length (badSort order n l) ≡ length l
  allTrueRespectsBadsort : {a b c : _} {A : Set a} (order : TotalOrder A) → (n : ℕ) → (l : List A) → (pred : A → Set c) → allTrue pred l → allTrue pred (badSort order n l)

  badSort order zero = insertionSort order
  badSort order (succ n) [] = []
  badSort {A = A} order (succ n) (x :: l) = head (badSort (lexicographicOrder order) n (permutations (x :: l))) bsNonempty
    where
      bs : List (List A)
      bs = badSort (lexicographicOrder order) n (permutations (x :: l))
      bsNonempty : 0 <N length bs
      bsNonempty with bs
      bsNonempty | [] = {!!}
      bsNonempty | bl :: _ = succIsPositive _

  allTrueRespectsBadsort order n [] pred record {} = {!!}
  allTrueRespectsBadsort order n (x :: l) pred (fst ,, snd) = {!!}
  badSortLength order zero [] = refl
  badSortLength order zero (x :: l) = transitivity (insertionIncreasesLength order (insertionSort order l) x (insertionSortIsSorted order l)) (applyEquality succ (equalityCommutative (insertionSortLength order l)))
  badSortLength order (succ n) [] = refl
  badSortLength order (succ n) (x :: l) = {!!}
    where
      allLen : allTrue (λ i → length i ≡ succ (length l)) (badSort (lexicographicOrder order) n (flatten (map (allInsertions x) (permutations l))))
      allLen = {!!}

-- TODO: show that insertion sort actually produces a permutation


text:
-- Andreas, 2017-11-12, issue #2803

-- Problem: names of hidden variable patterns
-- can get lost during case splitting.

-- They actually get lost already during lhs type checking,
-- but it is noticed only when printed back to the user
-- during case splitting.

-- {-# OPTIONS -v tc.lhs:40 #-}

record HFun (A B : Set) : Set where
  field apply : {a : A} → B

postulate A : Set

test : HFun A (A → A)
HFun.apply test {β} = {!!} -- C-c C-c

-- YIELDS:
-- HFun.apply test {a} x = ?

-- EXPECTED:
-- HFun.apply test {β} x = ?

max_stars_repo_name: asr/eagda

max_issues_repo_name: asr/eagda

max_forks_repo_name: asr/eagda


text:
{-# OPTIONS --injective-type-constructors #-}

module InjectiveTypeConstructors where

data D (A : Set) : Set where

data _==_ (A : Set) : Set → Set where
  refl : A == A

D' = D

injD : ∀ {A B} → D A == D' B → A == B
injD refl = refl

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- A quotient inductive-inductive definition of the lifting
-- construction on ω-cpos
------------------------------------------------------------------------

-- The code in this module is based on a suggestion from Paolo
-- Capriotti.

{-# OPTIONS --erased-cubical --safe #-}

open import Omega-cpo

module Lifting {ℓ} (cpo : ω-cpo ℓ ℓ) where

import Equality.Path as P
open import Equality.Propositional.Cubical
open import Logical-equivalence using (_⇔_)
open import Prelude hiding (⊥)

open import Bijection equality-with-J using (_↔_)
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J hiding (_∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J

private
  module CPO = ω-cpo cpo

------------------------------------------------------------------------
-- An ω-cppo

-- The carrier type (Carrier) and the information ordering (_⊑_) are
-- defined simultaneously.

infix 4 _⊑_ _⊒_

data Carrier : Type ℓ
data _⊑_     : Carrier → Carrier → Type ℓ

_⊒_ : Carrier → Carrier → Type ℓ
x ⊒ y = y ⊑ x

private
  variable
    x y : Carrier

-- Increasing sequences.

Increasing-sequence : Type ℓ
Increasing-sequence = ∃ λ (f : ℕ → Carrier) → ∀ n → f n ⊑ f (suc n)

-- Projection functions for Increasing-sequence.

infix 30 _[_]

_[_] : Increasing-sequence → ℕ → Carrier
_[_] = proj₁

increasing : (s : Increasing-sequence) →
             ∀ n → s [ n ] ⊑ s [ suc n ]
increasing = proj₂

-- Upper bounds.

Is-upper-bound : Increasing-sequence → Carrier → Type ℓ
Is-upper-bound s x = ∀ n → s [ n ] ⊑ x

-- Originally these types were postulated. After the release of
-- Cubical Agda they were turned into a QIIT, but in order to not get
-- any extra computation rules they were made abstract.

abstract

  -- _⊥ "constructors".

  data Carrier where
    never′        : Carrier
    now′          : CPO.Carrier → Carrier
    ⨆′            : Increasing-sequence → Carrier
    antisymmetry′ : x ⊑ y → x ⊒ y → x P.≡ y

    -- We have chosen to explicitly make the type set-truncated.
    -- However, this constructor is only used in the definition of the
    -- eliminator below.
    ≡-propositional′ : P.Is-set Carrier

  -- _⊑_ "constructors".

  data _⊑_ where
    ⊑-refl′            : ∀ x → x ⊑ x
    ⊑-trans′           : ∀ x y z → x ⊑ y → y ⊑ z → x ⊑ z
    never⊑′            : ∀ x → never′ ⊑ x
    upper-bound′       : ∀ s → Is-upper-bound s (⨆′ s)
    least-upper-bound′ : ∀ s ub → Is-upper-bound s ub → ⨆′ s ⊑ ub
    now-mono′          : ∀ {x y} → x CPO.⊑ y → now′ x ⊑ now′ y
    now-⨆″             : ∀ s →
                         now′ (CPO.⨆ s) ⊑
                         ⨆′ (Σ-map (now′ ∘_) (now-mono′ ∘_) s)
    ⊑-propositional′   : ∀ {x y} → P.Is-proposition (x ⊑ y)

  never : Carrier
  never = never′

  now : CPO.Carrier → Carrier
  now = now′

  ⨆ : Increasing-sequence → Carrier
  ⨆ = ⨆′

  antisymmetry : x ⊑ y → y ⊑ x → x ≡ y
  antisymmetry = λ p q → _↔_.from ≡↔≡ (antisymmetry′ p q)

  ⊑-refl : ∀ x → x ⊑ x
  ⊑-refl = ⊑-refl′

  ⊑-trans : ∀ x y z → x ⊑ y → y ⊑ z → x ⊑ z
  ⊑-trans = ⊑-trans′

  never⊑ : ∀ x → never ⊑ x
  never⊑ = never⊑′

  upper-bound : ∀ s → Is-upper-bound s (⨆ s)
  upper-bound = upper-bound′

  least-upper-bound : ∀ s ub → Is-upper-bound s ub → ⨆ s ⊑ ub
  least-upper-bound = least-upper-bound′

  now-mono : ∀ {x y} → x CPO.⊑ y → now x ⊑ now y
  now-mono = now-mono′

  now-⨆′ : ∀ s → now (CPO.⨆ s) ⊑ ⨆ (Σ-map (now ∘_) (now-mono ∘_) s)
  now-⨆′ = now-⨆″

  ⊑-propositional : ∀ {x y} → Is-proposition (x ⊑ y)
  ⊑-propositional {x = x} {y = y} =
                              $⟨ ⊑-propositional′ ⟩
    P.Is-proposition (x ⊑ y)  ↝⟨ _↔_.from (H-level↔H-level 1) ⟩□
    Is-proposition (x ⊑ y)    □

-- The construction above is an ω-cppo.

cppo : ω-cppo ℓ ℓ
cppo = record
  { cpo = record
    { Carrier           = Carrier
    ; _⊑_               = _⊑_
    ; reflexivity       = ⊑-refl _
    ; antisymmetry      = antisymmetry
    ; transitivity      = ⊑-trans _ _ _
    ; ⊑-propositional   = ⊑-propositional
    ; ⨆                 = ⨆
    ; upper-bound       = upper-bound
    ; least-upper-bound = least-upper-bound _ _
    }
  ; least  = never
  ; least⊑ = never⊑ _
  }

------------------------------------------------------------------------
-- Dependent eliminators

-- Predicate transformer related to increasing sequences.

Inc : ∀ {p q}
      (P : Carrier → Type p)
      (Q : ∀ {x y} → P x → P y → x ⊑ y → Type q) →
      Increasing-sequence → Type (p ⊔ q)
Inc P Q s =
  ∃ λ (p : ∀ n → P (s [ n ])) →
    ∀ n → Q (p n) (p (suc n)) (increasing s n)

-- Record wrapping up the eliminators' arguments.

record Rec-args
         {p q}
         (P : Carrier → Type p)
         (Q : ∀ {x y} → P x → P y → x ⊑ y → Type q) :
         Type (ℓ ⊔ p ⊔ q) where
  field
    pe : P never
    po : ∀ x → P (now x)
    pl : ∀ s (pq : Inc P Q s) → P (⨆ s)
    pa : ∀ {x y} (x⊑y : x ⊑ y) (x⊒y : x ⊒ y)
         (p-x : P x) (p-y : P y)
         (q-x⊑y : Q p-x p-y x⊑y) (q-x⊒y : Q p-y p-x x⊒y) →
         subst P (antisymmetry x⊑y x⊒y) p-x ≡ p-y
    pp : ∀ {x} {p₁ p₂ : P x} → Is-proposition (p₁ ≡ p₂)
    qr : ∀ x (p : P x) → Q p p (⊑-refl x)
    qt : ∀ {x y z}
         (x⊑y : x ⊑ y) (y⊑z : y ⊑ z)
         (p-x : P x) (p-y : P y) (p-z : P z) →
         Q p-x p-y x⊑y → Q p-y p-z y⊑z →
         Q p-x p-z (⊑-trans x y z x⊑y y⊑z)
    qe : ∀ x (p : P x) → Q pe p (never⊑ x)
    qu : ∀ s (pq : Inc P Q s) n →
         Q (proj₁ pq n) (pl s pq) (upper-bound s n)
    ql : ∀ s ub is-ub (pq : Inc P Q s) (pu : P ub)
         (qu : ∀ n → Q (proj₁ pq n) pu (is-ub n)) →
         Q (pl s pq) pu (least-upper-bound s ub is-ub)
    qm : ∀ {x y} (le : x CPO.⊑ y) →
         Q (po x) (po y) (now-mono le)
    q⨆ : ∀ s →
         Q (po (CPO.⨆ s))
           (pl (Σ-map (now ∘_) (now-mono ∘_) s)
               ( (λ n → po (s CPO.[ n ]))
               , (λ n → qm (CPO.increasing s n))
               ))
           (now-⨆′ s)
    qp : ∀ {x y} (p-x : P x) (p-y : P y) (x⊑y : x ⊑ y) →
         Is-proposition (Q p-x p-y x⊑y)

-- The eliminators.

module _ {p q}
         {P : Carrier → Type p}
         {Q : ∀ {x y} → P x → P y → x ⊑ y → Type q}
         (args : Rec-args P Q) where

  open Rec-args args

  mutual

    inc-rec : (s : Increasing-sequence) → Inc P Q s
    inc-rec (s , inc) = (λ n → ⊥-rec (s   n))
                      , (λ n → ⊑-rec (inc n))

    abstract

      ⊥-rec : (x : Carrier) → P x
      ⊥-rec never′ = pe

      ⊥-rec (now′ x) = po x

      ⊥-rec (⨆′ s) = pl s (inc-rec s)

      ⊥-rec (antisymmetry′ {x = x} {y = y} p q i) =
        subst≡→[]≡
          {B = P}
          {eq = antisymmetry′ p q}
          (pa p q (⊥-rec x) (⊥-rec y) (⊑-rec p) (⊑-rec q)) i

      ⊥-rec (≡-propositional′ {x = x} {y = y} p q i j) = lemma i j
        where
        ≡-propositional : P.Is-set Carrier
        ≡-propositional = ≡-propositional′

        lemma :
          P.[ (λ i → P.[ (λ j → P (≡-propositional p q i j)) ]
                       ⊥-rec x ≡ ⊥-rec y) ]
            (λ i → ⊥-rec (p i)) ≡ (λ i → ⊥-rec (q i))
        lemma = P.heterogeneous-UIP
                  (λ x → _↔_.to (H-level↔H-level 2) (pp {x = x}))
                  (≡-propositional′ p q)
                  _ _

      ⊑-rec : (x⊑y : x ⊑ y) → Q (⊥-rec x) (⊥-rec y) x⊑y
      ⊑-rec (⊑-refl′ x) = qr x (⊥-rec x)

      ⊑-rec (⊑-trans′ x y z p q) =
        qt p q (⊥-rec x) (⊥-rec y) (⊥-rec z) (⊑-rec p) (⊑-rec q)

      ⊑-rec (never⊑′ x) = qe x (⊥-rec x)

      ⊑-rec (upper-bound′ s n) = qu s (inc-rec s) n

      ⊑-rec (least-upper-bound′ s ub is-ub) =
        ql s ub is-ub (inc-rec s) (⊥-rec ub)
          (λ n → ⊑-rec {x = proj₁ s n} (is-ub n))

      ⊑-rec (now-mono′ x) = qm x

      ⊑-rec (now-⨆″ s) = q⨆ s

      ⊑-rec (⊑-propositional′ {x = x} {y = y} p q i) = lemma i
        where
        ⊑-propositional″ : ∀ {x y} → P.Is-proposition (x ⊑ y)
        ⊑-propositional″ = ⊑-propositional′

        lemma : P.[ (λ i → Q (⊥-rec x) (⊥-rec y)
                             (⊑-propositional″ p q i)) ]
                  ⊑-rec p ≡ ⊑-rec q
        lemma =
          P.heterogeneous-irrelevance
            (λ p → _↔_.to (H-level↔H-level 1)
                     (qp (⊥-rec x) (⊥-rec y) p))

      -- Some computation rules.

      ⊥-rec-never : ⊥-rec never ≡ pe
      ⊥-rec-never = refl

      ⊥-rec-now : ∀ x → ⊥-rec (now x) ≡ po x
      ⊥-rec-now _ = refl

      ⊥-rec-⨆ : ∀ s → ⊥-rec (⨆ s) ≡ pl s (inc-rec s)
      ⊥-rec-⨆ _ = refl

------------------------------------------------------------------------
-- Some lemmas

-- The inequality now-⨆′ can be strengthened to an equality.

now-⨆ : (s : CPO.Increasing-sequence) →
        now (CPO.⨆ s) ≡ ⨆ (Σ-map (now ∘_) (now-mono ∘_) s)
now-⨆ s =
  antisymmetry
    (now-⨆′ s)
    (least-upper-bound _ _ λ n → now-mono (CPO.upper-bound s n))

private

  -- A lemma.

  Carrier-is-set-and-equality-characterisation : Is-set Carrier × _
  Carrier-is-set-and-equality-characterisation =
    Eq.propositional-identity≃≡
      (λ x y → x ⊑ y × x ⊒ y)
      (λ _ _ → ×-closure 1 ⊑-propositional ⊑-propositional)
      (λ x → ⊑-refl x , ⊑-refl x)
      (λ x y → uncurry {B = λ _ → x ⊒ y} antisymmetry)

-- Carrier is a set. (This lemma is analogous to Theorem 11.3.9 in
-- "Homotopy Type Theory: Univalent Foundations of Mathematics" (first
-- edition).)

Carrier-is-set : Is-set Carrier
Carrier-is-set = proj₁ Carrier-is-set-and-equality-characterisation

-- Equality characterisation lemma for Carrier.

equality-characterisation-Carrier :
  ∀ {x y} → (x ⊑ y × x ⊒ y) ≃ (x ≡ y)
equality-characterisation-Carrier =
  proj₂ Carrier-is-set-and-equality-characterisation ext

-- Equality characterisation lemma for increasing sequences.

equality-characterisation-increasing :
  {s₁ s₂ : Increasing-sequence} →
  (∀ n → s₁ [ n ] ≡ s₂ [ n ]) ↔ s₁ ≡ s₂
equality-characterisation-increasing {s₁} {s₂} =
  (∀ n → s₁ [ n ] ≡ s₂ [ n ])  ↔⟨ Eq.extensionality-isomorphism ext ⟩
  proj₁ s₁ ≡ proj₁ s₂          ↝⟨ ignore-propositional-component
                                    (Π-closure ext 1 λ _ →
                                     ⊑-propositional) ⟩□
  s₁ ≡ s₂                      □

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
{-# OPTIONS --without-K #-}
module Explore.Subset where

open import Relation.Binary.PropositionalEquality

-- TODO

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
{-# OPTIONS --safe #-}
module Cubical.HITs.FreeAbGroup where

open import Cubical.HITs.FreeAbGroup.Base public

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
-- Inductive types
-- See Chapter 15 of "Practical Foundations for Programming Languages" by Robert Harper

module ITypes where

open import Data.Vec
open import Data.Nat
open import Data.List
open import Data.Fin.Base

-- auxiliary
data Bool : Set where
  True False : Bool

_if_else_ : {A : Set} → A → Bool → A → A
A if True  else B = A
A if False else B = B
-- end of auxiliary

{-- required later on
data IType' (n : ℕ) : Set
data IType' n where
   Unit Nat : IType' n
   Pair Sum : IType n → IType n → IType' n

Map'[_,_]_ : ∀ {n} → Fin n → IType' n → IType n → IType' n
Map'[ var , Unit ] type'           = Unit
Map'[ var , Nat ] type'            = Nat
Map'[ var , Pair x x₁ ] type'      = Pair (Map[ var , x ] type') (Map[ var , x₁ ] type')
Map'[ var , Sum x x₁ ] type'       = Sum (Map[ var , x ] type') (Map[ var , x₁ ] type')
--}

data IType (n : ℕ) : Set

data IType n where
  Unit Nat : IType n
  Pair Sum : IType n → IType n → IType n
  Ind : IType (suc n)  → IType n
  Var : Fin n → IType n
  Func : IType n → IType n → IType n

FinEq : ∀ {n} → Fin n → Fin n → Bool
FinEq zero zero         = True
FinEq zero (suc b)      = False
FinEq (suc a) zero      = False
FinEq (suc a) (suc b) = FinEq a b

-- Substitute type' for var in type
Map[_,_]_ : ∀ {n} → Fin (suc n) → IType (suc n) → IType n → IType n
Map[ var , Unit ] type'            = Unit
Map[ var , Nat ] type'             = Nat
Map[ var , Pair type type₁ ] type' = Pair (Map[ var , type ] type') (Map[ var , type₁ ] type')
Map[ var , Sum type type₁ ] type'  = Pair (Map[ var , type ] type') (Map[ var , type₁ ] type')
Map[ var , Ind x ] type'           = {!!} --Ind (Map[ var , x ] type')
Map[ var , Func a b ] type'        = Func (Map[ var , a ] type') (Map[ var , b ] type')
Map[ var , Var x ] type'           = type' if (FinEq var x) else Var {!!}

-- Alternative notation
[_/_]_ : ∀ {n} → IType n → Fin (suc n) → IType (suc n) → IType n
[ type' / var ] type = Map[ var , type ] type'

Env : ℕ → Set
Env n = List (IType n)

-- Environment lookup
data _∈`_ {n} : IType n → Env n → Set where
  here  : ∀ {φ A}    → A ∈` (A ∷ φ)
  there : ∀ {φ A A'} → A ∈` φ → A ∈` (A' ∷ φ)

-- Expressions
data Expr {n} : Env n → IType n → Set where
--  Fold       : ∀ {ϕ t τ} → Expr ϕ ([ Ind τ / t ] τ) → Expr ϕ (Ind τ)
--  Rec        : ∀ {ϕ t τ ρ} → Expr ((Map[ t , τ ] ρ) ∷ ϕ) ρ → Expr ϕ (Ind τ) → {!!}
  FoldNat    : ∀ {ϕ}     → Expr ϕ (Sum Unit Nat) → Expr ϕ Nat
  RecNat     : ∀ {ϕ}   → Expr (Sum Unit Nat ∷ ϕ) Nat → Expr ϕ Nat → Expr ϕ Nat
  Var        : ∀ {φ τ}   → τ ∈` φ → Expr φ τ
  Abs        : ∀ {φ τ τ'} → Expr (τ ∷ φ) τ' → Expr φ (Func τ τ')
  App        : ∀ {φ τ τ'} → Expr φ (Func τ τ') → Expr φ τ → Expr φ τ'

-- Expression substitution
[_//_] : ∀ {n ϕ} {τ τ' : IType n} → Expr (τ' ∷ ϕ) τ → Expr ϕ τ' → Expr ϕ τ
-- TODO

data _↦_ {n ϕ} : {τ : IType n} → Expr ϕ τ → Expr ϕ τ → Set where

  ξ-RecNat : ∀ {e} {e' e''}
             → e' ↦ e''
             → _↦_ {τ = Nat} (RecNat e e') (RecNat e e'')

  β-RecNat : ∀ {e e'}
             → _↦_ {τ = Nat} (RecNat e (FoldNat e')) [ e // e' ]

-- IValue
-- data IValue (n : ℕ) : Set where

-- Interpreter
-- int : ∀ {n} → IType n → Set
-- int' : ∀ {n} → IType' n → Set
--- int {n} (Ind it') = IValue n (int' it')

max_stars_repo_name: kcaliban/ldlc

max_issues_repo_name: kcaliban/ldlc

max_forks_repo_name: kcaliban/ldlc


text:
module Numeric.Nat.BinarySearch where

open import Prelude
open import Numeric.Nat.Properties
open import Tactic.Nat
open import Control.WellFounded
open import Numeric.Nat.DivMod

data SearchResult! {a} (P : Nat → Set a) (lo hi : Nat) : Set a where
  here : ∀ k (!pk : ¬ P k) (psk : P (suc k)) (lo≤k : lo ≤ k) (k<hi : k < hi) → SearchResult! P lo hi

data SearchResult {a} (P : Nat → Set a) (lo hi : Nat) : Set a where
  here      : ∀ k (!pk : ¬ P k) (psk : P (suc k)) (lo≤k : lo ≤ k) (k<hi : k < hi) → SearchResult P lo hi
  below     : P lo → SearchResult P lo hi
  none      : ¬ P hi → SearchResult P lo hi
  bad-range : lo > hi → SearchResult P lo hi

private
  infixr 0 _⟨=<⟩_ _⟨<=⟩_
  _⟨=<⟩_ : ∀ {a : Nat} {b c} → a ≡ b → b < c → a < c
  refl ⟨=<⟩ b<c = b<c

  _⟨<=⟩_ : ∀ {a : Nat} {b c} → a < b → b ≡ c → a < c
  a<b ⟨<=⟩ refl = a<b

private
  lem-half : ∀ n → suc n div 2 < suc n
  lem-half n with suc n div 2 | suc n mod 2 | divmod-sound 2 (suc n)
  lem-half n | zero  | r | eq = auto
  lem-half n | suc q | r | eq = by eq

  lem-half-nonzero : ∀ n → NonZero ((2 + n) div 2)
  lem-half-nonzero n with (2 + n) div 2 | (2 + n) mod 2 | divmod-sound 2 (2 + n) | mod-less 2 (2 + n)
  lem-half-nonzero n | zero  | ._ | refl | lt = refute lt
  lem-half-nonzero n | suc q | r  | _    | _  = _

  lem-upper : ∀ {lo hi d} d′ {{_ : NonZero d′}} →
              hi ≡ suc (d + lo) → hi - (d′ + lo) ≤ d
  lem-upper zero {{}}
  lem-upper {d = d} (suc d′) refl = by (sub-leq d d′)

  search : ∀ {a} {P : Nat → Set a} lo hi d → hi ≡ d + lo → Acc _<_ d →
             (∀ n → Dec (P n)) →
             ¬ P lo → P hi → SearchResult! P lo hi
  search lo .lo 0 refl wf check !plo phi = ⊥-elim (!plo phi)
  search lo .(suc lo) 1 refl wf check !plo phi = here lo !plo phi (diff! 0) (diff! 0)
  search lo hi (suc (suc d₀)) eq (acc wf) check !plo phi =
    let d = suc d₀
        d′ = suc d div 2
        m = d′ + lo
        d′<d : d′ < suc d
        d′<d = lem-half d in
    case check m of λ
     { (yes pm) →
         case search lo m d′ refl (wf _ d′<d) check !plo pm of λ
         { (here k !pk psk lo≤k k<m) → here k !pk psk lo≤k $
             k<m ⟨<⟩ by d′<d ⟨<=⟩ sym eq
         }
     ; (no !pm) →
         let m≤hi : m ≤ hi
             m≤hi = by d′<d ⟨≤⟩ diff 1 (cong suc eq)
             instance d′≠0 : NonZero d′
                      d′≠0 = lem-half-nonzero d₀
             eq′ : hi ≡ hi - m + m
             eq′ = eraseEquality (sym (sub-less m≤hi))
         in
         case search m hi (hi - m) eq′ (wf (hi - m) (lem-upper d′ eq)) check !pm phi of λ
         { (here k !pk psk m≤k k<hi) → here k !pk psk (auto ⟨≤⟩ m≤k) k<hi }
     }

private
  unbang : ∀ {a} {P : Nat → Set a} {lo hi} → SearchResult! P lo hi → SearchResult P lo hi
  unbang (here k x x₁ x₂ x₃) = here k x x₁ x₂ x₃

binarySearch : ∀ {a} {P : Nat → Set a} lo hi →
                 (∀ n → Dec (P n)) →
                 SearchResult P lo hi
binarySearch lo hi check with compare lo hi
... | greater lo>hi = bad-range lo>hi
binarySearch lo .lo check | equal refl =
  case check lo of λ
  { (yes p) → below p
  ; (no !p) → none !p
  }
binarySearch lo ._ check | less (diff! d) =
  let hi = suc d + lo in
  case check lo of λ
  { (yes p) → below p
  ; (no !p) →
    case check hi of λ
    { (yes p) → unbang $ search lo hi (suc d) refl (wfNat (suc d)) check !p p
    ; (no !p) → none !p }
  }

max_stars_repo_name: t-more/agda-prelude

max_issues_repo_name: t-more/agda-prelude

max_forks_repo_name: t-more/agda-prelude


text:
-- Andreas, 2011-10-04
-- I'd like to infer the type of a even though it is irrelevant
-- E.g. when pressing C-c C-.
module InferIrrelevant where

f : (A : Set)(g : .A → A).(a : A) → A
f A g a = {!a!}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda