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

module Categories.Category.Instance.Properties.Setoids.Extensive where

open import Level
open import Data.Product using (∃; Σ; proj₁; proj₂; _,_; _×_)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
open import Data.Sum.Relation.Binary.Pointwise using (inj₁; inj₂; _⊎ₛ_; drop-inj₁; drop-inj₂)
open import Data.Unit.Polymorphic using (tt)
open import Function.Equality using (Π; _⟶_; _⇨_; _∘_)
open import Relation.Binary using (Setoid)
import  Relation.Binary.Reasoning.Setoid as SetoidR

open import Categories.Category using (Category; _[_,_])
open import Categories.Category.Instance.Setoids using (Setoids)
open import Categories.Category.Extensive using (Extensive)
open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Diagram.Pullback using (Pullback)
open import Categories.Category.Instance.Properties.Setoids.Limits.Canonical using (pullback; FiberProduct)
open import Categories.Category.Monoidal.Instance.Setoids using (Setoids-Cocartesian)

open Π
open Pullback

-- Note the Setoids is extensive if the two levels coincide.  Whether it happens more generally
-- is unknown at this point.

Setoids-Extensive : (ℓ : Level) → Extensive (Setoids ℓ ℓ)
Setoids-Extensive ℓ = record
   { cocartesian = record { initial = initial ; coproducts = coproducts }
   ; pullback₁ = λ f → pullback ℓ ℓ f i₁
   ; pullback₂ = λ f → pullback ℓ ℓ f i₂
   ; pullback-of-cp-is-cp = λ f → record
        { [_,_] = λ g h → copair f g h
        ; inject₁ = λ {X g h z} eq →
             trans (isEquivalence X) (copair-inject₁ f g h z) (cong g eq)
        ; inject₂ = λ {X g h z} eq →
             trans (isEquivalence X) (copair-inject₂ f g h z) (cong h eq)
        ; unique = λ {X u g h} feq₁ feq₂ {z} eq →
             trans (isEquivalence X) (copair-unique f g h u z (λ {z} → feq₁ {z}) (λ {z} → feq₂ {z})) (cong u eq)
        }
   ; pullback₁-is-mono = λ _ _ eq x≈y → drop-inj₁ (eq x≈y)
   ; pullback₂-is-mono = λ _ _ eq x≈y → drop-inj₂ (eq x≈y)
   ; disjoint = λ {A B} → record
        { commute = λ { {()} _}
        ; universal = λ {C f g} eq → record
           { _⟨$⟩_ = λ z → conflict A B (eq {x = z} (refl (isEquivalence C)))
           ; cong = λ z → tt
           }
        ; unique = λ _ _ _ → tt
        ; p₁∘universal≈h₁ = λ {_ _ _ eq} x≈y → conflict A B (eq x≈y)
        ; p₂∘universal≈h₂ = λ {_ _ _ eq} x≈y → conflict A B (eq x≈y)
        }
   }
     where
       open Cocartesian (Setoids-Cocartesian {ℓ} {ℓ})
       open Relation.Binary.IsEquivalence
       open Setoid renaming (_≈_ to [_][_≈_]; Carrier to ∣_∣) using (isEquivalence)

       -- must be in the standard library. Maybe it is?
       conflict : ∀ {ℓ ℓ' ℓ''} (X Y : Setoid ℓ ℓ') {Z : Set ℓ''}
         {x : ∣ X ∣} {y : ∣ Y ∣} → [ X ⊎ₛ Y ][ inj₁ x ≈ inj₂ y ] → Z
       conflict X Y ()

       module Diagram {A B C X : Setoid ℓ ℓ} (f : C ⟶ A ⊎ₛ B)
         (g : P (pullback ℓ ℓ f i₁) ⟶ X) (h : P (pullback ℓ ℓ f i₂) ⟶ X) where

         private
           module A = Setoid A
           module B = Setoid B
           module C = Setoid C
           module X = Setoid X
           A⊎B = A ⊎ₛ B
           module A⊎B = Setoid (A ⊎ₛ B)

           A′ = P (pullback ℓ ℓ f i₁)
           B′ = P (pullback ℓ ℓ f i₂)
           A⊎B′ = A′ ⊎ₛ B′
           module A⊎B′ = Setoid A⊎B′
           open SetoidR A⊎B′

         _⊎⟶_ : {o₁ o₂ o₃ ℓ₁ ℓ₂ ℓ₃ : Level} {X : Setoid o₁ ℓ₁} {Y : Setoid o₂ ℓ₂} {Z : Setoid o₃ ℓ₃} →
           (X ⟶ Z) → (Y ⟶ Z) → (X ⊎ₛ Y) ⟶ Z
         f₁ ⊎⟶ f₂ = record
           { _⟨$⟩_ = Sum.[ f₁ ⟨$⟩_ , f₂ ⟨$⟩_ ]
           ; cong = λ { (inj₁ x) → cong f₁ x ; (inj₂ x) → cong f₂ x}
           }

         to-⊎ₛ : (z : ∣ C ∣) → (w : ∣ A ⊎ₛ B ∣) → (eq : [ A⊎B ][ f ⟨$⟩ z ≈ w ]) → ∣ A′ ⊎ₛ B′ ∣
         to-⊎ₛ z (inj₁ x) eq = inj₁ (record { elem₁ = z ; elem₂ = x ; commute = eq })
         to-⊎ₛ z (inj₂ y) eq = inj₂ (record { elem₁ = z ; elem₂ = y ; commute = eq })

         to-⊎ₛ-cong : {z : ∣ C ∣} {w w′ : ∣ A ⊎ₛ B ∣ } → [ A⊎B ][ w ≈ w′ ] →
           {eq : [ A⊎B ][ f ⟨$⟩ z ≈ w ]} → {eq′ : [ A⊎B ][ f ⟨$⟩ z ≈ w′ ]} → [ A⊎B′ ][ to-⊎ₛ z w eq ≈ to-⊎ₛ z w′ eq′ ]
         to-⊎ₛ-cong (inj₁ x) = inj₁ (C.refl , x)
         to-⊎ₛ-cong (inj₂ x) = inj₂ (C.refl , x)

         f⟨$⟩→ : (z : ∣ C ∣) → ∣ A′ ⊎ₛ B′ ∣
         f⟨$⟩→ z = to-⊎ₛ z (f ⟨$⟩ z) A⊎B.refl

         f⟨$⟩-cong′ : {z z′ : ∣ C ∣} → (z≈z′ : [ C ][ z ≈ z′ ]) → (w w′ : ∣ A ⊎ₛ B ∣) →
           [ A⊎B ][ f ⟨$⟩ z ≈ w ] → [ A⊎B ][ f ⟨$⟩ z′ ≈ w′ ] → [ A′ ⊎ₛ B′ ][ f⟨$⟩→ z ≈ f⟨$⟩→ z′ ]
         f⟨$⟩-cong′ {z} {z′} z≈z′ (inj₁ x) (inj₁ x₁) fz≈w fz′≈w′ = begin
           f⟨$⟩→ z                       ≈⟨ A⊎B′.refl ⟩
           to-⊎ₛ z (f ⟨$⟩ z) A⊎B.refl   ≈⟨ to-⊎ₛ-cong fz≈w ⟩
           to-⊎ₛ z (inj₁ x) fz≈w       ≈⟨ inj₁ (z≈z′ , (drop-inj₁ (A⊎B.trans (A⊎B.sym fz≈w) (A⊎B.trans (cong f z≈z′) fz′≈w′)))) ⟩
           to-⊎ₛ z′ (inj₁ x₁) fz′≈w′   ≈⟨ to-⊎ₛ-cong (A⊎B.sym fz′≈w′) ⟩
           to-⊎ₛ z′ (f ⟨$⟩ z′) A⊎B.refl ≈⟨ A⊎B′.refl ⟩
           f⟨$⟩→ z′ ∎
         f⟨$⟩-cong′ z≈z′ (inj₁ x) (inj₂ y) fz≈w fz′≈w′ = conflict A B (A⊎B.trans (A⊎B.sym fz≈w) (A⊎B.trans (cong f z≈z′) fz′≈w′))
         f⟨$⟩-cong′ z≈z′ (inj₂ y) (inj₁ x) fz≈w fz′≈w′ = conflict A B (A⊎B.trans (A⊎B.sym fz′≈w′) (A⊎B.trans (cong f (C.sym z≈z′)) fz≈w))
         f⟨$⟩-cong′ {z} {z′} z≈z′ (inj₂ y) (inj₂ y₁) fz≈w fz′≈w′ = begin
           to-⊎ₛ z (f ⟨$⟩ z) A⊎B.refl   ≈⟨ to-⊎ₛ-cong fz≈w ⟩
           to-⊎ₛ z (inj₂ y) fz≈w       ≈⟨ inj₂ (z≈z′ , (drop-inj₂ (A⊎B.trans (A⊎B.sym fz≈w) (A⊎B.trans (cong f z≈z′) fz′≈w′)))) ⟩
           to-⊎ₛ z′ (inj₂ y₁) fz′≈w′   ≈⟨ to-⊎ₛ-cong (A⊎B.sym fz′≈w′) ⟩
           to-⊎ₛ z′ (f ⟨$⟩ z′) A⊎B.refl ∎

         f⟨$⟩-cong : {i j : ∣ C ∣} → i C.≈ j → [ A′ ⊎ₛ B′ ][ f⟨$⟩→ i ≈ f⟨$⟩→ j ]
         f⟨$⟩-cong {i} {j} i≈j = f⟨$⟩-cong′ i≈j (f ⟨$⟩ i) (f ⟨$⟩ j) A⊎B.refl A⊎B.refl

         f⟨$⟩ : C ⟶ A′ ⊎ₛ B′
         f⟨$⟩ = record { _⟨$⟩_ = f⟨$⟩→ ; cong = f⟨$⟩-cong }

         -- copairing of g : A′ → X and h : B′ → X, resulting in C → X
         copair : C ⟶ X
         copair = (g ⊎⟶ h) ∘ f⟨$⟩

         copair-inject₁ : (z : FiberProduct f i₁) → [ X ][ copair ⟨$⟩ (FiberProduct.elem₁ z) ≈ g ⟨$⟩ z ]
         copair-inject₁ record { elem₁ = z ; elem₂ = x ; commute = eq } = cong (g ⊎⟶ h) (to-⊎ₛ-cong eq)

         copair-inject₂ : (z : FiberProduct f i₂) → [ X ][ copair ⟨$⟩ (FiberProduct.elem₁ z) ≈ h ⟨$⟩ z ]
         copair-inject₂ record { elem₁ = z ; elem₂ = y ; commute = eq } = cong (g ⊎⟶ h) (to-⊎ₛ-cong eq)

         copair-unique′ : (u : C ⟶ X) (z : ∣ C ∣) →
           [ A′ ⇨ X ][ u ∘ p₁ (pullback ℓ ℓ f i₁) ≈ g ] →
           [ B′ ⇨ X ][ u ∘ p₁ (pullback ℓ ℓ f i₂) ≈ h ] →
           (w : ∣ A⊎B ∣) → [ A⊎B ][ f ⟨$⟩ z ≈ w ] →
           [ X ][ copair ⟨$⟩ z ≈ u ⟨$⟩ z ]
         copair-unique′ u z feq₁ feq₂ (inj₁ x) fz≈w = XR.begin
           copair ⟨$⟩ z                                XR.≈⟨ X.refl ⟩
           g ⊎⟶ h ⟨$⟩ (to-⊎ₛ z (f ⟨$⟩ z) A⊎B.refl)     XR.≈⟨ cong (g ⊎⟶ h) (to-⊎ₛ-cong fz≈w) ⟩
           g ⊎⟶ h ⟨$⟩ (to-⊎ₛ z (inj₁ x) fz≈w)         XR.≈⟨ X.refl ⟩
           g ⟨$⟩ fb                                    XR.≈⟨ X.sym (feq₁ {x = fb} (C.refl , A.refl)) ⟩
           u ⟨$⟩ z                                     XR.∎

           where
             module XR = SetoidR X
             fb = record {elem₁ = z ; elem₂ = x; commute = fz≈w }
         copair-unique′ u z feq₁ feq₂ (inj₂ y) fz≈w = XR.begin
           copair ⟨$⟩ z                                XR.≈⟨ X.refl ⟩
           g ⊎⟶ h ⟨$⟩ (to-⊎ₛ z (f ⟨$⟩ z) A⊎B.refl)     XR.≈⟨ cong (g ⊎⟶ h) (to-⊎ₛ-cong fz≈w) ⟩
           g ⊎⟶ h ⟨$⟩ (to-⊎ₛ z (inj₂ y) fz≈w)         XR.≈⟨ X.refl ⟩
           h ⟨$⟩ fb                                    XR.≈⟨ X.sym (feq₂ {x = fb} {y = fb} (C.refl , B.refl)) ⟩
           u ⟨$⟩ z                                     XR.∎
           where
             module XR = SetoidR X
             fb = record {elem₁ = z ; elem₂ = y; commute = fz≈w }

         copair-unique : (u : C ⟶ X) (z : ∣ C ∣) →
           [ A′ ⇨ X ][ u ∘ p₁ (pullback ℓ ℓ f i₁) ≈ g ] →
           [ B′ ⇨ X ][ u ∘ p₁ (pullback ℓ ℓ f i₂) ≈ h ] →
           [ X ][ copair ⟨$⟩ z ≈ u ⟨$⟩ z ]
         copair-unique u z feq₁ feq₂ = copair-unique′ u z (λ {x} {y} → feq₁ {x} {y}) (λ {x} {y} → feq₂ {x} {y}) (f ⟨$⟩ z) A⊎B.refl

       open Diagram

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
module A4 where

-- open import Data.Nat
open import Data.Empty
open import Data.Unit
open import Data.Sum
open import Data.Product

open import Groupoid

------------------------------------------------------------------------------
-- Level 0:
-- types are collections of points
-- equivalences are between points

module Pi0 where

  infixr 10 _◎_
  infixr 30 _⟷_

  -- types
  data U : Set where
    ZERO  : U
    ONE   : U
    PLUS  : U → U → U
    TIMES : U → U → U

  -- values
  ⟦_⟧ : U → Set
  ⟦ ZERO ⟧        = ⊥
  ⟦ ONE ⟧         = ⊤
  ⟦ PLUS t₁ t₂ ⟧  = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
  ⟦ TIMES t₁ t₂ ⟧ = ⟦ t₁ ⟧ × ⟦ t₂ ⟧

  -- Examples

  BOOL : U
  BOOL = PLUS ONE ONE

  BOOL² : U
  BOOL² = TIMES BOOL BOOL

  TRUE : ⟦ BOOL ⟧
  TRUE = inj₁ tt

  FALSE : ⟦ BOOL ⟧
  FALSE = inj₂ tt

  -- combinators
  data _⟷_ : U → U → Set where
    unite₊  : {t : U} → PLUS ZERO t ⟷ t
    uniti₊  : {t : U} → t ⟷ PLUS ZERO t
    swap₊   : {t₁ t₂ : U} → PLUS t₁ t₂ ⟷ PLUS t₂ t₁
    assocl₊ : {t₁ t₂ t₃ : U} → PLUS t₁ (PLUS t₂ t₃) ⟷ PLUS (PLUS t₁ t₂) t₃
    assocr₊ : {t₁ t₂ t₃ : U} → PLUS (PLUS t₁ t₂) t₃ ⟷ PLUS t₁ (PLUS t₂ t₃)
    unite⋆  : {t : U} → TIMES ONE t ⟷ t
    uniti⋆  : {t : U} → t ⟷ TIMES ONE t
    swap⋆   : {t₁ t₂ : U} → TIMES t₁ t₂ ⟷ TIMES t₂ t₁
    assocl⋆ : {t₁ t₂ t₃ : U} → TIMES t₁ (TIMES t₂ t₃) ⟷ TIMES (TIMES t₁ t₂) t₃
    assocr⋆ : {t₁ t₂ t₃ : U} → TIMES (TIMES t₁ t₂) t₃ ⟷ TIMES t₁ (TIMES t₂ t₃)
    distz   : {t : U} → TIMES ZERO t ⟷ ZERO
    factorz : {t : U} → ZERO ⟷ TIMES ZERO t
    dist    : {t₁ t₂ t₃ : U} →
              TIMES (PLUS t₁ t₂) t₃ ⟷ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃)
    factor  : {t₁ t₂ t₃ : U} →
              PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) ⟷ TIMES (PLUS t₁ t₂) t₃
    id⟷    : {t : U} → t ⟷ t
    sym⟷   : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
    _◎_     : {t₁ t₂ t₃ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
    _⊕_     : {t₁ t₂ t₃ t₄ : U} →
              (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (PLUS t₁ t₂ ⟷ PLUS t₃ t₄)
    _⊗_     : {t₁ t₂ t₃ t₄ : U} →
              (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (TIMES t₁ t₂ ⟷ TIMES t₃ t₄)

  -- Examples

  COND : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (t₁ ⟷ t₂) →
         ((TIMES BOOL t₁) ⟷ (TIMES BOOL t₂))
  COND f g = dist ◎ ((id⟷ ⊗ f) ⊕ (id⟷ ⊗ g)) ◎ factor

  CONTROLLED : {t : U} → (t ⟷ t) → ((TIMES BOOL t) ⟷ (TIMES BOOL t))
  CONTROLLED f = COND f id⟷

  CNOT : BOOL² ⟷ BOOL²
  CNOT = CONTROLLED swap₊

------------------------------------------------------------------------------
-- Level 1
-- types are collections of paths (where paths are equivalences between points)
-- equivalences are between paths

module Pi1 where
  -- types
  data U : Set where
{-
    LIFT : Pi0.U → U
    PLUS : U → U → U
    TIMES : U → U → U
-}
    EQUIV : {t₁ t₂ : Pi0.U} → (t₁ Pi0.⟷ t₂) → Pi0.⟦ t₁ ⟧ → Pi0.⟦ t₂ ⟧ → U

  -- extractor, dependently typed.
  srcU : U → Σ Pi0.U Pi0.⟦_⟧
  srcU (EQUIV {t₁} {t₂} c x y) = t₁ , x

  -- values

  data Path⊤ : Set where
    pathtt : Path⊤

  data Path⊎ (A B : Set) : Set where
    pathLeft  : A → Path⊎ A B
    pathRight : B → Path⊎ A B

  data Path× (A B : Set) : Set where
    pathPair : A → B → Path× A B

  data Unite₊ {t : Pi0.U} : Pi0.⟦ Pi0.PLUS Pi0.ZERO t ⟧ → Pi0.⟦ t ⟧ → Set where
    pathUnite₊ : (v : Pi0.⟦ t ⟧) → Unite₊ (inj₂ v) v

  data Uniti₊ {t : Pi0.U} : Pi0.⟦ t ⟧ → Pi0.⟦ Pi0.PLUS Pi0.ZERO t ⟧ → Set where
    pathUniti₊ : (v : Pi0.⟦ t ⟧) → Uniti₊ v (inj₂ v)

  data Swap₊ {t₁ t₂ : Pi0.U} :
    Pi0.⟦ Pi0.PLUS t₁ t₂ ⟧ → Pi0.⟦ Pi0.PLUS t₂ t₁ ⟧ → Set where
    path1Swap₊ : (v₁ : Pi0.⟦ t₁ ⟧) → Swap₊ (inj₁ v₁) (inj₂ v₁)
    path2Swap₊ : (v₂ : Pi0.⟦ t₂ ⟧) → Swap₊ (inj₂ v₂) (inj₁ v₂)

  data Assocl₊ {t₁ t₂ t₃ : Pi0.U} :
    Pi0.⟦ Pi0.PLUS t₁ (Pi0.PLUS t₂ t₃) ⟧ →
    Pi0.⟦ Pi0.PLUS (Pi0.PLUS t₁ t₂) t₃ ⟧ → Set where
    path1Assocl₊ : (v₁ : Pi0.⟦ t₁ ⟧) → Assocl₊ (inj₁ v₁) (inj₁ (inj₁ v₁))
    path2Assocl₊ : (v₂ : Pi0.⟦ t₂ ⟧) → Assocl₊ (inj₂ (inj₁ v₂)) (inj₁ (inj₂ v₂))
    path3Assocl₊ : (v₃ : Pi0.⟦ t₃ ⟧) → Assocl₊ (inj₂ (inj₂ v₃)) (inj₂ v₃)

  data Assocr₊ {t₁ t₂ t₃ : Pi0.U} :
    Pi0.⟦ Pi0.PLUS (Pi0.PLUS t₁ t₂) t₃ ⟧ →
    Pi0.⟦ Pi0.PLUS t₁ (Pi0.PLUS t₂ t₃) ⟧ → Set where
    path1Assocr₊ : (v₁ : Pi0.⟦ t₁ ⟧) → Assocr₊ (inj₁ (inj₁ v₁)) (inj₁ v₁)
    path2Assocr₊ : (v₂ : Pi0.⟦ t₂ ⟧) →
      Assocr₊ (inj₁ (inj₂ v₂)) (inj₂ (inj₁ v₂))
    path3Assocr₊ : (v₃ : Pi0.⟦ t₃ ⟧) → Assocr₊ (inj₂ v₃) (inj₂ (inj₂ v₃))

  data Unite⋆ {t : Pi0.U} : Pi0.⟦ Pi0.TIMES Pi0.ONE t ⟧ → Pi0.⟦ t ⟧ → Set where
    pathUnite⋆ : (v : Pi0.⟦ t ⟧) → Unite⋆ (tt , v) v

  data Uniti⋆ {t : Pi0.U} : Pi0.⟦ t ⟧ → Pi0.⟦ Pi0.TIMES Pi0.ONE t ⟧ → Set where
    pathUniti⋆ : (v : Pi0.⟦ t ⟧) → Uniti⋆ v (tt , v)

  data Swap⋆ {t₁ t₂ : Pi0.U} :
    Pi0.⟦ Pi0.TIMES t₁ t₂ ⟧ → Pi0.⟦ Pi0.TIMES t₂ t₁ ⟧ → Set where
    pathSwap⋆ :
      (v₁ : Pi0.⟦ t₁ ⟧) → (v₂ : Pi0.⟦ t₂ ⟧) → Swap⋆ (v₁ , v₂) (v₂ , v₁)

  data Assocl⋆ {t₁ t₂ t₃ : Pi0.U} :
    Pi0.⟦ Pi0.TIMES t₁ (Pi0.TIMES t₂ t₃) ⟧ →
    Pi0.⟦ Pi0.TIMES (Pi0.TIMES t₁ t₂) t₃ ⟧ → Set where
    pathAssocl⋆ :
      (v₁ : Pi0.⟦ t₁ ⟧) → (v₂ : Pi0.⟦ t₂ ⟧) → (v₃ : Pi0.⟦ t₃ ⟧) →
      Assocl⋆ (v₁ , (v₂ , v₃)) ((v₁ , v₂) , v₃)

  data Assocr⋆ {t₁ t₂ t₃ : Pi0.U} :
    Pi0.⟦ Pi0.TIMES (Pi0.TIMES t₁ t₂) t₃ ⟧ →
    Pi0.⟦ Pi0.TIMES t₁ (Pi0.TIMES t₂ t₃) ⟧ → Set where
    pathAssocr⋆ :
      (v₁ : Pi0.⟦ t₁ ⟧) → (v₂ : Pi0.⟦ t₂ ⟧) → (v₃ : Pi0.⟦ t₃ ⟧) →
      Assocr⋆ ((v₁ , v₂) , v₃) (v₁ , (v₂ , v₃))

  data Dist {t₁ t₂ t₃ : Pi0.U} :
    Pi0.⟦ Pi0.TIMES (Pi0.PLUS t₁ t₂) t₃ ⟧ →
    Pi0.⟦ Pi0.PLUS (Pi0.TIMES t₁ t₃) (Pi0.TIMES t₂ t₃) ⟧ → Set where
    path1Dist :
      (v₁ : Pi0.⟦ t₁ ⟧) → (v₃ : Pi0.⟦ t₃ ⟧) →
      Dist (inj₁ v₁ , v₃) (inj₁ (v₁ , v₃))
    path2Dist :
      (v₂ : Pi0.⟦ t₂ ⟧) → (v₃ : Pi0.⟦ t₃ ⟧) →
      Dist (inj₂ v₂ , v₃) (inj₂ (v₂ , v₃))

  data Factor {t₁ t₂ t₃ : Pi0.U} :
    Pi0.⟦ Pi0.PLUS (Pi0.TIMES t₁ t₃) (Pi0.TIMES t₂ t₃) ⟧ →
    Pi0.⟦ Pi0.TIMES (Pi0.PLUS t₁ t₂) t₃ ⟧ → Set where
    path1Factor :
      (v₁ : Pi0.⟦ t₁ ⟧) → (v₃ : Pi0.⟦ t₃ ⟧) →
      Factor (inj₁ (v₁ , v₃)) (inj₁ v₁ , v₃)
    path2Factor :
      (v₂ : Pi0.⟦ t₂ ⟧) → (v₃ : Pi0.⟦ t₃ ⟧) →
      Factor (inj₂ (v₂ , v₃)) (inj₂ v₂ , v₃)

  data Id⟷ {t : Pi0.U} : Pi0.⟦ t ⟧ → Pi0.⟦ t ⟧ → Set where
    pathId⟷ : (v : Pi0.⟦ t ⟧) → Id⟷ v v

  data PathRev (A : Set) : Set where
    pathRev : A → PathRev A

  record PathTrans (A : Set) (B C : A → Set) : Set where
    constructor pathTrans
    field
      anchor : A
      pre    : B anchor
      post   : C anchor

  mutual
    ⟦_⟧ : U → Set
{-
    ⟦ LIFT u ⟧             = Pi0.⟦ u ⟧
    ⟦ ZERO ⟧          = ⊥
    ⟦ ONE ⟧           = Path⊤
    ⟦ PLUS t₁ t₂ ⟧    = Path⊎ ⟦ t₁ ⟧ ⟦ t₂ ⟧
    ⟦ TIMES t₁ t₂ ⟧   = Path× ⟦ t₁ ⟧ ⟦ t₂ ⟧
-}
    ⟦ EQUIV c v₁ v₂ ⟧ = Paths c v₁ v₂ -- space of paths from v₁ to v₂ using c

    Paths : {t₁ t₂ : Pi0.U} → (t₁ Pi0.⟷ t₂) → Pi0.⟦ t₁ ⟧ → Pi0.⟦ t₂ ⟧ → Set
    Paths Pi0.unite₊ (inj₁ ()) _
    Paths Pi0.unite₊ (inj₂ v) v' = Unite₊ (inj₂ v) v'
    Paths Pi0.uniti₊ v (inj₁ ())
    Paths Pi0.uniti₊ v (inj₂ v') = Uniti₊ v (inj₂ v')
    Paths Pi0.swap₊ v v' = Swap₊ v v'
    Paths Pi0.assocl₊ v v' = Assocl₊ v v'
    Paths Pi0.assocr₊ v v' = Assocr₊ v v'
    Paths Pi0.unite⋆ v v' = Unite⋆ v v'
    Paths Pi0.uniti⋆ v v' = Uniti⋆ v v'
    Paths Pi0.swap⋆ v v' = Swap⋆ v v'
    Paths Pi0.assocl⋆ v v' = Assocl⋆ v v'
    Paths Pi0.assocr⋆ v v' = Assocr⋆ v v'
    Paths Pi0.distz v ()
    Paths Pi0.factorz () v'
    Paths Pi0.dist v v' = Dist v v'
    Paths Pi0.factor v v' = Factor v v'
    Paths Pi0.id⟷ v v' = Id⟷ v v'
    Paths (Pi0.sym⟷ c) v v' = PathRev (Paths c v' v)
    Paths (Pi0._◎_ {t₂ = t₂} c₁ c₂) v₁ v₃ =
      PathTrans Pi0.⟦ t₂ ⟧ (λ v₂ → Paths c₁ v₁ v₂) (λ v₂ → Paths c₂ v₂ v₃)
      -- Σ[ v₂ ∈ Pi0.⟦ t₂ ⟧ ] (Paths c₁ v₁ v₂ × Paths c₂ v₂ v₃)
    Paths (c₁ Pi0.⊕ c₂) (inj₁ v₁) (inj₁ v₁') = Path⊎ (Paths c₁ v₁ v₁') ⊥
    Paths (c₁ Pi0.⊕ c₂) (inj₁ v₁) (inj₂ v₂') = ⊥
    Paths (c₁ Pi0.⊕ c₂) (inj₂ v₂) (inj₁ v₁') = ⊥
    Paths (c₁ Pi0.⊕ c₂) (inj₂ v₂) (inj₂ v₂') = Path⊎ ⊥ (Paths c₂ v₂ v₂')
    Paths (c₁ Pi0.⊗ c₂) (v₁ , v₂) (v₁' , v₂') =
      Path× (Paths c₁ v₁ v₁') (Paths c₂ v₂ v₂')

  -- Examples
  -- A few paths between FALSE and FALSE

  p₁ : ⟦ EQUIV Pi0.id⟷ Pi0.FALSE Pi0.FALSE ⟧
  p₁ = pathId⟷ Pi0.FALSE

  p₂ : ⟦ EQUIV (Pi0.id⟷ Pi0.◎ Pi0.id⟷) Pi0.FALSE Pi0.FALSE ⟧
  p₂ = pathTrans Pi0.FALSE p₁ p₁

  p₃ : ⟦ EQUIV (Pi0.swap₊ Pi0.◎ Pi0.swap₊) Pi0.FALSE Pi0.FALSE ⟧
  p₃ = pathTrans Pi0.TRUE (path2Swap₊ tt) (path1Swap₊ tt)

  p₄ : ⟦ EQUIV (Pi0.id⟷ Pi0.⊕ Pi0.id⟷) Pi0.FALSE Pi0.FALSE ⟧
  p₄ = pathRight (pathId⟷ tt)

  -- A few paths between (TRUE,TRUE) and (TRUE,TRUE)

  p₅ : ⟦ EQUIV Pi0.id⟷ (Pi0.TRUE , Pi0.TRUE) (Pi0.TRUE , Pi0.TRUE) ⟧
  p₅ = pathId⟷ (Pi0.TRUE , Pi0.TRUE)

  p₆ : ⟦ EQUIV (Pi0.id⟷ Pi0.⊗ Pi0.id⟷)
        (Pi0.TRUE , Pi0.TRUE) (Pi0.TRUE , Pi0.TRUE) ⟧
  p₆ = pathPair (pathId⟷ Pi0.TRUE) (pathId⟷ Pi0.TRUE)

  -- A few paths between (TRUE,FALSE) and (TRUE,TRUE)

  p₇ : ⟦ EQUIV (Pi0.id⟷ Pi0.⊗ Pi0.swap₊)
        (Pi0.TRUE , Pi0.FALSE) (Pi0.TRUE , Pi0.TRUE) ⟧
  p₇ = pathPair (pathId⟷ Pi0.TRUE) (path2Swap₊ tt)

  p₇' : ⟦ EQUIV (Pi0.swap₊ Pi0.⊗ Pi0.id⟷)
        (Pi0.FALSE , Pi0.TRUE) (Pi0.TRUE , Pi0.TRUE) ⟧
  p₇' = pathPair (path2Swap₊ tt) (pathId⟷ Pi0.TRUE)

  p₈ : ⟦ EQUIV Pi0.CNOT (Pi0.TRUE , Pi0.FALSE) (Pi0.TRUE , Pi0.TRUE) ⟧
  p₈ = pathTrans (inj₁ (tt , Pi0.FALSE))
         (path1Dist tt Pi0.FALSE)
         (pathTrans (inj₁ (tt , Pi0.TRUE))
            (pathLeft (pathPair (pathId⟷ tt) (path2Swap₊ tt)))
            (path1Factor tt Pi0.TRUE))

  -- Examples using sum and products of paths
{-
  q₀ : ⟦ TIMES (LIFT Pi0.ONE) (EQUIV Pi0.id⟷ Pi0.FALSE Pi0.FALSE) ⟧
  q₀ = pathPair pathtt p₁

  q₁ : ⟦ (LIFT Pi0.PLUS) (EQUIV Pi0.id⟷ Pi0.FALSE Pi0.FALSE)
              (EQUIV (Pi0.id⟷ Pi0.⊗ Pi0.swap₊)
                     (Pi0.TRUE , Pi0.FALSE) (Pi0.TRUE , Pi0.TRUE)) ⟧
  q₁ = pathRight p₇

  q₂ : ⟦ (LIFT Pi0.PLUS) (EQUIV Pi0.id⟷ Pi0.FALSE Pi0.FALSE) (LIFT Pi0.ZERO) ⟧
  q₂ = pathLeft p₁
-}
  -- combinators
  -- the usual semiring combinators to reason about 0, 1, +, and *, and
  -- the groupoid combinators to reason about id, rev, and trans
  data _⟷_ : U → U → Set where
{-
    unite₊  : {t : U} → PLUS ZERO t ⟷ t
    uniti₊  : {t : U} → t ⟷ PLUS ZERO t
    swap₊   : {t₁ t₂ : U} → PLUS t₁ t₂ ⟷ PLUS t₂ t₁
    assocl₊ : {t₁ t₂ t₃ : U} → PLUS t₁ (PLUS t₂ t₃) ⟷ PLUS (PLUS t₁ t₂) t₃
    assocr₊ : {t₁ t₂ t₃ : U} → PLUS (PLUS t₁ t₂) t₃ ⟷ PLUS t₁ (PLUS t₂ t₃)
    unite⋆  : {t : U} → TIMES ONE t ⟷ t
    uniti⋆  : {t : U} → t ⟷ TIMES ONE t
    swap⋆   : {t₁ t₂ : U} → TIMES t₁ t₂ ⟷ TIMES t₂ t₁
    assocl⋆ : {t₁ t₂ t₃ : U} → TIMES t₁ (TIMES t₂ t₃) ⟷ TIMES (TIMES t₁ t₂) t₃
    assocr⋆ : {t₁ t₂ t₃ : U} → TIMES (TIMES t₁ t₂) t₃ ⟷ TIMES t₁ (TIMES t₂ t₃)
    distz   : {t : U} → TIMES ZERO t ⟷ ZERO
    factorz : {t : U} → ZERO ⟷ TIMES ZERO t
    dist    : {t₁ t₂ t₃ : U} →
              TIMES (PLUS t₁ t₂) t₃ ⟷ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃)
    factor  : {t₁ t₂ t₃ : U} →
              PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) ⟷ TIMES (PLUS t₁ t₂) t₃
-}
    id⟷    : {t₁ t₂ : Pi0.U} {c : t₁ Pi0.⟷ t₂} {v₀ : Pi0.⟦ t₁ ⟧} {v₁ : Pi0.⟦ t₂ ⟧} → EQUIV c v₀ v₁ ⟷ EQUIV c v₀ v₁
    sym⟷  : {t₁ t₂ : Pi0.U} {c d : t₁ Pi0.⟷ t₂} {v₀ : Pi0.⟦ t₁ ⟧} {v₁ : Pi0.⟦ t₂ ⟧} → EQUIV c v₀ v₁ ⟷ EQUIV d v₀ v₁ → EQUIV d v₀ v₁ ⟷ EQUIV c v₀ v₁
    _◎_     :  {t₁ t₂ : Pi0.U} {c d e : t₁ Pi0.⟷ t₂} {v₀ : Pi0.⟦ t₁ ⟧} {v₁ : Pi0.⟦ t₂ ⟧} → EQUIV c v₀ v₁ ⟷ EQUIV d v₀ v₁ → EQUIV d v₀ v₁ ⟷ EQUIV e v₀ v₁ → EQUIV c v₀ v₁ ⟷ EQUIV e v₀ v₁
{-
    _⊕_     : {t₁ t₂ t₃ t₄ : U} →
              (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (PLUS t₁ t₂ ⟷ PLUS t₃ t₄)
    _⊗_     : {t₁ t₂ t₃ t₄ : U} →
              (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (TIMES t₁ t₂ ⟷ TIMES t₃ t₄)
-}
    lidl    : {t₁ t₂ : Pi0.U}
              {c : t₁ Pi0.⟷ t₂} {v₁ : Pi0.⟦ t₁ ⟧} {v₂ : Pi0.⟦ t₂ ⟧} →
              EQUIV (Pi0.id⟷ Pi0.◎ c) v₁ v₂ ⟷ EQUIV c v₁ v₂
    lidr    : {t₁ t₂ : Pi0.U}
              {c : t₁ Pi0.⟷ t₂} {v₁ : Pi0.⟦ t₁ ⟧} {v₂ : Pi0.⟦ t₂ ⟧} →
              EQUIV c v₁ v₂ ⟷ EQUIV (Pi0.id⟷ Pi0.◎ c) v₁ v₂
    ridl    : {t₁ t₂ : Pi0.U}
              {c : t₁ Pi0.⟷ t₂} {v₁ : Pi0.⟦ t₁ ⟧} {v₂ : Pi0.⟦ t₂ ⟧} →
              EQUIV (c Pi0.◎ Pi0.id⟷) v₁ v₂ ⟷ EQUIV c v₁ v₂
    ridr    : {t₁ t₂ : Pi0.U}
              {c : t₁ Pi0.⟷ t₂} {v₁ : Pi0.⟦ t₁ ⟧} {v₂ : Pi0.⟦ t₂ ⟧} →
              EQUIV c v₁ v₂ ⟷ EQUIV (c Pi0.◎ Pi0.id⟷) v₁ v₂
    invll   : {t₁ t₂ : Pi0.U} {c : t₁ Pi0.⟷ t₂} {v₀ v₂ : Pi0.⟦ t₂ ⟧}  →
              EQUIV (Pi0.sym⟷ c Pi0.◎ c) v₀ v₂ ⟷ EQUIV Pi0.id⟷ v₀ v₂
    invlr   : {t₁ t₂ : Pi0.U} {c : t₁ Pi0.⟷ t₂} {v₀ v₂ : Pi0.⟦ t₂ ⟧}  →
              EQUIV Pi0.id⟷ v₀ v₂ ⟷ EQUIV (Pi0.sym⟷ c Pi0.◎ c) v₀ v₂
    invrl   : {t₁ t₂ : Pi0.U} {c : t₁ Pi0.⟷ t₂} {v₀ v₁ : Pi0.⟦ t₁ ⟧}  →
              EQUIV (c Pi0.◎ Pi0.sym⟷ c) v₀ v₁ ⟷ EQUIV Pi0.id⟷ v₀ v₁
    invrr   : {t₁ t₂ : Pi0.U} {c : t₁ Pi0.⟷ t₂} {v₀ v₁ : Pi0.⟦ t₁ ⟧}  →
              EQUIV Pi0.id⟷ v₀ v₁ ⟷ EQUIV (c Pi0.◎ Pi0.sym⟷ c) v₀ v₁
    invinvl : {t₁ t₂ : Pi0.U}
              {c : t₁ Pi0.⟷ t₂} {v₁ : Pi0.⟦ t₁ ⟧} {v₂ : Pi0.⟦ t₂ ⟧} →
              EQUIV (Pi0.sym⟷ (Pi0.sym⟷ c)) v₁ v₂ ⟷ EQUIV c v₁ v₂
    invinvr : {t₁ t₂ : Pi0.U}
              {c : t₁ Pi0.⟷ t₂} {v₁ : Pi0.⟦ t₁ ⟧} {v₂ : Pi0.⟦ t₂ ⟧} →
              EQUIV c v₁ v₂ ⟷ EQUIV (Pi0.sym⟷ (Pi0.sym⟷ c)) v₁ v₂
    tassocl : {t₁ t₂ t₃ t₄ : Pi0.U}
              {c₁ : t₁ Pi0.⟷ t₂} {c₂ : t₂ Pi0.⟷ t₃} {c₃ : t₃ Pi0.⟷ t₄}
              {v₁ : Pi0.⟦ t₁ ⟧} {v₄ : Pi0.⟦ t₄ ⟧} →
              EQUIV (c₁ Pi0.◎ (c₂ Pi0.◎ c₃)) v₁ v₄ ⟷
              EQUIV ((c₁ Pi0.◎ c₂) Pi0.◎ c₃) v₁ v₄
    tassocr : {t₁ t₂ t₃ t₄ : Pi0.U}
              {c₁ : t₁ Pi0.⟷ t₂} {c₂ : t₂ Pi0.⟷ t₃} {c₃ : t₃ Pi0.⟷ t₄}
              {v₁ : Pi0.⟦ t₁ ⟧} {v₄ : Pi0.⟦ t₄ ⟧} →
              EQUIV ((c₁ Pi0.◎ c₂) Pi0.◎ c₃) v₁ v₄ ⟷
              EQUIV (c₁ Pi0.◎ (c₂ Pi0.◎ c₃)) v₁ v₄
    -- this is closely related to Eckmann-Hilton
    resp◎   : {t₁ t₂ t₃ : Pi0.U}
              {c₁ : t₁ Pi0.⟷ t₂} {c₂ : t₂ Pi0.⟷ t₃}
              {c₃ : t₁ Pi0.⟷ t₂} {c₄ : t₂ Pi0.⟷ t₃}
              {v₁ : Pi0.⟦ t₁ ⟧} {v₂ : Pi0.⟦ t₂ ⟧} {v₃ : Pi0.⟦ t₃ ⟧} →
              (EQUIV c₁ v₁ v₂ ⟷ EQUIV c₃ v₁ v₂) →
              (EQUIV c₂ v₂ v₃ ⟷ EQUIV c₄ v₂ v₃) →
               EQUIV (c₁ Pi0.◎ c₂) v₁ v₃ ⟷ EQUIV (c₃ Pi0.◎ c₄) v₁ v₃

  -- extractor for ⟷
  src : {t₁ t₂ : U} → t₁ ⟷ t₂ → Pi0.U
  src (id⟷ {t₁}) = t₁
  src (sym⟷ {t₁} c) = t₁
  src (_◎_ {t₁} _ _) = t₁
  src (lidl {t₁}) = t₁
  src (lidr {t₁}) = t₁
  src (ridl {t₁}) = t₁
  src (ridr {t₁}) = t₁
  src (invll {t₁}) = t₁
  src (invlr {t₁}) = t₁
  src (invrl {t₁}) = t₁
  src (invrr {t₁}) = t₁
  src (invinvl {t₁}) = t₁
  src (invinvr {t₁}) = t₁
  src (tassocl {t₁}) = t₁
  src (tassocr {t₁}) = t₁
  src (resp◎ {t₁} _ _) = t₁

  val : {t₁ t₂ : U} → (c : t₁ ⟷ t₂) → Pi0.⟦ src c ⟧
  val (id⟷ {v₀ = v₀}) = v₀
  val (sym⟷ {v₀ = v₀} c) = v₀
  val (c ◎ c₁) = {!!}
  val lidl = {!!}
  val lidr = {!!}
  val ridl = {!!}
  val ridr = {!!}
  val invll = {!!}
  val invlr = {!!}
  val invrl = {!!}
  val invrr = {!!}
  val invinvl = {!!}
  val invinvr = {!!}
  val tassocl = {!!}
  val tassocr = {!!}
  val (resp◎ c c₅) = {!!}

  -- Examples
  -- id;swap₊ is equivalent to swap₊
  e₁ : EQUIV (Pi0.id⟷ Pi0.◎ Pi0.swap₊) Pi0.FALSE Pi0.TRUE ⟷
       EQUIV Pi0.swap₊ Pi0.FALSE Pi0.TRUE
  e₁ = lidl

  -- swap₊;id;swap₊ is equivalent to id
  e₂ : EQUIV (Pi0.swap₊ Pi0.◎ (Pi0.id⟷ Pi0.◎ Pi0.swap₊)) Pi0.FALSE Pi0.FALSE ⟷
       EQUIV Pi0.id⟷ Pi0.FALSE Pi0.FALSE
  e₂ = {!!}

  arr : {t₁ t₂ : Pi0.U} {c : t₁ Pi0.⟷ t₂} → Pi0.⟦ t₁ ⟧ → Pi0.⟦ t₂ ⟧ → Set
  arr {t₁} {t₂} {c} v₁ v₂ = ⟦ EQUIV c v₁ v₂ ⟧

  -- we have a 1Groupoid structure
  G : 1Groupoid
  G = record
        { set = Pi0.U
        ; _↝_ = Pi0._⟷_
        ; _≈_ = λ c₀ c₁ → ∀ {v₀ v₁} → EQUIV c₀ v₀ v₁ ⟷ EQUIV c₁ v₀ v₁
        ; id = Pi0.id⟷
        ; _∘_ = λ c₀ c₁ → c₁ Pi0.◎ c₀
        ; _⁻¹ = Pi0.sym⟷
        ; lneutr = λ α → ridl {c = α}
        ; rneutr = λ α → lidl { c = α}
        ; assoc = λ α β δ {v₁} {v₄} → tassocl
        ; equiv = record { refl = id⟷
                         ; sym = λ c → sym⟷ c
                         ; trans = λ c₀ c₁ → c₀ ◎ c₁ }
        ; linv = λ α → invrl {c = α}
        ; rinv = λ α → invll {c = α}
        ; ∘-resp-≈ = λ {_} {_} {_} {f} {h} {g} {i} f⟷h g⟷i {v₀} {v₁} →
                     resp◎  {v₂ = {!val f⟷h!}} g⟷i f⟷h
        }

------------------------------------------------------------------------------
-- Level 2 explicitly...
{-
module Pi2 where
  -- types
  data U : Set where
    ZERO  : U
    ONE   : U
    PLUS  : U → U → U
    TIMES : U → U → U
    EQUIV : {t₁ t₂ : Pi1.U} → (t₁ Pi1.⟷ t₂) → Pi1.⟦ t₁ ⟧ → Pi1.⟦ t₂ ⟧ → U

  data Unite₊ {t : Pi1.U} : Pi1.⟦ Pi1.PLUS Pi1.ZERO t ⟧ → Pi1.⟦ t ⟧ → Set where
    pathUnite₊ : (v₁ : Pi1.⟦ Pi1.PLUS Pi1.ZERO t ⟧) → (v₂ : Pi1.⟦ t ⟧) → Unite₊ v₁ v₂

  data Id⟷ {t : Pi1.U} : Pi1.⟦ t ⟧ → Pi1.⟦ t ⟧ → Set where
    pathId⟷ : (v₁ : Pi1.⟦ t ⟧) → (v₂ : Pi1.⟦ t ⟧) → Id⟷ v₁ v₂

  -- values
  mutual

    ⟦_⟧ : U → Set
    ⟦ ZERO ⟧          = ⊥
    ⟦ ONE ⟧           = ⊤
    ⟦ PLUS t₁ t₂ ⟧    = ⟦ t₁ ⟧ ⊎ ⟦ t₂ ⟧
    ⟦ TIMES t₁ t₂ ⟧   = ⟦ t₁ ⟧ × ⟦ t₂ ⟧
    ⟦ EQUIV c v₁ v₂ ⟧ = f c v₁ v₂

    f : {t₁ t₂ : Pi1.U} → (t₁ Pi1.⟷ t₂) → Pi1.⟦ t₁ ⟧ → Pi1.⟦ t₂ ⟧ → Set
    f (Pi1.id⟷ {t}) v v' = Id⟷ {t} v v'
    f (Pi1._◎_ {t₂ = t₂} c₁ c₂) v₁ v₃ =
      Σ[ v₂ ∈ Pi1.⟦ t₂ ⟧ ] (f c₁ v₁ v₂ × f c₂ v₂ v₃)
--    f (Pi1.lidl {v₁ = v₁}) (pathTrans .v₁ (Pi1.pathId⟷ .v₁) q) q' = ⊥ -- todo
    f c v₁ v₂ = ⊥ -- to do

  -- combinators
  data _⟷_ : U → U → Set where
    unite₊  : {t : U} → PLUS ZERO t ⟷ t
    uniti₊  : {t : U} → t ⟷ PLUS ZERO t
    swap₊   : {t₁ t₂ : U} → PLUS t₁ t₂ ⟷ PLUS t₂ t₁
    assocl₊ : {t₁ t₂ t₃ : U} → PLUS t₁ (PLUS t₂ t₃) ⟷ PLUS (PLUS t₁ t₂) t₃
    assocr₊ : {t₁ t₂ t₃ : U} → PLUS (PLUS t₁ t₂) t₃ ⟷ PLUS t₁ (PLUS t₂ t₃)
    unite⋆  : {t : U} → TIMES ONE t ⟷ t
    uniti⋆  : {t : U} → t ⟷ TIMES ONE t
    swap⋆   : {t₁ t₂ : U} → TIMES t₁ t₂ ⟷ TIMES t₂ t₁
    assocl⋆ : {t₁ t₂ t₃ : U} → TIMES t₁ (TIMES t₂ t₃) ⟷ TIMES (TIMES t₁ t₂) t₃
    assocr⋆ : {t₁ t₂ t₃ : U} → TIMES (TIMES t₁ t₂) t₃ ⟷ TIMES t₁ (TIMES t₂ t₃)
    distz   : {t : U} → TIMES ZERO t ⟷ ZERO
    factorz : {t : U} → ZERO ⟷ TIMES ZERO t
    dist    : {t₁ t₂ t₃ : U} →
              TIMES (PLUS t₁ t₂) t₃ ⟷ PLUS (TIMES t₁ t₃) (TIMES t₂ t₃)
    factor  : {t₁ t₂ t₃ : U} →
              PLUS (TIMES t₁ t₃) (TIMES t₂ t₃) ⟷ TIMES (PLUS t₁ t₂) t₃
    id⟷     : {t : U} → t ⟷ t
    sym⟷    : {t₁ t₂ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₁)
    _◎_     : {t₁ t₂ t₃ : U} → (t₁ ⟷ t₂) → (t₂ ⟷ t₃) → (t₁ ⟷ t₃)
    _⊕_     : {t₁ t₂ t₃ t₄ : U} →
              (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (PLUS t₁ t₂ ⟷ PLUS t₃ t₄)
    _⊗_     : {t₁ t₂ t₃ t₄ : U} →
              (t₁ ⟷ t₃) → (t₂ ⟷ t₄) → (TIMES t₁ t₂ ⟷ TIMES t₃ t₄)
    lid     : {t₁ t₂ : Pi1.U} {v₁ : Pi1.⟦ t₁ ⟧} {v₂ : Pi1.⟦ t₂ ⟧}
              {c : t₁ Pi1.⟷ t₂} →
              EQUIV (Pi1.id⟷ Pi1.◎ c) v₁ v₂ ⟷ EQUIV c v₁ v₂
-}
------------------------------------------------------------------------------

ext: agda

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


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

open import Categories.Category

module Categories.Object.Terminal.Limit {o ℓ e} (C : Category o ℓ e) where

open import Categories.Category.Lift
open import Categories.Category.Finite.Fin.Construction.Discrete
open import Categories.Object.Terminal C
open import Categories.Diagram.Limit
open import Categories.Functor.Core

import Categories.Category.Construction.Cones as Co

private
  module C = Category C
  open C

module _ {o′ ℓ′ e′} {F : Functor (liftC o′ ℓ′ e′ (Discrete 0)) C} where
  limit⇒⊥ : Limit F → Terminal
  limit⇒⊥ L = record
    { ⊤        = apex
    ; !        = rep record
      { apex = record
        { ψ       = λ ()
        ; commute = λ { {()} }
        }
      }
    ; !-unique = λ f → terminal.!-unique record
      { arr     = f
      ; commute = λ { {()} }
      }
    }
    where open Limit L

module _ o′ ℓ′ e′ where

  ⊥⇒limit-F : Functor (liftC o′ ℓ′ e′ (Discrete 0)) C
  ⊥⇒limit-F = record
    { F₀           = λ ()
    ; F₁           = λ { {()} }
    ; identity     = λ { {()} }
    ; homomorphism = λ { {()} }
    ; F-resp-≈     = λ { {()} }
    }

  ⊥⇒limit : Terminal → Limit ⊥⇒limit-F
  ⊥⇒limit t = record
    { terminal = record
      { ⊤        = record
        { N    = ⊤
        ; apex = record
          { ψ       = λ ()
          ; commute = λ { {()} }
          }
        }
      ; !        = λ {K} →
        let open Co.Cone ⊥⇒limit-F K
        in record
        { arr     = !
        ; commute = λ { {()} }
        }
      ; !-unique = λ f →
        let module f = Co.Cone⇒ ⊥⇒limit-F f
        in !-unique f.arr
      }
    }
    where open Terminal t

max_stars_repo_name: laMudri/agda-categories

max_issues_repo_name: laMudri/agda-categories

max_forks_repo_name: laMudri/agda-categories


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Booleans
------------------------------------------------------------------------

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

module Data.Bool where

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl)

------------------------------------------------------------------------
-- The boolean type and some operations

open import Data.Bool.Base public

------------------------------------------------------------------------
-- Publicly re-export queries

open import Data.Bool.Properties public
  using (_≟_)

------------------------------------------------------------------------
-- Some properties

decSetoid : DecSetoid _ _
decSetoid = PropEq.decSetoid _≟_


text:
-- 2010-09-29

module IllegalUseOfIrrelevantDeclaration where

import Common.Irrelevance

record Subset (A : Set) (P : A -> Set) : Set where
  constructor _#_
  field
    elem         : A
    .certificate : P elem

postulate
  .irrelevant : {A : Set} -> .A -> A

certificate : {A : Set}{P : A -> Set} -> (x : Subset A P) -> P (Subset.elem x)
certificate (a # p) = irrelevant p
-- since certificate is not declared irrelevant, cannot use irrelevant postulate here

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import lib.Base
open import lib.PathGroupoid
open import lib.cubical.Square

module lib.cubical.Cube where

{- Coordinates are yzx, where
     x : left -> right
     y : back -> front
     z : top  -> bottom
 -}

data Cube {i} {A : Type i} {a₀₀₀ : A} :
  {a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  (sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀) -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  (sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁) -- right

  {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
  (sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁) -- back
  (sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁) -- top
  (sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁) -- bottom
  (sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁) -- front
  → Type i

  where
  idc : Cube ids ids ids ids ids ids

{- Just transport, but less clutter to use -}
module _ {i} {A : Type i} {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right

  {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
  {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
  {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
  {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
  {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
  where

  cube-shift-left : {sq₋₋₀' : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀}
    → sq₋₋₀ == sq₋₋₀'
    → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
    → Cube sq₋₋₀' sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
  cube-shift-left idp cu = cu

  cube-shift-right : {sq₋₋₁' : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁}
    → sq₋₋₁ == sq₋₋₁'
    → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
    → Cube sq₋₋₀ sq₋₋₁' sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
  cube-shift-right idp cu = cu

  cube-shift-back : {sq₀₋₋' : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁}
    → sq₀₋₋ == sq₀₋₋'
    → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
    → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋' sq₋₀₋ sq₋₁₋ sq₁₋₋
  cube-shift-back idp cu = cu

  cube-shift-top : {sq₋₀₋' : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁}
    → sq₋₀₋ == sq₋₀₋'
    → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
    → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋' sq₋₁₋ sq₁₋₋
  cube-shift-top idp cu = cu

  cube-shift-bot : {sq₋₁₋' : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁}
    → sq₋₁₋ == sq₋₁₋'
    → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
    → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋' sq₁₋₋
  cube-shift-bot idp cu = cu

  cube-shift-front : {sq₁₋₋' : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁}
    → sq₁₋₋ == sq₁₋₋'
    → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
    → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋'
  cube-shift-front idp cu = cu

{- A cube where two opposite squares are both [ids] is a square -}
module _ {i} {A : Type i} where

  x-id-cube-in : {a₀ a₁ : A} {p₀₀ p₀₁ p₁₀ p₁₁ : a₀ == a₁}
    {α₀₋ : p₀₀ == p₁₀} {α₁₋ : p₀₁ == p₁₁}
    {α₋₀ : p₀₀ == p₀₁} {α₋₁ : p₁₀ == p₁₁}
    → Square α₀₋ α₋₀ α₋₁ α₁₋
    → Cube ids ids (vert-degen-square α₀₋) (vert-degen-square α₋₀)
           (vert-degen-square α₋₁) (vert-degen-square α₁₋)
  x-id-cube-in {p₀₀ = idp} ids = idc

  y-id-cube-in : {a₀ a₁ : A} {p₀₀ p₀₁ p₁₀ p₁₁ : a₀ == a₁}
    {α₀₋ : p₀₀ == p₁₀} {α₁₋ : p₀₁ == p₁₁}
    {α₋₀ : p₀₀ == p₀₁} {α₋₁ : p₁₀ == p₁₁}
    → Square α₀₋ α₋₀ α₋₁ α₁₋
    → Cube (vert-degen-square α₀₋) (vert-degen-square α₁₋)
           ids (horiz-degen-square α₋₀) (horiz-degen-square α₋₁) ids
  y-id-cube-in {p₀₀ = idp} ids = idc

  z-id-cube-in : {a₀ a₁ : A} {p₀₀ p₁₀ p₀₁ p₁₁ : a₀ == a₁}
    {α₀₋ : p₀₀ == p₁₀} {α₁₋ : p₀₁ == p₁₁}
    {α₋₀ : p₀₀ == p₀₁} {α₋₁ : p₁₀ == p₁₁}
    → Square α₀₋ α₋₀ α₋₁ α₁₋
    → Cube (horiz-degen-square α₀₋) (horiz-degen-square α₁₋)
           (horiz-degen-square α₋₀) ids ids (horiz-degen-square α₋₁)
  z-id-cube-in {p₀₀ = idp} ids = idc

{- Cube fillers -}
module _ {i} {A : Type i} where
  fill-cube-left : {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
    {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
    {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
    -- missing left

    {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
    {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
    (sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁) -- right

    {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
    {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
    (sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁) -- back
    (sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁) -- top
    (sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁) -- bottom
    (sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁) -- front
    → Σ (Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀)
        (λ sq₋₋₀ → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋)
  fill-cube-left {p₋₀₀ = p₋₀₀} {p₋₁₀ = p₋₁₀} sq₋₋₁ ids sq₋₀₋ sq₋₁₋ ids =
    (_ ,
     cube-shift-right (vert-degen-square-β sq₋₋₁)
       (cube-shift-top (horiz-degen-square-β sq₋₀₋)
         (cube-shift-bot (horiz-degen-square-β sq₋₁₋)
           cu)))
    where
    fill-sq : Σ (p₋₀₀ == p₋₁₀) (λ α₋₋₀ →
      Square α₋₋₀ (horiz-degen-path sq₋₀₋)
             (horiz-degen-path sq₋₁₋) (vert-degen-path sq₋₋₁))
    fill-sq = fill-square-left _ _ _

    cu : Cube (vert-degen-square (fst fill-sq))
              (vert-degen-square (vert-degen-path sq₋₋₁)) ids
              (horiz-degen-square (horiz-degen-path sq₋₀₋))
              (horiz-degen-square (horiz-degen-path sq₋₁₋)) ids
    cu = y-id-cube-in (snd fill-sq)

  fill-cube-right : {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
    {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
    {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
    (sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀) -- left

    {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
    {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
    -- missing right

    {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
    {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
    (sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁) -- back
    (sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁) -- top
    (sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁) -- bottom
    (sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁) -- front
    → Σ (Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁)
        (λ sq₋₋₁ → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋)
  fill-cube-right sq₋₋₀ {p₋₀₁ = p₋₀₁} {p₋₁₁ = p₋₁₁} ids sq₋₀₋ sq₋₁₋ ids =
    (_ ,
     cube-shift-left (vert-degen-square-β sq₋₋₀)
       (cube-shift-top (horiz-degen-square-β sq₋₀₋)
         (cube-shift-bot (horiz-degen-square-β sq₋₁₋)
           cu)))
    where
    fill-sq : Σ (p₋₀₁ == p₋₁₁) (λ α₋₋₁ →
      Square (vert-degen-path sq₋₋₀) (horiz-degen-path sq₋₀₋)
             (horiz-degen-path sq₋₁₋) α₋₋₁)
    fill-sq = fill-square-right _ _ _

    cu : Cube (vert-degen-square (vert-degen-path sq₋₋₀))
              (vert-degen-square (fst fill-sq)) ids
              (horiz-degen-square (horiz-degen-path sq₋₀₋))
              (horiz-degen-square (horiz-degen-path sq₋₁₋)) ids
    cu = y-id-cube-in (snd fill-sq)

fill-cube-left-unique : ∀ {i} {A : Type i} {a₀₀₀ : A}
  {a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right

  {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
  {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
  {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
  {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
  {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
  → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
  → sq₋₋₀ == fst (fill-cube-left sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋)
fill-cube-left-unique idc = idp

fill-cube-right-unique : ∀ {i} {A : Type i} {a₀₀₀ : A}
  {a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right

  {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
  {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
  {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
  {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
  {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
  → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
  → sq₋₋₁ == fst (fill-cube-right sq₋₋₀ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋)
fill-cube-right-unique idc = idp

{- Paths as degenerate cubes -}
module _ {i} {A : Type i} where

  x-degen-cube : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    {sq₋₋₀ sq₋₋₁ : Square p₀₋ p₋₀ p₋₁ p₁₋}
    → sq₋₋₀ == sq₋₋₁
    → Cube sq₋₋₀ sq₋₋₁ hid-square hid-square hid-square hid-square
  x-degen-cube {sq₋₋₀ = ids} idp = idc

  y-degen-cube : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    {sq₀₋₋ sq₁₋₋ : Square p₀₋ p₋₀ p₋₁ p₁₋}
    → sq₀₋₋ == sq₁₋₋
    → Cube hid-square hid-square sq₀₋₋ vid-square vid-square sq₁₋₋
  y-degen-cube {sq₀₋₋ = ids} idp = idc

  z-degen-cube : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    {sq₋₀₋ sq₋₁₋ : Square p₀₋ p₋₀ p₋₁ p₁₋}
    → sq₋₀₋ == sq₋₁₋
    → Cube vid-square vid-square vid-square sq₋₀₋ sq₋₁₋ vid-square
  z-degen-cube {sq₋₀₋ = ids} idp = idc

  x-degen-cube-out : {a₀₀ a₀₁ a₁₀ a₁₁ : A}
    {p₀₋ : a₀₀ == a₀₁} {p₋₀ : a₀₀ == a₁₀}
    {p₋₁ : a₀₁ == a₁₁} {p₁₋ : a₁₀ == a₁₁}
    {sq₋₋₀ sq₋₋₁ : Square p₀₋ p₋₀ p₋₁ p₁₋}
    → Cube sq₋₋₀ sq₋₋₁ hid-square hid-square hid-square hid-square
    → sq₋₋₀ == sq₋₋₁
  x-degen-cube-out cu =
    fill-cube-left-unique cu ∙ ! (fill-cube-left-unique (x-degen-cube idp))

{- A pathover between squares can be represented as a cube -}
module _ {i j} {A : Type i} {B : Type j} {b₀₀ b₀₁ b₁₀ b₁₁ : A → B}
  {p₀₋ : (a : A) → b₀₀ a == b₀₁ a} {p₋₀ : (a : A) → b₀₀ a == b₁₀ a}
  {p₋₁ : (a : A) → b₀₁ a == b₁₁ a} {p₁₋ : (a : A) → b₁₀ a == b₁₁ a}
  where

  ↓-square-to-cube :  {x y : A} {q : x == y}
    {u : Square (p₀₋ x) (p₋₀ x) (p₋₁ x) (p₁₋ x)}
    {v : Square (p₀₋ y) (p₋₀ y) (p₋₁ y) (p₁₋ y)}
    → u == v [ (λ z → Square (p₀₋ z) (p₋₀ z) (p₋₁ z) (p₁₋ z)) ↓ q ]
    → Cube u v (natural-square p₀₋ q ) (natural-square p₋₀ q)
           (natural-square p₋₁ q) (natural-square p₁₋ q)
  ↓-square-to-cube {q = idp} r = x-degen-cube r

  cube-to-↓-square : {x y : A} {q : x == y}
    {sqx : Square (p₀₋ x) (p₋₀ x) (p₋₁ x) (p₁₋ x)}
    {sqy : Square (p₀₋ y) (p₋₀ y) (p₋₁ y) (p₁₋ y)}
    → Cube sqx sqy (natural-square p₀₋ q) (natural-square p₋₀ q)
           (natural-square p₋₁ q) (natural-square p₁₋ q)
    → sqx == sqy [ (λ z → Square (p₀₋ z) (p₋₀ z) (p₋₁ z) (p₁₋ z)) ↓ q ]
  cube-to-↓-square {q = idp} cu = x-degen-cube-out cu

module _ {i j} {A : Type i} {B : Type j} {b₀₀ b₀₁ b₁₀ b₁₁ : B}
  {p₀₋ : (a : A) → b₀₀ == b₀₁} {p₋₀ : (a : A) → b₀₀ == b₁₀}
  {p₋₁ : (a : A) → b₀₁ == b₁₁} {p₁₋ : (a : A) → b₁₀ == b₁₁}
  where

  cube-to-disc-square : {x y : A} {q : x == y}
    {sqx : Square (p₀₋ x) (p₋₀ x) (p₋₁ x) (p₁₋ x)}
    {sqy : Square (p₀₋ y) (p₋₀ y) (p₋₁ y) (p₁₋ y)}
    → Cube sqx sqy (natural-square p₀₋ q) (natural-square p₋₀ q)
           (natural-square p₋₁ q) (natural-square p₁₋ q)
    → Square (square-to-disc sqx) (ap (λ z → p₀₋ z ∙ p₋₁ z) q)
             (ap (λ z → p₋₀ z ∙ p₁₋ z) q) (square-to-disc sqy)
  cube-to-disc-square cu =
    ↓-='-to-square (ap↓ square-to-disc (cube-to-↓-square cu))

ap-cube : ∀ {i j} {A : Type i} {B : Type j} (f : A → B)
  {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right

  {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
  {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
  {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
  {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
  {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
  → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
  → Cube (ap-square f sq₋₋₀) (ap-square f sq₋₋₁) (ap-square f sq₀₋₋)
         (ap-square f sq₋₀₋) (ap-square f sq₋₁₋) (ap-square f sq₁₋₋)
ap-cube f idc = idc

natural-cube : ∀ {i j} {A : Type i} {B : Type j}
  {f₀₀ f₀₁ f₁₀ f₁₁ : A → B}
  {p₀₋ : (a : A) → f₀₀ a == f₀₁ a} {p₋₀ : (a : A) → f₀₀ a == f₁₀ a}
  {p₋₁ : (a : A) → f₀₁ a == f₁₁ a} {p₁₋ : (a : A) → f₁₀ a == f₁₁ a}
  (sq : ∀ a → Square (p₀₋ a) (p₋₀ a) (p₋₁ a) (p₁₋ a))
  {x y : A} (q : x == y)
  → Cube (sq x) (sq y)
         (natural-square p₀₋ q) (natural-square p₋₀ q)
         (natural-square p₋₁ q) (natural-square p₁₋ q)
natural-cube sq idp = x-degen-cube idp

cube-rotate-x→z : ∀ {i} {A : Type i}
  {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right

  {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
  {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
  {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
  {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
  {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
  → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
  → Cube (square-symmetry sq₀₋₋) (square-symmetry sq₁₋₋)
         (square-symmetry sq₋₀₋) sq₋₋₀ sq₋₋₁ (square-symmetry sq₋₁₋)
cube-rotate-x→z idc = idc

cube-symmetry-x : ∀ {i} {A : Type i}
  {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right

  {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
  {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
  {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
  {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
  {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
  → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
  → Cube (square-symmetry sq₋₋₀) (square-symmetry sq₋₋₁)
         sq₋₀₋ sq₀₋₋ sq₁₋₋ sq₋₁₋
cube-symmetry-x idc = idc

cube-!-x : ∀ {i} {A : Type i}
  {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- right

  {p₀₀₋ : a₀₀₀ == a₀₀₁} {p₀₁₋ : a₀₁₀ == a₀₁₁}
  {p₁₀₋ : a₁₀₀ == a₁₀₁} {p₁₁₋ : a₁₁₀ == a₁₁₁}
  {sq₀₋₋ : Square p₀₋₀ p₀₀₋ p₀₁₋ p₀₋₁} -- back
  {sq₋₀₋ : Square p₋₀₀ p₀₀₋ p₁₀₋ p₋₀₁} -- top
  {sq₋₁₋ : Square p₋₁₀ p₀₁₋ p₁₁₋ p₋₁₁} -- bottom
  {sq₁₋₋ : Square p₁₋₀ p₁₀₋ p₁₁₋ p₁₋₁} -- front
  → Cube sq₋₋₀ sq₋₋₁ sq₀₋₋ sq₋₀₋ sq₋₁₋ sq₁₋₋
  → Cube sq₋₋₁ sq₋₋₀ (!□h sq₀₋₋) (!□h sq₋₀₋) (!□h sq₋₁₋) (!□h sq₁₋₋)
cube-!-x idc = idc

_∙³x_ : ∀ {i} {A : Type i}
  {a₀₀₀ a₀₁₀ a₁₀₀ a₁₁₀ a₀₀₁ a₀₁₁ a₁₀₁ a₁₁₁ a₀₀₂ a₀₁₂ a₁₀₂ a₁₁₂ : A}
  {p₀₋₀ : a₀₀₀ == a₀₁₀} {p₋₀₀ : a₀₀₀ == a₁₀₀}
  {p₋₁₀ : a₀₁₀ == a₁₁₀} {p₁₋₀ : a₁₀₀ == a₁₁₀}
  {sq₋₋₀ : Square p₀₋₀ p₋₀₀ p₋₁₀ p₁₋₀} -- left

  {p₀₋₁ : a₀₀₁ == a₀₁₁} {p₋₀₁ : a₀₀₁ == a₁₀₁}
  {p₋₁₁ : a₀₁₁ == a₁₁₁} {p₁₋₁ : a₁₀₁ == a₁₁₁}
  {sq₋₋₁ : Square p₀₋₁ p₋₀₁ p₋₁₁ p₁₋₁} -- middle

  {p₀₋₂ : a₀₀₂ == a₀₁₂} {p₋₀₂ : a₀₀₂ == a₁₀₂}
  {p₋₁₂ : a₀₁₂ == a₁₁₂} {p₁₋₂ : a₁₀₂ == a₁₁₂}
  {sq₋₋₂ : Square p₀₋₂ p₋₀₂ p₋₁₂ p₁₋₂} -- right

  {p₀₀l : a₀₀₀ == a₀₀₁} {p₀₁l : a₀₁₀ == a₀₁₁}
  {p₁₀l : a₁₀₀ == a₁₀₁} {p₁₁l : a₁₁₀ == a₁₁₁}
  {sq₀₋l : Square p₀₋₀ p₀₀l p₀₁l p₀₋₁} -- backl
  {sq₋₀l : Square p₋₀₀ p₀₀l p₁₀l p₋₀₁} -- topl
  {sq₋₁l : Square p₋₁₀ p₀₁l p₁₁l p₋₁₁} -- bottoml
  {sq₁₋l : Square p₁₋₀ p₁₀l p₁₁l p₁₋₁} -- frontl

  {p₀₀r : a₀₀₁ == a₀₀₂} {p₀₁r : a₀₁₁ == a₀₁₂}
  {p₁₀r : a₁₀₁ == a₁₀₂} {p₁₁r : a₁₁₁ == a₁₁₂}
  {sq₀₋r : Square p₀₋₁ p₀₀r p₀₁r p₀₋₂} -- backr
  {sq₋₀r : Square p₋₀₁ p₀₀r p₁₀r p₋₀₂} -- topr
  {sq₋₁r : Square p₋₁₁ p₀₁r p₁₁r p₋₁₂} -- bottomr
  {sq₁₋r : Square p₁₋₁ p₁₀r p₁₁r p₁₋₂} -- frontr

  → Cube sq₋₋₀ sq₋₋₁ sq₀₋l sq₋₀l sq₋₁l sq₁₋l
  → Cube sq₋₋₁ sq₋₋₂ sq₀₋r sq₋₀r sq₋₁r sq₁₋r
  → Cube sq₋₋₀ sq₋₋₂ (sq₀₋l ⊡h sq₀₋r) (sq₋₀l ⊡h sq₋₀r)
         (sq₋₁l ⊡h sq₋₁r) (sq₁₋l ⊡h sq₁₋r)
idc ∙³x cu = cu

infixr 8 _∙³x_

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import Categories.Category
open import Categories.Monad

module Categories.Adjoint.Construction.EilenbergMoore {o ℓ e} {C : Category o ℓ e} (M : Monad C) where

open import Categories.Category.Construction.EilenbergMoore M
open import Categories.Adjoint
open import Categories.Functor
open import Categories.Functor.Properties
open import Categories.NaturalTransformation
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_)
open import Categories.Morphism.Reasoning C

private
  module C = Category C
  module M = Monad M
  open M.F
  open C
  open HomReasoning

Forgetful : Functor EilenbergMoore C
Forgetful = record
  { F₀           = λ X → Module.A X
  ; F₁           = λ f → Module⇒.arr f
  ; identity     = refl
  ; homomorphism = refl
  ; F-resp-≈     = λ eq → eq
  }

Free : Functor C EilenbergMoore
Free = record
  { F₀           = λ A → record
    { A        = F₀ A
    ; action   = M.μ.η A
    ; commute  = M.assoc
    ; identity = M.identityʳ
    }
  ; F₁           = λ f → record
    { arr     = F₁ f
    ; commute = ⟺ (M.μ.commute f)
    }
  ; identity     = identity
  ; homomorphism = homomorphism
  ; F-resp-≈     = F-resp-≈
  }

FF≃F : Forgetful ∘F Free ≃ M.F
FF≃F = record
  { F⇒G = record
    { η           = λ X → F₁ C.id
    ; commute     = λ f → [ M.F ]-resp-square id-comm-sym
    ; sym-commute = λ f → [ M.F ]-resp-square id-comm
    }
  ; F⇐G = record
    { η       = λ X → F₁ C.id
    ; commute = λ f → [ M.F ]-resp-square id-comm-sym
    ; sym-commute = λ f → [ M.F ]-resp-square id-comm
    }
  ; iso = λ X → record
    { isoˡ = elimˡ identity ○ identity
    ; isoʳ = elimˡ identity ○ identity
    }
  }

Free⊣Forgetful : Free ⊣ Forgetful
Free⊣Forgetful = record
  { unit   = record
    { η           = M.η.η
    ; commute     = M.η.commute
    ; sym-commute = M.η.sym-commute
    }
  ; counit = record
    { η           = λ X →
      let module X = Module X
      in record
        { arr     = X.action
        ; commute = ⟺ X.commute
        }
    ; commute     = λ f → ⟺ (Module⇒.commute f)
    ; sym-commute = Module⇒.commute
    }
  ; zig    = M.identityˡ
  ; zag    = λ {B} → Module.identity B
  }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
open import Data.Product using ( _×_ ; _,_ )
open import Relation.Binary.PropositionalEquality using ( refl )
open import Relation.Unary using ( _∈_ )
open import Web.Semantic.DL.ABox using ( ABox ; ⟨ABox⟩ )
open import Web.Semantic.DL.ABox.Interp using ( Interp ; Surjective ; _,_ ; ⌊_⌋ ; ind ; _*_ ; emp )
open import Web.Semantic.DL.ABox.Interp.Morphism using ( _≲_ ; _,_ ; ≲⌊_⌋ ; ≲-resp-ind ; _≋_ ; _**_ )
open import Web.Semantic.DL.ABox.Model using ( _⊨a_ ; ⟨ABox⟩-resp-⊨ ; *-resp-⟨ABox⟩ ; ⊨a-resp-≡ )
open import Web.Semantic.DL.Integrity using ( _⊕_⊨_ ; Initial ; Mediator ; Mediated ; _,_ )
open import Web.Semantic.DL.KB using ( KB ; _,_ )
open import Web.Semantic.DL.KB.Model using ( _⊨_ )
open import Web.Semantic.DL.Signature using ( Signature )
open import Web.Semantic.DL.TBox.Interp using ( _⊨_≈_ ; ≈-refl )
open import Web.Semantic.DL.TBox.Interp.Morphism using ( morph ; ≲-image )
open import Web.Semantic.Util using ( False ; _∘_ ; _⊕_⊕_ ; bnode ; inode ; enode )

module Web.Semantic.DL.Integrity.Closed {Σ : Signature} {X : Set} where

infix 2 _⊨₀_ sur_⊨₀_
infixr 4 _,_

-- A closed-world variant on integrity constraints.

data Mediated₀ (I J : Interp Σ X) : Set where
  _,_ : (I≲J : I ≲ J) → (∀ (I≲₁J I≲₂J : I ≲ J) → (I≲₁J ≋ I≲₂J)) → Mediated₀ I J

data Initial₀ KB (I : Interp Σ X) : Set₁ where
  _,_ : (I ⊨ KB) → (∀ J → (J ⊨ KB) → Mediated₀ I J) → (I ∈ Initial₀ KB)

data _⊨₀_ (KB₁ KB₂ : KB Σ X) : Set₁ where
  _,_ : ∀ I → ((I ∈ Initial₀ KB₁) × (I ⊨ KB₂)) → (KB₁ ⊨₀ KB₂)

-- Surjective variant

data sur_⊨₀_ (KB₁ KB₂ : KB Σ X) : Set₁ where
  _,_ : ∀ I → ((I ∈ Surjective) × (I ∈ Initial₀ KB₁) × (I ⊨ KB₂)) → (sur KB₁ ⊨₀ KB₂)

-- Closed-world ICs are given by specializing the open-world case
-- to the empty imported interpretion.

exp : KB Σ X → KB Σ (False ⊕ False ⊕ X)
exp (T , A) = (T , ⟨ABox⟩ enode A)

enode⁻¹ : (False ⊕ False ⊕ X) → X
enode⁻¹ (inode ())
enode⁻¹ (bnode ())
enode⁻¹ (enode x) = x

emp-≲ : ∀ (I : Interp Σ False) → (emp ≲ I)
emp-≲ I = (morph (λ ()) (λ {}) (λ ()) (λ {r} → λ {}) , λ ())

⊨₀-impl-⊨ : ∀ KB₁ KB₂ → (KB₁ ⊨₀ KB₂) → (emp ⊕ exp KB₁ ⊨ KB₂)
⊨₀-impl-⊨ (T , A) (U , B) (I , ((I⊨T , I⊨A) , I-med) , I⊨U , I⊨B) =
  (I′ , I′-init , I⊨U , ⊨a-resp-≡ I (ind I) refl B I⊨B) where

  A′ : ABox Σ (False ⊕ False ⊕ X)
  A′ = ⟨ABox⟩ enode A

  I′ : Interp Σ (False ⊕ False ⊕ X)
  I′ = enode⁻¹ * I

  emp≲I′ : emp ≲ inode * I′
  emp≲I′ = emp-≲ (inode * I′)

  I′-med : Mediator emp I′ emp≲I′ (T , A′)
  I′-med J′ emp≲J′ (J′⊨T , J′⊨A′) = lemma (I-med J (J′⊨T , J⊨A)) where

    J : Interp Σ X
    J = enode * J′

    J⊨A : J ⊨a A
    J⊨A = *-resp-⟨ABox⟩ enode J′ A J′⊨A′

    lemma : Mediated₀ I J → Mediated emp I′ J′ emp≲I′ emp≲J′
    lemma ((I≲J , i≲j) , I≲J-uniq) = ((I≲J , i′≲j′) , (λ ()) , I′≲J′-uniq) where

      i′≲j′ : ∀ x → ⌊ J′ ⌋ ⊨ ≲-image I≲J (ind I (enode⁻¹ x)) ≈ ind J′ x
      i′≲j′ (inode ())
      i′≲j′ (bnode ())
      i′≲j′ (enode x) = i≲j x

      I′≲J′-uniq : ∀ (I≲₁J I≲₂J : I′ ≲ J′)_ _ →  I≲₁J ≋ I≲₂J
      I′≲J′-uniq I≲₁J I≲₂J _ _ = I≲J-uniq
        (≲⌊ I≲₁J ⌋ , λ x → ≲-resp-ind I≲₁J (enode x))
        (≲⌊ I≲₂J ⌋ , λ x → ≲-resp-ind I≲₂J (enode x))

  I′⊨A′ : I′ ⊨a A′
  I′⊨A′ = ⟨ABox⟩-resp-⊨ enode (λ x → ≈-refl ⌊ I ⌋) A I⊨A

  I′-init : I′ ∈ Initial emp (T , A′)
  I′-init = ( emp-≲ (inode * I′) , (I⊨T , I′⊨A′) , I′-med )

⊨-impl-⊨₀ : ∀ KB₁ KB₂ → (emp ⊕ exp KB₁ ⊨ KB₂) → (KB₁ ⊨₀ KB₂)
⊨-impl-⊨₀ (T , A) (U , B)
  (I′ , (emp≲I′ , (I′⊨T , I′⊨A) , I′-med) , I′⊨U , I′⊨B) =
    (I , ((I′⊨T , I⊨A) , I-med) , I′⊨U , I′⊨B) where

  I : Interp Σ X
  I = enode * I′

  I⊨A : I ⊨a A
  I⊨A = *-resp-⟨ABox⟩ enode I′ A I′⊨A

  I-med : ∀ J → (J ⊨ T , A) → Mediated₀ I J
  I-med J (J⊨T , J⊨A) = lemma (I′-med J′ emp≲J′ (J⊨T , J′⊨A)) where

    J′ : Interp Σ (False ⊕ False ⊕ X)
    J′ = enode⁻¹ * J

    emp≲J′ : emp ≲ inode * J′
    emp≲J′ = emp-≲ (inode * J′)

    J′⊨A : J′ ⊨a ⟨ABox⟩ enode A
    J′⊨A = ⟨ABox⟩-resp-⊨ enode (λ x → ≈-refl ⌊ J ⌋) A J⊨A

    I≲J-impl-I′≲J′ : (I ≲ J) → (I′ ≲ J′)
    I≲J-impl-I′≲J′ I≲J = (≲⌊ I≲J ⌋ , i≲j) where

      i≲j : ∀ x → ⌊ J ⌋ ⊨ ≲-image ≲⌊ I≲J ⌋ (ind I′ x) ≈ ind J (enode⁻¹ x)
      i≲j (inode ())
      i≲j (bnode ())
      i≲j (enode x) = ≲-resp-ind I≲J x

    lemma : Mediated emp I′ J′ emp≲I′ emp≲J′ → Mediated₀ I J
    lemma (I≲J , _ , I≲J-uniq) =
      ( (≲⌊ I≲J ⌋ , λ x → ≲-resp-ind I≲J (enode x))
      , λ I≲₁J I≲₂J x → I≲J-uniq
          (I≲J-impl-I′≲J′ I≲₁J) (I≲J-impl-I′≲J′ I≲₂J) (λ ()) (λ ()) x)

max_stars_repo_name: agda/agda-web-semantic

max_issues_repo_name: bblfish/agda-web-semantic

max_forks_repo_name: bblfish/agda-web-semantic


text:
-- The natural numbers.

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

module Tools.Nat where

open import Tools.PropositionalEquality
open import Tools.Nullary

-- We reexport Agda's built-in type of natural numbers.

open import Agda.Builtin.Nat using (zero; suc)
open import Agda.Builtin.Nat using (Nat) public

pattern 1+ n = suc n

infix 4 _≟_

-- Predecessor, cutting off at 0.

pred : Nat → Nat
pred zero = zero
pred (suc n) = n

-- Decision of number equality.

_≟_ : (m n : Nat) → Dec (m ≡ n)
zero  ≟ zero   = yes refl
suc m ≟ suc n  with m ≟ n
suc m ≟ suc .m | yes refl = yes refl
suc m ≟ suc n  | no prf   = no (λ x → prf (subst (λ y → m ≡ pred y) x refl))
zero  ≟ suc n  = no λ()
suc m ≟ zero   = no λ()

max_stars_repo_name: loic-p/logrel-mltt

max_issues_repo_name: loic-p/logrel-mltt

max_forks_repo_name: loic-p/logrel-mltt


text:
------------------------------------------------------------------------
-- A counterexample: The number of steps taken by the uninstrumented
-- interpreter is not, in general, linear in the number of steps taken
-- by the virtual machine for the corresponding compiled program
------------------------------------------------------------------------

open import Prelude

import Lambda.Syntax

module Lambda.Interpreter.Steps.Counterexample
  {Name : Type}
  (open Lambda.Syntax Name)
  (def : Name → Tm 1)
  where

import Equality.Propositional as E
open import Prelude.Size

open import Conat E.equality-with-J as Conat
  hiding ([_]_∼_; step-∼) renaming (_+_ to _⊕_; _*_ to _⊛_)
open import Monad E.equality-with-J hiding (_⊛_)
import Nat E.equality-with-J as Nat
open import Vec.Data E.equality-with-J

open import Delay-monad
open import Delay-monad.Bisimilarity

open import Lambda.Delay-crash
open import Lambda.Interpreter def
open import Lambda.Compiler def
open import Lambda.Virtual-machine comp-name
open import Lambda.Virtual-machine.Instructions Name hiding (crash)

open Closure Tm

-- The uninstrumented interpreter does not provide a suitable cost
-- measure, in the sense that there is a family of programs for which
-- the running "time" (number of steps) of the corresponding compiled
-- programs on the virtual machine is not linear in the running time
-- on the interpreter.

not-suitable-cost-measure :
  ∃ λ (t : ℕ → Tm 0) →
    ¬ ∃ λ k₁ → ∃ λ k₂ → ∀ n →
      [ ∞ ] steps (exec ⟨ comp₀ (t n) , [] , [] ⟩) ≤
            ⌜ k₁ ⌝ ⊕ ⌜ k₂ ⌝ ⊛ steps (⟦ t n ⟧ [])
not-suitable-cost-measure =
  t , λ { (k₁ , k₂ , hyp) → Nat.+≮ 2 $ ⌜⌝-mono⁻¹ (
    ⌜ 3 + k₁ ⌝                               ∼⟨ symmetric-∼ (steps-exec-t∼ k₁) ⟩≤
    steps (exec ⟨ comp₀ (t k₁) , [] , [] ⟩)  ≤⟨ hyp k₁ ⟩
    ⌜ k₁ ⌝ ⊕ ⌜ k₂ ⌝ ⊛ steps (⟦ t k₁ ⟧ [])    ∼⟨ (⌜ k₁ ⌝ ∎∼) +-cong (_ ∎∼) *-cong steps⟦t⟧∼0 k₁ ⟩≤
    ⌜ k₁ ⌝ ⊕ ⌜ k₂ ⌝ ⊛ zero                   ∼⟨ (_ ∎∼) +-cong *-right-zero ⟩≤
    ⌜ k₁ ⌝ ⊕ zero                            ∼⟨ +-right-identity _ ⟩≤
    ⌜ k₁ ⌝                                   ∎≤) }
  where
  -- A family of programs.

  t : ℕ → Tm 0
  t zero    = con true · con true
  t (suc n) = con true · t n

  -- The semantics of every program in this family is strongly
  -- bisimilar to crash.

  ⟦t⟧∼crash : ∀ {i} n → [ i ] ⟦ t n ⟧ [] ∼ crash
  ⟦t⟧∼crash zero    = crash  ∎
  ⟦t⟧∼crash (suc n) =
    ⟦ t (suc n) ⟧ []            ∼⟨⟩
    ⟦ t n ⟧ [] >>= con true ∙_  ∼⟨ ⟦t⟧∼crash n >>=-cong (λ _ → _ ∎) ⟩
    crash >>= con true ∙_       ∼⟨⟩
    crash                       ∎

  -- Thus these programs all terminate (unsuccessfully) in zero steps.

  steps⟦t⟧∼0 : ∀ {i} n → Conat.[ i ] steps (⟦ t n ⟧ []) ∼ zero
  steps⟦t⟧∼0 = steps-cong ∘ ⟦t⟧∼crash

  -- However, running the compiled program corresponding to t n on the
  -- virtual machine takes 3 + n steps.

  steps-exec-t∼ :
    ∀ {i} n →
    Conat.[ i ] steps (exec ⟨ comp₀ (t n) , [] , [] ⟩) ∼ ⌜ 3 + n ⌝
  steps-exec-t∼ = lemma
    where
    lemma :
      ∀ {i c s} n →
      Conat.[ i ] steps (exec ⟨ comp false (t n) c , s , [] ⟩) ∼
                  ⌜ 3 + n ⌝
    lemma zero    = suc λ { .force →
                    suc λ { .force →
                    suc λ { .force →
                    zero }}}
    lemma (suc n) = suc λ { .force → lemma n }

max_stars_repo_name: nad/definitional-interpreters

max_issues_repo_name: nad/definitional-interpreters

max_forks_repo_name: nad/definitional-interpreters


text:
open import Common.Prelude

test : Bool → Nat
test = if_then 4 Common.Prelude.else 5

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------------
-- Totality properties of the division
------------------------------------------------------------------------------

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

module LTC-PCF.Program.Division.Totality where

open import LTC-PCF.Base
open import LTC-PCF.Data.Nat
open import LTC-PCF.Data.Nat.Inequalities
open import LTC-PCF.Program.Division.ConversionRules
open import LTC-PCF.Program.Division.Division
open import LTC-PCF.Program.Division.Specification

------------------------------------------------------------------------------
-- The division is total when the dividend is less than the divisor.
div-x<y-N : ∀ {i j} → i < j → N (div i j)
div-x<y-N i<j = subst N (sym (div-x<y i<j)) nzero

-- The division is total when the dividend is greater or equal than
-- the divisor.

--  N (div (i ∸ j) j)       i ≮ j → div i j ≡ succ (div (i ∸ j) j)
------------------------------------------------------------------
--                   N (div i j)

div-x≮y-N : ∀ {i j} →
            (divSpec (i ∸ j) j (div (i ∸ j) j)) →
            i ≮ j →
            N (div i j)
div-x≮y-N ih i≮j = subst N (sym (div-x≮y i≮j)) (nsucc (∧-proj₁ ih))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
module sn-calculus where

open import utility

open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.Properties
open import Esterel.Lang.CanFunction
  using (Canθₛ ; Canθₛₕ ; [S]-env)
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; sig ; []env ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.Context
  using (EvaluationContext ; EvaluationContext1 ; _⟦_⟧e ; _≐_⟦_⟧e ;
         Context ; Context1 ; _⟦_⟧c ; _≐_⟦_⟧c)
open import Esterel.Variable.Signal as Signal
  using (Signal)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar)
open import Esterel.Context.Properties

open import Relation.Nullary
  using (¬_)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; refl ; cong ; sym)
open import Data.Empty
  using (⊥ ; ⊥-elim)
import Data.FiniteMap
open import Data.List
  using (List ; _∷_ ; [])
open import Data.List.All as All
  using (All ; _∷_ ; [])
open import Data.Nat
  using (ℕ ; zero ; suc ; _+_)
open import Data.Product
  using (Σ-syntax ; Σ ; _,_ ; proj₁ ; proj₂ ; _×_ ; _,′_)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)

open _≐_⟦_⟧e
open _≐_⟦_⟧c

open EvaluationContext1
open Context1

infix 4 _sn⟶₁_
infix 4 _sn⟶_
infix 4 _sn⟶*_

-- The environment created by rraise-signal rule
-- [S]-env, is defined in Esterel.Lang.CanFunction
-- It's simply Θ SigMap.[ S ↦ Signal.unknown ] ShrMap.empty VarMap.empty

-- The environment created by rraise-shared rule
[s,δe]-env : (s : SharedVar) → (v : ℕ) → Env
[s,δe]-env s δe' =
  Θ SigMap.empty
    ShrMap.[ s ↦ (SharedVar.old ,′ δe') ]
    VarMap.empty

-- The environment created by rraise-var rule
[x,δe]-env : (x : SeqVar) → (v : ℕ) → Env
[x,δe]-env x δe' =
  Θ SigMap.empty ShrMap.empty VarMap.[ x ↦ δe' ]

[s,δe-new]-env : (s : SharedVar) → (v : ℕ) → Env
[s,δe-new]-env s δe' =
  Θ SigMap.empty
    ShrMap.[ s ↦ (SharedVar.new ,′ δe') ]
    VarMap.empty

data bound-ready : Env → s/l → Set where
  brnum : ∀{θ n} → bound-ready θ (num n)
  brseq : ∀{θ x} → (Env.isVar∈ x θ) → bound-ready θ (seq-ref x)
  brshr : ∀{θ s} →
    (s∈ : (Env.isShr∈ s θ)) →
    Env.shr-stats{s} θ s∈ ≡ SharedVar.ready →
    bound-ready θ (shr-ref s)

data all-ready : Expr → Env → Set where
  aplus : ∀{θ operators} → All (bound-ready θ) operators → all-ready (plus operators) θ

δ : ∀{e θ} → all-ready e θ → ℕ
δ {(plus [])}              {θ} (aplus [])                 = 0
δ {(plus (num n     ∷ _))} {θ} (aplus (brnum      ∷ ops)) = n + δ (aplus ops)
δ {(plus (seq-ref x ∷ _))} {θ} (aplus (brseq x∈   ∷ ops)) = Env.var-vals{x} θ x∈ + δ (aplus ops)
δ {(plus (shr-ref s ∷ _))} {θ} (aplus (brshr s∈ _ ∷ ops)) = Env.shr-vals{s} θ s∈ + δ (aplus ops)

δ-e-irr : ∀{e θ} →  (e' : all-ready e θ) → (e'' : all-ready e θ) → δ e' ≡ δ e''
δ-e-irr {plus []} (aplus []) (aplus []) = refl
δ-e-irr {plus ((num n) ∷ x₁)} (aplus (brnum ∷ x₂)) (aplus (brnum ∷ x₃))
   = cong (_+_ n)  (δ-e-irr (aplus x₂) (aplus x₃))
δ-e-irr {plus ((seq-ref x) ∷ x₁)}{θ} (aplus (brseq x₂ ∷ x₃)) (aplus (brseq x₄ ∷ x₅))
  with Env.var-vals-∈-irr{x}{θ} x₂ x₄
... | k rewrite sym k =  (cong (_+_ (Env.var-vals{x} θ x₂)) (δ-e-irr (aplus x₃) (aplus x₅)))
δ-e-irr {plus ((shr-ref s) ∷ x₁)}{θ} (aplus (brshr s∈ x ∷ x₂)) (aplus (brshr s∈₁ x₃ ∷ x₄))
   with Env.shr-vals-∈-irr{s}{θ} s∈ s∈₁
... | k rewrite sym k = cong (_+_ (Env.shr-vals{s} θ s∈)) (δ-e-irr (aplus x₂) (aplus x₄))

{-
  In the current formalization, for reduction rules involving evaluation
  contexts, we will write them in the following form to enable pattern
  matching on p:

  (r ≐ E ⟦ p ⟧e) → (something r sn⟶₁ something E ⟦ p'⟧)
-}

{- this relation is the strongly normalizing subset of
   the calculus. It is just like _⟶₁_ in calculus.agda,
   but without the [par-swap] constructor. -}

data _sn⟶₁_ : Term → Term → Set where
  rpar-done-right : ∀{p q} →
    (p' : halted p) →
    (q' : done q) →
    (p ∥ q) sn⟶₁ (value-max (dhalted p') q' (inj₁ p'))

  rpar-done-left : ∀{p q} →
    (p' : done p) →
    (q' : halted q) →
    (p ∥ q) sn⟶₁ (value-max p' (dhalted q') (inj₂ q'))

  ris-present : ∀{θ S r p q E A} →
    (S∈ : (Env.isSig∈ S θ)) →
    Env.sig-stats{S} θ S∈ ≡ Signal.present →
    r ≐ E ⟦ present S ∣⇒ p ∣⇒ q ⟧e →
    (ρ⟨ θ , A ⟩· r) sn⟶₁ (ρ⟨ θ , A ⟩· E ⟦ p ⟧e)

  ris-absent : ∀{θ S r p q E A} →
    (S∈ : (Env.isSig∈ S θ)) →
    Env.sig-stats{S} θ S∈ ≡ Signal.absent →
    r ≐ E ⟦ present S ∣⇒ p ∣⇒ q ⟧e →
    (ρ⟨ θ , A ⟩· r) sn⟶₁ (ρ⟨ θ , A ⟩· E ⟦ q ⟧e)

  remit : ∀{θ r S E} →
    (S∈ : (Env.isSig∈ S θ)) →
    (¬S≡a : ¬ (Env.sig-stats{S} θ S∈) ≡ Signal.absent) →
    r ≐ E ⟦ emit S ⟧e →
    (ρ⟨ θ , GO ⟩· r) sn⟶₁
    (ρ⟨ (Env.set-sig{S} θ S∈ Signal.present) , GO ⟩·
      E ⟦ nothin ⟧e)

  rloop-unroll : ∀{p} →
    (loop p)
    sn⟶₁
    (loopˢ p p)

  rseq-done : ∀{q} →
    (nothin >> q) sn⟶₁ q

  rseq-exit : ∀{q n} →
    (exit n >> q) sn⟶₁ (exit n)

  rloopˢ-exit : ∀{q n} →
    (loopˢ (exit n) q) sn⟶₁ (exit n)

  rsuspend-done : ∀{p S} →
    halted p →
    (suspend p S) sn⟶₁ p

  -- traps
  rtrap-done : ∀{p} →
    (p' : halted p) →
    (trap p) sn⟶₁ (↓ p')

  -- lifting signals
  rraise-signal : ∀{p S} →
    (signl S p) sn⟶₁
    (ρ⟨ (Θ SigMap.[ S ↦ Signal.unknown ] ShrMap.empty VarMap.empty) , WAIT ⟩·
      p)

  -- shared state
  rraise-shared : ∀{θ r s e p E A} →
    (e' : all-ready e θ) →
    r ≐ E ⟦ shared s ≔ e in: p ⟧e →
    (ρ⟨ θ , A ⟩· r) sn⟶₁
    (ρ⟨ θ , A ⟩·
      E ⟦ (ρ⟨ [s,δe]-env s (δ e') , WAIT ⟩· p) ⟧e)

  rset-shared-value-old : ∀{θ r s e E} →
    (e' : all-ready e θ) →
    (s∈ : (Env.isShr∈ s θ)) →
    Env.shr-stats{s} θ s∈ ≡ SharedVar.old →
    r ≐ E ⟦ s ⇐ e ⟧e →
    (ρ⟨ θ , GO ⟩· r) sn⟶₁
    (ρ⟨ (Env.set-shr{s} θ s∈ (SharedVar.new) (δ e')) , GO ⟩·
      E ⟦ nothin ⟧e)

  rset-shared-value-new : ∀{θ r s e E} →
    (e' : all-ready e θ) →
    (s∈ : (Env.isShr∈ s θ)) →
    Env.shr-stats{s} θ s∈ ≡ SharedVar.new →
    r ≐ E ⟦ s ⇐ e ⟧e →
    (ρ⟨ θ , GO ⟩· r) sn⟶₁
    (ρ⟨ (Env.set-shr{s} θ s∈ (SharedVar.new) (Env.shr-vals{s} θ s∈ + δ e')) , GO ⟩·
      E ⟦ nothin ⟧e)

  -- unshared state
  rraise-var : ∀{θ r x p e E A} →
    (e' : all-ready e θ) →
    r ≐ E ⟦ var x ≔ e in: p ⟧e →
    (ρ⟨ θ , A ⟩· r) sn⟶₁
    (ρ⟨ θ , A ⟩·
      E ⟦ (ρ⟨ [x,δe]-env x (δ e') , WAIT ⟩· p) ⟧e)

  rset-var : ∀{θ r x e E A} →
    (x∈ : (Env.isVar∈ x θ)) →
    (e' : all-ready e θ) →
    r ≐ E ⟦ x ≔ e ⟧e →
    (ρ⟨ θ , A ⟩· r) sn⟶₁
    (ρ⟨ (Env.set-var{x} θ x∈ (δ e')) , A ⟩·
      E ⟦ nothin ⟧e)

  -- if
  rif-false : ∀{θ r p q x E A} →
    (x∈ : (Env.isVar∈ x θ)) →
    Env.var-vals{x} θ x∈ ≡ zero →
    r ≐ E ⟦ if x ∣⇒ p ∣⇒ q ⟧e →
    (ρ⟨ θ , A ⟩· r) sn⟶₁ (ρ⟨ θ , A ⟩· E ⟦ q ⟧e)

  rif-true : ∀{θ r p q x E n A} →
    (x∈ : (Env.isVar∈ x θ)) →
    Env.var-vals{x} θ x∈ ≡ suc n →
    r ≐ E ⟦ if x ∣⇒ p ∣⇒ q ⟧e →
    (ρ⟨ θ , A ⟩· r) sn⟶₁ (ρ⟨ θ , A ⟩· E ⟦ p ⟧e)

  -- progression
  {-
    Thoughts:
    * These two rules are expressed differently to the definition in model/shared.rkt
      for simplicity. Instead of being more 'computative', the definition here is
      more 'declarative'. Keep an eye on the original definition to make sure that
      they are equivalent.
  -}
  rabsence : ∀{θ p S A} →
    (S∈ : (Env.isSig∈ S θ)) →
    Env.sig-stats{S} θ S∈ ≡ Signal.unknown →
    (Signal.unwrap S) ∉ Canθₛ (sig θ) 0 p []env →
    (ρ⟨ θ , A ⟩· p) sn⟶₁
    (ρ⟨ (Env.set-sig{S} θ S∈ (Signal.absent)) , A ⟩·
      p)

  rreadyness : ∀{θ p s A} →
    (s∈ : (Env.isShr∈ s θ)) →
    (Env.shr-stats{s} θ s∈ ≡ SharedVar.old) ⊎ (Env.shr-stats{s} θ s∈ ≡ SharedVar.new) →
    (SharedVar.unwrap s) ∉ Canθₛₕ (sig θ) 0 p []env →
    (ρ⟨ θ , A ⟩· p) sn⟶₁
    (ρ⟨ (Env.set-shr{s} θ s∈ (SharedVar.ready) (Env.shr-vals{s} θ s∈)) , A ⟩·
      p)

  rmerge : ∀{θ₁ θ₂ r p E A₁ A₂} →
    r ≐ E ⟦ ρ⟨ θ₂ , A₂ ⟩· p ⟧e →
    (ρ⟨ θ₁ , A₁ ⟩· r) sn⟶₁ (ρ⟨ (θ₁ ← θ₂) , (A-max A₁ A₂) ⟩· E ⟦ p ⟧e)

-- The compatible closure of _sn⟶₁_.
data _sn⟶_ : Term → Term → Set where
  rcontext : ∀{r p p'} →
    (C : Context) →
    (dc : r ≐ C ⟦ p ⟧c) →
    (psn⟶₁p' : p sn⟶₁ p') →
    r sn⟶ (C ⟦ p' ⟧c)

sn⟶-inclusion : ∀{p q} → p sn⟶₁ q → p sn⟶ q
sn⟶-inclusion psn⟶₁q = rcontext [] dchole psn⟶₁q

data _sn⟶*_ : Term → Term → Set where
  rrefl : ∀{p} → (p sn⟶* p)
  rstep : ∀{p q r} → (psn⟶q : p sn⟶ q) → (qsn⟶*r : q sn⟶* r) → (p sn⟶* r)

sn⟶*-inclusion : ∀{p q} → p sn⟶ q → p sn⟶* q
sn⟶*-inclusion psn⟶q = rstep psn⟶q rrefl

data _sn≡ₑ_ : Term → Term → Set where
  rstp : ∀{p q} → (psn⟶q : p sn⟶ q) → p sn≡ₑ q
  rsym : ∀{p q BV FV} → (psn≡ₑq : p sn≡ₑ q) → (CBp : CorrectBinding p BV FV) → q sn≡ₑ p
  rref : ∀{p} → p sn≡ₑ p
  rtrn : ∀{p q r} → (psn≡ₑr : p sn≡ₑ r) → (rsn≡ₑq : r sn≡ₑ q) → p sn≡ₑ q

-- rstep, reversed: walk many steps first then walk one step
rpets : ∀ {p q r} → p sn⟶* q → q sn⟶ r → p sn⟶* r
rpets rrefl qsn⟶r = sn⟶*-inclusion qsn⟶r
rpets (rstep psn⟶s ssn⟶*q) qsn⟶r = rstep psn⟶s (rpets ssn⟶*q qsn⟶r)

{-
Properties relating halted, paused, done programs and the reduction relation.
* Halted, paused and done programs do not reduce under the original reduction relation _sn⟶₁_.
    halted-¬sn⟶₁ : ∀{p p'} → halted p → ¬ p sn⟶₁ p'
    paused-¬sn⟶₁ : ∀{p p'} → paused p → ¬ p sn⟶₁ p'
    done-¬sn⟶₁ : ∀{p p'} → done p → ¬ p sn⟶₁ p'
* Halted programs do not reduce under the compatible closure relation _sn⟶_.
    halted-¬sn⟶ : ∀{p p'} → halted p → ¬ p sn⟶ p'
* Paused programs remain paused under the compatible closure relation _sn⟶_.
    paused-sn⟶ : ∀{p p'} → paused p → p sn⟶ p' → paused p'
-}
halted-¬sn⟶₁ : ∀{p p'} → halted p → ¬ p sn⟶₁ p'
halted-¬sn⟶₁ hnothin ()
halted-¬sn⟶₁ (hexit n) ()

paused-¬sn⟶₁ : ∀{p p'} → paused p → ¬ p sn⟶₁ p'
paused-¬sn⟶₁ ppause ()
paused-¬sn⟶₁ (pseq ()) rseq-done
paused-¬sn⟶₁ (pseq ()) rseq-exit
paused-¬sn⟶₁ (ploopˢ ppause) ()
paused-¬sn⟶₁ (ploopˢ (pseq a)) ()
paused-¬sn⟶₁ (ploopˢ (ppar a a₁)) ()
paused-¬sn⟶₁ (ploopˢ (psuspend a)) ()
paused-¬sn⟶₁ (ploopˢ (ptrap a)) ()
paused-¬sn⟶₁ (ploopˢ (ploopˢ a)) ()
paused-¬sn⟶₁ (ppar paused₁ paused₂) (rpar-done-right p' q') =
  halted-paused-disjoint p' paused₁
paused-¬sn⟶₁ (ppar paused₁ paused₂) (rpar-done-left p' q') =
  halted-paused-disjoint q' paused₂
paused-¬sn⟶₁ (psuspend paused) (rsuspend-done halted) =
  halted-paused-disjoint halted paused
paused-¬sn⟶₁ (ptrap paused) (rtrap-done halted) =
  halted-paused-disjoint halted paused

done-¬sn⟶₁ : ∀{p p'} → done p → ¬ p sn⟶₁ p'
done-¬sn⟶₁ (dhalted halted) psn⟶₁p' = halted-¬sn⟶₁ halted psn⟶₁p'
done-¬sn⟶₁ (dpaused paused) psn⟶₁p' = paused-¬sn⟶₁ paused psn⟶₁p'

halted-¬sn⟶ : ∀{p p'} → halted p → ¬ p sn⟶ p'
halted-¬sn⟶ halted (rcontext C dc psn⟶₁p') =
  halted-¬sn⟶₁ (halted-⟦⟧c halted dc) psn⟶₁p'

paused-sn⟶ : ∀{p p'} → paused p → p sn⟶ p' → paused p'
paused-sn⟶ ppause                 (rcontext _ dchole psn⟶₁p') =
  ⊥-elim (paused-¬sn⟶₁ ppause psn⟶₁p')
paused-sn⟶ (pseq paused)          (rcontext _ dchole psn⟶₁p') =
  ⊥-elim (paused-¬sn⟶₁ (pseq paused) psn⟶₁p')
paused-sn⟶ (ppar paused₁ paused₂) (rcontext _ dchole psn⟶₁p') =
  ⊥-elim (paused-¬sn⟶₁ (ppar paused₁ paused₂) psn⟶₁p')
paused-sn⟶ (psuspend paused)      (rcontext _ dchole psn⟶₁p') =
  ⊥-elim (paused-¬sn⟶₁ (psuspend paused) psn⟶₁p')
paused-sn⟶ (ptrap paused)         (rcontext _ dchole psn⟶₁p') =
  ⊥-elim (paused-¬sn⟶₁ (ptrap paused) psn⟶₁p')
paused-sn⟶ (ploopˢ paused)          (rcontext _ dchole psn⟶₁p') =
  ⊥-elim (paused-¬sn⟶₁ (ploopˢ paused) psn⟶₁p')
paused-sn⟶ (ploopˢ paused)          (rcontext _ (dcloopˢ₁ dc) psn⟶₁p') =
  ploopˢ (paused-sn⟶ paused (rcontext _ dc psn⟶₁p'))
paused-sn⟶ (ploopˢ paused)          (rcontext _ (dcloopˢ₂ dc) psn⟶₁p') =
  ploopˢ paused
paused-sn⟶ (pseq paused)          (rcontext _ (dcseq₁ dc) psn⟶₁p') =
  pseq (paused-sn⟶ paused (rcontext _ dc psn⟶₁p'))
paused-sn⟶ (pseq paused)          (rcontext _ (dcseq₂ dc) psn⟶₁p') =
  pseq paused
paused-sn⟶ (ppar paused₁ paused₂) (rcontext _ (dcpar₁ dc) psn⟶₁p') =
  ppar (paused-sn⟶ paused₁ (rcontext _ dc psn⟶₁p')) paused₂
paused-sn⟶ (ppar paused₁ paused₂) (rcontext _ (dcpar₂ dc) psn⟶₁p') =
  ppar paused₁ (paused-sn⟶ paused₂ (rcontext _ dc psn⟶₁p'))
paused-sn⟶ (psuspend paused)      (rcontext _ (dcsuspend dc) psn⟶₁p') =
  psuspend (paused-sn⟶ paused (rcontext _ dc psn⟶₁p'))
paused-sn⟶ (ptrap paused)         (rcontext _ (dctrap dc) psn⟶₁p') =
  ptrap (paused-sn⟶ paused (rcontext _ dc psn⟶₁p'))

done-sn⟶ : ∀{p q} → done p → p sn⟶ q → done q
done-sn⟶ (dhalted p/halted) psn⟶q = ⊥-elim (halted-¬sn⟶ p/halted psn⟶q)
done-sn⟶ (dpaused p/paused) psn⟶q = dpaused (paused-sn⟶ p/paused psn⟶q)

Context1-sn⟶ : ∀{p p'} → (C1 : Context1) → p sn⟶ p' → (C1 ∷ []) ⟦ p ⟧c sn⟶ (C1 ∷ []) ⟦ p' ⟧c
Context1-sn⟶ (ceval (epar₁ q)) (rcontext C dc psn⟶₁p') =
  rcontext (ceval (epar₁ q) ∷ C) (dcpar₁ dc) psn⟶₁p'
Context1-sn⟶ (ceval (epar₂ p₁)) (rcontext C dc psn⟶₁p') =
  rcontext (ceval (epar₂ p₁) ∷ C) (dcpar₂ dc) psn⟶₁p'
Context1-sn⟶ (ceval (eseq q)) (rcontext C dc psn⟶₁p') =
  rcontext (ceval (eseq q) ∷ C) (dcseq₁ dc) psn⟶₁p'
Context1-sn⟶ (ceval (eloopˢ q)) (rcontext C dc psn⟶₁p') =
  rcontext (ceval (eloopˢ q) ∷ C) (dcloopˢ₁ dc) psn⟶₁p'
Context1-sn⟶ (ceval (esuspend S)) (rcontext C dc psn⟶₁p') =
  rcontext (ceval (esuspend S) ∷ C) (dcsuspend dc) psn⟶₁p'
Context1-sn⟶ (ceval etrap) (rcontext C dc psn⟶₁p') =
  rcontext (ceval etrap ∷ C) (dctrap dc) psn⟶₁p'
Context1-sn⟶ (csignl S) (rcontext C dc psn⟶₁p') =
  rcontext (csignl S ∷ C) (dcsignl dc) psn⟶₁p'
Context1-sn⟶ (cpresent₁ S q)(rcontext C dc psn⟶₁p') =
  rcontext (cpresent₁ S q ∷ C) (dcpresent₁ dc) psn⟶₁p'
Context1-sn⟶ (cpresent₂ S p') (rcontext C dc psn⟶₁p') =
  rcontext (cpresent₂ S p' ∷ C) (dcpresent₂ dc) psn⟶₁p'
Context1-sn⟶ (cloop) (rcontext C dc psn⟶₁p') =
  rcontext (cloop ∷ C) (dcloop dc) psn⟶₁p'
Context1-sn⟶ (cloopˢ₂ p) (rcontext C dc psn⟶₁p') =
  rcontext (cloopˢ₂ p ∷ C) (dcloopˢ₂ dc) psn⟶₁p'
Context1-sn⟶ (cseq₂ p') (rcontext C dc psn⟶₁p') =
  rcontext (cseq₂ p' ∷ C) (dcseq₂ dc) psn⟶₁p'
Context1-sn⟶ (cshared s e) (rcontext C dc psn⟶₁p') =
  rcontext (cshared s e ∷ C) (dcshared dc) psn⟶₁p'
Context1-sn⟶ (cvar x e) (rcontext C dc psn⟶₁p') =
  rcontext (cvar x e ∷ C) (dcvar dc) psn⟶₁p'
Context1-sn⟶ (cif₁ x q) (rcontext C dc psn⟶₁p') =
  rcontext (cif₁ x q ∷ C) (dcif₁ dc) psn⟶₁p'
Context1-sn⟶ (cif₂ x p') (rcontext C dc psn⟶₁p') =
  rcontext (cif₂ x p' ∷ C) (dcif₂ dc) psn⟶₁p'
Context1-sn⟶ (cenv θ A) (rcontext C dc psn⟶₁p') =
  rcontext (cenv θ A ∷ C) (dcenv dc) psn⟶₁p'

Context1-sn⟶* : ∀{p p'} → (C1 : Context1) → p sn⟶* p' → (C1 ∷ []) ⟦ p ⟧c sn⟶* (C1 ∷ []) ⟦ p' ⟧c
Context1-sn⟶* C1 rrefl                 = rrefl
Context1-sn⟶* C1 (rstep psn⟶p' p'sn⟶*p'') = rstep (Context1-sn⟶ C1 psn⟶p') (Context1-sn⟶* C1 p'sn⟶*p'')

-- Unused helper function: compatible context append for _sn⟶_
-- We can't just give r sn⟶ C ⟦ p' ⟧c as the result since we can't pattern match on it
Context-sn⟶ : ∀{r p p'} →
  (C : Context) → r ≐ C ⟦ p ⟧c → p sn⟶ p' →
  Σ[ r' ∈ Term ] (r' ≐ C ⟦ p' ⟧c) × (r sn⟶ r')
Context-sn⟶ [] dchole psn⟶p' =
  _ , dchole ,′ psn⟶p'
Context-sn⟶ (_ ∷ C) (dcpar₁ dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcpar₁ dc₂ ,′ rcontext _ (dcpar₁ dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dcpar₂ dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcpar₂ dc₂ ,′ rcontext _ (dcpar₂ dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dcseq₁ dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcseq₁ dc₂ ,′ rcontext _ (dcseq₁ dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dcseq₂ dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcseq₂ dc₂ ,′ rcontext _ (dcseq₂ dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dcsuspend dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcsuspend dc₂ ,′ rcontext _ (dcsuspend dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dctrap dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dctrap dc₂ ,′ rcontext _ (dctrap dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dcsignl dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcsignl dc₂ ,′ rcontext _ (dcsignl dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dcpresent₁ dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcpresent₁ dc₂ ,′ rcontext _ (dcpresent₁ dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dcpresent₂ dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcpresent₂ dc₂ ,′ rcontext _ (dcpresent₂ dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dcloop dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcloop dc₂ ,′ rcontext _ (dcloop dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dcloopˢ₁ dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcloopˢ₁ dc₂ ,′ rcontext _ (dcloopˢ₁ dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dcloopˢ₂ dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcloopˢ₂ dc₂ ,′ rcontext _ (dcloopˢ₂ dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dcshared dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcshared dc₂ ,′ rcontext _ (dcshared dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dcvar dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcvar dc₂ ,′ rcontext _ (dcvar dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dcif₁ dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcif₁ dc₂ ,′ rcontext _ (dcif₁ dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dcif₂ dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcif₂ dc₂ ,′ rcontext _ (dcif₂ dc') psn⟶₁p'
Context-sn⟶ (_ ∷ C) (dcenv dc₁) psn⟶p' with Context-sn⟶ C dc₁ psn⟶p'
... | _ , dc₂ , rcontext _ dc' psn⟶₁p' =
  _ , dcenv dc₂ ,′ rcontext _ (dcenv dc') psn⟶₁p'

Context-sn⟶⟦⟧ : ∀{p q} → (C : Context) → p sn⟶ q → ((C ⟦ p ⟧c) sn⟶ (C ⟦ q ⟧c))
Context-sn⟶⟦⟧{p}  C psn⟶q with Context-sn⟶{r = C ⟦ p ⟧c} C Crefl psn⟶q
... | (r' , r=C⟦q⟧ , rsn⟶r') rewrite unplugc r=C⟦q⟧ = rsn⟶r'

Context-sn⟶* : ∀{p q} → (C : Context) → p sn⟶* q → (C ⟦ p ⟧c) sn⟶* (C ⟦ q ⟧c)
Context-sn⟶* C rrefl = rrefl
Context-sn⟶* C₁ (rstep C→ psn⟶*q) = (rstep (Context-sn⟶⟦⟧ C₁ C→) (Context-sn⟶* C₁ psn⟶*q))

sn⟶*+ : ∀{p q r} → p sn⟶* r → r sn⟶* q → p sn⟶* q
sn⟶*+ rrefl rsn⟶*q = rsn⟶*q
sn⟶*+ (rstep x psn⟶*r) rsn⟶*q = rstep x (sn⟶*+ psn⟶*r rsn⟶*q)

ρ-stays-ρ-sn⟶₁ : ∀{θ p q A} → (ρ⟨ θ , A ⟩· p) sn⟶₁ q → Σ[ θ' ∈ Env.Env ] Σ[ qin ∈ Term ] Σ[ A' ∈ Ctrl ] q ≡ (ρ⟨ θ' , A' ⟩· qin)
ρ-stays-ρ-sn⟶₁ {θ} {A = A} (ris-present{p = p}{E = E} S∈ x x₁) = θ , E ⟦ p ⟧e , A , refl
ρ-stays-ρ-sn⟶₁ {θ} {A = A} (ris-absent{q = q}{E = E} S∈ x x₁) = θ , E ⟦ q ⟧e , A , refl
ρ-stays-ρ-sn⟶₁ {θ} {A = A} (remit{S = S}{E = E} S∈ _ x) = (Env.set-sig{S} θ S∈ Signal.present) , E ⟦ nothin ⟧e , A , refl
ρ-stays-ρ-sn⟶₁ {θ} {A = A} (rraise-shared{s = s}{p = p}{E = E} e' x) = θ , (E ⟦ (ρ⟨ (Θ SigMap.empty ShrMap.[ s ↦ (SharedVar.old ,′ (δ e'))] VarMap.empty) , WAIT ⟩· p) ⟧e) , A , refl
ρ-stays-ρ-sn⟶₁ {θ} {A = A} (rset-shared-value-old{s = s}{E = E} e' s∈ x x₁) = (Env.set-shr{s} θ s∈ (SharedVar.new) (δ e')) , E ⟦ nothin ⟧e , A , refl
ρ-stays-ρ-sn⟶₁ {θ} {A = A} (rset-shared-value-new{s = s}{E = E} e' s∈ x x₁) = (Env.set-shr{s} θ s∈ (SharedVar.new) (Env.shr-vals{s} θ s∈ + δ e')) , E ⟦ nothin ⟧e , A , refl
ρ-stays-ρ-sn⟶₁ {θ} {A = A} (rraise-var{x = x}{p = p}{E = E} e' x₁) = θ , (E ⟦ (ρ⟨ (Θ SigMap.empty ShrMap.empty VarMap.[ x ↦ δ e' ]) , WAIT ⟩· p) ⟧e) , A , refl
ρ-stays-ρ-sn⟶₁ {θ} {A = A} (rset-var{x = x}{E = E} x∈ e' x₁) = (Env.set-var{x} θ x∈ (δ e')) , E ⟦ nothin ⟧e , A , refl
ρ-stays-ρ-sn⟶₁ {θ} {A = A} (rif-false{q = q}{E = E} x∈ x₁ x₂) = θ , E ⟦ q ⟧e , A , refl
ρ-stays-ρ-sn⟶₁ {θ} {A = A} (rif-true{p = p}{E = E} x∈ x₁ x₂) = θ , E ⟦ p ⟧e , A , refl
ρ-stays-ρ-sn⟶₁ {θ} {A = A} (rabsence{.θ}{p}{S} S∈ x x₁) = (Env.set-sig{S} θ S∈ (Signal.absent)) , p , A , refl
ρ-stays-ρ-sn⟶₁ {θ} {A = A} (rreadyness{.θ}{p}{s} s∈ x x₁) = (Env.set-shr{s} θ s∈ (SharedVar.ready) (Env.shr-vals{s} θ s∈)) , p , A , refl
ρ-stays-ρ-sn⟶₁ {θ} (rmerge{θ₁}{θ₂}{r}{p}{E}{A₁}{A₂} x) =  (θ₁ ← θ₂) , E ⟦ p ⟧e , (A-max A₁ A₂) , refl

ρ-stays-ρ-sn⟶ : ∀{θ p q A} → (ρ⟨ θ , A ⟩· p) sn⟶ q → Σ[ θ' ∈ Env.Env ] Σ[ qin ∈ Term ] Σ[ A' ∈ Ctrl ] q ≡ (ρ⟨ θ' , A' ⟩· qin)
ρ-stays-ρ-sn⟶ (rcontext .[] dchole psn⟶₁p') = ρ-stays-ρ-sn⟶₁ psn⟶₁p'
ρ-stays-ρ-sn⟶ (rcontext .(cenv _ _ ∷ _) (dcenv dc) psn⟶₁p') = _ , _ , _ , refl

ρ-stays-ρ-sn⟶* : ∀{θ p q A} → (ρ⟨ θ , A ⟩· p) sn⟶* q → Σ[ θ' ∈ Env.Env ] Σ[ qin ∈ Term ] Σ[ A ∈ Ctrl ] q ≡ (ρ⟨ θ' , A ⟩· qin)
ρ-stays-ρ-sn⟶* rrefl = _ , _ , _ , refl
ρ-stays-ρ-sn⟶* (rstep x psn⟶*q) rewrite proj₂ (proj₂ (proj₂ (ρ-stays-ρ-sn⟶ x))) = ρ-stays-ρ-sn⟶* psn⟶*q

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
module Lambda where

open import Prelude

-- Simply typed λ-calculus

infixr 70 _⟶_

data Type : Set where
  ι   : Type
  _⟶_ : Type -> Type -> Type

Ctx : Set
Ctx = List Type

infixl 80 _•_
infix  20  ƛ_

data Term : Ctx -> Type -> Set where
  vz  : forall {Γ τ  } -> Term (Γ , τ) τ
  wk  : forall {Γ σ τ} -> Term Γ τ -> Term (Γ , σ) τ
  _•_ : forall {Γ σ τ} -> Term Γ (σ ⟶ τ) -> Term Γ σ -> Term Γ τ
  ƛ_  : forall {Γ σ τ} -> Term (Γ , σ) τ -> Term Γ (σ ⟶ τ)

Terms : Ctx -> Ctx -> Set
Terms Γ Δ = All (Term Γ) Δ

infixl 60 _◄_
infixr 70 _⇒_

_⇒_ : Ctx -> Type -> Type
ε       ⇒ τ = τ
(Δ , σ) ⇒ τ = Δ ⇒ σ ⟶ τ

infixl 80 _•ˢ_

_•ˢ_ : {Γ Δ : Ctx}{τ : Type} -> Term Γ (Δ ⇒ τ) -> Terms Γ Δ -> Term Γ τ
t •ˢ ∅        = t
t •ˢ (us ◄ u) = t •ˢ us • u

Var : Ctx -> Type -> Set
Var Γ τ = τ ∈ Γ

var : forall {Γ τ} -> Var Γ τ -> Term Γ τ
var hd     = vz
var (tl x) = wk (var x)

vzero : forall {Γ τ} -> Var (Γ , τ) τ
vzero = hd

vsuc : forall {Γ σ τ} -> Var Γ τ -> Var (Γ , σ) τ
vsuc = tl


text:
-- Andreas, 2016-06-13 issue #2027: Unbound variables in pattern synonyms
-- Quiz by Ulf

postulate Nat : Set

pattern hm = x
-- This pattern synonym should fail with a message like
-- Unbound variables in pattern synonym:  x

quiz₁ : Nat → Nat → Nat
quiz₁ hm hm = hm

quiz₂ : Nat → Nat
quiz₂ x = hm

quiz₃ : Nat → Nat
quiz₃ hm = x
-- OLD ERROR: Not in scope: x


text:
-- This is the preferred version of the integers in the library. Other
-- versions can be found in the MoreInts directory.
{-# OPTIONS --safe #-}
module Cubical.Data.Int where

open import Cubical.Data.Int.Base public
open import Cubical.Data.Int.Properties public

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
-- Andreas, 2014-05-08
-- Reported by guillaume.brunerie, Yesterday

{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.cc:25 -v reduce.compiled:95 #-}
-- {-# OPTIONS --show-implicit -v tc.inj:30 -v tc.conv:20 -v tc.meta.assign:10 #-}

-- The code below gives the following odd error:

-- > Incomplete pattern matching when applying Cubical._.C

-- The definition of [C] by pattern matching does not seem incomplete, but even if it were, it should be detected when type checking [C], not when using it (!).
-- The last definition [test] is the one triggering the error, if you comment it then everything typechecks.

record Unit : Set where
  constructor unit

data _==_ {i} {A : Set i} (a : A) : A → Set where
  idp : a == a

data Nat : Set where
  O : Nat
  S : Nat → Nat

record BS (B : Set) (C : B → Set) : Set where
  constructor bs
  field
    {b₁ b₂} : B
    c₁ : C b₁
    c₂ : C b₂
    p : b₁ == b₂

postulate A : Set

B : Nat → Set
C : (n : Nat) → B n → Set

B O = Unit
B (S n) = BS (B n) (C n)

-- No bug if no match on unit
-- C O _ = A
C O unit = A
C (S n) (bs {b₁} c₁ c₂ idp) = _==_ {A = _} c₁ c₂

-- Due to a bug in TypeChecking.Patterns.Match
-- a failed match of (C n b) against (C O unit)
-- turned into (C n unit).
-- This was because all patterns were matched in
-- parallel, and evaluations of successfull matches
-- (and a record constructor like unit can always
-- be successfully matched) were returned, leading
-- to a reassembly of (C n b) as (C n unit) which is
-- illtyped.

-- Now patterns are matched left to right and
-- upon failure, no further matching is performed.

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B
open _×_ public

PathOver : {A : Set} (B : A → Set)
  {x y : A} (p : x == y) (u : B x) (v : B y) → Set
PathOver B idp u v = (u == v)

syntax PathOver B p u v =
  u == v [ B ↓ p ]

pair×= : {A B : Set} {a a' : A} (p : a == a') {b b' : B} (q : b == b') → (a , b) == (a' , b')
pair×= idp idp = idp

bs= : {B : Set} {C : B → Set}
      {b₁ b₁' : B} {pb₁ : b₁ == b₁'}
      {b₂ b₂' : B} {pb₂ : b₂ == b₂'}
      {c₁ : C b₁} {c₁' : C b₁'} (pc₁ : c₁ == c₁' [ C ↓ pb₁ ])
      {c₂ : C b₂} {c₂' : C b₂'} (pc₂ : c₂ == c₂' [ C ↓ pb₂ ])
      {p : b₁ == b₂} {p' : b₁' == b₂'} (α : p == p' [ (λ u → fst u == snd u) ↓ pair×= pb₁ pb₂ ])
      → bs c₁ c₂ p == bs c₁' c₂' p'
bs= {pb₁ = idp} {pb₂ = idp} idp idp idp = idp

_=□^[_]_ : {a b c d : A} (p : a == b) (qr : (a == c) × (b == d)) (s : c == d) → Set
p =□^[ qr ] s = C (S (S O)) (bs {b₁ = bs _ _ idp} p s (bs= {pb₁ = idp} {pb₂ = idp} (fst qr) (snd qr) idp))

test : {a b : A} (p q : a == b) → (p =□^[ idp , idp ] q) == (p == q)
test p q = idp

{-
compareTerm (C n unit) =< (?0 n {b₁} c₁ c₂) : Set
term (?0 n {b₁} c₁ c₂) :>= (C n unit)
term (?0 n {b₁} c₁ c₂) :>= (C n unit)
solving _111 := (λ n {b₁} c₁ c₂ → C n unit)
-}


text:
module Equality where

  postulate _==_ : {A : Set} -> A -> A -> Set
	    refl : {A : Set}{x : A} -> x == x

  {-# BUILTIN EQUAL _==_ #-}
  {-# BUILTIN REFL  refl #-}

  private
   primitive
    primEqElim : {A : Set}(x : A)(C : (y : A) -> x == y -> Set) ->
		 C x refl -> (y : A) -> (p : x == y) -> C y p

  elim-== = \{A : Set} -> primEqElim {A}

  subst : {A : Set}(C : A -> Set){x y : A} -> x == y -> C y -> C x
  subst C {x}{y} p Cy = elim-== x (\z _ -> C z -> C x) (\Cx -> Cx) y p Cy

  sym : {A : Set}{x y : A} -> x == y -> y == x
  sym {x = x}{y = y} p = subst (\z -> y == z) p refl

  trans : {A : Set}{x y z : A} -> x == y -> y == z -> x == z
  trans {x = x}{y = y}{z = z} xy yz = subst (\w -> w == z) xy yz

  cong : {A B : Set}{x y : A}(f : A -> B) -> x == y -> f x == f y
  cong {y = y} f xy = subst (\ ∙ -> f ∙ == f y) xy refl


text:
{-

Proof of the standard formulation of the univalence theorem and
various consequences of univalence

- Re-exports Glue types from Cubical.Core.Glue
- The ua constant and its computation rule (up to a path)
- Proof of univalence using that unglue is an equivalence ([EquivContr])
- Equivalence induction ([EquivJ], [elimEquiv])
- Univalence theorem ([univalence])
- The computation rule for ua ([uaβ])
- Isomorphism induction ([elimIso])

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Foundations.Univalence where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.GroupoidLaws

open import Cubical.Data.Sigma.Base

open import Cubical.Core.Glue public
  using ( Glue ; glue ; unglue ; lineToEquiv )

open import Cubical.Reflection.StrictEquiv

private
  variable
    ℓ ℓ' : Level

-- The ua constant
ua : ∀ {A B : Type ℓ} → A ≃ B → A ≡ B
ua {A = A} {B = B} e i = Glue B (λ { (i = i0) → (A , e)
                                   ; (i = i1) → (B , idEquiv B) })

uaIdEquiv : {A : Type ℓ} → ua (idEquiv A) ≡ refl
uaIdEquiv {A = A} i j = Glue A {φ = i ∨ ~ j ∨ j} (λ _ → A , idEquiv A)

-- Propositional extensionality
hPropExt : {A B : Type ℓ} → isProp A → isProp B → (A → B) → (B → A) → A ≡ B
hPropExt Aprop Bprop f g = ua (propBiimpl→Equiv Aprop Bprop f g)

-- the unglue and glue primitives specialized to the case of ua

ua-unglue : ∀ {A B : Type ℓ} (e : A ≃ B) (i : I) (x : ua e i)
            → B {- [ _ ↦ (λ { (i = i0) → e .fst x ; (i = i1) → x }) ] -}
ua-unglue e i x = unglue (i ∨ ~ i) x

ua-glue : ∀ {A B : Type ℓ} (e : A ≃ B) (i : I) (x : Partial (~ i) A)
            (y : B [ _ ↦ (λ { (i = i0) → e .fst (x 1=1) }) ])
          → ua e i {- [ _ ↦ (λ { (i = i0) → x 1=1 ; (i = i1) → outS y }) ] -}
ua-glue e i x y = glue {φ = i ∨ ~ i} (λ { (i = i0) → x 1=1 ; (i = i1) → outS y }) (outS y)

module _ {A B : Type ℓ} (e : A ≃ B) {x : A} {y : B} where
  -- sometimes more useful are versions of these functions with the (i : I) factored in

  ua-ungluePath : PathP (λ i → ua e i) x y → e .fst x ≡ y
  ua-ungluePath p i = ua-unglue e i (p i)

  ua-gluePath : e .fst x ≡ y → PathP (λ i → ua e i) x y
  ua-gluePath p i = ua-glue e i (λ { (i = i0) → x }) (inS (p i))

  -- ua-ungluePath and ua-gluePath are definitional inverses
  ua-ungluePath-Equiv : (PathP (λ i → ua e i) x y) ≃ (e .fst x ≡ y)
  unquoteDef ua-ungluePath-Equiv =
    defStrictEquiv ua-ungluePath-Equiv ua-ungluePath ua-gluePath

-- ua-unglue and ua-glue are also definitional inverses, in a way
-- strengthening the types of ua-unglue and ua-glue gives a nicer formulation of this, see below

ua-unglue-glue : ∀ {A B : Type ℓ} (e : A ≃ B) (i : I) (x : Partial (~ i) A) (y : B [ _ ↦ _ ])
                 → ua-unglue e i (ua-glue e i x y) ≡ outS y
ua-unglue-glue _ _ _ _ = refl

ua-glue-unglue : ∀ {A B : Type ℓ} (e : A ≃ B) (i : I) (x : ua e i)
                 → ua-glue e i (λ { (i = i0) → x }) (inS (ua-unglue e i x)) ≡ x
ua-glue-unglue _ _ _ = refl

-- mainly for documentation purposes, ua-unglue and ua-glue wrapped in cubical subtypes

ua-unglueS : ∀ {A B : Type ℓ} (e : A ≃ B) (i : I) (x : A) (y : B)
             → ua e i [ _ ↦ (λ { (i = i0) → x        ; (i = i1) → y }) ]
             → B      [ _ ↦ (λ { (i = i0) → e .fst x ; (i = i1) → y }) ]
ua-unglueS e i x y s = inS (ua-unglue e i (outS s))

ua-glueS : ∀ {A B : Type ℓ} (e : A ≃ B) (i : I) (x : A) (y : B)
           → B      [ _ ↦ (λ { (i = i0) → e .fst x ; (i = i1) → y }) ]
           → ua e i [ _ ↦ (λ { (i = i0) → x        ; (i = i1) → y }) ]
ua-glueS e i x y s = inS (ua-glue e i (λ { (i = i0) → x }) (inS (outS s)))

ua-unglueS-glueS : ∀ {A B : Type ℓ} (e : A ≃ B) (i : I) (x : A) (y : B)
                     (s : B [ _ ↦ (λ { (i = i0) → e .fst x ; (i = i1) → y }) ])
                   → outS (ua-unglueS e i x y (ua-glueS e i x y s)) ≡ outS s
ua-unglueS-glueS _ _ _ _ _ = refl

ua-glueS-unglueS : ∀ {A B : Type ℓ} (e : A ≃ B) (i : I) (x : A) (y : B)
                     (s : ua e i [ _ ↦ (λ { (i = i0) → x ; (i = i1) → y }) ])
                   → outS (ua-glueS e i x y (ua-unglueS e i x y s)) ≡ outS s
ua-glueS-unglueS _ _ _ _ _ = refl

-- a version of ua-glue with a single endpoint, identical to `ua-gluePath e {x} refl i`
ua-gluePt : ∀ {A B : Type ℓ} (e : A ≃ B) (i : I) (x : A)
            → ua e i {- [ _ ↦ (λ { (i = i0) → x ; (i = i1) → e .fst x }) ] -}
ua-gluePt e i x = ua-glue e i (λ { (i = i0) → x }) (inS (e .fst x))

-- Proof of univalence using that unglue is an equivalence:

-- unglue is an equivalence
unglueIsEquiv : ∀ (A : Type ℓ) (φ : I)
                (f : PartialP φ (λ o → Σ[ T ∈ Type ℓ ] T ≃ A)) →
                isEquiv {A = Glue A f} (unglue φ)
equiv-proof (unglueIsEquiv A φ f) = λ (b : A) →
  let u : I → Partial φ A
      u i = λ{ (φ = i1) → equivCtr (f 1=1 .snd) b .snd (~ i) }
      ctr : fiber (unglue φ) b
      ctr = ( glue (λ { (φ = i1) → equivCtr (f 1=1 .snd) b .fst }) (hcomp u b)
            , λ j → hfill u (inS b) (~ j))
  in ( ctr
     , λ (v : fiber (unglue φ) b) i →
         let u' : I → Partial (φ ∨ ~ i ∨ i) A
             u' j = λ { (φ = i1) → equivCtrPath (f 1=1 .snd) b v i .snd (~ j)
                      ; (i = i0) → hfill u (inS b) j
                      ; (i = i1) → v .snd (~ j) }
         in ( glue (λ { (φ = i1) → equivCtrPath (f 1=1 .snd) b v i .fst }) (hcomp u' b)
            , λ j → hfill u' (inS b) (~ j)))

-- Any partial family of equivalences can be extended to a total one
-- from Glue [ φ ↦ (T,f) ] A to A
unglueEquiv : ∀ (A : Type ℓ) (φ : I)
              (f : PartialP φ (λ o → Σ[ T ∈ Type ℓ ] T ≃ A)) →
              (Glue A f) ≃ A
unglueEquiv A φ f = ( unglue φ , unglueIsEquiv A φ f )

-- The following is a formulation of univalence proposed by Martín Escardó:
-- https://groups.google.com/forum/#!msg/homotopytypetheory/HfCB_b-PNEU/Ibb48LvUMeUJ
-- See also Theorem 5.8.4 of the HoTT Book.
--
-- The reason we have this formulation in the core library and not the
-- standard one is that this one is more direct to prove using that
-- unglue is an equivalence. The standard formulation can be found in
-- Cubical/Basics/Univalence.
--
EquivContr : ∀ (A : Type ℓ) → ∃![ T ∈ Type ℓ ] (T ≃ A)
EquivContr {ℓ = ℓ} A =
  ( (A , idEquiv A)
  , idEquiv≡ )
 where
  idEquiv≡ : (y : Σ (Type ℓ) (λ T → T ≃ A)) → (A , idEquiv A) ≡ y
  idEquiv≡ w = \ { i .fst                   → Glue A (f i)
                 ; i .snd .fst              → unglueEquiv _ _ (f i) .fst
                 ; i .snd .snd .equiv-proof → unglueEquiv _ _ (f i) .snd .equiv-proof
                 }
    where
      f : ∀ i → PartialP (~ i ∨ i) (λ x → Σ[ T ∈ Type ℓ ] T ≃ A)
      f i = λ { (i = i0) → A , idEquiv A ; (i = i1) → w }

contrSinglEquiv : {A B : Type ℓ} (e : A ≃ B) → (B , idEquiv B) ≡ (A , e)
contrSinglEquiv {A = A} {B = B} e =
  isContr→isProp (EquivContr B) (B , idEquiv B) (A , e)

-- Equivalence induction
EquivJ : {A B : Type ℓ} (P : (A : Type ℓ) → (e : A ≃ B) → Type ℓ')
       → (r : P B (idEquiv B)) → (e : A ≃ B) → P A e
EquivJ P r e = subst (λ x → P (x .fst) (x .snd)) (contrSinglEquiv e) r

-- Assuming that we have an inverse to ua we can easily prove univalence
module Univalence (au : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → A ≃ B)
                  (aurefl : ∀ {ℓ} {A B : Type ℓ} → au refl ≡ idEquiv A) where

  ua-au : {A B : Type ℓ} (p : A ≡ B) → ua (au p) ≡ p
  ua-au {B = B} = J (λ _ p → ua (au p) ≡ p)
                    (cong ua (aurefl {B = B}) ∙ uaIdEquiv)

  au-ua : {A B : Type ℓ} (e : A ≃ B) → au (ua e) ≡ e
  au-ua {B = B} = EquivJ (λ _ f → au (ua f) ≡ f)
                         (subst (λ r → au r ≡ idEquiv _) (sym uaIdEquiv) (aurefl {B = B}))

  isoThm : ∀ {ℓ} {A B : Type ℓ} → Iso (A ≡ B) (A ≃ B)
  isoThm .Iso.fun = au
  isoThm .Iso.inv = ua
  isoThm .Iso.rightInv = au-ua
  isoThm .Iso.leftInv = ua-au

  thm : ∀ {ℓ} {A B : Type ℓ} → isEquiv au
  thm {A = A} {B = B} = isoToIsEquiv {B = A ≃ B} isoThm

pathToEquiv : {A B : Type ℓ} → A ≡ B → A ≃ B
pathToEquiv p = lineToEquiv (λ i → p i)

pathToEquivRefl : {A : Type ℓ} → pathToEquiv refl ≡ idEquiv A
pathToEquivRefl {A = A} = equivEq (λ i x → transp (λ _ → A) i x)

pathToEquiv-ua : {A B : Type ℓ} (e : A ≃ B) → pathToEquiv (ua e) ≡ e
pathToEquiv-ua = Univalence.au-ua pathToEquiv pathToEquivRefl

ua-pathToEquiv : {A B : Type ℓ} (p : A ≡ B) → ua (pathToEquiv p) ≡ p
ua-pathToEquiv = Univalence.ua-au pathToEquiv pathToEquivRefl

-- Univalence
univalenceIso : {A B : Type ℓ} → Iso (A ≡ B) (A ≃ B)
univalenceIso = Univalence.isoThm pathToEquiv pathToEquivRefl

univalence : {A B : Type ℓ} → (A ≡ B) ≃ (A ≃ B)
univalence = ( pathToEquiv , Univalence.thm pathToEquiv pathToEquivRefl  )

-- The original map from UniMath/Foundations
eqweqmap : {A B : Type ℓ} → A ≡ B → A ≃ B
eqweqmap {A = A} e = J (λ X _ → A ≃ X) (idEquiv A) e

eqweqmapid : {A : Type ℓ} → eqweqmap refl ≡ idEquiv A
eqweqmapid {A = A} = JRefl (λ X _ → A ≃ X) (idEquiv A)

univalenceStatement : {A B : Type ℓ} → isEquiv (eqweqmap {ℓ} {A} {B})
univalenceStatement = Univalence.thm eqweqmap eqweqmapid

univalenceUAH : {A B : Type ℓ} → (A ≡ B) ≃ (A ≃ B)
univalenceUAH = ( _ , univalenceStatement )

univalencePath : {A B : Type ℓ} → (A ≡ B) ≡ Lift (A ≃ B)
univalencePath = ua (compEquiv univalence LiftEquiv)

-- The computation rule for ua. Because of "ghcomp" it is now very
-- simple compared to cubicaltt:
-- https://github.com/mortberg/cubicaltt/blob/master/examples/univalence.ctt#L202
uaβ : {A B : Type ℓ} (e : A ≃ B) (x : A) → transport (ua e) x ≡ equivFun e x
uaβ e x = transportRefl (equivFun e x)

uaη : ∀ {A B : Type ℓ} → (P : A ≡ B) → ua (pathToEquiv P) ≡ P
uaη = J (λ _ q → ua (pathToEquiv q) ≡ q) (cong ua pathToEquivRefl ∙ uaIdEquiv)

-- Lemmas for constructing and destructing dependent paths in a function type where the domain is ua.
ua→ : ∀ {ℓ ℓ'} {A₀ A₁ : Type ℓ} {e : A₀ ≃ A₁} {B : (i : I) → Type ℓ'}
  {f₀ : A₀ → B i0} {f₁ : A₁ → B i1}
  → ((a : A₀) → PathP B (f₀ a) (f₁ (e .fst a)))
  → PathP (λ i → ua e i → B i) f₀ f₁
ua→ {e = e} {f₀ = f₀} {f₁} h i a =
  hcomp
    (λ j → λ
      { (i = i0) → f₀ a
      ; (i = i1) → f₁ (lem a j)
      })
    (h (transp (λ j → ua e (~ j ∧ i)) (~ i) a) i)
  where
  lem : ∀ a₁ → e .fst (transport (sym (ua e)) a₁) ≡ a₁
  lem a₁ = retEq e _ ∙ transportRefl _

ua→⁻ : ∀ {ℓ ℓ'} {A₀ A₁ : Type ℓ} {e : A₀ ≃ A₁} {B : (i : I) → Type ℓ'}
  {f₀ : A₀ → B i0} {f₁ : A₁ → B i1}
  → PathP (λ i → ua e i → B i) f₀ f₁
  → ((a : A₀) → PathP B (f₀ a) (f₁ (e .fst a)))
ua→⁻ {e = e} {f₀ = f₀} {f₁} p a i =
  hcomp
    (λ k → λ
      { (i = i0) → f₀ a
      ; (i = i1) → f₁ (uaβ e a k)
      })
    (p i (transp (λ j → ua e (j ∧ i)) (~ i) a))

-- Useful lemma for unfolding a transported function over ua
-- If we would have regularity this would be refl
transportUAop₁ : ∀ {A B : Type ℓ} → (e : A ≃ B) (f : A → A) (x : B)
               → transport (λ i → ua e i → ua e i) f x ≡ equivFun e (f (invEq e x))
transportUAop₁ e f x i = transportRefl (equivFun e (f (invEq e (transportRefl x i)))) i

-- Binary version
transportUAop₂ : ∀ {ℓ} {A B : Type ℓ} → (e : A ≃ B) (f : A → A → A) (x y : B)
               → transport (λ i → ua e i → ua e i → ua e i) f x y ≡
                 equivFun e (f (invEq e x) (invEq e y))
transportUAop₂ e f x y i =
    transportRefl (equivFun e (f (invEq e (transportRefl x i))
                                 (invEq e (transportRefl y i)))) i

-- Alternative version of EquivJ that only requires a predicate on functions
elimEquivFun : {A B : Type ℓ} (P : (A : Type ℓ) → (A → B) → Type ℓ')
             → (r : P B (idfun B)) → (e : A ≃ B) → P A (e .fst)
elimEquivFun P r e = subst (λ x → P (x .fst) (x .snd .fst)) (contrSinglEquiv e) r

-- Isomorphism induction
elimIso : {B : Type ℓ} → (Q : {A : Type ℓ} → (A → B) → (B → A) → Type ℓ') →
          (h : Q (idfun B) (idfun B)) → {A : Type ℓ} →
          (f : A → B) → (g : B → A) → section f g → retract f g → Q f g
elimIso {ℓ} {ℓ'} {B} Q h {A} f g sfg rfg = rem1 f g sfg rfg
  where
  P : (A : Type ℓ) → (f : A → B) → Type (ℓ-max ℓ' ℓ)
  P A f = (g : B → A) → section f g → retract f g → Q f g

  rem : P B (idfun B)
  rem g sfg rfg = subst (Q (idfun B)) (λ i b → (sfg b) (~ i)) h

  rem1 : {A : Type ℓ} → (f : A → B) → P A f
  rem1 f g sfg rfg = elimEquivFun P rem (f , isoToIsEquiv (iso f g sfg rfg)) g sfg rfg

uaInvEquiv : ∀ {A B : Type ℓ} → (e : A ≃ B) → ua (invEquiv e) ≡ sym (ua e)
uaInvEquiv {B = B} = EquivJ (λ _ e → ua (invEquiv e) ≡ sym (ua e))
                            (cong ua (invEquivIdEquiv B))

uaCompEquiv : ∀ {A B C : Type ℓ} → (e : A ≃ B) (f : B ≃ C) → ua (compEquiv e f) ≡ ua e ∙ ua f
uaCompEquiv {B = B} {C} = EquivJ (λ _ e → (f : B ≃ C) → ua (compEquiv e f) ≡ ua e ∙ ua f)
                                 (λ f → cong ua (compEquivIdEquiv f)
                                        ∙ sym (cong (λ x → x ∙ ua f) uaIdEquiv
                                        ∙ sym (lUnit (ua f))))

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.List using (List; []; _∷_; [_]; _++_)
open import Data.List.Any using (Any; here; there)
open import Data.List.Any.Membership.Propositional using (_∈_)
open import Data.Nat using (ℕ)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
-- open import Data.List.Any.Membership.Propositional.Properties using (∈-++⁺ˡ; ∈-++⁺ʳ; ∈-++⁻)

Id = ℕ

_⊆_ : List Id → List Id → Set
xs ⊆ ys = ∀ {w} → w ∈ xs → w ∈ ys

lemma : ∀ {x : Id} → x ∈ [ x ]
lemma = here refl