text:
------------------------------------------------------------------------
-- Overloaded "equational" reasoning combinators
------------------------------------------------------------------------

{-# OPTIONS --safe #-}

module Equational-reasoning where

open import Equality.Propositional
open import Prelude

infix  -1 _■
          finally₁ finally₁∽ finally₁→ finally₁←
          finally₂ finally₂∽ finally₂→ finally₂←
          finally₁-≡∼ finally₁-≡∽ finally₁-≡→ finally₁-≡←
          finally₂-≡∼ finally₂-≡∽ finally₂-≡→ finally₂-≡←
infixr -2 step-⟨⟩∼ step-≡∼ step-≡→ step-∼ step-∼→ step-∼′ step-∼→′
infixl -2 step-⟨⟩∽ step-≡∽ step-≡← step-∽ step-∼← step-∽′ step-∼←′

------------------------------------------------------------------------
-- Reflexivity

record Reflexive {a p} {A : Type a}
                 (P : A → A → Type p) :
                 Type (a ⊔ p) where
  constructor is-reflexive
  field
    reflexive : ∀ {x} → P x x

open Reflexive ⦃ … ⦄ public

_■ : ∀ {a p} {A : Type a} {P : A → A → Type p} ⦃ r : Reflexive P ⦄
     (x : A) → P x x
_ ■ = reflexive

-- Transitivity-like combinators. These combinators can be used when
-- two arguments are definitionally equal. (The Reflexive instance
-- argument is used to make type inference easier.)

step-⟨⟩∼ step-⟨⟩∽ :
  ∀ {a p} {A : Type a} {P : A → A → Type p}
    ⦃ p : Reflexive P ⦄ x {y} →
  P x y → P x y
step-⟨⟩∼ _ p = p
step-⟨⟩∽     = step-⟨⟩∼

syntax step-⟨⟩∼ x Pxy = x ∼⟨⟩ Pxy
syntax step-⟨⟩∽ x Pxy = Pxy ∽⟨⟩ x

-- Transitivity-like combinators. These combinators can be used when
-- two arguments are propositionally equal. (The Reflexive instance
-- argument is used to make type inference easier.)

-- It can be easier for Agda to type-check typical "equational"
-- reasoning chains if the transitivity proof gets the equality
-- arguments in the opposite order, because then the y argument is
-- (perhaps more) known once the proof of P x y is type-checked.
--
-- This optimisation can be quite effective for some examples, but did
-- not seem to have much effect when I applied it to the current code
-- base.
--
-- The idea behind this optimisation came up in discussions with Ulf
-- Norell.

step-≡∼ step-≡∽ step-≡→ step-≡← :
  ∀ {a p} {A : Type a} {P : A → A → Type p}
    ⦃ r : Reflexive P ⦄ x {y z} →
  P y z → x ≡ y → P x z
step-≡∼ _ p refl = p
step-≡∽          = step-≡∼
step-≡→          = step-≡∼
step-≡←          = step-≡∼

syntax step-≡∼ x Pyz x≡y = x ∼≡⟨ x≡y ⟩ Pyz
syntax step-≡∽ x Pyz x≡y = Pyz ∽≡⟨ x≡y ⟩ x
syntax step-≡→ x Pyz x≡y = x →≡⟨ x≡y ⟩ Pyz
syntax step-≡← x Pyz x≡y = Pyz ←≡⟨ x≡y ⟩ x

finally₂-≡∼ finally₂-≡∽ finally₂-≡→ finally₂-≡← :
  ∀ {a p} {A : Type a}
    {P : A → A → Type p}
    ⦃ r : Reflexive P ⦄ x y →
  x ≡ y → P x y
finally₂-≡∼ _ _ refl = reflexive
finally₂-≡∽          = finally₂-≡∼
finally₂-≡→          = finally₂-≡∼
finally₂-≡←          = finally₂-≡∼

syntax finally₂-≡∼ x y x≡y = x ∼≡⟨ x≡y ⟩■ y
syntax finally₂-≡∽ x y x≡y = y ∽≡⟨ x≡y ⟩■ x
syntax finally₂-≡→ x y x≡y = x →≡⟨ x≡y ⟩■ y
syntax finally₂-≡← x y x≡y = y ←≡⟨ x≡y ⟩■ x

finally₁-≡∼ finally₁-≡∽ finally₁-≡→ finally₁-≡← :
  ∀ {a p} {A : Type a}
    {P : A → A → Type p}
    ⦃ r : Reflexive P ⦄ x {y} →
  x ≡ y → P x y
finally₁-≡∼ _ refl = reflexive
finally₁-≡∽        = finally₁-≡∼
finally₁-≡→        = finally₁-≡∼
finally₁-≡←        = finally₁-≡∼

syntax finally₁-≡∼ x x≡y = x ∼≡⟨ x≡y ⟩■
syntax finally₁-≡∽ x x≡y = ∽≡⟨ x≡y ⟩■ x
syntax finally₁-≡→ x x≡y = x →≡⟨ x≡y ⟩■
syntax finally₁-≡← x x≡y = ←≡⟨ x≡y ⟩■ x

------------------------------------------------------------------------
-- Symmetry

record Symmetric {a p} {A : Type a}
                 (P : A → A → Type p) :
                 Type (a ⊔ p) where
  constructor is-symmetric
  field
    symmetric : ∀ {x y} → P x y → P y x

open Symmetric ⦃ … ⦄ public

------------------------------------------------------------------------
-- Transitivity

-- One variant of transitivity.
--
-- Note that the combinator can (depending on the available instances)
-- be used to convert from one type to another, but only in its first
-- argument (in order to make instance resolution easier).

record Transitive {a b p q} {A : Type a} {B : Type b}
                  (P : A → A → Type p) (Q : A → B → Type q) :
                  Type (a ⊔ b ⊔ p ⊔ q) where
  constructor is-transitive
  field
    transitive : ∀ {x y z} → P x y → Q y z → Q x z

open Transitive ⦃ … ⦄ public

step-∼ step-∽ step-∼→ step-∼← :
  ∀ {a b p q} {A : Type a} {B : Type b}
    {P : A → A → Type p} {Q : A → B → Type q}
    ⦃ t : Transitive P Q ⦄ x {y z} →
  Q y z → P x y → Q x z
step-∼ _ = flip transitive
step-∽   = step-∼
step-∼→  = step-∼
step-∼←  = step-∼

syntax step-∼  x Qyz Pxy = x ∼⟨ Pxy ⟩ Qyz
syntax step-∽  x Qyz Pxy = Qyz ∽⟨ Pxy ⟩ x
syntax step-∼→ x Qyz Pxy = x →⟨ Pxy ⟩ Qyz
syntax step-∼← x Qyz Pxy = Qyz ←⟨ Pxy ⟩ x

-- Another variant of transitivity.
--
-- Note that the combinator can (depending on the available instances)
-- be used to convert from one type to another, but only in its second
-- argument (in order to make instance resolution easier).

record Transitive′ {a b p q} {A : Type a} {B : Type b}
                   (P : A → B → Type p) (Q : B → B → Type q) :
                   Type (a ⊔ b ⊔ p ⊔ q) where
  constructor is-transitive
  field
    transitive′ : ∀ {x y z} → P x y → Q y z → P x z

open Transitive′ ⦃ … ⦄ public

step-∼′ step-∽′ step-∼→′ step-∼←′ :
  ∀ {a b p q} {A : Type a} {B : Type b}
    {P : A → B → Type p} {Q : B → B → Type q}
    ⦃ t : Transitive′ P Q ⦄ x {y z} →
  Q y z → P x y → P x z
step-∼′ _ = flip transitive′
step-∽′   = step-∼′
step-∼→′  = step-∼′
step-∼←′  = step-∼′

syntax step-∼′  x Qyz Pxy = x ∼′⟨ Pxy ⟩ Qyz
syntax step-∽′  x Qyz Pxy = Qyz ∽′⟨ Pxy ⟩ x
syntax step-∼→′ x Qyz Pxy = x →′⟨ Pxy ⟩ Qyz
syntax step-∼←′ x Qyz Pxy = Qyz ←′⟨ Pxy ⟩ x

------------------------------------------------------------------------
-- A finally combinator

-- This combinator is intended to be used in the last step of an
-- equational reasoning proof:
--
--   x  ∼⟨ ? ⟩■
--   y
--
-- Note that the combinator can (depending on the available instances)
-- be used to convert from one type to another.

record Convertible {a b p q} {A : Type a} {B : Type b}
                   (P : A → B → Type p) (Q : A → B → Type q) :
                   Type (a ⊔ b ⊔ p ⊔ q) where
  constructor is-convertible
  field
    convert : ∀ {x y} → P x y → Q x y

open Convertible ⦃ … ⦄ public

finally₂ finally₂∽ finally₂→ finally₂← :
  ∀ {a b p q} {A : Type a} {B : Type b}
    {P : A → B → Type p} {Q : A → B → Type q}
    ⦃ c : Convertible P Q ⦄ x y →
  P x y → Q x y
finally₂ _ _ = convert
finally₂∽    = finally₂
finally₂→    = finally₂
finally₂←    = finally₂

syntax finally₂  x y x∼y = x ∼⟨ x∼y ⟩■ y
syntax finally₂∽ x y x∼y = y ∽⟨ x∼y ⟩■ x
syntax finally₂→ x y x→y = x →⟨ x→y ⟩■ y
syntax finally₂← x y x→y = y ←⟨ x→y ⟩■ x

finally₁ finally₁∽ finally₁→ finally₁← :
  ∀ {a b p q} {A : Type a} {B : Type b}
    {P : A → B → Type p} {Q : A → B → Type q}
    ⦃ c : Convertible P Q ⦄ x {y} →
  P x y → Q x y
finally₁ _ = convert
finally₁∽  = finally₁
finally₁→  = finally₁
finally₁←  = finally₁

syntax finally₁  x x∼y = x ∼⟨ x∼y ⟩■
syntax finally₁∽ x x∼y = ∽⟨ x∼y ⟩■ x
syntax finally₁→ x x→y = x →⟨ x→y ⟩■
syntax finally₁← x x→y = ←⟨ x→y ⟩■ x

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
open import Prelude hiding (Bool)

module Implicits.Oliveira.Improved.Deterministic (TC' : Set) (_tc≟'_ : (a b : TC') → Dec (a ≡ b)) where

{-
open import Data.Fin.Substitution
open import Implicits.Oliveira.Types
open import Implicits.Oliveira.Types.Unification
open import Implicits.Oliveira.Terms
open import Implicits.Oliveira.Contexts
open import Implicits.Oliveira.Substitutions
open import Implicits.Oliveira.Improved.Resolution
open import Extensions.ListFirst
-}

-- This is more troublesome than I expected; the tricky thing is the rule r-simp.
-- r-simp requires an instance of first, which has 2 constructors:
--    (a) here: which relies on a proof that r can yield "a" (K ⊢ r ↓ a)
--    (b) there: which relies on a proof that r can NOT yield "a" (¬ K ⊢ r ↓ a)

-- Proving (b) deterministic is nonsensical. Check for example the example below:
-- (we give two ways to derive (b) for a single K, r and a)
-- Because (b) appears in _⊢ᵣ_, this makes _⊢ᵣ_ non-deterministic, which in turn makes
-- the r-iabs case of (a) non-deterministic.
-- The thing is that all non-determinism is situated in the "unhappy-path": (b).
-- Because the exact instance for (b) does not influence rule instantiation,
-- we should be able to give a weaker,
-- but still powerful enough, version of "equivalence" on derivations.

private

  data TC : Set where
    tc-int : TC
    tc-bool : TC

  _tc≟_ : (a b : TC) → Dec (a ≡ b)
  tc-int tc≟ tc-int = yes refl
  tc-int tc≟ tc-bool = no (λ ())
  tc-bool tc≟ tc-int = no (λ ())
  tc-bool tc≟ tc-bool = yes refl

  open import Data.Fin.Substitution
  open import Implicits.Oliveira.Types
  open import Implicits.Oliveira.Types.Unification
  open import Implicits.Oliveira.Terms
  open import Implicits.Oliveira.Contexts
  open import Implicits.Oliveira.Substitutions
  open import Implicits.Oliveira.Improved.Resolution
  open import Extensions.ListFirst

  Bool : Type 0
  Bool = simpl $ tc tc-bool

  Int : ∀ {ν} → Type ν
  Int = simpl $ tc tc-int

module Example₁ where

  K : Ktx 0 1
  K = (Int ⇒ Bool) ∷K nil

  p₁ : ¬ (K ⊢ Int ⇒ Bool ↓ tc tc-int)
  p₁ (i-iabs (r-simp (here (i-iabs _ ()) .List.[])) _)
  p₁ (i-iabs (r-simp (there ._ _ ())) _)

  p₂ : ¬ (K ⊢ Int ⇒ Bool ↓ tc tc-int)
  p₂ (i-iabs x ())

ext: agda


text:
{-# OPTIONS --rewriting #-}
module DualLM where

open import Data.Bool
open import Data.Nat hiding (compare)
open import Data.Nat.Properties
open import Data.Fin hiding (_+_)
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality hiding (Extensionality)
open import Agda.Builtin.Equality.Rewrite
open import Extensionality
open import Direction

-- variables

variable
  n m : ℕ

----------------------------------------------------------------------
-- auxiliaries for automatic rewriting

n+1=suc-n : n + 1 ≡ suc n
n+1=suc-n {zero} = refl
n+1=suc-n {suc n} = cong suc (n+1=suc-n {n})

{-# REWRITE n+1=suc-n #-}

n+0=n : n + 0 ≡ n
n+0=n {zero} = refl
n+0=n {suc n} = cong suc (n+0=n {n})

{-# REWRITE n+0=n #-}

inject+0-x=x : {x : Fin m} → inject+ 0 x ≡ x
inject+0-x=x {x = zero} = refl
inject+0-x=x {x = suc x} = cong suc inject+0-x=x

{-# REWRITE inject+0-x=x #-}

n+sucm : n + suc m ≡ suc (n + m)
n+sucm {0F} = refl
n+sucm {suc n} = cong suc (n+sucm{n})

{-# REWRITE n+sucm #-}

----------------------------------------------------------------------
-- session type inductively with explicit rec

module IND where

  data Polarity : Set where
    POS NEG : Polarity

  mutual
    data Type (n : ℕ) : Set where
      TUnit TInt : Type n
      TPair : (T₁ : Type n) (T₂ : Type n) → Type n
      TChan : (S : SType n) → Type n

    data SType (n : ℕ) : Set where
      gdd : (G : GType n) → SType n
      rec : (G : GType (suc n) ) → SType n
      var : (p : Polarity) → (x : Fin n) → SType n

    data GType (n : ℕ) : Set where
      transmit : (d : Dir) (T : Type n) (S : SType n) → GType n
      choice : (d : Dir) (m : ℕ) (alt : Fin m → SType n) → GType n
      end : GType n

  TType = Type

  -- weakening

  weakenS : (n : ℕ) → SType m → SType (m + n)
  weakenG : (n : ℕ) → GType m → GType (m + n)
  weakenT : (n : ℕ) → TType m → TType (m + n)

  weakenS n (gdd gst) = gdd (weakenG n gst)
  weakenS n (rec gst) = rec (weakenG n gst)
  weakenS n (var p x) = var p (inject+ n x)

  weakenG n (transmit d t s) = transmit d (weakenT n t) (weakenS n s)
  weakenG n (choice d m alt) = choice d m (weakenS n ∘ alt)
  weakenG n end = end

  weakenT n TUnit = TUnit
  weakenT n TInt = TInt
  weakenT n (TPair ty ty₁) = TPair (weakenT n ty) (weakenT n ty₁)
  weakenT n (TChan x) = TChan (weakenS n x)

  weaken1 : SType m → SType (suc m)
  weaken1{m} stm with weakenS 1 stm
  ... | r rewrite n+1=suc-n {m} = r

  module CheckWeaken where
    s0 : SType 0
    s0 = rec (transmit SND TUnit (var POS zero))
    s1 : SType 1
    s1 = rec (transmit SND TUnit (var POS zero))
    s2 : SType 2
    s2 = rec (transmit SND TUnit (var POS zero))

    check-weakenS1 : weakenS 1 s0 ≡ s1
    check-weakenS1 = cong rec (cong (transmit SND TUnit) refl)

    check-weakenS2 : weakenS 2 s0 ≡ s2
    check-weakenS2 = cong rec (cong (transmit SND TUnit) refl)

  weaken1'N : Fin (suc n) → Fin n → Fin (suc n)
  weaken1'N zero x = suc x
  weaken1'N (suc i) zero = zero
  weaken1'N (suc i) (suc x) = suc (weaken1'N i x)

  weaken1'S : Fin (suc n) → SType n → SType (suc n)
  weaken1'G : Fin (suc n) → GType n → GType (suc n)
  weaken1'T : Fin (suc n) → TType n → TType (suc n)

  weaken1'S i (gdd gst) = gdd (weaken1'G i gst)
  weaken1'S i (rec gst) = rec (weaken1'G (suc i) gst)
  weaken1'S i (var p x) = var p (weaken1'N i x)

  weaken1'G i (transmit d t s) = transmit d (weaken1'T i t) (weaken1'S i s)
  weaken1'G i (choice d m alt) = choice d m (weaken1'S i ∘ alt)
  weaken1'G i end = end

  weaken1'T i TUnit = TUnit
  weaken1'T i TInt = TInt
  weaken1'T i (TPair t₁ t₂) = TPair (weaken1'T i t₁) (weaken1'T i t₂)
  weaken1'T i (TChan x) = TChan (weaken1'S i x)

  weaken1S : SType n → SType (suc n)
  weaken1G : GType n → GType (suc n)
  weaken1T : Type n → Type (suc n)

  weaken1S = weaken1'S zero
  weaken1G = weaken1'G zero
  weaken1T = weaken1'T zero

  module CheckWeaken1' where
    sxy : ∀ n → Fin (suc n) → SType n
    sxy n x = rec (transmit SND TUnit (var POS x))

    s00 : SType 0
    s00 = sxy 0 0F
    s10 : SType 1
    s10 = sxy 1 0F
    s11 : SType 1
    s11 = sxy 1 1F
    s22 : SType 2
    s22 = sxy 2 2F

    check-weaken-s01 : weaken1'S 0F s00 ≡ s10
    check-weaken-s01 = refl

    check-weaken-s1-s2 : weaken1'S 0F s11 ≡ s22
    check-weaken-s1-s2 = refl

    check-weaken-s21 : weaken1'S 1F (sxy 2 1F) ≡ sxy 3 1F
    check-weaken-s21 = refl
  ----------------------------------------------------------------------

  dual-pol : Polarity → Polarity
  dual-pol POS = NEG
  dual-pol NEG = POS

  dual-pol-inv : ∀ p → dual-pol (dual-pol p) ≡ p
  dual-pol-inv POS = refl
  dual-pol-inv NEG = refl

  swap-polS : (i : Fin (suc n)) → SType (suc n) → SType (suc n)
  swap-polG : (i : Fin (suc n)) → GType (suc n) → GType (suc n)
  swap-polT : (i : Fin (suc n)) → Type (suc n) → Type (suc n)

  swap-polG i (transmit d t st) = transmit d (swap-polT i t) (swap-polS i st)
  swap-polG i (choice d m alt) = choice d m (swap-polS i ∘ alt)
  swap-polG i end = end

  swap-polS i (gdd gst) = gdd (swap-polG i gst)
  swap-polS i (rec st) = rec (swap-polG (suc i) st)
  swap-polS zero (var p zero) = var (dual-pol p) zero
  swap-polS (suc i) (var p zero) = var p zero
  swap-polS zero (var p (suc x)) = var p (suc x)
  swap-polS {suc n} (suc i) (var p (suc x)) = weaken1S (swap-polS i (var p x))

  swap-polT i TUnit = TUnit
  swap-polT i TInt = TInt
  swap-polT i (TPair t₁ t₂) = TPair (swap-polT i t₁) (swap-polT i t₂)
  swap-polT i (TChan x) = TChan (swap-polS i x)

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

  weak-weakN : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (x : Fin n)
    → weaken1'N (suc i) (weaken1'N j x) ≡ weaken1'N (inject₁ j) (weaken1'N i x)
  weak-weakG : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (g : GType n)
    → weaken1'G (suc i) (weaken1'G j g) ≡ weaken1'G (inject₁ j) (weaken1'G i g)
  weak-weakS : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (s : SType n)
    → weaken1'S (suc i) (weaken1'S j s) ≡ weaken1'S (inject₁ j) (weaken1'S i s)
  weak-weakT : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (t : Type n)
    → weaken1'T (suc i) (weaken1'T j t) ≡ weaken1'T (inject₁ j) (weaken1'T i t)

  weak-weakN 0F 0F le x                              = refl
  weak-weakN (suc i) 0F le x                         = refl
  weak-weakN (suc i) (suc j) (s≤s le) zero           = refl
  weak-weakN{suc n} (suc i) (suc j) (s≤s le) (suc x) = cong suc (weak-weakN i j le x)

  weak-weakG i j le (transmit d t s) = cong₂ (transmit d) (weak-weakT i j le t) (weak-weakS i j le s)
  weak-weakG i j le (choice d m alt) = cong (choice d m) (ext (weak-weakS i j le ∘ alt))
  weak-weakG i j le end              = refl

  weak-weakS i j le (gdd gst) = cong gdd (weak-weakG i j le gst)
  weak-weakS i j le (rec gst) = cong rec (weak-weakG (suc i) (suc j) (s≤s le) gst)
  weak-weakS i j le (var p x) = cong (var p) (weak-weakN i j le x)

  weak-weakT i j le TUnit        = refl
  weak-weakT i j le TInt         = refl
  weak-weakT i j le (TPair t t₁) = cong₂ TPair (weak-weakT i j le t) (weak-weakT i j le t₁)
  weak-weakT i j le (TChan s)    = cong TChan (weak-weakS i j le s)

  weaken1-weakenN : (m : ℕ) (j : Fin (suc n)) (x : Fin n)
    → inject+ m (weaken1'N j x) ≡ weaken1'N (inject+ m j) (inject+ m x)
  weaken1-weakenN m 0F 0F           = refl
  weaken1-weakenN m 0F (suc x)      = refl
  weaken1-weakenN m (suc j) 0F      = refl
  weaken1-weakenN m (suc j) (suc x) = cong suc (weaken1-weakenN m j x)

  weaken1-weakenS : (m : ℕ) (j : Fin (suc n)) (s : SType n)
    → weakenS m (weaken1'S j s) ≡ weaken1'S (inject+ m j) (weakenS m s)
  weaken1-weakenG : (m : ℕ) (j : Fin (suc n)) (g : GType n)
    → weakenG m (weaken1'G j g) ≡ weaken1'G (inject+ m j) (weakenG m g)
  weaken1-weakenT : (m : ℕ) (j : Fin (suc n)) (t : Type n)
    → weakenT m (weaken1'T j t) ≡ weaken1'T (inject+ m j) (weakenT m t)
  weaken1-weakenS m j (gdd gst) = cong gdd (weaken1-weakenG m j gst)
  weaken1-weakenS m j (rec gst) = cong rec (weaken1-weakenG m (suc j) gst)
  weaken1-weakenS m 0F (var p 0F)      = refl
  weaken1-weakenS m 0F (var p (suc x)) = refl
  weaken1-weakenS {suc n} m (suc j) (var p 0F)      = refl
  weaken1-weakenS {suc n} m (suc j) (var p (suc x)) = cong (var p) (cong suc (weaken1-weakenN m j x))

  weaken1-weakenG m j (transmit d t s)  = cong₂ (transmit d) (weaken1-weakenT m j t) (weaken1-weakenS m j s)
  weaken1-weakenG m j (choice d m₁ alt) = cong (choice d m₁) (ext (weaken1-weakenS m j ∘ alt))
  weaken1-weakenG m j end = refl

  weaken1-weakenT m j TUnit = refl
  weaken1-weakenT m j TInt = refl
  weaken1-weakenT m j (TPair t t₁) = cong₂ TPair (weaken1-weakenT m j t) (weaken1-weakenT m j t₁)
  weaken1-weakenT m j (TChan x) = cong TChan (weaken1-weakenS m j x)

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

  -- weakening of later index
  swap-weaken1'G : (i : Fin (suc (suc n))) (j : Fin′ i) (gst : GType (suc n)) →
    swap-polG (inject j) (weaken1'G i gst) ≡ weaken1'G i (swap-polG (inject! j) gst)
  swap-weaken1'S : (i : Fin (suc (suc n))) (j : Fin′ i) (sst : SType (suc n)) →
    swap-polS (inject j) (weaken1'S i sst) ≡ weaken1'S i (swap-polS (inject! j) sst)
  swap-weaken1'T : (i : Fin (suc (suc n))) (j : Fin′ i) (t : Type (suc n)) →
    swap-polT (inject j) (weaken1'T i t) ≡ weaken1'T i (swap-polT (inject! j) t)

  swap-weaken1'G i j (transmit d t s) = cong₂ (transmit d) (swap-weaken1'T i j t) (swap-weaken1'S i j s)
  swap-weaken1'G i j (choice d m alt) = cong (choice d m) (ext (swap-weaken1'S i j ∘ alt))
  swap-weaken1'G i j end = refl

  swap-weaken1'S i j (gdd gst) = cong gdd (swap-weaken1'G i j gst)
  swap-weaken1'S i j (rec gst) = cong rec (swap-weaken1'G (suc i) (suc j) gst)
  swap-weaken1'S zero () (var p x)
  swap-weaken1'S (suc i) zero (var p zero) = refl
  swap-weaken1'S (suc i) zero (var p (suc x)) = refl
  swap-weaken1'S (suc i) (suc j) (var p zero) = refl
  swap-weaken1'S{suc n} (suc i) (suc j) (var p (suc x)) rewrite (weak-weakS i 0F z≤n (swap-polS (inject! j) (var p x))) =
    let sws = swap-weaken1'S{n} i j (var p x) in cong (weaken1'S 0F) sws

  swap-weaken1'T i j TUnit         = refl
  swap-weaken1'T i j TInt          = refl
  swap-weaken1'T i j (TPair t₁ t₂) = cong₂ TPair (swap-weaken1'T i j t₁) (swap-weaken1'T i j t₂)
  swap-weaken1'T i j (TChan s)     = cong TChan (swap-weaken1'S i j s)

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

  -- weakening of earlier index
  swap-weaken1'S< : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) → (s : SType (suc n)) →
    swap-polS (suc i) (weaken1'S (inject₁ j) s) ≡ weaken1'S (inject₁ j) (swap-polS i s)
  swap-weaken1'G< : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) → (g : GType (suc n)) →
    swap-polG (suc i) (weaken1'G (inject₁ j) g) ≡ weaken1'G (inject₁ j) (swap-polG i g)
  swap-weaken1'T< : (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) → (t : Type (suc n)) →
    swap-polT (suc i) (weaken1'T (inject₁ j) t) ≡ weaken1'T (inject₁ j) (swap-polT i t)

  swap-weaken1'S< i j le (gdd gst)       = cong gdd (swap-weaken1'G< i j le gst)
  swap-weaken1'S< i j le (rec gst)       = cong rec (swap-weaken1'G< (suc i) (suc j) (s≤s le) gst)
  swap-weaken1'S< 0F 0F le (var p x)     = refl
  swap-weaken1'S< (suc i) 0F le (var p x) = refl
  swap-weaken1'S<{suc n} (suc i) (suc j) le (var p zero) = refl
  swap-weaken1'S<{suc n} (suc i) (suc j) (s≤s le) (var p (suc x)) rewrite (weak-weakS (inject₁ j) 0F z≤n (swap-polS i (var p x))) =
    let sws = swap-weaken1'S<{n} i j le (var p x) in cong (weaken1'S 0F) sws

  swap-weaken1'G< i j le (transmit d t s) = cong₂ (transmit d) (swap-weaken1'T< i j le t) (swap-weaken1'S< i j le s)
  swap-weaken1'G< i j le (choice d m alt) = cong (choice d m) (ext ((swap-weaken1'S< i j le) ∘ alt))
  swap-weaken1'G< i j le end = refl

  swap-weaken1'T< i j le TUnit = refl
  swap-weaken1'T< i j le TInt = refl
  swap-weaken1'T< i j le (TPair t t₁) = cong₂ (TPair) (swap-weaken1'T< i j le t) (swap-weaken1'T< i j le t₁)
  swap-weaken1'T< i j le (TChan s) = cong (TChan) (swap-weaken1'S< i j le s)

  swap-weakenS : (i : Fin (suc n)) → (s : SType (suc n)) →
    swap-polS (suc i) (weaken1S s) ≡ weaken1S (swap-polS i s)
  swap-weakenG : (i : Fin (suc n)) → (g : GType (suc n)) →
    swap-polG (suc i) (weaken1G g) ≡ weaken1G (swap-polG i g)
  swap-weakenT : (i : Fin (suc n)) → (t : Type (suc n)) →
    swap-polT (suc i) (weaken1T t) ≡ weaken1T (swap-polT i t)

  swap-weakenS i s = swap-weaken1'S< i 0F z≤n s
  swap-weakenG i g = swap-weaken1'G< i 0F z≤n g
  swap-weakenT i t = swap-weaken1'T< i 0F z≤n t

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

  -- swapping of general weakening
  swap-weakenG' : (m : ℕ) (j : Fin (suc n)) (gst : GType (suc n))
    → swap-polG (inject+ m j) (weakenG m gst) ≡ weakenG m (swap-polG j gst)
  swap-weakenS' : (m : ℕ) (j : Fin (suc n)) (s : SType (suc n))
    → swap-polS (inject+ m j) (weakenS m s) ≡ weakenS m (swap-polS j s)
  swap-weakenT' : (m : ℕ) (j : Fin (suc n)) (t : Type (suc n))
    → swap-polT (inject+ m j) (weakenT m t) ≡ weakenT m (swap-polT j t)

  swap-weakenG' m j (transmit d t s) = cong₂ (transmit d) (swap-weakenT' m j t) (swap-weakenS' m j s)
  swap-weakenG' m j (choice d m₁ alt) = cong (choice d m₁) (ext (swap-weakenS' m j ∘ alt))
  swap-weakenG' m j end = refl

  swap-weakenS' m j (gdd gst) = cong gdd (swap-weakenG' m j gst)
  swap-weakenS' m j (rec gst) = cong rec (swap-weakenG' m (suc j) gst)
  swap-weakenS' m 0F (var p 0F)      = refl
  swap-weakenS' m (suc j) (var p 0F) = refl
  swap-weakenS' m 0F (var p 1F)      = refl
  swap-weakenS' m 0F (var p (suc (suc x))) = refl
  swap-weakenS' {suc n} m (suc j) (var p (suc x)) rewrite (weaken1-weakenS m 0F (swap-polS j (var p x))) =
     let rst = swap-weakenS'{n} m j (var p x) in cong weaken1S rst

  swap-weakenT' m j TUnit = refl
  swap-weakenT' m j TInt = refl
  swap-weakenT' m j (TPair t t₁) = cong₂ TPair (swap-weakenT' m j t) (swap-weakenT' m j t₁)
  swap-weakenT' m j (TChan x) = cong TChan (swap-weakenS' m j x)

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

  swap-pol-invS : (i : Fin (suc n)) → (st : SType (suc n)) →
    swap-polS i (swap-polS i st) ≡ st
  swap-pol-invG : (i : Fin (suc n)) → (st : GType (suc n)) →
    swap-polG i (swap-polG i st) ≡ st
  swap-pol-invT : (i : Fin (suc n)) → (ty : Type (suc n)) →
    swap-polT i (swap-polT i ty) ≡ ty

  swap-pol-invS i (gdd gst) = cong gdd (swap-pol-invG i gst)
  swap-pol-invS i (rec gst) = cong rec (swap-pol-invG (suc i) gst)
  swap-pol-invS zero (var p zero) rewrite dual-pol-inv p = refl
  swap-pol-invS (suc i) (var p zero) = refl
  swap-pol-invS zero (var p (suc x)) rewrite dual-pol-inv p = refl
  swap-pol-invS {suc n} (suc i) (var p (suc x))
    rewrite swap-weakenS i (swap-polS i (var p x)) | swap-pol-invS i (var p x) = refl

  -- extensionality needed
  swap-pol-invG i (transmit d t s) = cong₂ (transmit d) (swap-pol-invT i t) (swap-pol-invS i s)
  swap-pol-invG i (choice d m alt) = cong (choice d m) (ext R)
    where R : ∀ x → swap-polS i (swap-polS i (alt x)) ≡ alt x
          R x rewrite swap-pol-invS i (alt x) = refl
  swap-pol-invG i end = refl

  swap-pol-invT i TUnit = refl
  swap-pol-invT i TInt = refl
  swap-pol-invT i (TPair ty ty₁) = cong₂ TPair (swap-pol-invT i ty) (swap-pol-invT i ty₁)
  swap-pol-invT i (TChan x) = cong TChan (swap-pol-invS i x)

  dualS : SType n → SType n
  dualG : GType n → GType n

  dualG (transmit d t st) = transmit (dual-dir d) t (dualS st)
  dualG (choice d m alt) = choice (dual-dir d) m (dualS ∘ alt)
  dualG end = end

  dualS (gdd gst) = gdd (dualG gst)
  dualS (rec gst) = rec (swap-polG zero (dualG gst))
  dualS (var p x) = var (dual-pol p) x

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

  dual-weakenS : (i : Fin (suc n)) (s : SType n) → dualS (weaken1'S i s) ≡ weaken1'S i (dualS s)
  dual-weakenG : (i : Fin (suc n)) (g : GType n) → dualG (weaken1'G i g) ≡ weaken1'G i (dualG g)

  dual-weakenS i (gdd gst) = cong gdd (dual-weakenG i gst)
  dual-weakenS i (rec gst) rewrite (sym (swap-weaken1'G (suc i) 0F (dualG gst))) = cong rec (cong (swap-polG 0F) (dual-weakenG (suc i) gst))
  dual-weakenS i (var p x) = refl

  dual-weakenG i (transmit d t s) = cong₂ (transmit (dual-dir d)) refl (dual-weakenS i s)
  dual-weakenG i (choice d m alt) = cong (choice (dual-dir d) m) (ext (dual-weakenS i ∘ alt))
  dual-weakenG i end = refl

  dual-weakenS' : (m : ℕ) (s : SType n) → dualS (weakenS m s) ≡ weakenS m (dualS s)
  dual-weakenG' : (m : ℕ) (g : GType n) → dualG (weakenG m g) ≡ weakenG m (dualG g)

  dual-weakenS' n (gdd gst) = cong gdd (dual-weakenG' n gst)
  dual-weakenS' n (rec gst) rewrite (sym (swap-weakenG' n 0F (dualG gst))) = cong rec (cong (swap-polG 0F) (dual-weakenG' n gst))
  dual-weakenS' n (var p x) = refl

  dual-weakenG' n (transmit d t s) = cong₂ (transmit (dual-dir d)) refl (dual-weakenS' n s)
  dual-weakenG' n (choice d m alt) = cong (choice (dual-dir d) m) (ext (dual-weakenS' n ∘ alt))
  dual-weakenG' n end = refl

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

  aux : (i : Fin n) (x : Fin n) (p' : Polarity) →
    var p' (suc (suc x)) ≡ weaken1S (var p' (suc x))
  aux i x p = refl

  var-suc : (i : Fin n) (x : Fin n) (p : Polarity) →
    ∃ λ p' → swap-polS (suc i) (var p (suc x)) ≡ var p' (suc x)
  var-suc zero zero p = dual-pol p , refl
  var-suc (suc i) zero p = p , refl
  var-suc zero (suc x) p = p , refl
  var-suc (suc i) (suc x) p
    with var-suc i x p
  ... | p' , snd
    rewrite sym (aux i x p') = p' , cong weaken1S snd

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

  swap-swapG : (gst : GType (suc n)) → (i : Fin (suc n)) (j : Fin′ i) →
    swap-polG i (swap-polG (inject j) gst) ≡ swap-polG (inject j) (swap-polG i gst)
  swap-swapT : (t : Type (suc n)) → (i : Fin (suc n)) (j : Fin′ i) →
    swap-polT i (swap-polT (inject j) t) ≡ swap-polT (inject j) (swap-polT i t)
  swap-swapS : (st : SType (suc n)) → (i : Fin (suc n)) (j : Fin′ i) →
    swap-polS i (swap-polS (inject j) st) ≡ swap-polS (inject j) (swap-polS i st)

  swap-swapG (transmit d t s) i j = cong₂ (transmit d) (swap-swapT t i j) (swap-swapS s i j)
  swap-swapG (choice d m alt) i j = cong (choice d m) (ext (λ x → swap-swapS (alt x) i j))
  swap-swapG end i j = refl

  swap-swapT TUnit i j = refl
  swap-swapT TInt i j = refl
  swap-swapT (TPair t t₁) i j = cong₂ TPair (swap-swapT t i j) (swap-swapT t₁ i j)
  swap-swapT (TChan x) i j = cong TChan (swap-swapS x i j)

  swap-swapS (gdd gst) i j = cong gdd (swap-swapG gst i j)
  swap-swapS (rec gst) i j = cong rec (swap-swapG gst (suc i) (suc j))
  swap-swapS (var p zero) zero ()
  swap-swapS (var p zero) (suc i) zero = refl
  swap-swapS (var p zero) (suc i) (suc j) = refl
  swap-swapS (var p (suc x)) zero ()
  swap-swapS (var p (suc x)) (suc i) zero
    with var-suc i x p
  ... | p' , snd rewrite snd = refl
  swap-swapS {suc n} (var p (suc x)) (suc i) (suc j)
    rewrite swap-weakenS i (swap-polS (inject j) (var p x))
    with swap-swapS (var p x) i j
  ... | pxij rewrite swap-weakenS (inject j) (swap-polS i (var p x))
    = cong weaken1S pxij

  swap-pol-dualG : (i : Fin (suc n)) (gst : GType (suc n)) →
    swap-polG i (dualG gst) ≡ dualG (swap-polG i gst)
  swap-pol-dualS : (i : Fin (suc n)) (st : SType (suc n)) →
    swap-polS i (dualS st) ≡ dualS (swap-polS i st)

  swap-pol-dualG i (transmit d t s) = cong (transmit _ (swap-polT i t)) (swap-pol-dualS i s)
  swap-pol-dualG i (choice d m alt) = cong (choice _ _) (ext (swap-pol-dualS i ∘ alt))
  swap-pol-dualG i end = refl

  swap-pol-dualS i (gdd gst) = cong gdd (swap-pol-dualG i gst)
  swap-pol-dualS i (rec gst) rewrite sym (swap-pol-dualG (suc i) gst) =
    cong rec (swap-swapG (dualG gst) (suc i) zero)
  swap-pol-dualS zero (var p zero) = refl
  swap-pol-dualS (suc i) (var p zero) = refl
  swap-pol-dualS zero (var p (suc x)) = refl
  swap-pol-dualS {suc n} (suc i) (var p (suc x))
     rewrite (dual-weakenS 0F (swap-polS i (var p x))) =  cong weaken1S (swap-pol-dualS i (var p x))

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

  dual-invS : (st : SType n) → st ≡ dualS (dualS st)
  dual-invG : (gst : GType n) → gst ≡ dualG (dualG gst)

  dual-invS (gdd gst) = cong gdd (dual-invG gst)
  dual-invS (rec gst) rewrite sym (swap-pol-dualG zero (dualG gst)) | swap-pol-invG zero (dualG (dualG gst)) = cong rec (dual-invG gst)
  dual-invS (var p x) rewrite dual-pol-inv p = refl

  dual-invG (transmit d t s) rewrite dual-dir-inv d = cong₂ (transmit d) refl (dual-invS s)
  dual-invG (choice d m alt) rewrite dual-dir-inv d = cong (choice d m) (ext R)
    where R : (x : Fin m) → alt x ≡ dualS (dualS (alt x))
          R x rewrite sym (dual-invS (alt x)) = refl
  dual-invG end = refl

  dual-if : Polarity → SType n → SType n
  dual-if POS s = s
  dual-if NEG s = dualS s

  dual-if-dual : (p : Polarity) (ist : SType 0) → dual-if p ist ≡ dual-if (dual-pol p) (dualS ist)
  dual-if-dual POS ist = (dual-invS ist)
  dual-if-dual NEG ist = refl

  ----------------------------------------------------------------------
  -- substitution

  st-substS : SType (suc n) → Fin (suc n) → SType 0 → SType n
  st-substG : GType (suc n) → Fin (suc n) → SType 0 → GType n
  st-substT : Type (suc n) → Fin (suc n) → SType 0 → Type n

  st-substS (gdd gst) i st0 = gdd (st-substG gst i st0)
  st-substS (rec gst) i st0 = rec (st-substG gst (suc i) st0)
  st-substS {n} (var p zero) zero st0 = weakenS n (dual-if p st0)
  st-substS {suc n} (var p zero) (suc i) st0 = var p zero
  st-substS {suc n} (var p (suc x)) zero st0 = var p x
  st-substS {suc n} (var p (suc x)) (suc i) st0 = weaken1S (st-substS (var p x) i st0)

  st-substG (transmit d t s) i st0 = transmit d (st-substT t i st0) (st-substS s i st0)
  st-substG (choice d m alt) i st0 = choice d m (λ j → st-substS (alt j) i st0)
  st-substG end i st0 = end

  st-substT TUnit i st0 = TUnit
  st-substT TInt i st0 = TInt
  st-substT (TPair ty ty₁) i st0 = TPair (st-substT ty i st0) (st-substT ty₁ i st0)
  st-substT (TChan st) i st0 = TChan (st-substS st i st0)

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

  trivial-subst-var : (p : Polarity) (x : Fin n) (ist₁ ist₂ : SType 0)
    → st-substS (var p (suc x)) 0F ist₁ ≡ st-substS (var p (suc x)) 0F ist₂
  trivial-subst-var p 0F ist1 ist2 = refl
  trivial-subst-var p (suc x) ist1 ist2 = refl

  trivial-subst-var' : (p : Polarity) (i : Fin n) (ist₁ ist₂ : SType 0)
    → st-substS (var p 0F) (suc i) ist₁ ≡ st-substS (var p 0F) (suc i) ist₂
  trivial-subst-var' p 0F ist1 ist2 = refl
  trivial-subst-var' p (suc x) ist1 ist2 = refl

  ----------------------------------------------------------------------
  -- equivalence
  variable
    t t₁ t₂ t₁' t₂' : Type n
    s s₁ s₂ : SType n
    g g₁ g₂ : GType n

  unfold : SType 0 → GType 0
  unfold (gdd gst) = gst
  unfold (rec gst) = st-substG gst 0F (rec gst)

  -- type equivalence
  data EquivT (R : SType n → SType n → Set) : Type n → Type n → Set where
    eq-unit : EquivT R TUnit TUnit
    eq-int  : EquivT R TInt TInt
    eq-pair : EquivT R t₁ t₁' → EquivT R t₂ t₂' → EquivT R (TPair t₁ t₂) (TPair t₁' t₂')
    eq-chan : R s₁ s₂ → EquivT R (TChan s₁) (TChan s₂)

  -- session type equivalence
  data EquivG (R : SType n → SType n → Set) : GType n → GType n → Set where
    eq-transmit : (d : Dir) → EquivT R t₁ t₂ → R s₁ s₂ → EquivG R (transmit d t₁ s₁) (transmit d t₂ s₂)
    eq-choice : ∀ {alt alt'} → (d : Dir) → ((i : Fin m) → R (alt i) (alt' i)) → EquivG R (choice d m alt) (choice d m alt')
    eq-end : EquivG R end end

  record Equiv (s₁ s₂ : SType 0) : Set where
    coinductive
    field force : EquivG Equiv (unfold s₁) (unfold s₂)

  open Equiv

  _≈_ = Equiv
  _≈'_ = EquivG Equiv
  _≈ᵗ_ = EquivT Equiv

  -- reflexive

  ≈-refl : s ≈ s
  ≈'-refl : g ≈' g
  ≈ᵗ-refl : t ≈ᵗ t

  force (≈-refl {s}) = ≈'-refl

  ≈'-refl {transmit d t s} = eq-transmit d ≈ᵗ-refl ≈-refl
  ≈'-refl {choice d m alt} = eq-choice d (λ i → ≈-refl)
  ≈'-refl {end} = eq-end

  ≈ᵗ-refl {TUnit} = eq-unit
  ≈ᵗ-refl {TInt} = eq-int
  ≈ᵗ-refl {TPair t t₁} = eq-pair ≈ᵗ-refl ≈ᵗ-refl
  ≈ᵗ-refl {TChan x} = eq-chan ≈-refl

  -- symmetric

  ≈-symm : s₁ ≈ s₂ → s₂ ≈ s₁
  ≈'-symm : g₁ ≈' g₂ → g₂ ≈' g₁
  ≈ᵗ-symm : t₁ ≈ᵗ t₂ → t₂ ≈ᵗ t₁

  force (≈-symm s₁≈s₂) = ≈'-symm (force s₁≈s₂)

  ≈'-symm (eq-transmit d x x₁) = eq-transmit d (≈ᵗ-symm x) (≈-symm x₁)
  ≈'-symm (eq-choice d x) = eq-choice d (≈-symm ∘ x)
  ≈'-symm eq-end = eq-end

  ≈ᵗ-symm eq-unit = eq-unit
  ≈ᵗ-symm eq-int = eq-int
  ≈ᵗ-symm (eq-pair t₁≈ᵗt₂ t₁≈ᵗt₃) = eq-pair (≈ᵗ-symm t₁≈ᵗt₂) (≈ᵗ-symm t₁≈ᵗt₃)
  ≈ᵗ-symm (eq-chan x) = eq-chan (≈-symm x)

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

-- Proof of equivalence to coinductive definition
open import DualCoinductive hiding (n)
open COI
open IND hiding (_≈_ ; _≈'_ ; ≈-refl ; ≈'-refl ; ≈ᵗ-refl)

ind2coiT : IND.Type 0 → COI.Type
ind2coiS : IND.SType 0 → COI.SType
ind2coiG : IND.GType 0 → COI.STypeF COI.SType

ind2coiT TUnit = TUnit
ind2coiT TInt = TInt
ind2coiT (TPair it it₁) = TPair (ind2coiT it) (ind2coiT it₁)
ind2coiT (TChan st) = TChan (ind2coiS st)

ind2coiG (transmit d t ist) = transmit d (ind2coiT t) (ind2coiS ist)
ind2coiG (choice d m alt) = choice d m (ind2coiS ∘ alt)
ind2coiG end = end

SType.force (ind2coiS (gdd gst)) = ind2coiG gst
SType.force (ind2coiS (rec gst)) = ind2coiG (st-substG gst zero (rec gst))

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

subst-weakenS : (s : IND.SType (suc n)) (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (s0 : IND.SType 0)
  → st-substS (weaken1'S (inject₁ j) s) (suc i) s0 ≡ weaken1'S j (st-substS s i s0)
subst-weakenG : (g : IND.GType (suc n)) (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (s0 : IND.SType 0)
  → st-substG (weaken1'G (inject₁ j) g) (suc i) s0 ≡ weaken1'G j (st-substG g i s0)
subst-weakenT : (t : IND.Type (suc n)) (i : Fin (suc n)) (j : Fin (suc n)) (le : Data.Fin._≤_ j i) (s0 : IND.SType 0)
  → st-substT (weaken1'T (inject₁ j) t) (suc i) s0 ≡ weaken1'T j (st-substT t i s0)

subst-weakenS (gdd gst) i j le s0 = cong gdd (subst-weakenG gst i j le s0)
subst-weakenS (rec gst) i j le s0 = cong rec (subst-weakenG gst (suc i) (suc j) (s≤s le) s0)
subst-weakenS (var p x) 0F 0F le s0 = refl
subst-weakenS {suc n} (var p x) (suc i) 0F le s0 = refl
subst-weakenS {suc n} (var p 0F) (suc i) (suc j) le s0 = refl
subst-weakenS {suc n} (var p (suc x)) (suc i) (suc j) (s≤s le) s0 rewrite (weak-weakS j 0F z≤n (st-substS (var p x) i s0))
  = cong (weaken1'S 0F) (subst-weakenS (var p x) i j le s0)

subst-weakenG (transmit d t s) i j le s0 = cong₂ (transmit d) (subst-weakenT t i j le s0) (subst-weakenS s i j le s0)
subst-weakenG (choice d m alt) i j le s0 = cong (choice d m) (ext (λ m' → subst-weakenS (alt m') i j le s0 ))
subst-weakenG end i j le s0 = refl

subst-weakenT TUnit i j le s0 = refl
subst-weakenT TInt i j le s0 = refl
subst-weakenT (TPair t t₁) i j le s0 = cong₂ TPair (subst-weakenT t i j le s0) (subst-weakenT t₁ i j le s0)
subst-weakenT (TChan s) i j le s0 = cong TChan (subst-weakenS s i j le s0)

subst-swap-dualT : ∀ {ist} → (t : IND.Type (suc n)) (i : Fin (suc n)) →
  st-substT t i ist ≡ st-substT (swap-polT i t) i (IND.dualS ist)
subst-swap-dualS : ∀ {ist} → (st : IND.SType (suc n)) (i : Fin (suc n)) →
  st-substS st i ist ≡ st-substS (swap-polS i st) i (IND.dualS ist)
subst-swap-dualG : ∀ {ist} → (gst : IND.GType (suc n)) (i : Fin (suc n)) →
  st-substG gst i ist ≡ st-substG (swap-polG i gst) i (IND.dualS ist)

subst-swap-dualT TUnit i = refl
subst-swap-dualT TInt i = refl
subst-swap-dualT (TPair ty ty₁) i = cong₂ TPair (subst-swap-dualT ty i) (subst-swap-dualT ty₁ i)
subst-swap-dualT (TChan x) i = cong TChan (subst-swap-dualS x i)

subst-swap-dualS (gdd gst) i = cong gdd (subst-swap-dualG gst i)
subst-swap-dualS (rec gst) i = cong rec (subst-swap-dualG gst (suc i))
subst-swap-dualS {n} {ist} (var p zero) zero = cong (weakenS n) (dual-if-dual p ist)
subst-swap-dualS {suc n} (var p zero) (suc i) = refl
subst-swap-dualS {suc n} (var p (suc x)) zero = refl
subst-swap-dualS {suc n}{ist} (var p (suc x)) (suc i)
  rewrite subst-weakenS (swap-polS i (var p x)) i 0F z≤n (dualS ist)
  = cong (weaken1'S 0F) (subst-swap-dualS ((var p x)) i)

subst-swap-dualG (transmit d t s) i = cong₂ (transmit d) (subst-swap-dualT t i) (subst-swap-dualS s i)
subst-swap-dualG (choice d m alt) i = cong (choice d m) (ext (λ x → subst-swap-dualS (alt x) i))
subst-swap-dualG end i = refl

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

swap-i-weakenS : (i : Fin (suc n)) (s : IND.SType n) → swap-polS i (weaken1'S i s) ≡ weaken1'S i s
swap-i-weakenG : (i : Fin (suc n)) (g : IND.GType n) → swap-polG i (weaken1'G i g) ≡ weaken1'G i g
swap-i-weakenT : (i : Fin (suc n)) (t : IND.TType n) → swap-polT i (weaken1'T i t) ≡ weaken1'T i t

swap-i-weakenS i (gdd gst) = cong gdd (swap-i-weakenG i gst)
swap-i-weakenS i (rec gst) = cong rec (swap-i-weakenG (suc i) gst)
swap-i-weakenS zero (var p zero) = refl
swap-i-weakenS (suc i) (var p zero) = refl
swap-i-weakenS zero (var p (suc x)) = refl
swap-i-weakenS (suc i) (var p (suc x)) = cong weaken1S (swap-i-weakenS i (var p x))

swap-i-weakenG i (transmit d t s) = cong₂ (transmit d) (swap-i-weakenT i t) (swap-i-weakenS i s)
swap-i-weakenG i (choice d m alt) = cong (choice d m) (ext (swap-i-weakenS i ∘ alt))
swap-i-weakenG i end = refl

swap-i-weakenT i TUnit = refl
swap-i-weakenT i TInt = refl
swap-i-weakenT i (TPair t₁ t₂) = cong₂ TPair (swap-i-weakenT i t₁) (swap-i-weakenT i t₂)
swap-i-weakenT i (TChan x) = cong TChan (swap-i-weakenS i x)

subst-swapG : (ist : IND.SType 0) (i : Fin (suc (suc n))) (j : Fin′ i) (g : GType (suc (suc n))) →
  st-substG (swap-polG (inject j) g) i ist ≡ swap-polG (inject! j) (st-substG g i ist)
subst-swapS : (ist : IND.SType 0) (i : Fin (suc (suc n))) (j : Fin′ i) (s : IND.SType (suc (suc n))) →
  st-substS (swap-polS (inject j) s) i ist ≡ swap-polS (inject! j) (st-substS s i ist)
subst-swapT : (ist : IND.SType 0) (i : Fin (suc (suc n))) (j : Fin′ i) (g : IND.Type (suc (suc n))) →
  st-substT (swap-polT (inject j) g) i ist ≡ swap-polT (inject! j) (st-substT g i ist)

subst-swapG ist i j (transmit d t s) = cong₂ (transmit d) (subst-swapT ist i j t) (subst-swapS ist i j s)
subst-swapG ist i j (choice d m alt) = cong (choice d m) (ext (λ x → subst-swapS ist i j (alt x)))
subst-swapG ist i j end = refl

subst-swapS ist i j (gdd gst) = cong gdd (subst-swapG ist i j gst)
subst-swapS ist i j (rec gst) = cong rec (subst-swapG ist (suc i) (suc j) gst)
subst-swapS{zero} ist zero () (var p zero)
subst-swapS {zero} ist (suc zero) zero (var p zero) = refl
subst-swapS {zero} ist (suc zero) zero (var p (suc x))
  rewrite swap-i-weakenS zero (st-substS (var p x) zero ist) = refl
subst-swapS{suc n} ist (suc i) zero (var p zero) = refl
subst-swapS{suc n} ist (suc i) (suc j) (var p zero) = refl
subst-swapS{suc n} ist zero () (var p (suc x))
subst-swapS{suc n} ist (suc i) zero (var p (suc x))
  rewrite swap-i-weakenS zero (st-substS (var p x) i ist) = refl
subst-swapS{suc n} ist (suc i) (suc j) (var p (suc x))
  rewrite subst-weakenS (swap-polS (inject j) (var p x)) i 0F z≤n ist
  | swap-weakenS (inject! j) (st-substS (var p x) i ist)
  = cong weaken1S (subst-swapS ist i j (var p x))

subst-swapT ist i j TUnit = refl
subst-swapT ist i j TInt = refl
subst-swapT ist i j (TPair t t₁) = cong₂ TPair (subst-swapT ist i j t) (subst-swapT ist i j t₁)
subst-swapT ist i j (TChan x) = cong TChan (subst-swapS ist i j x)

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

dual-recT' : (t : TType (suc n)) (i : Fin (suc n)) (ist : IND.SType 0)
  → st-substT (swap-polT i t) i (dualS ist) ≡ st-substT t i ist
dual-recG' : (g : GType (suc n)) (i : Fin (suc n)) (ist : IND.SType 0)
  → st-substG (swap-polG i g) i (dualS ist) ≡ st-substG g i ist
dual-recS' : (s : IND.SType (suc n)) (i : Fin (suc n)) (ist : IND.SType 0)
  → st-substS (swap-polS i s) i (dualS ist) ≡ st-substS s i ist

dual-recT' TUnit i ist = refl
dual-recT' TInt i ist = refl
dual-recT' (TPair t t₁) i ist = cong₂ TPair (dual-recT' t i ist) (dual-recT' t₁ i ist)
dual-recT' (TChan s) i ist = cong TChan (dual-recS' s i ist)

dual-recG' (transmit d t s) i ist = cong₂ (transmit d) (dual-recT' t i ist) (dual-recS' s i ist)
dual-recG' (choice d m alt) i ist = cong (choice d m) (ext (λ m' → dual-recS' (alt m') i ist))
dual-recG' end i ist = refl

dual-recS' (gdd gst) i ist = cong gdd (dual-recG' gst i ist)
dual-recS' (rec gst) i ist = cong rec (dual-recG' gst (suc i) ist)
dual-recS' (var p 0F) 0F ist rewrite (dual-if-dual p ist) = refl
dual-recS' (var p (suc x)) 0F ist = trivial-subst-var p x (dualS ist) (ist)
dual-recS' (var p 0F) (suc i) ist = trivial-subst-var' p i (dualS ist) (ist)
dual-recS' (var p (suc x)) (suc i) ist rewrite (subst-swap-dualS{ist = ist} (var p (suc x)) (suc i))
  = refl

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

-- show that the dualS function is compatible with unfolding
-- that is
-- COI.dual ∘ ind2coi ≈ ind2coi ∘ IND.dual

dual-lemmaS : (s : IND.SType (suc n)) (j : Fin (suc n)) (s0 : IND.SType 0)
  → st-substS (dualS s) j s0 ≡ dualS (st-substS s j s0)
dual-lemmaG : (g : IND.GType (suc n)) (j : Fin (suc n)) (s0 : IND.SType 0)
  → st-substG (dualG g) j s0 ≡ dualG (st-substG g j s0)

dual-lemmaS (gdd gst) j s0 = cong gdd (dual-lemmaG gst j s0)
dual-lemmaS (rec gst) j s0 rewrite (subst-swapG s0 (suc j) 0F (dualG gst)) =
  let rst = dual-lemmaG gst (suc j) s0 in cong rec (cong (swap-polG 0F) rst)
dual-lemmaS {n} (var POS 0F) 0F s0          = sym (dual-weakenS' n s0)
dual-lemmaS {n} (var NEG 0F) 0F s0 rewrite (sym (dual-weakenS' n s0)) | (sym (dual-invS (weakenS n s0))) = refl
dual-lemmaS {suc n} (var POS 0F) (suc j) s0 = refl
dual-lemmaS {suc n} (var NEG 0F) (suc j) s0 = refl
dual-lemmaS {suc n} (var POS (suc x)) 0F s0 = refl
dual-lemmaS {suc n} (var NEG (suc x)) 0F s0 = refl
dual-lemmaS {suc n} (var POS (suc x)) (suc j) s0 rewrite (dual-weakenS 0F (st-substS (var POS x) j s0)) = cong (weaken1'S 0F) (dual-lemmaS (var POS x) j s0)
dual-lemmaS {suc n} (var NEG (suc x)) (suc j) s0 rewrite (dual-weakenS 0F (st-substS (var NEG x) j s0)) = cong (weaken1'S 0F) (dual-lemmaS (var NEG x) j s0)

dual-lemmaG (transmit d t s) j s0 = cong₂ (transmit (dual-dir d)) refl (dual-lemmaS s j s0)
dual-lemmaG (choice d m alt) j s0 = cong (choice (dual-dir d) m) (ext (λ m' → dual-lemmaS (alt m') j s0))
dual-lemmaG end j s0 = refl

dual-compatibleS : (ist : IND.SType 0) →
  COI.dual (ind2coiS ist) ≈ ind2coiS (IND.dualS ist)
dual-compatibleG : (gst : IND.GType 0) →
  COI.dualF (ind2coiG gst) ≈' ind2coiG (IND.dualG gst)

Equiv.force (dual-compatibleS (gdd gst)) = dual-compatibleG gst
Equiv.force (dual-compatibleS (rec gst))
  rewrite (dual-recG' (dualG gst) 0F (rec gst))  | dual-lemmaG gst 0F (rec gst) = dual-compatibleG (st-substG gst zero (rec gst))

dual-compatibleG (transmit d t s) = eq-transmit (dual-dir d) ≈ᵗ-refl (dual-compatibleS s)
dual-compatibleG (choice d m alt) = eq-choice (dual-dir d) (dual-compatibleS ∘ alt)
dual-compatibleG end = eq-end

max_stars_repo_name: kcaliban/dual-session

max_issues_repo_name: kcaliban/dual-session

max_forks_repo_name: kcaliban/dual-session


text:
------------------------------------------------------------------------------
-- Axiomatic PA properties
------------------------------------------------------------------------------

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

module PA.Axiomatic.Standard.PropertiesI where

open import Common.FOL.Relation.Binary.EqReasoning

open import PA.Axiomatic.Standard.Base

------------------------------------------------------------------------------
-- Congruence properties

succCong : ∀ {m n} → m ≡ n → succ m ≡ succ n
succCong refl = refl

+-leftCong : ∀ {m n o} → m ≡ n → m + o ≡ n + o
+-leftCong refl = refl

+-rightCong : ∀ {m n o} → n ≡ o → m + n ≡ m + o
+-rightCong refl = refl

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

+-leftIdentity : ∀ n → zero + n ≡ n
+-leftIdentity = PA₃

+-rightIdentity : ∀ n → n + zero ≡ n
+-rightIdentity = ℕ-ind A A0 is
  where
  A : ℕ → Set
  A i = i + zero ≡ i

  A0 : A zero
  A0 = +-leftIdentity zero

  is : ∀ i → A i → A (succ i)
  is i ih = succ i + zero   ≡⟨ PA₄ i zero ⟩
            succ (i + zero) ≡⟨ succCong ih ⟩
            succ i          ∎

+-asocc : ∀ m n o → m + n + o ≡ m + (n + o)
+-asocc m n o = ℕ-ind A A0 is m
  where
  A : ℕ → Set
  A i = i + n + o ≡ i + (n + o)

  A0 : A zero
  A0 = zero + n + o   ≡⟨ +-leftCong (+-leftIdentity n) ⟩
       n + o          ≡⟨ sym (+-leftIdentity (n + o)) ⟩
       zero + (n + o) ∎

  is : ∀ i → A i → A (succ i)
  is i ih = succ i + n + o     ≡⟨ +-leftCong (PA₄ i n) ⟩
            succ (i + n) + o   ≡⟨ PA₄ (i + n) o ⟩
            succ (i + n + o)   ≡⟨ succCong ih ⟩
            succ (i + (n + o)) ≡⟨ sym (PA₄ i (n + o)) ⟩
            succ i + (n + o)   ∎

x+Sy≡S[x+y] : ∀ m n → m + succ n ≡ succ (m + n)
x+Sy≡S[x+y] m n = ℕ-ind A A0 is m
  where
  A : ℕ → Set
  A i = i + succ n ≡ succ (i + n)

  A0 : A zero
  A0 = zero + succ n   ≡⟨ +-leftIdentity (succ n) ⟩
       succ n          ≡⟨ succCong (sym (+-leftIdentity n)) ⟩
       succ (zero + n) ∎

  is : ∀ i → A i → A (succ i)
  is i ih = succ i + succ n     ≡⟨ PA₄ i (succ n) ⟩
            succ (i + succ n)   ≡⟨ succCong ih ⟩
            succ (succ (i + n)) ≡⟨ succCong (sym (PA₄ i n)) ⟩
            succ (succ i + n)   ∎

+-comm : ∀ m n → m + n ≡ n + m
+-comm m n = ℕ-ind A A0 is m
  where
  A : ℕ → Set
  A i = i + n ≡ n + i

  A0 : A zero
  A0 = zero + n ≡⟨ +-leftIdentity n ⟩
       n        ≡⟨ sym (+-rightIdentity n) ⟩
       n + zero ∎

  is : ∀ i → A i → A (succ i)
  is i ih = succ i + n   ≡⟨ PA₄ i n ⟩
            succ (i + n) ≡⟨ succCong ih ⟩
            succ (n + i) ≡⟨ sym (x+Sy≡S[x+y] n i) ⟩
            n + succ i   ∎

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import HoTT
open import cohomology.Exactness

module cohomology.ExactPairIso where

{- An exact sequence 0 → G → H → 0 implies that G == H -}

module _ {i} {G H K L : Group i} {φ : H →ᴳ K}
  (ex : is-exact-seq (G ⟨ cst-hom ⟩→ H ⟨ φ ⟩→ K ⟨ cst-hom ⟩→ L ⊣|)) where

  private
    inj : (h₁ h₂ : Group.El H) → GroupHom.f φ h₁ == GroupHom.f φ h₂ → h₁ == h₂
    inj = zero-kernel-injective φ
      (λ h p → Trunc-rec (Group.El-level H _ _) (λ s → ! (snd s))
                 (ktoi (exact-get ex 0) h p))

  exact-pair-iso : H == K
  exact-pair-iso = surj-inj-= φ inj (λ k → ktoi (exact-get ex 1) k idp)

module _ {i} {G H K J : Group i} {φ : G →ᴳ H} {ψ : H →ᴳ K}
  {χ : K →ᴳ J} (p : G == 0ᴳ) (q : J == 0ᴳ)
  (ex : is-exact-seq (G ⟨ φ ⟩→ H ⟨ ψ ⟩→ K ⟨ χ ⟩→ J ⊣|)) where

  private
    ex₁ : is-exact-seq (0ᴳ ⟨ cst-hom ⟩→ H ⟨ ψ ⟩→ K ⟨ χ ⟩→ J ⊣|)
    ex₁ = transport
      (λ {(G' , φ') → is-exact-seq (G' ⟨ φ' ⟩→ H ⟨ ψ ⟩→ K ⟨ χ ⟩→ J ⊣|)})
      (pair= p (prop-has-all-paths-↓ {B = λ L → L →ᴳ H}
                 (raise-level -2 0ᴳ-hom-out-level)))
      ex

    ex₂ : is-exact-seq (0ᴳ ⟨ cst-hom ⟩→ H ⟨ ψ ⟩→ K ⟨ cst-hom ⟩→ 0ᴳ ⊣|)
    ex₂ = transport
      (λ {(J' , χ') → is-exact-seq (0ᴳ ⟨ cst-hom ⟩→ H ⟨ ψ ⟩→ K ⟨ χ' ⟩→ J' ⊣|)})
      (pair= q (prop-has-all-paths-↓ {B = λ L → K →ᴳ L}
                 (raise-level _ 0ᴳ-hom-in-level)))
      ex₁

  exact-pair-path-iso : H == K
  exact-pair-path-iso = exact-pair-iso ex₂

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
{-# OPTIONS --copatterns --sized-types #-}

{- | The purpose of this module is to demonstrate how observational type theory
  can be implemented for arbitrary types in Agda through the use of tests
  and a corresponding bisimulation proof method.

  To use the equivalence for a type A, the type has to be made _testable_ by
  creating an instance of Testable for it, see the accompanying module
  TestsInstances. Such an instance effectively encodes A as inductive or
  coinductive type, by giving an observation map to a coproduct of product
  of components of A. For now, we do not pose any restrictions on this encoding,
  hence it can be used to induce trivial equivalences.

  Using such an instance of Testable for A, we can define _tests_ and
  _observational equivalence_ for A. Moreover, we give a bisimulation proof
  method and prove its soundness.
-}
module Tests where

open import Size
open import Level
open import Data.Product
open import Data.Bool
open import Function
open import Relation.Binary.PropositionalEquality as P
open ≡-Reasoning
open import Relation.Binary

open import Isomorphisms

-- | Write dependent functions as Π-type to make duality between
-- inductive and coinducitve types clearer.
record Π {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  field
    app : (x : A) → B x
open Π public

-- | Generalised copairing for coproducts:
-- Turn an I-indexed tuple of maps fᵢ : Bᵢ → C into a map Σ I B → C.
cotuple : {I C : Set} → {B : I → Set} → ((i : I) → B i → C) → (Σ I B → C)
cotuple f x = f (proj₁ x) (proj₂ x)

-- | Distinguish inductive and coinductive types
data Kind : Set where
  ind   : Kind
  coind : Kind

--- | Make a type observable. An inductive type shall be represented by
---   a coproduct, whereas a coinductive type is represented by a product.
ObsTy : (I : Set) (B : I → Set) → Kind → Set
ObsTy I B ind   = Σ I B
ObsTy I B coind = Π I B

-- | Make a type testable
record Testable (A : Set) : Set₁ where
  coinductive
  field
    index : Set
    parts : index → Set
    kind : Kind
    obs : A → ObsTy index parts kind
    partsTestable : (i : index) → Testable (parts i)

open Testable public

record IsoTestable (A : Set) : Set₁ where
  field
    testable : Testable A
    obsIso : IsIso (obs testable)
open IsoTestable public

SubTests : {l : Size} → {A : Set} → Testable A → Kind → Set

-- | Test formulae
data Test {i : Size} {A : Set} (T : Testable A) : Set where
  ⊤ : Test T
  ⊥ : Test T
  nonTriv : {j : Size< i} → SubTests {j} T (kind T) → Test {i} {A} T

SubTests {l} T ind   = Π (index T) (λ i → Test {l} (partsTestable T i))
SubTests {l} T coind = Σ (index T) (λ i → Test {l} (partsTestable T i))

-- | Satisfaction of subtests.
sat : {A : Set} {T : Testable A} {l : Size} →
      (k : Kind) → SubTests {l} T k → ObsTy (index T) (parts T) k → Bool

-- | Test satisfaction
_⊨_ : {A : Set} {T : Testable A} → A → Test T → Bool
x ⊨ ⊤ = true
x ⊨ ⊥ = false
_⊨_ {A} {T} x (nonTriv nt) = sat (kind T) nt (obs T x)

sat ind   φs      o = cotuple (λ i y → y ⊨ app φs i) o
sat coind (i , φ) o = app o i ⊨ φ

-- | Observational equivalence: terms are equal if they satisfy the same tests.
record _≃⟨_⟩_ {A : Set} (x : A) (T : Testable A) (y : A) : Set₁ where
  field
    eqProof : (φ : Test T) → (x ⊨ φ ≡ y ⊨ φ)

open _≃⟨_⟩_ public

≡→≃ : {A : Set} → {T : Testable A} →
      {a b : A} → a ≡ b → a ≃⟨ T ⟩ b
≡→≃ p = record { eqProof = λ φ → cong (λ x → x ⊨ φ) p  }

≃-refl :  {A : Set} → (T : Testable A) →
          {a : A} → a ≃⟨ T ⟩ a
≃-refl T = record { eqProof = λ φ → refl }

≃-sym :  {A : Set} → (T : Testable A) →
         {a b : A} → a ≃⟨ T ⟩ b → b ≃⟨ T ⟩ a
≃-sym T p = record { eqProof = sym ∘ (eqProof p)  }

≃-trans :  {A : Set} → (T : Testable A) →
           {a b c : A} → a ≃⟨ T ⟩ b → b ≃⟨ T ⟩ c → a ≃⟨ T ⟩ c
≃-trans T p₁ p₂ =
  record { eqProof = λ φ → trans (eqProof p₁ φ) (eqProof p₂ φ) }

≃-setoid : {A : Set} → (T : Testable A) → Setoid _ _
≃-setoid {A} T = record
  { Carrier = A
  ;_≈_ = λ x y → x ≃⟨ T ⟩ y
  ; isEquivalence = record
    { refl = ≃-refl T
    ; sym = ≃-sym T
    ; trans = ≃-trans T }
  }

-- Most likely impossible to prove within Agda.
-- Is it consistent with the system to postulate this for _IsoTestable_ ?
-- ≃-cong :  {A B : Set} → {T₁ : Testable A} → {T₂ : Testable B} → {a b : A} →
--           (f : A → B) → a ≃⟨ T₁ ⟩ b → f a ≃⟨ T₂ ⟩ f b

-- If A is testable and there is a map B → A, then B is also testable.
comap-testable : {A B : Set} → (B → A) → Testable A → Testable B
comap-testable {A} {B} f T =
  record
  { index = index T
  ; parts = parts T
  ; kind = kind T
  ; obs = (obs T) ∘ f
  ; partsTestable = partsTestable T
  }

-- | If A is testable and A ≅ B, then B is iso-testable as well.
iso-testable : {A B : Set} → Iso B A → IsoTestable A → IsoTestable B
iso-testable {A} {B} I T =
  record
  { testable = comap-testable (Iso.iso I) (testable T)
  ; obsIso = iso-comp (Iso.indeedIso I) (obsIso T)
  }

-- | Heterogeneous
record _~⟨_∥_⟩_ {A B : Set}
                (x : A) (T : Testable A) (I : Iso B A) (y : B) : Set₁ where
  field
    eqProofH : (φ : Test T) → (x ⊨ φ ≡ (Iso.iso I y) ⊨ φ)

open _~⟨_∥_⟩_ public

-- | Helper to match on Kind in construction of ≈.
≈-Proof : {A : Set} →
          (k : Kind) →
          (T : Testable A) →
          (A → ObsTy (index T) (parts T) k) →
          A → A → Set

-- | Bisimilarity induced from testable types.
record _≈⟨_⟩_ {A : Set} (x : A) (T : Testable A) (y : A) : Set where
  coinductive
  field
    proof : ≈-Proof (kind T) T (obs T) x y
open _≈⟨_⟩_ public

-- | Helper to fiddle around with index in construction of IndProof.
ResolveIdx : {A : Set} → (T : Testable A) →
             (i : index T) → (r s : ObsTy (index T) (parts T) ind) →
             proj₁ r ≡ i → proj₁ s ≡ i → Set
ResolveIdx T i (.i , x') (.i , y') refl refl = x' ≈⟨ partsTestable T i ⟩ y'

-- | Proofs of bisimilarity on inductive types.
record IndProof {A : Set}
  (T : Testable A)
  (o : A → ObsTy (index T) (parts T) ind)
  (x y : A) : Set where
  coinductive
  field
    which : index T
    eqIndex₁ : proj₁ (o x) ≡ which
    eqIndex₂ : proj₁ (o y) ≡ which
    eqTrans : ResolveIdx T which (o x) (o y) eqIndex₁ eqIndex₂
open IndProof public

-- | Proofs of bisimilarity on coinductive types.
record CoindProof {A : Set}
  (T : Testable A)
  (o : A → ObsTy (index T) (parts T) coind)
  (x y : A) : Set where
  coinductive
  field
    eqStep : (i : index T) → app (o x) i ≈⟨ partsTestable T i ⟩ app (o y) i
open CoindProof public

≈-Proof ind   = IndProof
≈-Proof coind = CoindProof

-- | Lemma for induction to prove soundness of bisimilarity
lem-≈→≃-testInduct : {j : Size} {A : Set} → (T : Testable A) → (x y : A) →
                     x ≈⟨ T ⟩ y → (φ : Test {j} T) → x ⊨ φ ≡ y ⊨ φ
lem-≈→≃-testInduct _ _ _ _ ⊤ = refl
lem-≈→≃-testInduct _ _ _ _ ⊥ = refl
lem-≈→≃-testInduct {j} {A} T x y x≈y (nonTriv {l} nt)
  = matchKind (kind T) nt (obs T) (proof x≈y)
  where

    matchKind : (k : Kind) →
           (nt : SubTests {l} T k) →
           (o : A → ObsTy (index T) (parts T) k) →
           ≈-Proof k T o x y →
           sat k nt (o x) ≡ sat k nt (o y)
    matchKind ind   nt o p
      = refine (which p) (o x) (o y) (eqIndex₁ p) (eqIndex₂ p) (eqTrans p)
      where
        --| Do pattern matching on IndProof
        refine :  (i : index T) → (r s : ObsTy (index T) (parts T) ind) →
                  (eqP₁ : proj₁ r ≡ i) → (eqP₂ : proj₁ s ≡ i) →
                  ResolveIdx T i r s eqP₁ eqP₂ →
                  (proj₂ r) ⊨ app nt (proj₁ r) ≡ (proj₂ s) ⊨ app nt (proj₁ s)
        refine i (.i , x') (.i , y') refl refl p'
          = lem-≈→≃-testInduct (partsTestable T i) x' y' p' (app nt i)
    matchKind coind nt o p
      = lem-≈→≃-testInduct (partsTestable T i) x' y' (eqStep p i) ψ
      where
        i : index T
        i = proj₁ nt
        ψ = proj₂ nt
        x' = app (o x) i
        y' = app (o y) i

-- | Bisimulation proofs are sound for observational equivalence.
≈→≃ : {A : Set} → (T : Testable A) → (x y : A) →
      x ≈⟨ T ⟩ y → x ≃⟨ T ⟩ y
≈→≃ T x y x≈y = record { eqProof = lem-≈→≃-testInduct T x y x≈y }

{-
≃→≈ : {A : Set} → (T : Testable A) → (x y : A) →
      x ≃⟨ T ⟩ y → x ≈⟨ T ⟩ y
≃→≈ {A} T x y x≃y = record { proof = matchKind (kind T) (obs T) }
  where
    matchKind : (k : Kind) →
                (o : A → ObsTy (index T) (parts T) k) →
                ≈-Proof k T o x y
    matchKind ind o = {!!}
    matchKind coind o = {!!}
-}

max_stars_repo_name: hbasold/Sandbox

max_issues_repo_name: hbasold/Sandbox

max_forks_repo_name: hbasold/Sandbox


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

open import Generics.Prelude hiding (lookup)
open import Generics.Telescope
open import Generics.Desc
open import Generics.All
open import Generics.HasDesc
import Generics.Helpers as Helpers

module Generics.Constructions.Elim {P I ℓ} {A : Indexed P I ℓ} where

module _ (H : HasDesc A) (open HasDesc H)
         {p c} (Pr : Pred′ I (λ i → A′ (p , i) → Set c))
         where

  private
    variable
      V : ExTele P
      i : ⟦ I ⟧tel p
      v : ⟦ V ⟧tel p

  Pr′ : A′ (p , i) → Set c
  Pr′ {i} = unpred′ I _ Pr i

  --------------------------
  -- Types of methods

  levelElimIndArg levelElimCon : ConDesc P V I → Level

  levelElimIndArg (var x) = c
  levelElimIndArg (π {ℓ} i S C) = ℓ ⊔ levelElimIndArg C
  levelElimIndArg (A ⊗ B) = levelElimIndArg A ⊔ levelElimIndArg B

  levelElimCon (var x) = c
  levelElimCon (π {ℓ′} i S C) = ℓ′ ⊔ levelElimCon C
  levelElimCon (A ⊗ B) = levelIndArg A ℓ ⊔ levelElimIndArg A ⊔ levelElimCon B

  MethodIndArg : (C : ConDesc P V I)
               → ⟦ C ⟧IndArg A′ (p , v)
               → Set (levelElimIndArg C)
  MethodIndArg (var x    ) X = Pr′ X
  MethodIndArg (π ia S C) X = Π< ia > (S _) (MethodIndArg C ∘ app< ia > X)
  MethodIndArg (A ⊗ B) (mA , mB) = MethodIndArg A mA × MethodIndArg B mB

  MethodCon : (C : ConDesc P V I)
            → (∀ {i} → ⟦ C ⟧Con A′ (p , v , i) → Set c)
            → Set (levelElimCon C)
  MethodCon (var x) f = f refl
  MethodCon (π ia S C) f = Π< ia > (S _) (λ s → MethodCon C (f ∘ (s ,_)))
  MethodCon (A ⊗ B) f = {g  : ⟦ A ⟧IndArg A′ (p , _)}
                        (Pg : MethodIndArg A g)
                      → MethodCon B (f ∘ (g ,_))

  Methods : ∀ k → Set (levelElimCon (lookupCon D k))
  Methods k = MethodCon (lookupCon D k) λ x → Pr′ (constr (k , x))

  --------------------------
  -- Eliminator

  module _ (methods : Els Methods) where

    elimData-wf
      : (x : ⟦ D ⟧Data A′ (p , i))
      → AllDataω Acc D x
      → Pr′ (constr x)

    elim-wf : (x : A′ (p , i)) → Acc x → Pr′ x
    elim-wf x (acc a) = subst Pr′ (constr∘split x) (elimData-wf (split x) a)

    elimData-wf (k , x) a
      = elimCon (lookupCon D k) (methods k) x a
      where
        elimIndArg
          : (C : ConDesc P V I)
          → (x : ⟦ C ⟧IndArg A′ (p , v))
          → AllIndArgω Acc C x
          → MethodIndArg C x
        elimIndArg (var _) x a = elim-wf x a
        elimIndArg (π ia S C) x a = fun< ia > (λ s → elimIndArg C (app< ia > x s) (a s))
        elimIndArg (A ⊗ B) (xa , xb) (aa , ab)
          = elimIndArg A xa aa
          , elimIndArg B xb ab

        elimCon
          : (C   : ConDesc P V I)
            {mk  : ∀ {i} → ⟦ C ⟧Con A′ (p , v , i) → ⟦ D ⟧Data A′ (p , i)}
            (mot : MethodCon C (λ x → Pr′ (constr (mk x))))
            (x   : ⟦ C ⟧Con A′ (p , v , i))
          → AllConω Acc C x
          → Pr′ (constr (mk x))
        elimCon (var _) mot refl a = mot
        elimCon (π ia _ C) mot (s , x) a = elimCon C (app< ia > mot s) x a
        elimCon (A ⊗ B) mot (xa , xb) (aa , ab)
          = elimCon B (mot (elimIndArg A xa aa)) xb ab

    elim′ : (x : A′ (p , i)) → Pr′ x
    elim′ x = elim-wf x (wf x)

  deriveElim : Arrows Methods (Pred′ I λ i → (x : A′ (p , i)) → Pr′ x)
  deriveElim = curryₙ (λ m → pred′ I _ λ i → elim′ m)

elim : ∀ ⦃ H : HasDesc A ⦄ (open HasDesc H) {p c} (Pr : Pred′ I (λ i → A′ (p , i) → Set c))
     → Arrows (Methods H Pr) (Pred′ I λ i → (x : A′ (p , i)) → Pr′ H Pr x)
elim ⦃ H ⦄ Pr = deriveElim H Pr

max_stars_repo_name: flupe/generics

max_issues_repo_name: flupe/generics

max_forks_repo_name: flupe/generics


text:
open import Theory

module Categories.Functor.Construction.Inclusion {ℓ₁ ℓ₂ ℓ₃} (Th : Theory ℓ₁ ℓ₂ ℓ₃) where

open import Syntax

open Theory.Theory Th
open Signature Sg
open Term Sg

open import Categories.Category.Construction.Renaming Sg as Renaming using (Ren; ren; _≐_)
open import Categories.Category.Construction.Classifying Th using (Cl; CC)

open import Categories.Functor
open import Categories.Category
open import Categories.Morphism Cl using (_≅_; Iso)
open import Categories.Category.CartesianClosed Cl
open import Categories.Category.Cartesian Cl
open import Categories.Category.BinaryProducts Cl

open import Data.List using (List; []; _∷_; _++_)
import Relation.Binary.Reasoning.Setoid as Reasoning
module TermReasoning {Γ A} = Reasoning (TermSetoid {Γ} {A})

inclusion : Functor Ren Cl
inclusion = record
      { F₀ = F₀
      ; F₁ = F₁
      ; identity = C.Equiv.refl
      ; homomorphism = λ {Γ₁} {Γ₂} {Γ₃} {f} {g} -> homomorphism f g
      ; F-resp-≈ = F-resp-≈
      }
  where
    module C = Category Cl
    open CartesianClosed CC
    open Cartesian cartesian
    open BinaryProducts products
    open import Categories.Morphism.Reasoning Cl

    id⁂id : forall {A B} -> C.id ⁂ C.id C.≈ C.id {A = A * B}
    id⁂id = trans (⟨⟩-cong₂ C.identityˡ C.identityˡ) η

    F₀ : Context -> Type
    F₀ [] = Unit
    F₀ (A ∷ Γ) = F₀ Γ * A

    F₀/*⇒++ : forall {Γ Δ} -> F₀ Γ * F₀ Δ C.⇒ F₀ (Δ ++ Γ)
    F₀/*⇒++ {Γ} {[]} = fst var
    F₀/*⇒++ {Γ} {A ∷ Δ} = (F₀/*⇒++ ⁂ C.id) C.∘ assocʳ

    F₀/++⇒* : forall {Γ Δ} -> F₀ (Δ ++ Γ) C.⇒ F₀ Γ * F₀ Δ
    F₀/++⇒* {Γ} {[]} = pair var unit
    F₀/++⇒* {Γ} {A ∷ Δ} = assocˡ C.∘ (F₀/++⇒* ⁂ C.id)

    F₀/*≅++ : forall {Γ Δ} -> F₀ Γ * F₀ Δ ≅ F₀ (Δ ++ Γ)
    F₀/*≅++ = record
      { from = F₀/*⇒++
      ; to = F₀/++⇒*
      ; iso = record { isoˡ = isoˡ ; isoʳ = isoʳ }
      }
      where
        isoˡ : forall {Γ Δ} -> F₀/++⇒* C.∘ F₀/*⇒++ C.≈ C.id {A = F₀ Γ * F₀ Δ}
        isoˡ {Γ} {[]} =
          begin
            pair var unit [ ext ! (fst var) ]
          ≈⟨ trans comm/pair (cong/pair (var/ext _ _) (comm/unit _ _ _)) ⟩
            pair (fst var) unit
          ≈⟨ cong/pair refl (eta/Unit _) ⟩
            pair (fst var) (snd var)
          ≈⟨ eta/* _ ⟩
            var
          ∎
          where open TermReasoning
        isoˡ {Γ} {A ∷ Δ} =
          begin
            (assocˡ C.∘ (F₀/++⇒* ⁂ var)) C.∘ ((F₀/*⇒++ ⁂ var) C.∘ assocʳ)
          ≈⟨ C.assoc ⟩
            assocˡ C.∘ (F₀/++⇒* ⁂ var) C.∘ (F₀/*⇒++ ⁂ var) C.∘ assocʳ
          ≈⟨ C.∘-resp-≈ʳ (pullˡ ⁂∘⁂) ⟩
            assocˡ C.∘ (F₀/++⇒* C.∘ F₀/*⇒++ ⁂ var C.∘ var) C.∘ assocʳ
          ≈⟨ C.∘-resp-≈ʳ (C.∘-resp-≈ˡ (⁂-cong₂ isoˡ C.identity²)) ⟩
            assocˡ C.∘ (var ⁂ var) C.∘ assocʳ
          ≈⟨ elim-center id⁂id ⟩
            assocˡ C.∘ assocʳ
          ≈⟨ assocˡ∘assocʳ ⟩
            var
          ∎
          where open TermReasoning

        isoʳ : forall {Γ Δ} -> F₀/*⇒++ C.∘ F₀/++⇒* {Γ = Γ} C.≈ C.id {A = F₀ (Δ ++ Γ)}
        isoʳ {Γ} {[]} = trans comm/fst (trans (cong/fst (var/ext _ _)) (beta/*₁ _ _))
        isoʳ {Γ} {A ∷ Δ} =
          begin
            ((F₀/*⇒++ ⁂ var) C.∘ assocʳ) C.∘ (assocˡ C.∘ (F₀/++⇒* ⁂ var))
          ≈⟨ cancelInner assocʳ∘assocˡ ⟩
            (F₀/*⇒++ ⁂ var) C.∘ (F₀/++⇒* ⁂ var)
          ≈⟨ ⁂∘⁂ ⟩
            F₀/*⇒++ C.∘ F₀/++⇒* ⁂ var C.∘ var
          ≈⟨ ⁂-cong₂ isoʳ C.identity² ⟩
            var ⁂ var
          ≈⟨ id⁂id ⟩
            var
          ∎
          where open TermReasoning

    F₁p : forall {Γ Δ} -> F₀ (Δ ++ Γ) ∷ [] ⊢ F₀ Γ
    F₁p = fst var C.∘ F₀/++⇒*

    F₁q : forall {Γ Δ} -> F₀ (Δ ++ Γ) ∷ [] ⊢ F₀ Δ
    F₁q = snd var C.∘ F₀/++⇒*

    F₁ : forall {Γ Δ : Context} -> ren Γ Δ -> F₀ Γ ∷ [] ⊢ F₀ Δ
    F₁ Renaming.id = C.id
    F₁ (r Renaming.∙ r₁) = F₁ r C.∘ F₁ r₁
    F₁ Renaming.! = unit
    F₁ Renaming.⟪ r , r₁ ⟫ = F₀/*⇒++ C.∘ pair (F₁ r) (F₁ r₁)
    F₁ Renaming.p = F₁p
    F₁ Renaming.q = F₁q

    homomorphism : forall {Γ₁ Γ₂ Γ₃} (f : ren Γ₁ Γ₂) (g : ren Γ₂ Γ₃)
      -> F₀ Γ₁ ∷ [] ⊢ F₁ g [ ext ! (F₁ f) ] ≡ F₁ g [ ext ! (F₁ f) ]
    homomorphism f g = refl

    F-resp-≈ : forall {Γ Δ} {f g : ren Γ Δ} -> f ≐ g -> F₀ Γ ∷ [] ⊢ F₁ f ≡ F₁ g
    F-resp-≈ _≐_.refl = refl
    F-resp-≈ (_≐_.sym x) = sym (F-resp-≈ x)
    F-resp-≈ (_≐_.trans x x₁) = trans (F-resp-≈ x) (F-resp-≈ x₁)
    F-resp-≈ _≐_.identityˡ = var/ext _ _
    F-resp-≈ _≐_.identityʳ = trans (cong/sub (trans (cong/ext !-unique refl) η-pair) refl) sub/id
    F-resp-≈ _≐_.assoc = C.assoc
    F-resp-≈ _≐_.!-unique = eta/Unit _
    F-resp-≈ _≐_.β₁/⟪⟫ = trans (cancelInner (Iso.isoˡ (_≅_.iso F₀/*≅++))) project₁
    F-resp-≈ _≐_.β₂/⟪⟫ = trans (cancelInner (Iso.isoˡ (_≅_.iso F₀/*≅++))) project₂
    F-resp-≈ _≐_.η/⟪⟫ = trans (C.∘-resp-≈ʳ (trans (⟨⟩-cong₂ C.assoc C.assoc) g-η)) (cancelˡ (Iso.isoʳ (_≅_.iso F₀/*≅++)))
    F-resp-≈ (_≐_.cong/∙ x x₁) = cong/sub (cong/ext refl (F-resp-≈ x₁)) (F-resp-≈ x)
    F-resp-≈ (_≐_.cong/⟪⟫ x x₁) = cong/sub (cong/ext refl (cong/pair (F-resp-≈ x) (F-resp-≈ x₁))) refl

max_stars_repo_name: elpinal/exsub-ccc

max_issues_repo_name: elpinal/exsub-ccc

max_forks_repo_name: elpinal/exsub-ccc


text:
module Haskell.Prim.Double where

open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.Float public renaming (Float to Double)
open import Agda.Builtin.FromNat
open import Agda.Builtin.FromNeg

instance
  iNumberDouble : Number Double
  iNumberDouble .Number.Constraint _ = ⊤
  iNumberDouble .fromNat n = primNatToFloat n

  iNegativeDouble : Negative Double
  iNegativeDouble .Negative.Constraint _ = ⊤
  iNegativeDouble .fromNeg n = primFloatMinus 0.0 (fromNat n)


text:
module Structure.Numeral.Integer.Proofs where

open import Data.Either as Either using (Left ; Right)
import      Data.Tuple as Tuple
open import Functional
open import Function.Proofs
open import Logic.IntroInstances
open import Logic.Predicate
open import Logic.Propositional
import      Lvl
open import Structure.Function.Domain
open import Structure.Function
open import Structure.Numeral.Integer
open import Structure.Relator
open import Structure.Relator.Proofs
open import Structure.Relator.Properties
open import Structure.Setoid
open import Structure.Operator
open import Structure.Operator.Properties
open import Structure.Operator.Ring.Proofs
open import Structure.Operator.Ring
open import Structure.OrderedField
open import Syntax.Implication
open import Syntax.Transitivity
open import Type

private variable ℓₒ ℓₗ ℓₑ ℓₗ₁ ℓₗ₂ : Lvl.Level
private variable Z : Type{ℓₒ}
private variable _+_ _⋅_ : Z → Z → Z
private variable _≤_ : Z → Z → Type{ℓₗ}

module _ ⦃ equiv : Equiv{ℓₑ}(Z) ⦄ ⦃ int : Integer ⦃ equiv ⦄ (_+_)(_⋅_)(_≤_) ⦄ where
  open Integer(int)

  negative-induction : ∀{ℓ}{P : Z → Type{ℓ}} ⦃ rel-p : UnaryRelator(P) ⦄ → P(𝟎) → (∀{n} → (n ≤ 𝟎) → P(n) → P(𝐏(n))) → (∀{n} → (n ≤ 𝟎) → P(n))
  negative-induction {P = P} pz ps {n} neg =
    substitute₁(P) (involution(−_)) (positive-induction
      {P = P ∘ (−_)}
      ⦃ [∘]-unaryRelator ⦄
      (substitute₁ₗ(P) [−]-of-𝟎 pz)
      (\{n} pos pnn → substitute₁ₗ(P) [+]-negation-distribution (ps{− n} ([↔]-to-[→] [≤]-flip-positive pos) pnn))
      {− n}
      ([↔]-to-[→] [≤]-flip-negative neg)
    )

  induction : ∀{ℓ}{P : Z → Type{ℓ}} ⦃ rel-p : UnaryRelator(P) ⦄ → P(𝟎) → (∀{n} → (n ≤ 𝟎) → P(n) → P(𝐏(n))) → (∀{n} → (𝟎 ≤ n) → P(n) → P(𝐒(n))) → (∀{n} → P(n))
  induction pz pp ps {n} with converseTotal(_≤_) {n}{𝟎}
  ... | Left  neg = negative-induction pz pp neg
  ... | Right pos = positive-induction pz ps pos

  [⋅]-commutativity : Commutativity(_⋅_)
  [⋅]-commutativity = intro(induction{P = x ↦ ∀{y} → (x ⋅ y ≡ y ⋅ x)} ⦃ {!!} ⦄ base (const pred) (const succ)) where
    base : ∀{y} → (𝟎 ⋅ y ≡ y ⋅ 𝟎)
    base{y} =
      𝟎 ⋅ y 🝖[ _≡_ ]-[ absorberₗ(_⋅_)(𝟎) ]
      𝟎     🝖[ _≡_ ]-[ absorberᵣ(_⋅_)(𝟎) ]-sym
      y ⋅ 𝟎 🝖-end

    pred : ∀{x} → (∀{y} → (x ⋅ y ≡ y ⋅ x)) → (∀{y} → (𝐏(x) ⋅ y ≡ y ⋅ 𝐏(x)))
    pred {x} p {y} =
      𝐏(x) ⋅ y          🝖[ _≡_ ]-[]
      (x − 𝟏) ⋅ y       🝖[ _≡_ ]-[ distributivityᵣ(_⋅_)(_−_) ⦃ [⋅][−]-distributivityᵣ ⦄ ]
      (x ⋅ y) − (𝟏 ⋅ y) 🝖[ _≡_ ]-[ congruence₂ᵣ(_−_) ⦃ [−]-binaryOperator ⦄ (_) (identityₗ(_⋅_)(𝟏)) ]
      (x ⋅ y) − y       🝖[ _≡_ ]-[ congruence₂ₗ(_−_) ⦃ [−]-binaryOperator ⦄ (_) p ]
      (y ⋅ x) − y       🝖[ _≡_ ]-[ congruence₂ᵣ(_−_) ⦃ [−]-binaryOperator ⦄ (_) (identityᵣ(_⋅_)(𝟏)) ]-sym
      (y ⋅ x) − (y ⋅ 𝟏) 🝖[ _≡_ ]-[ distributivityₗ(_⋅_)(_−_) ⦃ [⋅][−]-distributivityₗ ⦄ ]-sym
      y ⋅ (x − 𝟏)       🝖[ _≡_ ]-[]
      y ⋅ 𝐏(x)          🝖-end

    succ : ∀{x} → (∀{y} → (x ⋅ y ≡ y ⋅ x)) → (∀{y} → (𝐒(x) ⋅ y ≡ y ⋅ 𝐒(x)))
    succ {x} p {y} =
      𝐒(x) ⋅ y          🝖[ _≡_ ]-[]
      (x + 𝟏) ⋅ y       🝖[ _≡_ ]-[ distributivityᵣ(_⋅_)(_+_) ]
      (x ⋅ y) + (𝟏 ⋅ y) 🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(_) (identityₗ(_⋅_)(𝟏)) ]
      (x ⋅ y) + y       🝖[ _≡_ ]-[ congruence₂ₗ(_+_)(_) p ]
      (y ⋅ x) + y       🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(_) (identityᵣ(_⋅_)(𝟏)) ]-sym
      (y ⋅ x) + (y ⋅ 𝟏) 🝖[ _≡_ ]-[ distributivityₗ(_⋅_)(_+_) ]-sym
      y ⋅ (x + 𝟏)       🝖[ _≡_ ]-[]
      y ⋅ 𝐒(x)          🝖-end

  [≤]-identities : (𝟎 ≤ 𝟏)
  [≤]-identities with converseTotal(_≤_) {𝟎}{− 𝟏}
  ... | Left omi =
    omi ⇒
    (𝟎 ≤ (− 𝟏))           ⇒-[ swap apply₂ [≤][⋅]-zero ]
    (𝟎 ≤ ((− 𝟏) ⋅ (− 𝟏))) ⇒-[ _🝖 sub₂(_≡_)(_≤_) [⋅]-of-[−]  ]
    (𝟎 ≤ (𝟏 ⋅ 𝟏))         ⇒-[ _🝖 sub₂(_≡_)(_≤_) (identityₗ(_⋅_)(𝟏))  ]
    (𝟎 ≤ 𝟏)               ⇒-end
  ... | Right mio = [↔]-to-[←] [≤]-flip-positive mio

  [<]-identities : (𝟎 < 𝟏)
  [<]-identities = [≤][≢]-to-[<] [≤]-identities (NonZero.proof distinct-identities ∘ symmetry(_≡_))

  𝐒-of-𝟎 : 𝐒(𝟎) ≡ 𝟏
  𝐒-of-𝟎 =
    𝐒(𝟎)  🝖[ _≡_ ]-[]
    𝟎 + 𝟏 🝖[ _≡_ ]-[ identityₗ(_+_)(𝟎) ]
    𝟏     🝖-end

  instance
    postulate 𝐒-function : Function(𝐒)
    -- 𝐒-function = {!!}

  instance
    postulate [<]-relator : BinaryRelator(_<_)
    -- [<]-relator = {![¬]-binaryRelator!}

  [≤]-with-𝐒 : ∀{x y} → (x ≤ y) → (𝐒(x) ≤ 𝐒(y))
  [≤]-with-𝐒 = [≤][+]ₗ-preserve

  [<]-with-𝐒 : ∀{x y} → (x < y) → (𝐒(x) < 𝐒(y))
  [<]-with-𝐒 = [<][+]-preserveₗ

  [≤]-with-𝐏 : ∀{x y} → (x ≤ y) → (𝐏(x) ≤ 𝐏(y))
  [≤]-with-𝐏 = [≤][−]ₗ-preserve

  [<]-with-𝐏 : ∀{x y} → (x < y) → (𝐏(x) < 𝐏(y))
  [<]-with-𝐏 = [<][+]-preserveₗ

  𝐒-𝐏-inverse : ∀{x} → (𝐒(𝐏(x)) ≡ x)
  𝐒-𝐏-inverse = associativity(_+_) 🝖 congruence₂ᵣ(_+_)(_) (inverseFunctionₗ(_+_)(−_)) 🝖 identityᵣ(_+_)(𝟎)

  𝐏-𝐒-inverse : ∀{x} → (𝐏(𝐒(x)) ≡ x)
  𝐏-𝐒-inverse = associativity(_+_) 🝖 congruence₂ᵣ(_+_)(_) (inverseFunctionᵣ(_+_)(−_)) 🝖 identityᵣ(_+_)(𝟎)

  𝐒-order : ∀{x} → (x < 𝐒(x))
  𝐒-order {x} = induction
    {P = x ↦ x < 𝐒(x)}
    ⦃ binary-unaryRelator ⦃ rel-P = [∘]-binaryRelator ⦄ ⦄
    (subtransitivityᵣ(_<_)(_≡_) [<]-identities (symmetry(_≡_) 𝐒-of-𝟎))
    (const (p ↦ subtransitivityᵣ(_<_)(_≡_) ([<]-with-𝐏 p) (𝐏-𝐒-inverse 🝖 symmetry(_≡_) 𝐒-𝐏-inverse)))
    (const [<]-with-𝐒)

  𝐒-least-upper-bound : ∀{x m} → (x < m) → (𝐒(x) ≤ m)
  𝐒-least-upper-bound {x}{m} xm with converseTotal(_≤_) {x}{m} |  converseTotal(_≤_) {𝐒(x)}{m}
  ... | Left x₁ | Left x₂ = x₂
  ... | Left x₁ | Right x₂ = {!!} -- x<m x≤m m≤𝐒x
  ... | Right x₁ | Left x₂ = x₂
  ... | Right x₁ | Right x₂ with () ← xm x₁
  {-... | Left  𝐒xm  = {!!}
  ... | Right ¬m𝐒x = {!!}
  -}
  {-=
    𝐒(x) 🝖[ _≤_ ]-[ {!!} ]
    m    🝖-end-}

  least-upper-bound-existence : ∃{Obj = Z → Z}(S ↦ (∀{x} → (x < S(x))) ∧ (∀{x m} → (x < m) → (S(x) ≤ m)))
  ∃.witness            least-upper-bound-existence  = 𝐒
  Tuple.left  (∃.proof least-upper-bound-existence) = 𝐒-order
  Tuple.right (∃.proof least-upper-bound-existence) = 𝐒-least-upper-bound

  {- TODO: Not here. Needs invertible mult
  record Exponentiation(_^_ : Z → Z → Z) : Type{ℓₑ Lvl.⊔ Lvl.of(Z) Lvl.⊔ Lvl.of(𝟎 ≤ 𝟎)} where
    field
      base : ∀{a} → (a ^ 𝟎 ≡ 𝟏)
      step : ∀{a b} → (𝟎 ≤ b) → (a ^ (b + 𝟏) ≡ a ⋅ (a ^ b))
      neg  : ∀{a b} → (𝟎 ≤ 𝟎) → (a ^ (− b) ≡ ⅟(a ^ b))
  -}

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 --without-K --safe #-}

module Data.Sum where

open import Level
open import Data.Bool.Base using (Bool; true; false)
open import Function using (const)

data _⊎_ (A : Type a) (B : Type b) : Type (a ℓ⊔ b) where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

either : ∀ {ℓ} {C : A ⊎ B → Type ℓ} →  ((a : A) → C (inl a)) → ((b : B) → C (inr b))
        → (x : A ⊎ B) → C x
either f _ (inl x) = f x
either _ g (inr y) = g y

⟦l_,r_⟧ = either

either′ : (A → C) → (B → C) → (A ⊎ B) → C
either′ = either

_▿_ : (A → C) → (B → C) → A ⊎ B → C
_▿_ = either

is-l : A ⊎ B → Bool
is-l = either′ (const true) (const false)

map-⊎ : ∀ {a₁ a₂ b₁ b₂} {A₁ : Type a₁} {A₂ : Type a₂} {B₁ : Type b₁} {B₂ : Type b₂} →
      (A₁ → A₂) →
      (B₁ → B₂) →
      (A₁ ⊎ B₁) →
      (A₂ ⊎ B₂)
map-⊎ f g (inl x) = inl (f x)
map-⊎ f g (inr x) = inr (g x)

mapˡ : (A → B) → A ⊎ C → B ⊎ C
mapˡ f (inl x) = inl (f x)
mapˡ f (inr x) = inr x

mapʳ : (A → B) → C ⊎ A → C ⊎ B
mapʳ f (inl x) = inl x
mapʳ f (inr x) = inr (f x)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
-- Written by P. Hausmann
module Vec where

open import IO
open import Data.Vec
open import Data.Nat
open import Data.Nat.Show
open import Level using (0ℓ)

Matrix : Set -> ℕ -> ℕ -> Set
Matrix a n m = Vec (Vec a m) n

madd : {n m : ℕ} -> Matrix ℕ m n -> Matrix ℕ m n -> Matrix ℕ m n
madd a b = map (λ x → \y -> map _+_ x ⊛ y) a ⊛ b

idMatrix : {n : ℕ} -> Matrix ℕ n n
idMatrix {zero} = []
idMatrix {suc n} = (1 ∷ (replicate zero)) ∷ (map (λ x → zero ∷ x) idMatrix)

transposeM : {n m : ℕ} {a : Set} -> Matrix a m n -> Matrix a n m
transposeM {zero} {zero} a₁ = []
transposeM {zero} {suc m} {a} x = []
transposeM {suc n} {zero} a₁ = replicate []
transposeM {suc n} {suc m} {a} (_∷_ x₁ x₂) with map head (x₁ ∷ x₂)
... | vm = vm ∷ (map _∷_ (tail x₁) ⊛ transposeM (map tail x₂))

-- We use quite small numbers right now, as with big number the computation
-- gets very slow (at least in MAlonzo)
-- correct result : 109
compute : ℕ
compute = sum (map sum g)
  where m : Matrix ℕ 3 3
        m = (3 ∷ 5 ∷ 9 ∷ []) ∷
              (12 ∷ 0 ∷ 7 ∷ []) ∷ (11 ∷ 2 ∷ 4 ∷ []) ∷ []
        g : Matrix ℕ 3 3
        g = madd (transposeM (transposeM m)) (transposeM (madd m idMatrix))

main = run {0ℓ} (putStrLn (show compute))

max_stars_repo_name: guilhermehas/agda

max_issues_repo_name: guilhermehas/agda

max_forks_repo_name: guilhermehas/agda


text:
open import Oscar.Prelude
open import Oscar.Class.IsCategory
open import Oscar.Class.Reflexivity
open import Oscar.Class.Transitivity

module Oscar.Class.Category where

record Category 𝔬 𝔯 ℓ : Ø ↑̂ (𝔬 ∙̂ 𝔯 ∙̂ ℓ) where
  constructor ∁
  infix 4 _∼̇_
  field
    {𝔒} : Ø 𝔬
    _∼_ : 𝔒 → 𝔒 → Ø 𝔯
    _∼̇_ : ∀ {x y} → x ∼ y → x ∼ y → Ø ℓ
    category-ε : Reflexivity.type _∼_
    _↦_ : Transitivity.type _∼_
    ⦃ `IsCategory ⦄ : IsCategory _∼_ _∼̇_ category-ε _↦_


text:
open import Common.Prelude
open import Common.Reflection

module TermSplicingLooping where

mutual
  f : Set -> Set
  f = unquote (give (def (quote f) []))

-- Expected error:
--
-- Termination checking failed for the following functions:
--   f
-- Problematic calls:
--   f

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module _ where

open import Common.Prelude renaming (_∸_ to _-_) -- work-around for #1855

_<_ : Nat → Nat → Bool
a < b with b - a
... | zero  = false
... | suc _ = true

insert : Nat → List Nat → List Nat
insert x [] = x ∷ []
insert x (y ∷ xs) = if x < y then x ∷ y ∷ xs else (y ∷ insert x xs)

sort : List Nat → List Nat
sort [] = []
sort (x ∷ xs) = insert x (sort xs)

downFrom : Nat → List Nat
downFrom zero = []
downFrom (suc n) = n ∷ downFrom n

mapM! : {A : Set} → (A → IO Unit) → List A → IO Unit
mapM! f [] = return unit
mapM! f (x ∷ xs) = f x >>= λ _ → mapM! f xs

main : IO Unit
main = mapM! printNat (sort (downFrom 1200))

-- 1000   0.6s
-- 2000   4.8s
-- 4000   36.2s


text:
{-# OPTIONS --cubical --no-import-sorts #-}

module Number.Definitions where

open import Agda.Primitive renaming (_⊔_ to ℓ-max; lsuc to ℓ-suc; lzero to ℓ-zero)
open import Cubical.Foundations.Everything renaming (_⁻¹ to _⁻¹ᵖ; assoc to ∙-assoc)
open import Cubical.Foundations.Logic

open import Utils
open import MoreLogic.Definitions
open import MoreLogic.Properties
open import MorePropAlgebra.Definitions
open import MorePropAlgebra.Consequences
open import MorePropAlgebra.Structures

max_stars_repo_name: mchristianl/synthetic-reals

max_issues_repo_name: mchristianl/synthetic-reals

max_forks_repo_name: mchristianl/synthetic-reals


text:
open import Agda.Primitive
open import Empty
open import Logic
open import Boolean

module Peano where

  data ℕ : Set where
    zero : ℕ
    succ : ℕ → ℕ
  {-# BUILTIN NATURAL ℕ #-}

  pred : ℕ → ℕ
  pred zero = zero
  pred (succ x) = x

  _+_ : ℕ → ℕ → ℕ
  zero + m = m
  (succ n) + m = succ (n + m)
  {-# BUILTIN NATPLUS _+_ #-}

  _∘_ : ℕ → ℕ → ℕ
  zero ∘ _ = zero
  (succ n) ∘ m = (n ∘ m) + m
  {-# BUILTIN NATTIMES _∘_ #-}

  data _≡_ (x : ℕ) : ℕ → Set where
    refl : x ≡ x

  data _≢_ : ℕ → ℕ → Set where
    z≢s : ∀ {n} → zero ≢ succ n
    s≢z : ∀ {n} → succ n ≢ zero
    s≢s : ∀ {m n} → m ≢ n → succ m ≢ succ n

  data Equal? (m n : ℕ) : Set where
    yes : m ≡ n → Equal? m n
    no : m ≢ n → Equal? m n

  _≟_ : (m n : ℕ) → Equal? m n
  _≟_ zero zero = yes refl
  _≟_ zero (succ _) = no z≢s
  _≟_ (succ _) zero = no s≢z
  _≟_ (succ m) (succ n) with m ≟ n
  _≟_ (succ m) (succ .m) | yes refl = yes refl
  _≟_ (succ m) (succ n) | no p = no (s≢s p)

  equality-disjoint : (m n : ℕ) → m ≡ n → m ≢ n → ⊥
  equality-disjoint zero zero refl ()
  equality-disjoint zero (succ _) () z≢s
  equality-disjoint (succ _) zero () s≢z
  equality-disjoint (succ m) (succ .m) refl (s≢s e) = equality-disjoint m m refl e

  private
    -- to make the last `equality-disjoint` match clearer, verify that s≢s can be nested
    test-s≢s : (succ (succ (succ zero))) ≢ (succ (succ zero))
    test-s≢s = s≢s (s≢s s≢z)

  data Ordering : Rel ℕ where
    less : ∀ m k → Ordering m (succ (m + k))
    equal : ∀ m → Ordering m m
    greater : ∀ m k → Ordering (succ (m + k)) m

  compare : ∀ m n → Ordering m n
  compare zero zero = equal zero
  compare (succ m) zero = greater zero m
  compare zero (succ n) = less zero n
  compare (succ m) (succ n) with compare m n
  compare (succ .m) (succ .(succ m + k)) | less m k = less (succ m) k
  compare (succ .m) (succ .m) | equal m = equal (succ m)
  compare (succ .(succ m + k)) (succ .m) | greater m k = greater (succ m) k

  infix 4 _≤_ _<_ _≥_ _>_ _≰_ _≮_ _≱_ _≯_

  data _≤_ : Rel ℕ where
    z≤n : ∀ {n} → zero ≤ n
    s≤s : ∀ {m n} (m≤n : m ≤ n) → succ m ≤ succ n

  _<_ : Rel ℕ
  m < n = succ m ≤ n

  _≥_ : Rel ℕ
  m ≥ n = n ≤ m

  _>_ : Rel ℕ
  m > n = n < m

  _≰_ : Rel ℕ
  a ≰ b = ¬ (a ≤ b)

  _≮_ : Rel ℕ
  a ≮ b = ¬ (a < b)

  _≱_ : Rel ℕ
  a ≱ b = ¬ (a ≥ b)

  _≯_ : Rel ℕ
  a ≯ b = ¬ (a > b)

  data _even : ℕ → Set where
    ZERO : zero even
    STEP : ∀ {x} → x even → succ (succ x) even

  private
    proof₁ : succ(succ(succ(succ(zero)))) even
    proof₁ = STEP (STEP ZERO)

    proof₂ : (A : Set) → A → A
    proof₂ _ ν = ν

    proof'₂ : ℕ → ℕ
    proof'₂ = proof₂ ℕ

max_stars_repo_name: cantsin/agda-experiments

max_issues_repo_name: cantsin/agda-experiments

max_forks_repo_name: cantsin/agda-experiments


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

open import HoTT
open import cw.CW

module cw.examples.Empty where

cw-empty-skel : Skeleton {lzero} 0
cw-empty-skel = Empty , Empty-is-set
CWEmpty = ⟦ cw-empty-skel ⟧

CWEmpty-equiv-Empty : CWEmpty ≃ Empty
CWEmpty-equiv-Empty = ide _

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

open import Categories.Category

module Categories.Category.Construction.Pullbacks {o ℓ e} (C : Category o ℓ e) where

open import Level using (_⊔_)
open import Function using (_$_)
open import Data.Product using (_×_; _,_)

open import Categories.Diagram.Pullback C
open import Categories.Morphism.Reasoning C

open Category C

record PullbackObj W : Set (o ⊔ ℓ ⊔ e) where
  field
    {A} {B}  : Obj
    arr₁     : A ⇒ W
    arr₂     : B ⇒ W
    pullback : Pullback arr₁ arr₂

  module pullback = Pullback pullback

open HomReasoning

record Pullback⇒ W (X Y : PullbackObj W) : Set (o ⊔ ℓ ⊔ e) where
  module X = PullbackObj X
  module Y = PullbackObj Y
  field
    mor₁     : X.A ⇒ Y.A
    mor₂     : X.B ⇒ Y.B
    commute₁ : Y.arr₁ ∘ mor₁ ≈ X.arr₁
    commute₂ : Y.arr₂ ∘ mor₂ ≈ X.arr₂

  pbarr : X.pullback.P ⇒ Y.pullback.P
  pbarr = Y.pullback.universal $ begin
    Y.arr₁ ∘ mor₁ ∘ X.pullback.p₁ ≈⟨ pullˡ commute₁ ⟩
    X.arr₁ ∘ X.pullback.p₁        ≈⟨ X.pullback.commute ⟩
    X.arr₂ ∘ X.pullback.p₂        ≈˘⟨ pullˡ commute₂ ⟩
    Y.arr₂ ∘ mor₂ ∘ X.pullback.p₂ ∎

open Pullback⇒

Pullbacks : Obj → Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) e
Pullbacks W = record
  { Obj       = PullbackObj W
  ; _⇒_       = Pullback⇒ W
  ; _≈_       = λ f g → mor₁ f ≈ mor₁ g × mor₂ f ≈ mor₂ g
  ; id        = record
    { mor₁     = id
    ; mor₂     = id
    ; commute₁ = identityʳ
    ; commute₂ = identityʳ
    }
  ; _∘_       = λ f g → record
    { mor₁     = mor₁ f ∘ mor₁ g
    ; mor₂     = mor₂ f ∘ mor₂ g
    ; commute₁ = pullˡ (commute₁ f) ○ commute₁ g
    ; commute₂ = pullˡ (commute₂ f) ○ commute₂ g
    }
  ; assoc     = assoc , assoc
  ; sym-assoc = sym-assoc , sym-assoc
  ; identityˡ = identityˡ , identityˡ
  ; identityʳ = identityʳ , identityʳ
  ; identity² = identity² , identity²
  ; equiv     = record
    { refl  = refl , refl
    ; sym   = λ { (eq₁ , eq₂) → sym eq₁ , sym eq₂ }
    ; trans = λ { (eq₁ , eq₂) (eq₃ , eq₄) → trans eq₁ eq₃ , trans eq₂ eq₄ }
    }
  ; ∘-resp-≈  = λ { (eq₁ , eq₂) (eq₃ , eq₄) → ∘-resp-≈ eq₁ eq₃ , ∘-resp-≈ eq₂ eq₄ }
  }

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.Algebra.GradedRing.Instances.PolynomialsFun where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat hiding (_·_) renaming (_+_ to _+n_)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Sigma

open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Ring
open import Cubical.Algebra.GradedRing.Base
open import Cubical.Algebra.GradedRing.DirectSumFun

private variable
  ℓ : Level

module _
  (ARing@(A , Astr) : Ring ℓ)
  (n : ℕ)
  where

  open RingStr Astr
  open RingTheory ARing

  PolyGradedRing : GradedRing ℓ-zero ℓ
  PolyGradedRing = ⊕Fun-GradedRing
                   _+n_ (makeIsMonoid isSetℕ +-assoc +-zero λ _ → refl) (λ _ _ → refl)
                   (λ _ → A)
                   (λ _ → snd (Ring→AbGroup ARing))
                   1r _·_ 0LeftAnnihilates 0RightAnnihilates
                   (λ a b c → ΣPathP ((+-assoc _ _ _) , (·Assoc _ _ _)))
                   (λ a → ΣPathP ((+-zero _) , (·IdR _)))
                   (λ a → ΣPathP (refl , (·IdL _)))
                   ·DistR+
                   ·DistL+

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
postulate
  List      : Set
  List-like : Set → Set

instance
  postulate
    List-is-list-like : List-like List

postulate
  to-List : ∀ {F : Set} ⦃ list-like : ∀ {X : Set} → List-like F ⦄ → F → List
  F       : Set

f : ⦃ list-like : List-like F ⦄ → List
f = to-List _


text:
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRingSolver.Utility where

open import Cubical.Foundations.Prelude

open import Cubical.Data.Bool
open import Cubical.Data.Empty using (⊥) renaming (rec to recEmpty)
open import Cubical.Data.Sigma

open import Cubical.Relation.Nullary.Base

private
  variable
    ℓ ℓ' : Level
byBoolAbsurdity : {Anything : Type ℓ} → false ≡ true → Anything
byBoolAbsurdity p = recEmpty (false≢true p)

byAbsurdity : {Anything : Type ℓ} → ⊥ → Anything
byAbsurdity x = recEmpty x

extractFromAnd : (P Q : Bool)
              → P and Q ≡ true
              → (P ≡ true) × (Q ≡ true)
extractFromAnd false false eq = byBoolAbsurdity eq
extractFromAnd false true eq = byBoolAbsurdity eq
extractFromAnd true false eq = byBoolAbsurdity eq
extractFromAnd true true eq = eq , eq

extractFromAndLeft : {P Q : Bool}
             → P and Q ≡ true
             → P ≡ true
extractFromAndLeft eq = fst (extractFromAnd _ _ eq)

extractFromAndRight : {P Q : Bool}
             → P and Q ≡ true
             → Q ≡ true
extractFromAndRight eq = snd (extractFromAnd _ _ eq)


text:
{-

This file contains:

- Homotopy natural equivalences of pushout spans
  Written by: Loïc Pujet, September 2019

- 3×3 lemma for pushouts
  Written by: Loïc Pujet, April 2019

-}

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

module Cubical.HITs.Pushout.Properties where

open import Cubical.Core.Glue

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HAEquiv
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Transport

open import Cubical.Data.Prod.Base
open import Cubical.Data.Unit

open import Cubical.HITs.Pushout.Base

{-
  Definition of pushout diagrams
-}

record 3-span : Type₁ where
  field
    A0 A2 A4 : Type₀
    f1 : A2 → A0
    f3 : A2 → A4

spanPushout : (s : 3-span) → Type₀
spanPushout s = Pushout (3-span.f1 s) (3-span.f3 s)

{-
  Definition of a homotopy natural diagram equivalence
-}

record 3-span-equiv (s1 : 3-span) (s2 : 3-span) : Type₀ where
   field
     e0 : 3-span.A0 s1 ≃ 3-span.A0 s2
     e2 : 3-span.A2 s1 ≃ 3-span.A2 s2
     e4 : 3-span.A4 s1 ≃ 3-span.A4 s2
     H1 : ∀ x → 3-span.f1 s2 (e2 .fst x) ≡ e0 .fst (3-span.f1 s1 x)
     H3 : ∀ x → 3-span.f3 s2 (e2 .fst x) ≡ e4 .fst (3-span.f3 s1 x)

{-
  Proof that homotopy equivalent spans are in fact equal
-}
spanEquivToPath : {s1 : 3-span} → {s2 : 3-span} → (e : 3-span-equiv s1 s2) → s1 ≡ s2
spanEquivToPath {s1} {s2} e = spanPath
  where
    open 3-span-equiv e
    open 3-span

    path0 : A0 s1 ≡ A0 s2
    path0 = ua e0

    path2 : A2 s1 ≡ A2 s2
    path2 = ua e2

    path4 : A4 s1 ≡ A4 s2
    path4 = ua e4

    spanPath1 : I → 3-span
    spanPath1 i = record { A0 = path0 i ; A2 = path2 i ; A4 = path4 i ;
                           f1 = λ x → (transp (λ j → path0 (i ∧ j)) (~ i) (f1 s1 (transp (λ j → path2 (~ j ∧ i)) (~ i) x))) ;
                           f3 = λ x → (transp (λ j → path4 (i ∧ j)) (~ i) (f3 s1 (transp (λ j → path2 (~ j ∧ i)) (~ i) x))) }

    spanPath2 : I → 3-span
    spanPath2 i = record { A0 = A0 s2 ; A2 = A2 s2 ; A4 = A4 s2 ; f1 = f1Path i ; f3 = f3Path i }
      where
        f1Path : I → A2 s2 → A0 s2
        f1Path i x = ((uaβ e0 (f1 s1 (transport (λ j → path2 (~ j)) x)))
                     ∙ (H1 (transport (λ j → path2 (~ j)) x)) ⁻¹
                     ∙ (λ j → f1 s2 (uaβ e2 (transport (λ j → path2 (~ j)) x) (~ j)))
                     ∙ (λ j → f1 s2 (transportTransport⁻ path2 x j))) i

        f3Path : I → A2 s2 → A4 s2
        f3Path i x = ((uaβ e4 (f3 s1 (transport (λ j → path2 (~ j)) x)))
                     ∙ (H3 (transport (λ j → path2 (~ j)) x)) ⁻¹
                     ∙ (λ j → f3 s2 (uaβ e2 (transport (λ j → path2 (~ j)) x) (~ j)))
                     ∙ (λ j → f3 s2 (transportTransport⁻ path2 x j))) i

    spanPath : s1 ≡ s2
    spanPath = (λ i → spanPath1 i) ∙ (λ i → spanPath2 i)

-- as a corollary, they have the same pushout
spanEquivToPushoutPath : {s1 : 3-span} → {s2 : 3-span} → (e : 3-span-equiv s1 s2)
                         → spanPushout s1 ≡ spanPushout s2
spanEquivToPushoutPath {s1} {s2} e = cong spanPushout (spanEquivToPath e)

{-

  3×3 lemma for pushouts

Let Aᵢⱼ denote a type, fᵢⱼ a map and Hᵢⱼ a homotopy. Given a diagram of the following shape:

A00 ←—f01—— A02 ——f03—→ A04
 ↑           ↑           ↑
f10   H11   f12   H13   f14
 |           |           |
A20 ←—f21—— A22 ——f23—→ A24
 |           |           |
f30   H31   f32   H33   f34
 ↓           ↓           ↓
A40 ←—f41—— A42 ——f43—→ A44

one can build its colimit from pushouts in two ways:
- either build pushouts A□0, A□2, A□4 of the lines and then build the pushout A□○ of the resulting
  diagram A□0 ←—f□1—— A□2 ——f□3—→ A□4 ;
- or build pushouts of the columns and build the pushout A○□ of the resulting diagram A0□ ← A2□ → A4□.

Then the lemma states there is an equivalence A□○ ≃ A○□.

-}

record 3x3-span : Type₁ where
  field
    A00 A02 A04 A20 A22 A24 A40 A42 A44 : Type₀

    f10 : A20 → A00
    f12 : A22 → A02
    f14 : A24 → A04

    f30 : A20 → A40
    f32 : A22 → A42
    f34 : A24 → A44

    f01 : A02 → A00
    f21 : A22 → A20
    f41 : A42 → A40

    f03 : A02 → A04
    f23 : A22 → A24
    f43 : A42 → A44

    H11 : ∀ x → f01 (f12 x) ≡ f10 (f21 x)
    H13 : ∀ x → f03 (f12 x) ≡ f14 (f23 x)
    H31 : ∀ x → f41 (f32 x) ≡ f30 (f21 x)
    H33 : ∀ x → f43 (f32 x) ≡ f34 (f23 x)

  -- pushouts of the lines
  A□0 : Type₀
  A□0 = Pushout f10 f30

  A□2 : Type₀
  A□2 = Pushout f12 f32

  A□4 : Type₀
  A□4 = Pushout f14 f34

  -- maps between pushouts
  f□1 : A□2 → A□0
  f□1 (inl x) = inl (f01 x)
  f□1 (inr x) = inr (f41 x)
  f□1 (push a j) = ((λ i → inl (H11 a i))
                   ∙∙ push (f21 a)
                   ∙∙ (λ i → inr (H31 a (~ i)))) j

  f□3 : A□2 → A□4
  f□3 (inl x) = inl (f03 x)
  f□3 (inr x) = inr (f43 x)
  f□3 (push a j) = ((λ i → inl (H13 a i))
                   ∙∙ push (f23 a)
                   ∙∙ (λ i → inr (H33 a (~ i)))) j

  -- total pushout
  A□○ : Type₀
  A□○ = Pushout f□1 f□3

  -- pushouts of the columns
  A0□ : Type₀
  A0□ = Pushout f01 f03

  A2□ : Type₀
  A2□ = Pushout f21 f23

  A4□ : Type₀
  A4□ = Pushout f41 f43

  -- maps between pushouts
  f1□ : A2□ → A0□
  f1□ (inl x) = inl (f10 x)
  f1□ (inr x) = inr (f14 x)
  f1□ (push a j) = ((λ i → inl (H11 a (~ i)))
                   ∙∙ push (f12 a)
                   ∙∙ (λ i → inr (H13 a i))) j

  f3□ : A2□ → A4□
  f3□ (inl x) = inl (f30 x)
  f3□ (inr x) = inr (f34 x)
  f3□ (push a j) = ((λ i → inl (H31 a (~ i)))
                   ∙∙ push (f32 a)
                   ∙∙ (λ i → inr (H33 a i))) j

  -- total pushout
  A○□ : Type₀
  A○□ = Pushout f1□ f3□

  -- the claimed result
  3x3-lemma : A□○ ≡ A○□
  3x3-lemma = isoToPath (iso A□○→A○□ A○□→A□○ A○□→A□○→A○□ A□○→A○□→A□○)
    where
      -- forward map of the equivalence A□○ ≃ A○□
      forward-l : A□0 → A○□
      forward-l (inl x) = inl (inl x)
      forward-l (inr x) = inr (inl x)
      forward-l (push a i) = push (inl a) i

      forward-r : A□4 → A○□
      forward-r (inl x) = inl (inr x)
      forward-r (inr x) = inr (inr x)
      forward-r (push a i) = push (inr a) i

      forward-filler : A22 → I → I → I → A○□
      forward-filler a i j = hfill (λ t → λ { (i = i0) → inl (doubleCompPath-filler (λ k → inl (H11 a (~ k))) (push (f12 a)) (λ k → inr (H13 a k)) j (~ t))
                                     ; (i = i1) → inr (doubleCompPath-filler (λ k → inl (H31 a (~ k))) (push (f32 a)) (λ k → inr (H33 a k)) j (~ t))
                                     ; (j = i0) → forward-l (doubleCompPath-filler (λ k → inl (H11 a k)) (push (f21 a)) (λ k → inr (H31 a (~ k))) i t)
                                     ; (j = i1) → forward-r (doubleCompPath-filler (λ k → inl (H13 a k)) (push (f23 a)) (λ k → inr (H33 a (~ k))) i t) })
                            (inS (push (push a j) i))

      A□○→A○□ : A□○ → A○□
      A□○→A○□ (inl x) = forward-l x
      A□○→A○□ (inr x) = forward-r x
      A□○→A○□ (push (inl x) i) = inl (push x i)
      A□○→A○□ (push (inr x) i) = inr (push x i)
      A□○→A○□ (push (push a i) j) = forward-filler a i j i1

      -- backward map
      backward-l : A0□ → A□○
      backward-l (inl x) = inl (inl x)
      backward-l (inr x) = inr (inl x)
      backward-l (push a i) = push (inl a) i

      backward-r : A4□ → A□○
      backward-r (inl x) = inl (inr x)
      backward-r (inr x) = inr (inr x)
      backward-r (push a i) = push (inr a) i

      backward-filler : A22 → I → I → I → A□○
      backward-filler a i j = hfill (λ t → λ { (i = i0) → inl (doubleCompPath-filler (λ k → inl (H11 a k)) (push (f21 a)) (λ k → inr (H31 a (~ k))) j (~ t))
                                     ; (i = i1) → inr (doubleCompPath-filler (λ k → inl (H13 a k)) (push (f23 a)) (λ k → inr (H33 a (~ k))) j (~ t))
                                     ; (j = i0) → backward-l (doubleCompPath-filler (λ k → inl (H11 a (~ k))) (push (f12 a)) (λ k → inr (H13 a k)) i t)
                                     ; (j = i1) → backward-r (doubleCompPath-filler (λ k → inl (H31 a (~ k))) (push (f32 a)) (λ k → inr (H33 a k)) i t) })
                            (inS (push (push a j) i))

      A○□→A□○ : A○□ → A□○
      A○□→A□○ (inl x) = backward-l x
      A○□→A□○ (inr x) = backward-r x
      A○□→A□○ (push (inl x) i) = inl (push x i)
      A○□→A□○ (push (inr x) i) = inr (push x i)
      A○□→A□○ (push (push a i) j) = backward-filler a i j i1

      -- first homotopy
      homotopy1-l : ∀ x → A□○→A○□ (backward-l x) ≡ inl x
      homotopy1-l (inl x) = refl
      homotopy1-l (inr x) = refl
      homotopy1-l (push a i) = refl

      homotopy1-r : ∀ x → A□○→A○□ (backward-r x) ≡ inr x
      homotopy1-r (inl x) = refl
      homotopy1-r (inr x) = refl
      homotopy1-r (push a i) = refl

      A○□→A□○→A○□ : ∀ x → A□○→A○□ (A○□→A□○ x) ≡ x
      A○□→A□○→A○□ (inl x) = homotopy1-l x
      A○□→A□○→A○□ (inr x) = homotopy1-r x
      A○□→A□○→A○□ (push (inl x) i) k = push (inl x) i
      A○□→A□○→A○□ (push (inr x) i) k = push (inr x) i
      A○□→A□○→A○□ (push (push a i) j) k =
        hcomp (λ t → λ { (i = i0) → forward-l (doubleCompPath-filler (λ k → inl (H11 a k)) (push (f21 a)) (λ k → inr (H31 a (~ k))) j (~ t))
                       ; (i = i1) → forward-r (doubleCompPath-filler (λ k → inl (H13 a k)) (push (f23 a)) (λ k → inr (H33 a (~ k))) j (~ t))
                       ; (j = i0) → homotopy1-l (doubleCompPath-filler (λ k → inl (H11 a (~ k))) (push (f12 a)) (λ k → inr (H13 a k)) i t) k
                       ; (j = i1) → homotopy1-r (doubleCompPath-filler (λ k → inl (H31 a (~ k))) (push (f32 a)) (λ k → inr (H33 a k)) i t) k
                       ; (k = i0) → A□○→A○□ (backward-filler a i j t)
                       ; (k = i1) → forward-filler a j i (~ t) })
              (forward-filler a j i i1)

      -- second homotopy
      homotopy2-l : ∀ x → A○□→A□○ (forward-l x) ≡ inl x
      homotopy2-l (inl x) = refl
      homotopy2-l (inr x) = refl
      homotopy2-l (push a i) = refl

      homotopy2-r : ∀ x → A○□→A□○ (forward-r x) ≡ inr x
      homotopy2-r (inl x) = refl
      homotopy2-r (inr x) = refl
      homotopy2-r (push a i) = refl

      A□○→A○□→A□○ : ∀ x → A○□→A□○ (A□○→A○□ x) ≡ x
      A□○→A○□→A□○ (inl x) = homotopy2-l x
      A□○→A○□→A□○ (inr x) = homotopy2-r x
      A□○→A○□→A□○ (push (inl x) i) k = push (inl x) i
      A□○→A○□→A□○ (push (inr x) i) k = push (inr x) i
      A□○→A○□→A□○ (push (push a i) j) k =
        hcomp (λ t → λ { (i = i0) → backward-l (doubleCompPath-filler (λ k → inl (H11 a (~ k))) (push (f12 a)) (λ k → inr (H13 a k)) j (~ t))
                       ; (i = i1) → backward-r (doubleCompPath-filler (λ k → inl (H31 a (~ k))) (push (f32 a)) (λ k → inr (H33 a k)) j (~ t))
                       ; (j = i0) → homotopy2-l (doubleCompPath-filler (λ k → inl (H11 a k)) (push (f21 a)) (λ k → inr (H31 a (~ k))) i t) k
                       ; (j = i1) → homotopy2-r (doubleCompPath-filler (λ k → inl (H13 a k)) (push (f23 a)) (λ k → inr (H33 a (~ k))) i t) k
                       ; (k = i0) → A○□→A□○ (forward-filler a i j t)
                       ; (k = i1) → backward-filler a j i (~ t) })
              (backward-filler a j i i1)

max_stars_repo_name: cj-xu/cubical

max_issues_repo_name: cj-xu/cubical

max_forks_repo_name: cj-xu/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Convenient syntax for "equational reasoning" using a strict partial
-- order
------------------------------------------------------------------------

open import Relation.Binary

module Relation.Binary.StrictPartialOrderReasoning
         {p₁ p₂ p₃} (S : StrictPartialOrder p₁ p₂ p₃) where

import Relation.Binary.PreorderReasoning as PreR
import Relation.Binary.Properties.StrictPartialOrder as SPO
open PreR (SPO.preorder S) public renaming (_∼⟨_⟩_ to _<⟨_⟩_)