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

module Paths where

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

open import PointedTypes

--infix  2  _∎      -- equational reasoning
--infixr 2  _≡⟨_⟩_  -- equational reasoning

------------------------------------------------------------------------------
-- Paths are pi-combinators

data _⇛_ {ℓ : Level} :
  (A• : Set• ℓ) → (B• : Set• ℓ) → Set (lsuc (lsuc ℓ)) where
  -- additive structure
  swap₁₊⇛    : {A B : Set ℓ} {a : A} {b : B} →
               •[ A ⊎ B , inj₁ a ] ⇛ •[ B ⊎ A , inj₂ a ]
  id⇛        : {A : Set ℓ} → (a : A) → •[ A , a ] ⇛ •[ A , a ]
  η⋆⇛        : {A : Set ℓ} {a : A} → •[ A , a ] ⇛ •[ (A → A) , id ]
  equiv⇛     : {A B : Set ℓ} {a : A} {b : B} →
               (f : •[ A , a ] →• •[ B , b ]) →
               (fequiv : isequiv• f) →
               •[ A , a ] ⇛ •[ B , b ]

swap₊ : {ℓ : Level} {A B : Set ℓ} → A ⊎ B → B ⊎ A
swap₊ (inj₁ a) = inj₂ a
swap₊ (inj₂ b) = inj₁ b

eval : {ℓ : Level} {A• B• : Set• ℓ} → A• ⇛ B• → (A• →• B•)
eval swap₁₊⇛ = record { fun = swap₊ ; resp• = refl }
eval (id⇛ _) = id•
eval η⋆⇛ = {!!}
eval (equiv⇛ _ _) = {!!}

pInversion : {ℓ : Level} {A• B• : Set• ℓ} → (c : A• ⇛ B•) → fun (eval c) (• A•) ≡ • B•
pInversion {ℓ} {A•} {B•} c = resp• (eval c)

funext : {ℓ : Level} {A• B• : Set• ℓ} {f g : A• →• B•} →
         (pt f ⇛ pt g) → (f ∼• g)
funext = {!!}

{--
  swap₂₊⇛    : {A• B• : Set• {ℓ}} → (A• ⊎•₂ B•) ⇛ (B• ⊎•₁ A•)
  assocl₁₊⇛  : {A• B• C• : Set• {ℓ}} →
               (A• ⊎•₁ (B• ⊎•₁ C•)) ⇛ ((A• ⊎•₁ B•) ⊎•₁ C•)
  assocl₁₊⇛' : {A• B• C• : Set• {ℓ}} →
               (A• ⊎•₁ (B• ⊎•₂ C•)) ⇛ ((A• ⊎•₁ B•) ⊎•₁ C•)
               •[ A ⊎ (B ⊎ C) , inj₁ a ] ⇛ •[ (A ⊎ B) ⊎ C , inj₁ (inj₁ a) ]
  assocl₂₁₊⇛ : {A B C : Set ℓ} → (b : B) →
               •[ A ⊎ (B ⊎ C) , inj₂ (inj₁ b) ] ⇛
               •[ (A ⊎ B) ⊎ C , inj₁ (inj₂ b) ]
  assocl₂₂₊⇛ : {A B C : Set ℓ} → (c : C) →
               •[ A ⊎ (B ⊎ C) , inj₂ (inj₂ c) ] ⇛ •[ (A ⊎ B) ⊎ C , inj₂ c ]
  assocr₁₁₊⇛ : {A B C : Set ℓ} → (a : A) →
               •[ (A ⊎ B) ⊎ C , inj₁ (inj₁ a) ] ⇛ •[ A ⊎ (B ⊎ C) , inj₁ a ]
  assocr₁₂₊⇛ : {A B C : Set ℓ} → (b : B) →
               •[ (A ⊎ B) ⊎ C , inj₁ (inj₂ b) ] ⇛
               •[ A ⊎ (B ⊎ C) , inj₂ (inj₁ b) ]
  assocr₂₊⇛  : {A B C : Set ℓ} → (c : C) →
               •[ (A ⊎ B) ⊎ C , inj₂ c ] ⇛ •[ A ⊎ (B ⊎ C) , inj₂ (inj₂ c) ]
  -- multiplicative structure
  unite⋆⇛    : {A : Set ℓ} → (a : A) → •[ ⊤ × A , (tt , a) ] ⇛ •[ A , a ]
  uniti⋆⇛    : {A : Set ℓ} → (a : A) → •[ A , a ] ⇛ •[ ⊤ × A , (tt , a) ]
  swap⋆⇛     : {A B : Set ℓ} → (a : A) → (b : B) →
               •[ A × B , (a , b) ] ⇛ •[ B × A , (b , a) ]
  assocl⋆⇛   : {A B C : Set ℓ} → (a : A) → (b : B) → (c : C) →
               •[ A × (B × C) , (a , (b , c)) ] ⇛
               •[ (A × B) × C , ((a , b) , c) ]
  assocr⋆⇛   : {A B C : Set ℓ} → (a : A) → (b : B) → (c : C) →
               •[ (A × B) × C , ((a , b) , c) ] ⇛
               •[ A × (B × C) , (a , (b , c)) ]
  -- distributivity
  dist₁⇛     : {A B C : Set ℓ} → (a : A) → (c : C) →
               •[ (A ⊎ B) × C , (inj₁ a , c) ] ⇛
               •[ (A × C) ⊎ (B × C) , inj₁ (a , c) ]
  dist₂⇛     : {A B C : Set ℓ} → (b : B) → (c : C) →
               •[ (A ⊎ B) × C , (inj₂ b , c) ] ⇛
               •[ (A × C) ⊎ (B × C) , inj₂ (b , c) ]
  factor₁⇛   : {A B C : Set ℓ} → (a : A) → (c : C) →
               •[ (A × C) ⊎ (B × C) , inj₁ (a , c) ] ⇛
               •[ (A ⊎ B) × C , (inj₁ a , c) ]
  factor₂⇛   : {A B C : Set ℓ} → (b : B) → (c : C) →
               •[ (A × C) ⊎ (B × C) , inj₂ (b , c) ] ⇛
               •[ (A ⊎ B) × C , (inj₂ b , c) ]
  -- congruence but without sym which is provable
  id⇛        : {A : Set ℓ} → (a : A) → •[ A , a ] ⇛ •[ A , a ]
  trans⇛     : {A B C : Set ℓ} {a : A} {b : B} {c : C} →
               (•[ A , a ] ⇛ •[ B , b ]) →
               (•[ B , b ] ⇛ •[ C , c ]) →
               (•[ A , a ] ⇛ •[ C , c ])
  plus₁⇛     : {A B C D : Set ℓ} {a : A} {b : B} {c : C} {d : D} →
               (•[ A , a ] ⇛ •[ C , c ]) →
               (•[ B , b ] ⇛ •[ D , d ]) →
               (•[ A ⊎ B , inj₁ a ] ⇛ •[ C ⊎ D , inj₁ c ])
  plus₂⇛     : {A B C D : Set ℓ} {a : A} {b : B} {c : C} {d : D} →
               (•[ A , a ] ⇛ •[ C , c ]) →
               (•[ B , b ] ⇛ •[ D , d ]) →
               (•[ A ⊎ B , inj₂ b ] ⇛ •[ C ⊎ D , inj₂ d ])
  times⇛     : {A B C D : Set ℓ} {a : A} {b : B} {c : C} {d : D} →
               (•[ A , a ] ⇛ •[ C , c ]) → (•[ B , b ] ⇛ •[ D , d ]) →
               (•[ A × B , (a , b) ] ⇛ •[ C × D , (c , d) ])
--}

-- Abbreviations and small examples

{--
Path : {ℓ : Level} {A B : Set ℓ} → (a : A) → (b : B) → Set (lsuc ℓ)
Path {ℓ} {A} {B} a b = •[ A , a ] ⇛ •[ B , b ]

2Path : {ℓ : Level} {A B C D : Set ℓ} {a : A} {b : B} {c : C} {d : D} →
  (p : Path a b) → (q : Path c d) → Set (lsuc (lsuc ℓ))
2Path {ℓ} {A} {B} {C} {D} {a} {b} {c} {d} p q = Path p q
  --  •[ Path a b , p ] ⇛ •[ Path c d , q ]
--}
{--
_≡⟨_⟩_ : ∀ {ℓ} → {A B C : Set ℓ} (a : A) {b : B} {c : C} →
         Path a b → Path b c → Path a c
_ ≡⟨ p ⟩ q = trans⇛ p q

_∎ : ∀ {ℓ} → {A : Set ℓ} (a : A) → Path a a
_∎ a = id⇛ a

test3 : {A : Set} {a : A} → Set•
test3 {A} {a} = •[ Path a a , id⇛ a ]

test4 : Set•
test4 = •[ Path ℕ ℕ , id⇛ ℕ ]

test5 : Set•
test5 = •[ Path (ℕ , Bool) (Bool , ℕ) , swap⋆⇛ ℕ Bool ]

test6 : Set•
test6 = •[ Path (tt , ℕ) ℕ , unite⋆⇛ ℕ ]

test7 : {A : Set} {a : A} → Set•
test7 {A} {a} = •[ 2Path (id⇛ a) (id⇛ a) , id⇛ (id⇛ a) ]

test8 : {A B C D : Set} {a : A} {b : B} {c : C} {d : D} →
        (p : Path a b) → (q : Path c d) → Set•
test8 {A} {B} {C} {D} {a} {b} {c} {d} p q =
  •[ Path (a , c) (b , d) , times⇛ p q ]

-- Propositional equality implies a path

≡Path : {ℓ : Level} {A : Set ℓ} {x y : A} → (x ≡ y) → Path x y
≡Path {ℓ} {A} {x} {.x} refl = id⇛ x
--}

------------------------------------------------------------------------------
-- Path induction

{--
pathInd : {ℓ ℓ' : Level} →
  (P : {A• B• : Set• {ℓ}} → (A• ⇛ B•) → Set ℓ') →
  ({A• B• : Set• {ℓ}} → P (swap₁₊⇛ {ℓ} {A•} {B•})) →
pathInd : {ℓ ℓ' : Level} →
  (P : {A B : Set ℓ} {a : A} {b : B} →
    (•[ A , a ] ⇛ •[ B , b ]) → Set ℓ') →
  ({A B : Set ℓ} → (a : A) → P (swap₁₊⇛ {ℓ} {A} {B} a)) →
  ({A B : Set ℓ} → (b : B) → P (swap₂₊⇛ {ℓ} {A} {B} b)) →
  ({A B C : Set ℓ} → (a : A) → P (assocl₁₊⇛ {ℓ} {A} {B} {C} a)) →
  ({A B C : Set ℓ} → (b : B) → P (assocl₂₁₊⇛ {ℓ} {A} {B} {C} b)) →
  ({A B C : Set ℓ} → (c : C) → P (assocl₂₂₊⇛ {ℓ} {A} {B} {C} c)) →
  ({A B C : Set ℓ} → (a : A) → P (assocr₁₁₊⇛ {ℓ} {A} {B} {C} a)) →
  ({A B C : Set ℓ} → (b : B) → P (assocr₁₂₊⇛ {ℓ} {A} {B} {C} b)) →
  ({A B C : Set ℓ} → (c : C) → P (assocr₂₊⇛ {ℓ} {A} {B} {C} c)) →
  ({A : Set ℓ} → (a : A) → P (unite⋆⇛ {ℓ} {A} a)) →
  ({A : Set ℓ} → (a : A) → P (uniti⋆⇛ {ℓ} {A} a)) →
  ({A B : Set ℓ} → (a : A) → (b : B) → P (swap⋆⇛ {ℓ} {A} {B} a b)) →
  ({A B C : Set ℓ} → (a : A) → (b : B) → (c : C) →
    P (assocl⋆⇛ {ℓ} {A} {B} {C} a b c)) →
  ({A B C : Set ℓ} → (a : A) → (b : B) → (c : C) →
    P (assocr⋆⇛ {ℓ} {A} {B} {C} a b c)) →
  ({A B C : Set ℓ} → (a : A) → (c : C) → P (dist₁⇛ {ℓ} {A} {B} {C} a c)) →
  ({A B C : Set ℓ} → (b : B) → (c : C) → P (dist₂⇛ {ℓ} {A} {B} {C} b c)) →
  ({A B C : Set ℓ} → (a : A) → (c : C) → P (factor₁⇛ {ℓ} {A} {B} {C} a c)) →
  ({A B C : Set ℓ} → (b : B) → (c : C) → P (factor₂⇛ {ℓ} {A} {B} {C} b c)) →
  ({A : Set ℓ} → (a : A) → P (id⇛ {ℓ} {A} a)) →
  ({A B C : Set ℓ} {a : A} {b : B} {c : C} →
    (p : (•[ A , a ] ⇛ •[ B , b ])) →
    (q : (•[ B , b ] ⇛ •[ C , c ])) →
    P p → P q → P (trans⇛ p q)) →
  ({A B C D : Set ℓ} {a : A} {b : B} {c : C} {d : D} →
    (p : (•[ A , a ] ⇛ •[ C , c ])) →
    (q : (•[ B , b ] ⇛ •[ D , d ])) →
    P p → P q → P (plus₁⇛ {ℓ} {A} {B} {C} {D} {a} {b} {c} {d} p q)) →
  ({A B C D : Set ℓ} {a : A} {b : B} {c : C} {d : D} →
    (p : (•[ A , a ] ⇛ •[ C , c ])) →
    (q : (•[ B , b ] ⇛ •[ D , d ])) →
    P p → P q → P (plus₂⇛ {ℓ} {A} {B} {C} {D} {a} {b} {c} {d} p q)) →
  ({A B C D : Set ℓ} {a : A} {b : B} {c : C} {d : D} →
    (p : (•[ A , a ] ⇛ •[ C , c ])) →
    (q : (•[ B , b ] ⇛ •[ D , d ])) →
    P p → P q → P (times⇛ p q)) →
  {A B : Set ℓ} {a : A} {b : B} → (p : •[ A , a ] ⇛ •[ B , b ]) → P p
  {A• B• : Set• {ℓ}} → (p : A• ⇛ B•) → P p
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (swap₁₊⇛ a) = swap₁₊ a
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (swap₂₊⇛ b) = swap₂₊ b
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (assocl₁₊⇛ a) = assocl₁₊ a
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (assocl₂₁₊⇛ b) = assocl₂₁₊ b
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (assocl₂₂₊⇛ c) = assocl₂₂₊ c
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (assocr₁₁₊⇛ a) = assocr₁₁₊ a
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (assocr₁₂₊⇛ b) = assocr₁₂₊ b
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (assocr₂₊⇛ c) = assocr₂₊ c
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (unite⋆⇛ a) = unite⋆ a
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (uniti⋆⇛ a) = uniti⋆ a
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (swap⋆⇛ a b) = swap⋆ a b
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (assocl⋆⇛ a b c) = assocl⋆ a b c
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (assocr⋆⇛ a b c) = assocr⋆ a b c
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (dist₁⇛ a c) = dist₁ a c
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (dist₂⇛ b c) = dist₂ b c
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (factor₁⇛ a c) = factor₁ a c
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (factor₂⇛ b c) = factor₂ b c
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (id⇛ a) = cid a
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (trans⇛ p q) =
    ctrans p q
      (pathInd P swap₁₊ swap₂₊
       assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
       unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
       cid ctrans plus₁ plus₂ times p)
      (pathInd P swap₁₊ swap₂₊
       assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
       unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
       cid ctrans plus₁ plus₂ times q)
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (plus₁⇛ p q) =
    plus₁ p q
      (pathInd P swap₁₊ swap₂₊
       assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
       unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
       cid ctrans plus₁ plus₂ times p)
      (pathInd P swap₁₊ swap₂₊
       assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
       unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
       cid ctrans plus₁ plus₂ times q)
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (plus₂⇛ p q) =
    plus₂ p q
      (pathInd P swap₁₊ swap₂₊
       assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
       unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
       cid ctrans plus₁ plus₂ times p)
      (pathInd P swap₁₊ swap₂₊
       assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
       unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
       cid ctrans plus₁ plus₂ times q)
pathInd P swap₁₊ swap₂₊
  assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
  unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
  cid ctrans plus₁ plus₂ times (times⇛ p q) =
    times p q
      (pathInd P swap₁₊ swap₂₊
       assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
       unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
       cid ctrans plus₁ plus₂ times p)
      (pathInd P swap₁₊ swap₂₊
       assocl₁₊ assocl₂₁₊ assocl₂₂₊ assocr₁₁₊ assocr₁₂₊ assocr₂₊
       unite⋆ uniti⋆ swap⋆ assocl⋆ assocr⋆ dist₁ dist₂ factor₁ factor₂
       cid ctrans plus₁ plus₂ times q)
pathInd P swap₁₊ swap₁₊⇛ = swap₁₊
--}

------------------------------------------------------------------------------
-- Groupoid structure (emerging...)
{--
sym⇛ : {ℓ : Level} {A B : Set ℓ} {a : A} {b : B} → Path a b → Path b a
sym⇛ {ℓ} {A} {B} {a} {b} p =
  (pathInd
    (λ {A} {B} {a} {b} p → Path b a)
    swap₂₊⇛ swap₁₊⇛
    assocr₁₁₊⇛ assocr₁₂₊⇛ assocr₂₊⇛ assocl₁₊⇛ assocl₂₁₊⇛ assocl₂₂₊⇛
    uniti⋆⇛ unite⋆⇛ (λ a b → swap⋆⇛ b a)
    assocr⋆⇛ assocl⋆⇛ factor₁⇛ factor₂⇛ dist₁⇛ dist₂⇛
    id⇛ (λ _ _ p' q' → trans⇛ q' p'))
    (λ _ _ p' q' → plus₁⇛ p' q') (λ _ _ p' q' → plus₂⇛ p' q')
    (λ _ _ p' q' → times⇛ p' q')
  {A} {B} {a} {b} p

test9 : {A : Set} {a : A} → Path (a , (tt , a)) ((tt , a) , a)
test9 {A} {a} = sym⇛ (times⇛ (unite⋆⇛ a) (uniti⋆⇛ a))
             -- evaluates to (times⇛ (uniti⋆⇛ a) (unite⋆⇛ a)
--}
{--
idright : {ℓ : Level} {A B : Set ℓ} {a : A} {b : B} {p : Path a b} →
          2Path (trans⇛ p (id⇛ b)) p
idright {ℓ} {A} {B} {a} {b} {p} =
  (pathInd
    (λ {A} {B} {a} {b} p → 2Path (trans⇛ p (id⇛ b)) p)
    (λ {A} {B} a₁ → {!!})
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!})
  {A} {B} {a} {b} p

aptransL : {ℓ : Level} {A B C : Set ℓ} {a : A} {b : B} {c : C} →
           (p q : Path a b) → (r : Path b c) → (α : 2Path p q) →
           2Path (trans⇛ p r) (trans⇛ q r)
aptransL {ℓ} {A} {B} {C} {a} {b} {c} p q r α =
  (pathInd
    (λ {B} {C} {b} {c} r → (A : Set ℓ) → (a : A) → (p q : Path a b) →
      (α : 2Path p q) → 2Path (trans⇛ p r) (trans⇛ q r))
    (λ a₁ A₂ a₂ p₁ q₁ α₁ → {!!})
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!}
    {!!})
  {B} {C} {b} {c} r A a p q α

symsym : {ℓ : Level} {A B : Set ℓ} {a : A} {b : B} → (p : Path a b) →
         2Path (sym⇛ (sym⇛ p)) p
symsym {ℓ} {A} {B} {a} {b} p =
  (pathInd
    (λ {A} {B} {a} {b} p → 2Path (sym⇛ (sym⇛ p)) p)
    (λ a → id⇛ (swap₁₊⇛ a))
    (λ b → id⇛ (swap₂₊⇛ b))
    (λ a → id⇛ (assocl₁₊⇛ a))
    (λ b → id⇛ (assocl₂₁₊⇛ b))
    (λ c → id⇛ (assocl₂₂₊⇛ c))
    (λ a → id⇛ (assocr₁₁₊⇛ a))
    (λ b → id⇛ (assocr₁₂₊⇛ b))
    (λ c → id⇛ (assocr₂₊⇛ c))
    (λ a → id⇛ (unite⋆⇛ a))
    (λ a → id⇛ (uniti⋆⇛ a))
    (λ a b → id⇛ (swap⋆⇛ a b))
    (λ a b c → id⇛ (assocl⋆⇛ a b c))
    (λ a b c → id⇛ (assocr⋆⇛ a b c))
    (λ a c → id⇛ (dist₁⇛ a c))
    (λ b c → id⇛ (dist₂⇛ b c))
    (λ a c → id⇛ (factor₁⇛ a c))
    (λ b c → id⇛ (factor₂⇛ b c))
    (λ a → id⇛ (id⇛ a))
    (λ p q α β → {!!})
    (λ p q α β → {!!})
    (λ p q α β → {!!})
    (λ p q α β → {!!}))
  {A} {B} {a} {b} p
--}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Explain connection to negative information.

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

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

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

open _⟶_

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

mutual

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

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

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

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

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

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

--}

--}

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
module STLC.Coquand.Substitution where

open import STLC.Coquand.Renaming public
open import Category

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

-- Substitutions
infix 3 _⊢⋆_
data _⊢⋆_ : 𝒞 → 𝒞 → Set
  where
    ∅   : ∀ {Γ} → Γ ⊢⋆ ∅

    _,_ : ∀ {Γ Ξ A} → (σ : Γ ⊢⋆ Ξ) (M : Γ ⊢ A)
                    → Γ ⊢⋆ Ξ , A

putₛ : ∀ {Ξ Γ} → (∀ {A} → Ξ ⊢ A → Γ ⊢ A) → Γ ⊢⋆ Ξ
putₛ {∅}     f = ∅
putₛ {Γ , A} f = putₛ (λ M → f (wk M)) , f 0

getₛ : ∀ {Γ Ξ A} → Γ ⊢⋆ Ξ → Ξ ∋ A → Γ ⊢ A
getₛ (σ , M) zero    = M
getₛ (σ , M) (suc i) = getₛ σ i

wkₛ : ∀ {A Γ Ξ} → Γ ⊢⋆ Ξ → Γ , A ⊢⋆ Ξ
wkₛ ∅       = ∅
wkₛ (σ , M) = wkₛ σ , wk M

liftₛ : ∀ {A Γ Ξ} → Γ ⊢⋆ Ξ → Γ , A ⊢⋆ Ξ , A
liftₛ σ = wkₛ σ , 0

idₛ : ∀ {Γ} → Γ ⊢⋆ Γ
idₛ {∅}     = ∅
idₛ {Γ , A} = liftₛ idₛ

sub : ∀ {Γ Ξ A} → Γ ⊢⋆ Ξ → Ξ ⊢ A → Γ ⊢ A
sub σ (𝓋 i)   = getₛ σ i
sub σ (ƛ M)   = ƛ (sub (liftₛ σ) M)
sub σ (M ∙ N) = sub σ M ∙ sub σ N

cut : ∀ {Γ A B} → Γ ⊢ A → Γ , A ⊢ B → Γ ⊢ B
cut M N = sub (idₛ , M) N

-- NOTE: _●_ = sub⋆
_●_ : ∀ {Γ Ξ Φ} → Γ ⊢⋆ Ξ → Ξ ⊢⋆ Φ → Γ ⊢⋆ Φ
σ₁ ● ∅        = ∅
σ₁ ● (σ₂ , M) = σ₁ ● σ₂ , sub σ₁ M

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

-- (wkgetₛ)
natgetₛ : ∀ {Γ Ξ A B} → (σ : Γ ⊢⋆ Ξ) (i : Ξ ∋ A)
                      → getₛ (wkₛ {B} σ) i ≡ (wk ∘ getₛ σ) i
natgetₛ (σ , M) zero    = refl
natgetₛ (σ , M) (suc i) = natgetₛ σ i

idgetₛ : ∀ {Γ A} → (i : Γ ∋ A)
                 → getₛ idₛ i ≡ 𝓋 i
idgetₛ zero    = refl
idgetₛ (suc i) = natgetₛ idₛ i
               ⦙ wk & idgetₛ i
               ⦙ 𝓋 & ( natgetᵣ idᵣ i
                     ⦙ suc & idgetᵣ i
                     )

idsub : ∀ {Γ A} → (M : Γ ⊢ A)
                → sub idₛ M ≡ M
idsub (𝓋 i)   = idgetₛ i
idsub (ƛ M)   = ƛ & idsub M
idsub (M ∙ N) = _∙_ & idsub M
                    ⊗ idsub N

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

⌊_⌋ : ∀ {Γ Γ′} → Γ′ ∋⋆ Γ → Γ′ ⊢⋆ Γ
⌊ ∅ ⌋     = ∅
⌊ η , i ⌋ = ⌊ η ⌋ , 𝓋 i

-- NOTE: _◐_ = getₛ⋆
_◐_ : ∀ {Γ Ξ Ξ′} → Γ ⊢⋆ Ξ′ → Ξ′ ∋⋆ Ξ → Γ ⊢⋆ Ξ
σ ◐ η = σ ● ⌊ η ⌋

-- NOTE: _◑_ = ren⋆
_◑_ : ∀ {Γ Γ′ Ξ} → Γ′ ∋⋆ Γ → Γ ⊢⋆ Ξ → Γ′ ⊢⋆ Ξ
η ◑ σ = ⌊ η ⌋ ● σ

⌊get⌋ : ∀ {Γ Γ′ A} → (η : Γ′ ∋⋆ Γ) (i : Γ ∋ A)
                   → getₛ ⌊ η ⌋ i ≡ 𝓋 (getᵣ η i)
⌊get⌋ (η , j) zero    = refl
⌊get⌋ (η , j) (suc i) = ⌊get⌋ η i

⌊wk⌋ : ∀ {Γ Γ′ A} → (η : Γ′ ∋⋆ Γ)
                  → wkₛ {A} ⌊ η ⌋ ≡ ⌊ wkᵣ η ⌋
⌊wk⌋ ∅       = refl
⌊wk⌋ (η , i) = (wkₛ ⌊ η ⌋ ,_) & (𝓋 & natgetᵣ idᵣ i)
             ⦙ _,_ & ⌊wk⌋ η
                   ⊗ 𝓋 ∘ suc & idgetᵣ i

⌊lift⌋ : ∀ {Γ Γ′ A} → (η : Γ′ ∋⋆ Γ)
                    → liftₛ {A} ⌊ η ⌋ ≡ ⌊ liftᵣ η ⌋
⌊lift⌋ η = (_, 0) & ⌊wk⌋ η

⌊id⌋ : ∀ {Γ} → idₛ {Γ} ≡ ⌊ idᵣ ⌋
⌊id⌋ {∅}     = refl
⌊id⌋ {Γ , A} = (_, 0) & ( wkₛ & ⌊id⌋
                        ⦙ ⌊wk⌋ idᵣ
                        )

⌊sub⌋ : ∀ {Γ Γ′ A} → (η : Γ′ ∋⋆ Γ) (M : Γ ⊢ A)
                   → sub ⌊ η ⌋ M ≡ ren η M
⌊sub⌋ η (𝓋 i)   = ⌊get⌋ η i
⌊sub⌋ η (ƛ M)   = ƛ & ( (λ σ → sub σ M) & ⌊lift⌋ η
                      ⦙ ⌊sub⌋ (liftᵣ η) M
                      )
⌊sub⌋ η (M ∙ N) = _∙_ & ⌊sub⌋ η M
                      ⊗ ⌊sub⌋ η N

⌊○⌋ : ∀ {Γ Γ′ Γ″} → (η₁ : Γ″ ∋⋆ Γ′) (η₂ : Γ′ ∋⋆ Γ)
                  → ⌊ η₁ ○ η₂ ⌋ ≡ ⌊ η₁ ⌋ ● ⌊ η₂ ⌋
⌊○⌋ η₁ ∅        = refl
⌊○⌋ η₁ (η₂ , i) = _,_ & ⌊○⌋ η₁ η₂
                      ⊗ (⌊get⌋ η₁ i ⁻¹)

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

zap◐ : ∀ {Γ Ξ Ξ′ A} → (σ : Γ ⊢⋆ Ξ′) (η : Ξ′ ∋⋆ Ξ) (M : Γ ⊢ A)
                    → (σ , M) ◐ wkᵣ η ≡ σ ◐ η
zap◐ σ ∅       M = refl
zap◐ σ (η , i) M = (_, getₛ σ i) & zap◐ σ η M

rid◐ : ∀ {Γ Ξ} → (σ : Γ ⊢⋆ Ξ)
               → σ ◐ idᵣ ≡ σ
rid◐ ∅       = refl
rid◐ (σ , M) = (_, M) & ( zap◐ σ idᵣ M
                        ⦙ rid◐ σ
                        )

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

get◐ : ∀ {Γ Ξ Ξ′ A} → (σ : Γ ⊢⋆ Ξ′) (η : Ξ′ ∋⋆ Ξ) (i : Ξ ∋ A)
                    → getₛ (σ ◐ η) i ≡ (getₛ σ ∘ getᵣ η) i
get◐ σ (η , j) zero    = refl
get◐ σ (η , j) (suc i) = get◐ σ η i

wk◐ : ∀ {Γ Ξ Ξ′ A} → (σ : Γ ⊢⋆ Ξ′) (η : Ξ′ ∋⋆ Ξ)
                   → wkₛ {A} (σ ◐ η) ≡ wkₛ σ ◐ η
wk◐ σ ∅       = refl
wk◐ σ (η , i) = _,_ & wk◐ σ η
                    ⊗ (natgetₛ σ i ⁻¹)

lift◐ : ∀ {Γ Ξ Ξ′ A} → (σ : Γ ⊢⋆ Ξ′) (η : Ξ′ ∋⋆ Ξ)
                     → liftₛ {A} (σ ◐ η) ≡ liftₛ σ ◐ liftᵣ η
lift◐ σ η = (_, 0) & ( wk◐ σ η
                   ⦙ zap◐ (wkₛ σ) η 0 ⁻¹
                   )

wkrid◐ : ∀ {Γ Ξ A} → (σ : Γ ⊢⋆ Ξ)
                   → wkₛ {A} σ ◐ idᵣ ≡ wkₛ σ
wkrid◐ σ = wk◐ σ idᵣ ⁻¹
         ⦙ wkₛ & rid◐ σ

liftwkrid◐ : ∀ {Γ Ξ A} → (σ : Γ ⊢⋆ Ξ)
                       → liftₛ {A} σ ◐ wkᵣ idᵣ ≡ wkₛ σ
liftwkrid◐ σ = zap◐ (wkₛ σ) idᵣ 0
             ⦙ wkrid◐ σ

mutual
  sub◐ : ∀ {Γ Ξ Ξ′ A} → (σ : Γ ⊢⋆ Ξ′) (η : Ξ′ ∋⋆ Ξ) (M : Ξ ⊢ A)
                      → sub (σ ◐ η) M ≡ (sub σ ∘ ren η) M
  sub◐ σ η (𝓋 i)   = get◐ σ η i
  sub◐ σ η (ƛ M)   = ƛ & sublift◐ σ η M
  sub◐ σ η (M ∙ N) = _∙_ & sub◐ σ η M
                         ⊗ sub◐ σ η N

  sublift◐ : ∀ {Γ Ξ Ξ′ A B} → (σ : Γ ⊢⋆ Ξ′) (η : Ξ′ ∋⋆ Ξ) (M : Ξ , B ⊢ A)
                            → sub (liftₛ {B} (σ ◐ η)) M ≡
                               (sub (liftₛ σ) ∘ ren (liftᵣ η)) M
  sublift◐ σ η M = (λ σ′ → sub σ′ M) & lift◐ σ η
                 ⦙ sub◐ (liftₛ σ) (liftᵣ η) M

subwk◐ : ∀ {Γ Ξ Ξ′ A B} → (σ : Γ ⊢⋆ Ξ′) (η : Ξ′ ∋⋆ Ξ) (M : Ξ ⊢ A)
                        → sub (wkₛ {B} (σ ◐ η)) M ≡
                           (sub (wkₛ σ) ∘ ren η) M
subwk◐ σ η M = (λ σ′ → sub σ′ M) & wk◐ σ η
             ⦙ sub◐ (wkₛ σ) η M

subliftwk◐ : ∀ {Γ Ξ Ξ′ A B} → (σ : Γ ⊢⋆ Ξ′) (η : Ξ′ ∋⋆ Ξ) (M : Ξ ⊢ A)
                            → sub (wkₛ {B} (σ ◐ η)) M ≡
                               (sub (liftₛ σ) ∘ ren (wkᵣ η)) M
subliftwk◐ σ η M = (λ σ′ → sub σ′ M) & ( wk◐ σ η
                                        ⦙ zap◐ (wkₛ σ) η 0 ⁻¹
                                        )
                 ⦙ sub◐ (liftₛ σ) (wkᵣ η) M

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

zap◑ : ∀ {Γ Γ′ Ξ A} → (η : Γ′ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ) (i : Γ′ ∋ A)
                    → (η , i) ◑ wkₛ σ ≡ η ◑ σ
zap◑ η ∅       i = refl
zap◑ η (σ , j) i = _,_ & zap◑ η σ i
                       ⊗ ( sub◐ (⌊ η ⌋ , 𝓋 i) (wkᵣ idᵣ) j ⁻¹
                         ⦙ (λ σ′ → sub σ′ j)
                           & ( zap◐ ⌊ η ⌋ idᵣ (𝓋 i)
                             ⦙ rid◐ ⌊ η ⌋
                             )
                         )

lid◑ : ∀ {Γ Ξ} → (σ : Γ ⊢⋆ Ξ)
               → idᵣ ◑ σ ≡ σ
lid◑ ∅       = refl
lid◑ (σ , M) = _,_ & lid◑ σ
                   ⊗ ( (λ σ′ → sub σ′ M) & ⌊id⌋ ⁻¹
                     ⦙ idsub M
                     )

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

zap● : ∀ {Γ Ξ Φ A} → (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ) (M : Γ ⊢ A)
                   → (σ₁ , M) ● wkₛ σ₂ ≡ σ₁ ● σ₂
zap● σ₁ ∅        M = refl
zap● σ₁ (σ₂ , N) M = _,_ & zap● σ₁ σ₂ M
                         ⊗ ( sub◐ (σ₁ , M) (wkᵣ idᵣ) N ⁻¹
                           ⦙ (λ σ′ → sub σ′ N)
                             & ( zap◐ σ₁ idᵣ M
                               ⦙ rid◐ σ₁
                               )
                           )

lid● : ∀ {Γ Ξ} → (σ : Γ ⊢⋆ Ξ)
               → idₛ ● σ ≡ σ
lid● ∅       = refl
lid● (σ , M) = _,_ & lid● σ
                   ⊗ idsub M

rid● : ∀ {Γ Ξ} → (σ : Γ ⊢⋆ Ξ)
               → σ ● idₛ ≡ σ
rid● σ = (σ ●_) & ⌊id⌋ ⦙ rid◐ σ

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

get◑ : ∀ {Γ Γ′ Ξ A} → (η : Γ′ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ) (i : Ξ ∋ A)
                    → getₛ (η ◑ σ) i ≡ (ren η ∘ getₛ σ) i
get◑ η (σ , M) zero    = ⌊sub⌋ η M
get◑ η (σ , M) (suc i) = get◑ η σ i

wk◑ : ∀ {Γ Γ′ Ξ A} → (η : Γ′ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ)
                   → wkₛ {A} (η ◑ σ) ≡ wkᵣ η ◑ σ
wk◑ η ∅       = refl
wk◑ η (σ , M) = _,_ & wk◑ η σ
                    ⊗ ( ren (wkᵣ idᵣ) & ⌊sub⌋ η M
                      ⦙ ren○ (wkᵣ idᵣ) η M ⁻¹
                      ⦙ (λ η′ → ren η′ M) & wklid○ η
                      ⦙ ⌊sub⌋ (wkᵣ η) M ⁻¹
                      )

lift◑ : ∀ {Γ Γ′ Ξ A} → (η : Γ′ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ)
                     → liftₛ {A} (η ◑ σ) ≡ liftᵣ η ◑ liftₛ σ
lift◑ η σ = (_, 0) & ( wk◑ η σ
                     ⦙ zap● ⌊ wkᵣ η ⌋ σ 0 ⁻¹
                     )

wklid◑ : ∀ {Γ Ξ A} → (σ : Γ ⊢⋆ Ξ)
                   → wkᵣ {A} idᵣ ◑ σ ≡ wkₛ σ
wklid◑ σ = wk◑ idᵣ σ ⁻¹
         ⦙ wkₛ & lid◑ σ

liftwklid◑ : ∀ {Γ Ξ A} → (σ : Γ ⊢⋆ Ξ)
                       → (liftᵣ {A} idᵣ ◑ wkₛ σ) ≡ wkₛ σ
liftwklid◑ σ = zap◑ (wkᵣ idᵣ) σ 0
             ⦙ wklid◑ σ

mutual
  sub◑ : ∀ {Γ Γ′ Ξ A} → (η : Γ′ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ) (M : Ξ ⊢ A)
                      → sub (η ◑ σ) M ≡ (ren η ∘ sub σ) M
  sub◑ η σ (𝓋 i)   = get◑ η σ i
  sub◑ η σ (ƛ M)   = ƛ & sublift◑ η σ M
  sub◑ η σ (M ∙ N) = _∙_ & sub◑ η σ M
                         ⊗ sub◑ η σ N

  sublift◑ : ∀ {Γ Γ′ Ξ A B} → (η : Γ′ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ) (M : Ξ , B ⊢ A)
                            → sub (liftₛ {B} (η ◑ σ)) M ≡
                               (ren (liftᵣ η) ∘ sub (liftₛ σ)) M
  sublift◑ η σ M = (λ σ′ → sub σ′ M) & lift◑ η σ
                 ⦙ sub◑ (liftᵣ η) (liftₛ σ) M

subwk◑ : ∀ {Γ Γ′ Ξ A B} → (η : Γ′ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ) (M : Ξ ⊢ A)
                        → sub (wkₛ {B} (η ◑ σ)) M ≡
                           (ren (wkᵣ η) ∘ sub σ) M
subwk◑ η σ M = (λ σ′ → sub σ′ M) & wk◑ η σ
             ⦙ sub◑ (wkᵣ η) σ M
subliftwk◑ : ∀ {Γ Γ′ Ξ A B} → (η : Γ′ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ) (M : Ξ ⊢ A)
                            → sub (wkₛ {B} (η ◑ σ)) M ≡
                               (ren (liftᵣ η) ∘ sub (wkₛ σ)) M
subliftwk◑ η σ M = (λ σ′ → sub σ′ M) & ( wk◑ η σ
                                        ⦙ zap◑ (wkᵣ η) σ 0 ⁻¹
                                        )
                 ⦙ sub◑ (liftᵣ η) (wkₛ σ) M

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

get● : ∀ {Γ Ξ Φ A} → (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ) (i : Φ ∋ A)
                   → getₛ (σ₁ ● σ₂) i ≡ (sub σ₁ ∘ getₛ σ₂) i
get● σ₁ (σ₂ , M) zero    = refl
get● σ₁ (σ₂ , M) (suc i) = get● σ₁ σ₂ i

wk● : ∀ {Γ Ξ Φ A} → (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ)
                  → wkₛ {A} (σ₁ ● σ₂) ≡ wkₛ σ₁ ● σ₂
wk● σ₁ ∅        = refl
wk● σ₁ (σ₂ , M) = _,_ & wk● σ₁ σ₂
                      ⊗ ( sub◑ (wkᵣ idᵣ) σ₁ M ⁻¹
                        ⦙ (λ σ′ → sub σ′ M) & wklid◑ σ₁
                        )

lift● : ∀ {Γ Ξ Φ A} → (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ)
                    → liftₛ {A} (σ₁ ● σ₂) ≡ liftₛ σ₁ ● liftₛ σ₂
lift● σ₁ σ₂ = (_, 0) & ( wk● σ₁ σ₂
                       ⦙ zap● (wkₛ σ₁) σ₂ 0 ⁻¹
                       )

wklid● : ∀ {Γ Ξ A} → (σ : Γ ⊢⋆ Ξ)
                   → wkₛ {A} idₛ ● σ ≡ wkₛ σ
wklid● σ = wk● idₛ σ ⁻¹
         ⦙ wkₛ & lid● σ

wkrid● : ∀ {Γ Ξ A} → (σ : Γ ⊢⋆ Ξ)
                   → wkₛ {A} σ ● idₛ ≡ wkₛ σ
wkrid● σ = wk● σ idₛ ⁻¹
         ⦙ wkₛ & rid● σ

liftwkrid● : ∀ {Γ Ξ A} → (σ : Γ ⊢⋆ Ξ)
                       → liftₛ {A} σ ● wkₛ idₛ ≡ wkₛ σ
liftwkrid● σ = zap● (wkₛ σ) idₛ 0
             ⦙ wkrid● σ

mutual
  sub● : ∀ {Γ Ξ Φ A} → (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ) (M : Φ ⊢ A)
                     → sub (σ₁ ● σ₂) M ≡ (sub σ₁ ∘ sub σ₂) M
  sub● σ₁ σ₂ (𝓋 i)   = get● σ₁ σ₂ i
  sub● σ₁ σ₂ (ƛ M)   = ƛ & sublift● σ₁ σ₂ M
  sub● σ₁ σ₂ (M ∙ N) = _∙_ & sub● σ₁ σ₂ M
                           ⊗ sub● σ₁ σ₂ N

  sublift● : ∀ {Γ Ξ Φ A B} → (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ) (M : Φ , B ⊢ A)
                           → sub (liftₛ {B} (σ₁ ● σ₂)) M ≡
                              (sub (liftₛ σ₁) ∘ sub (liftₛ σ₂)) M
  sublift● σ₁ σ₂ M = (λ σ′ → sub σ′ M) & lift● σ₁ σ₂
                   ⦙ sub● (liftₛ σ₁) (liftₛ σ₂) M

subwk● : ∀ {Γ Ξ Φ A B} → (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ) (M : Φ ⊢ A)
                       → sub (wkₛ {B} (σ₁ ● σ₂)) M ≡
                          (sub (wkₛ σ₁) ∘ sub σ₂) M
subwk● σ₁ σ₂ M = (λ σ′ → sub σ′ M) & wk● σ₁ σ₂
               ⦙ sub● (wkₛ σ₁) σ₂ M

subliftwk● : ∀ {Γ Ξ Φ A B} → (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ) (M : Φ ⊢ A)
                           → sub (wkₛ {B} (σ₁ ● σ₂)) M ≡
                              (sub (liftₛ σ₁) ∘ sub (wkₛ σ₂)) M
subliftwk● σ₁ σ₂ M = (λ σ′ → sub σ′ M) & ( wk● σ₁ σ₂
                                          ⦙ zap● (wkₛ σ₁) σ₂ 0 ⁻¹
                                          )
                   ⦙ sub● (liftₛ σ₁) (wkₛ σ₂) M

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

comp◐○ : ∀ {Γ Ξ Ξ′ Ξ″} → (σ : Γ ⊢⋆ Ξ″) (η₁ : Ξ″ ∋⋆ Ξ′) (η₂ : Ξ′ ∋⋆ Ξ)
                       → σ ◐ (η₁ ○ η₂) ≡ (σ ◐ η₁) ◐ η₂
comp◐○ σ η₁ ∅        = refl
comp◐○ σ η₁ (η₂ , i) = _,_ & comp◐○ σ η₁ η₂
                           ⊗ (get◐ σ η₁ i ⁻¹)

comp◑○ : ∀ {Γ Γ′ Γ″ Ξ} → (η₁ : Γ″ ∋⋆ Γ′) (η₂ : Γ′ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ)
                       → η₁ ◑ (η₂ ◑ σ) ≡ (η₁ ○ η₂) ◑ σ
comp◑○ η₁ η₂ ∅       = refl
comp◑○ η₁ η₂ (σ , M) = _,_ & comp◑○ η₁ η₂ σ
                           ⊗ ( sub● ⌊ η₁ ⌋ ⌊ η₂ ⌋ M ⁻¹
                             ⦙ (λ σ′ → sub σ′ M)
                               & ⌊○⌋ η₁ η₂ ⁻¹
                             )

comp◑◐ : ∀ {Γ Γ′ Ξ Ξ′} → (η₁ : Γ′ ∋⋆ Γ) (σ : Γ ⊢⋆ Ξ′) (η₂ : Ξ′ ∋⋆ Ξ)
                       → η₁ ◑ (σ ◐ η₂) ≡ (η₁ ◑ σ) ◐ η₂
comp◑◐ η₁ σ ∅        = refl
comp◑◐ η₁ σ (η₂ , i) = _,_ & comp◑◐ η₁ σ η₂
                           ⊗ ( ⌊sub⌋ η₁ (getₛ σ i)
                             ⦙ get◑ η₁ σ i ⁻¹
                             )

comp◑● : ∀ {Γ Γ′ Ξ Φ} → (η : Γ′ ∋⋆ Γ) (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ)
                      → η ◑ (σ₁ ● σ₂) ≡ (η ◑ σ₁) ● σ₂
comp◑● η σ₁ ∅        = refl
comp◑● η σ₁ (σ₂ , M) = _,_ & comp◑● η σ₁ σ₂
                           ⊗ (sub● ⌊ η ⌋ σ₁ M ⁻¹)

comp●◐ : ∀ {Γ Ξ Φ Φ′} → (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ′) (η : Φ′ ∋⋆ Φ)
                      → σ₁ ● (σ₂ ◐ η) ≡ (σ₁ ● σ₂) ◐ η
comp●◐ σ₁ σ₂ ∅       = refl
comp●◐ σ₁ σ₂ (η , i) = _,_ & comp●◐ σ₁ σ₂ η
                           ⊗ (get● σ₁ σ₂ i ⁻¹)

comp●◑ : ∀ {Γ Ξ Ξ′ Φ} → (σ₁ : Γ ⊢⋆ Ξ′) (η : Ξ′ ∋⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ)
                      → σ₁ ● (η ◑ σ₂) ≡ (σ₁ ◐ η) ● σ₂
comp●◑ σ₁ η ∅        = refl
comp●◑ σ₁ η (σ₂ , M) = _,_ & comp●◑ σ₁ η σ₂
                           ⊗ (sub● σ₁ ⌊ η ⌋ M ⁻¹)

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

assoc● : ∀ {Γ Ξ Φ Ψ} → (σ₁ : Γ ⊢⋆ Ξ) (σ₂ : Ξ ⊢⋆ Φ) (σ₃ : Φ ⊢⋆ Ψ)
                     → σ₁ ● (σ₂ ● σ₃) ≡ (σ₁ ● σ₂) ● σ₃
assoc● σ₁ σ₂ ∅        = refl
assoc● σ₁ σ₂ (σ₃ , M) = _,_ & assoc● σ₁ σ₂ σ₃
                            ⊗ (sub● σ₁ σ₂ M ⁻¹)

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

𝗦𝗧𝗟𝗖 : Category 𝒞 _⊢⋆_
𝗦𝗧𝗟𝗖 =
  record
    { idₓ    = idₛ
    ; _⋄_    = flip _●_
    ; lid⋄   = rid●
    ; rid⋄   = lid●
    ; assoc⋄ = assoc●
    }

subPsh : 𝒯 → Presheaf₀ 𝗦𝗧𝗟𝗖
subPsh A =
  record
    { Fₓ  = _⊢ A
    ; F   = sub
    ; idF = fext! idsub
    ; F⋄  = λ σ₁ σ₂ → fext! (sub● σ₂ σ₁)
    }

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

ext: agda

max_stars_repo_name: mietek/coquand-kovacs

max_issues_repo_name: mietek/coquand-kovacs

max_forks_repo_name: mietek/coquand-kovacs


text:
{-# OPTIONS --with-K -vtc.lhs.unify:50 #-}

open import Agda.Primitive        using (Setω)
open import Agda.Builtin.Equality using (_≡_; refl)

-- change `Set` to `Setω` breaks `seq`
data RecD  (I : Set) : Setω where
  ι : (i : I) → RecD I

data RecO {I J : Set} (e : I → J) : RecD I → RecD J → Setω where
  ι : (i : I) (j : J) (eq : e i ≡ j) → RecO e (ι i) (ι j)

seq : {I J K : Set} {e : I → J} {f : J → K} {D : RecD I} {E : RecD J} {F : RecD K}
  → RecO f E F → RecO e D E
  → RecO (λ i → f (e i)) D F
seq (ι _ _ refl) (ι _ _ refl) = ι _ _ refl

max_stars_repo_name: sseefried/agda


text:
{-# OPTIONS --cubical --no-import-sorts --postfix-projections --safe #-}

module Cubical.Categories.Presheaf.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.HITs.PropositionalTruncation

open import Cubical.Categories.Category
open import Cubical.Categories.Functor
open import Cubical.Categories.NaturalTransformation
open import Cubical.Categories.Instances.Sets
open import Cubical.Categories.Instances.Functors

module _ {ℓ ℓ'} where

  PreShv : Precategory ℓ ℓ' → (ℓS : Level) → Precategory (ℓ-max (ℓ-max ℓ ℓ') (ℓ-suc ℓS)) (ℓ-max (ℓ-max ℓ ℓ') ℓS)
  PreShv C ℓS = FUNCTOR (C ^op) (SET ℓS)

instance
  isCatPreShv : ∀ {ℓ ℓ'} {C : Precategory ℓ ℓ'} {ℓS}
    → isCategory (PreShv C ℓS)
  isCatPreShv {C = C} {ℓS} = isCatFUNCTOR (C ^op) (SET ℓS)

private
  variable
    ℓ ℓ' : Level

module Yoneda (C : Precategory ℓ ℓ') ⦃ C-cat : isCategory C ⦄ where
  open Functor
  open NatTrans
  open Precategory C

  yo : ob → Functor (C ^op) (SET ℓ')
  yo x .F-ob y .fst = C [ y , x ]
  yo x .F-ob y .snd = C-cat .isSetHom
  yo x .F-hom f g = f ⋆⟨ C ⟩ g
  yo x .F-id i f = ⋆IdL f i
  yo x .F-seq f g i h = ⋆Assoc g f h i

  YO : Functor C (PreShv C ℓ')
  YO .F-ob = yo
  YO .F-hom f .N-ob z g = g ⋆⟨ C ⟩ f
  YO .F-hom f .N-hom g i h = ⋆Assoc g h f i
  YO .F-id = makeNatTransPath λ i _ → λ f → ⋆IdR f i
  YO .F-seq f g = makeNatTransPath λ i _ → λ h → ⋆Assoc h f g (~ i)

  module _ {x} (F : Functor (C ^op) (SET ℓ')) where
    yo-yo-yo : NatTrans (yo x) F → F .F-ob x .fst
    yo-yo-yo α = α .N-ob _ (id _)

    no-no-no : F .F-ob x .fst → NatTrans (yo x) F
    no-no-no a .N-ob y f = F .F-hom f a
    no-no-no a .N-hom f = funExt λ g i → F .F-seq g f i a

    yoIso : Iso (NatTrans (yo x) F) (F .F-ob x .fst)
    yoIso .Iso.fun = yo-yo-yo
    yoIso .Iso.inv = no-no-no
    yoIso .Iso.rightInv b i = F .F-id i b
    yoIso .Iso.leftInv a = makeNatTransPath (funExt λ _ → funExt rem)
      where
        rem : ∀ {z} (x₁ : C [ z , x ]) → F .F-hom x₁ (yo-yo-yo a) ≡ (a .N-ob z) x₁
        rem g =
          F .F-hom g (yo-yo-yo a)
            ≡[ i ]⟨ a .N-hom g (~ i) (id x) ⟩
          a .N-hom g i0 (id x)
            ≡[ i ]⟨ a .N-ob _ (⋆IdR g i) ⟩
          (a .N-ob _) g
            ∎

    yoEquiv : NatTrans (yo x) F ≃ F .F-ob x .fst
    yoEquiv = isoToEquiv yoIso

  isFullYO : isFull YO
  isFullYO x y F[f] = ∣ yo-yo-yo _ F[f] , yoIso {x} (yo y) .Iso.leftInv F[f] ∣

  isFaithfulYO : isFaithful YO
  isFaithfulYO x y f g p i =
    hcomp
      (λ j → λ{ (i = i0) → ⋆IdL f j; (i = i1) → ⋆IdL g j})
      (yo-yo-yo _ (p i))

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
module UniqueFloatNaN where

-- See Issue: Inconsistency: Rounding op differentiates NaNs #3749
-- https://github.com/agda/agda/issues/3749

open import Agda.Builtin.Float
  renaming ( primRound to round
           ; primFloor to floor
           ; primCeiling to ceiling
           ; primFloatNegate to -_
           ; primFloatDiv  to _/_)
open import Agda.Builtin.Equality

PNaN : Float
PNaN = 0.0 / 0.0

NNaN : Float
NNaN = - (0.0 / 0.0)

f : round PNaN ≡ round NNaN
f = refl

g : floor PNaN ≡ floor NNaN
g = refl

h : ceiling PNaN ≡ ceiling NNaN
h = refl

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: Agda-zh/agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties about integers
------------------------------------------------------------------------

module Data.Integer.Properties where

open import Algebra
import Algebra.FunctionProperties
import Algebra.Morphism as Morphism
import Algebra.Properties.AbelianGroup
open import Algebra.Structures
open import Data.Integer hiding (suc; _≤?_)
import Data.Integer.Addition.Properties as Add
import Data.Integer.Multiplication.Properties as Mul
open import Data.Nat
  using (ℕ; suc; zero; _∸_; _≤?_; _<_; _≥_; _≱_; s≤s; z≤n; ≤-pred)
  renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
open import Data.Nat.Properties as ℕ using (_*-mono_)
open import Data.Product using (proj₁; proj₂; _,_)
open import Data.Sign as Sign using () renaming (_*_ to _S*_)
import Data.Sign.Properties as SignProp
open import Function using (_∘_; _$_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Negation using (contradiction)

open Algebra.FunctionProperties (_≡_ {A = ℤ})
open CommutativeMonoid Add.commutativeMonoid
  using ()
  renaming ( assoc to +-assoc; comm to +-comm; identity to +-identity
           ; isCommutativeMonoid to +-isCommutativeMonoid
           ; isMonoid to +-isMonoid
           )
open CommutativeMonoid Mul.commutativeMonoid
  using ()
  renaming ( assoc to *-assoc; comm to *-comm; identity to *-identity
           ; isCommutativeMonoid to *-isCommutativeMonoid
           ; isMonoid to *-isMonoid
           )
open CommutativeSemiring ℕ.commutativeSemiring
  using () renaming (zero to *-zero; distrib to *-distrib)
open DecTotalOrder Data.Nat.decTotalOrder
  using () renaming (refl to ≤-refl)
open Morphism.Definitions ℤ ℕ _≡_
open ℕ.SemiringSolver
open ≡-Reasoning

------------------------------------------------------------------------
-- Miscellaneous properties

-- Some properties relating sign and ∣_∣ to _◃_.

sign-◃ : ∀ s n → sign (s ◃ suc n) ≡ s
sign-◃ Sign.- _ = refl
sign-◃ Sign.+ _ = refl

sign-cong : ∀ {s₁ s₂ n₁ n₂} →
            s₁ ◃ suc n₁ ≡ s₂ ◃ suc n₂ → s₁ ≡ s₂
sign-cong {s₁} {s₂} {n₁} {n₂} eq = begin
  s₁                  ≡⟨ sym $ sign-◃ s₁ n₁ ⟩
  sign (s₁ ◃ suc n₁)  ≡⟨ cong sign eq ⟩
  sign (s₂ ◃ suc n₂)  ≡⟨ sign-◃ s₂ n₂ ⟩
  s₂                  ∎

abs-◃ : ∀ s n → ∣ s ◃ n ∣ ≡ n
abs-◃ _      zero    = refl
abs-◃ Sign.- (suc n) = refl
abs-◃ Sign.+ (suc n) = refl

abs-cong : ∀ {s₁ s₂ n₁ n₂} →
           s₁ ◃ n₁ ≡ s₂ ◃ n₂ → n₁ ≡ n₂
abs-cong {s₁} {s₂} {n₁} {n₂} eq = begin
  n₁           ≡⟨ sym $ abs-◃ s₁ n₁ ⟩
  ∣ s₁ ◃ n₁ ∣  ≡⟨ cong ∣_∣ eq ⟩
  ∣ s₂ ◃ n₂ ∣  ≡⟨ abs-◃ s₂ n₂ ⟩
  n₂           ∎

-- ∣_∣ commutes with multiplication.

abs-*-commute : Homomorphic₂ ∣_∣ _*_ _ℕ*_
abs-*-commute i j = abs-◃ _ _

-- If you subtract a natural from itself, then you get zero.

n⊖n≡0 : ∀ n → n ⊖ n ≡ + 0
n⊖n≡0 zero    = refl
n⊖n≡0 (suc n) = n⊖n≡0 n

------------------------------------------------------------------------
-- The integers form a commutative ring

private

  ----------------------------------------------------------------------
  -- Additive abelian group.

  inverseˡ : LeftInverse (+ 0) -_ _+_
  inverseˡ -[1+ n ]  = n⊖n≡0 n
  inverseˡ (+ zero)  = refl
  inverseˡ (+ suc n) = n⊖n≡0 n

  inverseʳ : RightInverse (+ 0) -_ _+_
  inverseʳ i = begin
    i + - i  ≡⟨ +-comm i (- i) ⟩
    - i + i  ≡⟨ inverseˡ i ⟩
    + 0      ∎

  +-isAbelianGroup : IsAbelianGroup _≡_ _+_ (+ 0) -_
  +-isAbelianGroup = record
    { isGroup = record
      { isMonoid = +-isMonoid
      ; inverse  = inverseˡ , inverseʳ
      ; ⁻¹-cong  = cong -_
      }
    ; comm = +-comm
    }

  open Algebra.Properties.AbelianGroup
         (record { isAbelianGroup = +-isAbelianGroup })
    using () renaming (⁻¹-involutive to -‿involutive)

  ----------------------------------------------------------------------
  -- Distributivity

  -- Various lemmas used to prove distributivity.

  sign-⊖-< : ∀ {m n} → m < n → sign (m ⊖ n) ≡ Sign.-
  sign-⊖-< {zero}  (s≤s z≤n) = refl
  sign-⊖-< {suc n} (s≤s m<n) = sign-⊖-< m<n

  sign-⊖-≱ : ∀ {m n} → m ≱ n → sign (m ⊖ n) ≡ Sign.-
  sign-⊖-≱ = sign-⊖-< ∘ ℕ.≰⇒>

  +-⊖-left-cancel : ∀ a b c → (a ℕ+ b) ⊖ (a ℕ+ c) ≡ b ⊖ c
  +-⊖-left-cancel zero    b c = refl
  +-⊖-left-cancel (suc a) b c = +-⊖-left-cancel a b c

  ⊖-swap : ∀ a b → a ⊖ b ≡ - (b ⊖ a)
  ⊖-swap zero    zero    = refl
  ⊖-swap (suc _) zero    = refl
  ⊖-swap zero    (suc _) = refl
  ⊖-swap (suc a) (suc b) = ⊖-swap a b

  -- Lemmas relating _⊖_ and _∸_.

  ∣⊖∣-< : ∀ {m n} → m < n → ∣ m ⊖ n ∣ ≡ n ∸ m
  ∣⊖∣-< {zero}  (s≤s z≤n) = refl
  ∣⊖∣-< {suc n} (s≤s m<n) = ∣⊖∣-< m<n

  ∣⊖∣-≱ : ∀ {m n} → m ≱ n → ∣ m ⊖ n ∣ ≡ n ∸ m
  ∣⊖∣-≱ = ∣⊖∣-< ∘ ℕ.≰⇒>

  ⊖-≥ : ∀ {m n} → m ≥ n → m ⊖ n ≡ + (m ∸ n)
  ⊖-≥ z≤n       = refl
  ⊖-≥ (s≤s n≤m) = ⊖-≥ n≤m

  ⊖-< : ∀ {m n} → m < n → m ⊖ n ≡ - + (n ∸ m)
  ⊖-< {zero}  (s≤s z≤n) = refl
  ⊖-< {suc m} (s≤s m<n) = ⊖-< m<n

  ⊖-≱ : ∀ {m n} → m ≱ n → m ⊖ n ≡ - + (n ∸ m)
  ⊖-≱ = ⊖-< ∘ ℕ.≰⇒>

  -- Lemmas working around the fact that _◃_ pattern matches on its
  -- second argument before its first.

  +‿◃ : ∀ n → Sign.+ ◃ n ≡ + n
  +‿◃ zero    = refl
  +‿◃ (suc _) = refl

  -‿◃ : ∀ n → Sign.- ◃ n ≡ - + n
  -‿◃ zero    = refl
  -‿◃ (suc _) = refl

  -- The main distributivity proof.

  distrib-lemma :
    ∀ a b c → (c ⊖ b) * -[1+ a ] ≡ a ℕ+ b ℕ* suc a ⊖ (a ℕ+ c ℕ* suc a)
  distrib-lemma a b c
    rewrite +-⊖-left-cancel a (b ℕ* suc a) (c ℕ* suc a)
          | ⊖-swap (b ℕ* suc a) (c ℕ* suc a)
    with b ≤? c
  ... | yes b≤c
    rewrite ⊖-≥ b≤c
          | ⊖-≥ (b≤c *-mono (≤-refl {x = suc a}))
          | -‿◃ ((c ∸ b) ℕ* suc a)
          | ℕ.*-distrib-∸ʳ (suc a) c b
          = refl
  ... | no b≰c
    rewrite sign-⊖-≱ b≰c
          | ∣⊖∣-≱ b≰c
          | +‿◃ ((b ∸ c) ℕ* suc a)
          | ⊖-≱ (b≰c ∘ ℕ.cancel-*-right-≤ b c a)
          | -‿involutive (+ (b ℕ* suc a ∸ c ℕ* suc a))
          | ℕ.*-distrib-∸ʳ (suc a) b c
          = refl

  distribʳ : _*_ DistributesOverʳ _+_

  distribʳ (+ zero) y z
    rewrite proj₂ *-zero ∣ y ∣
          | proj₂ *-zero ∣ z ∣
          | proj₂ *-zero ∣ y + z ∣
          = refl

  distribʳ x (+ zero) z
    rewrite proj₁ +-identity z
          | proj₁ +-identity (sign z S* sign x ◃ ∣ z ∣ ℕ* ∣ x ∣)
          = refl

  distribʳ x y (+ zero)
    rewrite proj₂ +-identity y
          | proj₂ +-identity (sign y S* sign x ◃ ∣ y ∣ ℕ* ∣ x ∣)
          = refl

  distribʳ -[1+ a ] -[1+ b ] -[1+ c ] = cong +_ $
    solve 3 (λ a b c → (con 2 :+ b :+ c) :* (con 1 :+ a)
                    := (con 1 :+ b) :* (con 1 :+ a) :+
                       (con 1 :+ c) :* (con 1 :+ a))
            refl a b c

  distribʳ (+ suc a) (+ suc b) (+ suc c) = cong +_ $
    solve 3 (λ a b c → (con 1 :+ b :+ (con 1 :+ c)) :* (con 1 :+ a)
                    := (con 1 :+ b) :* (con 1 :+ a) :+
                       (con 1 :+ c) :* (con 1 :+ a))
          refl a b c

  distribʳ -[1+ a ] (+ suc b) (+ suc c) = cong -[1+_] $
    solve 3 (λ a b c → a :+ (b :+ (con 1 :+ c)) :* (con 1 :+ a)
                     := (con 1 :+ b) :* (con 1 :+ a) :+
                        (a :+ c :* (con 1 :+ a)))
           refl a b c

  distribʳ (+ suc a) -[1+ b ] -[1+ c ] = cong -[1+_] $
    solve 3 (λ a b c → a :+ (con 1 :+ a :+ (b :+ c) :* (con 1 :+ a))
                    := (con 1 :+ b) :* (con 1 :+ a) :+
                       (a :+ c :* (con 1 :+ a)))
           refl a b c

  distribʳ -[1+ a ] -[1+ b ] (+ suc c) = distrib-lemma a b c

  distribʳ -[1+ a ] (+ suc b) -[1+ c ] = distrib-lemma a c b

  distribʳ (+ suc a) -[1+ b ] (+ suc c)
    rewrite +-⊖-left-cancel a (c ℕ* suc a) (b ℕ* suc a)
    with b ≤? c
  ... | yes b≤c
    rewrite ⊖-≥ b≤c
          | +-comm (- (+ (a ℕ+ b ℕ* suc a))) (+ (a ℕ+ c ℕ* suc a))
          | ⊖-≥ (b≤c *-mono ≤-refl {x = suc a})
          | ℕ.*-distrib-∸ʳ (suc a) c b
          | +‿◃ (c ℕ* suc a ∸ b ℕ* suc a)
          = refl
  ... | no b≰c
    rewrite sign-⊖-≱ b≰c
          | ∣⊖∣-≱ b≰c
          | -‿◃ ((b ∸ c) ℕ* suc a)
          | ⊖-≱ (b≰c ∘ ℕ.cancel-*-right-≤ b c a)
          | ℕ.*-distrib-∸ʳ (suc a) b c
          = refl

  distribʳ (+ suc c) (+ suc a) -[1+ b ]
    rewrite +-⊖-left-cancel c (a ℕ* suc c) (b ℕ* suc c)
    with b ≤? a
  ... | yes b≤a
    rewrite ⊖-≥ b≤a
          | ⊖-≥ (b≤a *-mono ≤-refl {x = suc c})
          | +‿◃ ((a ∸ b) ℕ* suc c)
          | ℕ.*-distrib-∸ʳ (suc c) a b
          = refl
  ... | no b≰a
    rewrite sign-⊖-≱ b≰a
          | ∣⊖∣-≱ b≰a
          | ⊖-≱ (b≰a ∘ ℕ.cancel-*-right-≤ b a c)
          | -‿◃ ((b ∸ a) ℕ* suc c)
          | ℕ.*-distrib-∸ʳ (suc c) b a
          = refl

  -- The IsCommutativeSemiring module contains a proof of
  -- distributivity which is used below.

  isCommutativeSemiring : IsCommutativeSemiring _≡_ _+_ _*_ (+ 0) (+ 1)
  isCommutativeSemiring = record
    { +-isCommutativeMonoid = +-isCommutativeMonoid
    ; *-isCommutativeMonoid = *-isCommutativeMonoid
    ; distribʳ              = distribʳ
    ; zeroˡ                 = λ _ → refl
    }

commutativeRing : CommutativeRing _ _
commutativeRing = record
  { Carrier           = ℤ
  ; _≈_               = _≡_
  ; _+_               = _+_
  ; _*_               = _*_
  ; -_                = -_
  ; 0#                = + 0
  ; 1#                = + 1
  ; isCommutativeRing = record
    { isRing = record
      { +-isAbelianGroup = +-isAbelianGroup
      ; *-isMonoid       = *-isMonoid
      ; distrib          = IsCommutativeSemiring.distrib
                             isCommutativeSemiring
      }
    ; *-comm = *-comm
    }
  }

import Algebra.RingSolver.Simple as Solver
import Algebra.RingSolver.AlmostCommutativeRing as ACR
module RingSolver =
  Solver (ACR.fromCommutativeRing commutativeRing) _≟_

------------------------------------------------------------------------
-- More properties

-- Multiplication is right cancellative for non-zero integers.

cancel-*-right : ∀ i j k →
                 k ≢ + 0 → i * k ≡ j * k → i ≡ j
cancel-*-right i j k            ≢0 eq with signAbs k
cancel-*-right i j .(+ 0)       ≢0 eq | s ◂ zero  = contradiction refl ≢0
cancel-*-right i j .(s ◃ suc n) ≢0 eq | s ◂ suc n
  with ∣ s ◃ suc n ∣ | abs-◃ s (suc n) | sign (s ◃ suc n) | sign-◃ s n
...  | .(suc n)      | refl            | .s               | refl =
  ◃-cong (sign-i≡sign-j i j eq) $
         ℕ.cancel-*-right ∣ i ∣ ∣ j ∣ $ abs-cong eq
  where
  sign-i≡sign-j : ∀ i j →
                  sign i S* s ◃ ∣ i ∣ ℕ* suc n ≡
                  sign j S* s ◃ ∣ j ∣ ℕ* suc n →
                  sign i ≡ sign j
  sign-i≡sign-j i              j              eq with signAbs i | signAbs j
  sign-i≡sign-j .(+ 0)         .(+ 0)         eq | s₁ ◂ zero   | s₂ ◂ zero   = refl
  sign-i≡sign-j .(+ 0)         .(s₂ ◃ suc n₂) eq | s₁ ◂ zero   | s₂ ◂ suc n₂
    with ∣ s₂ ◃ suc n₂ ∣ | abs-◃ s₂ (suc n₂)
  ... | .(suc n₂) | refl
    with abs-cong {s₁} {sign (s₂ ◃ suc n₂) S* s} {0} {suc n₂ ℕ* suc n} eq
  ...   | ()
  sign-i≡sign-j .(s₁ ◃ suc n₁) .(+ 0)         eq | s₁ ◂ suc n₁ | s₂ ◂ zero
    with ∣ s₁ ◃ suc n₁ ∣ | abs-◃ s₁ (suc n₁)
  ... | .(suc n₁) | refl
    with abs-cong {sign (s₁ ◃ suc n₁) S* s} {s₁} {suc n₁ ℕ* suc n} {0} eq
  ...   | ()
  sign-i≡sign-j .(s₁ ◃ suc n₁) .(s₂ ◃ suc n₂) eq | s₁ ◂ suc n₁ | s₂ ◂ suc n₂
    with ∣ s₁ ◃ suc n₁ ∣ | abs-◃ s₁ (suc n₁)
       | sign (s₁ ◃ suc n₁) | sign-◃ s₁ n₁
       | ∣ s₂ ◃ suc n₂ ∣ | abs-◃ s₂ (suc n₂)
       | sign (s₂ ◃ suc n₂) | sign-◃ s₂ n₂
  ... | .(suc n₁) | refl | .s₁ | refl | .(suc n₂) | refl | .s₂ | refl =
    SignProp.cancel-*-right s₁ s₂ (sign-cong eq)

-- Multiplication with a positive number is right cancellative (for
-- _≤_).

cancel-*-+-right-≤ : ∀ m n o → m * + suc o ≤ n * + suc o → m ≤ n
cancel-*-+-right-≤ (-[1+ m ]) (-[1+ n ]) o (-≤- n≤m) =
  -≤- (≤-pred (ℕ.cancel-*-right-≤ (suc n) (suc m) o (s≤s n≤m)))
cancel-*-+-right-≤ ℤ.-[1+ _ ] (+ _)      _ _         = -≤+
cancel-*-+-right-≤ (+ 0)      ℤ.-[1+ _ ] _ ()
cancel-*-+-right-≤ (+ suc _)  ℤ.-[1+ _ ] _ ()
cancel-*-+-right-≤ (+ 0)      (+ 0)      _ _         = +≤+ z≤n
cancel-*-+-right-≤ (+ 0)      (+ suc _)  _ _         = +≤+ z≤n
cancel-*-+-right-≤ (+ suc _)  (+ 0)      _ (+≤+ ())
cancel-*-+-right-≤ (+ suc m)  (+ suc n)  o (+≤+ m≤n) =
  +≤+ (ℕ.cancel-*-right-≤ (suc m) (suc n) o m≤n)

-- Multiplication with a positive number is monotone.

*-+-right-mono : ∀ n → (λ x → x * + suc n) Preserves _≤_ ⟶ _≤_
*-+-right-mono _ (-≤+             {n = 0})         = -≤+
*-+-right-mono _ (-≤+             {n = suc _})     = -≤+
*-+-right-mono x (-≤-                         n≤m) =
  -≤- (≤-pred (s≤s n≤m *-mono ≤-refl {x = suc x}))
*-+-right-mono _ (+≤+ {m = 0}     {n = 0}     m≤n) = +≤+ m≤n
*-+-right-mono _ (+≤+ {m = 0}     {n = suc _} m≤n) = +≤+ z≤n
*-+-right-mono _ (+≤+ {m = suc _} {n = 0}     ())
*-+-right-mono x (+≤+ {m = suc _} {n = suc _} m≤n) =
  +≤+ (m≤n *-mono ≤-refl {x = suc x})


text:
open import Nat
open import Prelude
open import List
open import contexts
open import judgemental-erase
open import moveerase
open import sensibility
open import statics-checks
open import statics-core

module examples where
  -- actions must always specify enough names to name all inserted holes. depending on
  -- the context, not all names are used, and we pass this argument to make that clear.
  -- an actual implementation could automatically insert hole names as needed
  no-hole : Nat
  no-hole = 0

  -- the function (λx. x + 1) where x is named "0".
  add1 : hexp
  add1 = ·λ 0 (X 0 ·+ N 1)

  -- this is the derivation that fn has type num ==> num
  ex1 : ∅ ⊢ add1 <= (num ==> num)
  ex1 = ALam refl MAArr
             (ASubsume (SPlus (ASubsume (SVar refl) TCRefl) (ASubsume SNum TCRefl))
                       TCRefl)

  -- the derivation that when applied to the numeric argument 10 add1
  -- produces a num.
  ex2 : ∅ ⊢ (add1 ·: (num ==> num)) ∘ (N 10) => num
  ex2 = SAp (SAsc ex1) MAArr (ASubsume SNum TCRefl)

  -- the slightly longer derivation that argues that add1 applied to a
  -- variable that's known to be a num produces a num
  ex2b : (∅ ,, (1 , num)) ⊢ (add1 ·: (num ==> num)) ∘ (X 1) => num
  ex2b = SAp (SAsc (ALam refl MAArr
                   (ASubsume (SPlus (ASubsume (SVar refl) TCRefl) (ASubsume SNum TCRefl))
                             TCRefl)))
             MAArr (ASubsume (SVar refl) TCRefl)

  -- eta-expanding addition to curry it gets num → num → num
  ex3 : ∅ ⊢ ·λ 0 ( (·λ 1 (X 0 ·+ X 1)) ·: (num ==> num))
               <= (num ==> (num ==> num))
  ex3 = ALam refl MAArr (ASubsume (SAsc (ALam refl MAArr (ASubsume
                                                            (SPlus (ASubsume (SVar refl) TCRefl) (ASubsume (SVar refl) TCRefl))
                                                            TCRefl))) TCRefl)

  -- applying three to four has type hole -- but there is no action that
  -- can fill the hole in the type so this term is forever incomplete.
  ex4 : ∅ ⊢ ((N 3) ·: ⦇-⦈) ∘ (N 4) => ⦇-⦈
  ex4 = SAp (SAsc (ASubsume SNum TCHole2)) MAHole (ASubsume SNum TCHole2)

  -- this module contains small examples that demonstrate the judgements
  -- and definitions in action. a few of them are directly from the paper,
  -- to aid in comparision between the on-paper notation and the
  -- corresponding agda syntax.

  -- these smaller derivations motivate the need for the zipper rules: you
  -- have to unzip down to the point of the structure where you want to
  -- apply an edit, do the local edit rule, and then put it back together
  -- around you
  talk0 :  ∅ ⊢ (▹ ⦇-⦈[ 0 ] ◃ ·+₁ ⦇-⦈[ 1 ]) => num ~ construct (numlit 7 no-hole) ~>
               (▹ N 7 ◃  ·+₁ ⦇-⦈[ 1 ]) => num
  talk0 = SAZipPlus1 (AASubsume EETop SEHole SAConNumlit TCRefl)

  talk1 : ∅ ⊢ (·λ 0 ⦇-⦈[ 0 ] ·:₂ (▹ ⦇-⦈ ◃ ==>₁ ⦇-⦈)) => (⦇-⦈ ==> ⦇-⦈) ~ construct num ~>
              (·λ 0 ⦇-⦈[ 0 ] ·:₂ (▹ num ◃ ==>₁ ⦇-⦈)) => (num ==> ⦇-⦈)
  talk1 = SAZipAsc2 (TMArrZip1 TMConNum) (ETArrL ETTop) (ETArrL ETTop)
                    (ALam refl MAArr (ASubsume SEHole TCRefl))

  -- this is similar to figure one from the paper, but with a half annotated lambda
  -- rather than a lambda with a full type ascription
  fig1-l : List action
  fig1-l = construct (lam 0 no-hole no-hole) ::
           construct num ::
           move parent ::
           move (child 2) ::
           construct (var 0 no-hole) ::
           construct (plus no-hole no-hole) ::
           construct (numlit 1 no-hole) ::
           []

  figure1 : runsynth ∅ ▹ ⦇-⦈[ 0 ] ◃ ⦇-⦈ fig1-l
            (·λ 0 ·[ num ]₂ (X 0 ·+₂ ▹ N 1 ◃)) (num ==> num)
  figure1 =
    DoSynth (SAConLam refl)
   (DoSynth (SAZipLam1 refl ETTop ETTop TMConNum SEHole SEHole)
   (DoSynth (SAMove EMHalfLamParent1)
   (DoSynth (SAMove EMHalfLamChild2)
   (DoSynth (SAZipLam2 refl EETop SEHole (SAConVar refl))
   (DoSynth (SAZipLam2 refl EETop (SVar refl) (SAConPlus1 TCRefl))
   (DoSynth (SAZipLam2 refl (EEPlusR EETop)
            (SPlus (ASubsume (SVar refl) TCRefl) (ASubsume SEHole TCHole1))
            (SAZipPlus2 (AASubsume EETop SEHole SAConNumlit TCRefl))) DoRefl))))))

  -- this is figure two from the paper
  incr : Nat
  incr = 0

  fig2-l : List action
  fig2-l = construct (var incr no-hole) ::
           construct (ap no-hole no-hole) ::
           construct (var incr 0) ::
           construct (ap no-hole no-hole) ::
           construct (numlit 3 no-hole) ::
           move parent ::
           move parent ::
           finish ::
           []

  figure2 : runsynth (∅ ,, (incr , num ==> num)) ▹ ⦇-⦈[ 0 ] ◃ ⦇-⦈ fig2-l
            (X incr ∘₂ ▹ X incr ∘ (N 3) ◃)  num
  figure2 =
    DoSynth (SAConVar refl)
   (DoSynth (SAConApArr MAArr)
   (DoSynth (SAZipApAna MAArr (SVar refl) (AAConVar (λ ()) refl))
   (DoSynth (SAZipApAna MAArr (SVar refl)
            (AASubsume (EENEHole EETop) (SNEHole (SVar refl))
                       (SAZipNEHole EETop (SVar refl) (SAConApArr MAArr)) TCHole1))
   (DoSynth (SAZipApAna MAArr (SVar refl)
            (AASubsume (EENEHole (EEApR EETop))
                       (SNEHole (SAp (SVar refl) MAArr (ASubsume SEHole TCHole1)))
                       (SAZipNEHole (EEApR EETop)
                                    (SAp (SVar refl) MAArr (ASubsume SEHole TCHole1))
                                    (SAZipApAna MAArr (SVar refl)
                                                (AASubsume EETop SEHole SAConNumlit TCRefl)))
            TCHole1))
   (DoSynth (SAZipApAna MAArr (SVar refl)
            (AASubsume (EENEHole (EEApR EETop))
                       (SNEHole (SAp (SVar refl) MAArr (ASubsume SNum TCRefl)))
                       (SAZipNEHole (EEApR EETop) (SAp (SVar refl) MAArr
                                    (ASubsume SNum TCRefl)) (SAMove EMApParent2))
                       TCHole1))
   (DoSynth (SAZipApAna MAArr (SVar refl) (AAMove EMNEHoleParent))
   (DoSynth (SAZipApAna MAArr (SVar refl)
            (AAFinish (ASubsume (SAp (SVar refl) MAArr (ASubsume SNum TCRefl)) TCRefl)))
            DoRefl)))))))

  --- this demonstrates that the other ordering discussed is also fine. it
  --- results in different proof terms and actions but ultimately produces
  --- the same expression. there are many other lists of actions that would
  --- also work, these are just two.
  fig2alt-l : List action
  fig2alt-l = construct (var incr no-hole) ::
              construct (ap no-hole 0) ::
              construct (ap no-hole 1) ::
              construct (numlit 3 no-hole) ::
              move parent ::
              move (child 1) ::
              construct (var incr no-hole) ::
              move parent ::
              []

  figure2alt : runsynth (∅ ,, (incr , num ==> num)) ▹ ⦇-⦈[ 0 ] ◃ ⦇-⦈ fig2alt-l
                        (X incr ∘₂ ▹ X incr ∘ (N 3) ◃) num
  figure2alt =
    DoSynth (SAConVar refl)
   (DoSynth (SAConApArr MAArr)
   (DoSynth (SAZipApAna MAArr (SVar refl)
                        (AASubsume EETop SEHole (SAConApArr MAHole) TCHole1))
   (DoSynth (SAZipApAna MAArr (SVar refl) (AASubsume (EEApR EETop)
            (SAp SEHole MAHole (ASubsume SEHole TCRefl))
            (SAZipApAna MAHole SEHole (AASubsume EETop SEHole SAConNumlit TCHole2)) TCHole1))
   (DoSynth (SAZipApAna MAArr (SVar refl) (AAMove EMApParent2))
   (DoSynth (SAZipApAna MAArr (SVar refl) (AAMove EMApChild1))
   (DoSynth (SAZipApAna MAArr (SVar refl) (AASubsume (EEApL EETop)
            (SAp SEHole MAHole (ASubsume SNum TCHole2))
            (SAZipApArr MAArr EETop SEHole (SAConVar refl) (ASubsume SNum TCRefl)) TCRefl))
   (DoSynth (SAZipApAna MAArr (SVar refl) (AAMove EMApParent1))
            DoRefl)))))))

  -- these motivate why actions aren't deterministic, and why it's
  -- reasonable to ban the derivations that we do. the things that differ
  -- in the term as a result of the appeal to subsumption in the second
  -- derivation aren't needed -- the ascription is redundant because the
  -- type is already pinned to num, so that's the only thing that
  -- could fill the holes produced.
  notdet1A : ∅ ⊢ ▹ ⦇-⦈[ 0 ] ◃ ~ construct asc ~> ⦇-⦈[ 0 ] ·:₂ ▹ num ◃ ⇐ num
  notdet1A = AAConAsc

  notdet1B : ∅ ⊢ ▹ ⦇-⦈[ 0 ] ◃ ~ construct asc ~> ⦇-⦈[ 0 ] ·:₂ ▹ ⦇-⦈ ◃ ⇐ num
  notdet1B = AASubsume EETop SEHole SAConAsc TCHole1

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


text:
module 050-group where

-- We need monoids.

open import 040-monoid

-- A group is a monoid where every element has an inverse. This is
-- equivalent to saying that we have a function mapping every element
-- to an inverse of that element: this function is called "invert"
-- below.

record Group
  {M : Set}
  (_==_ : M -> M -> Set)
  (_*_ : M -> M -> M)
  (id : M)
  (invert : M -> M)
  : Set1 where
  field
    monoid : Monoid _==_ _*_ id
    icong : ∀ {r s} -> (r == s) -> (invert r) == (invert s)
    r*ir==id : ∀ {r} -> (r * (invert r)) == id
    ir*r==id : ∀ {r} -> ((invert r) * r) == id

  open Monoid monoid public

  -- Trivial but useful equalities.
  id==r*ir : ∀ {r} -> id == (r * (invert r))
  id==r*ir = symm r*ir==id
  id==ir*r : ∀ {r} -> id == ((invert r) * r)
  id==ir*r = symm ir*r==id

  -- Double inverse gets back original.
  iir==r : ∀ {r} -> (invert (invert r)) == r
  iir==r {r} = trans3 iir==r*ir*iir r*ir*iir==r*id r*id==r
    where iir==r*ir*iir :
            (invert (invert r)) == (r * ((invert r) * (invert (invert r))))
          iir==r*ir*iir = trans3 r==id*r (cong id==r*ir refl) assoc
          -- assoc {r} {ir} {iir} : (r * ir) * iir == r * (ir * iir)
          -- id==r*ir             : id == r * ir
          -- cong % (refl {iir})  : id * iir == (r * ir) * iir
          -- id*r==r {iir}        : iir == id * iir
          -- trans3 % %% %%%%     : iir == r * (ir * iir)
          r*ir*iir==r*id : (r * ((invert r) * (invert (invert r)))) == (r * id)
          r*ir*iir==r*id = cong refl r*ir==id

  -- Uniqueness of (left and right) inverse.
  irleftunique : ∀ {r} -> ∀ {s} -> (s * r) == id -> s == (invert r)
  irleftunique {r} {s} s*r==id = trans (symm s*r*ir==s) (s*r*ir==ir)
    where s*r*ir==ir : ((s * r) * (invert r)) == (invert r)
          s*r*ir==ir = trans (cong s*r==id refl) id*r==r
          s*r*ir==s : ((s * r) * (invert r)) == s
          s*r*ir==s = trans3 assoc (cong refl r*ir==id) r*id==r
  irrightunique : ∀ {r} -> ∀ {s} -> (r * s) == id -> s == (invert r)
  irrightunique {r} {s} r*s==id = trans (symm ir*r*s==s) (ir*r*s==ir)
    where ir*r*s==ir : ((invert r) * (r * s)) == (invert r)
          ir*r*s==ir = trans (cong refl r*s==id) r*id==r
          ir*r*s==s : ((invert r) * (r * s)) == s
          ir*r*s==s = trans3 (symm assoc) (cong ir*r==id refl) id*r==r

max_stars_repo_name: mcmtroffaes/agda-proofs

max_issues_repo_name: mcmtroffaes/agda-proofs

max_forks_repo_name: mcmtroffaes/agda-proofs


text:
------------------------------------------------------------------------------
-- Some properties of the function iter₀
------------------------------------------------------------------------------

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

module FOTC.Program.Iter0.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import FOTC.Base
open import FOTC.Base.PropertiesI
open import FOTC.Base.List
open import FOTC.Data.List.PropertiesI
open import FOTC.Data.Nat.Type
open import FOTC.Data.Nat.List.Type
open import FOTC.Program.Iter0.Iter0

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

iter₀-0 : ∀ f → iter₀ f zero ≡ []
iter₀-0 f =
  iter₀ f zero
    ≡⟨ iter₀-eq f zero ⟩
  (if (iszero₁ zero) then [] else (zero ∷ iter₀ f (f · zero)))
    ≡⟨ ifCong₁ iszero-0 ⟩
  (if true then [] else (zero ∷ iter₀ f (f · zero)))
    ≡⟨ if-true [] ⟩
  [] ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

{- After a few preliminary lemmata about representing dependent functions,
   this module will derive the dependent universal property of
   our truncations (defined later) from the non-dependent one. -}
module Universe.Trunc.Universal where

open import lib.Basics
open import lib.Equivalences2
open import lib.NType2
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Unit

open import Universe.Utility.General
open import Universe.Utility.TruncUniverse

-- In the fibration fst : Σ A B → A, the fiber over a is given by B a.
trivial-fibers : ∀ {i j} {A : Type i} {B : A → Type j} (a : A)
                 → B a ≃ Σ (Σ A B) (λ s → a == fst s)
trivial-fibers {A = A} {B} a =
  B a                               ≃⟨ Σ₁-Unit ⁻¹ ⟩
  Σ ⊤ (λ _ → B a)                   ≃⟨ equiv-Σ-fst _ (snd (e ⁻¹)) ⟩
  Σ (Σ A (λ s → a == s)) (B ∘ fst)  ≃⟨ Σ-comm-snd ⟩
  Σ (Σ A B) (λ s → a == fst s)      ≃∎ where

  e : Σ A (λ s → a == s) ≃ ⊤
  e = contr-equiv-Unit (pathfrom-is-contr a)

{- Liftings of u : Π A B through fst : {a : A} → Σ (B a) (C a) → B a
   correponds to dependent functions from (a : A) to C a (u a).

   As mentioned in the article, we will make use only of a special case:
   liftings of u : A → B through fst : Σ B C → B correponds to
   dependent functions from (a : A) to C a. -}
Π-as-liftings : ∀ {i j k} {A : Type i} {B : A → Type j}
             (u : Π A B) {C : (a : A) → B a → Type k} → _
Π-as-liftings {A = A} {B} u {C} =
    Π A (λ a → C a (u a))
  ≃⟨ trivial-fibers u ⟩
    Σ (Σ (Π A B) (λ r → Π A (λ a → C a (r a)))) (λ {(r , _) → u == r})
  ≃⟨ equiv-Σ-fst _ (snd choice) ⁻¹ ⟩
    Σ (Π A (λ a → Σ (B a) (C a))) (λ s → u == fst ∘ s)
  ≃∎

{- Dependent functions from (a : A) to B a
   are given by sections of fst : Σ A B → A.

   Noting that sections are non-dependent functions, this folklore insight
   is a main ingredient in passing from non-dependent universal property
   to the dependent one. -}
Π-as-sections : ∀ {i j} {A : Type i} {B : A → Type j}
                → Π A B ≃ Σ (A → Σ A B) (λ s → idf _ == fst ∘ s)
Π-as-sections = Π-as-liftings (idf _)

{- Fix a truncation level n and a Type A. We will examine what it means
   for an n-type 'type' with constructor cons : A → ⟦ type ⟧
   to have the universal property of the n-truncation of A. -}
module _ {i} {n : ℕ₋₂} {A : Type i}
         (type : n -Type i) (cons : A → ⟦ type ⟧) where

  -- *** Definition 6.2 ***
  {- The (non-dependent) universal property:
     λ f → f ∘ cons  induces equivalence  (type → X) ≃ (A → X) -}
  univ-Type : ∀ (k : ULevel) → Type (i ⊔ lsucc k)
  univ-Type k = (X : n -Type k) → is-equiv
                  {A = ⟦ type ⟧ → ⟦ X ⟧}
                  {B = A → ⟦ X ⟧}
                  (λ f → f ∘ cons)

  {- The dependent universal property:
     λ f → f ∘ cons  induces  ((a : type) → X a) ≃ ((a : A) → X (cons a)) -}
  duniv-Type : ∀ (k : ULevel) → Type (i ⊔ lsucc k)
  duniv-Type k = (X : ⟦ type ⟧ → n -Type k) → is-equiv
                   {A = Π ⟦ type ⟧ (⟦_⟧ ∘ X )}
                   {B = Π A (⟦_⟧ ∘ X ∘ cons)}
                   (λ f → f ∘ cons)

  {- If the universal property holds for a certain elimination universe U_j₂,
     then also for an elimination universe U_j₁ with j₁ ≤ j₂.
     Agda does not support specifying ordering relations between
     universe levels directly, but we may simulate j₁ ≤ j₂
     by decomposing j₁ = k₁ and j₂ = k₁ ⊔ k₂. -}
  univ-lower : ∀ {k₁} (k₂ : ULevel) → univ-Type (k₁ ⊔ k₂) → univ-Type k₁
  univ-lower {k₁} k₂ univ X = transport (λ z → is-equiv (λ f → z ∘ f ∘ cons))
                                        (λ= (<–-inv-r e)) hup where
    e : Lift {j = k₁ ⊔ k₂} ⟦ X ⟧ ≃ ⟦ X ⟧
    e = lift-equiv

    hup : is-equiv (λ f → –> e ∘ <– e ∘ f ∘ cons)
    hup = pre∘-is-equiv (snd e)
     ∘ise univ (Lift-≤ X)
     ∘ise pre∘-is-equiv (snd (e ⁻¹))

  -- *** Lemma 6.6 ***
  {- We will now prove the main lemma of this section:
     The (non-dependent) universal property implies the dependent one. -}
  module with-univ {j} (univ : univ-Type (i ⊔ j)) (P : ⟦ type ⟧ → n -Type j) where

    -- abbreviating the underlying types (for readability)
    T = ⟦ type ⟧
    Q = ⟦_⟧ ∘ P

    {- As is usual for deriving dependent eliminators, the crux for deriving
       the dependent universal property is to first transform the *dependent*
       function spaces into *non-dependent* sections/liftings according to
       the lemmata above. -}
    eqv : Π T Q ≃ Π A (Q ∘ cons)
    eqv = Π-as-liftings cons ⁻¹ ∘e eqv-liftings ∘e Π-as-liftings (idf _) where

      {- Our goal now is an equivalence of Σ-types where the first components
         fit the template of the *non-dependent* universal property. -}
      eqv-liftings : Σ (T → Σ T Q) (λ s → idf _ == fst ∘ s)
                   ≃ Σ (A → Σ T Q) (λ t → cons  == fst ∘ t)
      eqv-liftings = equiv-Σ' (_ , univ (Σ-≤ type P)) lem where

        {- What remains is just the universal property applied to X itself,
           and then switching to path spaces. In the usual derivation of
           dependent elimination, this corresponds to application of
           the η-rule to the identity function. -}
        lem : (s : T → Σ T Q) → (idf _ == fst ∘ s) ≃ (cons == fst ∘ s ∘ cons)
        lem s = equiv-ap (_ , univ-lower (i ⊔ j) univ type) (idf _) (fst ∘ s)

    {- Due to construction of the above equivalence via conjugation of
       the (non-dependent) universal property (on the first component),
       its action ends up being precisely composition with the constructor.
       Because of technical limitations of the Agda type-checker,
       we encapsulate the result in an abstract block to prevent
       the type checker from unnecessarily unfolding its value later on. -}
    abstract
      duniv : is-equiv (λ (f : ⟦ Π-≤ ⟦ type ⟧ P ⟧) → f ∘ cons)
      duniv = snd eqv

max_stars_repo_name: sattlerc/HoTT-Agda

max_issues_repo_name: sattlerc/HoTT-Agda

max_forks_repo_name: sattlerc/HoTT-Agda


text:
-- notes-03-wednesday.agda

open import mylib

{-
  Classical vs intuitionistic logic
  In classical logica, we assume that each proposition is either true or false.
  Excluded middle, tertium non datur (the third is not given).
  To prove P, assume not P and derive a contradiction: indirect proof, reduction
  ad absurdum, reduction to the absurd.

-}

TND : prop → prop
TND P = P ∨ ¬ P

deMorgan' : TND P → ¬ (P ∧ Q) ⇔ ¬ P ∨ ¬ Q
proj₁ (deMorgan' (inj₁ p)) h = inj₂ (λ q → h (p , q))
proj₁ (deMorgan' (inj₂ np)) h = inj₁ np
proj₂ (deMorgan' tnd) (inj₁ np) (p , q) = np p
proj₂ (deMorgan' _)  (inj₂ nq) (p , q) = nq q

RAA : prop → prop
RAA P = ¬ ¬ P → P

tnd→raa : TND P → RAA P
tnd→raa (inj₁ p) nnp = p
tnd→raa (inj₂ np) nnp = case⊥ (nnp np)

{-
raa→tnd : RAA P → TND P
is not provable.
-}

nntnd : ¬ ¬ (P ∨ ¬ P)
nntnd h = h (inj₂ (λ p → h (inj₁ p)))

raa→tnd : ({P : prop} → RAA P) → {Q : prop} → TND Q
raa→tnd raa = raa nntnd

{-
  Datatypes, infinite types
  ℕ - natural numbers, Peano
  Every natural number is either 0 or a successor of a number.
  Peano arithmetic.
-}

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

one : ℕ
one = suc zero

two : ℕ
two = suc one

{-# BUILTIN NATURAL ℕ #-}

fifteen : ℕ
fifteen = 15

infixl 2 _+_
_+_ : ℕ → ℕ → ℕ -- structural recursive definition
zero + n = n
suc m + n = suc (m + n)

infixl 4 _*_
_*_ : ℕ → ℕ → ℕ
zero * n = 0
suc m * n = m * n + n

data List (A : Set) : Set where
  [] : List A -- nil
  _∷_ : A → List A → List A -- cons

-- ℕ = List ⊤

_++_ : List A → List A → List A -- append
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

-- _++'_ : List A \to List B \to List (A \vee B)?

-- recursive but not inductive
{-# NO_POSITIVITY_CHECK #-}
data Λ : Set where
  lam : (Λ → Λ) → Λ

app : Λ → Λ → Λ
app (lam f) x = f x

self-apply : Λ
self-apply = lam λ x → app x x

Ω : Λ
Ω = app self-apply self-apply
-- normalisation doesn't terminate

data Ord : Set where
  zero : Ord
  suc : Ord → Ord
  lim : (ℕ → Ord) → Ord

-- strictly positive

{-# NO_POSITIVITY_CHECK #-}
data Reynolds : Set where
  inn : ((Reynolds → Bool) → Bool) → Reynolds

{-
  Inconsistent with classical logic
  It doesn't adhere to the intuitionistic explanation of inductive datatypes.
  Hence we reject types like this.
  - strictly positive = recursive type only appears on the right of an arrow
    type.
  - strictly positive = container / polynomial functors.
-}

max_stars_repo_path: Type Theory/notes-03-wednesday.agda

max_issues_repo_path: Type Theory/notes-03-wednesday.agda

max_forks_repo_path: Type Theory/notes-03-wednesday.agda


text:
------------------------------------------------------------------------
-- Substitutions
------------------------------------------------------------------------

module RecursiveTypes.Substitution where

open import Data.Fin.Substitution
open import Data.Fin.Substitution.Lemmas
import Data.Fin.Substitution.List as ListSubst
open import Data.Nat
open import Data.List
open import Data.Vec as Vec
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl; sym; cong₂)
open PropEq.≡-Reasoning
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
  using (Star; ε; _◅_; _▻_)

open import RecursiveTypes.Syntax

-- Code for applying substitutions.

module TyApp {T : ℕ → Set} (l : Lift T Ty) where
  open Lift l hiding (var)

  -- Applies a substitution to a recursive type.

  infixl 8 _/_

  _/_ : ∀ {m n} → Ty m → Sub T m n → Ty n
  ⊥       / ρ = ⊥
  ⊤       / ρ = ⊤
  var x   / ρ = lift (Vec.lookup ρ x)
  σ ⟶ τ   / ρ = (σ / ρ) ⟶ (τ / ρ)
  μ σ ⟶ τ / ρ = μ (σ / ρ ↑) ⟶ (τ / ρ ↑)

  open Application (record { _/_ = _/_ }) using (_/✶_)

  -- Some lemmas about _/_.

  ⊥-/✶-↑✶ : ∀ k {m n} (ρs : Subs T m n) → ⊥ /✶ ρs ↑✶ k ≡ ⊥
  ⊥-/✶-↑✶ k ε        = refl
  ⊥-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (⊥-/✶-↑✶ k ρs) refl

  ⊤-/✶-↑✶ : ∀ k {m n} (ρs : Subs T m n) → ⊤ /✶ ρs ↑✶ k ≡ ⊤
  ⊤-/✶-↑✶ k ε        = refl
  ⊤-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (⊤-/✶-↑✶ k ρs) refl

  ⟶-/✶-↑✶ : ∀ k {m n σ τ} (ρs : Subs T m n) →
            σ ⟶ τ /✶ ρs ↑✶ k ≡ (σ /✶ ρs ↑✶ k) ⟶ (τ /✶ ρs ↑✶ k)
  ⟶-/✶-↑✶ k ε        = refl
  ⟶-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (⟶-/✶-↑✶ k ρs) refl

  μ⟶-/✶-↑✶ : ∀ k {m n σ τ} (ρs : Subs T m n) →
             μ σ ⟶ τ /✶ ρs ↑✶ k ≡
             μ (σ /✶ ρs ↑✶ suc k) ⟶ (τ /✶ ρs ↑✶ suc k)
  μ⟶-/✶-↑✶ k ε        = refl
  μ⟶-/✶-↑✶ k (ρ ◅ ρs) = cong₂ _/_ (μ⟶-/✶-↑✶ k ρs) refl

tySubst : TermSubst Ty
tySubst = record { var = var; app = TyApp._/_ }

open TermSubst tySubst hiding (var)

-- σ [0≔ τ ] replaces all occurrences of variable 0 in σ with τ.

infix 8 _[0≔_]

_[0≔_] : ∀ {n} → Ty (suc n) → Ty n → Ty n
σ [0≔ τ ] = σ / sub τ

-- The unfolding of a fixpoint.

unfold[μ_⟶_] : ∀ {n} → Ty (suc n) → Ty (suc n) → Ty n
unfold[μ σ ⟶ τ ] = σ ⟶ τ [0≔ μ σ ⟶ τ ]

-- Substitution lemmas.

tyLemmas : TermLemmas Ty
tyLemmas = record
  { termSubst = tySubst
  ; app-var   = refl
  ; /✶-↑✶     = Lemma./✶-↑✶
  }
  where
  module Lemma {T₁ T₂} {lift₁ : Lift T₁ Ty} {lift₂ : Lift T₂ Ty} where

    open Lifted lift₁ using () renaming (_↑✶_ to _↑✶₁_; _/✶_ to _/✶₁_)
    open Lifted lift₂ using () renaming (_↑✶_ to _↑✶₂_; _/✶_ to _/✶₂_)

    /✶-↑✶ : ∀ {m n} (ρs₁ : Subs T₁ m n) (ρs₂ : Subs T₂ m n) →
            (∀ k x → var x /✶₁ ρs₁ ↑✶₁ k ≡ var x /✶₂ ρs₂ ↑✶₂ k) →
            ∀ k t → t /✶₁ ρs₁ ↑✶₁ k ≡ t /✶₂ ρs₂ ↑✶₂ k
    /✶-↑✶ ρs₁ ρs₂ hyp k ⊥ = begin
      ⊥ /✶₁ ρs₁ ↑✶₁ k  ≡⟨ TyApp.⊥-/✶-↑✶ _ k ρs₁ ⟩
      ⊥                ≡⟨ sym (TyApp.⊥-/✶-↑✶ _ k ρs₂) ⟩
      ⊥ /✶₂ ρs₂ ↑✶₂ k  ∎
    /✶-↑✶ ρs₁ ρs₂ hyp k ⊤ = begin
      ⊤ /✶₁ ρs₁ ↑✶₁ k  ≡⟨ TyApp.⊤-/✶-↑✶ _ k ρs₁ ⟩
      ⊤                ≡⟨ sym (TyApp.⊤-/✶-↑✶ _ k ρs₂) ⟩
      ⊤ /✶₂ ρs₂ ↑✶₂ k  ∎
    /✶-↑✶ ρs₁ ρs₂ hyp k (var x) = hyp k x
    /✶-↑✶ ρs₁ ρs₂ hyp k (σ ⟶ τ) = begin
      σ ⟶ τ /✶₁ ρs₁ ↑✶₁ k                    ≡⟨ TyApp.⟶-/✶-↑✶ _ k ρs₁ ⟩
      (σ /✶₁ ρs₁ ↑✶₁ k) ⟶ (τ /✶₁ ρs₁ ↑✶₁ k)  ≡⟨ cong₂ _⟶_ (/✶-↑✶ ρs₁ ρs₂ hyp k σ)
                                                          (/✶-↑✶ ρs₁ ρs₂ hyp k τ) ⟩
      (σ /✶₂ ρs₂ ↑✶₂ k) ⟶ (τ /✶₂ ρs₂ ↑✶₂ k)  ≡⟨ sym (TyApp.⟶-/✶-↑✶ _ k ρs₂) ⟩
      σ ⟶ τ /✶₂ ρs₂ ↑✶₂ k                    ∎
    /✶-↑✶ ρs₁ ρs₂ hyp k (μ σ ⟶ τ) = begin
      μ σ ⟶ τ /✶₁ ρs₁ ↑✶₁ k                            ≡⟨ TyApp.μ⟶-/✶-↑✶ _ k ρs₁ ⟩
      μ (σ /✶₁ ρs₁ ↑✶₁ suc k) ⟶ (τ /✶₁ ρs₁ ↑✶₁ suc k)  ≡⟨ cong₂ μ_⟶_ (/✶-↑✶ ρs₁ ρs₂ hyp (suc k) σ)
                                                                     (/✶-↑✶ ρs₁ ρs₂ hyp (suc k) τ) ⟩
      μ (σ /✶₂ ρs₂ ↑✶₂ suc k) ⟶ (τ /✶₂ ρs₂ ↑✶₂ suc k)  ≡⟨ sym (TyApp.μ⟶-/✶-↑✶ _ k ρs₂) ⟩
      μ σ ⟶ τ /✶₂ ρs₂ ↑✶₂ k                            ∎

open TermLemmas tyLemmas public hiding (var)

module // where

  private
    open module LS = ListSubst lemmas₄ public hiding (_//_)

  -- _//_ is redefined in order to make it bind weaker than
  -- RecursiveTypes.Subterm._∗, which binds weaker than _/_.

  infixl 6 _//_

  _//_ : ∀ {m n} → List (Ty m) → Sub Ty m n → List (Ty n)
  _//_ = LS._//_

max_stars_repo_name: nad/codata

max_issues_repo_name: nad/codata

max_forks_repo_name: nad/codata


text:
-- A tactic that applies congruence and symmetry of equality proofs.
-- Given a hole and a lemma it tries (in order)
--   - refl
--   - lemma
--   - sym lemma
--   - f $≡ X₁ *≡ .. *≡ Xₙ and recurses on Xᵢ
--     if the goal is f us ≡ f vs
--     Hidden and instance arguments of f are left alone.

module Tactic.Cong where

open import Prelude
open import Container.Traversable
open import Tactic.Reflection

private
  refl′ : ∀ {a} {A : Set a} (x : A) → x ≡ x
  refl′ _ = refl

  pattern `refl a = def₁ (quote refl′) a

  parseEq : Term → Maybe (Term × Term)
  parseEq (def (quote _≡_) (hArg _ ∷ hArg _ ∷ vArg x ∷ vArg y ∷ [])) = just (x , y)
  parseEq _ = nothing

  -- build-cong f ps = f $≡ p₁ *≡ .. *≡ pₙ
  build-cong : Term → List Term → Term
  build-cong f [] = `refl unknown -- we tried this
  build-cong f (p ∷ ps) = foldl ap (def₂ (quote cong) f p) ps
    where
      ap = λ p q → def₂ (quote _*≡_) p q

  zipWithM!₃ : {A B C : Set} → (A → B → C → TC ⊤) → List A → List B → List C → TC ⊤
  zipWithM!₃ f (x ∷ xs) (y ∷ ys) (z ∷ zs) = f x y z *> zipWithM!₃ f xs ys zs
  zipWithM!₃ _ _ _ _ = pure _

  module _ (lemma : Term) where

    go go-cong : (d : Nat) (lhs rhs hole : Term) → TC ⊤
    go d lhs rhs hole =
      checkType hole (def₂ (quote _≡_) lhs rhs) *>
      (   unify hole (`refl lhs)
      <|> unify hole lemma
      <|> unify hole (def₁ (quote sym) lemma)
      <|> go-cong d lhs rhs hole
      <|> do lhs ← reduce lhs
             rhs ← reduce rhs
             go-cong d lhs rhs hole)

    solve : (d : Nat) (hole : Term) → TC ⊤
    solve d hole =
      caseM parseEq <$> (reduce =<< inferType hole) of λ where
        nothing → typeErrorS "Goal is not an equality type."
        (just (lhs , rhs)) → go d lhs rhs hole

    go-cong′ : ∀ d f us vs hole → TC ⊤
    go-cong′ d f us vs hole = do
      let us₁ = map unArg (filter isVisible us)
          vs₁ = map unArg (filter isVisible vs)
      holes ← traverse (const newMeta!) us₁
      zipWithM!₃ (go d) us₁ vs₁ holes
      unify hole (build-cong f holes)

    go-cong (suc d) (def f us) (def f₁ vs) hole = guard (f == f₁) (go-cong′ d (def₀ f) us vs hole)
    go-cong (suc d) (con c us) (con c₁ vs) hole = guard (c == c₁) (go-cong′ d (con₀ c) us vs hole)
    go-cong (suc d) (var x us) (var x₁ vs) hole = guard (x == x₁) (go-cong′ d (var₀ x) us vs hole)
    go-cong _ lhs rhs _ = empty

macro
  by-cong : ∀ {a} {A : Set a} {x y : A} → x ≡ y → Tactic
  by-cong {x = x} {y} lemma hole = do
      `lemma  ← quoteTC lemma
      ensureNoMetas =<< inferType hole
      lemMeta ← lemProxy `lemma
      solve lemMeta 100 hole <|> typeErrorS "Congruence failed"
      unify lemMeta `lemma
    where
      -- Create a meta for the lemma to avoid retype-checking it in case
      -- it's expensive. Don't do this if the lemma is a variable.
      lemProxy : Term → TC Term
      lemProxy lemma@(var _ []) = pure lemma
      lemProxy lemma = newMeta =<< quoteTC (x ≡ y)

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
------------------------------------------------------------------------
-- A definitional interpreter
------------------------------------------------------------------------

{-# OPTIONS --cubical --sized-types #-}

module Lambda.Partiality-monad.Inductive.Interpreter where

open import Equality.Propositional.Cubical
open import Prelude hiding (⊥)

open import Bijection equality-with-J using (_↔_)
open import Function-universe equality-with-J hiding (id; _∘_)
open import Maybe equality-with-J
open import Monad equality-with-J
open import Vec.Function equality-with-J

open import Partiality-monad.Inductive
open import Partiality-monad.Inductive.Fixpoints
open import Partiality-monad.Inductive.Monad

open import Lambda.Syntax hiding ([_])

open Closure Tm

------------------------------------------------------------------------
-- An interpreter monad

-- The interpreter monad.

M : ∀ {ℓ} → Type ℓ → Type ℓ
M = MaybeT _⊥

-- Information ordering.

infix 4 _⊑M_

_⊑M_ : ∀ {a} {A : Type a} → M A → M A → Type a
x ⊑M y = run x ⊑ run y

-- Bind is monotone.

_>>=ᵐ-mono_ :
  ∀ {ℓ} {A B : Type ℓ} {x y : M A} {f g : A → M B} →
  x ⊑M y → (∀ z → f z ⊑M g z) → x >>= f ⊑M y >>= g
_>>=ᵐ-mono_ {x = x} {y} {f} {g} x⊑y f⊑g =
  run x >>= maybe (MaybeT.run ∘ f) (return nothing)  ⊑⟨ x⊑y >>=-mono maybe f⊑g (run fail ■) ⟩■
  run y >>= maybe (MaybeT.run ∘ g) (return nothing)  ■

-- A variant of bind for sequences.

infix 5 _>>=ˢ_

_>>=ˢ_ : {A B : Type} →
         Increasing-sequence (Maybe A) →
         (A → Increasing-sequence (Maybe B)) →
         Increasing-sequence (Maybe B)
s >>=ˢ f =
    (λ n → MaybeT.run (wrap (s [ n ]) >>= λ x → wrap (f x [ n ])))
  , (λ n → increasing s n >>=ᵐ-mono λ x → increasing (f x) n)

------------------------------------------------------------------------
-- One interpreter

module Interpreter₁ where

  -- This interpreter is defined as the least upper bound of a
  -- sequence of increasingly defined interpreters.

  infix 10 _∙_

  mutual

    ⟦_⟧′ : ∀ {n} → Tm n → Env n → ℕ → M Value
    ⟦ con i ⟧′   ρ n = return (con i)
    ⟦ var x ⟧′   ρ n = return (ρ x)
    ⟦ ƛ t ⟧′     ρ n = return (ƛ t ρ)
    ⟦ t₁ · t₂ ⟧′ ρ n = ⟦ t₁ ⟧′ ρ n >>= λ v₁ →
                       ⟦ t₂ ⟧′ ρ n >>= λ v₂ →
                       (v₁ ∙ v₂) n

    _∙_ : Value → Value → ℕ → M Value
    (con i  ∙ v₂) n       = fail
    (ƛ t₁ ρ ∙ v₂) zero    = liftʳ never
    (ƛ t₁ ρ ∙ v₂) (suc n) = ⟦ t₁ ⟧′ (cons v₂ ρ) n

  mutual

    ⟦⟧′-increasing :
      ∀ {n} (t : Tm n) ρ n → ⟦ t ⟧′ ρ n ⊑M ⟦ t ⟧′ ρ (suc n)
    ⟦⟧′-increasing (con i)   ρ n = MaybeT.run (return (con i)) ■
    ⟦⟧′-increasing (var x)   ρ n = MaybeT.run (return (ρ x))   ■
    ⟦⟧′-increasing (ƛ t)     ρ n = MaybeT.run (return (ƛ t ρ)) ■
    ⟦⟧′-increasing (t₁ · t₂) ρ n =
      ⟦⟧′-increasing t₁ ρ n >>=ᵐ-mono λ v₁ →
      ⟦⟧′-increasing t₂ ρ n >>=ᵐ-mono λ v₂ →
      ∙-increasing v₁ v₂ n

    ∙-increasing : ∀ v₁ v₂ n → (v₁ ∙ v₂) n ⊑M (v₁ ∙ v₂) (suc n)
    ∙-increasing (con i)  v₂ n       = run fail ■
    ∙-increasing (ƛ t₁ ρ) v₂ (suc n) = ⟦⟧′-increasing t₁ (cons v₂ ρ) n
    ∙-increasing (ƛ t₁ ρ) v₂ zero    =
      never >>= return ∘ just      ≡⟨ never->>= ⟩⊑
      never                        ⊑⟨ never⊑ _ ⟩■
      run (⟦ t₁ ⟧′ (cons v₂ ρ) 0)  ■

  ⟦_⟧ˢ : ∀ {n} → Tm n → Env n → Increasing-sequence (Maybe Value)
  ⟦ t ⟧ˢ ρ = MaybeT.run ∘ ⟦ t ⟧′ ρ , ⟦⟧′-increasing t ρ

  ⟦_⟧ : ∀ {n} → Tm n → Env n → M Value
  run (⟦ t ⟧ ρ) = ⨆ (⟦ t ⟧ˢ ρ)

------------------------------------------------------------------------
-- Another interpreter

module Interpreter₂ where

  -- This interpreter is defined using a fixpoint combinator.

  M′ : Type → Type₁
  M′ = MaybeT (Partial (∃ λ n → Tm n × Env n) (λ _ → Maybe Value))

  infix 10 _∙_

  _∙_ : Value → Value → M′ Value
  con i  ∙ v₂ = fail
  ƛ t₁ ρ ∙ v₂ = wrap (rec (_ , t₁ , cons v₂ ρ))

  ⟦_⟧′ : ∀ {n} → Tm n → Env n → M′ Value
  ⟦ con i ⟧′   ρ = return (con i)
  ⟦ var x ⟧′   ρ = return (ρ x)
  ⟦ ƛ t ⟧′     ρ = return (ƛ t ρ)
  ⟦ t₁ · t₂ ⟧′ ρ = ⟦ t₁ ⟧′ ρ >>= λ v₁ →
                   ⟦ t₂ ⟧′ ρ >>= λ v₂ →
                   v₁ ∙ v₂

  ⟦_⟧ : ∀ {n} → Tm n → Env n → M Value
  run (⟦ t ⟧ ρ) =
    fixP {A = ∃ λ n → Tm n × Env n}
         (λ { (_ , t , ρ) → run (⟦ t ⟧′ ρ) }) (_ , t , ρ)

------------------------------------------------------------------------
-- The two interpreters are pointwise equal

interpreters-equal :
  ∀ {n} (t : Tm n) ρ →
  Interpreter₁.⟦ t ⟧ ρ ≡ Interpreter₂.⟦ t ⟧ ρ
interpreters-equal = λ t ρ →
                                                           $⟨ ⟦⟧-lemma t ρ ⟩
  (∀ n → run (Interpreter₁.⟦ t ⟧′ ρ n) ≡
         app→ step₂ (suc n) (_ , t , ρ))                   ↝⟨ cong ⨆ ∘ _↔_.to equality-characterisation-increasing ⟩

  ⨆ (Interpreter₁.⟦ t ⟧ˢ ρ) ≡
  ⨆ (tailˢ (at (fix→-sequence step₂) (_ , t , ρ)))         ↝⟨ flip trans (⨆tail≡⨆ _) ⟩

  ⨆ (Interpreter₁.⟦ t ⟧ˢ ρ) ≡
  ⨆ (at (fix→-sequence step₂) (_ , t , ρ))                 ↝⟨ id ⟩

  run (Interpreter₁.⟦ t ⟧ ρ) ≡ run (Interpreter₂.⟦ t ⟧ ρ)  ↝⟨ cong wrap ⟩□

  Interpreter₁.⟦ t ⟧ ρ ≡ Interpreter₂.⟦ t ⟧ ρ              □
  where
  open Partial
  open Trans-⊑

  step₂ : Trans-⊑ (∃ λ n → Tm n × Env n) (λ _ → Maybe Value)
  step₂ = transformer λ { (_ , t , ρ) → run (Interpreter₂.⟦ t ⟧′ ρ) }

  mutual

    ⟦⟧-lemma :
      ∀ {n} (t : Tm n) ρ n →
      run (Interpreter₁.⟦ t ⟧′ ρ n) ≡
      function (run (Interpreter₂.⟦ t ⟧′ ρ)) (app→ step₂ n)
    ⟦⟧-lemma (con i)   ρ n = refl
    ⟦⟧-lemma (var x)   ρ n = refl
    ⟦⟧-lemma (ƛ t)     ρ n = refl
    ⟦⟧-lemma (t₁ · t₂) ρ n =
      cong₂ _>>=_ (⟦⟧-lemma t₁ ρ n) $ ⟨ext⟩ $ flip maybe refl λ v₁ →
      cong₂ _>>=_ (⟦⟧-lemma t₂ ρ n) $ ⟨ext⟩ $ flip maybe refl λ v₂ →
      ∙-lemma v₁ v₂ n

    ∙-lemma :
      ∀ v₁ v₂ n →
      run ((v₁ Interpreter₁.∙ v₂) n) ≡
      function (run (v₁ Interpreter₂.∙ v₂)) (app→ step₂ n)
    ∙-lemma (con i)  v₂ n       = refl
    ∙-lemma (ƛ t₁ ρ) v₂ zero    = never >>= return ∘ just  ≡⟨ never->>= ⟩∎
                                  never                    ∎
    ∙-lemma (ƛ t₁ ρ) v₂ (suc n) = ⟦⟧-lemma t₁ (cons v₂ ρ) n

-- Let us use Interpreter₁ as the default interpreter.

open Interpreter₁ public

------------------------------------------------------------------------
-- An example

-- The semantics of Ω is the non-terminating computation never.

Ω-loops : run (⟦ Ω ⟧ nil) ≡ never
Ω-loops =
  antisymmetry (least-upper-bound _ _ lemma) (never⊑ _)
  where
  ω-nil = ƛ (var fzero · var fzero) nil

  reduce-twice :
    ∀ n → run (⟦ Ω ⟧′ nil n) ≡ run ((ω-nil ∙ ω-nil) n)
  reduce-twice n =
    run (⟦ Ω ⟧′ nil n)                            ≡⟨ now->>= ⟩
    run (⟦ ω ⟧′ nil n >>= λ v₂ → (ω-nil ∙ v₂) n)  ≡⟨ now->>= ⟩∎
    run ((ω-nil ∙ ω-nil) n)                       ∎

  lemma : ∀ n → run (⟦ Ω ⟧′ nil n) ⊑ never
  lemma zero    =
    run (⟦ Ω ⟧′ nil zero)       ≡⟨ reduce-twice zero ⟩⊑
    run ((ω-nil ∙ ω-nil) zero)  ≡⟨ never->>= ⟩⊑
    never                       ■
  lemma (suc n) =
    run (⟦ Ω ⟧′ nil (suc n))  ≡⟨ reduce-twice (suc n) ⟩⊑
    run (⟦ Ω ⟧′ nil n)        ⊑⟨ lemma n ⟩■
    never                     ■

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
import Issue953

g : Set₁
g = Issue953.f

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda


text:
--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems

open import Agda.Builtin.Equality
open import Data.Product
open import Data.Sum
open import Data.Vec using (Vec; fromList; length) renaming (lookup to get)
open import Data.Fin using (Fin)
open import Level
open import Relation.Unary using (_⊆_)

module is-lib.InfSys.Base {𝓁} where

  record MetaRule {𝓁c 𝓁p : Level} (U : Set 𝓁) : Set (𝓁 ⊔ suc 𝓁c ⊔ suc 𝓁p) where
    field
      Ctx : Set 𝓁c
      Pos : Ctx → Set 𝓁p
      prems : (c : Ctx) → Pos c → U
      conclu : Ctx → U

    addSideCond : ∀{𝓁'} → (U → Set 𝓁') → MetaRule {𝓁c ⊔ 𝓁'} U
    (addSideCond P) .Ctx = Σ[ c ∈ Ctx ] P (conclu c)
    (addSideCond P) .Pos (c , _) = Pos c
    (addSideCond P) .prems (c , _) p = prems c p
    (addSideCond P) .conclu (c , _) = conclu c

    RF[_] : ∀{𝓁'} → (U → Set 𝓁') → (U → Set _)
    RF[_] P u = Σ[ c ∈ Ctx ] (u ≡ conclu c × (∀ p → P (prems c p)))

    RClosed : ∀{𝓁'} → (U → Set 𝓁') → Set _
    RClosed P = ∀ c → (∀ p → P (prems c p)) → P (conclu c)

  {- Finitary Rule -}

  record FinMetaRule {𝓁c n} (U : Set 𝓁) : Set (𝓁 ⊔ suc 𝓁c) where
    field
      Ctx : Set 𝓁c
      comp : Ctx → Vec U n × U

    from : MetaRule {𝓁c} {zero} U
    from .MetaRule.Ctx = Ctx
    from .MetaRule.Pos = λ _ → Fin n
    from .MetaRule.prems c n = get (proj₁ (comp c)) n
    from .MetaRule.conclu c = proj₂ (comp c)

  open MetaRule

  record IS {𝓁c 𝓁p 𝓁n : Level} (U : Set 𝓁) : Set (𝓁 ⊔ suc 𝓁c ⊔ suc 𝓁p ⊔ suc 𝓁n) where
    field
      Names : Set 𝓁n
      rules : Names → MetaRule {𝓁c} {𝓁p} U

    ISF[_] : ∀{𝓁'} → (U → Set 𝓁') → (U → Set _)
    ISF[_] P u = Σ[ rn ∈ Names ] RF[ rules rn ] P u

    ISClosed : ∀{𝓁'} → (U → Set 𝓁') → Set _
    ISClosed P = ∀ rn → RClosed (rules rn) P

  open IS

  _∪_ : ∀{𝓁c 𝓁p 𝓁n 𝓁n'}{U : Set 𝓁} → IS {𝓁c} {𝓁p} {𝓁n} U → IS {_} {_} {𝓁n'} U → IS {_} {_} {𝓁n ⊔ 𝓁n'} U
  (is1 ∪ is2) .Names = (is1 .Names) ⊎ (is2 .Names)
  (is1 ∪ is2) .rules = [ is1 .rules , is2 .rules ]

  _⊓_ : ∀{𝓁c 𝓁p 𝓁n 𝓁'}{U : Set 𝓁} → IS {𝓁c} {𝓁p} {𝓁n} U → (U → Set 𝓁') → IS {𝓁c ⊔ 𝓁'} {_} {_} U
  (is ⊓ P) .Names = is .Names
  (is ⊓ P) .rules rn = addSideCond (is .rules rn) P

  {- Properties -}

  -- closed implies prefix
  closed⇒prefix : ∀{𝓁c 𝓁p}{U : Set 𝓁} → (m : MetaRule {𝓁c} {𝓁p} U) → ∀{𝓁'}{P : U → Set 𝓁'} → RClosed m {𝓁'} P → RF[ m ] P ⊆ P
  closed⇒prefix _ cl (_ , refl , pr) = cl _ pr

  -- prefix implies closed
  prefix⇒closed : ∀{𝓁c 𝓁p}{U : Set 𝓁} → (m : MetaRule {𝓁c} {𝓁p} U) → ∀{𝓁'}{P : U → Set 𝓁'} → (RF[ m ] P ⊆ P) → RClosed m {𝓁'} P
  prefix⇒closed _ prf c pr = prf (c , refl , pr)

max_stars_repo_name: boystrange/FairSubtypingAgda

max_issues_repo_name: boystrange/FairSubtypingAgda

max_forks_repo_name: boystrange/FairSubtypingAgda