text:
------------------------------------------------------------------------
-- A lookahead operator cannot be defined
------------------------------------------------------------------------

-- In "Parsing with First-Class Derivatives" Brachthäuser, Rendel and
-- Ostermann state that "Lookahead and [...] cannot be expressed as
-- user defined combinators". Here I give a formal proof of a variant
-- of this statement (in the present setting).

module TotalParserCombinators.NoLookahead where

open import Data.List
open import Data.List.Properties
open import Data.Product
open import Data.Unit
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (Equivalence; _⇔_)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Relation.Nullary

open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser
open import TotalParserCombinators.Semantics.Continuation

-- It is impossible to define a lookahead operator satisfying a
-- certain specification (without changing the interface of the parser
-- combinator library).

no-lookahead :
  ¬ ∃ λ (look : ∀ {Tok R} {f-bag : List Tok → List R} →
                ((s : List Tok) → Parser Tok R (f-bag s)) →
                Parser Tok R (f-bag [])) →
      ∀ {Tok R x s₁ s₂} {f-bag : List Tok → List R}
        {f : (s : List Tok) → Parser Tok R (f-bag s)} →
      x ⊕ s₂ ∈ look f · s₁ ⇔ x ⊕ s₂ ∈ f s₁ · s₁
no-lookahead (look , correct) = ¬f[-]·[-] f[-]·[-]
  where
  f-bag : List ⊤ → List ⊤
  f-bag []      = [ _ ]
  f-bag (_ ∷ _) = []

  f : (s : List ⊤) → Parser ⊤ ⊤ (f-bag s)
  f []      = return _
  f (_ ∷ _) = fail

  f[]·[] : _ ⊕ [] ∈ f [] · []
  f[]·[] = return

  look-f·[] : _ ⊕ [] ∈ look f · []
  look-f·[] = Equivalence.from correct ⟨$⟩ f[]·[]

  look-f·[-] : _ ⊕ [ _ ] ∈ look f · [ _ ]
  look-f·[-] = extend look-f·[]

  f[-]·[-] : _ ⊕ [ _ ] ∈ f [ _ ] · [ _ ]
  f[-]·[-] = Equivalence.to correct ⟨$⟩ look-f·[-]

  ¬f[-]·[-] : ¬ _ ⊕ [ _ ] ∈ f [ _ ] · [ _ ]
  ¬f[-]·[-] ()

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------------
-- Agda-Prop Library.
-- Theorems of ⇔ connective.
------------------------------------------------------------------------------

open import Data.Nat using ( ℕ )

module Data.PropFormula.Theorems.Biimplication ( n : ℕ ) where

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

open import Data.PropFormula.Theorems.Classical n
open import Data.PropFormula.Theorems.Implication n
  using ( ⊃-to-¬∨; ⊃⊃-to-∧⊃; ∧⊃-to-⊃⊃ )
open import Data.PropFormula.Theorems.Negation n
  using ( ¬-equiv₁ ; ¬-equiv₂; ¬∨-to-⊃; ¬¬-equiv₁; ¬¬-equiv₂ )
open import Data.PropFormula.Syntax n

open import Function using ( _$_ )

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

-- Theorem.
⇔-equiv₁
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ φ ⇔ ψ
  → Γ ⊢ (φ ⊃ ψ) ∧ (ψ ⊃ φ)

-- Proof.
⇔-equiv₁ {Γ}{φ}{ψ} Γ⊢φ⇔ψ =
  ∧-intro
    (⊃-intro
      (⇔-elim₁
        (assume φ)
        (weaken φ Γ⊢φ⇔ψ)))
    (⊃-intro
      (⇔-elim₂
        (assume ψ)
         (weaken ψ Γ⊢φ⇔ψ)))
-------------------------------------------------------------------------- ∎

-- Theorem.
⇔-equiv₂
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ (φ ⊃ ψ) ∧ (ψ ⊃ φ)
  → Γ ⊢ φ ⇔ ψ

-- Proof.
⇔-equiv₂ {φ = φ}{ψ} Γ⊢⟪φ⊃ψ⟫∧⟪ψ⊃φ⟫ =
  ⇔-intro
    (⊃-elim
      (weaken φ (∧-proj₁ Γ⊢⟪φ⊃ψ⟫∧⟪ψ⊃φ⟫))
      (assume φ))
    (⊃-elim
      (weaken ψ (∧-proj₂ Γ⊢⟪φ⊃ψ⟫∧⟪ψ⊃φ⟫))
      (assume ψ))
-------------------------------------------------------------------------- ∎

-- Theorem.
⇔-equiv
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ (φ ⇔ ψ) ⇔ ((φ ⊃ ψ) ∧ (ψ ⊃ φ))

-- Proof.
⇔-equiv {Γ}{φ}{ψ} =
  ⇔-intro
    (⇔-equiv₁
      (assume (φ ⇔ ψ)))
    (⇔-equiv₂
      (assume ((φ ⊃ ψ) ∧ (ψ ⊃ φ))))
-------------------------------------------------------------------------- ∎

-- Theorem.
⇔-assoc₁
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ φ ⇔ (ψ ⇔ γ)
  → Γ ⊢ (φ ⇔ ψ) ⇔ γ

-- Proof.
⇔-assoc₁ {Γ}{φ = φ}{ψ}{γ} thm =
  ⇔-intro
    (RAA
      (¬-elim
        (¬-intro
          (¬-elim
            (¬-intro
              (¬-elim
                (weaken φ $ weaken (ψ ⇔ γ) $ assume {Γ = Γ , φ ⇔ ψ} (¬ γ))
                (⇔-elim₁
                  (⇔-elim₁
                    (assume {Γ = Γ , φ ⇔ ψ , ¬ γ , ψ ⇔ γ} φ)
                    (weaken φ $ weaken (ψ ⇔ γ)
                        (weaken (¬ γ) $ assume (φ ⇔ ψ))))
                  (⇔-elim₁
                    (assume {Γ = Γ , φ ⇔ ψ , ¬ γ , ψ ⇔ γ} φ)
                    (weaken φ $ weaken (ψ ⇔ γ) $ weaken (¬ γ) $
                      weaken (φ ⇔ ψ) thm)))))
            (⇔-elim₂
              (assume {Γ = Γ , φ ⇔ ψ , ¬ γ} (ψ ⇔ γ))
              (weaken (ψ ⇔ γ) $ weaken (¬ γ) $ weaken (φ ⇔ ψ) thm))))
        (⇔-intro
          (⊥-elim γ
            (¬-elim
              (⊥-elim (¬ ψ)
                (¬-elim
                  (¬-intro -- ¬ φ
                    (¬-elim
                      (weaken φ $ weaken ψ $ assume {Γ = Γ , φ ⇔ ψ} (¬ γ))
                      (⇔-elim₁
                        (⇔-elim₁
                          (assume {Γ = Γ , φ ⇔ ψ , ¬ γ , ψ} φ)
                          (weaken φ
                            (weaken ψ
                              (weaken (¬ γ)
                                (assume (φ ⇔ ψ))))))
                        (⇔-elim₁
                          (assume {Γ = Γ , φ ⇔ ψ , ¬ γ , ψ} φ)
                          (weaken φ $
                            weaken ψ $ weaken (¬ γ) $ weaken (φ ⇔ ψ) thm)))))
                  (⇔-elim₂ -- φ
                    (assume {Γ = Γ , φ ⇔ ψ , ¬  γ} ψ)
                    (weaken ψ (weaken (¬ γ) (assume (φ ⇔ ψ)))))))
              (assume {Γ = Γ , φ ⇔ ψ , ¬ γ} ψ)))
          (⊥-elim ψ
            (¬-elim
              (weaken γ $ assume {Γ = Γ , φ ⇔ ψ} (¬ γ))
              (assume {Γ = Γ , φ ⇔ ψ , ¬ γ} γ))))))
    (⇔-intro
      (⇔-elim₂
        (weaken φ $ assume γ)
        (⇔-elim₁
          (assume {Γ = Γ , γ} φ)
          (weaken φ $ weaken γ thm)))
      (⇔-elim₂
        (⇔-intro
          (weaken ψ $ weaken ψ $ assume γ)
          (weaken γ $ assume {Γ = Γ , γ} ψ))
        (weaken ψ $ weaken γ thm)))
-------------------------------------------------------------------------- ∎

-- Theorem.
⇔-assoc₂
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ (φ ⇔ ψ) ⇔ γ
  → Γ ⊢ φ ⇔ (ψ ⇔ γ)

-- Proof.
⇔-assoc₂ {Γ}{φ}{ψ}{γ} thm =
  ⇔-intro
    (⇔-intro
      (⇔-elim₁
        (⇔-intro
          (weaken φ (assume {Γ = Γ , φ} ψ))
          (weaken ψ (weaken ψ (assume φ))))
        (weaken ψ (weaken φ thm)))
      (⇔-elim₁
        (weaken γ (assume φ))
          (⇔-elim₂
            (assume {Γ = Γ , φ} γ)
            (weaken γ (weaken φ thm)))))
    (RAA
      (¬-elim
        (¬-intro
          (¬-elim
            (¬-intro
              (¬-elim
                (weaken γ $ weaken (φ ⇔ ψ) $ assume {Γ = Γ , ψ ⇔ γ} (¬ φ))
                (⇔-elim₂
                  (⇔-elim₂
                    (assume {Γ = Γ , ψ ⇔ γ , ¬ φ , (φ ⇔ ψ)} γ)
                    (weaken γ $ weaken (φ ⇔ ψ) $ weaken (¬ φ) $
                      assume (ψ ⇔ γ)))
                  (⇔-elim₂
                    (assume {Γ = Γ , ψ ⇔ γ , ¬ φ , (φ ⇔ ψ)} γ)
                    (weaken γ $ weaken (φ ⇔ ψ) $ weaken (¬ φ) $
                      weaken (ψ ⇔ γ) thm)))))
            (⇔-elim₁
              (assume {Γ = Γ , ψ ⇔ γ , ¬ φ} (φ ⇔ ψ))
              (weaken (φ ⇔ ψ) (weaken (¬ φ) (weaken (ψ ⇔ γ) thm))))))
        (⇔-intro
          (⊥-elim ψ
            (¬-elim
              (weaken φ $ assume {Γ = Γ , ψ ⇔ γ} (¬ φ))
              (assume {Γ = Γ , ψ ⇔ γ , ¬ φ} φ)))
          (⊥-elim φ
            (¬-elim
              (⊥-elim (¬ ψ)
                (¬-elim
                  (¬-intro
                    (¬-elim
                      (weaken γ $ weaken ψ $ assume {Γ = Γ , ψ ⇔ γ} (¬ φ))
                      (⇔-elim₂
                        (weaken γ $ assume {Γ = Γ , ψ ⇔ γ , ¬ φ} ψ)
                        (⇔-elim₂
                          (assume {Γ = Γ , ψ ⇔ γ , ¬ φ , ψ} γ)
                          (weaken γ $ weaken ψ $ weaken (¬ φ) $
                            weaken (ψ ⇔ γ) thm)))))
                  (⇔-elim₁
                    (assume {Γ = Γ , ψ ⇔ γ , ¬ φ} ψ)
                    (weaken ψ (weaken (¬ φ) (assume (ψ ⇔ γ)))))))
              (assume {Γ = Γ , ψ ⇔ γ , ¬ φ} ψ))))))
-------------------------------------------------------------------------- ∎

-- Theorem.
⇔-assoc
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ (φ ⇔ (ψ ⇔ γ)) ⇔ ((φ ⇔ ψ) ⇔ γ)

-- Proof.
⇔-assoc {φ = φ}{ψ}{γ} =
  ⇔-intro
    (⇔-assoc₁ (assume (φ ⇔ ψ ⇔ γ)))
    (⇔-assoc₂ (assume ((φ ⇔ ψ) ⇔ γ)))
-------------------------------------------------------------------------- ∎

-- Theorem.
⇔-comm
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ φ ⇔ ψ
  → Γ ⊢ ψ ⇔ φ

-- Proof.
⇔-comm {Γ}{φ}{ψ} Γ⊢φ⇔ψ =
  ⇔-intro
    (⇔-elim₂ (assume ψ) (weaken ψ Γ⊢φ⇔ψ))
    (⇔-elim₁ (assume φ) (weaken φ Γ⊢φ⇔ψ))
-------------------------------------------------------------------------- ∎

-- Theorem.
⊃-⇔-¬∨
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ (φ ⊃ ψ) ⇔ (¬ φ ∨ ψ)

-- Proof.

⊃-⇔-¬∨ {Γ}{φ}{ψ} =
  ⇔-intro
    (⊃-to-¬∨ (assume (φ ⊃ ψ)))
    (¬∨-to-⊃ (assume (¬ φ ∨ ψ)))
-------------------------------------------------------------------------- ∎

-- Theorem.
bicon₀-thm
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ φ ⇔ ψ → Γ ⊢ ¬ φ
  → Γ ⊢ ¬ ψ
⇔-¬-to-¬ = bicon₀-thm

-- Proof.
bicon₀-thm {Γ}{φ}{ψ} Γ⊢φ⇔ψ Γ⊢¬ψ =
  ¬-equiv₂
    (⊃-intro
      (¬-elim
        (weaken ψ Γ⊢¬ψ)
      (⇔-elim₂
        (assume ψ)
        (weaken ψ Γ⊢φ⇔ψ))))
-------------------------------------------------------------------------- ∎

-- Theorem.
bicon₁-thm
  : ∀ {Γ} {φ ψ}
  → Γ ⊢ ¬ φ ⇔ ψ → Γ ⊢ φ
  → Γ ⊢ ¬ ψ
¬⇔-to-¬ = bicon₁-thm

-- Proof.
bicon₁-thm {Γ}{φ}{ψ} Γ⊢¬φ⇔ψ Γ⊢φ =
  ¬-equiv₂
    (⊃-intro
      (¬-elim
        (⇔-elim₂
          (assume ψ)
          (weaken ψ Γ⊢¬φ⇔ψ))
        (weaken ψ Γ⊢φ)))
-------------------------------------------------------------------------- ∎

-- Theorem.
¬-equiv
  : ∀ {Γ} {φ}
  → Γ ⊢ ¬ φ ⇔ (φ ⊃ ⊥)

-- Proof.
¬-equiv {Γ}{φ} =
  ⇔-intro
    (¬-equiv₁ (assume (¬ φ)))
    (¬-equiv₂ (assume (φ ⊃ ⊥)))
-------------------------------------------------------------------------- ∎

-- Theorem.
¬¬-equiv
  : ∀ {Γ} {φ}
  → Γ ⊢ ¬ (¬ φ) ⇔ φ

-- Proof.
¬¬-equiv {Γ}{φ} =
  ⇔-intro
    (¬¬-equiv₁ (assume (¬ (¬ φ))))
    (¬¬-equiv₂ (assume φ))
-------------------------------------------------------------------------- ∎

-- Theorem.
⊃⊃-⇔-∧⊃
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ (φ ⊃ (ψ ⊃ γ)) ⇔ ((φ ∧ ψ) ⊃ γ)

-- Proof.
⊃⊃-⇔-∧⊃ {φ = φ}{ψ}{γ} =
  ⇔-intro
    (⊃⊃-to-∧⊃ (assume (φ ⊃ ψ ⊃ γ)))
    (∧⊃-to-⊃⊃ (assume (φ ∧ ψ ⊃ γ)))
-------------------------------------------------------------------------- ∎

-- Theorem.
⇔-trans
  : ∀ {Γ} {φ ψ γ}
  → Γ ⊢ γ ⇔ φ
  → Γ ⊢ φ ⇔ ψ
  → Γ ⊢ γ ⇔ ψ
subst⊢⇔₁ = ⇔-trans

-- Proof.
⇔-trans {φ = φ}{ψ}{γ} Γ⊢γ⇔φ Γ⊢φ⇔ψ =
  ⇔-intro
    (⇔-elim₁
      (⇔-elim₁
        (assume γ)
        (weaken γ Γ⊢γ⇔φ))
      (weaken γ Γ⊢φ⇔ψ))
    (⇔-elim₂
      (⇔-elim₂
        (assume ψ)
        (weaken ψ Γ⊢φ⇔ψ))
      (weaken ψ Γ⊢γ⇔φ))
-------------------------------------------------------------------------- ∎

ext: agda

max_stars_repo_name: jonaprieto/agda-prop

max_issues_repo_name: jonaprieto/agda-prop

max_forks_repo_name: jonaprieto/agda-prop


text:
module Logic.ChainReasoning where

module Mono where

  module Homogenous
    { A : Set }
    ( _==_ : A -> A -> Set )
    (refl  : (x : A) -> x == x)
    (trans : (x y z : A) -> x == y -> y == z -> x == z)
    where

    infix 2 chain>_
    infixl 2 _===_
    infix 3 _by_

    chain>_ : (x : A) -> x == x
    chain> x = refl _

    _===_ : {x y z : A} -> x == y -> y == z -> x == z
    xy === yz = trans _ _ _ xy yz

    _by_ : {x : A}(y : A) -> x == y -> x == y
    y by eq = eq

module Poly where

  module Homogenous
    ( _==_ : {A : Set} -> A -> A -> Set )
    (refl  : {A : Set}(x : A) -> x == x)
    (trans : {A : Set}(x y z : A) -> x == y -> y == z -> x == z)
    where

    infix 2 chain>_
    infixl 2 _===_
    infix 3 _by_

    chain>_ : {A : Set}(x : A) -> x == x
    chain> x = refl _

    _===_ : {A : Set}{x y z : A} -> x == y -> y == z -> x == z
    xy === yz = trans _ _ _ xy yz

    _by_ : {A : Set}{x : A}(y : A) -> x == y -> x == y
    y by eq = eq

  module Heterogenous
    ( _==_ : {A B : Set} -> A -> B -> Set )
    (refl  : {A : Set}(x : A) -> x == x)
    (trans : {A B C : Set}(x : A)(y : B)(z : C) -> x == y -> y == z -> x == z)
    where

    infix 2 chain>_
    infixl 2 _===_
    infix 3 _by_

    chain>_ : {A : Set}(x : A) -> x == x
    chain> x = refl _

    _===_ : {A B C : Set}{x : A}{y : B}{z : C} -> x == y -> y == z -> x == z
    xy === yz = trans _ _ _ xy yz

    _by_ : {A B : Set}{x : A}(y : B) -> x == y -> x == y
    y by eq = eq

  module Heterogenous1
    ( _==_ : {A B : Set1} -> A -> B -> Set1 )
    (refl  : {A : Set1}(x : A) -> x == x)
    (trans : {A B C : Set1}(x : A)(y : B)(z : C) -> x == y -> y == z -> x == z)
    where

    infix 2 chain>_
    infixl 2 _===_
    infix 3 _by_

    chain>_ : {A : Set1}(x : A) -> x == x
    chain> x = refl _

    _===_ : {A B C : Set1}{x : A}{y : B}{z : C} -> x == y -> y == z -> x == z
    xy === yz = trans _ _ _ xy yz

    _by_ : {A B : Set1}{x : A}(y : B) -> x == y -> x == y
    y by eq = eq

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{-# OPTIONS --without-K --no-pattern-matching #-}

module Ch2-7 where

open import Level hiding (lift)

open import Ch2-1
open import Ch2-2
open import Ch2-3
open import Ch2-4
open import Ch2-5
open import Ch2-6

open import Data.Product
open import Function using (id; _∘_)

Definition-2-7-2-i : ∀ {a b} {A : Set a} {P : A → Set b}
  → (w w' : Σ[ x ∈ A ] P x)
  → (w ≡ w')
  → (Σ[ p ∈ proj₁ w ≡ proj₁ w' ] transport P p (proj₂ w) ≡ proj₂ w')
Definition-2-7-2-i {_} {_} {A} {P} w w' p = J (Σ-syntax A P) D d w w' p
  where
    D : (w w' : Σ[ x ∈ A ] P x) (p : w ≡ w') → Set _
    D w w' p = Σ[ p ∈ proj₁ w ≡ proj₁ w' ] transport P p (proj₂ w) ≡ proj₂ w'

    d : (x : Σ[ x ∈ A ] P x) → D x x refl
    d x = refl , refl

Definition-2-7-2-ii : ∀ {a b} {A : Set a} {P : A → Set b}
  → (w w' : Σ[ x ∈ A ] P x)
  → (Σ[ p ∈ proj₁ w ≡ proj₁ w' ] transport P p (proj₂ w) ≡ proj₂ w')
  → (w ≡ w')
Definition-2-7-2-ii {_} {_} {A} {P} w w' p = J A D d (proj₁ w) (proj₁ w') (proj₁ p) (proj₂ w) (proj₂ w') (proj₂ p)
  -- J A D d w1 w1' fst w2 w2' snd
  where
    D : (w1 w1' : A) (p : w1 ≡ w1') → Set _
    D w1 w1' p = (w2 : P w1) (w2' : P w1') (q : transport P p w2 ≡ w2') → (w1 , w2) ≡ (w1' , w2')

    d : (x : A) → D x x refl
    d x w2 w2' snd = J (P x) E e w2 w2' snd

      where
        E : (w2 w2' : P x) (q : w2 ≡ w2') → Set _
        E w2 w2' q = (x , w2) ≡ (x , w2')

        e : (y : P x) → E y y refl
        e y = refl

Lemma-2-7-2-iii : ∀ {a b} {A : Set a} {P : A → Set b}
  → (w w' : Σ[ x ∈ A ] P x)
  → isequiv (Definition-2-7-2-i w w')
Lemma-2-7-2-iii {_} {_} {A} {P} w w' = (Definition-2-7-2-ii w w' , α) , (Definition-2-7-2-ii w w' , β)
  where
    α : Definition-2-7-2-i w w' ∘ Definition-2-7-2-ii w w' ~ id
    α p = J A D d (proj₁ w) (proj₁ w') (proj₁ p) (proj₂ w) (proj₂ w') (proj₂ p)
      where
        D : (x y : A) (p : x ≡ y) → Set _
        D x y p = (x' : P x) (y' : P y) (q : transport P p x' ≡ y')
          → (Definition-2-7-2-i (x , x') (y , y')
              ∘ Definition-2-7-2-ii (x , x') (y , y')) (p , q) ≡ id (p , q)

        d : (s : A) → D s s refl
        d s x' y' q = J (P s) E e x' y' q
          where
            E : (x' y' : P s) (q : x' ≡ y') → Set _
            E x' y' q =
              (Definition-2-7-2-i (s , x') (s , y')
                  ∘ Definition-2-7-2-ii (s , x') (s , y')) (refl , q) ≡ id (refl , q)

            e : (t : P s) → E t t refl
            e t = refl

    β : Definition-2-7-2-ii w w' ∘ Definition-2-7-2-i w w' ~ id
    β p = J (Σ[ x ∈ A ] P x) D d w w' p
      where
        D : (w w' : Σ[ x ∈ A ] P x) (p : w ≡ w') → Set _
        D w w' p = (Definition-2-7-2-ii w w' ∘ Definition-2-7-2-i w w') p ≡ id p

        d : (x : Σ[ x ∈ A ] P x) → D x x refl
        d x = refl

-- Theorem 2.7.2
Theorem-2-7-2 : ∀ {a b} {A : Set a} {P : A → Set b}
  → (w w' : Σ[ x ∈ A ] P x)
  → (w ≡ w') ≅ (Σ[ p ∈ proj₁ w ≡ proj₁ w' ] transport P p (proj₂ w) ≡ proj₂ w')
Theorem-2-7-2 {_} {_} {A} {P} w w' = Definition-2-7-2-i w w' , Lemma-2-7-2-iii w w'

-- Corollary 2.7.3
Corollary-2-7-3 : ∀ {a b} {A : Set a} {P : A → Set b}
  → (z : Σ[ x ∈ A ] P x)
  → z ≡ (proj₁ z , proj₂ z)
Corollary-2-7-3 {a} {b} {A} {P} z
  = ←≅ (Theorem-2-7-2 z z) (refl , refl)

-- Theorem 2.7.4
Theorem-2-7-4 : ∀ {a b} {A : Set a}
  → {P : A → Set b}
  → {Q : Σ[ x ∈ A ] P x → Set b}
  → {x y : A}
  → (p : x ≡ y)
  → (f : Σ[ u ∈ P x ] Q (x , u))
  → transport (λ w → Σ[ u ∈ P w ] Q (w , u)) p f
      ≡ (transport P p (proj₁ f) , transport Q
          (←≅ (Theorem-2-7-2 (x , (proj₁ f))
          (y , (transport P p (proj₁ f)))) (p , refl)) (proj₂ f))
Theorem-2-7-4 {a} {b} {A} {P} {Q} {x} {y} p f = J A D d x y p f
  where
    D : (x y : A) (p : x ≡ y) → Set _
    D x y p = (f : Σ[ u ∈ P x ] Q (x , u))
      → transport (λ w → Σ-syntax (P w) (λ u → Q (w , u))) p f ≡
      (transport P p (proj₁ f) ,
       transport Q
       (←≅ (Theorem-2-7-2 (x , proj₁ f) (y , transport P p (proj₁ f)))
        (p , refl))
       (proj₂ f))

    d : (x : A) → D x x refl
    d x f = refl

max_stars_repo_name: banacorn/hott

max_issues_repo_name: banacorn/hott

max_forks_repo_name: banacorn/hott


text:
-- In a mutual block, either all or none must have a MEASURE declaration.

module _ where

open import Common.Prelude

mutual

  {-# MEASURE n #-}
  f : (n : Nat) → Nat
  f zero = zero
  f (suc n) = g n

  {-# MEASURE n #-}
  g : (n : Nat) → Nat
  g zero = zero
  g (suc n) = suc (f n)

max_stars_repo_name: masondesu/agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

module README where

-- Formalization for "Decidability of Conversion for Type Theory in Type Theory"
-- Git repository: https://github.com/mr-ohman/logrel-mltt

------------------
-- INTRODUCTION --
------------------

-- A minimal library necessary for formalization:

-- Embedding types into larger universes
import Tools.Embedding

-- The empty type and its elimination rule.
import Tools.Empty

-- The unit type.
import Tools.Unit

-- Sum type.
import Tools.Sum

-- Product type.
import Tools.Product

-- Identity function and composition.
import Tools.Function

-- Negation and decidability type.
import Tools.Nullary

-- Propositional equality and its properties.
import Tools.PropositionalEquality

-- Natural numbers and decidability of equality.
import Tools.Nat

---------------------------
-- LANGUAGE INTRODUCTION --
---------------------------

-- Syntax and semantics of weakening and substitution.
import Definition.Untyped

-- Propositional equality properties: Equalities between expressions,
-- weakenings, substitutions and their combined composition.
-- (These lemmas are not in the paper.)
import Definition.Untyped.Properties

-- Judgements: Typing rules, conversion, reduction rules
-- and well-formed substitutions and respective equality.
import Definition.Typed

-- Well-formed context extraction and reduction properties.
import Definition.Typed.Properties

-- Well-formed weakening and its properties.
import Definition.Typed.Weakening

------------------------------
-- KRIPKE LOGICAL RELATIONS --
------------------------------

-- Generic equality relation definition.
import Definition.Typed.EqualityRelation

-- The judgemental instance of the generic equality.
import Definition.Typed.EqRelInstance

-- Logical relations definitions.
import Definition.LogicalRelation

-- Properties of logical relation:

-- Reflexivity of the logical relation.
import Definition.LogicalRelation.Properties.Reflexivity

-- Escape lemma for the logical relation.
import Definition.LogicalRelation.Properties.Escape

-- Shape view of two or more types.
import Definition.LogicalRelation.ShapeView

-- Proof irrelevance for the logical relation.
import Definition.LogicalRelation.Irrelevance

-- Weakening of logical relation judgements.
import Definition.LogicalRelation.Weakening

-- Conversion of the logical relation.
import Definition.LogicalRelation.Properties.Conversion

-- Symmetry of the logical relation.
import Definition.LogicalRelation.Properties.Symmetry

-- Transitvity of the logical relation.
import Definition.LogicalRelation.Properties.Transitivity

-- Neutral introduction in the logical relation.
import Definition.LogicalRelation.Properties.Neutral

-- Weak head expansion of the logical relation.
import Definition.LogicalRelation.Properties.Reduction

-- Application in the logical relation.
import Definition.LogicalRelation.Application

-- Validity judgements definitions
import Definition.LogicalRelation.Substitution

-- Properties of validity judgements:

-- Proof irrelevance for the validity judgements.
import Definition.LogicalRelation.Substitution.Irrelevance

-- Properties about valid substitutions:
-- * Substitution well-formedness.
-- * Substitution weakening.
-- * Substitution lifting.
-- * Identity substitution.
-- * Reflexivity, symmetry and transitivity of substitution equality.
import Definition.LogicalRelation.Substitution.Properties

-- Single term substitution of validity judgements.
import Definition.LogicalRelation.Substitution.Introductions.SingleSubst

-- The fundamental theorem.
import Definition.LogicalRelation.Fundamental

-- Certain cases of the logical relation:

-- Validity of Π-types.
import Definition.LogicalRelation.Substitution.Introductions.Pi

-- Validity of applications.
import Definition.LogicalRelation.Substitution.Introductions.Application

-- Validity of λ-terms.
import Definition.LogicalRelation.Substitution.Introductions.Lambda

-- Validity of natural recursion of natural numbers.
import Definition.LogicalRelation.Substitution.Introductions.Natrec

-- Reducibility of well-formedness.
import Definition.LogicalRelation.Fundamental.Reducibility

-- Consequences of the fundamental theorem:

-- Canonicity of the system.
import Definition.Typed.Consequences.Canonicity

-- Injectivity of Π-types.
import Definition.Typed.Consequences.Injectivity

-- Syntactic validitiy of the system.
import Definition.Typed.Consequences.Syntactic

-- All types and terms fully reduce to WHNF.
import Definition.Typed.Consequences.Reduction

-- Strong equality of types.
import Definition.Typed.Consequences.Equality

-- Substiution in judgements and substitution composition.
import Definition.Typed.Consequences.Substitution

-- Uniqueness of the types of neutral terms.
import Definition.Typed.Consequences.NeTypeEq

-- Universe membership of types.
import Definition.Typed.Consequences.InverseUniv

-- Consistency of the type theory.
import Definition.Typed.Consequences.Consistency

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:
{-# OPTIONS --without-K --rewriting #-}

open import lib.Base
open import lib.PathFunctor
open import lib.PathGroupoid
open import lib.path-seq.Reasoning

module lib.path-seq.Ap where

module _ {i j} {A : Type i} {B : Type j} (f : A → B) where

  ap-seq : {a a' : A} → a =-= a' → f a =-= f a'
  ap-seq [] = []
  ap-seq (p ◃∙ s) = ap f p ◃∙ ap-seq s

  private
    ap-seq-∙-= : {a a' : A} → (s : a =-= a')
      → ap f (↯ s) == ↯ (ap-seq s)
    ap-seq-∙-= [] = idp
    ap-seq-∙-= (p ◃∙ []) = idp
    ap-seq-∙-= (idp ◃∙ s@(_ ◃∙ _)) = ap-seq-∙-= s

  ap-seq-∙ : {a a' : A} (s : a =-= a')
    → (ap f (↯ s) ◃∎) =ₛ ap-seq s
  ap-seq-∙ s = =ₛ-in (ap-seq-∙-= s)

  ∙-ap-seq : {a a' : A} (s : a =-= a')
    → ap-seq s =ₛ (ap f (↯ s) ◃∎)
  ∙-ap-seq s = !ₛ (ap-seq-∙ s)

  ap-seq-=ₛ : {a a' : A} {s t : a =-= a'}
    → s =ₛ t
    → ap-seq s =ₛ ap-seq t
  ap-seq-=ₛ {s = s} {t = t} (=ₛ-in p) =
    ap-seq s
      =ₛ⟨ ∙-ap-seq s ⟩
    ap f (↯ s) ◃∎
      =ₛ₁⟨ ap (ap f) p ⟩
    ap f (↯ t) ◃∎
      =ₛ⟨ ap-seq-∙ t ⟩
    ap-seq t ∎ₛ

module _ {i j k} {A : Type i} {B : Type j} {C : Type k} (f : A → B → C) where

  ap2-seq : {a a' : A} {b b' : B} → a =-= a' → b =-= b' → f a b =-= f a' b'
  ap2-seq [] [] = []
  ap2-seq {a = a} [] t@(_ ◃∙ _) = ap-seq (f a) t
  ap2-seq {b = b} s@(_ ◃∙ _) [] = ap-seq (λ a → f a b) s
  ap2-seq (p ◃∙ s) (q ◃∙ t) = ap2 f p q ◃∙ ap2-seq s t

  private
    ap2-seq-∙-= : {a a' : A} {b b' : B}
      (s : a =-= a') (t : b =-= b')
      → ap2 f (↯ s) (↯ t) == ↯ (ap2-seq s t)
    ap2-seq-∙-= [] [] = idp
    ap2-seq-∙-= {a = a} [] t@(_ ◃∙ _) =
      ap2 f idp (↯ t)
        =⟨ ap2-idp-l f (↯ t) ⟩
      ap (f a) (↯ t)
        =⟨ =ₛ-out (ap-seq-∙ (f a) t) ⟩
      ↯ (ap-seq (f a) t) =∎
    ap2-seq-∙-= {b = b} s@(_ ◃∙ _) [] =
      ap2 f (↯ s) idp
        =⟨ ap2-idp-r f (↯ s) ⟩
      ap (λ a → f a b) (↯ s)
        =⟨ =ₛ-out (ap-seq-∙ (λ a → f a b) s ) ⟩
      ↯ (ap-seq (λ a → f a b) s) =∎
    ap2-seq-∙-= (p ◃∙ []) (q ◃∙ []) = idp
    ap2-seq-∙-= {a' = a'} (p ◃∙ []) (q ◃∙ t@(_ ◃∙ _)) =
      ap2 f p (q ∙ ↯ t)
        =⟨ ap (λ r → ap2 f r (q ∙ ↯ t)) (! (∙-unit-r p)) ⟩
      ap2 f (p ∙ idp) (q ∙ ↯ t)
        =⟨ ap2-∙ f p idp q (↯ t) ⟩
      ap2 f p q ∙ ap2 f idp (↯ t)
        =⟨ ap (ap2 f p q ∙_) (ap2-idp-l f (↯ t)) ⟩
      ap2 f p q ∙ ap (f a') (↯ t)
        =⟨ ap (ap2 f p q ∙_) (=ₛ-out (ap-seq-∙ (f a') t)) ⟩
      ap2 f p q ∙ ↯ (ap-seq (f a') t) =∎
    ap2-seq-∙-= {b' = b'} (p ◃∙ s@(_ ◃∙ _)) (q ◃∙ []) =
      ap2 f (p ∙ ↯ s) q
        =⟨ ap (ap2 f (p ∙ ↯ s)) (! (∙-unit-r q)) ⟩
      ap2 f (p ∙ ↯ s) (q ∙ idp)
        =⟨ ap2-∙ f p (↯ s) q idp ⟩
      ap2 f p q ∙ ap2 f (↯ s) idp
        =⟨ ap (ap2 f p q ∙_) (ap2-idp-r f (↯ s)) ⟩
      ap2 f p q ∙ ap (λ a → f a b') (↯ s)
        =⟨ ap (ap2 f p q ∙_) (=ₛ-out (ap-seq-∙ (λ a → f a b') s)) ⟩
      ap2 f p q ∙ ↯ (ap-seq (λ a → f a b') s) =∎
    ap2-seq-∙-= (p ◃∙ s@(_ ◃∙ _)) (q ◃∙ t@(_ ◃∙ _)) =
      ap2 f (p ∙ ↯ s) (q ∙ ↯ t)
        =⟨ ap2-∙ f p (↯ s) q (↯ t) ⟩
      ap2 f p q ∙ ap2 f (↯ s) (↯ t)
        =⟨ ap (ap2 f p q ∙_) (ap2-seq-∙-= s t) ⟩
      ap2 f p q ∙ ↯ (ap2-seq s t) =∎

  ap2-seq-∙ : {a a' : A} {b b' : B}
    (s : a =-= a') (t : b =-= b')
    → ap2 f (↯ s) (↯ t) ◃∎ =ₛ ap2-seq s t
  ap2-seq-∙ s t = =ₛ-in (ap2-seq-∙-= s t)

  ∙-ap2-seq : {a a' : A} {b b' : B}
    (s : a =-= a') (t : b =-= b')
    → ap2-seq s t =ₛ ap2 f (↯ s) (↯ t) ◃∎
  ∙-ap2-seq s t = !ₛ (ap2-seq-∙ s t)

max_stars_repo_name: AntoineAllioux/HoTT-Agda

max_issues_repo_name: AntoineAllioux/HoTT-Agda

max_forks_repo_name: AntoineAllioux/HoTT-Agda


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

--open import HoTT
open import homotopy.3x3.PushoutPushout
open import homotopy.3x3.Transpose
import homotopy.3x3.To as To
import homotopy.3x3.From as From
open import homotopy.3x3.Common

module homotopy.3x3.ToFrom2 {i} (d : Span^2 {i}) where

open Span^2 d
open M d hiding (Pushout^2)
open M (transpose d) using () renaming (A₀∙ to A∙₀; A₂∙ to A∙₂; A₄∙ to A∙₄;
                                        module F₁∙ to F∙₁; f₁∙ to f∙₁;
                                        module F₃∙ to F∙₃; f₃∙ to f∙₃;
                                        v-h-span to h-v-span)
open M using (Pushout^2)

open To d
open From d

open import homotopy.3x3.ToFromInit d

module M2 (c : A₂₂) where

  coh : ∀ {i} {A : Type i} {a b c d : A}
    {p q : a == b} (α : p == q)
    {v w : b == d} {β β' : w == v} (eqβ : β == β')
    {t u : a == c} {ε ε' : u == t} (eqε : ε == ε')
    {r s : c == d} (ζ : r == s)
    (γ : (q , v =□ t , s))
    (δ : (p , w =□ u , r))
    (eq : γ == δ ∙□-i/ ! β' / ε' / ∙□-o/ ! α / ζ /)
    → (α , β , γ =□□ δ , ε , ζ)
  coh idp {β = idp} idp {ε = idp} idp idp _ _ x = x

  end-lemma1 : ap (right ∘ f∙₃) (glue c) == ap (to ∘ i∙₄ ∘ f∙₃) (glue c) :> E₂∙Red.T-lhs c
  end-lemma1 =
    ap (right ∘ f∙₃) (glue c)
         =⟨ ap-∘ right f∙₃ (glue c) ⟩
    ap right (ap f∙₃ (glue c))
         =⟨ ap (ap right) (F∙₃.glue-β c) ⟩
    ap right (ap left (H₁₃ c) ∙ glue (f₂₃ c) ∙ ap right (! (H₃₃ c)))
         =⟨ ap-∙∙`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c)) ⟩
    ap (right ∘ left) (H₁₃ c) ∙ ap right (glue (f₂₃ c)) ∙ ap (right ∘ right) (! (H₃₃ c))
         =⟨ ! (to-from-r-g (f₂₃ c)) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))) ⟩
    ap (right ∘ left) (H₁₃ c) ∙ (ap (to ∘ i∙₄) (glue (f₂₃ c))) ∙ ap (right ∘ right) (! (H₃₃ c))
         =⟨ ! (ap-∙∙`∘`∘ (to ∘ i∙₄) left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))) ⟩
    ap (to ∘ i∙₄) (ap left (H₁₃ c) ∙ glue (f₂₃ c) ∙ ap right (! (H₃₃ c)))
         =⟨ ! (ap (ap (to ∘ i∙₄)) (F∙₃.glue-β c)) ⟩
    ap (to ∘ i∙₄) (ap f∙₃ (glue c))
         =⟨ ∘-ap (to ∘ i∙₄) f∙₃ (glue c) ⟩
    ap (to ∘ i∙₄ ∘ f∙₃) (glue c) ∎

  abstract
   lemma1 : ↓-='-out (apd (to-from-r ∘ f∙₃) (glue c)) == end-lemma1
   lemma1 =
    ↓-='-out (apd (to-from-r ∘ f∙₃) (glue c))

         =⟨ apd-∘'' to-from-r f∙₃ (glue c) (F∙₃.glue-β c) |in-ctx ↓-='-out ⟩

    ↓-='-out (↓-ap-out= (λ b → to (from (right b)) == right b) f∙₃ (glue c) (F∙₃.glue-β c) (apd to-from-r (ap left (H₁₃ c) ∙ glue (f₂₃ c) ∙ ap right (! (H₃₃ c)))))

         =⟨ apd-∙∙`∘`∘ to-from-r left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c)) |in-ctx (λ u → ↓-='-out (↓-ap-out= (λ b → to (from (right b)) == right b) f∙₃ (glue c) (F∙₃.glue-β c) u)) ⟩

    ↓-='-out (↓-ap-out= (λ b → to (from (right b)) == right b) f∙₃ (glue c) (F∙₃.glue-β c) (↓-ap-in _ _ (apd (λ _ → idp) (H₁₃ c)) ∙ᵈ apd to-from-r (glue (f₂₃ c)) ∙ᵈ ↓-ap-in _ _  (apd (λ _ → idp) (! (H₃₃ c)))))

         =⟨ ToFromR.glue-β (f₂₃ c) |in-ctx (λ u → ↓-='-out (↓-ap-out= (λ b → to (from (right b)) == right b) f∙₃ (glue c) (F∙₃.glue-β c)
                                                                      (↓-ap-in _ _ (apd (λ _ → idp) (H₁₃ c)) ∙ᵈ u ∙ᵈ ↓-ap-in _ _  (apd (λ _ → idp) (! (H₃₃ c)))))) ⟩

    ↓-='-out (↓-ap-out= (λ b → to (from (right b)) == right b) f∙₃ (glue c) (F∙₃.glue-β c)
                        (↓-ap-in _ _ (apd (λ _ → idp) (H₁₃ c)) ∙ᵈ ↓-='-in (! (to-from-r-g (f₂₃ c))) ∙ᵈ ↓-ap-in _ _  (apd (λ _ → idp) (! (H₃₃ c)))))

         =⟨ lemma-a _ f∙₃ (glue c) (F∙₃.glue-β c) _ ⟩

    ↓-='-out (↓-ap-in _ _ (apd (λ x → idp {a = right (left x)}) (H₁₃ c)) ∙ᵈ ↓-='-in (! (to-from-r-g (f₂₃ c))) ∙ᵈ ↓-ap-in _ _  (apd (λ _ → idp) (! (H₃₃ c))))
    ∙□-i/ ap-∘ right f∙₃ (glue c) ∙ ap (ap right) (F∙₃.glue-β c)
        / ! (ap (ap (to ∘ i∙₄)) (F∙₃.glue-β c)) ∙ ∘-ap (to ∘ i∙₄) f∙₃ (glue c) /

         =⟨ lemma-b (glue (f₂₃ c)) (apd (λ _ → idp) (H₁₃ c)) (! (to-from-r-g (f₂₃ c))) (apd (λ _ → idp) (! (H₃₃ c))) |in-ctx (λ u → u ∙□-i/ ap-∘ right f∙₃ (glue c) ∙ ap (ap right) (F∙₃.glue-β c)
                                      / ! (ap (ap (to ∘ i∙₄)) (F∙₃.glue-β c)) ∙ ∘-ap (to ∘ i∙₄) f∙₃ (glue c) /) ⟩

    (↓-='-out (apd (λ x → idp {a = right (left x)}) (H₁₃ c))
    ∙□h ((! (to-from-r-g (f₂₃ c)))
    ∙□h (↓-='-out (apd (λ _ → idp) (! (H₃₃ c))))))
    ∙□-i/ ap-∙∙`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))
        / ! (ap-∙∙`∘`∘ (to ∘ i∙₄) left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))) /
    ∙□-i/ ap-∘ right f∙₃ (glue c) ∙ ap (ap right) (F∙₃.glue-β c)
        / ! (ap (ap (to ∘ i∙₄)) (F∙₃.glue-β c)) ∙ ∘-ap (to ∘ i∙₄) f∙₃ (glue c) /

         =⟨ coh3 |in-ctx (λ u → u
                                ∙□-i/ ap-∙∙`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))
                                    / ! (ap-∙∙`∘`∘ (to ∘ i∙₄) left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))) /
                                ∙□-i/ ap-∘ right f∙₃ (glue c) ∙ ap (ap right) (F∙₃.glue-β c)
                                    / ! (ap (ap (to ∘ i∙₄)) (F∙₃.glue-β c)) ∙ ∘-ap (to ∘ i∙₄) f∙₃ (glue c) /) ⟩

    ((! (to-from-r-g (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
    ∙□-i/ ap-∙∙`∘`∘ right left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))
        / ! (ap-∙∙`∘`∘ (to ∘ i∙₄) left right (H₁₃ c) (glue (f₂₃ c)) (! (H₃₃ c))) /
    ∙□-i/ ap-∘ right f∙₃ (glue c) ∙ ap (ap right) (F∙₃.glue-β c)
        / ! (ap (ap (to ∘ i∙₄)) (F∙₃.glue-β c)) ∙ ∘-ap (to ∘ i∙₄) f∙₃ (glue c) /

         =⟨ coh' ⟩
    end-lemma1 ∎  where

      coh' : ∀ {i} {A : Type i} {x y : A} {a b c d e f g h : x == y} {p : a == b} {q : b == c}
        {r : c == d} {s : d == e} {t : e == f} {u : f == g} {v : g == h}
        → (s ∙□-i/ r / t / ∙□-i/ p ∙ q / u ∙ v /) == (a =⟨ p ⟩ b =⟨ q ⟩ c =⟨ r ⟩ d =⟨ s ⟩ e =⟨ t ⟩ f =⟨ u ⟩ g =⟨ v ⟩ h ∎)
      coh' {p = idp} {idp} {idp} {idp} {idp} {idp} {idp} = idp

      coh2 : ∀ {i j} {A : Type i} {B : Type j} {f : A → B} {x y : A} {p : x == y}
        → ↓-='-out (apd (λ x → idp {a = f x}) p) == idp {a = ap f p}
      coh2 {p = idp} = idp

      coh3 : (↓-='-out (apd (λ x → idp {a = right (left x)}) (H₁₃ c))
              ∙□h ((! (to-from-r-g (f₂₃ c)))
              ∙□h (↓-='-out (apd (λ _ → idp) (! (H₃₃ c)))))) == ((! (to-from-r-g (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c))))
      coh3 =
        ↓-='-out (apd (λ x → idp {a = right (left x)}) (H₁₃ c))
        ∙□h ((! (to-from-r-g (f₂₃ c)))
        ∙□h (↓-='-out (apd (λ _ → idp) (! (H₃₃ c)))))

             =⟨ coh2 {f = right ∘ left} {p = H₁₃ c} |in-ctx (λ u → u ∙□h ((! (to-from-r-g (f₂₃ c))) ∙□h (↓-='-out (apd (λ _ → idp) (! (H₃₃ c)))))) ⟩

        idp {a = ap (right ∘ left) (H₁₃ c)} ∙□h ((! (to-from-r-g (f₂₃ c)))
            ∙□h (↓-='-out (apd (λ _ → idp) (! (H₃₃ c)))))

             =⟨ coh2 {f = right ∘ right} {p = ! (H₃₃ c)} |in-ctx (λ u → idp {a = ap (right ∘ left) (H₁₃ c)} ∙□h ((! (to-from-r-g (f₂₃ c))) ∙□h u)) ⟩

        idp {a = ap (right ∘ left) (H₁₃ c)} ∙□h ((! (to-from-r-g (f₂₃ c))) ∙□h idp {a = ap (right ∘ right) (! (H₃₃ c))})

              =⟨ coh4 (ap (right ∘ left) (H₁₃ c)) (ap (right ∘ right) (! (H₃₃ c))) (! (to-from-r-g (f₂₃ c))) ⟩

        ((! (to-from-r-g (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ap (right ∘ right) (! (H₃₃ c)))) ∎  where

          coh4 : ∀ {i} {A : Type i} {x y z t : A} (p : x == y) (q : z == t) {s t : y == z} (r : s == t)
            → (idp {a = p} ∙□h (r ∙□h idp {a = q})) == (r |in-ctx (λ u → p ∙ u ∙ q))
          coh4 idp idp idp = idp

  end-lemma3 : ap (left ∘ f∙₁) (glue c) == ap (to ∘ i∙₀ ∘ f∙₁) (glue c)
  end-lemma3 =
    ap (left ∘ f∙₁) (glue c)
         =⟨ ap-∘ left f∙₁ (glue c) ⟩
    ap left (ap f∙₁ (glue c))
         =⟨ ap (ap left) (F∙₁.glue-β c) ⟩
    ap left (ap left (! (H₁₁ c)) ∙ glue (f₂₁ c) ∙ ap right (H₃₁ c))
         =⟨ ap-∙∙`∘`∘ left left right (! (H₁₁ c)) (glue (f₂₁ c)) (H₃₁ c) ⟩
    ap (left ∘ left) (! (H₁₁ c)) ∙ ap left (glue (f₂₁ c)) ∙ ap (left ∘ right) (H₃₁ c)
         =⟨ ! (to-from-l-g (f₂₁ c)) |in-ctx (λ u → ap (left ∘ left) (! (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)) ⟩
    ap (left ∘ left) (! (H₁₁ c)) ∙ (ap (to ∘ i∙₀) (glue (f₂₁ c))) ∙ ap (left ∘ right) (H₃₁ c)
         =⟨ ! (ap-∙∙`∘`∘ (to ∘ i∙₀) left right (! (H₁₁ c)) (glue (f₂₁ c)) (H₃₁ c)) ⟩
    ap (to ∘ i∙₀) (ap left (! (H₁₁ c)) ∙ glue (f₂₁ c) ∙ ap right (H₃₁ c))
         =⟨ ! (ap (ap (to ∘ i∙₀)) (F∙₁.glue-β c)) ⟩
    ap (to ∘ i∙₀) (ap f∙₁ (glue c))
         =⟨ ∘-ap (to ∘ i∙₀) f∙₁ (glue c) ⟩
    ap (to ∘ i∙₀ ∘ f∙₁) (glue c) ∎

  lemma3 : ↓-='-out (apd (to-from-l ∘ f∙₁) (glue c)) == end-lemma3
  lemma3 =
    ↓-='-out (apd (to-from-l ∘ f∙₁) (glue c))

      =⟨ apd-∘'' to-from-l f∙₁ (glue c) (F∙₁.glue-β c) |in-ctx ↓-='-out ⟩

    ↓-='-out (↓-ap-out= (λ b → to (from (left b)) == left b) f∙₁ (glue c) (F∙₁.glue-β c) (apd to-from-l (ap left (! (H₁₁ c)) ∙ glue (f₂₁ c) ∙ ap right (H₃₁ c))))

      =⟨ lemma-a _ f∙₁ (glue c) (F∙₁.glue-β c) (apd to-from-l (ap left (! (H₁₁ c)) ∙ glue (f₂₁ c) ∙ ap right (H₃₁ c))) ⟩

    ↓-='-out (apd to-from-l (ap left (! (H₁₁ c)) ∙ glue (f₂₁ c) ∙ ap right (H₃₁ c)))
    ∙□-i/ ap-∘ left f∙₁ (glue c) ∙ ap (ap left) (F∙₁.glue-β c) / ! (ap (ap (to ∘ from ∘ left)) (F∙₁.glue-β c)) ∙ ∘-ap (to ∘ from ∘ left) f∙₁ (glue c) /

      =⟨ apd-∙∙`∘`∘ to-from-l left right (! (H₁₁ c)) (glue (f₂₁ c)) (H₃₁ c) |in-ctx
         (λ u → ↓-='-out u ∙□-i/ ap-∘ left f∙₁ (glue c) ∙ ap (ap left) (F∙₁.glue-β c) / ! (ap (ap (to ∘ from ∘ left)) (F∙₁.glue-β c)) ∙ ∘-ap (to ∘ from ∘ left) f∙₁ (glue c) /) ⟩

    ↓-='-out (↓-ap-in _ _ (apd (λ _ → idp) (! (H₁₁ c))) ∙ᵈ apd to-from-l (glue (f₂₁ c)) ∙ᵈ ↓-ap-in _ _ (apd (λ _ → idp) (H₃₁ c)))
    ∙□-i/ ap-∘ left f∙₁ (glue c) ∙ ap (ap left) (F∙₁.glue-β c) / ! (ap (ap (to ∘ from ∘ left)) (F∙₁.glue-β c)) ∙ ∘-ap (to ∘ from ∘ left) f∙₁ (glue c) /

      =⟨ ToFromL.glue-β (f₂₁ c) |in-ctx (λ u → ↓-='-out (↓-ap-in _ _ (apd (λ _ → idp) (! (H₁₁ c))) ∙ᵈ u ∙ᵈ ↓-ap-in _ _ (apd (λ _ → idp) (H₃₁ c)))
         ∙□-i/ ap-∘ left f∙₁ (glue c) ∙ ap (ap left) (F∙₁.glue-β c) / ! (ap (ap (to ∘ from ∘ left)) (F∙₁.glue-β c)) ∙ ∘-ap (to ∘ from ∘ left) f∙₁ (glue c) /) ⟩

    ↓-='-out (↓-ap-in _ _ (apd (λ _ → idp) (! (H₁₁ c))) ∙ᵈ ↓-='-in (! (to-from-l-g (f₂₁ c))) ∙ᵈ ↓-ap-in _ _ (apd (λ _ → idp) (H₃₁ c)))
    ∙□-i/ ap-∘ left f∙₁ (glue c) ∙ ap (ap left) (F∙₁.glue-β c) / ! (ap (ap (to ∘ from ∘ left)) (F∙₁.glue-β c)) ∙ ∘-ap (to ∘ from ∘ left) f∙₁ (glue c) /

      =⟨ lemma-b (glue (f₂₁ c)) (apd (λ _ → idp) (! (H₁₁ c))) (! (to-from-l-g (f₂₁ c))) (apd (λ _ → idp) (H₃₁ c))
         |in-ctx (λ u → u ∙□-i/ ap-∘ left f∙₁ (glue c) ∙ ap (ap left) (F∙₁.glue-β c) / ! (ap (ap (to ∘ from ∘ left)) (F∙₁.glue-β c)) ∙ ∘-ap (to ∘ from ∘ left) f∙₁ (glue c) /) ⟩

    (↓-='-out (apd (λ _ → idp) (! (H₁₁ c))) ∙□h ((! (to-from-l-g (f₂₁ c))) ∙□h ↓-='-out (apd (λ _ → idp) (H₃₁ c))))
    ∙□-i/ ap-∙∙`∘`∘ left left right (! (H₁₁ c)) (glue (f₂₁ c)) (H₃₁ c) / ! (ap-∙∙`∘`∘ (to ∘ i∙₀) left right (! (H₁₁ c)) (glue (f₂₁ c)) (H₃₁ c)) /
    ∙□-i/ ap-∘ left f∙₁ (glue c) ∙ ap (ap left) (F∙₁.glue-β c) / ! (ap (ap (to ∘ from ∘ left)) (F∙₁.glue-β c)) ∙ ∘-ap (to ∘ from ∘ left) f∙₁ (glue c) /

      =⟨ coh2 (left ∘ left) (left ∘ right) (! (H₁₁ c)) (! (to-from-l-g (f₂₁ c))) (H₃₁ c) |in-ctx (λ u →
         u ∙□-i/ ap-∙∙`∘`∘ left left right (! (H₁₁ c)) (glue (f₂₁ c)) (H₃₁ c) / ! (ap-∙∙`∘`∘ (to ∘ i∙₀) left right (! (H₁₁ c)) (glue (f₂₁ c)) (H₃₁ c)) /
    ∙□-i/ ap-∘ left f∙₁ (glue c) ∙ ap (ap left) (F∙₁.glue-β c) / ! (ap (ap (to ∘ from ∘ left)) (F∙₁.glue-β c)) ∙ ∘-ap (to ∘ from ∘ left) f∙₁ (glue c) /) ⟩

    ((! (to-from-l-g (f₂₁ c))) |in-ctx (λ u → ap (left ∘ left) (! (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)))
    ∙□-i/ ap-∙∙`∘`∘ left left right (! (H₁₁ c)) (glue (f₂₁ c)) (H₃₁ c) / ! (ap-∙∙`∘`∘ (to ∘ i∙₀) left right (! (H₁₁ c)) (glue (f₂₁ c)) (H₃₁ c)) /
    ∙□-i/ ap-∘ left f∙₁ (glue c) ∙ ap (ap left) (F∙₁.glue-β c) / ! (ap (ap (to ∘ from ∘ left)) (F∙₁.glue-β c)) ∙ ∘-ap (to ∘ from ∘ left) f∙₁ (glue c) /

      =⟨ coh3 ⟩

    end-lemma3 ∎  where

      coh2 : ∀ {i i' j} {A : Type i} {A' : Type i'} {B : Type j} (f : A → B) (f' : A' → B)
             {a b : A} {a' b' : A'} (p : a == b) {s s' : f b == f' a'} (q : s == s') (r : a' == b')
             → (↓-='-out (apd (λ x → idp) p) ∙□h (q ∙□h (↓-='-out (apd (λ _ → idp) r))))
               == (q |in-ctx (λ u → ap f p ∙ u ∙ ap f' r))
      coh2 f f' idp idp idp = idp

      coh3 : ∀ {i} {A : Type i} {x y : A} {a b c d e f g h : x == y} {p : a == b} {q : b == c}
        {r : c == d} {s : d == e} {t : e == f} {u : f == g} {v : g == h}
        → (s ∙□-i/ r / t / ∙□-i/ p ∙ q / u ∙ v /) == (a =⟨ p ⟩ b =⟨ q ⟩ c =⟨ r ⟩ d =⟨ s ⟩ e =⟨ t ⟩ f =⟨ u ⟩ g =⟨ v ⟩ h ∎)
      coh3 {p = idp} {idp} {idp} {idp} {idp} {idp} {idp} = idp

{- Lemma 2 -}

  lemma2-7 =
    ↓-='-out (ap↓ (ap to) (apd (glue {d = v-h-span}) (glue c)))

         =⟨ to-glue-glue-β c |in-ctx ↓-='-out ⟩

    ↓-='-out (↓-='-in (E₂∙Red.coh c (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                                      ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /)
                       ∙□-i/ E₂∙Red.lhs-o c / E₂∙Red.rhs-o c /)
              ◃/ To.glue-β (left (f₂₁ c)) / ! (To.glue-β (right (f₂₃ c))) /)

         =⟨ thing _ (To.glue-β (left (f₂₁ c))) _ ⟩

    E₂∙Red.coh c (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                   ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /)
    ∙□-i/ E₂∙Red.lhs-o c / E₂∙Red.rhs-o c /
    ∙□-o/ To.glue-β (left (f₂₁ c)) / ! (To.glue-β (right (f₂₃ c))) / ∎

  lemma2-6 =
    ap□ to (↓-='-out (apd (glue {d = v-h-span}) (glue c)))

         =⟨ ap□-↓-='-out-β _ _ to (apd (glue {d = v-h-span}) (glue c)) ⟩

    ↓-='-out (ap↓ (ap to) (apd (glue {d = v-h-span}) (glue c)))
    ∙□-i/ ∘-ap to (right ∘ f₃∙) (glue c) / ap-∘ to (left ∘ f₁∙) (glue c) /

         =⟨ lemma2-7 |in-ctx (λ u → (u ∙□-i/ ∘-ap to (right ∘ f₃∙) (glue c) / ap-∘ to (left ∘ f₁∙) (glue c) /)) ⟩

    E₂∙Red.coh c (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                   ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /)
    ∙□-i/ E₂∙Red.lhs-o c / E₂∙Red.rhs-o c /
    ∙□-o/ To.glue-β (left (f₂₁ c)) / ! (To.glue-β (right (f₂₃ c))) /
    ∙□-i/ ∘-ap to (right ∘ f₃∙) (glue c) / ap-∘ to (left ∘ f₁∙) (glue c) / ∎

  lemma2-5 =
    ap□ to (↓-='-out (apd (glue {d = v-h-span}) (glue c))
              ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)

         =⟨ ap□-∙□-i/ to _ (E∙₂Red.lhs-i c) _ ⟩

    ap□ to (↓-='-out (apd (glue {d = v-h-span}) (glue c)))
    ∙□-i/ ap (ap to) (E∙₂Red.lhs-i c) / ap (ap to) (E∙₂Red.rhs-i c) /

         =⟨ lemma2-6 |in-ctx (λ u → u ∙□-i/ ap (ap to) (E∙₂Red.lhs-i c) / ap (ap to) (E∙₂Red.rhs-i c) /) ⟩

    E₂∙Red.coh c (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                   ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /)
    ∙□-i/ E₂∙Red.lhs-o c / E₂∙Red.rhs-o c /
    ∙□-o/ To.glue-β (left (f₂₁ c)) / ! (To.glue-β (right (f₂₃ c))) /
    ∙□-i/ ∘-ap to (right ∘ f₃∙) (glue c) / ap-∘ to (left ∘ f₁∙) (glue c) /
    ∙□-i/ ap (ap to) (E∙₂Red.lhs-i c) / ap (ap to) (E∙₂Red.rhs-i c) / ∎

  lemma2'-1 =
    E∙₂Red.ap-ap-coh!-lhs-i c to ∙ ap (ap to) (E∙₂Red.lhs-i c) ∙ ∘-ap to (right ∘ f₃∙) (glue c) ∙ E₂∙Red.lhs-o c

         =⟨ eq1 {f = ap to}
                {q = ! (ap-∙∙`∘`∘ right left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c))}
                { ! (ap (ap right) (F₃∙.glue-β c))}
                { ! (F₃∙.glue-β c) |in-ctx (ap right)}
                (!-ap (ap right) (F₃∙.glue-β c))
                {∘-ap right f₃∙ (glue c)}
                {p = E∙₂Red.ap-ap-coh!-lhs-i c to}
                {∘-ap to (right ∘ f₃∙) (glue c)}
                {ap-∘ i₄∙ f₃∙ (glue c)}
                {F₃∙.glue-β c |in-ctx (ap i₄∙)}
                {ap-∙∙`∘`∘ i₄∙ left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c)}
                {I₄∙.glue-β (f₃₂ c) |in-ctx (λ u → ap (left ∘ right) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c))}
          ⟩

    (! (ap-∙∙`∘`∘ to (right ∘ left) (right ∘ right) (H₃₁ c) (ap right (glue (f₃₂ c))) (H₃₃ c))
     ∙ ap (ap to) (! (ap-∙∙`∘`∘ right left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c)))
     ∙ (ap (ap to) (! (F₃∙.glue-β c) |in-ctx (ap right))
        ∙ (ap (ap to) (∘-ap right f₃∙ (glue c))
           ∙ ∘-ap to (right ∘ f₃∙) (glue c)
           ∙ ap-∘ i₄∙ f₃∙ (glue c))
        ∙ (F₃∙.glue-β c |in-ctx (ap i₄∙)))
     ∙ ap-∙∙`∘`∘ i₄∙ left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c))
    ∙ (I₄∙.glue-β (f₃₂ c) |in-ctx (λ u → ap (left ∘ right) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c)))

         =⟨ ap-∘^3-coh to right f₃∙ (glue c) |in-ctx (λ u →
    (! (ap-∙∙`∘`∘ to (right ∘ left) (right ∘ right) (H₃₁ c) (ap right (glue (f₃₂ c))) (H₃₃ c))
     ∙ ap (ap to) (! (ap-∙∙`∘`∘ right left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c)))
     ∙ (ap (ap to) (! (F₃∙.glue-β c) |in-ctx (ap right))
        ∙ u
        ∙ (F₃∙.glue-β c |in-ctx (ap i₄∙)))
     ∙ ap-∙∙`∘`∘ i₄∙ left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c))
    ∙ (I₄∙.glue-β (f₃₂ c) |in-ctx (λ u → ap (left ∘ right) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c))))
          ⟩

    (! (ap-∙∙`∘`∘ to (right ∘ left) (right ∘ right) (H₃₁ c) (ap right (glue (f₃₂ c))) (H₃₃ c))
     ∙ ap (ap to) (! (ap-∙∙`∘`∘ right left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c)))
     ∙ (ap (ap to) (! (F₃∙.glue-β c) |in-ctx (ap right))
        ∙ ∘-ap to right (ap f₃∙ (glue c))
        ∙ (F₃∙.glue-β c |in-ctx (ap i₄∙)))
     ∙ ap-∙∙`∘`∘ i₄∙ left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c))
    ∙ (I₄∙.glue-β (f₃₂ c) |in-ctx (λ u → ap (left ∘ right) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c)))

         =⟨ ap-∘-ap-coh to right (F₃∙.glue-β c) |in-ctx (λ u →
    (! (ap-∙∙`∘`∘ to (right ∘ left) (right ∘ right) (H₃₁ c) (ap right (glue (f₃₂ c))) (H₃₃ c))
     ∙ ap (ap to) (! (ap-∙∙`∘`∘ right left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c)))
     ∙ u
     ∙ ap-∙∙`∘`∘ i₄∙ left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c))
    ∙ (I₄∙.glue-β (f₃₂ c) |in-ctx (λ u → ap (left ∘ right) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c)))) ⟩

    (! (ap-∙∙`∘`∘ to (right ∘ left) (right ∘ right) (H₃₁ c) (ap right (glue (f₃₂ c))) (H₃₃ c))
     ∙ ap (ap to) (! (ap-∙∙`∘`∘ right left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c)))
     ∙ ∘-ap to right (ap left (H₃₁ c) ∙ glue (f₃₂ c) ∙ ap right (H₃₃ c))
     ∙ ap-∙∙`∘`∘ i₄∙ left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c))
    ∙ (I₄∙.glue-β (f₃₂ c) |in-ctx (λ u → ap (left ∘ right) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c)))

         =⟨ ap-∘-ap-∙∙3`∘`∘-coh to right left right (H₃₁ c) (glue (f₃₂ c)) (H₃₃ c) |in-ctx (λ u →
                 u ∙ (I₄∙.glue-β (f₃₂ c) |in-ctx (λ u → ap (left ∘ right) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c)))) ⟩

    (∘-ap to right (glue (f₃₂ c)) |in-ctx (λ u → ap (left ∘ right) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c)))
    ∙ (I₄∙.glue-β (f₃₂ c) |in-ctx (λ u → ap (left ∘ right) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c)))

         =⟨ ∙-|in-ctx (λ u → ap (left ∘ right) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c)) (∘-ap to right (glue (f₃₂ c))) (I₄∙.glue-β (f₃₂ c)) ⟩

    ((∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c)) |in-ctx (λ u → ap (left ∘ right) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c))) ∎

    where

      eq1 : ∀ {i j} {A : Type i} {B : Type j} {f : A → B} {a b c d : A}
        {q : a == b} {r r' : b == c} (e : r == r') {s : c == d}
        {g h k l m n : B} {p : g == f a} {t : f d == h} {u : h == k}
        {v : k == l} {w : l == m} {x : m == n}
         → p ∙ ap f (_ =⟨ q ⟩ _ =⟨ r ⟩ _ =⟨ s ⟩ _ ∎) ∙ t
           ∙ (_ =⟨ u ⟩ _ =⟨ v ⟩ _ =⟨ w ⟩ _ =⟨ x ⟩ _ ∎)
         == (p ∙ ap f q ∙ (ap f r' ∙ (ap f s ∙ t ∙ u) ∙ v) ∙ w) ∙ x
      eq1 {q = idp} {idp} {.idp} idp {idp} {p = p} {idp} {idp} {idp} {idp} {idp} = ! (∙-unit-r (p ∙ idp))

  lemma2'-2 :
    E₂∙Red.rhs-o c
    ∙ ap-∘ to (left ∘ f₁∙) (glue c)
    ∙ ap (ap to) (E∙₂Red.rhs-i c)
    ∙ E∙₂Red.ap-ap-coh!-rhs-i c to
    == (! (∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c)) |in-ctx (λ u → ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (right ∘ left) (H₁₃ c)))
  lemma2'-2 =
    E₂∙Red.rhs-o c ∙ ap-∘ to (left ∘ f₁∙) (glue c) ∙ ap (ap to) (E∙₂Red.rhs-i c) ∙ E∙₂Red.ap-ap-coh!-rhs-i c to

      =⟨ eq1 {f = ap to}
             {p = ! (I₀∙.glue-β (f₁₂ c) |in-ctx (λ u → (ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (right ∘ left) (H₁₃ c))))}
             { ! (ap-∙∙`∘`∘ i₀∙ left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c))}
             { ! (F₁∙.glue-β c |in-ctx ap i₀∙)}
             {∘-ap i₀∙ f₁∙ (glue c)}
             {ap-∘ to (left ∘ f₁∙) (glue c)}
             {ap-∘ left f₁∙ (glue c)}
             {F₁∙.glue-β c |in-ctx (ap left)}
             {ap-∙∙`∘`∘ left left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c)}
             {ap-∙∙`∘`∘ to (left ∘ left) (left ∘ right) (H₁₁ c) (ap left (glue (f₁₂ c))) (H₁₃ c)}
       ⟩

    (! (I₀∙.glue-β (f₁₂ c) |in-ctx (λ u → (ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (right ∘ left) (H₁₃ c)))))
    ∙ ((! (ap-∙∙`∘`∘ i₀∙ left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c)))
       ∙ ((! (F₁∙.glue-β c |in-ctx (λ u → ap i₀∙ u)))
          ∙ (∘-ap i₀∙ f₁∙ (glue c)
             ∙ ap-∘ to (left ∘ f₁∙) (glue c)
             ∙ ap (ap to) (ap-∘ left f₁∙ (glue c)))
          ∙ ap (ap to) (F₁∙.glue-β c |in-ctx (ap left)))
       ∙ ap (ap to) (ap-∙∙`∘`∘ left left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c))
       ∙ ap-∙∙`∘`∘ to (left ∘ left) (left ∘ right) (H₁₁ c) (ap left (glue (f₁₂ c))) (H₁₃ c))

      =⟨ ap-∘^3-coh' to left f₁∙ (glue c)
         |in-ctx (λ u → (! (I₀∙.glue-β (f₁₂ c) |in-ctx (λ u → (ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (right ∘ left) (H₁₃ c)))))
    ∙ ((! (ap-∙∙`∘`∘ i₀∙ left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c)))
       ∙ ((! (F₁∙.glue-β c |in-ctx (λ u → ap i₀∙ u)))
          ∙ u
          ∙ ap (ap to) (F₁∙.glue-β c |in-ctx (ap left)))
       ∙ ap (ap to) (ap-∙∙`∘`∘ left left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c))
       ∙ ap-∙∙`∘`∘ to (left ∘ left) (left ∘ right) (H₁₁ c) (ap left (glue (f₁₂ c))) (H₁₃ c))) ⟩

    (! (I₀∙.glue-β (f₁₂ c) |in-ctx (λ u → (ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (right ∘ left) (H₁₃ c)))))
    ∙ ((! (ap-∙∙`∘`∘ i₀∙ left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c)))
       ∙ ((! (F₁∙.glue-β c |in-ctx (ap i₀∙)))
          ∙ ap-∘ to left (ap f₁∙ (glue c))
          ∙ ap (ap to) (F₁∙.glue-β c |in-ctx (ap left)))
       ∙ ap (ap to) (ap-∙∙`∘`∘ left left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c))
       ∙ ap-∙∙`∘`∘ to (left ∘ left) (left ∘ right) (H₁₁ c) (ap left (glue (f₁₂ c))) (H₁₃ c))

      =⟨ ap-∘-ap-coh'2 to left (F₁∙.glue-β c)
         |in-ctx (λ u → (! (I₀∙.glue-β (f₁₂ c) |in-ctx (λ u → (ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (right ∘ left) (H₁₃ c)))))
    ∙ ((! (ap-∙∙`∘`∘ i₀∙ left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c)))
       ∙ u
       ∙ ap (ap to) (ap-∙∙`∘`∘ left left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c))
       ∙ ap-∙∙`∘`∘ to (left ∘ left) (left ∘ right) (H₁₁ c) (ap left (glue (f₁₂ c))) (H₁₃ c))) ⟩

    (! (I₀∙.glue-β (f₁₂ c) |in-ctx (λ u → (ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (right ∘ left) (H₁₃ c)))))
    ∙ ((! (ap-∙∙`∘`∘ i₀∙ left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c)))
       ∙ ap-∘ to left (ap left (H₁₁ c) ∙ glue (f₁₂ c) ∙ ap right (H₁₃ c))
       ∙ ap (ap to) (ap-∙∙`∘`∘ left left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c))
       ∙ ap-∙∙`∘`∘ to (left ∘ left) (left ∘ right) (H₁₁ c) (ap left (glue (f₁₂ c))) (H₁₃ c))

      =⟨ ap-∘-ap-∙∙2`∘`∘-coh to left left right (H₁₁ c) (glue (f₁₂ c)) (H₁₃ c)
         |in-ctx (λ u → (! (I₀∙.glue-β (f₁₂ c) |in-ctx (λ u → (ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (right ∘ left) (H₁₃ c)))) ∙ u)) ⟩

    (! (I₀∙.glue-β (f₁₂ c) |in-ctx (λ u → (ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (right ∘ left) (H₁₃ c)))))
    ∙ (ap-∘ to left (glue (f₁₂ c)) |in-ctx (λ u → ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (right ∘ left) (H₁₃ c)))

      =⟨ coh2 (glue (f₁₂ c)) (I₀∙.glue-β (f₁₂ c)) ⟩

    (! (∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c)) |in-ctx (λ u → ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (right ∘ left) (H₁₃ c))) ∎

    where

      eq1 : ∀ {i j} {A : Type i} {B : Type j} {f : A → B} {a b c d e : B} {k l m n : A} {o : B}
         {p : a == b} {q : b == c} {r : c == d} {s : d == e} {t : e == f k} {u : k == l}
         {v : l == m} {w : m == n} {x : f n == o}
         → (_ =⟨ p ⟩ _ =⟨ q ⟩ _ =⟨ r ⟩ _ =⟨ s ⟩ _ ∎) ∙ t ∙ ap f (_ =⟨ u ⟩ _ =⟨ v ⟩ _ =⟨ w ⟩ _ ∎) ∙ x
         == (p ∙ (q ∙ ((r ∙ (s ∙ t ∙ ap f u) ∙ ap f v) ∙ ap f w ∙ x)))
      eq1 {p = idp} {idp} {idp} {idp} {t = t} {idp} {idp} {idp} {idp} = ! (∙-unit-r (t ∙ idp)) ∙ ! (∙-unit-r ((t ∙ idp) ∙ idp))

      coh2 : ∀ {i j k l} {A : Type i} {B : Type j} {C : Type k} {D : Type l}
        {a a' : A} (q : a == a') {h : A → B} {g : B → C} {f : (g (h a) == g (h a')) → D} {r : g (h a) == g (h a')} (p : ap (g ∘ h) q == r)
        → (! (p |in-ctx f)) ∙ (ap-∘ g h q |in-ctx f) == (! (∘-ap g h q ∙ p) |in-ctx f)
      coh2 idp idp = idp

  lemma2-4' =
    ap□ to (↓-='-out (apd (glue {d = v-h-span}) (glue c))
              ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
    ∙□-i/ E∙₂Red.ap-ap-coh!-lhs-i c to / E∙₂Red.ap-ap-coh!-rhs-i c to /

         =⟨ lemma2-5 |in-ctx (λ u → u ∙□-i/ E∙₂Red.ap-ap-coh!-lhs-i c to / E∙₂Red.ap-ap-coh!-rhs-i c to /) ⟩

    E₂∙Red.coh c (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                  ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /)
    ∙□-i/ E₂∙Red.lhs-o c / E₂∙Red.rhs-o c /
    ∙□-o/ To.glue-β (left (f₂₁ c)) / ! (To.glue-β (right (f₂₃ c))) /
    ∙□-i/ ∘-ap to (right ∘ f₃∙) (glue c) / ap-∘ to (left ∘ f₁∙) (glue c) /
    ∙□-i/ ap (ap to) (E∙₂Red.lhs-i c) / ap (ap to) (E∙₂Red.rhs-i c) /
    ∙□-i/ E∙₂Red.ap-ap-coh!-lhs-i c to / E∙₂Red.ap-ap-coh!-rhs-i c to /

         =⟨ assoc (E₂∙Red.coh c (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                   ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /))
                   (E₂∙Red.lhs-o c) (∘-ap to (right ∘ f₃∙) (glue c)) (ap (ap to) (E∙₂Red.lhs-i c))
                   (E∙₂Red.ap-ap-coh!-lhs-i c to) _ _ _ _ (To.glue-β (left (f₂₁ c))) _ ⟩

    E₂∙Red.coh c (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                   ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /)
    ∙□-o/ To.glue-β (left (f₂₁ c)) / ! (To.glue-β (right (f₂₃ c))) /
    ∙□-i/ E∙₂Red.ap-ap-coh!-lhs-i c to ∙ ap (ap to) (E∙₂Red.lhs-i c) ∙ ∘-ap to (right ∘ f₃∙) (glue c) ∙ E₂∙Red.lhs-o c
        / E₂∙Red.rhs-o c ∙ ap-∘ to (left ∘ f₁∙) (glue c) ∙ ap (ap to) (E∙₂Red.rhs-i c) ∙ E∙₂Red.ap-ap-coh!-rhs-i c to /

         =⟨ ∙□-i/-rewrite (E₂∙Red.coh c (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                   ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /)
    ∙□-o/ To.glue-β (left (f₂₁ c)) / ! (To.glue-β (right (f₂₃ c))) /) lemma2'-1 lemma2'-2 ⟩

    E₂∙Red.coh c (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                   ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /)
    ∙□-o/ To.glue-β (left (f₂₁ c)) / ! (To.glue-β (right (f₂₃ c))) /
    ∙□-i/ (∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c)) |in-ctx (λ u → ap (left ∘ right) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c))
        / (! (∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c))) |in-ctx (λ u → ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (right ∘ left) (H₁₃ c)) / ∎  where

      assoc : ∀ {i} {A : Type i} {a b b' c : A} {u u' : a == b} {v v1 v2 v3 v4 : b == c}
         {w w1 w2 w3 w4 : a == b'} {x x' : b' == c} (α : (u , v =□ w , x))
         (p1 : v1 == v) (p2 : v2 == v1) (p3 : v3 == v2) (p4 : v4 == v3)
         (q1 : w == w1) (q2 : w1 == w2) (q3 : w2 == w3) (q4 : w3 == w4)
         (r : u' == u) (s : x == x')
         → α ∙□-i/ p1 / q1 / ∙□-o/ r / s / ∙□-i/ p2 / q2 / ∙□-i/ p3 / q3 / ∙□-i/ p4 / q4 /
         == α ∙□-o/ r / s / ∙□-i/ p4 ∙ p3 ∙ p2 ∙ p1 / q1 ∙ q2 ∙ q3 ∙ q4 /
      assoc α idp idp idp idp idp idp idp idp idp idp = idp

  lemma2-4'' =
    E∙₂Red.ap-ap-coh! c to (ap□ to (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                                       ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
                             ∙□-i/ E∙₂Red.ap-ap-coh!-lhs-i c to / E∙₂Red.ap-ap-coh!-rhs-i c to /)

         =⟨ lemma2-4' |in-ctx (E∙₂Red.ap-ap-coh! c to) ⟩

    E∙₂Red.ap-ap-coh! c to (E₂∙Red.coh c (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                                            ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /)
                             ∙□-o/ To.glue-β (left (f₂₁ c)) / ! (To.glue-β (right (f₂₃ c))) /
                             ∙□-i/ (∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c)) |in-ctx (λ u → ap (left ∘ right) (H₃₁ c) ∙ u ∙ ap (right ∘ right) (H₃₃ c))
                                 / (! (∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c))) |in-ctx (λ u → ap (left ∘ left) (H₁₁ c) ∙ u ∙ ap (right ∘ left) (H₁₃ c))/)

         =⟨ lemma! (∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c)) (To.glue-β (right (f₂₃ c))) (To.glue-β (left (f₂₁ c))) (∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c))
                   (↓-='-out (apd (glue {d = h-v-span}) (glue c))
                   ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /) ⟩

    ↓-='-out (apd (glue {d = h-v-span}) (glue c))
    ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /
    ∙□-o/ ∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c) / ! (∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c)) /
    ∙□-i/ (To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c)))
        / (! (To.glue-β (left (f₂₁ c)))) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)) / ∎

  lemma2-4 =
    ap□ to (E∙₂Red.coh! c (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                            ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /))

         =⟨ E∙₂Red.ap-ap-coh!-β c to (↓-='-out (apd (glue {d = v-h-span}) (glue c)) ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /) ⟩

    E∙₂Red.ap-ap-coh! c to (ap□ to (↓-='-out (apd (glue {d = v-h-span}) (glue c))
                                       ∙□-i/ E∙₂Red.lhs-i c / E∙₂Red.rhs-i c /)
                             ∙□-i/ E∙₂Red.ap-ap-coh!-lhs-i c to / E∙₂Red.ap-ap-coh!-rhs-i c to /)
    ∙□-i/ E∙₂Red.ap-ap-coh!-lhs-o c to / E∙₂Red.ap-ap-coh!-rhs-o c to /

         =⟨ lemma2-4'' |in-ctx (λ u → u ∙□-i/ E∙₂Red.ap-ap-coh!-lhs-o c to / E∙₂Red.ap-ap-coh!-rhs-o c to /) ⟩

    ↓-='-out (apd (glue {d = h-v-span}) (glue c))
    ∙□-i/ E₂∙Red.lhs-i c / E₂∙Red.rhs-i c /
    ∙□-o/ ∘-ap to left (glue (f₁₂ c)) ∙ I₀∙.glue-β (f₁₂ c) / ! (∘-ap to right (glue (f₃₂ c)) ∙ I₄∙.glue-β (f₃₂ c)) /
    ∙□-i/ (To.glue-β (right (f₂₃ c))) |in-ctx (λ u → ap (right ∘ left) (H₁₃ c) ∙ u ∙ ! (ap (right ∘ right) (H₃₃ c)))
        / (! (To.glue-β (left (f₂₁ c)))) |in-ctx (λ u → ! (ap (left ∘ left) (H₁₁ c)) ∙ u ∙ ap (left ∘ right) (H₃₁ c)) /
    ∙□-i/ E∙₂Red.ap-ap-coh!-lhs-o c to / E∙₂Red.ap-ap-coh!-rhs-o c to / ∎

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
open import Common
open import Global
open import Projection
open import Local

open import Data.Fin
open import Data.Product
open import Data.Vec
open import Relation.Binary.PropositionalEquality

n = 4

Role = Fin n

p : Role
p = zero

q : Role
q = suc zero

r : Role
r = suc (suc zero)

s : Role
s = suc (suc (suc zero))

l : Label
l = 0

l′ : Label
l′ = 1

g₁ : Global n
g₁ = msgSingle′ p q l endG

lp : Local n
lp = sendSingle q l endL

g₁-proj-p-is-lp : project g₁ p ≡ lp
g₁-proj-p-is-lp = refl

lq : Local n
lq = recvSingle p l endL

g₁-proj-q-is-lq : project g₁ q ≡ lq
g₁-proj-q-is-lq = refl

p→q : Action n
p→q = action′ p q l

r→s : Action n
r→s = action′ r s l′

g₂ : Global n
g₂ = msgSingle′ r s l′ g₁

g₂′ : Global n
g₂′ = msgSingle′ r s l′ endG

g₁→end : g₁ - p→q →g endG
g₁→end = →g-prefix

g₂→g₁ : g₂ - r→s →g g₁
g₂→g₁ = →g-prefix

g₂→g₂′ : g₂ - p→q →g g₂′
g₂→g₂′ = →g-cont g₁→end (λ ()) (λ ()) (λ ()) (λ ())

g₁-proj-p→end : (p , project g₁ p) - p→q →l (p , endL)
g₁-proj-p→end = →l-send p refl λ ()

g₁-proj-q→end : (q , project g₁ q) - p→q →l (q , endL)
g₁-proj-q→end = →l-recv q refl λ ()

g₂-proj-p→g₂′-proj-p : (p , project g₂ p) - p→q →l (p , project g₂′ p)
g₂-proj-p→g₂′-proj-p = →l-send p refl λ ()

g₂-proj-q→g₂′-proj-q : (q , project g₂ q) - p→q →l (q , project g₂′ q)
g₂-proj-q→g₂′-proj-q = →l-recv q refl λ ()

c₁ : Configuration n
c₁ = lp ∷ lq ∷ endL ∷ endL ∷ []

cEnd : Configuration n
cEnd = endL ∷ endL ∷ endL ∷ endL ∷ []

c₁→cEnd : c₁ - p→q →c cEnd
c₁→cEnd = →c-comm c₁ (λ ()) refl refl refl g₁-proj-p→end g₁-proj-q→end

g₁↔c₁ : g₁ ↔ c₁
g₁↔c₁ = record { isProj = refls }
  where
    refls : (p : Fin n) -> lookup c₁ p ≡ project g₁ p
    refls zero = refl
    refls (suc zero) = refl
    refls (suc (suc zero)) = refl
    refls (suc (suc (suc zero))) = refl

max_stars_repo_name: fangyi-zhou/mpst-in-agda

max_issues_repo_name: fangyi-zhou/mpst-in-agda

max_forks_repo_name: fangyi-zhou/mpst-in-agda


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

open import LogicalFormulae
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Integers.RingStructure.Ring
open import Semirings.Definition
open import Rings.Orders.Partial.Definition
open import Rings.Orders.Total.Definition
open import Orders.Total.Definition
open import Orders.Partial.Definition
open import Setoids.Orders.Total.Definition

module Numbers.Integers.Order where

infix 5 _<Z_
record _<Z_ (a : ℤ) (b : ℤ) : Set where
  constructor le
  field
    x : ℕ
    proof : (nonneg (succ x)) +Z a ≡ b

lessLemma : (a x : ℕ) → succ x +N a ≡ a → False
lessLemma zero x pr = naughtE (equalityCommutative pr)
lessLemma (succ a) x pr = lessLemma a x q
  where
    q : succ x +N a ≡ a
    q rewrite Semiring.commutative ℕSemiring a (succ x) | Semiring.commutative ℕSemiring x a | Semiring.commutative ℕSemiring (succ a) x = succInjective pr

irreflexive : (x : ℤ) → x <Z x → False
irreflexive (nonneg x) record { x = y ; proof = proof } = lessLemma x y (nonnegInjective proof)
irreflexive (negSucc a) record { x = x ; proof = proof } = naughtE (equalityCommutative q)
  where
    pr' : nonneg (succ x) +Z (negSucc a +Z nonneg (succ a)) ≡ negSucc a +Z nonneg (succ a)
    pr' rewrite +ZAssociative (nonneg (succ x)) (negSucc a) (nonneg (succ a)) = applyEquality (λ t → t +Z nonneg (succ a)) proof
    pr'' : nonneg (succ x) +Z nonneg 0 ≡ nonneg 0
    pr'' rewrite equalityCommutative (additiveInverseExists a) = identityOfIndiscernablesLeft _≡_ pr' q
      where
        q : nonneg (succ x) +Z (negSucc a +Z nonneg (succ a)) ≡ nonneg (succ (x +N 0))
        q rewrite Semiring.commutative ℕSemiring x 0 | additiveInverseExists a | Semiring.commutative ℕSemiring x 0 = refl
    pr''' : succ x +N 0 ≡ 0
    pr''' = nonnegInjective pr''
    q : succ x ≡ 0
    q rewrite Semiring.commutative ℕSemiring 0 (succ x) = pr'''

lessZTransitive : {a b c : ℤ} → (a <Z b) → (b <Z c) → (a <Z c)
lessZTransitive {a} {b} {c} (le d1 pr1) (le d2 pr2) rewrite equalityCommutative pr1 = le (d1 +N succ d2) pr
  where
    pr : nonneg (succ (d1 +N succ d2)) +Z a ≡ c
    pr rewrite +ZAssociative (nonneg (succ d2)) (nonneg (succ d1)) a | Semiring.commutative ℕSemiring (succ d2) (succ d1) = pr2

lessInherits : {a b : ℕ} → (a <N b) → ((nonneg a) <Z (nonneg b))
_<Z_.x (lessInherits {a} {b} (le x proof)) = x
_<Z_.proof (lessInherits {a} {.(succ (x +N a))} (le x refl)) = refl

lessInheritsNegsucc : {a b : ℕ} → (a <N b) → ((negSucc b) <Z negSucc a)
_<Z_.x (lessInheritsNegsucc {a} {b} (le x proof)) = x
_<Z_.proof (lessInheritsNegsucc {a} {b} (le x proof)) rewrite equalityCommutative proof = transitivity (transitivity (+ZCommutative (nonneg x) (negSucc (x +N a))) (applyEquality (λ i → negSucc i +Z nonneg x) (Semiring.commutative ℕSemiring x a))) (equalityCommutative (negSucc+Nonneg a x))

lessNegsuccNonneg : {a b : ℕ} → (negSucc a <Z nonneg b)
_<Z_.x (lessNegsuccNonneg {a} {b}) = a +N b
_<Z_.proof (lessNegsuccNonneg {zero} {b}) = refl
_<Z_.proof (lessNegsuccNonneg {succ a} {b}) = _<Z_.proof (lessNegsuccNonneg {a} {b})

lessThanTotalZ : {a b : ℤ} → ((a <Z b) || (b <Z a)) || (a ≡ b)
lessThanTotalZ {nonneg a} {nonneg b} with TotalOrder.totality ℕTotalOrder a b
lessThanTotalZ {nonneg a} {nonneg b} | inl (inl a<b) = inl (inl (lessInherits a<b))
lessThanTotalZ {nonneg a} {nonneg b} | inl (inr b<a) = inl (inr (lessInherits b<a))
lessThanTotalZ {nonneg a} {nonneg b} | inr a=b = inr (applyEquality nonneg a=b)
lessThanTotalZ {nonneg a} {negSucc b} = inl (inr (lessNegsuccNonneg {b} {a}))
lessThanTotalZ {negSucc a} {nonneg x} = inl (inl (lessNegsuccNonneg {a} {x}))
lessThanTotalZ {negSucc a} {negSucc b} with TotalOrder.totality ℕTotalOrder a b
... | inl (inl a<b) = inl (inr (lessInheritsNegsucc a<b))
... | inl (inr b<a) = inl (inl (lessInheritsNegsucc b<a))
lessThanTotalZ {negSucc a} {negSucc .a} | inr refl = inr refl

ℤOrder : TotalOrder ℤ
PartialOrder._<_ (TotalOrder.order ℤOrder) = _<Z_
PartialOrder.irreflexive (TotalOrder.order ℤOrder) {a} = irreflexive a
PartialOrder.<Transitive (TotalOrder.order ℤOrder) = lessZTransitive
TotalOrder.totality ℤOrder a b = lessThanTotalZ {a} {b}

orderRespectsAddition : (a b : ℤ) → a <Z b → (c : ℤ) → a +Z c <Z b +Z c
orderRespectsAddition (nonneg a) (nonneg b) (le x proof) (nonneg c) = le x (transitivity (+ZAssociative (nonneg (succ x)) (nonneg a) (nonneg c)) (applyEquality (_+Z nonneg c) proof))
orderRespectsAddition (nonneg a) (nonneg b) (le x proof) (negSucc c) = le x (transitivity (+ZAssociative (nonneg (succ x)) (nonneg a) (negSucc c)) (applyEquality (_+Z negSucc c) proof))
orderRespectsAddition (negSucc a) (nonneg b) (le x proof) (nonneg c) = le x (transitivity (+ZAssociative (nonneg (succ x)) (negSucc a) (nonneg c)) (applyEquality (_+Z nonneg c) proof))
orderRespectsAddition (negSucc a) (nonneg b) (le x proof) (negSucc c) = le x (transitivity (+ZAssociative (nonneg (succ x)) (negSucc a) (negSucc c)) (applyEquality (_+Z negSucc c) proof))
orderRespectsAddition (negSucc a) (negSucc b) (le x proof) (nonneg c) = le x (transitivity (+ZAssociative (nonneg (succ x)) (negSucc a) (nonneg c)) (applyEquality (_+Z nonneg c) proof))
orderRespectsAddition (negSucc a) (negSucc b) (le x proof) (negSucc c) = le x (transitivity (+ZAssociative (nonneg (succ x)) (negSucc a) (negSucc c)) (applyEquality (_+Z negSucc c) proof))

orderRespectsMultiplication : (a b : ℤ) → nonneg 0 <Z a → nonneg 0 <Z b → nonneg 0 <Z a *Z b
orderRespectsMultiplication (nonneg (succ a)) (nonneg (succ b)) 0<a 0<b = lessInherits (succIsPositive (b +N a *N succ b))

ℤPOrderedRing : PartiallyOrderedRing ℤRing (SetoidTotalOrder.partial (totalOrderToSetoidTotalOrder ℤOrder))
PartiallyOrderedRing.orderRespectsAddition ℤPOrderedRing {a} {b} = orderRespectsAddition a b
PartiallyOrderedRing.orderRespectsMultiplication ℤPOrderedRing {a} {b} = orderRespectsMultiplication a b

ℤOrderedRing : TotallyOrderedRing ℤPOrderedRing
TotallyOrderedRing.total ℤOrderedRing = totalOrderToSetoidTotalOrder ℤOrder


text:
module Data.Option where

import      Lvl
open import Data
open import Type

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level
private variable T : Type{ℓ}

data Option (T : Type{ℓ}) : Type{ℓ} where
  None : Option(T)
  Some : T → Option(T)

elim : ∀{A : Type{ℓ₁}}{B : Option(A) → Type{ℓ₂}} → B(None) → ((a : A) → B(Some a)) → ((o : Option(A)) → B(o))
elim b _  None     = b
elim b ab (Some a) = ab a

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-# OPTIONS --universe-polymorphism #-}

module IDesc where

--********************************************
-- Prelude
--********************************************

-- Some preliminary stuffs, to avoid relying on the stdlib

--****************
-- Universe polymorphism
--****************

data Level : Set where
      zero : Level
      suc  : Level -> Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO zero  #-}
{-# BUILTIN LEVELSUC  suc   #-}

max : Level -> Level -> Level
max  zero    m      = m
max (suc n)  zero   = suc n
max (suc n) (suc m) = suc (max n m)

{-# BUILTIN LEVELMAX max #-}

data Lifted {l : Level} (A : Set l) : Set (suc l) where
       lifter : A → Lifted A

lift : {i : Level} -> Set i -> Set (suc i)
lift x =  Lifted x

unlift : {l : Level}{A : Set l} -> Lifted A -> A
unlift (lifter a) = a

--****************
-- Sigma and friends
--****************

data Sigma {i j : Level}(A : Set i) (B : A -> Set j) : Set (max i j) where
  _,_ : (x : A) (y : B x) -> Sigma A B

pair : {i j : Level}{A : Set i}{B : A -> Set j} ->
       (x : A) (y : B x) -> Sigma {i = i}{j = j} A B
pair x y = x , y

_*_ : {i j : Level}(A : Set i)(B : Set j) -> Set (max i j)
A * B = Sigma A \_ -> B

fst : {i j : Level}{A : Set i}{B : A -> Set j} -> Sigma A B -> A
fst (a , _) = a

snd : {i j : Level}{A : Set i}{B : A -> Set j} (p : Sigma A B) -> B (fst p)
snd (a , b) = b

data Zero {i : Level} : Set i where
data Unit  {i : Level} : Set i where
  Void : Unit

--****************
-- Sum and friends
--****************

data _+_ {i j : Level}(A : Set i)(B : Set j) : Set (max i j) where
  l : A -> A + B
  r : B -> A + B

--****************
-- Equality
--****************

data _==_ {l : Level}{A : Set l}(x : A) : A -> Set l where
  refl : x == x

cong : {l m : Level}{A : Set l}{B : Set m}
       (f : A -> B){x y : A} -> x == y -> f x == f y
cong f refl = refl

cong2 : {l m n : Level}{A : Set l}{B : Set m}{C : Set n}
        (f : A -> B -> C){x y : A}{z t : B} ->
        x == y -> z == t -> f x z == f y t
cong2 f refl refl = refl

trans : {l : Level}{A : Set l}{x y z : A} -> x == y -> y == z -> x == z
trans refl refl = refl

proof-lift-unlift-eq : {l : Level}{A : Set l}(x : Lifted A) -> lifter (unlift x) == x
proof-lift-unlift-eq (lifter a) = refl

postulate
  reflFun : {l m : Level}{A : Set l}{B : Set m}(f : A -> B)(g : A -> B)-> ((a : A) -> f a == g a) -> f == g

--********************************************
-- Desc code
--********************************************

data IDesc {l : Level}(I : Set (suc l)) : Set (suc l) where
  var : I -> IDesc I
  const : Set l -> IDesc I
  prod : IDesc I -> IDesc I -> IDesc I
  sigma : (S : Set l) -> (S -> IDesc I) -> IDesc I
  pi : (S : Set l) -> (S -> IDesc I) -> IDesc I

--********************************************
-- Desc interpretation
--********************************************

desc : {l : Level}{I : Set (suc l)} -> IDesc I -> (I -> Set l) -> Set l
desc (var i) P = P i
desc (const X) P = X
desc (prod D D') P = desc D P * desc D' P
desc (sigma S T) P = Sigma S (\s -> desc (T s) P)
desc (pi S T) P = (s : S) -> desc (T s) P

--********************************************
-- Fixpoint construction
--********************************************

data IMu {l : Level}{I : Set (suc l)}(R : I -> IDesc {l = l} I)(i : I) : Set l where
  con : desc (R i) (\j -> IMu R j) -> IMu R i

--********************************************
-- Predicate: Box
--********************************************

box : {l : Level}{I : Set (suc l)}(D : IDesc I)(X : I -> Set l) -> desc D X -> IDesc (Sigma I X)
box (var i)     X x        = var (i , x)
box (const _)   X x        = const Unit
box (prod D D') X (d , d') = prod (box D X d) (box D' X d')
box (sigma S T) X (a , b)  = box (T a) X b
box (pi S T)    X f        = pi S (\s -> box (T s) X (f s))

--********************************************
-- Elimination principle: induction
--********************************************

module Elim {l : Level}
            {I : Set (suc l)}
            (R : I -> IDesc I)
            (P : Sigma I (IMu R) -> Set l)
            (m : (i : I)
                 (xs : desc (R i) (IMu R))
                 (hs : desc (box (R i) (IMu R) xs) P) ->
                 P ( i , con xs ))
       where

  mutual
    induction : (i : I)(x : IMu R i) -> P (i , x)
    induction i (con xs) = m i xs (hyps (R i) xs)

    hyps : (D : IDesc I) ->
           (xs : desc D (IMu R)) ->
           desc (box D (IMu R) xs) P
    hyps (var i) x = induction i x
    hyps (const X) x = Void
    hyps (prod D D') (d , d') =  hyps D d , hyps D' d'
    hyps (pi S R) f = \ s -> hyps (R s) (f s)
    hyps (sigma S R) ( a , b ) = hyps (R a) b

induction : {l : Level}
            {I : Set (suc l)}
            (R : I -> IDesc I)
            (P : Sigma I (IMu R) -> Set l)
            (m : (i : I)
                 (xs : desc (R i) (IMu R))
                 (hs : desc (box (R i) (IMu R) xs) P) ->
                 P ( i , con xs)) ->
            (i : I)(x : IMu R i) -> P ( i , x )
induction = Elim.induction

--********************************************
-- DescD
--********************************************

data DescDConst {l : Level} : Set l where
  lvar   : DescDConst
  lconst : DescDConst
  lprod  : DescDConst
  lpi    : DescDConst
  lsigma : DescDConst

descDChoice : {l : Level} -> Set (suc l) -> DescDConst -> IDesc Unit
descDChoice I lvar = const I
descDChoice _ lconst = const (Set _)
descDChoice _ lprod = prod (var Void) (var Void)
descDChoice _ lpi = sigma (Set _) (\S -> pi (lift S) (\s -> var Void))
descDChoice _ lsigma = sigma (Set _) (\S -> pi (lift S) (\s -> var Void))

IDescD : {l : Level}(I : Set (suc l)) -> IDesc {l = suc l} Unit
IDescD I = sigma DescDConst (descDChoice I)

IDescl0 : {l : Level}(I : Set (suc l)) -> Unit -> Set (suc l)
IDescl0 {x} I = IMu {l = suc x} (\_ -> IDescD {l = x} I)

IDescl : {l : Level}(I : Set (suc l)) -> Set (suc l)
IDescl I = IDescl0 I Void

varl : {l : Level}{I : Set (suc l)}(i : I) -> IDescl I
varl {x} i = con (lvar {l = suc x} , i)

constl : {l : Level}{I : Set (suc l)}(X : Set l) -> IDescl I
constl {x} X = con (lconst {l = suc x} , X)

prodl : {l : Level}{I : Set (suc l)}(D D' : IDescl I) -> IDescl I
prodl {x} D D' = con (lprod {l = suc x} , (D , D'))

pil : {l : Level}{I : Set (suc l)}(S : Set l)(T : S -> IDescl I) -> IDescl I
pil {x} S T = con (lpi {l = suc x} , pair {i = suc x}{j = suc x} S (\s -> T (unlift s)))

sigmal : {l : Level}{I : Set (suc l)}(S : Set l)(T : S -> IDescl I) -> IDescl I
sigmal {x} S T = con (lsigma {l = suc x} , pair {i = suc x}{j = suc x} S (\s -> T (unlift s)))

--********************************************
-- From the embedding to the host
--********************************************

cases : {l : Level}
        {I : Set (suc l)}
        (xs : desc (IDescD I) (IMu (λ _ -> IDescD I)))
        (hs : desc (box (IDescD I) (IMu (λ _ -> IDescD I)) xs) (λ _ -> IDesc I)) ->
        IDesc I
cases ( lvar , i ) hs =  var i
cases ( lconst , X ) hs =  const X
cases ( lprod , (D , D') ) ( d , d' ) =  prod d d'
cases ( lpi , ( S , T ) ) hs =  pi S (\s -> hs (lifter s) )
cases ( lsigma , ( S , T ) ) hs = sigma S (\s -> hs (lifter s))

phi : {l : Level}{I : Set (suc l)} -> IDescl I -> IDesc I
phi {x} {I} d = induction (\_ -> IDescD I) (\_ -> IDesc I) (\_ -> cases) Void d

--********************************************
-- From the host to the embedding
--********************************************

psi : {l : Level}{I : Set (suc l)} -> IDesc I -> IDescl I
psi (var i) = varl i
psi (const X) = constl X
psi (prod D D') = prodl (psi D) (psi D')
psi (pi S T) = pil S (\s -> psi (T s))
psi (sigma S T) = sigmal S (\s -> psi (T s))

--********************************************
-- Isomorphism proof
--********************************************

-- From host to host

proof-phi-psi : {l : Level}{I : Set (suc l)} -> (D : IDesc I) -> phi (psi D) == D
proof-phi-psi (var i) = refl
proof-phi-psi (const x) = refl
proof-phi-psi (prod D D') with proof-phi-psi D | proof-phi-psi D'
...  | p | q = cong2 prod p q
proof-phi-psi {x} (pi S T) = cong (pi S)
                                  (reflFun (\s -> phi (psi (T s)))
                                           T
                                           (\s -> proof-phi-psi (T s)))
proof-phi-psi (sigma S T) = cong (sigma S)
                                 (reflFun (\ s -> phi (psi (T s)))
                                          T
                                          (\s -> proof-phi-psi (T s)))

-- From embedding to embedding

proof-psi-phi : {l : Level}(I : Set (suc l)) -> (D : IDescl I) -> psi (phi D) == D
proof-psi-phi {x} I D =  induction (\ _ -> IDescD I)
                               P
                               proof-psi-phi-cases
                               Void
                               D
    where P : Sigma Unit (IMu (\ x -> IDescD I)) -> Set (suc x)
          P ( Void , D ) = psi (phi D) == D
          proof-psi-phi-cases : (i : Unit)
                                (xs : desc (IDescD I) (IDescl0 I))
                                (hs : desc (box (IDescD I) (IDescl0 I) xs) P)
                                -> P (i , con xs)
          proof-psi-phi-cases Void (lvar , i) hs = refl
          proof-psi-phi-cases Void (lconst , x) hs = refl
          proof-psi-phi-cases Void (lprod , ( D , D' )) ( p , q ) = cong2 prodl p q
          proof-psi-phi-cases Void (lpi , ( S , T )) hs = cong (\T -> con (lpi {l = suc x} , ( S , T ) ))
                                                               (trans (reflFun (\ s -> psi (phi (T (lifter (unlift s)))))
                                                                               (\ s -> psi (phi (T (s))))
                                                                               (\s -> cong (\ s -> psi (phi (T (s))))
                                                                                (proof-lift-unlift-eq s)))
                                                                       (reflFun (\s -> psi (phi (T s)))
                                                                                T
                                                                                hs))
          proof-psi-phi-cases Void (lsigma , ( S , T )) hs = cong (\T -> con (lsigma {l = suc x} , ( S , T ) ))
                                                                  (trans (reflFun (\ s → psi (phi (T (lifter (unlift s)))))
                                                                                (\ s → psi (phi (T (s))))
                                                                                (\s -> cong (\ s -> psi (phi (T (s))))
                                                                                (proof-lift-unlift-eq s)))
                                                                         (reflFun (\s -> psi (phi (T s)))
                                                                                T
                                                                                hs))

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram


text:
open import OutsideIn.Prelude
open import OutsideIn.X
module OutsideIn.Instantiations.Simple where
  open import Data.Fin hiding (_+_)

  data Type ( n :  Set) : Set where
    funTy : Type n
    _·_   : Type n → Type n → Type n
    Var   : n → Type n

  private
    fmap-τ : ∀ {a b} → (a → b) → Type a → Type b
    fmap-τ f (funTy) = funTy
    fmap-τ f (x · y) = fmap-τ f x · fmap-τ f y
    fmap-τ f (Var v) = Var (f v)
    fmap-τ-id : ∀   {A : Set} {f : A → A} → isIdentity f → isIdentity (fmap-τ f)
    fmap-τ-id {f = f} isid {funTy} = refl
    fmap-τ-id {f = f} isid {α ·  β} = cong₂ _·_  (fmap-τ-id isid) (fmap-τ-id isid)
    fmap-τ-id {f = f} isid {Var  v} = cong Var isid
    fmap-τ-comp : {A B C : Set} {f : A → B} {g : B → C} {x : Type A}
                → fmap-τ (g ∘ f) x ≡ fmap-τ g (fmap-τ f x)
    fmap-τ-comp {x = funTy} = refl
    fmap-τ-comp {x = α ·  β} = cong₂ _·_ fmap-τ-comp fmap-τ-comp
    fmap-τ-comp {x = Var v}  = cong Var refl

  type-is-functor : Functor Type
  type-is-functor = record { map = fmap-τ
                           ; identity = fmap-τ-id
                           ; composite = fmap-τ-comp
                           }
  type-is-monad : Monad Type
  type-is-monad = record { is-functor = type-is-functor
                         ; point = Var
                         ; join = join-τ
                         ; is-left-ident  = left-id
                         ; is-right-ident = refl
                         ; >=>-assoc = λ {_}{_}{_}{_}{_}{_}{c}{v} → assoc {τ = c v}
                         }
     where join-τ :{a : Set} → Type (Type a)  → Type a
           join-τ (funTy) = funTy
           join-τ (x · y) = join-τ x · join-τ y
           join-τ (Var v) = v

           open Functor (type-is-functor)
           assoc : ∀{A B C}{a : B → Type C}{b : A → Type B}{τ : Type A}
                 → join-τ (fmap-τ a (join-τ (fmap-τ b τ)))
                 ≡ join-τ (fmap-τ (λ v' → join-τ (fmap-τ a (b v'))) τ)
           assoc {a = a}{b}{funTy} = refl
           assoc {a = a}{b}{α  · β} = cong₂ _·_  (assoc {τ = α}) (assoc {τ = β})
           assoc {a = a}{b}{Var  v} = refl
           left-id : ∀ {a}{τ : Type a} → join-τ (Var <$> τ) ≡ τ
           left-id {_}{funTy} = refl
           left-id {_}{α ·  β} = cong₂ _·_  (left-id {τ = α}) (left-id {τ = β})
           left-id {_}{Var  v} = refl

  data SConstraint (x : Set) : Set where
     _∼_ : Type x → Type x → SConstraint x
     _∧′_ : SConstraint x → SConstraint x → SConstraint x
     ε : SConstraint x

  sconstraint-is-functor : Functor SConstraint
  sconstraint-is-functor = record { map = s-map; identity = s-ident; composite = s-comp }
     where open Functor (type-is-functor)
           s-map : {A B : Set} → (A → B) → SConstraint A → SConstraint B
           s-map f (ε) = ε
           s-map f (a ∼ b) = map f a ∼ map f b
           s-map f (a ∧′ b) = s-map f a ∧′ s-map f b
           s-ident : {A : Set} {f : A → A} → isIdentity f → isIdentity (s-map f)
           s-ident isid {ε} = refl
           s-ident isid {a ∼ b} = cong₂ _∼_ (identity isid) (identity isid)
           s-ident isid {a ∧′ b} = cong₂ _∧′_ (s-ident isid) (s-ident isid)
           s-comp : {A B C : Set} {f : A → B} {g : B → C} {x : SConstraint A}
                  → s-map (g ∘ f) x ≡ s-map g (s-map f x)
           s-comp {x = ε} = refl
           s-comp {x = a ∼ b} = cong₂ _∼_ composite composite
           s-comp {x = a ∧′ b} = cong₂ _∧′_ s-comp s-comp

  _⟶_ : ∀ {n} → Type n → Type n → Type n
  a ⟶ b = (funTy · a) · b

  types : Types
  types = record { Type = Type
                 ; type-is-monad = type-is-monad
                 ; funType = _⟶_; appType = _·_
                 }

  data SVar (tc : Set)(n : ℕ) : Set where
    base : tc → SVar tc n
    unification : Fin n → SVar tc n

  thin : {n : ℕ} → Fin (suc n) → Fin n → Fin (suc n)
  thin zero y          = suc y
  thin (suc x) zero    = zero
  thin (suc x) (suc y) = suc (thin x y)

  thick : ∀ {n} → (x y : Fin (suc n)) → Ⓢ (Fin n)
  thick zero zero = zero
  thick zero (suc y) = suc y
  thick {zero } (suc ()) _
  thick {suc _} (suc x)  zero = suc zero
  thick {suc _} (suc x) (suc y) with thick x y
  ... | zero = zero
  ... | suc n = suc (suc n)

  check : ∀ {tc}{n} → Fin (suc n) → Type (SVar tc (suc n)) → Ⓢ (Type (SVar tc n))
  check x (funTy) = suc funTy
  check x (Var (base v)) = suc (Var (base v))
  check x (Var (unification n)) = map (Var ∘ unification) (thick x n)
   where open Functor (Monad.is-functor Ⓢ-is-monad)
  check x (a · b) = check x a >>= λ a′ →
                     check x b >>= λ b′ →
                      unit (a′ · b′)
   where open Monad (Ⓢ-is-monad)

  data AList (tc : Set) : ℕ → ℕ → Set where
    anil : ∀ {n} → AList tc n n
    _asnoc_/_ : ∀ {m n} → AList tc m n → Type (SVar tc m) → Fin (suc m) → AList tc (suc m) n

  _∃asnoc_/_ : ∀ {tc}{m} (a : ∃ (AList tc m)) (t' : Type (SVar tc m)) (x : Fin (suc m))
             →  ∃ (AList tc (suc m))
  (n , σ) ∃asnoc t' / x = n , σ asnoc t' / x

  _for_ : ∀{tc}{n} → (Type (SVar tc n)) → Fin (suc n)
        → SVar tc (suc n) → Type (SVar tc n)
  (t′ for x) (base y) = Var (base y)
  (t′ for x) (unification y) with thick x y
  ... | suc y′ = Var (unification y′)
  ... | zero   = t′

  sub : ∀ {m n}{tc} → AList tc m n → SVar tc m → Type (SVar tc n)
  sub anil = Var
  sub (σ asnoc t / x) = sub σ >=> (t for x)
    where open Monad (type-is-monad)

  flexFlex : ∀ {tc}{m} (x y : Fin m) → ∃ (AList tc m)
  flexFlex {_}{suc m} x y with thick x y
  ...              | suc y′ = m , anil asnoc Var (unification y′) / x
  ...              | zero   = suc m , anil
  flexFlex {_}{zero} () _

  flexRigid : ∀ {tc}{m} (x : Fin m) (t : Type (SVar tc m)) -> Ⓢ (∃(AList tc m))
  flexRigid {_}{suc m} x t with check x t
  ...                      | suc t′ = suc (m , anil asnoc t′ / x)
  ...                      | zero   = zero
  flexRigid {_}{zero} () _

  amgu : ∀{tc}{m} → (Eq tc) → (s t : Type (SVar tc m)) → ∃ (AList tc m) → Ⓢ (∃ (AList tc m))
  amgu eq (funTy) (funTy) acc = suc acc
  amgu eq (Var (base a)) (Var (base b)) acc with eq a b
  ... | true = suc acc
  ... | false = zero
  amgu eq (Var (base a)) (funTy) acc = zero
  amgu eq (funTy) (Var (base b)) acc = zero
  amgu eq (funTy) (a · b) acc = zero
  amgu eq (Var (base _)) (a · b) acc = zero
  amgu eq (a · b) (funTy) acc = zero
  amgu eq (a · b) (Var (base _)) acc = zero
  amgu eq (a · b) (a′ · b′) acc = amgu eq a a′ acc >>= amgu eq b b′
     where open Monad (Ⓢ-is-monad)
  amgu eq (Var (unification x)) (Var (unification y)) (m , anil) = suc (flexFlex x y)
  amgu eq (Var (unification x)) t (m , anil) = flexRigid x t
  amgu eq t (Var (unification x)) (m , anil) = flexRigid x t
  amgu eq s t (n , σ asnoc r / z) = Ⓢ-f.map (λ σ → σ ∃asnoc r / z) (amgu eq (s >>= (r for z))
                                                                             (t >>= (r for z))
                                                                             (n , σ))
    where module Ⓢ-f = Functor (Monad.is-functor Ⓢ-is-monad)
          open Monad (type-is-monad)

  mgu : ∀{tc}{m}(eq : Eq tc)(s t : Type (SVar tc m)) → Ⓢ (∃ (AList tc m))
  mgu {m = m} eq s t = amgu eq s t (m , anil)

  prf : ∀ {m n} → m + suc n ≡ suc m + n
  prf {zero} = refl
  prf {suc n} = cong suc (prf {n})
  prf₂ : ∀ {m} →  m + zero ≡ m
  prf₂ {zero} = refl
  prf₂ {suc n} = cong suc prf₂

  svar-iso₁′ : ∀{m n}{tc} → SVar tc n ⨁ m → SVar tc (m + n)
  svar-iso₁′ {zero} x = x
  svar-iso₁′ {suc m}{n}{tc} v = subst (SVar tc) (prf {m}{n}) (svar-iso₁′ {m}{suc n} (pm-f.map ind v))
   where module pm-f = Functor (Monad.is-functor (PlusN-is-monad {m}))
         ind : ∀{tc}{m} → Ⓢ (SVar tc m) → SVar tc (suc m)
         ind zero = unification zero
         ind (suc n) with n
         ... | base v = base v
         ... | unification x = unification (suc x)

  svar-iso₂′ : ∀{m}{tc} → Fin m → tc ⨁ m
  svar-iso₂′ {zero} ()
  svar-iso₂′ {suc n} zero = pn-m.unit zero
   where module pn-m = Monad (PlusN-is-monad {n})
  svar-iso₂′ {suc n} (suc v) = pm-f.map suc (svar-iso₂′ {n} v)
   where module pm-f = Functor (Monad.is-functor (PlusN-is-monad {n}))

  svar-iso₁ : ∀{m}{tc} → tc ⨁ m → SVar tc m
  svar-iso₁ {m}{tc} v = subst (SVar tc) prf₂ (svar-iso₁′ {m}{zero}{tc} (pm-f.map base v))
   where module pm-f = Functor (Monad.is-functor (PlusN-is-monad {m}))

  svar-iso₂ : ∀{m}{tc} → SVar tc m → tc ⨁ m
  svar-iso₂ {m}{tc} (base v) = pm-m.unit v
   where module pm-m = Monad (PlusN-is-monad {m})
  svar-iso₂ {m}{tc} (unification v) = svar-iso₂′ v

  open Functor (Monad.is-functor type-is-monad) using () renaming (map to τ-map)

  mgu′ : ∀{tc}{m}(eq : Eq tc)(s t : Type (tc ⨁ m)) → Ⓢ (∃ (λ n → tc ⨁ m → Type (tc ⨁ n)))
  mgu′ {tc}{m} eq s t with mgu {tc}{m} eq (τ-map svar-iso₁ s) (τ-map svar-iso₁ t)
  ... | zero = zero
  ... | suc (n , al) = suc (n , τ-map svar-iso₂ ∘ sub al ∘ svar-iso₁)

  data SConstraintShape (x : Set) : Shape → Set where
     _∼_ : Type x → Type x → SConstraintShape x Nullary
     ε : SConstraintShape x Nullary
     _∧′_ : ∀ {a b} → SConstraintShape x a → SConstraintShape x b → SConstraintShape x (Binary a b)

  applySubst : ∀ {a b}{s} → (a → Type b) → SConstraintShape a s → SConstraintShape b s
  applySubst f (a ∼ b) = (a >>= f) ∼ (b >>= f)
    where open Monad (type-is-monad)
  applySubst f (a ∧′ b) = applySubst f a ∧′ applySubst f b
  applySubst f (ε) = ε

  constraint-types : ∀{a b} → (Type a → Type b) → (SConstraint a → SConstraint b)
  constraint-types f ε = ε
  constraint-types f (a ∧′ b) = constraint-types f a ∧′ constraint-types f b
  constraint-types f (a ∼ b) = f a ∼ f b

  applySubst′ : ∀ {a b} → (a → Type b) → SConstraint a  → SConstraint b
  applySubst′ f (a ∼ b) = (a >>= f) ∼ (b >>= f)
    where open Monad (type-is-monad)
  applySubst′ f (a ∧′ b) = applySubst′ f a ∧′ applySubst′ f b
  applySubst′ f (ε) = ε

  data AxiomScheme (n : Set) : Set where
    ax : AxiomScheme n

  coerceAxioms : ∀ {a b} → AxiomScheme a → AxiomScheme b
  coerceAxioms ax = ax

  coerceId : ∀ {x} → isIdentity (coerceAxioms {x} {x})
  coerceId {_}{ax} = refl

  axiom-schemes : AxiomSchemes
  axiom-schemes = record { AxiomScheme = AxiomScheme
                         ; axiomscheme-types = λ f → coerceAxioms
                         ; axiomscheme-is-functor = record { map = λ f → coerceAxioms; identity = λ f → coerceId; composite = λ { {x = ax} → refl }}
                         }

  is-ε : ∀ {m} (x : SConstraint m) → Dec (x ≡ ε)
  is-ε ε = yes refl
  is-ε (a ∧′ b) = no (λ ())
  is-ε (a ∼ b) = no (λ ())

  qconstraints : QConstraints
  qconstraints = record { QConstraint = SConstraint
                        ; qconstraint-is-functor = sconstraint-is-functor
                        ; constraint-types = constraint-types
                        ; _∼_ = _∼_; _∧_ = _∧′_; ε = ε; is-ε = is-ε
                        }

  open Monad (type-is-monad) hiding (_>=>_)
  open Functor (type-is-functor)
  data _,_⊩_ {n : Set}(Q : AxiomScheme n) : SConstraint n → SConstraint n → Set where
    ent-refl  : ∀ {q q′} → Q , (q ∧′ q′) ⊩ q′
    ent-trans : ∀ {q q₁ q₂ q₃} → Q , (q ∧′ q₁) ⊩ q₂ → Q , (q ∧′ q₂) ⊩ q₃ → Q , (q ∧′ q₁) ⊩ q₃
    ent-typeq-refl : ∀ {q}{τ} → Q , q ⊩ (τ ∼ τ)
    ent-typeq-sym : ∀ {q}{τ₁ τ₂} → Q , q ⊩ (τ₁ ∼ τ₂) → Q , q ⊩ (τ₂ ∼ τ₁)
    ent-typeq-trans : ∀ {q}{τ₁ τ₂ τ₃} → Q , q ⊩ (τ₁ ∼ τ₂) → Q , q ⊩ (τ₂ ∼ τ₃) → Q , q ⊩ (τ₁ ∼ τ₃)
    ent-conj : ∀ {q q₁ q₂} → Q , q ⊩ q₁ → Q , q ⊩ q₂ → Q , q ⊩ (q₁ ∧′ q₂)

  ent-subst : ∀ {a b}{θ : a → Type b}{Q : AxiomScheme a}{q q₁ q₂ : SConstraint a} → Q , (q ∧′ q₁) ⊩ q₂ → coerceAxioms Q , constraint-types (join ∘ map θ) (q ∧′ q₁) ⊩ constraint-types (join ∘ map θ) q₂
  ent-subst ent-refl = ent-refl
  ent-subst (ent-trans a b) = ent-trans (ent-subst a) (ent-subst b)
  ent-subst (ent-typeq-refl) = ent-typeq-refl
  ent-subst (ent-typeq-sym a) = ent-typeq-sym (ent-subst a)
  ent-subst (ent-typeq-trans a b) = ent-typeq-trans (ent-subst a) (ent-subst b)
  ent-subst (ent-conj a b) = ent-conj (ent-subst a) (ent-subst b)

  ent-typeq-subst : ∀ {a b}{Q : AxiomScheme a}{q : SConstraint a}{τ₁ τ₂ : Type a}{θ : a → Type b}
                  → Q , q ⊩ (τ₁ ∼ τ₂) → coerceAxioms Q , constraint-types (join ∘ map θ) q
                                      ⊩ ((join ∘ map θ) τ₁ ∼ (join ∘ map θ) τ₂)
  ent-typeq-subst ent-refl = ent-refl
  ent-typeq-subst (ent-trans a b) = ent-trans (ent-subst a) (ent-typeq-subst b)
  ent-typeq-subst (ent-typeq-refl) = ent-typeq-refl
  ent-typeq-subst (ent-typeq-sym a) = ent-typeq-sym (ent-typeq-subst a)
  ent-typeq-subst (ent-typeq-trans a b) = ent-typeq-trans (ent-typeq-subst a) (ent-typeq-subst b)

  shapify : ∀ {a} → SConstraint a → ∃ (SConstraintShape a)
  shapify (a ∼ b) = Nullary , a ∼ b
  shapify (a ∧′ b) with shapify a | shapify b
  ... | r₁ , a′ | r₂ , b′ = Binary r₁ r₂ , a′ ∧′ b′
  shapify (ε) = Nullary , ε

  entailment : Entailment
  entailment = record { _,_⊩_ = _,_⊩_
                      ; ent-refl = ent-refl
                      ; ent-trans = ent-trans
                      ; ent-subst = ent-subst
                      ; ent-typeq-refl = ent-typeq-refl
                      ; ent-typeq-sym = ent-typeq-sym
                      ; ent-typeq-trans = ent-typeq-trans
                      ; ent-typeq-subst = ent-typeq-subst
                      ; ent-conj = ent-conj
                      }

  open SimplificationPrelude ⦃ types ⦄ ⦃ axiom-schemes ⦄ ⦃ qconstraints ⦄ ⦃ entailment ⦄

  constraint : ∀{s}{tc}{m} → Eq tc → SConstraintShape (tc ⨁ m) s  → SimplifierResult tc m
  constraint {Unary _} _ ()
  constraint {Nullary}{m = m} _ ε = m , ε , solved ε Var
  constraint {Nullary}{tc}{m} eq (a ∼ b) = convert (mgu′ {tc}{m} eq a b)
   where
    convert : Ⓢ (∃ (λ n → tc ⨁ m → Type (tc ⨁ n))) →  SimplifierResult tc m
    convert (suc (n , θ)) = n , ε , solved ε θ
    convert zero = m , (a ∼ b) , solved _ Var
  constraint {Binary r₁ r₂}{tc}{m} eq (a ∧′ b)  = convert (constraint {r₁}{tc}{m} eq a)
    where open Monad (type-is-monad)
          _special-∧_ : ∀ {n} → SConstraint n → SConstraint n → SConstraint n
          ε special-∧ n = n
          n special-∧ ε = n
          n special-∧ m = n ∧′ m
          convert :  SimplifierResult tc m →  SimplifierResult tc m
          convert (n , Qr , solved .Qr θ) = convert′ ( constraint {r₂}{tc}{n} eq (applySubst θ b))
            where convert′ :  SimplifierResult tc n →  SimplifierResult tc m
                  convert′ (n′ , Qr′ , solved .Qr′ θ′) = n′ , Qr′ special-∧ applySubst′ θ′ Qr , solved _ (θ′ >=> θ)

  simplifier : {x : Set} → Eq x → (n : ℕ) → AxiomScheme x → SConstraint x
                         → SConstraint (x ⨁ n) → SimplifierResult x n
  simplifier {x} eq n ax con₁ con₂ with shapify con₂
  ... | r , v = constraint {r}{x}{n} eq v

  postulate simplifier-sound : {x : Set} {n : ℕ} {eq : Eq x} (Q : AxiomScheme x) (Qg : SConstraint x) (Qw : SConstraint (x ⨁ n))
                             → IsSound Q Qg Qw (simplifier eq n Q Qg Qw)

  simplification : Simplification
  simplification = record {simplifier = simplifier; simplifier-sound = λ {x}{n}{eq} → simplifier-sound {x}{n}{eq} }

  Simple : (ℕ → Set) → X
  Simple dc = record { dc = dc
                     ; types = types
                     ; axiom-schemes = axiom-schemes
                     ; qconstraints = qconstraints
                     ; entailment = entailment
                     ; simplification = simplification
                     }

max_stars_repo_name: liamoc/outside-in

max_issues_repo_name: liamoc/outside-in

max_forks_repo_name: liamoc/outside-in


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

module Library where

open import Data.Product
  using    ( Σ ; Σ-syntax ; _×_ )
  public

open import Function
  using    ()
  renaming ( id   to λ-id
           ; _∘_  to λ-comp
           ; flip to λ-flip )
  public

open import Level
  using    ( Level )
  renaming ( zero to ℓ-zero
           ; suc  to ℓ-suc
           ; _⊔_  to ℓ-max )
  public

open import Relation.Binary.Core
  using    ( Rel )
  public

open import Relation.Unary
  using    ( Pred )
  public

open import Relation.Binary.PropositionalEquality
  using    ( _≡_ ; module ≡-Reasoning )
  renaming ( refl  to ≡-refl
           ; sym   to ≡-sym
           ; trans to ≡-trans)
  public

open ≡-Reasoning
  using    ( _≡⟨_⟩_ )
  renaming ( begin_ to ≡-proof_
           ; _∎     to _≡-qed )
  public

max_stars_repo_name: gunpinyo/agda-cat

max_issues_repo_name: gunpinyo/agda-cat

max_forks_repo_name: gunpinyo/agda-cat