text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Base definitions for the left-biased universe-sensitive functor and
-- monad instances for These.
--
-- To minimize the universe level of the RawFunctor, we require that
-- elements of B are "lifted" to a copy of B at a higher universe level
-- (a ⊔ b).
-- See the Data.Product.Categorical.Examples for how this is done in a
-- Product-based similar setting.
------------------------------------------------------------------------

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

open import Level

module Data.These.Categorical.Left.Base {a} (A : Set a) (b : Level) where

open import Data.These
open import Category.Functor
open import Category.Applicative
open import Category.Monad
open import Function

Theseₗ : Set (a ⊔ b) → Set (a ⊔ b)
Theseₗ B = These A B

functor : RawFunctor Theseₗ
functor = record { _<$>_ = map₂ }

------------------------------------------------------------------------
-- Get access to other monadic functions

module _ {F} (App : RawApplicative {a ⊔ b} F) where

  open RawApplicative App

  sequenceA : ∀ {A} → Theseₗ (F A) → F (Theseₗ A)
  sequenceA (this a)    = pure (this a)
  sequenceA (that b)    = that <$> b
  sequenceA (these a b) = these a <$> b

  mapA : ∀ {A B} → (A → F B) → Theseₗ A → F (Theseₗ B)
  mapA f = sequenceA ∘ map₂ f

  forA : ∀ {A B} → Theseₗ A → (A → F B) → F (Theseₗ B)
  forA = flip mapA

module _ {M} (Mon : RawMonad {a ⊔ b} M) where

  private App = RawMonad.rawIApplicative Mon

  sequenceM : ∀ {A} → Theseₗ (M A) → M (Theseₗ A)
  sequenceM = sequenceA App

  mapM : ∀ {A B} → (A → M B) → Theseₗ A → M (Theseₗ B)
  mapM = mapA App

  forM : ∀ {A B} → Theseₗ A → (A → M B) → M (Theseₗ B)
  forM = forA App


text:
open import Data.Sum
open import Data.Fin
open import Data.Maybe
open import Signature

module MixedTest (Σ : Sig) (D : Set) where

-- Δ : Sig
-- Δ = record { ∥_∥ = D ; ar = λ x → Fin 1 }

mutual
  data Term : Set where
    cons : ⟪ Σ ⟫ (Term ⊎ CoTerm) → Term

  record CoTerm : Set where
    coinductive
    field destr : D → Maybe (Term ⊎ CoTerm)

open CoTerm public

ext: agda

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


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

module Erased-cubical.Cubical-again where

open import Agda.Builtin.Cubical.Path

open import Erased-cubical.Erased public

-- Code defined using --erased-cubical can be imported and used by
-- regular Cubical Agda code.

_ : {A : Set} → A → ∥ A ∥
_ = ∣_∣

-- The constructor trivialᶜ is defined in a module that uses --cubical
-- and re-exported from a module that uses --erased-cubical. Because
-- the current module uses --cubical it is fine to use trivialᶜ in a
-- non-erased setting.

_ : {A : Set} (x y : ∥ A ∥ᶜ) → x ≡ y
_ = trivialᶜ

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- 2015-05-05 Bad error message

_=R_ : Rel → Rel → Set
R =R S : (R ⊆ S) × (S ⊆ R) -- here is a typo, : instead of =

ldom : Rel → Pred
ldom R a = ∃ λ b → R a b

-- More than one matching type signature for left hand side ldom R a
-- it could belong to any of: ldom R


text:
module Data.Finitude.FinType where
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Data.Nat as ℕ
open import Data.Fin as Fin using (Fin; #_)
open import Data.Finitude
open import Function.Equality using (_⟨$⟩_)
open import Function.Injection as Inj using (Injective)
open import Function.Inverse as Inv using (Inverse)
open import Data.Vec
open import Data.Vec.Membership.Propositional
open import Data.Vec.Membership.Propositional.Properties
open import Data.Vec.Membership.Propositional.Distinct as Distinct using (Distinct)

record FinType {a} (A : Set a) : Set a where
  field
    size : ℕ
    finitude : Finitude (P.setoid A) size
  open import Data.Vec.Properties

  index  : A → Fin size
  index  = Inverse.to finitude ⟨$⟩_

  index-injective : ∀ {x y} → index x ≡ index y → x ≡ y
  index-injective = Inverse.injective finitude

  enum  : Fin size → A
  enum = Inverse.from finitude ⟨$⟩_

  enum-injective : ∀ {i j} → enum i ≡ enum j → i ≡ j
  enum-injective = Inverse.injective (Inv.sym finitude)

  elems : Vec A size
  elems = tabulate enum

  elems-distinct : Distinct elems
  elems-distinct = Distinct.tabulate (Inverse.injection (Inv.sym finitude))

  _∈elems : ∀ x → x ∈ elems
  x ∈elems rewrite P.sym (Inverse.left-inverse-of finitude x) = ∈-tabulate⁺ enum (index x)

open FinType ⦃ ... ⦄ using (index ; _∈elems)

size : ∀ {a} (A : Set a) ⦃ fin : FinType A ⦄ → ℕ
size A {{ fin }} = FinType.size fin

elems : ∀ {a} (A : Set a) ⦃ fin : FinType A ⦄ → Vec A (size A)
elems A {{ fin }} = FinType.elems fin

instance
  open import Data.Bool
  open import Data.Unit
  open import Data.Empty
  empty   : FinType ⊥
  empty = record {
            size = 0
          ; finitude = record {
              to = P.→-to-⟶ λ()
            ; from = P.→-to-⟶ λ()
            ; inverse-of = record {
              left-inverse-of = λ ()
            ; right-inverse-of = λ ()
            }
            }
          }

  unit   : FinType ⊤
  unit   = record {
          size = 1
        ; finitude = record {
          to = P.→-to-⟶ λ _ → Fin.zero
        ; from = P.→-to-⟶ λ _ → tt
        ; inverse-of = record {
           left-inverse-of = λ _ → P.refl
         ; right-inverse-of = λ { Fin.zero → P.refl ; (Fin.suc ()) }
        }
        }
        }

  bool    : FinType Bool
  bool    = record {
          size = 2
        ; finitude = record {
            to = P.→-to-⟶ λ { false → # 0 ; true → # 1 }
          ; from = P.→-to-⟶ λ { Fin.zero → false ; (Fin.suc Fin.zero) → true ; (Fin.suc (Fin.suc ())) }
          ; inverse-of = record {
            left-inverse-of = λ { false → P.refl ; true → P.refl }
          ; right-inverse-of = λ { Fin.zero → P.refl ; (Fin.suc Fin.zero) → P.refl ; (Fin.suc (Fin.suc ())) }
          }
          }
          }
private
  bools : Vec Bool _
  bools = elems Bool

  example : bools ≡ false ∷ true ∷ []
  example = P.refl

max_stars_repo_name: tizmd/agda-finitary

max_issues_repo_name: tizmd/agda-finitary

max_forks_repo_name: tizmd/agda-finitary


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

open import lib.Basics
open import lib.types.Group
open import lib.types.Bool
open import lib.types.Nat
open import lib.types.Pi
open import lib.types.Sigma
open import lib.groups.Homomorphisms
open import lib.groups.Lift
open import lib.groups.Unit

module lib.groups.GroupProduct where

{- binary product -}
×-group-struct : ∀ {i j} {A : Type i} {B : Type j}
  (GS : GroupStructure A) (HS : GroupStructure B)
  → GroupStructure (A × B)
×-group-struct GS HS = record {
  ident = (ident GS , ident HS);
  inv = λ {(g , h) → (inv GS g , inv HS h)};
  comp = λ {(g₁ , h₁) (g₂ , h₂) → (comp GS g₁ g₂ , comp HS h₁ h₂)};
  unitl = λ {(g , h) → pair×= (unitl GS g) (unitl HS h)};
  unitr = λ {(g , h) → pair×= (unitr GS g) (unitr HS h)};
  assoc = λ {(g₁ , h₁) (g₂ , h₂) (g₃ , h₃) →
    pair×= (assoc GS g₁ g₂ g₃) (assoc HS h₁ h₂ h₃)};
  invl = λ {(g , h) → pair×= (invl GS g) (invl HS h)};
  invr = λ {(g , h) → pair×= (invr GS g) (invr HS h)}}
  where open GroupStructure

_×ᴳ_ : ∀ {i j} → Group i → Group j → Group (lmax i j)
_×ᴳ_ (group A A-level A-struct) (group B B-level B-struct) =
  group (A × B) (×-level A-level B-level) (×-group-struct A-struct B-struct)

{- general product -}
Π-group-struct : ∀ {i j} {I : Type i} {A : I → Type j}
  (FS : (i : I) → GroupStructure (A i))
  → GroupStructure (Π I A)
Π-group-struct FS = record {
  ident = ident ∘ FS;
  inv = λ f i → inv (FS i) (f i);
  comp = λ f g i → comp (FS i) (f i) (g i);
  unitl = λ f → (λ= (λ i → unitl (FS i) (f i)));
  unitr = λ f → (λ= (λ i → unitr (FS i) (f i)));
  assoc = λ f g h → (λ= (λ i → assoc (FS i) (f i) (g i) (h i)));
  invl = λ f → (λ= (λ i → invl (FS i) (f i)));
  invr = λ f → (λ= (λ i → invr (FS i) (f i)))}
  where open GroupStructure

Πᴳ : ∀ {i j} (I : Type i) (F : I → Group j) → Group (lmax i j)
Πᴳ I F = group (Π I (El ∘ F)) (Π-level (λ i → El-level (F i)))
               (Π-group-struct (group-struct ∘ F))
  where open Group

{- the product of abelian groups is abelian -}
×ᴳ-abelian : ∀ {i j} {G : Group i} {H : Group j}
  → is-abelian G → is-abelian H → is-abelian (G ×ᴳ H)
×ᴳ-abelian aG aH (g₁ , h₁) (g₂ , h₂) = pair×= (aG g₁ g₂) (aH h₁ h₂)

Πᴳ-abelian : ∀ {i j} {I : Type i} {F : I → Group j}
  → (∀ i → is-abelian (F i)) → is-abelian (Πᴳ I F)
Πᴳ-abelian aF f₁ f₂ = λ= (λ i → aF i (f₁ i) (f₂ i))

{- defining a homomorphism into a binary product -}
×ᴳ-hom-in : ∀ {i j k} {G : Group i} {H : Group j} {K : Group k}
  → (G →ᴳ H) → (G →ᴳ K) → (G →ᴳ H ×ᴳ K)
×ᴳ-hom-in (group-hom h h-comp) (group-hom k k-comp) = record {
  f = λ x → (h x , k x);
  pres-comp = λ x y → pair×= (h-comp x y) (k-comp x y)}

{- projection homomorphisms -}
×ᴳ-fst : ∀ {i j} {G : Group i} {H : Group j} → (G ×ᴳ H →ᴳ G)
×ᴳ-fst = record {f = fst; pres-comp = λ _ _ → idp}

×ᴳ-snd : ∀ {i j} {G : Group i} {H : Group j} → (G ×ᴳ H →ᴳ H)
×ᴳ-snd = record {f = snd; pres-comp = λ _ _ → idp}

Πᴳ-proj : ∀ {i j} {I : Type i} {F : I → Group j} (i : I)
  → (Πᴳ I F →ᴳ F i)
Πᴳ-proj i = record {
  f = λ f → f i;
  pres-comp = λ _ _ → idp}

{- injection homomorphisms -}
module _ {i j} {G : Group i} {H : Group j} where

  ×ᴳ-inl : G →ᴳ G ×ᴳ H
  ×ᴳ-inl = ×ᴳ-hom-in (idhom G) cst-hom

  ×ᴳ-inr : H →ᴳ G ×ᴳ H
  ×ᴳ-inr = ×ᴳ-hom-in (cst-hom {H = G}) (idhom H)

×ᴳ-diag : ∀ {i} {G : Group i} → (G →ᴳ G ×ᴳ G)
×ᴳ-diag = ×ᴳ-hom-in (idhom _) (idhom _)

{- when G is abelian, we can define a map H×K → G as a sum of maps
 - H → G and K → G (that is, the product behaves as a sum)         -}
module _ {i j k} {G : Group i} {H : Group j} {K : Group k}
  (G-abelian : is-abelian G) where

  private
    module G = Group G
    module H = Group H
    module K = Group K

    lemma : (g₁ g₂ g₃ g₄ : G.El) →
      G.comp (G.comp g₁ g₂) (G.comp g₃ g₄)
      == G.comp (G.comp g₁ g₃) (G.comp g₂ g₄)
    lemma g₁ g₂ g₃ g₄ =
      (g₁ □ g₂) □ (g₃ □ g₄)
         =⟨ G.assoc g₁ g₂ (g₃ □ g₄) ⟩
       g₁ □ (g₂ □ (g₃ □ g₄))
         =⟨ G-abelian g₃ g₄ |in-ctx (λ w → g₁ □ (g₂ □ w)) ⟩
       g₁ □ (g₂ □ (g₄ □ g₃))
         =⟨ ! (G.assoc g₂ g₄ g₃) |in-ctx (λ w → g₁ □ w) ⟩
       g₁ □ ((g₂ □ g₄) □ g₃)
         =⟨ G-abelian (g₂ □ g₄) g₃ |in-ctx (λ w → g₁ □ w) ⟩
       g₁ □ (g₃ □ (g₂ □ g₄))
         =⟨ ! (G.assoc g₁ g₃ (g₂ □ g₄)) ⟩
       (g₁ □ g₃) □ (g₂ □ g₄) ∎
       where _□_ = G.comp

  ×ᴳ-sum-hom : (H →ᴳ G) → (K →ᴳ G) → (H ×ᴳ K →ᴳ G)
  ×ᴳ-sum-hom φ ψ = record {
    f = λ {(h , k) → G.comp (φ.f h) (ψ.f k)};

    pres-comp = λ {(h₁ , k₁) (h₂ , k₂) →
      G.comp (φ.f (H.comp h₁ h₂)) (ψ.f (K.comp k₁ k₂))
        =⟨ φ.pres-comp h₁ h₂ |in-ctx (λ w → G.comp w (ψ.f (K.comp k₁ k₂))) ⟩
      G.comp (G.comp (φ.f h₁) (φ.f h₂)) (ψ.f (K.comp k₁ k₂))
        =⟨ ψ.pres-comp k₁ k₂
           |in-ctx (λ w → G.comp (G.comp (φ.f h₁) (φ.f h₂)) w)  ⟩
      G.comp (G.comp (φ.f h₁) (φ.f h₂)) (G.comp (ψ.f k₁) (ψ.f k₂))
        =⟨ lemma (φ.f h₁) (φ.f h₂) (ψ.f k₁) (ψ.f k₂) ⟩
      G.comp (G.comp (φ.f h₁) (ψ.f k₁)) (G.comp (φ.f h₂) (ψ.f k₂)) ∎}}
      where
      module φ = GroupHom φ
      module ψ = GroupHom ψ

abstract
  ×ᴳ-sum-hom-η : ∀ {i j} (G : Group i) (H : Group j)
    (aGH : is-abelian (G ×ᴳ H))
    → idhom (G ×ᴳ H) == ×ᴳ-sum-hom aGH (×ᴳ-inl {G = G}) (×ᴳ-inr {G = G})
  ×ᴳ-sum-hom-η G H aGH = hom= _ _ $ λ= $ λ {(g , h) →
    ! (pair×= (Group.unitr G g) (Group.unitl H h))}

  ∘-×ᴳ-sum-hom : ∀ {i j k l}
    {G : Group i} {H : Group j} {K : Group k} {L : Group l}
    (aK : is-abelian K) (aL : is-abelian L)
    (φ : K →ᴳ L) (ψ : G →ᴳ K) (χ : H →ᴳ K)
    → ×ᴳ-sum-hom aL (φ ∘ᴳ ψ) (φ ∘ᴳ χ) == φ ∘ᴳ (×ᴳ-sum-hom aK ψ χ)
  ∘-×ᴳ-sum-hom aK aL φ ψ χ = hom= _ _ $ λ= $ λ {(g , h) →
    ! (GroupHom.pres-comp φ (GroupHom.f ψ g) (GroupHom.f χ h))}

{- define a homomorphism G₁ × G₂ → H₁ × H₂ from homomorphisms
 - G₁ → H₁ and G₂ → H₂ -}
×ᴳ-parallel-hom : ∀ {i j k l} {G₁ : Group i} {G₂ : Group j}
  {H₁ : Group k} {H₂ : Group l}
  → (G₁ →ᴳ H₁) → (G₂ →ᴳ H₂) → (G₁ ×ᴳ G₂ →ᴳ H₁ ×ᴳ H₂)
×ᴳ-parallel-hom φ ψ = record {
  f = λ {(h₁ , h₂) → (φ.f h₁ , ψ.f h₂)};
  pres-comp = λ {(h₁ , h₂) (h₁' , h₂') →
    pair×= (φ.pres-comp h₁ h₁') (ψ.pres-comp h₂ h₂')}}
  where
  module φ = GroupHom φ
  module ψ = GroupHom ψ

{- 0ᴳ is a unit for product -}
×ᴳ-unit-l : ∀ {i} {G : Group i} → 0ᴳ {i} ×ᴳ G == G
×ᴳ-unit-l = group-ua
  (×ᴳ-snd {G = 0ᴳ} ,
   is-eq snd (λ g → (lift unit , g)) (λ _ → idp) (λ _ → idp))

×ᴳ-unit-r : ∀ {i} {G : Group i} → G ×ᴳ 0ᴳ {i} == G
×ᴳ-unit-r = group-ua
  (×ᴳ-fst , (is-eq fst (λ g → (g , lift unit)) (λ _ → idp) (λ _ → idp)))

{- A product Πᴳ indexed by Bool is the same as a binary product -}
module _ {i} (Pick : Lift {j = i} Bool → Group i) where

  Πᴳ-Bool-is-×ᴳ :
    Πᴳ (Lift Bool) Pick == (Pick (lift true)) ×ᴳ (Pick (lift false))
  Πᴳ-Bool-is-×ᴳ = group-ua (φ , e)
    where
    φ = ×ᴳ-hom-in (Πᴳ-proj {F = Pick} (lift true))
                  (Πᴳ-proj {F = Pick} (lift false))

    e : is-equiv (GroupHom.f φ)
    e = is-eq _ (λ {(g , h) → λ {(lift true) → g; (lift false) → h}})
          (λ _ → idp)
          (λ _ → λ= (λ {(lift true) → idp; (lift false) → idp}))

{- Commutativity of ×ᴳ -}
×ᴳ-comm : ∀ {i j} (H : Group i) (K : Group j) → H ×ᴳ K ≃ᴳ K ×ᴳ H
×ᴳ-comm H K =
  (record {
     f = λ {(h , k) → (k , h)};
     pres-comp = λ _ _ → idp} ,
   snd (equiv _ (λ {(k , h) → (h , k)}) (λ _ → idp) (λ _ → idp)))

{- Associativity of ×ᴳ -}
×ᴳ-assoc : ∀ {i j k} (G : Group i) (H : Group j) (K : Group k)
  → ((G ×ᴳ H) ×ᴳ K) == (G ×ᴳ (H ×ᴳ K))
×ᴳ-assoc G H K = group-ua
  (record {
     f = λ {((g , h) , k) → (g , (h , k))};
     pres-comp = λ _ _ → idp} ,
   snd (equiv _ (λ {(g , (h , k)) → ((g , h) , k)}) (λ _ → idp) (λ _ → idp)))

module _ {i} where

  _^ᴳ_ : Group i → ℕ → Group i
  H ^ᴳ O = 0ᴳ
  H ^ᴳ (S n) = H ×ᴳ (H ^ᴳ n)

  ^ᴳ-sum : (H : Group i) (m n : ℕ) → (H ^ᴳ m) ×ᴳ (H ^ᴳ n) == H ^ᴳ (m + n)
  ^ᴳ-sum H O n = ×ᴳ-unit-l {G = H ^ᴳ n}
  ^ᴳ-sum H (S m) n =
    ×ᴳ-assoc H (H ^ᴳ m) (H ^ᴳ n) ∙ ap (λ K → H ×ᴳ K) (^ᴳ-sum H m n)

max_stars_repo_name: danbornside/HoTT-Agda

max_issues_repo_name: danbornside/HoTT-Agda

max_forks_repo_name: danbornside/HoTT-Agda


text:
postulate
  f : {A B : Set₁} (C : Set) → C → C

module _ (A B C : Set) where
  test : Set
  test = {!!}


text:
module _ where

module A where

  infix 2 c
  infix 1 d

  syntax c x   = x ↑
  syntax d x y = x ↓ y

  data D : Set where
    ● : D
    c : D → D
    d : D → D → D

module B where

  syntax d x y = x ↓ y

  data D : Set where
    d : D → D → D

open A
open B

rejected : A.D
rejected = ● ↑ ↓ ●

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# NON_TERMINATING #-}

mutual

  data D : Set where
    c : T₁ → D

  T₁ : Set
  T₁ = T₂

  T₂ : Set
  T₂ = T₁ → D


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.Polynomials.Multivariate.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels

open import Cubical.Data.Nat renaming (_+_ to _+n_)
open import Cubical.Data.Vec

open import Cubical.Algebra.Ring
open import Cubical.Algebra.CommRing

private variable
  ℓ ℓ' : Level

module _ (A' : CommRing ℓ) where
  private
    A = fst A'
  open CommRingStr (snd A')

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

  data Poly (n : ℕ) : Type ℓ where
    -- elements
    0P     : Poly n
    base   : (v : Vec ℕ n) → (a : A) → Poly n
    _poly+_  : (P : Poly n) → (Q : Poly n) → Poly n
      -- AbGroup eq
    poly+Assoc : (P Q R : Poly n) → P poly+ (Q poly+ R) ≡ (P poly+ Q) poly+ R
    poly+IdR   : (P : Poly n) → P poly+ 0P ≡ P
    poly+Comm  : (P Q : Poly n) → P poly+ Q ≡ Q poly+ P
      -- Base eq
    base-0P : (v : Vec ℕ n) → base v 0r ≡ 0P
    base-poly+     : (v : Vec ℕ n) → (a b : A) → (base v a) poly+ (base v b) ≡ base v (a + b)
      -- Set Trunc
    trunc : isSet(Poly n)

-----------------------------------------------------------------------------
-- Induction and Recursion

module _ (A' : CommRing ℓ) where
  private
    A = fst A'
  open CommRingStr (snd A')

  module Poly-Ind-Set
    -- types
    (n : ℕ)
    (F : (P : Poly A' n) → Type ℓ')
    (issd : (P : Poly A' n) → isSet (F P))
    -- elements
    (0P* : F 0P)
    (base* : (v : Vec ℕ n) → (a : A) → F (base v a))
    (_poly+*_ : {P Q : Poly A' n} → (PS : F P) → (QS : F Q) → F (P poly+ Q))
    -- AbGroup eq
    (poly+Assoc* : {P Q R : Poly A' n} → (PS : F P) → (QS : F Q) → (RS : F R)
                    → PathP (λ i → F (poly+Assoc P Q R i)) (PS poly+* (QS poly+* RS)) ((PS poly+* QS) poly+* RS))
    (poly+IdR*   : {P : Poly A' n} → (PS : F P) →
                   PathP (λ i → F (poly+IdR P i)) (PS poly+* 0P*) PS)
    (poly+Comm*  : {P Q : Poly A' n} → (PS : F P) → (QS : F Q)
                    → PathP (λ i → F (poly+Comm P Q i)) (PS poly+* QS) (QS poly+* PS))
    -- Base eq
    (base-0P* : (v : Vec ℕ n) → PathP (λ i → F (base-0P v i)) (base* v 0r) 0P*)
    (base-poly+*     : (v : Vec ℕ n) → (a b : A)
                     → PathP (λ i → F (base-poly+ v a b i)) ((base* v a) poly+* (base* v b)) (base* v (a + b)))
    where

    f : (P : Poly A' n) → F P
    f 0P = 0P*
    f (base v a) = base* v a
    f (P poly+ Q) = (f P) poly+* (f Q)
    f (poly+Assoc P Q R i) = poly+Assoc* (f P) (f Q) (f R) i
    f (poly+IdR P i) = poly+IdR* (f P) i
    f (poly+Comm P Q i) = poly+Comm* (f P) (f Q) i
    f (base-0P v i) = base-0P* v i
    f (base-poly+ v a b i) = base-poly+* v a b i
    f (trunc P Q p q i j) = isOfHLevel→isOfHLevelDep 2 issd  (f P) (f Q) (cong f p) (cong f q) (trunc P Q p q) i j

  module Poly-Rec-Set
    -- types
    (n  : ℕ)
    (B  : Type ℓ')
    (iss : isSet B)
    -- elements
    (0P*      : B)
    (base*    : (v : Vec ℕ n) → (a : A) → B)
    (_poly+*_ : B → B → B)
    -- AbGroup eq
    (poly+Assoc* : (PS QS RS : B) → (PS poly+* (QS poly+* RS)) ≡ ((PS poly+* QS) poly+* RS))
    (poly+IdR*   : (PS : B)       → (PS poly+* 0P*) ≡  PS)
    (poly+Comm*  : (PS QS : B)    → (PS poly+* QS) ≡ (QS poly+* PS))
    -- Base eq
    (base-0P* : (v : Vec ℕ n) → (base* v 0r) ≡  0P*)
    (base-poly+*     : (v : Vec ℕ n) → (a b : A) → ((base* v a) poly+* (base* v b)) ≡ (base* v (a + b)))
    where

    f : Poly A' n → B
    f = Poly-Ind-Set.f n (λ _ → B) (λ _ → iss) 0P* base* _poly+*_ poly+Assoc* poly+IdR* poly+Comm* base-0P* base-poly+*

  module Poly-Ind-Prop
    -- types
    (n : ℕ)
    (F : (P : Poly A' n) → Type ℓ')
    (ispd : (P : Poly A' n) → isProp (F P))
    -- elements
    (0P* : F 0P)
    (base* : (v : Vec ℕ n) → (a : A) → F (base v a))
    (_poly+*_ : {P Q : Poly A' n} → (PS : F P) → (QS : F Q) → F (P poly+ Q))
    where

    f : (P : Poly A' n) → F P
    f = Poly-Ind-Set.f n F (λ P → isProp→isSet (ispd P)) 0P* base* _poly+*_
          (λ {P Q R} PS QS RQ → toPathP (ispd _ (transport (λ i → F (poly+Assoc P Q R i)) _) _))
          (λ {P} PS           → toPathP (ispd _ (transport (λ i → F (poly+IdR P i))       _) _))
          (λ {P Q} PS QS      → toPathP (ispd _ (transport (λ i → F (poly+Comm P Q i))    _) _))
          (λ v                → toPathP (ispd _ (transport (λ i → F (base-0P v i))    _) _))
          (λ v a b            → toPathP (ispd _ (transport (λ i → F (base-poly+ v a b i))    _) _))

  module Poly-Rec-Prop
    -- types
    (n : ℕ)
    (B : Type ℓ')
    (isp : isProp B)
    -- elements
    (0P* : B)
    (base* : (v : Vec ℕ n) → (a : A) → B)
    (_poly+*_ : B → B → B)
    where

    f : Poly A' n → B
    f = Poly-Ind-Prop.f n (λ _ → B) (λ _ → isp) 0P* base* _poly+*_

max_stars_repo_name: guilhermehas/cubical

max_issues_repo_name: guilhermehas/cubical

max_forks_repo_name: guilhermehas/cubical


text:
------------------------------------------------------------------------
-- The syntax of, and a type system for, the untyped λ-calculus with
-- constants
------------------------------------------------------------------------

module Lambda.Syntax where

open import Codata.Musical.Notation
open import Data.Nat
open import Data.Fin hiding (_≤?_)
open import Data.Vec
open import Relation.Nullary.Decidable

------------------------------------------------------------------------
-- Terms

-- Variables are represented using de Bruijn indices.

infixl 9 _·_

data Tm (n : ℕ) : Set where
  con : (i : ℕ) → Tm n
  var : (x : Fin n) → Tm n
  ƛ   : (t : Tm (suc n)) → Tm n
  _·_ : (t₁ t₂ : Tm n) → Tm n

-- Convenient helper.

vr : ∀ m {n} {m<n : True (suc m ≤? n)} → Tm n
vr _ {m<n = m<n} = var (#_ _ {m<n = m<n})

------------------------------------------------------------------------
-- Values, potentially with free variables

module WHNF where

  data Value (n : ℕ) : Set where
    con : (i : ℕ) → Value n
    ƛ   : (t : Tm (suc n)) → Value n

  ⌜_⌝ : ∀ {n} → Value n → Tm n
  ⌜ con i ⌝ = con i
  ⌜ ƛ t   ⌝ = ƛ t

------------------------------------------------------------------------
-- Closure-based definition of values

-- Environments and values. Defined in a module parametrised on the
-- type of terms.

module Closure (Tm : ℕ → Set) where

  mutual

    -- Environments.

    Env : ℕ → Set
    Env n = Vec Value n

    -- Values. Lambdas are represented using closures, so values do
    -- not contain any free variables.

    data Value : Set where
      con : (i : ℕ) → Value
      ƛ   : ∀ {n} (t : Tm (suc n)) (ρ : Env n) → Value

------------------------------------------------------------------------
-- Type system (following Leroy and Grall)

-- Recursive, simple types, defined coinductively.

infixr 8 _⇾_

data Ty : Set where
  nat : Ty
  _⇾_ : (σ τ : ∞ Ty) → Ty

-- Contexts.

Ctxt : ℕ → Set
Ctxt n = Vec Ty n

-- Type system.

infix 4 _⊢_∈_

data _⊢_∈_ {n} (Γ : Ctxt n) : Tm n → Ty → Set where
  con : ∀ {i} → Γ ⊢ con i ∈ nat
  var : ∀ {x} → Γ ⊢ var x ∈ lookup Γ x
  ƛ   : ∀ {t σ τ} (t∈ : ♭ σ ∷ Γ ⊢ t ∈ ♭ τ) → Γ ⊢ ƛ t ∈ σ ⇾ τ
  _·_ : ∀ {t₁ t₂ σ τ} (t₁∈ : Γ ⊢ t₁ ∈ σ ⇾ τ) (t₂∈ : Γ ⊢ t₂ ∈ ♭ σ) →
        Γ ⊢ t₁ · t₂ ∈ ♭ τ

------------------------------------------------------------------------
-- Example

-- A non-terminating term.

ω : Tm 0
ω = ƛ (vr 0 · vr 0)

Ω : Tm 0
Ω = ω · ω

-- Ω is well-typed.

Ω-well-typed : (τ : Ty) → [] ⊢ Ω ∈ τ
Ω-well-typed τ =
  _·_ {σ = ♯ σ} {τ = ♯ τ} (ƛ (var · var)) (ƛ (var · var))
  where σ = ♯ σ ⇾ ♯ τ

-- A call-by-value fix-point combinator.

Z : Tm 0
Z = ƛ (t · t)
  where t = ƛ (vr 1 · ƛ (vr 1 · vr 1 · vr 0))

-- This combinator is also well-typed.

fix-well-typed :
  ∀ {σ τ} → [] ⊢ Z ∈ ♯ (♯ (σ ⇾ τ) ⇾ ♯ (σ ⇾ τ)) ⇾ ♯ (σ ⇾ τ)
fix-well-typed =
  ƛ (_·_ {σ = υ} {τ = ♯ _}
         (ƛ (var · ƛ (var · var · var)))
         (ƛ (var · ƛ (var · var · var))))
  where
  υ : ∞ Ty
  υ = ♯ (υ ⇾ ♯ _)

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


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

open import Agda.Builtin.Equality

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

postulate
  T  : (Set → Set → Set) → Set
  T₀ : Set

module _ (F : Set → Set) where

  postulate rew : T (λ X Y → F X) ↦ T₀

  {-# REWRITE rew #-}

  test : T (λ X Y → F X) ≡ T₀
  test = refl

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
module Oscar.Class.TermSubstitution.Internal {𝔣} (FunctionName : Set 𝔣) where

open import Oscar.Data.Term.Core FunctionName
open import Oscar.Data.Nat.Core
open import Oscar.Data.Fin.Core
open import Oscar.Data.Vec.Core
open import Oscar.Data.Equality.Core
open import Oscar.Data.Product.Core
open import Oscar.Function
open import Oscar.Level

_⊸_ : (m n : ℕ) → Set 𝔣
m ⊸ n = Fin m → Term n

⊸-Property : {ℓ : Level} → ℕ → Set (lsuc ℓ ⊔ 𝔣)
⊸-Property {ℓ} m = ∀ {n} → m ⊸ n → Set ℓ

_≐_ : {m n : ℕ} → m ⊸ n → m ⊸ n → Set 𝔣
f ≐ g = ∀ x → f x ≡ g x

⊸-Extensional : {ℓ : Level} {m : ℕ} → ⊸-Property {ℓ} m → Set (ℓ ⊔ 𝔣)
⊸-Extensional P = ∀ {m f g} → f ≐ g → P {m} f → P g

⊸-ExtentionalProperty : {ℓ : Level} → ℕ → Set (lsuc ℓ ⊔ 𝔣)
⊸-ExtentionalProperty {ℓ} m = Σ (⊸-Property {ℓ} m) ⊸-Extensional

mutual

  _◃Term_ : ∀ {m n} → (f : m ⊸ n) → Term m → Term n
  f ◃Term i x = f x
  f ◃Term leaf = leaf
  f ◃Term (s fork t) = (f ◃Term s) fork (f ◃Term t)
  f ◃Term (function fn ts) = function fn (f ◃VecTerm ts) where

  _◃VecTerm_ : ∀ {N m n} → m ⊸ n → Vec (Term m) N → Vec (Term n) N
  f ◃VecTerm [] = []
  f ◃VecTerm (t ∷ ts) = f ◃Term t ∷ f ◃VecTerm ts

_◇_ : ∀ {l m n} → m ⊸ n → l ⊸ m → l ⊸ n
_◇_ f g = (f ◃Term_) ∘ g

record Substitution {a} (A : ℕ → Set a) : Set (a ⊔ 𝔣) where
  field
    _◃_ : ∀ {m n} → m ⊸ n → A m → A n
    ◃-extentionality : ∀ {m n} {f g : m ⊸ n} → f ≐ g → (t : A m) → f ◃ t ≡ g ◃ t
    ◃-identity : ∀ {n} → (t : A n) → i ◃ t ≡ t

  field
    ◃-associativity : ∀ {l m n} → {f : m ⊸ n} {g : _} (t : A l) → (f ◇ g) ◃ t ≡ f ◃ (g ◃ t)

  ⊸-Unifies : ∀ {m} (s t : A m) → ⊸-Property m
  ⊸-Unifies s t f = f ◃ s ≡ f ◃ t

open Substitution ⦃ … ⦄ public

{-# DISPLAY Substitution._◃_ _ = _◃_ #-}


text:
module vector where

open import bool
open import eq
open import list
open import list-to-string
open import nat
open import nat-thms
open import product
open import string

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

data 𝕍 {ℓ} (A : Set ℓ) : ℕ → Set ℓ where
  [] : 𝕍 A 0
  _::_ : {n : ℕ} → A → 𝕍 A n → 𝕍 A (suc n)

vector = 𝕍

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

infixr 6 _::_ _++𝕍_

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

[_]𝕍 : ∀ {ℓ} {A : Set ℓ} → A → 𝕍 A 1
[ x ]𝕍 = x :: []

_++𝕍_ : ∀ {ℓ} {A : Set ℓ}{n m : ℕ} → 𝕍 A n → 𝕍 A m → 𝕍 A (n + m)
[]        ++𝕍 ys = ys
(x :: xs) ++𝕍 ys = x :: xs ++𝕍 ys

head𝕍 : ∀ {ℓ} {A : Set ℓ}{n : ℕ} → 𝕍 A (suc n) → A
head𝕍 (x :: _) = x

tail𝕍 : ∀ {ℓ} {A : Set ℓ}{n : ℕ} → 𝕍 A n → 𝕍 A (pred n)
tail𝕍 [] = []
tail𝕍 (_ :: xs) = xs

map𝕍 : ∀ {ℓ ℓ'} {A : Set ℓ} {B : Set ℓ'}{n : ℕ} → (A → B) → 𝕍 A n → 𝕍 B n
map𝕍 f []       = []
map𝕍 f (x :: xs) = f x :: map𝕍 f xs

concat𝕍 : ∀{ℓ}{A : Set ℓ}{n m : ℕ} → 𝕍 (𝕍 A n) m → 𝕍 A (m * n)
concat𝕍 [] = []
concat𝕍 (x :: xs) = x ++𝕍 (concat𝕍 xs)

nth𝕍 : ∀ {ℓ} {A : Set ℓ}{m : ℕ} → (n : ℕ) → n < m ≡ tt → 𝕍 A m → A
nth𝕍 0 _ (x :: _) = x
nth𝕍 (suc n) p (_ :: xs) = nth𝕍 n p xs
nth𝕍 (suc n) () []
nth𝕍 0 () []

repeat𝕍 : ∀ {ℓ} {A : Set ℓ} → (a : A)(n : ℕ) → 𝕍 A n
repeat𝕍 a 0 = []
repeat𝕍 a (suc n) = a :: (repeat𝕍 a n)

foldl𝕍 : ∀{ℓ ℓ'}{A : Set ℓ}{B : Set ℓ'} → B → (B → A → B) → {n : ℕ} → 𝕍 A n → 𝕍 B n
foldl𝕍 b _f_ [] = []
foldl𝕍 b _f_ (x :: xs) = let r = (b f x) in r :: (foldl𝕍 r _f_  xs)

zipWith𝕍 : ∀ {ℓ ℓ' ℓ''} {A : Set ℓ}{B : Set ℓ'}{C : Set ℓ''} →
           (A → B → C) → {n : ℕ} → 𝕍 A n → 𝕍 B n → 𝕍 C n
zipWith𝕍 f [] [] = []
zipWith𝕍 _f_ (x :: xs) (y :: ys) = (x f y) :: (zipWith𝕍 _f_ xs ys)

-- helper function for all𝕍
allh𝕍 : ∀ {ℓ} {A : Set ℓ}{n : ℕ}(p : ℕ → A → 𝔹) → 𝕍 A n → ℕ → 𝔹
allh𝕍 p [] n = tt
allh𝕍 p (x :: xs) n = p n x && allh𝕍 p xs (suc n)

-- given a predicate p which takes in an index and the element of
-- the given 𝕍 at that index, return tt iff the predicate
-- returns true for all indices (and their elements).
all𝕍 : ∀ {ℓ} {A : Set ℓ}{n : ℕ}(p : ℕ → A → 𝔹) → 𝕍 A n → 𝔹
all𝕍 p v = allh𝕍 p v 0

𝕍-to-𝕃 : ∀ {ℓ} {A : Set ℓ}{n : ℕ} → 𝕍 A n → 𝕃 A
𝕍-to-𝕃 [] = []
𝕍-to-𝕃 (x :: xs) = x :: (𝕍-to-𝕃 xs)

𝕃-to-𝕍 : ∀ {ℓ} {A : Set ℓ} → 𝕃 A → Σ ℕ (λ n → 𝕍 A n)
𝕃-to-𝕍 [] = (0 , [])
𝕃-to-𝕍 (x :: xs) with 𝕃-to-𝕍 xs
... | (n , v) = (suc n , x :: v)

{- turn the given 𝕍 into a string by calling f on each element, and separating the elements
   with the given separator string -}
𝕍-to-string : ∀ {ℓ} {A : Set ℓ}{n : ℕ} → (f : A → string) → (separator : string) → 𝕍 A n → string
𝕍-to-string f sep v = 𝕃-to-string f sep (𝕍-to-𝕃 v)

max_stars_repo_name: heades/AUGL

max_issues_repo_name: heades/AUGL

max_forks_repo_name: heades/AUGL


text:
open import Function using (_∘_)
open import Data.Fin as Fin using (Fin; toℕ)
open import Data.Nat as Nat using (ℕ; suc; zero)
open import Data.Nat.Show using () renaming (show to showℕ)
open import Data.String
open import Data.Vec using (Vec; []; _∷_)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl)

module Unification.Show
  (Sym : ℕ → Set)
  (showSym : ∀ {k} (s : Sym k) → String)
  (decEqSym : ∀ {k} (f g : Sym k) → Dec (f ≡ g)) where

  import Unification
  module UI = Unification Sym decEqSym
  open UI hiding (_++_)

  showFin : ∀ {n} → Fin n → String
  showFin {n} x = (showℕ (toℕ x)) ++ "/" ++ (showℕ n)

  mutual
    showTerm : ∀ {n} → Term n → String
    showTerm (var x) = "?" ++ showFin x
    showTerm (con {zero} s []) = showSym s
    showTerm (con {suc k} s ts) = showSym s ++ "(" ++ showTermArgs ts ++ ")"

    showTermArgs : ∀ {n k} → Vec (Term n) k → String
    showTermArgs []             = ""
    showTermArgs (t ∷ [])       = showTerm t
    showTermArgs (t₁ ∷ t₂ ∷ ts) = showTerm t₁ ++ " , " ++ showTermArgs (t₂ ∷ ts)

  showSubst : ∀ {m n} → Subst m n → String
  showSubst s = "{" ++ showSubst' s ++ "}"
    where
    showFor : ∀ {n} (x : Fin (suc n)) (t : Term n) → String
    showFor x t = "?" ++ showFin x ++ " → " ++ showTerm t

    showSubst' : ∀ {m n} → Subst m n → String
    showSubst' nil = ""
    showSubst' (snoc nil t x)
      = "?" ++ showFin x ++ " → " ++ showTerm t
    showSubst' (snoc (snoc s t₂ x₂) t₁ x₁)
      = showFor x₁ t₁ ++ " , " ++ showSubst' (snoc s t₂ x₂)

max_stars_repo_name: wenkokke/FirstOrderUnificationInAgda

max_issues_repo_name: wenkokke/FirstOrderUnificationInAgda

max_forks_repo_name: wenkokke/FirstOrderUnificationInAgda


text:
-- Andreas, 2017-08-25, issue #1611.
-- Fixed by Jesper Cockx as #2621.

open import Common.Prelude

data D : Bool → Set where
  dt : D true
  df : D false

Works : ∀{b} → D b → Set
Works dt = Bool
Works df = Bool

Fails : ∀{b : Bool} → D _ → Set
Fails dt = Bool
Fails df = Bool

-- WAS:
-- false != true of type Bool
-- when checking that the pattern df has type D true

-- SHOULD BE:
-- Don't know whether to split on dt

-- NOW:
-- I'm not sure if there should be a case for the constructor dt,
-- because I get stuck when trying to solve the following unification
-- problems (inferred index ≟ expected index):
--   true ≟ _9
-- when checking that the pattern dt has type D _9


text:
import Issue2447.M
import Issue2447.Parse-error


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

module Relation.Nullary.Decidable where

open import Level
open import Data.Bool
open import Data.Empty
open import Function.Biconditional

Reflects : Type a → Bool → Type a
Reflects A true  = A
Reflects A false = ¬ A

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

pattern yes p  = true   because p
pattern no ¬p  = false  because ¬p

map-reflects : (A → B) → (¬ A → ¬ B) → ∀ {d} → Reflects A d → Reflects B d
map-reflects {A = A} {B = B} to fro {d = d} = bool {P = λ d → Reflects A d → Reflects B d} fro to d

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

iff-dec : (A ↔ B) → Dec A → Dec B
iff-dec (to iff fro) = map-dec to (λ ¬y x → ¬y (fro x))

infixr 1 dec
dec : (A → B) → (¬ A → B) → Dec A → B
dec {A = A} {B = B} on-yes on-no d = bool {P = λ d → Reflects A d → B} on-no on-yes (d .does) (d .why)

syntax dec (λ yv → ye) (λ nv → ne) dc = ∣ dc ∣yes yv ⇒ ye ∣no nv ⇒ ne

T? : (b : Bool) → Dec (T b)
T? b .does = b
T? false .why ()
T? true  .why = _

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module Problem3 where

open import Problem1
open import Problem2

data Fin : Nat -> Set where
  fzero : {n : Nat} -> Fin (suc n)
  fsuc  : {n : Nat} -> Fin n -> Fin (suc n)

data False : Set where

-- 3.1

empty : Fin zero -> False
empty ()

-- 3.2

_!_ : {A : Set}{n : Nat} -> Vec A n -> Fin n -> A
ε        ! ()
(x ► xs) ! fzero  = x
(x ► xs) ! fsuc i = xs ! i

-- 3.3

-- The simply typed composition would do here, but the more
-- dependent version is more interesting.
-- _∘_ : {A B C : Set} -> (B -> C) -> (A -> B) -> A -> C

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

tabulate : {A : Set}{n : Nat} -> (Fin n -> A) -> Vec A n
tabulate {n = zero } f = ε
tabulate {n = suc n} f = f fzero ► tabulate (f ∘ fsuc)


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

open import Categories.Category
open import Categories.Category.Monoidal

module Categories.Category.Monoidal.Symmetric {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where

open import Level

open import Data.Product using (Σ; _,_)

open import Categories.Functor.Bifunctor
open import Categories.Functor.Properties
open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)

open import Categories.Morphism C
open import Categories.Morphism.Properties C
open import Categories.Category.Monoidal.Braided M
open Category C
open Commutation

private
  variable
    X Y Z : Obj

-- symmetric monoidal category
-- commutative braided monoidal category
--
-- the reason why we define symmetric categories via braided monoidal categories could
-- be not obvious, but it is the right definition: it requires again a redundant
-- hexagon proof which allows achieves definitional equality of the opposite.
record Symmetric : Set (levelOfTerm M) where
  field
    braided : Braided

  module braided = Braided braided
  open braided public

  private
    B : ∀ {X Y} → X ⊗₀ Y ⇒ Y ⊗₀ X
    B {X} {Y} = braiding.⇒.η (X , Y)

  field
    commutative : B {X} {Y} ∘ B {Y} {X} ≈ id

  braided-iso : X ⊗₀ Y ≅ Y ⊗₀ X
  braided-iso = record
    { from = B
    ; to   = B
    ; iso  = record
      { isoˡ = commutative
      ; isoʳ = commutative
      }
    }

  module braided-iso {X Y} = _≅_ (braided-iso {X} {Y})

private
  record Symmetric′ : Set (levelOfTerm M) where
    open Monoidal M

    field
      braiding : NaturalIsomorphism ⊗ (flip-bifunctor ⊗)

    module braiding = NaturalIsomorphism braiding

    private
      B : ∀ {X Y} → X ⊗₀ Y ⇒ Y ⊗₀ X
      B {X} {Y} = braiding.⇒.η (X , Y)

    field
      commutative : B {X} {Y} ∘ B {Y} {X} ≈ id
      hexagon     : [ (X ⊗₀ Y) ⊗₀ Z ⇒ Y ⊗₀ Z ⊗₀ X ]⟨
                      B  ⊗₁ id                    ⇒⟨ (Y ⊗₀ X) ⊗₀ Z ⟩
                      associator.from             ⇒⟨ Y ⊗₀ X ⊗₀ Z ⟩
                      id ⊗₁ B
                    ≈ associator.from             ⇒⟨ X ⊗₀ Y ⊗₀ Z ⟩
                      B                           ⇒⟨ (Y ⊗₀ Z) ⊗₀ X ⟩
                      associator.from
                    ⟩

    braided-iso : X ⊗₀ Y ≅ Y ⊗₀ X
    braided-iso = record
      { from = B
      ; to   = B
      ; iso  = record
        { isoˡ = commutative
        ; isoʳ = commutative
        }
      }

    module braided-iso {X Y} = _≅_ (braided-iso {X} {Y})

    -- we don't define [Symmetric] from [Braided] because we want to avoid asking
    -- [hexagon₂], which can readily be proven using the [hexagon] and [commutative].
    braided : Braided
    braided = record
      { braiding = braiding
      ; hexagon₁ = hexagon
      ; hexagon₂ = λ {X Y Z} →
                     Iso-≈ hexagon
                           (Iso-∘ (Iso-∘ ([ -⊗ Y ]-resp-Iso braided-iso.iso) associator.iso)
                                  ([ X ⊗- ]-resp-Iso braided-iso.iso))
                           (Iso-∘ (Iso-∘ associator.iso braided-iso.iso)
                                  associator.iso)
      }

symmetricHelper : Symmetric′ → Symmetric
symmetricHelper S = record
  { braided     = braided
  ; commutative = commutative
  }
  where open Symmetric′ S

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
{-# OPTIONS --without-K #-}
module hw1 where

open import Level using (_⊔_)
open import Function using (id)
open import Data.Nat using (ℕ; suc; _+_; _*_)
open import Data.Empty using (⊥)
open import Data.Sum using (_⊎_; inj₁; inj₂)

import Level

infix 4 _≡_

recℕ : ∀ {ℓ} → (C : Set ℓ) → C → (ℕ → C → C) → ℕ → C
recℕ C z f 0 = z
recℕ C z f (suc n) = f n (recℕ C z f n)

indℕ : ∀ {ℓ}
         → (C : ℕ → Set ℓ)
         → C 0
         → ((n : ℕ) → C n → C (suc n))
         → (n : ℕ)
         → C n
indℕ C z f 0 = z
indℕ C z f (suc n) = f n (indℕ C z f n)

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

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

rec≡ : {A : Set} →
       (R : A → A → Set) {reflexiveR : {a : A} → R a a} →
       ({x y : A} (p : x ≡ y) → R x y)
rec≡ R {reflR} (refl y) = reflR {y}

subst : ∀ {ℓ} {A : Set ℓ} {C : A → Set ℓ} →
        ({x y : A} (p : x ≡ y) → C x → C y)
subst (refl x) = id

------------------------------------------------------------------------------
-- Exercise 1.1
-- show h ∘ (g ∘ f) = (h ∘ g) ∘ f
------------------------------------------------------------------------------

_∘_ : {A B C : Set} → (f : B → C) → (g : A → B) → A → C
f ∘ g = (λ a → f (g a))

compose≡ : {A B C D : Set}
            → (f : A → B)
            → (g : B → C)
            → (h : C → D)
            → h ∘ (g ∘ f) ≡ (h ∘ g) ∘ f
compose≡ = λ f g h → refl (λ a → (h (g (f a))))

------------------------------------------------------------------------------
-- Exercise 1.2
-- Derive the recursion principle for products recA×B
-- using only the projections, and verify that the definitional
-- equalities are valid. Do the same for Σ-types.
------------------------------------------------------------------------------
---------------------------------------------------
-- Product Types
data _×_ {ℓ₁ ℓ₂} (A : Set ℓ₁) (B : Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
  pair : A → B → A × B

fst : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} → A × B → A
fst (pair a _) = a

snd : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂}  -> A × B -> B
snd (pair _ b) = b

rec× : ∀ {ℓ} {A B : Set ℓ}
       → (C : Set ℓ)
       → (A → B → C)
       → A × B → C
rec× c f = λ p -> (f (fst p) (snd p))

fstofab≡a : ∀ {A B : Set}
              (a : A)
              → (b : B)
              → fst (pair a b) ≡ a
fstofab≡a {A} {B} = λ a b → refl a

sndofab≡b : ∀ {A B : Set}
              (a : A)
              → (b : B)
              → snd (pair a b) ≡ b
sndofab≡b {A} {B} = λ a b → refl b

uniq× : ∀ {ℓ₁ ℓ₂}
          {A : Set ℓ₁}
          {B : Set ℓ₂}
          (p : A × B)
          → (pair (fst p) (snd p)) ≡ p
uniq× (pair a b) = refl (pair a b)

rec×g≡g : ∀ {A B C : Set}
            (g : A → B → C)
            (a : A)
            → (b : B)
            → rec× C g (pair a b) ≡ g a b
rec×g≡g {A} {B} {C} = λ g a b → refl (g a b)

recfst : ∀ (A B : Set)
           → fst {B = B} ≡ rec× A (λ a b → a)
recfst A B = refl fst

---------------------------------------------------
-- Sigma Types
data Σ {ℓ₁ ℓ₂} (A : Set ℓ₁)
               (B : A → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂)
     where dpair : (a : A) → (B a) → Σ A B

dfst : ∀ {A : Set} {B : A → Set} → Σ A B → A
dfst (dpair a _) = a

dsnd : ∀ {A : Set} {B : A → Set} → (p : Σ A B) → (B (dfst p))
dsnd (dpair _ b) = b

dfstofab≡a : ∀ {A : Set}
               {B : A → Set}
               (a : A)
               (b : B a) →
               dfst {B = B} (dpair a b) ≡ a
dfstofab≡a {A} {B} = λ a b → refl a

dsndofab≡a : ∀ {A : Set}
               {B : A → Set}
               (a : A)
               (b : B a) →
               dsnd {B = B} (dpair a b) ≡ b
dsndofab≡a {A} {B} = λ a b → refl b

uniqΣ : ∀ {A : Set}
          {B : A → Set}
          (p : Σ A B)
          → (dpair (dfst p) (dsnd p)) ≡ p
uniqΣ (dpair a b) = refl (dpair a b)

------------------------------------------------------------------------------
-- Exercise 1.3
-- Derive the induction principle for products indA×B,
-- using only the projections and the propositional uniqueness
-- principle uniqA×B. Verify that the definitional equalities are
-- valid. Generalize uniqA×B to Σ-types, and do the same for Σ-types.
------------------------------------------------------------------------------

ind× : ∀ {ℓ} {A : Set ℓ} {B : Set ℓ}
         → (C : (A × B) → Set ℓ)
         → ((a : A) (b : B) → (C (pair a b)))
         → (p : (A × B)) → (C p)
ind× = λ C f → λ p → subst {C = C}
                           (uniq× p)
                           (f (fst p) (snd p))

indΣ' : ∀  {A : Set} {B : A → Set} → (C : Σ A B → Set) →
        ((a : A) → (b : B a) → C (dpair a b)) → (p : Σ A B) → C p
indΣ' C g s = subst {C = C}
                    (uniqΣ s)
                    (g (dfst s) (dsnd s))

------------------------------------------------------------------------------
--- Exercise 1.4 Given the function iter, derive a function having the
--- type of the recursor recN. Show that the defining equations of the
--- recursor hold propositionally for this function, using the
--- induction principle for Nats.
------------------------------------------------------------------------------

iter : ∀ {ℓ} {C : Set ℓ} → C → (C → C) → ℕ → C
iter c₀ c₊ 0 = c₀
iter c₀ c₊ (suc n) = c₊ (iter c₀ c₊ n)

recℕ' : ∀ {ℓ} → (C : Set ℓ) → C → (ℕ → C → C) → ℕ → C
recℕ' C c₀ f n =
  snd (iter (pair 0 c₀)
            (λ nc →
                  (pair (suc (fst nc))
                        (f (fst nc) (snd nc))))
            n)

-- quick def and sanity check of fact via recℕ
fact = recℕ ℕ 1 (λ n nfact → (suc n) * nfact)
fact1 : fact 0 ≡ 1
fact1 = refl 1
fact5 : fact 5 ≡ 120
fact5 = refl 120

-- quick def and sanity check of fact via recℕ'
fact' = recℕ' ℕ 1 (λ n nfact → (suc n) * nfact)
fact'1 : fact' 0 ≡ 1
fact'1 = refl 1
fact'5 : fact' 5 ≡ 120
fact'5 = refl 120

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f (refl y) = refl (f y)

-- this _is_ valid but I haven't done enough Agda
-- to see how to prove this. I proved it in the Coq HoTT library...
-- https://github.com/andmkent/HoTT/blob/5f9faf5ef4ea21db249d6ad45bcee0adf97f8f9d/contrib/HoTTBookExercises.v#L124
postulate
  punt1 : ∀ {ℓ} (C : Set ℓ) →
           (c₀ : C) →
           (f : (ℕ → C → C)) →
           (n : ℕ) →
           recℕ C c₀ f (suc n) ≡ recℕ' C c₀ f (suc n)

recℕ≡recℕ' : ∀ {ℓ} (C : Set ℓ) →
           (c₀ : C) →
           (f : (ℕ → C → C)) →
           ((n : ℕ) → recℕ C c₀ f n ≡ recℕ' C c₀ f n)

recℕ≡recℕ' {ℓ} C c₀ f n =
  indℕ {ℓ = ℓ}
       (λ n → (((recℕ  {ℓ = ℓ} C c₀ f) n)
                ≡
               ((recℕ' {ℓ = ℓ} C c₀ f) n)))
       (refl c₀)
       (λ n IH → (punt1 C c₀ f n))
       n

------------------------------------------------------------------------------
--- Exercise 1.5 Show that if we define A + B Σ(x:2) rec2(U, A, B,
--- x), then we can give a definition of indA+B for which the
--- definitional equalities stated in §1.7 hold.
------------------------------------------------------------------------------

data 𝟚 : Set where
  true  : 𝟚
  false : 𝟚

rec𝟚 : ∀ {ℓ} → {C : Set ℓ} → C → C → 𝟚 → C
rec𝟚 th el false = el
rec𝟚 th el true = th

if_then_else_ : ∀ {ℓ} {C : Set ℓ} → 𝟚 → C → C → C
if b then X else Y = rec𝟚 X Y b

ind𝟚 : ∀ {ℓ} → {C : 𝟚 → Set ℓ} → C true → C false → (b : 𝟚) → C b
ind𝟚 th el false = el
ind𝟚 th el true = th

bsum : ∀ (A : Set) → (B : Set) → Set
bsum  A B = Σ 𝟚 (rec𝟚 A B)

injbs1 : ∀ (A : Set) → (B : Set) → A → bsum A B
injbs1 A B a =  dpair true a

injbs2 : ∀ (A : Set) → (B : Set) → B → bsum A B
injbs2 A B b =  dpair false b

recΣ : ∀ {ℓ₁ ℓ₂ ℓ₃} → {A : Set ℓ₁} {B : A → Set ℓ₂} → (C : Set ℓ₃) →
       ((a : A) → B a → C) → Σ A B → C
recΣ C g (dpair a b) = g a b

indΣ : ∀ {ℓ₁ ℓ₂ ℓ₃} → {A : Set ℓ₁} {B : A → Set ℓ₂} → (C : Σ A B → Set ℓ₃) →
        ((a : A) → (b : B a) → C (dpair a b)) → (p : Σ A B) → C p
indΣ C g (dpair a b) = g a b

indbsum : (A : Set) (B : Set) (C : (bsum A B → Set))
           → ((a : A) → (C (injbs1 A B a)))
           → ((b : B) → (C (injbs2 A B b)))
           → (a+b : bsum A B) → (C a+b)
indbsum A B C ca cb = indΣ C (ind𝟚 ca cb)
-- where ind𝟚's C = (λ b →  (t : rec𝟚 A B b) → C (dpair b t))

indbs1 : ∀ {A B : Set} (P : (bsum A B) → Set)
         → (fa : (a : A) → P (injbs1 A B a))
         → (fb : (b : B) → P (injbs2 A B b))
         → (a : A)
         → indbsum A B P fa fb (injbs1 A B a) ≡ fa a
indbs1 P fa fb x = refl (fa x)

indbs2 : ∀ {A B : Set} (P : (bsum A B) → Set)
         → (fa : (a : A) → P (injbs1 A B a))
         → (fb : (b : B) → P (injbs2 A B b))
         → (b : B)
         → indbsum A B P fa fb (injbs2 A B b) ≡ fb b
indbs2 P fa fb x = refl (fb x)

rec⊎ : ∀ {ℓ₁ ℓ₂ ℓ₃} → {A : Set ℓ₁} {B : Set ℓ₂} →
       (C : Set ℓ₃) → (A → C) → (B → C) → (A ⊎ B → C)
rec⊎ C f g (inj₁ a) = f a
rec⊎ C f g (inj₂ b) = g b

------------------------------------------------------------------------------
--- Exercise 1.10
-- Show that the Ackermann function ack : ℕ → ℕ → ℕ is definable using
-- only recℕ satisfying the following equations:
-- ack(0, m) = succ(m)  -> ack(0) = suc
-- ack(succ(n), 0) = ack(n, 1)  -> ack (suc n) =
-- ack(succ(n), succ(m)) = ack(n, ack(succ(n), m)).

ack : ℕ → ℕ → ℕ
ack = recℕ (ℕ → ℕ)
           suc
           (λ n ackn → recℕ ℕ (ackn 1) (λ m res → (ackn res)))

acktest00 : ack 0 0 ≡ 1
acktest00 = refl 1

acktest01 : ack 0 1 ≡ 2
acktest01 = refl 2

acktest10 : ack 1 0 ≡ 2
acktest10 = refl 2

acktest11 : ack 1 1 ≡ 3
acktest11 = refl 3

acktest22 : ack 2 2 ≡ 7
acktest22 = refl 7

------------------------------------------------------------------------------
--- Exercise 1.11
-- Show that for any type A, we have ¬¬¬A → ¬A.

¬ : Set → Set
¬ P = P → ⊥

ex11 : ∀ (P : Set) → ¬ (¬ (¬ P)) → ¬ P
ex11 P = λ nnnP → λ P → nnnP (λ nP → nP P)

------------------------------------------------------------------------------
-- Exercise 1.12
-- Using the propositions as types interpretation, derive the following tautologies.
-- (i) If A, then (if B then A).
-- (ii) If A, then not (not A).
-- (iii) If (not A or not B), then not (A and B).

ex12i : ∀ (A : Set) → A → (Set → A)
ex12i = λ A a _ → a

ex12ii : ∀ (A : Set) → A → (¬ (¬ A))
ex12ii = λ A a → λ nA → nA a

ex12iii : ∀ (A B : Set) → (¬ (A ⊎ B)) → (¬ (A × B))
ex12iii = λ A B → λ nAorB → λ AandB → nAorB (inj₁ (fst AandB))

------------------------------------------------------------------------------
-- Exercise 1.13
-- Using propositions-as-types, derive the double negation of the principle of ex-
-- cluded middle, i.e. prove not (not (P or not P)).

ex13 : ∀ (P : Set) → (¬ (¬ (P ⊎ (¬ P))))
ex13 = λ P nPorPnot → nPorPnot (inj₂ (λ P → nPorPnot (inj₁ P)))

------------------------------------------------------------------------------
-- Exercise 1.16
-- Show that addition of natural numbers is commutative.

ex16 : ∀ (a b c : ℕ) → a + (b + c) ≡ (a + b) + c
ex16 = indℕ (λ a → (b c : ℕ) → a + (b + c) ≡ a + b + c)
            (λ b c → refl (b + c))
            (λ n IHn b c → cong suc (IHn b c))

max_stars_repo_name: andmkent/misc-HoTT

max_issues_repo_name: andmkent/misc-HoTT

max_forks_repo_name: andmkent/misc-HoTT


text:
module Data.Either.Equiv.Id where

import      Lvl
open import Data
open import Data.Either as Either
open import Data.Either.Equiv
open import Relator.Equals
open import Relator.Equals.Proofs.Equiv
open import Structure.Setoid
open import Structure.Function.Domain
open import Type

private variable ℓ ℓₑ ℓₑ₁ ℓₑ₂ : Lvl.Level
private variable A B : Type{ℓ}

module _ ⦃ equiv-A : Equiv{ℓₑ₁}(A) ⦄ ⦃ equiv-B : Equiv{ℓₑ₂}(B) ⦄ where
  instance
    Left-injectivity : Injective(Left{A = A}{B = B})
    Injective.proof Left-injectivity [≡]-intro = [≡]-intro

  instance
    Right-injectivity : Injective(Right{A = A}{B = B})
    Injective.proof Right-injectivity [≡]-intro = [≡]-intro

  instance
    Either-Id-extensionality : Extensionality{A = A}{B = B} [≡]-equiv
    Either-Id-extensionality = intro \()

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


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

module SetInf where

id : ∀ {A} → A → A
id x = x

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
-- Andreas, 2018-06-14, issue #2513, surviving shape-irrelevance annotations.

record Foo (A : Set) : Set where
  field
    @shape-irrelevant foo : A

test : ∀ A → Foo A → A
test A = Foo.foo


text:
module context-properties where

open import utility
open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.Properties
open import Esterel.Lang.CanFunction
open import Esterel.Lang.CanFunction.Properties
  using (canₛ-⊆-FV ; canₛₕ-⊆-FV ; canθₛ-E₁⟦p⟧⊆canθₛ-p ; canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p)
open import Esterel.Environment
open import Esterel.Context
open import Esterel.Context.Properties public  -- 'public' for backward compatibility
open import Data.Product
  using (Σ ; Σ-syntax ; ∃ ; proj₁ ; proj₂ ; _,_ ; _,′_ ; _×_)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Data.Bool
  using (Bool ; true ; false ; if_then_else_)
open import Data.List
  using (List ; _∷_ ; [] ; _++_ ; map)
open import Data.List.Properties
  using (map-id ; map-cong ; map-compose)
open import Data.List.Any
  using (Any ; any ; here ; there)
open import Data.List.Any.Properties
  using ()
  renaming (++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ)
open import Data.Maybe
  using (Maybe ; just ; nothing)
open import Data.Nat
  using (ℕ ; zero ; suc ; _+_ ; _≟_)
open import Data.Nat.Properties.Simple
  using (+-comm)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import sn-calculus
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar ; _ᵥ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Function
  using (_∘_ ; id ; _∋_)

open import Data.OrderedListMap Signal Signal.unwrap Signal.Status as SigM
open import Data.OrderedListMap SharedVar SharedVar.unwrap (Σ SharedVar.Status (λ _ → ℕ)) as ShrM
open import Data.OrderedListMap SeqVar SeqVar.unwrap ℕ as SeqM

infix 20 _~_
infix 20 _a~_

data _~_ : EvaluationContext → EvaluationContext → Set where
  hole  : [] ~ []
  parr  : ∀{p p' E E'} → E ~ E' → (epar₁ p ∷ E) ~ (epar₁ p' ∷ E')
  parl  : ∀{p p' E E'} → E ~ E' → (epar₂ p ∷ E) ~ (epar₂ p' ∷ E')
  seq   : ∀{p p' E E'} → E ~ E' → (eseq p ∷ E) ~ (eseq p' ∷ E')
  loopˢ : ∀{p p' E E'} → E ~ E' → (eloopˢ p ∷ E) ~ (eloopˢ p' ∷ E')
  susp  : ∀{S E E'} → E ~ E' → (esuspend S ∷ E) ~ (esuspend S ∷ E')
  trp   : ∀{E E'} → E ~ E' → (etrap ∷ E) ~ (etrap ∷ E')

data R : Term → Set where
  mit  : ∀{S} → R (emit S)
  <==  : ∀{s e} → R (s ⇐ e)
  :==  : ∀{x e} → R (x ≔ e)
  pres : ∀{S p q} → R (present S ∣⇒ p ∣⇒ q)
  iff  : ∀{x p q} → R (if x ∣⇒ p ∣⇒ q)
  shrd : ∀{s e p} → R (shared s ≔ e in: p)
  varr : ∀{x e p} → R (var x ≔ e in: p)

~ref : (E : EvaluationContext) → E ~ E
~ref [] = hole
~ref (epar₁ q ∷ E) = parr (~ref E)
~ref (epar₂ p ∷ E) = parl (~ref E)
~ref (eseq q ∷ E) = seq (~ref E)
~ref (eloopˢ q ∷ E) = loopˢ (~ref E)
~ref (esuspend S ∷ E) = susp (~ref E)
~ref (etrap ∷ E) = trp (~ref E)

~sym : ∀{E1 E2} → E1 ~ E2 → E2 ~ E1
~sym hole = hole
~sym (parr eq) = parr (~sym eq)
~sym (parl eq) = parl (~sym eq)
~sym (seq eq) = seq (~sym eq)
~sym (loopˢ eq) = loopˢ (~sym eq)
~sym (susp eq) = susp (~sym eq)
~sym (trp eq) = trp (~sym eq)

~:: : ∀{E E' Ei} → (Ei ∷ E) ~ (Ei ∷ E') → E ~ E'
~:: (parr ~) = ~
~:: (parl ~) = ~
~:: (seq ~) = ~
~:: (loopˢ ~) = ~
~:: (susp ~) = ~
~:: (trp ~) = ~

CB-rho-rho-imp-dist : ∀{p q θ θ' BV FV A A'} → CorrectBinding ((ρ⟨ θ , A ⟩· p) ∥ (ρ⟨ θ' , A' ⟩· q)) BV FV → distinct (Dom θ) (Dom θ')
CB-rho-rho-imp-dist (CBpar{BVp = BVp}{BVq = BVq} (CBρ cb) (CBρ cb₁) x x₁ x₂ x₃) = dist++b x

ddb-r-rec : ∀{E' q BV FV θ θ' r s A A'} → CorrectBinding ((ρ⟨ θ , A ⟩· r) ∥ q) BV FV → q ≐ E' ⟦ (ρ⟨ θ' , A' ⟩· s) ⟧e → (distinct (Dom θ) (Dom θ'))

ddb-r-rec {[]} {ρ⟨ θ' , A' ⟩· p} (CBpar cb cb₁ x x₁ x₂ x₃) dehole = CB-rho-rho-imp-dist (CBpar cb cb₁ x x₁ x₂ x₃)
ddb-r-rec {.(epar₁ _) ∷ E'} (CBpar cb (CBpar cb₁ cb₂ x x₁ x₂ x₃) x₄ x₅ x₆ x₇) (depar₁ eq2)
  = ddb-r-rec {E'} (CBpar cb cb₁ (dist++ˡ x₄) (dist++ˡ x₅) (dist++ˡ x₆) (dist'++ˡ x₇)) eq2
ddb-r-rec {.(epar₂ _) ∷ E'} (CBpar cb (CBpar{BVp = BVp}{FVp = FVp@(S , s , xs)} cb₁ cb₂ x x₁ x₂ x₃) x₄ x₅ x₆ x₇) (depar₂ eq2)
  = ddb-r-rec {E'} (CBpar cb cb₂ (dist++ʳ{VL2 = BVp} x₄) (dist++ʳ{VL2 = BVp} x₅) (dist++ʳ{VL2 = FVp} x₆) (dist'++ʳ{V2 = xs} x₇)) eq2
ddb-r-rec {.(esuspend _) ∷ E'}{q = (suspend _ S)} (CBpar cb (CBsusp cb₁ x) x₁ x₂ x₃ x₄) (desuspend eq2)
  = ddb-r-rec {E'} (CBpar cb cb₁ x₁ x₂ (dist::{S = S} x₃) x₄) eq2
ddb-r-rec {.etrap ∷ E'} (CBpar cb (CBtrap cb₁) x₁ x₂ x₃ x₄) (detrap eq2)
  = ddb-r-rec {E'} (CBpar cb cb₁ x₁ x₂ x₃ x₄) eq2
ddb-r-rec {.(eseq _) ∷ E'} (CBpar cb (CBseq cb₁ cb₂ x) x₁ x₂ x₃ x₄) (deseq eq2)
  = ddb-r-rec ((CBpar cb cb₁ (dist++ˡ x₁) (dist++ˡ x₂) (dist++ˡ x₃) (dist'++ˡ x₄))) eq2
ddb-r-rec {.(eloopˢ _) ∷ E'} (CBpar cb (CBloopˢ cb₁ cb₂ x _) x₁ x₂ x₃ x₄) (deloopˢ eq2)
  = ddb-r-rec ((CBpar cb cb₁ (dist++ˡ x₁) (dist++ˡ x₂) (dist++ˡ x₃) (dist'++ˡ x₄))) eq2

dist++l2 : ∀{VL1 VL2 VL3} → (distinct (VL2 U̬ VL3) VL1) → (distinct VL2 VL1)
dist++l2 d = (distinct-sym (dist++ˡ (distinct-sym d)))
dist'++l2 : ∀{A VL1 VL2 VL3} → (distinct'{A} (VL2 ++ VL3) VL1) → (distinct' VL2 VL1)
dist'++l2 d = (distinct'-sym (dist'++ˡ (distinct'-sym d)))
dist++r2 : ∀{VL1 VL2 VL3} → (distinct (VL2 U̬ VL3) VL1) → (distinct VL3 VL1)
dist++r2{VL2 = VL2} d = (distinct-sym (dist++ʳ{VL2 = VL2} (distinct-sym d)))
dist'++r2 : ∀{A VL1 VL2 VL3} → (distinct'{A} (VL2 ++ VL3) VL1) → (distinct' VL3 VL1)
dist'++r2{VL2 = VL2} d = (distinct'-sym (dist'++ʳ{V2 = VL2} (distinct'-sym d)))

dist::2 :  ∀{VL1 VL2 S} → (distinct (+S S VL1) VL2) → (distinct VL1 VL2)
dist::2{S = S} d = (distinct-sym ( dist::{S = S} (distinct-sym d) ))

decomp-distinct-binding : ∀{E E' p q BV FV θ θ' r s A A'} → CorrectBinding (p ∥ q) BV FV → p ≐ E ⟦ (ρ⟨ θ , A ⟩· r) ⟧e → q ≐ E' ⟦ (ρ⟨ θ' , A' ⟩· s) ⟧e → (distinct (Dom θ) (Dom θ'))
decomp-distinct-binding {[]} {E} (CBpar cb cb₁ x₁ x₂ x₃ x₄) dehole eq2 = ddb-r-rec (CBpar cb cb₁ x₁ x₂ x₃ x₄) eq2
decomp-distinct-binding {x ∷ E} {[]} (CBpar cb cb₁ x₁ x₂ x₃ x₄) eq1 dehole = distinct-sym (ddb-r-rec {x ∷ E} (CBpar cb₁ cb (distinct-sym x₁) (distinct-sym x₃) (distinct-sym x₂) (distinct'-sym x₄)) eq1)
decomp-distinct-binding {.(epar₁ _) ∷ E} {x₁ ∷ E'} (CBpar{BVq = BVq} (CBpar cb cb₁ x x₂ x₃ x₄) cb₂ x₅ x₆ x₇ x₈) (depar₁ eq1) eq2
  = decomp-distinct-binding (CBpar cb cb₂ (dist++l2 x₅)  (dist++l2 x₆) (dist++l2 x₇) (dist'++l2 x₈)) eq1 eq2
decomp-distinct-binding {.(epar₂ _) ∷ E} {x₁ ∷ E'} (CBpar (CBpar{BVp = BVp}{FVp = FVp@(S , s , xs)}{BVq = BVq} cb cb₁ x x₂ x₃ x₄) cb₂ x₅ x₆ x₇ x₈) (depar₂ eq1) eq2
  = decomp-distinct-binding (CBpar cb₁ cb₂ (dist++r2{VL2 = BVp} x₅)  (dist++r2{VL2 = FVp} x₆) (dist++r2{VL2 = BVp} x₇) (dist'++r2{VL2 = xs} x₈)) eq1 eq2
decomp-distinct-binding {.(eseq _) ∷ E} {x₁ ∷ E'} (CBpar (CBseq cb cb₁ x) cb₂ x₂ x₃ x₄ x₅) (deseq eq1) eq2
  = decomp-distinct-binding {E} ((CBpar cb cb₂ (dist++l2 x₂) (dist++l2 x₃) (dist++l2 x₄) (dist'++l2 x₅))) eq1 eq2
decomp-distinct-binding {.(eloopˢ _) ∷ E} {x₁ ∷ E'} (CBpar (CBloopˢ cb cb₁ x _) cb₂ x₂ x₃ x₄ x₅) (deloopˢ eq1) eq2
  = decomp-distinct-binding {E} ((CBpar cb cb₂ (dist++l2 x₂) (dist++l2 x₃) (dist++l2 x₄) (dist'++l2 x₅))) eq1 eq2
decomp-distinct-binding {.(esuspend _) ∷ E} {x₁ ∷ E'} {p = (suspend _ S)}  (CBpar (CBsusp cb x) cb₁ x₂ x₃ x₄ x₅) (desuspend eq1) eq2
  = decomp-distinct-binding {E} (CBpar cb cb₁ x₂ ( (dist::2{S = S} x₃) ) x₄ x₅) eq1 eq2
decomp-distinct-binding {.etrap ∷ E} {x₁ ∷ E'} (CBpar (CBtrap cb) cb₁ x₂ x₃ x₄ x₅) (detrap eq1) eq2
  = decomp-distinct-binding ((CBpar cb cb₁ x₂ x₃ x₄ x₅)) eq1 eq2

data _a~_ : EvaluationContext → EvaluationContext → Set where
  parr  : ∀{p p' E E'} → E a~ E' → (epar₁ p ∷ E) a~ (epar₁ p' ∷ E')
  parl  : ∀{p p' E E'} → E a~ E' → (epar₂ p ∷ E) a~ (epar₂ p' ∷ E')
  seq   : ∀{p p' E E'} → E a~ E' → (eseq p ∷ E) a~ (eseq p' ∷ E')
  loopˢ : ∀{p p' E E'} → E a~ E' → (eloopˢ p ∷ E) a~ (eloopˢ p' ∷ E')
  susp  : ∀{S E E'} → E a~ E' → (esuspend S ∷ E) a~ (esuspend S ∷ E')
  trp   : ∀{E E'} → E a~ E' → (etrap ∷ E) a~ (etrap ∷ E')

  par   : ∀{p q E E'}  → (epar₂ p ∷ E) a~ (epar₁ q ∷ E')
  par2  : ∀{p q E E'}  → (epar₁ p ∷ E) a~ (epar₂ q ∷ E')

a~-sym : ∀{E E'} → E a~ E' → E' a~ E
a~-sym (parr ~) = parr (a~-sym ~)
a~-sym (parl ~) = parl (a~-sym ~)
a~-sym (seq ~) = seq (a~-sym ~)
a~-sym (loopˢ ~) = loopˢ (a~-sym ~)
a~-sym (susp ~) = susp (a~-sym ~)
a~-sym (trp ~) = trp (a~-sym ~)
a~-sym par = par2
a~-sym par2 = par

decomp-maint-bind : ∀{E E' p r s θ θ' BV FV A A'} → CorrectBinding p BV FV
                      → p ≐ E ⟦ (ρ⟨ θ , A ⟩· r ) ⟧e
                      → p ≐ E' ⟦ (ρ⟨ θ' , A' ⟩· s ) ⟧e
                      → (E ≡ E' × r ≡ s × θ ≡ θ' × A ≡ A') ⊎ ((distinct (Dom θ) (Dom θ')) × E a~ E')

decomp-maint-bind {[]} {[]} {.(ρ⟨ _ , _ ⟩· _)} bv dehole dehole = inj₁ (refl , refl , refl , refl)
decomp-maint-bind {[]} {x ∷ E'} {.(ρ⟨ _ , _ ⟩· _)} bv dehole ()
decomp-maint-bind {.(epar₁ _) ∷ E} {[]} {.(_ ∥ _)} bv (depar₁ d1) ()

decomp-maint-bind {.(epar₂ _) ∷ E} {[]} {.(_ ∥ _)} bv (depar₂ d1) ()
decomp-maint-bind {.(eseq _) ∷ E} {[]} {.(_ >> _)} bv (deseq d1) ()
decomp-maint-bind {.(eloopˢ _) ∷ E} {[]} {.(loopˢ _ _)} bv (deloopˢ d1) ()
decomp-maint-bind {.(esuspend _) ∷ E} {[]} {.(suspend _ _)} bv (desuspend d1) ()
decomp-maint-bind {.etrap ∷ E} {[]} {.(trap _)} bv (detrap d1) ()
decomp-maint-bind {(epar₁ q) ∷ E} {(epar₂ p) ∷ E'} {.(_ ∥ _)} bv (depar₁ d1) (depar₂ d2) = inj₂ ((decomp-distinct-binding bv d1 d2) ,  par2 )
decomp-maint-bind {.(epar₂ _) ∷ E} {.(epar₁ _) ∷ E'} {.(_ ∥ _)} bv (depar₂ d1) (depar₁ d2) with (decomp-distinct-binding bv d2 d1)
... | c = inj₂ ((distinct-sym c) , par)
decomp-maint-bind {.(epar₁ _) ∷ E} {.(epar₁ _) ∷ E'} {.(_ ∥ _)} (CBpar bv bv₁ x x₁ x₂ x₃) (depar₁ d1) (depar₁ d2) with decomp-maint-bind bv d1 d2
... | inj₁ (eq1 , eq2 , eq3 , eq4) rewrite eq1 | eq2 | eq3 | eq4 = inj₁ (refl , refl , refl , refl)
... | inj₂ (y , neg) = inj₂ (y , parr neg)
decomp-maint-bind {.(epar₂ _) ∷ E} {.(epar₂ _) ∷ E'} {.(_ ∥ _)} (CBpar bv bv₁ x x₁ x₂ x₃) (depar₂ d1) (depar₂ d2) with decomp-maint-bind bv₁ d1 d2
... | inj₁ (eq1 , eq2 , eq3 , eq4) rewrite eq1 | eq2 | eq3 | eq4 = inj₁ (refl , refl , refl , refl)
... | inj₂ (y , neg) = inj₂ (y , parl neg)
decomp-maint-bind {.(eseq _) ∷ E} {.(eseq _) ∷ E'} {.(_ >> _)} (CBseq bv bv₁ x) (deseq d1) (deseq d2) with decomp-maint-bind bv d1 d2
... | inj₁ (eq1 , eq2 , eq3 , eq4) rewrite eq1 | eq2 | eq3 | eq4 = inj₁ (refl , refl , refl , refl)
... | inj₂ (y , neg) = inj₂ (y , seq neg)
decomp-maint-bind {.(eloopˢ _) ∷ E} {.(eloopˢ _) ∷ E'} {.(loopˢ _ _)} (CBloopˢ bv bv₁ x _) (deloopˢ d1) (deloopˢ d2) with decomp-maint-bind bv d1 d2
... | inj₁ (eq1 , eq2 , eq3 , eq4) rewrite eq1 | eq2 | eq3 | eq4 = inj₁ (refl , refl , refl , refl)
... | inj₂ (y , neg) = inj₂ (y , loopˢ neg)
decomp-maint-bind {.(esuspend _) ∷ E} {.(esuspend _) ∷ E'} {.(suspend _ _)} (CBsusp bv x) (desuspend d1) (desuspend d2) with decomp-maint-bind bv d1 d2
... | inj₁ (eq1 , eq2 , eq3 , eq4) rewrite eq1 | eq2 | eq3 | eq4 = inj₁ (refl , refl , refl , refl)
... | inj₂ (y , neg) = inj₂ (y , susp neg)
decomp-maint-bind {.etrap ∷ E} {.etrap ∷ E'} {.(trap _)} (CBtrap bv) (detrap d1) (detrap d2) with decomp-maint-bind bv d1 d2
... | inj₁ (eq1 , eq2 , eq3 , eq4) rewrite eq1 | eq2 | eq3 | eq4 = inj₁ (refl , refl , refl , refl)
... | inj₂ (y , neg) = inj₂ (y , trp neg)

data ->E-view : ∀{p q pin qin E θ θ' A A'} → (ρ⟨ θ , A ⟩· p) sn⟶₁ (ρ⟨ θ' , A' ⟩· q) → p ≐ E ⟦ pin ⟧e →  q ≐ E ⟦ qin ⟧e → Set where
  vmerge :  ∀{θ₁ θ₂ r p E A A'' dec} → ∀{dec2 : E ⟦ p ⟧e ≐ E ⟦ p ⟧e} → (->E-view{A = A} (rmerge{θ₁}{θ₂}{r}{p}{E}{A}{A''} dec) dec dec2)
  vis-present : ∀{θ S r p q E S∈ ineq dec A} → ∀{dec2 : E ⟦ p ⟧e ≐ E ⟦ p ⟧e} → (->E-view{A = A} (ris-present{θ}{S}{r}{p}{q}{E} S∈ ineq dec) dec dec2)
  vis-absent : ∀{θ S r p q E S∈ ineq dec A} → ∀{dec2 : E ⟦ q ⟧e ≐ E ⟦ q ⟧e} → (->E-view{A = A} (ris-absent{θ}{S}{r}{p}{q}{E} S∈ ineq dec) dec dec2)
  vemit : ∀{θ r S E S∈ ¬S≡a dec} → ∀{dec2 : E ⟦ nothin ⟧e ≐ E ⟦ nothin ⟧e} → (->E-view (remit{θ}{r}{S}{E} S∈ ¬S≡a dec) dec dec2)
  vraise-shared : ∀{θ r s e p E e' dec A} → ∀{dec2 : E ⟦ (ρ⟨ (Θ SigMap.empty ShrMap.[ s ↦ (SharedVar.old ,′ (δ e'))] VarMap.empty) , WAIT ⟩· p) ⟧e ≐ E ⟦ (ρ⟨ (Θ SigMap.empty ShrMap.[ s ↦ (SharedVar.old ,′ (δ e'))] VarMap.empty) , WAIT ⟩· p) ⟧e}
                  → (->E-view{A = A} (rraise-shared{θ}{r}{s}{e}{p}{E} e' dec) dec dec2)
  vset-shared-value-old :  ∀{θ r s e E e' s∈ ineq dec} → ∀{dec2 : E ⟦ nothin ⟧e ≐ E ⟦ nothin ⟧e} → (->E-view (rset-shared-value-old{θ}{r}{s}{e}{E} e' s∈ ineq dec) dec dec2)
  vset-shared-value-new :  ∀{θ r s e E e' s∈ ineq dec} → ∀{dec2 : E ⟦ nothin ⟧e ≐ E ⟦ nothin ⟧e} → (->E-view (rset-shared-value-new{θ}{r}{s}{e}{E} e' s∈ ineq dec) dec dec2)
  vraise-var : ∀{θ r x p e E e' dec A} → ∀{dec2 : E ⟦ (ρ⟨ (Θ SigMap.empty ShrMap.empty VarMap.[ x ↦ δ e' ]) , WAIT ⟩· p) ⟧e ≐ E ⟦ (ρ⟨ (Θ SigMap.empty ShrMap.empty VarMap.[ x ↦ δ e' ]) , WAIT ⟩· p) ⟧e}
               → (->E-view{A = A} (rraise-var{θ}{r}{x}{p}{e}{E} e' dec) dec dec2)

  vset-var : ∀{θ r x e E x∈ e' dec A} → ∀{dec2 : E ⟦ nothin ⟧e ≐ E ⟦ nothin ⟧e}→  (->E-view{A = A} (rset-var{θ}{r}{x}{e}{E} x∈ e' dec) dec dec2)
  vif-false : ∀{θ r p q x E x∈ ineq dec A} → ∀{dec2 : E ⟦ q ⟧e ≐ E ⟦ q ⟧e} → (->E-view{A = A} (rif-false{θ}{r}{p}{q}{x}{E} x∈ ineq dec) dec dec2)
  vif-true : ∀{θ r p q x E n x∈ ineq dec A} → ∀{dec2 : E ⟦ p ⟧e ≐ E ⟦ p ⟧e} → (->E-view{A = A} (rif-true{θ}{r}{p}{q}{x}{E}{n} x∈ ineq dec) dec dec2)

data ->pot-view : ∀{p θ q θ' A A'} → (ρ⟨ θ , A ⟩· p) sn⟶₁ (ρ⟨ θ' , A' ⟩· q) → p ≡ q → A ≡ A' → Set where
  vabsence : ∀{θ p A} S S∈ θS≡unknown S∉can-p-θ → (->pot-view{A = A} (rabsence{θ}{p}{S} S∈ θS≡unknown S∉can-p-θ) refl refl)
  vreadyness : ∀{θ p A} s s∈ θs≡old⊎θs≡new s∉can-p-θ → (->pot-view{A = A} (rreadyness{θ}{p}{s} s∈ θs≡old⊎θs≡new s∉can-p-θ) refl refl)

data ->θview :  ∀{p θ q θ' A A'} → (ρ⟨ θ , A ⟩· p) sn⟶₁ (ρ⟨ θ' , A' ⟩· q) → Set where
  ->θE-view   :  ∀{p q pin qin E θ θ' A A'}
               → ∀{red : (ρ⟨ θ , A ⟩· p) sn⟶₁ (ρ⟨ θ' , A' ⟩· q)}
               → ∀{pin : p ≐ E ⟦ pin ⟧e}
               → ∀{qin : q ≐ E ⟦ qin ⟧e}
               → ->E-view red pin qin
               → ->θview red

  ->θpot-view : ∀{p θ q θ' A A'}
                → ∀{red : (ρ⟨ θ , A ⟩· p) sn⟶₁ (ρ⟨ θ' , A' ⟩· q)}
                → ∀{eq : p ≡ q}
                → ∀{eq2 : A ≡ A'}
                → ->pot-view red eq eq2
                → ->θview red

-- views for the term inside an ->E-view reduction
data ->E-view-term : Term → Set where
  evt-merge        : ∀ {θ p A}   → ->E-view-term (ρ⟨ θ , A ⟩· p)
  evt-present      : ∀ {S p q} → ->E-view-term (present S ∣⇒ p ∣⇒ q)
  evt-emit         : ∀ {S}     → ->E-view-term (emit S)
  evt-raise-shared : ∀ {s e p} → ->E-view-term (shared s ≔ e in: p)
  evt-set-shared   : ∀ {s e}   → ->E-view-term (s ⇐ e)
  evt-raise-var    : ∀ {x e p} → ->E-view-term (var x ≔ e in: p)
  evt-set-var      : ∀ {x e}   → ->E-view-term (x ≔ e)
  evt-if           : ∀ {x p q} → ->E-view-term (if x ∣⇒ p ∣⇒ q)

->E-view-inner-term : ∀ {E pin poin p po θ θo A Ao} →
  { p≐E⟦pin⟧       :  p  ≐ E ⟦ pin  ⟧e } →
  { po≐E⟦poin⟧     :  po ≐ E ⟦ poin ⟧e } →
  { ρθ·psn⟶₁ρθo·po  :  ρ⟨ θ , A ⟩· p sn⟶₁ ρ⟨ θo , Ao ⟩· po } →
  ->E-view  ρθ·psn⟶₁ρθo·po  p≐E⟦pin⟧  po≐E⟦poin⟧ →
  ->E-view-term pin
->E-view-inner-term vmerge                = evt-merge
->E-view-inner-term vis-present           = evt-present
->E-view-inner-term vis-absent            = evt-present
->E-view-inner-term vemit                 = evt-emit
->E-view-inner-term vraise-shared         = evt-raise-shared
->E-view-inner-term vset-shared-value-old = evt-set-shared
->E-view-inner-term vset-shared-value-new = evt-set-shared
->E-view-inner-term vraise-var            = evt-raise-var
->E-view-inner-term vset-var              = evt-set-var
->E-view-inner-term vif-false             = evt-if
->E-view-inner-term vif-true              = evt-if

-- terms inside the hole of an ->E-view cannot be done
done-E-view-term-disjoint : ∀ {p} → done p → ->E-view-term p → ⊥
done-E-view-term-disjoint (dhalted hnothin) ()
done-E-view-term-disjoint (dhalted (hexit n)) ()
done-E-view-term-disjoint (dpaused ppause) ()
done-E-view-term-disjoint (dpaused (pseq p/paused)) ()
done-E-view-term-disjoint (dpaused (ploopˢ p/paused)) ()
done-E-view-term-disjoint (dpaused (ppar p/paused q/paused)) ()
done-E-view-term-disjoint (dpaused (psuspend p/paused)) ()
done-E-view-term-disjoint (dpaused (ptrap p/paused)) ()

unwrap-rho : ∀{E₁ E p θ θ' pin q qin po qo A A'}
             → (red : (ρ⟨ θ , A ⟩· p) sn⟶₁ (ρ⟨ θ' , A' ⟩· q))
             → (peq : p ≐ (E₁ ∷ E) ⟦ pin ⟧e)
             → (qeq : q ≐ (E₁ ∷ E) ⟦ qin ⟧e)
             → (poeq : po ≐ E ⟦ pin ⟧e)
             → (qoeq : qo ≐ E ⟦ qin ⟧e)
             → (->E-view red peq qeq)
             → Σ[ redo ∈ (ρ⟨ θ , A ⟩· po) sn⟶₁ (ρ⟨ θ' , A' ⟩· qo) ] (->E-view redo poeq qoeq)
unwrap-rho{E = E}{θ = θ}{θ' = θ'}{qin = qin}{po = po} red@(rmerge{θ₁}{θ₂} .peq) peq qeq poeq qoeq (vmerge) with sym (unplug qoeq)
... | refl = rmerge poeq , vmerge{θ}{_}{po}{qin}{E}{_}{_}{poeq}
unwrap-rho (ris-present S∈ ineq .peq) peq qeq poeq qoeq vis-present with sym (unplug qoeq)
... | refl = (ris-present S∈ ineq poeq) , vis-present
unwrap-rho (ris-absent S∈ ineq .peq) peq qeq poeq qoeq vis-absent with sym (unplug qoeq)
... | refl = (ris-absent S∈ ineq poeq) , vis-absent
unwrap-rho (remit x eq .peq) peq qeq poeq qoeq vemit with sym (unplug qoeq)
... | refl = (remit x eq poeq) , vemit
unwrap-rho (rraise-shared x .peq) peq qeq poeq qoeq vraise-shared with sym (unplug qoeq)
... | refl = rraise-shared x poeq , vraise-shared
unwrap-rho (rset-shared-value-old a b c .peq) peq qeq poeq qoeq vset-shared-value-old with sym (unplug qoeq)
... | refl = (rset-shared-value-old a b c poeq) , vset-shared-value-old
unwrap-rho (rset-shared-value-new a b c .peq) peq qeq poeq qoeq vset-shared-value-new with sym (unplug qoeq)
... | refl = (rset-shared-value-new a b c poeq) , vset-shared-value-new
unwrap-rho (rraise-var a .peq) peq qeq poeq qoeq vraise-var with sym (unplug qoeq)
... | refl = (rraise-var a poeq) , vraise-var
unwrap-rho (rset-var a b .peq) peq qeq poeq qoeq vset-var with sym (unplug qoeq)
... | refl =  (rset-var a b poeq)  ,  vset-var
unwrap-rho (rif-false a b .peq) peq qeq poeq qoeq vif-false with sym (unplug qoeq)
... | refl = rif-false a b poeq , vif-false
unwrap-rho (rif-true a b .peq) peq qeq poeq qoeq vif-true with sym (unplug qoeq)
... | refl = rif-true a b poeq , vif-true

wrap-rho : ∀{θ θ' pout qout pin qin E po qo A A'}
           → (red : (ρ⟨ θ , A ⟩· pout) sn⟶₁ (ρ⟨ θ' , A' ⟩· qout))
           → (peq : pout ≐ E ⟦ pin ⟧e)
           → (qeq : qout ≐ E ⟦ qin ⟧e)
           → ->E-view red peq qeq
           → (E₁ : EvaluationContext1)
           → (poeq : po ≐ (E₁ ∷ E) ⟦ pin ⟧e)
           → (qoeq : qo ≐ (E₁ ∷ E) ⟦ qin ⟧e)
           → Σ[ redo ∈ (ρ⟨ θ , A ⟩· po) sn⟶₁ (ρ⟨ θ' , A' ⟩· qo) ] ->E-view redo poeq qoeq
wrap-rho .(rmerge peq) peq qeq vmerge Eo poeq qoeq with sym (unplug qoeq)
... | refl = rmerge poeq , vmerge
wrap-rho (ris-present S∈ ineq .peq) peq qeq vis-present Eo poeq qoeq with sym (unplug qoeq)
... | refl = ris-present S∈ ineq poeq , vis-present
wrap-rho (ris-absent S∈ ineq .peq) peq qeq vis-absent Eo poeq qoeq with sym (unplug qoeq)
... | refl = ris-absent S∈ ineq poeq , vis-absent
wrap-rho (remit S∈ eq .peq) peq qeq vemit Eo poeq qoeq with sym (unplug qoeq)
... | refl = remit S∈ eq poeq , vemit
wrap-rho (rraise-shared a .peq) peq qeq vraise-shared Eo poeq qoeq with sym (unplug qoeq)
... | refl = rraise-shared a poeq , vraise-shared
wrap-rho (rset-shared-value-old a b c .peq) peq qeq vset-shared-value-old Eo poeq qoeq with sym (unplug qoeq)
... | refl = rset-shared-value-old a b c poeq , vset-shared-value-old
wrap-rho (rset-shared-value-new a b c .peq) peq qeq vset-shared-value-new Eo poeq qoeq with sym (unplug qoeq)
... | refl = rset-shared-value-new a b c poeq , vset-shared-value-new
wrap-rho (rraise-var a .peq) peq qeq vraise-var Eo poeq qoeq with sym (unplug qoeq)
... | refl = rraise-var a poeq , vraise-var
wrap-rho (rset-var a b .peq) peq qeq vset-var Eo poeq qoeq with sym (unplug qoeq)
... | refl = rset-var a b poeq , vset-var
wrap-rho (rif-false a b .peq) peq qeq vif-false Eo poeq qoeq with sym (unplug qoeq)
... | refl = rif-false a b poeq , vif-false
wrap-rho (rif-true a b .peq) peq qeq vif-true Eo poeq qoeq with sym (unplug qoeq)
... | refl = rif-true a b poeq , vif-true

wrap-rho-pot : ∀ {E₁ pin θ θ' pin≡pin E₁⟦nothin⟧ BV FV A A≡A} →
  -- distinct (Dom θ) (FV (E₁ ⟦ nothin ⟧))
  E₁⟦nothin⟧ ≐ (E₁ ∷ []) ⟦ nothin ⟧e →
  CorrectBinding E₁⟦nothin⟧ BV FV →
  distinct (Dom θ) FV →

  (ρθpinsn⟶₁ρθ'qin  :  ρ⟨ θ , A ⟩· pin sn⟶₁ ρ⟨ θ' , A ⟩· pin) →
  ->pot-view  ρθpinsn⟶₁ρθ'qin  pin≡pin A≡A →

  ∃ λ po →
    Σ[ po≐E₁⟦pin⟧             ∈  po ≐ (E₁ ∷ []) ⟦ pin ⟧e ]
    Σ[ ρθE₁⟦pin⟧sn⟶₁ρθ'E₁⟦pin⟧  ∈  ρ⟨ θ , A ⟩· po sn⟶₁ ρ⟨ θ' , A ⟩· po ]
      ->pot-view  ρθE₁⟦pin⟧sn⟶₁ρθ'E₁⟦pin⟧ refl refl
wrap-rho-pot {epar₁ q} {pin} {θ} {FV = FV} (depar₁ dehole) cb Domθ≠FV
  .(rabsence {S = S} S∈ θS≡unknown S∉canθ-θ-p)
  (vabsence S S∈ θS≡unknown S∉canθ-θ-p)
  = _ , depar₁ dehole ,
    rabsence {S = S} S∈ θS≡unknown S∉canθ-θ-E₁⟦p⟧-[]env ,
    vabsence S S∈ θS≡unknown S∉canθ-θ-E₁⟦p⟧-[]env
  where
    S∉canθ-θ-E₁⟦p⟧-[]env =
      S∉canθ-θ-p ∘
      canθₛ-E₁⟦p⟧⊆canθₛ-p (sig θ) 0 []env (depar₁ dehole) cb
        (subst (λ dom → distinct' dom (proj₁ FV))
          (sym (map-id (proj₁ (Dom θ))))
          (proj₁ Domθ≠FV))
        S (proj₁ Domθ≠FV (Signal.unwrap S) S∈)
wrap-rho-pot {epar₂ p} {pin} {θ} {FV = FV} (depar₂ dehole) cb Domθ≠FV
  .(rabsence {S = S} S∈ θS≡unknown S∉can-p-θ)
  (vabsence S S∈ θS≡unknown S∉can-p-θ)
  = _ , depar₂ dehole ,
    rabsence {S = S} S∈ θS≡unknown S∉canθ-θ-E₁⟦p⟧-[]env ,
    vabsence S S∈ θS≡unknown S∉canθ-θ-E₁⟦p⟧-[]env
  where
    S∉canθ-θ-E₁⟦p⟧-[]env =
      S∉can-p-θ ∘
      canθₛ-E₁⟦p⟧⊆canθₛ-p (sig θ) 0 []env (depar₂ dehole) cb
        (subst (λ dom → distinct' dom (proj₁ FV))
          (sym (map-id (proj₁ (Dom θ))))
          (proj₁ Domθ≠FV))
        S (proj₁ Domθ≠FV (Signal.unwrap S) S∈)
wrap-rho-pot {eseq q} {pin} {θ} {FV = FV} (deseq dehole) cb Domθ≠FV
  .(rabsence {S = S} S∈ θS≡unknown S∉can-p-θ)
  (vabsence S S∈ θS≡unknown S∉can-p-θ)
  = _ , deseq dehole ,
    rabsence {S = S} S∈ θS≡unknown S∉canθ-θ-E₁⟦p⟧-[]env ,
    vabsence S S∈ θS≡unknown S∉canθ-θ-E₁⟦p⟧-[]env
  where
    S∉canθ-θ-E₁⟦p⟧-[]env =
      S∉can-p-θ ∘
      canθₛ-E₁⟦p⟧⊆canθₛ-p (sig θ) 0 []env (deseq dehole) cb
        (subst (λ dom → distinct' dom (proj₁ FV))
          (sym (map-id (proj₁ (Dom θ))))
          (proj₁ Domθ≠FV))
        S (proj₁ Domθ≠FV (Signal.unwrap S) S∈)
wrap-rho-pot {eloopˢ q} {pin} {θ} {FV = FV} (deloopˢ dehole) cb Domθ≠FV
  .(rabsence {S = S} S∈ θS≡unknown S∉can-p-θ)
  (vabsence S S∈ θS≡unknown S∉can-p-θ)
  = _ , deloopˢ dehole ,
    rabsence {S = S} S∈ θS≡unknown S∉canθ-θ-E₁⟦p⟧-[]env ,
    vabsence S S∈ θS≡unknown S∉canθ-θ-E₁⟦p⟧-[]env
  where
    S∉canθ-θ-E₁⟦p⟧-[]env =
      S∉can-p-θ ∘
      canθₛ-E₁⟦p⟧⊆canθₛ-p (sig θ) 0 []env (deloopˢ dehole) cb
        (subst (λ dom → distinct' dom (proj₁ FV))
          (sym (map-id (proj₁ (Dom θ))))
          (proj₁ Domθ≠FV))
        S (proj₁ Domθ≠FV (Signal.unwrap S) S∈)
wrap-rho-pot {esuspend S'} {pin} {θ} {FV = FV} (desuspend dehole) cb Domθ≠FV
  .(rabsence {S = S} S∈ θS≡unknown S∉can-p-θ)
  (vabsence S S∈ θS≡unknown S∉can-p-θ)
  = _ , desuspend dehole ,
    rabsence {S = S} S∈ θS≡unknown S∉canθ-θ-E₁⟦p⟧-[]env ,
    vabsence S S∈ θS≡unknown S∉canθ-θ-E₁⟦p⟧-[]env
  where
    S∉canθ-θ-E₁⟦p⟧-[]env =
      S∉can-p-θ ∘
      canθₛ-E₁⟦p⟧⊆canθₛ-p (sig θ) 0 []env (desuspend dehole) cb
        (subst (λ dom → distinct' dom (proj₁ FV))
          (sym (map-id (proj₁ (Dom θ))))
          (proj₁ Domθ≠FV))
        S (proj₁ Domθ≠FV (Signal.unwrap S) S∈)
wrap-rho-pot {etrap} {pin} {θ} {FV = FV} (detrap dehole) cb Domθ≠FV
  .(rabsence {S = S} S∈ θS≡unknown S∉can-p-θ)
  (vabsence S S∈ θS≡unknown S∉can-p-θ)
  = _ , detrap dehole ,
    rabsence {S = S} S∈ θS≡unknown S∉canθ-θ-E₁⟦p⟧-[]env ,
    vabsence S S∈ θS≡unknown S∉canθ-θ-E₁⟦p⟧-[]env
  where
    S∉canθ-θ-E₁⟦p⟧-[]env =
      S∉can-p-θ ∘
      canθₛ-E₁⟦p⟧⊆canθₛ-p (sig θ) 0 []env (detrap dehole) cb
        (subst (λ dom → distinct' dom (proj₁ FV))
          (sym (map-id (proj₁ (Dom θ))))
          (proj₁ Domθ≠FV))
        S (proj₁ Domθ≠FV (Signal.unwrap S) S∈)
wrap-rho-pot {epar₁ q} {pin} {θ} {FV = FV} (depar₁ dehole) cb Domθ≠FV
  .(rreadyness {s = s} s∈ θs≡old⊎θs≡new s∉can-p-θ)
  (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
  = _ , depar₁ dehole ,
    rreadyness {s = s} s∈ θs≡old⊎θs≡new s∉canθ-θ-E₁⟦p⟧-[]env ,
    vreadyness s s∈ θs≡old⊎θs≡new s∉canθ-θ-E₁⟦p⟧-[]env
  where
    s∉canθ-θ-E₁⟦p⟧-[]env =
      s∉can-p-θ ∘
      canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p (sig θ) 0 []env (depar₁ dehole) cb
        (subst (λ dom → distinct' dom (proj₁ FV))
          (sym (map-id (proj₁ (Dom θ))))
          (proj₁ Domθ≠FV))
        s (proj₁ (proj₂ Domθ≠FV) (SharedVar.unwrap s) s∈)
wrap-rho-pot {epar₂ p} {pin} {θ} {FV = FV} (depar₂ dehole) cb Domθ≠FV
  .(rreadyness {s = s} s∈ θs≡old⊎θs≡new s∉can-p-θ)
  (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
  = _ , depar₂ dehole ,
    rreadyness {s = s} s∈ θs≡old⊎θs≡new s∉canθ-θ-E₁⟦p⟧-[]env ,
    vreadyness s s∈ θs≡old⊎θs≡new s∉canθ-θ-E₁⟦p⟧-[]env
  where
    s∉canθ-θ-E₁⟦p⟧-[]env =
      s∉can-p-θ ∘
      canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p (sig θ) 0 []env (depar₂ dehole) cb
        (subst (λ dom → distinct' dom (proj₁ FV))
          (sym (map-id (proj₁ (Dom θ))))
          (proj₁ Domθ≠FV))
        s (proj₁ (proj₂ Domθ≠FV) (SharedVar.unwrap s) s∈)
wrap-rho-pot {eseq q} {pin} {θ} {FV = FV} (deseq dehole) cb Domθ≠FV
  .(rreadyness {s = s} s∈ θs≡old⊎θs≡new s∉can-p-θ)
  (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
  = _ , deseq dehole ,
    rreadyness {s = s} s∈ θs≡old⊎θs≡new s∉canθ-θ-E₁⟦p⟧-[]env ,
    vreadyness s s∈ θs≡old⊎θs≡new s∉canθ-θ-E₁⟦p⟧-[]env
  where
    s∉canθ-θ-E₁⟦p⟧-[]env =
      s∉can-p-θ ∘
      canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p (sig θ) 0 []env (deseq dehole) cb
        (subst (λ dom → distinct' dom (proj₁ FV))
          (sym (map-id (proj₁ (Dom θ))))
          (proj₁ Domθ≠FV))
        s (proj₁ (proj₂ Domθ≠FV) (SharedVar.unwrap s) s∈)
wrap-rho-pot {eloopˢ q} {pin} {θ} {FV = FV} (deloopˢ dehole) cb Domθ≠FV
  .(rreadyness {s = s} s∈ θs≡old⊎θs≡new s∉can-p-θ)
  (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
  = _ , deloopˢ dehole ,
    rreadyness {s = s} s∈ θs≡old⊎θs≡new s∉canθ-θ-E₁⟦p⟧-[]env ,
    vreadyness s s∈ θs≡old⊎θs≡new s∉canθ-θ-E₁⟦p⟧-[]env
  where
    s∉canθ-θ-E₁⟦p⟧-[]env =
      s∉can-p-θ ∘
      canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p (sig θ) 0 []env (deloopˢ dehole) cb
        (subst (λ dom → distinct' dom (proj₁ FV))
          (sym (map-id (proj₁ (Dom θ))))
          (proj₁ Domθ≠FV))
        s (proj₁ (proj₂ Domθ≠FV) (SharedVar.unwrap s) s∈)
wrap-rho-pot {esuspend S} {pin} {θ} {FV = FV} (desuspend dehole) cb Domθ≠FV
  .(rreadyness {s = s} s∈ θs≡old⊎θs≡new s∉can-p-θ)
  (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
  = _ , desuspend dehole ,
    rreadyness {s = s} s∈ θs≡old⊎θs≡new s∉canθ-θ-E₁⟦p⟧-[]env ,
    vreadyness s s∈ θs≡old⊎θs≡new s∉canθ-θ-E₁⟦p⟧-[]env
  where
    s∉canθ-θ-E₁⟦p⟧-[]env =
      s∉can-p-θ ∘
      canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p (sig θ) 0 []env (desuspend dehole) cb
        (subst (λ dom → distinct' dom (proj₁ FV))
          (sym (map-id (proj₁ (Dom θ))))
          (proj₁ Domθ≠FV))
        s (proj₁ (proj₂ Domθ≠FV) (SharedVar.unwrap s) s∈)
wrap-rho-pot {etrap} {pin} {θ} {FV = FV} (detrap dehole) cb Domθ≠FV
  .(rreadyness {s = s} s∈ θs≡old⊎θs≡new s∉can-p-θ)
  (vreadyness s s∈ θs≡old⊎θs≡new s∉can-p-θ)
  = _ , detrap dehole ,
    rreadyness {s = s} s∈ θs≡old⊎θs≡new s∉canθ-θ-E₁⟦p⟧-[]env ,
    vreadyness s s∈ θs≡old⊎θs≡new s∉canθ-θ-E₁⟦p⟧-[]env
  where
    s∉canθ-θ-E₁⟦p⟧-[]env =
      s∉can-p-θ ∘
      canθₛₕ-E₁⟦p⟧⊆canθₛₕ-p (sig θ) 0 []env (detrap dehole) cb
        (subst (λ dom → distinct' dom (proj₁ FV))
          (sym (map-id (proj₁ (Dom θ))))
          (proj₁ Domθ≠FV))
        s (proj₁ (proj₂ Domθ≠FV) (SharedVar.unwrap s) s∈)

-- p and p' are not important at all; we use them to extract the
-- distinctness condition of FV E₁ and Dom θ
wrap-rho-pot' : ∀ {θ θ' E₁ E pin p p' BV FV A} →
  p ≐ (E₁ ∷ E) ⟦ ρ⟨ θ , A ⟩· p' ⟧e →
  CorrectBinding p BV FV →

  (ρθpinsn⟶₁ρθ'pin  :  ρ⟨ θ , A ⟩· pin sn⟶₁ ρ⟨ θ' , A ⟩· pin) →
  ->pot-view  ρθpinsn⟶₁ρθ'pin  refl refl →

  ∃ λ po →
    Σ[ po≐E₁⟦pin⟧             ∈  po ≐ (E₁ ∷ []) ⟦ pin ⟧e ]
    Σ[ ρθE₁⟦pin⟧sn⟶₁ρθ'E₁⟦pin⟧  ∈  ρ⟨ θ , A ⟩· po sn⟶₁ ρ⟨ θ' , A ⟩· po ]
      ->pot-view  ρθE₁⟦pin⟧sn⟶₁ρθ'E₁⟦pin⟧ refl refl
wrap-rho-pot' {θ} (depar₁ p≐E⟦ρθp'⟧) (CBpar cbp cbq _ _ BVp≠FVq _) ρθpinsn⟶₁ρθ'pin pot
  with binding-extract cbp p≐E⟦ρθp'⟧
... | (BVρθ , _) , (BVρθ⊆BVp , _) , CBρ _ =
  wrap-rho-pot (depar₁ dehole) cb' (⊆-respect-distinct-left (∪-unjoin-⊆ˡ {xs³ = Dom θ} BVρθ⊆BVp) BVp≠FVq) ρθpinsn⟶₁ρθ'pin pot
  where cb' = CBpar CBnothing cbq distinct-empty-left distinct-empty-left distinct-empty-left (λ _ ())
wrap-rho-pot' {θ} (depar₂ q≐E⟦ρθp'⟧) (CBpar cbp cbq _ FVp≠BVq _ _) ρθpinsn⟶₁ρθ'pin pot
  with binding-extract cbq q≐E⟦ρθp'⟧
... | (BVρθ , _) , (BVρθ⊆BVq , _) , CBρ _ = -- Test your eyesight :  1) ⊃   2) ∪   3) ⊂   4) ∩
  wrap-rho-pot (depar₂ dehole) cb' -- hack to delete (_∪ base) in (distinct  (FVq ∪ base))
    (⊆-respect-distinct-right (∪-join-⊆ ⊆-refl ⊆-empty-left) -- using (FVq ∪ base) ⊆ FVq here
      (⊆-respect-distinct-left (∪-unjoin-⊆ˡ {xs³ = Dom θ} BVρθ⊆BVq) (distinct-sym FVp≠BVq)))
    ρθpinsn⟶₁ρθ'pin pot
  where cb' = CBpar cbp CBnothing distinct-empty-right distinct-empty-right distinct-empty-right (λ _ _ ())
wrap-rho-pot' {θ} (deseq p≐E⟦ρθp'⟧) (CBseq cbp cbq BVp≠FVq) ρθpinsn⟶₁ρθ'pin pot
  with binding-extract cbp p≐E⟦ρθp'⟧
... | (BVρθ , _) , (BVρθ⊆BVp , _) , CBρ _ =
  wrap-rho-pot (deseq dehole) cb' (⊆-respect-distinct-left (∪-unjoin-⊆ˡ {xs³ = Dom θ} BVρθ⊆BVp) BVp≠FVq) ρθpinsn⟶₁ρθ'pin pot
  where cb' = CBseq CBnothing cbq distinct-empty-left
wrap-rho-pot' {θ} (deloopˢ p≐E⟦ρθp'⟧) (CBloopˢ cbp cbq BVp≠FVq BVq≠FVq) ρθpinsn⟶₁ρθ'pin pot
  with binding-extract cbp p≐E⟦ρθp'⟧
... | (BVρθ , _) , (BVρθ⊆BVp , _) , CBρ _ =
  wrap-rho-pot (deloopˢ dehole) cb' (⊆-respect-distinct-left (∪-unjoin-⊆ˡ {xs³ = Dom θ} BVρθ⊆BVp) BVp≠FVq) ρθpinsn⟶₁ρθ'pin pot
  where cb' = CBloopˢ CBnothing cbq distinct-empty-left BVq≠FVq
wrap-rho-pot' {θ} (desuspend p≐E⟦ρθp'⟧) (CBsusp cb [S]≠BVp) ρθpinsn⟶₁ρθ'pin pot
  with binding-extract cb p≐E⟦ρθp'⟧
... | (BVρθ , _) , (BVρθ⊆BVp , _) , CBρ _ =
  wrap-rho-pot (desuspend dehole) cb'
    ((distinct'-sym (⊆¹-respect-distinct'-right
                      (proj₁ (∪¹-unjoin-⊆¹ (proj₁ (Dom θ)) (proj₁ BVρθ⊆BVp))) [S]≠BVp)) ,′
     (λ _ _ ()) ,′ (λ _ _ ()))
    ρθpinsn⟶₁ρθ'pin pot
  where cb' = CBsusp CBnothing (λ _ _ ())
wrap-rho-pot' {θ} (detrap p≐E⟦ρθp'⟧) cb@(CBtrap cb') ρθpinsn⟶₁ρθ'pin pot =
  wrap-rho-pot (detrap dehole) (CBtrap CBnothing) distinct-empty-right ρθpinsn⟶₁ρθ'pin pot

E-view-main-bind : ∀{El Er p il ir iol ior ql qr θ θl θr A Al Ar}
                    → ∀{redl : (ρ⟨ θ , A ⟩· p) sn⟶₁ (ρ⟨ θl , Al ⟩· ql) }
                    → ∀{redr : (ρ⟨ θ , A ⟩· p) sn⟶₁ (ρ⟨ θr , Ar ⟩· qr) }
                    → ∀{dec1l : p  ≐ El ⟦ il ⟧e}
                    → ∀{dec2l : ql ≐ El ⟦ iol ⟧e}
                    → ∀{dec1r : p  ≐ Er ⟦ ir ⟧e}
                    → ∀{dec2r : qr ≐ Er ⟦ ior ⟧e}
                    → ->E-view redl dec1l dec2l
                    → ->E-view redr dec1r dec2r
                    → (El ≡ Er × ql ≡ qr × θl ≡ θr × Al ≡ Ar) ⊎ (El a~ Er)

E-view-main-bind {epar₁ q ∷ El} {epar₂ p ∷ Er} v1 v2 = inj₂ par2
E-view-main-bind {epar₂ p ∷ El} {epar₁ q ∷ Er} v1 v2 = inj₂ par
E-view-main-bind {[]} {[]} {(present S ∣⇒ _ ∣⇒ _)}{θ = θ} {redl = (ris-present ∈1 eq1 dehole)} {(ris-absent ∈2 eq2 dehole)} {dehole} {dehole} {dehole} {dehole} vis-present vis-absent with sig-stats-∈-irr{S}{θ} ∈1 ∈2
... | k with trans (sym (trans k eq2)) eq1
... | ()
E-view-main-bind {[]} {[]} {(present S ∣⇒ _ ∣⇒ _)}{θ = θ} {redl = (ris-absent ∈1 eq1 dehole)} {(ris-present ∈2 eq2 dehole)} {dehole} {dehole} {dehole} {dehole} vis-absent vis-present with sig-stats-∈-irr{S}{θ} ∈1 ∈2
... | k with trans (sym (trans k eq2)) eq1
... | ()
E-view-main-bind {[]} {[]} {(if x ∣⇒ _ ∣⇒ _)}{θ = θ} {redl = (rif-false ∈1 eq1 dehole)} {(rif-true ∈2 eq2 dehole)} {dehole} {dehole} {dehole} {dehole} vif-false vif-true with var-vals-∈-irr{x}{θ} ∈1 ∈2
... | k with trans (sym (trans k eq2)) eq1
... | ()
E-view-main-bind {[]} {[]} {(if x ∣⇒ _ ∣⇒ _)}{θ = θ} {redl = (rif-true ∈1 eq1 dehole)} {(rif-false ∈2 eq2 dehole)} {dehole} {dehole} {dehole} {dehole} vif-true vif-false with var-vals-∈-irr{x}{θ} ∈1 ∈2
... | k with trans (sym (trans k eq2)) eq1
... | ()
E-view-main-bind {[]} {[]} {(s ⇐ _)}{θ = θ} {redl = (rset-shared-value-new _ ∈1 eq1 dehole)} {(rset-shared-value-old _ ∈2 eq2 dehole)} {dehole} {dehole} {dehole} {dehole} vset-shared-value-new vset-shared-value-old
  with shr-stats-∈-irr{s}{θ} ∈1 ∈2
... | k with trans (sym (trans k eq2)) eq1
... | ()
E-view-main-bind {[]} {[]} {(s ⇐ _)}{θ = θ} {redl = (rset-shared-value-old _ ∈1 eq1 dehole)} {(rset-shared-value-new _ ∈2 eq2 dehole)} {dehole} {dehole} {dehole} {dehole} vset-shared-value-old vset-shared-value-new   with shr-stats-∈-irr{s}{θ} ∈1 ∈2
... | k with trans (sym (trans k eq2)) eq1
... | ()

E-view-main-bind {[]} {[]} {.(ρ⟨ _ , _ ⟩· _)} {redl = .(rmerge dehole)} {.(rmerge dehole)} {dehole} {dehole} {dehole} {dehole} vmerge vmerge = inj₁ (refl , refl , refl , refl)
E-view-main-bind {[]} {[]} {.(present _ ∣⇒ _ ∣⇒ _)} {redl = .(ris-present _ _ dehole)} {.(ris-present _ _ dehole)} {dehole} {dehole} {dehole} {dehole} vis-present vis-present = inj₁ (refl , refl , refl , refl)
E-view-main-bind {[]} {[]} {.(present _ ∣⇒ _ ∣⇒ _)} {redl = .(ris-absent _ _ dehole)} {.(ris-absent _ _ dehole)} {dehole} {dehole} {dehole} {dehole} vis-absent vis-absent = inj₁ (refl , refl , refl , refl)
E-view-main-bind {[]} {[]} {.(emit _)} {redl = .(remit _ _ dehole)} {.(remit _ _ dehole)} {dehole} {dehole} {dehole} {dehole} vemit vemit = inj₁ (refl , refl , refl , refl)
E-view-main-bind {[]} {[]} {.(shared _ ≔ _ in: _)} {redl = (rraise-shared e' dehole)} {(rraise-shared e'' dehole)} {dehole} {dehole} {dehole} {dehole} vraise-shared vraise-shared
  rewrite δ-e-irr e' e'' = inj₁ (refl , refl , refl , refl)
E-view-main-bind {[]} {[]} {.(_ ⇐ _)} {redl = (rset-shared-value-old e' _ _ dehole)} {(rset-shared-value-old e'' _ _ dehole)} {dehole} {dehole} {dehole} {dehole} vset-shared-value-old vset-shared-value-old
   rewrite δ-e-irr e' e'' = inj₁ (refl , refl , refl , refl)
E-view-main-bind {[]} {[]} {(s ⇐ _)}{θ = θ} {redl = (rset-shared-value-new e' s∈' _ dehole)} {(rset-shared-value-new e'' s∈'' _ dehole)} {dehole} {dehole} {dehole} {dehole} vset-shared-value-new vset-shared-value-new
   rewrite δ-e-irr e' e'' | (shr-vals-∈-irr{s}{θ} s∈' s∈'') = inj₁ (refl , refl , refl , refl)
E-view-main-bind {[]} {[]} {.(var _ ≔ _ in: _)} {redl = (rraise-var e' dehole)} {(rraise-var e'' dehole)} {dehole} {dehole} {dehole} {dehole} vraise-var vraise-var
   rewrite δ-e-irr e' e'' = inj₁ (refl , refl , refl , refl)
E-view-main-bind {[]} {[]} {(x ≔ e)} {redl = (rset-var{e = .e} _ e' dehole)} {(rset-var{e = .e} _ e'' dehole)} {dehole} {dehole} {dehole} {dehole} vset-var vset-var
   rewrite δ-e-irr e' e'' = inj₁ (refl , refl , refl , refl)
E-view-main-bind {[]} {[]} {.(if _ ∣⇒ _ ∣⇒ _)} {redl = .(rif-false _ _ dehole)} {.(rif-false _ _ dehole)} {dehole} {dehole} {dehole} {dehole} vif-false vif-false = inj₁ (refl , refl , refl , refl)
E-view-main-bind {[]} {[]} {.(if _ ∣⇒ _ ∣⇒ _)} {redl = .(rif-true _ _ dehole)} {.(rif-true _ _ dehole)} {dehole} {dehole} {dehole} {dehole} vif-true vif-true = inj₁ (refl , refl , refl , refl)
E-view-main-bind {[]} {.(epar₁ _) ∷ Er} {.(_ ∥ _)} {redl = redl} {redr} {dehole} {dec2l} {depar₁ dec1r} {dec2r} () v2
E-view-main-bind {[]} {.(epar₂ _) ∷ Er} {.(_ ∥ _)} {redl = redl} {redr} {dehole} {dec2l} {depar₂ dec1r} {dec2r} () v2
E-view-main-bind {[]} {.(eseq _) ∷ Er} {.(_ >> _)} {redl = redl} {redr} {dehole} {dec2l} {deseq dec1r} {dec2r} () v2
E-view-main-bind {[]} {.(eloopˢ _) ∷ Er} {.(loopˢ _ _)} {redl = redl} {redr} {dehole} {dec2l} {deloopˢ dec1r} {dec2r} () v2
E-view-main-bind {[]} {.(esuspend _) ∷ Er} {.(suspend _ _)} {redl = redl} {redr} {dehole} {dec2l} {desuspend dec1r} {dec2r} () v2
E-view-main-bind {[]} {.etrap ∷ Er} {.(trap _)} {redl = redl} {redr} {dehole} {dec2l} {detrap dec1r} {dec2r} () v2
E-view-main-bind {.(epar₁ _) ∷ El} {[]} {.(_ ∥ _)} {redl = redl} {redr} {depar₁ dec1l} {dec2l} {dehole} {dec2r} v1 ()
E-view-main-bind {.(epar₂ _) ∷ El} {[]} {.(_ ∥ _)} {redl = redl} {redr} {depar₂ dec1l} {dec2l} {dehole} {dec2r} v1 ()
E-view-main-bind {.(eseq _) ∷ El} {[]} {.(_ >> _)} {redl = redl} {redr} {deseq dec1l} {dec2l} {dehole} {dec2r} v1 ()
E-view-main-bind {.(eloopˢ _) ∷ El} {[]} {.(loopˢ _ _)} {redl = redl} {redr} {deloopˢ dec1l} {dec2l} {dehole} {dec2r} v1 ()
E-view-main-bind {.(esuspend _) ∷ El} {[]} {.(suspend _ _)} {redl = redl} {redr} {desuspend dec1l} {dec2l} {dehole} {dec2r} v1 ()
E-view-main-bind {.etrap ∷ El} {[]} {.(trap _)} {redl = redl} {redr} {detrap dec1l} {dec2l} {dehole} {dec2r} v1 ()
E-view-main-bind {epar₁ q ∷ El} {epar₁ .q ∷ Er} {dec1l = depar₁ dec1l} {depar₁ dec2l} {depar₁ dec1r} {depar₁ dec2r} v1 v2 with unwrap-rho _ _ _ dec1l dec2l v1 | unwrap-rho _ _ _ dec1r dec2r v2
... | (redil , viewil) | (redir , viewir) with E-view-main-bind viewil viewir
... | (inj₁ (refl , refl , refl , refl)) = inj₁ (refl , refl , refl , refl)
... | (inj₂ y) = inj₂ (parr y)
E-view-main-bind {.(epar₂ _) ∷ El} {.(epar₂ _) ∷ Er} {.(_ ∥ _)} {dec1l = depar₂ dec1l} {depar₂ dec2l} {depar₂ dec1r} {depar₂ dec2r} v1 v2 with unwrap-rho _ _ _ dec1l dec2l v1 | unwrap-rho _ _ _ dec1r dec2r v2
... | (redil , viewil) | (redir , viewir) with E-view-main-bind viewil viewir
... | (inj₁ (refl , refl , refl , refl)) = inj₁ (refl , refl , refl , refl)
... | (inj₂ y) = inj₂ (parl y)
E-view-main-bind {.(eseq _) ∷ El} {.(eseq _) ∷ Er} {.(_ >> _)} {dec1l = deseq dec1l} {deseq dec2l} {deseq dec1r} {deseq dec2r} v1 v2  with unwrap-rho _ _ _ dec1l dec2l v1 | unwrap-rho _ _ _ dec1r dec2r v2
... | (redil , viewil) | (redir , viewir) with E-view-main-bind viewil viewir
... | (inj₁ (refl , refl , refl , refl)) = inj₁ (refl , refl , refl , refl)
... | (inj₂ y) = inj₂ (seq y)
E-view-main-bind {.(eloopˢ _) ∷ El} {.(eloopˢ _) ∷ Er} {.(loopˢ _ _)} {dec1l = deloopˢ dec1l} {deloopˢ dec2l} {deloopˢ dec1r} {deloopˢ dec2r} v1 v2  with unwrap-rho _ _ _ dec1l dec2l v1 | unwrap-rho _ _ _ dec1r dec2r v2
... | (redil , viewil) | (redir , viewir) with E-view-main-bind viewil viewir
... | (inj₁ (refl , refl , refl , refl)) = inj₁ (refl , refl , refl , refl)
... | (inj₂ y) = inj₂ (loopˢ y)
E-view-main-bind {.(esuspend _) ∷ El} {.(esuspend _) ∷ Er} {.(suspend _ _)} {dec1l = desuspend dec1l} {desuspend dec2l} {desuspend dec1r} {desuspend dec2r} v1 v2  with unwrap-rho _ _ _ dec1l dec2l v1 | unwrap-rho _ _ _ dec1r dec2r v2
... | (redil , viewil) | (redir , viewir) with E-view-main-bind viewil viewir
... | (inj₁ (refl , refl , refl , refl)) = inj₁ (refl , refl , refl , refl)
... | (inj₂ y) = inj₂ (susp y)
E-view-main-bind {.etrap ∷ El} {.etrap ∷ Er} {.(trap _)} {dec1l = detrap dec1l} {detrap dec2l} {detrap dec1r} {detrap dec2r} v1 v2  with unwrap-rho _ _ _ dec1l dec2l v1 | unwrap-rho _ _ _ dec1r dec2r v2
... | (redil , viewil) | (redir , viewir) with E-view-main-bind viewil viewir
... | (inj₁ (refl , refl , refl , refl)) = inj₁ (refl , refl , refl , refl)
... | (inj₂ y) = inj₂ (trp y)

get-view : ∀{θ θ' p q A A'}
           → (red : (ρ⟨ θ , A ⟩· p) sn⟶₁ (ρ⟨ θ' , A' ⟩· q))
           → (Σ[ E ∈ EvaluationContext ]
             Σ[ pin ∈ Term ]
             Σ[ qin ∈ Term ]
             Σ[ peq ∈ (p ≐ E ⟦ pin ⟧e) ]
             Σ[ qeq ∈ (q ≐ E ⟦ qin ⟧e) ]
             (->E-view{p}{q}{pin}{qin}{E}{θ}{θ'}{A}{A'} red peq qeq ))
             ⊎ Σ[ eq ∈  (p ≡ q) ] Σ[ eq2 ∈  (A ≡ A') ] (->pot-view red eq eq2)

get-view (ris-present S∈ x x₁) = inj₁ (_ , _ , _ , x₁ , Erefl , vis-present)
get-view (ris-absent S∈ x x₁) = inj₁ (_ , _ , _ , x₁ , Erefl , vis-absent)
get-view (remit S∈ _ x) = inj₁ (_ , _ , _ , x , Erefl , vemit)
get-view (rraise-shared e' x) = inj₁ (_ , _ , _ , x , Erefl , vraise-shared)
get-view (rset-shared-value-old e' s∈ x x₁) = inj₁ (_ , _ , _ , x₁ , Erefl , vset-shared-value-old)
get-view (rset-shared-value-new e' s∈ x x₁) = inj₁ (_ , _ , _ , x₁ , Erefl , vset-shared-value-new)
get-view (rraise-var e' x₁) = inj₁ (_ , _ , _ , x₁ , Erefl , vraise-var)
get-view (rset-var x∈ e' x₁) = inj₁ (_ , _ , _ , x₁ , Erefl , vset-var)
get-view (rif-false x∈ x₁ x₂) = inj₁ (_ , _ , _ , x₂ , Erefl , vif-false)
get-view (rif-true x∈ x₁ x₂) = inj₁ (_ , _ , _ , x₂ , Erefl , vif-true)
get-view (rmerge x) = inj₁ (_ , _ , _ , x , Erefl , vmerge)
get-view (rabsence {S = S} S∈ x x₁) = inj₂ (refl , refl , vabsence S S∈ x x₁)
get-view (rreadyness {s = s} s∈ x x₁) = inj₂ (refl , refl , vreadyness s s∈ x x₁)

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
{-# OPTIONS --subtyping #-}

open import Agda.Builtin.Equality

postulate
  A : Set

mutual
  I : (A -> A) → .A → A
  I f = _

  testQ : {f : .A -> A} → I f ≡ f
  testQ = refl


text:
module stateDependentIO where

open import Level using (_⊔_ ) renaming (suc to lsuc; zero to lzero)
open import Size renaming (Size to AgdaSize)
open import NativeIO
open import Function

module _  {γ ρ μ} where
  record IOInterfaceˢ : Set (lsuc (γ ⊔ ρ ⊔ μ )) where
    field
      StateIOˢ     :  Set γ
      Commandˢ     :  StateIOˢ → Set ρ
      Responseˢ    :  (s : StateIOˢ) → Commandˢ s → Set μ
      nextIOˢ      :  (s : StateIOˢ) → (c : Commandˢ s) → Responseˢ s c
                     → StateIOˢ

open IOInterfaceˢ public

module _  {α γ ρ μ}(i   : IOInterfaceˢ {γ} {ρ} {μ} )
          (let S = StateIOˢ i)  (let C  = Commandˢ i)
          (let R = Responseˢ i) (let next = nextIOˢ i)
  where
    mutual

      record IOˢ (i : AgdaSize)  (A : S → Set α) (s : S)
                 : Set (lsuc (α ⊔ γ ⊔ ρ ⊔ μ )) where
        coinductive
        constructor delay
        field forceˢ : {j : Size< i} → IOˢ' j A s

      data IOˢ' (i : AgdaSize)  (A : S → Set α) : S
               → Set (lsuc (α ⊔ γ ⊔ ρ ⊔ μ )) where
        doˢ'      :  {s : S} → (c : C s) → (f : (r : R s c)
                                                  → IOˢ i A (next s c r) )
                     → IOˢ' i A s
        returnˢ'  :  {s : S} → (a : A s) → IOˢ' i A s

open IOˢ public

module _  {α γ ρ μ}{I   : IOInterfaceˢ {γ} {ρ} {μ}}
                   (let S = StateIOˢ I)     (let C  = Commandˢ I)
                   (let  R  = Responseˢ I) (let next = nextIOˢ I) where

  returnIOˢ : ∀{i}{A : S → Set α} {s : S} (a : A s) → IOˢ  I i A s
  forceˢ (returnIOˢ a) = returnˢ' a

  doˢ  :  ∀{i}{A : S → Set α} {s : S}
          (c : C s) (f : (r : R s c) → IOˢ I i A (next s c r)) → IOˢ I i A s
  forceˢ (doˢ c f) = doˢ' c f

module _  {γ ρ}{I   : IOInterfaceˢ {γ} {ρ} {lzero}}
                (let S = StateIOˢ I)     (let C  = Commandˢ I)
                (let  R  = Responseˢ I) (let next = nextIOˢ I) where

  {-# NON_TERMINATING #-}
  translateIOˢ : ∀{A : Set }{s : S}
    →  (translateLocal : (s : S) → (c : C s) → NativeIO (R s c))
    →  IOˢ I ∞ (λ s → A) s
    →  NativeIO A
  translateIOˢ {A} {s} translateLocal p = case (forceˢ p {_}) of
    λ{ (doˢ' {.s} c f)    → (translateLocal s c)     native>>= λ r →
                             translateIOˢ translateLocal (f r)
     ; (returnˢ' a) → nativeReturn a
     }

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module New.FunctionLemmas where

open import New.Changes

module BinaryValid
  {A : Set} {{CA : ChAlg A}}
  {B : Set} {{CB : ChAlg B}}
  {C : Set} {{CC : ChAlg C}}
  (f : A → B → C) (df : A → Ch A → B → Ch B → Ch C)
  where

  binary-valid-preserve-hp =
    ∀ a da (ada : valid a da)
      b db (bdb : valid b db)
    → valid (f a b) (df a da b db)

  binary-valid-eq-hp =
    ∀ a da (ada : valid a da)
      b db (bdb : valid b db)
    → (f ⊕ df) (a ⊕ da) (b ⊕ db) ≡ f a b ⊕ df a da b db

  binary-valid :
    binary-valid-preserve-hp →
    binary-valid-eq-hp →
    valid f df
  binary-valid ext-valid proof a da ada =
      (λ b db bdb → ext-valid a da ada b db bdb , lem2 b db bdb)
    , ext lem1
    where
      lem1 : ∀ b → f (a ⊕ da) b ⊕ df (a ⊕ da) (nil (a ⊕ da)) b (nil b) ≡
        f a b ⊕ df a da b (nil b)
      lem1 b
        rewrite sym (update-nil b)
        | proof a da ada b (nil b) (nil-valid b)
        | update-nil b = refl
      lem2 : ∀ b (db : Ch B) (bdb : valid b db) →
        f a (b ⊕ db) ⊕ df a da (b ⊕ db) (nil (b ⊕ db)) ≡
        f a b ⊕ df a da b db
      lem2 b db bdb
        rewrite sym (proof a da ada (b ⊕ db) (nil (b ⊕ db)) (nil-valid (b ⊕ db)))
        | update-nil (b ⊕ db) = proof a da ada b db bdb

module TernaryValid
  {A : Set} {{CA : ChAlg A}}
  {B : Set} {{CB : ChAlg B}}
  {C : Set} {{CC : ChAlg C}}
  {D : Set} {{CD : ChAlg D}}
  (f : A → B → C → D) (df : A → Ch A → B → Ch B → C → Ch C → Ch D)
  where

  ternary-valid-preserve-hp =
    ∀ a da (ada : valid a da)
      b db (bdb : valid b db)
      c dc (cdc : valid c dc)
    → valid (f a b c) (df a da b db c dc)

  -- These are explicit definitions only to speed up typechecking.
  CA→B→C→D : ChAlg (A → B → C → D)
  CA→B→C→D = funCA
  f⊕df = (_⊕_ {{CA→B→C→D}} f df)

  -- Already this definition takes a while to typecheck.
  ternary-valid-eq-hp =
    ∀ a (da : Ch A {{CA}}) (ada : valid {{CA}} a da)
      b (db : Ch B {{CB}}) (bdb : valid {{CB}} b db)
      c (dc : Ch C {{CC}}) (cdc : valid {{CC}} c dc)
    → f⊕df (a ⊕ da) (b ⊕ db) (c ⊕ dc) ≡ f a b c ⊕ df a da b db c dc

  ternary-valid :
    ternary-valid-preserve-hp →
    ternary-valid-eq-hp →
    valid f df
  ternary-valid ext-valid proof a da ada =
    binary-valid
      (λ b db bdb c dc cdc → ext-valid a da ada b db bdb c dc cdc)
      lem2
    , ext (λ b → ext (lem1 b))
    where
      open BinaryValid (f a) (df a da)
      lem1 : ∀ b c → f⊕df (a ⊕ da) b c ≡ (f a ⊕ df a da) b c
      lem1 b c
        rewrite sym (update-nil b)
        | sym (update-nil c)
        |
          proof
            a da ada
            b (nil b) (nil-valid b)
            c (nil c) (nil-valid c)
        | update-nil b
        | update-nil c = refl
        -- rewrite
        --   sym
        --   (proof
        --     (a ⊕ da) (nil (a ⊕ da)) (nil-valid (a ⊕ da))
        --     b (nil b) (nil-valid b)
        --     c (nil c) (nil-valid c))
        -- | update-nil (a ⊕ da)
        -- | update-nil b
        -- | update-nil c = {! !}
      lem2 : ∀ b db (bdb : valid b db)
               c dc (cdc : valid c dc) →
                 (f a ⊕ df a da) (b ⊕ db) (c ⊕ dc)
               ≡ f a b c ⊕ df a da b db c dc
      lem2 b db bdb c dc cdc
        rewrite sym
          (proof
            a da ada
            (b ⊕ db) (nil (b ⊕ db)) (nil-valid (b ⊕ db))
            (c ⊕ dc) (nil (c ⊕ dc)) (nil-valid (c ⊕ dc))
          )
        | update-nil (b ⊕ db)
        | update-nil (c ⊕ dc) = proof a da ada b db bdb c dc cdc

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


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

module Relation.Nullary.Omniscience where

open import Prelude
open import Relation.Nullary.Decidable
open import Relation.Nullary.Decidable.Properties
open import Relation.Nullary.Decidable.Logic
open import Relation.Nullary
open import Data.Bool using (bool)

private
  variable
    p : Level
    P : A → Type p

Omniscient Exhaustible Prop-Omniscient : ∀ p {a} → Type a → Type _

Omniscient p A = ∀ {P : A → Type p} → (∀ x → Dec (P x)) → Dec (∃ x × P x)

Exhaustible p A = ∀ {P : A → Type p} → (∀ x → Dec (P x)) → Dec (∀ x → P x)

Omniscient→Exhaustible : Omniscient p A → Exhaustible p A
Omniscient→Exhaustible omn P? =
  map-dec
    (λ ¬∃P x → Dec→Stable _ (P? x) (¬∃P ∘ (x ,_)))
    (λ ¬∃P ∀P → ¬∃P λ p → p .snd (∀P (p .fst)))
    (! (omn (! ∘ P?)))
Prop-Omniscient p A = ∀ {P : A → Type p} → (∀ x → Dec (P x)) → Dec ∥ ∃ x × P x ∥


text:
-- Andreas, 2017-06-20, issue #2613, reported by Jonathan Prieto.
-- Regression introduced by fix of #2458 (which is obsolete since #2403)

module _ where

open import Agda.Builtin.Nat

module Prop' (n : Nat) where

  data Prop' : Set where
    _∧_ _∨_ : Prop' → Prop' → Prop'

open Prop' zero

data DView : Prop' → Set where
  case₁ : (a b c : Prop') → DView ((a ∨ b) ∧ c)
  case₂ : (a : Prop')     → DView a

dView : (p : Prop') → DView p
dView ((a ∨ b) ∧ c) = case₁  _ _ _
dView a             = case₂ _

dist-∧ : Prop' → Prop'
dist-∧ p with dView p
dist-∧ .((a ∨ b) ∧ c) | case₁ a b c = dist-∧ (a ∧ c)
dist-∧ a              | case₂ .a = a

-- WAS:
-- Termination checking failed for the following functions:
--   dist-∧
-- Problematic calls:
--   dist-∧ (a ∧ c)

-- Should succeed.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module #11 where

{-
  Show that for any type A, we have ¬¬¬A → ¬A.
-}

open import Data.Empty
open import Relation.Nullary

tripleNeg : ∀{x}{A : Set x} → ¬ (¬ (¬ A)) → ¬ A
tripleNeg = λ z z₁ → z (λ z₂ → z₂ z₁)

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
{-# OPTIONS --safe #-}
module Cubical.Data.Vec where

open import Cubical.Data.Vec.Base public
open import Cubical.Data.Vec.Properties public
open import Cubical.Data.Vec.NAry public
open import Cubical.Data.Vec.OperationsNat public

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
------------------------------------------------------------------------------
-- Properties related with lists of natural numbers
------------------------------------------------------------------------------

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

module FOTC.Data.Nat.List.PropertiesI where

open import FOTC.Base
open import FOTC.Data.Nat
open import FOTC.Data.Nat.List
open import FOTC.Data.List

------------------------------------------------------------------------------
-- See the ATP version.
postulate ++-ListN : ∀ {ms ns} → ListN ms → ListN ns → ListN (ms ++ ns)

map-ListN : ∀ f {ns} → (∀ {n} → N n → N (f · n)) → ListN ns → ListN (map f ns)
map-ListN f h lnnil                    = subst ListN (sym (map-[] f)) lnnil
map-ListN f h (lncons {n} {ns} Nn Lns) =
  subst ListN (sym (map-∷ f n ns)) (lncons (h Nn) (map-ListN f h Lns))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc