text:
{-# OPTIONS --safe #-}
module Cubical.HITs.Sn.Properties where

open import Cubical.Foundations.Pointed
open import Cubical.Foundations.Path
open import Cubical.Foundations.Function
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Univalence
open import Cubical.HITs.S1 renaming (_·_ to _*_)
open import Cubical.Data.Nat hiding (elim)
open import Cubical.Data.Sigma
open import Cubical.HITs.Sn.Base
open import Cubical.HITs.Susp
open import Cubical.HITs.Truncation
-- open import Cubical.Homotopy.Loopspace
open import Cubical.Homotopy.Connected
open import Cubical.HITs.Join
open import Cubical.Data.Bool

private
  variable
    ℓ : Level

IsoSucSphereSusp : (n : ℕ) → Iso (S₊ (suc n)) (Susp (S₊ n))
IsoSucSphereSusp zero = S¹IsoSuspBool
IsoSucSphereSusp (suc n) = idIso

-- Elimination principles for spheres
sphereElim : (n : ℕ) {A : (S₊ (suc n)) → Type ℓ} → ((x : S₊ (suc n)) → isOfHLevel (suc n) (A x))
          → A (ptSn (suc n))
          → (x : S₊ (suc n)) → A x
sphereElim zero hlev pt = toPropElim hlev pt
sphereElim (suc n) hlev pt north = pt
sphereElim (suc n) {A = A} hlev pt south = subst A (merid (ptSn (suc n))) pt
sphereElim (suc n) {A = A} hlev pt (merid a i) =
  sphereElim n {A = λ a → PathP (λ i → A (merid a i)) pt (subst A (merid (ptSn (suc n))) pt)}
               (λ a → isOfHLevelPathP' (suc n) (hlev south) _ _)
               (λ i → transp (λ j → A (merid (ptSn (suc n)) (i ∧ j))) (~ i) pt)
               a i

sphereElim2 : ∀ {ℓ} (n : ℕ) {A : (S₊ (suc n)) → (S₊ (suc n)) → Type ℓ}
          → ((x y : S₊ (suc n)) → isOfHLevel (suc n) (A x y))
          → A (ptSn (suc n)) (ptSn (suc n))
          → (x y : S₊ (suc n)) → A x y
sphereElim2 n hlev pt = sphereElim n (λ _ → isOfHLevelΠ (suc n) λ _ → hlev _ _)
                                     (sphereElim n (hlev _ ) pt)

private
  compPath-lem : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : z ≡ y)
              → PathP (λ i → (p ∙ sym q) i ≡ y) p q
  compPath-lem {y = y} p q i j =
    hcomp (λ k → λ { (i = i0) → p j
                    ; (i = i1) → q (~ k ∨ j)
                    ; (j = i1) → y })
          (p (j ∨ i))

sphereToPropElim : (n : ℕ) {A : (S₊ (suc n)) → Type ℓ} → ((x : S₊ (suc n)) → isProp (A x))
          → A (ptSn (suc n))
          → (x : S₊ (suc n)) → A x
sphereToPropElim zero = toPropElim
sphereToPropElim (suc n) hlev pt north = pt
sphereToPropElim (suc n) {A = A} hlev pt south = subst A (merid (ptSn (suc n))) pt
sphereToPropElim (suc n) {A = A} hlev pt (merid a i) =
  isProp→PathP {B = λ i → A (merid a i)} (λ _ → hlev _) pt (subst A (merid (ptSn (suc n))) pt) i

-- Elimination rule for fibrations (x : Sⁿ) → (y : Sᵐ) → A x y of h-Level (n + m).
-- The following principle is just the special case of the "Wedge Connectivity Lemma"
-- for spheres (See Cubical.Homotopy.WedgeConnectivity or chapter 8.6 in the HoTT book).
-- We prove it directly here for three reasons:
-- (i) it should perform better
-- (ii) we get a slightly stronger statement for spheres: one of the homotopies will, by design, be refl
-- (iii) the fact that the two homotopies only differ by (composition with) the homotopy leftFunction(base) ≡ rightFunction(base)
-- is close to trivial

wedgeconFun : (n m : ℕ) {A : (S₊ (suc n)) → (S₊ (suc m)) → Type ℓ}
          → ((x : S₊ (suc n)) (y : S₊ (suc m)) → isOfHLevel ((suc n) + (suc m)) (A x y))
          → (f : (x : _) → A (ptSn (suc n)) x)
          → (g : (x : _) → A x (ptSn (suc m)))
          → (g (ptSn (suc n)) ≡ f (ptSn (suc m)))
          → (x : S₊ (suc n)) (y : S₊ (suc m)) → A x y
wedgeconLeft : (n m : ℕ) {A : (S₊ (suc n)) → (S₊ (suc m)) → Type ℓ}
             → (hLev : ((x : S₊ (suc n)) (y : S₊ (suc m)) → isOfHLevel ((suc n) + (suc m)) (A x y)))
             → (f : (x : _) → A (ptSn (suc n)) x)
             → (g : (x : _) → A x (ptSn (suc m)))
             → (hom : g (ptSn (suc n)) ≡ f (ptSn (suc m)))
             → (x : _) → wedgeconFun n m hLev f g hom (ptSn (suc n)) x ≡ f x
wedgeconRight : (n m : ℕ) {A : (S₊ (suc n)) → (S₊ (suc m)) → Type ℓ}
             → (hLev : ((x : S₊ (suc n)) (y : S₊ (suc m)) → isOfHLevel ((suc n) + (suc m)) (A x y)))
             → (f : (x : _) → A (ptSn (suc n)) x)
             → (g : (x : _) → A x (ptSn (suc m)))
             → (hom : g (ptSn (suc n)) ≡ f (ptSn (suc m)))
             → (x : _) → wedgeconFun n m hLev f g hom x (ptSn (suc m)) ≡ g x
wedgeconFun zero zero {A = A} hlev f g hom = F
  where
  helper : SquareP (λ i j → A (loop i) (loop j)) (cong f loop) (cong f loop)
                        (λ i → hcomp (λ k → λ { (i = i0) → hom k
                                                ; (i = i1) → hom k })
                                      (g (loop i)))
                         λ i → hcomp (λ k → λ { (i = i0) → hom k
                                                ; (i = i1) → hom k })
                                       (g (loop i))
  helper = toPathP (isOfHLevelPathP' 1 (hlev _ _) _ _ _ _)

  F : (x y : S¹) → A x y
  F base y = f y
  F (loop i) base = hcomp (λ k → λ { (i = i0) → hom k
                                    ; (i = i1) → hom k })
                          (g (loop i))
  F (loop i) (loop j) = helper i j

wedgeconFun zero (suc m) {A = A} hlev f g hom = F₀
  module _ where
  transpLemma₀ : (x : S₊ (suc m)) → transport (λ i₁ → A base (merid x i₁)) (g base) ≡ f south
  transpLemma₀ x = cong (transport (λ i₁ → A base (merid x i₁)))
                                  hom
              ∙ (λ i → transp (λ j → A base (merid x (i ∨ j))) i
                               (f (merid x i)))

  pathOverMerid₀ : (x : S₊ (suc m)) → PathP (λ i₁ → A base (merid x i₁))
                                            (g base)
                                            (transport (λ i₁ → A base (merid (ptSn (suc m)) i₁))
                                                       (g base))
  pathOverMerid₀ x i = hcomp (λ k → λ { (i = i0) → g base
                                      ; (i = i1) → (transpLemma₀ x ∙ sym (transpLemma₀ (ptSn (suc m)))) k})
                            (transp (λ i₁ → A base (merid x (i₁ ∧ i))) (~ i)
                                    (g base))

  pathOverMeridId₀ : pathOverMerid₀ (ptSn (suc m)) ≡ λ i → transp (λ i₁ → A base (merid (ptSn (suc m)) (i₁ ∧ i))) (~ i)
                                                                 (g base)
  pathOverMeridId₀  =
       (λ j i → hcomp (λ k → λ {(i = i0) → g base
                               ; (i = i1) → rCancel (transpLemma₀ (ptSn (suc m))) j k})
                      (transp (λ i₁ → A base (merid (ptSn (suc m)) (i₁ ∧ i))) (~ i)
                              (g base)))
     ∙ λ j i → hfill (λ k → λ { (i = i0) → g base
                                ; (i = i1) → transport (λ i₁ → A base (merid (ptSn (suc m)) i₁))
                                                        (g base)})
                      (inS (transp (λ i₁ → A base (merid (ptSn (suc m)) (i₁ ∧ i))) (~ i)
                                   (g base))) (~ j)

  indStep₀ : (x : _) (a : _) → PathP (λ i → A x (merid a i))
                                             (g x)
                                             (subst (λ y → A x y) (merid (ptSn (suc m)))
                                                    (g x))
  indStep₀ = wedgeconFun zero m (λ _ _ → isOfHLevelPathP' (2 + m) (hlev _ _) _ _)
                              pathOverMerid₀
                              (λ a i → transp (λ i₁ → A a (merid (ptSn (suc m)) (i₁ ∧ i))) (~ i)
                                               (g a))
                              (sym pathOverMeridId₀)

  F₀ : (x : S¹) (y : Susp (S₊ (suc m))) → A x y
  F₀ x north = g x
  F₀ x south = subst (λ y → A x y) (merid (ptSn (suc m))) (g x)
  F₀ x (merid a i) = indStep₀ x a i
wedgeconFun (suc n) m {A = A} hlev f g hom = F₁
  module _ where
  transpLemma₁ : (x : S₊ (suc n)) → transport (λ i₁ → A (merid x i₁) (ptSn (suc m))) (f (ptSn (suc m))) ≡ g south
  transpLemma₁ x = cong (transport (λ i₁ → A (merid x i₁) (ptSn (suc m))))
                       (sym hom)
                ∙ (λ i → transp (λ j → A (merid x (i ∨ j)) (ptSn (suc m))) i
                                 (g (merid x i)))

  pathOverMerid₁ : (x : S₊ (suc n)) → PathP (λ i₁ → A (merid x i₁) (ptSn (suc m)))
                                            (f (ptSn (suc m)))
                                            (transport (λ i₁ → A (merid (ptSn (suc n)) i₁) (ptSn (suc m)))
                                                       (f (ptSn (suc m))))
  pathOverMerid₁ x i = hcomp (λ k → λ { (i = i0) → f (ptSn (suc m))
                                      ; (i = i1) → (transpLemma₁ x ∙ sym (transpLemma₁ (ptSn (suc n)))) k })
                            (transp (λ i₁ → A (merid x (i₁ ∧ i)) (ptSn (suc m))) (~ i)
                                    (f (ptSn (suc m))))

  pathOverMeridId₁ : pathOverMerid₁ (ptSn (suc n)) ≡ λ i → transp (λ i₁ → A (merid (ptSn (suc n)) (i₁ ∧ i)) (ptSn (suc m))) (~ i)
                                                                 (f (ptSn (suc m)))
  pathOverMeridId₁ =
        (λ j i → hcomp (λ k → λ { (i = i0) → f (ptSn (suc m))
                                  ; (i = i1) → rCancel (transpLemma₁ (ptSn (suc n))) j k })
                        (transp (λ i₁ → A (merid (ptSn (suc n)) (i₁ ∧ i)) (ptSn (suc m))) (~ i)
                                (f (ptSn (suc m)))))
       ∙ λ j i → hfill (λ k → λ { (i = i0) → f (ptSn (suc m))
                                  ; (i = i1) → transport (λ i₁ → A (merid (ptSn (suc n)) i₁) (ptSn (suc m)))
                                                          (f (ptSn (suc m))) })
                        (inS (transp (λ i₁ → A (merid (ptSn (suc n)) (i₁ ∧ i)) (ptSn (suc m))) (~ i)
                                     (f (ptSn (suc m))))) (~ j)

  indStep₁ : (a : _) (y : _) → PathP (λ i → A (merid a i) y)
                                             (f y)
                                             (subst (λ x → A x y) (merid (ptSn (suc n)))
                                                    (f y))
  indStep₁ = wedgeconFun n m (λ _ _ → isOfHLevelPathP' (suc (n + suc m)) (hlev _ _) _ _)
                           (λ a i → transp (λ i₁ → A (merid (ptSn (suc n)) (i₁ ∧ i)) a) (~ i)
                                            (f a))
                           pathOverMerid₁
                           pathOverMeridId₁

  F₁ : (x : Susp (S₊ (suc n))) (y : S₊ (suc m))  → A x y
  F₁ north y = f y
  F₁ south y = subst (λ x → A x y) (merid (ptSn (suc n))) (f y)
  F₁ (merid a i) y = indStep₁ a y i
wedgeconRight zero zero {A = A} hlev f g hom = right
  where
  right : (x : S¹) → _
  right base = sym hom
  right (loop i) j = hcomp (λ k → λ { (i = i0) → hom (~ j ∧ k)
                                     ; (i = i1) → hom (~ j ∧ k)
                                     ; (j = i1) → g (loop i) })
                           (g (loop i))
wedgeconRight zero (suc m) {A = A} hlev f g hom x = refl
wedgeconRight (suc n) m {A = A} hlev f g hom = right
  where
  lem : (x : _) → indStep₁ n m hlev f g hom x (ptSn (suc m)) ≡ _
  lem = wedgeconRight n m (λ _ _ → isOfHLevelPathP' (suc (n + suc m)) (hlev _ _) _ _)
                           (λ a i → transp (λ i₁ → A (merid (ptSn (suc n)) (i₁ ∧ i)) a) (~ i)
                                            (f a))
                           (pathOverMerid₁ n m hlev f g hom)
                           (pathOverMeridId₁ n m hlev f g hom)

  right : (x : Susp (S₊ (suc n))) → _ ≡ g x
  right north = sym hom
  right south = cong (subst (λ x → A x (ptSn (suc m)))
                            (merid (ptSn (suc n))))
                            (sym hom)
              ∙ λ i → transp (λ j → A (merid (ptSn (suc n)) (i ∨ j)) (ptSn (suc m))) i
                              (g (merid (ptSn (suc n)) i))
  right (merid a i) j =
    hcomp (λ k → λ { (i = i0) → hom (~ j)
                    ; (i = i1) → transpLemma₁ n m hlev f g hom (ptSn (suc n)) j
                    ; (j = i0) → lem a (~ k) i
                    ; (j = i1) → g (merid a i)})
          (hcomp (λ k →  λ { (i = i0) → hom (~ j)
                            ; (i = i1) → compPath-lem (transpLemma₁ n m hlev f g hom a) (transpLemma₁ n m hlev f g hom (ptSn (suc n))) k j
                            ; (j = i1) → g (merid a i)})
                 (hcomp (λ k → λ { (i = i0) → hom (~ j)
                                  ; (j = i0) → transp (λ i₂ → A (merid a (i₂ ∧ i)) (ptSn (suc m))) (~ i)
                                                       (f (ptSn (suc m)))
                                  ; (j = i1) → transp (λ j → A (merid a (i ∧ (j ∨ k))) (ptSn (suc m))) (k ∨ ~ i)
                                                       (g (merid a (i ∧ k))) })
                        (transp (λ i₂ → A (merid a (i₂ ∧ i)) (ptSn (suc m))) (~ i)
                                (hom (~ j)))))
wedgeconLeft zero zero {A = A} hlev f g hom x = refl
wedgeconLeft zero (suc m) {A = A} hlev f g hom = help
  where
  left₁ : (x : _) → indStep₀ m hlev f g hom base x ≡ _
  left₁ = wedgeconLeft zero m (λ _ _ → isOfHLevelPathP' (2 + m) (hlev _ _) _ _)
                              (pathOverMerid₀ m hlev f g hom)
                              (λ a i → transp (λ i₁ → A a (merid (ptSn (suc m)) (i₁ ∧ i))) (~ i)
                                               (g a))
                              (sym (pathOverMeridId₀ m hlev f g hom))

  help : (x : S₊ (suc (suc m))) → _
  help north = hom
  help south = cong (subst (A base) (merid (ptSn (suc m)))) hom
             ∙ λ i → transp (λ j → A base (merid (ptSn (suc m)) (i ∨ j))) i
                             (f (merid (ptSn (suc m)) i))
  help (merid a i) j =
    hcomp (λ k → λ { (i = i0) → hom j
                    ; (i = i1) → transpLemma₀ m hlev f g hom (ptSn (suc m)) j
                    ; (j = i0) → left₁ a (~ k) i
                    ; (j = i1) → f (merid a i)})
          (hcomp (λ k →  λ { (i = i0) → hom j
                            ; (i = i1) → compPath-lem (transpLemma₀ m hlev f g hom a)
                                                       (transpLemma₀ m hlev f g hom (ptSn (suc m))) k j
                            ; (j = i1) → f (merid a i)})
                 (hcomp (λ k → λ { (i = i0) → hom j
                                  ; (j = i0) → transp (λ i₂ → A base (merid a (i₂ ∧ i))) (~ i)
                                                       (g base)
                                  ; (j = i1) → transp (λ j → A base (merid a (i ∧ (j ∨ k)))) (k ∨ ~ i)
                                                       (f (merid a (i ∧ k)))})
                        (transp (λ i₂ → A base (merid a (i₂ ∧ i))) (~ i)
                                (hom j))))
wedgeconLeft (suc n) m {A = A} hlev f g hom _ = refl

---------- Connectedness -----------

sphereConnected : (n : HLevel) → isConnected (suc n) (S₊ n)
sphereConnected n = ∣ ptSn n ∣ , elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _)
                                     (λ a → sym (spoke ∣_∣ (ptSn n)) ∙ spoke ∣_∣ a)

-- The fact that path spaces of Sn are connected can be proved directly for Sⁿ.
-- (Unfortunately, this does not work for higher paths)
pathIdTruncSⁿ : (n : ℕ) (x y : S₊ (suc n))
             → Path (hLevelTrunc (2 + n) (S₊ (suc n))) ∣ x ∣ ∣ y ∣
             → hLevelTrunc (suc n) (x ≡ y)
pathIdTruncSⁿ n = sphereElim n (λ _ → isOfHLevelΠ (suc n) λ _ → isOfHLevelΠ (suc n)  λ _ → isOfHLevelTrunc (suc n))
                     (sphereElim n (λ _ → isOfHLevelΠ (suc n)  λ _ → isOfHLevelTrunc (suc n))
                       λ _ → ∣ refl ∣)

pathIdTruncSⁿ⁻ : (n : ℕ) (x y : S₊ (suc n))
             → hLevelTrunc (suc n) (x ≡ y)
             → Path (hLevelTrunc (2 + n) (S₊ (suc n))) ∣ x ∣ ∣ y ∣
pathIdTruncSⁿ⁻ n x y = rec (isOfHLevelTrunc (2 + n) _ _)
                           (J (λ y _ → Path (hLevelTrunc (2 + n) (S₊ (suc n))) ∣ x ∣ ∣ y ∣) refl)

pathIdTruncSⁿretract : (n : ℕ) (x y : S₊ (suc n)) → (p : hLevelTrunc (suc n) (x ≡ y)) → pathIdTruncSⁿ n x y (pathIdTruncSⁿ⁻ n x y p) ≡ p
pathIdTruncSⁿretract n =
  sphereElim n (λ _ → isOfHLevelΠ (suc n) λ _ → isOfHLevelΠ (suc n) λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _)
    λ y → elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _)
      (J (λ y p → pathIdTruncSⁿ n (ptSn (suc n)) y (pathIdTruncSⁿ⁻ n (ptSn (suc n)) y ∣ p ∣) ≡ ∣ p ∣)
         (cong (pathIdTruncSⁿ n (ptSn (suc n)) (ptSn (suc n))) (transportRefl refl) ∙ pm-help n))
  where
  pm-help : (n : ℕ) → pathIdTruncSⁿ n (ptSn (suc n)) (ptSn (suc n)) refl  ≡ ∣ refl ∣
  pm-help zero = refl
  pm-help (suc n) = refl

isConnectedPathSⁿ : (n : ℕ) (x y : S₊ (suc n)) → isConnected (suc n) (x ≡ y)
isConnectedPathSⁿ n x y =
  isContrRetract
   (pathIdTruncSⁿ⁻ n x y)
   (pathIdTruncSⁿ n x y)
   (pathIdTruncSⁿretract n x y)
     ((isContr→isProp (sphereConnected (suc n)) ∣ x ∣ ∣ y ∣)
      , isProp→isSet (isContr→isProp (sphereConnected (suc n))) _ _ _)

-- Equivalence Sⁿ*Sᵐ≃Sⁿ⁺ᵐ⁺¹
IsoSphereJoin : (n m : ℕ)
  → Iso (join (S₊ n) (S₊ m)) (S₊ (suc (n + m)))
IsoSphereJoin zero m =
  compIso join-comm
    (compIso (invIso Susp-iso-joinBool)
             (invIso (IsoSucSphereSusp m)))
IsoSphereJoin (suc n) m =
  compIso (Iso→joinIso
            (subst (λ x → Iso (S₊ (suc x)) (join (S₊ n) Bool))
                   (+-comm n 0) (invIso (IsoSphereJoin n 0)))
            idIso)
          (compIso (equivToIso joinAssocDirect)
            (compIso (Iso→joinIso idIso
                      (compIso join-comm
                       (compIso (invIso Susp-iso-joinBool)
                                (invIso (IsoSucSphereSusp m)))))
                (compIso
                  (IsoSphereJoin n (suc m))
                    (pathToIso λ i → S₊ (suc (+-suc n m i))))))

-- Some lemmas on the H
rUnitS¹ : (x : S¹) → x * base ≡ x
rUnitS¹ base = refl
rUnitS¹ (loop i₁) = refl

commS¹ : (a x : S¹) → a * x ≡ x * a
commS¹ = wedgeconFun _ _ (λ _ _ → isGroupoidS¹ _ _)
         (sym ∘ rUnitS¹)
         rUnitS¹
         refl

SuspS¹-hom : (a x : S¹)
  → Path (Path (hLevelTrunc 4 (S₊ 2)) _ _)
          (cong ∣_∣ₕ (merid (a * x) ∙ sym (merid base)))
          (cong ∣_∣ₕ (merid a ∙ sym (merid base))
        ∙ (cong ∣_∣ₕ (merid x ∙ sym (merid base))))
SuspS¹-hom = wedgeconFun _ _ (λ _ _ → isOfHLevelTrunc 4 _ _ _ _)
           (λ x → lUnit _
                 ∙ cong (_∙ cong ∣_∣ₕ (merid x ∙ sym (merid base)))
                        (cong (cong ∣_∣ₕ) (sym (rCancel (merid base)))))
           (λ x → (λ i → cong ∣_∣ₕ (merid (rUnitS¹ x i) ∙ sym (merid base)))
               ∙∙ rUnit _
               ∙∙ cong (cong ∣_∣ₕ (merid x ∙ sym (merid base)) ∙_)
                       (cong (cong ∣_∣ₕ) (sym (rCancel (merid base)))))
           (sym (l (cong ∣_∣ₕ (merid base ∙ sym (merid base)))
                (cong (cong ∣_∣ₕ) (sym (rCancel (merid base))))))
  where
  l : ∀ {ℓ} {A : Type ℓ} {x : A} (p : x ≡ x) (P : refl ≡ p)
    → lUnit p ∙ cong (_∙ p) P ≡ rUnit p ∙ cong (p ∙_) P
  l p = J (λ p P → lUnit p ∙ cong (_∙ p) P ≡ rUnit p ∙ cong (p ∙_) P) refl

rCancelS¹ : (x : S¹) → ptSn 1 ≡ x * (invLooper x)
rCancelS¹ base = refl
rCancelS¹ (loop i) j =
  hcomp (λ r → λ {(i = i0) → base ; (i = i1) → base ; (j = i0) → base})
        base

SuspS¹-inv : (x : S¹) → Path (Path (hLevelTrunc 4 (S₊ 2)) _ _)
                         (cong ∣_∣ₕ (merid (invLooper x) ∙ sym (merid base)))
                         (cong ∣_∣ₕ (sym (merid x ∙ sym (merid base))))
SuspS¹-inv x = (lUnit _
       ∙∙ cong (_∙ cong ∣_∣ₕ (merid (invLooper x) ∙ sym (merid base)))
               (sym (lCancel (cong ∣_∣ₕ (merid x ∙ sym (merid base)))))
                  ∙∙ sym (assoc _ _ _))
       ∙∙ cong (sym (cong ∣_∣ₕ (merid x ∙ sym (merid base))) ∙_) lem
       ∙∙ (assoc _ _ _
       ∙∙ cong (_∙ (cong ∣_∣ₕ (sym (merid x ∙ sym (merid base)))))
               (lCancel (cong ∣_∣ₕ (merid x ∙ sym (merid base))))
       ∙∙ sym (lUnit _))
  where
  lem : cong ∣_∣ₕ (merid x ∙ sym (merid base))
      ∙ cong ∣_∣ₕ (merid (invLooper x) ∙ sym (merid base))
     ≡ cong ∣_∣ₕ (merid x ∙ sym (merid base))
     ∙ cong ∣_∣ₕ (sym (merid x ∙ sym (merid base)))
  lem = sym (SuspS¹-hom x (invLooper x))
     ∙ ((λ i → cong ∣_∣ₕ (merid (rCancelS¹ x (~ i)) ∙ sym (merid base)))
     ∙ cong (cong ∣_∣ₕ) (rCancel (merid base))) ∙ sym (rCancel _)

max_stars_repo_name: ecavallo/cubical

max_issues_repo_name: ecavallo/cubical

max_forks_repo_name: ecavallo/cubical


text:
open import Data.Product using ( ∃ ; _×_ ; _,_ ; proj₁ ; proj₂ )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.TBox.Interp using
  ( Interp ; Δ ; _⊨_≈_ ; con ; rol ; ≈-refl ; ≈-sym ; ≈-trans ; con-≈ ; rol-≈ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.Util using ( id ; _∘_ )

module Web.Semantic.DL.TBox.Interp.Morphism {Σ : Signature} where

infix 2 _≲_ _≃_

-- I ≲ J whenever J respects all the properties of I

data _≲_ (I J : Interp Σ) : Set where
  morph :
    (f : Δ I → Δ J) →
    (≲-resp-≈ : ∀ {x y} → (I ⊨ x ≈ y) → (J ⊨ f x ≈ f y)) →
    (≲-resp-con : ∀ {c x} → (x ∈ con I c) → (f x ∈ con J c)) →
    (≲-resp-rol : ∀ {r x y} → ((x , y) ∈ rol I r) → ((f x , f y) ∈ rol J r)) →
    (I ≲ J)

≲-image : ∀ {I J} → (I ≲ J) → Δ I → Δ J
≲-image (morph f ≲-resp-≈ ≲-resp-con ≲-resp-rol) = f

≲-image² : ∀ {I J} → (I ≲ J) → (Δ I × Δ I) → (Δ J × Δ J)
≲-image² I≲J (x , y) = (≲-image I≲J x , ≲-image I≲J y)

≲-resp-≈ : ∀ {I J} → (I≲J : I ≲ J) → ∀ {x y} → (I ⊨ x ≈ y) →
  (J ⊨ ≲-image I≲J x ≈ ≲-image I≲J y)
≲-resp-≈ (morph f ≲-resp-≈ ≲-resp-con ≲-resp-rol) = ≲-resp-≈

≲-resp-con : ∀ {I J} → (I≲J : I ≲ J) → ∀ {c x} → (x ∈ con I c) →
  (≲-image I≲J x ∈ con J c)
≲-resp-con (morph f ≲-resp-≈ ≲-resp-con ≲-resp-rol) = ≲-resp-con

≲-resp-rol : ∀ {I J} → (I≲J : I ≲ J) → ∀ {r xy} → (xy ∈ rol I r) →
  (≲-image² I≲J xy ∈ rol J r)
≲-resp-rol (morph f ≲-resp-≈ ≲-resp-con ≲-resp-rol) {r} {x , y} = ≲-resp-rol

≲-refl : ∀ I → (I ≲ I)
≲-refl I = morph id id id id

≲-trans : ∀ {I J K} → (I ≲ J) → (J ≲ K) → (I ≲ K)
≲-trans I≲J J≲K = morph
  (≲-image J≲K ∘ ≲-image I≲J)
  (≲-resp-≈ J≲K ∘ ≲-resp-≈ I≲J)
  (≲-resp-con J≲K ∘ ≲-resp-con I≲J)
  (≲-resp-rol J≲K ∘ ≲-resp-rol I≲J)

-- I ≃ J whenever there is an isomprhism between I and J

data _≃_ (I J : Interp Σ) : Set where
  iso :
    (≃-impl-≲ : I ≲ J) →
    (≃-impl-≳ : J ≲ I) →
    (≃-iso : ∀ x → I ⊨ (≲-image ≃-impl-≳ (≲-image ≃-impl-≲ x)) ≈ x) →
    (≃-iso⁻¹ : ∀ x → J ⊨ (≲-image ≃-impl-≲ (≲-image ≃-impl-≳ x)) ≈ x) →
    (I ≃ J)

≃-impl-≲ : ∀ {I J} → (I ≃ J) → (I ≲ J)
≃-impl-≲ (iso ≃-impl-≲ ≃-impl-≳ ≃-iso ≃-iso⁻¹) = ≃-impl-≲

≃-impl-≳ : ∀ {I J} → (I ≃ J) → (J ≲ I)
≃-impl-≳ (iso ≃-impl-≲ ≃-impl-≳ ≃-iso ≃-iso⁻¹) = ≃-impl-≳

≃-image : ∀ {I J} → (I ≃ J) → Δ I → Δ J
≃-image I≃J = ≲-image (≃-impl-≲ I≃J)

≃-image² : ∀ {I J} → (I ≃ J) → (Δ I × Δ I) → (Δ J × Δ J)
≃-image² I≃J = ≲-image² (≃-impl-≲ I≃J)

≃-image⁻¹ : ∀ {I J} → (I ≃ J) → Δ J → Δ I
≃-image⁻¹ I≃J = ≲-image (≃-impl-≳ I≃J)

≃-image²⁻¹ : ∀ {I J} → (I ≃ J) → (Δ J × Δ J) → (Δ I × Δ I)
≃-image²⁻¹ I≃J = ≲-image² (≃-impl-≳ I≃J)

≃-iso : ∀ {I J} → (I≃J : I ≃ J) → ∀ x → (I ⊨ (≃-image⁻¹ I≃J (≃-image I≃J x)) ≈ x)
≃-iso (iso ≃-impl-≲ ≃-impl-≳ ≃-iso ≃-iso⁻¹) = ≃-iso

≃-iso⁻¹ : ∀ {I J} → (I≃J : I ≃ J) → ∀ x → (J ⊨ (≃-image I≃J (≃-image⁻¹ I≃J x)) ≈ x)
≃-iso⁻¹ (iso ≃-impl-≲ ≃-impl-≳ ≃-iso ≃-iso⁻¹) = ≃-iso⁻¹

≃-resp-≈ : ∀ {I J} → (I≃J : I ≃ J) → ∀ {x y} →
  (I ⊨ x ≈ y) → (J ⊨ ≃-image I≃J x ≈ ≃-image I≃J y)
≃-resp-≈ I≃J = ≲-resp-≈ (≃-impl-≲ I≃J)

≃-refl-≈ : ∀ {I J} → (I≃J : I ≃ J) → ∀ {x y} →
  (I ⊨ ≃-image⁻¹ I≃J x ≈ ≃-image⁻¹ I≃J y) → (J ⊨ x ≈ y)
≃-refl-≈ {I} {J} I≃J {x} {y} x≈y =
  ≈-trans J (≈-sym J (≃-iso⁻¹ I≃J x))
    (≈-trans J (≃-resp-≈ I≃J x≈y) (≃-iso⁻¹ I≃J y))

≃-refl : ∀ I → (I ≃ I)
≃-refl I = iso (≲-refl I) (≲-refl I) (λ x → ≈-refl I) (λ x → ≈-refl I)

≃-sym : ∀ {I J} → (I ≃ J) → (J ≃ I)
≃-sym I≃J = iso (≃-impl-≳ I≃J) (≃-impl-≲ I≃J) (≃-iso⁻¹ I≃J) (≃-iso I≃J)

≃-trans : ∀ {I J K} → (I ≃ J) → (J ≃ K) → (I ≃ K)
≃-trans {I} {J} {K} I≃J J≃K = iso
  (≲-trans (≃-impl-≲ I≃J) (≃-impl-≲ J≃K))
  (≲-trans (≃-impl-≳ J≃K) (≃-impl-≳ I≃J))
  (λ x → ≈-trans I (≲-resp-≈ (≃-impl-≳ I≃J) (≃-iso J≃K (≃-image I≃J x)))
    (≃-iso I≃J x))
  (λ x → ≈-trans K (≲-resp-≈ (≃-impl-≲ J≃K) (≃-iso⁻¹ I≃J (≃-image⁻¹ J≃K x)))
    (≃-iso⁻¹ J≃K x))

ext: agda

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: agda/agda-web-semantic

max_forks_repo_name: agda/agda-web-semantic


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

module Light.Implementation.Data.Empty where

open import Light.Library.Data.Empty using (Library ; Dependencies)
open import Light.Level using (0ℓ)
open import Light.Variable.Sets

instance dependencies : Dependencies
dependencies = record {}

instance library : Library dependencies
library = record { Implementation }
      where
      module Implementation where
            data Empty : Set where

            eliminate : Empty → 𝕒
            eliminate ()

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


text:
-- Andreas, 2018-06-19, issue #3130
-- Do not treat .(p) as projection pattern, but always as dot pattern.

record R : Set₁ where
  field f : Set
open R

-- Shouldn't pass.

mkR : (A : Set) → R
mkR A .(f) = A

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
--  Alternative proof of LLPO => MP∨

{-# OPTIONS --without-K --safe #-}
module Constructive.Axiom.Properties.Alternative where

-- agda-stdlib
open import Level renaming (suc to lsuc; zero to lzero)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Data.Bool using (Bool; true; false; not)
open import Data.Sum as Sum
open import Data.Product as Prod
open import Data.Nat as ℕ using (ℕ; zero; suc; _≤_; s≤s; z≤n; _≤?_)
import Data.Nat.Properties as ℕₚ
import Data.Nat.Induction as ℕInd
open import Function.Base
import Induction.WellFounded as Ind
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Binary
  using (tri≈; tri<; tri>; Rel; Trichotomous)
open import Relation.Binary.PropositionalEquality

-- agda-misc
open import Constructive.Axiom
open import Constructive.Combinators
open import Constructive.Common

-- LLPO => MP∨
record HasPropertiesForLLPO⇒MP∨
  {a} r p (A : Set a) : Set (a ⊔ lsuc r ⊔ lsuc p)
  where
  field
    _<_       : Rel A r
    <-cmp     : Trichotomous _≡_ _<_
    <-all-dec : {P : A → Set p} → DecU P → DecU (λ n → ∀ i → i < n → P i)
    <-wf      : Ind.WellFounded _<_

llpo⇒mp∨ : ∀ {r p a} {A : Set a} →
           HasPropertiesForLLPO⇒MP∨ r p A → LLPO A (p ⊔ a ⊔ r) → MP∨ A p
llpo⇒mp∨ {r} {p} {a} {A = A} has llpo {P = P} {Q} P? Q? ¬¬[∃x→Px⊎Qx] =
  Sum.swap ¬¬∃Q⊎¬¬∃P
  where
  open HasPropertiesForLLPO⇒MP∨ has
  -- ex. R 5
  -- n : 0 1 2 3 4 5 6 7 8
  -- P : 0 0 0 0 0 1 ? ? ?
  -- Q : 0 0 0 0 0 0 ? ? ?
  R S : A → Set (r ⊔ p ⊔ a)
  R n = (∀ i → i < n → ¬ P i × ¬ Q i) × P n × ¬ Q n
  S n = (∀ i → i < n → ¬ P i × ¬ Q i) × ¬ P n × Q n

  lem : DecU (λ n → ∀ i → i < n → ¬ P i × ¬ Q i)
  lem = <-all-dec (DecU-× (¬-DecU P?) (¬-DecU Q?))

  R? : DecU R
  R? = DecU-× lem (DecU-× P? (¬-DecU Q?))

  S? : DecU S
  S? = DecU-× lem (DecU-× (¬-DecU P?) Q?)

  ¬[∃R×∃S] : ¬ (∃ R × ∃ S)
  ¬[∃R×∃S] ((m , ∀i→i<m→¬Pi×¬Qi , Pm , ¬Qm) ,
            (n , ∀i→i<n→¬Pi×¬Qi , ¬Pn , Qn)) with <-cmp m n
  ... | tri< m<n _ _ = proj₁ (∀i→i<n→¬Pi×¬Qi m m<n) Pm
  ... | tri≈ _ m≡n _ = ¬Pn (subst P m≡n Pm)
  ... | tri> _ _ n<m = proj₂ (∀i→i<m→¬Pi×¬Qi n n<m) Qn

  -- use LLPO
  ¬∃R⊎¬∃S : ¬ ∃ R ⊎ ¬ ∃ S
  ¬∃R⊎¬∃S = llpo R? S? ¬[∃R×∃S]

  -- Induction by _<_
  byacc₁ : (∀ x → ¬ R x) → (∀ x → ¬ Q x) → ∀ x → Ind.Acc _<_ x → ¬ P x
  byacc₁ ∀¬R ∀¬Q x (Ind.acc rs) Px =
    ∀¬R x ((λ i i<x → (λ Pi → byacc₁ ∀¬R ∀¬Q i (rs i i<x) Pi) , ∀¬Q i) , (Px , ∀¬Q x))

  ∀¬R→∀¬Q→∀¬P : (∀ x → ¬ R x) → (∀ x → ¬ Q x) → ∀ x → ¬ P x
  ∀¬R→∀¬Q→∀¬P ∀¬R ∀¬Q x Px = byacc₁ ∀¬R ∀¬Q x (<-wf x) Px

  ¬∃R→¬∃Q→¬∃P : ¬ ∃ R → ¬ ∃ Q → ¬ ∃ P
  ¬∃R→¬∃Q→¬∃P ¬∃R ¬∃Q = ∀¬P→¬∃P $ ∀¬R→∀¬Q→∀¬P (¬∃P→∀¬P ¬∃R) (¬∃P→∀¬P ¬∃Q)

  byacc₂ : (∀ x → ¬ S x) → (∀ x → ¬ P x) → ∀ x → Ind.Acc _<_ x → ¬ Q x
  byacc₂ ∀¬S ∀¬P x (Ind.acc rs) Qx =
    ∀¬S x ((λ i i<x → ∀¬P i , λ Qi → byacc₂ ∀¬S ∀¬P i (rs i i<x) Qi) , (∀¬P x , Qx))

  ∀¬S→∀¬P→∀¬Q : (∀ x → ¬ S x) → (∀ x → ¬ P x) → ∀ x → ¬ Q x
  ∀¬S→∀¬P→∀¬Q ∀¬S ∀¬P x Qx = byacc₂ ∀¬S ∀¬P x (<-wf x) Qx

  ¬∃S→¬∃P→¬∃Q : ¬ ∃ S → ¬ ∃ P → ¬ ∃ Q
  ¬∃S→¬∃P→¬∃Q ¬∃S ¬∃P = ∀¬P→¬∃P $ ∀¬S→∀¬P→∀¬Q (¬∃P→∀¬P ¬∃S) (¬∃P→∀¬P ¬∃P)

  ¬¬[∃P⊎∃Q] : ¬ ¬ (∃ P ⊎ ∃ Q)
  ¬¬[∃P⊎∃Q] = DN-map ∃-distrib-⊎ ¬¬[∃x→Px⊎Qx]

  ¬¬∃Q⊎¬¬∃P : ¬ ¬ ∃ Q ⊎ ¬ ¬ ∃ P
  ¬¬∃Q⊎¬¬∃P =
    Sum.map
      (λ ¬∃R ¬∃Q → ¬¬[∃P⊎∃Q] Sum.[ ¬∃R→¬∃Q→¬∃P ¬∃R ¬∃Q , ¬∃Q ])
      (λ ¬∃S ¬∃P → ¬¬[∃P⊎∃Q] Sum.[ ¬∃P , ¬∃S→¬∃P→¬∃Q ¬∃S ¬∃P ])
      ¬∃R⊎¬∃S


text:
-- Andreas, 2021-04-28, issue #5336
-- data...where is already extensible.

module _ where

module C where
  postulate
    Name QName : Set

variable
  x  y  : C.Name
  xs ys : C.QName

interleaved mutual

  -- Scope of a declaration.

  data Scope : Set
  variable
    sc sc' : Scope

  -- Declarations in a scope.

  data Decls (sc : Scope) : Set
  variable
    ds₀ ds ds' : Decls sc

  -- A definition in a scope.
  -- So far, we can only define modules, which hold declarations.

  data Val : (sc : Scope) → Set

  -- We use letter v ("value") for definitions.

  variable
    v v' : Val sc

  -- A well-scoped name pointing to its definition.

  data Name : (sc : Scope) → Val sc → Set

  variable
    n n' : Name sc v

  -- A well-scoped declaration is one of
  --
  --   * A module definition.
  --   * Importing the declarations of another module via `open`.

  data Decl (sc : Scope) : Set where
    modl : (x : C.Name) (ds : Decls sc) → Decl sc
    opn  : (n : Name sc v)              → Decl sc

  variable
    d d' : Decl sc

  -- A scope is a snoc list of lists of declarations.

  data Scope where
    ε   : Scope

  data Scope where
    _▷_ : (sc : Scope) (ds : Decls sc) → Scope

  -- Lists of declarations are also given in snoc-form.

  data Decls where
    ε   : Decls sc

  data Decls where
    _▷_ : (ds : Decls sc) (d : Decl (sc ▷ ds)) → Decls sc

  data Val where
    -- The content of a module.
    content : (ds : Decls sc) → Val sc
    -- Qualifying a value that is taken from inside module x.
    inside  : (x : C.Name) (v : Val ((sc ▷ ds) ▷ ds')) → Val (sc ▷ (ds ▷ modl x ds'))
    imp     : (n : Name (sc ▷ ds₀) (content ds')) (v : Val ((sc ▷ ds₀) ▷ ds'))
            → Val (sc ▷ (ds₀ ▷ opn n))

  -- Weakning from one scope to an extended scope.

  data _⊆_ : (sc sc' : Scope) → Set

  variable
    τ : sc ⊆ sc'

  -- Weakning by a list of declarations or a single declaration.

  wk1  : sc ⊆ (sc ▷ ds)
  wk01 : (sc ▷ ds) ⊆ (sc ▷ (ds ▷ d))

  -- Weakening a definition.

  data WkVal : (τ : sc ⊆ sc') → Val sc → Val sc' → Set

  variable
    wv wv' wv₀ : WkVal τ v v'

  data WkDecl  (τ : sc ⊆ sc') : Decl  sc → Decl  sc' → Set
  variable
    wd wd' : WkDecl τ d d'

  data WkDecls : (τ : sc ⊆ sc') → Decls sc → Decls sc' → Set
  variable
    wds₀ wds wds' : WkDecls τ ds ds'

  -- Names resolving in a list of declarations.

  data DsName (sc : Scope) : (ds : Decls sc) → Val (sc ▷ ds) → Set -- where
  variable
    nds nds' : DsName sc ds v

  -- Names resolving in a declaration.

  data DName  (sc : Scope) (ds₀ : Decls sc) : (d : Decl (sc ▷ ds₀)) → Val (sc ▷ (ds₀ ▷ d)) → Set where

    modl   : (wds : WkDecls wk01 ds ds')
           → DName sc ds₀ (modl x ds) (content ds')

    inside : (n : DsName (sc ▷ ds₀) ds' v)
           → DName sc ds₀ (modl x ds') (inside x v)

    imp    : (n : Name (sc ▷ ds₀) (content ds'))
             (nds : DsName (sc ▷ ds₀) ds' v)
           → DName sc ds₀ (opn n) (imp n v)

  variable
    nd nd' : DName sc ds d  v

  -- This finally allows us to define names resolving in a scope.

  data DsName where
    here  : (nd  : DName  sc ds d v)                     → DsName sc (ds ▷ d) v
    there : (w : WkVal wk01 v v') (nds : DsName sc ds v) → DsName sc (ds ▷ d) v'

  data Name where
    site   :                      (nds : DsName sc ds v) → Name (sc ▷ ds) v
    parent : (w : WkVal wk1 v v') (n   : Name   sc    v) → Name (sc ▷ ds) v'

  ------------------------------------------------------------------------
  -- Relating entities defined in a scope to their weakenings.

  -- Weakenings are order-preserving embeddings.

  data _⊆_ where
    ε    : ε ⊆ ε
    _▷_  : (τ : sc ⊆ sc') (wds : WkDecls τ ds ds') → (sc ▷ ds) ⊆ (sc' ▷ ds')
    _▷ʳ_ : (τ : sc ⊆ sc') (ds  : Decls sc')        → sc        ⊆ (sc' ▷ ds)

  data WkDecls where
    ε     : WkDecls τ ε ε
    _▷_   : (ws : WkDecls τ ds ds') (wd : WkDecl (τ ▷ ws) d d') → WkDecls τ (ds ▷ d) (ds' ▷ d')
    _▷ʳ_  : (ws : WkDecls τ ds ds') (d  : Decl (_ ▷ ds'))       → WkDecls τ  ds      (ds' ▷ d)

  refl-⊆         : sc ⊆ sc
  wkDecls-refl-⊆ : WkDecls τ ds ds
  wkDecl-refl-⊆  : WkDecl  τ d  d

  wkDecls-refl-⊆ {ds = ε}      = ε
  wkDecls-refl-⊆ {ds = ds ▷ d} = wkDecls-refl-⊆ ▷ wkDecl-refl-⊆

  refl-⊆ {sc = ε}       = ε
  refl-⊆ {sc = sc ▷ ds} = refl-⊆ ▷ wkDecls-refl-⊆

  -- We can now define the singleton weaknings.

  -- By another list of declarations.
  wk1 {ds = ds} = refl-⊆ ▷ʳ ds

  -- By a single declaration.
  wk01 {d = d} = refl-⊆ ▷ (wkDecls-refl-⊆ ▷ʳ d)

  -- Weakning names

  data WkName : (τ : sc ⊆ sc') (wv : WkVal τ v v') → Name sc v → Name sc' v' → Set

  postulate
    wkVal-refl-⊆  : WkVal  τ    v v
    wkName-refl-⊆ : WkName τ wv n n

  data WkDecl where
    modl : (w  : WkDecls τ    ds ds') → WkDecl τ (modl x ds) (modl x ds')
    opn  : (wn : WkName  τ wv n  n' ) → WkDecl τ (opn n)   (opn n')

  wkDecl-refl-⊆ {d = modl x ds} = modl wkDecls-refl-⊆
  wkDecl-refl-⊆ {d = opn n    } = opn {wv = wkVal-refl-⊆} wkName-refl-⊆

  -- We can prove that the identity weaking leaves definitions unchanged.

  data WkVal where
    content : (wds : WkDecls τ ds ds') → WkVal τ (content ds) (content ds')
    inside  : (wv : WkVal ((τ ▷ wds) ▷ wds') v  v' )
            → WkVal (τ ▷ (wds ▷ modl wds')) (inside x v) (inside x v')

  data WkName where
    site   : WkName τ wv (site nds) (site nds')

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --rewriting #-}
{-# OPTIONS --no-fast-reduce #-}

open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}

data A : Set where
  a b : A

postulate rew : a ≡ b
{-# REWRITE rew #-}

test : a ≡ b
test = refl

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Lvl.Functions where

open import Lvl
open import Numeral.Natural

add : ℕ → Lvl.Level → Lvl.Level
add ℕ.𝟎     ℓ = ℓ
add (ℕ.𝐒 n) ℓ = Lvl.𝐒(add n ℓ)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module RawSemantics where

open import Data.Maybe
open import Data.Nat hiding (_⊔_; _⊓_)
open import Data.Product
open import Data.Sum
open import Data.String using (String)
open import Data.Unit hiding (_≟_)
open import Data.Empty

open import Function using (_∘_)

open import Relation.Nullary
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_;_≢_; refl)
open Eq.≡-Reasoning
open import Level hiding (_⊔_) renaming (zero to lzero; suc to lsuc)

{- TODO:
* might be useful to distinguish positive and negative (refinement) types from the start
* subtyping of refinement types
* union types: want a rule to convert from a (union) type to a sum type using a decidable predicate
* intersection types
-}

Id = String

variable
  x y : Id
  ℓ ℓ′ : Level
  n : ℕ

data Expr : Set where
  Nat : ℕ → Expr
  Var : Id → Expr
  Lam : Id → Expr → Expr
  App : Expr → Expr → Expr
  Pair : Expr → Expr → Expr
  LetPair : Id → Id → Expr → Expr → Expr
  Fst Snd : Expr → Expr
  Inl Inr : Expr → Expr
  Case : Expr → Id → Expr → Id → Expr → Expr

-- raw types are the types which support standard execution
-- currently just simple types

data RawType : Set where
  Nat : RawType
  _⇒_ _⋆_ _⊹_ : RawType → RawType → RawType

ss⇒tt : ∀ {S S₁ T T₁ : RawType} → (S ⇒ S₁) ≡ (T ⇒ T₁) → (S ≡ T × S₁ ≡ T₁)
ss⇒tt refl = refl , refl

ss⋆tt : ∀ {S S₁ T T₁ : RawType} → (S ⋆ S₁) ≡ (T ⋆ T₁) → (S ≡ T × S₁ ≡ T₁)
ss⋆tt refl = refl , refl

ss⊹tt : ∀ {S S₁ T T₁ : RawType} → (S ⊹ S₁) ≡ (T ⊹ T₁) → (S ≡ T × S₁ ≡ T₁)
ss⊹tt refl = refl , refl

-- semantics of raw types
R⟦_⟧ : RawType → Set
R⟦ Nat ⟧ = ℕ
R⟦ S ⇒ T ⟧ = R⟦ S ⟧ → R⟦ T ⟧
R⟦ S ⋆ T ⟧ = R⟦ S ⟧ × R⟦ T ⟧
R⟦ S ⊹ T ⟧ = R⟦ S ⟧ ⊎ R⟦ T ⟧

data Env (A : Set ℓ) : Set ℓ where
  · : Env A
  _,_⦂_ : Env A → (x : Id) → (a : A) → Env A

data AllEnv (A : Set ℓ) (P : A → Set) : Env A → Set ℓ where
  · : AllEnv A P ·
  _,_ : ∀ {γ}{x : Id}{a : A} → AllEnv A P γ → P a → AllEnv A P (γ , x ⦂ a)

variable
  L M N : Expr

  RS RT RU RV RW : RawType
  Δ Δ₁ Δ₂ : Env RawType

-- mapping a function over an environment

_⁺ : ∀ {A : Set ℓ′}{B : Set ℓ} → (A → B) → (Env A → Env B)
(f ⁺) · = ·
(f ⁺) (Φ , x ⦂ a) = (f ⁺) Φ , x ⦂ f a

RE⟦_⟧ : Env RawType → Env Set
RE⟦_⟧ = R⟦_⟧ ⁺

data _⦂_∈_ {A : Set ℓ} : Id → A → Env A → Set ℓ where

  found : ∀ {a : A}{E : Env A} →
    x ⦂ a ∈ (E , x ⦂ a)

  there : ∀ {a a' : A}{E : Env A} →
    x ⦂ a ∈ E →
      -- x ≢ y →
    x ⦂ a ∈ (E , y ⦂ a')

data iEnv : Env Set → Set where
  · : iEnv ·
  _,_⦂_ : ∀ {E}{A} → iEnv E → (x : Id) → (a : A) → iEnv (E , x ⦂ A)

data jEnv {A : Set ℓ} (⟦_⟧ : A → Set) : Env A → Set where
  · : jEnv ⟦_⟧ ·
  _,_⦂_ : ∀ {E}{A} → jEnv ⟦_⟧ E → (x : Id) → (a : ⟦ A ⟧) → jEnv ⟦_⟧ (E , x ⦂ A)

-- F here is a natural transformation
jEnvMap : {A : Set ℓ} {⟦_⟧ ⟦_⟧′ : A → Set}{E : Env A} →
  (F : {a : A} → ⟦ a ⟧ → ⟦ a ⟧′) →
  jEnv ⟦_⟧ E → jEnv ⟦_⟧′ E
jEnvMap F · = ·
jEnvMap F (env , x ⦂ ⟦a⟧) = (jEnvMap F env) , x ⦂ F ⟦a⟧

-- should be in terms of RawType for evaluation

data _⊢_⦂_ : Env RawType → Expr → RawType → Set₁ where

  nat :
    Δ ⊢ Nat n ⦂ Nat

  var :
    (x∈ : x ⦂ RT ∈ Δ) →
    --------------------
    Δ ⊢ Var x ⦂ RT

  lam :
    (Δ , x ⦂ RS) ⊢ M ⦂ RT →
    --------------------
    Δ ⊢ Lam x M ⦂ (RS ⇒ RT)

  app :
    Δ ⊢ M ⦂ (RS ⇒ RT) →
    Δ ⊢ N ⦂ RS →
    --------------------
    Δ ⊢ App M N ⦂ RT

  pair :
    Δ ⊢ M ⦂ RS →
    Δ ⊢ N ⦂ RT →
    --------------------
    Δ ⊢ Pair M N ⦂ (RS ⋆ RT)

  pair-E :
    Δ ⊢ M ⦂ (RS ⋆ RT) →
    ((Δ , x ⦂ RS) , y ⦂ RT) ⊢ N ⦂ RU →
    ------------------------------
    Δ ⊢ LetPair x y M N ⦂ RU

  pair-E1 :
    Δ ⊢ M ⦂ (RS ⋆ RT) →
    --------------------
    Δ ⊢ Fst M ⦂ RS

  pair-E2 :
    Δ ⊢ M ⦂ (RS ⋆ RT) →
    --------------------
    Δ ⊢ Snd M ⦂ RT

  sum-I1 :
    Δ ⊢ M ⦂ RS →
    --------------------
    Δ ⊢ Inl M ⦂ (RS ⊹ RT)

  sum-I2 :
    Δ ⊢ N ⦂ RT →
    --------------------
    Δ ⊢ Inr N ⦂ (RS ⊹ RT)

  sum-E :
    Δ ⊢ L ⦂ (RS ⊹ RT) →
    (Δ , x ⦂ RS) ⊢ M ⦂ RU →
    (Δ , y ⦂ RT) ⊢ N ⦂ RV →
    RW ≡ RU × RW ≡ RV →
    --------------------
    Δ ⊢ Case L x M y N ⦂ RW

glookup : ∀ {A : Set ℓ} {⟦_⟧ : A → Set}{Φ : Env A}{a : A} →
  (x ⦂ a ∈ Φ) → jEnv ⟦_⟧ Φ → ⟦ a ⟧
glookup found (γ , _ ⦂ a) = a
glookup (there x∈) (γ , _ ⦂ a) = glookup x∈ γ
{-
lookup : (x ⦂ RT ∈ Δ) → jEnv R⟦_⟧ Δ → R⟦ RT ⟧
lookup found (γ , _ ⦂ a) = a
lookup (there x∈) (γ , _ ⦂ a) = lookup x∈ γ
-}
eval : Δ ⊢ M ⦂ RT → jEnv R⟦_⟧ Δ → R⟦ RT ⟧
eval (nat{n = n}) γ = n
eval (var x∈) γ = glookup x∈ γ
eval (lam ⊢M) γ = λ s → eval ⊢M (γ , _ ⦂ s)
eval (app ⊢M ⊢N) γ = eval ⊢M γ (eval ⊢N γ)
eval (pair ⊢M ⊢N) γ = (eval ⊢M γ) , (eval ⊢N γ)
eval (pair-E ⊢M ⊢N) γ with eval ⊢M γ
... | vx , vy = eval ⊢N ((γ , _ ⦂ vx) , _ ⦂ vy)
eval (pair-E1 ⊢M) γ = proj₁ (eval ⊢M γ)
eval (pair-E2 ⊢M) γ = proj₂ (eval ⊢M γ)
eval (sum-I1 ⊢M) γ = inj₁ (eval ⊢M γ)
eval (sum-I2 ⊢N) γ = inj₂ (eval ⊢N γ)
eval (sum-E ⊢L ⊢M ⊢N (refl , refl)) γ =
  [ (λ s → eval ⊢M (γ , _ ⦂ s)) , (λ t → eval ⊢N (γ , _ ⦂ t)) ] (eval ⊢L γ)

----------------------------------------------------------------------
-- refinement types that drive the incorrectness typing

data Type : Set₁ where
  Base : (P : ℕ → Set) (p : ∀ n → Dec (P n)) → Type -- refinement
  Nat : Type
  _⇒_ _⋆_ : (S : Type) (T : Type) → Type
  _⊹_ _⊹ˡ_ _⊹ʳ_ : (S : Type) (T : Type) → Type

T-Nat : Type
T-Nat = Base (λ n → ⊤) (λ n → yes tt) -- all natural numbers

-- characterize non-empty types

data ne : Type → Set where
  ne-base : ∀ {P p} → (∃P : Σ ℕ P) → ne (Base P p)
  ne-nat : ne Nat
  ne-⇒ : ∀ {S T} → ne S → ne T → ne (S ⇒ T)
  ne-⋆ : ∀ {S T} → ne S → ne T → ne (S ⋆ T)
  ne-⊹L : ∀ {S T} → ne S → ne (S ⊹ T)
  ne-⊹R : ∀ {S T} → ne T → ne (S ⊹ T)

∥_∥ : Type → RawType
∥ Base P p ∥ = Nat
∥ Nat ∥ = Nat
∥ S ⇒ S₁ ∥ = ∥ S ∥ ⇒ ∥ S₁ ∥
∥ S ⋆ S₁ ∥ = ∥ S ∥ ⋆ ∥ S₁ ∥
∥ S ⊹ S₁ ∥ = ∥ S ∥ ⊹ ∥ S₁ ∥
∥ S ⊹ˡ S₁ ∥ = ∥ S ∥ ⊹ ∥ S₁ ∥
∥ S ⊹ʳ S₁ ∥ = ∥ S ∥ ⊹ ∥ S₁ ∥

T⟦_⟧ : Type → Set
T⟦ Base P p ⟧ = Σ ℕ P
T⟦ Nat ⟧ = ℕ
T⟦ S ⇒ T ⟧ = T⟦ S ⟧ → T⟦ T ⟧
T⟦ S ⋆ T ⟧ = T⟦ S ⟧ × T⟦ T ⟧
T⟦ S ⊹ T ⟧ = T⟦ S ⟧ ⊎ T⟦ T ⟧
T⟦ S ⊹ˡ T ⟧ = T⟦ S ⟧
T⟦ S ⊹ʳ T ⟧ = T⟦ T ⟧

M⟦_⟧ V⟦_⟧ : Type → (Set → Set) → Set

V⟦ Base P p ⟧ m = Σ ℕ P
V⟦ Nat ⟧ m = ℕ
V⟦ T ⇒ T₁ ⟧ m = V⟦ T ⟧ m → M⟦ T₁ ⟧ m
V⟦ T ⋆ T₁ ⟧ m = V⟦ T ⟧ m × V⟦ T₁ ⟧ m
V⟦ T ⊹ T₁ ⟧ m = V⟦ T ⟧ m ⊎ V⟦ T₁ ⟧ m
V⟦ T ⊹ˡ T₁ ⟧ m = V⟦ T ⟧ m
V⟦ T ⊹ʳ T₁ ⟧ m = V⟦ T₁ ⟧ m

M⟦ T ⟧ m = m (V⟦ T ⟧ m)

E⟦_⟧ : Env Type → Env Set
E⟦_⟧ = T⟦_⟧ ⁺

∥_∥⁺ : Env Type → Env RawType
∥_∥⁺ = ∥_∥ ⁺

-- a value is a member of refinement type T

_∋_ : (T : Type) → R⟦ ∥ T ∥ ⟧ → Set
Base P p ∋ x = P x
Nat ∋ x = ⊤
(T ⇒ T₁) ∋ f = ∀ x → T ∋ x → T₁ ∋ f x
(T ⋆ T₁) ∋ (fst , snd) = T ∋ fst × T₁ ∋ snd
(T ⊹ T₁) ∋ inj₁ x = T ∋ x
(T ⊹ T₁) ∋ inj₂ y = T₁ ∋ y
(S ⊹ˡ T) ∋ inj₁ x = S ∋ x
(S ⊹ˡ T) ∋ inj₂ y = ⊥
(S ⊹ʳ T) ∋ inj₁ x = ⊥
(S ⊹ʳ T) ∋ inj₂ y = T ∋ y

-- operations on predicates
_∨_ : (P Q : ℕ → Set) → ℕ → Set
P ∨ Q = λ n → P n ⊎ Q n

_∧_ : (P Q : ℕ → Set) → ℕ → Set
P ∧ Q = λ n → P n × Q n

implies : ∀ {P Q : ℕ → Set} → (n : ℕ) → P n → (P n ⊎ Q n)
implies n Pn = inj₁ Pn

p*q->p : ∀ {P Q : ℕ → Set} → (n : ℕ) → (P n × Q n) → P n
p*q->p n (Pn , Qn) = Pn

dec-P∨Q : ∀ {P Q : ℕ → Set} → (p : ∀ n → Dec (P n)) (q : ∀ n → Dec (Q n)) → (∀ n → Dec ((P ∨ Q) n))
dec-P∨Q p q n with p n | q n
... | no ¬p | no ¬q = no [ ¬p , ¬q ]
... | no ¬p | yes !q = yes (inj₂ !q)
... | yes !p | no ¬q = yes (inj₁ !p)
... | yes !p | yes !q = yes (inj₁ !p)

dec-P∧Q : ∀ {P Q : ℕ → Set} → (p : ∀ n → Dec (P n)) (q : ∀ n → Dec (Q n)) → (∀ n → Dec ((P ∧ Q) n))
dec-P∧Q p q n with p n | q n
... | no ¬p | no ¬q = no (¬p ∘ proj₁)
... | no ¬p | yes !q = no (¬p ∘ proj₁)
... | yes !p | no ¬q = no (¬q ∘ proj₂)
... | yes !p | yes !q = yes (!p , !q)

_⊔_ _⊓_  : (S T : Type) {r : ∥ S ∥ ≡ ∥ T ∥} → Type

(Base P p ⊔ Base P₁ p₁) {refl} = Base (P ∨ P₁) (dec-P∨Q p p₁)
(Base P p ⊔ Nat) = Nat
(Nat ⊔ Base P p) = Nat
(Nat ⊔ Nat) = Nat
((S ⇒ S₁) ⊔ (T ⇒ T₁)) {r} with ss⇒tt r
... | sss , ttt = (S ⊓ T){sss} ⇒ (S₁ ⊔ T₁){ttt}
((S ⋆ S₁) ⊔ (T ⋆ T₁)) {r} with ss⋆tt r
... | sss , ttt = (S ⊔ T){sss} ⋆ (S₁ ⊔ T₁){ttt}
((S ⊹ S₁) ⊔ (T ⊹ T₁)) {r} with ss⊹tt r
... | sss , ttt = (S ⊔ T){sss} ⊹ (S₁ ⊔ T₁){ttt}
((S ⊹ S₁) ⊔ (T ⊹ˡ T₁)) {r} with ss⊹tt r
... | sss , ttt = (S ⊔ T){sss} ⊹ S₁
((S ⊹ S₁) ⊔ (T ⊹ʳ T₁)) {r} with ss⊹tt r
... | sss , ttt = S ⊹ (S₁ ⊔ T₁){ttt}
((S ⊹ˡ S₁) ⊔ (T ⊹ T₁)) {r} with ss⊹tt r
... | sss , ttt = ((S ⊔ T){sss}) ⊹ (S₁ ⊔ T₁){ttt}
((S ⊹ˡ S₁) ⊔ (T ⊹ˡ T₁)) {r} with ss⊹tt r
... | sss , ttt = ((S ⊔ T){sss}) ⊹ˡ ((S₁ ⊔ T₁){ttt})
((S ⊹ˡ S₁) ⊔ (T ⊹ʳ T₁)) {r} = S ⊹ T₁
((S ⊹ʳ S₁) ⊔ (T ⊹ T₁)) {r} with ss⊹tt r
... | sss , ttt = T ⊹ ((S₁ ⊔ T₁) {ttt})
((S ⊹ʳ S₁) ⊔ (T ⊹ˡ T₁)) {r} = T ⊹ S₁
((S ⊹ʳ S₁) ⊔ (T ⊹ʳ T₁)) {r} with ss⊹tt r
... | sss , ttt = (S ⊔ T) {sss} ⊹ (S₁ ⊔ T₁) {ttt}

Base P p ⊓ Base P₁ p₁ = Base (P ∧ P₁) (dec-P∧Q p p₁)
Base P p ⊓ Nat = Base P p
Nat ⊓ Base P p = Base P p
Nat ⊓ Nat = Nat
((S ⇒ S₁) ⊓ (T ⇒ T₁)){r} with ss⇒tt r
... | sss , ttt = (S ⊔ T){sss} ⇒ (S₁ ⊓ T₁){ttt}
((S ⋆ S₁) ⊓ (T ⋆ T₁)){r} with ss⋆tt r
... | sss , ttt = (S ⊓ T){sss} ⋆ (S₁ ⊓ T₁){ttt}
((S ⊹ S₁) ⊓ (T ⊹ T₁)){r} with ss⊹tt r
... | sss , ttt = (S ⊓ T){sss} ⊹ (S₁ ⊓ T₁){ttt}
((S ⊹ˡ S₁) ⊓ (T ⊹ T₁)) {r} = {!!}
((S ⊹ʳ S₁) ⊓ (T ⊹ T₁)) {r} = {!!}
((S ⊹ S₁) ⊓ (T ⊹ˡ T₁)) {r} = {!!}
((S ⊹ˡ S₁) ⊓ (T ⊹ˡ T₁)) {r} = {!!}
((S ⊹ʳ S₁) ⊓ (T ⊹ˡ T₁)) {r} = {!!}
((S ⊹ S₁) ⊓ (T ⊹ʳ T₁)) {r} = {!!}
((S ⊹ˡ S₁) ⊓ (T ⊹ʳ T₁)) {r} = {!!}
((S ⊹ʳ S₁) ⊓ (T ⊹ʳ T₁)) {r} = {!!}

variable
  S T U S′ T′ U′ U″ : Type
  Γ Γ₁ Γ₂ : Env Type
  P : ℕ → Set
  p : ∀ n → Dec (P n)
  A : Set ℓ
  a : A
  Φ Φ₁ Φ₂ : Env A

⊔-preserves : ∀ S T {st : ∥ S ∥ ≡ ∥ T ∥} →
  ∥ (S ⊔ T){st} ∥ ≡ ∥ S ∥ × ∥ (S ⊔ T){st} ∥ ≡ ∥ T ∥
⊓-preserves : ∀ S T {st : ∥ S ∥ ≡ ∥ T ∥} →
  ∥ (S ⊓ T){st} ∥ ≡ ∥ S ∥ × ∥ (S ⊓ T){st} ∥ ≡ ∥ T ∥

⊔-preserves (Base P p) (Base P₁ p₁) {refl} = refl , refl
⊔-preserves (Base P p) Nat {st} = refl , refl
⊔-preserves Nat (Base P p) {st} = refl , refl
⊔-preserves Nat Nat {st} = refl , refl
⊔-preserves (S ⇒ S₁) (T ⇒ T₁) {st} with ss⇒tt st
... | sss , ttt with ⊓-preserves S T {sss} | ⊔-preserves S₁ T₁ {ttt}
... | sut=s , sut=t | sut=s₁ , sut=t₁ rewrite sut=s | sut=s₁ = refl , st
⊔-preserves (S ⋆ S₁) (T ⋆ T₁) {st} with ss⋆tt st
... | sss , ttt with ⊔-preserves S T {sss} | ⊔-preserves S₁ T₁ {ttt}
... | sut=s , sut=t | sut=s₁ , sut=t₁ rewrite sut=s | sut=s₁ = refl , st
⊔-preserves (S ⊹ S₁) (T ⊹ T₁) {st} with ss⊹tt st
... | sss , ttt with ⊔-preserves S T {sss} | ⊔-preserves S₁ T₁ {ttt}
... | sut=s , sut=t | sut=s₁ , sut=t₁ rewrite sut=s | sut=s₁ = refl , st
⊔-preserves (S ⊹ S₁) (T ⊹ˡ T₁) {st} with ss⊹tt st
... | sss , ttt with ⊔-preserves S T {sss} | ⊔-preserves S₁ T₁ {ttt}
... | sut=s , sut=t | sut=s₁ , sut=t₁ rewrite sut=s = refl , st
⊔-preserves (S ⊹ S₁) (T ⊹ʳ T₁) {st} with ss⊹tt st
... | sss , ttt with ⊔-preserves S T {sss} | ⊔-preserves S₁ T₁ {ttt}
... | sut=s , sut=t | sut=s₁ , sut=t₁ rewrite sut=s | sut=s₁ = refl , st
⊔-preserves (S ⊹ˡ S₁) (T ⊹ T₁) {st} with ss⊹tt st
... | sss , ttt with ⊔-preserves S T {sss} | ⊔-preserves S₁ T₁ {ttt}
... | sut=s , sut=t | sut=s₁ , sut=t₁ rewrite sut=s | sut=s₁ = refl , st
⊔-preserves (S ⊹ˡ S₁) (T ⊹ˡ T₁) {st} with ss⊹tt st
... | sss , ttt with ⊔-preserves S T {sss} | ⊔-preserves S₁ T₁ {ttt}
... | sut=s , sut=t | sut=s₁ , sut=t₁ rewrite sut=s | sut=s₁ = refl , st
⊔-preserves (S ⊹ˡ S₁) (T ⊹ʳ T₁) {st} with ss⊹tt st
... | sss , ttt rewrite sss | ttt = refl , refl
⊔-preserves (S ⊹ʳ S₁) (T ⊹ T₁) {st} with ss⊹tt st
... | sss , ttt rewrite sss with ⊔-preserves S₁ T₁ {ttt}
... | sut=s , sut=t rewrite sut=t = (Eq.sym st) , refl
⊔-preserves (S ⊹ʳ S₁) (T ⊹ˡ T₁) {st} with ss⊹tt st
... | sss , ttt rewrite sss = refl , st
⊔-preserves (S ⊹ʳ S₁) (T ⊹ʳ T₁) {st} with ss⊹tt st
... | sss , ttt with ⊔-preserves S T {sss} | ⊔-preserves S₁ T₁ {ttt}
... | sut=s , sut=t | sut=s₁ , sut=t₁ rewrite sut=s | sut=s₁ = refl , st

⊓-preserves (Base P p) (Base P₁ p₂) {st} = refl , refl
⊓-preserves (Base P p) Nat {st} = refl , refl
⊓-preserves Nat (Base P p) {st} = refl , refl
⊓-preserves Nat Nat {st} = refl , refl
⊓-preserves (S ⇒ S₁) (T ⇒ T₁) {st} with ss⇒tt st
... | sss , ttt with ⊔-preserves S T {sss} | ⊓-preserves S₁ T₁ {ttt}
... | sut=s , sut=t | sut=s1 , sut=t1 rewrite sut=s | sut=s1 = refl , st
⊓-preserves (S ⋆ S₁) (T ⋆ T₁) {st} with ss⋆tt st
... | sss , ttt with ⊓-preserves S T {sss} | ⊓-preserves S₁ T₁ {ttt}
... | sut=s , sut=t | sut=s1 , sut=t1 rewrite sut=s | sut=s1 = refl , st
⊓-preserves (S ⊹ S₁) (T ⊹ T₁) {st} with ss⊹tt st
... | sss , ttt with ⊓-preserves S T {sss} | ⊓-preserves S₁ T₁ {ttt}
... | sut=s , sut=t | sut=s1 , sut=t1 rewrite sut=s | sut=s1 = refl , st
⊓-preserves (S ⊹ˡ S₁) (T ⊹ T₁) {st} = {!!}
⊓-preserves (S ⊹ʳ S₁) (T ⊹ T₁) {st} = {!!}
⊓-preserves S (T ⊹ˡ T₁) {st} = {!!}
⊓-preserves S (T ⊹ʳ T₁) {st} = {!!}

data Split {A : Set ℓ} : Env A → Env A → Env A → Set ℓ where
  nil : Split · · ·
  lft : ∀ {a : A}{Γ Γ₁ Γ₂ : Env A} → Split Γ Γ₁ Γ₂ → Split (Γ , x ⦂ a) (Γ₁ , x ⦂ a) Γ₂
  rgt : ∀ {a : A}{Γ Γ₁ Γ₂ : Env A} → Split Γ Γ₁ Γ₂ → Split (Γ , x ⦂ a) Γ₁ (Γ₂ , x ⦂ a)

-- subtyping

data _<:_ : Type → Type → Set where

  <:-refl :
    T <: T

  <:-base :
    (P Q : ℕ → Set) →
    {p : ∀ n → Dec (P n)}
    {q : ∀ n → Dec (Q n)}
    (p→q : ∀ n → P n → Q n) →
    Base P p <: Base Q q

  <:-base-nat : ∀ {p : ∀ n → Dec (P n)} →
    Base P p <: Nat

  <:-⇒ :
    S′ <: S →
    T <: T′ →
    (S ⇒ T) <: (S′ ⇒ T′)

  <:-⋆ :
    S <: S′ →
    T <: T′ →
    (S ⋆ T) <: (S′ ⋆ T′)

  <:-⊹ :
    S <: S′ →
    T <: T′ →
    (S ⊹ T) <: (S′ ⊹ T′)

  <:-⊹ˡ-⊹ :
    S <: S′ →
    (S ⊹ˡ T) <: (S′ ⊹ T)

  <:-⊹ʳ-⊹ :
    T <: T′ →
    (S ⊹ʳ T) <: (S ⊹ T′)

-- subtyping is compatible with raw types

<:-raw : S <: T → ∥ S ∥ ≡ ∥ T ∥
<:-raw <:-refl = refl
<:-raw (<:-base P Q p→q) = refl
<:-raw <:-base-nat = refl
<:-raw (<:-⇒ s<:t s<:t₁) = Eq.cong₂ _⇒_ (Eq.sym (<:-raw s<:t)) (<:-raw s<:t₁)
<:-raw (<:-⋆ s<:t s<:t₁) = Eq.cong₂ _⋆_ (<:-raw s<:t) (<:-raw s<:t₁)
<:-raw (<:-⊹ s<:t s<:t₁) = Eq.cong₂ _⊹_ (<:-raw s<:t) (<:-raw s<:t₁)
<:-raw (<:-⊹ˡ-⊹ s<:t) = Eq.cong₂ _⊹_ (<:-raw s<:t) refl
<:-raw (<:-⊹ʳ-⊹ s<:t) = Eq.cong₂ _⊹_ refl (<:-raw s<:t)

<:-⊔ : ∀ S T → {c : ∥ S ∥ ≡ ∥ T ∥} → S <: (S ⊔ T){c}
<:-⊓ : ∀ S T → {c : ∥ S ∥ ≡ ∥ T ∥} → (S ⊓ T){c} <: S

<:-⊔ (Base P p) (Base P₁ p₁) {refl} = <:-base P (P ∨ P₁) implies
<:-⊔ (Base P p) Nat = <:-base-nat
<:-⊔ Nat (Base P p) = <:-refl
<:-⊔ Nat Nat = <:-refl
<:-⊔ (S ⇒ S₁) (T ⇒ T₁) {c} with ss⇒tt c
... | c1 , c2 = <:-⇒ (<:-⊓ S T) (<:-⊔ S₁ T₁)
<:-⊔ (S ⋆ S₁) (T ⋆ T₁) {c} with ss⋆tt c
... | c1 , c2 = <:-⋆ (<:-⊔ S T) (<:-⊔ S₁ T₁)
<:-⊔ (S ⊹ S₁) (T ⊹ T₁) {c} with ss⊹tt c
... | c1 , c2 = <:-⊹ (<:-⊔ S T) (<:-⊔ S₁ T₁)
<:-⊔ (S ⊹ S₁) (T ⊹ˡ T₁) {c} with ss⊹tt c
... | c1 , c2 = <:-⊹ (<:-⊔ S T) <:-refl
<:-⊔ (S ⊹ S₁) (T ⊹ʳ T₁) {c} with ss⊹tt c
... | c1 , c2 = <:-⊹ <:-refl (<:-⊔ S₁ T₁)
<:-⊔ (S ⊹ˡ S₁) (T ⊹ T₁) {c} with ss⊹tt c
... | c12 = {!<:-⊹!}
<:-⊔ (S ⊹ˡ S₁) (T ⊹ˡ T₁) = {!!}
<:-⊔ (S ⊹ˡ S₁) (T ⊹ʳ T₁) = {!!}
<:-⊔ (S ⊹ʳ S₁) T = {!!}

<:-⊓ (Base P p) (Base P₁ p₁) {refl} = <:-base (P ∧ P₁) P p*q->p
<:-⊓ (Base P p) Nat = <:-refl
<:-⊓ Nat (Base P p) = <:-base-nat
<:-⊓ Nat Nat = <:-refl
<:-⊓ (S ⇒ S₁) (T ⇒ T₁) {c} with ss⇒tt c
... | c1 , c2 = <:-⇒ (<:-⊔ S T) (<:-⊓ S₁ T₁)
<:-⊓ (S ⋆ S₁) (T ⋆ T₁) {c} with ss⋆tt c
... | c1 , c2 = <:-⋆ (<:-⊓ S T) (<:-⊓ S₁ T₁)
<:-⊓ (S ⊹ S₁) (T ⊹ T₁) {c} with ss⊹tt c
... | c1 , c2 = <:-⊹ (<:-⊓ S T) (<:-⊓ S₁ T₁)
<:-⊓ (S ⊹ S₁) (T ⊹ˡ T₁) = {!!}
<:-⊓ (S ⊹ S₁) (T ⊹ʳ T₁) = {!!}
<:-⊓ (S ⊹ˡ S₁) T = {!!}
<:-⊓ (S ⊹ʳ S₁) T = {!!}

-- subtyping generates an embedding and a projection
embed : (S <: T) → T⟦ S ⟧ → T⟦ T ⟧
embed <:-refl s = s
embed (<:-base P Q p→q) (s , p) = s , p→q s p
embed <:-base-nat (s , p) = s
embed (<:-⇒ s<:t s<:t₁) s = λ x → embed s<:t₁ (s (embed s<:t x))
embed (<:-⋆ s<:t s<:t₁) (s , t) = (embed s<:t s) , (embed s<:t₁ t)
embed (<:-⊹ s<:t s<:t₁) (inj₁ x) = inj₁ (embed s<:t x)
embed (<:-⊹ s<:t s<:t₁) (inj₂ y) = inj₂ (embed s<:t₁ y)
embed (<:-⊹ˡ-⊹ s<:t) s = inj₁ (embed s<:t s)
embed (<:-⊹ʳ-⊹ s<:t) s = inj₂ (embed s<:t s)

{- no definable
inject : T⟦ S ⟧ → V⟦ S ⟧ Maybe
eject  : V⟦ S ⟧ Maybe → Maybe T⟦ S ⟧

inject {Base P p} s = s
inject {Nat} s = s
inject {S ⇒ S₁} s = λ x → eject{S} x >>= λ x₁ → let s₁ = s x₁ in just (inject {S₁} s₁)
inject {S ⋆ S₁} (s , s₁) = (inject{S} s) , (inject{S₁} s₁)
inject {S ⊹ S₁} (inj₁ x) = inj₁ (inject{S} x)
inject {S ⊹ S₁} (inj₂ y) = inj₂ (inject{S₁} y)
inject {S ⊹ˡ S₁} s = inject{S} s
inject {S ⊹ʳ S₁} s = inject{S₁} s

eject {Base P p} s = {!!}
eject {Nat} s = {!!}
eject {S ⇒ S₁} s = just (λ x → {!!})
eject {S ⋆ S₁} s = {!!}
eject {S ⊹ S₁} s = {!!}
eject {S ⊹ˡ S₁} s = {!!}
eject {S ⊹ʳ S₁} s = {!!}
-}

project : (S <: T) → V⟦ T ⟧ Maybe → M⟦ S ⟧ Maybe
project <:-refl t = just t
project (<:-base P Q {p = p} p→q) (t , qt)
  with p t
... | no ¬p = nothing
... | yes p₁ = just (t , p₁)
project (<:-base-nat{p = p}) t
  with p t
... | no ¬p = nothing
... | yes p₁ = just (t , p₁)
project (<:-⇒ s<:t s<:t₁) t = just λ s → project s<:t s >>= t >>= project s<:t₁
project (<:-⋆ s<:t s<:t₁) (s , t) = project s<:t s >>= λ x → project s<:t₁ t >>= λ x₁ → just (x , x₁)
project (<:-⊹ s<:t s<:t₁) (inj₁ x) = Data.Maybe.map inj₁ (project s<:t x)
project (<:-⊹ s<:t s<:t₁) (inj₂ y) = Data.Maybe.map inj₂ (project s<:t₁ y)
project (<:-⊹ˡ-⊹ s<:t) (inj₁ x) = project s<:t x
project (<:-⊹ˡ-⊹ s<:t) (inj₂ y) = nothing
project (<:-⊹ʳ-⊹ s<:t) (inj₁ x) = nothing
project (<:-⊹ʳ-⊹ s<:t) (inj₂ y) = project s<:t y

split-sym : Split Φ Φ₁ Φ₂ → Split Φ Φ₂ Φ₁
split-sym nil = nil
split-sym (lft sp) = rgt (split-sym sp)
split-sym (rgt sp) = lft (split-sym sp)

split-map : ∀ {A : Set ℓ}{B : Set ℓ′}{Φ Φ₁ Φ₂ : Env A} →
  {f : A → B} → Split Φ Φ₁ Φ₂ → Split ((f ⁺) Φ) ((f ⁺) Φ₁) ((f ⁺) Φ₂)
split-map nil = nil
split-map (lft sp) = lft (split-map sp)
split-map (rgt sp) = rgt (split-map sp)

weaken-∈ : Split Φ Φ₁ Φ₂ → x ⦂ a ∈ Φ₁ → x ⦂ a ∈ Φ
weaken-∈ (lft sp) found = found
weaken-∈ (rgt sp) found = there (weaken-∈ sp found)
weaken-∈ (lft sp) (there x∈) = there (weaken-∈ sp x∈)
weaken-∈ (rgt sp) (there x∈) = there (weaken-∈ sp (there x∈))

weaken : Split Δ Δ₁ Δ₂ → Δ₁ ⊢ M ⦂ RT → Δ ⊢ M ⦂ RT
weaken sp (nat) = nat
weaken sp (var x∈) = var (weaken-∈ sp x∈)
weaken sp (lam ⊢M) = lam (weaken (lft sp) ⊢M)
weaken sp (app ⊢M ⊢N) = app (weaken sp ⊢M) (weaken sp ⊢N)
weaken sp (pair ⊢M ⊢N) = pair (weaken sp ⊢M) (weaken sp ⊢N)
weaken sp (pair-E ⊢M ⊢N) = pair-E (weaken sp ⊢M) (weaken (lft (lft sp)) ⊢N)
weaken sp (pair-E1 ⊢M) = pair-E1 (weaken sp ⊢M)
weaken sp (pair-E2 ⊢M) = pair-E2 (weaken sp ⊢M)
weaken sp (sum-I1 ⊢M) = sum-I1 (weaken sp ⊢M)
weaken sp (sum-I2 ⊢N) = sum-I2 (weaken sp ⊢N)
weaken sp (sum-E ⊢L ⊢M ⊢N (RT=RU , RT=RV)) =
  sum-E (weaken sp ⊢L) (weaken (lft sp) ⊢M) (weaken (lft sp) ⊢N) (RT=RU , RT=RV)

-- incorrectness typing

-- a positive type contains refinements only in positive positions

mutual
  data Pos : Type → Set where
    Pos-Base : Pos (Base P p)
    Pos-Nat : Pos Nat
    Pos-⇒ : Neg S → Pos T → Pos (S ⇒ T)
    Pos-⋆ : Pos S → Pos T → Pos (S ⋆ T)
    Pos-⊹ : Pos S → Pos T → Pos (S ⊹ T)
    Pos-⊹ˡ : Pos S → Pos (S ⊹ˡ T)
    Pos-⊹ʳ : Pos T → Pos (S ⊹ʳ T)

  data Neg : Type → Set where
    Neg-Nat : Neg Nat
    Neg-⇒ : Pos S → Neg T → Neg (S ⇒ T)
    Neg-⋆ : Neg S → Neg T → Neg (S ⋆ T)
    Neg-⊹ : Neg S → Neg T → Neg (S ⊹ T)

pos-unique : ∀ T → (pos pos' : Pos T) → pos ≡ pos'
neg-unique : ∀ T → (neg neg' : Neg T) → neg ≡ neg'

pos-unique (Base P p) Pos-Base Pos-Base = refl
pos-unique Nat Pos-Nat Pos-Nat = refl
pos-unique (T ⇒ T₁) (Pos-⇒ x pos) (Pos-⇒ x₁ pos') rewrite neg-unique T x x₁ | pos-unique T₁ pos pos' = refl
pos-unique (T ⋆ T₁) (Pos-⋆ pos pos₁) (Pos-⋆ pos' pos'') rewrite pos-unique T pos pos' | pos-unique T₁ pos₁ pos'' = refl
pos-unique (T ⊹ T₁) (Pos-⊹ pos pos₁) (Pos-⊹ pos' pos'') rewrite pos-unique T pos pos' | pos-unique T₁ pos₁ pos'' = refl
pos-unique (T ⊹ˡ T₁) (Pos-⊹ˡ pos) (Pos-⊹ˡ pos') rewrite pos-unique T pos pos' = refl
pos-unique (T ⊹ʳ T₁) (Pos-⊹ʳ pos) (Pos-⊹ʳ pos') rewrite pos-unique T₁ pos pos' = refl
--etc
neg-unique T neg neg' = {!!}

module positive-restricted where
  toRaw : ∀ T → Pos T → T⟦ T ⟧ → R⟦ ∥ T ∥ ⟧
  fromRaw : ∀ T → Neg T → R⟦ ∥ T ∥ ⟧ → T⟦ T ⟧

  toRaw (Base P p) Pos-Base (n , pn) = n
  toRaw Nat Pos-Nat t = t
  toRaw (T ⇒ T₁) (Pos-⇒ neg pos₁) t = toRaw T₁ pos₁ ∘ t ∘ fromRaw T neg
  toRaw (T ⋆ T₁) (Pos-⋆ pos pos₁) (t , t₁) = toRaw T pos t , (toRaw T₁ pos₁ t₁)
  toRaw (T ⊹ T₁) (Pos-⊹ pos pos₁) (inj₁ x) = inj₁ (toRaw T pos x)
  toRaw (T ⊹ T₁) (Pos-⊹ pos pos₁) (inj₂ y) = inj₂ (toRaw T₁ pos₁ y)
  toRaw (S ⊹ˡ T) (Pos-⊹ˡ pos) x = inj₁ (toRaw S pos x)
  toRaw (S ⊹ʳ T) (Pos-⊹ʳ pos) y = inj₂ (toRaw T pos y)

  fromRaw (Base P p) () r
  fromRaw Nat Neg-Nat r = r
  fromRaw (T ⇒ T₁) (Neg-⇒ pos neg) r = fromRaw T₁ neg ∘ r ∘ toRaw T pos
  fromRaw (T ⋆ T₁) (Neg-⋆ neg neg₁) (r , r₁) = fromRaw T neg r , fromRaw T₁ neg₁ r₁
  fromRaw (T ⊹ T₁) (Neg-⊹ neg neg₁) (inj₁ x) = inj₁ (fromRaw T neg x)
  fromRaw (T ⊹ T₁) (Neg-⊹ neg neg₁) (inj₂ y) = inj₂ (fromRaw T₁ neg₁ y)

  toRawEnv : AllEnv Type Pos Γ → jEnv T⟦_⟧ Γ → jEnv R⟦_⟧ ∥ Γ ∥⁺
  toRawEnv{·} posΓ · = ·
  toRawEnv{Γ , _ ⦂ T} (posΓ , x₁) (γ , x ⦂ a) = toRawEnv{Γ} posΓ γ , x ⦂ toRaw T x₁ a

{-
-- attempt to map type (interpretation) to corresponding raw type (interpretation)
-- * must be monadic because of refinement
-- * fails at function types
module monadic where
  toRaw : ∀ T → T⟦ T ⟧ → Maybe R⟦ ∥ T ∥ ⟧
  fromRaw : ∀ T → R⟦ ∥ T ∥ ⟧ → Maybe T⟦ T ⟧

  toRaw (Base P p) (n , Pn) = just n
  toRaw Nat n = just n
  toRaw (T ⇒ T₁) t = {!!}
  toRaw (T ⋆ T₁) (t , t₁) = toRaw T t >>= (λ r → toRaw T₁ t₁ >>= (λ r₁ → just (r , r₁)))
  toRaw (T ⊹ T₁) (inj₁ x) = Data.Maybe.map inj₁ (toRaw T x)
  toRaw (T ⊹ T₁) (inj₂ y) = Data.Maybe.map inj₂ (toRaw T₁ y)

  fromRaw (Base P p) r with p r
  ... | no ¬p = nothing
  ... | yes pr = just (r , pr)
  fromRaw Nat r = just r
  fromRaw (T ⇒ T₁) r = {!!}
  fromRaw (T ⋆ T₁) (r , r₁) = fromRaw T r >>= (λ t → fromRaw T₁ r₁ >>= (λ t₁ → just (t , t₁)))
  fromRaw (T ⊹ T₁) (inj₁ x) = Data.Maybe.map inj₁ (fromRaw T x)
  fromRaw (T ⊹ T₁) (inj₂ y) = Data.Maybe.map inj₂ (fromRaw T₁ y)
-}

corr-sp : Split Γ Γ₁ Γ₂ → Split ∥ Γ ∥⁺ ∥ Γ₁ ∥⁺ ∥ Γ₂ ∥⁺
corr-sp nil = nil
corr-sp (lft sp) = lft (corr-sp sp)
corr-sp (rgt sp) = rgt (corr-sp sp)

postulate
  ext : ∀ {A B : Set}{f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g

unsplit-env :  ∀ {A : Set ℓ} {⟦_⟧ : A → Set}{Φ Φ₁ Φ₂ : Env A}→
  Split Φ Φ₁ Φ₂ → jEnv ⟦_⟧ Φ₁ → jEnv ⟦_⟧ Φ₂ → jEnv ⟦_⟧ Φ
unsplit-env nil γ₁ γ₂ = ·
unsplit-env (lft sp) (γ₁ , _ ⦂ a) γ₂ = (unsplit-env sp γ₁ γ₂) , _ ⦂ a
unsplit-env (rgt sp) γ₁ (γ₂ , _ ⦂ a) = (unsplit-env sp γ₁ γ₂) , _ ⦂ a

unsplit-split :  ∀ {A : Set ℓ} {⟦_⟧ : A → Set}{Φ Φ₁ Φ₂ : Env A} →
  (sp : Split Φ Φ₁ Φ₂) (γ₁ : jEnv ⟦_⟧ Φ₁) (γ₂ : jEnv ⟦_⟧ Φ₂) →
  unsplit-env sp γ₁ γ₂ ≡ unsplit-env (split-sym sp) γ₂ γ₁
unsplit-split nil γ₁ γ₂ = refl
unsplit-split (lft sp) (γ₁ , _ ⦂ a) γ₂ rewrite unsplit-split sp γ₁ γ₂ = refl
unsplit-split (rgt sp) γ₁ (γ₂ , _ ⦂ a) rewrite unsplit-split sp γ₁ γ₂ = refl

lookup-unsplit :  ∀ {A : Set ℓ} {⟦_⟧ : A → Set}{Φ Φ₁ Φ₂ : Env A}{a : A} →
  (sp : Split Φ Φ₁ Φ₂) (γ₁ : jEnv ⟦_⟧ Φ₁) (γ₂ : jEnv ⟦_⟧ Φ₂) →
  (x∈ : x ⦂ a ∈ Φ₁) →
  glookup (weaken-∈ sp x∈) (unsplit-env sp γ₁ γ₂) ≡ glookup x∈ γ₁
lookup-unsplit (lft sp) (γ₁ , _ ⦂ a) γ₂ found = refl
lookup-unsplit (rgt sp) γ₁ (γ₂ , _ ⦂ a) found = lookup-unsplit sp γ₁ γ₂ found
lookup-unsplit (lft sp) (γ₁ , _ ⦂ a) γ₂ (there x∈) = lookup-unsplit sp γ₁ γ₂ x∈
lookup-unsplit (rgt sp) γ₁ (γ₂ , _ ⦂ a) (there x∈) = lookup-unsplit sp γ₁ γ₂ (there x∈)

open positive-restricted
eval-unsplit' : (sp : Split Γ Γ₁ Γ₂) (γ₁ : jEnv T⟦_⟧ Γ₁) (γ₂ : jEnv T⟦_⟧ Γ₂) →
  (posΓ₁ : AllEnv Type Pos Γ₁) (posΓ₂ : AllEnv Type Pos Γ₂) →
  (⊢M : ∥ Γ₁ ∥⁺ ⊢ M ⦂ RT) →
  eval (weaken (corr-sp sp) ⊢M) (unsplit-env (corr-sp sp) (toRawEnv posΓ₁ γ₁) (toRawEnv posΓ₂ γ₂)) ≡ eval ⊢M (toRawEnv posΓ₁ γ₁)
eval-unsplit' sp γ₁ γ₂ posΓ₁ posΓ₂ ⊢M = {!!}
{-
      (eval (weaken (corr-sp sp) (corr ÷M))
       (toRawEnv posΓ (unsplit-env sp γ₁ γ₂)))
-}

eval-unsplit : (sp : Split Δ Δ₁ Δ₂) (γ₁ : jEnv R⟦_⟧ Δ₁) (γ₂ : jEnv R⟦_⟧ Δ₂) →
  (⊢M : Δ₁ ⊢ M ⦂ RT) →
  eval (weaken sp ⊢M) (unsplit-env sp γ₁ γ₂) ≡ eval ⊢M γ₁
eval-unsplit sp γ₁ γ₂ (nat)= refl
eval-unsplit sp γ₁ γ₂ (var x∈) = lookup-unsplit sp γ₁ γ₂ x∈
eval-unsplit sp γ₁ γ₂ (lam ⊢M) = ext (λ s → eval-unsplit (lft sp) (γ₁ , _ ⦂ s) γ₂ ⊢M)
eval-unsplit sp γ₁ γ₂ (app ⊢M ⊢M₁)
  rewrite eval-unsplit sp γ₁ γ₂ ⊢M | eval-unsplit sp γ₁ γ₂ ⊢M₁ = refl
eval-unsplit sp γ₁ γ₂ (pair ⊢M ⊢M₁)
  rewrite eval-unsplit sp γ₁ γ₂ ⊢M | eval-unsplit sp γ₁ γ₂ ⊢M₁ = refl
eval-unsplit sp γ₁ γ₂ (pair-E ⊢M ⊢N)
  rewrite eval-unsplit sp γ₁ γ₂ ⊢M = eval-unsplit (lft (lft sp)) ((γ₁ , _ ⦂ _) , _ ⦂ _) γ₂ ⊢N
eval-unsplit sp γ₁ γ₂ (pair-E1 ⊢M)
  rewrite eval-unsplit sp γ₁ γ₂ ⊢M = refl
eval-unsplit sp γ₁ γ₂ (pair-E2 ⊢M)
  rewrite eval-unsplit sp γ₁ γ₂ ⊢M = refl
eval-unsplit sp γ₁ γ₂ (sum-I1 ⊢M)
  rewrite eval-unsplit sp γ₁ γ₂ ⊢M = refl
eval-unsplit sp γ₁ γ₂ (sum-I2 ⊢N)
  rewrite eval-unsplit sp γ₁ γ₂ ⊢N = refl
eval-unsplit sp γ₁ γ₂ (sum-E ⊢L ⊢M ⊢N (refl , refl))
  rewrite eval-unsplit sp γ₁ γ₂ ⊢L
        | ext (λ s → eval-unsplit (lft sp) (γ₁ , _ ⦂ s) γ₂ ⊢M)
        | ext (λ t → eval-unsplit (lft sp) (γ₁ , _ ⦂ t) γ₂ ⊢N)
  = refl

module rule-by-rule where

  open positive-restricted
  open Eq.≡-Reasoning

  data _⊢_÷_ : Env Type → Expr → Type → Set₁ where

    nat' :
      --------------------
      · ⊢ Nat n ÷ Base (_≡_ n) (_≟_ n)

    var' :
      ( · , x ⦂ T) ⊢ Var x ÷ T

    pair-I :
      Split Γ Γ₁ Γ₂ →
      Γ₁ ⊢ M ÷ S →
      Γ₂ ⊢ N ÷ T →
      --------------------
      Γ ⊢ Pair M N ÷ (S ⋆ T)

    sum-I1 :
      Γ ⊢ M ÷ S →
      --------------------
      Γ ⊢ Inl M ÷ (S ⊹ˡ T)

    sum-I2 :
      Γ ⊢ M ÷ T →
      --------------------
      Γ ⊢ Inr M ÷ (S ⊹ʳ T)

    {- perhaps this rule should involve splitting between L and M,N -}
    sum-Case :
      Split Γ Γ₁ Γ₂ →
      Γ₁ ⊢ L ÷ (S ⊹ T) →
      (Γ₂ , x ⦂ S) ⊢ M ÷ (U ⊹ˡ U′) →
      (Γ₂ , y ⦂ T) ⊢ N ÷ (U ⊹ʳ U′) →
      ------------------------------
      Γ ⊢ Case L x M y N ÷ (U ⊹ U′)

  corr : Γ ⊢ M ÷ T → ∥ Γ ∥⁺ ⊢ M ⦂ ∥ T ∥
  corr nat' =
    nat
  corr var' =
    var found
  corr (pair-I sp ÷M ÷N) =
    pair (weaken (corr-sp sp) (corr ÷M)) (weaken (split-sym (corr-sp sp)) (corr ÷N))
  corr (sum-I1 ÷M) =
    sum-I1 (corr ÷M)
  corr (sum-I2 ÷M) =
    sum-I2 (corr ÷M)
  corr (sum-Case sp ÷L ÷M ÷N) =
    sum-E (weaken (corr-sp sp) (corr ÷L))
          (weaken (split-sym (corr-sp (rgt sp))) (corr ÷M))
          (weaken (split-sym (corr-sp (rgt sp))) (corr ÷N))
          (refl , refl)

  applySplit : {A : Set ℓ}{P : A → Set}{Θ Θ₁ Θ₂ : Env A} →
    Split Θ Θ₁ Θ₂ → AllEnv A P Θ → AllEnv A P Θ₁ × AllEnv A P Θ₂
  applySplit nil · = · , ·
  applySplit (lft sp) (ae , x)
    with applySplit sp ae
  ... | ae1 , ae2 = (ae1 , x) , ae2
  applySplit (rgt sp) (ae , x)
    with applySplit sp ae
  ... | ae1 , ae2 = ae1 , (ae2 , x)

  lave' :
    (÷M : Γ ⊢ M ÷ T) →
    (posT : Pos T) →
    (posΓ : AllEnv Type Pos Γ) →
    ∀ (t : T⟦ T ⟧) →
    ∃ λ (γ : jEnv T⟦_⟧ Γ) →
    eval (corr ÷M) (toRawEnv posΓ γ) ≡ toRaw T posT t
  lave' nat' Pos-Base posΓ (n , refl) = · , refl
  lave' var' posT (· , posT') t rewrite pos-unique _ posT posT' = (· , _ ⦂ t) , refl
  lave' (pair-I x ÷M ÷M₁) posT posΓ t = {!!}
  lave' (sum-I1 ÷M) (Pos-⊹ˡ posT) posΓ t
    with lave' ÷M posT posΓ t
  ... | γ , ih = γ , Eq.cong inj₁ ih
  lave' (sum-I2 ÷M) (Pos-⊹ʳ posT) posΓ t
    with lave' ÷M posT posΓ t
  ... | γ , ih = γ , Eq.cong inj₂ ih
  lave' (sum-Case sp ÷M ÷M₁ ÷M₂) (Pos-⊹ posT posT₁) posΓ (inj₁ x)
    with applySplit sp posΓ
  ... | posΓ₁ , posΓ₂
    with lave' ÷M₁ (Pos-⊹ˡ posT) (posΓ₂ , {!!}) x
  ... | (γ₂ , _ ⦂ s) , ih₂
    with lave' ÷M (Pos-⊹ {!!} {!!}) posΓ₁ (inj₁ s)
  ... | γ₁ , ih₁ =
    let ih₂′ = {!eval-unsplit' sp γ₁ γ₂ posΓ₁ posΓ₂ (corr ÷M) !} in
    (unsplit-env sp γ₁ γ₂) , {!!}
  lave' (sum-Case sp ÷M ÷M₁ ÷M₂) (Pos-⊹ posT posT₁) posΓ (inj₂ y) = {!!}

  lave :
    (÷M : Γ ⊢ M ÷ T) →
    (pos : Pos T) →
    ∀ (t : T⟦ T ⟧) →
    ∃ λ (γ : jEnv R⟦_⟧ ∥ Γ ∥⁺) →
    eval (corr ÷M) γ ≡ toRaw T pos t
  lave nat' Pos-Base (n , pn) = · , pn
  lave var' pos t = (· , _ ⦂ toRaw _ pos t) , refl
  lave (pair-I sp ÷M ÷N) (Pos-⋆ pos₁ pos₂) (t₁ , t₂)
    with lave ÷M pos₁ t₁ | lave ÷N pos₂ t₂
  ... | γ₁ , ih₁ | γ₂ , ih₂ =
    (unsplit-env (corr-sp sp) γ₁ γ₂) ,
    Eq.cong₂ _,_
      (begin (eval (weaken (corr-sp sp) (corr ÷M)) (unsplit-env (corr-sp sp) γ₁ γ₂)
           ≡⟨ eval-unsplit (corr-sp sp) γ₁ γ₂ (corr ÷M) ⟩
             ih₁))
      (begin (eval (weaken (split-sym (corr-sp sp)) (corr ÷N)) (unsplit-env (corr-sp sp) γ₁ γ₂)
           ≡⟨ Eq.cong (eval (weaken (split-sym (corr-sp sp)) (corr ÷N))) (unsplit-split (corr-sp sp) γ₁ γ₂) ⟩
             eval (weaken (split-sym (corr-sp sp)) (corr ÷N)) (unsplit-env (split-sym (corr-sp sp)) γ₂ γ₁)
           ≡⟨ eval-unsplit (split-sym (corr-sp sp)) γ₂ γ₁ (corr ÷N) ⟩
             ih₂))
  lave (sum-I1 ÷M) (Pos-⊹ˡ pos) t
    with lave ÷M pos t
  ... | γ , ih = γ , Eq.cong inj₁ ih
  lave (sum-I2 ÷M) (Pos-⊹ʳ pos) t
    with lave ÷M pos t
  ... | γ , ih = γ , Eq.cong inj₂ ih
  lave (sum-Case sp ÷L ÷M ÷N) (Pos-⊹ p p₁) (inj₁ x)
    with lave ÷M (Pos-⊹ˡ p) x
  ... | (γ₂ , _ ⦂ a) , ih₂
    with lave ÷L {!!} (inj₁ {!!})
  ... | γ₁ , ih₁ = {!!}
  lave (sum-Case sp ÷L ÷M ÷N) (Pos-⊹ p p₁) (inj₂ y) = {!!}

data _⊢_÷_ : Env Type → Expr → Type → Set₁ where

  nat' :
    --------------------
    · ⊢ Nat n ÷ Base (_≡_ n) λ n₁ → n ≟ n₁

  var1 :
    ( · , x ⦂ T) ⊢ Var x ÷ T

{-
  var :
    x ⦂ T ∈ Γ →
    --------------------
    Γ ⊢ Var x ÷ T
-}

  lam :
    (· , x ⦂ S) ⊢ M ÷ T →
    --------------------
    · ⊢ Lam x M ÷ (S ⇒ T)

  pair :
    Split Γ Γ₁ Γ₂ →
    Γ₁ ⊢ M ÷ S →
    Γ₂ ⊢ N ÷ T →
    --------------------
    Γ ⊢ Pair M N ÷ (S ⋆ T)

  pair-E1 :
    Γ ⊢ M ÷ (S ⋆ T) →
    --------------------
    Γ ⊢ Fst M ÷ S

  pair-E2 :
    Γ ⊢ M ÷ (S ⋆ T) →
    --------------------
    Γ ⊢ Snd M ÷ T

  sum-E :
    Split Γ Γ₁ Γ₂ →
    Γ₁ ⊢ L ÷ (S ⊹ T) →
    (Γ₂ , x ⦂ S) ⊢ M ÷ U →
    (Γ₂ , y ⦂ T) ⊢ N ÷ U →
    --------------------
    Γ ⊢ Case L x M y N ÷ U

  sum-E′ : ∀ {ru′=ru″} →
    Split Γ Γ₁ Γ₂ →
    Γ₁ ⊢ L ÷ (S ⊹ T) →
    (Γ₂ , x ⦂ S) ⊢ M ÷ U′ →
    (Γ₂ , y ⦂ T) ⊢ N ÷ U″ →
    U ≡ (U′ ⊔ U″){ru′=ru″} →
    --------------------
    Γ ⊢ Case L x M y N ÷ U

{-
  `sub` :
    Γ ⊢ M ÷ S →
    T <: S →
    --------------------
    Γ ⊢ M ÷ T
-}

corr : Γ ⊢ M ÷ T → ∥ Γ ∥⁺ ⊢ M ⦂ ∥ T ∥
corr (nat') = nat
corr var1 = var found
-- corr (var x) = var x
corr (lam ⊢M) = lam (corr ⊢M)
corr (pair-E1 ÷M) = pair-E1 (corr ÷M)
corr (pair-E2 ÷M) = pair-E2 (corr ÷M)
corr (pair sp ÷M ÷N) =
  pair (weaken (corr-sp sp) (corr ÷M)) (weaken (split-sym (corr-sp sp)) (corr ÷N))
corr (sum-E sp ÷L ÷M ÷N) =
  sum-E (weaken (corr-sp sp) (corr  ÷L))
        (weaken (lft (split-sym (corr-sp sp))) (corr ÷M))
        (weaken (lft (split-sym (corr-sp sp))) (corr ÷N))
        (refl , refl)
corr (sum-E′ {S = S}{T = T}{U′ = U′}{U″ = U″}{U = U}{ru′=ru″ = ru′=ru″} sp ÷L ÷M ÷N refl) =
  sum-E (weaken (corr-sp sp) (corr ÷L))
        (weaken (lft (split-sym (corr-sp sp))) (corr ÷M))
        (weaken (lft (split-sym (corr-sp sp))) (corr ÷N))
        (⊔-preserves U′ U″)

-- pick one element of a type to demonstrate non-emptiness
one : ∀ (T : Type) {ne-T : ne T} → T⟦ T ⟧
one (Base P p) {ne-base ∃P} = ∃P
one Nat = zero
one (T ⇒ T₁) {ne-⇒ ne-T ne-T₁} = λ x → one T₁ {ne-T₁}
one (T ⋆ T₁) {ne-⋆ ne-T ne-T₁} = (one T {ne-T}) , (one T₁ {ne-T₁})
one (T ⊹ T₁) {ne-⊹L ne-T} = inj₁ (one T {ne-T})
one (T ⊹ T₁) {ne-⊹R ne-T₁} = inj₂ (one T₁ {ne-T₁})

{- not needed
many : iEnv E⟦ Γ ⟧
many {·} = ·
many {Γ , x ⦂ T} = many , x ⦂ one T

gen : (x∈ : x ⦂ T ∈ Γ) (t  : T⟦ T ⟧) → iEnv E⟦ Γ ⟧
gen found t = many , _ ⦂ t
gen (there x∈) t = (gen x∈ t) , _ ⦂ one {!!}

lookup-gen : (x∈ : x ⦂ T ∈ Γ) (t  : T⟦ T ⟧) → lookup x∈ (gen x∈ t) ≡ t
lookup-gen found t = refl
lookup-gen (there x∈) t = lookup-gen x∈ t
-}

{-
-- soundness of the incorrectness rules
lave :
  (÷M : Γ ⊢ M ÷ T) →
  ∀ (t : T⟦ T ⟧) →
  ∃ λ (γ : iEnv E⟦ Γ ⟧) →
  eval (corr ÷M) γ ≡ t

lave nat' (n , refl) = · , refl

lave var1 t = (· , _ ⦂ t) , refl
-- lave (var x∈) t =  (gen x∈ t) , lookup-gen x∈ t
lave (lam{x = x}{S = S} ÷M) t = · , ext aux
  where
    aux : (s : T⟦ S ⟧) → eval (corr ÷M) (· , x ⦂ s) ≡ t s
    aux s with lave ÷M (t s)
    ... | (· , .x ⦂ a) , snd = {!!} -- impossible to complete!

lave (pair-E1 ÷M) t with lave ÷M (t , one {!!})
... | γ , ih = γ , Eq.cong proj₁ ih
lave (pair-E2 ÷M) t with lave ÷M (one {!!} , t)
... | γ , ih = γ , Eq.cong proj₂ ih

lave (pair sp ÷M ÷N) (s , t) with lave ÷M s | lave ÷N t
... | γ₁ , ih-M | γ₂ , ih-N =
  unsplit-env sp γ₁ γ₂ ,
  Eq.cong₂ _,_ (Eq.trans (eval-unsplit sp γ₁ γ₂ (corr ÷M)) ih-M)
               (begin eval (weaken (split-sym sp) (corr ÷N)) (unsplit-env sp γ₁ γ₂)
               ≡⟨ Eq.cong (eval (weaken (split-sym sp) (corr ÷N))) (unsplit-split sp γ₁ γ₂) ⟩
               eval (weaken (split-sym sp) (corr ÷N)) (unsplit-env (split-sym sp) γ₂ γ₁)
               ≡⟨ eval-unsplit (split-sym sp) γ₂ γ₁ (corr ÷N) ⟩
               ih-N)

-- works, but unsatisfactory!
-- this proof uses only one branch of the case
-- this choice is possible because both branches ÷M and ÷N have the same type
-- in general, U could be the union of the types of ÷M and ÷N
lave (sum-E{S = S}{T = T}{U = U} sp ÷L ÷M ÷N) u
  with lave ÷M u | lave ÷N u
... | (γ₁ , x ⦂ s) , ih-M | (γ₂ , y ⦂ t) , ih-N
  with lave ÷L (inj₁ s)
... | γ₀ , ih-L
  =
  unsplit-env sp γ₀ γ₁ ,
  (begin [
      (λ s₁ →
         eval (weaken (lft (split-sym sp)) (corr ÷M))
         (unsplit-env sp γ₀ γ₁ , x ⦂ s₁))
      ,
      (λ t₁ →
         eval (weaken (lft (split-sym sp)) (corr ÷N))
         (unsplit-env sp γ₀ γ₁ , y ⦂ t₁))
      ]
      (eval (weaken sp (corr ÷L)) (unsplit-env sp γ₀ γ₁))
  ≡⟨ Eq.cong [
      (λ s₁ →
         eval (weaken (lft (split-sym sp)) (corr ÷M))
         (unsplit-env sp γ₀ γ₁ , x ⦂ s₁))
      ,
      (λ t₁ →
         eval (weaken (lft (split-sym sp)) (corr ÷N))
         (unsplit-env sp γ₀ γ₁ , y ⦂ t₁))
      ] (eval-unsplit sp γ₀ γ₁ (corr ÷L)) ⟩
    [
      (λ s₁ →
         eval (weaken (lft (split-sym sp)) (corr ÷M))
         (unsplit-env sp γ₀ γ₁ , x ⦂ s₁))
      ,
      (λ t₁ →
         eval (weaken (lft (split-sym sp)) (corr ÷N))
         (unsplit-env sp γ₀ γ₁ , y ⦂ t₁))
      ]
      (eval (corr ÷L) γ₀)
  ≡⟨ Eq.cong
       [
       (λ s₁ →
          eval (weaken (lft (split-sym sp)) (corr ÷M))
          (unsplit-env sp γ₀ γ₁ , x ⦂ s₁))
       ,
       (λ t₁ →
          eval (weaken (lft (split-sym sp)) (corr ÷N))
          (unsplit-env sp γ₀ γ₁ , y ⦂ t₁))
       ]
       ih-L ⟩
    eval (weaken (lft (split-sym sp)) (corr ÷M)) (unsplit-env sp γ₀ γ₁ , x ⦂ s)
  ≡⟨  Eq.cong (λ γ → eval (weaken (lft (split-sym sp)) (corr ÷M)) (γ , x ⦂ s)) (unsplit-split sp γ₀ γ₁) ⟩
    eval (weaken (lft (split-sym sp)) (corr ÷M)) (unsplit-env (split-sym sp) γ₁ γ₀ , x ⦂ s)
  ≡⟨⟩
    eval (weaken (lft (split-sym sp)) (corr ÷M)) (unsplit-env (lft (split-sym sp)) (γ₁ , x ⦂ s) γ₀)
  ≡⟨ eval-unsplit (lft (split-sym sp)) (γ₁ , x ⦂ s) γ₀ (corr ÷M) ⟩
    ih-M)

lave (sum-E′{S = S}{T = T}{U = U} sp ÷L ÷M ÷N uuu) u = {!!}
-}

-- unused stuff

{- unused - needed?
record _←_ (A B : Set) : Set where
  field
    func : A → B
    back : ∀ (b : B) → ∃ λ (a : A) → func a ≡ b

open _←_
-}

max_stars_repo_name: proglang/incorrectness

max_issues_repo_name: proglang/incorrectness

max_forks_repo_name: proglang/incorrectness


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Many properties which hold for `∼` also hold for `flip ∼`. Unlike
-- the module `Relation.Binary.Construct.Flip` this module does not
-- flip the underlying equality.
------------------------------------------------------------------------

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

open import Relation.Binary

module Relation.Binary.Construct.Converse where

open import Function
open import Data.Product

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

module _ {a ℓ} {A : Set a} (∼ : Rel A ℓ) where

  refl : Reflexive ∼ → Reflexive (flip ∼)
  refl refl = refl

  sym : Symmetric ∼ → Symmetric (flip ∼)
  sym sym = sym

  trans : Transitive ∼ → Transitive (flip ∼)
  trans trans = flip trans

  asym : Asymmetric ∼ → Asymmetric (flip ∼)
  asym asym = asym

  total : Total ∼ → Total (flip ∼)
  total total x y = total y x

  resp : ∀ {p} (P : A → Set p) → Symmetric ∼ →
             P Respects ∼ → P Respects (flip ∼)
  resp _ sym resp ∼ = resp (sym ∼)

  max : ∀ {⊥} → Minimum ∼ ⊥ → Maximum (flip ∼) ⊥
  max min = min

  min : ∀ {⊤} → Maximum ∼ ⊤ → Minimum (flip ∼) ⊤
  min max = max

module _ {a ℓ₁ ℓ₂} {A : Set a} {≈ : Rel A ℓ₁} (∼ : Rel A ℓ₂) where

  reflexive : Symmetric ≈ → (≈ ⇒ ∼) → (≈ ⇒ flip ∼)
  reflexive sym impl = impl ∘ sym

  irrefl : Symmetric ≈ → Irreflexive ≈ ∼ → Irreflexive ≈ (flip ∼)
  irrefl sym irrefl x≈y y∼x = irrefl (sym x≈y) y∼x

  antisym : Antisymmetric ≈ ∼ → Antisymmetric ≈ (flip ∼)
  antisym antisym = flip antisym

  compare : Trichotomous ≈ ∼ → Trichotomous ≈ (flip ∼)
  compare cmp x y with cmp x y
  ... | tri< x<y x≉y y≮x = tri> y≮x x≉y x<y
  ... | tri≈ x≮y x≈y y≮x = tri≈ y≮x x≈y x≮y
  ... | tri> x≮y x≉y y<x = tri< y<x x≉y x≮y

module _ {a ℓ₁ ℓ₂} {A : Set a} (∼₁ : Rel A ℓ₁) (∼₂ : Rel A ℓ₂) where

  resp₂ : ∼₁ Respects₂ ∼₂ → (flip ∼₁) Respects₂ ∼₂
  resp₂ (resp₁ , resp₂) = resp₂ , resp₁

module _ {a b ℓ} {A : Set a} {B : Set b} (∼ : REL A B ℓ) where

  dec : Decidable ∼ → Decidable (flip ∼)
  dec dec = flip dec

------------------------------------------------------------------------
-- Structures

module _ {a ℓ} {A : Set a} {≈ : Rel A ℓ} where

  isEquivalence : IsEquivalence ≈ → IsEquivalence (flip ≈)
  isEquivalence eq = record
    { refl  = refl  ≈ Eq.refl
    ; sym   = sym   ≈ Eq.sym
    ; trans = trans ≈ Eq.trans
    }
    where module Eq = IsEquivalence eq

  isDecEquivalence : IsDecEquivalence ≈ → IsDecEquivalence (flip ≈)
  isDecEquivalence eq = record
    { isEquivalence = isEquivalence Dec.isEquivalence
    ; _≟_           = dec ≈ Dec._≟_
    }
    where module Dec = IsDecEquivalence eq

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

  isPreorder : IsPreorder ≈ ∼ → IsPreorder ≈ (flip ∼)
  isPreorder O = record
    { isEquivalence = O.isEquivalence
    ; reflexive     = reflexive ∼ O.Eq.sym O.reflexive
    ; trans         = trans ∼ O.trans
    }
    where module O = IsPreorder O

  isPartialOrder : IsPartialOrder ≈ ∼ → IsPartialOrder ≈ (flip ∼)
  isPartialOrder O = record
    { isPreorder = isPreorder O.isPreorder
    ; antisym    = antisym ∼ O.antisym
    }
    where module O = IsPartialOrder O

  isTotalOrder : IsTotalOrder ≈ ∼ → IsTotalOrder ≈ (flip ∼)
  isTotalOrder O = record
    { isPartialOrder = isPartialOrder O.isPartialOrder
    ; total          = total ∼ O.total
    }
    where module O = IsTotalOrder O

  isDecTotalOrder : IsDecTotalOrder ≈ ∼ → IsDecTotalOrder ≈ (flip ∼)
  isDecTotalOrder O = record
    { isTotalOrder = isTotalOrder O.isTotalOrder
    ; _≟_          = O._≟_
    ; _≤?_         = dec ∼ O._≤?_
    }
    where module O = IsDecTotalOrder O

  isStrictPartialOrder : IsStrictPartialOrder ≈ ∼ →
                         IsStrictPartialOrder ≈ (flip ∼)
  isStrictPartialOrder O = record
    { isEquivalence = O.isEquivalence
    ; irrefl        = irrefl ∼ O.Eq.sym O.irrefl
    ; trans         = trans ∼ O.trans
    ; <-resp-≈      = resp₂ ∼ ≈ O.<-resp-≈
    }
    where module O = IsStrictPartialOrder O

  isStrictTotalOrder : IsStrictTotalOrder ≈ ∼ →
                       IsStrictTotalOrder ≈ (flip ∼)
  isStrictTotalOrder O = record
    { isEquivalence = O.isEquivalence
    ; trans         = trans ∼ O.trans
    ; compare       = compare ∼ O.compare
    }
    where module O = IsStrictTotalOrder O

module _ {a ℓ} where

  setoid : Setoid a ℓ → Setoid a ℓ
  setoid S = record
    { isEquivalence = isEquivalence S.isEquivalence
    }
    where module S = Setoid S

  decSetoid : DecSetoid a ℓ → DecSetoid a ℓ
  decSetoid S = record
    { isDecEquivalence = isDecEquivalence S.isDecEquivalence
    }
    where module S = DecSetoid S

module _ {a ℓ₁ ℓ₂} where

  preorder : Preorder a ℓ₁ ℓ₂ → Preorder a ℓ₁ ℓ₂
  preorder O = record
    { isPreorder = isPreorder O.isPreorder
    }
    where module O = Preorder O

  poset : Poset a ℓ₁ ℓ₂ → Poset a ℓ₁ ℓ₂
  poset O = record
    { isPartialOrder = isPartialOrder O.isPartialOrder
    }
    where module O = Poset O

  totalOrder : TotalOrder a ℓ₁ ℓ₂ → TotalOrder a ℓ₁ ℓ₂
  totalOrder O = record
    { isTotalOrder = isTotalOrder O.isTotalOrder
    }
    where module O = TotalOrder O

  decTotalOrder : DecTotalOrder a ℓ₁ ℓ₂ → DecTotalOrder a ℓ₁ ℓ₂
  decTotalOrder O = record
    { isDecTotalOrder = isDecTotalOrder O.isDecTotalOrder
    }
    where module O = DecTotalOrder O

  strictPartialOrder : StrictPartialOrder a ℓ₁ ℓ₂ →
                       StrictPartialOrder a ℓ₁ ℓ₂
  strictPartialOrder O = record
    { isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
    }
    where module O = StrictPartialOrder O

  strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂ →
                     StrictTotalOrder a ℓ₁ ℓ₂
  strictTotalOrder O = record
    { isStrictTotalOrder = isStrictTotalOrder O.isStrictTotalOrder
    }
    where module O = StrictTotalOrder O


text:
-- {-# OPTIONS -v tc.conv:50 -v tc.reduce:100 -v tc:50 -v tc.term.expr.coind:15 -v tc.meta:20 #-}
-- 2012-03-15, reported by Nisse
module Issue585 where

open import Common.Coinduction

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

data Fin : ℕ → Set where
  zero : ∀ {n}         → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)

infixr 5 _∷_

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

lookup : ∀ {n A} → Fin n → Vec A n → A
lookup zero    (x ∷ xs) = x
lookup (suc i) (x ∷ xs) = lookup i xs

infixl 9 _·_

data Tm (n : ℕ) : Set where
  var : Fin n → Tm n
  ƛ   : Tm (suc n) → Tm n
  _·_ : Tm n → Tm n → Tm n

infixr 8 _⇾_

data Ty : Set where
  _⇾_ : ∞ Ty → ∞ Ty → Ty

Ctxt : ℕ → Set
Ctxt n = Vec Ty n

infix 4 _⊢_∈_

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

Ω : Tm zero
Ω = ω · ω
  where ω = ƛ (var zero · var zero)

Ω-has-any-type : ∀ τ → [] ⊢ Ω ∈ τ
Ω-has-any-type τ =
  _·_ {σ = σ} {τ = ♯ _} (ƛ (var · var)) (ƛ (var · var))
  where
  σ : ∞ Ty
  σ = ♯ (σ ⇾ ♯ _) -- τ)

-- If the last
-- underscore is replaced by τ, then the code checks successfully.

-- WAS: Agda seems to loop when checking Ω-has-any-type.

-- NOW: this should leave metas unsolved.


text:
module IPC.Metatheory.Gentzen-KripkeExploding where

open import IPC.Syntax.Gentzen public
open import IPC.Semantics.KripkeExploding public

-- Soundness with respect to all models, or evaluation.

eval : ∀ {A Γ} → Γ ⊢ A → Γ ⊨ A
eval (var i)                  γ = lookup i γ
eval (lam {A} {B} t)          γ = return {A ▻ B} λ ξ a →
                                    eval t (mono⊩⋆ ξ γ , a)
eval (app {A} {B} t u)        γ = bind {A ▻ B} {B} (eval t γ) λ ξ f →
                                    _⟪$⟫_ {A} {B} f (eval u (mono⊩⋆ ξ γ))
eval (pair {A} {B} t u)       γ = return {A ∧ B} (eval t γ , eval u γ)
eval (fst {A} {B} t)          γ = bind {A ∧ B} {A} (eval t γ) (K π₁)
eval (snd {A} {B} t)          γ = bind {A ∧ B} {B} (eval t γ) (K π₂)
eval unit                     γ = return {⊤} ∙
eval (boom {C} t)             γ = bind {⊥} {C} (eval t γ) (K elim𝟘)
eval (inl {A} {B} t)          γ = return {A ∨ B} (ι₁ (eval t γ))
eval (inr {A} {B} t)          γ = return {A ∨ B} (ι₂ (eval t γ))
eval (case {A} {B} {C} t u v) γ = bind {A ∨ B} {C} (eval t γ) λ ξ s → elim⊎ s
                                    (λ a → eval u (mono⊩⋆ ξ γ , λ ξ′ k → a ξ′ k))
                                    (λ b → eval v (mono⊩⋆ ξ γ , λ ξ′ k → b ξ′ k))

-- TODO: Correctness of evaluation with respect to conversion.

-- The canonical model.

private
  instance
    canon : Model
    canon = record
      { World   = Cx Ty
      ; _≤_     = _⊆_
      ; refl≤   = refl⊆
      ; trans≤  = trans⊆
      ; _⊪ᵅ_   = λ Γ P → Γ ⊢ α P
      ; mono⊪ᵅ = mono⊢
      ; _‼_     = λ Γ A → Γ ⊢ A
      }

-- Soundness and completeness with respect to the canonical model.

mutual
  reflectᶜ : ∀ {A Γ} → Γ ⊢ A → Γ ⊩ A
  reflectᶜ {α P}   t = return {α P} t
  reflectᶜ {A ▻ B} t = return {A ▻ B} λ η a →
                         reflectᶜ {B} (app (mono⊢ η t) (reifyᶜ {A} a))
  reflectᶜ {A ∧ B} t = return {A ∧ B} (reflectᶜ {A} (fst t) , reflectᶜ {B} (snd t))
  reflectᶜ {⊤}    t = return {⊤} ∙
  reflectᶜ {⊥}    t = λ η k → boom (mono⊢ η t)
  reflectᶜ {A ∨ B} t = λ η k → case (mono⊢ η t)
                                  (k weak⊆ (ι₁ (reflectᶜ {A} v₀)))
                                  (k weak⊆ (ι₂ (reflectᶜ {B} (v₀))))

  reifyᶜ : ∀ {A Γ} → Γ ⊩ A → Γ ⊢ A
  reifyᶜ {α P}   k = k refl≤ λ η s → s
  reifyᶜ {A ▻ B} k = k refl≤ λ η s → lam (reifyᶜ {B} (s weak⊆ (reflectᶜ {A} (v₀))))
  reifyᶜ {A ∧ B} k = k refl≤ λ η s → pair (reifyᶜ {A} (π₁ s)) (reifyᶜ {B} (π₂ s))
  reifyᶜ {⊤}    k = k refl≤ λ η s → unit
  reifyᶜ {⊥}    k = k refl≤ λ η ()
  reifyᶜ {A ∨ B} k = k refl≤ λ η s → elim⊎ s
                                        (λ a → inl (reifyᶜ {A} (λ η′ k → a η′ k)))
                                        (λ b → inr (reifyᶜ {B} (λ η′ k → b η′ k)))

reflectᶜ⋆ : ∀ {Ξ Γ} → Γ ⊢⋆ Ξ → Γ ⊩⋆ Ξ
reflectᶜ⋆ {∅}     ∙        = ∙
reflectᶜ⋆ {Ξ , A} (ts , t) = reflectᶜ⋆ ts , reflectᶜ t

reifyᶜ⋆ : ∀ {Ξ Γ} → Γ ⊩⋆ Ξ → Γ ⊢⋆ Ξ
reifyᶜ⋆ {∅}     ∙        = ∙
reifyᶜ⋆ {Ξ , A} (ts , t) = reifyᶜ⋆ ts , reifyᶜ t

-- Reflexivity and transitivity.

refl⊩⋆ : ∀ {Γ} → Γ ⊩⋆ Γ
refl⊩⋆ = reflectᶜ⋆ refl⊢⋆

trans⊩⋆ : ∀ {Γ Γ′ Γ″} → Γ ⊩⋆ Γ′ → Γ′ ⊩⋆ Γ″ → Γ ⊩⋆ Γ″
trans⊩⋆ ts us = reflectᶜ⋆ (trans⊢⋆ (reifyᶜ⋆ ts) (reifyᶜ⋆ us))

-- Completeness with respect to all models, or quotation.

quot : ∀ {A Γ} → Γ ⊨ A → Γ ⊢ A
quot s = reifyᶜ (s refl⊩⋆)

-- Normalisation by evaluation.

norm : ∀ {A Γ} → Γ ⊢ A → Γ ⊢ A
norm = quot ∘ eval

-- TODO: Correctness of normalisation with respect to conversion.

max_stars_repo_name: mietek/hilbert-gentzen

max_issues_repo_name: mietek/hilbert-gentzen

max_forks_repo_name: mietek/hilbert-gentzen


text:
-- 2013-11-xx Andreas
-- Previous clauses did not reduce in later clauses under
-- a module telescope.

{-# OPTIONS --copatterns #-}
-- {-# OPTIONS -v interaction.give:20 -v tc.cc:60 -v reify.clause:60 -v tc.section.check:10 -v tc:90 #-}
-- {-# OPTIONS -v tc.lhs:20 #-}
-- {-# OPTIONS -v tc.cover:20 #-}

module Issue937 where

data Nat : Set where
  zero : Nat
  suc : Nat → Nat
{-# BUILTIN NATURAL Nat #-}

infixr 4 _,_

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

open Σ public

data _≤_ : Nat → Nat → Set  where
  z≤n : ∀ {n}                 → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

_<_ : Nat → Nat → Set
m < n = suc m ≤ n

ex : Σ Nat (λ n → zero < n)
proj₁ ex = suc zero
proj₂ ex = s≤s z≤n -- works

ex' : Σ Nat (λ n → zero < n)
proj₁ ex' = suc zero
proj₂ ex' = {! s≤s z≤n !}

module _ (A : Set) where

  ex'' : Σ Nat (λ n → zero < n)
  proj₁ ex'' = suc zero
  proj₂ ex'' = s≤s z≤n -- works

  ex''' : Σ Nat (λ n → zero < n)
  proj₁ ex''' = suc zero
  proj₂ ex''' = {! s≤s z≤n !}

-- The normalized goals should be printed as 1 ≤ 1


text:
-- MIT License

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

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

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

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

{-# OPTIONS --guardedness #-}

open import Data.Product
open import Data.Sum

open import Common

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

open import SessionType message
open import Transitions message
open import Session message

data Progress : Session -> Set where
  win#def : ∀{T S} (w : Win T) (def : Defined S) -> Progress (T # S)
  inp#out : ∀{f g} (W : Witness g) -> Progress (inp f # out g)
  out#inp : ∀{f g} (W : Witness f) -> Progress (out f # inp g)

progress-sound : ∀{S} -> Progress S -> ProgressS S
progress-sound (win#def e def) = inj₁ (win#def e def)
progress-sound (inp#out (_ , !x)) = inj₂ (_ , sync inp (out !x))
progress-sound (out#inp (_ , !x)) = inj₂ (_ , sync (out !x) inp)

progress-complete : ∀{S} -> ProgressS S -> Progress S
progress-complete (inj₁ (win#def e def)) = win#def e def
progress-complete (inj₂ (_ , sync inp (out !x))) = inp#out (_ , !x)
progress-complete (inj₂ (_ , sync (out !x) inp)) = out#inp (_ , !x)

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda


text:
open import Functional
open import Logic
open import Logic.Propositional
open import Type

module Relator.Ordering where

module From-[<][≡] {ℓ₁}{ℓ₂}{ℓ₃} {T : Type{ℓ₁}} (_<_ : T → T → Stmt{ℓ₂}) (_≡_ : T → T → Stmt{ℓ₃}) where
  -- Greater than
  _>_ : T → T → Stmt
  _>_ = swap(_<_)

  -- Lesser than or equals
  _≤_ : T → T → Stmt
  x ≤ y = (x < y) ∨ (x ≡ y)

  -- Greater than or equals
  _≥_ : T → T → Stmt
  x ≥ y = (x > y) ∨ (x ≡ y)

  -- In an open interval
  _<_<_ : T → T → T → Stmt
  x < y < z = (x < y) ∧ (y < z)

  -- In an closed interval
  _≤_≤_ : T → T → T → Stmt
  x ≤ y ≤ z = (x ≤ y) ∧ (y ≤ z)

  _≮_ : T → T → Stmt
  _≮_ = (¬_) ∘₂ (_<_)

  _≯_ : T → T → Stmt
  _≯_ = (¬_) ∘₂ (_>_)

  _≰_ : T → T → Stmt
  _≰_ = (¬_) ∘₂ (_≤_)

  _≱_ : T → T → Stmt
  _≱_ = (¬_) ∘₂ (_≥_)

module From-[≤] {ℓ₁}{ℓ₂} {T : Type{ℓ₁}} (_≤_ : T → T → Stmt{ℓ₂}) where
  -- Greater than or equals
  _≥_ : T → T → Stmt
  _≥_ = swap(_≤_)

  _≰_ : T → T → Stmt
  _≰_ = (¬_) ∘₂ (_≤_)

  _≱_ : T → T → Stmt
  _≱_ = swap(_≰_)

  -- Greater than
  _>_ : T → T → Stmt
  _>_ = _≰_

  -- Lesser than or equals
  _<_ : T → T → Stmt
  _<_ = swap(_>_)

  -- In an open interval
  _<_<_ : T → T → T → Stmt
  x < y < z = (x < y) ∧ (y < z)

  -- In an closed interval
  _≤_≤_ : T → T → T → Stmt
  x ≤ y ≤ z = (x ≤ y) ∧ (y ≤ z)

  _≮_ : T → T → Stmt
  _≮_ = (¬_) ∘₂ (_<_)

  _≯_ : T → T → Stmt
  _≯_ = (¬_) ∘₂ (_>_)

module From-[≤][<] {ℓ₁}{ℓ₂}{ℓ₃} {T : Type{ℓ₁}} (_≤_ : T → T → Stmt{ℓ₂}) (_<_ : T → T → Stmt{ℓ₃}) where
  -- Greater than
  _>_ : T → T → Stmt
  _>_ = swap(_<_)

  -- Greater than or equals
  _≥_ : T → T → Stmt
  _≥_ = swap(_≤_)

  -- In an open interval
  _<_<_ : T → T → T → Stmt
  x < y < z = (x < y) ∧ (y < z)

  -- In an closed interval
  _≤_≤_ : T → T → T → Stmt
  x ≤ y ≤ z = (x ≤ y) ∧ (y ≤ z)

  _≮_ : T → T → Stmt
  _≮_ = (¬_) ∘₂ (_<_)

  _≯_ : T → T → Stmt
  _≯_ = (¬_) ∘₂ (_>_)

  _≰_ : T → T → Stmt
  _≰_ = (¬_) ∘₂ (_≤_)

  _≱_ : T → T → Stmt
  _≱_ = (¬_) ∘₂ (_≥_)

module From-[≤][≢] {ℓ₁}{ℓ₂}{ℓ₃} {T : Type{ℓ₁}} (_≤_ : T → T → Stmt{ℓ₂}) (_≢_ : T → T → Stmt{ℓ₃}) where
  -- Lesser than or equals
  _<_ : T → T → Stmt
  x < y = (x ≤ y) ∧ (x ≢ y)

  -- Greater than
  _>_ : T → T → Stmt
  _>_ = swap(_<_)

  -- Greater than or equals
  _≥_ : T → T → Stmt
  _≥_ = swap(_≤_)

  -- In an open interval
  _<_<_ : T → T → T → Stmt
  x < y < z = (x < y) ∧ (y < z)

  -- In an closed interval
  _≤_≤_ : T → T → T → Stmt
  x ≤ y ≤ z = (x ≤ y) ∧ (y ≤ z)

  _≮_ : T → T → Stmt
  _≮_ = (¬_) ∘₂ (_<_)

  _≯_ : T → T → Stmt
  _≯_ = (¬_) ∘₂ (_>_)

  _≰_ : T → T → Stmt
  _≰_ = (¬_) ∘₂ (_≤_)

  _≱_ : T → T → Stmt
  _≱_ = (¬_) ∘₂ (_≥_)


text:
{-
This second-order equational theory was created from the following second-order syntax description:

syntax Sub | S

type
  L : 0-ary
  T : 0-ary

term
  vr : L  ->  T
  sb : L.T  T  ->  T

theory
  (C) x y : T |> sb (a. x[], y[]) = x[]
  (L) x : T |> sb (a. vr(a), x[]) = x[]
  (R) a : L  x : L.T |> sb (b. x[b], vr(a[])) = x[a[]]
  (A) x : (L,L).T  y : L.T  z : T |> sb (a. sb (b. x[a,b], y[a]), z[]) = sb (b. sb (a. x[a, b], z[]), sb (a. y[a], z[]))
-}

module Sub.Equality where

open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Families.Build
open import SOAS.ContextMaps.Inductive

open import Sub.Signature
open import Sub.Syntax

open import SOAS.Metatheory.SecondOrder.Metasubstitution S:Syn
open import SOAS.Metatheory.SecondOrder.Equality S:Syn

private
  variable
    α β γ τ : ST
    Γ Δ Π : Ctx

infix 1 _▹_⊢_≋ₐ_

-- Axioms of equality
data _▹_⊢_≋ₐ_ : ∀ 𝔐 Γ {α} → (𝔐 ▷ S) α Γ → (𝔐 ▷ S) α Γ → Set where
  C : ⁅ T ⁆ ⁅ T ⁆̣     ▹ ∅ ⊢              sb 𝔞 𝔟 ≋ₐ 𝔞
  L : ⁅ T ⁆̣           ▹ ∅ ⊢        sb (vr x₀) 𝔞 ≋ₐ 𝔞
  R : ⁅ L ⁆ ⁅ L ⊩ T ⁆̣ ▹ ∅ ⊢ sb (𝔟⟨ x₀ ⟩) (vr 𝔞) ≋ₐ 𝔟⟨ 𝔞 ⟩
  A : ⁅ L · L ⊩ T ⁆ ⁅ L ⊩ T ⁆ ⁅ T ⁆̣ ▹ ∅
    ⊢  sb (sb (𝔞⟨ x₁ ◂ x₀ ⟩) (𝔟⟨ x₀ ⟩)) 𝔠
    ≋ₐ sb (sb (𝔞⟨ x₀ ◂ x₁ ⟩) 𝔠) (sb (𝔟⟨ x₀ ⟩) 𝔠)

open EqLogic _▹_⊢_≋ₐ_
open ≋-Reasoning

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

open import LogicalFormulae
open import Functions.Definition

module Orders.Partial.Definition {a : _} (carrier : Set a) where

record PartialOrder {b : _} : Set (a ⊔ lsuc b) where
  field
    _<_ : Rel {a} {b} carrier
    irreflexive : {x : carrier} → (x < x) → False
    <Transitive : {a b c : carrier} → (a < b) → (b < c) → (a < c)
  <WellDefined : {r s t u : carrier} → (r ≡ t) → (s ≡ u) → r < s → t < u
  <WellDefined refl refl r<s = r<s


text:
module x08-747Quantifiers-hc where

-- Library

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; z≤n; s≤s) -- added ≤
-- open import Data.Nat.Properties using (≤-refl)
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) -- added proj₂
open import Data.Sum using (_⊎_; inj₁; inj₂ ) -- added inj₁, inj₂
open import Function using (_∘_) -- added

-- BEGIN: Copied from 747Isomorphism.
postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    → f ≡ g

infix 0 _≃_
record _≃_ (A B : Set) : Set where
  constructor mk-≃
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
open _⇔_
-- END: Copied from 747Isomorphism.

-- Logical forall is ∀.
-- Forall elimination is function application.
∀-elim : ∀ {A : Set} {B : A → Set}
  → (L : ∀ (x : A) → B x)
  → (M : A)
    -----------------
  → B M
∀-elim L M = L M

-- A → B is nicer syntax for ∀ (_ : A) → B.

-- 747/PLFA exercise: ForAllDistProd (1 point)
-- ∀ distributes over ×
-- (note: → distributes over × was shown in Connectives)

∀-distrib-× : ∀ {A : Set} {B C : A → Set} →
  (∀ (a : A) → B a × C a) ≃ (∀ (a : A) → B a) × (∀ (a : A) → C a)
to      ∀-distrib-× a→Ba×Ca         = ⟨ proj₁ ∘ a→Ba×Ca , proj₂ ∘ a→Ba×Ca ⟩
from    ∀-distrib-× ⟨ a→ba , a→ca ⟩ = λ a → ⟨ a→ba a , a→ca a ⟩
from∘to ∀-distrib-× a→Ba×Ca         = refl
to∘from ∀-distrib-× ⟨ a→ba , a→ca ⟩ = refl

-- 747/PLFA exercise: SumForAllImpForAllSum (1 point)
-- disjunction of foralls implies a forall of disjunctions
⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set} →
  (∀ (a : A) → B a) ⊎ (∀ (a : A) → C a)  →  ∀ (a : A) → B a ⊎ C a
⊎∀-implies-∀⊎ (inj₁ a→ba) = inj₁ ∘ a→ba
⊎∀-implies-∀⊎ (inj₂ a→ca) = inj₂ ∘ a→ca

-- Existential quantification
-- a pair:
-- - a witness and
-- - a proof that the witness satisfies the property
data Σ (A : Set) (B : A → Set) : Set where
  ⟨_,_⟩ : (a : A) → B a → Σ A B

-- convenient syntax

Σ-syntax = Σ
infix 2 Σ-syntax
syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

-- can use the RHS syntax in code,
-- but LHS will show up in displays of goal and context.
-- This syntax is equivalent to defining a dependent record type.

record Σ′ (A : Set) (B : A → Set) : Set where
  field
    proj₁′ : A
    proj₂′ : B proj₁′

-- convention : library uses ∃ when domain of bound variable is implicit

∃ : ∀ {A : Set} (B : A → Set) → Set
∃ {A} B = Σ A B

-- syntax

∃-syntax = ∃
syntax ∃-syntax (λ x → B) = ∃[ x ] B

-- eliminate existential with a function
-- that consumes the witness and proof
-- and reaches a conclusion C
∃-elim : ∀ {A : Set} {B : A → Set} {C : Set}
  → (∀ a → B a → C)
  → ∃[ a ] B a
    ---------------
  → C
∃-elim a→Ba→C ⟨ a , Ba ⟩ = a→Ba→C a Ba

-- generalization of currying (from Connectives)
-- currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)
∀∃-currying : ∀ {A : Set} {B : A → Set} {C : Set}
  → (∀ a → B a → C) ≃ (∃[ a ] B a → C)
_≃_.to      ∀∃-currying a→Ba→C ⟨ a , Ba ⟩ = a→Ba→C a Ba
_≃_.from    ∀∃-currying ∃xB a Ba          = ∃xB ⟨ a , Ba ⟩
_≃_.from∘to ∀∃-currying a→Ba→C            = refl
_≃_.to∘from ∀∃-currying ∃xB               = extensionality λ { ⟨ a , Ba ⟩ → refl}

-- 747/PLFA exercise: ExistsDistSum (2 points)
-- existentials distribute over disjunction
∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set} →
  ∃[ a ] (B a ⊎ C a) ≃ (∃[ a ] B a) ⊎ (∃[ a ] C a)
to      ∃-distrib-⊎       ⟨ a , inj₁ Ba ⟩  = inj₁ ⟨ a ,      Ba ⟩
to      ∃-distrib-⊎       ⟨ a , inj₂ Ca ⟩  = inj₂ ⟨ a ,      Ca ⟩
from    ∃-distrib-⊎ (inj₁ ⟨ a ,      Ba ⟩) =      ⟨ a , inj₁ Ba ⟩
from    ∃-distrib-⊎ (inj₂ ⟨ a ,      Ca ⟩) =      ⟨ a , inj₂ Ca ⟩
from∘to ∃-distrib-⊎       ⟨ a , inj₁ Ba ⟩  = refl
from∘to ∃-distrib-⊎       ⟨ a , inj₂ Ca ⟩  = refl
to∘from ∃-distrib-⊎ (inj₁ ⟨ a ,      Ba ⟩) = refl
to∘from ∃-distrib-⊎ (inj₂ ⟨ a ,      Ca ⟩) = refl

-- 747/PLFA exercise: ExistsProdImpProdExists (1 point)
-- existentials distribute over ×
∃×-implies-×∃ : ∀ {A : Set} {B C : A → Set} →
  ∃[ a ] (B a × C a) → (∃[ a ] B a) × (∃[ a ] C a)
∃×-implies-×∃ ⟨ a , ⟨ Ba , Ca ⟩ ⟩ = ⟨ ⟨ a , Ba ⟩ , ⟨ a , Ca ⟩ ⟩

-- existential example: revisiting even/odd.
-- mutually-recursive definitions of even and odd.
data even : ℕ → Set
data odd  : ℕ → Set

data even where

  even-zero : even zero

  even-suc : ∀ {n : ℕ}
    → odd n
      ------------
    → even (suc n)

data odd where
  odd-suc : ∀ {n : ℕ}
    → even n
      -----------
    → odd (suc n)

-- number is even iff it is          double some other number
even-∃ : ∀ {n : ℕ} → even n → ∃[ m ] (    m * 2 ≡ n)
-- number is odd  iff it is one plus double some other number
odd-∃  : ∀ {n : ℕ} →  odd n → ∃[ m ] (1 + m * 2 ≡ n)

even-∃  even-zero = ⟨ zero , refl ⟩
even-∃ (even-suc odd-suc-x*2)
    with odd-∃ odd-suc-x*2
... | ⟨ x , refl ⟩ = ⟨ suc x , refl ⟩
odd-∃  (odd-suc  even-x*2)
    with even-∃ even-x*2
... | ⟨ x , refl ⟩ = ⟨     x , refl ⟩

∃-even : ∀ {n : ℕ} → ∃[ m ] (    m * 2 ≡ n) → even n
∃-odd  : ∀ {n : ℕ} → ∃[ m ] (1 + m * 2 ≡ n) →  odd n

∃-even ⟨ zero  , refl ⟩ = even-zero
∃-even ⟨ suc x , refl ⟩ = even-suc (∃-odd  ⟨ x , refl ⟩)
∃-odd  ⟨     x , refl ⟩ = odd-suc  (∃-even ⟨ x , refl ⟩)

-- PLFA exercise: what if we write the arithmetic more "naturally"?
-- (Proof gets harder but is still doable).

-- 747/PLFA exercise: AltLE (3 points)
-- alternate definition of y ≤ z
-- (Optional exercise: Is this an isomorphism?)
+0 : ∀ (m : ℕ) → m + zero ≡ m
+0  zero   = refl
+0 (suc m) = cong suc (+0 m)

open import x03-842Relations-hc-2 using (s≤s)

xxx : ∀ {m n : ℕ} → m ≤ n → suc (m + zero) ≤ suc n
xxx {m} {n} p rewrite +0 m = s≤s p

≤-refl : ∀ {n : ℕ}
    -----
  → n ≤ n
≤-refl {zero}  = z≤n
≤-refl {suc n} = s≤s (≤-refl {n})

+-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)
+-suc  zero   n = refl
+-suc (suc m) n = cong suc (+-suc m n)

aaa : ∀ {x y z : ℕ} → y + suc x ≡ z → y ≤ y + suc x
--aaa {x} {y} y+sucx≡z rewrite sym y+sucx≡z {- | +-suc y x -} = {!!}
aaa {zero}  {zero}  refl = z≤n
aaa {suc x} {zero}  refl = z≤n
aaa {zero}  {suc y} refl = s≤s {!!}
aaa {suc x} {suc y} refl = s≤s {!!}

zzz : ∀ {y z : ℕ} → y + zero ≡ z → y ≤ z
zzz {y} y+x≡z rewrite +0 y | y+x≡z | sym y+x≡z = ≤-refl {y}

∃-≤ : ∀ {y z : ℕ} → ( (y ≤ z) ⇔ ( ∃[ x ] (y + x ≡ z) ) )
{-
∃-≤ {y} {z} = record { to = λ { z≤n → ⟨ zero , {!!} ⟩ ; (s≤s y≤z) → {!!} }; from = {!!} }
-}
to   ∃-≤           z≤n        = ⟨          zero  , {!!} ⟩
to   ∃-≤      (s≤s z≤n)       = ⟨      suc zero  , {!!} ⟩
to   ∃-≤ (s≤s (s≤s m≤n))      = ⟨ suc (suc zero) , {!!} ⟩
from ∃-≤ ⟨ zero  , y+zero≡z ⟩ = zzz y+zero≡z
from ∃-≤ ⟨ suc x , y+sucx≡z ⟩ rewrite sym y+sucx≡z = {!!}

-- The negation of an existential is isomorphic to a universal of a negation.
¬∃≃∀¬ : ∀ {A : Set} {B : A → Set}
  → (¬ ∃[ a ] B a) ≃ ∀ a → ¬ B a
to      ¬∃≃∀¬ = λ { ¬∃B     a → λ Ba   → ¬∃B ⟨ a , Ba ⟩ }
from    ¬∃≃∀¬ = λ { a→¬Ba ⟨ a ,   Ba ⟩ → a→¬Ba a   Ba }
from∘to ¬∃≃∀¬ = λ   ¬∃B                → {!!} -- TODO
to∘from ¬∃≃∀¬ = λ   a→¬Ba              → refl

-- 747/PLFA exercise: ExistsNegImpNegForAll (1 point)
-- Existence of negation implies negation of universal.

∃¬-implies-¬∀ : ∀ {A : Set} {B : A → Set}
  → ∃[ a ] (¬ B a)
    --------------
  → ¬ (∀ a → B a)
∃¬-implies-¬∀ ⟨ a , ¬Ba ⟩ = λ a→Ba → ¬Ba (a→Ba a)

-- The converse cannot be proved in intuitionistic logic.

-- PLFA exercise: isomorphism between naturals and existence of canonical binary.
-- This is essentially what we did at the end of 747Isomorphism.

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.Vec.Relation.Unary.Any directly.
------------------------------------------------------------------------

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

module Data.Vec.Any where

open import Data.Vec.Relation.Unary.Any public