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

module Data.ByteString.Primitive.Strict where

open import Data.Word8.Primitive using (Word8)
open import Agda.Builtin.Nat using (Nat)
open import Agda.Builtin.List using (List)
open import Agda.Builtin.String using (String)
open import Agda.Builtin.Bool using (Bool)
open import Agda.Builtin.IO using (IO)
open import Data.Tuple.Base using (Pair)

{-# FOREIGN GHC import qualified Data.Word    #-}
{-# FOREIGN GHC import qualified Data.Text    #-}
{-# FOREIGN GHC import qualified Data.ByteString    #-}
open import Foreign.Haskell using (Unit)

open import Data.ByteString.Primitive.Int

postulate
  ByteStringStrict : Set
  readBinaryFileStrict    : String → IO ByteStringStrict
  writeBinaryFileStrict   : String → ByteStringStrict → IO Unit
  List←Strict : ByteStringStrict → List Word8
  List→Strict : List Word8 → ByteStringStrict
  emptyStrict : ByteStringStrict
  nullStrict : ByteStringStrict → Bool
  lengthStrict : ByteStringStrict → Int
  headStrict : ByteStringStrict → Word8
  tailStrict : ByteStringStrict → ByteStringStrict
  indexStrict : ByteStringStrict → Int → Word8
  splitAtStrict : Int → ByteStringStrict → Pair ByteStringStrict ByteStringStrict

{-# COMPILE GHC ByteStringStrict = type
    Data.ByteString.ByteString
#-}
{-# COMPILE GHC readBinaryFileStrict =
    ( Data.ByteString.readFile
    . Data.Text.unpack
    )
#-}
{-# COMPILE GHC writeBinaryFileStrict =
    ( Data.ByteString.writeFile
    . Data.Text.unpack
    )
#-}
{-# COMPILE GHC List←Strict =
    ( Data.ByteString.unpack ) #-}
{-# COMPILE GHC List→Strict =
    ( Data.ByteString.pack ) #-}
{-# COMPILE GHC emptyStrict = (Data.ByteString.empty) #-}
{-# COMPILE GHC nullStrict = (Data.ByteString.null) #-}
{-# COMPILE GHC lengthStrict = (Data.ByteString.length) #-}
{-# COMPILE GHC headStrict = (Data.ByteString.head) #-}
{-# COMPILE GHC tailStrict = (Data.ByteString.tail) #-}
{-# COMPILE GHC indexStrict = (Data.ByteString.index) #-}
{-# COMPILE GHC splitAtStrict = (Data.ByteString.splitAt) #-}

max_stars_repo_name: semenov-vladyslav/bytes-agda

max_issues_repo_name: semenov-vladyslav/bytes-agda

max_forks_repo_name: semenov-vladyslav/bytes-agda


text:
module Logics.Not where

open import Function
open import Relation.Nullary

------------------------------------------------------------------------
-- internal stuffs

private

  a=¬∘¬a : ∀ {a} {A : Set a} → A → ¬ (¬ A)
  a=¬∘¬a a z = z a

  /p→q/→¬/p→¬q/ : ∀ {p q} {P : Set p} {Q : Set q} → (P → Q) → (¬ Q → ¬ P)
  /p→q/→¬/p→¬q/ p→q ¬q p = ¬q $ p→q p

------------------------------------------------------------------------
-- public aliases

not-not : ∀ {ℓ} {A : Set ℓ} → A → ¬ (¬ A)
not-not = a=¬∘¬a

contrapositive : ∀ {p q} {P : Set p} {Q : Set q} → (P → Q) → (¬ Q → ¬ P)
contrapositive = /p→q/→¬/p→¬q/

ext: agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

open import Algebra

module Algebra.Properties.Group {g₁ g₂} (G : Group g₁ g₂) where

open Group G
import Algebra.FunctionProperties as P; open P _≈_
import Relation.Binary.EqReasoning as EqR; open EqR setoid
open import Function
open import Data.Product

⁻¹-involutive : ∀ x → x ⁻¹ ⁻¹ ≈ x
⁻¹-involutive x = begin
  x ⁻¹ ⁻¹               ≈⟨ sym $ proj₂ identity _ ⟩
  x ⁻¹ ⁻¹ ∙ ε           ≈⟨ refl ⟨ ∙-cong ⟩ sym (proj₁ inverse _) ⟩
  x ⁻¹ ⁻¹ ∙ (x ⁻¹ ∙ x)  ≈⟨ sym $ assoc _ _ _ ⟩
  x ⁻¹ ⁻¹ ∙ x ⁻¹ ∙ x    ≈⟨ proj₁ inverse _ ⟨ ∙-cong ⟩ refl ⟩
  ε ∙ x                 ≈⟨ proj₁ identity _ ⟩
  x                     ∎

private

  left-helper : ∀ x y → x ≈ (x ∙ y) ∙ y ⁻¹
  left-helper x y = begin
    x              ≈⟨ sym (proj₂ identity x) ⟩
    x ∙ ε          ≈⟨ refl ⟨ ∙-cong ⟩ sym (proj₂ inverse y) ⟩
    x ∙ (y ∙ y ⁻¹) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩
    (x ∙ y) ∙ y ⁻¹ ∎

  right-helper : ∀ x y → y ≈ x ⁻¹ ∙ (x ∙ y)
  right-helper x y = begin
    y              ≈⟨ sym (proj₁ identity y) ⟩
    ε          ∙ y ≈⟨ sym (proj₁ inverse x) ⟨ ∙-cong ⟩ refl ⟩
    (x ⁻¹ ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩
    x ⁻¹ ∙ (x ∙ y) ∎

left-identity-unique : ∀ x y → x ∙ y ≈ y → x ≈ ε
left-identity-unique x y eq = begin
  x              ≈⟨ left-helper x y ⟩
  (x ∙ y) ∙ y ⁻¹ ≈⟨ eq ⟨ ∙-cong ⟩ refl ⟩
       y  ∙ y ⁻¹ ≈⟨ proj₂ inverse y ⟩
  ε              ∎

right-identity-unique : ∀ x y → x ∙ y ≈ x → y ≈ ε
right-identity-unique x y eq = begin
  y              ≈⟨ right-helper x y ⟩
  x ⁻¹ ∙ (x ∙ y) ≈⟨ refl ⟨ ∙-cong ⟩ eq ⟩
  x ⁻¹ ∙  x      ≈⟨ proj₁ inverse x ⟩
  ε              ∎

identity-unique : ∀ {x} → Identity x _∙_ → x ≈ ε
identity-unique {x} id = left-identity-unique x x (proj₂ id x)

left-inverse-unique : ∀ x y → x ∙ y ≈ ε → x ≈ y ⁻¹
left-inverse-unique x y eq = begin
  x              ≈⟨ left-helper x y ⟩
  (x ∙ y) ∙ y ⁻¹ ≈⟨ eq ⟨ ∙-cong ⟩ refl ⟩
       ε  ∙ y ⁻¹ ≈⟨ proj₁ identity (y ⁻¹) ⟩
            y ⁻¹ ∎

right-inverse-unique : ∀ x y → x ∙ y ≈ ε → y ≈ x ⁻¹
right-inverse-unique x y eq = begin
  y       ≈⟨ sym (⁻¹-involutive y) ⟩
  y ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong (sym (left-inverse-unique x y eq)) ⟩
  x ⁻¹    ∎


text:
record R (A B : Set) : Set where
  constructor c₁
  field
    x : A

mutual

  T : Set
  T = R D T

  data D : Set where
    c₂ : T → D

f : T → Set
f (c₁ (c₂ x)) = f x

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Auto.Core                  using (Rule; RuleName; _≟-RuleName_; name2rule; IsHintDB)
open import Level                      using (zero)
open import Function                   using (id; _∘_)
open import Category.Functor           using (module RawFunctor)
open import Data.Bool    as Bool       using (if_then_else_)
open import Data.List    as List       using (List; _++_; []; [_])
open import Data.Maybe   as Maybe      using (Maybe; just; nothing)
open import Data.Nat     as Nat        using (ℕ; pred)
open import Data.Product as Prod       using (∃; _,_; proj₂)
open import Data.Sum     as Sum        using (_⊎_; inj₁; inj₂)
open import Data.Unit    as Unit       using (⊤)
open import Reflection                 using (Name)
open import Relation.Nullary.Decidable using (⌊_⌋)

module Auto.Counting where

--------------------------------------------------------------------------------
-- Define a 'counting' hint database which, upon selection of a rule will     --
-- decrement an associated 'count' value, and upon reaching 0 will delete     --
-- the hint from the hint database.                                           --
--                                                                            --
-- The count values can either be natural numbers, in which case they         --
-- will be decremented as expected, or the value ⊤, in which case they        --
-- will not be decremented, effectively inserting infinite copies of the      --
-- rule into the hint database.                                               --
--------------------------------------------------------------------------------

module CountingHintDB where

  open RawFunctor (Maybe.functor {zero}) using (_<$>_)

  Count : Set
  Count = ℕ ⊎ ⊤

  record Hint (k : ℕ) : Set where
    constructor mkHint
    field
      rule  : Rule k
      count : Count

    ruleName : RuleName
    ruleName = Rule.name rule

  HintDB : Set
  HintDB = List (∃ Hint)

  decrCount : ∀ {k} → Hint k → Maybe (Hint k)
  decrCount {k} (mkHint r c) = mkHint r <$> decrCount′ c
    where
      decrCount′ : Count → Maybe Count
      decrCount′ (inj₁ 0) = nothing
      decrCount′ (inj₁ 1) = nothing
      decrCount′ (inj₁ x) = just (inj₁ (pred x))
      decrCount′ (inj₂ _) = just (inj₂ _)

  getTr : ∀ {k} → Hint k → (HintDB → HintDB)
  getTr h₁ = List.concatMap (List.fromMaybe ∘ mdecr₁)
    where
      mdecr₁ : ∃ Hint → Maybe (∃ Hint)
      mdecr₁ (_ , h₂) =
        if ⌊ Hint.ruleName h₁ ≟-RuleName Hint.ruleName h₂ ⌋
        then (_,_ _) <$> decrCount h₂
        else just (_ , h₂)

  countingHintDB : IsHintDB
  countingHintDB = record
    { HintDB   = HintDB
    ; Hint     = Hint
    ; getHints = id
    ; getRule  = Hint.rule
    ; getTr    = getTr
    ; ε        = []
    ; _∙_      = _++_
    ; return   = λ r → [ _ , mkHint r (inj₂ _) ]
    }

open CountingHintDB using (mkHint; countingHintDB)
open import Auto.Extensible countingHintDB public

--------------------------------------------------------------------------------
-- Define some new syntax in order to insert rules with limited usage.        --
--------------------------------------------------------------------------------

infixl 5 _<<[_]_

_<<[_]_ : HintDB → ℕ → Name → HintDB
db <<[ 0 ] _ = db
db <<[ x ] n with (name2rule n)
db <<[ x ] n | inj₁ msg     = db
db <<[ x ] n | inj₂ (k , r) = db ∙ [ k , mkHint r (inj₁ x) ]

max_stars_repo_name: wenkokke/AutoInAgda

max_issues_repo_name: wenkokke/AutoInAgda

max_forks_repo_name: wenkokke/AutoInAgda


text:
module Cats.Category.Setoids.Facts.Initial where

open import Data.Empty using (⊥)
open import Level

open import Cats.Category
open import Cats.Category.Setoids using (Setoids ; ≈-intro)

module Build {l} {l≈} where

  open Category (Setoids l l≈)

  Zero : Obj
  Zero = record
      { Carrier = Lift l ⊥
      ; _≈_ = λ()
      ; isEquivalence = record
          { refl = λ{}
          ; sym = λ{}
          ; trans = λ{}
          }
      }

  isInitial : IsInitial Zero
  isInitial X = ∃!-intro
      (record { arr = λ() ; resp = λ{} })
      _
      λ _ → ≈-intro λ {}

open Build

instance
  hasInitial : ∀ l l≈ → HasInitial (Setoids l l≈)
  hasInitial l l≈ = record
      { Zero = Zero
      ; isInitial = isInitial
      }

max_stars_repo_name: alessio-b-zak/cats

max_issues_repo_name: alessio-b-zak/cats

max_forks_repo_name: alessio-b-zak/cats


text:
module Generic.Lib.Data.Nat where

open import Data.Nat.Base hiding (_⊔_; _^_) public

open import Generic.Lib.Decidable

instance
  ℕEq : Eq ℕ
  ℕEq = viaBase Nat._≟_ where
    import Data.Nat as Nat

foldℕ : ∀ {α} {A : Set α} -> (A -> A) -> A -> ℕ -> A
foldℕ f x  0      = x
foldℕ f x (suc n) = f (foldℕ f x n)

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


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

module container.equality where

open import level
open import sum
open import equality.core
open import function.isomorphism
open import function.extensionality
open import container.core
open import container.fixpoint

module Equality {li la lb lx}
                (c : Container li la lb)
                (fp : Fixpoint c lx) where
  open Container c
  open Fixpoint fp

  substX : {i : I}{a a' : A i}(p : a ≡ a')(b : B a)
         → X (r (subst B p b)) → X (r b)
  substX refl _ x = x

  substX-β : ∀ {i} {a a' : A i}
             (f : (b : B a) → X (r b))
             (f' : (b : B a') → X (r b))
             (p : a ≡ a')
           → (subst (λ a → (b : B a) → X (r b)) p f ≡ f')
           ≅ ((b : B a) → f b ≡ substX p b (f' (subst B p b)))
  substX-β f f' refl = sym≅ strong-funext-iso

  -- structural equality for container fixpoints
  I-≡ : Set (li ⊔ lx)
  I-≡ = Σ I λ i → X i × X i

  A-≡ : I-≡ → Set la
  A-≡ (_ , u , v) = head u ≡ head v

  B-≡ : {j : I-≡} → A-≡ j → Set lb
  B-≡ {_ , u , _} _ = B (head u)

  r-≡ : {j : I-≡}{p : A-≡ j} → B-≡ p → I-≡
  r-≡ {i , u , v}{p} b = r b , tail u b , substX p b (tail v (subst B p b))

  equality : Container _ _ _
  equality = record
    { I = I-≡
    ; A = A-≡
    ; B = B-≡
    ; r = (λ {j p} → r-≡ {j} {p}) }

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text: module Issue2487.A where

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Class.Show where

open import Data.String using (String)

record Show {a} (A : Set a) : Set a where
  field
    show : A -> String

open Show {{...}} public

max_stars_repo_name: WhatisRT/meta-cedille

max_issues_repo_name: WhatisRT/meta-cedille

max_forks_repo_name: WhatisRT/meta-cedille


text:
postulate
  Nat : Set
  succ : Nat → Nat
  Le : Nat → Nat → Set
  Fin : Nat → Set
  low : ∀ {m n} → Le m n → Fin n → Fin m
  instance
    Le-refl : ∀ {n} → Le n n
    Le-succ : ∀ {m n} ⦃ _ : Le m n ⦄ → Le m (succ n)
  Chk1 : ∀ {n} → Fin n → Set
  Chk2 : ∀ {n} → Fin n → Fin n → Set
  Chk3 : ∀ {m n} ⦃ _ : Le m n ⦄ → Fin m → Fin n → Set

variable
  le : Le _ _
  X G : Fin _

postulate

  works : Chk1 G
        → Chk2 (low le G) X
        → Chk3 X G
  -- WAS: Instance argument got solved with `Le-refl`, which is not
  -- type-correct.
  -- SHOULD: result in a failed instance search

  fails : Chk2 (low le G) X
        → Chk3 X G


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.FinData.Properties where

open import Cubical.Foundations.Function
open import Cubical.Foundations.Prelude

open import Cubical.Data.FinData.Base as Fin
import Cubical.Data.Nat as ℕ
open import Cubical.Data.Empty as Empty
open import Cubical.Relation.Nullary

private
 variable
   ℓ : Level
   A : Type ℓ

znots : ∀{k} {m : Fin k} → ¬ (zero ≡ (suc m))
znots {k} {m} x = subst (Fin.rec (Fin k) ⊥) x m

snotz : ∀{k} {m : Fin k} → ¬ ((suc m) ≡ zero)
snotz {k} {m} x = subst (Fin.rec ⊥ (Fin k)) x m

isPropFin0 : isProp (Fin 0)
isPropFin0 = Empty.rec ∘ ¬Fin0

isContrFin1 : isContr (Fin 1)
isContrFin1 .fst = zero
isContrFin1 .snd zero = refl

injSucFin : ∀ {n} { p q : Fin n} → suc p ≡ suc q → p ≡ q
injSucFin {ℕ.suc ℕ.zero} {zero} {zero} pf = refl
injSucFin {ℕ.suc (ℕ.suc n)} pf = cong predFin pf

discreteFin : ∀{k} → Discrete (Fin k)
discreteFin zero zero = yes refl
discreteFin zero (suc y) = no znots
discreteFin (suc x) zero = no snotz
discreteFin (suc x) (suc y) with discreteFin x y
... | yes p = yes (cong suc p)
... | no ¬p = no (λ q → ¬p (injSucFin q))

isSetFin : ∀{k} → isSet (Fin k)
isSetFin = Discrete→isSet discreteFin

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Sandbox.IndRecIndexed where
-- Ornamental Algebras, Algebraic Ornaments, CONOR McBRIDE
-- https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/Ornament.pdf
-- A Finite Axiomtization of Inductive-Recursion definitions, Peter Dybjer, Anton Setzer
-- http://www.cse.chalmers.se/~peterd/papers/Finite_IR.pdf

open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Data.Bool
open import Data.Unit
open import Data.Empty
open import Function
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

data Desc (I : Set) : Set₁ where
    arg : (A : Set) → (A → Desc I) → Desc I
    rec : I → Desc I → Desc I
    ret : I → Desc I

⟦_⟧ : ∀ {I} → Desc I → (I → Set) → (I → Set)
⟦ arg A D ⟧ R i = Σ A (λ a → ⟦ D a ⟧ R i)
⟦ rec j D ⟧ R i = R j × ⟦ D ⟧ R i
⟦ ret j   ⟧ R i = j ≡ i

data Data {I} (D : Desc I) : I → Set where
    ⟨_⟩ : ∀ {i} → ⟦ D ⟧ (Data D) i → Data D i

-- an arrow that respects indices
_⇒_ : ∀ {I} → (I → Set) → (I → Set) → Set
_⇒_ {I} X Y = (i : I) → X i → Y i

map : ∀ {I} {A B : I → Set} → (D : Desc I) → (A ⇒ B) → ⟦ D ⟧ A ⇒ ⟦ D ⟧ B
map (arg T U) f i (t , u) = t     , map (U t) f i u
map (rec j D) f i (a , u) = f j a , map D     f i u
map (ret j)   f i i≡j     = i≡j

Alg : ∀ {I} (D : Desc I) → (A : I → Set) → Set
Alg D A = ⟦ D ⟧ A ⇒ A

-- fold D alg i ⟨ x ⟩ = alg i (map D (fold D alg) i x)
-- mapFold F G alg i x = map F (fold G alg) i x

mapFold : ∀ {I} {A : I → Set} (F G : Desc I) → Alg G A → ⟦ F ⟧ (Data G) ⇒ ⟦ F ⟧ A
mapFold (arg Tags decoder) G alg i (tag , subnode) = tag , (mapFold (decoder tag) G alg i subnode)
mapFold (rec j F)          G alg i (⟨ x ⟩ , xs) = alg j (mapFold G G alg j x) , mapFold F G alg i xs
mapFold (ret j)            G alg i x = x

fold : ∀ {I} {A : I → Set} (D : Desc I) → Alg D A → Data D ⇒ A
fold D alg i ⟨ x ⟩ = alg i (mapFold D D alg i x)

-- ℕ
ℕDesc : Desc ⊤
ℕDesc = arg Bool (λ { true → rec tt (ret tt) ; false → ret tt })

ℕ : Set
ℕ = Data ℕDesc tt

zero : ℕ
zero = ⟨ (false , refl) ⟩

suc : ℕ → ℕ
suc n = ⟨ (true , (n , refl)) ⟩

-- indℕ : (P : ℕ → Set)
--      → P zero
--      → ((n : ℕ) → P n → P (suc n))
--      → (x : ℕ)
--      → P x
-- indℕ P base step ⟨ true , n , refl ⟩ = step n (indℕ P base step n)
-- indℕ P base step ⟨ false , refl ⟩ = base
--
-- _+_ : ℕ → ℕ → ℕ
-- x + y = indℕ (λ _ → ℕ) y (λ n prf → suc prf) x

+alg : ℕ → Alg ℕDesc (λ _ → ℕ)
+alg y .tt (true , sum , refl) = suc sum
+alg y .tt (false , refl) = y

_+_ : ℕ → ℕ → ℕ
x + y = fold ℕDesc (+alg y) tt x

one : ℕ
one = suc zero

two : ℕ
two = suc one

+-suc-left : (m n : ℕ) → suc m + n ≡ suc (m + n)
+-suc-left ⟨ true , m , refl ⟩ n = refl
+-suc-left ⟨ false , refl ⟩ n = refl

-- Nat
NatDesc : Desc ℕ
NatDesc = arg Bool (
    λ { true → arg ℕ (λ { n → rec n (ret (suc n)) })
      ; false → ret zero
      })

Nat : ℕ → Set
Nat n = Data NatDesc n

zeroNat : Nat zero
zeroNat = ⟨ (false , refl) ⟩

sucNat : ∀ {n} → Nat n → Nat (suc n)
sucNat {n} x = ⟨ (true , (n , (x , refl))) ⟩

-- Maybe
MaybeDesc : Set → Desc ⊤
MaybeDesc A = arg Bool (λ { true → arg A (λ _ → ret tt) ; false → ret tt })

Maybe : Set → Set
Maybe A = Data (MaybeDesc A) tt

nothing : ∀ {A} → Maybe A
nothing = ⟨ (false , refl) ⟩

just : ∀ {A} → A → Maybe A
just n = ⟨ (true , (n , refl)) ⟩

-- List
ListDesc : Set → Desc ⊤
ListDesc A = arg Bool (
    λ { true  → arg A (λ _ → rec tt (ret tt))
      ; false → ret tt
      })

List : Set → Set
List A = Data (ListDesc A) tt

nil : ∀ {A} → List A
nil = ⟨ (false , refl) ⟩

cons : ∀ {A} → A → List A → List A
cons x xs = ⟨ (true , (x , (xs , refl))) ⟩

indList : ∀ {A} (P : List A → Set)
        → P nil
        → ((x : A) → (xs : List A) → P xs → P (cons x xs))
        → (xs : List A)
        → P xs
indList P base step ⟨ true , x , xs , refl ⟩ = step x xs (indList P base step xs)
indList P base step ⟨ false , refl ⟩ = base

-- Vec
VecDesc : Set → Desc ℕ
VecDesc A = arg Bool (
  λ { true → arg A (λ _ → arg ℕ (λ n → rec n (ret (suc n))))
    ; false → ret zero
    })

Vec : Set → ℕ → Set
Vec A n = Data (VecDesc A) n

nilV : ∀ {A} → Vec A zero
nilV = ⟨ false , refl ⟩

consV : ∀ {A n} → A → Vec A n → Vec A (suc n)
consV {A} {n} x xs = ⟨ true , x , n , xs , refl ⟩

++alg : ∀ {A n} → Vec A n → Alg (VecDesc A) (λ m → Vec A (m + n))
++alg {A} {n} ys .(suc o) (true , z , o , zs , refl) = ⟨ true , z , o + n , zs , sym (+-suc-left o n) ⟩
++alg ys .zero    (false , refl) = ys

_++_ : ∀ {A m n} → Vec A m → Vec A n → Vec A (m + n)
_++_ {A} {m} {n} xs ys = fold (VecDesc A) (++alg ys) m xs

-- inverse image of e : J → I
data Inv {J I : Set} (e : J → I) : I → Set where
    inv : (j : J) → Inv e (e j)

data Orn {J I : Set} (e : J → I) : Desc I → Set₁ where
    arg : (A : Set) → {D : A → Desc I} → ((a : A) → Orn e (D a)) → Orn e (Desc.arg A D)
    rec : ∀ {h D} → Inv e h → Orn e D → Orn e (rec h D)
    ret : ∀ {o} → Inv e o → Orn e (ret o)
    new : ∀ {D} → (A : Set) → ((a : A) → Orn e D) → Orn e D

ListOrn : Set → Orn (λ x → tt) ℕDesc
ListOrn A = arg Bool (λ { true → Orn.new A (λ a → rec (inv tt) (ret (inv tt)))
                        ; false → Orn.ret (inv tt)})

orn : ∀ {I J} {D : Desc I} {e : J → I} → Orn e D → Desc J
orn (arg A O)       = arg A (λ x → orn (O x))
orn (rec (inv j) O) = rec j (orn O)
orn (ret (inv j))   = ret j
orn (new A O)       = arg A (λ x → orn (O x))

ListDesc' : Set → Desc ⊤
ListDesc' A = orn (ListOrn A)

erase : ∀ {I J} {R : I → Set} {e : J → I} {D : Desc I} → (O : Orn e D) → ⟦ orn O ⟧ (R ∘ e) ⇒ (⟦ D ⟧ R ∘ e)
erase (arg A O) i (a , os) = a , (erase (O a) i os)
erase (rec (inv i) O) j (r , os) = r , erase O j os
erase (ret (inv j)) .j refl = refl
erase (new A O) j (a , os) = erase (O a) j os

ornament-algebra : ∀ {I J} {e : J → I} {D : Desc I} → (O : Orn e D) → Alg (orn O) (λ j → Data D (e j))
ornament-algebra O j x = ⟨ erase O j x ⟩

forget : ∀ {I J} {e : J → I} {D : Desc I} {O : Orn e D} {j : J} → Data (orn O) j → Data D (e j)
forget {I} {J} {e} {D} {O} {j} = fold (orn O) (ornament-algebra O) j

algo : ∀ {I A} → (D : Desc I) → Alg D A → Orn {Σ I {! A  !}} proj₁ D
algo (arg A x) alg = arg A (λ a → algo (x a) (λ j ds → alg j (a , ds)))
algo {I} {A} (rec i D) alg = new (A i) (λ a → rec (inv (i , a)) (algo D (λ j ds → alg i (a , {! ds  !}))))
algo (ret i) alg = ret (inv (i , alg i refl))

max_stars_repo_name: banacorn/numeral

max_issues_repo_name: banacorn/numeral

max_forks_repo_name: banacorn/numeral


text:
{-# OPTIONS --without-K #-}
open import Type using (Type₀; Type₁)
open import Type.Identities
open import Data.Zero using (𝟘)
open import Data.One using (𝟙; 0₁)
open import Data.Two.Base using (𝟚; 0₂; 1₂)
open import Data.Product.NP using (Σ; _×_)
open import Data.Sum.NP using (_⊎_)
open import Data.Nat.Base using (ℕ; zero; suc)
open import Data.Fin using (Fin)
open import Data.Vec using (Vec)
open import HoTT using (ua; UA; module Equivalences)
open import Relation.Binary.PropositionalEquality.NP using (_≡_; !_; _∙_; idp)
open        Equivalences using (_≃_; ≃-!; ≃-refl; _≃-∙_)

module Explore.Universe.Type {X : Type₀} where

infixr 2 _×ᵁ_

data U : Type₁
El : U → Type₀

data U where
  𝟘ᵁ 𝟙ᵁ 𝟚ᵁ : U
  _×ᵁ_ _⊎ᵁ_ : U → U → U
  Σᵁ : (u : U) (f : El u → U) → U
  Xᵁ : U
  ≃ᵁ : (u : U) (A : Type₀) (e : El u ≃ A) → U

El 𝟘ᵁ = 𝟘
El 𝟙ᵁ = 𝟙
El 𝟚ᵁ = 𝟚
El (u₀ ×ᵁ u₁) = El u₀ × El u₁
El (u₀ ⊎ᵁ u₁) = El u₀ ⊎ El u₁
El (Σᵁ u f) = Σ (El u) λ x → El (f x)
El Xᵁ = X
El (≃ᵁ u A e) = A

infix  8 _^ᵁ_
_^ᵁ_ : U → ℕ → U
u ^ᵁ zero  = 𝟙ᵁ
u ^ᵁ suc n = u ×ᵁ u ^ᵁ n

^ᵁ≃Vec : ∀ u n → El (u ^ᵁ n) ≃ Vec (El u) n
^ᵁ≃Vec u zero = ≃-! Vec0≃𝟙
^ᵁ≃Vec u (suc n) = ×≃-second (El u) (^ᵁ≃Vec u n) ≃-∙ ≃-! Vec∘suc≃×

^ᵁ≡Vec : ∀ {{_ : UA}} u n → El (u ^ᵁ n) ≡ Vec (El u) n
^ᵁ≡Vec u n = ua (^ᵁ≃Vec u n)

Finᵁ : ℕ → U
Finᵁ zero    = 𝟘ᵁ
Finᵁ (suc n) = 𝟙ᵁ ⊎ᵁ Finᵁ n

Finᵁ' : ℕ → U
Finᵁ' zero          = 𝟘ᵁ
Finᵁ' (suc zero)    = 𝟙ᵁ
Finᵁ' (suc (suc n)) = 𝟙ᵁ ⊎ᵁ Finᵁ' (suc n)

Finᵁ≃Fin : ∀ n → El (Finᵁ n) ≃ Fin n
Finᵁ≃Fin zero    = ≃-! Fin0≃𝟘
Finᵁ≃Fin (suc n) = ⊎≃ ≃-refl (Finᵁ≃Fin n) ≃-∙ ≃-! Fin∘suc≃𝟙⊎Fin

Finᵁ'≃Fin : ∀ n → El (Finᵁ' n) ≃ Fin n
Finᵁ'≃Fin zero          = ≃-! Fin0≃𝟘
Finᵁ'≃Fin (suc zero)    = ≃-! Fin1≃𝟙
Finᵁ'≃Fin (suc (suc n)) = ⊎≃ ≃-refl (Finᵁ'≃Fin (suc n)) ≃-∙ ≃-! Fin∘suc≃𝟙⊎Fin

max_stars_repo_name: crypto-agda/explore

max_issues_repo_name: crypto-agda/explore

max_forks_repo_name: crypto-agda/explore


text:
module Oscar.Property.Preservativity where

open import Oscar.Level
open import Oscar.Relation

record Preservativity
  {a} {A : Set a} {b} {B : A → Set b} {c} {C : (x : A) → B x → Set c}
    (_▻₁_ : (x : A) → (y : B x) → C x y)
  {d} {D : Set d} {e} {E : D → Set e} {f} {F : (x : D) → E x → Set f}
    (_▻₂_ : (x : D) → (y : E x) → F x y)
  {ℓ}
    (_≤_ : ∀ {x y} → F x y → F x y → Set ℓ)
    (◽ : A → D)
    (◻ : ∀ {x} → B x → E (◽ x))
    (□ : ∀ {x y} → C x y → F (◽ x) (◻ y))
  : Set (a ⊔ b ⊔ c ⊔ d ⊔ e ⊔ f ⊔ ℓ) where
  field
    preservativity : ∀ (x : A) (y : B x) → □ (x ▻₁ y) ≤ (◽ x ▻₂ ◻ y)

open Preservativity ⦃ … ⦄ public

-- -- record Preservativity
-- --   {𝔞₁} {𝔄₁ : Set 𝔞₁} {𝔰₁} {_►₁_ : 𝔄₁ → 𝔄₁ → Set 𝔰₁}
-- --     (_◅₁_ : ∀ {m n} → m ►₁ n → ∀ {l} → m ⟨ l ►₁_ ⟩→ n)
-- --   {𝔞₂} {𝔄₂ : Set 𝔞₂} {𝔰₂} (_►₂_ : 𝔄₂ → 𝔄₂ → Set 𝔰₂)
-- --     (_◅₂_ : ∀ {m n} → m ►₂ n → ∀ {l} → m ⟨ l ►₂_ ⟩→ n)
-- --   {ℓ}
-- --     (_≤_ : ∀ {m n} → m ►₂ n → m ►₂ n → Set ℓ)
-- --   {μ : 𝔄₁ → 𝔄₂}
-- --     (◽ : ∀ {m n} → m ►₁ n → μ m ►₂ μ n)
-- --   : Set (𝔞₁ ⊔ 𝔰₁ ⊔ 𝔞₂ ⊔ 𝔰₂ ⊔ ℓ) where
-- --   field
-- --     preservativity : ∀ {l m} (f : l ►₁ m) {n} (g : m ►₁ n) → ◽ (g ◅₁ f) ≤ (◽ g ◅₂ ◽ f)

-- -- open Preservativity ⦃ … ⦄ public

-- -- -- record Preservativity
-- -- --   {𝔞₁} {𝔄₁ : Set 𝔞₁} {𝔰₁}
-- -- --     (_►₁_ : 𝔄₁ → 𝔄₁ → Set 𝔰₁) {𝔱₁}
-- -- --   {▸₁ : 𝔄₁ → Set 𝔱₁}
-- -- --     (_◃₁_ : ∀ {m n} → m ►₁ n → m ⟨ ▸₁ ⟩→ n)
-- -- --   {𝔞₂} {𝔄₂ : Set 𝔞₂} {𝔰₂}
-- -- --     (_►₂_ : 𝔄₂ → 𝔄₂ → Set 𝔰₂) {𝔱₂}
-- -- --   {▸₂ : 𝔄₂ → Set 𝔱₂}
-- -- --     (_◃₂_ : ∀ {m n} → m ►₂ n → m ⟨ ▸₂ ⟩→ n)
-- -- --   {ℓ}
-- -- --     (_≤_ : ∀ {n} → ▸₂ n → ▸₂ n → Set ℓ)
-- -- --   {μ : 𝔄₁ → 𝔄₂}
-- -- --     (◽ : ∀ {n} → ▸₁ n → ▸₂ (μ n))
-- -- --     (□ : ∀ {m n} → m ►₁ n → μ m ►₂ μ n)
-- -- --   : Set (𝔞₁ ⊔ 𝔰₁ ⊔ 𝔱₁ ⊔ 𝔞₂ ⊔ 𝔰₂ ⊔ 𝔱₂ ⊔ ℓ) where
-- -- --   field
-- -- --     preservativity : ∀ {m n} (f : ▸₁ m) (g : m ►₁ n) → ◽ (g ◃₁ f) ≤ (□ g ◃₂ ◽ f)

-- -- -- open Preservativity ⦃ … ⦄ public

-- -- -- open import Oscar.Class.Associativity
-- -- -- open import Oscar.Class.Symmetry
-- -- -- open import Oscar.Function

-- -- -- instance

-- -- --   Preservativity⋆ : ∀
-- -- --     {𝔞} {𝔄 : Set 𝔞} {𝔰} {_►_ : 𝔄 → 𝔄 → Set 𝔰}
-- -- --       {_◅_ : ∀ {m n} → m ► n → ∀ {l} → m ⟨ l ►_ ⟩→ n}
-- -- --     {𝔱} {▸ : 𝔄 → Set 𝔱}
-- -- --       {_◃_ : ∀ {m n} → m ► n → m ⟨ ▸ ⟩→ n}
-- -- --     {ℓ}
-- -- --       {_≤_ : ∀ {n} → ▸ n → ▸ n → Set ℓ}
-- -- --     ⦃ _ : Associativity _◅_ _◃_ _≤_ ⦄
-- -- --     → ∀ {n} {x : ▸ n}
-- -- --     → Preservativity _►_ (λ ⋆ → _◅_ ⋆) _►_ _◃_ (flip _≤_) (_◃ x) id
-- -- --   Preservativity.preservativity (Preservativity⋆ {_◅_ = _◅_} {_◃_ = _◃_} {_≤_ = _≤_} ⦃ ′associativity ⦄ {x = x}) f = associativity {_◅_ = _◅_} {_◃_ = _◃_} {_≤_ = _≤_} ⦃ {-′associativity-}_ ⦄ x f

-- -- -- preservation : ∀
-- -- --   {𝔞₁} {𝔄₁ : Set 𝔞₁} {𝔰₁} {_►₁_ : 𝔄₁ → 𝔄₁ → Set 𝔰₁} {𝔱₁} {▸₁ : 𝔄₁ → Set 𝔱₁}
-- -- --     (_◃₁_ : ∀ {m n} → m ►₁ n → m ⟨ ▸₁ ⟩→ n)
-- -- --   {𝔞₂} {𝔄₂ : Set 𝔞₂} {𝔰₂} {_►₂_ : 𝔄₂ → 𝔄₂ → Set 𝔰₂} {𝔱₂} {▸₂ : 𝔄₂ → Set 𝔱₂}
-- -- --     (_◃₂_ : ∀ {m n} → m ►₂ n → m ⟨ ▸₂ ⟩→ n)
-- -- --   {ℓ}
-- -- --     (_≤_ : ∀ {n} → ▸₂ n → ▸₂ n → Set ℓ)
-- -- --   {μ : 𝔄₁ → 𝔄₂}
-- -- --   {◽ : ∀ {n} → ▸₁ n → ▸₂ (μ n)}
-- -- --   {□ : ∀ {m n} → m ►₁ n → μ m ►₂ μ n}
-- -- --   ⦃ _ : Preservativity _►₁_ _◃₁_ _►₂_ _◃₂_ _≤_ ◽ □ ⦄
-- -- --   {m n} (f : ▸₁ m) (g : m ►₁ n) → ◽ (g ◃₁ f) ≤ (□ g ◃₂ ◽ f)
-- -- -- preservation _◃₁_ _◃₂_ _≤_ f g = preservativity {_◃₁_ = _◃₁_} {_◃₂_ = _◃₂_} {_≤_ = _≤_} f g


text:
module Relation.Equality.Extensionality where

open import Relation.Equality
open import Data.Inductive.Higher.Interval
open import Relation.Path.Operation

funext : ∀ {a b}{A : Set a}{B : A → Set b}{f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g
funext {A = A}{B = B} {f = f}{g = g} p = ap {f = h} path-seg
  where
    h : I → (x : A) → B x
    h i x = interval-rec (f x) (g x) (p x) i

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
module Issue205 where

data ⊥ : Set where

data D : Set₁ where
  d : (Set → Set) → D

_*_ : D → Set → Set
d F * A = F A

foo : (F : D) → F * ⊥
foo (d _) = ⊥


text:
postulate
  A : Set
  P : ..(_ : A) → Set
  f : {x : A} → P x

g : ..(x : A) → P x
g x = f


text:
{-# OPTIONS --without-K --safe #-}
open import Level

open import Categories.Category

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

open import Function using (flip)
open import Relation.Binary hiding (_⇒_)
open import Relation.Binary.Construct.Closure.Transitive

open Category C

-- Defining the Path Category
∘-tc : {A B : Obj} → A [ _⇒_ ]⁺ B → A ⇒ B
∘-tc [ f ]            = f
∘-tc (_ ∼⁺⟨ f⁺ ⟩ f⁺′) = ∘-tc f⁺′ ∘ ∘-tc f⁺

infix 4 _≈⁺_
_≈⁺_ : {A B : Obj} → (i j : A [ _⇒_ ]⁺ B) → Set e
f⁺ ≈⁺ g⁺ = ∘-tc f⁺ ≈ ∘-tc g⁺

Path : Category o (o ⊔ ℓ) e
Path = record
  { Obj       = Obj
  ; _⇒_       = λ A B → A [ _⇒_ ]⁺ B
  ; _≈_       = _≈⁺_
  ; id        = [ id ]
  ; _∘_       = flip (_ ∼⁺⟨_⟩_)
  ; assoc     = assoc
  ; sym-assoc = sym-assoc
  ; identityˡ = identityˡ
  ; identityʳ = identityʳ
  ; identity² = identity²
  ; equiv     = record
    { refl  = refl
    ; sym   = sym
    ; trans = trans
    }
  ; ∘-resp-≈  = ∘-resp-≈
  }
  where open HomReasoning

max_stars_repo_name: MirceaS/agda-categories

max_issues_repo_name: MirceaS/agda-categories

max_forks_repo_name: MirceaS/agda-categories


text:
{-# OPTIONS --cubical #-}
module PathWithBoundary where

open import Agda.Builtin.Cubical.Path

open import Agda.Builtin.Nat

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

-- if the with abstraction correcly propagates the boundary the second
-- clause will not typecheck.
false : ∀ n {m} → (pred n + m) ≡ m
false n {m} i with pred n
... | zero  = m
... | suc q = m


text:
module Typing where

open import Data.Fin hiding (_≤_)
open import Data.List hiding (drop)
open import Data.List.All
open import Data.Maybe
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product

open import Relation.Binary.PropositionalEquality

-- linearity indicator
data LU : Set where
  LL UU : LU

data Dir : Set where
  SND RCV : Dir

-- coinductive view on session types
-- following "Interactive Programming in Agda"
-- http://www.cse.chalmers.se/~abela/ooAgda.pdf
mutual
  data Type : Set where
    TUnit TInt : Type
    TPair : Type → Type → Type
    TChan : STypeF SType → Type
    TFun  : LU → Type → Type → Type

  data STypeF (S : Set) : Set where
    transmit : (d : Dir) (t : Type) (s : S) → STypeF S
    choice : (d : Dir) (s1 : S) (s2 : S) → STypeF S
    choiceN : (d : Dir) (m : ℕ) (alt : Fin m → S) → STypeF S
    end : (d : Dir) → STypeF S

  record SType : Set where
    coinductive
    constructor delay
    field force : STypeF SType

open SType

pattern send t s = transmit SND t s
pattern recv t s = transmit RCV t s

pattern sintern s1 s2 = choice SND s1 s2
pattern sextern s1 s2 = choice RCV s1 s2

pattern sintN m a = choiceN SND m a
pattern sextN m a = choiceN RCV m a

pattern send! = end SND
pattern send? = end RCV

-- session type equivalence
data EquivF (R : SType → SType → Set) : STypeF SType → STypeF SType → Set where
  eq-send : ∀ {s1 s1'} → (t : Type) → R s1 s1' → EquivF R (send t s1) (send t s1')
  eq-recv : ∀ {s1 s1'} → (t : Type) → R s1 s1' → EquivF R (recv t s1) (recv t s1')
  eq-sintern : ∀ {s1 s1' s2 s2'} → R s1 s1' → R s2 s2' → EquivF R (sintern s1 s2) (sintern s1' s2')
  eq-sextern : ∀ {s1 s1' s2 s2'} → R s1 s1' → R s2 s2' → EquivF R (sextern s1 s2) (sextern s1' s2')
  eq-sintN : ∀ {m alt alt'} → ((i : Fin m) → R (alt i) (alt' i)) → EquivF R (sintN m alt) (sintN m alt')
  eq-sextN : ∀ {m alt alt'} → ((i : Fin m) → R (alt i) (alt' i)) → EquivF R (sextN m alt) (sextN m alt')
  eq-send! : EquivF R send! send!
  eq-send? : EquivF R send? send?

record Equiv (s1 : SType) (s2 : SType) : Set where
  coinductive
  field force : EquivF Equiv (force s1) (force s2)

open Equiv

_≈_ = Equiv
_≈'_ = EquivF Equiv

-- equivalence is reflexive
equivF-refl : ∀ s → s ≈' s
equiv-refl : ∀ s → s ≈ s

force (equiv-refl s) = equivF-refl (force s)

equivF-refl (send t s) = eq-send t (equiv-refl s)
equivF-refl (recv t s) = eq-recv t (equiv-refl s)
equivF-refl (sintern s1 s2) = eq-sintern (equiv-refl s1) (equiv-refl s2)
equivF-refl (sextern s1 s2) = eq-sextern (equiv-refl s1) (equiv-refl s2)
equivF-refl (sintN m alt) = eq-sintN λ i → equiv-refl (alt i)
equivF-refl (sextN m alt) = eq-sextN λ i → equiv-refl (alt i)
equivF-refl send! = eq-send!
equivF-refl send? = eq-send?

-- equivalence is symmetric

eqF-sym : ∀ {s1 s2} → s1 ≈' s2 → s2 ≈' s1
eq-sym : ∀ {s1 s2} → s1 ≈ s2 → s2 ≈ s1

eqF-sym (eq-send t x) = eq-send t (eq-sym x)
eqF-sym (eq-recv t x) = eq-recv t (eq-sym x)
eqF-sym (eq-sintern x x₁) = eq-sintern (eq-sym x) (eq-sym x₁)
eqF-sym (eq-sextern x x₁) = eq-sextern (eq-sym x) (eq-sym x₁)
eqF-sym (eq-sintN x) = eq-sintN λ i → eq-sym (x i)
eqF-sym (eq-sextN x) = eq-sextN λ i → eq-sym (x i)
eqF-sym eq-send! = eq-send!
eqF-sym eq-send? = eq-send?

force (eq-sym s1~s2) = eqF-sym (force s1~s2)

-- equivalence is transitive
equivF-trans : ∀ {s1 s2 s3} → EquivF Equiv s1 s2 → EquivF Equiv s2 s3 → EquivF Equiv s1 s3
equiv-trans : ∀ {s1 s2 s3} → Equiv s1 s2 → Equiv s2 s3 → Equiv s1 s3

force (equiv-trans s1~s2 s2~s3) = equivF-trans (force s1~s2) (force s2~s3)

equivF-trans (eq-send t x) (eq-send .t x₁) = eq-send t (equiv-trans x x₁)
equivF-trans (eq-recv t x) (eq-recv .t x₁) = eq-recv t (equiv-trans x x₁)
equivF-trans (eq-sintern x x₁) (eq-sintern x₂ x₃) = eq-sintern (equiv-trans x x₂) (equiv-trans x₁ x₃)
equivF-trans (eq-sextern x x₁) (eq-sextern x₂ x₃) = eq-sextern (equiv-trans x x₂) (equiv-trans x₁ x₃)
equivF-trans (eq-sintN x) (eq-sintN x₁) = eq-sintN λ i → equiv-trans (x i) (x₁ i)
equivF-trans (eq-sextN x) (eq-sextN x₁) = eq-sextN λ i → equiv-trans (x i) (x₁ i)
equivF-trans eq-send! eq-send! = eq-send!
equivF-trans eq-send? eq-send? = eq-send?

-- dual
dual-dir : Dir → Dir
dual-dir SND = RCV
dual-dir RCV = SND

dual : SType → SType
dualF : STypeF SType → STypeF SType

force (dual s) = dualF (force s)

dualF (transmit d t s) = transmit (dual-dir d) t (dual s)
dualF (choice d s1 s2) = choice (dual-dir d) (dual s1) (dual s2)
dualF (choiceN d m alt) = choiceN (dual-dir d) m λ i → dual (alt i)
dualF (end d) = end (dual-dir d)

-- properties

dual-involution : (s : SType) → s ≈ dual (dual s)
dual-involutionF : (s : STypeF SType) → s ≈' dualF (dualF s)

force (dual-involution s) = dual-involutionF (force s)

dual-involutionF (send t s) = eq-send t (dual-involution s)
dual-involutionF (recv t s) = eq-recv t (dual-involution s)
dual-involutionF (sintern s1 s2) = eq-sintern (dual-involution s1) (dual-involution s2)
dual-involutionF (sextern s1 s2) = eq-sextern (dual-involution s1) (dual-involution s2)
dual-involutionF (sintN m alt) = eq-sintN λ i → dual-involution (alt i)
dual-involutionF (sextN m alt) = eq-sextN λ i → dual-involution (alt i)
dual-involutionF send! = eq-send!
dual-involutionF send? = eq-send?

mutual
  -- subtyping
  data SubT : Type → Type → Set where
    sub-unit : SubT TUnit TUnit
    sub-int  : SubT TInt TInt
    sub-pair : ∀ {t₁ t₂ t₁' t₂'} → SubT t₁ t₁' → SubT t₂ t₂' → SubT (TPair t₁ t₂) (TPair t₁' t₂')
    sub-fun  : ∀ {t₁ t₂ t₁' t₂' lu} → SubT t₁' t₁ → SubT t₂ t₂' → SubT (TFun lu t₁ t₂) (TFun lu t₁' t₂')
    sub-chan : ∀ {s s'} → SubF Sub s s' → SubT (TChan s) (TChan s')

  -- session type subtyping
  data SubF (R : SType → SType → Set) : STypeF SType → STypeF SType → Set where
    sub-send : ∀ {s1 s1'} → (t t' : Type) → (t'<=t : SubT t' t) → (s1<=s1' : R s1 s1') → SubF R (send t s1) (send t' s1')
    sub-recv : ∀ {s1 s1'} → (t t' : Type) → (t<=t' : SubT t t') → (s1<=s1' : R s1 s1') → SubF R (recv t s1) (recv t' s1')
    sub-sintern : ∀ {s1 s1' s2 s2'} → (s1<=s1' : R s1 s1') → (s2<=s2' : R s2 s2') → SubF R (sintern s1 s2) (sintern s1' s2')
    sub-sextern : ∀ {s1 s1' s2 s2'} → (s1<=s1' : R s1 s1') → (s2<=s2' : R s2 s2') → SubF R (sextern s1 s2) (sextern s1' s2')
    sub-sintN : ∀ {m m' alt alt'} → (m'≤m : m' ≤ m) → ((i : Fin m') → R (alt (inject≤ i m'≤m)) (alt' i)) → SubF R (sintN m alt) (sintN m' alt')
    sub-sextN : ∀ {m m' alt alt'} → (m≤m' : m ≤ m') → ((i : Fin m) → R (alt i) (alt' (inject≤ i m≤m'))) → SubF R (sextN m alt) (sextN m' alt')
    sub-send! : SubF R send! send!
    sub-send? : SubF R send? send?

  record Sub (s1 : SType) (s2 : SType) : Set where
    coinductive
    field force : SubF Sub (force s1) (force s2)

open Sub

_≲_ = Sub
_≲'_ = SubF Sub

inject-refl : ∀ {m} → (i : Fin m) → inject≤ i ≤-refl ≡ i
inject-refl zero = refl
inject-refl (suc i) = cong suc (inject-refl i)

inject-trans : ∀ {m m' m''} → (m'≤m : m' ≤ m) → (m''≤m' : m'' ≤ m') → (i : Fin m'')
  → (inject≤ (inject≤ i m''≤m') m'≤m) ≡ (inject≤ i (≤-trans m''≤m' m'≤m))
inject-trans z≤n z≤n ()
inject-trans (s≤s m'≤m) z≤n ()
inject-trans (s≤s m'≤m) (s≤s m''≤m') zero = refl
inject-trans (s≤s m'≤m) (s≤s m''≤m') (suc i) = cong suc (inject-trans m'≤m m''≤m' i)

-- subtyping is reflexive
subt-refl : ∀ t → SubT t t
subF-refl : ∀ s → s ≲' s
sub-refl : ∀ s → s ≲ s

force (sub-refl s) = subF-refl (force s)

subF-refl (send t s) = sub-send t t (subt-refl t) (sub-refl s)
subF-refl (recv t s) = sub-recv t t (subt-refl t) (sub-refl s)
subF-refl (sintern s1 s2) = sub-sintern (sub-refl s1) (sub-refl s2)
subF-refl (sextern s1 s2) = sub-sextern (sub-refl s1) (sub-refl s2)
subF-refl (sintN m alt) = sub-sintN ≤-refl auxInt
  where
    auxInt : (i : Fin m) → Sub (alt (inject≤ i ≤-refl)) (alt i)
    auxInt i rewrite inject-refl i = sub-refl (alt i)
subF-refl (sextN m alt) = sub-sextN ≤-refl auxExt
  where
    auxExt : (i : Fin m) → Sub (alt i) (alt (inject≤ i ≤-refl))
    auxExt i rewrite inject-refl i = sub-refl (alt i)
subF-refl send! = sub-send!
subF-refl send? = sub-send?

subt-refl TUnit = sub-unit
subt-refl TInt = sub-int
subt-refl (TPair t t₁) = sub-pair (subt-refl t) (subt-refl t₁)
subt-refl (TChan s) = sub-chan (subF-refl s)
subt-refl (TFun x t t₁) = sub-fun (subt-refl t) (subt-refl t₁)

-- subtyping is transitive
subt-trans : ∀ {t1 t2 t3} → SubT t1 t2 → SubT t2 t3 → SubT t1 t3
sub-trans : ∀ {s1 s2 s3} → s1 ≲ s2 → s2 ≲ s3 → s1 ≲ s3
subF-trans : ∀ {s1 s2 s3} → s1 ≲' s2 → s2 ≲' s3 → s1 ≲' s3

subt-trans sub-unit sub-unit = sub-unit
subt-trans sub-int sub-int = sub-int
subt-trans (sub-pair t1<:t2 t1<:t3) (sub-pair t2<:t3 t2<:t4) = sub-pair (subt-trans t1<:t2 t2<:t3) (subt-trans t1<:t3 t2<:t4)
subt-trans (sub-fun t1<:t2 t1<:t3) (sub-fun t2<:t3 t2<:t4) = sub-fun (subt-trans t2<:t3 t1<:t2) (subt-trans t1<:t3 t2<:t4)
subt-trans (sub-chan s1<:s2) (sub-chan s2<:s3) = sub-chan (subF-trans s1<:s2 s2<:s3)

force (sub-trans s1<:s2 s2<:s3) = subF-trans (force s1<:s2) (force s2<:s3)

subF-trans (sub-send t t' x x₁) (sub-send .t' t'' x₂ x₃) = sub-send t t'' (subt-trans x₂ x) (sub-trans x₁ x₃)
subF-trans (sub-recv t t' x x₁) (sub-recv .t' t'' x₂ x₃) = sub-recv t t'' (subt-trans x x₂) (sub-trans x₁ x₃)
subF-trans (sub-sintern x x₁) (sub-sintern x₂ x₃) = sub-sintern (sub-trans x x₂) (sub-trans x₁ x₃)
subF-trans (sub-sextern x x₁) (sub-sextern x₂ x₃) = sub-sextern (sub-trans x x₂) (sub-trans x₁ x₃)
subF-trans {sintN m alt}{sintN m' alt'}{sintN m'' alt''} (sub-sintN m'≤m palt) (sub-sintN m''≤m' palt') =
  sub-sintN (≤-trans m''≤m' m'≤m) λ i → sub-trans (auxInt i) (palt' i)
  where
    auxInt : (i : Fin m'') → Sub (alt (inject≤ i (≤-trans m''≤m' m'≤m))) (alt' (inject≤ i m''≤m'))
    auxInt i with palt (inject≤ i m''≤m')
    ... | r rewrite (inject-trans  m'≤m m''≤m' i) = r
subF-trans {sextN m alt}{sextN m' alt'}{sextN m'' alt''} (sub-sextN m≤m' palt) (sub-sextN m'≤m'' palt') =
  sub-sextN (≤-trans m≤m' m'≤m'') λ i → sub-trans (palt i) (auxExt i)
  where
    auxExt : (i : Fin m) → Sub (alt' (inject≤ i m≤m')) (alt'' (inject≤ i (≤-trans m≤m' m'≤m'')))
    auxExt i with palt' (inject≤ i m≤m')
    ... | r rewrite (inject-trans m'≤m'' m≤m' i) = r
subF-trans sub-send! sub-send! = sub-send!
subF-trans sub-send? sub-send? = sub-send?

-- duality and subtyping
dual-sub : ∀ {s1 s2} → s1 ≲ s2 → dual s2 ≲ dual s1
dual-subF : ∀ {s1 s2} → s1 ≲' s2 → dualF s2 ≲' dualF s1

force (dual-sub s1<=s2) = dual-subF (force s1<=s2)

dual-subF (sub-send t t' t'<=t s1<=s1') = sub-recv t' t t'<=t (dual-sub s1<=s1')
dual-subF (sub-recv t t' t<=t' s1<=s1') = sub-send t' t t<=t' (dual-sub s1<=s1')
dual-subF (sub-sintern s1<=s1' s2<=s2') = sub-sextern (dual-sub s1<=s1') (dual-sub s2<=s2')
dual-subF (sub-sextern s1<=s1' s2<=s2') = sub-sintern (dual-sub s1<=s1') (dual-sub s2<=s2')
dual-subF (sub-sintN m'≤m x) = sub-sextN m'≤m λ i → dual-sub (x i)
dual-subF (sub-sextN m≤m' x) = sub-sintN m≤m' λ i → dual-sub (x i)
dual-subF sub-send! = sub-send?
dual-subF sub-send? = sub-send!

-- equivalence and subtyping
eq-implies-sub : ∀ {s1 s2} → s1 ≈ s2 → s1 ≲ s2
eqF-implies-subF : ∀ {s1 s2} → s1 ≈' s2 → s1 ≲' s2

force (eq-implies-sub s1~s2) = eqF-implies-subF (force s1~s2)

eqF-implies-subF (eq-send t x) = sub-send t t (subt-refl t) (eq-implies-sub x)
eqF-implies-subF (eq-recv t x) = sub-recv t t (subt-refl t) (eq-implies-sub x)
eqF-implies-subF (eq-sintern x x₁) = sub-sintern (eq-implies-sub x) (eq-implies-sub x₁)
eqF-implies-subF (eq-sextern x x₁) = sub-sextern (eq-implies-sub x) (eq-implies-sub x₁)
eqF-implies-subF {sintN m alt} {sintN .m alt'} (eq-sintN x) = sub-sintN ≤-refl auxInt
  where
    auxInt : (i : Fin m) → Sub (alt (inject≤ i ≤-refl)) (alt' i)
    auxInt i rewrite inject-refl i = eq-implies-sub (x i)
eqF-implies-subF {sextN m alt} {sextN .m alt'} (eq-sextN x) = sub-sextN ≤-refl auxExt
  where
    auxExt : (i : Fin m) → Sub (alt i) (alt' (inject≤ i ≤-refl))
    auxExt i rewrite inject-refl i = eq-implies-sub (x i)
eqF-implies-subF eq-send! = sub-send!
eqF-implies-subF eq-send? = sub-send?

-- unrestricted
data Unr : Type → Set where
  UUnit : Unr TUnit
  UInt : Unr TInt
  UPair : ∀ {t₁ t₂} → Unr t₁ → Unr t₂ → Unr (TPair t₁ t₂)
  UFun :  ∀ {t₁ t₂} → Unr (TFun UU t₁ t₂)

classify-type : (t : Type) → Maybe (Unr t)
classify-type TUnit = just UUnit
classify-type TInt = just UInt
classify-type (TPair t₁ t₂) with classify-type t₁ | classify-type t₂
classify-type (TPair t₁ t₂) | just x | just x₁ = just (UPair x x₁)
classify-type (TPair t₁ t₂) | just x | nothing = nothing
classify-type (TPair t₁ t₂) | nothing | just x = nothing
classify-type (TPair t₁ t₂) | nothing | nothing = nothing
classify-type (TChan x) = nothing
classify-type (TFun LL t₁ t₂) = nothing
classify-type (TFun UU t₁ t₂) = just UFun

TCtx = List Type

-- context splitting, respecting linearity
data Split : TCtx → TCtx → TCtx → Set where
  [] : Split [] [] []
  dupl : ∀ {t Φ Φ₁ Φ₂} → Unr t → Split Φ Φ₁ Φ₂ → Split (t ∷ Φ) (t ∷ Φ₁) (t ∷ Φ₂)
  drop : ∀ {t Φ Φ₁ Φ₂} → Unr t → Split Φ Φ₁ Φ₂ → Split (t ∷ Φ) Φ₁ Φ₂
  left : ∀ {t Φ Φ₁ Φ₂} → Split Φ Φ₁ Φ₂ → Split (t ∷ Φ) (t ∷ Φ₁) Φ₂
  rght : ∀ {t Φ Φ₁ Φ₂} → Split Φ Φ₁ Φ₂ → Split (t ∷ Φ) Φ₁ (t ∷ Φ₂)

-- split is symmetric
split-sym : ∀ {φ φ₁ φ₂} → Split φ φ₁ φ₂ → Split φ φ₂ φ₁
split-sym [] = []
split-sym (dupl x sp) = dupl x (split-sym sp)
split-sym (drop un-t sp) = drop un-t (split-sym sp)
split-sym (left sp) = rght (split-sym sp)
split-sym (rght sp) = left (split-sym sp)

split-unr : ∀ {φ φ₁ φ₂} → (sp : Split φ φ₁ φ₂) → All Unr φ₁ → All Unr φ₂ → All Unr φ
split-unr [] [] [] = []
split-unr (dupl x sp) (px ∷ unr1) (px₁ ∷ unr2) = px ∷ split-unr sp unr1 unr2
split-unr (drop x sp) unr1 unr2 = x ∷ split-unr sp unr1 unr2
split-unr (left sp) (px ∷ unr1) unr2 = px ∷ split-unr sp unr1 unr2
split-unr (rght sp) unr1 (px ∷ unr2) = px ∷ split-unr sp unr1 unr2

split-all-left : (φ : TCtx) → Split φ φ []
split-all-left [] = []
split-all-left (x ∷ φ) = left (split-all-left φ)

split-all-right : (φ : TCtx) → Split φ [] φ
split-all-right [] = []
split-all-right (x ∷ φ) = rght (split-all-right φ)

-- split the unrestricted part from a typing context
split-refl-left : (φ : TCtx) → ∃ λ φ' → All Unr φ' × Split φ φ φ'
split-refl-left [] = [] , [] , []
split-refl-left (t ∷ φ) with split-refl-left φ | classify-type t
split-refl-left (t ∷ φ) | φ' , unr-φ' , sp' | nothing = φ' , unr-φ' , left sp'
split-refl-left (t ∷ φ) | φ' , unr-φ' , sp' | just y = t ∷ φ' , y ∷ unr-φ' , dupl y sp'

split-all-unr : ∀ {φ} → All Unr φ → Split φ φ φ
split-all-unr [] = []
split-all-unr (px ∷ un-φ) = dupl px (split-all-unr un-φ)

split-from-disjoint : (φ₁ φ₂ : TCtx) → ∃ λ φ → Split φ φ₁ φ₂
split-from-disjoint [] φ₂ = φ₂ , split-all-right φ₂
split-from-disjoint (t ∷ φ₁) φ₂ with split-from-disjoint φ₁ φ₂
... | φ' , sp = t ∷ φ' , left sp

split-unr-right : ∀ {φ φ₁ φ₂ φ₃ φ₄}
  → Split φ φ₁ φ₂ → Split φ₁ φ₃ φ₄ → All Unr φ₂ → Split φ φ₃ φ₄
split-unr-right [] [] unr1 = []
split-unr-right (dupl x sp012) (dupl x₁ sp134) (px ∷ unr1) = dupl x₁ (split-unr-right sp012 sp134 unr1)
split-unr-right (dupl x sp012) (drop x₁ sp134) (px ∷ unr1) = drop px (split-unr-right sp012 sp134 unr1)
split-unr-right (dupl x sp012) (left sp134) (px ∷ unr1) = left (split-unr-right sp012 sp134 unr1)
split-unr-right (dupl x sp012) (rght sp134) (px ∷ unr1) = rght (split-unr-right sp012 sp134 unr1)
split-unr-right (drop x sp012) [] unr1 = drop x (split-unr-right sp012 [] unr1)
split-unr-right (drop x sp012) (dupl x₁ sp134) unr1 = drop x (split-unr-right sp012 (dupl x₁ sp134) unr1)
split-unr-right (drop x sp012) (drop x₁ sp134) unr1 = drop x (split-unr-right sp012 (drop x₁ sp134) unr1)
split-unr-right (drop x sp012) (left sp134) unr1 = drop x (split-unr-right sp012 (left sp134) unr1)
split-unr-right (drop x sp012) (rght sp134) unr1 = drop x (split-unr-right sp012 (rght sp134) unr1)
split-unr-right (left sp012) (dupl x sp134) unr1 = dupl x (split-unr-right sp012 sp134 unr1)
split-unr-right (left sp012) (drop x sp134) unr1 = drop x (split-unr-right sp012 sp134 unr1)
split-unr-right (left sp012) (left sp134) unr1 = left (split-unr-right sp012 sp134 unr1)
split-unr-right (left sp012) (rght sp134) unr1 = rght (split-unr-right sp012 sp134 unr1)
split-unr-right (rght sp012) [] (px ∷ unr1) = drop px (split-unr-right sp012 [] unr1)
split-unr-right (rght sp012) (dupl x sp134) (px ∷ unr1) = drop px (split-unr-right sp012 (dupl x sp134) unr1)
split-unr-right (rght sp012) (drop x sp134) (px ∷ unr1) = drop px (split-unr-right sp012 (drop x sp134) unr1)
split-unr-right (rght sp012) (left sp134) (px ∷ unr1) = drop px (split-unr-right sp012 (left sp134) unr1)
split-unr-right (rght sp012) (rght sp134) (px ∷ unr1) = drop px (split-unr-right sp012 (rght sp134) unr1)

split-unr-left : ∀ {φ φ₁ φ₂ φ₃ φ₄}
  → Split φ φ₁ φ₂ → Split φ₂ φ₃ φ₄ → All Unr φ₁ → Split φ φ₃ φ₄
split-unr-left [] [] [] = []
split-unr-left (dupl x sp012) (dupl x₁ sp234) (px ∷ unr1) = dupl px (split-unr-left sp012 sp234 unr1)
split-unr-left (dupl x sp012) (drop x₁ sp234) (px ∷ unr1) = drop px (split-unr-left sp012 sp234 unr1)
split-unr-left (dupl x sp012) (left sp234) (px ∷ unr1) = left (split-unr-left sp012 sp234 unr1)
split-unr-left (dupl x sp012) (rght sp234) (px ∷ unr1) = rght (split-unr-left sp012 sp234 unr1)
split-unr-left (drop x₁ sp012) [] unr1 = drop x₁ (split-unr-left sp012 [] unr1)
split-unr-left (drop x₁ sp012) (dupl x₂ sp234) unr1 = drop x₁ (split-unr-left sp012 (dupl x₂ sp234) unr1)
split-unr-left (drop x₁ sp012) (drop x₂ sp234) unr1 = drop x₁ (split-unr-left sp012 (drop x₂ sp234) unr1)
split-unr-left (drop x₁ sp012) (left sp234) unr1 = drop x₁ (split-unr-left sp012 (left sp234) unr1)
split-unr-left (drop x₁ sp012) (rght sp234) unr1 = drop x₁ (split-unr-left sp012 (rght sp234) unr1)
split-unr-left (left sp012) [] (px ∷ unr1) = drop px (split-unr-left sp012 [] unr1)
split-unr-left (left sp012) (dupl x sp234) (px ∷ unr1) = drop px (split-unr-left sp012 (dupl x sp234) unr1)
split-unr-left (left sp012) (drop x sp234) (px ∷ unr1) = drop px (split-unr-left sp012 (drop x sp234) unr1)
split-unr-left (left sp012) (left sp234) (px ∷ unr1) = drop px (split-unr-left sp012 (left sp234) unr1)
split-unr-left (left sp012) (rght sp234) (px ∷ unr1) = drop px (split-unr-left sp012 (rght sp234) unr1)
split-unr-left (rght sp012) (dupl x₁ sp234) unr1 = dupl x₁ (split-unr-left sp012 sp234 unr1)
split-unr-left (rght sp012) (drop x₁ sp234) unr1 = drop x₁ (split-unr-left sp012 sp234 unr1)
split-unr-left (rght sp012) (left sp234) unr1 = left (split-unr-left sp012 sp234 unr1)
split-unr-left (rght sp012) (rght sp234) unr1 = rght (split-unr-left sp012 sp234 unr1)

-- reorganize splits
split-rotate : ∀ {φ φ₁ φ₂ φ₁₁ φ₁₂}
  → Split φ φ₁ φ₂ → Split φ₁ φ₁₁ φ₁₂ → ∃ λ φ' → Split φ φ₁₁ φ' × Split φ' φ₁₂ φ₂
split-rotate [] [] = [] , [] , []
split-rotate (drop x sp12) [] with split-rotate sp12 []
... | φ' , sp-φ' , φ'-sp =  _ ∷ φ' , rght sp-φ' , drop x φ'-sp
split-rotate (dupl x sp12) (dupl x₁ sp1112) with split-rotate sp12 sp1112
... | φ' , sp-φ' , φ'-sp = _ ∷ φ' , dupl x₁ sp-φ' , dupl x₁ φ'-sp
split-rotate (dupl x sp12) (drop x₁ sp1112) with split-rotate sp12 sp1112
... | φ' , sp-φ' , φ'-sp = _ ∷ φ' , rght sp-φ' , rght φ'-sp
split-rotate (dupl x sp12) (left sp1112) with split-rotate sp12 sp1112
... | φ' , sp-φ' , φ'-sp = _ ∷ φ' , dupl x sp-φ' , rght φ'-sp
split-rotate (dupl x sp12) (rght sp1112) with split-rotate sp12 sp1112
... | φ' , sp-φ' , φ'-sp = _ ∷ φ' , rght sp-φ' , dupl x φ'-sp
split-rotate (drop px sp12) sp1112 with split-rotate sp12 sp1112
... | φ' , sp-φ' , φ'-sp = _ ∷ φ' , rght sp-φ' , drop px φ'-sp
split-rotate (left sp12) (dupl x₁ sp1112) with split-rotate sp12 sp1112
... | φ' , sp-φ' , φ'-sp = _ ∷ φ' , dupl x₁ sp-φ' , left φ'-sp
split-rotate (left sp12) (left sp1112) with split-rotate sp12 sp1112
... | φ' , sp-φ' , φ'-sp = φ' , left sp-φ' , φ'-sp
split-rotate (left sp12) (rght sp1112) with split-rotate sp12 sp1112
... | φ' , sp-φ' , φ'-sp = _ ∷ φ' , rght sp-φ' , left φ'-sp
split-rotate (left sp12) (drop px sp1112) with split-rotate sp12 sp1112
... | φ' , sp-φ' , φ'-sp = φ' , drop px sp-φ' , φ'-sp
split-rotate (rght sp12) sp1112 with split-rotate sp12 sp1112
... | φ' , sp-φ' , φ'-sp = _ ∷ φ' , rght sp-φ' , rght φ'-sp

-- extract from type context where all other entries are unrestricted
data _∈_ (x : Type) : List Type → Set where
  here  : ∀ { xs } → All Unr xs → x ∈ (x ∷ xs)
  there : ∀ { x₀ xs } → Unr x₀ → x ∈ xs → x ∈ (x₀ ∷ xs)

-- unrestricted weakening
unr-weaken-var : ∀ {Φ Φ₁ Φ₂ t} → Split Φ Φ₁ Φ₂ → All Unr Φ₂ → t ∈ Φ₁ → t ∈ Φ
unr-weaken-var [] un-Φ₂ ()
unr-weaken-var (dupl x₁ sp) (_ ∷ un-Φ₂) (here x) = here (split-unr sp x un-Φ₂)
unr-weaken-var (dupl x₁ sp) un-Φ₂ (there x x₂) = unr-weaken-var (rght sp) un-Φ₂ x₂
unr-weaken-var (drop un-t sp) un-Φ₂ x = there un-t (unr-weaken-var sp un-Φ₂ x)
unr-weaken-var {t = _} (left sp) un-Φ₂ (here x) = here (split-unr sp x un-Φ₂)
unr-weaken-var {t = t} (left sp) un-Φ₂ (there x x₁) = there x (unr-weaken-var sp un-Φ₂ x₁)
unr-weaken-var {t = t} (rght sp) (unr-t ∷ un-Φ₂) (here x) = there unr-t (unr-weaken-var sp un-Φ₂ (here x))
unr-weaken-var {t = t} (rght sp) (unr-t ∷ un-Φ₂) (there x x₁) = there unr-t (unr-weaken-var sp un-Φ₂ (there x x₁))

-- left and right branching
data Selector : Set where
  Left Right : Selector

selection : ∀ {A : Set} → Selector → A → A → A
selection Left x y = x
selection Right x y = y

max_stars_repo_name: peterthiemann/definitional-session

max_issues_repo_name: peterthiemann/definitional-session

max_forks_repo_name: peterthiemann/definitional-session


text:
open import Level using () renaming (zero to ℓ₀)
open import Relation.Binary using (DecSetoid)

module CheckInsert (A : DecSetoid ℓ₀ ℓ₀) where

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)
open import Data.Fin.Properties using (_≟_)
open import Data.Maybe using (Maybe ; nothing ; just) renaming (setoid to MaybeSetoid ; Eq to MaybeEq)
open import Data.Vec using (Vec) renaming (_∷_ to _∷V_)
open import Data.Vec.Equality using () renaming (module Equality to VecEq)
open import Relation.Nullary using (Dec ; yes ; no ; ¬_)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary using (Setoid ; module DecSetoid)
open import Relation.Binary.Core using (refl ; _≡_ ; _≢_)
import Relation.Binary.EqReasoning as EqR
open import Relation.Binary.PropositionalEquality using (cong ; sym ; inspect ; [_] ; trans)

open import FinMap

private
  open module A = DecSetoid A using (Carrier ; _≈_) renaming (_≟_ to deq)

checkInsert : {n : ℕ} → Fin n → Carrier → FinMapMaybe n Carrier → Maybe (FinMapMaybe n Carrier)
checkInsert i b m with lookupM i m
...               | nothing = just (insert i b m)
...               | just c with deq b c
...                         | yes b≈c = just m
...                         | no b≉c  = nothing

data InsertionResult {n : ℕ} (i : Fin n) (x : Carrier) (h : FinMapMaybe n Carrier) : Maybe (FinMapMaybe n Carrier) → Set where
  same : (x' : Carrier) → x ≈ x' → lookupM i h ≡ just x' → InsertionResult i x h (just h)
  new : lookupM i h ≡ nothing → InsertionResult i x h (just (insert i x h))
  wrong : (x' : Carrier) → ¬ (x ≈ x') → lookupM i h ≡ just x' → InsertionResult i x h nothing

insertionresult : {n : ℕ} → (i : Fin n) → (x : Carrier) → (h : FinMapMaybe n Carrier) → InsertionResult i x h (checkInsert i x h)
insertionresult i x h with lookupM i h | inspect (lookupM i) h
insertionresult i x h | just x' | _ with deq x x'
insertionresult i x h | just x' | [ il ] | yes x≈x' = same x' x≈x' il
insertionresult i x h | just x' | [ il ] | no x≉x' = wrong x' x≉x' il
insertionresult i x h | nothing | [ il ] = new il

lemma-checkInsert-same : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ just x → checkInsert i x m ≡ just m
lemma-checkInsert-same i x m p with lookupM i m
lemma-checkInsert-same i x m refl | .(just x) with deq x x
lemma-checkInsert-same i x m refl | .(just x) | yes x≈x = refl
lemma-checkInsert-same i x m refl | .(just x) | no x≉x = contradiction A.refl x≉x

lemma-checkInsert-new : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → lookupM i m ≡ nothing → checkInsert i x m ≡ just (insert i x m)
lemma-checkInsert-new i x m p with lookupM i m
lemma-checkInsert-new i x m refl | .nothing = refl

lemma-checkInsert-wrong : {n : ℕ} → (i : Fin n) → (x : Carrier) → (m : FinMapMaybe n Carrier) → (x' : Carrier) → ¬ (x ≈ x') → lookupM i m ≡ just x' → checkInsert i x m ≡ nothing
lemma-checkInsert-wrong i x m x' d p with lookupM i m
lemma-checkInsert-wrong i x m x' d refl | .(just x') with deq x x'
lemma-checkInsert-wrong i x m x' d refl | .(just x') | yes q = contradiction q d
lemma-checkInsert-wrong i x m x' d refl | .(just x') | no ¬q = refl

lemma-checkInsert-restrict : {n m : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : Vec (Fin n) m) → checkInsert i (f i) (restrict f is) ≡ just (restrict f (i ∷V is))
lemma-checkInsert-restrict f i is with checkInsert i (f i) (restrict f is) | insertionresult i (f i) (restrict f is)
lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = cong just (lemma-insert-same _ i (trans p (cong just (sym (lemma-lookupM-restrict i f is p)))))
lemma-checkInsert-restrict f i is | ._ | new _ = refl
lemma-checkInsert-restrict f i is | ._ | wrong x fi≉x p = contradiction (Setoid.reflexive A.setoid (lemma-lookupM-restrict i f is p)) fi≉x

lemma-lookupM-checkInsert : {n : ℕ} → (i j : Fin n) → (h : FinMapMaybe n Carrier) → {x : Carrier} → lookupM i h ≡ just x → (y : Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert j y h ≡ just h' → lookupM i h' ≡ just x
lemma-lookupM-checkInsert i j h pl y ph' with checkInsert j y h | insertionresult j y h
lemma-lookupM-checkInsert i j h pl y refl | ._ | same _ _ _ = pl
lemma-lookupM-checkInsert i j h pl y ph'  | ._ | new _ with i ≟ j
lemma-lookupM-checkInsert i .i h pl y ph' | ._ | new pl' | yes refl = contradiction (trans (sym pl) pl') (λ ())
lemma-lookupM-checkInsert i j h {x} pl y refl | ._ | new _ | no i≢j = begin
  lookupM i (insert j y h)
    ≡⟨ lemma-lookupM-insert-other i j y h i≢j ⟩
  lookupM i h
    ≡⟨ pl ⟩
  just x ∎
  where open Relation.Binary.PropositionalEquality.≡-Reasoning

lemma-lookupM-checkInsert i j h pl y () | ._ | wrong _ _ _

lemma-lookupM-checkInsert-other : {n : ℕ} → (i j : Fin n) → i ≢ j → (x : Carrier) → (h : FinMapMaybe n Carrier) → {h' : FinMapMaybe n Carrier} → checkInsert j x h ≡ just h' → lookupM i h' ≡ lookupM i h
lemma-lookupM-checkInsert-other i j i≢j x h ph' with lookupM j h
lemma-lookupM-checkInsert-other i j i≢j x h ph' | just y with deq x y
lemma-lookupM-checkInsert-other i j i≢j x h refl | just y | yes x≈y = refl
lemma-lookupM-checkInsert-other i j i≢j x h () | just y | no x≉y
lemma-lookupM-checkInsert-other i j i≢j x h refl | nothing = lemma-lookupM-insert-other i j x h i≢j

max_stars_repo_name: jvoigtlaender/bidiragda

max_issues_repo_name: jvoigtlaender/bidiragda

max_forks_repo_name: jvoigtlaender/bidiragda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of First
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.First.Properties where

open import Data.Empty
open import Data.Fin using (suc)
open import Data.List.Base as List using (List; []; _∷_)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any as Any using (here; there)
open import Data.List.Relation.Unary.First
import Data.Sum as Sum
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl; _≗_)
open import Relation.Unary
open import Relation.Nullary.Negation

------------------------------------------------------------------------
-- map

module _ {a b p q} {A : Set a} {B : Set b} {P : Pred B p} {Q : Pred B q} where

  map⁺ : {f : A → B} → First (P ∘′ f) (Q ∘′ f) ⊆ First P Q ∘′ List.map f
  map⁺ [ qfx ]        = [ qfx ]
  map⁺ (pfxs ∷ pqfxs) = pfxs ∷ map⁺ pqfxs

  map⁻ : {f : A → B} → First P Q ∘′ List.map f ⊆ First (P ∘′ f) (Q ∘′ f)
  map⁻ {f} {[]}     ()
  map⁻ {f} {x ∷ xs} [ qfx ]       = [ qfx ]
  map⁻ {f} {x ∷ xs} (pfx ∷ pqfxs) = pfx ∷ map⁻ pqfxs

------------------------------------------------------------------------
-- (++)

module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where

  ++⁺ : ∀ {xs ys} → All P xs → First P Q ys → First P Q (xs List.++ ys)
  ++⁺ []         pqys = pqys
  ++⁺ (px ∷ pxs) pqys = px ∷ ++⁺ pxs pqys

  ⁺++ : ∀ {xs} → First P Q xs → ∀ ys → First P Q (xs List.++ ys)
  ⁺++ [ qx ]      ys = [ qx ]
  ⁺++ (px ∷ pqxs) ys = px ∷ ⁺++ pqxs ys

------------------------------------------------------------------------
-- Relationship to All

module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where

  All⇒¬First : P ⊆ ∁ Q → All P ⊆ ∁ (First P Q)
  All⇒¬First p⇒¬q []         ()
  All⇒¬First p⇒¬q (px ∷ pxs) [ qx ]   = ⊥-elim (p⇒¬q px qx)
  All⇒¬First p⇒¬q (_ ∷ pxs)  (_ ∷ hf) = All⇒¬First p⇒¬q pxs hf

  First⇒¬All : Q ⊆ ∁ P → First P Q ⊆ ∁ (All P)
  First⇒¬All q⇒¬p [ qx ]     (px ∷ pxs) = q⇒¬p qx px
  First⇒¬All q⇒¬p (_ ∷ pqxs) (_ ∷ pxs)  = First⇒¬All q⇒¬p pqxs pxs

------------------------------------------------------------------------
-- Irrelevance

  unique-index : ∀ {xs} → P ⊆ ∁ Q → (f₁ f₂ : First P Q xs) → index f₁ ≡ index f₂
  unique-index p⇒¬q [ _ ]    [ _ ]    = refl
  unique-index p⇒¬q [ qx ]   (px ∷ _) = ⊥-elim (p⇒¬q px qx)
  unique-index p⇒¬q (px ∷ _) [ qx ]   = ⊥-elim (p⇒¬q px qx)
  unique-index p⇒¬q (_ ∷ f₁) (_ ∷ f₂) = P.cong suc (unique-index p⇒¬q f₁ f₂)

  irrelevant : P ⊆ ∁ Q → Irrelevant P → Irrelevant Q → Irrelevant (First P Q)
  irrelevant p⇒¬q p-irr q-irr [ qx₁ ]    [ qx₂ ]    = P.cong [_] (q-irr qx₁ qx₂)
  irrelevant p⇒¬q p-irr q-irr [ qx₁ ]    (px₂ ∷ f₂) = ⊥-elim (p⇒¬q px₂ qx₁)
  irrelevant p⇒¬q p-irr q-irr (px₁ ∷ f₁) [ qx₂ ]    = ⊥-elim (p⇒¬q px₁ qx₂)
  irrelevant p⇒¬q p-irr q-irr (px₁ ∷ f₁) (px₂ ∷ f₂) =
    P.cong₂ _∷_ (p-irr px₁ px₂) (irrelevant p⇒¬q p-irr q-irr f₁ f₂)

------------------------------------------------------------------------
-- Decidability

module _ {a p} {A : Set a} {P : Pred A p} where

  first? : Decidable P → Decidable (First P (∁ P))
  first? P? xs = Sum.toDec
               $ Sum.map₂ (All⇒¬First contradiction)
               $ first (Sum.fromDec ∘ P?) xs

------------------------------------------------------------------------
-- Conversion to Any

module _ {a p} {A : Set a} {P : Pred A p} where

  fromAny∘toAny≗id : ∀ {xs} → fromAny {Q = P} {x = xs} ∘′ toAny ≗ id
  fromAny∘toAny≗id [ qx ]      = refl
  fromAny∘toAny≗id (px ∷ pqxs) = P.cong (_ ∷_) (fromAny∘toAny≗id pqxs)

  toAny∘fromAny≗id : ∀ {xs} → toAny {Q = P} ∘′ fromAny {x = xs} ≗ id
  toAny∘fromAny≗id (here px) = refl
  toAny∘fromAny≗id (there v) = P.cong there (toAny∘fromAny≗id v)

------------------------------------------------------------------------
-- Equivalence between the inductive definition and the view

module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where

  toView : ∀ {as} → First P Q as → FirstView P Q as
  toView [ qx ] = [] ++ qx ∷ _
  toView (px ∷ pqxs) with toView pqxs
  ... | pxs ++  qy ∷ ys = (px ∷ pxs) ++ qy ∷ ys

  fromView : ∀ {as} → FirstView P Q as → First P Q as
  fromView (pxs ++ qy ∷ ys) = ++⁺ pxs [ qy ]


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

open import Sets.EquivalenceRelations
open import Functions.Definition
open import Agda.Primitive using (Level; lzero; lsuc; _⊔_; Setω)
open import Setoids.Setoids
open import Groups.Definition
open import LogicalFormulae
open import Orders.WellFounded.Definition
open import Numbers.Naturals.Semiring
open import Groups.Lemmas

module Groups.FreeProduct.Setoid {i : _} {I : Set i} (decidableIndex : (x y : I) → ((x ≡ y) || ((x ≡ y) → False))) {a b : _} {A : I → Set a} {S : (i : I) → Setoid {a} {b} (A i)} {_+_ : (i : I) → (A i) → (A i) → A i} (decidableGroups : (i : I) → (x y : A i) → ((Setoid._∼_ (S i) x y)) || ((Setoid._∼_ (S i) x y) → False)) (G : (i : I) → Group (S i) (_+_ i)) where

open import Groups.FreeProduct.Definition decidableIndex decidableGroups G

=RP' : {m n : _} (s1 : ReducedSequenceBeginningWith m) (s2 : ReducedSequenceBeginningWith n) → Set b
=RP' (ofEmpty i g nonZero) (ofEmpty j h nonZero₁) with decidableIndex i j
=RP' (ofEmpty i g nonZero) (ofEmpty .i h nonZero₁) | inl refl = Setoid._∼_ (S i) g h
=RP' (ofEmpty i g nonZero) (ofEmpty j h nonZero₁) | inr x = False'
=RP' (ofEmpty i g nonZero) (prependLetter i₁ g₁ nonZero₁ s2 x) = False'
=RP' (prependLetter i g nonZero s1 x) (ofEmpty i₁ g₁ nonZero₁) = False'
=RP' (prependLetter i g nonZero s1 x) (prependLetter j h nonZero₁ s2 x₁) with decidableIndex i j
=RP' (prependLetter i g nonZero s1 x) (prependLetter .i h nonZero₁ s2 x₁) | inl refl = Setoid._∼_ (S i) g h && =RP' s1 s2
=RP' (prependLetter i g nonZero s1 x) (prependLetter j h nonZero₁ s2 x₁) | inr x₂ = False'

_=RP_ : Rel ReducedSequence
empty =RP empty = True'
empty =RP nonempty i x = False'
nonempty i x =RP empty = False'
nonempty i x =RP nonempty j y = =RP' x y

=RP'reflex : {i : _} (x : ReducedSequenceBeginningWith i) → =RP' x x
=RP'reflex (ofEmpty i g nonZero) with decidableIndex i i
=RP'reflex (ofEmpty i g nonZero) | inl refl = Equivalence.reflexive (Setoid.eq (S i))
=RP'reflex (ofEmpty i g nonZero) | inr x = exFalso (x refl)
=RP'reflex (prependLetter i g nonZero x x₁) with decidableIndex i i
=RP'reflex (prependLetter i g nonZero x x₁) | inl refl = Equivalence.reflexive (Setoid.eq (S i)) ,, =RP'reflex x
=RP'reflex (prependLetter i g nonZero x x₁) | inr bad = exFalso (bad refl)

private
  reflex : Reflexive _=RP_
  reflex {empty} = record {}
  reflex {nonempty i (ofEmpty .i g nonZero)} with decidableIndex i i
  reflex {nonempty i (ofEmpty .i g nonZero)} | inl refl = Equivalence.reflexive (Setoid.eq (S i))
  ... | inr bad = exFalso (bad refl)
  reflex {nonempty i (prependLetter .i g nonZero x x₁)} with decidableIndex i i
  reflex {nonempty i (prependLetter .i g nonZero x x₁)} | inl refl = Equivalence.reflexive (Setoid.eq (S i)) ,, =RP'reflex x
  reflex {nonempty i (prependLetter .i g nonZero x x₁)} | inr bad = exFalso (bad refl)

=RP'symm : {i j : _} (x : ReducedSequenceBeginningWith i) (y : ReducedSequenceBeginningWith j) → =RP' x y → =RP' y x
=RP'symm (ofEmpty i g nonZero) (ofEmpty j h nonZero2) with decidableIndex i j
=RP'symm (ofEmpty i g nonZero) (ofEmpty j h nonZero2) | inl pr with decidableIndex j i
=RP'symm (ofEmpty .j g nonZero) (ofEmpty j h nonZero2) | inl refl | inl refl = Equivalence.symmetric (Setoid.eq (S j)) {g} {h}
=RP'symm (ofEmpty i g nonZero) (ofEmpty j h nonZero2) | inl pr | inr x = exFalso (x (equalityCommutative pr))
=RP'symm (ofEmpty i g nonZero) (ofEmpty j h nonZero2) | inr x with decidableIndex j i
=RP'symm (ofEmpty i g nonZero) (ofEmpty j h nonZero2) | inr x | inl pr = exFalso (x (equalityCommutative pr))
=RP'symm (ofEmpty i g nonZero) (ofEmpty j h nonZero2) | inr x | inr _ = id
=RP'symm (ofEmpty i g nonZero) (prependLetter i₁ g₁ nonZero₁ y x) = id
=RP'symm (prependLetter i g nonZero x x₁) (ofEmpty i₁ g₁ nonZero₁) = id
=RP'symm (prependLetter i g nonZero x x₁) (prependLetter j h nonZero2 y pr2) pr with decidableIndex i j
=RP'symm (prependLetter .j g nonZero x x₁) (prependLetter j h nonZero2 y pr2) pr | inl refl with decidableIndex j j
=RP'symm (prependLetter .j g nonZero x x₁) (prependLetter j h nonZero2 y pr2) (fst ,, snd) | inl refl | inl refl = Equivalence.symmetric (Setoid.eq (S j)) fst ,, =RP'symm x y snd
=RP'symm (prependLetter .j g nonZero x x₁) (prependLetter j h nonZero2 y pr2) pr | inl refl | inr bad = exFalso (bad refl)
=RP'symm (prependLetter i g nonZero x x₁) (prependLetter j h nonZero2 y pr2) () | inr i!=j

private
  symm : Symmetric _=RP_
  symm {empty} {empty} x = record {}
  symm {nonempty i m} {nonempty i₁ n} x = =RP'symm m n x

=RP'trans : {i j k : _} (x : ReducedSequenceBeginningWith i) (y : ReducedSequenceBeginningWith j) (z : ReducedSequenceBeginningWith k) → =RP' x y → =RP' y z → =RP' x z
=RP'trans (ofEmpty i g nonZero) (ofEmpty j g₁ nonZero₁) (ofEmpty k g₂ nonZero₂) x=y y=z with decidableIndex i j
=RP'trans (ofEmpty .j g nonZero) (ofEmpty j g₁ nonZero₁) (ofEmpty k g₂ nonZero₂) x=y y=z | inl refl with decidableIndex j k
=RP'trans (ofEmpty .j g nonZero) (ofEmpty j g₁ nonZero₁) (ofEmpty .j g₂ nonZero₂) x=y y=z | inl refl | inl refl = Equivalence.transitive (Setoid.eq (S j)) x=y y=z
=RP'trans (prependLetter i g nonZero x x₁) (prependLetter j g₁ nonZero₁ y x₂) (prependLetter k g₂ nonZero₂ z x₃) x=y y=z with decidableIndex i j
=RP'trans (prependLetter .j g nonZero x x₁) (prependLetter j g₁ nonZero₁ y x₂) (prependLetter k g₂ nonZero₂ z x₃) x=y y=z | inl refl with decidableIndex j k
=RP'trans (prependLetter .j g nonZero x x₁) (prependLetter j g₁ nonZero₁ y x₂) (prependLetter .j g₂ nonZero₂ z x₃) (fst1 ,, snd1) (fst2 ,, snd2) | inl refl | inl refl = Equivalence.transitive (Setoid.eq (S j)) fst1 fst2 ,, =RP'trans x y z snd1 snd2

private
  trans : (x y z : ReducedSequence) → x =RP y → y =RP z → x =RP z
  trans empty empty empty x=y y=z = record {}
  trans (nonempty i x) (nonempty i₁ y) (nonempty i₂ z) x=y y=z = =RP'trans x y z x=y y=z

notEqualIfStartDifferent : {j1 j2 : I} (neq : (j1 ≡ j2) → False) → (x1 : ReducedSequenceBeginningWith j1) (x2 : ReducedSequenceBeginningWith j2) → =RP' x1 x2 → False
notEqualIfStartDifferent neq (ofEmpty i g nonZero) (ofEmpty j g₁ nonZero₁) eq with decidableIndex i j
notEqualIfStartDifferent neq (ofEmpty i g nonZero) (ofEmpty j g₁ nonZero₁) eq | inl i=j = neq i=j
notEqualIfStartDifferent neq (prependLetter i g nonZero x1 x) (prependLetter j g₁ nonZero₁ x2 x₁) eq with decidableIndex i j
notEqualIfStartDifferent neq (prependLetter i g nonZero x1 x) (prependLetter j g₁ nonZero₁ x2 x₁) eq | inl eq' = neq eq'

freeProductSetoid : Setoid ReducedSequence
Setoid._∼_ freeProductSetoid = _=RP_
Equivalence.reflexive (Setoid.eq freeProductSetoid) {x} = reflex {x}
Equivalence.symmetric (Setoid.eq freeProductSetoid) {a} {b} = symm {a} {b}
Equivalence.transitive (Setoid.eq freeProductSetoid) {x} {y} {z} = trans x y z


text:
open import Function using (_∘_)
open import Data.List using (List; _++_) renaming (_∷_ to _,_; _∷ʳ_ to _,′_; [] to ∅)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (∃; _,_)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (True; toWitness)
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; sym; cong)

module LambekGrishinCalculus (U : Set) (R : U) (⟦_⟧ᵁ : U → Set) where

infixr 30 _⊗_ _⊕_
infixr 20 _⇒_ _⇛_
infixl 20 _⇐_ _⇚_
infix  5  _⊢_ [_]⊢_ _⊢[_]

data Polarity : Set where
  + : Polarity
  - : Polarity

_≟ᴾ_ : (p q : Polarity) → Dec (p ≡ q)
+ ≟ᴾ + = yes refl
+ ≟ᴾ - = no (λ ())
- ≟ᴾ + = no (λ ())
- ≟ᴾ - = yes refl

data Type : Set where
  el   : (A : U) → (p : Polarity) → Type
  _⊗_  : Type → Type → Type
  _⇒_  : Type → Type → Type
  _⇐_  : Type → Type → Type
  _⊕_  : Type → Type → Type
  _⇚_  : Type → Type → Type
  _⇛_  : Type → Type → Type

data Pos : Type → Set where
  el : ∀ A → Pos (el A +)
  _⊗_ : ∀ A B → Pos (A ⊗ B)
  _⇚_ : ∀ B A → Pos (B ⇚ A)
  _⇛_ : ∀ A B → Pos (A ⇛ B)

Pos? : ∀ A → Dec (Pos A)
Pos? (el A +) = yes (el A)
Pos? (el A -) = no (λ ())
Pos? (A ⊗ B) = yes (A ⊗ B)
Pos? (A ⇒ B) = no (λ ())
Pos? (A ⇐ B) = no (λ ())
Pos? (A ⊕ B) = no (λ ())
Pos? (A ⇚ B) = yes (A ⇚ B)
Pos? (A ⇛ B) = yes (A ⇛ B)

data Neg : Type → Set where
  el : ∀ A → Neg (el A -)
  _⊕_ : ∀ A B → Neg (A ⊕ B)
  _⇒_ : ∀ A B → Neg (A ⇒ B)
  _⇐_ : ∀ B A → Neg (B ⇐ A)

Neg? : ∀ A → Dec (Neg A)
Neg? (el A +) = no (λ ())
Neg? (el A -) = yes (el A)
Neg? (A ⊗ B) = no (λ ())
Neg? (A ⇒ B) = yes (A ⇒ B)
Neg? (A ⇐ B) = yes (A ⇐ B)
Neg? (A ⊕ B) = yes (A ⊕ B)
Neg? (A ⇚ B) = no (λ ())
Neg? (A ⇛ B) = no (λ ())

Pol? : ∀ A → Pos A ⊎ Neg A
Pol? (el A +)  = inj₁ (el A)
Pol? (el A -)  = inj₂ (el A)
Pol? (A ⊗ B)   = inj₁ (A ⊗ B)
Pol? (A ⇚ B)  = inj₁ (A ⇚ B)
Pol? (A ⇛ B)  = inj₁ (A ⇛ B)
Pol? (A ⊕ B)   = inj₂ (A ⊕ B)
Pol? (A ⇒ B)  = inj₂ (A ⇒ B)
Pol? (A ⇐ B)  = inj₂ (A ⇐ B)

mutual
  data Struct+ : Set where
    ·_·  : Type → Struct+
    _⊗_  : Struct+ → Struct+ → Struct+
    _⇚_  : Struct+ → Struct- → Struct+
    _⇛_  : Struct- → Struct+ → Struct+

  data Struct- : Set where
    ·_·  : Type → Struct-
    _⊕_  : Struct- → Struct- → Struct-
    _⇒_  : Struct+ → Struct- → Struct-
    _⇐_  : Struct- → Struct+ → Struct-

mutual
  data _⊢[_] : Struct+ → Type → Set where
    var    : ∀ {A} → · A · ⊢[ A ]
    μ      : ∀ {X A} {p : True (Neg? A)} → X ⊢ · A · → X ⊢[ A ]
    ⊗R     : ∀ {X Y A B} → X ⊢[ A ] → Y ⊢[ B ] → X ⊗ Y ⊢[ A ⊗ B ]
    ⇚R    : ∀ {X Y A B} → X ⊢[ A ] → [ B ]⊢ Y → X ⇚ Y ⊢[ A ⇚ B ]
    ⇛R    : ∀ {X Y A B} → [ A ]⊢ X → Y ⊢[ B ] → X ⇛ Y ⊢[ A ⇛ B ]

  data [_]⊢_ : Type → Struct- → Set where
    covar  : ∀ {A} → [ A ]⊢ · A ·
    μ̃      : ∀ {X A} {p : True (Pos? A)} → · A · ⊢ X → [ A ]⊢ X
    ⊕L     : ∀ {X Y A B} → [ A ]⊢ Y → [ B ]⊢ X → [ A ⊕ B ]⊢ X ⊕ Y
    ⇒L    : ∀ {X Y A B} → X ⊢[ A ] → [ B ]⊢ Y → [ A ⇒ B ]⊢ X ⇒ Y
    ⇐L    : ∀ {X Y A B} → [ A ]⊢ Y → X ⊢[ B ] → [ A ⇐ B ]⊢ Y ⇐ X

  data _⊢_ : Struct+ → Struct- → Set where
    μ*     : ∀ {X A} {p : True (Pos? A)} → X ⊢[ A ] → X ⊢ · A ·
    μ̃*     : ∀ {X A} {p : True (Neg? A)}→ [ A ]⊢ X → · A · ⊢ X
    ⊗L     : ∀ {X A B} → · A · ⊗ · B · ⊢ X → · A ⊗ B · ⊢ X
    ⇚L    : ∀ {X A B} → · A · ⇚ · B · ⊢ X → · A ⇚ B · ⊢ X
    ⇛L    : ∀ {X A B} → · A · ⇛ · B · ⊢ X → · A ⇛ B · ⊢ X
    ⊕R     : ∀ {X A B} → X ⊢ · A · ⊕ · B · → X ⊢ · A ⊕ B ·
    ⇒R    : ∀ {X A B} → X ⊢ · A · ⇒ · B · → X ⊢ · A ⇒ B ·
    ⇐R    : ∀ {X A B} → X ⊢ · A · ⇐ · B · → X ⊢ · A ⇐ B ·
    res₁   : ∀ {X Y Z} → Y ⊢ X ⇒ Z → X ⊗ Y ⊢ Z
    res₂   : ∀ {X Y Z} → X ⊗ Y ⊢ Z → Y ⊢ X ⇒ Z
    res₃   : ∀ {X Y Z} → X ⊢ Z ⇐ Y → X ⊗ Y ⊢ Z
    res₄   : ∀ {X Y Z} → X ⊗ Y ⊢ Z → X ⊢ Z ⇐ Y
    dres₁  : ∀ {X Y Z} → Z ⇚ X ⊢ Y → Z ⊢ Y ⊕ X
    dres₂  : ∀ {X Y Z} → Z ⊢ Y ⊕ X → Z ⇚ X ⊢ Y
    dres₃  : ∀ {X Y Z} → Y ⇛ Z ⊢ X → Z ⊢ Y ⊕ X
    dres₄  : ∀ {X Y Z} → Z ⊢ Y ⊕ X → Y ⇛ Z ⊢ X
    dist₁  : ∀ {X Y Z W} → X ⊗ Y ⊢ Z ⊕ W → X ⇚ W ⊢ Z ⇐ Y
    dist₂  : ∀ {X Y Z W} → X ⊗ Y ⊢ Z ⊕ W → Y ⇚ W ⊢ X ⇒ Z
    dist₃  : ∀ {X Y Z W} → X ⊗ Y ⊢ Z ⊕ W → Z ⇛ X ⊢ W ⇐ Y
    dist₄  : ∀ {X Y Z W} → X ⊗ Y ⊢ Z ⊕ W → Z ⇛ Y ⊢ X ⇒ W

raise : ∀ {A B} → · A · ⊢ · (B ⇐ A) ⇒ B ·
raise = ⇒R (res₂ (res₃ (μ̃* (⇐L covar var))))

lower : ∀ {A B} → · B ⇚ (A ⇛ B) · ⊢ · A ·
lower = ⇚L (dres₂ (dres₃ (μ* (⇛R covar var))))

import IntuitionisticLogic U ⟦_⟧ᵁ as IL
open IL.Explicit hiding ([_]; _⊢_; reify)
import LinearLogic U R ⟦_⟧ᵁ as LP
open LP renaming (Type to TypeLP; _⊢_ to _⊢LP_; [_] to reifyLP)

mutual
  ⟦_⟧+ : Type → TypeLP
  ⟦ el A +  ⟧+ = el A
  ⟦ el A -  ⟧+ = ¬ (¬ el A)
  ⟦ A ⊗ B   ⟧+ =      ⟦ A ⟧+ ⊗ ⟦ B ⟧+
  ⟦ A ⇚ B  ⟧+ =      ⟦ A ⟧+ ⊗ ⟦ B ⟧-
  ⟦ A ⇛ B  ⟧+ =      ⟦ A ⟧- ⊗ ⟦ B ⟧+
  ⟦ A ⊕ B   ⟧+ = ¬ (  ⟦ A ⟧- ⊗ ⟦ B ⟧-)
  ⟦ A ⇒ B  ⟧+ = ¬ (  ⟦ A ⟧+ ⊗ ⟦ B ⟧-)
  ⟦ A ⇐ B  ⟧+ = ¬ (  ⟦ A ⟧- ⊗ ⟦ B ⟧+)

  ⟦_⟧- : Type → TypeLP
  ⟦ el A +  ⟧- = ¬ el A
  ⟦ el A -  ⟧- = ¬ el A
  ⟦ A ⊗ B   ⟧- = ¬ (  ⟦ A ⟧+ ⊗ ⟦ B ⟧+)
  ⟦ A ⇚ B  ⟧- = ¬ (  ⟦ A ⟧+ ⊗ ⟦ B ⟧-)
  ⟦ A ⇛ B  ⟧- = ¬ (  ⟦ A ⟧- ⊗ ⟦ B ⟧+)
  ⟦ A ⊕ B   ⟧- =      ⟦ A ⟧- ⊗ ⟦ B ⟧-
  ⟦ A ⇒ B  ⟧- =      ⟦ A ⟧+ ⊗ ⟦ B ⟧-
  ⟦ A ⇐ B  ⟧- =      ⟦ A ⟧- ⊗ ⟦ B ⟧+

mutual
  str+ : Struct+ → List TypeLP
  str+ (· A ·)   = ⟦ A ⟧+ , ∅
  str+ (A ⊗ B)   = str+ A ++ str+ B
  str+ (A ⇚ B)  = str+ A ++ str- B
  str+ (A ⇛ B)  = str- A ++ str+ B

  str- : Struct- → List TypeLP
  str- (· A ·)   = ⟦ A ⟧- , ∅
  str- (A ⊕ B)   = str- A ++ str- B
  str- (A ⇒ B)  = str+ A ++ str- B
  str- (A ⇐ B)  = str- A ++ str+ B

open Reify {{...}} using (⟦_⟧)

instance
  Struct+Reify : Reify Struct+ (List TypeLP)
  Struct+Reify = record { ⟦_⟧ = str+ }

instance
  Struct-Reify : Reify Struct- (List TypeLP)
  Struct-Reify = record { ⟦_⟧ = str- }

instance
  TypeReify : Reify Type Set
  TypeReify = record { ⟦_⟧ = λ A → ⟦ ⟦ ⟦ A ⟧+ ⟧ ⟧ }

instance
  StructReify : Reify Struct+ (List Set)
  StructReify = record { ⟦_⟧ = λ X → ⟦ ⟦ ⟦ X ⟧ ⟧ ⟧ }

Neg-≡ : ∀ {A} → Neg A → ⟦ A ⟧+ ≡ ⟦ A ⟧- ⊸ ⊥
Neg-≡ {.(el A -)} (el A) = refl
Neg-≡ {.(A ⊕ B)} (A ⊕ B) = refl
Neg-≡ {.(A ⇒ B)} (A ⇒ B) = refl
Neg-≡ {.(A ⇐ B)} (A ⇐ B) = refl

Pos-≡ : ∀ {A} → Pos A → ⟦ A ⟧- ≡ ⟦ A ⟧+ ⊸ ⊥
Pos-≡ {.(el A +)} (el A) = refl
Pos-≡ {.(A ⊗ B)} (A ⊗ B) = refl
Pos-≡ {.(A ⇚ B)} (A ⇚ B) = refl
Pos-≡ {.(A ⇛ B)} (A ⇛ B) = refl

mutual
  reifyʳ : ∀ {X A} → X ⊢[ A ] → ⟦ X ⟧ ⊢LP ⟦ A ⟧+
  reifyʳ var = var
  reifyʳ (μ {X} {A} {q} t) rewrite Neg-≡ (toWitness q) = abs (to-back (reify t))
  reifyʳ (⊗R {X} {Y} {A} {B} s t) = pair (reifyʳ s) (reifyʳ t)
  reifyʳ (⇚R {X} {Y} {A} {B} s t) = pair (reifyʳ s) (reifyˡ t)
  reifyʳ (⇛R {X} {Y} {A} {B} s t) = pair (reifyˡ s) (reifyʳ t)

  reifyˡ : ∀ {A Y} → [ A ]⊢ Y → ⟦ Y ⟧ ⊢LP ⟦ A ⟧-
  reifyˡ covar = var
  reifyˡ (μ̃ {X} {A} {p} t) rewrite Pos-≡ (toWitness p) = abs (reify t)
  reifyˡ (⊕L {X} {Y} {A} {B} s t) = YX↝XY ⟦ X ⟧ ⟦ Y ⟧ (pair (reifyˡ s) (reifyˡ t))
  reifyˡ (⇒L {X} {Y} {A} {B} s t) = pair (reifyʳ s) (reifyˡ t)
  reifyˡ (⇐L {X} {Y} {A} {B} s t) = pair (reifyˡ s) (reifyʳ t)

  reify  : ∀ {X Y} → X ⊢ Y → ⟦ X ⟧ ++ ⟦ Y ⟧ ⊢LP ⊥
  reify (μ* {X} {A} {p} t) rewrite Pos-≡ (toWitness p) = to-front (app var (reifyʳ t))
  reify (μ̃* {X} {A} {q} t) rewrite Neg-≡ (toWitness q) = app var (reifyˡ t)
  reify (⊗L {X} {A} {B} t) = pair-left (reify t)
  reify (⇚L {X} {A} {B} t) = pair-left (reify t)
  reify (⇛L {X} {A} {B} t) = pair-left (reify t)
  reify (⊕R {X} {A} {B} t) = pair-left′ {⟦ X ⟧} {⟦ A ⟧- } {⟦ B ⟧- } (reify t)
  reify (⇒R {X} {A} {B} t) = pair-left′ {⟦ X ⟧} {⟦ A ⟧+ } {⟦ B ⟧- } (reify t)
  reify (⇐R {X} {A} {B} t) = pair-left′ {⟦ X ⟧} {⟦ A ⟧- } {⟦ B ⟧+ } (reify t)
  reify (res₁ {X} {Y} {Z} t) rewrite sym (++-assoc ⟦ X ⟧ ⟦ Y ⟧ ⟦ Z ⟧) = Y[XZ]↝X[YZ] ⟦ X ⟧ ⟦ Y ⟧ ⟦ Z ⟧ (reify t)
  reify (res₂ {X} {Y} {Z} t) rewrite      ++-assoc ⟦ Y ⟧ ⟦ X ⟧ ⟦ Z ⟧  = [YX]Z↝[XY]Z ⟦ Y ⟧ ⟦ X ⟧ ⟦ Z ⟧ (reify t)
  reify (res₃ {X} {Y} {Z} t) rewrite sym (++-assoc ⟦ X ⟧ ⟦ Y ⟧ ⟦ Z ⟧) = X[ZY]↝X[YZ] ⟦ X ⟧ ⟦ Y ⟧ ⟦ Z ⟧ (reify t)
  reify (res₄ {X} {Y} {Z} t) rewrite      ++-assoc ⟦ X ⟧ ⟦ Z ⟧ ⟦ Y ⟧  = [XZ]Y↝[XY]Z ⟦ X ⟧ ⟦ Z ⟧ ⟦ Y ⟧ (reify t)
  reify (dres₁ {X} {Y} {Z} t) rewrite      ++-assoc ⟦ Z ⟧ ⟦ Y ⟧ ⟦ X ⟧  = [XZ]Y↝[XY]Z ⟦ Z ⟧ ⟦ Y ⟧ ⟦ X ⟧ (reify t)
  reify (dres₂ {X} {Y} {Z} t) rewrite sym (++-assoc ⟦ Z ⟧ ⟦ X ⟧ ⟦ Y ⟧) = X[ZY]↝X[YZ] ⟦ Z ⟧ ⟦ X ⟧ ⟦ Y ⟧ (reify t)
  reify (dres₃ {X} {Y} {Z} t) rewrite      ++-assoc ⟦ Z ⟧ ⟦ Y ⟧ ⟦ X ⟧  = [YX]Z↝[XY]Z ⟦ Z ⟧ ⟦ Y ⟧ ⟦ X ⟧ (reify t)
  reify (dres₄ {X} {Y} {Z} t) rewrite sym (++-assoc ⟦ Y ⟧ ⟦ Z ⟧ ⟦ X ⟧) = Y[XZ]↝X[YZ] ⟦ Y ⟧ ⟦ Z ⟧ ⟦ X ⟧ (reify t)
  reify (dist₁ {X} {Y} {Z} {W} t) = XYZW↝XWZY ⟦ X ⟧ ⟦ Y ⟧ ⟦ Z ⟧ ⟦ W ⟧ (reify t)
  reify (dist₂ {X} {Y} {Z} {W} t) = XYZW↝YWXZ ⟦ X ⟧ ⟦ Y ⟧ ⟦ Z ⟧ ⟦ W ⟧ (reify t)
  reify (dist₃ {X} {Y} {Z} {W} t) = XYZW↝ZXWY ⟦ X ⟧ ⟦ Y ⟧ ⟦ Z ⟧ ⟦ W ⟧ (reify t)
  reify (dist₄ {X} {Y} {Z} {W} t) = XYZW↝ZYXW ⟦ X ⟧ ⟦ Y ⟧ ⟦ Z ⟧ ⟦ W ⟧ (reify t)

[_] : ∀ {X A} → X ⊢[ A ] → (Ctxt ⟦ X ⟧ → ⟦ A ⟧)
[_] = reifyLP ∘ reifyʳ


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

module Ch1 where

-- open import lib.Base
open import Base

-- warmup
module Eq-1-11-2 {i j} {A : Type i} {B : Type j} where

  -- import lib.types.Coproduct
  -- open import lib.types.Empty
  -- open import lib.types.Sigma

  -- If not A and not B, then not (A or B)
  deMorgan1 : (A → ⊥) × (B → ⊥) → (Coprod A B → ⊥)
  -- deMorgan1 (notA , notB) ab = {!!} -- {!!} becomes =>
  -- deMorgan1 (notA , notB) (inl x) = {!!} -- by cases, C-c C-c on param ab
  -- deMorgan1 (notA , notB) (inr x) = {!!}
  deMorgan1 (notA , notB) (inl a) = notA a -- the 'a part' of (A + B) → ⊥
  deMorgan1 (notA , notB) (inr b) = notB b

module Ex1-1 where

  {-
  Exercise 1.1. Given functions f : A -> B and g : B -> C, define their composite g o f : A ->  C.
  Show that we have h o (g o f ) == (h o g) o f
  -}

  _o_ : ∀ {i} {A B C : Type i} → (B → C) → (A → B) → A → C
  (g o f) x = g (f x)

  o-assoc : ∀ {i} {A B C D : Type i} →
    (h : C → D) → (g : B → C) → (f : A → B) →
    h o (g o f) == (h o g) o f
  o-assoc _ _ _ = idp -- "it's de proof"

module Ex1-2 where

  -- open import lib.types.Sigma

  -- Derive the recursion principle for products recA×B using only the projections, and
  -- verify that the definitional equalities are valid. Do the same for Σ-types.

  recAxB : ∀ {i} {A B C : Type i} →
    (A → B → C) → A × B → C
  recAxB f ab = f (fst ab) (snd ab)

  recAxB= : ∀ {i} {A B C : Type i}
    {f : A → B → C}
    {a : A} {b : B} →
    recAxB f (a , b) == f a b
  recAxB= = idp

  recA+B : ∀ {i j} {A : Type i} {B : Type j} {C : Type (lmax i j)} →
    (A → C) → (B → C) → (Coprod A B → C)
  recA+B f g (inl x) = f x
  recA+B f g (inr x) = g x

  recA+B= : {A B C : Type0}
    {f : A → C} {g : B → C}
    {a : A} {b : B} →
    (recA+B f g (inl a) == f a) × (recA+B f g (inr b) == g b)
  recA+B= = idp , idp

  recΣ : ∀ {i j} {A : Type i} {B : A → Type j} {C : Type (lmax i j)} →
    ((a : A) → B a → C) →
    Σ A B → C
  recΣ f ab = f (fst ab) (snd ab)

  recΣ= : ∀ {i j} {A : Type i} {B : A → Type j} {C : Type (lmax i j)}
    {f : (a : A) → B a → C}
    {a : A} {ba : B a} →
    recΣ f (a , ba) == f a ba
  recΣ= = idp

module Ex1-3 {i j} {A : Type i} {B : Type j} where

  -- open import lib.types.Sigma

  {- Derive the induction principle for products indA×B, using only the projections
  and the propositional uniqueness principle uppt. Verify that the definitional
  equalities are valid. Gen- eralize uppt to Σ-types, and do the same for Σ-types.
  -}

  -- book definition of uppt
  uppt-× : (ab : (A × B)) → (fst ab , snd ab) == ab
  uppt-× = λ _ → idp

  -- definition of induction principle the projections and the transported uniqueness principle
  -- (this was a confusing question to work out in Agda, since the transport is redundant / inferred by the typechecker)
  ind-× : (C :  (A × B) → Type (lmax i j)) →
    ((a : A ) → (b : B) → C (a , b)) → Π (A × B) C
  ind-× C g ab = transport C (uppt-× ab) (g (fst ab) (snd ab))

  -- (propositional) verification of defining equations
  ind-×= : (C :  (A × B) → Type (lmax i j)) →
    (g : ((a : A ) → (b : B) → C (a , b))) →
    ∀ {a b} → ind-× C g (a , b) == g a b
  ind-×= C g {a} {b} = -- idp
    ind-× C g (a , b) =⟨ idp ⟩
    transport C (uppt-× (a , b)) (g a b) =⟨ idp ⟩
    transport C idp (g a b) =⟨ idp ⟩
    g a b ∎

  -- book definition of induction principle using pattern matching
  pattern-match-ind-× : (C :  (A × B) → Type (lmax i j)) →
    Π A (λ x → Π B (λ y → C (x , y))) → Π (A × B) C
  pattern-match-ind-× _ g (a , b) = g a b

  -- alternative definition of uniqueness principle (from induction principle)
  ind-uppt-× : (x : (A × B)) → (fst x , snd x) == x
  ind-uppt-× = ind-× (λ z → z == z) (λ x x₁ → idp)

  -- validate definition for uppt
  uppt-×= : {x : (A × B)} → (uppt-× x) == (ind-uppt-× x)
  uppt-×= = idp

  -- uppt for Σ types
  upptΣ : {B : (a : A) → Type j} → (ab : Σ A B) → ab == (fst ab , snd ab)
  upptΣ _ = idp

module Ex1-4 where

  -- open import lib.types.Sigma

  {-
  Assuming as given only the iterator for natural numbers
  iter : ∏ C → (C → C) → N → C
       C:U
  with the defining equations
  iter(C, c0, cs, succ(n)) :≡ cs(iter(C, c0, cs, n)),
  derive a function having the type of the recursor recN. Show that the defining
  equations of the recursor hold propositionally for this function, using the
  induction principle for N.
  -}

  iter : {C : Type0} →
    C → (C → C) → ℕ → C
  iter c0 cs 0 = c0
  iter c0 cs (S n) = cs (iter c0 cs n)

  -- used in the definition of recNiter below to keep a count of the applications of a function
  sucApply : {C : Type0} → (ℕ → C → C) → ℕ × C → ℕ × C
  sucApply {C} cs = cs' where
    cs' : ℕ × C → ℕ × C
    cs' (n , c) = S n , cs n c

  {- Induction principle (dependent eliminator) for ℕ from the book:

  indN : ∏(C:N→U)C(0) → ∏(n:N)C(n) → C(succ(n)) → ∏(n:N)C(n)
  indN(C, c0, cs, 0) :≡ c0,
  indN(C, c0, cs, succ(n)) :≡ cs(n, indN(C, c0, cs, n)).
  -}
  indN : ∀ {i} {C : ℕ → Type i} →
    C 0 → ((n : ℕ) → C n → C (S n)) → (n : ℕ) → C n
  indN c0 cs 0 = c0
  indN c0 cs (S n) = cs n (indN c0 cs n)

  -- digression / warmup - inductive proof that evens-are-even

  -- nth even
  even : ℕ → ℕ
  even n = iter 0 (λ n → S (S n)) n

  S= : {m n : ℕ} → m == n → (S m == S n)
  S= idp = idp

  _*2 : ℕ → ℕ
  O *2 = O
  (S n) *2 = S (S (n *2))

  evens-are-even : (n : ℕ) → Σ ℕ (λ m → even n == m *2)
  evens-are-even = indN (0 , idp) inductiveCase where
    inductiveCase : (n : ℕ) → Σ ℕ (λ m → even n == m *2) → Σ ℕ (λ m → even (S n) == m *2)
    inductiveCase n (m , p) = S m , p'' where
      p' = S= p
      p'' = S= p'

  {- derive a function having the type of the recursor recN
  recN : ∏(C:U)C→(N→C→C)→N→C
  recN(C, c0, cs, 0) :≡ c0,
  recN(C, c0, cs, Sc(n)) :≡ cs(n, recN(C, c0, cs, n)).
  -}
  recNiter : {C : Type0} →
    C → (ℕ → C → C) → ℕ → C
  recNiter c0 cs n = snd (iter (0 , c0) cs' n) where
           cs' = sucApply cs

  {- Show that the defining
  equations of the recursor hold propositionally for this function, using the
  induction principle for N
  -}
  recNiter= : {C : Type0} {c0 : C} {cs : ℕ → C → C } →
    (n : ℕ) →
    (recNiter c0 cs (S n)) == (cs n (recNiter c0 cs n))
  recNiter= {C} {c0} {cs} n = cs= n'= -- or, as spelled out below (using equational reasoning from HoTT-Agda)
    -- recNiter c0 cs (S n) =⟨ idp ⟩
    -- snd (iter' (S n)) =⟨ idp ⟩
    -- snd (cs' (iter' n)) =⟨ idp ⟩
    -- snd (cs' (n' , snd (iter' n))) =⟨ idp ⟩
    -- cs n' (snd (iter' n)) =⟨ cs= n'= ⟩
    -- cs n (snd (iter' n)) =⟨ idp ⟩
    -- cs n (recNiter c0 cs n) ∎
    where
      cs' = sucApply cs

      iter' : ℕ → ℕ × C
      iter' = iter (0 , c0) cs'

      n' = fst (iter' n)

      -- proof that the first (counter) projection of the iter version of recN at n is just n
      fstIter'= : (n : ℕ) → (fst (iter (0 , c0) cs' n) == n)
      fstIter'= = indN idp inductiveCase where
        inductiveCase : (n : ℕ) →
          fst (iter' n) == n →
          fst (iter' (S n)) == S n
        inductiveCase m p = S= p -- or, as spelled out below
          -- fst (iter (0 , c0) cs' (S m)) =⟨ idp ⟩
          -- fst (cs' (iter (0 , c0) cs' m)) =⟨ idp ⟩
          -- fst (cs' (iter (0 , c0) cs' m)) =⟨ idp ⟩
          -- -- fst (cs' (fst (iter (0 , c0) cs' m) , _)) =⟨ idp ⟩ -- Agda loses track of some hidden
          -- -- fst (S (fst (iter (0 , c0) cs' m)) , _) =⟨ idp ⟩ -- type data here, thus double-protective comments
          -- S (fst (iter (0 , c0) cs' m)) =⟨ S= p ⟩
          -- S m ∎

      n'= : n' == n
      n'= = fstIter'= n

      cs= : ∀ {n m} {c : C} → n == m → cs n c == cs m c
      cs= idp = idp

-- recursor for Bool (used in next two exercises)
module RecBool where
  recBool : ∀ {i} {A : Type i} → A → A → Bool → A
  recBool x y true = x
  recBool x y false = y

module Ex1-5 where
  open RecBool
  {-
  Exercise 1.5. Show that if we define A + B :≡ ∑(x:2) rec2(U, A, B, x), then we can give a definition
  of indA+B for which the definitional equalities stated in §1.7 hold.
  -}
  _+_ : ∀ {i} → Type i → Type i → Type _
  A + B = Σ Bool (λ isA → recBool A B isA)

  inl-+ : ∀ {i} {A B : Type i} → A → A + B
  inl-+ a = true , a

  inr-+ : ∀ {i} {A B : Type i} → B → A + B
  inr-+ b = false , b

  ind-+ : ∀ {i j} {A B : Type i} (C : A + B → Type j) →
    ((a : A) → C (inl-+ a)) → ((b : B) → C (inr-+ b)) →
    (x : A + B) → C x
  ind-+ C g1 g2 (true , a) = g1 a
  ind-+ C g1 g2 (false , b) = g2 b

module Ex1-6 {i} {A B : Type i} where
  open RecBool
  open import FunExt
  {-
  Exercise 1.6. Show that if we define A × B :≡ ∏(x:2) rec2(U, A, B, x), then we can give a defini- tion of indA×B for which the definitional equalities stated in §1.5 hold propositionally (i.e. using equality types). (This requires the function extensionality axiom, which is introduced in §2.9.)
  -}

  _x_ : ∀ {i} → (A : Type i) → (B : Type i) → Type _
  A x B = Π Bool (λ ab → recBool A B ab)

  _,,_ : A → B → A x B
  _,,_ a b true = a
  _,,_ a b false = b

  fst-x : A x B → A
  fst-x ab = ab true

  snd-x : A x B → B
  snd-x ab = ab false

  uppt-x : (ab : (A x B)) → (fst-x ab ,, snd-x ab) == ab
  uppt-x ab = is-equiv.g fe h where -- (fst-x ab ,, snd-x ab) x == ab x
    fe = fun-ext ((fst-x ab ,, snd-x ab)) ab
    h : (c : Bool) → (fst-x ab ,, snd-x ab) c == ab c
    h true = idp
    h false = idp

  ind-x : ∀ {j} (C : A x B → Type j) →
    ((a : A) → (b : B) → C (a ,, b)) →
    (ab : A x B) → C ab
  ind-x C g ab = transport C (uppt-x ab) (g a b) where
    a = fst-x ab
    b = snd-x ab

module Ex1-7 where
  {-
  Exercise 1.7. Give an alternative derivation of ind′=A from ind=A which avoids the use of universes. (This is easiest
  using concepts from later chapters.)
  -}

  {-
  Section 1.12.2 "we can show that ind=A entails Lemmas2.3.1 and 3.11.8, and that these two principles imply ind′=A
  directly"
  -}

  {-
  Lemma 2.3.1 (Transport). Suppose that P is a type family over A and that p : x =A y. Then there is a function
    p∗ : P(x) → P(y).
  -}

  {-
  Lemma 3.11.8. For any A and any a : A, the type ∑(x:A)(a = x) is contractible.
  -}
  lemma-3-11-8 : ∀ {i} {A : Type i} (a : A) → is-contr (Σ A λ x → a == x)
  lemma-3-11-8 {_} {A} a = ((a , idp)) , λ { (x , p) → along {x} p } where
    along : {x : A}(p : a == x) → (a , idp) == (x , p)
    along idp = idp -- should really prove using ind== then ind='2 will indeed be based path induction from free
                    -- path induction

  ind='2 : ∀ {i j} {A : Type i} {a : A} →
    (D : (x : A) (p : a == x) → Type j) →
    D a idp →
    {x : A} (p : a == x) →
    D x p
  ind='2 {i} {j} {A} {a} D d {x} p = transport (λ { (x , p) → D x p}) (snd (lemma-3-11-8 a) (x , p)) d

module Ex1-14 where

  {- Exercise 1.14. Why do the induction principles for identity types not allow us to construct a
  function f : ∏(x:A) ∏(p:x=x)(p = reflx) with the defining equation f (x, reflx ) :≡ reflreflx ? -}

module Ex1-15 {i j} {A : Type i} {C : A → Type j} where
  {- Exercise 1.15. Show that indiscernability of identicals follows from path induction. -}

  f : ∀ {x y : A} (p : x == y) → C x → C y
  f idp = ind== (λ x y _ → C x → C y) (λ x → λ cx → cx) idp

max_stars_repo_name: aerskine/hott-ex

max_issues_repo_name: aerskine/hott-ex

max_forks_repo_name: aerskine/hott-ex