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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Sets.EquivalenceRelations
open import Setoids.Setoids

module Setoids.DirectSum {m n o p : _} {A : Set m} {B : Set n} (R : Setoid {m} {o} A) (S : Setoid {n} {p} B) where

directSumSetoid : Setoid {m ⊔ n} (A || B)
Setoid._∼_ directSumSetoid (inl x) (inl y) = embedLevel {o} {p} (Setoid._∼_ R x y)
Setoid._∼_ directSumSetoid (inl x) (inr y) = False'
Setoid._∼_ directSumSetoid (inr x) (inl y) = False'
Setoid._∼_ directSumSetoid (inr x) (inr y) = embedLevel {p} {o} (Setoid._∼_ S x y)
Equivalence.reflexive (Setoid.eq directSumSetoid) {inl x} = Equivalence.reflexive (Setoid.eq R) {x} ,, record {}
Equivalence.reflexive (Setoid.eq directSumSetoid) {inr x} = Equivalence.reflexive (Setoid.eq S) {x} ,, record {}
Equivalence.symmetric (Setoid.eq directSumSetoid) {inl x} {inl y} (x=y ,, _) = (Equivalence.symmetric (Setoid.eq R) x=y) ,, record {}
Equivalence.symmetric (Setoid.eq directSumSetoid) {inr x} {inr y} (x=y ,, _) = (Equivalence.symmetric (Setoid.eq S) x=y) ,, record {}
Equivalence.transitive (Setoid.eq directSumSetoid) {inl x} {inl y} {inl z} (x=y ,, _) (y=z ,, _) = Equivalence.transitive (Setoid.eq R) x=y y=z ,, record {}
Equivalence.transitive (Setoid.eq directSumSetoid) {inr x} {inr y} {inr z} (x=y ,, _) (y=z ,, _) = Equivalence.transitive (Setoid.eq S) x=y y=z ,, record {}


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

postulate
  ⊤ ⊥ : Set
  _&_ : Set → Set → Set
  _≤_ : Nat → Nat → Set

{-# TERMINATING #-}
_∣_ : Nat → Nat → Set
m     ∣ zero  = ⊤
zero  ∣ suc n = ⊥
suc m ∣ suc n = (suc m ≤ suc n) & (suc m ∣ (n - m))

variable m n : Nat

postulate
  divide-to-nat : n ∣ m → Nat
  trivial : m ≡ n

divide-to-nat-correct : (e : m ∣ n) → divide-to-nat e * n ≡ m
divide-to-nat-correct e = trivial

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K #-}
module hott.equivalence.core where

open import equality.core using (_≡_ ; refl ; ap)
open import sum using (Σ ; proj₁ ; proj₂ ; _,_)
open import level using (_⊔_)
open import hott.level.core using (contr ; prop ; _⁻¹_)
open import function.core using (_$_)
open import function.isomorphism.core using (_≅_ ; iso)

-- a function is a weak equivalence, if the inverse images of all points are contractible
weak-equiv : ∀ {i k} {X : Set i} {Y : Set k} (f : X → Y) → Set (i ⊔ k)
weak-equiv {_} {_} {X} {Y} f = (y : Y) → contr $ f ⁻¹ y

-- weak equivalences
_≈_ : ∀ {i j} (X : Set i) (Y : Set j) → Set _
X ≈ Y = Σ (X → Y) λ f → weak-equiv f

apply≈ : ∀ {i j} {X : Set i}{Y : Set j} → X ≈ Y → X → Y
apply≈ = proj₁

≈⇒≅ : ∀ {i j} {X : Set i} {Y : Set j} → X ≈ Y → X ≅ Y
≈⇒≅ {X = X}{Y} (f , we) = iso f g iso₁ iso₂
  where
    g : Y → X
    g y = proj₁ (proj₁ (we y))

    iso₁ : (x : X) → g (f x) ≡ x
    iso₁ x = ap proj₁ (proj₂ (we (f x)) (x , refl))

    iso₂ : (y : Y) → f (g y) ≡ y
    iso₂ y = proj₂ (proj₁ (we y))

invert≈ : ∀ {i j} {X : Set i}{Y : Set j} → X ≈ Y → Y → X
invert≈ (_ , we) y = proj₁ (proj₁ (we y))

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

module Data.Binary.Increment.Strict where

open import Prelude
open import Strict
open import Data.Binary.Definition
open import Data.Bits.Strict
open import Data.Binary.Increment

inc′ : 𝔹 → 𝔹
inc′ 0ᵇ      = 1ᵇ 0ᵇ
inc′ (1ᵇ xs) = 2ᵇ xs
inc′ (2ᵇ xs) = 0∷! inc′ xs

inc′≡inc : ∀ xs → inc′ xs ≡ inc xs
inc′≡inc 0ᵇ = refl
inc′≡inc (1ᵇ xs) = refl
inc′≡inc (2ᵇ xs) = 0∷!≡0∷ (inc′ xs) ; cong 1ᵇ_ (inc′≡inc xs)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

open import Cubical.Core.Everything
open import Cubical.Algebra.Group

module Cubical.Algebra.Group.Coset {ℓ} (G : Group ℓ) where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function using (id; _∘_; flip)
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels
open import Cubical.Functions.Embedding

open import Cubical.Algebra.Group.Subgroup

open import Cubical.Relation.Unary
open import Cubical.Relation.Unary.Properties
open import Cubical.Relation.Binary using (Reflexive; Symmetric; Transitive)
open import Cubical.HITs.PropositionalTruncation
open import Cubical.Relation.Binary.Reasoning.Equality

open Group G
open GroupLemmas G

private
  variable
    ℓ′ : Level

_≅[_]ˡ_ : ⟨ G ⟩ → Subgroup G ℓ′ → ⟨ G ⟩ → hProp _
x ≅[ H ]ˡ y = Subgroup.Member H (x ⁻¹ • y)

module _ (H : Subgroup G ℓ′) where
  private module H = Subgroup H

  ≅ˡ-reflexive : Reflexive _≅[ H ]ˡ_
  ≅ˡ-reflexive = subst⁻ (_∈ H.Member) (inverseˡ _) H.preservesId

  ≅ˡ-symmetric : Symmetric _≅[ H ]ˡ_
  ≅ˡ-symmetric {x} {y} = subst (_∈ H.Member) (invDistr (x ⁻¹) y ∙ cong (y ⁻¹ •_) (invInvo x)) ∘ H.preservesInv

  ≅ˡ-transitive : Transitive _≅[ H ]ˡ_
  ≅ˡ-transitive {i} {j} {k} x y = subst (_∈ H.Member) eq (H.preservesOp x y)
    where
      eq : _
      eq =
        (i ⁻¹ • j) • (j ⁻¹ • k) ≡˘⟨ assoc _ _ _ ⟩
        ((i ⁻¹ • j) • j ⁻¹) • k ≡⟨ cong (_• k) (assoc _ _ _) ⟩
        (i ⁻¹ • (j • j ⁻¹)) • k ≡⟨ cong (λ v → (i ⁻¹ • v) • k) (inverseʳ j) ⟩
        (i ⁻¹ • ε) • k          ≡⟨ cong (_• k) (identityʳ (i ⁻¹)) ⟩
        i ⁻¹ • k                ∎

infix 9 _<•_
infixr 9 _<•′_

_<•′_ : ⟨ G ⟩ → Pred ⟨ G ⟩ ℓ′ → Pred ⟨ G ⟩ _
g <•′ H = (g •_) ⊣ H

_<•_ : ⟨ G ⟩ → Subgroup G ℓ′ → Pred ⟨ G ⟩ _
g <• H = g <•′ Subgroup.Member H

module _ (H : Pred ⟨ G ⟩ ℓ′) where

  cosetˡ-identity→ : ε <•′ H ⊆ H
  cosetˡ-identity→ = rec (isProp[ H ] _)
      λ ((h , subh) , εh≡x) → subst (_∈ H) (sym (identityˡ h) ∙ εh≡x) subh

  cosetˡ-identity← : H ⊆ ε <•′ H
  cosetˡ-identity← x∈H = ∣ (_ , x∈H) , identityˡ _ ∣

  cosetˡ-identity : ε <•′ H ⇔ H
  cosetˡ-identity = cosetˡ-identity→ , cosetˡ-identity←

  cosetˡ-assoc→ : ∀ a b → (a • b) <•′ H ⊆ a <•′ b <•′ H
  cosetˡ-assoc→ a b =
    map λ ((h , subh) , abh≡x) → (b • h ,
            ∣ (h , subh) , refl ∣) ,
          sym (assoc _ _ _) ∙ abh≡x

  cosetˡ-assoc← : ∀ a b → a <•′ b <•′ H ⊆ (a • b) <•′ H
  cosetˡ-assoc← a b {x} =
    rec squash λ ((h , subh) , ah≡x) →
      map (λ ((g , subg) , bg≡h) → (g , subg) , (
            a • b • g   ≡⟨ assoc a b g ⟩
            a • (b • g) ≡⟨ cong (a •_) bg≡h ⟩
            a • h       ≡⟨ ah≡x ⟩
            x           ∎
          )) subh

  cosetˡ-assoc : ∀ a b → (a • b) <•′ H ≡ a <•′ b <•′ H
  cosetˡ-assoc a b = ⇔toPath _ _ (cosetˡ-assoc→ a b , cosetˡ-assoc← a b)

module _ (H : Subgroup G ℓ′) where
  private module H = Subgroup H

  g∈gH : ∀ g → g ∈ g <• H
  g∈gH g = ∣ H.ε , identityʳ _ ∣

  ≅-cosetˡ→ : ∀ x y → ⟨ x ≅[ H ]ˡ y ⟩ → x <• H ⇔ y <• H
  ≅-cosetˡ→ x y x≅y = xH⊆yH , xH⊇yH
    where
      xH⊆yH : x <• H ⊆ y <• H
      xH⊆yH {a} = map λ ((h , subh) , xh≡a) → (y ⁻¹ • x • h , H.preservesOp (≅ˡ-symmetric H x≅y) subh) ,
                                                (
                                                  y • (y ⁻¹ • x • h) ≡˘⟨ assoc y (y ⁻¹ • x) h ⟩
                                                  y • (y ⁻¹ • x) • h ≡˘⟨ cong (_• h) (assoc y (y ⁻¹) x) ⟩
                                                  y • y ⁻¹ • x • h   ≡⟨ cong (λ v → v • x • h) (inverseʳ y) ⟩
                                                  ε • x • h          ≡⟨ cong (_• h) (identityˡ x) ⟩
                                                  x • h              ≡⟨ xh≡a ⟩
                                                  a                  ∎)

      xH⊇yH : x <• H ⊇ y <• H
      xH⊇yH {a} = map λ ((h , subh) , yh≡a) → (x ⁻¹ • y • h , H.preservesOp x≅y subh) ,
                                                (
                                                  x • (x ⁻¹ • y • h) ≡˘⟨ assoc x (x ⁻¹ • y) h ⟩
                                                  x • (x ⁻¹ • y) • h ≡˘⟨ cong (_• h) (assoc x (x ⁻¹) y) ⟩
                                                  x • x ⁻¹ • y • h   ≡⟨ cong (λ v → v • y • h) (inverseʳ x) ⟩
                                                  ε • y • h          ≡⟨ cong (_• h) (identityˡ y) ⟩
                                                  y • h              ≡⟨ yh≡a ⟩
                                                  a                  ∎)

  ≅-cosetˡ← : ∀ x y → x <• H ⇔ y <• H → ⟨ x ≅[ H ]ˡ y ⟩
  ≅-cosetˡ← x y (xH⊆yH , yH⊆xH) = rec ((_ ≅[ H ]ˡ _) .snd)
      (λ ((h , subh) , yh≡x) →
        subst (_∈ H.Member) (cong _⁻¹ (
            h              ≡˘⟨ identityˡ h ⟩
            ε • h          ≡˘⟨ cong (_• h) (inverseˡ y) ⟩
            y ⁻¹ • y • h   ≡⟨ assoc _ _ _ ⟩
            y ⁻¹ • (y • h) ≡⟨ cong (y ⁻¹ •_) yh≡x ⟩
            y ⁻¹ • x       ∎
        ) ∙ invDistr (y ⁻¹) x ∙ cong (x ⁻¹ •_) (invInvo y)) (H.preservesInv subh)
      )
      (xH⊆yH {x} (g∈gH x))

  ≅-cosetˡ : ∀ x y → ⟨ x ≅[ H ]ˡ y ⟩ ≃ (x <• H ⇔ y <• H)
  ≅-cosetˡ x y = isPropEquiv→Equiv ((x ≅[ H ]ˡ y) .snd) (isProp⇔ (x <• H) (y <• H))
                                    (≅-cosetˡ→ x y) (≅-cosetˡ← x y)

  cosetˡ-idem→ : ((h , _) : ⟨ H ⟩) → h <• H ⊆ H.Member
  cosetˡ-idem→ (h , subh) = rec (isProp[ H.Member ] _)
    λ ((g , subg) , hg≡x) → subst (_∈ H.Member) hg≡x (H.preservesOp subh subg)

  cosetˡ-idem← : ((h , _) : ⟨ H ⟩) → H.Member ⊆ h <• H
  cosetˡ-idem← (h , subh) {x} subx =
    ∣
      (h ⁻¹ • x , H.preservesOp (H.preservesInv subh) subx) , (
        h • (h ⁻¹ • x) ≡˘⟨ assoc h (h ⁻¹) x ⟩
        (h • h ⁻¹) • x ≡⟨ cong (_• x) (inverseʳ h) ⟩
        ε • x          ≡⟨ identityˡ x ⟩
        x              ∎)
    ∣

  cosetˡ-idem : ((h , _) : ⟨ H ⟩) → h <• H ⇔ H.Member
  cosetˡ-idem h = cosetˡ-idem→ h , cosetˡ-idem← h

_≅[_]ʳ_ : ⟨ G ⟩ → Subgroup G ℓ′ → ⟨ G ⟩ → hProp _
x ≅[ H ]ʳ y = Subgroup.Member H (x • y ⁻¹)

module _ (H : Subgroup G ℓ′) where
  private module H = Subgroup H

  ≅ʳ-reflexive : Reflexive _≅[ H ]ʳ_
  ≅ʳ-reflexive = subst⁻ (_∈ H.Member) (inverseʳ _) H.preservesId

  ≅ʳ-symmetric : Symmetric _≅[ H ]ʳ_
  ≅ʳ-symmetric {x} {y} = subst (_∈ H.Member) (invDistr x (y ⁻¹) ∙ cong (_• x ⁻¹) (invInvo y)) ∘ H.preservesInv

  ≅ʳ-transitive : Transitive _≅[ H ]ʳ_
  ≅ʳ-transitive {i} {j} {k} x y = subst (_∈ H.Member) eq (H.preservesOp x y)
    where
      eq : _
      eq =
        (i • j ⁻¹) • (j • k ⁻¹) ≡˘⟨ assoc _ _ _ ⟩
        ((i • j ⁻¹) • j) • k ⁻¹ ≡⟨ cong (_• k ⁻¹) (assoc _ _ _) ⟩
        (i • (j ⁻¹ • j)) • k ⁻¹ ≡⟨ cong (λ v → (i • v) • k ⁻¹) (inverseˡ j) ⟩
        (i • ε) • k ⁻¹          ≡⟨ cong (_• k ⁻¹) (identityʳ i) ⟩
        i • k ⁻¹                ∎

infix 9 _•>_
infixl 9 _•>′_

_•>′_ : Pred ⟨ G ⟩ ℓ′ → ⟨ G ⟩ → Pred ⟨ G ⟩ _
H •>′ g = (_• g) ⊣ H

_•>_ : Subgroup G ℓ′ → ⟨ G ⟩ → Pred ⟨ G ⟩ _
H •> g = Subgroup.Member H •>′ g

module _ (H : Pred ⟨ G ⟩ ℓ′) where

  cosetʳ-identity→ : H •>′ ε ⊆ H
  cosetʳ-identity→ = rec (isProp[ H ] _)
      λ ((h , subh) , hε≡x) → subst (_∈ H) (sym (identityʳ h) ∙ hε≡x) subh

  cosetʳ-identity← : H ⊆ H •>′ ε
  cosetʳ-identity← x∈H = ∣ (_ , x∈H) , identityʳ _ ∣

  cosetʳ-identity : H •>′ ε ⇔ H
  cosetʳ-identity = cosetʳ-identity→ , cosetʳ-identity←

  cosetʳ-assoc→ : ∀ a b → H •>′ (a • b) ⊆ H •>′ a •>′ b
  cosetʳ-assoc→ a b =
    map λ ((h , subh) , hab≡x) → (h • a ,
            ∣ (h , subh) , refl ∣) ,
          assoc _ _ _ ∙ hab≡x

  cosetʳ-assoc← : ∀ a b → H •>′ a •>′ b ⊆ H •>′ (a • b)
  cosetʳ-assoc← a b {x} =
    rec squash λ ((h , subh) , hb≡x) →
      map (λ ((g , subg) , ga≡h) → (g , subg) , (
            g • (a • b) ≡˘⟨ assoc g a b ⟩
            (g • a) • b ≡⟨ cong (_• b) ga≡h ⟩
            h • b       ≡⟨ hb≡x ⟩
            x           ∎
          )) subh

  cosetʳ-assoc : ∀ a b → H •>′ (a • b) ≡ H •>′ a •>′ b
  cosetʳ-assoc a b = ⇔toPath _ _ (cosetʳ-assoc→ a b , cosetʳ-assoc← a b)

module _ (H : Subgroup G ℓ′) where
  private module H = Subgroup H

  g∈Hg : ∀ g → g ∈ H •> g
  g∈Hg g = ∣ H.ε , identityˡ _ ∣

  ≅-cosetʳ→ : ∀ x y → ⟨ x ≅[ H ]ʳ y ⟩ → H •> x ⇔ H •> y
  ≅-cosetʳ→ x y x≅y = Hx⊆Hy , Hx⊇Hy
    where
      Hx⊆Hy : H •> x ⊆ H •> y
      Hx⊆Hy {a} = map
        λ ((h , subh) , hx≡a) → (h • (x • y ⁻¹) , H.preservesOp subh x≅y) , (
                                  h • (x • y ⁻¹) • y   ≡˘⟨ cong (_• y) (assoc h x (y ⁻¹)) ⟩
                                  h • x • y ⁻¹ • y     ≡⟨ assoc (h • x) (y ⁻¹) y ⟩
                                  (h • x) • (y ⁻¹ • y) ≡⟨ cong (h • x •_) (inverseˡ y) ⟩
                                  h • x • ε            ≡⟨ identityʳ (h • x) ⟩
                                  h • x                ≡⟨ hx≡a ⟩
                                  a                    ∎)

      Hx⊇Hy : H •> x ⊇ H •> y
      Hx⊇Hy {a} = map
        λ ((h , subh) , hy≡a) → (h • (y • x ⁻¹) , H.preservesOp subh (≅ʳ-symmetric H x≅y)) , (
                                  h • (y • x ⁻¹) • x   ≡˘⟨ cong (_• x) (assoc h y (x ⁻¹)) ⟩
                                  h • y • x ⁻¹ • x     ≡⟨ assoc (h • y) (x ⁻¹) x ⟩
                                  (h • y) • (x ⁻¹ • x) ≡⟨ cong (h • y •_) (inverseˡ x) ⟩
                                  h • y • ε            ≡⟨ identityʳ (h • y) ⟩
                                  h • y                ≡⟨ hy≡a ⟩
                                  a                    ∎)

  ≅-cosetʳ← : ∀ x y → H •> x ⇔ H •> y → ⟨ x ≅[ H ]ʳ y ⟩
  ≅-cosetʳ← x y (Hx⊆Hy , Hy⊆Hx) = rec ((_ ≅[ H ]ʳ _) .snd)
      (λ ((h , subh) , hy≡x) →
        subst (_∈ H.Member) (
          h              ≡˘⟨ identityʳ h ⟩
          h • ε          ≡˘⟨ cong (h •_) (inverseʳ y) ⟩
          h • (y • y ⁻¹) ≡˘⟨ assoc h y (y ⁻¹) ⟩
          (h • y) • y ⁻¹ ≡⟨ cong (_• y ⁻¹) hy≡x ⟩
          x • y ⁻¹       ∎
        ) subh
      )
      (Hx⊆Hy {x} (g∈Hg x))

  ≅-cosetʳ : ∀ x y → ⟨ x ≅[ H ]ʳ y ⟩ ≃ (H •> x ⇔ H •> y)
  ≅-cosetʳ x y = isPropEquiv→Equiv ((x ≅[ H ]ʳ y) .snd) (isProp⇔ (H •> x) (H •> y))
                                    (≅-cosetʳ→ x y) (≅-cosetʳ← x y)

  cosetʳ-idem→ : ((h , _) : ⟨ H ⟩) → H •> h ⊆ H.Member
  cosetʳ-idem→ (h , subh) = rec (isProp[ H.Member ] _)
    λ ((g , subg) , gh≡x) → subst (_∈ H.Member) gh≡x (H.preservesOp subg subh)

  cosetʳ-idem← : ((h , _) : ⟨ H ⟩) → H.Member ⊆ H •> h
  cosetʳ-idem← (h , subh) {x} subx =
    ∣
      (x • h ⁻¹ , H.preservesOp subx (H.preservesInv subh)) , (
        (x • h ⁻¹) • h ≡⟨ assoc x (h ⁻¹) h ⟩
        x • (h ⁻¹ • h) ≡⟨ cong (x •_) (inverseˡ h) ⟩
        x • ε          ≡⟨ identityʳ x ⟩
        x              ∎)
    ∣

  cosetʳ-idem : ((h , _) : ⟨ H ⟩) → H •> h ⇔ H.Member
  cosetʳ-idem h = cosetʳ-idem→ h , cosetʳ-idem← h


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

pattern vArg x = arg (arg-info visible (modality relevant quantity-ω)) x

make2 : Term → TC ⊤
make2 hole = bindTC (normalise (def (quote _+_) (vArg (lit (nat 1)) ∷ vArg (lit (nat 1)) ∷ []))) (unify hole)

macro
  tester : Term → TC ⊤
  tester hole = onlyReduceDefs (quote _+_ ∷ []) (make2 hole)

_ = tester

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
-- a simple error monad
module error where

open import level
open import string

infixr 1 _≫=err_ _≫err_

data error-t{ℓ}(A : Set ℓ) : Set ℓ where
  no-error : A → error-t A
  yes-error : string → error-t A

_≫=err_ : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → error-t A → (A → error-t B) → error-t B
(no-error a) ≫=err f = f a
(yes-error e) ≫=err _ = yes-error e

_≫err_ : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → error-t A → error-t B → error-t B
a ≫err b = a ≫=err λ _ → b

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
-------------------------------------------
-- This file contains basic definitions. --
-------------------------------------------
module Basics where

  open import Level

  data ⊥-poly {l : Level} : Set l where

  ⊥-poly-elim : ∀ {l w} {Whatever : Set w} → ⊥-poly {l} → Whatever
  ⊥-poly-elim ()


text:
module leftpad where

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Data.Nat.Properties
open import Data.Vec
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality

data LeOrGt : ℕ → ℕ → Set where
  le : ∀ m k → LeOrGt m (k + m)
  gt : ∀ m k → LeOrGt (suc k + m) m

compare : ∀ m n → LeOrGt m n
compare zero n = cast $ le 0 n
  where cast = subst (LeOrGt 0) (+-identityʳ n)
compare (suc m) zero = cast $ gt 0 m
  where cast = subst (flip LeOrGt 0) (+-identityʳ (suc m))
compare (suc m) (suc n) with compare m n
... | le .m k = cast $ le (suc m) k
  where cast = subst (LeOrGt (suc m)) (+-suc k m)
... | gt .n k = cast $ gt (suc n) k
  where cast = subst (flip LeOrGt (suc n) ∘′ suc) (+-suc k n)

_⊔_ : ℕ → ℕ → ℕ
m ⊔ n with compare m n
... | le _ _ = n
... | gt _ _ = m

module _ {a} {A : Set a} (x : A) where

  data LeftPad {n : ℕ} (xs : Vec A n) : ∀ m → Vec A m → Set where
    Padded : ∀ k → LeftPad xs (k + n) (replicate {n = k} x ++ xs)

  leftPad : ∀ n m (xs : Vec A n) → ∃ (LeftPad xs (n ⊔ m))
  leftPad n m xs with compare n m
  ... | le .n k = , Padded k
  ... | gt .m k = , Padded 0

max_stars_repo_name: RomainGehrig/lets-prove-leftpad

max_issues_repo_name: RomainGehrig/lets-prove-leftpad

max_forks_repo_name: RomainGehrig/lets-prove-leftpad


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

module Term.Core where

open import Context
open import Type

open import Function
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Data.Empty
open import Data.Unit.Base
open import Data.Sum.Base

{-# BUILTIN REWRITE _≡_ #-}

{-# REWRITE foldlᶜ-▻-ε #-}
{-# REWRITE mapᶜ-▻▻    #-}

{-# REWRITE keep-id      #-}
{-# REWRITE dupl-keep-vs #-}

{-# REWRITE renᵗ-id #-}
{-# REWRITE renᵗ-∘  #-}

{-# REWRITE subᵗ-idᵉ  #-}
{-# REWRITE subᵗ-renᵗ #-}
{-# REWRITE subᵗ-Var  #-}

{-# REWRITE inject-foldr-⇒-renᵗ #-}
{-# REWRITE inject-foldr-⇒-subᵗ #-}

infix  3 _⊢_
infix  4 Λ_ ƛ_
infixl 7 _·_
infix  9 _[_]

unfold : ∀ {Θ κ} -> Θ ⊢ᵗ (κ ⇒ᵏ ⋆) ⇒ᵏ κ ⇒ᵏ ⋆ -> Θ ⊢ᵗ κ -> Θ ⊢ᵗ ⋆
unfold ψ α = normalize $ ψ ∙ Lam (μ (shiftᵗ ψ) (Var vz)) ∙ α

data _⊢_ : ∀ {Θ} -> Con (Star Θ) -> Star Θ -> Set where
  var  : ∀ {Θ Γ} {α : Star Θ}   -> α ∈ Γ -> Γ ⊢ α
  Λ_   : ∀ {Θ Γ σ} {α : Star (Θ ▻ σ)} -> shiftᶜ Γ ⊢ α -> Γ ⊢ π σ α
  -- A normalizing at the type level type instantiation.
  _[_] : ∀ {Θ Γ σ} {β : Star (Θ ▻ σ)} -> Γ ⊢ π σ β -> (α : Θ ⊢ᵗ σ) -> Γ ⊢ β [ α ]ᵗ
  -- A non-normalizing at the type level type instantiation.
  _<_> : ∀ {Θ Γ σ} {β : Star (Θ ▻ σ)} -> Γ ⊢ π σ β -> (α : Θ ⊢ᵗ σ) -> Γ ⊢ β < α >ᵗ
  -- A shorthand for `_< Var vz >` with more convenient computation at the type level.
  _<>  : ∀ {Θ σ Γ} {β : Star (Θ ▻ σ ▻ σ)} -> Γ ⊢ π σ β -> Γ ⊢ unshiftᵗ β
  ƛ_   : ∀ {Θ Γ} {α β : Star Θ} -> Γ ▻ α ⊢ β -> Γ ⊢ α ⇒ β
  _·_  : ∀ {Θ Γ} {α β : Star Θ} -> Γ ⊢ α ⇒ β -> Γ ⊢ α -> Γ ⊢ β
  iwrap  : ∀ {Θ Γ κ ψ} {α : Θ ⊢ᵗ κ} -> Γ ⊢ unfold ψ α -> Γ ⊢ μ ψ α
  unwrap : ∀ {Θ Γ κ ψ} {α : Θ ⊢ᵗ κ} -> Γ ⊢ μ ψ α -> Γ ⊢ unfold ψ α

Term⁺ : Star⁺ -> Set
Term⁺ α = ∀ {Θ} {Γ : Con (Star Θ)} -> Γ ⊢ normalize α

Term⁻ : ∀ {Θ} -> Star Θ -> Set
Term⁻ α = ∀ {Γ} -> Γ ⊢ normalize α

bind : ∀ {Θ Γ} {α β : Star Θ} -> Γ ⊢ α -> Γ ▻ α ⊢ β -> Γ ⊢ β
bind term body = (ƛ body) · term

ren : ∀ {Θ Γ Δ} {α : Star Θ} -> Γ ⊆ Δ -> Γ ⊢ α -> Δ ⊢ α
ren ι (var v)       = var (renᵛ ι v)
ren ι (Λ body)      = Λ (ren (mapᶜ-⊆ ι) body)
ren ι (fun [ α ])   = ren ι fun [ α ]
ren ι (fun < α >)   = ren ι fun < α >
ren ι (fun <>)      = ren ι fun <>
ren ι (ƛ body)      = ƛ (ren (keep ι) body)
ren ι (fun · arg)   = ren ι fun · ren ι arg
ren ι (iwrap  term) = iwrap (ren ι term)
ren ι (unwrap term) = unwrap (ren ι term)

shiftⁿ : ∀ {Θ Γ} {α : Star Θ} Δ -> Γ ⊢ α -> Γ ▻▻ Δ ⊢ α
shiftⁿ = ren ∘ extʳ

shift : ∀ {Θ Γ} {α β : Star Θ} -> Γ ⊢ α -> Γ ▻ β ⊢ α
shift = shiftⁿ (ε ▻ _)

instNonRec : ∀ {Θ Γ Δ} {α : Star Θ} -> Seq (Γ ⊢_) Δ -> Γ ▻▻ Δ ⊢ α -> Γ ⊢ α
instNonRec              ø           body = body
instNonRec {Δ = Δ ▻ _} (seq ▶ term) body = instNonRec seq (bind (shiftⁿ Δ term) body)

module Y where
  self : Type⁺ (⋆ ⇒ᵏ ⋆)
  self = Lam μ (Lam Lam (Var (vs vz) ∙ Var vz ⇒ Var vz)) (Var vz)

  unfoldˢ : Term⁺ (π ⋆ $ self ∙ Var vz ⇒ self ∙ Var vz ⇒ Var vz)
  unfoldˢ = Λ ƛ unwrap (var vz)

  unrollˢ : Term⁺ (π ⋆ $ self ∙ Var vz ⇒ Var vz)
  unrollˢ = Λ ƛ unfoldˢ [ Var vz ] · var vz · var vz

  fix : Term⁺ (π ⋆ $ (Var vz ⇒ Var vz) ⇒ Var vz)
  fix = Λ ƛ unrollˢ [ Var vz ] · iwrap (ƛ var (vs vz) · (unrollˢ [ Var vz ] · var vz))
open Y using (fix)

tuple : ∀ {Θ} -> Star (Θ ▻ ⋆) -> Star Θ
tuple Fv = π ⋆ $ Fv ⇒ Var vz

endo : ∀ {Θ} -> Star (Θ ▻ ⋆) -> Star Θ
endo Fv = π ⋆ $ Fv ⇒ Fv

fixBy
  : ∀ {Θ} {Γ : Con (Star Θ)}
  -> (Fv : Star (Θ ▻ ⋆))
  -> Γ ⊢ (tuple Fv ⇒ tuple Fv) ⇒ endo Fv ⇒ tuple Fv
fixBy Fv =
  ƛ fix < endo Fv ⇒ tuple Fv > ·
    (ƛ ƛ Λ ƛ (var (vs vs vs vz) ·
      (Λ ƛ (var (vs vs vs vz) · var (vs vs vz)) <> ·
        -- `bind` is in order to make REWRITE rules fire (yeah, it's silly).
        (bind (var (vs vs vz) <>) (var vz) · var vz))) <> · var vz)

ƛⁿ
  : ∀ {Θ Ξ Γ} {f : Star Ξ -> Star Θ} {β}
  -> ∀ Δ -> Γ ▻▻ mapᶜ f Δ ⊢ β -> Γ ⊢ conToTypeBy f Δ β
ƛⁿ  ε      term = term
ƛⁿ (Δ ▻ τ) body = ƛⁿ Δ (ƛ body)

ƛⁿ'
  : ∀ {Θ Γ} {β : Star Θ}
  -> ∀ Δ -> Γ ▻▻ Δ ⊢ β -> Γ ⊢ conToTypeBy id Δ β
ƛⁿ'  ε      term = term
ƛⁿ' (Δ ▻ τ) body = ƛⁿ' Δ (ƛ body)

applyⁿ
  : ∀ {Θ Ξ Γ} {β : Star Θ} {f : Star Ξ -> Star Θ}
  -> ∀ Δ -> Γ ⊢ conToTypeBy f Δ β -> Seq (λ τ -> Γ ⊢ f τ) Δ -> Γ ⊢ β
applyⁿ _ y  ø        = y
applyⁿ _ f (seq ▶ x) = applyⁿ _ f seq · x

deeply
  : ∀ {Θ Ξ Γ} {f : Star Ξ -> Star Θ} {β γ}
  -> ∀ Δ
  -> Γ ▻▻ mapᶜ f Δ ⊢ β ⇒ γ
  -> Γ ⊢ conToTypeBy f Δ β
  -> Γ ⊢ conToTypeBy f Δ γ
deeply  ε      g y = g · y
deeply (Δ ▻ τ) g f = deeply Δ (ƛ ƛ shiftⁿ (ε ▻ _ ▻ _) (ƛ g) · var vz · (var (vs vz) · var vz)) f

conToTypeShift : ∀ {Θ} -> Con (Star Θ) -> Star (Θ ▻ ⋆)
conToTypeShift Δ = conToTypeBy shiftᵗ Δ (Var vz)

-- This is not easy, but makes perfect sense and should be doable.
postulate
  shift-⊢ : ∀ {Θ Γ β} {α : Star Θ} -> Γ ⊢ α -> shiftᶜ {τ = β} Γ ⊢ shiftᵗ α

recursive
  : ∀ {Θ} {Γ : Con (Star (Θ ▻ ⋆))}
  -> (Δ : Con (Star Θ))
  -> Γ ⊢ π ⋆ (conToTypeBy (shiftᵗⁿ (ε ▻ _ ▻ _)) Δ (Var vz) ⇒ Var vz)
  -> Seq (λ β -> Γ ⊢ shiftᵗ β) Δ
recursive  ε      h = ø
recursive (Δ ▻ τ) h
  = recursive Δ (Λ ƛ shift (shift-⊢ h <>) · deeply Δ (ƛ ƛ var (vs vz)) (var vz))
  ▶ h < shiftᵗ τ > · (ƛⁿ Δ (ƛ var vz)) where

byCon : ∀ {Θ} (Δ : Con (Star Θ)) -> let F = conToTypeShift Δ in ∀ {Γ} -> Γ ⊢ tuple F ⇒ tuple F
byCon Δ = ƛ Λ ƛ applyⁿ Δ (var vz) (recursive Δ (var (vs vz)))

fixCon : ∀ {Θ} (Δ : Con (Star Θ)) -> let F = conToTypeShift Δ in ∀ {Γ} -> Γ ⊢ endo F ⇒ tuple F
fixCon Δ = fixBy (conToTypeShift Δ) · byCon Δ

record Tuple {Θ} (Γ Δ : Con (Star Θ)) : Set where
  constructor PackTuple
  field tupleTerm : Γ ⊢ tuple (conToTypeShift Δ)

mutualFix : ∀ {Θ} {Γ Δ : Con (Star Θ)} -> Seq (Γ ▻▻ Δ ⊢_) Δ -> Tuple Γ Δ
mutualFix {Γ = Γ} {Δ} seq
  = PackTuple
  $ fixCon Δ
  · (Λ ƛ ƛⁿ Δ (applyⁿ Δ (var (vsⁿ (shiftᶜ Δ))) $
      mapˢ (ren (keepⁿ (shiftᶜ Δ) ∘ extʳ $ ε ▻ _) ∘′ shift-⊢) seq))

-- Note that we do not perform the "pass the whole tuple in and extract each its element
-- separately" trick, because we do know the type of the result (it's `α`).
bindTuple : ∀ {Θ Γ Δ} {α : Star Θ} -> Tuple Γ Δ -> Γ ▻▻ Δ ⊢ α -> Γ ⊢ α
bindTuple {Θ} {Γ} {Δ} {α} (PackTuple tup) body = tup < α > · (ƛⁿ Δ body)

instRec : ∀ {Θ Γ Δ} {α : Star Θ} -> Seq (Γ ▻▻ Δ ⊢_) Δ -> Γ ▻▻ Δ ⊢ α -> Γ ⊢ α
instRec = bindTuple ∘ mutualFix

max_stars_repo_name: AriFordsham/plutus

max_issues_repo_name: AriFordsham/plutus

max_forks_repo_name: AriFordsham/plutus


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

record Erased (A : Set) : Set where
  constructor [_]
  field
    @0 erased : A

open Erased

data W (A : Set) (B : A → Set) : Set where
  sup : (x : A) → (B x → W A B) → W A B

lemma :
  {A : Set} {B : A → Set} →
  Erased (W A B) → W (Erased A) (λ x → Erased (B (erased x)))
lemma [ sup x f ] = sup [ x ] λ ([ y ]) → lemma [ f y ]

data ⊥ : Set where

data E : Set where
  c : E → E

magic : @0 E → ⊥
magic (c e) = magic e


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

open import Numbers.Naturals.Definition
open import Numbers.Integers.Definition
open import Numbers.Integers.Addition
open import Numbers.Integers.Multiplication
open import Numbers.Integers.Order
open import Groups.Definition

module Numbers.Integers.Integers where

open Numbers.Integers.Definition using (ℤ ; nonneg ; negSucc) public
open Numbers.Integers.Addition using (_+Z_ ; ℤGroup ; ℤAbGrp) public
open Numbers.Integers.Multiplication using (_*Z_) public
open import Numbers.Integers.RingStructure.IntegralDomain public using (ℤIntDom) public
open import Numbers.Integers.RingStructure.Ring public using (ℤRing) public
open Numbers.Integers.Order using (_<Z_ ; ℤOrderedRing) public

_-Z_ : ℤ → ℤ → ℤ
a -Z b = a +Z (Group.inverse ℤGroup b)

_^Z_ : ℤ → ℕ → ℤ
a ^Z zero = nonneg 1
a ^Z succ b = a *Z (a ^Z b)


text:
module AocUtil where
open import Data.Maybe
open import Data.String as String
open import Foreign.Haskell using (Unit)
open import Data.List as List
open import Data.Nat
open import Data.Char
open import Data.Bool.Base
open import AocIO

void : ∀ {a} {A : Set a} → IO A → IO Unit
void m = m >>= λ _ → return Unit.unit

printString : String → IO Unit
printString s = putStrLn (toCostring s)

mainBuilder : (String → (List String) → IO Unit) → IO Unit
mainBuilder main' = getProgName >>= λ name → getArgs >>= main' name

readFileMain : (String → IO Unit) → String → (List String) → IO Unit
readFileMain f name (file ∷ []) = readFiniteFile file >>= f
readFileMain f name _ = putStrLn (toCostring ("Usage: " String.++ name String.++ " FILE"))

splitWhen : ∀ {a} {A : Set a} → (A → Bool) → List A → List (List A)
splitWhen pred [] = []
splitWhen pred (x ∷ ls) with (pred x) | splitWhen pred ls
... | false | [] =  List.[ List.[ x ] ]
splitWhen pred (x ∷ ls) | false | top-list ∷ rest = (x ∷ top-list) ∷ rest
... | true | rec = [] ∷ rec

lines : List Char → List (List Char)
lines = splitWhen isNewline
  where
    isNewline : Char → Bool
    isNewline '\n' = true
    isNewline _ = false

words : List Char → List (List Char)
words = splitWhen isWhitespace
  where
    isWhitespace : Char → Bool
    isWhitespace ' ' = true
    isWhitespace '\t' = true
    isWhitespace _ = false

sequence-io-prim : ∀ {a} {A : Set a} → List (IO A) → IO (List A)
sequence-io-prim [] = return []
sequence-io-prim (m ∷ ms) = m >>= λ x → sequence-io-prim ms >>= λ xs → return (x ∷ xs)

toDigit : Char → Maybe ℕ
toDigit '0' = just 0
toDigit '1' = just 1
toDigit '2' = just 2
toDigit '3' = just 3
toDigit '4' = just 4
toDigit '5' = just 5
toDigit '6' = just 6
toDigit '7' = just 7
toDigit '8' = just 8
toDigit '9' = just 9
toDigit _ = nothing

unsafeParseNat : List Char → ℕ
unsafeParseNat ls = unsafeParseNat' 0 ls
  where
    unsafeParseNat' : ℕ → List Char → ℕ
    unsafeParseNat' acc [] = acc
    unsafeParseNat' acc (x ∷ ls) with (toDigit x)
    ... | nothing = acc * 10
    ... | just n = unsafeParseNat' (n + (acc * 10)) ls


text:
------------------------------------------------------------------------
-- The extensional sublist relation over decidable setoid equality.
------------------------------------------------------------------------

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

open import Relation.Binary

module Data.List.Relation.Binary.Subset.DecSetoid
  {c ℓ} (S : DecSetoid c ℓ) where

-- import Data.List.Relation.Binary.Permutation.Setoid as SetoidPerm
-- import Data.List.Relation.Binary.Subset.Setoid as SetoidSubset
-- import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
--   as HeterogeneousProperties
open import Level using (_⊔_)

-- open DecSetoid S
-- open SetoidSubset setoid public
-- open DecSetoidEquality S

open Relation.Binary using (Rel)
open import Data.List using (List)

------------------------------------------------------------------------
-- Subset relation

module _ where
  open import Function using (_∘_)
  open import Data.List
  open import Data.List.Membership.DecSetoid S using (_∈_; _∈?_)
  open import Relation.Nullary
  open import Data.List.Relation.Unary.Any public
  open import Data.List.Relation.Unary.Any.Properties using (¬Any[])

  open DecSetoid S

  infix 4 _⊆_ _⊈_
  _⊆_ : Rel (List Carrier) (c ⊔ ℓ)
  xs ⊆ ys = ∀ x → x ∈ xs → x ∈ ys

  _⊈_ : Rel (List Carrier) (c ⊔ ℓ)
  xs ⊈ ys = ¬ xs ⊆ ys

  -- lemma
  ∈-cong : ∀ {xs x y} → x ≈ y → x ∈ xs → y ∈ xs
  ∈-cong x≈y (here P) = here (trans (sym x≈y) P)
  ∈-cong x≈y (there P) = there (∈-cong x≈y P)

  ∉[] : ∀ {x xs} → ¬ x ∷ xs ⊆ []
  ∉[] {x} {xs} P = ¬Any[] (∈-cong {[]} {x} {x} refl (P x (here refl)))

  ⊆-refl : ∀ {xs} → xs ⊆ xs
  ⊆-refl  x P = P

  ∷-mono : ∀ {xs ys x y} → x ≈ y → xs ⊆ ys → x ∷ xs ⊆ y ∷ ys
  ∷-mono x≈y P x (here Q) = here (trans Q x≈y)
  ∷-mono x≈y P x (there Q) = there (P x Q)

  ⊆-swap : ∀ {xs x y} → x ∷ y ∷ xs ⊆ y ∷ x ∷ xs
  ⊆-swap x (here P) = there (here P)
  ⊆-swap x (there (here P)) = here P
  ⊆-swap x (there (there P)) = there (there P)

  infix 4 _⊆?_
  _⊆?_ : Decidable _⊆_
  [] ⊆? ys = yes (λ x ())
  x ∷ xs ⊆? [] = no ∉[]
  x ∷ xs ⊆? y ∷ ys with x ∈? y ∷ ys
  x ∷ xs ⊆? y ∷ ys | yes P with xs ⊆? y ∷ ys
  ... | yes Q = yes λ where x (here R) → ∈-cong (sym R) P
                            x (there R) → Q x R
  ... | no ¬Q = no λ R → ¬Q λ x S → R x (there S)
  x ∷ xs ⊆? y ∷ ys | no ¬P = no λ Q → ¬P (Q x (here refl))

------------------------------------------------------------------------
-- Equivalence relation

module _ where
  open DecSetoid S
  open import Data.Product
  open import Data.List
  open import Relation.Binary.Construct.Intersection
  open import Function.Base using (flip)
  infix 4 _≋_
  _≋_ : Rel (List Carrier) (c ⊔ ℓ)
  _≋_ = _⊆_ ∩ flip _⊆_
  {-# DISPLAY _⊆_ ∩ flip _⊆_ = _≋_ #-}

  ∷-cong : ∀ {xs ys x y} → x ≈ y → xs ≋ ys → x ∷ xs ≋ y ∷ ys
  ∷-cong x≈y (xs⊆ys , ys⊆xs) = ∷-mono x≈y xs⊆ys , ∷-mono (sym x≈y) ys⊆xs

  ≋-swap : ∀ {xs x y} → x ∷ y ∷ xs ≋ y ∷ x ∷ xs
  ≋-swap = ⊆-swap , ⊆-swap

  open import Data.List.Relation.Binary.Permutation.Homogeneous
  open import Relation.Nullary
  open import Relation.Nullary.Decidable

  infix 4 _≋?_
  _≋?_ : Decidable _≋_
  _≋?_ = decidable _⊆?_ (flip _⊆?_)

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

module _ where
  open import Data.Product

  ≋-isEquivalence : IsEquivalence _≋_
  ≋-isEquivalence = record
    { refl = (λ x z → z) , (λ x z → z)
    ; sym = λ where (P , Q) → Q , P
    ; trans = λ where (P , Q) (S , T) → (λ x U → S x (P x U)) , λ x V → Q x (T x V)
    }

  -- shorthands
  ≋-refl : Reflexive _≋_
  ≋-refl = IsEquivalence.refl ≋-isEquivalence

  ≋-sym : Symmetric _≋_
  ≋-sym = IsEquivalence.sym ≋-isEquivalence

  ≋-trans : Transitive _≋_
  ≋-trans = IsEquivalence.trans ≋-isEquivalence

  ⊆-IsPreorder : IsPreorder _≋_ _⊆_
  ⊆-IsPreorder = record
    { isEquivalence = ≋-isEquivalence
    ; reflexive = λ where (P , Q) x R → P x R
    ; trans = λ P Q x R → Q x (P x R)
    }

  ⊆-Antisymmetric : Antisymmetric _≋_ _⊆_
  ⊆-Antisymmetric P Q = P , Q

  ⊆-isPartialOrder : IsPartialOrder _≋_ _⊆_
  ⊆-isPartialOrder = record
    { isPreorder = ⊆-IsPreorder
    ; antisym = ⊆-Antisymmetric }

  ⊆-isDecPartialOrder : IsDecPartialOrder _≋_ _⊆_
  ⊆-isDecPartialOrder = record
    { isPartialOrder = ⊆-isPartialOrder
    ; _≟_            = _≋?_
    ; _≤?_           = _⊆?_
    }

------------------------------------------------------------------------
-- Bundles

poset : Poset _ _ _
poset = record
  { Carrier = List (DecSetoid.Carrier S)
  ; _≈_ = _≋_
  ; _≤_ = _⊆_
  ; isPartialOrder = ⊆-isPartialOrder
  }

setoid : Setoid _ _
setoid = record
  { Carrier = List (DecSetoid.Carrier S)
  ; _≈_ = _≋_
  ; isEquivalence = ≋-isEquivalence
  }

------------------------------------------------------------------------
-- Reasoning

module PosetReasoning where
  open import Relation.Binary.Reasoning.PartialOrder poset public
module EqReasoning where
  open import Relation.Binary.Reasoning.Setoid setoid public

max_stars_repo_name: banacorn/bidirectional

max_issues_repo_name: banacorn/bidirectional

max_forks_repo_name: banacorn/bidirectional


text:
module Esterel.Variable.Signal where

open import Data.Nat
  using (ℕ) renaming (_≟_ to _≟ℕ_)
open import Function
  using (_∘_)
open import Relation.Nullary
  using (Dec ; yes ; no ; ¬_)
open import Relation.Binary
  using (Decidable)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; cong ; trans ; sym)

data Signal : Set where
  _ₛ : (S : ℕ) → Signal

unwrap : Signal → ℕ
unwrap (n ₛ) = n

unwrap-inverse : ∀ {s} → (unwrap s) ₛ ≡ s
unwrap-inverse {_ ₛ} = refl

unwrap-injective : ∀ {s t} → unwrap s ≡ unwrap t → s ≡ t
unwrap-injective s'≡t' = trans (sym unwrap-inverse) (trans (cong _ₛ s'≡t') unwrap-inverse)

wrap : ℕ → Signal
wrap = _ₛ

bijective : ∀{x} → unwrap (wrap x) ≡ x
bijective = refl

-- for backward compatibility
unwrap-neq : ∀{k1 : Signal} → ∀{k2 : Signal} → ¬ k1 ≡ k2 → ¬ (unwrap k1) ≡ (unwrap k2)
unwrap-neq = (_∘ unwrap-injective)

_≟_ : Decidable {A = Signal} _≡_
(s ₛ) ≟ (t ₛ) with s ≟ℕ t
... | yes p = yes (cong _ₛ p)
... | no ¬p = no (¬p ∘ cong unwrap)

data Status : Set where
  present : Status
  absent  : Status
  unknown : Status

_≟ₛₜ_ : Decidable {A = Status} _≡_
present ≟ₛₜ present = yes refl
present ≟ₛₜ absent  = no λ()
present ≟ₛₜ unknown = no λ()
absent  ≟ₛₜ present = no λ()
absent  ≟ₛₜ absent  = yes refl
absent  ≟ₛₜ unknown = no λ()
unknown ≟ₛₜ present = no λ()
unknown ≟ₛₜ absent  = no λ()
unknown ≟ₛₜ unknown = yes refl

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


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

module Fragment.Examples.Semigroup.Arith.Base where

open import Fragment.Prelude public
open import Data.Nat using (ℕ; _*_; _+_) public
open import Data.Nat.Properties
  using (*-isSemigroup; +-isSemigroup)
open import Relation.Binary.PropositionalEquality public

open ≡-Reasoning public

+-semigroup = semigroup→model +-isSemigroup
*-semigroup = semigroup→model *-isSemigroup

max_stars_repo_name: yallop/agda-fragment

max_issues_repo_name: yallop/agda-fragment

max_forks_repo_name: yallop/agda-fragment


text:
module Bound.Lower.Order {A : Set}(_≤_ : A → A → Set) where

open import Bound.Lower A

data LeB : Bound → Bound → Set where
  lebx : {b : Bound}
                   → LeB bot b
  lexy : {a b : A}
                   → a ≤ b
                   → LeB (val a) (val b)

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
module Issue1078.A where -- The typo in the module name is intended!

open import Common.Level using (Level)
open import Issue1078A

test = Level


text:
------------------------------------------------------------------------
-- A quotient inductive-inductive definition of the partiality monad
------------------------------------------------------------------------

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

module Partiality-monad.Inductive 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 (id; _∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J

open import Partiality-algebra as PA hiding (_∘_)
open import Partiality-algebra.Eliminators as PAE hiding (Arguments)
import Partiality-algebra.Properties

private
  variable
    a ℓ p q : Level
    A       : Type a

mutual

  infix 10 _⊥
  infix 4  _⊑_

  -- Originally the monad was postulated. After the release of Cubical
  -- Agda it was turned into a QIIT, but in order to not get any extra
  -- computation rules it was made abstract.

  abstract

    -- The partiality monad.

    data _⊥ (A : Type a) : Type a where
      never        : A ⊥
      now          : A → A ⊥
      ⨆            : Increasing-sequence A → A ⊥
      antisymmetry : x ⊑ y → y ⊑ x → x P.≡ y

      -- We have chosen to explicitly make the type set-truncated.
      -- However, this constructor is mostly unused: it is used to
      -- define partiality-algebra below (and the corresponding record
      -- field is in turn also mostly unused, see its documentation
      -- for details), and it is mentioned in the implementation of
      -- eliminators (also below).
      ⊥-is-set-unused : P.Is-set (A ⊥)

  -- Increasing sequences.

  Increasing-sequence : Type ℓ → Type ℓ
  Increasing-sequence A =
    Σ (ℕ → A ⊥) λ f → ∀ n → f n ⊑ f (suc n)

  -- Upper bounds.

  Is-upper-bound :
    {A : Type a} → Increasing-sequence A → A ⊥ → Type a
  Is-upper-bound s x = ∀ n → (s [ n ]) ⊑ x

  -- A projection function for Increasing-sequence.

  infix 30 _[_]

  _[_] : Increasing-sequence A → ℕ → A ⊥
  _[_] s n = proj₁ {A = _ → _ ⊥} s n

  private
    variable
      x y z : A ⊥

  abstract

    -- An ordering relation.

    data _⊑_ {A : Type a} : A ⊥ → A ⊥ → Type a where
      ⊑-refl            : ∀ x → x ⊑ x
      ⊑-trans           : 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
      ⊑-propositional   : P.Is-proposition (x ⊑ y)

-- A partiality algebra for the partiality monad.

partiality-algebra : ∀ {a} (A : Type a) → Partiality-algebra a a A
partiality-algebra A = record
  { T                       = A ⊥
  ; partiality-algebra-with = record
    { _⊑_               = _⊑_
    ; never             = never′
    ; now               = now′
    ; ⨆                 = ⨆′
    ; antisymmetry      = antisymmetry′
    ; T-is-set-unused   = T-is-set-unused′
    ; ⊑-refl            = ⊑-refl′
    ; ⊑-trans           = ⊑-trans′
    ; never⊑            = never⊑′
    ; upper-bound       = upper-bound′
    ; least-upper-bound = least-upper-bound′
    ; ⊑-propositional   = ⊑-propositional′
    }
  }
  where

  abstract

    never′ : A ⊥
    never′ = never

    now′ : A → A ⊥
    now′ = now

    ⨆′ : Increasing-sequence A → A ⊥
    ⨆′ = ⨆

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

    T-is-set-unused′ : Is-set (A ⊥)
    T-is-set-unused′ =
                      $⟨ (λ {x y} → ⊥-is-set-unused {x = x} {y = y}) ⟩
      P.Is-set (A ⊥)  ↝⟨ _↔_.from (H-level↔H-level 2) ⟩□
      Is-set (A ⊥)    □

    ⊑-refl′ : (x : A ⊥) → x ⊑ x
    ⊑-refl′ = ⊑-refl

    ⊑-trans′ : 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

    ⊑-propositional′ : 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)    □

abstract

  -- The elimination principle.

  eliminators : Elimination-principle p q (partiality-algebra A)
  eliminators {A = A} args = record
    { ⊥-rec       = ⊥-rec
    ; ⊑-rec       = ⊑-rec
    ; ⊥-rec-never = refl
    ; ⊥-rec-now   = λ _ → refl
    ; ⊥-rec-⨆     = λ _ → refl
    }
    where
    module A = PAE.Arguments args

    mutual

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

      ⊥-rec : (x : A ⊥) → A.P x
      ⊥-rec never                                     = A.pe
      ⊥-rec (now x)                                   = A.po x
      ⊥-rec (⨆ s)                                     = A.pl s (inc-rec s)
      ⊥-rec (antisymmetry {x = x} {y = y} p q i)      = subst≡→[]≡
                                                          {B = A.P}
                                                          {eq = antisymmetry p q}
                                                          (A.pa p q
                                                             (⊥-rec x) (⊥-rec y)
                                                             (⊑-rec p) (⊑-rec q))
                                                          i
      ⊥-rec (⊥-is-set-unused {x = x} {y = y} p q i j) = lemma i j
        where
        ⊥-is-set-unused′ : P.Is-set (A ⊥)
        ⊥-is-set-unused′ = ⊥-is-set-unused

        lemma :
          P.[ (λ i → P.[ (λ j → A.P (⊥-is-set-unused′ 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) (A.pp {x = x}))
                  (⊥-is-set-unused p q)
                  _ _

      ⊑-rec : (x⊑y : x ⊑ y) → A.Q (⊥-rec x) (⊥-rec y) x⊑y
      ⊑-rec (⊑-refl x)                              = A.qr x (⊥-rec x)
      ⊑-rec (⊑-trans {x = x} {y = y} {z = z} p q)   = A.qt p q
                                                        (⊥-rec x) (⊥-rec y) (⊥-rec z)
                                                        (⊑-rec p) (⊑-rec q)
      ⊑-rec (never⊑ x)                              = A.qe x (⊥-rec x)
      ⊑-rec (upper-bound s n)                       = A.qu s (inc-rec s) n
      ⊑-rec (least-upper-bound s ub is-ub)          = A.ql s ub is-ub
                                                        (inc-rec s) (⊥-rec ub)
                                                        (λ n → ⊑-rec {x = proj₁ s n}
                                                                     (is-ub n))
      ⊑-rec (⊑-propositional {x = x} {y = y} p q i) = lemma i
        where
        ⊑-propositional′ : P.Is-proposition (x ⊑ y)
        ⊑-propositional′ = ⊑-propositional

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

module _ {A : Type a} where

  open Partiality-algebra (partiality-algebra A) public
    hiding (T; _⊑_; _[_]; Increasing-sequence; Is-upper-bound)
    renaming ( T-is-set to ⊥-is-set
             ; equality-characterisation-T to
               equality-characterisation-⊥
             )

  open Partiality-algebra.Properties (partiality-algebra A) public

-- The eliminators' arguments.

Arguments : ∀ {a} p q (A : Type a) → Type (a ⊔ lsuc (p ⊔ q))
Arguments p q A = PAE.Arguments p q (partiality-algebra A)

module _ (args : Arguments p q A) where
  open Eliminators (eliminators args) public

-- Initiality.

initial : Initial p q (partiality-algebra A)
initial = eliminators→initiality _ eliminators

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
module para where

module Top (A B : Set) where

  module A (C D : Set) where
    postulate f : A -> B -> C -> D

  module B (E F : Set) = A F E renaming (f to j)

  postulate h : A -> B

  module C (G H : Set) where

    module D = B G H

    g' : A -> B
    g' = h

    g : A -> H -> G
    g x y = D.j x (h x) y

module Bottom where

  postulate
    Nat : Set
    zero : Nat

  module D = Top Nat Nat
  module C = D.C Nat Nat

  x : Nat
  x = C.g zero zero


text:
-------------------------------------------------------------------------------

--
-- SET (in Hedberg library) for agda2
--  as of 2006.9.29 morning
--  Yoshiki.
--
module SET where
  ----------------------------------------------------------------------------
  -- Auxiliary.
  ----------------------------------------------------------------------------
  -- no : (x : A) -> B : Set  if A : Set B : Set
  -- yes : (x : A) -> B type   if A type  B type
  -- El M type   if  M : Set

  data Unop (A : Set) : Set1 where
    unopI : (A -> A) -> Unop A
  data Pred (A : Set) : Set1 where
    PredI : (A -> Set) -> Pred A
  data Rel (A : Set) : Set1 where
    RelI : (A -> A -> Set) -> Rel A
  data Reflexive {A : Set} (R : A -> A -> Set) : Set where
    reflexiveI : ((a : A) -> R a a) -> Reflexive R
  data Symmetrical {A : Set} (R : A -> A -> Set) : Set where
    symmetricalI : ({a b : A} -> R a b -> R a b) -> Symmetrical R
  data Transitive {A : Set} (R : A -> A -> Set) : Set where
    transitiveI : ({a b c : A} -> R a b -> R b c -> R a c) -> Transitive R
  compositionalI :
    {A : Set} -> (R : A -> A -> Set)
    -> ({a b c : A} -> R b c -> R a b -> R a c) -> Transitive R
  compositionalI {A} R f =
    transitiveI (\{a b c : A} -> \(x : R a b) -> \(y : R b c) -> f y x)
  data Substitutive {A : Set} (R : A -> A -> Set) : Set1 where
    substitutiveI : ((P : A -> Set) -> {a b : A} -> R a b -> P a -> P b)
                   -> Substitutive R
  data Collapsed (A : Set) : Set1 where
    collapsedI : ((P : A -> Set) -> {a b : A} -> P a -> P b) -> Collapsed A

  cmp : {A B C : Set} -> (B -> C) -> (A -> B) -> A -> C
  cmp f g a = f (g a)
  seq : {A B C : Set} -> (A -> B) -> (B -> C) -> A -> C
  seq f g = cmp g f

  S : {A B C : Set} -> (C -> B -> A) -> (C -> B) -> C -> A
  S x y z = x z (y z)
  K : {A B : Set} -> A -> B -> A
  K x y = x
  I : {A : Set} -> A -> A
  I a = a
  -- of course I = S K K

  id = \{A : Set} -> I {A}

  const = \{A B : Set} -> K {A}{B}

  -- Set version
  pS : {P Q R : Set} -> (R -> Q -> P) -> (R -> Q) -> R -> P
  pS x y z = x z (y z)
  pK : {P Q : Set} -> P -> Q -> P
  pK x y = x
  pI : {P : Set} -> P -> P
  pI a = a

  proj : {A : Set} -> (B : A -> Set) -> (a : A) -> (f : (aa : A) -> B aa) -> B a
  proj B a f = f a

  flip : {A B C : Set} (f : A -> B -> C) (b : B) (a : A) -> C
  flip f b a = f a b

  -- separate definition of FlipRel is necessary because it is not the case
  -- that Set : Set.
  FlipRel : {A : Set} -> (R : A -> A -> Set) -> (a b : A) -> Set
  FlipRel R a b = R b a

  ----------------------------------------------------------------------------
  -- Product sets.
  ----------------------------------------------------------------------------
--  Prod : (A : Set) -> (A -> Set) -> Set
--  Prod A B = (a : A) -> B a
--  The above is not type-correct since (a : A) -> B a is not well-formed
--  but the following works.
  data Prod (A : Set) (B : A -> Set) : Set where
    prodI : ((a : A) -> B a) -> Prod A B
  mapProd : {A : Set} -> {B C : A -> Set} -> ((a : A) -> B a -> C a)
           -> Prod A B -> Prod A C
  mapProd {A} f (prodI g) = prodI (\(a : A) -> f a (g a))

--  data Fun (A B : Set) : Set1 where
--    funI : (A -> B) -> Fun A B
  Fun : Set -> Set -> Set
  Fun A B = Prod A (\(_ : A) -> B)

  mapFun : {A B C D : Set} -> (B -> A) -> (C -> D) -> (A -> C) -> B -> D
  mapFun {A} {B} {C} {D} f g h x = g (h (f x))
--  mapFun (|X1 |X2 |Y1 |Y2 :: Set)
--    :: (X2 -> X1) -> (Y1 -> Y2) -> (X1 -> Y1) -> X2 -> Y2
--    = \f -> \g -> \h -> \x ->
--      g (h (f x))

---------------------------------------------------------------------------
-- Identity proof sets.
---------------------------------------------------------------------------
-- to accept the following definition more general scheme of
-- inductive definition is required
--  data Id (A : Set) (a b : A) : Set1 where
--    ref : (a : A) -> Id A a a
--
--  elimId (|X :: Set)
--         (C :: (x1 x2 :: X)  |-> Id x1 x2 -> Set)
--         (refC :: (x :: X) -> C (refId x))
--         (|x1 |x2 :: X)
--         (u :: Id x1 x2) ::
--         C u
--    = case u of { (ref x) -> refC x;}
--
--  abstract whenId (|X :: Set)(C :: Rel X)(c :: (x :: X) -> C x x)
--    :: (x1 x2 :: X)  |-> Id x1 x2 -> C x1 x2
--    = elimId (\x1 x2 |-> \(u :: Id x1 x2) -> C x1 x2) c
--
--  abstract substId (|X :: Set) :: Substitutive Id
--    = \(C :: Pred X) ->
--      whenId (\x1 x2 -> C x1 -> C x2) (\x -> id)
--
--  abstract mapId (|X :: Set)(|Y :: Set)(f :: X -> Y)
--    :: (x1 x2 :: X) |-> Id x1 x2 -> Id (f x1) (f x2)
--    = whenId (\x1 x2 -> Id (f x1) (f x2)) (\(x :: X) -> refId (f x))
--
--  abstract symId (|X :: Set) :: Symmetrical Id
--    =  whenId (\(x1 x2 :: X) ->  Id x2 x1) refId
--
--  abstract cmpId (|X :: Set) :: Compositional Id
--    = let lem :: (x y :: X) |-> Id x y -> (z :: X) |-> Id z x -> Id z y
--            = whenId ( \(x y :: _) -> (z :: X) |-> Id z x -> Id z y)
--                     ( \x -> \z |-> id)
--      in  \(x1 x2 x3 :: _) |->
--          \(u :: Id x2 x3) ->
--          \(v :: Id x1 x2) ->
--          lem  u v
--
--  abstract tranId (|X :: Set) :: Transitive  Id
--    = \(x1 x2 x3 :: X) |->
--      \(u :: Id x1 x2) ->
--      \(v :: Id x2 x3) ->
--      cmpId v u

  ----------------------------------------------------------------------------
  -- The empty set.
  ----------------------------------------------------------------------------
  data Zero : Set where
--  --abstract whenZero (X :: Set)(z :: Zero) :: X
--  --  = case z of { }
--  do not know how to encode whenZero;  the following does not work.
--  whenZero : (X : Set) -> (z : Zero) -> X
--  whenZero X z =
--  --elimZero (C :: Zero -> Set)(z :: Zero) :: C z
--  --  = case z of { }
--  elimZero either!
--  elimZero : (C : Zero -> Set) -> (z : Zero) -> C z
--  elimZero C z =
--
--  abstract collZero :: Collapsed Zero
--    = \(C :: Zero -> Set) ->
--      \(z1 z2 :: Zero) |->
--      \(c :: C z1) ->
--      case z1 of { }
--
----------------------------------------------------------------------------
-- The singleton set.
----------------------------------------------------------------------------
  data Unit : Set where
    uu : Unit
  elUnit = uu
  elimUnit : (C : Unit -> Set) -> C uu -> (u : Unit) -> C u
  elimUnit C c uu = c
--  Do not know of the exact use of Collapse!
--  collUnit : (C : Unit -> Set) -> {u1  u2 : Unit} -> C u1 -> Collapsed Unit
--  collUnit C {uu} {uu} A = collapsedI (\(P : Unit -> Set) -> \{a b : Unit} -> \(y : P a) -> A)
--  abstract collUnit :: Collapsed Unit
--    = \(C :: Unit -> Set) ->
--      \(u1 u2 :: Unit) |->
--      \(c :: C u1) ->
--      case u1 of { (tt) -> case u2 of { (tt) -> c;};}
---------------------------------------------------------------------------
-- The successor set adds a new element.
---------------------------------------------------------------------------

  data Succ (A : Set) : Set where
    zerS : Succ A
    sucS : A -> Succ A
  zerSucc = \{A : Set} -> zerS {A}
  sucSucc = \{A : Set} -> sucS {A}
  elimSucc : {X : Set} -> (C : Succ X -> Set)
            -> C zerS -> ((x : X) -> C (sucS x)) -> (xx : Succ X) -> (C xx)
  elimSucc C c_z c_s zerS = c_z
  elimSucc C c_z c_s (sucS x) = c_s x
  whenSucc : {X Y : Set} -> Y -> (X -> Y) -> (Succ X) -> Y
  whenSucc y_z y_s zerS = y_z
  whenSucc y_z y_s (sucS x) = y_s x
  mapSucc : {X Y : Set} -> (X -> Y) -> Succ X -> Succ Y
  mapSucc {X} {_} f
    = whenSucc zerS (\(x : X) -> sucS (f x))

---------------------------------------------------------------------------
-- The (binary) disjoint union.
---------------------------------------------------------------------------

  data Plus (A B : Set) : Set where
    inl : A -> Plus A B
    inr : B -> Plus A B
  elimPlus : {X Y : Set} ->
            (C : Plus X Y -> Set) ->
            ((x : X) -> C (inl x)) ->
            ((y : Y) -> C (inr y)) ->
            (z : Plus X Y) ->
            C z
  elimPlus {X} {Y} C c_lft c_rgt (inl x) = c_lft x
  elimPlus {X} {Y} C c_lft c_rgt (inr x) = c_rgt x
  when : {X Y Z : Set} -> (X -> Z) -> (Y -> Z) -> Plus X Y -> Z
  when {X} {Y} {Z} f g (inl x) = f x
  when {X} {Y} {Z} f g (inr y) = g y
  whenplus : {X Y Z : Set} -> (X -> Z) -> (Y -> Z) -> Plus X Y -> Z
  whenplus = when
  mapPlus : {X1 X2 Y1 Y2 : Set} -> (X1 -> X2) -> (Y1 -> Y2)
           -> Plus X1 Y1 -> Plus X2 Y2
  mapPlus f g = when (\x1 -> inl (f x1)) (\y1 -> inr (g y1))
  swapPlus : {X Y : Set} -> Plus X Y -> Plus Y X
  swapPlus = when inr inl

----------------------------------------------------------------------------
-- Dependent pairs.
----------------------------------------------------------------------------

  data Sum (A : Set) (B : A -> Set) : Set where
    sumI : (fst : A) -> B fst -> Sum A B
  depPair : {A : Set} -> {B : A -> Set} -> (a : A) -> B a -> Sum A B
  depPair a b = sumI a b
  depFst : {A : Set} -> {B : A -> Set} -> (c : Sum A B) -> A
  depFst (sumI fst snd) = fst
  depSnd : {A : Set} -> {B : A -> Set} -> (c : Sum A B) -> B (depFst c)
  depSnd (sumI fst snd) = snd
  depCur : {A : Set} -> {B : A -> Set} -> {C : Set} -> (f : Sum A B -> C)
           -> (a : A) -> B a -> C
  depCur f = \a -> \b -> f (depPair a b)
  -- the above works but the below does not---why?
  -- depCur : {X : Set} -> {Y : X -> Set} -> {Z : Set} -> (f : Sum X Y -> Z)
  --         -> {x : X} -> Y x -> Z
  -- depCur {X} {Y} {Z} f = \{x} -> \y ->  f (depPair  x  y)
  -- Error message :
  -- When checking that the expression \{x} -> \y -> f (depPair x y)
  -- has type Y _x -> Z
  -- found an implicit lambda where an explicit lambda was expected
  depUncur : {A : Set} -> {B : A -> Set} -> {C : Set}
    -> ((a : A) -> B a -> C) -> Sum A B -> C
  depUncur f ab = f (depFst ab) (depSnd ab)
  depCurry : {A : Set} ->
             {B : A -> Set} ->
             {C : Sum A B -> Set} ->
             (f : (ab : Sum A B) -> C ab) ->
             (a : A) ->
             (b : B a) ->
             C (depPair a b)
  depCurry f a b = f (depPair a b)
  depUncurry : {A : Set} ->
               {B : A -> Set} ->
               {C : Sum A B -> Set} ->
               (f : (a : A) -> (b : B a) -> C (depPair a b)) ->
               (ab : Sum A B) ->
               C ab
  depUncurry f (sumI fst snd) = f fst snd
  mapSum : {A : Set} -> {B1 : A -> Set} -> {B2 : A -> Set}
          -> (f : (a : A) -> B1 a -> B2 a)
          -> Sum A B1 -> Sum A B2
  mapSum f (sumI fst snd) = depPair fst (f fst snd)
  elimSum = \{A : Set}{B : A -> Set}{C : Sum A B -> Set} -> depUncurry{A}{B}{C}
---------------------------------------------------------------------------
-- Nondependent pairs (binary) cartesian product.
---------------------------------------------------------------------------
  Times : Set -> Set -> Set
  Times A B = Sum A (\(_ : A) -> B)
  pair : {A : Set} -> {B : Set} -> A -> B -> Times A B
  pair a b = sumI a b
  fst : {A : Set} -> {B : Set} -> Times A B -> A
  fst (sumI a _) = a
  snd : {A : Set} -> {B : Set} -> Times A B -> B
  snd (sumI _ b) = b
  pairfun : {C : Set} -> {A : Set} -> {B : Set}
           -> (C -> A) -> (C -> B) -> C -> Times A B
  pairfun f g c = pair (f c) (g c)
  mapTimes : {A1 : Set} -> {A2 : Set} -> {B1 : Set} -> {B2 : Set}
            -> (A1 -> A2) -> (B1 -> B2) -> Times A1 B1 -> Times A2 B2
  mapTimes f g (sumI a b) = pair (f a) (g b)
  swapTimes : {A : Set} -> {B : Set} -> Times A B -> Times B A
  swapTimes (sumI a b) = sumI b a
  cur : {A : Set} -> {B : Set} -> {C : Set} -> (f : Times A B -> C) -> A -> B -> C
  cur f a b = f (pair a b)
  uncur : {A : Set} -> {B : Set} -> {C : Set} -> (A -> B -> C) -> Times A B -> C
  uncur f (sumI a b) = f a b
  curry : {A : Set} -> {B : Set} -> {C : Times A B -> Set}
         -> ((p : Times A B) -> C p) -> (a : A) ->(b : B) -> C (pair a b)
  curry f a b = f (pair a b)
  uncurry : {A : Set} -> {B : Set} -> {C : Times A B -> Set}
           -> ((a : A) -> (b : B) -> C (pair a b)) -> (p : Times A B) -> C p
  uncurry f (sumI a b) = f a b
  elimTimes = \{A B : Set}{C : Times A B -> Set} -> uncurry{A}{B}{C}
  ---------------------------------------------------------------------------
  -- Natural numbers.
  ---------------------------------------------------------------------------
  data Nat : Set where
    zero : Nat
    succ : Nat -> Nat
  elimNat : (C : Nat -> Set)
           -> (C zero) -> ((m : Nat) -> C m -> C (succ m)) -> (n : Nat) -> C n
  elimNat C c_z c_s zero = c_z
  elimNat C c_z c_s (succ m') = c_s m' (elimNat C c_z c_s m')

  ----------------------------------------------------------------------------
  -- Linear universe of finite sets.
  ----------------------------------------------------------------------------
  Fin : (m : Nat) -> Set
  Fin zero = Zero
  Fin (succ n) = Succ (Fin n)
{-
  Fin 0 = {}
  Fin 1 = { zerS }
  Fin 2 = { zerS (sucS zerS) }
  Fin 3 = { zerS (sucS zerS) (sucS (sucS zerS)) }
-}
  valFin : (n' : Nat) -> Fin n' -> Nat
  valFin zero     ()
  valFin (succ n) zerS = zero
  valFin (succ n) (sucS x) = succ (valFin n x)
  zeroFin : (n : Nat) -> Fin (succ n)
  zeroFin n = zerS
  succFin : (n : Nat) -> Fin n -> Fin (succ n)
  succFin n N = sucS N
  ----------------------------------------------------------------------------
  -- Do these really belong here?
  ----------------------------------------------------------------------------
  HEAD : {A : Set} -> (n : Nat) -> (Fin (succ n) -> A) -> A
  HEAD n f = f (zeroFin n)
  TAIL : {A : Set} -> (n : Nat) -> (Fin (succ n) -> A) -> Fin n -> A
  TAIL n f N = f (succFin n N)
  ----------------------------------------------------------------------------
  -- Lists.
  ----------------------------------------------------------------------------
  data List (A : Set) : Set where
    nil : List A
    con : A -> List A -> List A
  elimList : {A : Set} ->
            (C : List A -> Set) ->
            (C nil) ->
            ((a : A) -> (as : List A) -> C as -> C (con a as)) ->
            (as : List A) ->
            C as
  elimList _ c_nil _ nil = c_nil
  elimList C c_nil c_con (con a as) = c_con a as (elimList C c_nil c_con as)
  ----------------------------------------------------------------------------
  -- Tuples are "dependently typed vectors".
  ----------------------------------------------------------------------------
  data Nill : Set where
    nill : Nill
  data Cons (A B : Set) : Set where
    cons : A -> B -> Cons A B
  Tuple : (n : Nat) -> (C : Fin n -> Set) -> Set
  Tuple zero = \ C -> Nill
  Tuple (succ n) = \ C -> Cons (C zerS) (Tuple n (\(N : Fin n) -> C (sucS N)))
  ----------------------------------------------------------------------------
  -- Vectors homogeneously typed tuples.
  ----------------------------------------------------------------------------
  Vec : Set -> Nat -> Set
  Vec A m = Tuple m (\(n : Fin m) -> A)
  ----------------------------------------------------------------------------
  -- Monoidal expressions.
  ----------------------------------------------------------------------------
  data Mon (A : Set) : Set where
    unit : Mon A
    at : A -> Mon A
    mul : Mon A -> Mon A -> Mon A
{-
-}

----------------------------------------------------------------------------
-- Propositions.
----------------------------------------------------------------------------
  data Implies (A B : Set) : Set where
    impliesI : (A -> B) -> Implies A B
  data Absurd : Set where
  data Taut : Set where
    tt : Taut
  data Not (P : Set) : Set where
    notI : (P -> Absurd) -> Not P
  -- encoding of Exists is unsatisfactory!  Its type should be Set.
  data Exists (A : Set) (P : A -> Set) : Set where
    existsI : (evidence : A) -> P evidence -> Exists A P
  data Forall (A : Set) (P : A -> Set) : Set where
    forallI : ((a : A) -> P a) -> Forall A P
  data And (A B : Set) : Set where
    andI : A -> B -> And A B
  Iff : Set -> Set -> Set
  Iff A B = And (Implies A B) (Implies B A)
  data Or (A B : Set) : Set where
    orIl : (a : A) -> Or A B
    orIr : (b : B) -> Or A B
  Decidable : Set -> Set
  Decidable P = Or P (Implies P Absurd)
  data DecidablePred {A : Set} (P : A -> Set) : Set where
   decidablepredIl : (a : A) -> (P a) -> DecidablePred P
   decidablepredIr : (a : A) -> (Implies (P a) Absurd) -> DecidablePred P
  data DecidableRel {A : Set} (R : A -> A -> Set) : Set where
   decidablerelIl : (a b : A) -> (R a b) -> DecidableRel R
   decidablerelIr : (a b : A) -> (Implies (R a b) Absurd) -> DecidableRel R
  data Least {A : Set} (_<=_ : A -> A -> Set) (P : A -> Set) (a : A) : Set where
    leastI : (P a) -> ((aa : A) -> P aa -> (a <= aa)) -> Least _<=_ P a
  data Greatest {A : Set} (_<=_ : A -> A -> Set) (P : A -> Set) (a : A) : Set where
    greatestI : (P a) -> ((aa : A) -> P aa -> (aa <= a)) -> Greatest _<=_ P a

----------------------------------------------------------------------------
-- Booleans.
----------------------------------------------------------------------------
  data Bool : Set where
    true : Bool
    false : Bool
  elimBool : (C : Bool -> Set) -> C true -> C false -> (b : Bool) -> C b
  elimBool C c_t c_f true = c_t
  elimBool C c_t c_f false = c_f
  whenBool : (C : Set) -> C -> C -> Bool -> C
  whenBool C c_t c_f b = elimBool (\(_ : Bool) -> C) c_t c_f b
  data pred (A : Set) : Set where
    predI : (A -> Bool) -> pred A
  data rel (A : Set) : Set where
    relI : (A -> A -> Bool) -> rel A
  True : Bool -> Set
  True true = Taut
  True false = Absurd
  bool2set = True
  pred2Pred : {A : Set} -> pred A -> Pred A
  pred2Pred (predI p) = PredI (\a -> True (p a))
  rel2Rel : {A : Set} -> rel A -> Rel A
  rel2Rel (relI r) = RelI (\a -> \b -> True (r a b))
--  decTrue : (p : Bool) -> Decidable (True p)
--  decTrue true = orIl tt
--  decTrue false = orIr (impliesI pI)
-- decTrue false = orIr (impliesI (\(p : (True false)) -> p))
--  dec_lem : {P : Set} -> (decP : Decidable P)
--           -> Exists A
{-
  abstract dec_lem (|P :: Set)(decP :: Decidable P)
    :: Exist |_ (\(b :: Bool) -> Iff (True b) P)
    = case decP of {
        (inl trueP) ->
          struct {
            fst = true@_;
            snd =
              struct {
                fst = const |_  |_ trueP;  -- (True true@_)
                snd = const |_ |_  tt;};};
        (inr notP) ->
          struct {
            fst = false@_;
            snd =
              struct {
                fst = whenZero P;
                snd = notP;};};}
  dec2bool :: (P :: Set) |-> (decP :: Decidable P) -> Bool
    = \(P :: Set) |-> \(decP :: Decidable P) -> (dec_lem |_ decP).fst
  dec2bool_spec (|P :: Set)(decP :: Decidable P)
    :: Iff (True (dec2bool |_ decP)) P
    = (dec_lem |_ decP).snd

  abstract collTrue :: (b :: Bool) -> Collapsed (True b)
    = let aux (X :: Set)(C :: X -> Set)
            :: (b :: Bool) ->
               (f :: True b -> X) ->
               (t1 :: True b) |->
               (t2 :: True b) |->
               C (f t1) -> C (f t2)
            = \(b :: Bool) ->
              case b of {
                (true) ->
                  \(f :: (x :: True true@_) -> X) ->
                  \(t1 t2 :: True true@_) |->
                  \(c :: C (f t1)) ->
                  case t1 of { (tt) -> case t2 of { (tt) -> c;};};
                (false) ->
                  \(f :: (x :: True false@_) -> X) ->
                  \(t1 t2 :: True false@_) |->
                  \(c :: C (f t1)) ->
                  case t1 of { };}
      in   \(b :: Bool) ->  \(P :: True b -> Set) -> aux (True b) P b id

  bool2nat (p :: Bool) :: Nat
    = case p of {
        (true) -> succ zero;
        (false) -> zero;}
-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
-- Andreas, 2014-09-23

module _ where

syntax c x   = ⟦ x ⟧
syntax c x y = x + y

-- Should complain about multiple notations.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- An Agda example file

module test where

open import Coinduction
open import Data.Bool
open import {- pointless comment between import and module name -} Data.Char
open import Data.Nat
open import Data.Nat.Properties
open import Data.String
open import Data.List hiding ([_])
open import Data.Vec hiding ([_])
open import Relation.Nullary.Core
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; trans; inspect; [_])

open SemiringSolver

{- this is a {- nested -} comment -}

-- Factorial
_! : ℕ → ℕ
0 ! = 1
(suc n) ! = (suc n) * n !

-- The binomial coefficient
_choose_ : ℕ → ℕ → ℕ
_ choose 0 = 1
0 choose _ = 0
(suc n) choose (suc m) = (n choose m) + (n choose (suc m)) -- Pascal's rule

choose-too-many : ∀ n m → n ≤ m → n choose (suc m) ≡ 0
choose-too-many .0 m z≤n = refl
choose-too-many (suc n) (suc m) (s≤s le) with n choose (suc m) | choose-too-many n m le | n choose (suc (suc m)) | choose-too-many n (suc m) (≤-step le)
... | .0 | refl | .0 | refl = refl

_++'_ : ∀ {a n m} {A : Set a} → Vec A n → Vec A m → Vec A (m + n)
_++'_ {_} {n} {m} v₁ v₂ rewrite solve 2 (λ a b → b :+ a := a :+ b) refl n m = v₁ Data.Vec.++ v₂

++'-test : (1 ∷ 2 ∷ 3 ∷ []) ++' (4 ∷ 5 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
++'-test = refl

data Coℕ : Set where
  co0   : Coℕ
  cosuc : ∞ Coℕ → Coℕ

nanana : Coℕ
nanana = let two = ♯ cosuc (♯ (cosuc (♯ co0))) in cosuc two

abstract
  data VacuumCleaner : Set where
    Roomba : VacuumCleaner

pointlessLemmaAboutBoolFunctions : (f : Bool → Bool) → f (f (f true)) ≡ f true
pointlessLemmaAboutBoolFunctions f with f true | inspect f true
... | true  | [ eq₁ ] = trans (cong f eq₁) eq₁
... | false | [ eq₁ ] with f false | inspect f false
... | true  | _       = eq₁
... | false | [ eq₂ ] = eq₂

mutual
  isEven : ℕ → Bool
  isEven 0       = true
  isEven (suc n) = not (isOdd n)

  isOdd : ℕ → Bool
  isOdd 0       = false
  isOdd (suc n) = not (isEven n)

foo : String
foo = "Hello World!"

nl : Char
nl = '\n'

private
  intersperseString : Char → List String → String
  intersperseString c []       = ""
  intersperseString c (x ∷ xs) = Data.List.foldl (λ a b → a Data.String.++ Data.String.fromList (c ∷ []) Data.String.++ b) x xs

baz : String
baz = intersperseString nl (Data.List.replicate 5 foo)

postulate
  Float : Set

{-# BUILTIN FLOAT Float  #-}

pi : Float
pi = 3.141593

-- Astronomical unit
au : Float
au = 1.496e11 -- m

plusFloat : Float → Float → Float
plusFloat a b = {! !}

record Subset (A : Set) (P : A → Set) : Set where
  constructor _#_
  field
    elem   : A
    .proof : P elem


text:
module Monad where

module Prelude where

  infixl 40 _∘_

  id : {A : Set} -> A -> A
  id x = x

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

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

module Base where

  data Monad (M : Set -> Set) : Set1 where
    monad : (return : {A : Set} -> A -> M A)                 ->
            (bind   : {A B : Set} -> M A -> (A -> M B) -> M B) ->
            Monad M

  monadReturn : {M : Set -> Set} -> Monad M -> {A : Set} -> A -> M A
  monadReturn (monad ret bind) = ret

  monadBind : {M : Set -> Set} -> Monad M -> {A B : Set} -> M A -> (A -> M B) -> M B
  monadBind (monad ret bind) = bind

module Monad {M : Set -> Set}(monadM : Base.Monad M) where

  open Prelude

  infixl 15 _>>=_

  -- Return and bind --------------------------------------------------------

  return : {A : Set} -> A -> M A
  return = Base.monadReturn monadM

  _>>=_ : {A B : Set} -> M A -> (A -> M B) -> M B
  _>>=_ = Base.monadBind monadM

  -- Other operations -------------------------------------------------------

  liftM : {A B : Set} -> (A -> B) -> M A -> M B
  liftM f m = m >>= return ∘ f

module List where

  infixr 20 _++_ _::_

  -- The list datatype ------------------------------------------------------

  data List (A : Set) : Set where
    nil  : List A
    _::_ : A -> List A -> List A

  -- Some list operations ---------------------------------------------------

  foldr : {A B : Set} -> (A -> B -> B) -> B -> List A -> B
  foldr f e nil     = e
  foldr f e (x :: xs) = f x (foldr f e xs)

  map : {A B : Set} -> (A -> B) -> List A -> List B
  map f nil     = nil
  map f (x :: xs) = f x :: map f xs

  _++_ : {A : Set} -> List A -> List A -> List A
  nil       ++ ys = ys
  (x :: xs) ++ ys = x :: (xs ++ ys)

  concat : {A : Set} -> List (List A) -> List A
  concat = foldr _++_ nil

  -- List is a monad --------------------------------------------------------

  open Base

  monadList : Monad List
  monadList = monad ret bind
    where
      ret : {A : Set} -> A -> List A
      ret x = x :: nil

      bind : {A B : Set} -> List A -> (A -> List B) -> List B
      bind xs f = concat (map f xs)

open Prelude
open List
module MonadList = Monad monadList
open MonadList


text:
module Highlighting.M where

postulate
  ℕ : Set
  _+_ _*_ : (x y : ℕ) → ℕ


text:
module Definitions where

data _∨_ (A B : Set) : Set where
  inl : A → A ∨ B
  inr : B → A ∨ B

data _∧_ (A B : Set) : Set where
  _,_ : A → B → A ∧ B

data ⊥ : Set where

¬_ : Set → Set
¬ A = A → ⊥

max_stars_repo_name: danr/agder

max_issues_repo_name: danr/agder

max_forks_repo_name: danr/agder


text:
{-# OPTIONS --without-K #-}
module equality.calculus where

open import sum using (Σ ; _,_ ; proj₁; proj₂)
open import equality.core
open import equality.groupoid public
open import function.core

ap' : ∀ {i j} {X : Set i}{Y : X → Set j}
        {x x' : X}(f : (x : X) → Y x)(p : x ≡ x')
      → subst Y p (f x) ≡ f x'
ap' _ refl = refl

subst-naturality : ∀ {i i' j} {X : Set i} {Y : Set i'}
                   {x x' : X} (P : Y → Set j)
                   (f : X → Y)(p : x ≡ x')(u : P (f x))
                 → subst (P ∘ f) p u ≡ subst P (ap f p) u
subst-naturality _ _ refl _ = refl

subst-hom : ∀ {i j}{X : Set i}(P : X → Set j){x y z : X}
          → (p : x ≡ y)(q : y ≡ z)(u : P x)
          → subst P q (subst P p u) ≡ subst P (p · q) u
subst-hom _ refl q u = refl

subst-eq : ∀ {i} {X : Set i}{x y z : X}
         → (p : y ≡ x)(q : y ≡ z)
         → subst (λ y → y ≡ z) p q
         ≡ sym p · q
subst-eq refl _ = refl

subst-eq₂ : ∀ {i} {X : Set i}{x y : X}
          → (p : x ≡ y)
          → (q : x ≡ x)
          → subst (λ z → z ≡ z) p q ≡ sym p · q · p
subst-eq₂ refl q = sym (left-unit _)

subst-const : ∀ {i j} {A : Set i}{X : Set j}
            → {a a' : A}(p : a ≡ a')(x : X)
            → subst (λ _ → X) p x ≡ x
subst-const refl x = refl

subst-const-ap : ∀ {i j} {A : Set i}{X : Set j}
                 → {a a' : A}(f : A → X)(p : a ≡ a')
                 → ap' f p ≡ subst-const p (f a) · ap f p
subst-const-ap f refl = refl

apΣ : ∀ {i j}{A : Set i}{B : A → Set j}
        {x x' : Σ A B}
     → (p : x ≡ x')
     → Σ (proj₁ x ≡ proj₁ x') λ q
     → subst B q (proj₂ x) ≡ proj₂ x'
apΣ {B = B} p =
  J (λ x x' p → Σ (proj₁ x ≡ proj₁ x') λ q
              → subst B q (proj₂ x) ≡ proj₂ x')
    (λ x → refl , refl)
    _ _ p

unapΣ : ∀ {i j}{A : Set i}{B : A → Set j}
          {a a' : A}{b : B a}{b' : B a'}
        → (Σ (a ≡ a') λ q → subst B q b ≡ b')
        → (a , b) ≡ (a' , b')
unapΣ (refl , refl) = refl

pair≡ : ∀ {i j}{A : Set i}{B : Set j}
          {a a' : A}{b b' : B}
        → (a ≡ a') → (b ≡ b')
        → (a , b) ≡ (a' , b')
pair≡ refl refl = refl

apΣ-proj : ∀ {i j}{A : Set i}{B : A → Set j}
             {a a' : A}{b : B a}{b' : B a'}
             (p : (a , b) ≡ (a' , b'))
           → proj₁ (apΣ p)
           ≡ ap proj₁ p
apΣ-proj =
  J (λ _ _ p → proj₁ (apΣ p) ≡ ap proj₁ p)
    (λ x → refl) _ _

apΣ-sym : ∀ {i j}{A : Set i}{B : A → Set j}
            {a a' : A}{b : B a}{b' : B a'}
            (p : (a , b) ≡ (a' , b'))
          → proj₁ (apΣ (sym p))
          ≡ sym (proj₁ (apΣ p))
apΣ-sym =
  J (λ _ _ p → proj₁ (apΣ (sym p))
             ≡ sym (proj₁ (apΣ p)))
    (λ x → refl) _ _

subst-ap : ∀ {i j}{A : Set i}{B : Set j}{a a' : A}
           → (f : A → B)
           → (p : a ≡ a')
           → ap f (sym p)
           ≡ subst (λ x → f x ≡ f a) p refl
subst-ap f refl = refl

ap-map-id : ∀ {i j}{X : Set i}{Y : Set j}{x : X}
            → (f : X → Y)
            → ap f (refl {x = x}) ≡ refl {x = f x}
ap-map-id f = refl

ap-map-hom : ∀ {i j}{X : Set i}{Y : Set j}{x y z : X}
             → (f : X → Y)(p : x ≡ y)(q : y ≡ z)
             → ap f (p · q) ≡ ap f p · ap f q
ap-map-hom f refl _ = refl

ap-id : ∀ {l} {A : Set l}{x y : A}(p : x ≡ y)
        → ap id p ≡ p
ap-id refl = refl

ap-hom : ∀ {l m n} {A : Set l}{B : Set m}{C : Set n}
           {x y : A}(f : A → B)(g : B → C)(p : x ≡ y)
         → ap g (ap f p) ≡ ap (g ∘ f) p
ap-hom f g refl = refl

ap-inv : ∀ {i j} {X : Set i} {Y : Set j}
         → {x x' : X}
         → (f : X → Y)(p : x ≡ x')
         → ap f (sym p) ≡ sym (ap f p)
ap-inv f refl = refl

double-inverse : ∀ {i} {X : Set i} {x y : X}
               (p : x ≡ y) → sym (sym p) ≡ p
double-inverse refl = refl

inverse-comp : ∀ {i} {X : Set i} {x y z : X}
               (p : x ≡ y)(q : y ≡ z)
             → sym (p · q) ≡ sym q · sym p
inverse-comp refl q = sym (left-unit (sym q))

inverse-unique : ∀ {i} {X : Set i} {x y : X}
                 (p : x ≡ y)(q : y ≡ x)
               → p · q ≡ refl
               → sym p ≡ q
inverse-unique refl q t = sym t

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
open import Relation.Nullary.Decidable using (False)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; module ≡-Reasoning)

open import Data.List using (List)
open List
open import Data.Unit using (tt)

module AKS.Binary.Base where

open import Polynomial.Simple.AlmostCommutativeRing using (AlmostCommutativeRing)
open import Polynomial.Simple.AlmostCommutativeRing.Instances using (module Nat)
open Nat.Reflection using (∀⟨_⟩)

open import AKS.Nat using (ℕ; _+_; _*_; _≟_; _<_; lte; suc-mono-≤)
open ℕ
open import AKS.Nat using (ℕ⁺; ℕ+; ⟅_⇑⟆)
open import AKS.Nat using (Euclidean; Euclidean✓; _div_)
open import AKS.Nat using (Acc; acc; <-well-founded)

2* : ℕ → ℕ
2* n = n + n

infixl 5 _0ᵇ _1ᵇ
data 𝔹⁺ : Set where
  𝕓1ᵇ : 𝔹⁺
  _0ᵇ _1ᵇ : 𝔹⁺ → 𝔹⁺

infixr 4 +_
data 𝔹 : Set where
  𝕓0ᵇ : 𝔹
  +_ : 𝔹⁺ → 𝔹

⟦_⇓⟧⁺ : 𝔹⁺ → ℕ
⟦ 𝕓1ᵇ  ⇓⟧⁺ = 1
⟦ x 0ᵇ ⇓⟧⁺ = 2* ⟦ x ⇓⟧⁺
⟦ x 1ᵇ ⇓⟧⁺ = 1 + 2* ⟦ x ⇓⟧⁺

⟦_⇓⟧ : 𝔹 → ℕ
⟦ 𝕓0ᵇ ⇓⟧ = 0
⟦ + x ⇓⟧ = ⟦ x ⇓⟧⁺

private
  lemma₁ : ∀ {q} → suc q < suc (q + suc (q + zero))
  lemma₁ {q} = lte q (∀⟨ q ∷ [] ⟩)
  lemma₂ : ∀ {q} → suc q < suc (suc (q + suc (q + zero)))
  lemma₂ {q} = lte (suc q) (∀⟨ q ∷ [] ⟩)

⟦_⇑_⟧ʰ : ∀ n → Acc _<_ n → ∀ {≢0 : False (n ≟ 0)} → 𝔹⁺
⟦ suc n ⇑ acc downward ⟧ʰ with suc n div 2
... | Euclidean✓ (suc q) 0 refl r<m = ⟦ suc q ⇑ downward lemma₁ ⟧ʰ 0ᵇ
... | Euclidean✓ zero 1 refl r<m = 𝕓1ᵇ
... | Euclidean✓ (suc q) 1 refl r<m = ⟦ suc q ⇑ downward lemma₂ ⟧ʰ 1ᵇ

⟦_⇑⟧⁺ : ℕ⁺ → 𝔹⁺
⟦ ℕ+ n ⇑⟧⁺ = ⟦ suc n ⇑ <-well-founded ⟧ʰ

⟦_⇑⟧ : ℕ → 𝔹
⟦ zero ⇑⟧ = 𝕓0ᵇ
⟦ suc n ⇑⟧ = + ⟦ ℕ+ n ⇑⟧⁺

ℕ→𝔹→ℕ : ∀ n → ⟦ ⟦ n ⇑⟧ ⇓⟧ ≡ n
ℕ→𝔹→ℕ zero = refl
ℕ→𝔹→ℕ (suc n) = ℕ⁺→𝔹⁺→ℕ (suc n) <-well-founded
  where
  ℕ⁺→𝔹⁺→ℕ : ∀ (n : ℕ) (rec : Acc _<_ n) {≢0 : False (n ≟ 0)} → ⟦ ⟦ n ⇑ rec ⟧ʰ {≢0} ⇓⟧⁺ ≡ n
  ℕ⁺→𝔹⁺→ℕ (suc n) (acc downward) with suc n div 2
  ... | Euclidean✓ (suc q) 0 refl r<m rewrite ℕ⁺→𝔹⁺→ℕ (suc q) (downward lemma₁) {tt} = ∀⟨ q ∷ [] ⟩
  ... | Euclidean✓ zero 1 refl r<m = refl
  ... | Euclidean✓ (suc q) 1 refl r<m rewrite ℕ⁺→𝔹⁺→ℕ (suc q) (downward lemma₂) {tt} = ∀⟨ q ∷ [] ⟩

⌈log₂_⌉⁺ : 𝔹⁺ → ℕ
⌈log₂ 𝕓1ᵇ ⌉⁺ = 1
⌈log₂ (b 0ᵇ) ⌉⁺ = 1 + ⌈log₂ b ⌉⁺
⌈log₂ (b 1ᵇ) ⌉⁺ = 1 + ⌈log₂ b ⌉⁺

⌈log₂_⌉ : 𝔹 → ℕ
⌈log₂ 𝕓0ᵇ ⌉ = 0
⌈log₂ + b ⌉ = ⌈log₂ b ⌉⁺

⌊_/2⌋⁺ : 𝔹⁺ → 𝔹⁺
⌊ 𝕓1ᵇ /2⌋⁺ = 𝕓1ᵇ
⌊ b 0ᵇ /2⌋⁺ = b
⌊ b 1ᵇ /2⌋⁺ = b

⌊_/2⌋ : 𝔹 → 𝔹
⌊ 𝕓0ᵇ /2⌋ = 𝕓0ᵇ
⌊ + b /2⌋ = + ⌊ b /2⌋⁺

-- _+ᵇ_ : 𝔹 → 𝔹 → 𝔹
-- n +ᵇ m = ⟦ ⟦ n ⇓⟧ + ⟦ m ⇓⟧ ⇑⟧

-- -- data Bit : Set where
-- --   0𝑏 : Bit
-- --   1𝑏 : Bit

-- -- _+ᵇ⁺_ : 𝔹⁺ → 𝔹⁺ → 𝔹⁺
-- -- n +ᵇ⁺ m = ⟦ ⟦ n ⇓⟧⁺ ⇑⟧⁺
--   -- where
--   -- loop : Bit → 𝔹⁺ → 𝔹⁺ → 𝔹⁺
--   -- loop carry x y = ?

-- -- unique⁺ : ∀ x y → ⟦ x ⇓⟧⁺ ≡ ⟦ y ⇓⟧⁺ → x ≡ y
-- -- unique⁺ 1ᵇ 1ᵇ p = refl
-- -- unique⁺ 1ᵇ (y 0ᵇ) p = {!!}
-- -- unique⁺ 1ᵇ (y 1ᵇ) p = {!!}
-- -- unique⁺ (x 0ᵇ) 1ᵇ p = {!!}
-- -- unique⁺ (x 0ᵇ) (y 0ᵇ) p = {!!}
-- -- unique⁺ (x 0ᵇ) (y 1ᵇ) p = {!!}
-- -- unique⁺ (x 1ᵇ) y p = {!!}

-- -- unique : ∀ x y → ⟦ x ⇓⟧ ≡ ⟦ y ⇓⟧ → x ≡ y
-- -- unique 𝕓0ᵇ 𝕓0ᵇ p = refl
-- -- unique 𝕓0ᵇ (𝕓 y) p = {!!}
-- -- unique (𝕓 x) 𝕓0ᵇ p = {!!}
-- -- unique (𝕓 x) (𝕓 y) p = {!!}

module Test where
  eval-unit₁ : ⟦ + 𝕓1ᵇ 0ᵇ 1ᵇ 0ᵇ ⇓⟧ ≡ 10
  eval-unit₁ = refl

  log-unit₁ : ⌈log₂ ⟦ 15 ⇑⟧ ⌉ ≡ 4
  log-unit₁ = refl

max_stars_repo_name: mckeankylej/thesis

max_issues_repo_name: mckeankylej/thesis

max_forks_repo_name: mckeankylej/thesis


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
open import LogicalFormulae
open import Sets.EquivalenceRelations
open import Setoids.Setoids

module Setoids.Algebra.Lemmas {a b : _} {A : Set a} (S : Setoid {a} {b} A) where

open Setoid S
open Equivalence eq
open import Setoids.Subset S
open import Setoids.Equality S
open import Setoids.Intersection.Definition S
open import Setoids.Union.Definition S

intersectionAndUnion : {c d e : _} {pred1 : A → Set c} {pred2 : A → Set d} {pred3 : A → Set e} → (s1 : subset pred1) (s2 : subset pred2) (s3 : subset pred3) → intersection s1 (union s2 s3) =S union (intersection s1 s2) (intersection s1 s3)
intersectionAndUnion s1 s2 s3 x = ans1 ,, ans2
  where
    ans1 : _
    ans1 (fst ,, inl x) = inl (fst ,, x)
    ans1 (fst ,, inr x) = inr (fst ,, x)
    ans2 : _
    ans2 (inl x) = _&&_.fst x ,, inl (_&&_.snd x)
    ans2 (inr x) = _&&_.fst x ,, inr (_&&_.snd x)


text:
-- {-# OPTIONS -v tc:30 #-}
-- Andreas, 2016-07-19, issue #2102

-- An abstract definition in a where block should not
-- stop metas of parent function to be solved!

test : _
test = Set  -- WAS: yellow
  where
  abstract def = Set

-- should succeed

test1 = Set
  module M where
  abstract def = Set

-- Similar situation

mutual
  test2 : _
  abstract def = Set
  test2 = Set

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.Groups.Wedge where

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure
open import Cubical.ZCohomology.Properties
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Function
open import Cubical.Foundations.GroupoidLaws
open import Cubical.HITs.Wedge
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; rec2 to pRec2 ; elim to sElim ; elim2 to sElim2 ; map to sMap)
open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; ∣_∣ to ∣_∣₁)
open import Cubical.HITs.Truncation renaming (elim to trElim ; rec to trRec ; elim2 to trElim2)
open import Cubical.Data.Nat
open import Cubical.Algebra.Group

open import Cubical.ZCohomology.Groups.Unit
open import Cubical.ZCohomology.Groups.Sn

open import Cubical.HITs.Pushout
open import Cubical.Data.Sigma

open import Cubical.Foundations.Isomorphism
open import Cubical.Homotopy.Connected
open import Cubical.HITs.Susp
open import Cubical.HITs.S1
open import Cubical.HITs.Sn
open import Cubical.Foundations.Equiv

open GroupIso renaming (map to map')
open GroupHom

{-
This module proves that Hⁿ(A ⋁ B) ≅ Hⁿ(A) × Hⁿ(B) for n ≥ 1 directly (rather than by means of Mayer-Vietoris).

Proof sketch:

Any ∣ f ∣₂ ∈ Hⁿ(A ⋁ B) is uniquely characterised by a pair of functions
  f₁ : A → Kₙ
  f₂ : B → Kₙ
together with a path
  p : f₁ (pt A) ≡ f₂ (pt B)

The map F : Hⁿ(A ⋁ B) → Hⁿ(A) × Hⁿ(B) simply forgets about p, i.e.:
  F(∣ f ∣₂) := (∣ f₁ ∣₂ , ∣ f₂ ∣₂)

The construction of its inverse is defined by
  F⁻(∣ f₁ ∣₂ , ∣ f₂ ∣₂) := ∣ f₁∨f₂ ∣₂
  where
  f₁∨f₂ : A ⋁ B → Kₙ is defined inductively by
  f₁∨f₂ (inl x) := f₁ x + f₂ (pt B)
  f₁∨f₂ (inr x) := f₂ x + f₁ (pt B)
  cong f₁∨f₂ (push tt) := "f₁ (pt A) + f₂ (pt B) =(commutativity) f₂ (pt B) + f₁ (pt A)"
  (this is the map wedgeFun⁻ below)
  Note that the cong-case above reduces to refl when f₁ (pt A) := f₂ (pt B) := 0

The fact that F and F⁻ cancel out is a proposition and we may thus assume for any
  ∣ f ∣₂ ∈ Hⁿ(A ⋁ B) and its corresponding f₁ that
  f₁ (pt A) = f₂ (pt B) = 0                (*)
  and
  f (inl (pt A)) = 0                       (**)

The fact that F(F⁻(∣ f₁ ∣₂ , ∣ f₂ ∣₂)) = ∣ f₁ ∣₂ , ∣ f₂ ∣₂) follows immediately from (*)

The other way is slightly trickier. We need to construct paths
  Pₗ : f (inl (x)) + f (inr (pt B)) ---> f (inl (x))
  Pᵣ  : f (inr (x)) + f (inl (pt A)) ---> f (inr (x))

Together with a filler of the following square

     cong f (push tt)
    ----------------->
   ^                  ^
   |                  |
   |                  |
Pₗ |                  | Pᵣ
   |                  |
   |                  |
   |                  |
    ----------------->
            Q
where Q is commutativity proof f (inl (pt A)) + f (inr (pt B)) = f (inr (pt B)) + f (inl (pt A))

The square is filled by first constructing Pₗ by
  f (inl (x)) + f (inr (pt B))    ---[cong f (push tt)⁻¹]--->
  f (inl (x)) + f (inl (pt A))    ---[(**)]--->
  f (inl (x)) + 0                 ---[right-unit]--->
  f (inl (x))

and then Pᵣ by
  f (inr (x)) + f (inl (pt A))    ---[(**)]--->
  f (inr (x)) + 0                 ---[right-unit]--->
  f (inr (x))

and finally by using the fact that the group laws for Kₙ are refl at its base point.
-}

module _ {ℓ ℓ'} (A : Pointed ℓ) (B : Pointed ℓ') where

  private
    wedgeFun⁻ : ∀ n → (f : typ A → coHomK (suc n)) (g : typ B → coHomK (suc n))
            → ((A ⋁ B) → coHomK (suc n))
    wedgeFun⁻ n f g (inl x) = f x +ₖ g (pt B)
    wedgeFun⁻ n f g (inr x) = g x +ₖ f (pt A)
    wedgeFun⁻ n f g (push a i) = commₖ (suc n) (f (pt A)) (g (pt B)) i

  Hⁿ-⋁ : (n : ℕ) → GroupIso (coHomGr (suc n) (A ⋁ B)) (×coHomGr (suc n) (typ A) (typ B))
  fun (map' (Hⁿ-⋁ zero)) =
    sElim (λ _ → isSet× setTruncIsSet setTruncIsSet)
           λ f → ∣ (λ x → f (inl x)) ∣₂ , ∣ (λ x → f (inr x)) ∣₂
  isHom (map' (Hⁿ-⋁ zero)) =
    sElim2 (λ _ _ → isOfHLevelPath 2 (isSet× setTruncIsSet setTruncIsSet) _ _)
            λ _ _ → refl
  inv (Hⁿ-⋁ zero) = uncurry (sElim2 (λ _ _ → setTruncIsSet)
                             λ f g → ∣ wedgeFun⁻ 0 f g ∣₂)
  rightInv (Hⁿ-⋁ zero) =
    uncurry
    (coHomPointedElim _ (pt A) (λ _ → isPropΠ λ _ → isSet× setTruncIsSet setTruncIsSet _ _)
      λ f fId → coHomPointedElim _ (pt B) (λ _ → isSet× setTruncIsSet setTruncIsSet _ _)
        λ g gId → ΣPathP (cong ∣_∣₂ (funExt (λ x → cong (f x +ₖ_) gId ∙ rUnitₖ 1 (f x))) ,
                           cong ∣_∣₂ (funExt (λ x → cong (g x +ₖ_) fId ∙ rUnitₖ 1 (g x)))))
  leftInv (Hⁿ-⋁ zero) =
    sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
      (λ f → pRec (setTruncIsSet _ _)
                   (λ fId → cong ∣_∣₂ (sym fId))
                   (helper f _ refl))
    where
    helper : (f : A ⋁ B → coHomK 1) (x : coHomK 1)
          → f (inl (pt A)) ≡ x
          → ∥ f ≡ wedgeFun⁻ 0 (λ x → f (inl x)) (λ x → f (inr x)) ∥
    helper f =
      trElim (λ _ → isProp→isOfHLevelSuc 2 (isPropΠ λ _ → propTruncIsProp))
        (sphereElim 0 (λ _ → isPropΠ λ _ → propTruncIsProp)
          λ inlId → (∣ funExt (λ { (inl x) → sym (rUnitₖ 1 (f (inl x)))
                                           ∙∙ cong ((f (inl x)) +ₖ_) (sym inlId)
                                           ∙∙ cong ((f (inl x)) +ₖ_) (cong f (push tt))
                                 ; (inr x) → sym (rUnitₖ 1 (f (inr x)))
                                            ∙ cong ((f (inr x)) +ₖ_) (sym inlId)
                                 ; (push tt i) j → cheating (f (inl (pt A))) (sym (inlId))
                                                             (f (inr (pt B)))
                                                             (cong f (push tt)) j i}) ∣₁))
      where
      cheating : (x : coHomK 1) (r : ∣ base ∣ ≡ x) (y : coHomK 1) (p : x ≡ y)
             → PathP (λ j → ((sym (rUnitₖ 1 x) ∙∙ cong (x +ₖ_) r ∙∙ cong (x +ₖ_) p)) j
                             ≡ (sym (rUnitₖ 1 y) ∙ cong (y +ₖ_) r) j)
                       p (commₖ 1 x y)
      cheating x = J (λ x r → (y : coHomK 1) (p : x ≡ y)
                            → PathP (λ j → ((sym (rUnitₖ 1 x) ∙∙ cong (x +ₖ_) r ∙∙ cong (x +ₖ_) p)) j
                                            ≡ (sym (rUnitₖ 1 y) ∙ cong (y +ₖ_) r) j)
                                     p (commₖ 1 x y))
                     λ y → J (λ y p → PathP (λ j → ((sym (rUnitₖ 1 ∣ base ∣) ∙∙ refl ∙∙ cong (∣ base ∣ +ₖ_) p)) j
                                                     ≡ (sym (rUnitₖ 1 y) ∙ refl) j)
                                              p (commₖ 1 ∣ base ∣ y))
                             λ i j → comp (λ _ → hLevelTrunc 3 S¹)
                                           (λ k → λ {(i = i0) → ∣ base ∣
                                                    ; (i = i1) → ∣ base ∣
                                                    ; (j = i0) → (rUnit (λ _ → ∣ base ∣) k) i
                                                    ; (j = i1) → (rUnit (λ _ → ∣ base ∣) k) i})
                                           ∣ base ∣
  fun (map' (Hⁿ-⋁ (suc n))) =
    sElim (λ _ → isSet× setTruncIsSet setTruncIsSet)
           λ f → ∣ (λ x → f (inl x)) ∣₂ , ∣ (λ x → f (inr x)) ∣₂
  isHom (map' (Hⁿ-⋁ (suc n))) =
    sElim2 (λ _ _ → isOfHLevelPath 2 (isSet× setTruncIsSet setTruncIsSet) _ _)
            λ _ _ → refl
  inv (Hⁿ-⋁ (suc n)) =
    uncurry (sElim2 (λ _ _ → setTruncIsSet)
                     λ f g → ∣ wedgeFun⁻ (suc n) f g ∣₂)
  rightInv (Hⁿ-⋁ (suc n)) =
   uncurry
    (coHomPointedElim _ (pt A) (λ _ → isPropΠ λ _ → isSet× setTruncIsSet setTruncIsSet _ _)
      λ f fId → coHomPointedElim _ (pt B) (λ _ → isSet× setTruncIsSet setTruncIsSet _ _)
        λ g gId → ΣPathP (cong ∣_∣₂ (funExt (λ x → cong (f x +ₖ_) gId ∙ rUnitₖ (2 + n) (f x))) ,
                           cong ∣_∣₂ (funExt (λ x → cong (g x +ₖ_) fId ∙ rUnitₖ (2 + n) (g x)))))
  leftInv (Hⁿ-⋁ (suc n)) =
    sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
      (λ f → pRec (setTruncIsSet _ _)
                   (λ fId → cong ∣_∣₂ (sym fId))
                   (helper f _ refl))
    where
    helper : (f : A ⋁ B → coHomK (2 + n)) (x : coHomK (2 + n))
          → f (inl (pt A)) ≡ x
          → ∥ f ≡ wedgeFun⁻ (suc n) (λ x → f (inl x)) (λ x → f (inr x)) ∥
    helper f =
      trElim (λ _ → isProp→isOfHLevelSuc (3 + n) (isPropΠ λ _ → propTruncIsProp))
        (sphereToPropElim (suc n) (λ _ → isPropΠ λ _ → propTruncIsProp)
          λ inlId → (∣ funExt (λ { (inl x) → sym (rUnitₖ (2 + n) (f (inl x)))
                                           ∙∙ cong ((f (inl x)) +ₖ_) (sym inlId)
                                           ∙∙ cong ((f (inl x)) +ₖ_) (cong f (push tt))
                                 ; (inr x) → sym (rUnitₖ (2 + n) (f (inr x)))
                                            ∙ cong ((f (inr x)) +ₖ_) (sym inlId)
                                 ; (push tt i) j → cheating (f (inl (pt A))) (sym (inlId))
                                                             (f (inr (pt B))) (cong f (push tt)) j i}) ∣₁))
      where
      cheating : (x : coHomK (2 + n)) (r : ∣ north ∣ ≡ x) (y : coHomK (2 + n)) (p : x ≡ y)
             → PathP (λ j → ((sym (rUnitₖ (2 + n) x) ∙∙ cong (x +ₖ_) r ∙∙ cong (x +ₖ_) p)) j
                             ≡ (sym (rUnitₖ (2 + n) y) ∙ cong (y +ₖ_) r) j)
                       p (commₖ (2 + n) x y)
      cheating x =
         J (λ x r → (y : coHomK (2 + n)) (p : x ≡ y)
                            → PathP (λ j → ((sym (rUnitₖ (2 + n) x) ∙∙ cong (x +ₖ_) r ∙∙ cong (x +ₖ_) p)) j
                                            ≡ (sym (rUnitₖ (2 + n) y) ∙ cong (y +ₖ_) r) j)
                                     p (commₖ (2 + n) x y))
                     doubleCheating
        where
        doubleCheating : (y : coHomK (2 + n)) → (p : ∣ north ∣ ≡ y)
                      → PathP (λ j → ((refl ∙∙ refl ∙∙ cong (∣ north ∣ +ₖ_) p)) j
                                      ≡ (sym (rUnitₖ (2 + n) y) ∙ refl) j)
                               p
                               (commₖ (2 + n) ∣ north ∣ y)
        doubleCheating y =
          J (λ y p → PathP (λ j → ((refl ∙∙ refl ∙∙ cong (∣ north ∣ +ₖ_) p)) j
                                      ≡ (sym (rUnitₖ (2 + n) y) ∙ refl) j)
                               p
                               (commₖ (2 + n) ∣ north ∣ y))
            λ i j → comp (λ _ → coHomK (2 + n))
                          (λ k → λ {(i = i0) → ∣ north ∣
                                   ; (i = i1) → commₖ-base (2 + n) (~ k) j
                                   ; (j = i0) → rUnit (λ _ → ∣ north ∣) k i
                                   ; (j = i1) → rUnit (λ _ → ∣ north ∣) k i})
                          ∣ north ∣

  wedgeConnected : ((x : typ A) → ∥ pt A ≡ x ∥) → ((x : typ B) → ∥ pt B ≡ x ∥) → (x : A ⋁ B) → ∥ inl (pt A) ≡ x ∥
  wedgeConnected conA conB =
    PushoutToProp (λ _ → propTruncIsProp)
                  (λ a → pRec propTruncIsProp (λ p → ∣ cong inl p ∣₁) (conA a))
                   λ b → pRec propTruncIsProp (λ p → ∣ push tt ∙ cong inr p ∣₁) (conB b)

open import Cubical.Data.Int
open import Cubical.Data.Empty renaming (rec to ⊥-rec)
open import Cubical.Data.Bool
open import Cubical.Data.Int renaming (+-comm to +-commℤ ; _+_ to _+ℤ_)

even : Int → Bool
even (pos zero) = true
even (pos (suc zero)) = false
even (pos (suc (suc n))) = even (pos n)
even (negsuc zero) = false
even (negsuc (suc n)) = even (pos n)

open import Cubical.Data.Sum

even-2 : (x : Int) → even (-2 +ℤ x) ≡ even x
even-2 (pos zero) = refl
even-2 (pos (suc zero)) = refl
even-2 (pos (suc (suc n))) =
    cong even (cong sucInt (sucInt+pos _ _)
            ∙∙ sucInt+pos _ _
            ∙∙ +-commℤ 0 (pos n))
  ∙ noClueWhy n
  where
  noClueWhy : (n : ℕ) → even (pos n) ≡ even (pos n)
  noClueWhy n = refl
even-2 (negsuc zero) = refl
even-2 (negsuc (suc n)) =
    cong even (predInt+negsuc n _
             ∙ +-commℤ -3 (negsuc n))
  ∙ noClueWhy n
  where
  noClueWhy : (n : ℕ) → even (negsuc (suc (suc (suc n)))) ≡ even (pos n)
  noClueWhy n = refl

test3 : (p : 0ₖ 1 ≡ 0ₖ 1) → even (ΩKn+1→Kn 0 (transport (λ i → ∣ (loop ∙ loop) i ∣ ≡ 0ₖ 1) p)) ≡ even (ΩKn+1→Kn 0 p)
test3 p = cong even (cong (ΩKn+1→Kn 0) (cong (transport (λ i → ∣ (loop ∙ loop) i ∣ ≡ 0ₖ 1)) (lUnit p)))
      ∙∙ cong even (cong (ΩKn+1→Kn 0) λ j → transp (λ i → ∣ (loop ∙ loop) (i ∨ j) ∣ ≡ 0ₖ 1) j ((λ i → ∣ (loop ∙ loop) (~ i ∧ j) ∣) ∙ p))
      ∙∙ cong even (ΩKn+1→Kn-hom 0 (sym (cong ∣_∣ (loop ∙ loop))) p)
       ∙ even-2 (ΩKn+1→Kn 0 p)

test2 :  Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 → Bool
test2 = uncurry (trElim (λ _ → isGroupoidΠ λ _ → isOfHLevelSuc 2 isSetBool)
                        λ {base p → even (ΩKn+1→Kn 0 p)
                        ; (loop i) p → hcomp (λ k → λ { (i = i0) → test3 p k
                                                        ; (i = i1) → even (ΩKn+1→Kn 0 p)})
                        (even (ΩKn+1→Kn 0 (transp (λ j → ∣ (loop ∙ loop) (i ∨ j) ∣ ≡ 0ₖ 1) i
                                                      p)))})

*' : (x y : coHomK 1) (p : x +ₖ x ≡ 0ₖ 1) (q : y +ₖ y ≡ 0ₖ 1) → ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂
*' =
  trElim2 (λ _ _ → isGroupoidΠ2 λ _ _ → isOfHLevelSuc 2 setTruncIsSet)
          (wedgeConSn _ _
            (λ _ _ → isSetΠ2 λ _ _ → setTruncIsSet)
            (λ x p q → ∣ ∣ x ∣ , cong₂ _+ₖ_ p q ∣₂)
            (λ y p q → ∣ ∣ y ∣ , sym (rUnitₖ 1 (∣ y ∣ +ₖ ∣ y ∣)) ∙ cong₂ _+ₖ_ p q ∣₂)
            (funExt λ p → funExt λ q → cong ∣_∣₂ (ΣPathP (refl , (sym (lUnit _))))) .fst)

_*_ : ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂ → ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂ → ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂
_*_ = sRec (isSetΠ (λ _ → setTruncIsSet)) λ a → sRec setTruncIsSet λ b → *' (fst a) (fst b) (snd a) (snd b)
*=∙ : (p q : 0ₖ 1 ≡ 0ₖ 1) → ∣ 0ₖ 1 , p ∣₂ * ∣ 0ₖ 1 , q ∣₂ ≡ ∣ 0ₖ 1 , p ∙ q ∣₂
*=∙ p q = cong ∣_∣₂ (ΣPathP (refl , sym (∙≡+₁ p q)))

help : (n : ℕ) → even (pos (suc n)) ≡ true → even (negsuc n) ≡ true
help zero p = ⊥-rec (true≢false (sym p))
help (suc n) p = p

help2 : (n : ℕ) → even (pos (suc n)) ≡ false → even (negsuc n) ≡ false
help2 zero p = refl
help2 (suc n) p = p

evenCharac : (x : Int) → even x ≡ true
    → Path ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂
            ∣ (0ₖ 1 , Kn→ΩKn+1 0 x) ∣₂
            ∣ (0ₖ 1 , refl) ∣₂
evenCharac (pos zero) iseven i = ∣ (0ₖ 1) , (rUnit refl (~ i)) ∣₂
evenCharac (pos (suc zero)) iseven = ⊥-rec (true≢false (sym iseven))
evenCharac (pos (suc (suc zero))) iseven = cong ∣_∣₂ ((λ i → 0ₖ 1 , rUnit (cong ∣_∣ ((lUnit loop (~ i)) ∙ loop)) (~ i))
                                           ∙  (ΣPathP (cong ∣_∣ loop , λ i j → ∣ (loop ∙ loop) (i ∨ j) ∣)))
evenCharac (pos (suc (suc (suc n)))) iseven =
     (λ i → ∣ 0ₖ 1 , Kn→ΩKn+1-hom 0 (pos (suc n)) 2 i ∣₂)
  ∙∙ sym (*=∙ (Kn→ΩKn+1 0 (pos (suc n))) (Kn→ΩKn+1 0 (pos 2)))
  ∙∙ (cong₂ _*_ (evenCharac (pos (suc n)) iseven) (evenCharac 2 refl))

evenCharac (negsuc zero) iseven = ⊥-rec (true≢false (sym iseven))
evenCharac (negsuc (suc zero)) iseven =
  cong ∣_∣₂ ((λ i → 0ₖ 1 , λ i₁ → hfill (doubleComp-faces (λ i₂ → ∣ base ∣) (λ _ → ∣ base ∣) i₁)
                                         (inS ∣ compPath≡compPath' (sym loop) (sym loop) i i₁ ∣) (~ i))
                                ∙ ΣPathP ((cong ∣_∣ (sym loop)) , λ i j → ∣ (sym loop ∙' sym loop) (i ∨ j) ∣))
evenCharac (negsuc (suc (suc n))) iseven =
     cong ∣_∣₂ (λ i → 0ₖ 1 , Kn→ΩKn+1-hom 0 (negsuc n) -2 i)
  ∙∙ sym (*=∙ (Kn→ΩKn+1 0 (negsuc n)) (Kn→ΩKn+1 0 -2))
  ∙∙ cong₂ _*_ (evenCharac (negsuc n) (help n iseven)) (evenCharac -2 refl) -- i

oddCharac : (x : Int) → even x ≡ false
    → Path ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂
            ∣ (0ₖ 1 , Kn→ΩKn+1 0 x) ∣₂
            ∣ (0ₖ 1 , cong ∣_∣ loop) ∣₂
oddCharac (pos zero) isOdd = ⊥-rec (true≢false isOdd)
oddCharac (pos (suc zero)) isOdd i =
  ∣ (0ₖ 1 , λ j → hfill (doubleComp-faces (λ i₂ → ∣ base ∣) (λ _ → ∣ base ∣) j)
                         (inS ∣ lUnit loop (~ i) j ∣) (~ i)) ∣₂
oddCharac (pos (suc (suc n))) isOdd =
  (λ i → ∣ 0ₖ 1 , Kn→ΩKn+1-hom 0 (pos n) 2 i ∣₂)
  ∙∙ sym (*=∙ (Kn→ΩKn+1 0 (pos n)) (Kn→ΩKn+1 0 2))
  ∙∙ cong₂ _*_ (oddCharac (pos n) isOdd) (evenCharac 2 refl)
oddCharac (negsuc zero) isOdd =
    cong ∣_∣₂ ((λ i → 0ₖ 1 , rUnit (sym (cong ∣_∣ loop)) (~ i))
  ∙ ΣPathP (cong ∣_∣ (sym loop) , λ i j → ∣ hcomp (λ k → λ { (i = i0) → loop (~ j ∧ k)
                                                           ; (i = i1) → loop j
                                                           ; (j = i1) → base})
                                                 (loop (j ∨ ~ i)) ∣))
oddCharac (negsuc (suc zero)) isOdd = ⊥-rec (true≢false isOdd)
oddCharac (negsuc (suc (suc n))) isOdd =
     cong ∣_∣₂ (λ i → 0ₖ 1 , Kn→ΩKn+1-hom 0 (negsuc n) -2 i)
  ∙∙ sym (*=∙ (Kn→ΩKn+1 0 (negsuc n)) (Kn→ΩKn+1 0 -2))
  ∙∙ cong₂ _*_ (oddCharac (negsuc n) (help2 n isOdd)) (evenCharac (negsuc 1) refl)

map⁻ : Bool → ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂
map⁻ false = ∣ 0ₖ 1 , cong ∣_∣ loop ∣₂
map⁻ true = ∣ 0ₖ 1 , refl ∣₂

testIso : Iso ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂ Bool
Iso.fun testIso = sRec isSetBool test2
Iso.inv testIso = map⁻
Iso.rightInv testIso false = refl
Iso.rightInv testIso true = refl
Iso.leftInv testIso =
  sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
        (uncurry (trElim
          (λ _ → isGroupoidΠ λ _ → isOfHLevelPlus {n = 1} 2 (setTruncIsSet _ _))
          (toPropElim (λ _ → isPropΠ (λ _ → setTruncIsSet _ _))
          (λ p → path p (even (ΩKn+1→Kn 0 p)) refl))))
  where
  path : (p : 0ₖ 1 ≡ 0ₖ 1) (b : Bool) → (even (ΩKn+1→Kn 0 p) ≡ b) → map⁻ (test2 (∣ base ∣ , p)) ≡ ∣ ∣ base ∣ , p ∣₂
  path p false q =
       (cong map⁻ q)
    ∙∙ sym (oddCharac (ΩKn+1→Kn 0 p) q)
    ∙∙ cong ∣_∣₂ λ i → 0ₖ 1 , Iso.rightInv (Iso-Kn-ΩKn+1 0) p i
  path p true q =
       cong map⁻ q
    ∙∙ sym (evenCharac (ΩKn+1→Kn 0 p) q)
    ∙∙ cong ∣_∣₂ λ i → 0ₖ 1 , Iso.rightInv (Iso-Kn-ΩKn+1 0) p i

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


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

-- This module defines a data type for balanced strings of parentheses,
-- which is isomorphic to binary trees.

module Data.Dyck.Rose where

open import Prelude
open import Data.Nat using (_+_)
open import Data.Vec.Iterated using (Vec; _∷_; []; foldlN; head)
open import Data.Tree.Rose
open import Data.List

private
  variable
    n : ℕ

--------------------------------------------------------------------------------
-- Programs: definition and associated functions
--------------------------------------------------------------------------------

data Prog (A : Type a) : ℕ → Type a where
  halt : Prog A 1
  pull : Prog A (1 + n) → Prog A n
  push : A → Prog A (1 + n) → Prog A (2 + n)

--------------------------------------------------------------------------------
-- Conversion from a Prog to a Tree
--------------------------------------------------------------------------------

prog→tree⊙ : Prog A n → Vec (Forest A) n → Forest A
prog→tree⊙ halt        (v ∷ [])       = v
prog→tree⊙ (pull   is) st             = prog→tree⊙ is ([] ∷ st)
prog→tree⊙ (push v is) (t₁ ∷ t₂ ∷ st) = prog→tree⊙ is (((v & t₂) ∷ t₁) ∷ st)

prog→tree : Prog A zero → Forest A
prog→tree ds = prog→tree⊙ ds []

--------------------------------------------------------------------------------
-- Conversion from a Tree to a Prog
--------------------------------------------------------------------------------

tree→prog⊙ : Forest A → Prog A (suc n) → Prog A n
tree→prog⊙ []              = pull
tree→prog⊙ ((t & ts) ∷ xs) = tree→prog⊙ ts ∘ tree→prog⊙ xs ∘ push t

tree→prog : Forest A → Prog A zero
tree→prog tr = tree→prog⊙ tr halt

--------------------------------------------------------------------------------
-- Proof of isomorphism
--------------------------------------------------------------------------------

tree→prog→tree⊙ : (e : Forest A) (is : Prog A (1 + n)) (st : Vec (Forest A) n) →
  prog→tree⊙ (tree→prog⊙ e is) st ≡ prog→tree⊙ is (e ∷ st)
tree→prog→tree⊙ []              is st = refl
tree→prog→tree⊙ ((t & ts) ∷ xs) is st =
  tree→prog→tree⊙ ts _ st ; tree→prog→tree⊙ xs (push t is) (ts ∷ st)

tree→prog→tree : (e : Forest A) → prog→tree (tree→prog e) ≡ e
tree→prog→tree e = tree→prog→tree⊙ e halt []

prog→tree→prog⊙ : (is : Prog A n) (st : Vec (Forest A) n) →
 tree→prog (prog→tree⊙ is st) ≡ foldlN (Prog A) tree→prog⊙ is st
prog→tree→prog⊙ halt        st = refl
prog→tree→prog⊙ (pull   is) st = prog→tree→prog⊙ is ([] ∷ st)
prog→tree→prog⊙ (push x is) (t₁ ∷ t₂ ∷ st) =
  prog→tree→prog⊙ is (((x & t₂) ∷ t₁) ∷ st)

prog→tree→prog : (is : Prog A 0) → tree→prog (prog→tree is) ≡ is
prog→tree→prog is = prog→tree→prog⊙ is []

prog-iso : Prog A zero ⇔ Forest A
prog-iso .fun = prog→tree
prog-iso .inv = tree→prog
prog-iso .rightInv = tree→prog→tree
prog-iso .leftInv  = prog→tree→prog

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

module Data.Sum.Properties where

open import Prelude
open import Data.Sum
open import Data.Bool

sumAsSigma : A ⊎ B ≃ Σ[ x ⦂ Bool ] (if x then A else B)
sumAsSigma = isoToEquiv $
  iso
    (either (true ,_) (false ,_))
    (uncurry (bool inr inl))
    (λ { (false , _) → refl ; (true , _) → refl})
    (λ { (inl _) → refl ; (inr _) → refl})

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper