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 renaming (assoc to assoc∙)
open import Cubical.HITs.Wedge
open import Cubical.Data.Int hiding (_+_)
open import Cubical.HITs.SetTruncation renaming (rec to sRec ; rec2 to sRec2 ; 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).
It also proves that Ĥⁿ(A ⋁ B) ≅ Ĥ⁰(A) × Ĥ⁰(B) (reduced groups)

Proof sketch for n ≥ 1:

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₁ (pt B) + f₂ x
  cong f₁∨f₂ (push tt) := refl
  (this is the map wedgeFun⁻ below)

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ₗ(x) : f (inl (x)) + f (inr (pt B)) ---> f (inl (x))
  Pᵣ(x)  : f (inl (pt A)) + f (inr (x)) ---> f (inr (x))

Together with a filler of the following square

           cong f (push tt)
          ----------------->
         ^                  ^
         |                  |
         |                  |
Pₗ(pr A) |                  | Pᵣ(pt B)
         |                  |
         |                  |
         |                  |
          ----------------->
                  refl

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 (inl (pt A)) + f (inr (x))    ---[(**)⁻¹]--->
  0 + f (inr (x))                 ---[left-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) = f (pt A) +ₖ g x
    wedgeFun⁻ n f g (push a i) = f (pt A) +ₖ g (pt B)

  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 ∙ lUnitₖ 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 (lUnitₖ 1 (f (inr x)))
                                            ∙ cong (_+ₖ (f (inr x))) (sym inlId)
                                 ; (push tt i) j → helper2 (f (inl (pt A))) (sym (inlId))
                                                            (f (inr (pt B))) (cong f (push tt)) j i} ) ∣₁)
      where
      helper2 : (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 (lUnitₖ 1 y) ∙ cong (_+ₖ y) r) j)
                       p refl
      helper2 x = J (λ x r → (y : coHomK 1) (p : x ≡ y)
                           → PathP (λ j → ((sym (rUnitₖ 1 x) ∙∙ cong (x +ₖ_) r ∙∙ cong (x +ₖ_) p)) j
                                           ≡ (sym (lUnitₖ 1 y) ∙ cong (_+ₖ y) r) j)
                                    p refl)
                     λ y → J (λ y p → PathP (λ j → ((sym (rUnitₖ 1 ∣ base ∣) ∙∙ refl ∙∙ cong (∣ base ∣ +ₖ_) p)) j
                                                    ≡ (sym (lUnitₖ 1 y) ∙ refl) j)
                                             p refl)
                               λ i _ → (refl ∙ (λ _ → 0ₖ 1)) i
  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 ∙ lUnitₖ (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 (lUnitₖ (2 + n) (f (inr x)))
                                            ∙ cong (_+ₖ (f (inr x))) (sym inlId)
                                 ; (push tt i) j → helper2 (f (inl (pt A))) (sym (inlId))
                                                            (f (inr (pt B))) (cong f (push tt)) j i}) ∣₁))
      where
      helper2 : (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 (lUnitₖ (2 + n) y) ∙ cong (_+ₖ y) r) j)
                      p refl
      helper2 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 (lUnitₖ (2 + n) y) ∙ cong (_+ₖ y) r) j)
                                    p refl)
                     λ y → J (λ y p → PathP (λ j → ((sym (rUnitₖ (2 + n) ∣ north ∣) ∙∙ refl ∙∙ cong (∣ north ∣ +ₖ_) p)) j
                                                    ≡ (sym (lUnitₖ (2 + n) y) ∙ refl) j)
                                             p refl)
                              λ i j → ((λ _ → ∣ north ∣) ∙ refl) i

  H⁰Red-⋁ : GroupIso (coHomRedGrDir 0 (A ⋁ B , inl (pt A)))
                      (dirProd (coHomRedGrDir 0 A) (coHomRedGrDir 0 B))
  fun (GroupIso.map H⁰Red-⋁) =
    sRec (isSet× setTruncIsSet setTruncIsSet)
         λ {(f , p) → ∣ (f ∘ inl) , p ∣₂
                     , ∣ (f ∘ inr) , cong f (sym (push tt)) ∙ p ∣₂}
  isHom (GroupIso.map H⁰Red-⋁) =
    sElim2 (λ _ _ → isOfHLevelPath 2 (isSet× setTruncIsSet setTruncIsSet) _ _)
           λ {(f , p) (g , q) → ΣPathP (cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _) refl)
                                       , cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _) refl))}
  inv H⁰Red-⋁ =
    uncurry (sRec2 setTruncIsSet
              λ {(f , p) (g , q) → ∣ (λ {(inl a) → f a
                                       ; (inr b) → g b
                                       ; (push tt i) → (p ∙ sym q) i})
                                       , p ∣₂})
  rightInv H⁰Red-⋁ =
    uncurry
      (sElim2 (λ _ _ → isOfHLevelPath 2 (isSet× setTruncIsSet setTruncIsSet) _ _)
        λ {(_ , _) (_ , _) → ΣPathP (cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _) refl)
                                    , cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _) refl))})
  leftInv H⁰Red-⋁ =
    sElim (λ _ → isOfHLevelPath 2 setTruncIsSet _ _)
      λ {(f , p) → cong ∣_∣₂ (Σ≡Prop (λ _ → isSetInt _ _)
                                 (funExt λ {(inl a) → refl
                                          ; (inr b) → refl
                                          ; (push tt i) j → (cong (p ∙_) (symDistr (cong f (sym (push tt))) p)
                                                           ∙∙ assoc∙ p (sym p) (cong f (push tt))
                                                           ∙∙ cong (_∙ (cong f (push tt))) (rCancel p)
                                                            ∙ sym (lUnit (cong f (push tt)))) j i}))}
                                          -- Alt. use isOfHLevel→isOfHLevelDep

  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)

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Consequences of a monomorphism between group-like structures
------------------------------------------------------------------------

-- See Data.Nat.Binary.Properties for examples of how this and similar
-- modules can be used to easily translate properties between types.

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

open import Algebra.Bundles
open import Algebra.Morphism.Structures
open import Relation.Binary.Core

module Algebra.Morphism.GroupMonomorphism
  {a b ℓ₁ ℓ₂} {G₁ : RawGroup a ℓ₁} {G₂ : RawGroup b ℓ₂} {⟦_⟧}
  (isGroupMonomorphism : IsGroupMonomorphism G₁ G₂ ⟦_⟧)
  where

open IsGroupMonomorphism isGroupMonomorphism
open RawGroup G₁ renaming
  (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; _⁻¹ to _⁻¹₁; ε to ε₁)
open RawGroup G₂ renaming
  (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; _⁻¹ to _⁻¹₂; ε to ε₂)

open import Algebra.Definitions
open import Algebra.Structures
open import Data.Product
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

------------------------------------------------------------------------
-- Re-export all properties of monoid monomorphisms

open import Algebra.Morphism.MonoidMonomorphism
  isMonoidMonomorphism public

------------------------------------------------------------------------
-- Properties

module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where

  open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
  open SetoidReasoning setoid

  inverseˡ : LeftInverse _≈₂_ ε₂ _⁻¹₂ _◦_ → LeftInverse _≈₁_ ε₁ _⁻¹₁  _∙_
  inverseˡ invˡ x = injective (begin
    ⟦ x ⁻¹₁ ∙ x ⟧     ≈⟨ ∙-homo (x ⁻¹₁ ) x ⟩
    ⟦ x ⁻¹₁ ⟧ ◦ ⟦ x ⟧ ≈⟨ ◦-cong (⁻¹-homo x) refl ⟩
    ⟦ x ⟧ ⁻¹₂ ◦ ⟦ x ⟧ ≈⟨ invˡ ⟦ x ⟧ ⟩
    ε₂                ≈˘⟨ ε-homo ⟩
    ⟦ ε₁ ⟧ ∎)

  inverseʳ : RightInverse _≈₂_ ε₂ _⁻¹₂ _◦_ → RightInverse _≈₁_ ε₁ _⁻¹₁  _∙_
  inverseʳ invʳ x = injective (begin
    ⟦ x ∙ x ⁻¹₁ ⟧     ≈⟨ ∙-homo x (x ⁻¹₁) ⟩
    ⟦ x ⟧ ◦ ⟦ x ⁻¹₁ ⟧ ≈⟨ ◦-cong refl (⁻¹-homo x) ⟩
    ⟦ x ⟧ ◦ ⟦ x ⟧ ⁻¹₂ ≈⟨ invʳ ⟦ x ⟧ ⟩
    ε₂                ≈˘⟨ ε-homo ⟩
    ⟦ ε₁ ⟧ ∎)

  inverse : Inverse _≈₂_ ε₂ _⁻¹₂ _◦_ → Inverse _≈₁_ ε₁ _⁻¹₁  _∙_
  inverse (invˡ , invʳ) = inverseˡ invˡ , inverseʳ invʳ

  ⁻¹-cong : Congruent₁ _≈₂_ _⁻¹₂ → Congruent₁ _≈₁_ _⁻¹₁
  ⁻¹-cong  ⁻¹-cong {x} {y} x≈y = injective (begin
    ⟦ x ⁻¹₁ ⟧ ≈⟨ ⁻¹-homo x ⟩
    ⟦ x ⟧ ⁻¹₂ ≈⟨ ⁻¹-cong (⟦⟧-cong x≈y) ⟩
    ⟦ y ⟧ ⁻¹₂ ≈˘⟨ ⁻¹-homo y ⟩
    ⟦ y ⁻¹₁ ⟧ ∎)

isGroup : IsGroup _≈₂_ _◦_ ε₂ _⁻¹₂ → IsGroup _≈₁_ _∙_ ε₁ _⁻¹₁
isGroup isGroup = record
  { isMonoid = isMonoid G.isMonoid
  ; inverse  = inverse  G.isMagma G.inverse
  ; ⁻¹-cong  = ⁻¹-cong  G.isMagma G.⁻¹-cong
  } where module G = IsGroup isGroup

isAbelianGroup : IsAbelianGroup _≈₂_ _◦_ ε₂ _⁻¹₂ → IsAbelianGroup _≈₁_ _∙_ ε₁ _⁻¹₁
isAbelianGroup isAbelianGroup = record
  { isGroup = isGroup G.isGroup
  ; comm    = comm G.isMagma G.comm
  } where module G = IsAbelianGroup isAbelianGroup

ext: agda


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

module Loop.Bundles where

open import Algebra.Core
open import Relation.Binary
open import Level
open import Loop.Structures
open import Algebra.Bundles
open import Algebra.Structures

record LeftBolLoop c ℓ : Set (suc (c ⊔ ℓ)) where
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    _\\_    : Op₂ Carrier
    _//_    : Op₂ Carrier
    ε       : Carrier
    isLeftBolLoop : IsLeftBolLoop  _≈_ _∙_ _\\_ _//_ ε

  open IsLeftBolLoop isLeftBolLoop public

  loop : Loop _ _
  loop = record { isLoop = isLoop }

  open Loop loop public
    using (quasigroup)

record RightBolLoop c ℓ : Set (suc (c ⊔ ℓ)) where
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    _\\_    : Op₂ Carrier
    _//_    : Op₂ Carrier
    ε       : Carrier
    isRightBolLoop : IsRightBolLoop  _≈_ _∙_ _\\_ _//_ ε

  open IsRightBolLoop isRightBolLoop public

  loop : Loop _ _
  loop = record { isLoop = isLoop }

  open Loop loop public
    using (quasigroup)

record MoufangLoop c ℓ : Set (suc (c ⊔ ℓ)) where
  field
    Carrier : Set c
    _≈_     : Rel Carrier ℓ
    _∙_     : Op₂ Carrier
    _\\_    : Op₂ Carrier
    _//_    : Op₂ Carrier
    ε       : Carrier
    isMoufangLoop : IsMoufangLoop  _≈_ _∙_ _\\_ _//_ ε

  open IsMoufangLoop isMoufangLoop public

  loop : Loop _ _
  loop = record { isLoop = isLoop }

  open Loop loop public
    using (quasigroup)


text:
------------------------------------------------------------------------
-- Support for reflection
------------------------------------------------------------------------

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

open import Equality

module TC-monad
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

import Agda.Builtin.Bool as B
open import Agda.Builtin.Char
open import Agda.Builtin.Float
import Agda.Builtin.Reflection
open import Agda.Builtin.Strict
open import Agda.Builtin.String

open import Logical-equivalence using (_⇔_)
open import Prelude as P hiding (Type)

import Maybe eq as _
open import Monad eq
open import Nat eq

-- Reflection primitives.

open Agda.Builtin.Reflection public hiding (isMacro; withNormalisation)

-- The TC monad is a "raw monad".

instance

  raw-monad : ∀ {d} → Raw-monad {d = d} TC
  Raw-monad.return raw-monad = returnTC
  Raw-monad._>>=_ raw-monad  = bindTC

-- Converts B.Bool to and from Bool.

Bool⇔Bool : B.Bool ⇔ Bool
Bool⇔Bool = record { to = to; from = from }
  where
  to : B.Bool → Bool
  to B.false = false
  to B.true  = true

  from : Bool → B.Bool
  from false = B.false
  from true  = B.true

-- Variants of some definitions from Agda.Builtin.Reflection.

isMacro : Name → TC Bool
isMacro x = _⇔_.to Bool⇔Bool ⟨$⟩ Agda.Builtin.Reflection.isMacro x

withNormalisation : ∀ {a} {A : P.Type a} → Bool → TC A → TC A
withNormalisation =
  Agda.Builtin.Reflection.withNormalisation ∘ _⇔_.from Bool⇔Bool

-- Constructs a visible, relevant argument that is not erased

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

-- Constructs a hidden, relevant argument that is not erased.

pattern harg x = arg (arg-info hidden (modality relevant quantity-ω)) x

-- An n-ary variant of pi.

pis : List (Abs (Arg Type)) → Type → Type
pis []             B = B
pis (abs x A ∷ As) B = pi A (abs x (pis As B))

mutual

  -- Checks if the terms are syntactically equal.
  --
  -- Pattern-matching lambdas and "unknown" are currently never seen
  -- as equal to anything.
  --
  -- Note that this function does not perform any kind of parameter
  -- reconstruction.

  eq-Term : Term → Term → Bool
  eq-Term (var x₁ ts₁)   (var x₂ ts₂)   = eq-ℕ x₁ x₂ ∧ eq-Args ts₁ ts₂
  eq-Term (con c₁ ts₁)   (con c₂ ts₂)   = eq-Name c₁ c₂ ∧ eq-Args ts₁ ts₂
  eq-Term (def f₁ ts₁)   (def f₂ ts₂)   = eq-Name f₁ f₂ ∧ eq-Args ts₁ ts₂
  eq-Term (lam v₁ t₁)    (lam v₂ t₂)    = eq-Visibility v₁ v₂ ∧ eq-Abs t₁ t₂
  eq-Term (pi a₁ b₁)     (pi a₂ b₂)     = eq-Arg a₁ a₁ ∧ eq-Abs b₁ b₂
  eq-Term (agda-sort s₁) (agda-sort s₂) = eq-Sort s₁ s₂
  eq-Term (lit l₁)       (lit l₂)       = eq-Literal l₁ l₂
  eq-Term (meta x₁ ts₁)  (meta x₂ ts₂)  = eq-Meta x₁ x₂ ∧ eq-Args ts₁ ts₂
  eq-Term _              _              = false

  eq-Name : Name → Name → Bool
  eq-Name x₁ x₂ = _⇔_.to Bool⇔Bool (primQNameEquality x₁ x₂)

  eq-ℕ : ℕ → ℕ → Bool
  eq-ℕ = _==_

  eq-Meta : Meta → Meta → Bool
  eq-Meta x₁ x₂ = _⇔_.to Bool⇔Bool (primMetaEquality x₁ x₂)

  eq-String : String → String → Bool
  eq-String x₁ x₂ = _⇔_.to Bool⇔Bool (primStringEquality x₁ x₂)

  eq-Sort : Sort → Sort → Bool
  eq-Sort (set t₁) (set t₂) = eq-Term t₁ t₂
  eq-Sort (lit n₁) (lit n₂) = eq-ℕ n₁ n₂
  eq-Sort _        _        = false

  eq-Literal : Literal → Literal → Bool
  eq-Literal (nat n₁)    (nat n₂)    = eq-ℕ n₁ n₂
  eq-Literal (float x₁)  (float x₂)  = _⇔_.to Bool⇔Bool
                                         (primFloatEquality x₁ x₂)
  eq-Literal (char c₁)   (char c₂)   = _⇔_.to Bool⇔Bool
                                         (primCharEquality c₁ c₂)
  eq-Literal (string s₁) (string s₂) = eq-String s₁ s₂
  eq-Literal (name x₁)   (name x₂)   = eq-Name x₁ x₂
  eq-Literal (meta x₁)   (meta x₂)   = eq-Meta x₁ x₂
  eq-Literal _           _           = false

  eq-Args : List (Arg Term) → List (Arg Term) → Bool
  eq-Args []         []         = true
  eq-Args (t₁ ∷ ts₁) (t₂ ∷ ts₂) = eq-Arg t₁ t₂ ∧ eq-Args ts₁ ts₂
  eq-Args _          _          = false

  eq-Abs : Abs Term → Abs Term → Bool
  eq-Abs (abs s₁ t₁) (abs s₂ t₂) =
    eq-String s₁ s₂ ∧ eq-Term t₁ t₂

  eq-ArgInfo : ArgInfo → ArgInfo → Bool
  eq-ArgInfo (arg-info v₁ m₁) (arg-info v₂ m₂) =
    eq-Visibility v₁ v₂ ∧ eq-Modality m₁ m₂

  eq-Arg : Arg Term → Arg Term → Bool
  eq-Arg (arg i₁ t₁) (arg i₂ t₂) =
    eq-ArgInfo i₁ i₂ ∧ eq-Term t₁ t₂

  eq-Visibility : Visibility → Visibility → Bool
  eq-Visibility visible   visible   = true
  eq-Visibility hidden    hidden    = true
  eq-Visibility instance′ instance′ = true
  eq-Visibility _         _         = false

  eq-Modality : Modality → Modality → Bool
  eq-Modality (modality r₁ q₁) (modality r₂ q₂) =
    eq-Relevance r₁ r₂ ∧ eq-Quantity q₁ q₂

  eq-Relevance : Relevance → Relevance → Bool
  eq-Relevance relevant   relevant   = true
  eq-Relevance irrelevant irrelevant = true
  eq-Relevance _          _          = false

  eq-Quantity : Quantity → Quantity → Bool
  eq-Quantity quantity-0 quantity-0 = true
  eq-Quantity quantity-ω quantity-ω = true
  eq-Quantity _          _          = false

-- Returns a fresh meta-variable of type Level.

fresh-level : TC Level
fresh-level =
  checkType unknown (def (quote Level) []) >>= λ ℓ →
  unquoteTC ℓ

-- Tries to apply the given term (of the given type) to the list of
-- arguments. The type of the resulting term is also returned.

apply : Type → Term → List (Arg Term) → TC (Type × Term)
apply A t []       = returnTC (A , t)
apply A t (a ∷ as) =
  reduce A      >>= λ A →
  apply₁ A t a  >>= λ { (A , t) →
  apply A t as        }
  where
  apply₁ : Type → Term → Arg Term → TC (Type × Term)
  apply₁ (pi (arg i₁@(arg-info k _) A) B) t₁ (arg i₂ t₂) =
    if not (eq-ArgInfo i₁ i₂)
    then typeError (strErr "apply: argument info mismatch" ∷ [])
    else
      bindTC fresh-level                   λ a →
      bindTC fresh-level                   λ b →
      bindTC (unquoteTC A)                 λ (A : P.Type a) →
      bindTC (unquoteTC (lam visible B))   λ (B : A → P.Type b) →
      bindTC (unquoteTC t₂)                λ (t₂ : A) →
      bindTC (quoteTC (B t₂))              λ Bt₂ →
      case k of λ where
        visible →
          bindTC (unquoteTC t₁)            λ (t₁ : (x : A) → B x) →
          bindTC (quoteTC (t₁ t₂))         λ t₁t₂ →
          return (Bt₂ , t₁t₂)
        hidden →
          bindTC (unquoteTC t₁)            λ (t₁ : {x : A} → B x) →
          bindTC (quoteTC (t₁ {x = t₂}))   λ t₁t₂ →
          return (Bt₂ , t₁t₂)
        instance′ →
          bindTC (unquoteTC t₁)            λ (t₁ : ⦃ x : A ⦄ → B x) →
          bindTC (quoteTC (t₁ ⦃ x = t₂ ⦄)) λ t₁t₂ →
          return (Bt₂ , t₁t₂)
  apply₁ (meta x _) _ _ = blockOnMeta x
  apply₁ A          _ _ =
    typeError (strErr "apply: not a pi" ∷ termErr A ∷ [])

mutual

  -- The number of variables bound in the pattern(s).

  bound-in-pattern : Pattern → ℕ
  bound-in-pattern (con _ ps) = bound-in-patterns ps
  bound-in-pattern (dot _)    = 0
  bound-in-pattern (var _)    = 1
  bound-in-pattern (lit _)    = 0
  bound-in-pattern (proj _)   = 0
  bound-in-pattern (absurd _) = 1

  bound-in-patterns : List (Arg Pattern) → ℕ
  bound-in-patterns []             = 0
  bound-in-patterns (arg _ p ∷ ps) =
    bound-in-pattern p + bound-in-patterns ps

mutual

  -- Renames the first variable to the second.
  --
  -- Pattern-matching lambdas are replaced by "unknown".

  rename-term : ℕ → ℕ → Term → Term
  rename-term old new = λ where
    (var x args)      → var (rename-var old new x)
                            (rename-args old new args)
    (con c args)      → con c (rename-args old new args)
    (def f args)      → def f (rename-args old new args)
    (lam v t)         → lam v (rename-abs old new t)
    (pat-lam cs args) → unknown
    (pi a b)          → pi (rename-arg old new a) (rename-abs old new b)
    (agda-sort s)     → agda-sort (rename-sort old new s)
    (lit l)           → lit l
    (meta x args)     → meta x (rename-args old new args)
    unknown           → unknown

  rename-var : ℕ → ℕ → ℕ → ℕ
  rename-var old new x = if eq-ℕ x old then new else old

  rename-abs : ℕ → ℕ → Abs Term → Abs Term
  rename-abs old new (abs s t) =
    abs s (rename-term (suc old) (suc new) t)

  rename-arg : ℕ → ℕ → Arg Term → Arg Term
  rename-arg old new (arg i t) = arg i (rename-term old new t)

  rename-args : ℕ → ℕ → List (Arg Term) → List (Arg Term)
  rename-args old new = λ where
    []       → []
    (a ∷ as) → rename-arg old new a ∷ rename-args old new as

  rename-sort : ℕ → ℕ → Sort → Sort
  rename-sort old new = λ where
    (set t)     → set (rename-term old new t)
    (prop t)    → prop (rename-term old new t)
    (lit n)     → lit n
    (propLit n) → propLit n
    (inf n)     → inf n
    unknown     → unknown

mutual

  -- Weakening: weaken-term from by increases variables "from" and
  -- higher by "by".
  --
  -- Pattern-matching lambdas are replaced by "unknown".

  weaken-term : ℕ → ℕ → Term → Term
  weaken-term from by = λ where
    (var x args)      → var (weaken-var from by x)
                            (weaken-args from by args)
    (con c args)      → con c (weaken-args from by args)
    (def f args)      → def f (weaken-args from by args)
    (lam v t)         → lam v (weaken-abs from by t)
    (pat-lam cs args) → unknown
    (pi a b)          → pi (weaken-arg from by a) (weaken-abs from by b)
    (agda-sort s)     → agda-sort (weaken-sort from by s)
    (lit l)           → lit l
    (meta x args)     → meta x (weaken-args from by args)
    unknown           → unknown

  weaken-var : ℕ → ℕ → ℕ → ℕ
  weaken-var from by x = if from <= x then x + by else x

  weaken-abs : ℕ → ℕ → Abs Term → Abs Term
  weaken-abs from by (abs s t) =
    abs s (weaken-term (suc from) by t)

  weaken-arg : ℕ → ℕ → Arg Term → Arg Term
  weaken-arg from by (arg i t) = arg i (weaken-term from by t)

  weaken-args : ℕ → ℕ → List (Arg Term) → List (Arg Term)
  weaken-args from by = λ where
    []       → []
    (a ∷ as) → weaken-arg from by a ∷ weaken-args from by as

  weaken-sort : ℕ → ℕ → Sort → Sort
  weaken-sort from by = λ where
    (set t)     → set (weaken-term from by t)
    (prop t)    → prop (weaken-term from by t)
    (lit n)     → lit n
    (propLit n) → propLit n
    (inf n)     → inf n
    unknown     → unknown

mutual

  -- Strengthening: strengthen-term from by subtracts "by" from
  -- variables "from" and higher. Applications of variable x, where
  -- from ≤ x and x < from + by, are replaced by "unknown".
  --
  -- Pattern-matching lambdas are replaced by "unknown".

  strengthen-term : ℕ → ℕ → Term → Term
  strengthen-term from by = λ where
    (var x args)      → let args′ = strengthen-args from by args in
                        if from + by <= x
                        then var (x ∸ by) args′
                        else if from <= x
                        then unknown
                        else var x args′
    (con c args)      → con c (strengthen-args from by args)
    (def f args)      → def f (strengthen-args from by args)
    (lam v t)         → lam v (strengthen-abs from by t)
    (pat-lam cs args) → unknown
    (pi a b)          → pi (strengthen-arg from by a)
                           (strengthen-abs from by b)
    (agda-sort s)     → agda-sort (strengthen-sort from by s)
    (lit l)           → lit l
    (meta x args)     → meta x (strengthen-args from by args)
    unknown           → unknown

  strengthen-abs : ℕ → ℕ → Abs Term → Abs Term
  strengthen-abs from by (abs s t) =
    abs s (strengthen-term (suc from) by t)

  strengthen-arg : ℕ → ℕ → Arg Term → Arg Term
  strengthen-arg from by (arg i t) = arg i (strengthen-term from by t)

  strengthen-args : ℕ → ℕ → List (Arg Term) → List (Arg Term)
  strengthen-args from by = λ where
    []       → []
    (a ∷ as) → strengthen-arg from by a ∷ strengthen-args from by as

  strengthen-sort : ℕ → ℕ → Sort → Sort
  strengthen-sort from by = λ where
    (set t)     → set (strengthen-term from by t)
    (prop t)    → prop (strengthen-term from by t)
    (lit n)     → lit n
    (propLit n) → propLit n
    (inf n)     → inf n
    unknown     → unknown

mutual

  -- The result of any-term and similar functions.
  --
  -- Note that "definitely true" can be returned even if the term
  -- contains meta-variables, the term unknown, the sort unknown, or
  -- pattern-matching lambdas.

  Any-result : P.Type
  Any-result = Any-result′ Bool

  -- A generalisation of Any-result. (Without the type parameter the
  -- raw monad instance below would not work.)

  data Any-result′ (A : P.Type) : P.Type where
    definitely : A → Any-result′ A
    -- The result is definitely true or false.
    meta : Meta → Any-result′ A
    -- There is no positive evidence that the result is true. At least
    -- one meta-variable (the given one) was encountered, and if this
    -- meta-variable is instantiated in a certain way, then the
    -- predicate might hold (depending on what the predicate is,
    -- any-term does not analyse the predicate).
    unknown : Any-result′ A
    -- There is no positive evidence that the result is true. The term
    -- contains the term unknown, the sort unknown, or a
    -- pattern-matching lambda (and pattern-matching lambdas are not
    -- analysed).

instance

  -- Any-result′ is a raw monad.

  Any-result-raw-monad : Raw-monad Any-result′
  Raw-monad.return Any-result-raw-monad = definitely
  Raw-monad._>>=_  Any-result-raw-monad = λ where
    (definitely x) f → f x
    (meta m)       f → meta m
    unknown        f → unknown

mutual

  -- Tries to figure out if the given predicate holds for some free
  -- variable in the given term. The predicate is adjusted when
  -- any-term goes under a binder.

  any-term : (ℕ → Bool) → Term → Any-result
  any-term p = λ where
    (var x args)      → (any-var p x ∨_) ⟨$⟩ any-args p args
    (con _ args)      → any-args p args
    (def _ args)      → any-args p args
    (lam _ t)         → any-abs p t
    (pat-lam cs args) → unknown
    (pi a b)          → _∨_ ⟨$⟩ any-arg p a ⊛ any-abs p b
    (agda-sort s)     → any-sort p s
    (lit l)           → definitely false
    (meta m args)     → case any-args p args of λ where
                          (definitely false) → meta m
                          r                  → r
    unknown           → unknown

  any-var : (ℕ → Bool) → ℕ → Bool
  any-var p x = p x

  any-abs : (ℕ → Bool) → Abs Term → Any-result
  any-abs p (abs _ t) =
    any-term (λ where
                zero    → false
                (suc n) → p n)
             t

  any-arg : (ℕ → Bool) → Arg Term → Any-result
  any-arg p (arg i t) = any-term p t

  any-args : (ℕ → Bool) → List (Arg Term) → Any-result
  any-args p = λ where
    []       → definitely false
    (a ∷ as) → _∨_ ⟨$⟩ any-arg p a ⊛ any-args p as

  any-sort : (ℕ → Bool) → Sort → Any-result
  any-sort p = λ where
    (set t)     → any-term p t
    (prop t)    → any-term p t
    (lit n)     → definitely false
    (propLit n) → definitely false
    (inf n)     → definitely false
    unknown     → unknown

-- Figures out if the given variable is bound in the given term.

bound? : ℕ → Term → Any-result
bound? x = any-term (eq-ℕ x)

-- Figures out if variables less than the given variable are bound
-- in the given term.

<bound? : ℕ → Term → Any-result
<bound? x = any-term (λ y → suc y <= x)

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The irrelevance axiom
------------------------------------------------------------------------

module Irrelevance where

import Level

------------------------------------------------------------------------
-- The irrelevance axiom

-- There is no guarantee that this axiom is sound. Use it at your own
-- risk.

postulate
  .irrelevance-axiom : ∀ {a} {A : Set a} → .A → A

{-# BUILTIN IRRAXIOM irrelevance-axiom #-}


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

test1 : Nat → Nat
test1 zero       = 0
test1 (suc zero) = 1
test1 (suc n)    = {!n!}

test2 : Nat → Nat → Nat
test2 zero zero    = zero
test2 zero (suc y) = y
test2 x    y       = {!x!}

test3 : Bool → Bool → Bool → Bool
test3 true  true  true  = true
test3 x     true  false = x
test3 false y     true  = y
test3 true  false z     = z
test3 x     y     z     = {!x y z!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- 2013-12-28 Andreas, issue reported by Christian Sattler

{-# OPTIONS --allow-unsolved-metas #-}
{-# OPTIONS -v tc.cc:15 #-} -- Keep! Debug printing triggered the problem.

record Σ (A : Set) (B : A → Set) : Set where
  field
    fst : A
    snd : B fst

test : {A : Set} → Σ A (λ {_ → A})
test = _

-- This used to trigger an internal error
-- (funnily only at -v tc.cc:15 verbosity)
-- because adding the clause to an
-- extended lambda failed.  Reason:
-- Extended lambda was registered as Axiom
-- during first checking, not Defn as
-- checkFunDef' now expects.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Desc where

--********************************************
-- Prelude
--********************************************

-- Some preliminary stuffs, to avoid relying on the stdlib

--****************
-- Universe polymorphism
--****************

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

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}

max : Level -> Level -> Level
max  zero    m      = m
max (suc n)  zero   = suc n
max (suc n) (suc m) = suc (max n m)

{-# BUILTIN LEVELMAX max #-}

data Lifted {l : Level} (A : Set l) : Set (suc l) where
       lifter : A → Lifted A

lift : {i : Level} -> Set i -> Set (suc i)
lift x =  Lifted x

unlift : {l : Level}{A : Set l} -> Lifted A -> A
unlift (lifter a) = a

--****************
-- Sigma and friends
--****************

data Sigma {i j : Level}(A : Set i) (B : A -> Set j) : Set (max i j) where
  _,_ : (x : A) (y : B x) -> Sigma A B

pair : {i j : Level}{A : Set i}{B : A -> Set j} ->
       (x : A) (y : B x) -> Sigma {i = i}{j = j} A B
pair x y = x , y

_*_ : {i j : Level}(A : Set i)(B : Set j) -> Set (max i j)
A * B = Sigma A \_ -> B

fst : {i j : Level}{A : Set i}{B : A -> Set j} -> Sigma A B -> A
fst (a , _) = a

snd : {i j : Level}{A : Set i}{B : A -> Set j} (p : Sigma A B) -> B (fst p)
snd (a , b) = b

data Zero {i : Level} : Set i where
data Unit  {i : Level} : Set i where
  Void : Unit

--****************
-- Sum and friends
--****************

data _+_ {i j : Level}(A : Set i)(B : Set j) : Set (max i j) where
  l : A -> A + B
  r : B -> A + B

--****************
-- Equality
--****************

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

cong : {l m : Level}{A : Set l}{B : Set m}
       (f : A -> B){x y : A} -> x == y -> f x == f y
cong f refl = refl

cong2 : {l m n : Level}{A : Set l}{B : Set m}{C : Set n}
        (f : A -> B -> C){x y : A}{z t : B} ->
        x == y -> z == t -> f x z == f y t
cong2 f refl refl = refl

trans : {l : Level}{A : Set l}{x y z : A} -> x == y -> y == z -> x == z
trans refl refl = refl

proof-lift-unlift-eq : {l : Level}{A : Set l}(x : Lifted A) -> lifter (unlift x) == x
proof-lift-unlift-eq (lifter a) = refl

postulate
  reflFun : {l m : Level}{A : Set l}{B : A -> Set m}(f : (a : A) -> B a)(g : (a : A) -> B a)-> ((a : A) -> f a == g a) -> f == g

--********************************************
-- Desc code
--********************************************

-- In the paper, we have presented Desc as the grammar of inductive
-- types. Hence, the codes in the paper closely follow this
-- grammar:

data DescPaper : Set1 where
  oneP : DescPaper
  sigmaP : (S : Set) -> (S -> DescPaper) -> DescPaper
  indx : DescPaper -> DescPaper
  hindx : Set -> DescPaper -> DescPaper

-- We take advantage of this model to give you an alternative
-- presentation. This alternative model is the one implemented in
-- Epigram. It is also the one which inspired the code for indexed
-- descriptions.

-- With sigma, we are actually "quoting" a standard type-former,
-- namely:
--     |Sigma : (S : Set) -> (S -> Set) -> Set|
-- With:
--     |sigma : (S : Set) -> (S -> Desc) -> Desc|

-- In the alternative presentation, we go further and present all our
-- codes as quotations of standard type-formers:

data Desc {l : Level} : Set (suc l) where
  id : Desc
  const : Set l -> Desc
  prod : Desc -> Desc -> Desc
  sigma : (S : Set l) -> (S -> Desc) -> Desc
  pi : (S : Set l) -> (S -> Desc) -> Desc

-- Note that we replace |oneP| by a more general |const| code. Whereas
-- |oneP| was interpreted as the unit set, |const K| is
-- interpreted as |K|, for any |K : Set|. Extensionally,
-- |const K| and |sigma K (\_ -> Unit)| are equivalent. However,
-- |const| is *first-order*, unlike its equivalent encoding. From a
-- definitional perspective, we are giving more opportunities to the
-- type-system, hence reducing the burden on the programmer. For the same
-- reason, we introduce |prod| that overlaps with |pi|.

-- This reorganisation is strictly equivalent to the |DescPaper|. For
-- instance, we can encode |indx| and |hindx| using the following
-- code:

indx2 : {l : Level} -> Desc {l = l} -> Desc {l = l}
indx2 D = prod id D

hindx2 : Set -> Desc -> Desc
hindx2 H D = prod (pi H (\_ -> id)) D

--********************************************
-- Desc interpretation
--********************************************

[|_|]_ : {l : Level} -> Desc -> Set l -> Set l
[| id |] Z        = Z
[| const X |] Z   = X
[| prod D D' |] Z = [| D |] Z * [| D' |] Z
[| sigma S T |] Z = Sigma S (\s -> [| T s |] Z)
[| pi S T |] Z    = (s : S) -> [| T s |] Z

--********************************************
-- Fixpoint construction
--********************************************

data Mu {l : Level}(D : Desc {l = l}) : Set l where
  con : [| D |] (Mu D) -> Mu D

--********************************************
-- Predicate: All
--********************************************

All : {l : Level}(D : Desc)(X : Set)(P : X -> Set l) -> [| D |] X -> Set l
All id          X P x        = P x
All (const Z)   X P x        = Unit
All (prod D D') X P (d , d') = (All D X P d) * (All D' X P d')
All (sigma S T) X P (a , b)  = All (T a) X P b
All (pi S T)    X P f        = (s : S) -> All (T s) X P (f s)

all : {l : Level}(D : Desc)(X : Set)(P : X -> Set l)(R : (x : X) -> P x)(x : [| D |] X) -> All D X P x
all id X P R x = R x
all (const Z) X P R z = Void
all (prod D D') X P R (d , d') = all D X P R d , all D' X P R d'
all (sigma S T) X P R (a , b) = all (T a) X P R b
all (pi S T) X P R f = \ s -> all (T s) X P R (f s)

--********************************************
-- Map
--********************************************

-- This one is bonus: one could rightfully expect our so-called
-- functors to have a morphism part! Here it is.

map : {l : Level}(D : Desc)(X Y : Set l)(f : X -> Y)(v : [| D |] X) -> [| D |] Y
map id X Y sig x = sig x
map (const Z) X Y sig z = z
map (prod D D') X Y sig (d , d') = map D X Y sig d , map D' X Y sig d'
map (sigma S T) X Y sig (a , b) = (a , map (T a) X Y sig b)
map (pi S T) X Y sig f = \x -> map (T x) X Y sig (f x)

-- Together with the proof that they respect the functor laws:

-- map id = id
proof-map-id : {l : Level}(D : Desc)(X : Set l)(v : [| D |] X) -> map D X X (\x -> x) v == v
proof-map-id id X v = refl
proof-map-id (const Z) X v = refl
proof-map-id (prod D D') X (v , v') = cong2 (\x y -> (x , y)) (proof-map-id D X v) (proof-map-id D' X v')
proof-map-id (sigma S T) X (a , b) = cong (\x -> (a , x)) (proof-map-id (T a) X b)
proof-map-id (pi S T) X f = reflFun (\a -> map (T a) X X (\x -> x) (f a)) f (\a -> proof-map-id (T a) X (f a))

-- map (f . g) = map f . map g
proof-map-compos : {l : Level}(D : Desc)(X Y Z : Set l)
                   (f : X -> Y)(g : Y -> Z)
                   (v : [| D |] X) ->
                   map D X Z (\x -> g (f x)) v == map D Y Z g (map D X Y f v)
proof-map-compos id X Y Z f g v = refl
proof-map-compos (const K) X Y Z f g v = refl
proof-map-compos (prod D D') X Y Z f g (v , v') = cong2 (\x y -> (x , y))
                                                        (proof-map-compos D X Y Z f g v)
                                                        (proof-map-compos D' X Y Z f g v')
proof-map-compos (sigma S T) X Y Z f g (a , b) = cong (\x -> (a , x)) (proof-map-compos (T a) X Y Z f g b)
proof-map-compos (pi S T) X Y Z f g fc = reflFun (\a -> map (T a) X Z (\x -> g (f x)) (fc a))
                                                 (\a -> map (T a) Y Z g (map (T a) X Y f (fc a)))
                                                 (\a -> proof-map-compos (T a) X Y Z f g (fc a))

--********************************************
-- Elimination principle: induction
--********************************************

-- One would like to write the following:

{-
ind : {l : Level}
            (D : Desc)
            (P : Mu D -> Set l) ->
            ( (x : [| D |] (Mu D)) ->
              All D (Mu D) P x -> P (con x)) ->
            (v : Mu D) ->
            P v
ind D P ms (con xs) = ms xs (all D (Mu D) P (\x -> ind D P ms x) xs)
-}

-- But the termination checker is unhappy.
-- So we write the following:

module Elim {l : Level}
            (D : Desc)
            (P : Mu D -> Set l)
            (ms : (x : [| D |] (Mu D)) ->
                  All D (Mu D) P x -> P (con x))
       where

    mutual
        ind : (x : Mu D) -> P x
        ind (con xs) =  ms xs (hyps D xs)

        hyps : (D' : Desc)
               (xs : [| D' |] (Mu D)) ->
               All D' (Mu D) P xs
        hyps id x = ind x
        hyps (const Z) z = Void
        hyps (prod D D') (d , d') = hyps D d , hyps D' d'
        hyps (sigma S T) (a , b) = hyps (T a) b
        hyps (pi S T) f = \s -> hyps (T s) (f s)

ind : {l : Level}
            (D : Desc)
            (P : Mu D -> Set l) ->
            ( (x : [| D |] (Mu D)) ->
              All D (Mu D) P x -> P (con x)) ->
            (v : Mu D) ->
            P v
ind D P ms x = Elim.ind D P ms x

--********************************************
-- Examples
--********************************************

--****************
-- Nat
--****************

data NatConst : Set where
  Ze : NatConst
  Su : NatConst

natCases : NatConst -> Desc
natCases Ze = const Unit
natCases Suc = id

NatD : Desc
NatD = sigma NatConst  natCases

Nat : Set
Nat = Mu NatD

ze : Nat
ze = con (Ze , Void)

su : Nat -> Nat
su n = con (Su , n)

-- Now we can get addition for example:

plusCase : (xs : [| NatD |] Nat) ->
           All NatD Nat (\_ -> Nat -> Nat) xs -> Nat -> Nat
plusCase ( Ze , Void ) hs y = y
plusCase ( Su , n ) hs y = su (hs y)

plus : Nat -> Nat -> Nat
plus x = ind NatD (\ _ -> (Nat -> Nat)) plusCase x

-- Do this thing in Epigram, you will see that this is *not*
-- hieroglyphic with a bit of elaboration.

--****************
-- List
--****************

data ListConst : Set where
  Nil : ListConst
  Cons : ListConst

listCases : Set -> ListConst -> Desc
listCases X Nil = const Unit
listCases X Cons = sigma X (\_ -> id)

ListD : Set -> Desc
ListD X = sigma ListConst (listCases X)

List : Set -> Set
List X = Mu (ListD X)

nil : {X : Set} -> List X
nil = con ( Nil , Void )

cons : {X : Set} -> X -> List X -> List X
cons x t = con ( Cons , ( x , t ))

--****************
-- Tree
--****************

data TreeConst : Set where
  Leaf : TreeConst
  Node : TreeConst

treeCases : Set -> TreeConst -> Desc
treeCases X Leaf = const Unit
treeCases X Node = sigma X (\_ -> prod id id)

TreeD : Set -> Desc
TreeD X = sigma TreeConst (treeCases X)

Tree : Set -> Set
Tree X = Mu (TreeD X)

leaf : {X : Set} -> Tree X
leaf = con (Leaf , Void)

node : {X : Set} -> X -> Tree X -> Tree X -> Tree X
node x le ri = con (Node , (x , (le , ri)))

--********************************************
-- Finite sets
--********************************************

-- If we weren't such big fans of levitating things, we would
-- implement finite sets with:

{-

data En : Set where
  nE : En
  cE : En -> En

spi : (e : En)(P : EnumT e -> Set) -> Set
spi nE P = Unit
spi (cE e) P = P EZe * spi e (\e -> P (ESu e))

switch : (e : En)(P : EnumT e -> Set)(b : spi e P)(x : EnumT e) -> P x
switch nE P b ()
switch (cE e) P b EZe = fst b
switch (cE e) P b (ESu n) = switch e (\e -> P (ESu e)) (snd b) n
-}

-- But no, we make it fly in Desc:

--****************
-- En
--****************

-- As we have no tags here, we use Nat instead of List.

EnD : Desc
EnD = NatD

En : Set
En = Nat

nE : En
nE = ze

cE : En -> En
cE e = su e

--****************
-- EnumT
--****************

-- Because I don't want to fall back on wacky unicode symbols, I will
-- write EnumT for #, EZe for 0, and ESu for 1+. Sorry about that

data EnumT : (e : En) -> Set where
  EZe : {e : En} -> EnumT (cE e)
  ESu : {e : En} -> EnumT e -> EnumT (cE e)

--****************
-- Small Pi
--****************

-- This corresponds to the small pi |\pi|.

casesSpi : {l : Level}(xs : [| EnD |] En) ->
           All EnD En (\e -> (EnumT e -> Set l) -> Set l) xs ->
           (EnumT (con xs) -> Set l) -> Set l
casesSpi (Ze , Void) hs P' = Unit
casesSpi (Su , n) hs P' = P' EZe * hs (\e -> P' (ESu e))

spi : {l : Level}(e : En)(P : EnumT e -> Set l) -> Set l
spi {x} e P =  ind EnD (\E -> (EnumT E -> Set x) -> Set x) casesSpi e P

--****************
-- Switch
--****************

casesSwitch : {l : Level}
              (xs : [| EnD |] En) ->
              All EnD En (\e -> (P' : EnumT e -> Set l)
                                (b' : spi e P')
                                (x' : EnumT e) -> P' x') xs ->
              (P' : EnumT (con xs) -> Set l)
              (b' : spi (con xs) P')
              (x' : EnumT (con xs)) -> P' x'
casesSwitch (Ze , Void) hs P' b' ()
casesSwitch (Su , n) hs P' b' EZe = fst b'
casesSwitch (Su , n) hs P' b' (ESu e') = hs (\e -> P' (ESu e)) (snd b') e'

switch : {l : Level}
         (e : En)
         (P : EnumT e -> Set l)
         (b : spi e P)
         (x : EnumT e) -> P x
switch {x} e P b xs =  ind EnD
                           (\e -> (P : EnumT e -> Set x)
                                  (b : spi e P)
                                  (xs : EnumT e) -> P xs)
                           casesSwitch e P b xs

--****************
-- Desc
--****************

-- In the following, we implement Desc in itself. As usual, we have a
-- finite set of constructors -- the name of the codes. Note that we
-- could really define these as a finite set built above. However, in
-- Agda, it's horribly verbose. For the sake of clarity, we won't do
-- that here.

data DescDef : Set1 where
  DescId : DescDef
  DescConst : DescDef
  DescProd : DescDef
  DescSigma : DescDef
  DescPi : DescDef

-- We slightly diverge here from the presentation of the paper: note
-- the presence of terminating "const Unit". Recall our Lisp-ish
-- notation for nested tuples:
--    |[a b c]|
-- Corresponds to
--    |[a , [ b , [c , []]]]|
-- So, if we want to write constructors using our Lisp-ish notation, the interpretation
-- [| DescD |] (Mu DescD) have to evaluates to [ constructor , [ arg1 , [ arg2 , []]]]

-- Hence, we define Desc's code as follow:

descCases : DescDef -> Desc
descCases DescId = const Unit
descCases DescConst = sigma Set (\_ -> const Unit)
descCases DescProd = prod id (prod id (const Unit))
descCases DescSigma = sigma Set (\S -> prod (pi (lift S) (\_ -> id)) (const Unit))
descCases DescPi = sigma Set (\S -> prod (pi (lift S) (\_ -> id)) (const Unit))

DescD : Desc
DescD = sigma DescDef descCases

DescIn : Set1
DescIn = Mu DescD

-- So that the constructors are:
-- (Note the annoying |pair|s to set the implicit levels. I could not
--  get rid of the yellow otherwise)

idIn : DescIn
idIn = con (pair {i = suc zero} {j =  suc zero} DescId Void)
constIn : Set -> DescIn
constIn K = con (pair {i = suc zero} {j = suc zero} DescConst (K , Void))
prodIn : (D D' : DescIn) -> DescIn
prodIn D D' = con (pair {i = suc zero} {j = suc zero} DescProd (D , ( D' , Void )))
sigmaIn : (S : Set)(D : S -> DescIn) -> DescIn
sigmaIn S D = con (pair {i = suc zero} {j = suc zero} DescSigma (S , ((\s -> D (unlift s)) , Void )))
piIn : (S : Set)(D : S -> DescIn) -> DescIn
piIn S D = con (pair {i = suc zero} {j = suc zero} DescPi (S , ((\s -> D (unlift s)) , Void )))

-- At this stage, we could prove the isomorphism between |DescIn| and
-- |Desc|. While not technically difficult, it is long and
-- laborious. We have carried this proof on the more complex and
-- interesting |IDesc| universe, in IDesc.agda.

--********************************************
-- Tagged description
--********************************************

TagDesc : {l : Level} -> Set (suc l)
TagDesc = Sigma En (\e -> spi e (\_ -> Desc))

de : TagDesc -> Desc
de (B , F) = sigma (EnumT B) (\E -> switch B (\_ -> Desc) F E)

--********************************************
-- Catamorphism
--********************************************

cata : (D : Desc)
       (T : Set) ->
       ([| D |] T -> T) ->
       (Mu D) -> T
cata D T phi x = ind D (\_ -> T) (\x ms -> phi (replace D T x ms)) x
  where replace : (D' : Desc)(T : Set)(xs : [| D' |] (Mu D))(ms : All D' (Mu D) (\_ -> T) xs) -> [| D' |] T
        replace id T x y = y
        replace (const Z) T z z' = z
        replace (prod D D') T (x , x') (y , y') = replace D T x y , replace D' T x' y'
        replace (sigma A B) T (a , b) t = a , replace (B a) T b t
        replace (pi A B) T f t = \s -> replace (B s) T (f s) (t s)

--********************************************
-- Free monad construction
--********************************************

_**_ : TagDesc -> (X : Set) -> TagDesc
(e , D) ** X = cE e , (const X , D)

--********************************************
-- Substitution
--********************************************

apply : (D : TagDesc)(X Y : Set) ->
        (X -> Mu (de (D ** Y))) ->
        [| de (D ** X) |] (Mu (de (D ** Y))) ->
        Mu (de (D ** Y))
apply (E , B) X Y sig (EZe , x) = sig x
apply (E , B) X Y sig (ESu n , t) = con (ESu n , t)

subst : (D : TagDesc)(X Y : Set) ->
        Mu (de (D ** X)) ->
        (X -> Mu (de (D ** Y))) ->
        Mu (de (D ** Y))
subst D X Y x sig = cata (de (D ** X)) (Mu (de (D ** Y))) (apply D X Y sig) x

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram


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

postulate +-comm : ∀ m n → m + n ≡ n + m

-- Note that the following does not work because
-- p+q is not abstracted over in `+-comm p q` which means
-- Agda gets stuck trying to unify `p + q` and `q + p`

-- Cf. test/Succeed/UsingEq.agda

rew : ∀ m n p q → m + (p + q) + n ≡ m + (q + p) + n
rew m n p q with p+q ← p + q with refl ← +-comm p q = refl


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

postulate _↦_ : ∀ {a} {A : Set a} → A → A → Set
{-# BUILTIN REWRITE _↦_ #-}

open import Agda.Primitive

postulate
  mekker : Level → Level → Set
  moomoo : Level → Set → Set
  rew : (a b : Level) → moomoo (a ⊔ b) (mekker a b) ↦ (Level → Level)

{-# REWRITE rew #-}

works : {a b : Level} → moomoo (a ⊔ b) (mekker a b) → Level
works f = f lzero

fails : {a : Level} → moomoo a (mekker a a) → Level
fails f = f lzero

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-# OPTIONS --without-K #-}
-- Finite types and paths between them
module FT where

open import Data.Empty
open import Data.Unit
open import Data.Nat
open import Data.Sum
open import Data.Product

infixl 10 _◎_

------------------------------------------------------------------------------
-- Finite types

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

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

------------------------------------------------------------------------------
-- Generalized paths are pi-combinators

data _⇛_ : FT → FT → Set where
  -- additive structure
  unite₊⇛  : { b : FT } → PLUS ZERO b ⇛ b

  uniti₊⇛  : { b : FT } → b ⇛ PLUS ZERO b
  swap₊⇛   : { b₁ b₂ : FT } → PLUS b₁ b₂ ⇛ PLUS b₂ b₁
  assocl₊⇛ : { b₁ b₂ b₃ : FT } → PLUS b₁ (PLUS b₂ b₃) ⇛ PLUS (PLUS b₁ b₂) b₃
  assocr₊⇛ : { b₁ b₂ b₃ : FT } → PLUS (PLUS b₁ b₂) b₃ ⇛ PLUS b₁ (PLUS b₂ b₃)
  -- multiplicative structure
  unite⋆⇛  : { b : FT } → TIMES ONE b ⇛ b
  uniti⋆⇛  : { b : FT } → b ⇛ TIMES ONE b
  swap⋆⇛   : { b₁ b₂ : FT } → TIMES b₁ b₂ ⇛ TIMES b₂ b₁
  assocl⋆⇛ : { b₁ b₂ b₃ : FT } →
             TIMES b₁ (TIMES b₂ b₃) ⇛ TIMES (TIMES b₁ b₂) b₃
  assocr⋆⇛ : { b₁ b₂ b₃ : FT } →
             TIMES (TIMES b₁ b₂) b₃ ⇛ TIMES b₁ (TIMES b₂ b₃)
  -- distributivity
  distz⇛   : { b : FT } → TIMES ZERO b ⇛ ZERO
  factorz⇛ : { b : FT } → ZERO ⇛ TIMES ZERO b
  dist⇛    : { b₁ b₂ b₃ : FT } →
            TIMES (PLUS b₁ b₂) b₃ ⇛ PLUS (TIMES b₁ b₃) (TIMES b₂ b₃)
  factor⇛  : { b₁ b₂ b₃ : FT } →
            PLUS (TIMES b₁ b₃) (TIMES b₂ b₃) ⇛ TIMES (PLUS b₁ b₂) b₃
  -- congruence
  id⇛    : { b : FT } → b ⇛ b
  sym⇛   : { b₁ b₂ : FT } → (b₁ ⇛ b₂) → (b₂ ⇛ b₁)
  _◎_    : { b₁ b₂ b₃ : FT } → (b₁ ⇛ b₂) → (b₂ ⇛ b₃) → (b₁ ⇛ b₃)
  _⊕_    : { b₁ b₂ b₃ b₄ : FT } →
           (b₁ ⇛ b₃) → (b₂ ⇛ b₄) → (PLUS b₁ b₂ ⇛ PLUS b₃ b₄)
  _⊗_    : { b₁ b₂ b₃ b₄ : FT } →
           (b₁ ⇛ b₃) → (b₂ ⇛ b₄) → (TIMES b₁ b₂ ⇛ TIMES b₃ b₄)

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

-- An alternative interpretation, as a Functor.
⟦_⟧′ : FT → (Set → Set)
⟦ ZERO ⟧′ A = ⊥
⟦ ONE ⟧′ A = A
⟦ PLUS B₁ B₂ ⟧′ A = ⟦ B₁ ⟧′ A ⊎ ⟦ B₂ ⟧′ A
⟦ TIMES B₁ B₂ ⟧′ A = ⟦ B₁ ⟧′ A × ⟦ B₂ ⟧′ A

{--

Not used

BOOL-FT : Set
BOOL-FT = ⟦ PLUS ONE ONE ⟧

true-FT : BOOL-FT
true-FT = inj₁ tt

false-FT : BOOL-FT
false-FT = inj₂ tt

witness : (B : FT) → Maybe ⟦ B ⟧
witness ZERO = nothing
witness ONE = just tt
witness (PLUS B₁ B₂) with witness B₁ | witness B₂
... | nothing | nothing = nothing
... | nothing | just b  = just (inj₂ b)
... | just b  | _ = just (inj₁ b)
witness (TIMES B₁ B₂) with witness B₁ | witness B₂
... | nothing | _ = nothing
... | just b  | nothing = nothing
... | just b₁ | just b₂ = just (b₁ , b₂)

elems : (B : FT) → List ⟦ B ⟧
elems ZERO          = []
elems ONE           = [ tt ]
elems (PLUS B₁ B₂)  = map inj₁ (elems B₁) ++ map inj₂ (elems B₂)
elems (TIMES B₁ B₂) = concatMap
                        (λ e₁ → map (λ e₂ → (e₁ , e₂)) (elems B₂))
                        (elems B₁)

expandF : {B₁ B₂ : FT} → (⟦ B₁ ⟧ → ⟦ B₂ ⟧) → List (⟦ B₁ ⟧ × ⟦ B₂ ⟧)
expandF {B₁} {B₂} f = map (λ e → (e , f e)) (elems B₁)

test0 : List ((⊤ × BOOL-FT) × BOOL-FT)
test0 = expandF (unite⋆ {BOOL-FT})

--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module sum where

open import level
open import bool
open import eq
open import maybe
open import product

----------------------------------------------------------------------
-- datatypes
----------------------------------------------------------------------

data _⊎_ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') : Set (ℓ ⊔ ℓ') where
  inj₁ : (x : A) → A ⊎ B
  inj₂ : (y : B) → A ⊎ B

_∨_ : ∀ {ℓ ℓ'} (A : Set ℓ) (B : Set ℓ') → Set (ℓ ⊔ ℓ')
_∨_ = _⊎_

----------------------------------------------------------------------
-- syntax
----------------------------------------------------------------------

infixr 0 _⊎_ _∨_

----------------------------------------------------------------------
-- operations
----------------------------------------------------------------------

_≫=⊎_ : ∀ {ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'}{C : Set (ℓ ⊔ ℓ')}  → A ⊎ B → (B → A ⊎ C) → A ⊎ C
inj₁ x ≫=⊎ f = inj₁ x
inj₂ x ≫=⊎ f = f x

return⊎ : ∀ {ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → B → A ⊎ B
return⊎ b = inj₂ b

infix 5 error⊎_

error⊎_ : ∀ {ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → A → A ⊎ B
error⊎_ a = inj₁ a

extract-inj₁≡ : ∀{ℓ}{ℓ'}{A : Set ℓ}{B : Set ℓ'}{a a' : A} → inj₁{B = B} a ≡ inj₁ a' → a ≡ a'
extract-inj₁≡ refl = refl

extract-inj₂≡ : ∀{ℓ}{ℓ'}{A : Set ℓ}{B : Set ℓ'}{b b' : B} → inj₂{A = A} b ≡ inj₂ b' → b ≡ b'
extract-inj₂≡ refl = refl

=⊎ : ∀{ℓ}{ℓ'}{A : Set ℓ}{B : Set ℓ'} → (A → A → 𝔹) → (B → B → 𝔹) → A ⊎ B → A ⊎ B → 𝔹
=⊎ eqa eqb (inj₁ a) (inj₁ a') = eqa a a'
=⊎ eqa eqb (inj₂ b) (inj₂ b') = eqb b b'
=⊎ _ _ _ _ = ff

=⊎-to-≡ : ∀{ℓ}{ℓ'}{A : Set ℓ}{B : Set ℓ'} → (_eqa_ : A → A → 𝔹) → (_eqb_ : B → B → 𝔹) → ((a a' : A) → (a eqa a' ≡ tt) → a ≡ a') → ((b b' : B) → (b eqb b' ≡ tt) → b ≡ b') →  (x y : A ⊎ B) → =⊎ _eqa_ _eqb_ x y  ≡ tt → x ≡ y
=⊎-to-≡ eqa eqb risea riseb (inj₁ a) (inj₁ a') p rewrite risea a a' p = refl
=⊎-to-≡ eqa eqb risea riseb (inj₂ b) (inj₂ b') p rewrite riseb b b' p = refl
=⊎-to-≡ eqa eqb risea riseb (inj₁ a) (inj₂ b) ()
=⊎-to-≡ eqa eqb risea riseb (inj₂ b) (inj₁ a) ()

≡⊎-to-= : ∀{ℓ}{ℓ'}{A : Set ℓ}{B : Set ℓ'} → (_eqa_ : A → A → 𝔹) → (_eqb_ : B → B → 𝔹) → ((a a' : A) → a ≡ a' → a eqa a' ≡ tt) → ((b b' : B) → b ≡ b' → b eqb b' ≡ tt) →  (x y : A ⊎ B) → x ≡ y → =⊎ _eqa_ _eqb_ x y  ≡ tt
≡⊎-to-= eqa eqb dropa dropb (inj₁ a) (inj₁ a') p = dropa a a' (extract-inj₁≡ p)
≡⊎-to-= eqa eqb dropa dropb (inj₂ b) (inj₂ b') p = dropb b b' (extract-inj₂≡ p)
≡⊎-to-= eqa eqb dropa dropb (inj₁ a) (inj₂ b) ()
≡⊎-to-= eqa eqb dropa dropb (inj₂ b) (inj₁ a) ()

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
open import Nat
open import Prelude
open import List

open import contexts
open import core

open import lemmas-env

module preservation where
  preservation : ∀{⛽ Δ Σ' Γ E e r k τ} →
                   Δ , Σ' , Γ ⊢ E →
                   Δ , Σ' , Γ ⊢ e :: τ →
                   E ⊢ e ⌊ ⛽ ⌋⇒ r ⊣ k →
                   Δ , Σ' ⊢ r ·: τ
  preservation ctxcons ta EFix = TAFix ctxcons ta
  preservation ctxcons (TAVar tah) (EVar h) with env-all-Γ ctxcons tah
  ... | π3 , π4 , π5 rewrite ctxunicity h π4 = π5
  preservation ctxcons (TAHole h) EHole = TAHole h ctxcons
  preservation ctxcons TAUnit EUnit = TAUnit
  preservation ctxcons (TAPair _ ta1 ta2) (EPair eval1 eval2)
    = TAPair (preservation ctxcons ta1 eval1 ) (preservation ctxcons ta2 eval2)
  preservation ctxcons (TACtor h1 h2 ta) (ECtor eval) = TACtor h1 h2 (preservation ctxcons ta eval)
  preservation ctxcons (TAApp _ ta-f ta-arg) (EAppFix _ h eval1 eval2 eval-ef)
    rewrite h
    with preservation ctxcons ta-f eval1
  ... | TAFix ctxcons-Ef (TAFix ta-ef) =
    preservation (EnvInd (EnvInd ctxcons-Ef (preservation ctxcons ta-f eval1)) (preservation ctxcons ta-arg eval2)) ta-ef eval-ef
  preservation ctxcons (TAApp _ ta1 ta2) (EAppUnfinished eval1 _ eval2) =
    TAApp (preservation ctxcons ta1 eval1) (preservation ctxcons ta2 eval2)
  preservation ctxcons (TAFst ta) (EFst eval)
    with preservation ctxcons ta eval
  ... | TAPair ta1 ta2 = ta1
  preservation ctxcons (TAFst ta) (EFstUnfinished eval x)
    = TAFst (preservation ctxcons ta eval)
  preservation ctxcons (TASnd ta) (ESnd eval)
    with preservation ctxcons ta eval
  ... | TAPair ta1 ta2 = ta2
  preservation ctxcons (TASnd ta) (ESndUnfinished eval x)
    = TASnd (preservation ctxcons ta eval)
  preservation {Σ' = Σ'} ctxcons (TACase d∈Σ' ta h1 h2) (EMatch _ form eval-e eval-ec) with h2 form
  ... | _ , _ , _ , c∈cctx2 , ta-ec with preservation ctxcons ta eval-e
  ... | TACtor {cctx = cctx} d∈Σ'2 c∈cctx ta' with ctxunicity {Γ = π1 Σ'} d∈Σ' d∈Σ'2
  ... | refl with ctxunicity {Γ = cctx} c∈cctx c∈cctx2
  ... | refl = preservation (EnvInd ctxcons ta') ta-ec eval-ec
  preservation ctxcons (TACase d∈Σ' ta h1 h2) (EMatchUnfinished eval h) =
    TACase d∈Σ' ctxcons (preservation ctxcons ta eval) h1 λ form' →
      let _ , _ , _ , p2 , p3 = h2 form' in
      _ , p2 , p3
  preservation ctxcons (TAAsrt _ ta1 ta2) (EAsrt eval1 eval2 _) = TAUnit

max_stars_repo_name: hazelgrove/hazelnat-myth-

max_issues_repo_name: hazelgrove/hazelnat-myth-

max_forks_repo_name: hazelgrove/hazelnat-myth-


text:
open import Common.IO
open import Common.Unit
open import Common.String
open import Common.Nat

record Stream (A : Set) : Set where
  coinductive
  field
    head : A
    tail : Stream A
open Stream public

repeat : Stream String
head repeat = "hello"
tail repeat = repeat

lookup : ∀ {A} → Stream A → Nat → A
lookup xs zero = xs .head
lookup xs (suc n) = lookup (xs .tail) n

main : IO Unit
main = putStr (lookup repeat 1000000)

max_stars_repo_name: xekoukou/agda-ocaml

max_issues_repo_name: xekoukou/agda-ocaml

max_forks_repo_name: xekoukou/agda-ocaml


text:
-- | An implementation of the Marketoritative PCM
module Relation.Ternary.Separation.Construct.Market where

open import Level hiding (Lift)
open import Data.Product

open import Relation.Unary
open import Relation.Binary hiding (_⇒_)
open import Relation.Binary.PropositionalEquality as P

open import Relation.Ternary.Separation
open import Relation.Ternary.Separation.Morphisms

module _ {ℓ} (A : Set ℓ) where

  data Market : Set ℓ where
    offer  : (l : A) → Market
    demand : (r : A) → Market

module _ {ℓ} {A : Set ℓ} {{ sep : RawSep A }} {{ _ : IsSep sep }} where

  data Split : Market A → Market A → Market A → Set ℓ where

    offerₗ : {r l₁ l₂ : A} (σ : l₂ ⊎ r ≣ l₁) → Split (offer l₁) (demand r) (offer l₂)
    offerᵣ : {r l₁ l₂ : A} (σ : r ⊎ l₂ ≣ l₁) → Split (demand r) (offer l₁) (offer l₂)
    demand : {r₁ r₂ r : A} (σ : r₁ ⊎ r₂ ≣ r) → Split (demand r₁) (demand r₂) (demand r)

  comm : ∀ {Φ₁ Φ₂ Φ} → Split Φ₁ Φ₂ Φ → Split Φ₂ Φ₁ Φ
  comm (demand p) = demand (⊎-comm p)
  comm (offerₗ σ) = offerᵣ (⊎-comm σ)
  comm (offerᵣ σ) = offerₗ (⊎-comm σ)

  assoc : ∀ {a b ab c abc} → Split a b ab → Split ab c abc → ∃ λ bc → (Split a bc abc) × (Split b c bc)
  assoc (offerₗ σ₁) (offerₗ σ₂) =
    let _ , σ₃ , σ₄ = ⊎-assoc σ₂ σ₁ in -, offerₗ σ₃ , demand (⊎-comm σ₄)
  assoc (offerᵣ σ₁) (offerₗ σ₂) =
    let _ , σ₃ , σ₄ = ⊎-unassoc σ₁ σ₂ in -, offerᵣ σ₃ , offerₗ σ₄
  assoc (demand σ₁) (offerᵣ σ₂) =
    let _ , σ₃ , σ₄ = ⊎-assoc (⊎-comm σ₁) σ₂ in -, offerᵣ σ₄ , offerᵣ σ₃
  assoc (demand σ₁) (demand σ₂) =
    let _ , σ₃ , σ₄ = ⊎-assoc σ₁ σ₂ in -, demand σ₃ , demand σ₄
  instance market-raw-sep : RawSep (Market A)
  RawSep._⊎_≣_ market-raw-sep = Split

  instance market-has-sep : IsSep market-raw-sep
  market-has-sep = record
    { ⊎-comm  = comm
    ; ⊎-assoc = assoc
    }

  instance market-sep : Separation _
  market-sep = record
    { isSep = market-has-sep }

module _ {a} {A : Set a} {{r : RawSep A}} {u} {{ s : IsUnitalSep r u }} where

  module U = IsUnitalSep
  instance market-is-unital : IsUnitalSep market-raw-sep (demand ε)
  U.isSep market-is-unital  = market-has-sep
  U.⊎-idˡ market-is-unital {offer l} = offerᵣ ⊎-idˡ
  U.⊎-idˡ market-is-unital {demand r} = demand ⊎-idˡ
  U.⊎-id⁻ˡ market-is-unital (offerᵣ σ) = cong offer (sym (⊎-id⁻ˡ σ))
  U.⊎-id⁻ˡ market-is-unital (demand σ) = cong demand (⊎-id⁻ˡ σ)

module _ {a} {{ s : MonoidalSep a }} where

  open MonoidalSep s using () renaming (Carrier to A)

  matching : ∀ {a b : A} {c d} → (demand a) ⊎ (offer b) ≣ c → (demand (d ∙ a)) ⊎ (offer (d ∙ b)) ≣ c
  matching (offerᵣ σ) = offerᵣ (⊎-∙ₗ σ)

module _ {ℓ} {A : Set ℓ} {{_ : RawSep A}} where

  private
    variable
      ℓv : Level
      P Q : Pred (A × A) ℓv

  [_]Completes : A → (A × A) → Set ℓ
  [_]Completes x (y , z) = x ⊎ z ≣ y

  data ● {p} (P : Pred (A × A) p) : Pred (Market A) (ℓ ⊔ p) where
    lift : ∀ {xs l₂} → P xs → [ l₂ ]Completes xs → ● P (offer l₂)

  ●-map : ∀[ P ⇒ Q ] → ∀[ ● P ⇒ ● Q ]
  ●-map f (lift px le) = lift (f px) le

module _ {a} {A : Set a} {{r : RawSep A}} {u} {{s₁ : IsUnitalSep r u}} where

  open Morphism

  instance market : Morphism A (Market A)
  j market                 = demand
  j-⊎ market s             = demand s
  j-⊎⁻ market (demand σ)   = -, refl , σ

module _ {a} {A : Set a} {{r : RawSep A}} {u} {{s₁ : IsUnitalSep r u}} where

  open import Relation.Ternary.Separation.Construct.Product
  open Morphism (market {A = A})

  data ○ {p} (P : Pred (A × A) p) : Pred (Market A) (p) where
    lift : ∀ {xs} → P (ε , xs) → ○ P (demand xs)

  module _ {p q} {P : Pred A p} {Q : Pred (A × A) q} where
    ○≺●ₗ : ∀[ P ⇒ⱼ ● Q ─✴ ● (Π₂ P ✴ Q) ]
    app (○≺●ₗ px) (lift qx σ₂) (offerᵣ σ₁) with ⊎-assoc (⊎-comm σ₁) σ₂
    ... | _ , σ₃ , σ₄ = lift (snd px ×⟨ ⊎-idˡ , σ₄ ⟩ qx ) σ₃

    ○≺●ᵣ : ∀[ ● (Π₂ P ✴ Q) ⇒ J P ✴ ● Q ]
    ○≺●ᵣ (lift (snd px ×⟨ σₗ , σᵣ ⟩ qx) σ₂) with ⊎-id⁻ˡ σₗ
    ... | refl with ⊎-unassoc σ₂ σᵣ
    ... | _ , σ₃ , σ₄ = inj px ×⟨ offerᵣ (⊎-comm σ₃) ⟩ lift qx σ₄

{- Complete with respect to a certain element -}
module _ {a} {A : Set a} {{r : RawSep A}} {u} {{ s : IsUnitalSep r u }} where

  open import Relation.Ternary.Separation.Construct.Product
  open Morphism (market {A = A})

  record _◑_ {p q} (P : Pred A p) (Q : Pred (A × A) q) (Φ : A × A) : Set (a ⊔ p ⊔ q) where
    constructor _◑⟨_⟩_
    field
      {Φp Φq} : _
      px  : P Φp
      inc : proj₁ Φ ⊎ Φp ≣ Φq
      qx  : Q (Φq , proj₂ Φ)

  -- the following cannot be proven unfortunately
  -- _ : ∀[ (P ◑ Q₁) ✴ Q₂ ⇒ P ◑ (Q₁ ✴ Q₂) ]

  absorb : ∀ {p q} {P : Pred A p} {Q : Pred (A × A) q} →
           ∀[ P ⇒ⱼ ● Q ─✴ ● (P ◑ Q) ]
  app (absorb px) (lift qx k) (offerᵣ σ) with ⊎-assoc (⊎-comm σ) k
  ... | _ , σ₂ , σ₃ with ⊎-unassoc σ₂ (⊎-comm σ₃)
  ... | _ , σ₄ , σ₅ = lift (px ◑⟨ σ₅ ⟩ qx) σ₄

  expell : ∀ {p q} {P : Pred A p} {Q : Pred (A × A) q} →
           ∀[ ● (P ◑ Q) ⇒ J P ✴ ● Q ]
  expell (lift (px ◑⟨ τ₁ ⟩ qx) k) with ⊎-unassoc (⊎-comm τ₁) k
  ... | _ , τ₃ , τ₄ = (inj px) ×⟨ offerᵣ τ₃ ⟩ (lift qx τ₄)

{- Completion preserving updates -}
module _ {a} {A : Set a} {{r : RawSep A}} {u} {{ s : IsUnitalSep r u }} where

  open import Relation.Ternary.Separation.Construct.Product

  record ⟰_ {p} (P : Pred (A × A) p) (Φᵢ : A × A) : Set (a ⊔ p) where
    constructor complete
    field
      updater : ∀ {Φⱼ Φₖ} →
                Φᵢ ⊎ Φⱼ ≣ (Φₖ , Φₖ) →
                ∃₂ λ Φₗ Φ → Φₗ ⊎ Φⱼ ≣ (Φ , Φ) × P Φₗ
  open ⟰_ public

  ●-update : ∀ {p q} {P : Pred (A × A) p} {Q : Pred (A × A) q} →
             ∀[ ○ (P ─✴ ⟰ Q) ⇒ ● P ─✴ ● Q ]
  app (●-update (lift f)) (lift px σ₁) (offerᵣ σ₂) with ⊎-assoc (⊎-comm σ₂) σ₁
  ... | _ , σ₃ , σ₄ with updater (app f px (⊎-idˡ , σ₄)) (⊎-idʳ , ⊎-comm σ₃)
  ... | _ , _ , (σ₅ , σ₆) , qx with ⊎-id⁻ʳ σ₅
  ... | refl = lift qx (⊎-comm σ₆)


text:
open import FRP.JS.List using ( List ; [] ; _∷_ ; build ) renaming ( length to llength )
open import FRP.JS.Char using ( Char ) renaming ( _<_ to _<C_ ; _≟_ to _≟C_ )
open import FRP.JS.Nat using ( ℕ )
open import FRP.JS.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )

module FRP.JS.String where

infixr 5 _++_
infix 4 _≟_

open import FRP.JS.Primitive public using ( String )

private
 primitive
  primStringAppend   : String → String → String
  primStringEquality : String → String → Bool
  primStringToList : String → List Char

_++_ : String → String → String
_++_ = primStringAppend

{-# COMPILED_JS _++_ function(x) { return function(y) { return x + y; }; } #-}

_≟_ : String → String → Bool
_≟_ = primStringEquality

{-# COMPILED_JS _≟_ function(x) { return function(y) { return x === y; }; } #-}

buildChars : (ℕ → Char) → ℕ → List Char
buildChars = build

toList : String → List Char
toList = primStringToList

{-# COMPILED_JS toList function(s) {
  return exports.buildChars(function(n) { return s.charAt(n); },s.length);
} #-}

length : String → ℕ
length s = llength (toList s)

{-# COMPILED_JS length function(s) { return s.length; } #-}

_<*_ : List Char → List Char → Bool
as       <* []       = false
[]       <* (b ∷ bs) = true
(a ∷ as) <* (b ∷ bs) = (a <C b) ∨ ((a ≟C b) ∧ (as <* bs))

_<_ : String → String → Bool
s < t = toList s <* toList t

{-# COMPILED_JS _<_ function(x) { return function(y) { return x < y; }; } #-}

_≤_ : String → String → Bool
s ≤ t = (s ≟ t) ∨ (s < t)

{-# COMPILED_JS _≤_ function(x) { return function(y) { return x <= y; }; } #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
open import Level using () renaming (zero to ℓ₀)
open import Relation.Binary using (DecSetoid)

module BFFPlug (A : DecSetoid ℓ₀ ℓ₀) where

open import Data.Nat using (ℕ ; _≟_ ; _+_ ; zero ; suc ; ⌈_/2⌉)
open import Data.Maybe using (Maybe ; just ; nothing)
open import Data.Vec using (Vec)
open import Data.Product using (∃ ; _,_)
open import Relation.Binary using (module DecSetoid)
open import Relation.Binary.PropositionalEquality using (refl ; cong ; subst ; sym ; module ≡-Reasoning) renaming (setoid to PropEq)
open import Relation.Nullary using (yes ; no)
open import Function using (flip ; id ; _∘_)
open import Function.LeftInverse using (_RightInverseOf_)
import Category.Monad
open Category.Monad.RawMonad {ℓ₀} Data.Maybe.monad using (_>>=_)

open import Generic using (sequenceV ; ≡-to-Π)
import BFF
import GetTypes
import Examples

open DecSetoid A using (Carrier)
open GetTypes.PartialVecVec public using (Get)
open BFF.PartialVecBFF A public using (sbff ; bff)

bffsameshape : (G : Get) → {i : Get.I G} → Vec Carrier (Get.gl₁ G i) → Vec Carrier (Get.gl₂ G i) → Maybe (Vec Carrier (Get.gl₁ G i))
bffsameshape G {i} = sbff G i

bffplug : (G : Get) → (Get.I G → ℕ → Maybe (Get.I G)) → {i : Get.I G} → {m : ℕ} → Vec Carrier (Get.gl₁ G i) → Vec Carrier m → Maybe (∃ λ j → Vec (Maybe Carrier) (Get.gl₁ G j))
bffplug G sput {i} {m} s v with sput i m
...                        | nothing = nothing
...                        | just j with Get.gl₂ G j ≟ m
...                                 | no gl₂j≢m  = nothing
bffplug G sput {i}     s v | just j | yes refl with bff G j s v
...                                            | nothing = nothing
...                                            | just s′ = just (j , s′)

_SimpleRightInvOf_ : {A B : Set} → (A → B) → (B → A) → Set
f SimpleRightInvOf g = ≡-to-Π f RightInverseOf ≡-to-Π g

bffinv : (G : Get) → (nelteg : ℕ → Get.I G) → nelteg SimpleRightInvOf Get.gl₂ G → {i : Get.I G} → {m : ℕ} → Vec Carrier (Get.gl₁ G i) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (Get.gl₁ G (nelteg m)))
bffinv G nelteg inv {m = m} s v = bff G (nelteg m) s (subst (Vec Carrier) (sym (inv m)) v)

module InvExamples where
  open Examples using (reverse' ; drop' ; sieve' ; tail' ; take')

  reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m)
  reverse-put s v = bffinv reverse' id (λ _ → refl) s v >>= sequenceV

  drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (k + m))
  drop-put k = bffinv (drop' k) id (λ _ → refl)

  double : ℕ → ℕ
  double zero    = zero
  double (suc n) = suc (suc (double n))

  sieve-inv-len : double SimpleRightInvOf ⌈_/2⌉
  sieve-inv-len zero          = refl
  sieve-inv-len (suc zero)    = refl
  sieve-inv-len (suc (suc x)) = cong (suc ∘ suc) (sieve-inv-len x)

  sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec (Maybe Carrier) (double m))
  sieve-put = bffinv sieve' double sieve-inv-len

  tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (suc m))
  tail-put = bffinv tail' id (λ _ → refl)

  take-put : (k : ℕ) → {n : ℕ}  → Vec Carrier (k + n) → Vec Carrier k → Maybe (Vec Carrier (k + n))
  take-put k = bffsameshape (take' k)

max_stars_repo_name: jvoigtlaender/bidiragda

max_issues_repo_name: jvoigtlaender/bidiragda

max_forks_repo_name: jvoigtlaender/bidiragda


text:
------------------------------------------------------------------------------
-- Subtraction using the rec combinator
------------------------------------------------------------------------------

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

module FOT.LTC-PCF.Data.Nat.SubtractionRecCombinator where

open import Common.FOL.Relation.Binary.EqReasoning

open import LTC-PCF.Base
open import LTC-PCF.Base.Properties
open import LTC-PCF.Data.Nat.Properties hiding ( ∸-x0 )
open import LTC-PCF.Data.Nat.Rec
open import LTC-PCF.Data.Nat.Rec.ConversionRules
open import LTC-PCF.Data.Nat.Type
open import LTC-PCF.Data.Nat.UnaryNumbers

-- We add 3 to the fixities of the Agda standard library 0.8.1 (see
-- Data/Nat.agda).
infixl 9 _∸_

------------------------------------------------------------------------------
-- Subtraction
_∸_ : D → D → D
m ∸ n = rec n m (lam (λ _ → lam pred₁))

------------------------------------------------------------------------------
-- Conversion rules from the Agda standard library 0.8.1 (see
-- Data/Nat.agda).

∸-x0 : ∀ n → n ∸ zero ≡ n
∸-x0 n = rec zero n _ ≡⟨ rec-0 n ⟩
         n            ∎

∸-0S : ∀ {n} → N n → zero ∸ succ₁ n ≡ zero
∸-0S nzero =
  rec [1] zero (lam (λ _ → lam pred₁))
    ≡⟨ rec-S zero zero (lam (λ _ → lam pred₁)) ⟩
  lam (λ _ → lam pred₁) · zero · (zero ∸ zero)
    ≡⟨ ·-leftCong (beta (λ _ → lam pred₁) zero) ⟩
  lam pred₁ · (zero ∸ zero)
    ≡⟨ beta pred₁ (zero ∸ zero) ⟩
  pred₁ (zero ∸ zero)
    ≡⟨ predCong (∸-x0 zero) ⟩
  pred₁ zero
    ≡⟨ pred-0 ⟩
  zero ∎

∸-0S (nsucc {n} Nn) =
  rec (succ₁ (succ₁ n)) zero (lam (λ _ → lam pred₁))
    ≡⟨ rec-S (succ₁ n) zero (lam (λ _ → lam pred₁)) ⟩
  lam (λ _ → lam pred₁) · (succ₁ n) · (zero ∸ (succ₁ n))
    ≡⟨ ·-leftCong (beta (λ _ → lam pred₁) (succ₁ n)) ⟩
  lam pred₁ · (zero ∸ (succ₁ n))
    ≡⟨ beta pred₁ (zero ∸ (succ₁ n)) ⟩
  pred₁ (zero ∸ (succ₁ n))
    ≡⟨ predCong (∸-0S Nn) ⟩
  pred₁ zero
    ≡⟨ pred-0 ⟩
  zero ∎

∸-0x : ∀ {n} → N n → zero ∸ n ≡ zero
∸-0x nzero      = ∸-x0 zero
∸-0x (nsucc Nn) = ∸-0S Nn

∸-SS : ∀ {m n} → N m → N n → succ₁ m ∸ succ₁ n ≡ m ∸ n
∸-SS {m} _ nzero =
  rec [1] (succ₁ m) (lam (λ _ → lam pred₁))
    ≡⟨ rec-S zero (succ₁ m) (lam (λ _ → lam pred₁)) ⟩
  lam (λ _ → lam pred₁) · zero · (succ₁ m ∸ zero)
    ≡⟨ ·-leftCong (beta (λ _ → lam pred₁) zero) ⟩
  lam pred₁ · (succ₁ m ∸ zero)
    ≡⟨ beta pred₁ (succ₁ m ∸ zero) ⟩
  pred₁ (succ₁ m ∸ zero)
    ≡⟨ predCong (∸-x0 (succ₁ m)) ⟩
  pred₁ (succ₁ m)
    ≡⟨ pred-S m ⟩
  m
    ≡⟨ sym (∸-x0 m) ⟩
  m ∸ zero ∎

∸-SS nzero (nsucc {n} Nn) =
  rec (succ₁ (succ₁ n)) [1] (lam (λ _ → lam pred₁))
    ≡⟨ rec-S (succ₁ n) [1] (lam (λ _ → lam pred₁))  ⟩
  lam (λ _ → lam pred₁) · (succ₁ n) · ([1] ∸ succ₁ n)
    ≡⟨ ·-leftCong (beta (λ _ → lam pred₁) (succ₁ n)) ⟩
  lam pred₁ · ([1] ∸ succ₁ n)
    ≡⟨ beta pred₁ ([1] ∸ succ₁ n) ⟩
  pred₁ ([1] ∸ succ₁ n)
    ≡⟨ predCong (∸-SS nzero Nn) ⟩
  pred₁ (zero ∸ n)
    ≡⟨ predCong (∸-0x Nn) ⟩
  pred₁ zero
    ≡⟨ pred-0 ⟩
  zero
    ≡⟨ sym (∸-0S Nn) ⟩
  zero ∸ succ₁ n ∎

∸-SS (nsucc {m} Nm) (nsucc {n} Nn) =
  rec (succ₁ (succ₁ n)) (succ₁ (succ₁ m)) (lam (λ _ → lam pred₁))
    ≡⟨ rec-S (succ₁ n) (succ₁ (succ₁ m)) (lam (λ _ → lam pred₁)) ⟩
  lam (λ _ → lam pred₁) · (succ₁ n) · (succ₁ (succ₁ m) ∸ succ₁ n)
    ≡⟨ ·-leftCong (beta (λ _ → lam pred₁) (succ₁ n)) ⟩
  lam pred₁ · (succ₁ (succ₁ m) ∸ succ₁ n)
    ≡⟨ beta pred₁ (succ₁ (succ₁ m) ∸ succ₁ n) ⟩
  pred₁ (succ₁ (succ₁ m) ∸ succ₁ n)
    ≡⟨ predCong (∸-SS (nsucc Nm) Nn) ⟩
  pred₁ (succ₁ m ∸ n)
    ≡⟨ sym (beta pred₁ (succ₁ m ∸ n)) ⟩
  lam pred₁ · (succ₁ m ∸ n)
    ≡⟨ ·-leftCong (sym (beta (λ _ → lam pred₁) n)) ⟩
  (lam (λ _ → lam pred₁)) · n · (succ₁ m ∸ n)
    ≡⟨ sym (rec-S n (succ₁ m) (lam (λ _ → lam pred₁))) ⟩
  rec (succ₁ n) (succ₁ m) (lam (λ _ → lam pred₁))
    ≡⟨ refl ⟩
  succ₁ m ∸ succ₁ n ∎

------------------------------------------------------------------------------
-- Conversion rules from the Agda standard library 0.8.1 (see
-- Data/Nat.agda) without totality hypotheses.

-- We could not prove this property.
-- ∸-0S₁ : ∀ n → zero ∸ succ₁ n ≡ zero
-- ∸-0S₁ n =
--   rec (succ₁ n) zero (lam (λ _ → lam pred₁))
--     ≡⟨ rec-S n zero (lam (λ _ → lam pred₁)) ⟩
--   lam (λ _ → lam pred₁) · n · (zero ∸ n)
--     ≡⟨ ·-leftCong (beta (λ _ → lam pred₁) n) ⟩
--   lam pred₁ · (zero ∸ n)
--     ≡⟨ beta pred₁ (zero ∸ n) ⟩
--   pred₁ (zero ∸ n)
--     ≡⟨ {!!} ⟩
--   {!!}
--     ≡⟨ {!!} ⟩
--   zero ∎

-- We could not prove this property.
-- ∸-SS₁ : ∀ m n → succ₁ m ∸ succ₁ n ≡ m ∸ n
-- ∸-SS₁ m n =
--   rec (succ₁ n) (succ₁ m) (lam (λ _ → lam pred₁))
--   ≡⟨ rec-S n (succ₁ m) (lam (λ _ → lam pred₁)) ⟩
--   lam (λ x → lam pred₁) · n · (succ₁ m ∸ n)
--     ≡⟨ ·-leftCong (beta (λ _ → lam pred₁) n) ⟩
--   lam pred₁ · (succ₁ m ∸ n)
--     ≡⟨ beta pred₁ (succ₁ m ∸ n) ⟩
--   pred₁ (succ₁ m ∸ n)
--     ≡⟨ {!!} ⟩
--   {!!}
--     ≡⟨ {!!} ⟩
--   m ∸ n ∎

------------------------------------------------------------------------------
-- Coq 8.4pl4 conversion rules (.../theories/Init/Peano.v):

-- Fixpoint minus (n m:nat) : nat :=
--   match n, m with
--   | O, _ => n
--   | S k, O => S k
--   | S k, S l => k - l
--   end

∸-x0-coq : ∀ n → n ∸ zero ≡ n
∸-x0-coq n = rec zero n _ ≡⟨ rec-0 n ⟩
             n            ∎

∸-S0-coq : ∀ n → succ₁ n ∸ zero ≡ succ₁ n
∸-S0-coq n =
  rec zero (succ₁ n) (lam (λ _ → lam pred₁))
    ≡⟨ rec-0 (succ₁ n) ⟩
  succ₁ n ∎

-- We could not prove this property.
-- ∸-SS-coq : ∀ m n → succ₁ m ∸ succ₁ n ≡ m ∸ n
-- ∸-SS-coq m n =
--   rec (succ₁ n) (succ₁ m) (lam (λ _ → lam pred₁))
--   ≡⟨ rec-S n (succ₁ m) (lam (λ _ → lam pred₁)) ⟩
--   lam (λ x → lam pred₁) · n · (succ₁ m ∸ n)
--     ≡⟨ ·-leftCong (beta (λ _ → lam pred₁) n) ⟩
--   lam pred₁ · (succ₁ m ∸ n)
--     ≡⟨ beta pred₁ (succ₁ m ∸ n) ⟩
--   pred₁ (succ₁ m ∸ n)
--     ≡⟨ {!!} ⟩
--   {!!}
--     ≡⟨ {!!} ⟩
--   m ∸ n ∎

------------------------------------------------------------------------------
-- Isabelle2014 conversion rules (from src/HOL/Nat.thy)

-- primrec minus_nat where
--   diff_0 [code]: "m - 0 = (m\<Colon>nat)"
-- | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"

∸-x0-isabelle : ∀ n → n ∸ zero ≡ n
∸-x0-isabelle n = rec zero n _ ≡⟨ rec-0 n ⟩
                  n            ∎

-- We could not prove this property.
-- ∸-xS-isabelle : ∀ m n → m ∸ succ₁ n ≡
--                         if (iszero₁ (m ∸ n)) then zero else pred₁ (m ∸ n)
-- ∸-xS-isabelle m n =
--   rec (succ₁ n) m (lam (λ _ → lam pred₁))
--     ≡⟨ rec-S n m (lam (λ _ → lam pred₁)) ⟩
--   lam (λ x → lam pred₁) · n · (m ∸ n)
--     ≡⟨ ·-leftCong (beta (λ _ → lam pred₁) n) ⟩
--   lam pred₁ · (m ∸ n)
--     ≡⟨ beta pred₁ (m ∸ n) ⟩
--   pred₁ (m ∸ n)
--   ≡⟨ {!!} ⟩
--   if (iszero₁ (m ∸ n)) then zero else pred₁ (m ∸ n) ∎

------------------------------------------------------------------------------
-- Peter conversion rules

-- The analogous situation for subtraction is that  given

-- rec-0 : ∀ a {f} → rec zero a f ≡ a
-- rec-S : ∀ n a f → rec (succ₁ n) a f ≡ f · n · (rec n a f)

-- and

-- _∸_ : D → D → D
-- m ∸ n = rec n m (lam (λ _ → lam pred₁))

-- you get the equations obtained by the special case (instantiate a
-- and f according to the def of subtraction)!  This has nothing to do
-- a priori with the Agda standard library.

∸-x0-peter : ∀ n → n ∸ zero ≡ n
∸-x0-peter n = rec zero n _ ≡⟨ rec-0 n ⟩
               n            ∎

∸-xS-peter : ∀ m n → m ∸ succ₁ n ≡ pred₁ (m ∸ n)
∸-xS-peter m n =
  rec (succ₁ n) m (lam (λ _ → lam pred₁))
    ≡⟨ rec-S n m (lam (λ _ → lam pred₁)) ⟩
  lam (λ x → lam pred₁) · n · (m ∸ n)
    ≡⟨ ·-leftCong (beta (λ _ → lam pred₁) n) ⟩
  lam pred₁ · (m ∸ n)
    ≡⟨ beta pred₁ (m ∸ n) ⟩
  pred₁ (m ∸ n) ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module Types4 where

open import Basics public

{-----------------------------------------------------------------------}
-- balanced search trees (based on my ICFP '14 paper
-- How to Keep Your Neighbours in Order

-- but the point here is to watch what the types buy us

{-----------------------------------------------------------------------}
-- compare natural numbers   {- might we visit Basics.agda? -}

_<=_ : Nat -> Nat -> Set
ze <= y = One
su x <= ze = Zero
su x <= su y = x <= y

{-(-}
cmp : (x y : Nat) -> (x <= y) + (y <= x)
cmp ze y = inl <>
cmp (su x) ze = inr <>
cmp (su x) (su x₁) = cmp x x₁
{-)-}

{-----------------------------------------------------------------------}
-- loose bounds (one good idea, not always obvious)

data Bnd : Set where
  bot : Bnd
  # : Nat -> Bnd
  top : Bnd

_<B=_ : Bnd -> Bnd -> Set
bot <B= _ = One
# x <B= # y = x <= y
_ <B= top = One
_ <B= _ = Zero

-- an interval lets you choose a number that fits in some bounds
data Intv (l u : Bnd) : Set where
  intv : (x : Nat)(lx : l <B= # x)(xu : # x <B= u) -> Intv l u

{-----------------------------------------------------------------------}
-- 2-3-trees, indexed by bounds and height

data T23 (l u : Bnd) : (h : Nat) -> Set where

  leaf : (lu : l <B= u) ->
    T23 l u ze

  node2 : forall {h} x
    (tlx : T23 l (# x) h)(txu : T23 (# x) u h) ->
    T23 l u (su h)

  node3 : forall {h} x y
    (tlx : T23 l (# x) h)(txy : T23 (# x) (# y) h)(tyu : T23 (# y) u h) ->
    T23 l u (su h)

{-----------------------------------------------------------------------}
-- insertion

TooBig : Bnd -> Bnd -> Nat -> Set
TooBig l u h = Sg Nat \ x -> T23 l (# x) h * T23 (# x) u h

{-(-}
insert : forall {h l u} -> Intv l u -> T23 l u h ->
          TooBig l u h + T23 l u h
insert (intv x lx xu) (leaf lu) = {!!}
insert (intv x lx xu) (node2 x₁ t t₁) = {!!}
insert (intv x lx xu) (node3 y z tly tyz tzu) with cmp x y
insert (intv x lx xu) (node3 y z tly tyz tzu) | inl xy with insert (intv x lx xy) tly
insert (intv x lx xu) (node3 y z tly tyz tzu) | inl xy | inl (v , tlv , tvy)
  = inl (y , node2 v tlv tvy , node2 z tyz tzu)
insert (intv x lx xu) (node3 y z tly tyz tzu) | inl xy | inr x₁ = {!!}
insert (intv x lx xu) (node3 y z tly tyz tzu) | inr x₁ = {!!}
{-)-}

{-----------------------------------------------------------------------}
-- confession

-- it took me about fifteen years to come up with that type for insert

{-----------------------------------------------------------------------}
-- question (0)

-- how can we make better use of the way types act as "problem statement?"

{-----------------------------------------------------------------------}
-- question (1)

-- how can we make better use of the way types act as "problem statement?"

   -- programmers should profit from the downpayment and focus on
   --   the actual choices

{-----------------------------------------------------------------------}
-- question (2)

-- how can we make better use of the way types act as "problem statement?"

   -- programmers should profit from the downpayment and focus on
   --   the actual choices

   -- "code" should be a readable record of a problem solving interaction

{-----------------------------------------------------------------------}
-- question (3)

-- how can we make better use of the way types act as "problem statement?"

   -- programmers should profit from the downpayment and focus on
   --   the actual choices

   -- "code" should be a readable record of a problem solving interaction

   -- we need tools to support redesign

{-----------------------------------------------------------------------}
-- an incomplete program is a formal document


text:
{-# OPTIONS --cubical --allow-unsolved-metas #-}
module TranspPiOnMeta where

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

-- Transporting along a function type with unknown sort of
-- domain/codomain shouldn't result into an impossible being thrown.

-- We equate to Set to trigger reduction.

test1 : (primTransp (\ i → (x : {!!}) → {!!}) i0 {!!} {!!}) ≡ Set
test1 i = Set

test2 : (primTransp (\ i → (x : Set) → {!!}) i0 {!!} {!!}) ≡ Set
test2 i = Set

Foo : Set₂
Foo = {!!}

test3 : (primTransp (\ i → (x : {!!}) → Foo) i0 {!!} {!!}) ≡ Set
test3 i = Set


text:
{-# OPTIONS --safe #-}
module tmp where

open import Relation.Nullary
open import Data.List public

data Suf {X : Set} : List X → List X → Set where
  sinit : ∀ l → Suf l l
  scons : ∀ x l l' → Suf l l' → Suf (x ∷ l) l'

lemma : ∀ {X} (x : X) l l' → Suf l (x ∷ l') → Suf l l'
lemma x .(x ∷ l') l' (sinit .(x ∷ l')) = scons x l' l' (sinit l')
lemma x .(x₁ ∷ l) l' (scons x₁ l .(x ∷ l') H) = scons x₁ l l' (lemma x l l' H)

less-is-not-more : ∀ {X} x (l : List X) → ¬ Suf l (x ∷ l)
less-is-not-more x [] = λ ()
less-is-not-more x (x₁ ∷ l) (scons .x₁ .l .(x ∷ x₁ ∷ l) H) = less-is-not-more x₁ l (lemma x l (x₁ ∷ l) H)

max_stars_repo_name: Brethland/LEARNING-STUFF

max_issues_repo_name: Brethland/LEARNING-STUFF

max_forks_repo_name: Brethland/LEARNING-STUFF


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

open import lib.Basics
open import lib.types.Group
open import lib.types.Unit
open import lib.groups.Homomorphisms
open import lib.groups.Lift

module lib.groups.Unit where

Unit-group-structure : GroupStructure Unit
Unit-group-structure = record
  { ident = unit
  ; inv = λ _ → unit
  ; comp = λ _ _ → unit
  ; unitl = λ _ → idp
  ; unitr = λ _ → idp
  ; assoc = λ _ _ _ → idp
  ; invr = λ _ → idp
  ; invl = λ _ → idp
  }

Unit-group : Group lzero
Unit-group = group _ Unit-is-set Unit-group-structure

Lift-Unit-group : ∀ {i} → Group i
Lift-Unit-group = Lift-group Unit-group

0ᴳ = Lift-Unit-group

contr-is-0ᴳ : ∀ {i} (G : Group i) → is-contr (Group.El G) → G == 0ᴳ
contr-is-0ᴳ G pA = group-ua
  (group-hom (λ _ → lift unit) (λ _ _ → idp) , snd (contr-equiv-LiftUnit pA))

0ᴳ-hom-out-level : ∀ {i j} {G : Group i}
  → is-contr (0ᴳ {j} →ᴳ G)
0ᴳ-hom-out-level {G = G} =
  (cst-hom ,
   λ φ → hom= _ _ (λ= (λ {(lift unit) → ! (GroupHom.pres-ident φ)})))

0ᴳ-hom-in-level : ∀ {i j} {G : Group i}
  → is-contr (G →ᴳ 0ᴳ {j})
0ᴳ-hom-in-level {G = G} =
  (cst-hom , λ φ → hom= _ _ (λ= (λ _ → idp)))

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Library.Data.Product where

open import Light.Level using (Level ; Setω)
open import Light.Variable.Sets
open import Light.Variable.Levels
import Light.Library.Data.Both as Both
open import Light.Library.Relation.Binary
      using (SelfTransitive ; SelfSymmetric ; Reflexive)
open import Light.Library.Relation.Binary.Equality.Decidable using (DecidableEquality)

record Dependencies : Setω where

record Library (dependencies : Dependencies) : Setω where
      field
            ℓf : Level → Level → Level
            Σ : ∀ (𝕒 : Set aℓ) → (𝕒 → Set bℓ) → Set (ℓf aℓ bℓ)
            both : ∀ {𝕓 : 𝕒 → Set bℓ} a (b : 𝕓 a) → Σ 𝕒 𝕓
            first : ∀ {𝕓 : 𝕒 → Set bℓ} → Σ 𝕒 𝕓 → 𝕒
            second : ∀ {𝕓 : 𝕒 → Set bℓ} (product : Σ 𝕒 𝕓) → 𝕓 (first product)
            ⦃ equals ⦄ :
                  ∀ ⦃ a‐c‐equals : DecidableEquality 𝕒 𝕔 ⦄ ⦃ b‐d‐equals : DecidableEquality 𝕓 𝕕 ⦄
                  → DecidableEquality (Σ 𝕒 (λ _ → 𝕓)) (Σ 𝕔 (λ _ → 𝕕))

      ∃ : ∀ {𝕒 : Set aℓ} → (𝕒 → Set bℓ) → Set (ℓf aℓ bℓ)
      ∃ = Σ _

      instance both‐library : Both.Library record {}
      both‐library = record
            {
                  Both = λ 𝕒 𝕓 → Σ 𝕒 (λ _ → 𝕓) ;
                  ℓf = ℓf ;
                  both = both ;
                  first = first ;
                  second = second ;
                  equals = equals
            }

open Library ⦃ ... ⦄ public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An irrelevant version of ⊥-elim
------------------------------------------------------------------------

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

module Data.Empty.Irrelevant where

open import Data.Empty hiding (⊥-elim)

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


text:
module _^_ where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

open import Naturals using (ℕ; zero; suc; _*_)

_^_ : ℕ → ℕ → ℕ
_ ^ zero    = 1
m ^ (suc n) = m * (m ^ n)

_ : 3 ^ 4 ≡ 81
_ =
  begin
    3 ^ 4
  ≡⟨⟩
    3 * (3 ^ 3)
  ≡⟨⟩
    3 * (3 * (3 ^ 2))
  ≡⟨⟩
    3 * (3 * (3 * (3 ^ 1)))
  ≡⟨⟩
    3 * (3 * (3 * (3 * (3 ^ 0))))
  ≡⟨⟩
    3 * (3 * (3 * (3 * 1)))
  ≡⟨⟩
    81
  ∎

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


text:
-- Andreas, 2011-10-03
-- Defining a universe for dependent types
-- where the El function only depends on the type code but not on its
-- proof of well-formedness
{-# OPTIONS --experimental-irrelevance --show-implicit --show-irrelevant #-}
module TerminationOnIrrelevantArgument where

data ⊥ : Set where

data D : Set where
  empty : D
  pi    : D -> D -> D
  other : D

postulate
  app : D -> D -> D

mutual

  data Ty : D -> Set where

    Empty : Ty empty

    Pi    : (a f : D) ->
            (A : Ty a) ->
            (F : (d : D) -> .(El a A d) -> Ty (app f d)) ->
            Ty (pi a f)

  El : (a : D) -> .(A : Ty a) -> D -> Set
  El  empty    Empty         g = ⊥
  El (pi a f) (Pi .a .f A F) g = (d : D) -> .(Ad : El a A d) ->
                                 El (app f d) (F d Ad) (app g d)
  El  other   ()             g

-- Termination checking needs to look inside irrelevant arguments.
-- This only works because the termination checker is syntactic
-- and does not respect equality of irrelevant things!

-- clearly, the derivation of Ty a does not matter when computing El
cast : (a : D)(A A' : Ty a)(d : D) -> El a A d -> El a A' d
cast a A A' d x = x

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Agda.Builtin.Nat

data ⊥ : Prop where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x
{-# BUILTIN REWRITE _≡_ #-}

infix 4 _≡_

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

ok : (n : Nat) (p : ⊥) → (n + n) ≡ 0
ok n p = ⊥-elim p

{-# REWRITE ok #-}

notok : (n : Nat) → n + n ≡ 0
notok n = refl

absurd : 2 ≡ 0
absurd = notok 1


text:
module SystemF.Syntax.Term where

open import Prelude
open import SystemF.Syntax.Type

infixl 9 _[_] _·_
data Term (ν n : ℕ) : Set where
  var  : (x : Fin n) → Term ν n
  Λ    : Term (suc ν) n → Term ν n
  λ'   : Type ν → Term ν (suc n) → Term ν n
  _[_] : Term ν n → Type ν → Term ν n
  _·_  : Term ν n → Term ν n → Term ν n


text:
module Mockingbird.Forest.Base where

open import Algebra using (Op₂; Congruent₂; LeftCongruent; RightCongruent)
open import Level using (_⊔_) renaming (suc to lsuc)
open import Relation.Binary using (Rel; IsEquivalence; Setoid)
open import Relation.Nullary using (¬_)

record IsForest {b ℓ} (Bird : Set b) (_≈_ : Rel Bird ℓ) (_∙_ : Op₂ Bird) : Set (b ⊔ ℓ) where
  field
    isEquivalence : IsEquivalence _≈_
    cong : Congruent₂ _≈_ _∙_

  open IsEquivalence isEquivalence public

  setoid : Setoid b ℓ
  setoid = record { isEquivalence = isEquivalence }

  congˡ : LeftCongruent _≈_ _∙_
  congˡ A≈B = cong refl A≈B

  congʳ : RightCongruent _≈_ _∙_
  congʳ A≈B = cong A≈B refl

record Forest {b ℓ} : Set (lsuc (b ⊔ ℓ)) where
  infix  4 _≈_
  infixl 6 _∙_

  field
    Bird : Set b
    _≈_ : Rel Bird ℓ
    _∙_ : Op₂ Bird
    isForest : IsForest Bird _≈_ _∙_

  _≉_ : Rel Bird ℓ
  x ≉ y = ¬ (x ≈ y)

  open IsForest isForest public

  import Relation.Binary.Reasoning.Base.Single _≈_ refl trans as Base
  open Base using (begin_; _∎) public

  infixr 2 _≈⟨⟩_ step-≈ step-≈˘

  _≈⟨⟩_ : ∀ x {y} → x Base.IsRelatedTo y → x Base.IsRelatedTo y
  _ ≈⟨⟩ x≈y = x≈y

  step-≈ = Base.step-∼
  syntax step-≈ x y≈z x≈y = x ≈⟨ x≈y ⟩ y≈z

  step-≈˘ : ∀ x {y z} → y Base.IsRelatedTo z → y ≈ x → x Base.IsRelatedTo z
  step-≈˘ x y∼z y≈x = x ≈⟨ sym y≈x ⟩ y∼z
  syntax step-≈˘ x y≈z y≈x = x ≈˘⟨ y≈x ⟩ y≈z

max_stars_repo_name: splintah/combinatory-logic

max_issues_repo_name: splintah/combinatory-logic

max_forks_repo_name: splintah/combinatory-logic


text:
module Data.BitVector where

open import Algebra.FunctionProperties.Core using (Op₁; Op₂)
open import Data.Bool public hiding (_≟_) renaming (Bool to Bit; false to 0#; true to 1#)
open import Data.Nat using (ℕ)
                     renaming (_+_ to _N+_; _*_ to _N*_; zero to Nzero; suc to Nsuc)
open import Data.Product using (_,_; _×_)
open import Data.Vec using (Vec; _∷_; []; map; tail; zipWith)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

infixl 6 _+_
infixl 7 _*_
infix  8 -_

BitVector = Vec Bit

bitwise-and : ∀ {n} → Op₂ (BitVector n)
bitwise-and = zipWith _∧_

bitwise-or : ∀ {n} → Op₂ (BitVector n)
bitwise-or = zipWith _∨_

half-adder : Bit → Bit → Bit × Bit
half-adder x y = x xor y , x ∧ y

full-adder : Bit → Bit → Bit → Bit × Bit
full-adder a b c0 with half-adder a b
... | s0 , c1 with half-adder s0 c0
... | s1 , c2 = s1 , c1 ∨ c2

add′ : ∀ {n} → Bit → BitVector n → BitVector n → BitVector n
add′ c [] [] = []
add′ c (x ∷ xs) (y ∷ ys) with full-adder x y c
... | s , cout = s ∷ add′ cout xs ys

_+_ : ∀ {n} → Op₂ (BitVector n)
x + y = add′ 0# x y

zero : ∀ n → BitVector n
zero Nzero = []
zero (Nsuc n) = 0# ∷ (zero n)

one : ∀ n → BitVector n
one Nzero = []
one (Nsuc n) = 1# ∷ zero n

bitwise-negation : ∀ {n} → Op₁ (BitVector n)
bitwise-negation = map not

ones : ∀ n → BitVector n
ones n = bitwise-negation (zero n)

droplast : ∀ {n} → BitVector (Nsuc n) → BitVector n
droplast {Nzero} _ = []
droplast {Nsuc n} (x ∷ xs) = x ∷ droplast xs

last : ∀ {n} → BitVector (Nsuc n) → Bit
last (x ∷ []) = x
last {Nsuc n} (x ∷ xs) = last xs

shift : ∀ {n} → Op₁ (BitVector n)
shift {Nzero} xs = xs
shift {Nsuc n} xs = 0# ∷ droplast xs

snoc : ∀ {n} → BitVector n → Bit → BitVector (Nsuc n)
snoc [] b = b ∷ []
snoc (x ∷ xs) b = x ∷ snoc xs b

unshift : ∀ {n} → Op₁ (BitVector n)
unshift [] = []
unshift (x ∷ xs) = snoc xs 0#

rotate : ∀ {n} → Op₁ (BitVector n)
rotate [] = []
rotate {Nsuc n} xs = last xs ∷ droplast xs

unrotate : ∀ {n} → Op₁ (BitVector n)
unrotate [] = []
unrotate (x ∷ xs) = snoc xs x

_*_ : ∀ {n} → Op₂ (BitVector n)
[] * [] = []
(0# ∷ xs) * yys = 0# ∷ xs * droplast yys
(1# ∷ xs) * yys = yys + (0# ∷ xs * droplast yys)

-_ : ∀ {n} → Op₁ (BitVector n)
- x = one _ + bitwise-negation x

open import Relation.Nullary
open import Relation.Binary

infix 4 _≟_

_≟_ : ∀ {n} → Decidable {A = BitVector n} _≡_
[] ≟ [] = yes refl
x ∷ xs ≟ y ∷ ys with xs ≟ ys
0# ∷ xs ≟ 0# ∷ .xs | yes refl = yes refl
1# ∷ xs ≟ 1# ∷ .xs | yes refl = yes refl
1# ∷ xs ≟ 0# ∷ ys  | yes _ = no λ()
0# ∷ xs ≟ 1# ∷ ys  | yes _ = no λ()
...                | no pf = no (λ q → pf (cong tail q))

val1  = 1# ∷ 0# ∷ 0# ∷ 0# ∷ 0# ∷ 0# ∷ 0# ∷ 0# ∷ []
val2  = 0# ∷ 1# ∷ 0# ∷ 0# ∷ 0# ∷ 0# ∷ 0# ∷ 0# ∷ []
val8  = 0# ∷ 0# ∷ 0# ∷ 1# ∷ 0# ∷ 0# ∷ 0# ∷ 0# ∷ []
val10 = 0# ∷ 1# ∷ 0# ∷ 1# ∷ 0# ∷ 0# ∷ 0# ∷ 0# ∷ []
val11 = 1# ∷ 1# ∷ 0# ∷ 1# ∷ 0# ∷ 0# ∷ 0# ∷ 0# ∷ []

max_stars_repo_name: copumpkin/bitvector

max_issues_repo_name: copumpkin/bitvector

max_forks_repo_name: copumpkin/bitvector


text:
module Subst (Gnd : Set)(U : Set)(El : U -> Set) where

open import Basics
open import Pr
open import Nom
import Kind
open Kind Gnd U El
import Cxt
open Cxt Kind
import Loc
open Loc Kind
import Term
open Term Gnd U El
import Shift
open Shift Gnd U El
import Inst
open Inst Gnd U El

data _-[_]_ : Cxt -> Kind -> Cxt -> Set where
  ES : {D : Cxt}{C : Kind} -> EC -[ C ] D
  _[_-_:=_] : {G D : Cxt}{C : Kind} -> (G -[ C ] D) ->
              (x : Nom){Gx : [| G Hasn't x |]}(S : Kind) ->
              D [! C !]- S ->
              (G [ x - S ]){Gx} -[ C ] D

fetch : {G D : Cxt}{C S : Kind} -> (G -[ C ] D) ->
        Nom :- GooN G S -> D [! C !]- S
fetch ES [ x / () ]
fetch (g [ x - S := s ]) [ y / p ] with nomEq x y
fetch (g [ x - S := s ]) [ .x / refl ] | yes refl = s
fetch (g [ x - S := s ]) [ y / p ]     | no n = fetch g [ y / p ]

closed : {G : Cxt}{L : Loc}{T : Kind} ->
         G [ EL / Head ]- T  ->  G [ L / Head ]- T
closed (` x -! xg) = ` x -! xg
closed (# () -! _)

mutual

  wsubst : {C : Kind}{G D : Cxt} -> (G -[ C ] D) ->
          {L : Loc}{T : Kind}(t : L [ Term C ]- T) -> [| Good G t |] ->
          D [ L / Term C ]- T
  wsubst g [ s ] sg = G[ wsubsts g s sg ]
  wsubst g (fn A f) fg = Gfn A \ a -> wsubst g (f a) (fg a)
  wsubst g (\\ b)    bg = G\\ (wsubst g b bg)
  wsubst g (# v $ s) pg = (# v -! _) G$ wsubsts g s (snd pg)
  wsubst g (` x $ s) pg =
    go (shift closed (fetch g [ x / fst pg ])) (wsubsts g s (snd pg))

  wsubsts : {C : Kind}{G D : Cxt} -> (G -[ C ] D) ->
           {L : Loc}{Z : Gnd}{S : Kind}
           (s : L [ Args C Z ]- S) -> [| Good G s |] ->
           D [ L / Args C Z ]- S
  wsubsts g (a ^ s)   sg = a G^ wsubsts g s sg
  wsubsts g (r & s)   pg = wsubst g r (fst pg) G& wsubsts g s (snd pg)
  wsubsts g nil       _  = Gnil

subst : {C : Kind}{G D : Cxt} -> (G -[ C ] D) ->
        {L : Loc}{T : Kind} -> G [ L / Term C ]- T -> D [ L / Term C ]- T
subst g (t -! tg) = wsubst g t tg

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda