text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Pointwise products of binary relations
------------------------------------------------------------------------

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

module Data.Product.Relation.Binary.Pointwise.NonDependent where

open import Data.Product as Prod
open import Data.Sum
open import Data.Unit.Base using (⊤)
open import Function
open import Function.Equality as F using (_⟶_; _⟨$⟩_)
open import Function.Equivalence as Eq
  using (Equivalence; _⇔_; module Equivalence)
open import Function.Injection as Inj
  using (Injection; _↣_; module Injection)
open import Function.Inverse as Inv
  using (Inverse; _↔_; module Inverse)
open import Function.LeftInverse as LeftInv
  using (LeftInverse; _↞_; _LeftInverseOf_; module LeftInverse)
open import Function.Related
open import Function.Surjection as Surj
  using (Surjection; _↠_; module Surjection)
import Relation.Nullary.Decidable as Dec
open import Relation.Nullary.Product
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where

------------------------------------------------------------------------
-- Pointwise lifting

  Pointwise : Rel A₁ ℓ₁ → Rel A₂ ℓ₂ → Rel (A₁ × A₂) _
  Pointwise _∼₁_ _∼₂_ = (_∼₁_ on proj₁) -×- (_∼₂_ on proj₂)

------------------------------------------------------------------------
-- Pointwise preserves many relational properties

  ×-reflexive : ∀ {_≈₁_ _∼₁_ _≈₂_ _∼₂_} →
    _≈₁_ ⇒ _∼₁_ → _≈₂_ ⇒ _∼₂_ →
    (Pointwise _≈₁_ _≈₂_) ⇒ (Pointwise _∼₁_ _∼₂_)
  ×-reflexive refl₁ refl₂ (x∼y₁ , x∼y₂) = refl₁ x∼y₁ , refl₂ x∼y₂

  ×-refl : ∀ {_∼₁_ _∼₂_} →
    Reflexive _∼₁_ → Reflexive _∼₂_ →
    Reflexive (Pointwise _∼₁_ _∼₂_)
  ×-refl refl₁ refl₂ = refl₁ , refl₂

  ×-irreflexive₁ : ∀ {_≈₁_ _<₁_ _≈₂_ _<₂_} →
    Irreflexive _≈₁_ _<₁_ →
    Irreflexive (Pointwise _≈₁_ _≈₂_) (Pointwise _<₁_ _<₂_)
  ×-irreflexive₁ ir x≈y x<y = ir (proj₁ x≈y) (proj₁ x<y)

  ×-irreflexive₂ : ∀ {_≈₁_ _<₁_ _≈₂_ _<₂_} →
    Irreflexive _≈₂_ _<₂_ →
    Irreflexive (Pointwise _≈₁_ _≈₂_) (Pointwise _<₁_ _<₂_)
  ×-irreflexive₂ ir x≈y x<y = ir (proj₂ x≈y) (proj₂ x<y)

  ×-symmetric : ∀ {_∼₁_ _∼₂_} → Symmetric _∼₁_ → Symmetric _∼₂_ →
    Symmetric (Pointwise _∼₁_ _∼₂_)
  ×-symmetric sym₁ sym₂ (x∼y₁ , x∼y₂) = sym₁ x∼y₁ , sym₂ x∼y₂

  ×-transitive : ∀ {_∼₁_ _∼₂_} → Transitive _∼₁_ → Transitive _∼₂_ →
    Transitive (Pointwise _∼₁_ _∼₂_)
  ×-transitive trans₁ trans₂ x∼y y∼z =
    trans₁ (proj₁ x∼y) (proj₁ y∼z) ,
    trans₂ (proj₂ x∼y) (proj₂ y∼z)

  ×-antisymmetric : ∀ {_≈₁_ _≤₁_ _≈₂_ _≤₂_} →
    Antisymmetric _≈₁_ _≤₁_ → Antisymmetric _≈₂_ _≤₂_ →
    Antisymmetric (Pointwise _≈₁_ _≈₂_) (Pointwise _≤₁_ _≤₂_)
  ×-antisymmetric antisym₁ antisym₂ (x≤y₁ , x≤y₂) (y≤x₁ , y≤x₂) =
    (antisym₁ x≤y₁ y≤x₁ , antisym₂ x≤y₂ y≤x₂)

  ×-asymmetric₁ : ∀ {_<₁_ _∼₂_} → Asymmetric _<₁_ →
    Asymmetric (Pointwise _<₁_ _∼₂_)
  ×-asymmetric₁ asym₁ x<y y<x = asym₁ (proj₁ x<y) (proj₁ y<x)

  ×-asymmetric₂ : ∀ {_∼₁_ _<₂_} → Asymmetric _<₂_ →
    Asymmetric (Pointwise _∼₁_ _<₂_)
  ×-asymmetric₂ asym₂ x<y y<x = asym₂ (proj₂ x<y) (proj₂ y<x)

  ×-respects₂ : ∀ {_≈₁_ _∼₁_ _≈₂_ _∼₂_} →
    _∼₁_ Respects₂ _≈₁_ → _∼₂_ Respects₂ _≈₂_ →
    (Pointwise _∼₁_ _∼₂_) Respects₂ (Pointwise _≈₁_ _≈₂_)
  ×-respects₂ {_≈₁_} {_∼₁_} {_≈₂_} {_∼₂_} resp₁ resp₂ = resp¹ , resp²
    where
    _∼_ = Pointwise _∼₁_ _∼₂_
    _≈_ = Pointwise _≈₁_ _≈₂_

    resp¹ : ∀ {x} → (x ∼_) Respects _≈_
    resp¹ y≈y' x∼y = proj₁ resp₁ (proj₁ y≈y') (proj₁ x∼y) ,
                     proj₁ resp₂ (proj₂ y≈y') (proj₂ x∼y)

    resp² : ∀ {y} → (_∼ y) Respects _≈_
    resp² x≈x' x∼y = proj₂ resp₁ (proj₁ x≈x') (proj₁ x∼y) ,
                     proj₂ resp₂ (proj₂ x≈x') (proj₂ x∼y)

  ×-total : ∀ {_∼₁_ _∼₂_} → Symmetric _∼₁_ →
    Total _∼₁_ → Total _∼₂_ →
    Total (Pointwise _∼₁_ _∼₂_)
  ×-total sym₁ total₁ total₂ (x₁ , x₂) (y₁ , y₂)
    with total₁ x₁ y₁ | total₂ x₂ y₂
  ... | inj₁ x₁∼y₁ | inj₁ x₂∼y₂ = inj₁ (     x₁∼y₁ , x₂∼y₂)
  ... | inj₁ x₁∼y₁ | inj₂ y₂∼x₂ = inj₂ (sym₁ x₁∼y₁ , y₂∼x₂)
  ... | inj₂ y₁∼x₁ | inj₂ y₂∼x₂ = inj₂ (     y₁∼x₁ , y₂∼x₂)
  ... | inj₂ y₁∼x₁ | inj₁ x₂∼y₂ = inj₁ (sym₁ y₁∼x₁ , x₂∼y₂)

  ×-decidable : ∀ {_∼₁_ _∼₂_} →
    Decidable _∼₁_ → Decidable _∼₂_ →
    Decidable (Pointwise _∼₁_ _∼₂_)
  ×-decidable _≟₁_ _≟₂_ (x₁ , x₂) (y₁ , y₂) =
    (x₁ ≟₁ y₁) ×-dec (x₂ ≟₂ y₂)

  -- Some collections of properties which are preserved by ×-Rel.

  ×-isEquivalence : ∀ {_≈₁_ _≈₂_} →
    IsEquivalence _≈₁_ → IsEquivalence _≈₂_ →
    IsEquivalence (Pointwise _≈₁_ _≈₂_)
  ×-isEquivalence {_≈₁_ = _≈₁_} {_≈₂_ = _≈₂_} eq₁ eq₂ = record
    { refl  = ×-refl        {_∼₁_ = _≈₁_} {_∼₂_ = _≈₂_}
                            (refl  eq₁) (refl  eq₂)
    ; sym   = ×-symmetric   {_∼₁_ = _≈₁_} {_∼₂_ = _≈₂_}
                            (sym   eq₁) (sym   eq₂)
    ; trans = ×-transitive  {_∼₁_ = _≈₁_} {_∼₂_ = _≈₂_}
                            (trans eq₁) (trans eq₂)
    }
    where open IsEquivalence

  ×-isDecEquivalence : ∀ {_≈₁_ _≈₂_} →
    IsDecEquivalence _≈₁_ → IsDecEquivalence _≈₂_ →
    IsDecEquivalence (Pointwise _≈₁_ _≈₂_)
  ×-isDecEquivalence eq₁ eq₂ = record
    { isEquivalence = ×-isEquivalence
                        (isEquivalence eq₁) (isEquivalence eq₂)
    ; _≟_           = ×-decidable (_≟_ eq₁) (_≟_ eq₂)
    }
    where open IsDecEquivalence

  ×-isPreorder : ∀ {_≈₁_ _∼₁_ _≈₂_ _∼₂_} →
    IsPreorder _≈₁_ _∼₁_ → IsPreorder _≈₂_ _∼₂_ →
    IsPreorder (Pointwise _≈₁_ _≈₂_) (Pointwise _∼₁_ _∼₂_)
  ×-isPreorder {_∼₁_ = _∼₁_} {_∼₂_ = _∼₂_} pre₁ pre₂ = record
    { isEquivalence = ×-isEquivalence
                        (isEquivalence pre₁) (isEquivalence pre₂)
    ; reflexive     = ×-reflexive {_∼₁_ = _∼₁_} {_∼₂_ = _∼₂_}
                        (reflexive pre₁) (reflexive pre₂)
    ; trans         = ×-transitive {_∼₁_ = _∼₁_} {_∼₂_ = _∼₂_}
                        (trans pre₁) (trans pre₂)
    }
    where open IsPreorder

  ×-isPartialOrder : ∀ {_≈₁_ _≤₁_ _≈₂_ _≤₂_} →
    IsPartialOrder _≈₁_ _≤₁_ → IsPartialOrder _≈₂_ _≤₂_ →
    IsPartialOrder (Pointwise _≈₁_ _≈₂_) (Pointwise _≤₁_ _≤₂_)
  ×-isPartialOrder {_≤₁_ = _≤₁_} {_≤₂_ = _≤₂_} po₁ po₂ = record
    { isPreorder = ×-isPreorder (isPreorder po₁) (isPreorder po₂)
    ; antisym    = ×-antisymmetric {_≤₁_ = _≤₁_} {_≤₂_ = _≤₂_}
                     (antisym po₁) (antisym po₂)
    }
    where open IsPartialOrder

  ×-isStrictPartialOrder : ∀ {_≈₁_ _<₁_ _≈₂_ _<₂_} →
    IsStrictPartialOrder _≈₁_ _<₁_ → IsStrictPartialOrder _≈₂_ _<₂_ →
    IsStrictPartialOrder (Pointwise _≈₁_ _≈₂_) (Pointwise _<₁_ _<₂_)
  ×-isStrictPartialOrder {_<₁_ = _<₁_} {_≈₂_ = _≈₂_} {_<₂_ = _<₂_}
                           spo₁ spo₂ =
    record
      { isEquivalence = ×-isEquivalence
                          (isEquivalence spo₁) (isEquivalence spo₂)
      ; irrefl        = ×-irreflexive₁ {_<₁_ = _<₁_} {_≈₂_} {_<₂_}
                          (irrefl spo₁)
      ; trans         = ×-transitive {_∼₁_ = _<₁_} {_<₂_}
                          (trans spo₁) (trans spo₂)
      ; <-resp-≈      = ×-respects₂ (<-resp-≈ spo₁) (<-resp-≈ spo₂)
      }
    where open IsStrictPartialOrder

------------------------------------------------------------------------
-- "Packages" can also be combined.

module _ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} where

  ×-preorder : Preorder ℓ₁ ℓ₂ _ → Preorder ℓ₃ ℓ₄ _ → Preorder _ _ _
  ×-preorder p₁ p₂ = record
    { isPreorder = ×-isPreorder (isPreorder p₁) (isPreorder p₂)
    } where open Preorder

  ×-setoid : Setoid ℓ₁ ℓ₂ → Setoid ℓ₃ ℓ₄ → Setoid _ _
  ×-setoid s₁ s₂ = record
    { isEquivalence =
        ×-isEquivalence (isEquivalence s₁) (isEquivalence s₂)
    } where open Setoid

  ×-decSetoid : DecSetoid ℓ₁ ℓ₂ → DecSetoid ℓ₃ ℓ₄ → DecSetoid _ _
  ×-decSetoid s₁ s₂ = record
    { isDecEquivalence =
        ×-isDecEquivalence (isDecEquivalence s₁) (isDecEquivalence s₂)
    } where open DecSetoid

  ×-poset : Poset ℓ₁ ℓ₂ _ → Poset ℓ₃ ℓ₄ _ → Poset _ _ _
  ×-poset s₁ s₂ = record
    { isPartialOrder = ×-isPartialOrder (isPartialOrder s₁)
                       (isPartialOrder s₂)
    } where open Poset

  ×-strictPartialOrder :
    StrictPartialOrder ℓ₁ ℓ₂ _ → StrictPartialOrder ℓ₃ ℓ₄ _ →
    StrictPartialOrder _ _ _
  ×-strictPartialOrder s₁ s₂ = record
    { isStrictPartialOrder = ×-isStrictPartialOrder
                               (isStrictPartialOrder s₁)
                               (isStrictPartialOrder s₂)
    } where open StrictPartialOrder

  -- A piece of infix notation for combining setoids
  infix 4 _×ₛ_
  _×ₛ_ : Setoid ℓ₁ ℓ₂ → Setoid ℓ₃ ℓ₄ → Setoid _ _
  _×ₛ_ = ×-setoid

------------------------------------------------------------------------
-- The propositional equality setoid over products can be
-- decomposed using ×-Rel

module _ {a b} {A : Set a} {B : Set b} where

  ≡×≡⇒≡ : Pointwise _≡_ _≡_ ⇒ _≡_ {A = A × B}
  ≡×≡⇒≡ (P.refl , P.refl) = P.refl

  ≡⇒≡×≡ : _≡_ {A = A × B} ⇒ Pointwise _≡_ _≡_
  ≡⇒≡×≡ P.refl = (P.refl , P.refl)

  Pointwise-≡↔≡ : Inverse (P.setoid A ×ₛ P.setoid B) (P.setoid (A × B))
  Pointwise-≡↔≡ = record
    { to         = record { _⟨$⟩_ = id; cong = ≡×≡⇒≡ }
    ; from       = record { _⟨$⟩_ = id; cong = ≡⇒≡×≡ }
    ; inverse-of = record
      { left-inverse-of  = λ _ → (P.refl , P.refl)
      ; right-inverse-of = λ _ → P.refl
      }
    }

  ≡?×≡?⇒≡? : Decidable {A = A} _≡_ → Decidable {A = B} _≡_ →
              Decidable {A = A × B} _≡_
  ≡?×≡?⇒≡? ≟₁ ≟₂ p q = Dec.map′ ≡×≡⇒≡ ≡⇒≡×≡ (×-decidable ≟₁ ≟₂ p q)

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.15

infixr 2 _×-Rel_
_×-Rel_ = Pointwise
{-# WARNING_ON_USAGE _×-Rel_
"Warning: _×-Rel_ was deprecated in v0.15.
Please use Pointwise instead."
#-}
Rel↔≡                     = Pointwise-≡↔≡
{-# WARNING_ON_USAGE Rel↔≡
"Warning: Rel↔≡ was deprecated in v0.15.
Please use Pointwise-≡↔≡ instead."
#-}
_×-reflexive_             = ×-reflexive
{-# WARNING_ON_USAGE _×-reflexive_
"Warning: _×-reflexive_ was deprecated in v0.15.
Please use ×-reflexive instead."
#-}
_×-refl_                  = ×-refl
{-# WARNING_ON_USAGE _×-refl_
"Warning: _×-refl_ was deprecated in v0.15.
Please use ×-refl instead."
#-}
_×-symmetric_             = ×-symmetric
{-# WARNING_ON_USAGE _×-symmetric_
"Warning: _×-symmetric_ was deprecated in v0.15.
Please use ×-symmetric instead."
#-}
_×-transitive_            = ×-transitive
{-# WARNING_ON_USAGE _×-transitive_
"Warning: _×-transitive_ was deprecated in v0.15.
Please use ×-transitive instead."
#-}
_×-antisymmetric_         = ×-antisymmetric
{-# WARNING_ON_USAGE _×-antisymmetric_
"Warning: _×-antisymmetric_ was deprecated in v0.15.
Please use ×-antisymmetric instead."
#-}
_×-≈-respects₂_           = ×-respects₂
{-# WARNING_ON_USAGE _×-≈-respects₂_
"Warning: _×-≈-respects₂_ was deprecated in v0.15.
Please use ×-respects₂ instead."
#-}
_×-decidable_             = ×-decidable
{-# WARNING_ON_USAGE _×-decidable_
"Warning: _×-decidable_ was deprecated in v0.15.
Please use ×-decidable instead."
#-}
_×-isEquivalence_         = ×-isEquivalence
{-# WARNING_ON_USAGE _×-isEquivalence_
"Warning: _×-isEquivalence_ was deprecated in v0.15.
Please use ×-isEquivalence instead."
#-}
_×-isDecEquivalence_      = ×-isDecEquivalence
{-# WARNING_ON_USAGE _×-isDecEquivalence_
"Warning: _×-isDecEquivalence_ was deprecated in v0.15.
Please use ×-isDecEquivalence instead."
#-}
_×-isPreorder_            = ×-isPreorder
{-# WARNING_ON_USAGE _×-isPreorder_
"Warning: _×-isPreorder_ was deprecated in v0.15.
Please use ×-isPreorder instead."
#-}
_×-isPartialOrder_        = ×-isPartialOrder
{-# WARNING_ON_USAGE _×-isPartialOrder_
"Warning: _×-isPartialOrder_ was deprecated in v0.15.
Please use ×-isPartialOrder instead."
#-}
_×-isStrictPartialOrder_  = ×-isStrictPartialOrder
{-# WARNING_ON_USAGE _×-isStrictPartialOrder_
"Warning: _×-isStrictPartialOrder_ was deprecated in v0.15.
Please use ×-isStrictPartialOrder instead."
#-}
_×-preorder_              = ×-preorder
{-# WARNING_ON_USAGE _×-preorder_
"Warning: _×-preorder_ was deprecated in v0.15.
Please use ×-preorder instead."
#-}
_×-setoid_                = ×-setoid
{-# WARNING_ON_USAGE _×-setoid_
"Warning: _×-setoid_ was deprecated in v0.15.
Please use ×-setoid instead."
#-}
_×-decSetoid_             = ×-decSetoid
{-# WARNING_ON_USAGE _×-decSetoid_
"Warning: _×-decSetoid_ was deprecated in v0.15.
Please use ×-decSetoid instead."
#-}
_×-poset_                 = ×-poset
{-# WARNING_ON_USAGE _×-poset_
"Warning: _×-poset_ was deprecated in v0.15.
Please use ×-poset instead."
#-}
_×-strictPartialOrder_    = ×-strictPartialOrder
{-# WARNING_ON_USAGE _×-strictPartialOrder_
"Warning: _×-strictPartialOrder_ was deprecated in v0.15.
Please use ×-strictPartialOrder instead."
#-}
_×-≟_                     = ≡?×≡?⇒≡?
{-# WARNING_ON_USAGE _×-≟_
"Warning: _×-≟_ was deprecated in v0.15.
Please use ≡?×≡?⇒≡? instead."
#-}


text:
-- Andreas, 2013-10-25 issue reported by Jesper Cockx
-- simplified test case by Nisse

-- {-# OPTIONS -v tc.meta:30 #-}

module Issue920 where

import Common.Level

postulate
  Eq    : (A : Set) (x : A) → A → Set
  cast  : (A B : Set) → A → B
  magic : (P : Set → Set) (A : Set) → P A

bad : (A : Set) (x : A) → Eq A (cast A A x) x
bad A x = magic (λ B → Eq B (cast A B x) {!x!}) A

-- Should produce yellow, since there is no solution for ?0

-- Handling of linearity in constraint solver was buggy:
--   ?0 : (A : Set) (x : A) (B : Set) -> B
--   ?0 A x A := x
-- was simply solved by ?0 := λ A x B → x
-- since the non-linear variable did not appear on the rhs.
-- However, this solution is ill-typed.

-- Instead, we now only attempt pruning in case of non-linearity,
-- which fails here: B cannot be pruned since its the return type,
-- and A cannot be pruned since its the type of argument x.

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2015-12-29

record ⊤ : Set where

data P : ⊤ → Set where
  c : P record{}
  d : P record{}

test : (x : ⊤) (p : P x) → Set
test _ c with Set
test _ d | z = ⊤

-- Expected error: with-clause pattern mismatch.
-- The error should be printed nicely, like:
--
-- With clause pattern d is not an instance of its parent pattern c
-- when checking that the clause
-- test _ c with Set
-- test _ d | z = ⊤
-- has type (x : ⊤) → P x → Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

-- A Category enriched over Setoids is... a Category!
module Categories.Enriched.Over.Setoids where

open import Level
open import Data.Product using (uncurry; proj₁; proj₂; Σ; _,_)
open import Data.Unit using (tt)
open import Function.Equality using (_⟨$⟩_; cong)
open import Relation.Binary.Bundles using (Setoid)

open import Categories.Category.Core using () renaming (Category to SCategory)
open import Categories.Category.Equivalence using (StrongEquivalence)
open import Categories.Category.Monoidal.Instance.Setoids
open import Categories.Functor renaming (id to idF)
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_)
open import Categories.Enriched.Category
import Categories.Morphism.Reasoning as MR

Category′ : (o ℓ t : Level) → Set (suc (o ⊔ ℓ ⊔ t))
Category′ o ℓ t = Category (Setoids-Monoidal {t} {ℓ}) o

-- Start with the translation functions
Cat→Cat′ : {o ℓ t : Level} → SCategory o ℓ t → Category′ o t ℓ
Cat→Cat′ C = record
  { Obj = Obj
  ; hom = λ a b → record
    { Carrier = a ⇒ b
    ; _≈_ = _≈_
    ; isEquivalence = equiv
    }
  ; id = record
    { _⟨$⟩_ = λ _ → id
    ; cong = λ _ → Equiv.refl
    }
  ; ⊚ = record
    { _⟨$⟩_ = uncurry _∘_
    ; cong = uncurry ∘-resp-≈
    }
  ; ⊚-assoc = λ { {x = (x₁ , x₂) , x₃} {(y₁ , y₂) , y₃} ((x₁≈y₁ , x₂≈y₂) , x₃≈y₃) → begin
    (x₁ ∘ x₂) ∘ x₃ ≈⟨ assoc {h = x₁} ⟩
    x₁ ∘ x₂ ∘ x₃   ≈⟨ (x₁≈y₁ ⟩∘⟨ x₂≈y₂ ⟩∘⟨ x₃≈y₃) ⟩
    y₁ ∘ y₂ ∘ y₃   ∎ }
  ; unitˡ = λ { {_} {_} {_ , x} {_ , y} (_ , x≈y) → Equiv.trans (identityˡ {f = x}) x≈y }
  ; unitʳ = λ z → Equiv.trans identityʳ (proj₁ z)
  }
  where
  open SCategory C
  open HomReasoning

Cat′→Cat : {o ℓ t : Level} → Category′ o ℓ t → SCategory o t ℓ
Cat′→Cat 𝓒 = record
  { Obj = Obj
  ; _⇒_ = λ a b → Carrier (hom a b)
  ; _≈_ = λ {a} {b} f g → _≈_ (hom a b) f g
  ; id = id ⟨$⟩ lift tt
  ; _∘_ = λ f g → ⊚ ⟨$⟩ (f , g)
  ; assoc = λ {A} {B} {C} {D} → ⊚-assoc ((refl (hom C D) , refl (hom B C)) , refl (hom A B))
  ; sym-assoc = λ {A} {B} {C} {D} → sym (hom A D) (⊚-assoc ((refl (hom C D) , refl (hom B C)) , refl (hom A B)))
  ; identityˡ = λ {A} {B} → unitˡ (lift tt , refl (hom A B))
  ; identityʳ = λ {A} {B} → unitʳ (refl (hom A B) , lift tt)
  ; identity² = λ {A} → unitˡ (lift tt , refl (hom A A)) -- Enriched doesn't have a unit²
  ; equiv = λ {A} {B} → record
    { refl = refl (hom A B)
    ; sym = sym (hom A B)
    ; trans = trans (hom A B)
    }
  ; ∘-resp-≈ = λ f≈h g≈i → cong ⊚ (f≈h , g≈i)
  }
  where
  open Category 𝓒
  open Setoid

-- Back-and-forth gives the same thing, SCat version
-- the details are trivial, but have to be spelled out
SCat-Equiv : {o ℓ t : Level} → (C : SCategory o ℓ t) → StrongEquivalence C (Cat′→Cat (Cat→Cat′ C))
SCat-Equiv C = record
  { F = fwd
  ; G = bwd
  ; weak-inverse = record
    { F∘G≈id = f∘b≃id
    ; G∘F≈id = b∘f≃id
    }
  }
  where
  open SCategory C
  open MR C
  fwd : Functor C (Cat′→Cat (Cat→Cat′ C))
  fwd = record
    { F₀ = λ x → x
    ; F₁ = λ f → f
    ; identity = Equiv.refl
    ; homomorphism = Equiv.refl
    ; F-resp-≈ = λ ≈ → ≈
    }
  bwd : Functor (Cat′→Cat (Cat→Cat′ C)) C
  bwd = record
    { F₀ = λ x → x
    ; F₁ = λ f → f
    ; identity = Equiv.refl
    ; homomorphism = Equiv.refl
    ; F-resp-≈ = λ ≈ → ≈
    }
  f∘b≃id : fwd ∘F bwd ≃ idF
  f∘b≃id = record
    { F⇒G = record { η = λ A → id {A} ; commute = λ _ → id-comm-sym ; sym-commute = λ _ → id-comm }
    ; F⇐G = record { η = λ A → id {A} ; commute = λ _ → id-comm-sym ; sym-commute = λ _ → id-comm }
    ; iso = λ X → record { isoˡ = identity² ; isoʳ = identity² }
    }
  b∘f≃id : bwd ∘F fwd ≃ idF
  b∘f≃id = record
    { F⇒G = record { η = λ A → id {A} ; commute = λ _ → id-comm-sym ; sym-commute = λ _ → id-comm }
    ; F⇐G = record { η = λ A → id {A} ; commute = λ _ → id-comm-sym ; sym-commute = λ _ → id-comm }
    ; iso = λ X → record { isoˡ = identity² ; isoʳ = identity² }
    }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


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

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

{-# BUILTIN REWRITE _≡_ #-}

data D : Set₁ where
  c : Set → D

unD : D → Set
unD (c X) = X

id : unD (c (Nat → Nat))
id x = x

postulate rew : c (Nat → Nat) ≡ c (Nat → Bool)
{-# REWRITE rew #-}

0' : Bool
0' = id 0


text:
module _ where

module LocalSetoidCalc (Node : Set) where
  module _ (A : Node) where
    module _IsRelatedTo_ where

module SGFunctorSetup (Obj₁ Obj₂ : Set) where
  open LocalSetoidCalc Obj₁ public renaming (module _IsRelatedTo_ to _IsRelatedTo₁_)
  open LocalSetoidCalc Obj₂ public renaming (module _IsRelatedTo_ to _IsRelatedTo₂_)

postulate X Y : Set
open SGFunctorSetup X Y


text:
------------------------------------------------------------------------------
-- Exclusive disjunction base
------------------------------------------------------------------------------

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

module FOL.ExclusiveDisjunction.Base where

open import FOL.Base

infixr 1 _⊻_

------------------------------------------------------------------------------
-- Exclusive disjunction.
_⊻_ : Set → Set → Set
P ⊻ Q = (P ∨ Q) ∧ ¬ (P ∧ Q)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Partly based on code due to Andrea Vezzosi.

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

open import Agda.Builtin.Bool

data D : Set where
  run-time        : Bool → D
  @0 compile-time : Bool → D

l : @0 D → D
l (run-time true)  = run-time true
l (run-time false) = run-time false
l (compile-time x) = compile-time x

max_stars_repo_name: guilhermehas/agda

max_issues_repo_name: guilhermehas/agda

max_forks_repo_name: guilhermehas/agda


text:
-- Product of two categories
{-# OPTIONS --safe #-}

module Cubical.Categories.Constructions.BinProduct where

open import Cubical.Categories.Category.Base
open import Cubical.Categories.Functor.Base
open import Cubical.Data.Sigma renaming (_×_ to _×'_)
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude

private
  variable
    ℓC ℓC' ℓD ℓD' ℓE ℓE' : Level

open Category

_×_ : (C : Category ℓC ℓC') → (D : Category ℓD ℓD')
    → Category (ℓ-max ℓC ℓD) (ℓ-max ℓC' ℓD')

(C × D) .ob = (ob C) ×' (ob D)
(C × D) .Hom[_,_] (c , d) (c' , d') = (C [ c , c' ]) ×' (D [ d , d' ])
(C × D) .id = (id C , id D)
(C × D) ._⋆_ _ _ = (_ ⋆⟨ C ⟩ _ , _ ⋆⟨ D ⟩ _)
(C × D) .⋆IdL _ = ≡-× (⋆IdL C _) (⋆IdL D _)
(C × D) .⋆IdR _ = ≡-× (⋆IdR C _) (⋆IdR D _)
(C × D) .⋆Assoc _ _ _ = ≡-× (⋆Assoc C _ _ _) (⋆Assoc D _ _ _)
(C × D) .isSetHom = isSet× (isSetHom C) (isSetHom D)

infixr 5 _×_

-- Some useful functors
module _ (C : Category ℓC ℓC')
         (D : Category ℓD ℓD') where
  open Functor

  module _ (E : Category ℓE ℓE') where
    -- Associativity of product
    ×C-assoc : Functor (C × (D × E)) ((C × D) × E)
    ×C-assoc .F-ob (c , (d , e)) = ((c , d), e)
    ×C-assoc .F-hom (f , (g , h)) = ((f , g), h)
    ×C-assoc .F-id = refl
    ×C-assoc .F-seq _ _ = refl

  -- Left/right injections into product
  linj : (d : ob D) → Functor C (C × D)
  linj d .F-ob c = (c , d)
  linj d .F-hom f = (f , id D)
  linj d .F-id = refl
  linj d .F-seq f g = ≡-× refl (sym (⋆IdL D _))

  rinj : (c : ob C) → Functor D (C × D)
  rinj c .F-ob d = (c , d)
  rinj c .F-hom f = (id C , f)
  rinj c .F-id = refl
  rinj c .F-seq f g = ≡-× (sym (⋆IdL C _)) refl

{-
  TODO:
    - define inverse to `assoc`, prove isomorphism
    - prove product is commutative up to isomorphism
-}

max_stars_repo_name: FernandoLarrain/cubical


text:
-- Basic intuitionistic modal logic S4, without ∨, ⊥, or ◇.
-- Gentzen-style formalisation of syntax with context pairs, after Pfenning-Davies.

module BasicIS4.Syntax.DyadicGentzen where

open import BasicIS4.Syntax.Common public

-- Derivations.

infix 3 _⊢_
data _⊢_ : Cx² Ty Ty → Ty → Set where
  var   : ∀ {A Γ Δ}   → A ∈ Γ → Γ ⁏ Δ ⊢ A
  lam   : ∀ {A B Γ Δ} → Γ , A ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ A ▻ B
  app   : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ▻ B → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ B
  mvar  : ∀ {A Γ Δ}   → A ∈ Δ → Γ ⁏ Δ ⊢ A
  box   : ∀ {A Γ Δ}   → ∅ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ □ A
  unbox : ∀ {A C Γ Δ} → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ , A ⊢ C → Γ ⁏ Δ ⊢ C
  pair  : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ A ∧ B
  fst   : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ∧ B → Γ ⁏ Δ ⊢ A
  snd   : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ∧ B → Γ ⁏ Δ ⊢ B
  unit  : ∀ {Γ Δ}     → Γ ⁏ Δ ⊢ ⊤

infix 3 _⊢⋆_
_⊢⋆_ : Cx² Ty Ty → Cx Ty → Set
Γ ⁏ Δ ⊢⋆ ∅     = 𝟙
Γ ⁏ Δ ⊢⋆ Ξ , A = Γ ⁏ Δ ⊢⋆ Ξ × Γ ⁏ Δ ⊢ A

-- Monotonicity with respect to context inclusion.

mono⊢ : ∀ {A Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢ A → Γ′ ⁏ Δ ⊢ A
mono⊢ η (var i)     = var (mono∈ η i)
mono⊢ η (lam t)     = lam (mono⊢ (keep η) t)
mono⊢ η (app t u)   = app (mono⊢ η t) (mono⊢ η u)
mono⊢ η (mvar i)    = mvar i
mono⊢ η (box t)     = box t
mono⊢ η (unbox t u) = unbox (mono⊢ η t) (mono⊢ η u)
mono⊢ η (pair t u)  = pair (mono⊢ η t) (mono⊢ η u)
mono⊢ η (fst t)     = fst (mono⊢ η t)
mono⊢ η (snd t)     = snd (mono⊢ η t)
mono⊢ η unit        = unit

mono⊢⋆ : ∀ {Ξ Γ Γ′ Δ} → Γ ⊆ Γ′ → Γ ⁏ Δ ⊢⋆ Ξ → Γ′ ⁏ Δ ⊢⋆ Ξ
mono⊢⋆ {∅}     η ∙        = ∙
mono⊢⋆ {Ξ , A} η (ts , t) = mono⊢⋆ η ts , mono⊢ η t

-- Monotonicity with respect to modal context inclusion.

mmono⊢ : ∀ {A Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ′ ⊢ A
mmono⊢ θ (var i)     = var i
mmono⊢ θ (lam t)     = lam (mmono⊢ θ t)
mmono⊢ θ (app t u)   = app (mmono⊢ θ t) (mmono⊢ θ u)
mmono⊢ θ (mvar i)    = mvar (mono∈ θ i)
mmono⊢ θ (box t)     = box (mmono⊢ θ t)
mmono⊢ θ (unbox t u) = unbox (mmono⊢ θ t) (mmono⊢ (keep θ) u)
mmono⊢ θ (pair t u)  = pair (mmono⊢ θ t) (mmono⊢ θ u)
mmono⊢ θ (fst t)     = fst (mmono⊢ θ t)
mmono⊢ θ (snd t)     = snd (mmono⊢ θ t)
mmono⊢ θ unit        = unit

mmono⊢⋆ : ∀ {Ξ Γ Δ Δ′} → Δ ⊆ Δ′ → Γ ⁏ Δ ⊢⋆ Ξ → Γ ⁏ Δ′ ⊢⋆ Ξ
mmono⊢⋆ {∅}     θ ∙        = ∙
mmono⊢⋆ {Ξ , A} θ (ts , t) = mmono⊢⋆ θ ts , mmono⊢ θ t

-- Monotonicity using context pairs.

mono²⊢ : ∀ {A Π Π′} → Π ⊆² Π′ → Π ⊢ A → Π′ ⊢ A
mono²⊢ (η , θ) = mono⊢ η ∘ mmono⊢ θ

-- Shorthand for variables.

v₀ : ∀ {A Γ Δ} → Γ , A ⁏ Δ ⊢ A
v₀ = var i₀

v₁ : ∀ {A B Γ Δ} → Γ , A , B ⁏ Δ ⊢ A
v₁ = var i₁

v₂ : ∀ {A B C Γ Δ} → Γ , A , B , C ⁏ Δ ⊢ A
v₂ = var i₂

mv₀ : ∀ {A Γ Δ} → Γ ⁏ Δ , A ⊢ A
mv₀ = mvar i₀

mv₁ : ∀ {A B Γ Δ} → Γ ⁏ Δ , A , B ⊢ A
mv₁ = mvar i₁

mv₂ : ∀ {A B C Γ Δ} → Γ ⁏ Δ , A , B , C ⊢ A
mv₂ = mvar i₂

-- Reflexivity.

refl⊢⋆ : ∀ {Γ Δ} → Γ ⁏ Δ ⊢⋆ Γ
refl⊢⋆ {∅}     = ∙
refl⊢⋆ {Γ , A} = mono⊢⋆ weak⊆ refl⊢⋆ , v₀

mrefl⊢⋆ : ∀ {Δ Γ} → Γ ⁏ Δ ⊢⋆ □⋆ Δ
mrefl⊢⋆ {∅}     = ∙
mrefl⊢⋆ {Δ , A} = mmono⊢⋆ weak⊆ mrefl⊢⋆ , box mv₀

mrefl⊢⋆′ : ∀ {Δ Δ′ Γ Γ′} → (∀ {A} → Γ ⁏ Δ ⊢ □ A → Γ′ ⁏ Δ′ ⊢ A) → Γ′ ⁏ Δ′ ⊢⋆ Δ
mrefl⊢⋆′ {∅}     f = ∙
mrefl⊢⋆′ {Δ , B} f = mrefl⊢⋆′ (f ∘ mmono⊢ weak⊆) , f (box mv₀)

-- Deduction theorem is built-in.

lam⋆ : ∀ {Ξ A Γ Δ} → Γ ⧺ Ξ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ Ξ ▻⋯▻ A
lam⋆ {∅}     = I
lam⋆ {Ξ , B} = lam⋆ {Ξ} ∘ lam

lam⋆₀ : ∀ {Γ A Δ} → Γ ⁏ Δ ⊢ A → ∅ ⁏ Δ ⊢ Γ ▻⋯▻ A
lam⋆₀ {∅}     = I
lam⋆₀ {Γ , B} = lam⋆₀ ∘ lam

-- Modal deduction theorem.

mlam : ∀ {A B Γ Δ} → Γ ⁏ Δ , A ⊢ B → Γ ⁏ Δ ⊢ □ A ▻ B
mlam t = lam (unbox v₀ (mono⊢ weak⊆ t))

mlam⋆ : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⧺ Ξ ⊢ A → Γ ⁏ Δ ⊢ □⋆ Ξ ▻⋯▻ A
mlam⋆ {∅}     = I
mlam⋆ {Ξ , B} = mlam⋆ {Ξ} ∘ mlam

mlam⋆₀ : ∀ {Δ A Γ} → Γ ⁏ Δ ⊢ A → Γ ⁏ ∅ ⊢ □⋆ Δ ▻⋯▻ A
mlam⋆₀ {∅}     = I
mlam⋆₀ {Δ , B} = mlam⋆₀ ∘ mlam

-- Detachment theorems.

det : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ▻ B → Γ , A ⁏ Δ ⊢ B
det t = app (mono⊢ weak⊆ t) v₀

det⋆ : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⊢ Ξ ▻⋯▻ A → Γ ⧺ Ξ ⁏ Δ ⊢ A
det⋆ {∅}     = I
det⋆ {Ξ , B} = det ∘ det⋆ {Ξ}

det⋆₀ : ∀ {Γ A Δ} → ∅ ⁏ Δ ⊢ Γ ▻⋯▻ A → Γ ⁏ Δ ⊢ A
det⋆₀ {∅}     = I
det⋆₀ {Γ , B} = det ∘ det⋆₀

mdet : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ A ▻ B → Γ ⁏ Δ , A ⊢ B
mdet t = app (mmono⊢ weak⊆ t) (box mv₀)

mdet⋆ : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⊢ □⋆ Ξ ▻⋯▻ A → Γ ⁏ Δ ⧺ Ξ ⊢ A
mdet⋆ {∅}     = I
mdet⋆ {Ξ , B} = mdet ∘ mdet⋆ {Ξ}

mdet⋆₀ : ∀ {Δ A Γ} → Γ ⁏ ∅ ⊢ □⋆ Δ ▻⋯▻ A → Γ ⁏ Δ ⊢ A
mdet⋆₀ {∅}     = I
mdet⋆₀ {Δ , B} = mdet ∘ mdet⋆₀

-- Context manipulation.

merge : ∀ {Δ A Γ} → Γ ⁏ Δ ⊢ A → Γ ⧺ (□⋆ Δ) ⁏ ∅ ⊢ A
merge {Δ} = det⋆ {□⋆ Δ} ∘ mlam⋆₀

mmerge : ∀ {Γ A Δ} → □⋆ Γ ⁏ Δ ⊢ A → ∅ ⁏ Δ ⧺ Γ ⊢ A
mmerge {Γ} = mdet⋆ {Γ} ∘ lam⋆₀

split : ∀ {Δ A Γ} → Γ ⧺ (□⋆ Δ) ⁏ ∅ ⊢ A → Γ ⁏ Δ ⊢ A
split {Δ} = mdet⋆₀ ∘ lam⋆ {□⋆ Δ}

msplit : ∀ {Γ A Δ} → ∅ ⁏ Δ ⧺ Γ ⊢ A → □⋆ Γ ⁏ Δ ⊢ A
msplit {Γ} = det⋆₀ ∘ mlam⋆ {Γ}

merge⋆ : ∀ {Ξ Δ Γ} → Γ ⁏ Δ ⊢⋆ Ξ → Γ ⧺ (□⋆ Δ) ⁏ ∅ ⊢⋆ Ξ
merge⋆ {∅}     ∙        = ∙
merge⋆ {Ξ , A} (ts , t) = merge⋆ ts , merge t

split⋆ : ∀ {Ξ Δ Γ} → Γ ⧺ (□⋆ Δ) ⁏ ∅ ⊢⋆ Ξ → Γ ⁏ Δ ⊢⋆ Ξ
split⋆ {∅}     ∙        = ∙
split⋆ {Ξ , A} (ts , t) = split⋆ ts , split t

-- Cut and multicut.

cut : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A → Γ , A ⁏ Δ ⊢ B → Γ ⁏ Δ ⊢ B
cut t u = app (lam u) t

mcut : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ , A ⊢ B → Γ ⁏ Δ ⊢ B
mcut t u = app (mlam u) t

multicut : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⊢⋆ Ξ → Ξ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ A
multicut {∅}     ∙        u = mono⊢ bot⊆ u
multicut {Ξ , B} (ts , t) u = app (multicut ts (lam u)) t

mmulticut : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⊢⋆ □⋆ Ξ → Γ ⁏ Ξ ⊢ A → Γ ⁏ Δ ⊢ A
mmulticut {∅}     ∙        u = mmono⊢ bot⊆ u
mmulticut {Ξ , B} (ts , t) u = app (mmulticut ts (mlam u)) t

multicut² : ∀ {Ξ Ξ′ A Γ Δ} → Γ ⁏ Δ ⊢⋆ Ξ → Γ ⁏ Δ ⊢⋆ □⋆ Ξ′ → Ξ ⁏ Ξ′ ⊢ A → Γ ⁏ Δ ⊢ A
multicut² {∅}     ∙        us v = mmulticut us (mono⊢ bot⊆ v)
multicut² {Ξ , B} (ts , t) us v = app (multicut² ts us (lam v)) t

-- Transitivity.

trans⊢⋆₀ : ∀ {Γ″ Γ′ Γ} → Γ ⁏ ∅ ⊢⋆ Γ′ → Γ′ ⁏ ∅ ⊢⋆ Γ″ → Γ ⁏ ∅ ⊢⋆ Γ″
trans⊢⋆₀ {∅}      ts ∙        = ∙
trans⊢⋆₀ {Γ″ , A} ts (us , u) = trans⊢⋆₀ ts us , multicut ts u

trans⊢⋆ : ∀ {Ξ Γ Γ′ Δ Δ′} → Γ ⁏ Δ ⊢⋆ Γ′ ⧺ (□⋆ Δ′) → Γ′ ⁏ Δ′ ⊢⋆ Ξ → Γ ⁏ Δ ⊢⋆ Ξ
trans⊢⋆ ts us = split⋆ (trans⊢⋆₀ (merge⋆ ts) (merge⋆ us))

-- Contraction.

ccont : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ (A ▻ A ▻ B) ▻ A ▻ B
ccont = lam (lam (app (app v₁ v₀) v₀))

cont : ∀ {A B Γ Δ} → Γ , A , A ⁏ Δ ⊢ B → Γ , A ⁏ Δ ⊢ B
cont t = det (app ccont (lam (lam t)))

mcont : ∀ {A B Γ Δ} → Γ ⁏ Δ , A , A ⊢ B → Γ ⁏ Δ , A ⊢ B
mcont t = mdet (app ccont (mlam (mlam t)))

-- Exchange, or Schönfinkel’s C combinator.

cexch : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ (A ▻ B ▻ C) ▻ B ▻ A ▻ C
cexch = lam (lam (lam (app (app v₂ v₀) v₁)))

exch : ∀ {A B C Γ Δ} → Γ , A , B ⁏ Δ ⊢ C → Γ , B , A ⁏ Δ ⊢ C
exch t = det (det (app cexch (lam (lam t))))

mexch : ∀ {A B C Γ Δ} → Γ ⁏ Δ , A , B ⊢ C → Γ ⁏ Δ , B , A ⊢ C
mexch t = mdet (mdet (app cexch (mlam (mlam t))))

-- Composition, or Schönfinkel’s B combinator.

ccomp : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ (B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
ccomp = lam (lam (lam (app v₂ (app v₁ v₀))))

comp : ∀ {A B C Γ Δ} → Γ , B ⁏ Δ ⊢ C → Γ , A ⁏ Δ ⊢ B → Γ , A ⁏ Δ ⊢ C
comp t u = det (app (app ccomp (lam t)) (lam u))

mcomp : ∀ {A B C Γ Δ} → Γ ⁏ Δ , B ⊢ □ C → Γ ⁏ Δ , A ⊢ □ B → Γ ⁏ Δ , A ⊢ □ C
mcomp t u = mdet (app (app ccomp (mlam t)) (mlam u))

-- Useful theorems in functional form.

dist : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ (A ▻ B) → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ ⊢ □ B
dist t u = unbox t (unbox (mmono⊢ weak⊆ u) (box (app mv₁ mv₀)))

up : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ ⊢ □ □ A
up t = unbox t (box (box mv₀))

down : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ ⊢ A
down t = unbox t mv₀

distup : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ (□ A ▻ B) → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ ⊢ □ B
distup t u = dist t (up u)

-- Useful theorems in combinatory form.

ci : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ A ▻ A
ci = lam v₀

ck : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ▻ B ▻ A
ck = lam (lam v₁)

cs : ∀ {A B C Γ Δ} → Γ ⁏ Δ ⊢ (A ▻ B ▻ C) ▻ (A ▻ B) ▻ A ▻ C
cs = lam (lam (lam (app (app v₂ v₀) (app v₁ v₀))))

cdist : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ (A ▻ B) ▻ □ A ▻ □ B
cdist = lam (lam (dist v₁ v₀))

cup : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ □ A ▻ □ □ A
cup = lam (up v₀)

cdown : ∀ {A Γ Δ} → Γ ⁏ Δ ⊢ □ A ▻ A
cdown = lam (down v₀)

cdistup : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ (□ A ▻ B) ▻ □ A ▻ □ B
cdistup = lam (lam (dist v₁ (up v₀)))

cunbox : ∀ {A C Γ Δ} → Γ ⁏ Δ ⊢ □ A ▻ (□ A ▻ C) ▻ C
cunbox = lam (lam (app v₀ v₁))

cpair : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ▻ B ▻ A ∧ B
cpair = lam (lam (pair v₁ v₀))

cfst : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ∧ B ▻ A
cfst = lam (fst v₀)

csnd : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ∧ B ▻ B
csnd = lam (snd v₀)

-- Internalisation, or lifting, and additional theorems.

lift : ∀ {Γ A Δ} → Γ ⁏ Δ ⊢ A → □⋆ Γ ⁏ Δ ⊢ □ A
lift {∅}     t = box t
lift {Γ , B} t = det (app cdist (lift (lam t)))

hypup : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ A ▻ B → Γ ⁏ Δ ⊢ □ A ▻ B
hypup t = lam (app (mono⊢ weak⊆ t) (down v₀))

hypdown : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ □ A ▻ B → Γ ⁏ Δ ⊢ □ A ▻ B
hypdown t = lam (app (mono⊢ weak⊆ t) (up v₀))

cxup : ∀ {Γ A Δ} → Γ ⁏ Δ ⊢ A → □⋆ Γ ⁏ Δ ⊢ A
cxup {∅}     t = t
cxup {Γ , B} t = det (hypup (cxup (lam t)))

cxdown : ∀ {Γ A Δ} → □⋆ □⋆ Γ ⁏ Δ ⊢ A → □⋆ Γ ⁏ Δ ⊢ A
cxdown {∅}     t = t
cxdown {Γ , B} t = det (hypdown (cxdown (lam t)))

box⋆ : ∀ {Ξ Γ Δ} → ∅ ⁏ Δ ⊢⋆ Ξ → Γ ⁏ Δ ⊢⋆ □⋆ Ξ
box⋆ {∅}     ∙        = ∙
box⋆ {Ξ , A} (ts , t) = box⋆ ts , box t

lift⋆ : ∀ {Ξ Γ Δ} → Γ ⁏ Δ ⊢⋆ Ξ → □⋆ Γ ⁏ Δ ⊢⋆ □⋆ Ξ
lift⋆ {∅}     ∙        = ∙
lift⋆ {Ξ , A} (ts , t) = lift⋆ ts , lift t

up⋆ : ∀ {Ξ Γ Δ} → Γ ⁏ Δ ⊢⋆ □⋆ Ξ → Γ ⁏ Δ ⊢⋆ □⋆ □⋆ Ξ
up⋆ {∅}     ∙        = ∙
up⋆ {Ξ , A} (ts , t) = up⋆ ts , up t

down⋆ : ∀ {Ξ Γ Δ} → Γ ⁏ Δ ⊢⋆ □⋆ Ξ → Γ ⁏ Δ ⊢⋆ Ξ
down⋆ {∅}     ∙        = ∙
down⋆ {Ξ , A} (ts , t) = down⋆ ts , down t

multibox : ∀ {Ξ A Γ Δ} → Γ ⁏ Δ ⊢⋆ □⋆ Ξ → □⋆ Ξ ⁏ ∅ ⊢ A → Γ ⁏ Δ ⊢ □ A
multibox ts u = multicut (up⋆ ts) (mmono⊢ bot⊆ (lift u))

dist′ : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ (A ▻ B) → Γ ⁏ Δ ⊢ □ A ▻ □ B
dist′ t = lam (dist (mono⊢ weak⊆ t) v₀)

mpair : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ A → Γ ⁏ Δ ⊢ □ B → Γ ⁏ Δ ⊢ □ (A ∧ B)
mpair t u = unbox t (unbox (mmono⊢ weak⊆ u) (box (pair mv₁ mv₀)))

mfst : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ (A ∧ B) → Γ ⁏ Δ ⊢ □ A
mfst t = unbox t (box (fst mv₀))

msnd : ∀ {A B Γ Δ} → Γ ⁏ Δ ⊢ □ (A ∧ B) → Γ ⁏ Δ ⊢ □ B
msnd t = unbox t (box (snd mv₀))

-- Closure under context concatenation.

concat : ∀ {A B Γ} Γ′ {Δ} → Γ , A ⁏ Δ ⊢ B → Γ′ ⁏ Δ ⊢ A → Γ ⧺ Γ′ ⁏ Δ ⊢ B
concat Γ′ t u = app (mono⊢ (weak⊆⧺₁ Γ′) (lam t)) (mono⊢ weak⊆⧺₂ u)

mconcat : ∀ {A B Γ Δ} Δ′ → Γ ⁏ Δ , A ⊢ B → Γ ⁏ Δ′ ⊢ □ A → Γ ⁏ Δ ⧺ Δ′ ⊢ B
mconcat Δ′ t u = app (mmono⊢ (weak⊆⧺₁ Δ′) (mlam t)) (mmono⊢ weak⊆⧺₂ u)

-- Substitution.

[_≔_]_ : ∀ {A B Γ Δ} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ B → Γ ∖ i ⁏ Δ ⊢ B
[ i ≔ s ] var j     with i ≟∈ j
[ i ≔ s ] var .i    | same   = s
[ i ≔ s ] var ._    | diff j = var j
[ i ≔ s ] lam t     = lam ([ pop i ≔ mono⊢ weak⊆ s ] t)
[ i ≔ s ] app t u   = app ([ i ≔ s ] t) ([ i ≔ s ] u)
[ i ≔ s ] mvar j    = mvar j
[ i ≔ s ] box t     = box t
[ i ≔ s ] unbox t u = unbox ([ i ≔ s ] t) ([ i ≔ mmono⊢ weak⊆ s ] u)
[ i ≔ s ] pair t u  = pair ([ i ≔ s ] t) ([ i ≔ s ] u)
[ i ≔ s ] fst t     = fst ([ i ≔ s ] t)
[ i ≔ s ] snd t     = snd ([ i ≔ s ] t)
[ i ≔ s ] unit      = unit

[_≔_]⋆_ : ∀ {Ξ A Γ Δ} → (i : A ∈ Γ) → Γ ∖ i ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢⋆ Ξ → Γ ∖ i ⁏ Δ ⊢⋆ Ξ
[_≔_]⋆_ {∅}     i s ∙        = ∙
[_≔_]⋆_ {Ξ , B} i s (ts , t) = [ i ≔ s ]⋆ ts , [ i ≔ s ] t

-- Modal substitution.

m[_≔_]_ : ∀ {A B Γ Δ} → (i : A ∈ Δ) → ∅ ⁏ Δ ∖ i ⊢ A → Γ ⁏ Δ ⊢ B → Γ ⁏ Δ ∖ i ⊢ B
m[ i ≔ s ] var j     = var j
m[ i ≔ s ] lam t     = lam (m[ i ≔ s ] t)
m[ i ≔ s ] app t u   = app (m[ i ≔ s ] t) (m[ i ≔ s ] u)
m[ i ≔ s ] mvar j    with i ≟∈ j
m[ i ≔ s ] mvar .i   | same   = mono⊢ bot⊆ s
m[ i ≔ s ] mvar ._   | diff j = mvar j
m[ i ≔ s ] box t     = box (m[ i ≔ s ] t)
m[ i ≔ s ] unbox t u = unbox (m[ i ≔ s ] t) (m[ pop i ≔ mmono⊢ weak⊆ s ] u)
m[ i ≔ s ] pair t u  = pair (m[ i ≔ s ] t) (m[ i ≔ s ] u)
m[ i ≔ s ] fst t     = fst (m[ i ≔ s ] t)
m[ i ≔ s ] snd t     = snd (m[ i ≔ s ] t)
m[ i ≔ s ] unit      = unit

m[_≔_]⋆_ : ∀ {Ξ A Γ Δ} → (i : A ∈ Δ) → ∅ ⁏ Δ ∖ i ⊢ A → Γ ⁏ Δ ⊢⋆ Ξ → Γ ⁏ Δ ∖ i ⊢⋆ Ξ
m[_≔_]⋆_ {∅}     i s ∙        = ∙
m[_≔_]⋆_ {Ξ , B} i s (ts , t) = m[ i ≔ s ]⋆ ts , m[ i ≔ s ] t

-- Convertibility.

data _⋙_ {Γ Δ : Cx Ty} : ∀ {A} → Γ ⁏ Δ ⊢ A → Γ ⁏ Δ ⊢ A → Set where
  refl⋙      : ∀ {A} → {t : Γ ⁏ Δ ⊢ A}
                      → t ⋙ t

  trans⋙     : ∀ {A} → {t t′ t″ : Γ ⁏ Δ ⊢ A}
                      → t ⋙ t′ → t′ ⋙ t″
                      → t ⋙ t″

  sym⋙       : ∀ {A} → {t t′ : Γ ⁏ Δ ⊢ A}
                      → t ⋙ t′
                      → t′ ⋙ t

  conglam⋙   : ∀ {A B} → {t t′ : Γ , A ⁏ Δ ⊢ B}
                        → t ⋙ t′
                        → lam t ⋙ lam t′

  congapp⋙   : ∀ {A B} → {t t′ : Γ ⁏ Δ ⊢ A ▻ B} → {u u′ : Γ ⁏ Δ ⊢ A}
                        → t ⋙ t′ → u ⋙ u′
                        → app t u ⋙ app t′ u′

  -- NOTE: Rejected by Pfenning and Davies.
  -- congbox⋙   : ∀ {A} → {t t′ : ∅ ⁏ Δ ⊢ A}
  --                     → t ⋙ t′
  --                     → box {Γ} t ⋙ box {Γ} t′

  congunbox⋙ : ∀ {A C} → {t t′ : Γ ⁏ Δ ⊢ □ A} → {u u′ : Γ ⁏ Δ , A ⊢ C}
                        → t ⋙ t′ → u ⋙ u′
                        → unbox t u ⋙ unbox t′ u′

  congpair⋙  : ∀ {A B} → {t t′ : Γ ⁏ Δ ⊢ A} → {u u′ : Γ ⁏ Δ ⊢ B}
                        → t ⋙ t′ → u ⋙ u′
                        → pair t u ⋙ pair t′ u′

  congfst⋙   : ∀ {A B} → {t t′ : Γ ⁏ Δ ⊢ A ∧ B}
                        → t ⋙ t′
                        → fst t ⋙ fst t′

  congsnd⋙   : ∀ {A B} → {t t′ : Γ ⁏ Δ ⊢ A ∧ B}
                        → t ⋙ t′
                        → snd t ⋙ snd t′

  beta▻⋙     : ∀ {A B} → {t : Γ , A ⁏ Δ ⊢ B} → {u : Γ ⁏ Δ ⊢ A}
                        → app (lam t) u ⋙ ([ top ≔ u ] t)

  eta▻⋙      : ∀ {A B} → {t : Γ ⁏ Δ ⊢ A ▻ B}
                        → t ⋙ lam (app (mono⊢ weak⊆ t) v₀)

  beta□⋙     : ∀ {A C} → {t : ∅ ⁏ Δ ⊢ A} → {u : Γ ⁏ Δ , A ⊢ C}
                        → unbox (box t) u ⋙ (m[ top ≔ t ] u)

  eta□⋙      : ∀ {A} → {t : Γ ⁏ Δ ⊢ □ A}
                      → t ⋙ unbox t (box mv₀)

  -- TODO: What about commuting conversions for □?

  beta∧₁⋙    : ∀ {A B} → {t : Γ ⁏ Δ ⊢ A} → {u : Γ ⁏ Δ ⊢ B}
                        → fst (pair t u) ⋙ t

  beta∧₂⋙    : ∀ {A B} → {t : Γ ⁏ Δ ⊢ A} → {u : Γ ⁏ Δ ⊢ B}
                        → snd (pair t u) ⋙ u

  eta∧⋙      : ∀ {A B} → {t : Γ ⁏ Δ ⊢ A ∧ B}
                        → t ⋙ pair (fst t) (snd t)

  eta⊤⋙     : ∀ {t : Γ ⁏ Δ ⊢ ⊤} → t ⋙ unit

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
-- MIT License

-- Copyright (c) 2021 Luca Ciccone and Luca Padovani

-- Permission is hereby granted, free of charge, to any person
-- obtaining a copy of this software and associated documentation
-- files (the "Software"), to deal in the Software without
-- restriction, including without limitation the rights to use,
-- copy, modify, merge, publish, distribute, sublicense, and/or sell
-- copies of the Software, and to permit persons to whom the
-- Software is furnished to do so, subject to the following
-- conditions:

-- The above copyright notice and this permission notice shall be
-- included in all copies or substantial portions of the Software.

-- THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-- EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
-- OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
-- NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
-- HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
-- WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
-- FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-- OTHER DEALINGS IN THE SOFTWARE.

{-# OPTIONS --guardedness #-}

open import Data.Empty
open import Data.Product
open import Data.List using ([]; _∷_; _∷ʳ_; _++_)

open import Relation.Nullary
open import Relation.Unary using (_∈_; _⊆_;_∉_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
import Relation.Binary.HeterogeneousEquality as Het

open import Common

module HasTrace {ℙ : Set} (message : Message ℙ)
  where

open import Trace message
open import SessionType message
open import Transitions message

_HasTrace_ : SessionType -> Trace -> Set
_HasTrace_ T φ = ∃[ S ] (Defined S × Transitions T φ S)

after : ∀{T φ} -> T HasTrace φ -> SessionType
after (S , _ , _) = S

-- data _HasTrace_ : SessionType -> Trace -> Set where
--   does : ∀{T φ S} (tr : Transitions T φ S) (def : Defined S) -> T Does φ

_HasTrace?_ : (T : SessionType) (φ : Trace) -> Dec (T HasTrace φ)
nil HasTrace? _ = no λ { (_ , () , refl)
                       ; (_ , _ , step () _) }
inp f HasTrace? [] = yes (_ , inp , refl)
inp f HasTrace? (I x ∷ φ) with x ∈? f
... | no nfx = no λ { (_ , def , step inp tr) → nfx (transitions+defined->defined tr def) }
... | yes fx with f x .force HasTrace? φ
... | yes (_ , def , tr) = yes (_ , def , step inp tr)
... | no ntφ = no λ { (_ , def , step inp tr) → ntφ (_ , def , tr) }
inp f HasTrace? (O x ∷ φ) = no λ { (_ , _ , step () _) }
out f HasTrace? [] = yes (_ , out , refl)
out f HasTrace? (I x ∷ φ) = no λ { (_ , _ , step () _) }
out f HasTrace? (O x ∷ φ) with x ∈? f
... | no nfx = no λ { (_ , _ , step (out fx) _) → nfx fx }
... | yes fx with f x .force HasTrace? φ
... | yes (_ , def , tr) = yes (_ , def , step (out fx) tr)
... | no ntφ = no λ { (_ , def , step (out fx) tr) → ntφ (_ , def , tr) }

has-trace->defined : ∀{T φ} -> T HasTrace φ -> Defined T
has-trace->defined (_ , tdef , tr) = transitions+defined->defined tr tdef

inp-has-trace : ∀{f x φ} -> f x .force HasTrace φ -> inp f HasTrace (I x ∷ φ)
inp-has-trace (_ , def , tr) = _ , def , step inp tr

inp-has-no-trace : ∀{f x φ} -> ¬ f x .force HasTrace φ -> ¬ inp f HasTrace (I x ∷ φ)
inp-has-no-trace nφ (_ , def , step inp tr) = nφ (_ , def , tr)

out-has-trace : ∀{f x φ} -> f x .force HasTrace φ -> out f HasTrace (O x ∷ φ)
out-has-trace (_ , def , tr) = _ , def , step (out (transitions+defined->defined tr def)) tr

out-has-no-trace : ∀{f x φ} -> ¬ f x .force HasTrace φ -> ¬ out f HasTrace (O x ∷ φ)
out-has-no-trace nφ (_ , def , step (out fx) tr) = nφ (_ , def , tr)

out-has-no-trace->undefined : ∀{f x} -> ¬ out f HasTrace (O x ∷ []) -> ¬ Defined (f x .force)
out-has-no-trace->undefined {f} {x} nt with x ∈? f
... | yes fx = ⊥-elim (nt (_ , fx , step (out fx) refl))
... | no nfx = nfx

unprefix-some : ∀{α φ ψ} -> (α ∷ ψ) ⊑ (α ∷ φ) -> ψ ⊑ φ
unprefix-some (some pre) = pre

⊑-has-trace : ∀{T φ ψ} -> ψ ⊑ φ -> T HasTrace φ -> T HasTrace ψ
⊑-has-trace none (_ , tdef , tr) = _ , transitions+defined->defined tr tdef , refl
⊑-has-trace (some pre) (_ , tdef , step t tr) =
  let _ , sdef , sr = ⊑-has-trace pre (_ , tdef , tr) in
  _ , sdef , step t sr

split-trace : ∀{T φ ψ} (tφ : T HasTrace φ) -> T HasTrace (φ ++ ψ) -> after tφ HasTrace ψ
split-trace (_ , tdef , refl) tφψ = tφψ
split-trace (_ , tdef , step inp tr) (_ , sdef , step inp sr) = split-trace (_ , tdef , tr) (_ , sdef , sr)
split-trace (_ , tdef , step (out _) tr) (_ , sdef , step (out _) sr) = split-trace (_ , tdef , tr) (_ , sdef , sr)

join-trace : ∀{T φ ψ} (tφ : T HasTrace φ) -> after tφ HasTrace ψ -> T HasTrace (φ ++ ψ)
join-trace (_ , _ , refl) tφ/ψ = tφ/ψ
join-trace (_ , tdef , step t tr) tφ/ψ =
  let (_ , sdef , sr) = join-trace (_ , tdef , tr) tφ/ψ in
  _ , sdef , step t sr

⊑-has-co-trace : ∀{T φ ψ} -> φ ⊑ ψ -> T HasTrace (co-trace ψ) -> T HasTrace (co-trace φ)
⊑-has-co-trace le tψ = ⊑-has-trace (⊑-co-trace le) tψ

⊑-tran-has-trace : ∀{T φ ψ χ} (pre1 : φ ⊑ ψ) (pre2 : ψ ⊑ χ) ->
  (tχ : T HasTrace χ) ->
  ⊑-has-trace pre1 (⊑-has-trace pre2 tχ) ≡ ⊑-has-trace (⊑-tran pre1 pre2) tχ
⊑-tran-has-trace none none tχ = refl
⊑-tran-has-trace none (some pre2) (fst , fst₁ , step t snd) = refl
⊑-tran-has-trace (some pre1) (some pre2) (_ , def , step _ tr) rewrite ⊑-tran-has-trace pre1 pre2 (_ , def , tr) = refl

⊑-has-trace-after : ∀{T φ} (tφ : T HasTrace φ) -> ⊑-has-trace (⊑-refl φ) tφ ≡ tφ
⊑-has-trace-after (_ , _ , refl) = refl
⊑-has-trace-after (_ , tdef , step inp tr) rewrite ⊑-has-trace-after (_ , tdef , tr) = refl
⊑-has-trace-after (_ , tdef , step (out _) tr) rewrite ⊑-has-trace-after (_ , tdef , tr) = refl

nil-has-no-trace : ∀{φ} -> ¬ nil HasTrace φ
nil-has-no-trace (_ , () , refl)
nil-has-no-trace (_ , _ , step () _)

end-has-empty-trace : ∀{φ T} -> End T -> T HasTrace φ -> φ ≡ []
end-has-empty-trace (inp U) (_ , _ , refl) = refl
end-has-empty-trace (inp U) (_ , def , step inp refl) = ⊥-elim (U _ def)
end-has-empty-trace (inp U) (_ , def , step inp (step t _)) = ⊥-elim (U _ (transition->defined t))
end-has-empty-trace (out U) (_ , _ , refl) = refl
end-has-empty-trace (out U) (_ , _ , step (out !x) _) = ⊥-elim (U _ !x)

has-trace-++ : ∀{T φ ψ} -> T HasTrace (φ ++ ψ) -> T HasTrace φ
has-trace-++ tφψ = ⊑-has-trace ⊑-++ tφψ

trace-coherence : ∀{T φ ψ₁ ψ₂ x y} -> T HasTrace (φ ++ I x ∷ ψ₁) -> T HasTrace (φ ++ O y ∷ ψ₂) -> ⊥
trace-coherence {_} {[]} (_ , _ , step inp _) (_ , _ , step () _)
trace-coherence {_} {I _ ∷ _} (_ , tdef , step inp tr) (_ , sdef , step inp sr) = trace-coherence (_ , tdef , tr) (_ , sdef , sr)
trace-coherence {_} {O _ ∷ _} (_ , tdef , step (out _) tr) (_ , sdef , step (out _) sr) = trace-coherence (_ , tdef , tr) (_ , sdef , sr)

defined->has-empty-trace : ∀{T} -> Defined T -> T HasTrace []
defined->has-empty-trace inp = _ , inp , refl
defined->has-empty-trace out = _ , out , refl

has-trace-double-negation : ∀{T φ} -> ¬ ¬ T HasTrace φ -> T HasTrace φ
has-trace-double-negation {T} {φ} p with T HasTrace? φ
... | yes tφ = tφ
... | no ntφ = ⊥-elim (p ntφ)

{- New -}
not-nil-has-trace : ∀{ϕ} → ¬ (nil HasTrace ϕ)
not-nil-has-trace (.(inp _) , inp , step () _)
not-nil-has-trace (.(out _) , out , step () _)

trace-after-in : ∀{f x ϕ} → (inp f) HasTrace (I x ∷ ϕ) → (f x .force) HasTrace ϕ
trace-after-in (_ , def , step inp red) = _ , def , red

trace-after-out : ∀{f x ϕ} → (out f) HasTrace (O x ∷ ϕ) → (f x .force) HasTrace ϕ
trace-after-out (_ , def , step (out _) red) = _ , def , red

inp-hastrace->defined : ∀{f x tr} → (inp f) HasTrace (I x ∷ tr) → x ∈ dom f
inp-hastrace->defined (_ , def , step inp refl) = def
inp-hastrace->defined (_ , def , step inp (step red _)) = transition->defined red

empty-inp-has-empty-trace : ∀{f ϕ} → EmptyContinuation f → (inp f) HasTrace ϕ → ϕ ≡ []
empty-inp-has-empty-trace e (_ , _ , refl) = refl
empty-inp-has-empty-trace {f} e (_ , _ , step (inp {x = x}) reds) with Defined? (f x .force)
empty-inp-has-empty-trace {f} e (_ , def , step (inp {x = _}) refl) | no ¬def = ⊥-elim (¬def def)
empty-inp-has-empty-trace {f} e (_ , _ , step (inp {x = _}) (step t _)) | no ¬def = ⊥-elim (¬def (transition->defined t))
... | yes def = ⊥-elim (e _ def)

empty-out-has-empty-trace : ∀{f ϕ} → EmptyContinuation f → (out f) HasTrace ϕ → ϕ ≡ []
empty-out-has-empty-trace e (_ , _ , refl) = refl
empty-out-has-empty-trace e (_ , _ , step (out def) _) = ⊥-elim (e _ def)

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
-- This module introduces parameterised modules.

module Introduction.Modules.Parameterised where

-- First some familiar datatypes.

data Bool : Set where
  false : Bool
  true  : Bool

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

infixr 15 _::_    -- see 'Introduction.Operators' for information on infix
                  -- declarations

-- Agda supports parameterised modules. A parameterised module is declared by
-- giving the parameters after the module name.

module Sorting {A : Set}(_<_ : A -> A -> Bool) where

  insert : A -> List A -> List A
  insert x  nil      = x :: nil
  insert x (y :: ys) = ins (x < y)
    where
      ins : Bool -> List A      -- local functions can do pattern matching and
      ins true  = x :: y :: ys  -- be recursive
      ins false = y :: insert x ys

  sort : List A -> List A
  sort  nil      = nil
  sort (x :: xs) = insert x (sort xs)

-- Before a parameterised module can be used it has to be instantiated. So, we
-- need something to instantiate it with.

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

_<_ : Nat -> Nat -> Bool
zero  < zero  = false
zero  < suc _ = true
suc _ < zero  = false
suc n < suc m = n < m

-- To instantiate a module you define a new module in terms of the
-- parameterised module. Module instantiation also supports the using, hiding
-- and renaming modifiers.
module SortNat = Sorting _<_

sort' : {A : Set}(_<_ : A -> A -> Bool) -> List A -> List A
sort' less = Sort'.sort
  where
    module Sort' = Sorting less

-- Now the instantiated module can be opened and we can use the sorting
-- function.
open SortNat

test = sort (suc zero :: zero :: suc (suc zero) :: nil)


text:
module MessageClosure where

open import Data.Fin using (Fin; zero; suc; toℕ)
open import Data.Nat
open import Function

open import Types.IND1 as IND
import Types.Tail1 as Tail

private
  variable
    m n : ℕ

-- message closure guarantees that the type of each message in a session type is closed

upS : SType m → SType (suc m)
upG : GType m → GType (suc m)
upT : Type m → Type (suc m)

upS (gdd G) = gdd (upG G)
upS (rec G) = rec (upG G)
upS (var x) = var (suc x)

upG (transmit d T S) = transmit d (upT T) (upS S)
upG (choice d m alt) = choice d m (upS ∘ alt)
upG end = end

upT TUnit = TUnit
upT TInt = TInt
upT (TPair t t₁) = TPair (upT t) (upT t₁)
upT (TChan S) = TChan (upS S)

shift : (Fin (m + n) → SType m) → (Fin (suc m + n) → SType (suc m))
shift σ zero = var zero
shift σ (suc x) = upS (σ x)

applyT : (Fin (m + n) → SType m) → TType (m + n) → TType m
applyS : (Fin (m + n) → SType m) → SType (m + n) → SType m
applyG : (Fin (m + n) → SType m) → GType (m + n) → GType m

applyT σ TUnit = TUnit
applyT σ TInt = TInt
applyT σ (TPair T T₁) = TPair (applyT σ T) (applyT σ T₁)
applyT σ (TChan x) = TChan (applyS σ x)

applyS σ (gdd gst) = gdd (applyG σ gst)
applyS σ (rec gst) = rec (applyG (shift σ) gst)
applyS σ (var x) = σ x

applyG σ (transmit d t s) = transmit d (applyT σ t) (applyS σ s)
applyG σ (choice d m alt) = choice d m (applyS σ ∘ alt)
applyG σ end = end

injectT : TType 0 → Tail.Type

injectT TUnit = Tail.TUnit
injectT TInt = Tail.TInt
injectT (TPair t t₁) = Tail.TPair (injectT t) (injectT t₁)
injectT (TChan S) = Tail.TChan S

ext : (Fin n → SType 0) → SType n → (Fin (suc n) → SType 0)

ext σ S zero = applyS σ S
ext σ S (suc i) = σ i

mcloS : (Fin n → SType 0) → SType n → Tail.SType n
mcloG : (Fin n → SType 0) → GType n → Tail.GType n

mcloS σ (gdd gst) = Tail.gdd (mcloG σ gst)
mcloS σ (rec gst) = Tail.rec (mcloG (ext σ (rec gst)) gst)
mcloS σ (var x) = Tail.var x

mcloG σ (transmit d t s) = Tail.transmit d (injectT (applyT σ t)) (mcloS σ s)
mcloG σ (choice d m alt) = Tail.choice d m (mcloS σ ∘ alt)
mcloG σ end = Tail.end

mclosureS : SType 0 → Tail.SType 0
mclosureS = mcloS IND.var

mclosureG : GType 0 → Tail.GType 0
mclosureG = mcloG IND.var

max_stars_repo_name: peterthiemann/dual-session

max_issues_repo_name: peterthiemann/dual-session

max_forks_repo_name: peterthiemann/dual-session


text:
module main where

import string-format
-- for parser for Cedille
open import cedille-types

-- for parser for options files
import options-types
import cedille-options

-- for parser for Cedille comments & whitespace
import cws-types

import io
open import constants
open import general-util
open import json

record cedille-args : Set where
  constructor mk-cedille-args
  field
    opts-file : maybe filepath
    file-to-process : maybe filepath
    about     : 𝔹
    help      : 𝔹
    do-elab   : maybe filepath
    confirm-read-stdin : 𝔹

default-cedille-args =
  record { opts-file = nothing ;
           file-to-process = nothing ;
           about = ff ;
           help = ff ;
           do-elab = nothing ;
           confirm-read-stdin = ff}

-- get $HOME/.cedille, creating it if it does not exist
getHomeCedilleDirectory : IO filepath
getHomeCedilleDirectory =
  getHomeDirectory >>= λ home →
  let d = dot-cedille-directory home in
    io.createDirectoryIfMissing ff d >>
    return d

postulate
  initializeStdinToUTF8 : IO ⊤
  setStdinNewlineMode : IO ⊤
  compileTime : UTC
  templatesDir : filepath
  die : {A : Set} → 𝕃 char → IO A

{-# FOREIGN GHC {-# LANGUAGE TemplateHaskell #-} #-}
{-# FOREIGN GHC import qualified System.IO #-}
{-# FOREIGN GHC import qualified System.Exit #-}
{-# FOREIGN GHC import qualified Data.Time.Clock #-}
{-# FOREIGN GHC import qualified Data.Time.Format #-}
{-# FOREIGN GHC import qualified Data.Time.Clock.POSIX #-}
{-# FOREIGN GHC import qualified Language.Haskell.TH.Syntax #-}
{-# COMPILE GHC die = \ _ -> System.Exit.die #-}
{-# COMPILE GHC initializeStdinToUTF8 = System.IO.hSetEncoding System.IO.stdin System.IO.utf8 #-}
{-# COMPILE GHC setStdinNewlineMode = System.IO.hSetNewlineMode System.IO.stdin System.IO.universalNewlineMode #-}
{-# COMPILE GHC compileTime =
  maybe (Data.Time.Clock.POSIX.posixSecondsToUTCTime (fromIntegral 0)) id
  (Data.Time.Format.parseTimeM True Data.Time.Format.defaultTimeLocale "%s"
    $(Language.Haskell.TH.Syntax.runIO
      (Data.Time.Clock.getCurrentTime >>= \ t ->
       return (Language.Haskell.TH.Syntax.LitE
         (Language.Haskell.TH.Syntax.StringL
           (Data.Time.Format.formatTime Data.Time.Format.defaultTimeLocale "%s" t)))))
    :: Maybe Data.Time.Clock.UTCTime) #-}

say-about : filepath → IO ⊤
say-about optfp =
   putStrLn $ "Compiled:     " ^ (utcToString compileTime) ^ "\n" ^
              "Options file: " ^ optfp ^ "\n"

createOptionsFile : (dot-ced-dir : string) → IO ⊤
createOptionsFile dot-ced-dir =
  let ops-fp = combineFileNames dot-ced-dir options-file-name in
  createDirectoryIfMissing ff (takeDirectory ops-fp) >>
  withFile ops-fp WriteMode (flip hPutRope (cedille-options.options-to-rope cedille-options.default-options))

options-absolute-path : (options-fp some-fp : filepath) → IO filepath
options-absolute-path ofp fp =
  (filepath-replace-tilde fp >>= flip maybe-else return
    (doesFileExist fp >>=r λ fpₑ →
      if fpₑ then fp else combineFileNames (takeDirectory (takeDirectory ofp)) fp))
  >>= canonicalizePath

opts-to-options : filepath → options-types.opts → IO cedille-options.options
opts-to-options ofp (options-types.OptsCons (options-types.Lib fps) ops) =
  opts-to-options ofp ops >>= λ ops → paths-to-stringset fps >>=r λ ip → record ops { include-path = ip }
  where paths-to-stringset : options-types.paths → IO (𝕃 string × stringset)
        paths-to-stringset (options-types.PathsCons fp fps) =
          let rfp = combineFileNames (takeDirectory (takeDirectory ofp)) fp in
          paths-to-stringset fps >>= λ ps →
          doesDirectoryExist rfp >>= λ rfpₑ →
          doesDirectoryExist fp >>= λ fpₑ →
          (if rfpₑ
            then (canonicalizePath rfp >>= λ rfp →
                  return (cedille-options.include-path-insert rfp ps))
            else return ps) >>= λ ps →
          if fpₑ
            then (canonicalizePath fp >>= λ fp →
                  return (cedille-options.include-path-insert fp ps))
            else return ps
        paths-to-stringset options-types.PathsNil = return ([] , empty-stringset)
opts-to-options ofp (options-types.OptsCons (options-types.UseCedeFiles b) ops) =
  opts-to-options ofp ops >>=r λ ops → record ops { use-cede-files = b }
opts-to-options ofp (options-types.OptsCons (options-types.MakeRktFiles b) ops) =
  opts-to-options ofp ops >>=r λ ops → record ops { make-rkt-files = b }
opts-to-options ofp (options-types.OptsCons (options-types.GenerateLogs b) ops) =
  opts-to-options ofp ops >>=r λ ops → record ops { generate-logs = b }
opts-to-options ofp (options-types.OptsCons (options-types.ShowQualifiedVars b) ops) =
  opts-to-options ofp ops >>=r λ ops → record ops { show-qualified-vars = b }
opts-to-options ofp (options-types.OptsCons (options-types.EraseTypes b) ops) =
  opts-to-options ofp ops >>=r λ ops → record ops { erase-types = b }
opts-to-options ofp (options-types.OptsCons (options-types.PrettyPrintColumns b) ops) =
  opts-to-options ofp ops >>=r λ ops → record ops { pretty-print-columns = string-to-ℕ0 b }
opts-to-options ofp (options-types.OptsCons (options-types.DatatypeEncoding fp?) ops) =
  maybe-map (options-absolute-path ofp) fp? >>=? λ fp? →
  opts-to-options ofp ops >>=r λ ops → record ops { datatype-encoding = (_, nothing) <$> fp? }
opts-to-options ofp options-types.OptsNil = return cedille-options.default-options

-- helper function to try to parse the options file
processOptions : filepath → string → IO (string ⊎ cedille-options.options)
processOptions filename s with options-types.scanOptions s
...| options-types.Left cs = return (inj₁ ("Parse error in file " ^ filename ^ " " ^ cs ^ "."))
...| options-types.Right (options-types.File oo) =
  opts-to-options filename oo
  >>= λ opts → if cedille-options.options.make-rkt-files opts
    then return ∘ inj₁ $ "Racket compilation disabled, please set to false in " ^ filename ^ "."
  else (return ∘ inj₂ $ opts)

getOptionsFile : (filepath : string) → string
getOptionsFile fp = combineFileNames (dot-cedille-directory fp) options-file-name

findOptionsFile' : (filepath : string) → IO (maybe string)
findOptionsFile' fp =
  traverseParents fp (fp-fuel fp)
  >>= λ where
    fpc?@(just fpc) → return fpc?
    nothing → getHomeDirectory >>= getOptions?

  where
  getOptions? : (filepath : string) → IO ∘ maybe $ string
  getOptions? fp =
    let fpc = getOptionsFile fp in
    doesFileExist fpc >>= λ where
      ff → return nothing
      tt → return ∘ just $ fpc

  traverseParents : string → ℕ → IO (maybe string)
  traverseParents fp 0 = return nothing
  traverseParents fp (suc n) =
    getOptions? fp >>= λ where
      nothing → traverseParents (takeDirectory fp) n
      fpc?@(just fpc) → return fpc?

  fp-fuel : (filepath : string) → ℕ
  fp-fuel fp = pred ∘' length ∘' splitPath $ fp

findOptionsFile : IO (maybe string)
findOptionsFile =
  (getCurrentDirectory >>= canonicalizePath) >>= findOptionsFile'

readOptions : maybe filepath → IO (filepath × cedille-options.options)
readOptions nothing =
  getHomeCedilleDirectory >>= λ home →
  createOptionsFile home >>r
  dot-cedille-directory home , cedille-options.default-options
readOptions (just fp) = readFiniteFile fp >>= λ fc →
  processOptions fp fc >>= λ where
    (inj₁ err) →
      putStrLn (global-error-string err) >>r
        fp , cedille-options.default-options
    (inj₂ ops) → return (fp , ops)

showCedilleUsage : IO ⊤
showCedilleUsage =
    putStrLn ("Command-line usage: cedille [--e elab-dir | --options options-file | --about ] file-to-check\n"
            ^ "With no arguments, read commands from the front-end on stdin.")

module main-with-options
  (compileTime : UTC)
  (options-filepath : filepath)
  (options : cedille-options.options)
  (die : {A : Set} → 𝕃 char → IO A) where

  open import ctxt
  --open import instances
  open import process-cmd options {IO}
  open import parser
  open import spans options {IO}
  open import syntax-util
  open import to-string options
  open import toplevel-state options {IO}
  open import interactive-cmds options
  open import rkt options
  open import elab-util options
  open import communication-util options

  logFilePathIO : IO filepath
  logFilePathIO = getHomeCedilleDirectory >>=r (flip combineFileNames $ "log")

  maybeClearLogFile : IO filepath
  maybeClearLogFile =
    logFilePathIO >>=
      λ logFilePath →
        ifM (cedille-options.options.generate-logs options) (clearFile logFilePath) >>
        return logFilePath

  fileBaseName : filepath → string
  fileBaseName fn = base-filename (takeFileName fn)

  fileSuffix : filepath → string
  fileSuffix = maybe-else cedille-extension id ∘ var-suffix

  {-------------------------------------------------------------------------------
    .cede support
  -------------------------------------------------------------------------------}

  cede-suffix = ".cede"
  rkt-suffix = ".rkt"

  ced-aux-filename : (suffix ced-path : filepath) → filepath
  ced-aux-filename sfx ced-path =
    let dir = takeDirectory ced-path in
      combineFileNames (dot-cedille-directory dir) (fileBaseName ced-path ^ sfx)

  cede-filename = ced-aux-filename cede-suffix
  rkt-filename = ced-aux-filename rkt-suffix

  maybe-write-aux-file : toplevel-state → include-elt → (create-dot-ced-if-missing : IO ⊤) →
                         (filename file-suffix : filepath) → (cedille-options.options → 𝔹) → (include-elt → 𝔹) → rope → IO ⊤
  maybe-write-aux-file s ie mk-dot-ced fn sfx f f' r with f options && ~ f' ie
  ...| ff = return triv
  ...| tt = mk-dot-ced >>
            logMsg s ("Starting writing " ^ sfx ^ " file " ^ fn) >>
            writeRopeToFile fn r >>
            logMsg s ("Finished writing " ^ sfx ^ " file " ^ fn)

  write-aux-files : toplevel-state → filepath → IO ⊤
  write-aux-files s filename with get-include-elt-if s filename
  ...| nothing = return triv
  ...| just ie =
    let dot-ced = createDirectoryIfMissing ff (dot-cedille-directory (takeDirectory filename)) in
    maybe-write-aux-file s ie dot-ced (cede-filename filename) cede-suffix
      cedille-options.options.use-cede-files
      include-elt.cede-up-to-date
      ((if include-elt.err ie then [[ "e" ]] else [[]]) ⊹⊹ json-to-rope (include-elt-spans-to-json ie)) >>
    maybe-write-aux-file s ie dot-ced (rkt-filename filename) rkt-suffix
      cedille-options.options.make-rkt-files
      include-elt.rkt-up-to-date
      (to-rkt-file filename (toplevel-state.Γ s) ie rkt-filename)

  -- we assume the cede file is known to exist at this point
  read-cede-file : toplevel-state → (ced-path : filepath) → IO (𝔹 × string)
  read-cede-file s ced-path =
    let cede = cede-filename ced-path in
    logMsg s ("Started reading .cede file " ^ cede) >>
    (get-file-contents cede >>= finish) >≯
    logMsg s ("Finished reading .cede file " ^ cede)
    where finish : maybe string → IO (𝔹 × string)
          finish nothing = return (tt , global-error-string ("Could not read the file " ^ cede-filename ced-path ^ "."))
          finish (just ss) with string-to-𝕃char ss
          finish (just ss)  | ('e' :: ss') = forceFileRead ss >>r tt , 𝕃char-to-string ss'
          finish (just ss) | _ = forceFileRead ss >>r ff , ss

  --add-cedille-extension : string → string
  --add-cedille-extension x = x ^ "." ^ cedille-extension

  --add-cdle-extension : string → string
  --add-cdle-extension x = x ^ "." ^ cdle-extension

  -- Allows you to say "import FOO.BAR.BAZ" rather than "import FOO/BAR/BAZ"
  replace-dots : filepath → filepath
  replace-dots s = 𝕃char-to-string (h (string-to-𝕃char s)) where
    h : 𝕃 char → 𝕃 char
    h ('.' :: '.' :: cs) = '.' :: '.' :: h cs
    h ('.' :: cs) = pathSeparator :: h cs
    h (c :: cs) = c :: h cs
    h [] = []

  find-imported-file : (sfx : string) → (dirs : 𝕃 filepath) → (unit-name : string) → IO (maybe filepath)
  find-imported-file sfx [] unit-name = return nothing
  find-imported-file sfx (dir :: dirs) unit-name =
    let e = combineFileNames dir (unit-name ^ "." ^ sfx) in
    doesFileExist e >>= λ where
      tt → canonicalizePath e >>=r just
      ff → find-imported-file sfx dirs unit-name
{-
  find-imported-file sfx (dir :: dirs) unit-name =
      let e₁ = combineFileNames dir (add-cedille-extension unit-name)
          e₂ = combineFileNames dir (add-cdle-extension unit-name)
          e? = λ e → doesFileExist e >>=r λ e? → ifMaybej e? e in
      (e? e₁ >>= λ e₁ → e? e₂ >>=r λ e₂ → e₁ maybe-or e₂) >>= λ where
        nothing → find-imported-file sfx dirs unit-name
        (just e) → canonicalizePath e >>=r just
-}

  find-imported-files : toplevel-state → (sfx : string) → (dirs : 𝕃 filepath) → (imports : 𝕃 string) → IO (𝕃 (string × filepath))
  find-imported-files s sfx dirs (u :: us) =
    find-imported-file sfx dirs (replace-dots u) >>= λ where
      nothing → logMsg s ("Error finding file: " ^ replace-dots u) >> find-imported-files s sfx dirs us
      (just fp) → logMsg s ("Found import: " ^ fp) >> find-imported-files s sfx dirs us >>=r (u , fp) ::_
  find-imported-files s sfx dirs [] = return []

  get-imports : ex-file → 𝕃 string
  get-imports (ExModule is _ _ mn _ cs _) =
    map (λ {(ExImport _ _ _ x _ _ _) → x}) (is ++ ex-cmds-to-imps cs)

  {- new parser test integration -}
  reparse : toplevel-state → filepath → IO toplevel-state
  reparse st filename =
     doesFileExist filename >>= λ fileExists →
       (if fileExists then
           (readFiniteFile filename >>= λ source →
            getCurrentTime >>= λ time →
            processText source >>= λ ie →
            return (set-last-parse-time-include-elt ie time) >>=r λ ie ->
            set-source-include-elt ie source)
        else return (error-include-elt ("The file " ^ filename ^ " could not be opened for reading.")))
       >>=r set-include-elt st filename
    where processText : string → IO include-elt
          processText x with parseStart x
          processText x | Left (Left cs)  = return (error-span-include-elt ("Error in file " ^ filename ^ ".") "Lexical error." cs)
          processText x | Left (Right cs) = return (error-span-include-elt ("Error in file " ^ filename ^ ".") "Parsing error." cs)
          processText x | Right t  with cws-types.scanComments x
          processText x | Right t | t2 =
            find-imported-files st (fileSuffix filename)
              (fst (cedille-options.include-path-insert (takeDirectory filename) (toplevel-state.include-path st)))
              (get-imports t) >>= λ deps →
            logMsg st ("deps for file " ^ filename ^ ": " ^ 𝕃-to-string (λ {(a , b) → "short: " ^ a ^ ", long: " ^ b}) ", " deps) >>r
            new-include-elt filename deps t t2 nothing

  reparse-file : filepath → toplevel-state → IO toplevel-state
  reparse-file filename s =
    reparse s filename >>=r λ s →
    set-include-elt s filename
      (set-cede-file-up-to-date-include-elt
        (set-do-type-check-include-elt
          (get-include-elt s filename) tt) ff)

  infixl 2 _&&>>_
  _&&>>_ : IO 𝔹 → IO 𝔹 → IO 𝔹
  (a &&>> b) = a >>= λ a → if a then b else return ff

  aux-up-to-date : filepath → toplevel-state → IO toplevel-state
  aux-up-to-date filename s =
    let rkt = rkt-filename filename in
    (doesFileExist rkt &&>> fileIsOlder filename rkt) >>=r
    (set-include-elt s filename ∘  (set-rkt-file-up-to-date-include-elt (get-include-elt s filename)))

  ie-up-to-date : filepath → include-elt → IO 𝔹
  ie-up-to-date filename ie =
    getModificationTime filename >>=r λ mt →
    maybe-else ff (λ lpt → lpt utc-after mt) (include-elt.last-parse-time ie)

  import-changed : toplevel-state → filepath → (import-file : string) → IO 𝔹
  import-changed s filename import-file =
    let dtc = include-elt.do-type-check (get-include-elt s import-file)
        cede = cede-filename filename
        cede' = cede-filename import-file in
    case cedille-options.options.use-cede-files options of λ where
      ff → return dtc
      tt → (doesFileExist cede &&>> doesFileExist cede') >>= λ where
        ff → return ff
        tt → fileIsOlder cede cede' >>=r λ fio → dtc || fio

  any-imports-changed : toplevel-state → filepath → (imports : 𝕃 string) → IO 𝔹
  any-imports-changed s filename [] = return ff
  any-imports-changed s filename (h :: t) =
    import-changed s filename h >>= λ where
      tt → return tt
      ff → any-imports-changed s filename t

  file-after-compile : filepath → IO 𝔹
  file-after-compile fn =
    getModificationTime fn >>= λ mt →
    case mt utc-after compileTime of λ where
      tt → doesFileExist options-filepath &&>> fileIsOlder options-filepath fn
      ff → return ff

  ensure-ast-depsh : filepath → toplevel-state → IO toplevel-state
  ensure-ast-depsh filename s with get-include-elt-if s filename
  ...| just ie = ie-up-to-date filename ie >>= λ where
    ff → reparse-file filename s
    tt → return s
  ...| nothing =
      let cede = cede-filename filename in
      (return (cedille-options.options.use-cede-files options) &&>>
       doesFileExist cede &&>>
       fileIsOlder filename cede &&>>
       file-after-compile cede) >>= λ where
         ff → reparse-file filename s
         tt → reparse s filename >>= λ s →
              read-cede-file s filename >>= λ where
                (err , ss) → return
                  (set-include-elt s filename
                  (set-do-type-check-include-elt
                  (set-need-to-add-symbols-to-context-include-elt
                  (set-spans-string-include-elt
                  (get-include-elt s filename) err ss) tt) ff))

  {- helper function for update-asts, which keeps track of the files we have seen so
     we avoid importing the same file twice, and also avoid following cycles in the import
     graph. -}
  {-# TERMINATING #-}
  update-astsh : stringset {- seen already -} → toplevel-state → filepath →
                 IO (stringset {- seen already -} × toplevel-state)
  update-astsh seen s filename =
    if stringset-contains seen filename then return (seen , s)
    else ((ensure-ast-depsh filename s >>= aux-up-to-date filename) >>= cont (stringset-insert seen filename))
    where cont : stringset → toplevel-state → IO (stringset × toplevel-state)
          cont seen s with get-include-elt s filename
          cont seen s | ie with include-elt.deps ie
          cont seen s | ie | ds =
            proc seen s ds
            where proc : stringset → toplevel-state → 𝕃 string → IO (stringset × toplevel-state)
                  proc seen s [] = any-imports-changed s filename ds >>=r λ changed →
                    seen , set-include-elt s filename (set-do-type-check-include-elt ie (include-elt.do-type-check ie || changed))
                  proc seen s (d :: ds) = update-astsh seen s d >>= λ p →
                                          proc (fst p) (snd p) ds

  {- this function updates the ast associated with the given filename in the toplevel state.
     So if we do not have an up-to-date .cede file (i.e., there is no such file at all,
     or it is older than the given file), reparse the file.  We do this recursively for all
     dependencies (i.e., imports) of the file. -}
  update-asts : toplevel-state → filepath → IO toplevel-state
  update-asts s filename = update-astsh empty-stringset s filename >>=r snd

  log-files-to-check : toplevel-state → IO ⊤
  log-files-to-check s = logRope s ([[ "\n" ]] ⊹⊹ (h (trie-mappings (toplevel-state.is s)))) where
    h : 𝕃 (string × include-elt) → rope
    h [] = [[]]
    h ((fn , ie) :: t) = [[ "file: " ]] ⊹⊹ [[ fn ]] ⊹⊹ [[ "\nadd-symbols: " ]] ⊹⊹ [[ 𝔹-to-string (include-elt.need-to-add-symbols-to-context ie) ]] ⊹⊹ [[ "\ndo-type-check: " ]] ⊹⊹ [[ 𝔹-to-string (include-elt.do-type-check ie) ]] ⊹⊹ [[ "\n\n" ]] ⊹⊹ h t

  {- this function checks the given file (if necessary), updates .cede and .rkt files (again, if necessary), and replies on stdout if appropriate -}
  checkFile : (string → IO ⊤) → toplevel-state → filepath → (should-print-spans : 𝔹) → IO toplevel-state
  checkFile progressUpdate s filename should-print-spans =
    update-asts s filename >>= λ s →
    log-files-to-check s >>
    logMsg s (𝕃-to-string (λ {(im , fn) → "im: " ^ im ^ ", fn: " ^ fn})
                "; "
                (trie-mappings (include-elt.import-to-dep (get-include-elt s filename)))) >>
    process-file progressUpdate (logMsg s) s filename (fileBaseName filename) >>= finish
    where
          reply : toplevel-state → IO ⊤
          reply s with get-include-elt-if s filename
          reply s | nothing = putStrLn (global-error-string ("Internal error looking up information for file " ^ filename ^ "."))
          reply s | just ie =
             if should-print-spans then
               putJson (include-elt-spans-to-json ie)
             else return triv
          finish : (toplevel-state × file × string × string × params × qualif) → IO toplevel-state
          finish (s @ (mk-toplevel-state ip mod is Γ logFilePath) , f , ret-mod) =
            logMsg s ("Started reply for file " ^ filename) >> -- Lazy, so checking has not been calculated yet?
            reply s >>
            logMsg s ("Finished reply for file " ^ filename) >>
            logMsg s ("Files with updated spans:\n" ^ 𝕃-to-string (λ x → x) "\n" mod) >>
            let Γ = ctxt-set-current-mod Γ ret-mod in
              writeo mod >>r -- Should process-file now always add files to the list of modified ones because now the cede-/rkt-up-to-date fields take care of whether to rewrite them?
              mk-toplevel-state ip [] is Γ logFilePath -- Reset files with updated spans
              where
                writeo : 𝕃 string → IO ⊤
                writeo [] = return triv
                writeo (f :: us) =
                  writeo us >>
                  --let ie = get-include-elt s f in
                  write-aux-files s f
                  --  (if cedille-options.options.make-rkt-files options && ~ include-elt.rkt-up-to-date ie then (write-rkt-file f (toplevel-state.Γ s) ie rkt-filename) else return triv)

  -- this is the function that handles requests (from the frontend) on standard input
  {-# TERMINATING #-}
  readCommandsFromFrontend : toplevel-state → IO ⊤
  readCommandsFromFrontend s =
      getLine >>= λ input →
      logMsg s ("Frontend input: " ^ input) >>
      let input-list : 𝕃 string
          input-list = string-split (undo-escape-string input) delimiter in
      handleCommands input-list s >>= readCommandsFromFrontend
    where
    errorCommand : 𝕃 string → toplevel-state → IO ⊤
    errorCommand ls s = putStrLn (global-error-string "Invalid command sequence \\\\\"" ^ (𝕃-to-string (λ x → x) ", " ls) ^ "\\\\\".")

    debugCommand : toplevel-state → IO ⊤
    debugCommand s = putStrLn (escape-string (toplevel-state-to-string s))

    checkCommand : 𝕃 string → toplevel-state → IO toplevel-state
    checkCommand (input :: []) s =
      canonicalizePath input >>= λ input-filename →
      checkFile progressUpdate (set-include-path s (cedille-options.include-path-insert (takeDirectory input-filename) (toplevel-state.include-path s))) input-filename tt {- should-print-spans -}
    checkCommand ls s = errorCommand ls s >>r s

    createArchive-h : toplevel-state → trie json → 𝕃 string → json
    createArchive-h s t (filename :: filenames) with trie-contains t filename | get-include-elt-if s filename
    ...| ff | just ie = createArchive-h s (trie-insert t filename $ include-elt-to-archive ie) (filenames ++ include-elt.deps ie)
    ...| _ | _ = createArchive-h s t filenames
    createArchive-h s t [] = json-object $ trie-mappings t

    createArchive : toplevel-state → string → json
    createArchive s filename = createArchive-h s empty-trie (filename :: [])

    archiveCommand : 𝕃 string → toplevel-state → IO toplevel-state
    archiveCommand (input :: []) s =
      canonicalizePath input >>= λ filename →
      update-asts s filename >>= λ s →
      process-file (λ _ → return triv) (λ _ → return triv) s
        filename (fileBaseName filename) >>=c λ s _ →
      putRopeLn (json-to-rope (createArchive s filename)) >>r s
    archiveCommand ls s = errorCommand ls s >>r s

    handleCommands : 𝕃 string → toplevel-state → IO toplevel-state
    handleCommands ("progress stub" :: xs) = return
    handleCommands ("status ping" :: xs) s = putStrLn "idle" >> return s
    handleCommands ("check" :: xs) s = checkCommand xs s
    handleCommands ("debug" :: []) s = debugCommand s >>r s
    handleCommands ("elaborate" :: fm :: to :: []) s = elab-all s fm to >>r s
    handleCommands ("interactive" :: xs) s = interactive-cmd xs s >>r s
    handleCommands ("archive" :: xs) s = archiveCommand xs s
    handleCommands ("br" :: xs) s = putJson interactive-not-br-cmd-msg >>r s
  --            handleCommands ("find" :: xs) s = findCommand xs s
    handleCommands xs s = errorCommand xs s >>r s

{-
  mk-new-toplevel-state : IO toplevel-state
  mk-new-toplevel-state =
    let s = new-toplevel-state (cedille-options.options.include-path options) in
    maybe-else' (cedille-options.options.datatype-encoding options) (return s)
      λ fp → readFiniteFile fp >>= λ de → case parseStart de of λ where
        (Left (Left e)) → putStrLn ("Lexical error in datatype encoding at position " ^ e) >>r s
        (Left (Right e)) → putStrLn ("Parse error in datatype encoding at position " ^ e) >>r s
        (Right de) → {!!}
-}

  processFile : (logFilePath : filepath) → string → IO toplevel-state
  processFile logFilePath input-filename =
    checkFile progressUpdate (new-toplevel-state logFilePath (cedille-options.include-path-insert (takeDirectory input-filename)
    (cedille-options.options.include-path options))) input-filename ff

  typecheckFile : (logFilePath : filepath) → string → IO toplevel-state
  typecheckFile logFilePath f =
    processFile logFilePath f >>= λ s →
    let ie = get-include-elt s f in
      if include-elt.err ie
      then die (string-to-𝕃char ("Type Checking Failed"))
      else return s

  -- function to process command-line arguments
  processArgs : (logFilePath : filepath) → cedille-args → IO ⊤
  -- this is the case for when we are called with a single command-line argument, the name of the file to process
  processArgs logFilePath (mk-cedille-args _ minput-filename about help do-elab confirm-read-stdin) =
    if help then
      showCedilleUsage
    else if about then
      say-about options-filepath
    else
      maybe-else' minput-filename
       (ifM confirm-read-stdin
         $ readCommandsFromFrontend (new-toplevel-state logFilePath (cedille-options.options.include-path options)))
      (λ input-filename →
        canonicalizePath input-filename >>= λ input-filename' →
        typecheckFile logFilePath input-filename' >>= λ s →
        whenM do-elab (λ target-dir → elab-all s input-filename' target-dir))

  main' : cedille-args → IO ⊤
  main' args =
    maybeClearLogFile >>= λ logFilePath →
    logMsg' logFilePath ("Started Cedille process (compiled at: " ^ utcToString compileTime ^ ")") >>
    processArgs logFilePath args

getCedilleArgs : IO cedille-args
getCedilleArgs = getArgs >>= λ where
                                     -- only read from stdin if there are no args at all
                                [] → return $ record default-cedille-args {confirm-read-stdin = tt}
                                args → getCedilleArgsH args default-cedille-args
  where
  bad-opts-flag : IO ⊤
  bad-opts-flag  = putStrLn "warning: flag --options should be followed by a Cedille options file"

  unknown-flag : string → IO ⊤
  unknown-flag f = putStrLn $ "warning: unknown flag " ^ f

  -- allow for later --options to override earlier. This is a bash idiom
  getCedilleArgsH : 𝕃 string → cedille-args → IO cedille-args
  getCedilleArgsH ("--options" :: y :: xs) args =
    getCedilleArgsH xs (record args { opts-file = just y})
  getCedilleArgsH ("--options" :: []) args =
    bad-opts-flag >> return args
  getCedilleArgsH ("--about" :: xs) args =
    getCedilleArgsH xs (record args { about = tt })
  getCedilleArgsH ("--help" :: xs) args =
    getCedilleArgsH xs (record args { help = tt })
  getCedilleArgsH ("--elab" :: to :: xs) args =
    getCedilleArgsH xs (record args { do-elab = just to})
  getCedilleArgsH (x :: []) args =
    -- assume it is a .ced file to check
    return $ record args {file-to-process = just x}
  getCedilleArgsH (x :: y :: xs) args =
    unknown-flag x >> return args
  getCedilleArgsH [] args = return args

process-encoding : filepath → cedille-options.options → IO cedille-options.options
process-encoding ofp ops @ (cedille-options.mk-options ip _ _ _ _ _ de _ _ _ _) =
  maybe-else' de (return ops) λ de-f →
  let de = fst de-f
      s = new-toplevel-state "no logfile path" (cedille-options.include-path-insert (takeDirectory de) ip) in
  update-asts s de >>= λ s →
  process-encoding-file s de >>= λ f? →
  maybe-else' f? (return ops) λ ast~ →
  return (record ops {datatype-encoding = just (de , just ast~)})
  where
  ops' = record ops {datatype-encoding = nothing; use-cede-files = ff}
  open main-with-options compileTime ofp ops' die
  open import spans ops' {IO}
  open import toplevel-state ops' {IO}
  open import process-cmd ops' {IO} (λ _ → return triv) (λ _ → return triv)
  open import syntax-util
  open import ctxt

  process-encoding-file : toplevel-state → filepath → IO (maybe file)
  process-encoding-file s fp with get-include-elt-if s fp >>= include-elt.ast
  ...| nothing = putStrLn ("Error looking up datatype encoding information from file " ^ fp) >> return nothing
  ...| just (ExModule is pi1 pi2 mn ps cs pi3) =
    (process-cmds (record s {Γ = ctxt-initiate-file (toplevel-state.Γ s) fp mn}) (map ExCmdImport is) >>=c λ s is' →
     process-params s first-position [] >>=c λ s _ →
     check-and-add-params (toplevel-state.Γ s) (params-end-pos first-position ps) ps >>=c λ Γₚₛ ps~ →
     process-cmds (record s {Γ = Γₚₛ}) cs >>=c λ s cs →
     return2 ps~ (is' ++ cs)) empty-spans >>=c uncurry λ ps cs _ →
    return (just (Module mn ps cs))

-- main entrypoint for the backend
main : IO ⊤
main = initializeStdoutToUTF8 >>
       initializeStdinToUTF8 >>
       setStdoutNewlineMode >>
       setStdinNewlineMode >>
       setToLineBuffering >>
       getCedilleArgs >>= λ args →
       maybe-else' (cedille-args.opts-file args)
         (findOptionsFile >>= readOptions) (readOptions ∘ just) >>=c λ ofp ops →
       let log = cedille-options.options.generate-logs ops in
       process-encoding ofp (record ops {generate-logs = ff}) >>= λ ops →
       let args = record args { opts-file = just ofp } in
       let ops = record ops { generate-logs = log ;
                              show-progress-updates = ~ (cedille-args.confirm-read-stdin args) } in
       main-with-options.main' compileTime ofp ops die args


text:
------------------------------------------------------------------------------
-- The inductive PA universe
------------------------------------------------------------------------------

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

-- This file contains some core definitions which are reexported by
-- PA.Inductive.Base.

module PA.Inductive.Base.Core where

-- PA universe.
data ℕ : Set where
  zero :     ℕ
  succ : ℕ → ℕ


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Commutative semirings with some additional structure ("almost"
-- commutative rings), used by the ring solver
------------------------------------------------------------------------

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

module Algebra.Solver.Ring.AlmostCommutativeRing where

open import Algebra
open import Algebra.Structures
open import Algebra.Definitions
import Algebra.Morphism as Morphism
import Algebra.Morphism.Definitions as MorphismDefinitions
open import Function
open import Level
open import Relation.Binary

record IsAlmostCommutativeRing {a ℓ} {A : Set a} (_≈_ : Rel A ℓ)
                               (_+_ _*_ : Op₂ A) (-_ : Op₁ A)
                               (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1#
    -‿cong                : Congruent₁ _≈_ -_
    -‿*-distribˡ          : ∀ x y → ((- x) * y)     ≈ (- (x * y))
    -‿+-comm              : ∀ x y → ((- x) + (- y)) ≈ (- (x + y))

  open IsCommutativeSemiring isCommutativeSemiring public

record AlmostCommutativeRing c ℓ : Set (suc (c ⊔ ℓ)) where
  infix  8 -_
  infixl 7 _*_
  infixl 6 _+_
  infix  4 _≈_
  field
    Carrier                 : Set c
    _≈_                     : Rel Carrier ℓ
    _+_                     : Op₂ Carrier
    _*_                     : Op₂ Carrier
    -_                      : Op₁ Carrier
    0#                      : Carrier
    1#                      : Carrier
    isAlmostCommutativeRing : IsAlmostCommutativeRing _≈_ _+_ _*_ -_ 0# 1#

  open IsAlmostCommutativeRing isAlmostCommutativeRing public

  commutativeSemiring : CommutativeSemiring _ _
  commutativeSemiring = record
    { isCommutativeSemiring = isCommutativeSemiring
    }

  open CommutativeSemiring commutativeSemiring public
    using
    ( +-magma; +-semigroup
    ; *-magma; *-semigroup; *-commutativeSemigroup
    ; +-monoid; +-commutativeMonoid
    ; *-monoid; *-commutativeMonoid
    ; semiring
    )

  rawRing : RawRing _ _
  rawRing = record
    { _≈_ = _≈_
    ; _+_ = _+_
    ; _*_ = _*_
    ; -_  = -_
    ; 0#  = 0#
    ; 1#  = 1#
    }

------------------------------------------------------------------------
-- Homomorphisms

record _-Raw-AlmostCommutative⟶_
  {r₁ r₂ r₃ r₄}
  (From : RawRing r₁ r₄)
  (To : AlmostCommutativeRing r₂ r₃) : Set (r₁ ⊔ r₂ ⊔ r₃) where
  private
    module F = RawRing From
    module T = AlmostCommutativeRing To
  open MorphismDefinitions F.Carrier T.Carrier T._≈_
  field
    ⟦_⟧    : Morphism
    +-homo : Homomorphic₂ ⟦_⟧ F._+_ T._+_
    *-homo : Homomorphic₂ ⟦_⟧ F._*_ T._*_
    -‿homo : Homomorphic₁ ⟦_⟧ F.-_  T.-_
    0-homo : Homomorphic₀ ⟦_⟧ F.0#  T.0#
    1-homo : Homomorphic₀ ⟦_⟧ F.1#  T.1#

-raw-almostCommutative⟶ :
  ∀ {r₁ r₂} (R : AlmostCommutativeRing r₁ r₂) →
  AlmostCommutativeRing.rawRing R -Raw-AlmostCommutative⟶ R
-raw-almostCommutative⟶ R = record
  { ⟦_⟧    = id
  ; +-homo = λ _ _ → refl
  ; *-homo = λ _ _ → refl
  ; -‿homo = λ _ → refl
  ; 0-homo = refl
  ; 1-homo = refl
  }
  where open AlmostCommutativeRing R

Induced-equivalence : ∀ {c₁ c₂ ℓ₁ ℓ₂} {Coeff : RawRing c₁ ℓ₁}
                      {R : AlmostCommutativeRing c₂ ℓ₂} →
                      Coeff -Raw-AlmostCommutative⟶ R →
                      Rel (RawRing.Carrier Coeff) ℓ₂
Induced-equivalence {R = R} morphism a b = ⟦ a ⟧ ≈ ⟦ b ⟧
  where
  open AlmostCommutativeRing R
  open _-Raw-AlmostCommutative⟶_ morphism

------------------------------------------------------------------------
-- Conversions

-- Commutative rings are almost commutative rings.

fromCommutativeRing : ∀ {r₁ r₂} → CommutativeRing r₁ r₂ → AlmostCommutativeRing r₁ r₂
fromCommutativeRing CR = record
  { isAlmostCommutativeRing = record
      { isCommutativeSemiring = isCommutativeSemiring
      ; -‿cong                = -‿cong
      ; -‿*-distribˡ          = -‿*-distribˡ
      ; -‿+-comm              = ⁻¹-∙-comm
      }
  }
  where
  open CommutativeRing CR
  open import Algebra.Properties.Ring ring
  open import Algebra.Properties.AbelianGroup +-abelianGroup

-- Commutative semirings can be viewed as almost commutative rings by
-- using identity as the "almost negation".

fromCommutativeSemiring : ∀ {r₁ r₂} → CommutativeSemiring r₁ r₂ → AlmostCommutativeRing _ _
fromCommutativeSemiring CS = record
  { -_                      = id
  ; isAlmostCommutativeRing = record
      { isCommutativeSemiring = isCommutativeSemiring
      ; -‿cong                = id
      ; -‿*-distribˡ          = λ _ _ → refl
      ; -‿+-comm              = λ _ _ → refl
      }
  }
  where open CommutativeSemiring CS


text:
data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

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

{-# NON_TERMINATING #-}
loop : Nat → Nat
loop n = loop n

thm : ∀ n → loop n ≡ 42
thm n = refl


text:
module ParseTreeOperations where
open import ParseTree
open import Data.List.NonEmpty
open import Data.Bool
open import Data.List hiding ([_])
open import Data.Nat
open import Relation.Nullary
open import Data.String

-- go from ((f a) b) representation to f [a, b]
expressionToList : Expr -> List⁺ Expr
expressionToList (functionApp e e₁ {false}) = expressionToList e ⁺∷ʳ e₁
expressionToList x = [ x ]

typeToList : Expr -> List⁺ Expr
typeToList (functionApp e e₁ {true}) = e ∷⁺ typeToList e₁
typeToList x = [ x ]

-- go from f [a, b] representation to ((f a) b)
{-# TERMINATING #-}
listToExpression : List⁺ Expr -> Expr
listToExpression (head₁ ∷ []) = head₁
listToExpression (head₁ ∷ x ∷ tail₁) =
  listToExpression (functionApp head₁ x {false} ∷ tail₁)

{-# TERMINATING #-}
listToType : List⁺ Expr -> Expr
listToType (head₁ ∷ []) = head₁
listToType (head₁ ∷ y ∷ tail) =
  functionApp head₁ (listToType (y ∷ tail)) {true}

emptyRange : Range
emptyRange = range 0 0

newHole : Expr
newHole = hole {""} {emptyRange} {[]} {[]}

newUnderscore : Expr
newUnderscore = underscore {emptyRange} {[]} {[]}

sameId : Identifier -> Identifier -> Bool
sameId (identifier name isInRange scope declaration) (identifier name₁ isInRange₁ scope₁ declaration₁)
  with declaration Data.Nat.≟ declaration₁
sameId (identifier name isInRange scope declaration) (identifier name₁ isInRange₁ scope₁ declaration₁) | yes p = true
sameId (identifier name isInRange scope declaration) (identifier name₁ isInRange₁ scope₁ declaration₁) | no ¬p = false

sameName : Identifier -> Identifier -> Bool
sameName (identifier name isInRange scope declaration) (identifier name₁ isInRange₁ scope₁ declaration₁) = name₁ == name

_doesNotAppearInExp_ : Identifier -> Expr -> Bool
x doesNotAppearInExp numLit = true
identifier name₁ isInRange₁ scope₁ declaration₁ doesNotAppearInExp ident
    (identifier name isInRange scope declaration) with compare declaration₁ declaration
(identifier name₁ isInRange₁ scope₁ declaration₁) doesNotAppearInExp (ident (identifier name isInRange scope .declaration₁)) | equal .declaration₁ = false
... | _ = true
x doesNotAppearInExp hole = true
x doesNotAppearInExp namedArgument (typeSignature funcName funcType) = x doesNotAppearInExp funcType
x doesNotAppearInExp functionApp y y₁ =
     (x doesNotAppearInExp y) ∧
     (x doesNotAppearInExp y₁)
x doesNotAppearInExp implicit x1 = x doesNotAppearInExp x1
x doesNotAppearInExp underscore = true

isImplicit : Expr -> Bool
isImplicit (implicit e) = true
isImplicit (namedArgument arg {explicit}) = not explicit
isImplicit x = false


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

open import HoTT
open import cw.CW
open import homotopy.PinSn

module cw.Degree
  {i} {n : ℕ} (skel : Skeleton {i} (S (S n)))
  (skel-has-dec-cells : has-dec-cells skel)
  (skel-is-aligned : is-aligned skel)
  -- the cells at the upper and lower dimensions
  (upper : cells-last skel)
  (lower : cells-nth (inr ltS) skel)
  where

private
  lower-skel = cw-take (inr ltS) skel
  lower-cells = cells-last lower-skel
  lower-cells-has-dec-eq = snd (fst skel-has-dec-cells)

-- squash the lower CW complex except one of its cells [lower]
cw-squash-lower-to-Sphere : ⟦ lower-skel ⟧ → Sphere (S n)
cw-squash-lower-to-Sphere = Attached-rec (λ _ → north) squash-hubs squash-spokes where
  -- squash cells except [lower]
  squash-hubs : lower-cells → Sphere (S n)
  squash-hubs c with lower-cells-has-dec-eq c lower
  ... | (inl _) = south
  ... | (inr _) = north
  -- squash cells except [lower]
  squash-spokes : (c : lower-cells) → Sphere n
    → north == squash-hubs c
  squash-spokes c s with lower-cells-has-dec-eq c lower
  ... | (inl _) = merid s
  ... | (inr _) = idp

degree-map : Sphere (S n) → Sphere (S n)
degree-map = cw-squash-lower-to-Sphere ∘ attaching-last skel upper

degree-⊙map : fst (⊙Sphere (S n) ⊙→ ⊙Sphere (S n))
degree-⊙map = degree-map , ap cw-squash-lower-to-Sphere (! (snd (snd skel-is-aligned upper)))

degree' : ℤ → ℤ
degree' = transport Group.El (πₙ₊₁Sⁿ⁺¹ n)
        ∘ GroupHom.f (πS-fmap n degree-⊙map)
        ∘ transport! Group.El (πₙ₊₁Sⁿ⁺¹ n)

degree : ℤ
degree = degree' 1

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda