text:
------------------------------------------------------------------------
-- Paolo Capriotti's variant of higher lenses
------------------------------------------------------------------------

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

import Equality.Path as P

module Lens.Non-dependent.Higher.Capriotti
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J as B using (_↔_)
open import Equality.Path.Isomorphisms eq hiding (univ)
open import Equivalence equality-with-J as Eq using (_≃_)
open import Function-universe equality-with-J as F hiding (_∘_)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq
open import Preimage equality-with-J
open import Univalence-axiom equality-with-J

open import Lens.Non-dependent eq
import Lens.Non-dependent.Higher      eq as Higher
import Lens.Non-dependent.Traditional eq as Traditional

private
  variable
    a b : Level
    A B : Set a

------------------------------------------------------------------------
-- The lens type family

-- Higher lenses, as presented by Paolo Capriotti, who seems to have
-- been first to describe a notion of higher lens
-- (http://homotopytypetheory.org/2014/04/29/higher-lenses/).

Lens : Set a → Set b → Set (lsuc (a ⊔ b))
Lens {a = a} A B =
  ∃ λ (g : A → B) →
  ∃ λ (H : Pow a ∥ B ∥) →
    (g ⁻¹_) ≡ H ∘ ∣_∣

-- Some derived definitions.

module Lens {A : Set a} {B : Set b} (l : Lens A B) where

  -- A getter.

  get : A → B
  get = proj₁ l

  -- A predicate.

  H : Pow a ∥ B ∥
  H = proj₁ (proj₂ l)

  -- An equality.

  get⁻¹-≡ : (get ⁻¹_) ≡ H ∘ ∣_∣
  get⁻¹-≡ = proj₂ (proj₂ l)

  -- A setter.
  --
  -- This definition is based on Paolo Capriotti's.

  set : A → B → A
  set a b =                  $⟨ truncation-is-proposition ∣ get a ∣ ∣ b ∣ ⟩
    ∣ get a ∣ ≡ ∣ b ∣        ↝⟨ cong H ⟩
    H ∣ get a ∣ ≡ H ∣ b ∣    ↝⟨ subst (λ f → f (get a) ≡ f b) (sym get⁻¹-≡) ⟩
    get ⁻¹ get a ≡ get ⁻¹ b  ↝⟨ ≡⇒≃ ⟩
    get ⁻¹ get a ≃ get ⁻¹ b  ↝⟨ flip _≃_.to (a , refl _) ⟩
    get ⁻¹ b                 ↝⟨ proj₁ ⟩□
    A                        □

instance

  -- The lenses defined above have getters and setters.

  has-getter-and-setter :
    Has-getter-and-setter (Lens {a = a} {b = b})
  has-getter-and-setter = record
    { get = Lens.get
    ; set = Lens.set
    }

------------------------------------------------------------------------
-- Equality characterisation lemmas

-- An equality characterisation lemma.

equality-characterisation₁ :
  {l₁ l₂ : Lens A B} →

  let open Lens in

  (l₁ ≡ l₂)
    ≃
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     trans (sym (cong _⁻¹_ (⟨ext⟩ g)))
       (trans (get⁻¹-≡ l₁) (⟨ext⟩ (h ∘ ∣_∣))) ≡
     get⁻¹-≡ l₂)
equality-characterisation₁ {A = A} {B = B} {l₁ = l₁} {l₂ = l₂} =
  l₁ ≡ l₂                                                                ↝⟨ inverse $ Eq.≃-≡ $ Eq.↔⇒≃ Σ-assoc ⟩

  ((get l₁ , H l₁) , get⁻¹-≡ l₁) ≡ ((get l₂ , H l₂) , get⁻¹-≡ l₂)        ↔⟨ inverse B.Σ-≡,≡↔≡ ⟩

  (∃ λ (eq : (get l₁ , H l₁) ≡ (get l₂ , H l₂)) →
     subst (λ (g , H) → g ⁻¹_ ≡ H ∘ ∣_∣) eq (get⁻¹-≡ l₁) ≡ get⁻¹-≡ l₂)   ↝⟨ (Σ-cong-contra ≡×≡↔≡ λ _ → F.id) ⟩

  (∃ λ ((g , h) : get l₁ ≡ get l₂ × H l₁ ≡ H l₂) →
     subst (λ (g , H) → g ⁻¹_ ≡ H ∘ ∣_∣) (cong₂ _,_ g h) (get⁻¹-≡ l₁) ≡
     get⁻¹-≡ l₂)                                                         ↔⟨ inverse Σ-assoc ⟩

  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     subst (λ (g , H) → g ⁻¹_ ≡ H ∘ ∣_∣) (cong₂ _,_ g h) (get⁻¹-≡ l₁) ≡
     get⁻¹-≡ l₂)                                                         ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ≡⇒↝ _ $ cong (_≡ _) $
                                                                             lemma _ _) ⟩
  (∃ λ (g : get l₁ ≡ get l₂) →
   ∃ λ (h : H l₁ ≡ H l₂) →
     trans (sym (cong _⁻¹_ g)) (trans (get⁻¹-≡ l₁) (cong (_∘ ∣_∣) h)) ≡
     get⁻¹-≡ l₂)                                                         ↝⟨ (Σ-cong-contra (Eq.extensionality-isomorphism bad-ext) λ _ →
                                                                             Σ-cong-contra (Eq.extensionality-isomorphism bad-ext) λ _ →
                                                                             F.id) ⟩
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     trans (sym (cong _⁻¹_ (⟨ext⟩ g)))
       (trans (get⁻¹-≡ l₁) (cong (_∘ ∣_∣) (⟨ext⟩ h))) ≡
     get⁻¹-≡ l₂)                                                         ↝⟨ (∃-cong λ _ → ∃-cong λ _ → ≡⇒↝ _ $
                                                                             cong (λ eq → trans _ (trans _ eq) ≡ _) $
                                                                             cong-pre-∘-ext _) ⟩□
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     trans (sym (cong _⁻¹_ (⟨ext⟩ g)))
       (trans (get⁻¹-≡ l₁) (⟨ext⟩ (h ∘ ∣_∣))) ≡
     get⁻¹-≡ l₂)                                                         □
  where
  open Lens

  lemma : ∀ _ _ → _
  lemma g h =
    subst (λ (g , H) → g ⁻¹_ ≡ H ∘ ∣_∣) (cong₂ _,_ g h) (get⁻¹-≡ l₁)     ≡⟨ subst-in-terms-of-trans-and-cong ⟩

    trans (sym (cong (λ (g , _) → g ⁻¹_) (cong₂ _,_ g h)))
      (trans (get⁻¹-≡ l₁) (cong (λ (_ , H) → H ∘ ∣_∣) (cong₂ _,_ g h)))  ≡⟨ cong₂ (λ p q → trans (sym p) (trans (get⁻¹-≡ l₁) q))
                                                                              (trans (sym $ cong-∘ _ _ _) $
                                                                               cong (cong _⁻¹_) $ cong-proj₁-cong₂-, _ _)
                                                                              (trans (sym $ cong-∘ _ _ _) $
                                                                               cong (cong (_∘ ∣_∣)) $ cong-proj₂-cong₂-, _ _) ⟩∎
    trans (sym (cong _⁻¹_ g)) (trans (get⁻¹-≡ l₁) (cong (_∘ ∣_∣) h))     ∎

-- Another equality characterisation lemma.

equality-characterisation₂ :
  {A : Set a} {B : Set b} {l₁ l₂ : Lens A B}
  (univ : Univalence (a ⊔ b)) →

  let open Lens in

  (l₁ ≡ l₂)
    ≃
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≃ H l₂ b) →
     trans (sym (cong _⁻¹_ (⟨ext⟩ g)))
       (trans (get⁻¹-≡ l₁) (⟨ext⟩ (≃⇒≡ univ ∘ h ∘ ∣_∣))) ≡
     get⁻¹-≡ l₂)
equality-characterisation₂ {A = A} {B = B} {l₁ = l₁} {l₂ = l₂} univ =
  l₁ ≡ l₂                                                   ↝⟨ equality-characterisation₁ ⟩

  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≡ H l₂ b) →
     trans (sym (cong _⁻¹_ (⟨ext⟩ g)))
       (trans (get⁻¹-≡ l₁) (⟨ext⟩ (h ∘ ∣_∣))) ≡
     get⁻¹-≡ l₂)                                            ↝⟨ (∃-cong λ _ →
                                                                Σ-cong-contra (∀-cong ext λ _ → inverse $ ≡≃≃ univ) λ _ → F.id) ⟩□
  (∃ λ (g : ∀ a → get l₁ a ≡ get l₂ a) →
   ∃ λ (h : ∀ b → H l₁ b ≃ H l₂ b) →
     trans (sym (cong _⁻¹_ (⟨ext⟩ g)))
       (trans (get⁻¹-≡ l₁) (⟨ext⟩ (≃⇒≡ univ ∘ h ∘ ∣_∣))) ≡
     get⁻¹-≡ l₂)                                            □
  where
  open Lens

------------------------------------------------------------------------
-- Conversions between different kinds of lenses

-- The lenses defined above can be converted to the lenses defined in
-- Higher.

Lens→Higher-lens : Lens A B → Higher.Lens A B
Lens→Higher-lens {A = A} {B = B} (g , H , eq) = record
  { R = Σ ∥ B ∥ H

  ; equiv =
      A                                      ↔⟨ (inverse $ drop-⊤-right λ _ → _⇔_.to contractible⇔↔⊤ $
                                                 other-singleton-contractible _) ⟩
      (∃ λ (a : A) → ∃ λ (b : B) → g a ≡ b)  ↔⟨ ∃-comm ⟩
      (∃ λ (b : B) → ∃ λ (a : A) → g a ≡ b)  ↔⟨⟩
      (∃ λ (b : B) → g ⁻¹ b)                 ↝⟨ (∃-cong λ b → ≡⇒↝ _ $ cong (_$ b) eq) ⟩
      (∃ λ (b : B) → H ∣ b ∣)                ↝⟨ (Σ-cong (inverse ∥∥×≃) λ _ → ≡⇒↝ _ $ cong H $ truncation-is-proposition _ _) ⟩
      (∃ λ ((b , _) : ∥ B ∥ × B) → H b)      ↔⟨ inverse Σ-assoc ⟩
      (∃ λ (b : ∥ B ∥) → B × H b)            ↔⟨ (∃-cong λ _ → ×-comm) ⟩
      (∃ λ (b : ∥ B ∥) → H b × B)            ↔⟨ Σ-assoc ⟩□
      Σ ∥ B ∥ H × B                          □

  ; inhabited = proj₁
  }

-- The conversion preserves getters and setters.

Lens→Higher-lens-preserves-getters-and-setters :
  Preserves-getters-and-setters-→ A B Lens→Higher-lens
Lens→Higher-lens-preserves-getters-and-setters l@(g , H , eq) =
    refl _
  , ⟨ext⟩ λ a → ⟨ext⟩ λ b →
    let h₁ = ≡⇒→ (cong (_$ g a) eq) (a , refl _)

        h₂ =
          _≃_.from (≡⇒↝ _ (cong H _))
            (subst (H ∘ proj₁) (sym (_≃_.left-inverse-of ∥∥×≃ _))
               (≡⇒→ (cong H _) h₁))

        lemma =
          h₂                                                         ≡⟨ sym $ subst-in-terms-of-inverse∘≡⇒↝ equivalence _ _ _ ⟩

          subst H _
            (subst (H ∘ proj₁) (sym (_≃_.left-inverse-of ∥∥×≃ _))
               (≡⇒→ (cong H _) h₁))                                  ≡⟨ cong (λ x → subst H (sym $ truncation-is-proposition _ _)
                                                                                (subst (H ∘ proj₁)
                                                                                (sym (_≃_.left-inverse-of ∥∥×≃ (∣ g a ∣ , b)))
                                                                                x)) $ sym $
                                                                        subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩
          subst H _
            (subst (H ∘ proj₁) (sym (_≃_.left-inverse-of ∥∥×≃ _))
               (subst H _ h₁))                                       ≡⟨ cong (λ x → subst H (sym $ truncation-is-proposition _ _) x) $
                                                                        subst-∘ _ _ _ ⟩

          subst H _ (subst H _ (subst H _ h₁))                       ≡⟨ cong (λ x → subst H (sym $ truncation-is-proposition _ _) x) $
                                                                        subst-subst _ _ _ _ ⟩

          subst H _ (subst H _ h₁)                                   ≡⟨ subst-subst _ _ _ _ ⟩

          subst H _ h₁                                               ≡⟨ cong (λ eq → subst H eq h₁) $
                                                                        mono₁ 1 truncation-is-proposition _ _ ⟩

          subst H _ h₁                                               ≡⟨ subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩∎

          ≡⇒→ (cong H _) h₁                                          ∎
    in
    (Higher.Lens.set (Lens→Higher-lens l) a b                      ≡⟨⟩

     proj₁ (_≃_.from (≡⇒↝ _ (cong (_$ b) eq)) h₂)                  ≡⟨ cong (λ f → proj₁ (f h₂)) $ sym $
                                                                      ≡⇒↝-sym equivalence ⟩

     proj₁ (≡⇒→ (sym (cong (_$ b) eq)) h₂)                         ≡⟨ cong (λ eq → proj₁ (≡⇒→ eq h₂)) $ sym $
                                                                      cong-sym _ _ ⟩

     proj₁ (≡⇒→ (cong (_$ b) (sym eq)) h₂)                         ≡⟨ cong (proj₁ ∘ ≡⇒→ (cong (_$ b) (sym eq)))
                                                                      lemma ⟩

     proj₁ (≡⇒→ (cong (_$ b) (sym eq)) (≡⇒→ (cong H _) h₁))        ≡⟨ cong (λ f → proj₁ (f h₁)) $ sym $
                                                                      ≡⇒↝-trans equivalence ⟩

     proj₁ (≡⇒→ (trans (cong H _) (cong (_$ b) (sym eq))) h₁)      ≡⟨⟩

     proj₁ (≡⇒→ (trans (cong H _) (cong (_$ b) (sym eq)))
              (≡⇒→ (cong (_$ g a) eq) (a , refl _)))               ≡⟨ cong (λ f → proj₁ (f (a , refl _))) $ sym $
                                                                      ≡⇒↝-trans equivalence ⟩
     proj₁ (≡⇒→ (trans (cong (_$ g a) eq)
                   (trans (cong H _) (cong (_$ b) (sym eq))))
              (a , refl _))                                        ≡⟨ cong (λ p → proj₁
                                                                                (≡⇒→ (trans p
                                                                                (trans (cong H (truncation-is-proposition _ _))
                                                                                (cong (_$ b) (sym eq))))
                                                                                (a , refl _))) $
                                                                      trans (cong (cong (_$ g a)) $ sym $ sym-sym _) $
                                                                      cong-sym _ _ ⟩
     proj₁ (≡⇒→ (trans (sym (cong (_$ g a) (sym eq)))
                   (trans (cong H _) (cong (_$ b) (sym eq))))
              (a , refl _))                                        ≡⟨ cong (λ eq → proj₁ (≡⇒→ eq (a , refl _))) $ sym $
                                                                      subst-in-terms-of-trans-and-cong ⟩
     proj₁ (≡⇒→ (subst (λ f → f (g a) ≡ f b) (sym eq) (cong H _))
              (a , refl _))                                        ≡⟨⟩

     Lens.set l a b                                                ∎)

-- Lens A B is equivalent to Higher.Lens A B (assuming univalence).

Lens≃Higher-lens :
  {A : Set a} {B : Set b} →
  Block "conversion" →
  Univalence (a ⊔ b) →
  Lens A B ≃ Higher.Lens A B
Lens≃Higher-lens {A = A} {B = B} ⊠ univ =
  Eq.↔→≃ to from to∘from from∘to
  where
  to = Lens→Higher-lens

  from : Higher.Lens A B → Lens A B
  from l =
      get
    , (λ _ → R)
    , (                      $⟨ (λ b → inverse (Higher.remainder≃get⁻¹ l b)) ⟩
       (∀ b → get ⁻¹ b ≃ R)  ↝⟨ (∀-cong _ λ _ → ≃⇒≡ univ) ⟩
       (∀ b → get ⁻¹ b ≡ R)  ↝⟨ ⟨ext⟩ ⟩□
       get ⁻¹_ ≡ const R     □)
    where
    open Higher.Lens l

  to∘from : ∀ l → to (from l) ≡ l
  to∘from l = _↔_.from (Higher.equality-characterisation₃ univ)
    ( (∥ B ∥ × R  ↔⟨ (drop-⊤-left-× λ r → _⇔_.to contractible⇔↔⊤ $
                      propositional⇒inhabited⇒contractible
                        truncation-is-proposition
                        (inhabited r)) ⟩□
       R          □)
    , (λ a →
         ≡⇒→ (cong (λ _ → R) (truncation-is-proposition _ _))
           (≡⇒→ (cong (_$ get a)
                   (⟨ext⟩ (≃⇒≡ univ ∘ inverse ∘
                           Higher.remainder≃get⁻¹ l)))
              (a , refl _))                                               ≡⟨ cong (λ eq → ≡⇒→ eq (≡⇒→ (cong (_$ get a)
                                                                                (⟨ext⟩ (≃⇒≡ univ ∘ inverse ∘
                                                                                Higher.remainder≃get⁻¹ l)))
                                                                                (a , refl _))) $
                                                                             cong-const _ ⟩
         ≡⇒→ (refl _)
           (≡⇒→ (cong (_$ get a)
                   (⟨ext⟩ (≃⇒≡ univ ∘ inverse ∘
                           Higher.remainder≃get⁻¹ l)))
              (a , refl _))                                               ≡⟨ cong (_$ ≡⇒→ (cong (_$ get a)
                                                                                (⟨ext⟩ (≃⇒≡ univ ∘ inverse ∘
                                                                                Higher.remainder≃get⁻¹ l)))
                                                                                (a , refl _))
                                                                             ≡⇒→-refl ⟩
         ≡⇒→ (cong (_$ get a)
                (⟨ext⟩ (≃⇒≡ univ ∘ inverse ∘ Higher.remainder≃get⁻¹ l)))
           (a , refl _)                                                   ≡⟨ cong (λ eq → ≡⇒→ eq (a , refl _)) $
                                                                             cong-ext _ ⟩
         ≡⇒→ (≃⇒≡ univ (inverse (Higher.remainder≃get⁻¹ l (get a))))
           (a , refl _)                                                   ≡⟨ cong (_$ a , refl _) $
                                                                             ≡⇒→-≃⇒≡ equivalence univ ⟩

         _≃_.from (Higher.remainder≃get⁻¹ l (get a)) (a , refl _)         ≡⟨⟩

         remainder a                                                      ∎)
    , (λ _ → refl _)
    )
    where
    open Higher.Lens l

  from∘to : ∀ l → from (to l) ≡ l
  from∘to l = _≃_.from (equality-characterisation₂ univ)
    ( (λ _ → refl _)
    , Σ∥B∥H≃H
    , (trans (sym (cong _⁻¹_ (⟨ext⟩ λ _ → refl _)))
         (trans
            (⟨ext⟩ (≃⇒≡ univ ∘ inverse ∘ Higher.remainder≃get⁻¹ (to l)))
            (⟨ext⟩ (≃⇒≡ univ ∘ Σ∥B∥H≃H ∘ ∣_∣)))                           ≡⟨ cong (flip trans _) $
                                                                             trans (cong (sym ∘ cong _⁻¹_) ext-refl) $
                                                                             trans (cong sym $ cong-refl _) $
                                                                             sym-refl ⟩
       trans (refl _)
         (trans
            (⟨ext⟩ (≃⇒≡ univ ∘ inverse ∘ Higher.remainder≃get⁻¹ (to l)))
            (⟨ext⟩ (≃⇒≡ univ ∘ Σ∥B∥H≃H ∘ ∣_∣)))                           ≡⟨ trans-reflˡ _ ⟩

       trans
         (⟨ext⟩ (≃⇒≡ univ ∘ inverse ∘ Higher.remainder≃get⁻¹ (to l)))
         (⟨ext⟩ (≃⇒≡ univ ∘ Σ∥B∥H≃H ∘ ∣_∣))                               ≡⟨ sym $ ext-trans _ _ ⟩

       (⟨ext⟩ λ b →
        trans
          (≃⇒≡ univ (inverse (Higher.remainder≃get⁻¹ (to l) b)))
          (≃⇒≡ univ (Σ∥B∥H≃H ∣ b ∣)))                                     ≡⟨ (cong ⟨ext⟩ $ ⟨ext⟩ λ _ → sym $
                                                                              ≃⇒≡-∘ univ ext _ _) ⟩
       (⟨ext⟩ λ b →
        ≃⇒≡ univ (Σ∥B∥H≃H ∣ b ∣ F.∘
                  inverse (Higher.remainder≃get⁻¹ (to l) b)))             ≡⟨ (cong ⟨ext⟩ $ ⟨ext⟩ λ _ → cong (≃⇒≡ univ) $ Eq.lift-equality ext $
                                                                              ⟨ext⟩ (lemma _)) ⟩

       (⟨ext⟩ λ b → ≃⇒≡ univ (≡⇒≃ (ext⁻¹ get⁻¹-≡ b)))                     ≡⟨ (cong ⟨ext⟩ $ ⟨ext⟩ λ _ →
                                                                              _≃_.left-inverse-of (≡≃≃ univ) _) ⟩

       (⟨ext⟩ λ b → ext⁻¹ get⁻¹-≡ b)                                      ≡⟨ _≃_.right-inverse-of (Eq.extensionality-isomorphism bad-ext) _ ⟩∎

       get⁻¹-≡                                                            ∎)
    )
    where
    open Lens l

    Σ∥B∥H≃H = λ b →
      Σ ∥ B ∥ H  ↔⟨ (drop-⊤-left-Σ $ _⇔_.to contractible⇔↔⊤ $
                     propositional⇒inhabited⇒contractible
                       truncation-is-proposition b) ⟩□
      H b        □

    lemma : ∀ b (p : get ⁻¹ b) → _
    lemma b p@(a , get-a≡b) =
      _≃_.to (Σ∥B∥H≃H ∣ b ∣)
        (_≃_.from (Higher.remainder≃get⁻¹ (to l) b) p)                    ≡⟨⟩

      subst H _
        (≡⇒→ (cong H _)
           (≡⇒→ (cong (_$ get a) get⁻¹-≡) (a , refl _)))                  ≡⟨ cong (subst H _) $ sym $
                                                                             subst-in-terms-of-≡⇒↝ equivalence _ _ _ ⟩

      subst H _ (subst H _ (≡⇒→ (cong (_$ get a) get⁻¹-≡) (a , refl _)))  ≡⟨ subst-subst _ _ _ _ ⟩

      subst H _ (≡⇒→ (cong (_$ get a) get⁻¹-≡) (a , refl _))              ≡⟨ cong (λ eq → subst H eq
                                                                                (≡⇒→ (cong (_$ get a) get⁻¹-≡) (a , refl _))) $
                                                                             mono₁ 1 truncation-is-proposition _ _ ⟩
      subst H (cong ∣_∣ get-a≡b)
        (≡⇒→ (cong (_$ get a) get⁻¹-≡) (a , refl _))                      ≡⟨ elim¹
                                                                               (λ {b} eq →
                                                                                subst H (cong ∣_∣ eq)
                                                                                (≡⇒→ (cong (_$ get a) get⁻¹-≡) (a , refl _)) ≡
                                                                                ≡⇒→ (cong (_$ b) get⁻¹-≡) (a , eq))
                                                                               (
          subst H (cong ∣_∣ (refl _))
            (≡⇒→ (cong (_$ get a) get⁻¹-≡) (a , refl _))                        ≡⟨ cong (λ eq → subst H eq
                                                                                (≡⇒→ (cong (_$ get a) get⁻¹-≡) (a , refl _))) $
                                                                                cong-refl _ ⟩
          subst H (refl _)
            (≡⇒→ (cong (_$ get a) get⁻¹-≡) (a , refl _))                        ≡⟨ subst-refl _ _ ⟩∎

          ≡⇒→ (cong (_$ get a) get⁻¹-≡) (a , refl _)                            ∎)
                                                                               get-a≡b ⟩
      ≡⇒→ (cong (_$ b) get⁻¹-≡) p                                         ≡⟨⟩

      ≡⇒→ (ext⁻¹ get⁻¹-≡ b) p                                             ∎

-- The equivalence preserves getters and setters.

Lens≃Higher-lens-preserves-getters-and-setters :
  {A : Set a} {B : Set b}
  (bc : Block "conversion")
  (univ : Univalence (a ⊔ b)) →
  Preserves-getters-and-setters-⇔ A B
    (_≃_.logical-equivalence (Lens≃Higher-lens bc univ))
Lens≃Higher-lens-preserves-getters-and-setters ⊠ univ =
  Preserves-getters-and-setters-→-↠-⇔
    (_≃_.surjection (Lens≃Higher-lens ⊠ univ))
    Lens→Higher-lens-preserves-getters-and-setters

-- An alternative proof showing that Lens A B is equivalent to
-- Higher.Lens A B (assuming univalence).
--
-- This proof was simplified following a suggestion by Paolo
-- Capriotti.
--
-- I have not proved that this equivalence preserves getters and
-- setters.

Lens≃Higher-lens′ :
  {A : Set a} {B : Set b} →
  Univalence (a ⊔ b) →
  Lens A B ≃ Higher.Lens A B
Lens≃Higher-lens′ {a = a} {b = b} {A = A} {B = B} univ =

  (∃ λ (g : A → B) → ∃ λ (H : Pow a ∥ B ∥) →
     (g ⁻¹_) ≡ H ∘ ∣_∣)                                  ↔⟨ Σ-cong lemma₂ (λ _ → ∃-cong (lemma₃ _)) ⟩

  (∃ λ (p : ∃ λ (P : Pow a B) → A ≃ ∃ P) →
   ∃ λ (H : Pow a ∥ B ∥) →
     proj₁ p ≡ H ∘ ∣_∣)                                  ↔⟨ ∃-comm ⟩

  (∃ λ (H : Pow a ∥ B ∥) →
   ∃ λ (p : ∃ λ (P : Pow a B) → A ≃ ∃ P) →
     proj₁ p ≡ H ∘ ∣_∣)                                  ↔⟨ (∃-cong λ _ → inverse Σ-assoc) ⟩

  (∃ λ (H : Pow a ∥ B ∥) →
   ∃ λ (P : Pow a B) →
      A ≃ ∃ P × P ≡ H ∘ ∣_∣)                             ↔⟨ (∃-cong λ _ → ∃-cong λ _ → ×-comm) ⟩

  (∃ λ (H : Pow a ∥ B ∥) →
   ∃ λ (P : Pow a B) →
      P ≡ H ∘ ∣_∣ × A ≃ ∃ P)                             ↔⟨ (∃-cong λ _ → ∃-cong λ _ → ∃-cong λ eq →
                                                             Eq.≃-preserves ext F.id (∃-cong λ x → ≡⇒↝ _ (cong (_$ x) eq))) ⟩
  (∃ λ (H : Pow a ∥ B ∥) →
   ∃ λ (P : Pow a B) →
      P ≡ H ∘ ∣_∣ × A ≃ ∃ (H ∘ ∣_∣))                     ↔⟨ (∃-cong λ _ → Σ-assoc) ⟩

  (∃ λ (H : Pow a ∥ B ∥) →
   (∃ λ (P : Pow a B) → P ≡ H ∘ ∣_∣) ×
   A ≃ ∃ (H ∘ ∣_∣))                                      ↔⟨ (∃-cong λ _ →
                                                             drop-⊤-left-× λ _ →
                                                             _⇔_.to contractible⇔↔⊤ (singleton-contractible _)) ⟩

  (∃ λ (H : Pow a ∥ B ∥) → A ≃ ∃ (H ∘ ∣_∣))              ↔⟨ inverse $
                                                            Σ-cong (inverse $ Pow↔Fam a ext univ) (λ _ →
                                                            Eq.≃-preserves ext F.id F.id) ⟩

  (∃ λ (H : Fam a ∥ B ∥) → A ≃ ∃ ((proj₂ H ⁻¹_) ∘ ∣_∣))  ↔⟨ inverse Σ-assoc ⟩

  (∃ λ (R : Set ℓ) →
   ∃ λ (f : R → ∥ B ∥) → A ≃ ∃ ((f ⁻¹_) ∘ ∣_∣))          ↔⟨ (∃-cong λ R → ∃-cong λ f →
                                                             Eq.≃-preserves ext F.id
                            (∃ ((f ⁻¹_) ∘ ∣_∣)                 ↔⟨ (∃-cong λ b → drop-⊤-right λ r →
                                                                     _⇔_.to contractible⇔↔⊤ $
                                                                       +⇒≡ truncation-is-proposition) ⟩
                             B × R                             ↔⟨ ×-comm ⟩□
                             R × B                             □)) ⟩

  (∃ λ (R : Set ℓ) → (R → ∥ B ∥) × (A ≃ (R × B)))        ↔⟨ (∃-cong λ _ → ×-comm) ⟩

  (∃ λ (R : Set ℓ) → (A ≃ (R × B)) × (R → ∥ B ∥))        ↔⟨ inverse Higher.Lens-as-Σ ⟩□

  Higher.Lens A B                                        □

  where
  ℓ = a ⊔ b

  lemma₁ : ∀ (g : A → B) b →
           g ⁻¹ b ↔ (g ∘ lower {ℓ = ℓ}) ⁻¹ b
  lemma₁ g b = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ { (a , ga≡b) → lift a , ga≡b }
        ; from = λ { (lift a , ga≡b) → a , ga≡b }
        }
      ; right-inverse-of = refl
      }
    ; left-inverse-of = refl
    }

  abstract

    lemma₂ : (A → B) ↔ ∃ λ (P : Pow a B) → A ≃ ∃ P
    lemma₂ = →↔Σ≃Σ ℓ ext univ

    lemma₃ :
      (g : A → B) (H : Pow a ∥ B ∥) →
      ((g ⁻¹_) ≡ H ∘ ∣_∣)
        ≃
      (proj₁ (_↔_.to lemma₂ g) ≡ H ∘ ∣_∣)
    lemma₃ g H =
      (g ⁻¹_) ≡ H ∘ ∣_∣                                            ↝⟨ inverse $ Eq.extensionality-isomorphism ext ⟩
      (∀ b → g ⁻¹ b ≡ H ∣ b ∣)                                     ↝⟨ ∀-cong ext (λ _ →
                                                                        ≡-preserves-≃ ext univ univ
                                                                          (Eq.↔⇒≃ $ lemma₁ _ _) F.id) ⟩
      (∀ b → (g ∘ lower) ⁻¹ b ≡ H ∣ b ∣)                           ↝⟨ Eq.extensionality-isomorphism ext ⟩
      ((g ∘ lower) ⁻¹_) ≡ H ∘ ∣_∣                                  ↝⟨ ≡⇒↝ _ $ cong (λ eq → (g ∘ lower ∘ _≃_.from eq ⁻¹_) ≡ H ∘ ∣_∣) lemma ⟩
      (g ∘ lower ∘ _≃_.from (≡⇒↝ _ (sym (refl _))) ⁻¹_) ≡ H ∘ ∣_∣  ↔⟨⟩
      proj₁ (_↔_.to lemma₂ g) ≡ H ∘ ∣_∣                            □
      where
      lemma =
        F.id                 ≡⟨ sym ≡⇒↝-refl ⟩
        ≡⇒↝ _ (refl _)       ≡⟨ cong (≡⇒↝ _) $ sym sym-refl ⟩∎
        ≡⇒↝ _ (sym (refl _)) ∎

-- If the domain A is a set, then Traditional.Lens A B and Lens A B
-- are isomorphic (assuming univalence).

Lens↔Traditional-lens :
  {A : Set a} {B : Set b} →
  Block "conversion" →
  Univalence (a ⊔ b) →
  Is-set A →
  Lens A B ↔ Traditional.Lens A B
Lens↔Traditional-lens {A = A} {B} bc univ A-set =
  Lens A B              ↔⟨ Lens≃Higher-lens bc univ ⟩
  Higher.Lens A B       ↝⟨ Higher.Lens↔Traditional-lens bc univ A-set ⟩□
  Traditional.Lens A B  □

-- The isomorphism preserves getters and setters.

Lens↔Traditional-lens-preserves-getters-and-setters :
  {A : Set a} {B : Set b}
  (bc : Block "conversion")
  (univ : Univalence (a ⊔ b))
  (s : Is-set A) →
  Preserves-getters-and-setters-⇔ A B
    (_↔_.logical-equivalence (Lens↔Traditional-lens bc univ s))
Lens↔Traditional-lens-preserves-getters-and-setters bc univ s =
  Preserves-getters-and-setters-⇔-∘
    {f = _↔_.logical-equivalence $
           Higher.Lens↔Traditional-lens bc univ s}
    {g = _≃_.logical-equivalence $ Lens≃Higher-lens bc univ}
    (Higher.Lens↔Traditional-lens-preserves-getters-and-setters
       bc univ s)
    (Lens≃Higher-lens-preserves-getters-and-setters bc univ)

max_stars_repo_name: Saizan/dependent-lenses

max_issues_repo_name: Saizan/dependent-lenses

max_forks_repo_name: Saizan/dependent-lenses


text:
module parse-test where

import parse
open import lib
open import cedille-types
import cedille

module parsem = parse cedille.gratr2-nt ptr
open parsem
open parsem.pnoderiv cedille.rrs cedille.cedille-rtn
open import run ptr
open noderiv {- from run.agda -}

process-start : start → string
process-start s = ""

process : Run → string
process (ParseTree (parsed-start p) :: []) = process-start p
process r = "Parsing failure (run with -" ^ "-showParsed).\n"

putStrRunIf : 𝔹 → Run → IO ⊤
putStrRunIf tt r = putStr (Run-to-string r) >> putStr "\n"
putStrRunIf ff r = return triv

parse-specific-nt : cedille.gratr2-nt → ℕ → (lc : 𝕃 char) → 𝕃 char ⊎ Run
parse-specific-nt nt starting-char-position lc with parse-filter lc lc [] [] (cedille.cedille-start nt) inj₁
...| inj₁ left = inj₁ left
...| inj₂ run = inj₂ (re-to-run starting-char-position (reverse run))

processArgs : (showRun : 𝔹) → (showParsed : 𝔹) → 𝕃 string → IO ⊤
processArgs showRun showParsed (input-filename :: []) = (readFiniteFile input-filename) >>= processText
  where processText : string → IO ⊤
        processText x with parse-specific-nt cedille._type 10 (string-to-𝕃char x)
        processText x | s with s
        processText x | s | inj₁ cs = putStr "Characters left before failure : " >> putStr (𝕃char-to-string cs) >> putStr "\nCannot proceed to parsing.\n"
        processText x | s | inj₂ r with putStrRunIf showRun r | rewriteRun r
        processText x | s | inj₂ r | sr | r' with putStrRunIf showParsed r'
        processText x | s | inj₂ r | sr | r' | sr' = sr >> sr' >> putStr (process r')

processArgs showRun showParsed ("--showRun" :: xs) = processArgs tt showParsed xs
processArgs showRun showParsed ("--showParsed" :: xs) = processArgs showRun tt xs
processArgs showRun showParsed (x :: xs) = putStr ("Unknown option " ^ x ^ "\n")
processArgs showRun showParsed [] = putStr "Please run with the name of a file to process.\n"

main : IO ⊤
main = getArgs >>= processArgs ff ff

ext: agda

max_stars_repo_name: xoltar/cedille

max_issues_repo_name: xoltar/cedille

max_forks_repo_name: xoltar/cedille


text:
-- Andreas, 2019-03-18, issue #3122, AIM XXIX
-- Also pick up hidden record fields from a module.

record R : Set₂ where
  field {f} : Set₁

module M where
  f : Set₁
  f = Set

r : R
r = record { M }

-- WAS: yellow
-- Should check.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

open import LogicalFormulae
open import Semirings.Definition
open import Numbers.Naturals.Definition
open import Numbers.Naturals.Semiring
open import Orders.Total.Definition
open import Orders.Partial.Definition

module Numbers.Naturals.Order where
open Semiring ℕSemiring
open import Decidable.Lemmas ℕDecideEquality

private
  infix 5 _<NLogical_
  _<NLogical_ : ℕ → ℕ → Set
  zero <NLogical zero = False
  zero <NLogical (succ n) = True
  (succ n) <NLogical zero = False
  (succ n) <NLogical (succ m) = n <NLogical m

infix 5 _<N_
record _<N_ (a : ℕ) (b : ℕ) : Set where
  constructor le
  field
    x : ℕ
    proof : (succ x) +N a ≡ b

infix 5 _<N'_
record _<N'_ (a : ℕ) (b : ℕ) : Set where
  constructor le'
  field
    x : ℕ
    .proof : (succ x) +N a ≡ b

infix 5 _≤N_
_≤N_ : ℕ → ℕ → Set
a ≤N b = (a <N b) || (a ≡ b)

succIsPositive : (a : ℕ) → zero <N succ a
succIsPositive a = le a (applyEquality succ (Semiring.commutative ℕSemiring a 0))

aLessSucc : (a : ℕ) → (a <NLogical succ a)
aLessSucc zero = record {}
aLessSucc (succ a) = aLessSucc a

private
  succPreservesInequalityLogical : {a b : ℕ} → (a <NLogical b) → (succ a <NLogical succ b)
  succPreservesInequalityLogical {a} {b} prAB = prAB

  lessTransitiveLogical : {a b c : ℕ} → (a <NLogical b) → (b <NLogical c) → (a <NLogical c)
  lessTransitiveLogical {a} {zero} {zero} prAB prBC = prAB
  lessTransitiveLogical {a} {(succ b)} {zero} prAB ()
  lessTransitiveLogical {zero} {zero} {(succ c)} prAB prBC = record {}
  lessTransitiveLogical {(succ a)} {zero} {(succ c)} () prBC
  lessTransitiveLogical {zero} {(succ b)} {(succ c)} prAB prBC = record {}
  lessTransitiveLogical {(succ a)} {(succ b)} {(succ c)} prAB prBC = lessTransitiveLogical {a} {b} {c} prAB prBC

  aLessXPlusSuccA : (a x : ℕ) → (a <NLogical x +N succ a)
  aLessXPlusSuccA a zero = aLessSucc a
  aLessXPlusSuccA zero (succ x) = record {}
  aLessXPlusSuccA (succ a) (succ x) = lessTransitiveLogical {a} {succ a} {x +N succ (succ a)} (aLessXPlusSuccA a zero) (aLessXPlusSuccA (succ a) x)

  leImpliesLogical<N : {a b : ℕ} → (a <N b) → (a <NLogical b)
  leImpliesLogical<N {zero} {zero} (le x ())
  leImpliesLogical<N {zero} {(succ b)} (le x proof) = record {}
  leImpliesLogical<N {(succ a)} {zero} (le x ())
  leImpliesLogical<N {(succ a)} {(succ .(succ a))} (le zero refl) = aLessSucc a
  leImpliesLogical<N {(succ a)} {(succ .(succ (x +N succ a)))} (le (succ x) refl) = succPreservesInequalityLogical {a} {succ (x +N succ a)} (lessTransitiveLogical {a} {succ a} {succ (x +N succ a)} (aLessSucc a) (aLessXPlusSuccA a x))

  logical<NImpliesLe : {a b : ℕ} → (a <NLogical b) → (a <N b)
  logical<NImpliesLe {zero} {zero} ()
  _<N_.x (logical<NImpliesLe {zero} {succ b} prAB) = b
  _<N_.proof (logical<NImpliesLe {zero} {succ b} prAB) = applyEquality succ (sumZeroRight b)
  logical<NImpliesLe {(succ a)} {zero} ()
  logical<NImpliesLe {(succ a)} {(succ b)} prAB with logical<NImpliesLe {a} prAB
  logical<NImpliesLe {(succ a)} {(succ .(succ (x +N a)))} prAB | le x refl = le x (applyEquality succ (transitivity (commutative x _) (applyEquality succ (commutative a _))))

lessTransitive : {a b c : ℕ} → (a <N b) → (b <N c) → (a <N c)
lessTransitive {a} {b} {c} prab prbc = logical<NImpliesLe (lessTransitiveLogical {a} {b} {c} (leImpliesLogical<N prab) (leImpliesLogical<N prbc))

lessIrreflexive : {a : ℕ} → (a <N a) → False
lessIrreflexive {zero} pr = leImpliesLogical<N pr
lessIrreflexive {succ a} pr = lessIrreflexive {a} (logical<NImpliesLe {a} {a} (leImpliesLogical<N {succ a} {succ a} pr))

succPreservesInequality : {a b : ℕ} → (a <N b) → (succ a <N succ b)
succPreservesInequality {a} {b} prAB = logical<NImpliesLe (succPreservesInequalityLogical {a} {b} (leImpliesLogical<N prAB))

canRemoveSuccFrom<N : {a b : ℕ} → (succ a <N succ b) → (a <N b)
canRemoveSuccFrom<N {a} {b} (le x proof) rewrite commutative x (succ a) | commutative a x = le x (succInjective proof)

a<SuccA : (a : ℕ) → a <N succ a
a<SuccA a = le zero refl

<NWellDefined : {a b : ℕ} → (p1 : a <N b) → (p2 : a <N b) → _<N_.x p1 ≡ _<N_.x p2
<NWellDefined {a} {b} (le x proof) (le y proof1) = equalityCommutative r
  where
    q : y +N a ≡ x +N a
    q = succInjective {y +N a} {x +N a} (transitivity proof1 (equalityCommutative proof))
    r : y ≡ x
    r = canSubtractFromEqualityRight q

canAddToOneSideOfInequality : {a b : ℕ} (c : ℕ) → a <N b → a <N (b +N c)
canAddToOneSideOfInequality {a} {b} c (le x proof) = le (x +N c) (transitivity (applyEquality succ (equalityCommutative (+Associative x c a))) (transitivity (applyEquality (λ i → (succ x) +N i) (commutative c a)) (transitivity (applyEquality succ (+Associative x a c)) (applyEquality (_+N c) proof))))

canAddToOneSideOfInequality' : {a b : ℕ} (c : ℕ) → a <N b → a <N (c +N b)
canAddToOneSideOfInequality' {a} {b} c (le x proof) = le (x +N c) ans
  where
    ans : succ ((x +N c) +N a) ≡ c +N b
    ans rewrite (equalityCommutative (+Associative x c a)) | commutative c a | (+Associative x a c) = transitivity (applyEquality (_+N c) proof) (commutative b c)

addingIncreases : (a b : ℕ) → a <N a +N succ b
addingIncreases zero b = succIsPositive b
addingIncreases (succ a) b = succPreservesInequality (addingIncreases a b)

zeroNeverGreater : {a : ℕ} → (a <N zero) → False
zeroNeverGreater {a} (le x ())

noIntegersBetweenXAndSuccX : {a : ℕ} (x : ℕ) → (x <N a) → (a <N succ x) → False
noIntegersBetweenXAndSuccX {zero} x x<a a<sx = zeroNeverGreater x<a
noIntegersBetweenXAndSuccX {succ a} x (le y proof) (le z proof1) with succInjective proof1
... | ah rewrite (equalityCommutative proof) | (succExtracts z (y +N x)) | +Associative (succ z) y x | commutative (succ (z +N y)) x = lessIrreflexive {x} (le (z +N y) (transitivity (commutative _ x) ah))

private
  orderIsTotal : (a b : ℕ) → ((a <N b) || (b <N a)) || (a ≡ b)
  orderIsTotal zero zero = inr refl
  orderIsTotal zero (succ b) = inl (inl (logical<NImpliesLe (record {})))
  orderIsTotal (succ a) zero = inl (inr (logical<NImpliesLe (record {})))
  orderIsTotal (succ a) (succ b) with orderIsTotal a b
  orderIsTotal (succ a) (succ b) | inl (inl x) = inl (inl (logical<NImpliesLe (leImpliesLogical<N x)))
  orderIsTotal (succ a) (succ b) | inl (inr x) = inl (inr (logical<NImpliesLe (leImpliesLogical<N x)))
  orderIsTotal (succ a) (succ b) | inr x = inr (applyEquality succ x)

  orderIsIrreflexive : {a b : ℕ} → (a <N b) → (b <N a) → False
  orderIsIrreflexive {zero} {b} prAB (le x ())
  orderIsIrreflexive {(succ a)} {zero} (le x ()) prBA
  orderIsIrreflexive {(succ a)} {(succ b)} prAB prBA = orderIsIrreflexive {a} {b} (logical<NImpliesLe (leImpliesLogical<N prAB)) (logical<NImpliesLe (leImpliesLogical<N prBA))

  orderIsTransitive : {a b c : ℕ} → (a <N b) → (b <N c) → (a <N c)
  orderIsTransitive {a} {.(succ (x +N a))} {.(succ (y +N succ (x +N a)))} (le x refl) (le y refl) = le (y +N succ x) (applyEquality succ (equalityCommutative (+Associative y (succ x) a)))

ℕTotalOrder : TotalOrder ℕ
PartialOrder._<_ (TotalOrder.order ℕTotalOrder) = _<N_
PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) = lessIrreflexive
PartialOrder.<Transitive (TotalOrder.order ℕTotalOrder) = orderIsTransitive
TotalOrder.totality ℕTotalOrder = orderIsTotal

cannotAddAndEnlarge : (a b : ℕ) → a <N succ (a +N b)
cannotAddAndEnlarge a b = le b (applyEquality succ (commutative b a))

cannotAddAndEnlarge' : {a b : ℕ} → a +N b <N a → False
cannotAddAndEnlarge' {a} {zero} pr rewrite sumZeroRight a = lessIrreflexive pr
cannotAddAndEnlarge' {a} {succ b} pr rewrite (succExtracts a b) = lessIrreflexive {a} (lessTransitive {a} {succ (a +N b)} {a} (cannotAddAndEnlarge a b) pr)

cannotAddAndEnlarge'' : {a b : ℕ} → a +N succ b ≡ a → False
cannotAddAndEnlarge'' {a} {b} pr = naughtE (equalityCommutative inter)
  where
    inter : succ b ≡ 0
    inter rewrite commutative a (succ b) = canSubtractFromEqualityRight pr

naturalsAreNonnegative : (a : ℕ) → (a <N zero) → False
naturalsAreNonnegative zero ()
naturalsAreNonnegative (succ x) ()

lessRespectsAddition : {a b : ℕ} (c : ℕ) → (a <N b) → ((a +N c) <N (b +N c))
lessRespectsAddition {a} {b} zero prAB rewrite commutative a 0 | commutative b 0 = prAB
lessRespectsAddition {a} {b} (succ c) prAB rewrite commutative a (succ c) | commutative b (succ c) | commutative c a | commutative c b = succPreservesInequality (lessRespectsAddition c prAB)

lessRespectsMultiplicationLeft : (a b c : ℕ) → (a <N b) → (zero <N c) → (c *N a <N c *N b)
lessRespectsMultiplicationLeft zero zero c (le x ()) cPos
lessRespectsMultiplicationLeft zero (succ b) zero prAB (le x ())
lessRespectsMultiplicationLeft zero (succ b) (succ c) prAB cPos = i
  where
    productNonzeroIsNonzero : {a b : ℕ} → zero <N a → zero <N b → zero <N a *N b
    productNonzeroIsNonzero {zero} {b} prA prB = prA
    productNonzeroIsNonzero {succ a} {zero} prA ()
    productNonzeroIsNonzero {succ a} {succ b} prA prB = le (b +N a *N succ b) (applyEquality succ (Semiring.sumZeroRight ℕSemiring _))

    j : zero <N succ c *N succ b
    j = productNonzeroIsNonzero cPos prAB
    i : succ c *N zero <N succ c *N succ b
    i = identityOfIndiscernablesLeft _<N_ j (equalityCommutative (productZeroRight c))
lessRespectsMultiplicationLeft (succ a) zero c (le x ()) cPos
lessRespectsMultiplicationLeft (succ a) (succ b) c prAB cPos = m
  where
    h : c *N a <N c *N b
    h = lessRespectsMultiplicationLeft a b c (canRemoveSuccFrom<N prAB) cPos
    j : c *N a +N c <N c *N b +N c
    j = lessRespectsAddition c h
    i : c *N succ a <N c *N b +N c
    i = identityOfIndiscernablesLeft _<N_ j (equalityCommutative (transitivity (multiplicationNIsCommutative c _) (transitivity (applyEquality (c +N_) (multiplicationNIsCommutative a _)) (commutative c _))))
    m : c *N succ a <N c *N succ b
    m = identityOfIndiscernablesRight _<N_ i (equalityCommutative (transitivity (multiplicationNIsCommutative c _) (transitivity (commutative c _) (applyEquality (_+N c) (multiplicationNIsCommutative b _)))))

canFlipMultiplicationsInIneq : {a b c d : ℕ} → (a *N b <N c *N d) → b *N a <N d *N c
canFlipMultiplicationsInIneq {a} {b} {c} {d} pr = identityOfIndiscernablesRight _<N_ (identityOfIndiscernablesLeft _<N_ pr (multiplicationNIsCommutative a b)) (multiplicationNIsCommutative c d)

lessRespectsMultiplication : (a b c : ℕ) → (a <N b) → (zero <N c) → (a *N c <N b *N c)
lessRespectsMultiplication a b c prAB cPos = canFlipMultiplicationsInIneq {c} {a} {c} {b} (lessRespectsMultiplicationLeft a b c prAB cPos)

squash<N : {a b : ℕ} → .(a <N b) → a <N b
squash<N {a} {b} a<b with orderIsTotal a b
... | inl (inl x) = x
... | inl (inr x) = exFalso (lessIrreflexive (orderIsTransitive x a<b))
squash<N {a} {b} a<b | inr refl = exFalso (lessIrreflexive a<b)

<NTo<N' : {a b : ℕ} → a <N b → a <N' b
<NTo<N' (le x proof) = le' x proof

<N'To<N : {a b : ℕ} → a <N' b → a <N b
<N'To<N {a} {b} (le' x proof) = le x (squash proof)

<N'Refl : {a b : ℕ} → (p1 p2 : a <N' b) → p1 ≡ p2
<N'Refl p1 p2 with <NWellDefined (<N'To<N p1) (<N'To<N p2)
... | refl = refl


text:
open import Common.List
open import Common.Equality

map-append : ∀{A B : Set}(f : A → B) (xs {ys} : List A) →
             map f (xs ++ ys) ≡ map f xs ++ map f ys
map-append f [] = refl
map-append f (x ∷ xs) = {!cong (f x ∷_)!}   -- Keep section on C-c C-r

map-append₂ : ∀{A B : Set}(f : A → B) (xs {ys} : List A) →
             map f (xs ++ ys) ≡ map f xs ++ map f ys
map-append₂ f [] = refl
map-append₂ f (x ∷ xs) = {!cong (λ section → f x ∷ section)!} -- Keep lambda on C-c C-r

-- Check that we print sections in goals
postulate
  _+_ : Set → Set → Set
  μ : (Set → Set) → Set

foo : (A : Set) → μ (_+ A)
foo A = {!!}

bar : (A : Set) → μ (λ section → section + A)
bar A = {!!}

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- Normalization by Evaluation for Intuitionistic Predicate Logic (IPL)

module Everything where

-- Imports from the standard library and simple definitions

import Library

-- Types and terms of IPL

import Formulas
import Derivations

-- Beth model

import TermModel
import NfModel

-- A variant where Cover : PSh → PSh

import NfModelCaseTree        -- Presented at ITC 2018-07-19
import NfModelCaseTreeConv

-- A generalization to any CoverMonad which includes the
-- continuation monad used in Danvy's algorithm

import NfModelMonad
import Consistency

-- A monadic interpreter using shift/reset and an optimization

import DanvyShiftReset
import DanvyShiftResetLiftable

-- SET-interpretation and soundness of NbE

import Interpretation
import NbeModel

-- A general theory of sheaves over preorders

import PresheavesAndSheaves

max_stars_repo_name: andreasabel/ipl

max_issues_repo_name: andreasabel/ipl

max_forks_repo_name: andreasabel/ipl


text:
module HasNeitherNor where

record HasNeitherNor (A : Set) : Set
 where
  field
    _⊗_ : A → A → A

open HasNeitherNor ⦃ … ⦄ public


text:
{-# OPTIONS --guardedness #-}

module ky where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; _≢_; refl; cong; cong₂; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open import Data.Rational using (ℚ; _+_; _*_; _-_)
open import Data.Bool
open import Data.Bool.Properties
open import Data.Rational
open import Data.Nat as ℕ using (ℕ; zero; suc)
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Agda.Builtin.Size
open import Data.Product
open import Data.Unit
open import Data.Maybe

data QRE : Set → Set → Set₁ where
  ⊥ : ∀{D C} → QRE D C
  ε : ∀{D C} → C → QRE D C
  α : ∀{D C}
    → (D → Bool)  --φ
    → (D → C)     --op
    → QRE D C
  split : ∀{D C B A}
    → QRE D A     --f
    → QRE D B     --g
    → (A → B → C) --op
    → QRE D C
  iter : ∀{D B A}
    → QRE D B     --init
    → QRE D A     --body
    → (B → A → B) --op
    → QRE D B
  or : ∀{D C}
    → QRE D C
    → QRE D C
    → QRE D C

Event : Set
Event = ℕ

data Val : Set → Set where
  VBool : Bool → Val Bool
  VNat  : ℕ → Val ℕ

data Exp : Set → Set where
  EVal : ∀{t : Set} → Val t → Exp t

data Com : Set → Set where
  CFlip : ∀{t} → Com t → Com t → Com t
  CUpd  : Exp Event → Com ⊤
  CIte  : ∀{t} → Exp Bool → Com t → Com t → Com t
  CSeq  : ∀{t} → Com ⊤ → Com t → Com t

is-true : Bool → Bool
is-true = λ{x → x}

data CoList (i : Size) (A : Set) : Set where
  nil  : CoList i A
  cons : A → ∀{j : Size< i} → CoList j A → CoList i A

_++_ : ∀{A} → CoList ∞ A → CoList ∞ A → CoList ∞ A
nil         ++ s₂ = s₂
(cons a s₁) ++ s₂ = cons a (s₁ ++ s₂)

interp : Com ⊤ → QRE Bool (CoList ∞ Event)
interp (CFlip c₁ c₂) =
  or (split (α is-true λ{_ → nil}) (interp c₁) (_++_))
     (split (α not     λ{_ → nil}) (interp c₂) (_++_))

max_stars_repo_name: OUPL/Zar

max_issues_repo_name: OUPL/Zar

max_forks_repo_name: OUPL/Zar


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

module Tools.Bool where

open import Data.Bool using (Bool; true; false; _∧_; if_then_else_) public


text:
module Text.Greek.Script where

open import Data.Maybe
open import Data.Vec
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality using (_≢_)

data Case : Set where
  lower upper : Case

data Letter : Set where
  α′ β′ γ′ δ′ ε′ ζ′ η′ θ′ ι′ κ′ λ′ μ′ ν′ ξ′ ο′ π′ ρ′ σ′ τ′ υ′ φ′ χ′ ψ′ ω′ : Letter

vowels : Vec _ _
vowels = α′ ∷ ε′ ∷ η′ ∷ ι′ ∷ ο′ ∷ υ′ ∷ ω′ ∷ []

always-short-letters : Vec _ _
always-short-letters = ε′ ∷ ο′ ∷ []

diaeresis-letters : Vec _ _
diaeresis-letters = ι′ ∷ υ′ ∷ []

iota-subscript-letters : Vec _ _
iota-subscript-letters = α′ ∷ η′ ∷ ω′ ∷ []

data _vowel : Letter → Set where
  is-vowel : ∀ {v} → v ∈ vowels → v vowel

data _always-short : Letter → Set where
  is-always-short : ∀ {v} → v vowel → v ∈ always-short-letters → v always-short

data _diaeresis : Letter → Set where
  add-diaeresis : ∀ {v} → v vowel → v ∈ diaeresis-letters → v diaeresis

data _⟦_⟧-final : Letter → Case → Set where
  make-final : σ′ ⟦ lower ⟧-final

data _⟦_⟧-smooth : Letter → Case → Set where
  add-smooth-lower-vowel : ∀ {v} → v vowel → v ⟦ lower ⟧-smooth
  add-smooth-ρ : ρ′ ⟦ lower ⟧-smooth
  add-smooth-upper-vowel-not-Υ : ∀ {v} → v vowel → v ≢ υ′ → v ⟦ upper ⟧-smooth

data _with-rough : Letter → Set where
  add-rough-vowel : ∀ {v} → v vowel → v with-rough
  add-rough-ρ : ρ′ with-rough

data _iota-subscript : Letter → Set where
  add-iota-subscript : ∀ {v} → v vowel → v ∈ iota-subscript-letters → v iota-subscript

data _⟦_⟧-breathing : Letter → Case → Set where
  smooth : ∀ {ℓ c} → ℓ ⟦ c ⟧-smooth → ℓ ⟦ c ⟧-breathing
  rough : ∀ {ℓ c} → ℓ with-rough → ℓ ⟦ c ⟧-breathing

data _long-vowel : Letter → Set where
  make-long-vowel : ∀ {v} → v vowel → ¬ v always-short → v long-vowel

data _accent : Letter → Set where
  acute : ∀ {ℓ} → ℓ vowel → ℓ accent
  grave : ∀ {ℓ} → ℓ vowel → ℓ accent
  circumflex : ∀ {ℓ} → ℓ long-vowel → ℓ accent

data Token : Set where
  unmarked : (ℓ : Letter) → (c : Case) → Token
  with-accent : (ℓ : Letter) → (c : Case) → ℓ accent → Token
  with-breathing : (ℓ : Letter) → (c : Case) → ℓ ⟦ c ⟧-breathing → Token
  with-accent-breathing : (ℓ : Letter) → (c : Case) → ℓ accent → ℓ ⟦ c ⟧-breathing → Token
  with-accent-breathing-iota : (ℓ : Letter) → (c : Case) → ℓ accent → ℓ ⟦ c ⟧-breathing → ℓ iota-subscript → Token
  with-diaeresis : (ℓ : Letter) → (c : Case) → ℓ diaeresis → Token
  with-accent-diaeresis : (ℓ : Letter) → (c : Case) → ℓ accent → ℓ diaeresis → Token
  with-accent-iota : (ℓ : Letter) → (c : Case) → ℓ accent → ℓ iota-subscript → Token
  with-breathing-iota : (ℓ : Letter) → (c : Case) → ℓ ⟦ c ⟧-breathing → ℓ iota-subscript → Token
  with-iota : (ℓ : Letter) → (c : Case) → ℓ iota-subscript → Token
  final : (ℓ : Letter) → (c : Case) → ℓ ⟦ c ⟧-final → Token

-- Constructions

-- Α α
α-vowel : α′ vowel
α-vowel = is-vowel here

¬α-always-short : ¬ α′ always-short
¬α-always-short (is-always-short x (there (there ())))

α-long-vowel : α′ long-vowel
α-long-vowel = make-long-vowel α-vowel ¬α-always-short

α-smooth : α′ ⟦ lower ⟧-smooth
α-smooth = add-smooth-lower-vowel (is-vowel here)

Α-smooth : α′ ⟦ upper ⟧-smooth
Α-smooth = add-smooth-upper-vowel-not-Υ (is-vowel here) (λ ())

α-rough : α′ with-rough
α-rough = add-rough-vowel (is-vowel here)

α-iota-subscript : α′ iota-subscript
α-iota-subscript = add-iota-subscript (is-vowel here) here

-- Ε ε
ε-vowel : ε′ vowel
ε-vowel = is-vowel (there here)

ε-always-short : ε′ always-short
ε-always-short = is-always-short (is-vowel (there here)) here

ε-smooth : ε′ ⟦ lower ⟧-smooth
ε-smooth = add-smooth-lower-vowel (is-vowel (there here))

Ε-smooth : ε′ ⟦ upper ⟧-smooth
Ε-smooth = add-smooth-upper-vowel-not-Υ (is-vowel (there here)) (λ ())

ε-rough : ε′ with-rough
ε-rough = add-rough-vowel (is-vowel (there here))

-- Η η
η-vowel : η′ vowel
η-vowel = is-vowel (there (there here))

¬η-always-short : ¬ η′ always-short
¬η-always-short (is-always-short x (there (there ())))

η-long-vowel : η′ long-vowel
η-long-vowel = make-long-vowel (is-vowel (there (there here))) ¬η-always-short

η-smooth : η′ ⟦ lower ⟧-smooth
η-smooth = add-smooth-lower-vowel (is-vowel (there (there here)))

Η-smooth : η′ ⟦ upper ⟧-smooth
Η-smooth = add-smooth-upper-vowel-not-Υ (is-vowel (there (there here))) (λ ())

η-rough : η′ with-rough
η-rough = add-rough-vowel (is-vowel (there (there here)))

η-iota-subscript : η′ iota-subscript
η-iota-subscript = add-iota-subscript (is-vowel (there (there here))) (there here)

-- Ι ι

ι-vowel : ι′ vowel
ι-vowel = is-vowel (there (there (there here)))

¬ι-always-short : ¬ ι′ always-short
¬ι-always-short (is-always-short x (there (there ())))

ι-long-vowel : ι′ long-vowel
ι-long-vowel = make-long-vowel (is-vowel (there (there (there here)))) ¬ι-always-short

ι-smooth : ι′ ⟦ lower ⟧-smooth
ι-smooth = add-smooth-lower-vowel (is-vowel (there (there (there here))))

Ι-smooth : ι′ ⟦ upper ⟧-smooth
Ι-smooth = add-smooth-upper-vowel-not-Υ
             (is-vowel (there (there (there here)))) (λ ())

ι-rough : ι′ with-rough
ι-rough = add-rough-vowel (is-vowel (there (there (there here))))

ι-diaeresis : ι′ diaeresis
ι-diaeresis = add-diaeresis (is-vowel (there (there (there here)))) here

-- Ο ο
ο-vowel : ο′ vowel
ο-vowel = is-vowel (there (there (there (there here))))

ο-always-short : ο′ always-short
ο-always-short = is-always-short (is-vowel (there (there (there (there here)))))
                   (there here)

ο-smooth : ο′ ⟦ lower ⟧-smooth
ο-smooth = add-smooth-lower-vowel
             (is-vowel (there (there (there (there here)))))

Ο-smooth : ο′ ⟦ upper ⟧-smooth
Ο-smooth = add-smooth-upper-vowel-not-Υ
             (is-vowel (there (there (there (there here))))) (λ ())

ο-rough : ο′ with-rough
ο-rough = add-rough-vowel (is-vowel (there (there (there (there here)))))

-- Ρ ρ
ρ-smooth : ρ′ ⟦ lower ⟧-smooth
ρ-smooth = add-smooth-ρ

ρ-rough : ρ′ with-rough
ρ-rough = add-rough-ρ

-- Σ σ
σ-final : σ′ ⟦ lower ⟧-final
σ-final = make-final

-- Υ υ
υ-vowel : υ′ vowel
υ-vowel = is-vowel (there (there (there (there (there here)))))

¬υ-always-short : ¬ υ′ always-short
¬υ-always-short (is-always-short x (there (there ())))

υ-long-vowel : υ′ long-vowel
υ-long-vowel = make-long-vowel υ-vowel ¬υ-always-short

υ-smooth : υ′ ⟦ lower ⟧-smooth
υ-smooth = add-smooth-lower-vowel
             (is-vowel (there (there (there (there (there here))))))

υ-rough : υ′ with-rough
υ-rough = add-rough-vowel
            (is-vowel (there (there (there (there (there here))))))

υ-diaeresis : υ′ diaeresis
υ-diaeresis = add-diaeresis
                (is-vowel (there (there (there (there (there here))))))
                (there here)

-- Ω ω
ω-vowel : ω′ vowel
ω-vowel = is-vowel (there (there (there (there (there (there here))))))

¬ω-always-short : ¬ ω′ always-short
¬ω-always-short (is-always-short x (there (there ())))

ω-long-vowel : ω′ long-vowel
ω-long-vowel = make-long-vowel ω-vowel ¬ω-always-short

ω-smooth : ω′ ⟦ lower ⟧-smooth
ω-smooth = add-smooth-lower-vowel
             (is-vowel (there (there (there (there (there (there here)))))))

Ω-smooth : ω′ ⟦ upper ⟧-smooth
Ω-smooth = add-smooth-upper-vowel-not-Υ
             (is-vowel (there (there (there (there (there (there here)))))))
             (λ ())

ω-rough : ω′ with-rough
ω-rough = add-rough-vowel
            (is-vowel (there (there (there (there (there (there here)))))))

ω-iota-subscript : ω′ iota-subscript
ω-iota-subscript = add-iota-subscript
                     (is-vowel (there (there (there (there (there (there here)))))))
                     (there (there here))

-- Mapping

get-letter : Token → Letter
get-letter (unmarked ℓ _) = ℓ
get-letter (with-accent ℓ _ _) = ℓ
get-letter (with-breathing ℓ _ _) = ℓ
get-letter (with-accent-breathing ℓ _ _ _) = ℓ
get-letter (with-accent-breathing-iota ℓ _ _ _ _) = ℓ
get-letter (with-diaeresis ℓ _ _) = ℓ
get-letter (with-accent-diaeresis ℓ _ _ _) = ℓ
get-letter (with-accent-iota ℓ _ _ _) = ℓ
get-letter (with-breathing-iota ℓ _ _ _) = ℓ
get-letter (with-iota ℓ _ _) = ℓ
get-letter (final ℓ _ _) = ℓ

get-case : Token → Case
get-case (unmarked _ c) = c
get-case (with-accent _ c _) = c
get-case (with-breathing _ c _) = c
get-case (with-accent-breathing _ c _ _) = c
get-case (with-accent-breathing-iota _ c _ _ _) = c
get-case (with-diaeresis _ c _) = c
get-case (with-accent-diaeresis _ c _ _) = c
get-case (with-accent-iota _ c _ _) = c
get-case (with-breathing-iota _ c _ _) = c
get-case (with-iota _ c _) = c
get-case (final _ c _) = c

data Accent : Set where
  acute-mark grave-mark circumflex-mark : Accent

letter-to-accent : ∀ {v} → v accent → Accent
letter-to-accent (acute x) = acute-mark
letter-to-accent (grave x) = grave-mark
letter-to-accent (circumflex x) = circumflex-mark

get-accent : Token → Maybe Accent
get-accent (with-accent _ _ a) = just (letter-to-accent a)
get-accent (with-accent-breathing _ _ a _) = just (letter-to-accent a)
get-accent (with-accent-breathing-iota _ _ a _ _) = just (letter-to-accent a)
get-accent (with-accent-diaeresis _ _ a _) = just (letter-to-accent a)
get-accent (with-accent-iota _ _ a _) = just (letter-to-accent a)
get-accent _ = nothing

data Breathing : Set where
  smooth-mark rough-mark : Breathing

letter-to-breathing : ∀ {ℓ c} → ℓ ⟦ c ⟧-breathing → Breathing
letter-to-breathing (smooth x) = smooth-mark
letter-to-breathing (rough x) = rough-mark

get-breathing : Token → Maybe Breathing
get-breathing (with-breathing _ _ x) = just (letter-to-breathing x)
get-breathing (with-accent-breathing _ _ _ x) = just (letter-to-breathing x)
get-breathing (with-accent-breathing-iota _ _ _ x _) = just (letter-to-breathing x)
get-breathing (with-breathing-iota _ _ x _) = just (letter-to-breathing x)
get-breathing _ = nothing

data IotaSubscript : Set where
  iota-subscript-mark : IotaSubscript

get-iota-subscript : Token → Maybe IotaSubscript
get-iota-subscript (with-accent-breathing-iota _ _ _ _ _) = just iota-subscript-mark
get-iota-subscript (with-accent-iota _ _ _ _) = just iota-subscript-mark
get-iota-subscript (with-breathing-iota _ _ _ _) = just iota-subscript-mark
get-iota-subscript _ = nothing

data Diaeresis : Set where
  diaeresis-mark : Diaeresis

get-diaeresis : Token → Maybe Diaeresis
get-diaeresis (with-diaeresis _ _ _) = just diaeresis-mark
get-diaeresis (with-accent-diaeresis _ _ _ _) = just diaeresis-mark
get-diaeresis _ = nothing

data FinalForm : Set where
  final-form : FinalForm

get-final-form : Token → Maybe FinalForm
get-final-form (final _ _ _) = just final-form
get-final-form _ = nothing

max_stars_repo_name: scott-fleischman/GreekGrammar

max_issues_repo_name: scott-fleischman/GreekGrammar

max_forks_repo_name: scott-fleischman/GreekGrammar


text:
module Partiality where

{- port from http://www.soimort.org/posts/programs-and-proofs/ -}

open import Data.Bool using (Bool; false; true)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Char using (_==_) renaming (Char to Symbol)
open import Coinduction using (∞; ♯_; ♭)
-- open import Category.Monad.Partiality renaming (monad to PM)
-- open import Category.Monad using (RawMonad; module RawMonad)

data Expr : Set where
  var : Symbol → Expr
  lambda : Symbol → Expr → Expr
  app : Expr → Expr → Expr

data Function : Set where
  def : Expr → Function

mutual

  data Env : Set where
    ε : Env
    _↦_,_ : Symbol → Value → Env → Env

  data Value : Set where
    closure : Function → Env → Value
    exception : Value

lookup : Symbol → Env → Maybe Value
lookup sym ε = nothing
lookup sym (sym′ ↦ val , env) with sym == sym′
... | true = just val
... | false = lookup sym env

-- partiality monad
data _⊥ (A : Set) : Set where
  now : A → A ⊥
  later : ∞ (A ⊥) → A ⊥

return : {a : Set} → a → a ⊥
return = now

_>>=_ : {a b : Set} → a ⊥ → (a → b ⊥) → b ⊥
(now x) >>= f = f x
(later x) >>= f = later (♯ (♭ x >>= f))
infixl 40 _>>=_

{-# TERMINATING #-}
force : Value ⊥ → Value
force (now x) = x
force (later x) = force (♭ x)

mutual

  {-# TERMINATING #-} -- TODO: ???
  interp : Expr → Env → Value ⊥
  interp (var x) env with lookup x env
  ... | just val = now val
  ... | nothing = now exception
  interp (lambda x e) env = now (closure (def (lambda x e)) env)
  interp (app e₁ e₂) env = later (♯ apply (interp e₁ env) (interp e₂ env))

  apply : Value ⊥ → Value ⊥ → Value ⊥
  apply (later f) a = later (♯ apply (♭ f) a)
  apply (now (closure (def (lambda x e)) env)) a =
                               a >>= \a′ → interp e (x ↦ a′ , env)
    -- let open RawMonad PM in a >>= \a′ → interp e (x ↦ a′ , env)
  apply _ _ = now exception

e0 = ε
t1 = lambda 'a' (var 'a')
t2 = app (lambda 'x' (var 'x')) (lambda 'a' (var 'a'))
t3 = app (app (lambda 'f' (lambda 'x' (app (var 'f') (var 'x'))))
              (lambda 'a' (var 'a')))
         (lambda 'b' (var 'b'))
t4 = app (lambda 'x' (app (var 'x') (var 'x')))
         (lambda 'x' (app (var 'x') (var 'x')))

r1 = force (interp t1 e0)
r2 = force (interp t2 e0)
r3 = force (interp t3 e0)
r4 = force (interp t4 e0)


text:
module Selective.Examples.Main-generated where
import Selective.Examples.PingPong as PingPong
import Selective.Examples.TestCall as Call
import Selective.Examples.TestCall2 as Call2
import Selective.Examples.Fibonacci as Fib
import Selective.Examples.Chat as Chat
import Selective.Examples.Bookstore as Bookstore
import Selective.Examples.TestAO as TestAO
import Selective.Examples.TestSelectiveReceive as SelectiveReceive
import Selective.Examples.TestSelectiveReceive-calc as SelectiveReceive-calc

open import Selective.Runtime
open import Selective.SimulationEnvironment
open import Selective.ActorMonad
import IO
open ∞ActorM

pingpongEntry = singleton-env (PingPong.spawner .force)
callEntry = singleton-env (Call.calltestActor .force)
call2Entry = singleton-env (Call2.calculator-test-actor .force)
fibEntry = singleton-env (Fib.spawner .force)
chatEntry = singleton-env (Chat.chat-supervisor .force)
bookstoreEntry = singleton-env (Bookstore.bookstore-supervisor .force)
testaoEntry = singleton-env (TestAO.calculator-test-actor .force)
testsrcalcEntry = singleton-env (SelectiveReceive-calc.calculator-test-actor .force)
testsrEntry = singleton-env (SelectiveReceive.receive-42-with-reference)

main = IO.run (run-env testsrcalcEntry)

max_stars_repo_name: Zalastax/thesis

max_issues_repo_name: Zalastax/singly-typed-actors

max_forks_repo_name: Zalastax/singly-typed-actors


text:
open import Agda.Primitive

record Functor {a b} (F : Set a → Set b) : Set (lsuc a ⊔ b) where
  field
    fmap : ∀ {A B} → (A → B) → F A → F B

open Functor {{...}} public

module _ {a b} (F : Set a → Set b) where
  record FunctorZero : Set (lsuc a ⊔ b) where
    field
      empty : ∀ {A} → F A
      overlap {{super}} : Functor F

  record Alternative : Set (lsuc a ⊔ b) where
    infixl 3 _<|>_
    field
      _<|>_ : ∀ {A} → F A → F A → F A
      overlap {{super}} : FunctorZero

open FunctorZero {{...}} public

open Alternative {{...}} public

record StateT {a} (S : Set a) (M : Set a → Set a) (A : Set a) : Set a where
  no-eta-equality
  constructor stateT
  field runStateT : S → M A

open StateT public

module _ {a} {S : Set a} {M : Set a → Set a} where

  instance
    FunctorStateT : {{_ : Functor M}} → Functor {a = a} (StateT S M)
    runStateT (fmap {{FunctorStateT}} f m) s = fmap f (runStateT m s)

    FunctorZeroStateT : {{_ : FunctorZero M}} → FunctorZero {a = a} (StateT S M)
    runStateT (empty {{FunctorZeroStateT}}) s = empty

    AlternativeStateT : {{_ : Alternative M}} → Alternative {a = a} (StateT S M)
    runStateT (_<|>_ {{AlternativeStateT}} x y) s = runStateT x s <|> runStateT y s

--- Example with some module parameter instantiations

open import Agda.Builtin.Nat
open import Agda.Builtin.Unit

data Vec (A : Set) : Nat → Set where
  []  : Vec A 0
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

postulate
  C₁ : Set → Set

record C₂ (A : Set) : Set where
  field
    f : A → A
    overlap {{super}} : C₁ A

open C₂ {{...}}

postulate
  T : (A : Set) → A → Set

module M (A : Set) (n : Nat) (xs : Vec A n) where

  unpackT : Vec A n → Set
  unpackT (x ∷ xs) = C₂ (T A x)
  unpackT [] = ⊤

  postulate instance C₁T : ∀ {x} {{C₁A : C₁ A}} → C₁ (T A x)

  C₂T : {{C₂A : C₂ A}} (ys : Vec A n) → unpackT ys
  C₂T [] = _
  f {{C₂T (y ∷ ys)}} x = x


text:
module Issue251 where

record Foo : Set₁ where
  field
    A : Set
    B : Set

foo : Set → Set → Foo
foo = λ A B → record {A = A; B = B}


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

module PathLemmas where

open import Relation.Binary.PropositionalEquality using
  (_≡_; sym; refl)

------------------------------------------------------------------------------
-- These also follow from irrelevance, but this is nicer

sym-sym : {A : Set} {x y : A} {p : x ≡ y} → sym (sym p) ≡ p
sym-sym {_} {x} {.x} {refl} = refl

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

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

module Interval where

open import Cubical.Core.Everything using (_≡_; Level; Type; Σ; _,_; fst; snd; _≃_; ~_)

open import Cubical.Foundations.Prelude     using (refl; sym; _∙_; cong; transport; subst; funExt; transp; I; i0; i1)
--open import Cubical.Foundations.Function    using (_∘_)
open import Cubical.Foundations.Univalence  using (ua)
open import Cubical.Foundations.Isomorphism using (iso; Iso; isoToPath; section; retract; isoToEquiv)

open import Data.Bool       using (Bool; true; false; _∨_; _∧_; not; if_then_else_)
open import Data.Integer    using (ℤ; +_; -[1+_]; _-_; ∣_∣; -_)
open import Data.Integer.DivMod using (_modℕ_)
open import Data.Fin        using (Fin; toℕ; #_)
open import Data.List       using (List; []; _∷_; foldl; map; reverse; length; _++_; take; drop)
open import Data.Nat        using (ℕ; zero; suc; _⊓_; _∸_) renaming (_≡ᵇ_ to _==_)
open import Data.Nat.DivMod using (_mod_)
open import Data.Sign       using (Sign)
open import Data.String     using (String; intersperse) renaming (_++_ to _++s_)
open import Data.Product    using (_×_; _,_; Σ; proj₁; proj₂)
open import Data.Vec        using (Vec; []; _∷_; lookup; replicate; _[_]%=_; toList; updateAt) renaming (map to vmap)

open import Pitch
open import Util using (allPairs; ◯pairs; firstPairs; _∘_)

-- Maximum number of interval classes (0 to 6).
ic7 : ℕ
ic7 = 7

PitchPair : Type
PitchPair = Pitch × Pitch

PCPair : Type
PCPair = PC × PC

-- Unordered pitch interval
-- Absolute distance in semitones between two pitches.
Upi : Type
Upi = ℕ

-- Ordered pitch interval
-- Relative distance in semitones between two pitches.
Opi : Type
Opi = ℤ

-- Interval Class
-- Also known as unodered pitch-class interval (upci).
IC : Type
IC = Fin ic7

-- (Ordered) pitch-class interval (also abbreviated opci)
PCI : Type
PCI = Fin s12

intervalWithinOctave : Upi → Upi
intervalWithinOctave i = toℕ (i mod s12)

absoluteInterval : Opi → Upi
absoluteInterval i = ∣ i ∣

makeSigned : Sign → Upi → Opi
makeSigned Sign.- zero    = + 0
makeSigned Sign.- (suc i) = -[1+ i ]
makeSigned Sign.+ i       = + i

-- Names for intervals
per1  = 0
min2  = 1
maj2  = 2
min3  = 3
maj3  = 4
per4  = 5
aug4  = 6
per5  = 7
min6  = 8
maj6  = 9
min7  = 10
maj7  = 11
per8  = 12
min9  = 13
maj9  = 14
min10 = 15
maj10 = 16
per11 = 17
aug11 = 18
per12 = 19

isConsonant : Upi → Bool
isConsonant iv =
  (i == per1)  ∨
  (i == min3)  ∨
  (i == maj3)  ∨
  (i == per5)  ∨
  (i == min6)  ∨
  (i == maj6)  ∨
  (i == per8)
  where i = intervalWithinOctave iv

isDissonant : Upi → Bool
isDissonant = not ∘ isConsonant

isPerfect : Upi → Bool
isPerfect iv =
  (i == per1)  ∨
  (i == per4)  ∨
  (i == per5)  ∨
  (i == per8)
  where i = intervalWithinOctave iv

isUnison : Upi → Bool
isUnison i = i == per1

isThird : Upi → Bool
isThird i = (i == min3) ∨ (i == maj3)

-- Half or whole step.
isStep : Upi → Bool
isStep i =
  (i == min2)  ∨
  (i == maj2)

PitchInterval : Type
PitchInterval = Pitch × Upi

pitchIntervalToPitchPair : PitchInterval → PitchPair
pitchIntervalToPitchPair (p , n) = (p , transposePitch (+ n)  p)

secondPitch : PitchInterval → Pitch
secondPitch = proj₂ ∘ pitchIntervalToPitchPair

pitchPairToOpi : PitchPair → Opi
pitchPairToOpi (p , q) = (+ q) - (+ p)

toIC : PCPair → IC
toIC (p , q) =
  let x = toℕ (∣ (+ (toℕ q)) - (+ (toℕ p)) ∣ mod s12)
  in x ⊓ (s12 ∸ x) mod ic7

toPCI : PCPair → PCI
toPCI (p , q) =
 (((+ (toℕ q)) - (+ (toℕ p))) modℕ s12) mod s12

-- Assumes p ≤ q
toPitchInterval : PitchPair → PitchInterval
toPitchInterval pq = proj₁ pq , absoluteInterval (pitchPairToOpi pq)

-- DEPRECATED? Note that the first and last pitches are compared in normal order, not circular order.
◯pcIntervals : List PC → List PCI
◯pcIntervals = map toPCI ∘ ◯pairs

-- Note that the first and last pitches are compared in normal order, not circular order.
pcIntervals : List PC → List PCI
pcIntervals = map toPCI ∘ reverse ∘ firstPairs

stepUp : Pitch → Pitch → Bool
stepUp p q with pitchPairToOpi (p , q)
... | +_     n = isStep n
... | -[1+_] n = false

stepDown : Pitch → Pitch → Bool
stepDown p q with pitchPairToOpi (p , q)
... | +_     n = false
... | -[1+_] n = isStep n

-- Check if q is a passing tone between p and r
-- The interval between end points need to be a 3rd
isPassingTone : Pitch → Pitch → Pitch → Bool
isPassingTone p q r =
  (stepUp p q ∧ stepUp q r) ∨ (stepDown p q ∧ stepDown q r) ∨
  (isThird (absoluteInterval (pitchPairToOpi (p , r))))

moveUp : Pitch → Pitch → Bool
moveUp p q with pitchPairToOpi (p , q)
... | +_     _ = true
... | -[1+_] _ = false

moveDown : Pitch → Pitch → Bool
moveDown p q = not (moveUp p q)

-- Check if q is left by step in the opposite direction from its approach
isOppositeStep : Pitch → Pitch → Pitch → Bool
isOppositeStep p q r = (moveUp p q ∧ stepDown q r) ∨ (moveDown p q ∧ stepUp q r)

transposePitchInterval : Opi → Pitch → Pitch
transposePitchInterval z p = transposePitch z p

-- transpose pitch class by pci
Tpci : PCI → PC → PC
Tpci n = Tp (toℕ n)

----------

-- Interval Class Vector
ICV : Type
ICV = Vec ℕ ic7

emptyICV : ICV
emptyICV = 0 ∷ 0 ∷ 0 ∷ 0 ∷ 0 ∷ 0 ∷ 0 ∷ []

icVector : List PC → ICV
icVector pcs =
  foldl
    (λ icv pc → updateAt (toIC pc) suc icv)
    (updateAt (# 0) (λ _ → length pcs) emptyICV)
    (allPairs pcs)

----------

--Construct matrix out of PC row
matrix : List PC → List (List PC)
matrix [] = []
matrix pcs@(pc ∷ _) =
  let r0 = map ((Tpci ∘ Ip) pc) pcs -- start first row at 0
  in map (λ p → map ((Tpci ∘ Ip) p) r0) r0

showMatrix : List (List PC) → String
showMatrix m = intersperse "\n" (map showPCs m)

{-
rr : List PC
rr = # 10 ∷ # 9 ∷ # 7 ∷ # 0 ∷ []
rp = rr ++ map (Tp 4) rr ++ map (Tp 8) rr

-- Belle's matrix
aa = showMatrix (matrix rp)

0 b 9 2 4 3 1 6 8 7 5 a
1 0 a 3 5 4 2 7 9 8 6 b
3 2 0 5 7 6 4 9 b a 8 1
a 9 7 0 2 1 b 4 6 5 3 8
8 7 5 a 0 b 9 2 4 3 1 6
9 8 6 b 1 0 a 3 5 4 2 7
b a 8 1 3 2 0 5 7 6 4 9
6 5 3 8 a 9 7 0 2 1 b 4
4 3 1 6 8 7 5 a 0 b 9 2
5 4 2 7 9 8 6 b 1 0 a 3
7 6 4 9 b a 8 1 3 2 0 5
2 1 b 4 6 5 3 8 a 9 7 0

rd : List PC
rd2 = reverse (map (Tp 4) rr)
rd3' = reverse (map (Tp 8) rr)
rd3 = reverse (take 2 rd3') ++ reverse (drop 2 rd3')
rd = rr ++ rd2 ++ rd3

-- Dan's matrix
ad = showMatrix (matrix rd)

0 b 9 2 6 1 3 4 5 a 8 7
1 0 a 3 7 2 4 5 6 b 9 8
3 2 0 5 9 4 6 7 8 1 b a
a 9 7 0 4 b 1 2 3 8 6 5
6 5 3 8 0 7 9 a b 4 2 1
b a 8 1 5 0 2 3 4 9 7 6
9 8 6 b 3 a 0 1 2 7 5 4
8 7 5 a 2 9 b 0 1 6 4 3
7 6 4 9 1 8 a b 0 5 3 2
2 1 b 4 8 3 5 6 7 0 a 9
4 3 1 6 a 5 7 8 9 2 0 b
5 4 2 7 b 6 8 9 a 3 1 0
-}

max_stars_repo_name: halfaya/MusicTools

max_issues_repo_name: halfaya/MusicTools

max_forks_repo_name: halfaya/MusicTools


text:
{-# OPTIONS --without-K #-}
open import HoTT.Base
open import HoTT.Equivalence
open import HoTT.Identity.Pi
open import HoTT.Identity.Product

module HoTT.Product.Universal where

×-univ : ∀ {i j k} {X : 𝒰 i} (A : X → 𝒰 j) (B : X → 𝒰 k) →
         ((c : X) → A c × B c) ≃ Π X A × Π X B
×-univ {X = X} A B = let open Iso in iso→eqv λ where
  .f f → pr₁ ∘ f , pr₂ ∘ f
  .g f x → pr₁ f x , pr₂ f x
  .η f → funext (×-uniq ∘ f)
  .ε f → ×-pair⁼ (refl , refl)

max_stars_repo_name: michaelforney/hott

max_issues_repo_name: michaelforney/hott

max_forks_repo_name: michaelforney/hott


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

module Spaces.Spheres where

open import Base
open import Spaces.Suspension public

-- [Sⁿ n] is the sphere of dimension n
Sⁿ : ℕ → Set
Sⁿ 0 = bool
Sⁿ (S n) = suspension (Sⁿ n)

⋆Sⁿ : (n : ℕ) → Sⁿ n
⋆Sⁿ 0 = true
⋆Sⁿ (S n) = north (Sⁿ n)

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
-- Properties of natural number

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

-- agad-stdlib
open import Relation.Binary.PropositionalEquality

module TypeTheory.Nat.Properties
  {a}
  (N : Set a)
  (zero : N)
  (suc : N → N)
  (ind : ∀ {p} (P : N → Set p) → P zero → (∀ k → P k → P (suc k)) → ∀ n → P n)
  (ind-base : ∀ {p} (P : N → Set p) P-base P-step →
              ind P P-base P-step zero ≡ P-base)
  (ind-step : ∀ {p} (P : N → Set p) P-base P-step n →
              ind P P-base P-step (suc n) ≡ P-step n (ind P P-base P-step n))
  where

-- agda-stdlib
open import Axiom.UniquenessOfIdentityProofs
open import Level renaming (zero to lzero; suc to lsuc)
open import Data.Bool using (Bool; true; false)
open import Data.Empty
open import Data.Unit using (⊤ ; tt)
open import Data.Product
import Data.Product.Properties as Prodₚ
open import Data.Sum as Sum
open import Function.Base
import Relation.Binary as B
open import Relation.Nullary
import Relation.Nullary.Decidable as NDec

-- agda-misc
open import TypeTheory.Nat.Operations N zero suc ind ind-base ind-step

open ≡-Reasoning

private
  variable
    A : Set a

-- Properties of rec
rec-base : ∀ {A : Set a} (z : A) s → rec z s zero ≡ z
rec-base {A} z s = ind-base (λ _ → A) z λ k x → s x

rec-step : ∀ {A : Set a} (z : A) s n → rec z s (suc n) ≡ s (rec z s n)
rec-step {A} z s n = ind-step (λ _ → A) z (λ k x → s x) n

ind2-zz : ∀ {p} (P : N → N → Set p) Pzz Pmn→Pms Pmn→Psn →
  ind2 P Pzz Pmn→Pms Pmn→Psn zero zero ≡ Pzz
ind2-zz P Pzz Pmn→Pms Pmn→Psn = begin
  ind2 P Pzz Pmn→Pms Pmn→Psn zero zero
    ≡⟨⟩
  ind
      (λ o → P o zero)
      (ind (λ p → P zero p) Pzz (λ k Pzk → Pmn→Pms zero k Pzk) zero)
      (λ k Pkn → ind (λ r → P (suc k) r) (( λ k → ind (λ x → P x zero) Pzz (λ k₂ Pk₂zero → Pmn→Psn k₂ zero Pk₂zero) k) (suc k))
        (λ k₁ P[1+k,k₁] → Pmn→Pms (suc k) k₁ P[1+k,k₁]) zero)
      zero
    ≡⟨ ind-base _ _ _ ⟩
  ind (λ p → P zero p) Pzz (Pmn→Pms zero) zero
    ≡⟨ ind-base _ _ _ ⟩
  Pzz
    ∎
  where open ≡-Reasoning

---------------------------------------------------------------------------
-- Properties of pred

pred-zero : pred zero ≡ zero
pred-zero = ind-base (λ _ → N) zero (λ k x → k)

pred-suc : ∀ n → pred (suc n) ≡ n
pred-suc n = ind-step (λ _ → N) zero (λ k x → k) n

-- Properties of suc
suc-injective : ∀ {m n} → suc m ≡ suc n → m ≡ n
suc-injective {m} {n} 1+m≡1+n = begin
  m            ≡⟨ sym $ pred-suc m ⟩
  pred (suc m) ≡⟨ cong pred 1+m≡1+n ⟩
  pred (suc n) ≡⟨ pred-suc n ⟩
  n            ∎

-- Properties of caseNat
caseNat-base : ∀ {l} {A : Set l} (z s : A) → caseNat z s zero ≡ z
caseNat-base z s = ind-base (λ x → _) z λ k x → s

caseNat-step : ∀ {l} {A : Set l} (z s : A) n → caseNat z s (suc n) ≡ s
caseNat-step z s n = ind-step (λ x → _) z (λ k x → s) n

NotZero : ∀ n → Set
NotZero n = caseNat ⊥ ⊤ n

NotZero[zero]≡⊥ : NotZero zero ≡ ⊥
NotZero[zero]≡⊥ = caseNat-base ⊥ ⊤

NotZero[suc[n]]≡⊤ : ∀ n → NotZero (suc n) ≡ ⊤
NotZero[suc[n]]≡⊤ n = caseNat-step ⊥ ⊤ n

private
  transport : ∀ {a} {A B : Set a} → A ≡ B → A → B
  transport eq = subst id eq

NotZero[suc[n]] : ∀ (n : N) → NotZero (suc n)
NotZero[suc[n]] n = transport (sym $ NotZero[suc[n]]≡⊤ n) tt

s≢z : ∀ (n : N) → suc n ≢ zero
s≢z n eq = transport NotZero[zero]≡⊥ $ subst NotZero eq (NotZero[suc[n]] n)

z≢s : ∀ (n : N) → zero ≢ suc n
z≢s n eq = s≢z n (sym eq)

1+n≢n : ∀ n → suc n ≢ n
1+n≢n n = ind (λ x → suc x ≢ x) (s≢z zero)
  (λ k 1+k≢k 1+[1+k]≡1+k → 1+k≢k (suc-injective 1+[1+k]≡1+k)) n

caseNat-extract-zero : ∀ {l} {A : Set l} (z s : A) n →
                       z ≢ s →
                       caseNat z s n ≡ z → n ≡ zero
caseNat-extract-zero z s n z≢s =
  ind (λ k → caseNat z s k ≡ z → k ≡ zero)
      (λ x → refl)
      (λ k c[z,s,k]≡z→k≡zero c[z,s,suc[k]]≡z → ⊥-elim $ z≢s
        $ trans (sym c[z,s,suc[k]]≡z) (caseNat-step _ _ _) ) n

-- Properties of _+_
+-identityˡ : ∀ n → zero + n ≡ n
+-identityˡ n = rec-base n suc

suc-+ : ∀ m n → suc m + n ≡ suc (m + n)
suc-+ m n = rec-step n suc m

+-identityʳ : ∀ n → n + zero ≡ n
+-identityʳ n₀ = ind (λ n → n + zero ≡ n) (+-identityˡ zero) step n₀
  where
  step : ∀ k → k + zero ≡ k → suc k + zero ≡ suc k
  step k k+zero≡k = begin
    suc k + zero   ≡⟨ suc-+ k zero ⟩
    suc (k + zero) ≡⟨ cong suc k+zero≡k ⟩
    suc k          ∎

+-assoc : ∀ m n o → (m + n) + o ≡ m + (n + o)
+-assoc m₀ n o = ind (λ m → (m + n) + o ≡ m + (n + o)) base step m₀
  where
  base : (zero + n) + o ≡ zero + (n + o)
  base = begin
    (zero + n) + o ≡⟨ cong (_+ o) $ +-identityˡ n ⟩
    n + o          ≡⟨ sym $ +-identityˡ (n + o) ⟩
    zero + (n + o) ∎

  step : ∀ k → (k + n) + o ≡ k + (n + o) → (suc k + n) + o ≡ suc k + (n + o)
  step k [k+n]+o≡k+[n+o] = begin
    (suc k + n) + o   ≡⟨ cong (_+ o) $ suc-+ k n ⟩
    suc (k + n) + o   ≡⟨ suc-+ (k + n) o ⟩
    suc ((k + n) + o) ≡⟨ cong suc [k+n]+o≡k+[n+o] ⟩
    suc (k + (n + o)) ≡⟨ sym $ suc-+ k (n + o) ⟩
    suc k + (n + o)   ∎

suc≡one+ : ∀ n → suc n ≡ one + n
suc≡one+ n = begin
  suc n          ≡⟨ cong suc (sym $ +-identityˡ n) ⟩
  suc (zero + n) ≡⟨ sym $ suc-+ zero n ⟩
  suc zero + n   ∎

+-suc : ∀ m n → m + suc n ≡ suc m + n
+-suc m₀ n = ind (λ m → m + suc n ≡ suc m + n)
   (begin
    zero + suc n   ≡⟨ +-identityˡ (suc n) ⟩
    suc n          ≡⟨ cong suc (sym $ +-identityˡ n) ⟩
    suc (zero + n) ≡⟨ sym $ suc-+ zero n ⟩
    suc zero + n   ∎
    )
  (λ m m+[1+n]≡[1+m]+n → begin
    suc m + suc n   ≡⟨ suc-+ m (suc n) ⟩
    suc (m + suc n) ≡⟨ cong suc m+[1+n]≡[1+m]+n ⟩
    suc (suc m + n) ≡⟨ sym $ suc-+ (suc m) n ⟩
    suc (suc m) + n ∎
    )
  m₀

+-comm : ∀ m n → m + n ≡ n + m
+-comm m₀ n =
  ind (λ m → m + n ≡ n + m)
      (begin
        zero + n ≡⟨ +-identityˡ n ⟩
        n        ≡⟨ sym $ +-identityʳ n ⟩
        n + zero ∎
        )
      (λ m m+n≡n+m → begin
        suc m + n   ≡⟨ suc-+ m n ⟩
        suc (m + n) ≡⟨ cong suc m+n≡n+m ⟩
        suc (n + m) ≡⟨ sym $ suc-+ n m ⟩
        suc n + m   ≡⟨ sym $ +-suc n m ⟩
        n + suc m   ∎
        )
      m₀

+-cancelˡ-≡ : ∀ m n o → (m + n) ≡ (m + o) → n ≡ o
+-cancelˡ-≡ m n o =
  ind (λ k → k + n ≡ k + o → n ≡ o)
      (λ zero+n≡zero+o → begin
          n        ≡⟨ sym $ +-identityˡ n ⟩
          zero + n ≡⟨ zero+n≡zero+o ⟩
          zero + o ≡⟨ +-identityˡ o ⟩
          o ∎)
      (λ k k+n≡k+o→n≡o suck+n≡suck+o → begin
         n ≡⟨ k+n≡k+o→n≡o $ suc-injective $ (begin
            suc (k + n) ≡⟨ sym $ suc-+ k n ⟩
            suc k + n   ≡⟨ suck+n≡suck+o ⟩
            suc k + o   ≡⟨ suc-+ k o ⟩
            suc (k + o) ∎
           ) ⟩
         o ∎)
      m

+-cancelʳ-≡ : ∀ m n o → (m + n) ≡ (o + n) → m ≡ o
+-cancelʳ-≡ m n o m+n≡o+n = +-cancelˡ-≡ n m o (begin
  n + m ≡⟨ +-comm n m ⟩
  m + n ≡⟨ m+n≡o+n ⟩
  o + n ≡⟨ +-comm o n ⟩
  n + o ∎)

+-conicalˡ : ∀ m n → m + n ≡ zero → m ≡ zero
+-conicalˡ m n =
  ind (λ k → k + n ≡ zero → k ≡ zero) (λ _ → refl)
      (λ k k+n≡zero→k≡zero suck+n≡zero →
          ⊥-elim $ z≢s (k + n) $ trans (sym suck+n≡zero) (suc-+ k n))
      m

+-conicalʳ : ∀ m n → m + n ≡ zero → n ≡ zero
+-conicalʳ m n m+n≡zero = +-conicalˡ n m (trans (+-comm n m) m+n≡zero)

-- Order
z≤n : ∀ {n} → zero ≤ n
z≤n {n} = n , +-identityˡ n

s≤s : ∀ {m n} → m ≤ n → suc m ≤ suc n
s≤s {m} {n} (o , m+o≡n) = o , trans (suc-+ m o) (cong suc m+o≡n)

≤-pred : ∀ {m n} → suc m ≤ suc n → m ≤ n
≤-pred {m} {n} (o , sucm+o≡sucn) =
  o , suc-injective (trans (sym $ suc-+ m o) sucm+o≡sucn)

≤-refl : ∀ {n} → n ≤ n
≤-refl {n} = ind (λ n → n ≤ n) z≤n (λ k → s≤s) n

≤-reflexive : ∀ {m n} → m ≡ n → m ≤ n
≤-reflexive {m} {n} m≡n = subst (m ≤_) m≡n (≤-refl {m})

≤-step : ∀ {m n} → m ≤ n → m ≤ suc n
≤-step {m} {n} (o , m+o≡n) = suc o , (begin
  m + suc o   ≡⟨ +-suc m o ⟩
  suc m + o   ≡⟨ suc-+ m o ⟩
  suc (m + o) ≡⟨ cong suc m+o≡n ⟩
  suc n       ∎)

≤-back : ∀ {m n} → suc m ≤ n → m ≤ n
≤-back {m} {n} (o , suc[m]+o≡n) = suc o , (begin
  m + suc o ≡⟨ +-suc m o ⟩
  suc m + o ≡⟨ suc[m]+o≡n ⟩
  n ∎)

≤-steps : ∀ {m n} o → m ≤ n → m ≤ o + n
≤-steps {m} {n} o m≤n =
  ind (λ k → m ≤ k + n)
      (subst (m ≤_) (sym $ +-identityˡ n) m≤n)
      (λ k m≤k+n → subst (m ≤_) (sym $ suc-+ k n) (≤-step m≤k+n))
      o

≤-antisym : ∀ {m n} → m ≤ n → n ≤ m → m ≡ n
≤-antisym {m} {n} (o , m+o≡n) (p , n+p≡m) = begin
  m        ≡⟨ sym n+p≡m ⟩
  n + p    ≡⟨ cong (n +_) $ p≡zero ⟩
  n + zero ≡⟨ +-identityʳ n ⟩
  n        ∎
  where
  m≡m+[o+p] : m ≡ m + (o + p)
  m≡m+[o+p] = begin
    m           ≡⟨ sym n+p≡m ⟩
    n + p       ≡⟨ cong (_+ p) $ sym m+o≡n ⟩
    (m + o) + p ≡⟨ +-assoc m o p ⟩
    m + (o + p) ∎
  zero≡o+p : zero ≡ o + p
  zero≡o+p = +-cancelˡ-≡ m zero (o + p) (begin
    m + zero    ≡⟨ +-identityʳ m ⟩
    m           ≡⟨ m≡m+[o+p] ⟩
    m + (o + p) ∎)
  p≡zero : p ≡ zero
  p≡zero = +-conicalʳ o p (sym zero≡o+p)

≤-trans : ∀ {m n o} → m ≤ n → n ≤ o → m ≤ o
≤-trans {m} {n} {o} (p , m+p≡n) (q , n+q≡o) = (p + q) , (begin
  m + (p + q) ≡⟨ sym $ +-assoc m p q ⟩
  (m + p) + q ≡⟨ cong (_+ q) m+p≡n ⟩
  n + q       ≡⟨ n+q≡o ⟩
  o           ∎)

n≤zero⇒n≡zero : ∀ {n} → n ≤ zero → n ≡ zero
n≤zero⇒n≡zero {n} (o , n+o≡zero) = +-conicalˡ n o n+o≡zero

-- +-mono-≤

zero<suc[n] : ∀ n → zero < suc n
zero<suc[n] n = s≤s z≤n

s<s : ∀ {m n} → m < n → suc m < suc n
s<s = s≤s

<-pred : ∀ {m n} → suc m < suc n → m < n
<-pred = ≤-pred

n≮zero : ∀ n → n ≮ zero
n≮zero n (m , sucn+m≡zero) = s≢z (n + m) $ trans (sym $ suc-+ n m) sucn+m≡zero

≤⇒≯ : ∀ {m n} → m ≤ n → m ≯ n
≤⇒≯  {m} {n} (o , m+o≡n) (p , suc[n]+p≡m) =
  s≢z (p + o) $ +-cancelˡ-≡ n (suc (p + o)) zero $ begin
  n + suc (p + o) ≡⟨ +-suc n (p + o) ⟩
  suc n + (p + o) ≡⟨ sym $ +-assoc (suc n) p o ⟩
  suc n + p + o   ≡⟨ cong (_+ o) $ suc[n]+p≡m ⟩
  m + o           ≡⟨ m+o≡n ⟩
  n               ≡⟨ sym $ +-identityʳ n ⟩
  n + zero        ∎

<⇒≱ : ∀ {m n} → m < n → m ≱ n
<⇒≱ {m} {n} m<n n≤m = ≤⇒≯ n≤m m<n

n≮n : ∀ n → n ≮ n
n≮n n (m , sucn+m≡n) = z≢s m $ +-cancelˡ-≡ n zero (suc m) (begin
  n + zero  ≡⟨ +-identityʳ n ⟩
  n         ≡⟨ sym sucn+m≡n ⟩
  suc n + m ≡⟨ sym $ +-suc n m ⟩
  n + suc m ∎)

<⇒≢ : ∀ {m n} → m < n → m ≢ n
<⇒≢ {m} {n} m<n m≡n = n≮n m (subst (m <_) (sym m≡n) m<n)

>⇒≢ : ∀ {m n} → m > n → m ≢ n
>⇒≢ {m} {n} m>n m≡n = <⇒≢ m>n (sym m≡n)

≤⇒<∨≡ : ∀ {m n} → m ≤ n → m < n ⊎ m ≡ n
≤⇒<∨≡ {m} {n} (o , m+o≡n) =
  ind (λ k → m + k ≡ n → m < n ⊎ m ≡ n)
      (λ m+zero≡n → inj₂ (trans (sym $ +-identityʳ m) m+zero≡n))
      (λ k _ m+suc[k]≡n → inj₁ (k , (begin
        suc m + k ≡⟨ sym $ +-suc m k ⟩
        m + suc k ≡⟨ m+suc[k]≡n ⟩
        n ∎)))
      o m+o≡n

<⇒≤ : ∀ {m n} → m < n → m ≤ n
<⇒≤ = ≤-back

n<suc[n] : ∀ n → n < suc n
n<suc[n] n = ≤-refl

<-step : ∀ {m} {n} → m < n → m < suc n
<-step {m} {n} m<n = ≤-step m<n

n∸zero≡n : ∀ n → n ∸ zero ≡ n
n∸zero≡n n = rec-base _ _

<⇒≯ : ∀ {m n} → m < n → m ≯ n
<⇒≯ {m} {n} m<n = ≤⇒≯ (<⇒≤ m<n)

m∸suc[n]≡pred[m∸n] : ∀ m n → m ∸ suc n ≡ pred (m ∸ n)
m∸suc[n]≡pred[m∸n] m n = rec-step _ _ _

zero∸n≡zero : ∀ n → zero ∸ n ≡ zero
zero∸n≡zero =
  ind (λ n → zero ∸ n ≡ zero) (n∸zero≡n zero)
      λ k zero∸k≡zero → (begin
        zero ∸ suc k    ≡⟨ m∸suc[n]≡pred[m∸n] zero k ⟩
        pred (zero ∸ k) ≡⟨ cong pred zero∸k≡zero ⟩
        pred zero       ≡⟨ pred-zero ⟩
        zero            ∎)

suc[m]∸suc[n]≡m∸n : ∀ m n → suc m ∸ suc n ≡ m ∸ n
suc[m]∸suc[n]≡m∸n m =
  ind (λ n → suc m ∸ suc n ≡ m ∸ n)
      (begin
        suc m ∸ suc zero    ≡⟨ m∸suc[n]≡pred[m∸n] (suc m) zero ⟩
        pred (suc m ∸ zero) ≡⟨ cong pred (n∸zero≡n (suc m)) ⟩
        pred (suc m)        ≡⟨ pred-suc m ⟩
        m                   ≡⟨ sym $ n∸zero≡n m ⟩
        m ∸ zero            ∎)
      λ k suc[m]∸suc[k]≡m∸k → begin
          suc m ∸ suc (suc k)  ≡⟨ m∸suc[n]≡pred[m∸n] (suc m) (suc k) ⟩
          pred (suc m ∸ suc k) ≡⟨ cong pred suc[m]∸suc[k]≡m∸k ⟩
          pred (m ∸ k)         ≡⟨ sym $ m∸suc[n]≡pred[m∸n] m k ⟩
          m ∸ suc k            ∎

m+n∸m≡n : ∀ m n → m + n ∸ m ≡ n
m+n∸m≡n m n =
  ind (λ k → (k + n) ∸ k ≡ n)
      (begin
        (zero + n) ∸ zero ≡⟨ cong (_∸ zero) $ +-identityˡ n ⟩
        n ∸ zero          ≡⟨ n∸zero≡n n ⟩
        n                 ∎)
      (λ k k+n∸k≡n → begin
          suc k + n ∸ suc k   ≡⟨ cong (_∸ suc k) $ suc-+ k n ⟩
          suc (k + n) ∸ suc k ≡⟨ suc[m]∸suc[n]≡m∸n (k + n) k ⟩
          k + n ∸ k           ≡⟨ k+n∸k≡n ⟩
          n                   ∎
        )
      m

m≤n⇒m+[n∸m]≡n : ∀ {m n} → m ≤ n → m + (n ∸ m) ≡ n
m≤n⇒m+[n∸m]≡n {m} {n} (o , m+o≡n) = begin
  m + (n ∸ m)     ≡⟨ cong (λ v → m + (v ∸ m)) (sym m+o≡n) ⟩
  m + (m + o ∸ m) ≡⟨ cong (m +_) $ m+n∸m≡n m o ⟩
  m + o           ≡⟨ m+o≡n ⟩
  n               ∎

m∸[m+n]≡zero : ∀ m n → m ∸ (m + n) ≡ zero
m∸[m+n]≡zero m n =
  ind (λ k → k ∸ (k + n) ≡ zero) (zero∸n≡zero (zero + n))
      (λ k k∸[k+n]≡zero → begin
        suc k ∸ (suc k + n) ≡⟨ cong (suc k ∸_) $ suc-+ k n ⟩
        suc k ∸ suc (k + n) ≡⟨ suc[m]∸suc[n]≡m∸n k (k + n) ⟩
        k ∸ (k + n)         ≡⟨ k∸[k+n]≡zero ⟩
        zero                ∎) m

m≤n⇒m∸n≡zero : ∀ {m n} → m ≤ n → m ∸ n ≡ zero
m≤n⇒m∸n≡zero {m} {n} (o , m+o≡n) = begin
  m ∸ n       ≡⟨ cong (m ∸_) (sym m+o≡n) ⟩
  m ∸ (m + o) ≡⟨ m∸[m+n]≡zero m o ⟩
  zero        ∎

pred[n]≡zero⇒n≡zero∨n≡one : ∀ n → pred n ≡ zero → n ≡ zero ⊎ n ≡ one
pred[n]≡zero⇒n≡zero∨n≡one =
  ind (λ n → pred n ≡ zero → n ≡ zero ⊎ n ≡ suc zero)
      (λ _ → inj₁ refl)
      λ k pred[k]≡zero→k≡zero∨k≡one pred[suc[k]]≡zero → inj₂
      (cong suc (trans (sym $ pred-suc k) pred[suc[k]]≡zero))

pred[m]≡suc[n]⇒m≡suc[suc[n]] : ∀ {m n} → pred m ≡ suc n → m ≡ suc (suc n)
pred[m]≡suc[n]⇒m≡suc[suc[n]] {m} {n} =
  ind (λ k → pred k ≡ suc n → k ≡ suc (suc n))
      (λ pred[zero]≡suc[n] → ⊥-elim $ z≢s n $ trans (sym pred-zero) pred[zero]≡suc[n] )
      (λ k _ pred[suc[k]]≡suc[n] →
          cong suc (trans (sym $ pred-suc k) pred[suc[k]]≡suc[n]))
      m

≤⇒≤ᵇ : ∀ {m n} → m ≤ n → m ≤ᵇ n ≡ true
≤⇒≤ᵇ {m} {n} (o , m+o≡n) = begin
  caseNat true false (m ∸ n)
    ≡⟨ cong (λ v → caseNat true false (m ∸ v)) $ sym m+o≡n ⟩
  caseNat true false (m ∸ (m + o))
    ≡⟨ cong (caseNat true false) $ m∸[m+n]≡zero m o ⟩
  caseNat true false zero
    ≡⟨ caseNat-base true false ⟩
  true
    ∎

data Order (m n : N) : Set a where
  lt : (m<n : m < n) → Order m n
  eq : (m≡n : m ≡ n) → Order m n
  gt : (m>n : m > n) → Order m n

private
  order?-zero : ∀ n → Order zero n
  order?-zero = ind (λ n → Order zero n) (eq refl) λ k _ → lt (zero<suc[n] k)

  order?-suc : ∀ n k → Order k n → Order (suc k) n
  order?-suc n k (lt k<n) with ≤⇒<∨≡ k<n
  ... | inj₁ suc[k]<n     = lt suc[k]<n
  ... | inj₂ suc[k]≡n     = eq suc[k]≡n
  order?-suc n k (eq k≡n) = gt (subst (_< suc k) k≡n $ n<suc[n] k)
  order?-suc n k (gt k>n) = gt (<-step k>n)

order? : ∀ m n → Order m n
order? m₀ n₀ =
  ind (λ k → Order k n₀) (order?-zero n₀) (λ k → order?-suc n₀ k) m₀

_≟_ : ∀ m n → Dec (m ≡ n)
m ≟ n with order? m n
... | lt m<n = no (<⇒≢ m<n)
... | eq m≡n = yes m≡n
... | gt m>n = no (>⇒≢ m>n)

≡-irrelevant : ∀ {m n : N} (p q : m ≡ n) → p ≡ q
≡-irrelevant = M.≡-irrelevant
  where module M = Decidable⇒UIP _≟_

≤-irrelevant : ∀ {m n : N} (p q : m ≤ n) → p ≡ q
≤-irrelevant {m} {n} (o , m+o≡n) (p , m+p≡n)
  with +-cancelˡ-≡ m o p (trans m+o≡n (sym m+p≡n))
... | refl = cong (o ,_) (≡-irrelevant m+o≡n m+p≡n)

≤-proj₁-≡ : ∀ {m n : N} (p q : m ≤ n) → proj₁ p ≡ proj₁ q
≤-proj₁-≡ p q = Prodₚ.,-injectiveˡ (≤-irrelevant p q)

≰⇒> : ∀ {m n} → m ≰ n → m > n
≰⇒> {m} {n} m≰n with order? m n
... | lt m<n = ⊥-elim $ m≰n (<⇒≤ m<n)
... | eq m≡n = ⊥-elim $ m≰n (≤-reflexive m≡n)
... | gt m>n = m>n

≮⇒≥ : ∀ {m n} → m ≮ n → m ≥ n
≮⇒≥ {m} {n} m≮n with order? m n
... | lt m<n = ⊥-elim $ m≮n m<n
... | eq m≡n = ≤-reflexive (sym m≡n)
... | gt m>n = <⇒≤ m>n

_≤?_ : ∀ m n → Dec (m ≤ n)
m ≤? n with order? m n
... | lt m<n = yes (<⇒≤ m<n)
... | eq m≡n = yes (≤-reflexive m≡n)
... | gt m>n = no λ m≤n → ≤⇒≯ m≤n m>n

_<?_ : ∀ m n → Dec (m < n)
m <? n with order? m n
... | lt m<n = yes m<n
... | eq m≡n = no λ m<n → <⇒≢ m<n m≡n
... | gt m>n = no λ m<n → <⇒≯ m<n m>n

≤∧≢⇒< : ∀ {m n} → m ≤ n → m ≢ n → m < n
≤∧≢⇒< {m} {n} m≤n m≢n with order? m n
... | lt m<n = m<n
... | eq m≡n = ⊥-elim $ m≢n m≡n
... | gt m>n = ⊥-elim $ ≤⇒≯ m≤n m>n

private
  subst-refl : ∀ {a b} {A : Set a} (B : A → Set b) {x : A} (y : B x) →
               subst B refl y ≡ y
  subst-refl _ _ = refl

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

  subst-cong-app : ∀ {a b c} {A : Set a} {B : Set b} {C : B → Set c}
                   (g : A → B) (f : (x : A) → C (g x)) {x y} (x≡y : x ≡ y) →
                   subst C (cong g x≡y) (f x) ≡ f y
  subst-cong-app {C = C} g f {x} {y} x≡y = begin
    subst C (cong g x≡y) (f x) ≡⟨ sym $ subst-∘ x≡y ⟩
    subst (C ∘ g) x≡y (f x)    ≡⟨ subst-app f x≡y ⟩
    f y                        ∎

  subst-other : ∀ {a b} {A : Set a} {B : A → Set b}
                (f : (x : A) → B x) {x y z} (x≡z : x ≡ z) (y≡z : y ≡ z) →
                subst B x≡z (f x) ≡ subst B y≡z (f y)
  subst-other _ refl refl = refl

  subst-other-g : ∀ {a b c} {A : Set a} {B : Set b} {C : B → Set c} →
                  B.Irrelevant (_≡_ {A = B}) →
                  ∀ (g : A → B) (f : (x : A) → C (g x))
                  {x y z} (x≡y : x ≡ y) (gx≡z : g x ≡ z) (gy≡z : g y ≡ z) →
                  subst C gx≡z (f x) ≡ subst C gy≡z (f y)
  subst-other-g B-irrelevant g f refl refl gy≡z with B-irrelevant gy≡z refl
  subst-other-g B-irrelevant g f refl refl .refl | refl = refl

  -- stdlib
  -- variant of subst-application
  subst-lemma : ∀ {a₁ a₂ b₁ b₂} {A₁ : Set a₁} {A₂ : Set a₂}
                  {B₁ : A₁ → Set b₁} {B₂ : A₂ → Set b₂}
                  (f : A₁ → A₂) (g : ∀ x → B₁ x → B₂ (f x))
                  {x₁ x₂ : A₁} (x₁≡x₂ : x₁ ≡ x₂) {y : B₁ x₁} →
                  subst B₂ (cong f x₁≡x₂) (g x₁ y) ≡ g x₂ (subst B₁ x₁≡x₂ y)
  subst-lemma _ _ refl = refl

module _ {p} (P : N → N → Set p) where
  inddiag-< : (∀ n → P zero (suc n)) → (∀ m n → P m n → P (suc m) (suc n)) →
              ∀ m o → P m (suc m + o)
  inddiag-< Pzs Pss m o =
    ind (λ k → P k (suc k + o))
        (subst (P zero) (suc≡one+ o) (Pzs o))
        (λ k P[k,suc[k]+o] → subst (P (suc k)) (sym $ suc-+ (suc k) o)
          $ Pss k (suc k + o) P[k,suc[k]+o]) m

  inddiag-≡ : P zero zero → (∀ m n → P m n → P (suc m) (suc n)) → ∀ n → P n n
  inddiag-≡ Pzz Pss n = ind (λ k → P k k) Pzz (λ k Pkk → Pss k k Pkk) n

  inddiag-> : (∀ n → P (suc n) zero) → (∀ m n → P m n → P (suc m) (suc n)) →
              ∀ n o → P (suc n + o) n
  inddiag-> Psz Pss n o =
    ind (λ k → P (suc k + o) k)
        (subst (λ k → P k zero) (suc≡one+ o) (Psz o))
        (λ k P[suc[k]+o,k] → subst (λ v → P v (suc k)) (sym $ suc-+ (suc k) o)
          (Pss (suc k + o) k P[suc[k]+o,k]))
        n

  -- diagonal induction
  inddiag : P zero zero →
            (∀ n → P zero (suc n)) →
            (∀ m → P (suc m) zero) →
            (∀ m n → P m n → P (suc m) (suc n)) →
            ∀ m n → P m n
  inddiag P-zz P-zs P-sz P-ss m n with order? m n
  ... | lt (o , sm+o≡n) = subst (P m) sm+o≡n (inddiag-< P-zs P-ss m o)
  ... | eq m≡n          = subst (P m) m≡n (inddiag-≡ P-zz P-ss m)
  ... | gt (o , sn+o≡m) = subst (λ k → P k n) sn+o≡m (inddiag-> P-sz P-ss n o)

  inddiag-zz : ∀ Pzz Pzs Psz Pss → inddiag Pzz Pzs Psz Pss zero zero ≡ Pzz
  inddiag-zz Pzz Pzs Psz Pss with order? zero zero
  ... | lt m<n = ⊥-elim $ n≮n zero m<n
  ... | eq m≡n = begin
    subst (P zero) m≡n (ind (λ k → P k k) Pzz (λ k → Pss k k) zero)
      ≡⟨ cong (λ v → subst (P zero) v _ ) (≡-irrelevant m≡n refl) ⟩
    subst (P zero) refl (ind (λ k → P k k) Pzz (λ k → Pss k k) zero)
      ≡⟨ subst-refl (P zero) (ind (λ k → P k k) Pzz (λ k → Pss k k) zero) ⟩
    ind (λ k → P k k) Pzz (λ k → Pss k k) zero
      ≡⟨ ind-base _ _ _ ⟩
    Pzz
      ∎
  ... | gt m>n = ⊥-elim $ n≮n zero m>n

  inddiag-zs : ∀ Pzz Pzs Psz Pss n → inddiag Pzz Pzs Psz Pss zero (suc n) ≡ Pzs n
  inddiag-zs Pzz Pzs Psz Pss n with order? zero (suc n)
  ... | lt (o , one+o≡suc[n]) = begin
    subst (P zero) one+o≡suc[n] (inddiag-< Pzs Pss zero o)
      ≡⟨ cong (subst (P zero) one+o≡suc[n]) $ ind-base _ _ _ ⟩
    subst (P zero) one+o≡suc[n] (subst (P zero) (suc≡one+ o) (Pzs o))
      ≡⟨ subst-subst (suc≡one+ o) ⟩ -- suc o -> one + o -> suc n
    subst (P zero) so≡sn (Pzs o)
      ≡⟨ cong (λ v → subst (P zero) v (Pzs o)) $ ≡-irrelevant so≡sn (cong suc o≡n) ⟩
    subst (P zero) (cong suc o≡n) (Pzs o)
      ≡⟨ subst-cong-app suc Pzs o≡n ⟩
    Pzs n
      ∎
    where
    so≡sn : suc o ≡ suc n
    so≡sn = trans (suc≡one+ o) one+o≡suc[n]
    o≡n : o ≡ n
    o≡n = suc-injective so≡sn
  ... | eq m≡n = ⊥-elim $ z≢s n m≡n
  ... | gt m>n = ⊥-elim $ n≮zero (suc n) m>n

  inddiag-sz : ∀ Pzz Pzs Psz Pss m → inddiag Pzz Pzs Psz Pss (suc m) zero ≡ Psz m
  inddiag-sz Pzz Pzs Psz Pss m with order? (suc m) zero
  ... | lt m<n = ⊥-elim $ n≮zero (suc m) m<n
  ... | eq m≡n = ⊥-elim $ s≢z m m≡n
  ... | gt (o , one+o≡suc[m]) = begin
    subst (λ k → P k zero) one+o≡suc[m] (inddiag-> Psz Pss zero o)
      ≡⟨ cong (subst (λ k → P k zero) one+o≡suc[m]) $ ind-base _ _ _ ⟩
    subst (λ k → P k zero) one+o≡suc[m] (subst (λ k → P k zero) (suc≡one+ o) (Psz o))
      ≡⟨ subst-subst (suc≡one+ o) ⟩
    subst (λ k → P k zero) so≡sm (Psz o)
      ≡⟨ cong (λ v → subst (λ k → P k zero) v (Psz o)) $ ≡-irrelevant so≡sm (cong suc o≡m) ⟩
    subst (λ k → P k zero) (cong suc o≡m) (Psz o)
      ≡⟨ subst-cong-app suc Psz o≡m ⟩
    Psz m
      ∎
    where
    so≡sm = trans (suc≡one+ o) one+o≡suc[m]
    o≡m = suc-injective so≡sm

  inddiag-ss : ∀ Pzz Pzs Psz Pss m n →
    inddiag Pzz Pzs Psz Pss (suc m) (suc n) ≡
    Pss m n (inddiag Pzz Pzs Psz Pss m n)
  inddiag-ss Pzz Pzs Psz Pss m n with order? (suc m) (suc n) | order? m n
  ... | lt sm<sn@(o , ssm+o≡sn) | lt m<n@(p , sm+p≡n) =
    begin
    subst (P (suc m)) ssm+o≡sn (inddiag-< Pzs Pss (suc m) o)
      ≡⟨ cong (subst (P (suc m)) ssm+o≡sn) $ ind-step _ _ _ m ⟩
    subst (P (suc m)) ssm+o≡sn (subst (P (suc m)) (sym $ suc-+ (suc m) o) $
      Pss m (suc m + o) (inddiag-< Pzs Pss m o))
      ≡⟨ subst-subst (sym $ suc-+ (suc m) o) ⟩
    subst (P (suc m)) suc[sm+o]≡sn
      (Pss m (suc m + o) (inddiag-< Pzs Pss m o))
      ≡⟨ cong (λ v → subst (P (suc m)) v (Pss m (suc m + o) (inddiag-< Pzs Pss m o))) $
           ≡-irrelevant suc[sm+o]≡sn (cong suc sm+o≡n) ⟩
    subst (P (suc m)) (cong suc sm+o≡n) (Pss m (suc m + o) (inddiag-< Pzs Pss m o))
      ≡⟨ subst-lemma suc (Pss m) sm+o≡n ⟩
    Pss m n (subst (P m) sm+o≡n (inddiag-< Pzs Pss m o))
      ≡⟨ cong (Pss m n) $ subst-other-g ≡-irrelevant (suc m +_) (inddiag-< Pzs Pss m) o≡p sm+o≡n sm+p≡n ⟩
    Pss m n (subst (P m) sm+p≡n (inddiag-< Pzs Pss m p))
      ∎
    where
    suc[sm+o]≡sn : suc (suc m + o) ≡ suc n
    suc[sm+o]≡sn = trans (sym $ suc-+ (suc m) o) ssm+o≡sn
    sm+o≡n : suc m + o ≡ n
    sm+o≡n = suc-injective suc[sm+o]≡sn
    o≡p : o ≡ p
    o≡p = ≤-proj₁-≡ (<-pred sm<sn) m<n
  ... | lt sm<sn | eq m≡n = ⊥-elim $ <⇒≢ (<-pred sm<sn) m≡n
  ... | lt sm<sn | gt m>n = ⊥-elim $ <⇒≯ (<-pred sm<sn) m>n
  ... | eq sm≡sn | lt m<n = ⊥-elim $ <⇒≢ m<n (suc-injective sm≡sn)
  ... | eq sm≡sn | eq m≡n = begin
    subst (P (suc m)) sm≡sn (i (suc m))
      ≡⟨ cong (subst (P (suc m)) sm≡sn) $ ind-step _ _ _ m ⟩
    subst (P (suc m)) sm≡sn (Pss m m (i m))
      ≡⟨ cong (λ v → subst (P (suc m)) v (Pss m m (i m))) $ ≡-irrelevant sm≡sn (cong suc m≡n) ⟩
    subst (P (suc m)) (cong suc m≡n) (Pss m m (i m))
      ≡⟨ subst-lemma suc (Pss m) m≡n ⟩
    Pss m n (subst (P m) m≡n (i m))
      ∎
      where
      i = ind (λ k → P k k) Pzz (λ k → Pss k k)
  ... | eq sm≡sn | gt m>n = ⊥-elim $ >⇒≢ m>n (suc-injective sm≡sn)
  ... | gt sm>sn | lt m<n = ⊥-elim $ <⇒≯ (<-pred sm>sn) m<n
  ... | gt sm>sn | eq m≡n = ⊥-elim $ >⇒≢ (<-pred sm>sn) m≡n
  ... | gt sm>sn@(o , ssn+o≡sm) | gt m>n@(p , sn+p≡m) = begin
    subst B₁ ssn+o≡sm (inddiag-> Psz Pss (suc n) o)
      ≡⟨ cong (subst B₁ ssn+o≡sm) $ ind-step _ _ _ n ⟩
    subst B₁ ssn+o≡sm (subst B₁ (sym $ suc-+ (suc n) o) (Pss (suc n + o) n u))
      ≡⟨ subst-subst (sym $ suc-+ (suc n) o) ⟩
    subst B₁ suc[sn+o]≡sm (Pss (suc n + o) n u)
      ≡⟨ cong (λ v → subst B₁ v (Pss (suc n + o) n u)) $ ≡-irrelevant suc[sn+o]≡sm (cong suc sn+o≡m) ⟩
    subst B₁ (cong suc sn+o≡m) (Pss (suc n + o) n u)
      ≡⟨ subst-lemma suc (λ k → Pss k n) sn+o≡m ⟩
    Pss m n (subst B₂ sn+o≡m (inddiag-> Psz Pss n o))
      ≡⟨ cong (Pss m n) $ subst-other-g ≡-irrelevant (suc n +_) (inddiag-> Psz Pss n) o≡p sn+o≡m sn+p≡m ⟩
    Pss m n (subst B₂ sn+p≡m (inddiag-> Psz Pss n p))
      ∎
    where
    B₁ = λ k → P k (suc n)
    B₂ = λ k → P k n
    u = inddiag-> Psz Pss n o
    suc[sn+o]≡sm : suc (suc n + o) ≡ suc m
    suc[sn+o]≡sm = trans (sym $ suc-+ (suc n) o) ssn+o≡sm
    sn+o≡m = suc-injective suc[sn+o]≡sm
    o≡p : o ≡ p
    o≡p = ≤-proj₁-≡ (<-pred sm>sn) m>n


text:
-- Andreas, 2012-07-31 no eager introduction of hidden abstractions
{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.conv.coerce:100 #-}
-- {-# OPTIONS -v tc.with:100 #-}
module Issue679 where

data Unit : Set where
  unit : Unit

-- works also now:
test : {u : Unit} → Unit
test = λ {u} → u

T : Unit → Set
T unit = {u : Unit} → Unit

works : (u : Unit) → T u
works unit = λ {u} → u

fails : (u : Unit) → T u
fails unit with unit
... | _ = λ {u} → u

-- Error was:
-- {u : _14 _} → _16 _ !=< Unit of type Set
-- when checking that the expression λ {u} → u has type Unit

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
------------------------------------------------------------------------
-- The two definitions of substitutions are isomorphic (assuming
-- extensionality)
------------------------------------------------------------------------

open import Data.Universe.Indexed

module deBruijn.Substitution.Isomorphic
  {i u e} {Uni : IndexedUniverse i u e} where

import Axiom.Extensionality.Propositional as E
import deBruijn.Context; open deBruijn.Context Uni
open import deBruijn.Substitution.Data.Basics as D using (ε; _▻_; [_])
open import deBruijn.Substitution.Function.Basics as F
  using (ε⇨; _▻⇨_) renaming (_▻⇨[_]_ to _▻⇨[_]F_)
open import Function using (_$_)
open import Function.Inverse using (Inverse)
open import Level using (_⊔_)
import Relation.Binary.PropositionalEquality as P

open P.≡-Reasoning

isomorphic :
  ∀ {t} {T : Term-like t} →
  E.Extensionality (i ⊔ u ⊔ e) (i ⊔ u ⊔ e ⊔ t) →
  ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} →
  Inverse ([ Var ⟶ T ]-setoid ρ̂) (P.setoid $ D.Sub T ρ̂)
isomorphic {T = T} ext = record
  { to         = record { _⟨$⟩_ = to _
                        ; cong  = λ ρ₁≅ρ₂ → D.≅-⇨-⇒-≡ $ to-cong ρ₁≅ρ₂
                        }
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = from∘to _
    ; right-inverse-of = λ ρ → D.≅-⇨-⇒-≡ $ to∘from ρ
    }
  }
  where
  to : ∀ Γ {Δ} {ρ̂ : Γ ⇨̂ Δ} → F.Sub T ρ̂ → D.Sub T ρ̂
  to ε               ρ = ε
  to (Γ ▻ σ) {ρ̂ = ρ̂} ρ =
    P.subst (λ v → D.Sub T (t̂ail ρ̂ ▻̂ v))
            (≅-Value-⇒-≡ $ P.sym $ F.head-lemma ρ)
            (to Γ (F.tail ρ) ▻ F.head ρ)

  from : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} → D.Sub T ρ̂ → F.Sub T ρ̂
  from ε       = ε⇨
  from (ρ ▻ t) = from ρ ▻⇨ t

  to-▻ : ∀ {Γ Δ σ} {ρ̂ : Γ ▻ σ ⇨̂ Δ} (ρ : F.Sub T ρ̂) →
         D._≅-⇨_ (to (Γ ▻ σ) ρ) (to Γ (F.tail ρ) ▻ F.head ρ)
  to-▻ {ρ̂ = ρ̂} ρ =
    D.drop-subst-Sub (λ v → t̂ail ρ̂ ▻̂ v)
                     (≅-Value-⇒-≡ $ P.sym $ F.head-lemma ρ)

  abstract

    to-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : F.Sub T ρ̂₁}
                {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : F.Sub T ρ̂₂} →
              F._≅-⇨_ ρ₁ ρ₂ → D._≅-⇨_ (to Γ₁ ρ₁) (to Γ₂ ρ₂)
    to-cong {Γ₁ = ε}     {ρ₁ = _ , _} {ρ₂ = ._ , _}     [ P.refl ] = P.refl
    to-cong {Γ₁ = Γ ▻ σ} {ρ₁ = ρ₁}    {ρ₂ = ._ , corr₂} [ P.refl ] =
      let ρ₂ = [_⟶_].function ρ₁ , corr₂ in begin
       [ to (Γ ▻ σ) ρ₁                ]  ≡⟨ to-▻ ρ₁ ⟩
       [ to Γ (F.tail ρ₁) ▻ F.head ρ₁ ]  ≡⟨ D.▻⇨-cong P.refl (to-cong [ P.refl ]) P.refl ⟩
       [ to Γ (F.tail ρ₂) ▻ F.head ρ₂ ]  ≡⟨ P.sym $ to-▻ ρ₂ ⟩
       [ to (Γ ▻ σ) ρ₂                ]  ∎

  from-cong : ∀ {Γ₁ Δ₁} {ρ̂₁ : Γ₁ ⇨̂ Δ₁} {ρ₁ : D.Sub T ρ̂₁}
                {Γ₂ Δ₂} {ρ̂₂ : Γ₂ ⇨̂ Δ₂} {ρ₂ : D.Sub T ρ̂₂} →
              D._≅-⇨_ ρ₁ ρ₂ → F._≅-⇨_ (from ρ₁) (from ρ₂)
  from-cong P.refl = [ P.refl ]

  abstract

    from∘to : ∀ Γ {Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : F.Sub T ρ̂) →
              F._≅-⇨_ (from (to Γ ρ)) ρ
    from∘to ε ρ =
      ε⇨  ≅-⟶⟨ sym-⟶ $ F.ηε ext ρ ⟩
      ρ   ∎-⟶
    from∘to (Γ ▻ σ) {ρ̂ = ρ̂} ρ =
      from (to (Γ ▻ σ) ρ)                 ≅-⟶⟨ from-cong $ to-▻ ρ ⟩
      from (to Γ (F.tail ρ) ▻ F.head ρ)   ≅-⟶⟨ _ ∎-⟶ ⟩
      from (to Γ (F.tail ρ)) ▻⇨ F.head ρ  ≅-⟶⟨ F.▻⇨-cong P.refl (from∘to Γ (F.tail ρ)) P.refl ⟩
      F.tail ρ ▻⇨ F.head ρ                ≅-⟶⟨ sym-⟶ $ F.η▻ ext ρ ⟩
      ρ                                   ∎-⟶

    to∘from : ∀ {Γ Δ} {ρ̂ : Γ ⇨̂ Δ} (ρ : D.Sub T ρ̂) →
              D._≅-⇨_ (to Γ (from ρ)) ρ
    to∘from ε                 = P.refl
    to∘from (_▻_ {σ = σ} ρ t) = begin
      [ to (_ ▻ _) (from ρ ▻⇨ t)            ]  ≡⟨ to-▻ (from ρ ▻⇨ t) ⟩
      [ to _ (F.tail (from ρ ▻⇨[ σ ]F t)) ▻
        F.head (from ρ ▻⇨[ σ ]F t)          ]  ≡⟨ D.▻⇨-cong P.refl (to-cong [ P.refl ]) P.refl ⟩
      [ to _ (from ρ) ▻ t                   ]  ≡⟨ D.▻⇨-cong P.refl (to∘from ρ) P.refl ⟩
      [ ρ ▻ t                               ]  ∎

max_stars_repo_name: nad/dependently-typed-syntax

max_issues_repo_name: nad/dependently-typed-syntax

max_forks_repo_name: nad/dependently-typed-syntax