text:
{-# OPTIONS --no-positivity-check #-}

module Section4a where

open import Section3 public

-- 4. The semantic model
-- =====================
--
-- As we want to deal with full conversion on open terms and the η-rule, we choose to describe
-- the semantics in a Kripke style model [6, 11, 15].  A Kripke model is a set of possible worlds,
-- `𝒲 : Set`, with a partial ordering `⊒ : 𝒲 → 𝒲 → Set`, of extensions of worlds.  We also have
-- a family of ground sets `𝒢 : 𝒲 → Set` over possible worlds which are the interpretation of
-- the base type.  We also need independence of the proof of `_⊒_`, i.e., if `c₁, c₂ : w′ ⊒ w`, then
-- `c₁ ≡ c₂`.  (…)

record Model : Set₁ where
  infix 3 _⊒_
  field
    𝒲     : Set
    _⊒_   : 𝒲 → 𝒲 → Set
    refl⊒ : ∀ {w} → w ⊒ w
    _◇_   : ∀ {w w′ w″} → w′ ⊒ w → w″ ⊒ w′ → w″ ⊒ w
    uniq⊒ : ∀ {w w′} → (c c′ : w′ ⊒ w) → c ≡ c′
    𝒢     : 𝒲 → Set
open Model {{…}} public

module _ {{_ : Model}} where
  trans⊒ : ∀ {w w′ w″} → w″ ⊒ w′ → w′ ⊒ w → w″ ⊒ w
  trans⊒ = flip _◇_

  id₁◇ : ∀ {w w′} → (c : w ⊒ w) (c′ : w′ ⊒ w) → c ◇ c′ ≡ c′
  id₁◇ c c′ = uniq⊒ (c ◇ c′) c′

  id₂◇ : ∀ {w w′} → (c : w′ ⊒ w) (c′ : w′ ⊒ w′) → c ◇ c′ ≡ c
  id₂◇ c c′ = uniq⊒ (c ◇ c′) c

  assoc◇ : ∀ {w w′ w″ w‴} → (c : w′ ⊒ w) (c′ : w″ ⊒ w′) (c″ : w‴ ⊒ w″) →
             c ◇ (c′ ◇ c″) ≡ (c ◇ c′) ◇ c″
  assoc◇ c c′ c″ = uniq⊒ (c ◇ (c′ ◇ c″)) ((c ◇ c′) ◇ c″)

  comp◇ : ∀ {w w′ w″} → (c : w′ ⊒ w) (c′ : w″ ⊒ w′) (c″ : w″ ⊒ w) →
            c ◇ c′ ≡ c″
  comp◇ c c′ c″ = uniq⊒ (c ◇ c′) c″

-- 4.1. Semantic objects
-- ---------------------
--
-- We define the set of semantic objects as usual in Kripke semantics.
--
-- Forcing is written `w ⊩ A`.  For the base type an element in `w ⊩ •` is a family of
-- elements in `𝒢 w′`, `w′ ⊒ w`.  For the type `A ⊃ B` an element in `w ⊩ A ⊃ B` is a family of
-- functions from `w′ ⊩ A` to `w′ ⊩ B`, `w′ ⊒ w`.  (…)

module _ {{_ : Model}} where
  -- TODO: Replace with strictly positive definition
  infix 3 _⊩_
  data _⊩_ : 𝒲 → 𝒯 → Set where
    ⟦𝒢⟧ : ∀ {w} →
            (∀ {w′} → w′ ⊒ w → 𝒢 w′) →
            w ⊩ •
    ⟦ƛ⟧ : ∀ {w A B} →
            (∀ {w′} → w′ ⊒ w → w′ ⊩ A → w′ ⊩ B) →
            w ⊩ A ⊃ B

-- We use the notational convention `⟦𝒢⟧` for the semantics of the ground type and
-- `⟦ƛ⟧` for the semantics of the function type.
--
-- We define the following two elimination rules:  (…)

module _ {{_ : Model}} where
  _⟦g⟧⟨_⟩ : ∀ {w w′} → w ⊩ • → w′ ⊒ w → 𝒢 w′
  (⟦𝒢⟧ f) ⟦g⟧⟨ c ⟩ = f c

  _⟦∙⟧⟨_⟩_ : ∀ {w w′ A B} → w ⊩ A ⊃ B → w′ ⊒ w → w′ ⊩ A → w′ ⊩ B
  (⟦ƛ⟧ f) ⟦∙⟧⟨ c ⟩ a = f c a

-- The monotonicity function `↑⟨_⟩⊩` lifts a semantic object in one world into a semantic object
-- in a bigger world and is defined by induction on the type.  (…)

module _ {{_ : Model}} where
  ↑⟨_⟩⊩ : ∀ {A w w′} → w′ ⊒ w → w ⊩ A → w′ ⊩ A
  ↑⟨_⟩⊩ {•}     c f = ⟦𝒢⟧ (λ c′   → f ⟦g⟧⟨ c ◇ c′ ⟩)
  ↑⟨_⟩⊩ {A ⊃ B} c f = ⟦ƛ⟧ (λ c′ a → f ⟦∙⟧⟨ c ◇ c′ ⟩ a)

  instance
    raise⊩ : ∀ {A} → Raiseable (_⊩ A)
    raise⊩ = record { ↑⟨_⟩ = ↑⟨_⟩⊩ }

-- We also need to define an equality, `Eq`, on semantic objects.  For the soundness of the
-- η-rule we need `f : w ⊩ A ⊃ B` to be equal to `⟦ƛ⟧ (λ c a → f ⟦∙⟧⟨ c ⟩ a)`, which corresponds
-- to η-expansion on the semantic level.  This means that the equality on our model must be
-- extensional and that application and the monotonicity function commutes, i.e., lifting the
-- result of an application up to a bigger world should be equal to first lifting the arguments and
-- then doing the application.  We say that a semantic object is uniform, `𝒰`, if the application and
-- monotonicity functions commute for this object (see Scott [17] for a discussion regarding
-- commutativity).  The predicates `Eq` and `𝒰` are mutually defined.
--
-- They both are defined by induction on the types; this way of defining extensionality is
-- presented by Gandy [10].  Two semantic objects of base type are equal if they are intensionally
-- equal in all bigger worlds and two semantic objects of function type are equal if the
-- application of them to a uniform semantic object in a bigger world is extensionally equal.
--
-- A semantic object of base type is always uniform.  A semantic object of function type is uniform
-- if it sends a uniform semantic object in a bigger world to a uniform semantic object,
-- if it sends two extensionally equal uniform objects in a bigger worlds to extensionally equal
-- semantic objects and if application and monotonicity commute for the semantic object.
--
-- The sets `Eq` and `𝒰` are defined by:  (…)

module _ {{_ : Model}} where
  mutual
    data Eq : ∀ {A w} → w ⊩ A → w ⊩ A → Set where
      eq• : ∀ {w} {f f′ : w ⊩ •} →
              (∀ {w′} →
                 (c : w′ ⊒ w) →
                 f ⟦g⟧⟨ c ⟩ ≡ f′ ⟦g⟧⟨ c ⟩) →
              Eq f f′
      eq⊃ : ∀ {A B w} {f f′ : w ⊩ A ⊃ B} →
              (∀ {w′} →
                 (c : w′ ⊒ w) → {a : w′ ⊩ A} → 𝒰 a →
                 Eq (f ⟦∙⟧⟨ c ⟩ a) (f′ ⟦∙⟧⟨ c ⟩ a)) →
              Eq f f′

    data 𝒰 : ∀ {A w} → w ⊩ A → Set where
      𝓊• : ∀ {w} {f : w ⊩ •} →
             𝒰 f
      𝓊⊃ : ∀ {A B w} {f : w ⊩ A ⊃ B} →
             (∀ {w′} →
                (c : w′ ⊒ w) → {a : w′ ⊩ A} → 𝒰 a →
                𝒰 (f ⟦∙⟧⟨ c ⟩ a)) →
             (∀ {w′} →
                (c : w′ ⊒ w) → {a a′ : w′ ⊩ A} → Eq a a′ → 𝒰 a → 𝒰 a′ →
                Eq (f ⟦∙⟧⟨ c ⟩ a) (f ⟦∙⟧⟨ c ⟩ a′)) →
             (∀ {w′ w″} →
                (c : w′ ⊒ w) (c′ : w″ ⊒ w′) (c″ : w″ ⊒ w) → {a : w′ ⊩ A} → 𝒰 a →
                Eq (↑⟨ c′ ⟩ (f ⟦∙⟧⟨ c ⟩ a)) (f ⟦∙⟧⟨ c″ ⟩ (↑⟨ c′ ⟩ a))) →
             𝒰 f

-- The equality `Eq` is transitive and symmetric and it is reflexive for uniform objects.

module _ {{_ : Model}} where
  reflEq : ∀ {A w} {a : w ⊩ A} → 𝒰 a → Eq a a
  reflEq 𝓊•            = eq• (λ c    → refl)
  reflEq (𝓊⊃ h₀ h₁ h₂) = eq⊃ (λ c uₐ → reflEq (h₀ c uₐ))

  -- TODO: Why do we restrict `Eq` so that it is reflexive only for uniform objects?
  reflEq′ : ∀ {A w} {a : w ⊩ A} → Eq a a
  reflEq′ {•}     = eq• (λ c    → refl)
  reflEq′ {A ⊃ B} = eq⊃ (λ c uₐ → reflEq′)

  symEq : ∀ {A w} {a a′ : w ⊩ A} → Eq a a′ → Eq a′ a
  symEq {•}     (eq• h) = eq• (λ c    → sym (h c))
  symEq {A ⊃ B} (eq⊃ h) = eq⊃ (λ c uₐ → symEq (h c uₐ))

  transEq : ∀ {A w} {a a′ a″ : w ⊩ A} → Eq a a′ → Eq a′ a″ → Eq a a″
  transEq {•}     (eq• h) (eq• h′) = eq• (λ c    → trans (h c) (h′ c))
  transEq {A ⊃ B} (eq⊃ h) (eq⊃ h′) = eq⊃ (λ c uₐ → transEq (h c uₐ) (h′ c uₐ))

module _ {{_ : Model}} where
  ≡→Eq : ∀ {A w} {a a′ : w ⊩ A} → 𝒰 a → a ≡ a′ → Eq a a′
  ≡→Eq u refl = reflEq u

  module EqReasoning where
    infix 1 begin_
    begin_ : ∀ {A w} {a a′ : w ⊩ A} → Eq a a′ → Eq a a′
    begin eq = eq

    infixr 2 _Eq⟨⟩_
    _Eq⟨⟩_ : ∀ {A w} (a {a′} : w ⊩ A) → Eq a a′ → Eq a a′
    a Eq⟨⟩ eq = eq

    infixr 2 _Eq⟨_⟩_
    _Eq⟨_⟩_ : ∀ {A w} (a {a′ a″} : w ⊩ A) → Eq a a′ → Eq a′ a″ → Eq a a″
    a Eq⟨ eq ⟩ eq′ = transEq eq eq′

    infixr 2 _≡⟨⟩_
    _≡⟨⟩_ : ∀ {A w} (a {a′} : w ⊩ A) → Eq a a′ → Eq a a′
    a ≡⟨⟩ eq = eq

    infixr 2 _≡⟨_∣_⟩_
    _≡⟨_∣_⟩_ : ∀ {A w} (a {a′ a″} : w ⊩ A) → a ≡ a′ → 𝒰 a → Eq a′ a″ → Eq a a″
    a ≡⟨ eq ∣ u ⟩ eq′ = transEq (≡→Eq u eq) eq′

    infix 3 _∎⟨_⟩
    _∎⟨_⟩ : ∀ {A w} (a : w ⊩ A) → 𝒰 a → Eq a a
    a ∎⟨ u ⟩ = reflEq u

-- Equal uniform values can be substituted in `⟦∙⟧⟨_⟩` and the function `↑⟨_⟩` returns uniform objects
-- for uniform input and equal results for equal input.

module _ {{_ : Model}} where
  cong⟦∙⟧⟨_⟩Eq : ∀ {A B w w′} {f f′ : w ⊩ A ⊃ B} {a a′ : w′ ⊩ A} →
                   (c : w′ ⊒ w) → Eq f f′ → 𝒰 f → 𝒰 f′ → Eq a a′ → 𝒰 a → 𝒰 a′ →
                   Eq (f ⟦∙⟧⟨ c ⟩ a) (f′ ⟦∙⟧⟨ c ⟩ a′)
  cong⟦∙⟧⟨ c ⟩Eq (eq⊃ h) (𝓊⊃ h₀ h₁ h₂) (𝓊⊃ h₀′ h₁′ h₂′) eqₐ uₐ uₐ′ =
    transEq (h₁ c eqₐ uₐ uₐ′) (h c uₐ′)

  cong↑⟨_⟩Eq : ∀ {A w w′} {a a′ : w ⊩ A} →
                 (c : w′ ⊒ w) → Eq a a′ →
                 Eq (↑⟨ c ⟩ a) (↑⟨ c ⟩ a′)
  cong↑⟨ c ⟩Eq (eq• h) = eq• (λ c′    → h (c ◇ c′))
  cong↑⟨ c ⟩Eq (eq⊃ h) = eq⊃ (λ c′ uₐ → h (c ◇ c′) uₐ)

  cong↑⟨_⟩𝒰 : ∀ {A w w′} {a : w ⊩ A} →
                (c : w′ ⊒ w) → 𝒰 a →
                𝒰 (↑⟨ c ⟩ a)
  cong↑⟨ c ⟩𝒰 𝓊•            = 𝓊•
  cong↑⟨ c ⟩𝒰 (𝓊⊃ h₀ h₁ h₂) = 𝓊⊃ (λ c′ uₐ         → h₀ (c ◇ c′) uₐ)
                                 (λ c′ eqₐ uₐ uₐ′ → h₁ (c ◇ c′) eqₐ uₐ uₐ′)
                                 (λ c′ c″ c‴ uₐ   → h₂ (c ◇ c′) c″ (c ◇ c‴) uₐ)

-- We also need to prove the following properties about `Eq` and `𝒰` which are used in the proofs of
-- soundness and completeness below.

module _ {{_ : Model}} where
  aux₄₁₁⟨_⟩ : ∀ {A w} →
                (c : w ⊒ w) → {a : w ⊩ A} → 𝒰 a →
                Eq (↑⟨ c ⟩ a) a
  aux₄₁₁⟨ c ⟩ {f} 𝓊•            = eq• (λ c′        → cong (f ⟦g⟧⟨_⟩)
                                                        (id₁◇ c c′))
  aux₄₁₁⟨ c ⟩ {f} (𝓊⊃ h₀ h₁ h₂) = eq⊃ (λ c′ {a} uₐ → ≡→Eq (h₀ (c ◇ c′) uₐ)
                                                        (cong (f ⟦∙⟧⟨_⟩ a)
                                                          (id₁◇ c c′)))

  aux₄₁₂ : ∀ {A w w′ w″} →
             (c : w′ ⊒ w) (c′ : w″ ⊒ w′) (c″ : w″ ⊒ w) → {a : w ⊩ A} → 𝒰 a →
             Eq (↑⟨ c′ ⟩ (↑⟨ c ⟩ a)) (↑⟨ c″ ⟩ a)
  aux₄₁₂ c c′ c″ {f} 𝓊•            = eq• (λ c‴        → cong (f ⟦g⟧⟨_⟩)
                                                           (trans (assoc◇ c c′ c‴)
                                                                  (comp◇ (c ◇ c′) c‴ (c″ ◇ c‴))))
  aux₄₁₂ c c′ c″ {f} (𝓊⊃ h₀ h₁ h₂) = eq⊃ (λ c‴ {a} uₐ → ≡→Eq (h₀ (c ◇ (c′ ◇ c‴)) uₐ)
                                                           (cong (f ⟦∙⟧⟨_⟩ a)
                                                             (trans (assoc◇ c c′ c‴)
                                                                    (comp◇ (c ◇ c′) c‴ (c″ ◇ c‴)))))
  aux₄₁₃ : ∀ {A B w w′} →
             (c : w′ ⊒ w) (c′ : w′ ⊒ w′) → {f : w ⊩ A ⊃ B} → 𝒰 f → {a : w′ ⊩ A} → 𝒰 a →
             Eq (f ⟦∙⟧⟨ c ⟩ a) (↑⟨ c ⟩ f ⟦∙⟧⟨ c′ ⟩ a)
  aux₄₁₃ c c′ {f} (𝓊⊃ h₀ h₁ h₂) {a} uₐ = ≡→Eq (h₀ c uₐ)
                                           (cong (f ⟦∙⟧⟨_⟩ a)
                                             (sym (id₂◇ c c′)))

-- 4.2. Semantic environments
-- --------------------------
--
-- We define the set of environments `_⊩⋆_`
-- where each variable in a context is associated with a semantic object.  (…)
--
-- The set is introduced by:  (…)

module _ {{_ : Model}} where
  infix 3 _⊩⋆_
  data _⊩⋆_ : 𝒲 → 𝒞 → Set where
    []      : ∀ {w} →
                w ⊩⋆ []
    [_,_≔_] : ∀ {Γ A w} →
                w ⊩⋆ Γ → (x : Name) {{_ : T (fresh x Γ)}} → w ⊩ A →
                w ⊩⋆ [ Γ , x ∷ A ]

-- We write `[]` for the empty environment and `[ ρ , x ≔ a ]` for updating an environment.
-- We define the following operations on semantic environments:
--
-- The function `lookup` is defined by induction on the environment.  (…)

module _ {{_ : Model}} where
  lookup : ∀ {Γ A w x} → w ⊩⋆ Γ → Γ ∋ x ∷ A → w ⊩ A
  lookup [ ρ , x ≔ a ] zero    = a
  lookup [ ρ , y ≔ b ] (suc i) = lookup ρ i

-- The function `↑⟨_⟩⊩⋆` that lifts
-- an environment into a bigger world is also defined by induction on the environment.  (…)

module _ {{_ : Model}} where
  ↑⟨_⟩⊩⋆ : ∀ {Γ w w′} → w′ ⊒ w → w ⊩⋆ Γ → w′ ⊩⋆ Γ
  ↑⟨ c ⟩⊩⋆ []            = []
  ↑⟨ c ⟩⊩⋆ [ ρ , x ≔ a ] = [ ↑⟨ c ⟩⊩⋆ ρ , x ≔ ↑⟨ c ⟩ a ]

  instance
    raise⊩⋆ : ∀ {Γ} → Raiseable (_⊩⋆ Γ)
    raise⊩⋆ = record { ↑⟨_⟩ = ↑⟨_⟩⊩⋆ }

-- The last function `↓⟨_⟩⊩⋆` is the projection on
-- environments and it is defined by induction on the proof of `Γ ⊇ Δ`.  (…)

module _ {{_ : Model}} where
  ↓⟨_⟩⊩⋆ : ∀ {Γ Δ w} → Γ ⊇ Δ → w ⊩⋆ Γ → w ⊩⋆ Δ
  ↓⟨ done ⟩⊩⋆             ρ = []
  ↓⟨ step {x = x} c i ⟩⊩⋆ ρ = [ ↓⟨ c ⟩⊩⋆ ρ , x ≔ lookup ρ i ]

  instance
    lower⊩⋆ : ∀ {w} → Lowerable (w ⊩⋆_)
    lower⊩⋆ = record { ↓⟨_⟩ = ↓⟨_⟩⊩⋆ }

-- We say that an environment is uniform `𝒰⋆ ρ : Set`, where `ρ : w ⊩⋆ Γ`, if each semantic
-- object in the environment is uniform.  Two environments are equal `Eq⋆ ρ ρ′ : Set`,
-- where `ρ, ρ′ : w ⊩⋆ Γ`, if they are equal component-wise.

module _ {{_ : Model}} where
  data Eq⋆ : ∀ {Γ w} → w ⊩⋆ Γ → w ⊩⋆ Γ → Set where
    eq⋆[] : ∀ {w} →
              Eq⋆ ([] {w}) ([] {w})
    eq⋆≔  : ∀ {Γ A w x} {{_ : T (fresh x Γ)}} {ρ ρ′ : w ⊩⋆ Γ} {a a′ : w ⊩ A} →
              Eq⋆ ρ ρ′ → Eq a a′ →
              Eq⋆ [ ρ , x ≔ a ] [ ρ′ , x ≔ a′ ]

  data 𝒰⋆ : ∀ {Γ w} → w ⊩⋆ Γ → Set where
    𝓊⋆[] : ∀ {w} →
             𝒰⋆ ([] {w})
    𝓊⋆≔  : ∀ {Γ A w x} {{_ : T (fresh x Γ)}} {ρ : w ⊩⋆ Γ} {a : w ⊩ A} →
             𝒰⋆ ρ → 𝒰 a →
             𝒰⋆ [ ρ , x ≔ a ]

-- The equality on semantic environments, `Eq⋆`, is transitive, symmetric, and for uniform
-- environments also reflexive.

module _ {{_ : Model}} where
  reflEq⋆ : ∀ {Γ w} {ρ : w ⊩⋆ Γ} → 𝒰⋆ ρ → Eq⋆ ρ ρ
  reflEq⋆ 𝓊⋆[]       = eq⋆[]
  reflEq⋆ (𝓊⋆≔ u⋆ u) = eq⋆≔ (reflEq⋆ u⋆) (reflEq u)

  symEq⋆ : ∀ {Γ w} {ρ ρ′ : w ⊩⋆ Γ} → Eq⋆ ρ ρ′ → Eq⋆ ρ′ ρ
  symEq⋆ eq⋆[]         = eq⋆[]
  symEq⋆ (eq⋆≔ eq⋆ eq) = eq⋆≔ (symEq⋆ eq⋆) (symEq eq)

  transEq⋆ : ∀ {Γ w} {ρ ρ′ ρ″ : w ⊩⋆ Γ} → Eq⋆ ρ ρ′ → Eq⋆ ρ′ ρ″ → Eq⋆ ρ ρ″
  transEq⋆ eq⋆[]         eq⋆[]           = eq⋆[]
  transEq⋆ (eq⋆≔ eq⋆ eq) (eq⋆≔ eq⋆′ eq′) = eq⋆≔ (transEq⋆ eq⋆ eq⋆′) (transEq eq eq′)

module _ {{_ : Model}} where
  ≡→Eq⋆ : ∀ {Γ w} {ρ ρ′ : w ⊩⋆ Γ} → 𝒰⋆ ρ → ρ ≡ ρ′ → Eq⋆ ρ ρ′
  ≡→Eq⋆ u⋆ refl = reflEq⋆ u⋆

  module Eq⋆Reasoning where
    infix 1 begin_
    begin_ : ∀ {Γ w} {ρ ρ′ : w ⊩⋆ Γ} → Eq⋆ ρ ρ′ → Eq⋆ ρ ρ′
    begin eq⋆ = eq⋆

    infixr 2 _Eq⋆⟨⟩_
    _Eq⋆⟨⟩_ : ∀ {Γ w} (ρ {ρ′} : w ⊩⋆ Γ) → Eq⋆ ρ ρ′ → Eq⋆ ρ ρ′
    ρ Eq⋆⟨⟩ eq⋆ = eq⋆

    infixr 2 _Eq⋆⟨_⟩_
    _Eq⋆⟨_⟩_ : ∀ {Γ w} (ρ {ρ′ ρ″} : w ⊩⋆ Γ) → Eq⋆ ρ ρ′ → Eq⋆ ρ′ ρ″ → Eq⋆ ρ ρ″
    ρ Eq⋆⟨ eq⋆ ⟩ eq⋆′ = transEq⋆ eq⋆ eq⋆′

    infixr 2 _≡⟨⟩_
    _≡⟨⟩_ : ∀ {Γ w} (ρ {ρ′} : w ⊩⋆ Γ) → Eq⋆ ρ ρ′ → Eq⋆ ρ ρ′
    ρ ≡⟨⟩ eq⋆ = eq⋆

    infixr 2 _≡⟨_∣_⟩_
    _≡⟨_∣_⟩_ : ∀ {Γ w} (ρ {ρ′ ρ″} : w ⊩⋆ Γ) → ρ ≡ ρ′ → 𝒰⋆ ρ → Eq⋆ ρ′ ρ″ → Eq⋆ ρ ρ″
    ρ ≡⟨ eq⋆ ∣ u⋆ ⟩ eq⋆′ = transEq⋆ (≡→Eq⋆ u⋆ eq⋆) eq⋆′

    infix 3 _∎⟨_⟩
    _∎⟨_⟩ : ∀ {Γ w} (ρ : w ⊩⋆ Γ) → 𝒰⋆ ρ → Eq⋆ ρ ρ
    ρ ∎⟨ u⋆ ⟩ = reflEq⋆ u⋆

-- We can substitute equal semantic environments in `lookup`, `↑⟨_⟩`, `↓⟨_⟩`
-- and the result of applying these functions to uniform environments is also uniform.

module _ {{_ : Model}} where
  conglookupEq : ∀ {Γ A w x} →
                   {ρ ρ′ : w ⊩⋆ Γ} → Eq⋆ ρ ρ′ → (i : Γ ∋ x ∷ A) →
                   Eq (lookup ρ i) (lookup ρ′ i)
  conglookupEq eq⋆[]         ()
  conglookupEq (eq⋆≔ eq⋆ eq) zero    = eq
  conglookupEq (eq⋆≔ eq⋆ eq) (suc i) = conglookupEq eq⋆ i

  cong↑⟨_⟩Eq⋆ : ∀ {Γ w w′} →
                  (c : w′ ⊒ w) → {ρ ρ′ : w ⊩⋆ Γ} → Eq⋆ ρ ρ′ →
                  Eq⋆ (↑⟨ c ⟩ ρ) (↑⟨ c ⟩ ρ′)
  cong↑⟨ c ⟩Eq⋆ eq⋆[]         = eq⋆[]
  cong↑⟨ c ⟩Eq⋆ (eq⋆≔ eq⋆ eq) = eq⋆≔ (cong↑⟨ c ⟩Eq⋆ eq⋆) (cong↑⟨ c ⟩Eq eq)

  cong↓⟨_⟩Eq⋆ : ∀ {Γ Δ w} →
                  (c : Γ ⊇ Δ) → {ρ ρ′ : w ⊩⋆ Γ} → Eq⋆ ρ ρ′ →
                  Eq⋆ (↓⟨ c ⟩ ρ) (↓⟨ c ⟩ ρ′)
  cong↓⟨ done ⟩Eq⋆     eq⋆ = eq⋆[]
  cong↓⟨ step c i ⟩Eq⋆ eq⋆ = eq⋆≔ (cong↓⟨ c ⟩Eq⋆ eq⋆) (conglookupEq eq⋆ i)

  conglookup𝒰 : ∀ {Γ A w x} →
                  {ρ : w ⊩⋆ Γ} → 𝒰⋆ ρ → (i : Γ ∋ x ∷ A) →
                  𝒰 (lookup ρ i)
  conglookup𝒰 𝓊⋆[]       ()
  conglookup𝒰 (𝓊⋆≔ u⋆ u) zero    = u
  conglookup𝒰 (𝓊⋆≔ u⋆ u) (suc i) = conglookup𝒰 u⋆ i

  cong↑⟨_⟩𝒰⋆ : ∀ {Γ w w′} →
                 (c : w′ ⊒ w) → {ρ : w ⊩⋆ Γ} → 𝒰⋆ ρ →
                 𝒰⋆ (↑⟨ c ⟩ ρ)
  cong↑⟨ c ⟩𝒰⋆ 𝓊⋆[]       = 𝓊⋆[]
  cong↑⟨ c ⟩𝒰⋆ (𝓊⋆≔ u⋆ u) = 𝓊⋆≔ (cong↑⟨ c ⟩𝒰⋆ u⋆) (cong↑⟨ c ⟩𝒰 u)

  cong↓⟨_⟩𝒰⋆ : ∀ {Γ Δ w} →
                 (c : Γ ⊇ Δ) → {ρ : w ⊩⋆ Γ} → 𝒰⋆ ρ →
                 𝒰⋆ (↓⟨ c ⟩ ρ)
  cong↓⟨ done ⟩𝒰⋆     u⋆ = 𝓊⋆[]
  cong↓⟨ step c i ⟩𝒰⋆ u⋆ = 𝓊⋆≔ (cong↓⟨ c ⟩𝒰⋆ u⋆) (conglookup𝒰 u⋆ i)

-- We also
-- need to prove the following properties about `Eq⋆` for semantic environments which basically
-- say that it doesn’t matter in which order we lift and project the substitution:

module _ {{_ : Model}} where
  aux₄₂₁⟨_⟩ : ∀ {Γ Δ A w x} →
                (c : Γ ⊇ Δ) → {ρ : w ⊩⋆ Γ} → 𝒰⋆ ρ → (i : Γ ∋ x ∷ A) (j : Δ ∋ x ∷ A) →
                Eq (lookup ρ i) (lookup (↓⟨ c ⟩ ρ) j)
  aux₄₂₁⟨ done ⟩      u⋆ i ()
  aux₄₂₁⟨ step c i′ ⟩ u⋆ i zero    rewrite uniq∋ i′ i
                                   = conglookupEq (reflEq⋆ u⋆) i
  aux₄₂₁⟨ step c i′ ⟩ u⋆ i (suc j) = aux₄₂₁⟨ c ⟩ u⋆ i j

  conglookup↑⟨_⟩Eq : ∀ {Γ A w w′ x} {ρ : w ⊩⋆ Γ} →
                       (c : w′ ⊒ w) → 𝒰⋆ ρ → (i : Γ ∋ x ∷ A) →
                       Eq (↑⟨ c ⟩ (lookup ρ i)) (lookup (↑⟨ c ⟩ ρ) i)
  conglookup↑⟨ c ⟩Eq 𝓊⋆[]       ()
  conglookup↑⟨ c ⟩Eq (𝓊⋆≔ u⋆ u) zero    = cong↑⟨ c ⟩Eq (reflEq u)
  conglookup↑⟨ c ⟩Eq (𝓊⋆≔ u⋆ u) (suc i) = conglookup↑⟨ c ⟩Eq u⋆ i

  aux₄₂₃ : ∀ {Γ Δ A w x} {{_ : T (fresh x Δ)}} {{_ : T (fresh x Γ)}} →
             (c : Γ ⊇ Δ) (c′ : [ Γ , x ∷ A ] ⊇ Δ) → {ρ : w ⊩⋆ Γ} → 𝒰⋆ ρ → {a : w ⊩ A} →
             Eq⋆ (↓⟨ c′ ⟩ [ ρ , x ≔ a ]) (↓⟨ c ⟩ ρ)
  aux₄₂₃               done       done               u⋆ = eq⋆[]
  aux₄₂₃ {x = x} {{φ}} (step c i) (step c′ zero)     u⋆ = elim⊥ (freshlem₁ x φ)
  aux₄₂₃ {x = x} {{φ}} (step c i) (step c′ (suc i′)) u⋆ rewrite uniq∋ i′ i
                                                        = eq⋆≔ (aux₄₂₃ {{freshlem₂ x φ}} c c′ u⋆)
                                                               (reflEq (conglookup𝒰 u⋆ i))

  aux₄₂₄⟨_⟩ : ∀ {Γ w} →
                (c : Γ ⊇ Γ) → {ρ : w ⊩⋆ Γ} → 𝒰⋆ ρ →
                Eq⋆ (↓⟨ c ⟩ ρ) ρ
  aux₄₂₄⟨ done ⟩     𝓊⋆[]       = eq⋆[]
  aux₄₂₄⟨ step c i ⟩ (𝓊⋆≔ u⋆ u) = eq⋆≔ (transEq⋆ (aux₄₂₃ refl⊇ c u⋆)
                                                 (aux₄₂₄⟨ refl⊇ ⟩ u⋆))
                                       (aux₄₂₁⟨ refl⊇ ⟩ (𝓊⋆≔ u⋆ u) i zero)

  aux₄₂₅⟨_⟩ : ∀ {Γ w} →
                (c : w ⊒ w) → {ρ : w ⊩⋆ Γ} → 𝒰⋆ ρ →
                Eq⋆ (↑⟨ c ⟩ ρ) ρ
  aux₄₂₅⟨ c ⟩ 𝓊⋆[]       = eq⋆[]
  aux₄₂₅⟨ c ⟩ (𝓊⋆≔ u⋆ u) = eq⋆≔ (aux₄₂₅⟨ c ⟩ u⋆) (aux₄₁₁⟨ c ⟩ u)

  aux₄₂₆ : ∀ {Γ Δ Θ w} →
             (c : Δ ⊇ Γ) (c′ : Θ ⊇ Δ) (c″ : Θ ⊇ Γ) → {ρ : w ⊩⋆ Θ} → 𝒰⋆ ρ →
             Eq⋆ (↓⟨ c ⟩ (↓⟨ c′ ⟩ ρ)) (↓⟨ c″ ⟩ ρ)
  aux₄₂₆ done        c′ done         u⋆ = eq⋆[]
  aux₄₂₆ (step c i)  c′ (step c″ i″) u⋆ = eq⋆≔ (aux₄₂₆ c c′ c″ u⋆)
                                               (symEq (aux₄₂₁⟨ c′ ⟩ u⋆ i″ i))

  aux₄₂₇ : ∀ {Γ w w′ w″} →
             (c : w′ ⊒ w) (c′ : w″ ⊒ w′) (c″ : w″ ⊒ w) → {ρ : w ⊩⋆ Γ} → 𝒰⋆ ρ →
             Eq⋆ (↑⟨ c′ ⟩ (↑⟨ c ⟩ ρ)) (↑⟨ c″ ⟩ ρ)
  aux₄₂₇ c c′ c″ 𝓊⋆[]       = eq⋆[]
  aux₄₂₇ c c′ c″ (𝓊⋆≔ u⋆ u) = eq⋆≔ (aux₄₂₇ c c′ c″ u⋆) (aux₄₁₂ c c′ c″ u)

  aux₄₂₈ : ∀ {Γ Δ w w′} →
             (c : Δ ⊇ Γ) (c′ : w′ ⊒ w) → {ρ : w ⊩⋆ Δ} → 𝒰⋆ ρ →
             Eq⋆ (↑⟨ c′ ⟩ (↓⟨ c ⟩ ρ)) (↓⟨ c ⟩ (↑⟨ c′ ⟩ ρ))
  aux₄₂₈ done       c′ u⋆ = eq⋆[]
  aux₄₂₈ (step c i) c′ u⋆ = eq⋆≔ (aux₄₂₈ c c′ u⋆) (conglookup↑⟨ c′ ⟩Eq u⋆ i)

-- These properties are used in the proofs of soundness and completeness below.

-- 4.3. The semantics of the λ-calculus
-- ------------------------------------
--
-- We define evaluation functions for proof trees and substitutions in a given environment:  (…)

module _ {{_ : Model}} where
  mutual
    ⟦_⟧ : ∀ {Γ A w} → Γ ⊢ A → w ⊩⋆ Γ → w ⊩ A
    ⟦ ν x i ⟧ ρ = lookup ρ i
    ⟦ ƛ x M ⟧ ρ = ⟦ƛ⟧ (λ c a → ⟦ M ⟧ [ ↑⟨ c ⟩ ρ , x ≔ a ])
    ⟦ M ∙ N ⟧ ρ = ⟦ M ⟧ ρ ⟦∙⟧⟨ refl⊒ ⟩ ⟦ N ⟧ ρ
    ⟦ M ▶ γ ⟧ ρ = ⟦ M ⟧ (⟦ γ ⟧ₛ ρ)

    ⟦_⟧ₛ : ∀ {Γ Δ w} → Δ ⋙ Γ → w ⊩⋆ Δ → w ⊩⋆ Γ
    ⟦ π⟨ c ⟩ ⟧ₛ        ρ = ↓⟨ c ⟩ ρ
    ⟦ γ ● γ′ ⟧ₛ        ρ = ⟦ γ ⟧ₛ (⟦ γ′ ⟧ₛ ρ)
    ⟦ [ γ , x ≔ M ] ⟧ₛ ρ = [ ⟦ γ ⟧ₛ ρ , x ≔ ⟦ M ⟧ ρ ]

max_stars_repo_name: mietek/coquand

max_issues_repo_name: mietek/coquand

max_forks_repo_name: mietek/coquand


text:
{-# OPTIONS --without-K #-}
module sets.list where

open import sets.list.core public

ext: agda

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
module UnicodeSetIndex where

X : Set₁₄₀
X = Set₁₃₉

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- Andreas, 2015-05-09 trigger some option errors

{-# OPTIONS
  --dont-termination-check
  --not-termination-check
  --without-K=4
  --without-k
  --senf-gurke
  #-}

{- Expected error:
Unrecognized options:
--dont-termination-check (did you mean --no-termination-check ?)
--not-termination-check (did you mean --no-termination-check ?)
--without-k (did you mean --without-K ?)
--senf-gurke
Option error:
option `--without-K' doesn't allow an argument
-}


text:
module utility where

open import Algebra
  using (Monoid)
open import Algebra.Structures
  using (IsMonoid ; IsSemigroup)
open import Data.Empty
open import Function
  using (_∘_)
open import Relation.Binary
  using (Decidable)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; setoid ; sym ; cong)
open import Relation.Nullary
open import Relation.Nullary.Decidable
  using (⌊_⌋)
open import Data.Bool
  using (not)
open import Data.List
open import Data.List.Properties
  using (map-id ; map-compose ; map-cong)
open import Data.List.Any as ListAny
  using (Any ; any ; here ; there)
open import Data.List.Any.Properties using ( ∷↔ ; ++⁻)
  renaming (++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ)
open import Data.Nat
  using (ℕ ; zero ; suc ; _≟_ ; _+_ ; _∸_)
open import Data.Nat.Properties.Simple
  using (+-comm)
open import Data.Nat.Properties
  using (n∸n≡0 ; m+n∸n≡m)
open import Data.Product
  using (_,_ ; _,′_ ; _×_ ; proj₁ ; proj₂ ; ∃)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Function
  using (_∘_ ; id)
import Data.List.Membership.Setoid

++-assoc : ∀{A : Set} → (xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc {_} xs ys zs =
  IsSemigroup.assoc (IsMonoid.isSemigroup (Monoid.isMonoid (Data.List.Properties.++-monoid _))) xs _ _

_∈_ : {A : Set} → (x : A) → (xs : List A) → Set
_∈_ {A} x xs = Data.List.Membership.Setoid._∈_ (setoid A) x xs

_∉_ : {A : Set} → (x : A) → (xs : List A) → Set
_∉_ {A} x xs = Data.List.Membership.Setoid._∉_ (setoid A) x xs

map-second : {A B C D : Set} →
  (f : B → D) →
  A × B × C → A × D × C
map-second f = Data.Product.map id (Data.Product.map f id)

any-map⁺ : ∀ {A B} {xs : List A} {x} (f : A → B) →
  x ∈ xs → f x ∈ map f xs
any-map⁺ f (here refl)  = here refl
any-map⁺ f (there x∈xs) = there (any-map⁺ f x∈xs)

-- the map-mono like the one in Data.List.Any.Membership
-- idk why I can't import that module so I just implement one here
map-mono : ∀ {A B} {ys zs : List A} (f : A → B) →
  (∀ x → x ∈ ys → x ∈ zs) → ∀ fx → fx ∈ map f ys → fx ∈ map f zs
map-mono {ys = []} f ys⊆zs fx ()
map-mono {ys = y ∷ ys} {zs} f ys⊆zs .(f y) (here refl) =
  any-map⁺ f (ys⊆zs y (here refl))
map-mono {ys = y ∷ ys} {zs} f ys⊆zs fx (there fx∈map-f-ys) =
  map-mono f (λ x z → ys⊆zs x (there z)) fx fx∈map-f-ys

any-map⁺² : ∀ {A B : Set} {xs x fxy} (f : A → List B) →
  x ∈ xs → fxy ∈ f x → fxy ∈ concatMap f xs
any-map⁺² f (here refl)  fxy∈fx = ++ˡ fxy∈fx
any-map⁺² f (there x∈xs) fxy∈fx = ++ʳ (f _) (any-map⁺² f x∈xs fxy∈fx)

map-mono² : ∀ {A B C} {xs xs' : List A} {ys ys' : List B} (f : A → B → C) →
  (∀ u → u ∈ xs → u ∈ xs') →
  (∀ v → v ∈ ys → v ∈ ys') →
  ∀ fuv →
    fuv ∈ concatMap (λ u → map (f u) ys)  xs →
    fuv ∈ concatMap (λ u → map (f u) ys') xs'
map-mono² {xs = []} {xs'} {ys} {ys'} f xs⊆xs' ys⊆ys' fuv ()
map-mono² {xs = x ∷ xs} {xs'} {ys} {ys'} f xs⊆xs' ys⊆ys' fuv fuv∈[[fuv|ys]|x∷xs]
  with ++⁻ (map (f x) ys) fuv∈[[fuv|ys]|x∷xs]
... | inj₂ fuv∈[[fuv|ys]|xs] =
  map-mono² f (λ u → xs⊆xs' u ∘ there) ys⊆ys' fuv fuv∈[[fuv|ys]|xs]
... | inj₁ fuv∈[fxv|ys] =
  any-map⁺² (λ u → map (f u) ys')
    (xs⊆xs' x (here refl))
    (map-mono (f x) ys⊆ys' fuv fuv∈[fxv|ys])

module ListSet {A : Set} (_≟_ : Decidable {A = A} _≡_) where
  open import Relation.Nullary.Negation using (¬?)
  ST : Set
  ST = List A

  set-subtract : List A → List A → List A
  set-subtract S T = filter (λ x → ¬? (ListAny.any (_≟_ x) T)) S

  set-remove : List A → A → List A
  set-remove S x = filter (¬? ∘ _≟_ x) S

  set-remove-removed : ∀{S L} → S ∉ set-remove L S
  set-remove-removed {S} {[]} ()
  set-remove-removed {S} {x ∷ L} Sin with S ≟ x | set-remove-removed{S}{L}
  set-remove-removed {S} {x ∷ L} Sin | yes refl | r = r Sin
  set-remove-removed {S} {x ∷ L} (here px) | no ¬p | r = ¬p px
  set-remove-removed {S} {x ∷ L} (there Sin) | no ¬p | r = r Sin

  set-remove-not-eq : ∀{a a' xs} → a ∈ set-remove xs a' → ¬ a' ≡ a
  set-remove-not-eq {a}{a'}{xs} a∈xs-a' with a' ≟ a
  ... | yes refl = ⊥-elim (set-remove-removed{a}{xs} a∈xs-a')
  ... | no ¬refl = ¬refl

  set-remove-mono-∈ : ∀ {xs a} a' → a ∈ set-remove xs a' → a ∈ xs
  set-remove-mono-∈ {[]}       {a} a' ()
  set-remove-mono-∈ {(x ∷ xs)} {a} a' a∈xs-[a'] with a' ≟ x
  set-remove-mono-∈ {(x ∷ xs)} {a} a' a∈xs-[a']
    | yes a'≡x = there (set-remove-mono-∈ a' a∈xs-[a'])
  set-remove-mono-∈ {(x ∷ xs)} {a} a' (here refl)
    | no ¬a'≡x = here refl
  set-remove-mono-∈ {(x ∷ xs)} {a} a' (there a∈xs-[a'])
    | no ¬a'≡x = there (set-remove-mono-∈ a' a∈xs-[a'])

  set-remove-not-removed : ∀ {a' a xs} → ¬ (a' ≡ a) → a ∈ xs → a ∈ set-remove xs a'
  set-remove-not-removed {a'} {a} {.a ∷ xs} a'≢a (here refl)  with a' ≟ a
  ... | yes a'≡a = ⊥-elim (a'≢a a'≡a)
  ... | no ¬a'≡a = here refl
  set-remove-not-removed {a'} {a} {x ∷ xs} a'≢a (there a∈xs) with a' ≟ x
  ... | yes a'≡x = set-remove-not-removed a'≢a a∈xs
  ... | no ¬a'≡x = there (set-remove-not-removed a'≢a a∈xs)

  set-subtract-[] : ∀ xs → set-subtract xs [] ≡ xs
  set-subtract-[] [] = refl
  set-subtract-[] (x ∷ xs) rewrite set-subtract-[] xs = refl

  set-subtract-[a]≡set-remove : ∀ xs a → set-subtract xs (a ∷ []) ≡ set-remove xs a
  set-subtract-[a]≡set-remove [] a = refl
  set-subtract-[a]≡set-remove (x ∷ xs) a
    with x ≟ a | a ≟ x
  ... | yes refl | no  a≢x  = ⊥-elim (a≢x refl)
  ... | no  x≢a  | yes refl = ⊥-elim (x≢a refl)
  ... | yes refl | yes a≡x =  set-subtract-[a]≡set-remove xs x
  ... | no  x≢a  | no  a≢x  rewrite set-subtract-[a]≡set-remove xs a =  refl

  set-subtract-merge : ∀ {xs ys z} → z ∈ set-subtract xs ys → (z ∈ xs) × (z ∉ ys)
  set-subtract-merge {[]} ()
  set-subtract-merge {x ∷ xs} {ys} z∈xs-ys with ListAny.any (_≟_ x) ys
  set-subtract-merge {x ∷ xs} {ys} (here refl)     | no x∉ys = here refl ,′ x∉ys
  set-subtract-merge {x ∷ xs} {ys} (there z∈xs-ys) | no x∉ys = there z∈xs , z∉ys
    where z∈xs,z∉ys = set-subtract-merge {xs} {ys} z∈xs-ys
          z∈xs      = proj₁ z∈xs,z∉ys
          z∉ys      = proj₂ z∈xs,z∉ys
  ... | yes x∈ys = there z∈xs , z∉ys
    where z∈xs,z∉ys = set-subtract-merge {xs} {ys} z∈xs-ys
          z∈xs      = proj₁ z∈xs,z∉ys
          z∉ys      = proj₂ z∈xs,z∉ys

  set-subtract-split : ∀ {xs ys z} → z ∈ xs → z ∈ set-subtract xs ys ⊎ z ∈ ys
  set-subtract-split {[]}     ()
  set-subtract-split {x ∷ xs} {ys} (here refl) with ListAny.any (_≟_ x) ys
  ... | yes x∈ys = inj₂ x∈ys
  ... | no  x∉ys = inj₁ ( (here refl) )
  set-subtract-split {x ∷ xs} {ys} (there x∈xs)
    with ListAny.any (_≟_ x) ys | set-subtract-split x∈xs
  ... | x∈ys⊎x∉ys | inj₂ z∈ys    = inj₂ z∈ys
  ... | yes x∈ys  | inj₁ z∈xs-ys = inj₁  z∈xs-ys
  ... | no  x∉ys  | inj₁ z∈xs-ys = inj₁ ( (there z∈xs-ys) )

  set-subtract-notin : ∀ {xs ys z} → z ∈ xs → z ∉ ys → z ∈ set-subtract xs ys
  set-subtract-notin{xs}{ys}{z} z∈ z∉ with set-subtract-split{xs}{ys}{z} z∈
  ... | inj₁ a = a
  ... | inj₂ b = ⊥-elim (z∉ b)

-- note: the fixity of our triple-apply _#_ combinator
-- is different from the usual fixity of _$_.
infixl 1 _#_

-- applying three functions to three values in parallel
_#_ : {A B C : Set} → {D : A → Set} → {E : B → Set} → {F : C → Set} →
  ((a : A) → D a) × ((b : B) → E b) × ((c : C) → F c) →
  (abc : A × B × C) → D (proj₁ abc) × E (proj₁ (proj₂ abc)) × F (proj₂ (proj₂ abc))
(f , g , h) # (x , y , z) = f x ,′ g y ,′ h z

infix 6 _U̬_

_U̬_ : List ℕ × List ℕ × List ℕ → List ℕ × List ℕ × List ℕ → List ℕ × List ℕ × List ℕ
(S , s , v) U̬ (S1 , s1 , v1) = S ++ S1 ,′ s ++ s1 ,′ v ++ v1
infixr 6 _|̌_
infixr 6 _|¹_
_|¹_ = ListSet.set-subtract Data.Nat._≟_
_|̌_ : List ℕ × List ℕ × List ℕ → List ℕ × List ℕ × List ℕ → List ℕ × List ℕ × List ℕ
(S , s , x) |̌ (S1 , s1 , x1)
   = (S |¹ S1) , (s |¹ s1) , (x |¹ x1)

∪-assoc : ∀ xs³ ys³ zs³ → (xs³ U̬ ys³) U̬ zs³ ≡ xs³ U̬ (ys³ U̬ zs³)
∪-assoc xs³ ys³ zs³
  rewrite ++-assoc (proj₁ xs³)         (proj₁ ys³)         (proj₁ zs³)
        | ++-assoc (proj₁ (proj₂ xs³)) (proj₁ (proj₂ ys³)) (proj₁ (proj₂ zs³))
        | ++-assoc (proj₂ (proj₂ xs³)) (proj₂ (proj₂ ys³)) (proj₂ (proj₂ zs³)) = refl

xs++[]≡xs : ∀{A : Set} → (xs : List A) → xs ++ [] ≡ xs
xs++[]≡xs xs = proj₂ (Monoid.identity (Data.List.Properties.++-monoid _)) xs

x∈xs++[]→x∈xs : ∀{A} → {x : A} → {xs : List A} → x ∈ (xs ++ []) → x ∈ xs
x∈xs++[]→x∈xs {xs = xs} x∈xs rewrite xs++[]≡xs xs = x∈xs

_⊆¹_ : List ℕ → List ℕ → Set
xs ⊆¹ ys = ∀ x → x ∈ xs → x ∈ ys

_⊆_ : List ℕ × List ℕ × List ℕ → List ℕ × List ℕ × List ℕ → Set
(Ss₁ , ss₁ , xs₁) ⊆ (Ss₂ , ss₂ , xs₂) =
  (Ss₁ ⊆¹ Ss₂) × (ss₁ ⊆¹ ss₂) × (xs₁ ⊆¹ xs₂)

⊆¹-refl : ∀ {xs} → xs ⊆¹ xs
⊆¹-refl _ p = p

⊆-refl : ∀ {xs³} → xs³ ⊆ xs³
⊆-refl = ⊆¹-refl ,′ ⊆¹-refl ,′ ⊆¹-refl

⊆-empty-left : ∀ {xs³} → ([] ,′ [] ,′ []) ⊆ xs³
⊆-empty-left = (λ _ ()) ,′ (λ _ ()) ,′ (λ _ ())

⊆¹-trans : ∀{xs ys zs} → xs ⊆¹ ys → ys ⊆¹ zs → xs ⊆¹ zs
⊆¹-trans xs⊆ys ys⊆zs w w∈xs = ys⊆zs _ (xs⊆ys _ w∈xs)

⊆-trans : ∀{xs³ ys³ zs³} → xs³ ⊆ ys³ → ys³ ⊆ zs³ → xs³ ⊆ zs³
⊆-trans xs³⊆ys³ ys³⊆zs³ = ⊆¹-trans ,′ ⊆¹-trans ,′ ⊆¹-trans # xs³⊆ys³ # ys³⊆zs³

⊆¹-respect-|¹ : ∀{xs ys} zs → xs ⊆¹ ys → (xs |¹ zs) ⊆¹ (ys |¹ zs)
⊆¹-respect-|¹{xs}{ys} zs xs⊂ys a a∈ with ListSet.set-subtract-merge Data.Nat._≟_ {xs}{zs}{a} a∈
... | (a∈xs , a∉zs) = ListSet.set-subtract-notin Data.Nat._≟_ (xs⊂ys a a∈xs) a∉zs

⊆-respect-|̌ : ∀{xs ys} zs → xs ⊆ ys → (xs |̌ zs) ⊆ (ys |̌ zs)
⊆-respect-|̌ zs sub = ⊆¹-respect-|¹ , ⊆¹-respect-|¹  , ⊆¹-respect-|¹  # zs # sub

∷-respect-⊆¹ : ∀{xs ys} z → xs ⊆¹ ys → (z ∷ xs) ⊆¹ (z ∷ ys)
∷-respect-⊆¹ z sub .z (here refl) = here refl
∷-respect-⊆¹ z sub a (there a∈) = there (sub a a∈)

∪ˡ : ∀{xs³ ys³ zs³} → xs³ ⊆ ys³ → xs³ ⊆ (ys³ U̬ zs³)
∪ˡ (Ss₁⊆Ss₂ , ss₁⊆ss₂ , xs₁⊆xs₂) =
  (λ S → ++ˡ ∘ Ss₁⊆Ss₂ S) ,′
  (λ s → ++ˡ ∘ ss₁⊆ss₂ s) ,′
  (λ x → ++ˡ ∘ xs₁⊆xs₂ x)

∪ʳ : ∀{xs³ ys³} → (zs³ : List ℕ × List ℕ × List ℕ) → xs³ ⊆ ys³ → xs³ ⊆ (zs³ U̬ ys³)
∪ʳ xs (Ss₁⊆Ss₂ , ss₁⊆ss₂ , xs₁⊆xs₂) =
  (λ S → ++ʳ (proj₁ xs)         ∘ Ss₁⊆Ss₂ S) ,′
  (λ s → ++ʳ (proj₁ (proj₂ xs)) ∘ ss₁⊆ss₂ s) ,′
  (λ x → ++ʳ (proj₂ (proj₂ xs)) ∘ xs₁⊆xs₂ x)

∪¹-unjoin-⊆¹ : ∀ {ys zs} xs → (xs ++ ys) ⊆¹ zs → xs ⊆¹ zs × ys ⊆¹ zs
∪¹-unjoin-⊆¹ xs xs++ys⊆zs = (λ x x∈xs → xs++ys⊆zs x (++ˡ x∈xs)) ,′
                           (λ x x∈ys → xs++ys⊆zs x (++ʳ xs x∈ys))

∪-unjoin-⊆ : ∀ {ys³ zs³} xs³ → (xs³ U̬ ys³) ⊆ zs³ → xs³ ⊆ zs³ × ys³ ⊆ zs³
∪-unjoin-⊆ xs³ xs³∪ys³⊆zs³ = unzip³ (∪¹-unjoin-⊆¹ ,′ ∪¹-unjoin-⊆¹ ,′ ∪¹-unjoin-⊆¹ #
                                      xs³ # xs³∪ys³⊆zs³)
  where unzip³ : {A B C D E F : Set} → (A × D) × (B × E) × (C × F) → (A × B × C) × (D × E × F)
        unzip³ ((a , d) , (b , e) , (c , f)) = (a , b , c) , (d , e , f)

∪-unjoin-⊆ˡ : ∀{xs³ ys³ zs³} → (xs³ U̬ ys³) ⊆ zs³ → xs³ ⊆ zs³
∪-unjoin-⊆ˡ {xs³} = proj₁ ∘ ∪-unjoin-⊆ xs³

∪-unjoin-⊆ʳ : ∀ {ys³ zs³} xs³ → (xs³ U̬ ys³) ⊆ zs³ → ys³ ⊆ zs³
∪-unjoin-⊆ʳ xs³ = proj₂ ∘ ∪-unjoin-⊆ xs³

∪¹-join-⊆¹ : ∀{xs ys zs} → xs ⊆¹ zs → ys ⊆¹ zs → (xs ++ ys) ⊆¹ zs
∪¹-join-⊆¹ {xs} xs⊆zs ys⊆zs w w∈xs++ys with ++⁻ xs w∈xs++ys
... | inj₁ w∈xs = xs⊆zs _ w∈xs
... | inj₂ w∈ys = ys⊆zs _ w∈ys

∪-join-⊆ : ∀{xs³ ys³ zs³} → xs³ ⊆ zs³ → ys³ ⊆ zs³ → (xs³ U̬ ys³) ⊆ zs³
∪-join-⊆ xs³⊆zs³ ys³⊆zs³ = ∪¹-join-⊆¹ ,′ ∪¹-join-⊆¹ ,′ ∪¹-join-⊆¹ # xs³⊆zs³ # ys³⊆zs³

∪-respect-⊆-left : ∀{xs³ ys³ zs³} → xs³ ⊆ ys³ → (xs³ U̬ zs³) ⊆ (ys³ U̬ zs³)
∪-respect-⊆-left {xs³} {ys³} {zs³} xs³⊆ys³ = ∪-join-⊆ (∪ˡ xs³⊆ys³) (∪ʳ ys³ ⊆-refl)

∪-respect-⊆-right : ∀{xs³ ys³} zs³ → xs³ ⊆ ys³ → (zs³ U̬ xs³) ⊆ (zs³ U̬ ys³)
∪-respect-⊆-right {xs³} {ys³} zs³ xs³⊆ys³ = ∪-join-⊆ (∪ˡ (⊆-refl {zs³})) (∪ʳ zs³ xs³⊆ys³)

∪¹-respect-⊆¹-right : ∀ {xs ys} zs → xs ⊆¹ ys → (zs ++ xs) ⊆¹ (zs ++ ys)
∪¹-respect-⊆¹-right zs xs⊆ys = proj₁ (∪-respect-⊆-right (zs ,′ [] ,′ []) (xs⊆ys ,′ ⊆¹-refl {[]} ,′ ⊆¹-refl {[]}))

∪¹-respect-⊆¹-left : ∀ {xs ys zs} → xs ⊆¹ ys → (xs ++ zs) ⊆¹ (ys ++ zs)
∪¹-respect-⊆¹-left{zs = zs} xs⊆ys =  proj₁ (∪-respect-⊆-left{zs³ = (zs ,′ [] ,′ [])} (xs⊆ys ,′ ⊆¹-refl {[]} ,′ ⊆¹-refl {[]}))

⊆-subst-left : ∀{xs³ ys³ zs³} → xs³ ≡ ys³ → xs³ ⊆ zs³ → ys³ ⊆ zs³
⊆-subst-left refl xs³⊆zs³ = xs³⊆zs³

∪-comm-⊆-left : ∀ {ys³ zs³} xs³ → (xs³ U̬ ys³) ⊆ zs³ → (ys³ U̬ xs³) ⊆ zs³
∪-comm-⊆-left xs³ xs³∪ys³⊆zs³ =
  ∪-join-⊆ (proj₂ (∪-unjoin-⊆ xs³ xs³∪ys³⊆zs³)) (proj₁ (∪-unjoin-⊆ xs³ xs³∪ys³⊆zs³))

∪-comm-⊆-right : ∀ {xs³ ys³} zs³ → xs³ ⊆ (ys³ U̬ zs³) → xs³ ⊆ (zs³ U̬ ys³)
∪-comm-⊆-right zs³ xs³⊆ys³∪zs³ = ⊆-trans xs³⊆ys³∪zs³ (∪-join-⊆ (∪ʳ zs³ ⊆-refl) (∪ˡ ⊆-refl))

distinct' : ∀{A : Set} -> (xs : List A) -> (ys : List A) -> Set
distinct'{A} xs ys = (z : A) -> z ∈ xs -> z ∈ ys -> ⊥

distinct : (xs : List ℕ × List ℕ × List ℕ) -> (ys : List ℕ × List ℕ × List ℕ) -> Set
distinct (S , s , v) (S1 , s1 , v1) = distinct' S S1 × distinct' s s1 × distinct' v v1

distinct-empty-left : ∀ {xs³} → distinct ([] ,′ [] ,′ []) xs³
distinct-empty-left = (λ _ ()) ,′ (λ _ ()) ,′ (λ _ ())

distinct-empty-right : ∀ {xs³} → distinct xs³ ([] ,′ [] ,′ [])
distinct-empty-right = (λ _ _ ()) ,′ (λ _ _ ()) ,′ (λ _ _ ())

distinct'-sym : ∀{A L1 L2} → (distinct'{A} L1 L2) → (distinct'{A} L2 L1)
distinct'-sym d = λ z x x₁ → d z x₁ x

distinct'-to-left : {xs ys zs : List ℕ} →
  (distinct' xs ys → distinct' xs zs) →
  distinct' ys xs → distinct' zs xs
distinct'-to-left f ys≠xs = distinct'-sym (f (distinct'-sym ys≠xs))

distinct-sym : ∀{VL1 VL2} → distinct VL1 VL2 → distinct VL2 VL1
distinct-sym (a , b , c) = (distinct'-sym a) , ((distinct'-sym b) , (distinct'-sym c))

dist'++ˡ : ∀{A V1 V2 V3} → (distinct'{A} V1 (V2 ++ V3)) → (distinct'{A} V1 V2)
dist'++ˡ {A} {V1} {V2} {V3} d = λ z x x₁ → d z x (++ˡ x₁)

dist'++ʳ : ∀{A V1 V2 V3} → (distinct'{A} V1 (V2 ++ V3)) → (distinct'{A} V1 V3)
dist'++ʳ {A} {V1} {V2} {V3} d = λ z x x₁ → d z x (++ʳ V2 x₁)

dist'++b : ∀{A V1 V2 V3 V4} → (distinct'{A} (V1 ++ V2) (V3 ++ V4)) → (distinct'{A} V1 V3)
dist'++b d = λ z x x₁ → d z (++ˡ x) (++ˡ x₁)

dist':: : ∀{A V1 V2 S} → (distinct'{A} V1 (S ∷ V2)) → (distinct' V1 V2)
dist'::{A}{V1}{V2}{S} d = dist'++ʳ{A}{V1}{[ S ]}{V2} d

dist'-sym : ∀{A L1 L2} → (distinct'{A} L1 L2) → (distinct' L2 L1)
dist'-sym d = λ z x x₁ →  d z x₁ x

distinct'-union-left : ∀ {xs ys zs : List ℕ} →
  distinct' xs zs → distinct' ys zs → distinct' (xs ++ ys) zs
distinct'-union-left {xs} xs≠zs ys≠zs x x∈xs++ys x∈zs with ++⁻ xs x∈xs++ys
... | inj₁ x∈xs = xs≠zs x x∈xs x∈zs
... | inj₂ x∈ys = ys≠zs x x∈ys x∈zs

distinct-union-left : ∀ {xs ys zs} →
  distinct xs zs → distinct ys zs → distinct (xs U̬ ys) zs
distinct-union-left xs≠zs xs≠ys =
  distinct'-union-left ,′ distinct'-union-left ,′ distinct'-union-left #
    xs≠zs # xs≠ys

distinct-union-right : ∀ {xs ys zs} →
  distinct zs xs → distinct zs ys → distinct zs (xs U̬ ys)
distinct-union-right zs≠xs zs≠ys =
  distinct-sym (distinct-union-left (distinct-sym zs≠xs) (distinct-sym zs≠ys))

⊆¹-respect-distinct'-left : ∀{xs ys zs} → xs ⊆¹ ys → distinct' ys zs → distinct' xs zs
⊆¹-respect-distinct'-left xs⊆ys ys≠zs x x∈xs x∈zs = ys≠zs x (xs⊆ys x x∈xs) x∈zs

⊆-respect-distinct-left : ∀{xs³ ys³ zs³} → xs³ ⊆ ys³ → distinct ys³ zs³ → distinct xs³ zs³
⊆-respect-distinct-left {xs³} {ys³} {zs³} xs³⊆ys³ ys³≠zs³ =
  ⊆¹-respect-distinct'-left ,′ ⊆¹-respect-distinct'-left ,′ ⊆¹-respect-distinct'-left #
    xs³⊆ys³ # ys³≠zs³

⊆¹-respect-distinct'-right : ∀{xs ys zs} → xs ⊆¹ ys → distinct' zs ys → distinct' zs xs
⊆¹-respect-distinct'-right xs⊆ys zs≠ys =
  distinct'-sym (⊆¹-respect-distinct'-left xs⊆ys (distinct'-sym zs≠ys))

⊆-respect-distinct-right : ∀{xs³ ys³ zs³} → xs³ ⊆ ys³ → distinct zs³ ys³ → distinct zs³ xs³
⊆-respect-distinct-right {xs³} {ys³} {zs³} xs³⊆ys³ zs³≠ys³ =
  distinct-sym (⊆-respect-distinct-left xs³⊆ys³ (distinct-sym zs³≠ys³))

distinct'-dec : (xs ys : List ℕ) -> Dec (∃ λ z -> z ∈ xs × z ∈ ys)
distinct'-dec [] ys = no λ { (z , () , z∈ys) }
distinct'-dec (x ∷ xs) ys with ListAny.any (\ x' -> x Data.Nat.≟ x') ys
distinct'-dec (x ∷ xs) ys | yes p = yes (x , here refl , p)
distinct'-dec (x ∷ xs) ys | no ¬p with distinct'-dec xs ys
distinct'-dec (x ∷ xs) ys | no ¬p | yes (z , z∈xs , x∈ys) = yes (z , there z∈xs , x∈ys)
distinct'-dec (x ∷ xs) ys | no ¬p₁ | no ¬p =
  no (\ { (.x , here refl , z∈ys) → ¬p₁ z∈ys ;
          (z , there z∈xs , z∈ys) → ¬p (z , z∈xs , z∈ys) } )

distinct-dec : (xs ys : List ℕ × List ℕ × List ℕ) ->
  Dec ((∃ λ S → (S ∈ proj₁ xs) × (S ∈ proj₁ ys)) ⊎
       (∃ λ s → (s ∈ proj₁ (proj₂ xs)) × (s ∈ proj₁ (proj₂ ys))) ⊎
       (∃ λ x → (x ∈ proj₂ (proj₂ xs)) × (x ∈ proj₂ (proj₂ ys))))
distinct-dec (S1 , s1 , x1) (S2 , s2 , x2) with distinct'-dec S1 S2
distinct-dec (S1 , s1 , x1) (S2 , s2 , x2) | yes S1S2 = yes (inj₁ S1S2)
distinct-dec (S1 , s1 , x1) (S2 , s2 , x2) | no ¬S1S2 with distinct'-dec s1 s2
distinct-dec (S1 , s1 , x1) (S2 , s2 , x2) | no ¬S1S2 | yes s1s2 =
  yes (inj₂ (inj₁ s1s2))
distinct-dec (S1 , s1 , x1) (S2 , s2 , x2) | no ¬S1S2 | no ¬s1s2 with distinct'-dec x1 x2
distinct-dec (S1 , s1 , x1) (S2 , s2 , x2) | no ¬S1S2 | no ¬s1s2 | yes x1x2 =
  yes (inj₂ (inj₂ x1x2))
distinct-dec (S1 , s1 , x1) (S2 , s2 , x2) | no ¬S1S2 | no ¬s1s2 | no ¬x1x2 =
  no (λ { (inj₁ x) → ¬S1S2 x ; (inj₂ (inj₁ x)) → ¬s1s2 x ; (inj₂ (inj₂ y)) → ¬x1x2 y })

distinct-not-distinct-dec : ∀ {xs ys} -> distinct xs ys ->
      ((∃ λ S → (S ∈ proj₁ xs) × (S ∈ proj₁ ys)) ⊎
       (∃ λ s → (s ∈ proj₁ (proj₂ xs)) × (s ∈ proj₁ (proj₂ ys))) ⊎
       (∃ λ x → (x ∈ proj₂ (proj₂ xs)) × (x ∈ proj₂ (proj₂ ys))))
      -> ⊥
distinct-not-distinct-dec {xs} {ys} DXY (inj₁ (NDXYS , NDXYs , NDXYx)) = (proj₁ DXY) NDXYS  NDXYs  NDXYx
distinct-not-distinct-dec {xs} {ys} DXY (inj₂ (inj₁ (NDXYS , NDXYs , NDXYx))) = (proj₁ (proj₂ DXY)) NDXYS  NDXYs  NDXYx
distinct-not-distinct-dec {xs} {ys} DXY (inj₂ (inj₂ (NDXYS , NDXYs , NDXYx))) = (proj₂ (proj₂ DXY)) NDXYS  NDXYs  NDXYx

distinct-dec-is-distinct : ∀ {xs ys} ->
      (((∃ λ S → (S ∈ proj₁ xs) × (S ∈ proj₁ ys)) ⊎
        (∃ λ s → (s ∈ proj₁ (proj₂ xs)) × (s ∈ proj₁ (proj₂ ys))) ⊎
        (∃ λ x → (x ∈ proj₂ (proj₂ xs)) × (x ∈ proj₂ (proj₂ ys))))
        -> ⊥) -> distinct xs ys
distinct-dec-is-distinct {xs} {ys} FAIL =
  ((λ z z∈xs z∈ys → FAIL (inj₁ (z , z∈xs , z∈ys))) ,
   (λ z z∈xs z∈ys → FAIL (inj₂ (inj₁ (z , z∈xs , z∈ys)))) ,
   (λ z z∈xs z∈ys → FAIL (inj₂ (inj₂ (z , z∈xs , z∈ys)))))

case_return_of_ : ∀ {a b} {A : Set a} (x : A) (B : A → Set b) → (∀ x → B x) → B x
case x return B of f = f x

case_of_ : ∀ {a b} {A : Set a} {B : Set b} → A → (A → B) → B
case x of f = f x

typeof : ∀{𝕝}{A : Set 𝕝} → A → Set 𝕝
typeof{_}{A} _ = A

fst : ∀{l} {A B C : Set l} → A × B × C → A
fst = proj₁

snd : ∀{l} {A B C : Set l} → A × B × C → B
snd = proj₁ ∘ proj₂

thd : ∀{l} {A B C : Set l} → A × B × C → C
thd = proj₂ ∘ proj₂

∈:: : ∀{A} {x y : A} → x ∈ (y ∷ []) → x ≡ y
∈:: (here px) = px
∈:: (there ())

n∉map-suc-n-+ : ∀ n xs  → ¬ (n ∈ map (suc n +_) xs)
n∉map-suc-n-+ n [] ()
n∉map-suc-n-+ n (x ∷ xs) (here n≡suc⟨n+x⟩) with cong (_∸ n) n≡suc⟨n+x⟩
... | n∸n≡suc⟨n+x⟩∸n rewrite n∸n≡0 n | +-comm n x | m+n∸n≡m (suc x) n with n∸n≡suc⟨n+x⟩∸n
... | ()
n∉map-suc-n-+ n (x ∷ xs) (there n∈map-suc-n-+) = n∉map-suc-n-+ n xs n∈map-suc-n-+

map-+-swap-suc : ∀ n xs →
  map (_+_ n) (map suc xs) ≡ map suc (map (_+_ n) xs)
map-+-swap-suc n xs
  rewrite sym (map-compose {g = _+_ n} {f = suc}      xs)
        |      map-cong (λ m → +-comm n (suc m))      xs
        |      map-cong (λ m → cong suc (+-comm m n)) xs
        |      map-compose {g = suc}   {f = _+_ n}    xs
  = refl

map-+-compose-suc : ∀ n xs →
  map (_+_ n) (map suc xs) ≡ map (_+_ (suc n)) xs
map-+-compose-suc n xs
  rewrite map-+-swap-suc n xs
        | sym (map-compose {g = suc} {f = _+_ n} xs)
  = refl

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties, related to reflexive transitive closures, that rely on
-- the K rule
------------------------------------------------------------------------

{-# OPTIONS --with-K --safe #-}

module
  Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties.WithK
  where

open import Function
open import Relation.Binary
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------
-- Equality

module _ {i t} {I : Set i} {T : Rel I t} {i j k} {x y : T i j} {xs ys}
  where

  ◅-injectiveˡ : (Star T i k ∋ x ◅ xs) ≡ y ◅ ys → x ≡ y
  ◅-injectiveˡ refl = refl

  ◅-injectiveʳ : (Star T i k ∋ x ◅ xs) ≡ y ◅ ys → xs ≡ ys
  ◅-injectiveʳ refl = refl


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

module PointedTypes where

open import Agda.Prim
open import Data.Unit
open import Data.Bool
open import Data.Nat hiding (_⊔_)
open import Data.Sum
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality

------------------------------------------------------------------------------
-- Pointed types

-- We need pointed types because paths are ultimately between points. A path
-- between false and 0 for example would be expressed as a path between
-- (pt false) and (pt 0) which expand to •[ Bool , false ] and •[ ℕ , 0 ]

-- First we define a pointed set as a carrier with a distinguished point

record Set• (ℓ : Level) : Set (lsuc ℓ) where
  constructor •[_,_]
  field
    ∣_∣ : Set ℓ
    • : ∣_∣

open Set• public

⊤• : Set• lzero
⊤• = •[ ⊤ , tt ]

_⊎•₁_ : {ℓ ℓ' : Level} → (A• : Set• ℓ) → (B• : Set• ℓ') → Set• (ℓ ⊔ ℓ')
A• ⊎•₁ B• = •[ ∣ A• ∣ ⊎ ∣ B• ∣ , inj₁ (• A•) ]

_⊎•₂_ : {ℓ ℓ' : Level} → (A• : Set• ℓ) → (B• : Set• ℓ') → Set• (ℓ ⊔ ℓ')
A• ⊎•₂ B• = •[ ∣ A• ∣ ⊎ ∣ B• ∣ , inj₂ (• B•) ]

_×•_ : {ℓ ℓ' : Level} → (A• : Set• ℓ) → (B• : Set• ℓ') → Set• (ℓ ⊔ ℓ')
A• ×• B• = •[ ∣ A• ∣ × ∣ B• ∣ , (• A• , • B•) ]

test0 : Set• lzero
test0 = •[ ℕ , 3 ]

test1 : Set• (lsuc lzero)
test1 = •[ Set , ℕ ]

test2 : {ℓ ℓ' : Level} {A : Set ℓ} {B : Set ℓ'} {a : A} → Set• (ℓ ⊔ ℓ')
test2 {ℓ} {ℓ'} {A} {B} {a} = •[ A ⊎ B , inj₁ a ]

test3 : ∀ {ℓ} → Set• (lsuc (lsuc ℓ))
test3 {ℓ} = •[ Set (lsuc ℓ) , Set ℓ ]

test4 : Set• lzero
test4 = •[ (Bool → Bool) , not ]

-- Now we focus on the points and move the carriers to the background

pt : {ℓ : Level} {A : Set ℓ} → (a : A) → Set• ℓ
pt {ℓ} {A} a = •[ A , a ]

test5 : Set• lzero
test5 = pt 3

test6 : Set• (lsuc lzero)
test6 = pt ℕ

test7 : {ℓ : Level} → Set• (lsuc (lsuc ℓ))
test7 {ℓ} = pt (Set ℓ)

-- See:
-- http://homotopytypetheory.org/2012/11/21/on-heterogeneous-equality/

beta : {ℓ : Level} {A : Set ℓ} {a : A} → • •[ A , a ] ≡ a
beta {ℓ} {A} {a} = refl

eta : {ℓ : Level} → (A• : Set• ℓ) → •[ ∣ A• ∣ , • A• ] ≡ A•
eta {ℓ} A• = refl

------------------------------------------------------------------------------
-- Functions between pointed types; our focus is on how the functions affect
-- the basepoint. We don't care what the functions do on the rest of the type.

record _→•_ {ℓ ℓ' : Level} (A• : Set• ℓ) (B• : Set• ℓ') : Set (ℓ ⊔ ℓ') where
  field
    fun   : ∣ A• ∣ → ∣ B• ∣
    resp• : fun (• A•) ≡ • B•

open _→•_ public

id• : {ℓ : Level} {A• : Set• ℓ} → (A• →• A•)
id• = record { fun = id ; resp• = refl }

f1 : pt 2 →• pt 4
f1 = record { fun = suc ∘ suc ; resp• = refl }

f2 : pt 2 →• pt 4
f2 = record { fun = λ x → 2 * x ; resp• = refl }

-- composition of functions between pointed types
_⊚_ : {ℓ₁ ℓ₂ ℓ₃ : Level} {A• : Set• ℓ₁} {B• : Set• ℓ₂} {C• : Set• ℓ₃} →
      (B• →• C•) → (A• →• B•) → (A• →• C•)
h ⊚ g = record {
          fun   = fun h ∘ fun g ;
          resp• = trans (cong (fun h) (resp• g)) (resp• h)
        }

f3 : pt 4 →• pt 2
f3 = record { fun = pred ∘ pred ; resp• = refl }

f1∘f3 : pt 4 →• pt 4
f1∘f3 = f1 ⊚ f3

-- two pointed functions are ∼ if they agree on the basepoints; we DON'T CARE
-- what they do on the rest of the type.

_∼•_ : {ℓ ℓ' : Level} {A• : Set• ℓ} {B• : Set• ℓ'} →
       (f• g• : A• →• B•) → Set ℓ'
_∼•_ {ℓ} {ℓ'} {A•} {B•} f• g• = fun f• (• A•) ≡ fun g• (• A•)

f1∼f2 : f1 ∼• f2
f1∼f2 = refl

f1∘f3∼id : f1∘f3 ∼• id•
f1∘f3∼id = refl

-- quasi-inverses

record qinv• {ℓ ℓ'} {A• : Set• ℓ} {B• : Set• ℓ'} (f• : A• →• B•) :
  Set (ℓ ⊔ ℓ') where
  constructor mkqinv•
  field
    g• : B• →• A•
    α• : (f• ⊚ g•) ∼• id•
    β• : (g• ⊚ f•) ∼• id•

idqinv• : ∀ {ℓ} → {A• : Set• ℓ} → qinv• {ℓ} {ℓ} {A•} {A•} id•
idqinv• = record { g• = id• ; α• = refl ; β• = refl }

f1qinv : qinv• f1
f1qinv = record { g• = f3 ; α• = refl ; β• = refl }

-- equivalences

record isequiv• {ℓ ℓ'} {A• : Set• ℓ} {B• : Set• ℓ'} (f• : A• →• B•) :
  Set (ℓ ⊔ ℓ') where
  constructor mkisequiv•
  field
    g• : B• →• A•
    α• : (f• ⊚ g•) ∼• id•
    h• : B• →• A•
    β• : (h• ⊚ f•) ∼• id•

equiv•₁ : ∀ {ℓ ℓ'} {A• : Set• ℓ} {B• : Set• ℓ'} {f• : A• →• B•} →
          qinv• f• → isequiv• f•
equiv•₁ (mkqinv• qg qα qβ) = mkisequiv• qg qα qg qβ

f1equiv : isequiv• f1
f1equiv = equiv•₁ f1qinv

_≃•_ : ∀ {ℓ ℓ'} (A• : Set• ℓ) (B• : Set• ℓ') → Set (ℓ ⊔ ℓ')
A ≃• B = Σ (A →• B) isequiv•

idequiv• : ∀ {ℓ} {A• : Set• ℓ} → A• ≃• A•
idequiv• = ( id• , equiv•₁ idqinv•)

pt24equiv : pt 2 ≃• pt 4
pt24equiv = (f1 , f1equiv)

------------------------------------------------------------------------------
{-- old stuff which we might need again

idright : {A B : Set} {a : A} {b : B} {p : •[ A , a ] ⇛ •[ B , b ]} →
          (trans⇛ p (id⇛ {B} {b})) 2⇛ p
idright = 2Path id⇛ id⇛

idleft : {A B : Set} {a : A} {b : B} {p : •[ A , a ] ⇛ •[ B , b ]} →
         (trans⇛ (id⇛ {A} {a}) p) 2⇛ p
idleft = 2Path id⇛ id⇛

assoc  : {A B C D : Set} {a : A} {b : B} {c : C} {d : D}
         {p : •[ A , a ] ⇛ •[ B , b ]}
         {q : •[ B , b ] ⇛ •[ C , c ]}
         {r : •[ C , c ] ⇛ •[ D , d ]} →
         (trans⇛ p (trans⇛ q r)) 2⇛ (trans⇛ (trans⇛ p q) r)
assoc = 2Path id⇛ id⇛

bifunctorid⋆ : {A B : Set} {a : A} {b : B} →
  (times⇛ (id⇛ {A} {a}) (id⇛ {B} {b})) 2⇛ (id⇛ {A × B} {(a , b)})
bifunctorid⋆ = 2Path id⇛ id⇛

bifunctorid₊₁ : {A B : Set} {a : A} →
  (plus₁⇛ {A} {B} {A} {B} (id⇛ {A} {a})) 2⇛ (id⇛ {A ⊎ B} {inj₁ a})
bifunctorid₊₁ = 2Path id⇛ id⇛

bifunctorid₊₂ : {A B : Set} {b : B} →
  (plus₂⇛ {A} {B} {A} {B} (id⇛ {B} {b})) 2⇛ (id⇛ {A ⊎ B} {inj₂ b})
bifunctorid₊₂ = 2Path id⇛ id⇛

bifunctorC⋆ : {A B C D E F : Set}
              {a : A} {b : B} {c : C} {d : D} {e : E} {f : F}
              {p : •[ A , a ] ⇛ •[ B , b ]}
              {q : •[ B , b ] ⇛ •[ C , c ]}
              {r : •[ D , d ] ⇛ •[ E , e ]}
              {s : •[ E , e ] ⇛ •[ F , f ]} →
  (trans⇛ (times⇛ p r) (times⇛ q s)) 2⇛ (times⇛ (trans⇛ p q) (trans⇛ r s))
bifunctorC⋆ = 2Path id⇛ id⇛

bifunctorC₊₁₁ : {A B C D E F : Set}
                {a : A} {b : B} {c : C}
                {p : •[ A , a ] ⇛ •[ B , b ]}
                {q : •[ B , b ] ⇛ •[ C , c ]} →
  (trans⇛ (plus₁⇛ {A} {D} {B} {E} p) (plus₁⇛ {B} {E} {C} {F} q)) 2⇛
  (plus₁⇛ {A} {D} {C} {F} (trans⇛ p q))
bifunctorC₊₁₁ = 2Path id⇛ id⇛

bifunctorC₊₂₂ : {A B C D E F : Set}
                {d : D} {e : E} {f : F}
                {r : •[ D , d ] ⇛ •[ E , e ]}
                {s : •[ E , e ] ⇛ •[ F , f ]} →
  (trans⇛ (plus₂⇛ {A} {D} {B} {E} r) (plus₂⇛ {B} {E} {C} {F} s)) 2⇛
  (plus₂⇛ {A} {D} {C} {F} (trans⇛ r s))
bifunctorC₊₂₂ = 2Path id⇛ id⇛

triangle : {A B : Set} {a : A} {b : B} →
  (trans⇛ (assocr⋆⇛ {A} {⊤} {B} {a} {tt} {b}) (times⇛ id⇛ unite⋆⇛)) 2⇛
  (times⇛ (trans⇛ swap⋆⇛ unite⋆⇛) id⇛)
triangle = 2Path id⇛ id⇛

-- Now interpret a path (x ⇛ y) as a value of type (1/x , y)

Recip : {A : Set} → (x : • A) → Set₁
Recip {A} x = (x ⇛ x)

η : {A : Set} {x : • A} → ⊤ → Recip x × • A
η {A} {x} tt = (id⇛ x , x)

lower : {A : Set} {x : • A} → x ⇛ x -> ⊤
lower c = tt

-- The problem here is that we can't assert that y == x.
ε : {A : Set} {x : • A} → Recip x × • A → ⊤
ε {A} {x} (rx , y) = lower (id⇛ ( ↑ (fun (ap rx) (focus y)) )) -- makes insufficient sense

apr : {A B : Set} {x : • A} {y : • B} → (x ⇛ y) → Recip y → Recip x
apr {A} {B} {x} {y} q ry = trans⇛ q (trans⇛ ry (sym⇛ q))
  x
    ≡⟨ q ⟩
  y
    ≡⟨ ry ⟩
  y
    ≡⟨ sym⇛ q ⟩
  x ∎

ε : {A B : Set} {x : A} {y : B} → Recip x → Singleton y → x ⇛ y
ε rx (singleton y) = rx y

pathV : {A B : Set} {x : A} {y : B} → (x ⇛ y) → Recip x × Singleton y
pathV unite₊⇛ = {!!}
pathV uniti₊⇛ = {!!}
--  swap₁₊⇛ : {A B : Set} {x : A} → _⇛_ {A ⊎ B} {B ⊎ A} (inj₁ x) (inj₂ x)
pathV (swap₁₊⇛ {A} {B} {x}) = ((λ x' → {!!}) , singleton (inj₂ x))
pathV swap₂₊⇛ = {!!}
pathV assocl₁₊⇛ = {!!}
pathV assocl₂₁₊⇛ = {!!}
pathV assocl₂₂₊⇛ = {!!}
pathV assocr₁₁₊⇛ = {!!}
pathV assocr₁₂₊⇛ = {!!}
pathV assocr₂₊⇛ = {!!}
pathV unite⋆⇛ = {!!}
pathV uniti⋆⇛ = {!!}
pathV swap⋆⇛ = {!!}
pathV assocl⋆⇛ = {!!}
pathV assocr⋆⇛ = {!!}
pathV dist₁⇛ = {!!}
pathV dist₂⇛ = {!!}
pathV factor₁⇛ = {!!}
pathV factor₂⇛ = {!!}
pathV dist0⇛ = {!!}
pathV factor0⇛ = {!!}
pathV {A} {.A} {x} (id⇛ .x) = {!!}
pathV (sym⇛ p) = {!!}
pathV (trans⇛ p p₁) = {!!}
pathV (plus₁⇛ p) = {!!}
pathV (plus₂⇛ p) = {!!}
pathV (times⇛ p p₁) = {!!}

-- these are individual paths so to speak
-- should we represent a path like swap+ as a family explicitly:
-- swap+ : (x : A) -> x ⇛ swapF x
-- I guess we can: swap+ : (x : A) -> case x of inj1 -> swap1 x else swap2 x

If A={x0,x1,x2}, 1/A has three values:
(x0<-x0, x0<-x1, x0<-x2)
(x1<-x0, x1<-x1, x1<-x2)
(x2<-x0, x2<-x1, x2<-x2)
It is a fake choice between x0, x1, and x2 (some negative information). You base
yourself at x0 for example and enforce that any other value can be mapped to x0.
So think of a value of type 1/A as an uncertainty about which value of A we
have. It could be x0, x1, or x2 but at the end it makes no difference. There is
no choice.

You can manipulate a value of type 1/A (x0<-x0, x0<-x1, x0<-x2) by with a
path to some arbitrary path to b0 for example:

(b0<-x0<-x0, b0<-x0<-x1, b0<-x0<-x2)

eta_3 will give (x0<-x0, x0<-x1, x0<-x2, x0) for example but any other
combination is equivalent.

epsilon_3 will take (x0<-x0, x0<-x1, x0<-x2) and one actual xi which is now
certain; we can resolve our previous uncertainty by following the path from
xi to x0 thus eliminating the fake choice we seemed to have.

Explain connection to negative information.

Knowing head or tails is 1 bits. Giving you a choice between heads and tails
and then cooking this so that heads=tails takes away your choice.

-- transp⇛ : {A B : Set} {x y : • A} →
-- (f : A → B) → x ⇛ y → ↑ (f (focus x)) ⇛ ↑ (f (focus y))

-- Morphism of pointed space: contains a path!
record _⟶_ {A B : Set} (pA : • A) (pB : • B) : Set₁ where
  field
    fun : A → B
    eq : ↑ (fun (focus pA)) ⇛ pB

open _⟶_

_○_ : {A B C : Set} {pA : • A} {pB : • B} {pC : • C} → pA ⟶ pB → pB ⟶ pC → pA ⟶ pC
f ○ g = record { fun = λ x → (fun g) ((fun f) x) ; eq = trans⇛ (transp⇛ (fun g) (eq f)) (eq g)}

mutual

  ap : {A B : Set} {x : • A} {y : • B} → x ⇛ y → x ⟶ y
  ap {y = y} unite₊⇛ = record { fun = λ { (inj₁ ())
                                        ; (inj₂ x) → x } ; eq = id⇛ y }
  ap uniti₊⇛ (singleton x) = singleton (inj₂ x)
  ap (swap₁₊⇛ {A} {B} {x}) (singleton .(inj₁ x)) = singleton (inj₂ x)
  ap (swap₂₊⇛ {A} {B} {y}) (singleton .(inj₂ y)) = singleton (inj₁ y)
  ap (assocl₁₊⇛ {A} {B} {C} {x}) (singleton .(inj₁ x)) =
    singleton (inj₁ (inj₁ x))
  ap (assocl₂₁₊⇛ {A} {B} {C} {y}) (singleton .(inj₂ (inj₁ y))) =
    singleton (inj₁ (inj₂ y))
  ap (assocl₂₂₊⇛ {A} {B} {C} {z}) (singleton .(inj₂ (inj₂ z))) =
    singleton (inj₂ z)
  ap (assocr₁₁₊⇛ {A} {B} {C} {x}) (singleton .(inj₁ (inj₁ x))) =
    singleton (inj₁ x)
  ap (assocr₁₂₊⇛ {A} {B} {C} {y}) (singleton .(inj₁ (inj₂ y))) =
    singleton (inj₂ (inj₁ y))
  ap (assocr₂₊⇛ {A} {B} {C} {z}) (singleton .(inj₂ z)) =
    singleton (inj₂ (inj₂ z))
  ap {.(⊤ × A)} {A} {.(tt , x)} {x} unite⋆⇛ (singleton .(tt , x)) =
    singleton x
  ap uniti⋆⇛ (singleton x) = singleton (tt , x)
  ap (swap⋆⇛ {A} {B} {x} {y}) (singleton .(x , y)) = singleton (y , x)
  ap (assocl⋆⇛ {A} {B} {C} {x} {y} {z}) (singleton .(x , (y , z))) =
    singleton ((x , y) , z)
  ap (assocr⋆⇛ {A} {B} {C} {x} {y} {z}) (singleton .((x , y) , z)) =
    singleton (x , (y , z))
  ap (dist₁⇛ {A} {B} {C} {x} {z}) (singleton .(inj₁ x , z)) =
    singleton (inj₁ (x , z))
  ap (dist₂⇛ {A} {B} {C} {y} {z}) (singleton .(inj₂ y , z)) =
    singleton (inj₂ (y , z))
  ap (factor₁⇛ {A} {B} {C} {x} {z}) (singleton .(inj₁ (x , z))) =
    singleton (inj₁ x , z)
  ap (factor₂⇛ {A} {B} {C} {y} {z}) (singleton .(inj₂ (y , z))) =
    singleton (inj₂ y , z)
  ap {.(⊥ × A)} {.⊥} {.(• , x)} {•} (dist0⇛ {A} {.•} {x}) (singleton .(• , x)) =
    singleton •
  ap factor0⇛ (singleton ())
  ap {x = x} (id⇛ .x) = record { fun = λ x → x; eq = id⇛ x }
  ap (sym⇛ c) = apI c
  ap (trans⇛ c₁ c₂) = (ap c₁) ○ (ap c₂)
  ap (transp⇛ f a) = record { fun = λ x → x; eq = transp⇛ f a }

  ap (plus₁⇛ {A} {B} {C} {D} {x} {z} c) (singleton .(inj₁ x))
    with ap c (singleton x)
  ... | singleton .z = singleton (inj₁ z)
  ap (plus₂⇛ {A} {B} {C} {D} {y} {w} c) (singleton .(inj₂ y))
    with ap c (singleton y)
  ... | singleton .w = singleton (inj₂ w)
  ap (times⇛ {A} {B} {C} {D} {x} {y} {z} {w} c₁ c₂) (singleton .(x , y))
    with ap c₁ (singleton x) | ap c₂ (singleton y)
  ... | singleton .z | singleton .w = singleton (z , w)

  apI : {A B : Set} {x : • A} {y : • B} → x ⇛ y → y ⟶ x
  apI {y = y} unite₊⇛ = record { fun = inj₂; eq = id⇛ (↑ (inj₂ (focus y))) }

 apI {A} {.(⊥ ⊎ A)} {x} uniti₊⇛ (singleton .(inj₂ x)) = singleton x
  apI (swap₁₊⇛ {A} {B} {x}) (singleton .(inj₂ x)) = singleton (inj₁ x)
  apI (swap₂₊⇛ {A} {B} {y}) (singleton .(inj₁ y)) = singleton (inj₂ y)
  apI (assocl₁₊⇛ {A} {B} {C} {x}) (singleton .(inj₁ (inj₁ x))) =
    singleton (inj₁ x)
  apI (assocl₂₁₊⇛ {A} {B} {C} {y}) (singleton .(inj₁ (inj₂ y))) =
    singleton (inj₂ (inj₁ y))
  apI (assocl₂₂₊⇛ {A} {B} {C} {z}) (singleton .(inj₂ z)) =
    singleton (inj₂ (inj₂ z))
  apI (assocr₁₁₊⇛ {A} {B} {C} {x}) (singleton .(inj₁ x)) =
    singleton (inj₁ (inj₁ x))
  apI (assocr₁₂₊⇛ {A} {B} {C} {y}) (singleton .(inj₂ (inj₁ y))) =
    singleton (inj₁ (inj₂ y))
  apI (assocr₂₊⇛ {A} {B} {C} {z}) (singleton .(inj₂ (inj₂ z))) =
    singleton (inj₂ z)
  apI unite⋆⇛ (singleton x) = singleton (tt , x)
  apI {A} {.(⊤ × A)} {x} uniti⋆⇛ (singleton .(tt , x)) = singleton x
  apI (swap⋆⇛ {A} {B} {x} {y}) (singleton .(y , x)) = singleton (x , y)
  apI (assocl⋆⇛ {A} {B} {C} {x} {y} {z}) (singleton .((x , y) , z)) =
    singleton (x , (y , z))
  apI (assocr⋆⇛ {A} {B} {C} {x} {y} {z}) (singleton .(x , (y , z))) =
    singleton ((x , y) , z)
  apI (dist₁⇛ {A} {B} {C} {x} {z}) (singleton .(inj₁ (x , z))) =
    singleton (inj₁ x , z)
  apI (dist₂⇛ {A} {B} {C} {y} {z}) (singleton .(inj₂ (y , z))) =
    singleton (inj₂ y , z)
  apI (factor₁⇛ {A} {B} {C} {x} {z}) (singleton .(inj₁ x , z)) =
    singleton (inj₁ (x , z))
  apI (factor₂⇛ {A} {B} {C} {y} {z}) (singleton .(inj₂ y , z)) =
    singleton (inj₂ (y , z))
  apI dist0⇛ (singleton ())
  apI {.⊥} {.(⊥ × A)} {•} (factor0⇛ {A} {.•} {x}) (singleton .(• , x)) =
    singleton •

  apI {x = x} (id⇛ .x) = record { fun = λ x → x; eq = id⇛ x }
  apI (sym⇛ c) = ap c
  apI (trans⇛ c₁ c₂) = (apI c₂) ○ (apI c₁)
  apI (transp⇛ f a) = record { fun = λ x → x; eq = transp⇛ f (sym⇛ a) }

  apI (plus₁⇛ {A} {B} {C} {D} {x} {z} c) (singleton .(inj₁ z))
    with apI c (singleton z)
  ... | singleton .x = singleton (inj₁ x)
  apI (plus₂⇛ {A} {B} {C} {D} {y} {w} c) (singleton .(inj₂ w))
    with apI c (singleton w)
  ... | singleton .y = singleton (inj₂ y)
  apI (times⇛ {A} {B} {C} {D} {x} {y} {z} {w} c₁ c₂) (singleton .(z , w))
    with apI c₁ (singleton z) | apI c₂ (singleton w)
  ... | singleton .x | singleton .y = singleton (x , y)

--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------------
-- Properties for the equality on Conat
------------------------------------------------------------------------------

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

module FOTC.Data.Conat.Equality.PropertiesATP where

open import FOTC.Base
open import FOTC.Data.Conat
open import FOTC.Data.Conat.Equality.Type

------------------------------------------------------------------------------
-- Because a greatest post-fixed point is a fixed-point, then the
-- relation _≈N_ is also a pre-fixed point of the functional ≈-F, i.e.
--
-- ≈-F _≈_ ≤ _≈_ (see FOTC.Data.Conat.Equality.Type).

-- See Issue https://github.com/asr/apia/issues/81 .
≈-inR : D → D → Set
≈-inR m n = m ≡ zero ∧ n ≡ zero
            ∨ (∃[ m' ] ∃[ n' ] m ≡ succ₁ m' ∧ n ≡ succ₁ n' ∧ m' ≈ n')
{-# ATP definition ≈-inR #-}

≈-in :
  ∀ {m n} →
  m ≡ zero ∧ n ≡ zero
    ∨ (∃[ m' ] ∃[ n' ] m ≡ succ₁ m' ∧ n ≡ succ₁ n' ∧ m' ≈ n') →
  m ≈ n
≈-in h = ≈-coind ≈-inR h' h
  where
  postulate
    h' : ∀ {m n} → ≈-inR m n →
         m ≡ zero ∧ n ≡ zero
           ∨ (∃[ m' ] ∃[ n' ] m ≡ succ₁ m' ∧ n ≡ succ₁ n' ∧ ≈-inR m' n')
  {-# ATP prove h' #-}

-- See Issue https://github.com/asr/apia/issues/81 .
≈-reflR : D → D → Set
≈-reflR a b = Conat a ∧ Conat b ∧ a ≡ b
{-# ATP definition ≈-reflR #-}

≈-refl : ∀ {n} → Conat n → n ≈ n
≈-refl {n} Cn = ≈-coind ≈-reflR h₁ h₂
  where
  postulate
    h₁ : ∀ {a b} → ≈-reflR a b →
         a ≡ zero ∧ b ≡ zero
           ∨ (∃[ a' ] ∃[ b' ] a ≡ succ₁ a' ∧ b ≡ succ₁ b' ∧ ≈-reflR a' b')
  {-# ATP prove h₁ #-}

  postulate h₂ : ≈-reflR n n
  {-# ATP prove h₂ #-}

  postulate ≡→≈ : ∀ {m n} → Conat m → Conat n → m ≡ n → m ≈ n
  {-# ATP prove ≡→≈ ≈-refl #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-

Product of structures S and T: X ↦ S X × T X

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Relational.Product where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.RelationalStructure
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Univalence
open import Cubical.Data.Sigma
open import Cubical.HITs.SetQuotients

open import Cubical.Structures.Product

private
  variable
    ℓ ℓ₁ ℓ₁' ℓ₂ ℓ₂' : Level

-- Structured relations

preservesSetsProduct : {S₁ : Type ℓ → Type ℓ₁} {S₂ : Type ℓ → Type ℓ₂}
  → preservesSets S₁ → preservesSets S₂ → preservesSets (ProductStructure S₁ S₂)
preservesSetsProduct p₁ p₂ setX = isSet× (p₁ setX) (p₂ setX)

ProductRelStr :
  {S₁ : Type ℓ → Type ℓ₁} (ρ₁ : StrRel S₁ ℓ₁')
  {S₂ : Type ℓ → Type ℓ₂} (ρ₂ : StrRel S₂ ℓ₂')
  → StrRel (ProductStructure S₁ S₂) (ℓ-max ℓ₁' ℓ₂')
ProductRelStr ρ₁ ρ₂ R (s₁ , s₂) (t₁ , t₂) =
  ρ₁ R s₁ t₁ × ρ₂ R s₂ t₂

open SuitableStrRel

productSuitableRel :
  {S₁ : Type ℓ → Type ℓ₁} {ρ₁ : StrRel S₁ ℓ₁'}
  {S₂ : Type ℓ → Type ℓ₂} {ρ₂ : StrRel S₂ ℓ₂'}
  → SuitableStrRel S₁ ρ₁ → SuitableStrRel S₂ ρ₂
  → SuitableStrRel (ProductStructure S₁ S₂) (ProductRelStr ρ₁ ρ₂)
productSuitableRel θ₁ θ₂ .quo (X , s₁ , s₂) R (r₁ , r₂) .fst .fst =
  θ₁ .quo (X , s₁) R r₁ .fst .fst , θ₂ .quo (X , s₂) R r₂ .fst .fst
productSuitableRel θ₁ θ₂ .quo (X , s₁ , s₂) R (r₁ , r₂) .fst .snd =
  θ₁ .quo (X , s₁) R r₁ .fst .snd , θ₂ .quo (X , s₂) R r₂ .fst .snd
productSuitableRel θ₁ θ₂ .quo (X , s₁ , s₂) R (r₁ , r₂) .snd ((q₁ , q₂) , (c₁ , c₂)) i .fst =
  θ₁ .quo (X , s₁) R r₁ .snd (q₁ , c₁) i .fst , θ₂ .quo (X , s₂) R r₂ .snd (q₂ , c₂) i .fst
productSuitableRel θ₁ θ₂ .quo (X , s₁ , s₂) R (r₁ , r₂) .snd ((q₁ , q₂) , (c₁ , c₂)) i .snd =
  θ₁ .quo (X , s₁) R r₁ .snd (q₁ , c₁) i .snd , θ₂ .quo (X , s₂) R r₂ .snd (q₂ , c₂) i .snd
productSuitableRel θ₁ θ₂ .symmetric R (r₁ , r₂) =
  θ₁ .symmetric R r₁ , θ₂ .symmetric R r₂
productSuitableRel θ₁ θ₂ .transitive R R' (r₁ , r₂) (r₁' , r₂') =
  θ₁ .transitive R R' r₁ r₁' , θ₂ .transitive R R' r₂ r₂'
productSuitableRel θ₁ θ₂ .prop propR (s₁ , s₂) (t₁ , t₂) =
  isProp× (θ₁ .prop propR s₁ t₁) (θ₂ .prop propR s₂ t₂)

productRelMatchesEquiv :
  {S₁ : Type ℓ → Type ℓ₁} (ρ₁ : StrRel S₁ ℓ₁') {ι₁ : StrEquiv S₁ ℓ₁'}
  {S₂ : Type ℓ → Type ℓ₂} (ρ₂ : StrRel S₂ ℓ₂') {ι₂ : StrEquiv S₂ ℓ₂'}
  → StrRelMatchesEquiv ρ₁ ι₁ → StrRelMatchesEquiv ρ₂ ι₂
  → StrRelMatchesEquiv (ProductRelStr ρ₁ ρ₂) (ProductEquivStr ι₁ ι₂)
productRelMatchesEquiv ρ₁ ρ₂ μ₁ μ₂ A B e =
  Σ-cong-equiv (μ₁ _ _ e) (λ _ → μ₂ _ _ e)

max_stars_repo_name: RobertHarper/cubical

max_issues_repo_name: RobertHarper/cubical

max_forks_repo_name: RobertHarper/cubical


text:
module Issue498b where

record ⊤ : Set where
  constructor tt

postulate
  U   : Set → Set
  pr  : ∀ {A} → A → U A
  _*_ : ∀ {A B} → U A → (A → U B) → U B

module M (I : Set)(J : I → Set)(K : (i : I)(j : J i) → Set) where

  data D (P : I → Set) : I → Set where
    r : ∀ {i} → P i → D P i
    d : (i : I)(j : J i)
        (f : K i j → D P i) → D P i

  module N (e : (i : I)(j : J i) → U (K i j)) where

    du : ∀ {P}{i : I} → D P i → U (P i)
    du (r p)     = pr p
    du (d i j f) = e i j * λ k → du (f k)

data j : ⊤ → Set where
  cj : j _

k : (i : ⊤)(j : j i) → Set
k _ j = ⊤

e : (i : ⊤)(j : j i) → U (k i j)
e tt cj = pr tt

open M ⊤ j k
open N e

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Andreas, 2016-10-08 issue #2243
-- This is a test case reported at #708 by pepijnkokke

open import Common.Bool using (Bool; true; false)
open import Common.Reflection using (QName)

example : QName → Bool
example (quote Bool) = true
example (quote Bool) = false
example _            = false


text:
module Data.Unsigned where

open import Data.Bit using
  (Bit
  ; b0
  ; b1
  ; Bits-num
  ; Overflowing
  ; _overflow:_
  ; result
  ; carry
  ; WithCarry
  ; _with-carry:_
  ; toBool
  ; tryToFinₙ
  ; !ₙ
  ) renaming
  ( _+_ to bit+
  ; _-_ to bit-
  ; ! to bit!
  ; _&_ to bit&
  ; _~|_ to bit|
  ; _^_ to bit^
  ; _>>_ to bit>>
  ; _<<_ to bit<<
  )
open import Data.Unit using (⊤)
open import Data.Nat using (ℕ)
open import Data.Vec using (Vec; head; replicate)
open import Data.Nat.Literal using (Number)
open import Data.Maybe using (just; nothing)

infixl 8 _-_ _+_
infixl 7 _<<_ _>>_
infixl 6 _&_
infixl 5 _^_
infixl 4 _~|_

record Unsigned (n : ℕ) : Set where
  constructor mk-uint
  field
    bits : Vec Bit n

open Unsigned public

instance
  Unsigned-num : {m : ℕ} → Number (Unsigned m)
  Unsigned-num {m} .Number.Constraint = Number.Constraint (Bits-num {m})
  Unsigned-num {m} .Number.fromNat n ⦃ p ⦄ = mk-uint (mk-bits p) where
    mk-bits : Number.Constraint (Bits-num {m}) n → Vec Bit m
    mk-bits p = Number.fromNat Bits-num n ⦃ p ⦄

_+_ : {n : ℕ} → Unsigned n → Unsigned n → Overflowing (Unsigned n)
p + q = mk-uint (result sum) overflow: toBool (head (carry sum)) where
  sum = bit+ (bits p) (bits q)

_-_ : {n : ℕ} → Unsigned n → Unsigned n → Overflowing (Unsigned n)
p - q = mk-uint (result sub) overflow: toBool (bit! (head (carry sub))) where
  sub = bit- (bits p) (bits q)

rotr : {n : ℕ} → Unsigned n → Unsigned n → WithCarry (Unsigned n) (Unsigned n)
rotr {n} (mk-uint ps) (mk-uint qs) = new-result with-carry: new-carry where
  shifted : WithCarry (Vec Bit n) (Vec Bit n)
  shifted with tryToFinₙ qs
  ...        | just i  = bit>> ps i
  ...        | nothing = replicate b0 with-carry: ps
  new-result : Unsigned n
  new-result = mk-uint (result shifted)
  new-carry : Unsigned n
  new-carry = mk-uint (carry shifted)

rotl : {n : ℕ} → Unsigned n → Unsigned n → WithCarry (Unsigned n) (Unsigned n)
rotl {n} (mk-uint ps) (mk-uint qs) = new-result with-carry: new-carry where
  shifted : WithCarry (Vec Bit n) (Vec Bit n)
  shifted with tryToFinₙ qs
  ...        | just i  = bit<< ps i
  ...        | nothing = replicate b0 with-carry: ps
  new-result : Unsigned n
  new-result = mk-uint (result shifted)
  new-carry : Unsigned n
  new-carry = mk-uint (carry shifted)

_>>_ : {n : ℕ} → Unsigned n → Unsigned n → Unsigned n
ps >> qs = result (rotr ps qs)

_<<_ : {n : ℕ} → Unsigned n → Unsigned n → Unsigned n
ps << qs = result (rotl ps qs)

! : {n : ℕ} → Unsigned n → Unsigned n
! (mk-uint ps) = mk-uint (!ₙ ps)

_&_ : {n : ℕ} → Unsigned n → Unsigned n → Unsigned n
(mk-uint ps) & (mk-uint qs) = mk-uint (bit& ps qs)

_~|_ : {n : ℕ} → Unsigned n → Unsigned n → Unsigned n
(mk-uint ps) ~| (mk-uint qs) = mk-uint (bit| ps qs)

_^_ : {n : ℕ} → Unsigned n → Unsigned n → Unsigned n
(mk-uint ps) ^ (mk-uint qs) = mk-uint (bit^ ps qs)

max_stars_repo_name: brunoczim/Celeste

max_issues_repo_name: brunoczim/Celeste

max_forks_repo_name: brunoczim/Celeste


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

module Definition.Conversion.Universe where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.RedSteps
open import Definition.Conversion
open import Definition.Conversion.Reduction
open import Definition.Conversion.Lift

import Tools.PropositionalEquality as PE

-- Algorithmic equality of terms in WHNF of type U are equal as types.
univConv↓ : ∀ {A B Γ}
          → Γ ⊢ A [conv↓] B ∷ U
          → Γ ⊢ A [conv↓] B
univConv↓ (ne-ins t u () x)
univConv↓ (univ x x₁ x₂) = x₂

-- Algorithmic equality of terms of type U are equal as types.
univConv↑ : ∀ {A B Γ}
      → Γ ⊢ A [conv↑] B ∷ U
      → Γ ⊢ A [conv↑] B
univConv↑ ([↑]ₜ B₁ t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u)
      rewrite PE.sym (whnfRed* D Uₙ) =
  reductionConv↑ (univ* d) (univ* d′) (liftConv (univConv↓ t<>u))


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

{- Here, we derive our main theorem: there is a type in the n-th universe
   that is not an n-type, implying the n-th universe is not n-truncated.
   The n-th universe restricted to n-types is hence a 'strict' n-type.
   For this, we first derive local-global looping in a modular way.

   A technical point worth noting is that Agda does not implement
   cumulative universes. Since that means the crucial steps in our
   transformations (where we pass between universes uning univalence)
   can not be expressed using equality without resorting to explicit lifting,
   we decide to explicitely uses equivalences (and pointed equivalences,
   respectively) instead where possible.
   As a drawback, we have to use lemmata showing preservation of
   (pointed) equivalences of various (pointed) type constructions,
   a parametricity property derived for free
   from univalence-induced equalities. -}
module HHHUU-ComplicatedTypes where

open import lib.Basics hiding (_⊔_)
open import lib.Equivalences2
open import lib.NType2
open import lib.types.Bool
open import lib.types.Nat hiding (_+_)
open import lib.types.Paths
open import lib.types.Sigma
open import lib.types.Pi
open import lib.types.TLevel

open import Preliminaries
open import Pointed
open import UniverseOfNTypes

-- The argument that (Type lzero) is not a set is standard.
-- We omit it and the argument that (Type (S lzero)) is not a 1-Type:
-- they are both special cases of the general theorem we prove.
-- The general theorem is formalised in this file.

--Definition 7.3.1
-- We have fibered notions of the loop space contruction and n-truncatedness.
module _ {i} {X : Type• i} {j} where
  {- Note that the definition of the family of path types differs slightly from
     that in the thesis, which would correspond to transport P p x == x.
     We use dependent paths since this follows the design of the HoTT
     community's Agda library. There is no actual difference;
     both types are equivalent. -}
  Ω̃ : Fam• X j → Fam• (Ω X) j
  Ω̃ (P , x) = ((λ p → x == x [ P ↓ p ]) , idp)

  fam-has-level : ℕ₋₂ → Fam• X j → Type (i ⊔ j)
  fam-has-level n Q = (a : base X) → has-level n (fst Q a)

{- == Pointed dependent sums ==
   Pointed families as defined above enable us to introduce a Σ-connective
   for pointed types. Because of the abstract nature of some of our lemmata, we
   give Σ• in its uncurried form and first define the type of its parameter. -}
Σ•-param : ∀ i j → Type (lsucc (i ⊔ j))
Σ•-param i j = Σ (Type• i) (λ X → Fam• X j)

module _ {i j} where
  Ω-Σ•-param : Σ•-param i j → Σ•-param i j
  Ω-Σ•-param (X , W) = (Ω X , Ω̃ W)

  -- Definition 7.3.2
  Σ• : Σ•-param i j → Type• (i ⊔ j)
  Σ• (X , Q) = (Σ (base X) (fst Q) , (pt X , snd Q))

  -- Lemma 7.3.3
  {- Commutativity of pointed dependent sums and the loop space construction
     will become an important technical tool, enabling us to work at a more
     abstract level later on. -}
  Ω-Σ•-comm : (R : Σ•-param i j) → Ω (Σ• R) ≃• Σ• (Ω-Σ•-param R)
  Ω-Σ•-comm _ = (=Σ-eqv _ _ , idp) ⁻¹•

{- Pointed dependent products.
   This is not quite the equivalent of Π for pointed types: the domain parameter
   is just an ordinary non-pointed type. However, to enable our goal of
   abstractly working with pointed types, defining this notion is useful. -}
Π•-param : ∀ i j → Type (lsucc (i ⊔ j))
Π•-param i j = Σ (Type i) (λ A → A → Type• j)

module _ {i j} where
  Ω-Π•-param : Π•-param i j → Π•-param i j
  Ω-Π•-param (A , F) = (A , Ω ∘ F)

  -- Definition 7.3.4
  Π• : Π•-param i j → Type• (i ⊔ j)
  Π• (A , Y) = (Π A (base ∘ Y) , pt ∘ Y)

  -- Lemma 7.3.5
  {- Pointed dependent products and loop space construction on
     its codomain parameter commute as well. -}
  Ω-Π•-comm : (R : Π•-param i j) → Ω (Π• R) ≃• Π• (Ω-Π•-param R)
  Ω-Π•-comm _ = (app=-equiv , idp)

  Ω^-Π•-comm : (C : Type i) (F : C → Type• j) (n : ℕ)
             → (Ω ^ n) (Π• (C , F)) ≃• Π• (C , ((Ω ^ n) ∘ F))
  Ω^-Π•-comm C F 0     = ide• _
  Ω^-Π•-comm C F (S n) = Ω^-Π•-comm C _ n ∘e• equiv-Ω^ n (Ω-Π•-comm _)

equiv-Π• : ∀ {i₀ i₁ j₀ j₁} {R₀ : Π•-param i₀ j₀} {R₁ : Π•-param i₁ j₁}
           → Σ (fst R₀ ≃ fst R₁) (λ u → ∀ a → snd R₀ (<– u a) ≃• snd R₁ a)
           → Π• R₀ ≃• Π• R₁
equiv-Π• (u , v) = (equiv-Π u (fst ∘ v) , λ= (snd ∘ v))

-- Lemma 7.4.1
-- In an n-th loop space, we can forget components of truncation level n.
forget-Ω^-Σ•₂ : ∀ {i j} {X : Type• i} (Q : Fam• X j) (n : ℕ)
                → fam-has-level (n -2) Q → (Ω ^ n) (Σ• (X , Q)) ≃• (Ω ^ n) X
forget-Ω^-Σ•₂     {X = X} Q    O  h = (Σ₂-contr h , idp)
forget-Ω^-Σ•₂ {i} {X = X} Q (S n) h =
  (Ω ^ (S n)) (Σ• (X , Q))  ≃•⟨ equiv-Ω^ n (Ω-Σ•-comm _) ⟩
  (Ω ^ n) (Σ• (Ω X , Ω̃ Q))  ≃•⟨ forget-Ω^-Σ•₂ {i} _ n (λ _ → ↓-level h) ⟩
  (Ω ^ (S n)) X             ≃•∎

-- Lemma 7.4.2
{- Our Local-global looping principle.
   We would like to state this principle in the form of
     Ωⁿ⁺¹ (Type i , A) == ∀• a → Ωⁿ (A , a)
   for n ≥ 1. Unfortunately, the two sides have different universe
   levels since (Type i , A) lives in Type• (suc i) instead of Type• i.
   Morally, this is outbalanced by the extra Ω on the left-hand side,
   which might help explain on an intuitive level why
   the n-th universe ends up being not an n-type.

   The reason why the univalence principle (A ≡ B) ≃ (A ≃ B)
   cannot be written as (A ≡ B) ≡ (A ≃ B) is precisely the same. -}
module _ {i} {A : Type i} where
  -- The degenerate pre-base case carries around a propositional component.
  Ω-Type : Ω (Type i , A) ≃• Σ• (Π• (A , λ a → (A , a))
                               , (is-equiv , idf-is-equiv _))
  Ω-Type =
      Ω (Type i , A)
    ≃•⟨ ide• _ ⟩
      ((A == A) , idp)
    ≃•⟨ ua-equiv• ⁻¹• ⟩
      ((A ≃ A) , ide _)
    ≃•⟨ ide• _ ⟩
      ((Σ (A → A) is-equiv) , (idf _ , idf-is-equiv _))
    ≃•⟨ ide• _ ⟩
      Σ• (Π• (A , λ a → (A , a)) , (is-equiv , idf-is-equiv _))
    ≃•∎

  -- The base case.
  Ω²-Type : (Ω ^ 2) (Type i , A) ≃• Π• (A , λ a → Ω (A , a))
  Ω²-Type =
      (Ω ^ 2) (Type i , A)
    ≃•⟨ equiv-Ω Ω-Type ⟩
      Ω (Σ• (Π• (A , λ a → (A , a)) , (is-equiv , idf-is-equiv _)))
    ≃•⟨ forget-Ω^-Σ•₂ {i} _ 1 (is-equiv-is-prop ∘ _) ⟩
      Ω (Π• (A , λ a → (A , a)))
    ≃•⟨ Ω-Π•-comm _ ⟩
      Π• (A , λ a → Ω (A , a))
    ≃•∎

  -- The general case follows by permuting Ω and Π• repeatedly.
  Ω^-Type : (n : ℕ) → (Ω ^ (n + 2)) (Type i , A)
                   ≃• Π• (A , λ a → (Ω ^ (n + 1)) (A , a))
  Ω^-Type n = Ω^-Π•-comm _ _ n ∘e• equiv-Ω^ n Ω²-Type

-- Lemma 7.4.3 is taken from the library
-- lib.NType2._-Type-level_

{- The pointed family P (see thesis).
   It takes an n-type A and returns the space of (n+1)-loops
   with basepoint A in U_n^n (the n-th universe restricted to n-types).
   This crucial restriction to n-types implies it is just a set. -}
module _ (n : ℕ) (A : ⟨ n ⟩ -Type ｢ n ｣) where

  -- Definition of P and
  -- Corollary 7.4.4
  P : ⟨0⟩ -Type• ｢ n + 1 ｣
  P = Ω^-≤' (n + 1) q where
    q : ⟨ n + 1 ⟩ -Type• ｢ n + 1 ｣
    q = –> Σ-comm-snd (((⟨ n ⟩ -Type-≤ ｢ n ｣) , A))

  -- Forgetting about the truncation level, we may present P as follows:
  Q : Type• ｢ n + 1 ｣
  Q = (Ω ^ (n + 1)) (Type ｢ n ｣ , fst A)

  P-is-Q : fst P ≃• Q
  P-is-Q = equiv-Ω^ n (forget-Ω^-Σ•₂ _ 1 (λ _ → has-level-is-prop))

-- Definition of the type 'Loop' and
-- Lemma 7.4.5
{- The type 'Loop' of (images of) n-loops in U_(n-1)^(n-1) is
   just the dependent sum over P except for the special case n ≡ 0,
   where we take U_(-1)^(-1) (and hence Loop) to be the booleans.

   The boilerplate with raise-≤T is just to verify that Loop n is
   n-truncated.
   The bulk of the rest of this module consists of showing
   the n-th universe is not n-truncated at basepoint Loop n,
   i.e. that Q n (Loop n) is not contractible.

   Warning: The indexing of Loop starts at -1 in the thesis,
            but we use natural numbers here (starting at 0),
            thus everything is shifted by one. -}
Loop : (n : ℕ) → ⟨ n ⟩ -Type ｢ n ｣
Loop 0     = (Bool , Bool-is-set)
Loop (S n) = Σ-≤ (⟨ n ⟩ -Type-≤ ｢ n ｣) (λ A →
               raise-≤T {n = ⟨ n + 1 ⟩} (≤T-+2+-l ⟨0⟩ (-2≤T _))
                                        (fst (<– Σ-comm-snd (P n A))))

-- Lemma 7.4.6, preparations
-- The base case is given in Section 7.2 or the thesis.
-- It is done as usual (there is a non-trivial automorphism on booleans).

-- Let us go slowly.
module negation where

  -- Negation.
  ~ : Bool → Bool
  ~ = λ {true → false; false → true}

  -- Negation is an equivalence.
  e : Bool ≃ Bool
  e = equiv ~ ~ inv inv where
    inv = λ {true → idp; false → idp}

  base-case : ¬ (is-contr• (Q 0 (Loop 0)))
  base-case c = Bool-false≠true false-is-true where
    -- Negation being equal to the identity yields a contradiction.
    false-is-true =
      false             =⟨ ! (coe-β e true) ⟩
      coe (ua e) true   =⟨ ap (λ p → coe p true) (! (c (ua e))) ⟩
      coe idp true      =⟨ idp ⟩
      true              ∎

-- Let us now turn towards the successor case.
module _ (m : ℕ) where

  -- We expand the type we are later going to assume contractible.
  Q-L-is-… =
      Q (m + 1) (Loop (m + 1))
    ≃•⟨ ide• _ ⟩
      (Ω ^ (m + 2)) (_ , ⟦ Loop (m + 1) ⟧)
    ≃•⟨ (Ω^-Type m) ⟩
      Π• (_ , λ {(A , q) → Ω ^ (m + 1) $ (⟦ Loop (m + 1) ⟧ , (A , q))})
    ≃•⟨ ide• _ ⟩
      Π• (_ , λ {(A , q) → Ω ^ (m + 1) $ Σ• ((_ , A) , (base ∘ fst ∘ P m , q))})
    ≃•∎

  -- What we really want is to arrive at contractibility of E (m ≥ 1)...
  E = Π• (⟦ Loop (m + 1) ⟧ , λ {(A , q) → Ω ^ (m + 1) $ ((⟨ m ⟩ -Type ｢ m ｣) , A)})

  -- ...or at least show that the following element f of E is trivial (m ≡ 0).
  f : base E
  f (_ , q) = q

-- We want to use our assumption of contractibility of Q (n + 1) (Loop (n + 1))
-- to show that f is trivial, i.e. constant with value the basepoint.
f-is-trivial : (m : ℕ) → is-contr• (Q (m + 1) (Loop (m + 1))) → f m == pt (E m)

-- m ≡ 0
f-is-trivial 0 c = ap (λ f' → fst ∘ f')
                      (! (–> (equiv-is-contr• …-is-E') c f')) where
  -- This is almost E, except for the additional component
  -- specifying that the first component p should commute with q.
  E' = Π• (_ , λ {(A , q) → (Σ (A == A) (λ p → q == q [ (λ x → x == x) ↓ p ])
                                       , (idp , idp))})

  -- This "almost" E comes from Q 1 (Loop 1), hence can be shown contractible.
  …-is-E' : Q 1 (Loop 1) ≃• E'
  …-is-E' = equiv-Π• (ide _ , Ω-Σ•-comm ∘ _) ∘e• Q-L-is-… 0

  -- Fortunately, f can be 'extended' to an element f' of E',
  -- and triviality of f' implies triviality of f.
  f' = λ {(_ , q) → (q , ↓-idf=idf-in (∙=∙' q q))}

-- m ≥ 1: We can show Q (k + 2) (Loop (k + 2)) ≃ E (k + 1),
--        thus E is contractible, hence f trivial.
f-is-trivial (S k) c = ! (–> (equiv-is-contr• (…-is-E ∘e• Q-L-is-… (k + 1)))
                             c
                             (f (k + 1))) where
  …-is-E : _ ≃• E (k + 1)
  …-is-E = equiv-Π• (ide _ , equiv-Ω^ k ∘ (λ {(A , q) → forget-Ω^-Σ•₂
             {｢ k + 2 ｣} (base ∘ fst ∘ P (k + 1) , q) 2
             (snd ∘ P (k + 1))}))

-- Lemma 7.4.6, part 1
-- Our main lemma: like in the thesis, but in negative form.
-- This is sufficient to prove our results, and easier to formalise.
main : (n : ℕ) → ¬ (is-contr• (Q n (Loop n)))
main 0       = negation.base-case
main (S m) c = main m step where
  {- We know Q (m + 1) (Loop (m + 1)) is contractible,
     use that to show that the above f is trivial,
     deduce f (Loop m , p) ≡ p is trivial for all p in P m (Loop m),
     which implies P m (Loop m) is contractible.
     But this is just another form of Q m (Loop m),
     so the conclusion follows by induction hypothesis. -}
  step : is-contr• (Q m (Loop m))
  step = –> (equiv-is-contr• (P-is-Q m (Loop m)))
            (λ q → app= (! (f-is-trivial m c)) (Loop m , q))

-- Lemma 7.4.6, part 2
-- Alternate form of the main lemma
main' : (n : ℕ) → ¬ (is-contr• ((Ω ^ (n + 1)) ((⟨ n ⟩ -Type ｢ n ｣) , Loop n )))
main' n = main n ∘ –> (equiv-is-contr• (P-is-Q n (Loop n)))

-- Small helper thingy
helpy : ∀ {i} {n : ℕ} {X : Type• i}
        → has-level• (n -1) X → is-contr• ((Ω ^ n) X)
helpy {n = n} {X} = <– contr•-equiv-prop
                  ∘ trunc-many n
                  ∘ transport (λ k → has-level• (k -2) X)
                              (+-comm 1 n)

-- Main theorems now fall out as corollaries.
module _ (n : ℕ) where
  {- Recall that L n is n-truncated.
     We also know it is not (n-1)-truncated, it is thus a 'strict' n-type. -}
  Loop-is-not-trunc : ¬ (has-level (n -1) ⟦ Loop n ⟧)
  Loop-is-not-trunc = main n ∘ helpy ∘ (λ t → universe-=-level t t)

  -- Theorem 7.4.7
  -- The n-th universe is not n-truncated.
  Type-is-not-trunc : ¬ (has-level ⟨ n ⟩ (Type ｢ n ｣))
  Type-is-not-trunc = main n ∘ helpy

  -- Theorem 7.4.8
  -- MAIN RESULT:
  --  The n-th universe restricted to n-types is a 'strict' (n+1)-type.
  --  We do not repeat that it is (n+1)-truncated; this is formalised above
  --  (7.4.3). Instead, we only show that it is not an n-type.
  Type-≤-is-not-trunc : ¬ (has-level ⟨ n ⟩ (⟨ n ⟩ -Type ｢ n ｣))
  Type-≤-is-not-trunc = main' n ∘ helpy

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module Issue478c where

record Ko (Q : Set) : Set₁ where
 field
  T : Set

foo : (Q : Set)(ko : Ko Q) → Ko.T ko
foo Q ko = Set

-- We should make sure not to destroy printing
-- outside the record module. Type should be
-- printed as it's given: Ko.T ko

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module NoSuchPrimitiveFunction where

postulate
  X : Set

primitive
  fooBar : X


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Change Structures.
--
-- This module defines the notion of change structures,
-- as well as change structures for groups, functions and lists.
--
-- This module corresponds to Section 2 of the PLDI paper.
------------------------------------------------------------------------

module Base.Change.Algebra where

open import Relation.Binary.PropositionalEquality
open import Level

-- Change Algebras
-- ===============
--
-- In the paper, change algebras are called "change structures"
-- and they are described in Section 2.1. We follow the design of
-- the Agda standard library and define change algebras as two
-- records, so Definition 2.1 from the PLDI paper maps to the
-- records IsChangeAlgebra and ChangeAlgebra.
--
-- A value of type (IsChangeAlgebra Change update diff) proves that
-- Change, update and diff together form a change algebra.
--
-- A value of type (ChangeAlgebra Carrier) contains the necessary
-- ingredients to create a change algebra for a carrier set.
--
-- In the paper, Carrier is called V (Def. 2.1a),
-- Change is called Δ (Def. 2.1b),
-- update is written as infix ⊕ (Def. 2.1c),
-- diff is written as infix ⊝ (Def. 2.1d),
-- and update-diff is specified in Def. 2.1e.

record IsChangeAlgebra
    {c}
    {Carrier : Set c}
    (Change : Carrier → Set c)
    (update : (v : Carrier) (dv : Change v) → Carrier)
    (diff : (u v : Carrier) → Change v)
    (nil : (u : Carrier) → Change u) : Set (c) where
  field
    update-diff : ∀ u v → update v (diff u v) ≡ u
    -- This corresponds to Lemma 2.3 from the paper.
    update-nil : ∀ v → update v (nil v) ≡ v

  -- abbreviations
  before : ∀ {v} → Change v → Carrier
  before {v} _ = v

  after : ∀ {v} → Change v → Carrier
  after {v} dv = update v dv

record ChangeAlgebra {c}
    (Carrier : Set c) : Set (suc c) where
  field
    Change : Carrier → Set c
    update : (v : Carrier) (dv : Change v) → Carrier
    diff : (u v : Carrier) → Change v

    -- This generalizes Def. 2.2. from the paper.
    nil : (u : Carrier) → Change u

    isChangeAlgebra : IsChangeAlgebra Change update diff nil

  infixl 6 update diff

  open IsChangeAlgebra isChangeAlgebra public

-- The following open ... public statement lets us use infix ⊞
-- and ⊟ for update and diff. In the paper, we use infix ⊕ and
-- ⊝.

open ChangeAlgebra {{...}} public
  using
    ( update-diff
    ; update-nil
    ; nil
    ; before
    ; after
    )
  renaming
    ( Change to Δ
    ; update to _⊞_
    ; diff to _⊟_
    )

-- Families of Change Algebras
-- ===========================
--
-- This is some Agda machinery to allow subscripting change
-- algebra operations to avoid ambiguity. In the paper,
-- we simply write (in the paragraph after Def. 2.1):
--
--   We overload operators ∆, ⊝ and ⊕ to refer to the
--   corresponding operations of different change structures; we
--   will subscript these symbols when needed to prevent
--   ambiguity.
--
-- The following definitions implement this idea formally.

record ChangeAlgebraFamily {a p} {A : Set a} (P : A → Set p): Set (suc p ⊔ a) where
  constructor
    family
  field
    change-algebra : ∀ x → ChangeAlgebra (P x)

  module _ x where
    open ChangeAlgebra (change-algebra x) public

module Family = ChangeAlgebraFamily {{...}}

open Family public
  using
    (
    )
  renaming
    ( Change to Δ₍_₎
    ; nil to nil₍_₎
    ; update-diff to update-diff₍_₎
    ; update-nil to update-nil₍_₎
    ; change-algebra to change-algebra₍_₎
    ; before to before₍_₎
    ; after to after₍_₎
    )

-- XXX not clear this is ever used
instance
  change-algebra-family-inst = change-algebra₍_₎

infixl 6 update′ diff′

update′ = Family.update
syntax update′ x v dv = v ⊞₍ x ₎ dv

diff′ = Family.diff
syntax diff′ x u v = u ⊟₍ x ₎ v

-- Derivatives
-- ===========
--
-- This corresponds to Def. 2.4 in the paper.

RawChange : ∀ {a b} {A : Set a} {B : Set b} →
  {{CA : ChangeAlgebra A}} →
  {{CB : ChangeAlgebra B}} →
  (f : A → B) →
  Set (a ⊔ b)
RawChange f = ∀ a (da : Δ a) → Δ (f a)

IsDerivative : ∀ {a b} {A : Set a} {B : Set b} →
  {{CA : ChangeAlgebra A}} →
  {{CB : ChangeAlgebra B}} →
  (f : A → B) →
  (df : RawChange f) →
  Set (a ⊔ b)
IsDerivative f df = ∀ a da → f a ⊞ df a da ≡ f (a ⊞ da)

-- This is a variant of IsDerivative for change algebra families.
RawChange₍_,_₎ : ∀ {a b p q} {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} →
  {{CP : ChangeAlgebraFamily P}} →
  {{CQ : ChangeAlgebraFamily Q}} →
  (x : A) →
  (y : B) →
  (f : P x → Q y) → Set (p ⊔ q)
RawChange₍ x , y ₎ f = ∀ px (dpx : Δ₍ x ₎ px) → Δ₍ y ₎ (f px)

IsDerivative₍_,_₎ : ∀ {a b p q} {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} →
  {{CP : ChangeAlgebraFamily P}} →
  {{CQ : ChangeAlgebraFamily Q}} →
  (x : A) →
  (y : B) →
  (f : P x → Q y) →
  (df : RawChange₍_,_₎ x y f) →
  Set (p ⊔ q)
IsDerivative₍_,_₎ {P = P} {{CP}} {{CQ}} x y f df = IsDerivative {{change-algebra₍ _ ₎}} {{change-algebra₍ _ ₎}} f df where
  CPx = change-algebra₍_₎ {{CP}} x
  CQy = change-algebra₍_₎ {{CQ}} y

-- Lemma 2.5 appears in Base.Change.Equivalence.

-- Abelian Groups Induce Change Algebras
-- =====================================
--
-- In the paper, as the first example for change structures after
-- Def. 2.1, we mention that "each abelian group ... induces a
-- change structure". This is the formalization of this result.
--
-- The module GroupChanges below takes a proof that A forms an
-- abelian group and provides a changeAlgebra for A. The proof of
-- Def 2.1e is by equational reasoning using the group axioms, in
-- the definition of changeAlgebra.isChangeAlgebra.update-diff.

open import Algebra.Structures
open import Data.Product
open import Function

-- For non-abelian groups
module PlainGroupChanges
    {a} (A : Set a) {_⊕_} {ε} {_⁻¹}
    {{isGroup : IsGroup {A = A} _≡_ _⊕_ ε _⁻¹}}
  where
    open IsGroup isGroup
      hiding
        ( refl
        ; sym
        )
      renaming
        ( ∙-cong to _⟨⊕⟩_
        )

    open ≡-Reasoning

    _⊝_ : A → A → A
    v ⊝ u = (u ⁻¹) ⊕ v

    changeAlgebraGroup : ChangeAlgebra A
    changeAlgebraGroup = record
      { Change = const A
      ; update = _⊕_
      ; diff = _⊝_
      ; nil = const ε
      ; isChangeAlgebra = record
        { update-diff = λ u v →
            begin
              v ⊕ (u ⊝ v)
            ≡⟨⟩
               v ⊕ ((v ⁻¹) ⊕ u)
            ≡⟨  sym (assoc _ _ _) ⟩
               (v ⊕ (v ⁻¹)) ⊕ u
            ≡⟨ proj₂ inverse v ⟨⊕⟩ refl ⟩
               ε ⊕ u
            ≡⟨ proj₁ identity u ⟩
              u
            ∎
        ; update-nil = proj₂ identity
        }
      }

module GroupChanges
    {a} (A : Set a) {_⊕_} {ε} {_⁻¹}
    {{isAbelianGroup : IsAbelianGroup {A = A} _≡_ _⊕_ ε _⁻¹}}
  where
    open IsAbelianGroup isAbelianGroup
      hiding
        ( refl
        )
      renaming
        ( _-_ to _⊝_
        ; ∙-cong to _⟨⊕⟩_
        )

    open ≡-Reasoning

    changeAlgebraGroup : ChangeAlgebra A
    changeAlgebraGroup = record
      { Change = const A
      ; update = _⊕_
      ; diff = _⊝_
      ; nil = const ε
      ; isChangeAlgebra = record
        { update-diff = λ u v →
            begin
              v ⊕ (u ⊝ v)
            ≡⟨ comm _ _ ⟩
              (u ⊝ v ) ⊕ v
            ≡⟨⟩
              (u ⊕ (v ⁻¹)) ⊕ v
            ≡⟨ assoc _ _ _ ⟩
              u ⊕ ((v ⁻¹) ⊕ v)
            ≡⟨  refl ⟨⊕⟩ proj₁ inverse v  ⟩
              u ⊕ ε
            ≡⟨  proj₂ identity u ⟩
              u
            ∎
        ; update-nil = proj₂ identity
        }
      }

-- Function Changes
-- ================
--
-- This is one of our most important results: Change structures
-- can be lifted to function spaces. We formalize this as a module
-- FunctionChanges that takes the change algebras for A and B as
-- arguments, and provides a changeAlgebra for (A → B). The proofs
-- are by equational reasoning using 2.1e for A and B.

module FunctionChanges
    {a} {b} (A : Set a) (B : Set b) {{CA : ChangeAlgebra A}} {{CB : ChangeAlgebra B}}
  where
    -- This corresponds to Definition 2.6 in the paper.
    record FunctionChange (f : A → B) : Set (a ⊔ b) where
      field
        -- Definition 2.6a
        apply : RawChange f

        -- Definition 2.6b.
        -- (for some reason, the version in the paper has the arguments of ≡
        -- flipped. Since ≡ is symmetric, this doesn't matter).
        correct : (a : A) (da : Δ a) →
          f (a ⊞ da) ⊞ apply (a ⊞ da) (nil (a ⊞ da)) ≡ f a ⊞ apply a da

    open FunctionChange public
    open ≡-Reasoning
    open import Postulate.Extensionality

    funDiff : (g f : A → B) → FunctionChange f
    funDiff = λ g f → record
        { apply = λ a da → g (a ⊞ da) ⊟ f a
          -- the proof of correct is the first half of what we
          -- have to prove for Theorem 2.7.
        ; correct = λ a da →
          begin
            f (a ⊞ da) ⊞ (g (a ⊞ da ⊞ nil (a ⊞ da)) ⊟ f (a ⊞ da))
          ≡⟨ cong (λ □ → f (a ⊞ da) ⊞ (g □ ⊟ f (a ⊞ da)))
               (update-nil (a ⊞ da)) ⟩
            f (a ⊞ da) ⊞ (g (a ⊞ da) ⊟ f (a ⊞ da))
          ≡⟨ update-diff (g (a ⊞ da)) (f (a ⊞ da)) ⟩
            g (a ⊞ da)
          ≡⟨ sym (update-diff (g (a ⊞ da)) (f a)) ⟩
            f a ⊞ (g (a ⊞ da) ⊟ f a)
          ∎
        }

    funUpdate : ∀ (f : A → B) (df : FunctionChange f) → A → B
    funUpdate = λ f df a → f a ⊞ apply df a (nil a)

    funNil : (f : A → B) → FunctionChange f
    funNil = λ f → funDiff f f
    private
      -- Realizer for funNil
      funNil-realizer : (f : A → B) → RawChange f
      funNil-realizer f = λ a da → f (a ⊞ da) ⊟ f a
      -- Note that it cannot use nil (f a), that would not be a correct function change!
      funNil-correct : ∀ f a da → funNil-realizer f a da ≡ apply (funNil f) a da
      funNil-correct f a da = refl

    mutual
      -- I have to write the type of funUpdateDiff without using changeAlgebra,
      -- so I just use the underlying implementations.
      funUpdateDiff : ∀ u v → funUpdate v (funDiff u v) ≡ u
      instance
        changeAlgebraFun : ChangeAlgebra (A → B)

      changeAlgebraFun = record
        { Change = FunctionChange
          -- in the paper, update and diff below are in Def. 2.7
        ; update = funUpdate
        ; diff = funDiff
        ; nil = funNil
        ; isChangeAlgebra = record
            -- the proof of update-diff is the second half of what
            -- we have to prove for Theorem 2.8.
          { update-diff = funUpdateDiff
          ; update-nil = λ v → funUpdateDiff v v
          }
        }
      -- XXX remove mutual recursion by inlining the algebra in here?
      funUpdateDiff = λ g f → ext (λ a →
        begin
          f a ⊞ (g (a ⊞ (nil a)) ⊟ f a)
        ≡⟨ cong (λ □ → f a ⊞ (g □ ⊟ f a)) (update-nil a) ⟩
          f a ⊞ (g a ⊟ f a)
        ≡⟨ update-diff (g a) (f a) ⟩
          g a
        ∎)

    -- This is Theorem 2.9 in the paper.
    incrementalization : ∀ (f : A → B) df a da →
      (f ⊞ df) (a ⊞ da) ≡ f a ⊞ apply df a da
    incrementalization f df a da = correct df a da

    -- This is Theorem 2.10 in the paper. However, the derivative of f is just
    -- the apply component of `nil f`, not the full `nil f`, which also includes
    -- a proof. This is not an issue in the paper, which is formulated in a
    -- proof-irrelevant metalanguage.
    nil-is-derivative : ∀ (f : A → B) →
      IsDerivative f (apply (nil f))
    nil-is-derivative f a da =
      begin
        f a ⊞ apply (nil f) a da
      ≡⟨ sym (incrementalization f (nil f) a da) ⟩
        (f ⊞ nil f) (a ⊞ da)
      ≡⟨ cong (λ □ → □ (a ⊞ da))
           (update-nil f) ⟩
        f (a ⊞ da)
      ∎

    -- Show that any derivative is a valid function change.

    -- In the paper, this is never actually stated. We just prove that nil
    -- changes are derivatives; the paper keeps talking about "the derivative",
    -- suggesting derivatives are unique. If derivatives were unique, we could
    -- say that the nil change is *the* derivative, hence the derivative is the
    -- nil change (hence also a change).
    --
    -- In fact, derivatives are only unique up to change equivalence and
    -- extensional equality; this is proven in Base.Change.Equivalence.derivative-unique.
    --
    Derivative-is-valid : ∀ {f : A → B} df (IsDerivative-f-df : IsDerivative f df) a da →
      f (a ⊞ da) ⊞ (df (a ⊞ da) (nil (a ⊞ da))) ≡ f a ⊞ df a da
    Derivative-is-valid {f} df IsDerivative-f-df a da rewrite IsDerivative-f-df (a ⊞ da) (nil (a ⊞ da)) | update-nil (a ⊞ da) = sym (IsDerivative-f-df a da)

    DerivativeAsChange : ∀ {f : A → B} {df} (IsDerivative-f-df : IsDerivative f df) → Δ f
    DerivativeAsChange {df = df} IsDerivative-f-df = record { apply = df ; correct = Derivative-is-valid df IsDerivative-f-df }
    -- In Equivalence.agda, derivative-is-nil-alternative then proves that a derivative is also a nil change.

-- Reexport a few members with A and B marked as implicit parameters. This
-- matters especially for changeAlgebra, since otherwise it can't be used for
-- instance search.
module _
    {a} {b} {A : Set a} {B : Set b} {{CA : ChangeAlgebra A}} {{CB : ChangeAlgebra B}}
  where
    open FunctionChanges A B {{CA}} {{CB}} public
      using
        ( changeAlgebraFun
        ; apply
        ; correct
        ; incrementalization
        ; DerivativeAsChange
        ; FunctionChange
        ; nil-is-derivative
        )

module BinaryFunctionChanges
    {a} {b} {c} (A : Set a) (B : Set b) (C : Set c) {{CA : ChangeAlgebra A}} {{CB : ChangeAlgebra B}} {{CC : ChangeAlgebra C}} where
    incrementalization-binary : ∀ (f : A → B → C) df a da b db →
      (f ⊞ df) (a ⊞ da) (b ⊞ db) ≡ f a b ⊞ apply (apply df a da) b db
    incrementalization-binary f df x dx y dy
      rewrite cong (λ □ → □ (y ⊞ dy)) (incrementalization f df x dx)
      = incrementalization (f x) (apply df x dx) y dy

-- List (== Environment) Changes
-- =============================
--
-- Here, we define a change structure on environments, given a
-- change structure on the values in the environments. In the
-- paper, we describe this in Definition 3.5. But note that this
-- Agda formalization uses de Bruijn indices instead of names, so
-- environments are just lists. Therefore, when we use Definition
-- 3.5 in the paper, in this formalization, we use the list-like
-- change structure defined here.

open import Data.List
open import Data.List.All

data All′ {a p q} {A : Set a}
    {P : A → Set p}
    (Q : {x : A} → P x → Set q)
  : {xs : List A} (pxs : All P xs) → Set (p ⊔ q ⊔ a) where
    []  : All′ Q []
    _∷_ : ∀ {x xs} {px : P x} {pxs : All P xs} (qx : Q px) (qxs : All′ Q pxs) → All′ Q (px ∷ pxs)

module ListChanges
    {a} {A : Set a} (P : A → Set) {{C : ChangeAlgebraFamily P}}
  where
    update-all : ∀ {xs} → (pxs : All P xs) → All′ Δ pxs  → All P xs
    update-all {[]} [] [] = []
    update-all {x ∷ xs} (px ∷ pxs) (dpx ∷ dpxs) = (px ⊞ dpx) ∷ update-all pxs dpxs

    diff-all : ∀ {xs} → (pxs′ pxs : All P xs) → All′ Δ pxs
    diff-all [] [] = []
    diff-all (px′ ∷ pxs′) (px ∷ pxs) = (px′ ⊟ px) ∷ diff-all pxs′ pxs

    update-diff-all : ∀ {xs} → (pxs′ pxs : All P xs) → update-all pxs (diff-all pxs′ pxs) ≡ pxs′
    update-diff-all [] [] = refl
    update-diff-all (px′ ∷ pxs′) (px ∷ pxs) = cong₂ _∷_ (update-diff px′ px) (update-diff-all pxs′ pxs)

    instance
      changeAlgebraListChanges : ChangeAlgebraFamily (All P)

    changeAlgebraListChanges = record
      { change-algebra = λ xs → record
        { Change = All′ Δ
        ; update = update-all
        ; diff = diff-all
        ; nil = λ xs → diff-all xs xs
        ; isChangeAlgebra = record
          { update-diff = update-diff-all
          ; update-nil = λ xs₁ → update-diff-all xs₁ xs₁
          }
        }
      }

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:
module Web.URI.Port.Primitive where

postulate Port? : Set
{-# COMPILED_TYPE Port? String #-}

postulate :80 : Port?
{-# COMPILED :80 ":80" #-}

postulate ε : Port?
{-# COMPILED ε "" #-}

max_stars_repo_name: agda/agda-web-uri

max_issues_repo_name: agda/agda-web-uri

max_forks_repo_name: agda/agda-web-uri