text:
module TestVec where
open import PreludeNatType
open import PreludeShow

infixr 40 _::_

data Vec (A : Set) : Nat -> Set where
    []   : Vec A zero
    _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

head : {A : Set}{n : Nat} -> Vec A (suc n) -> A
head (x :: _) = x  -- no need for a [] case

length : {A : Set}{n : Nat} -> Vec A n -> Nat
length {A} {n} v = n

three : Vec Nat 3
three = 1 :: 2 :: 3 :: []

mainS = showNat (length  three)

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_; Setω)

open import Boolean.Definition
open import Setoids.Setoids
open import Setoids.Subset
open import Setoids.Functions.Definition
open import LogicalFormulae
open import Functions.Definition
open import Lists.Lists

module LectureNotes.MetAndTop.Chapter1 where

PowerSet : {a : _} (A : Set a) → {b : _} → Set (a ⊔ lsuc b)
PowerSet A {b} = A → Set b

equality : {a b c : _} (A : Set a) → PowerSet A {b} → PowerSet A {c} → Set (a ⊔ b ⊔ c)
equality A x y = (z : A) → (x z → y z) && (y z → x z)

trans : {a b c d : _} {A : Set a} → {x : PowerSet A {b}} {y : PowerSet A {c}} {z : PowerSet A {d}} → equality A x y → equality A y z → equality A x z
trans {x} {y} {z} x=y y=z i with x=y i
... | r ,, s with y=z i
... | t ,, u = (λ z → t (r z)) ,, λ z → s (r (_&&_.snd (x=y i) (u z)))

symm : {a b c : _} {A : Set a} → {x : PowerSet A {b}} {y : PowerSet A {c}} → equality A x y → equality A y x
symm x=y i with x=y i
... | r ,, s = s ,, r

reflex : {a b : _} {A : Set a} → (x : PowerSet A {b}) → equality A x x
reflex x i = (λ z → z) ,, λ z → z

mapPower : {a b c : _} {A : Set a} {B : Set b} (f : A → B) → PowerSet B {c} → PowerSet A {c}
mapPower f p a = p (f a)

mapF : {a b c : _} {A : Set a} {B : Set b} (f : A → B) → PowerSet A {c} → PowerSet B {_}
mapF {A = A} f p b = Sg A (λ a → (p a) && (f a ≡ b))

singleton : {a b : _} {A : Set a} → (decidableEquality : (x y : A) → (x ≡ y) || ((x ≡ y) → False)) → A → PowerSet A {b}
singleton decidable a n with decidable a n
singleton decidable a n | inl x = True'
singleton decidable a n | inr x = False'

intersection : {a b c : _} {A : Set a} {B : Set b} (sets : A → PowerSet B {c}) → PowerSet B {a ⊔ c}
intersection {A = A} sets x = (a : A) → (sets a) x

union : {a b c : _} {A : Set a} {B : Set b} (sets : A → PowerSet B {c}) → PowerSet B {a ⊔ c}
union {A = A} sets x = Sg A λ i → sets i x

complement : {a b : _} {A : Set a} → (x : PowerSet A {b}) → PowerSet A
complement x t = x t → False

emptySet : {a b : _} (A : Set a) → PowerSet A {b}
emptySet A x = False'

decideIt : {a b : _} {A : Set a} → {f : A → Set b} → ((x : A) → (f x) || ((f x) → False)) → A → Set _
decideIt decide a with decide a
decideIt decide a | inl x = True
decideIt decide a | inr x = False

fromExtension : {a : _} {A : Set a} → ((x y : A) → (x ≡ y) || ((x ≡ y) → False)) → List A → PowerSet A
fromExtension decideEquality l = decideIt {f = contains l} (containsDecidable decideEquality l)

private

  data !1234 : Set where
    !1 : !1234
    !2 : !1234
    !3 : !1234
    !4 : !1234

  decidable1234 : (x y : !1234) → (x ≡ y) || ((x ≡ y) → False)
  decidable1234 !1 !1 = inl refl
  decidable1234 !1 !2 = inr (λ ())
  decidable1234 !1 !3 = inr (λ ())
  decidable1234 !1 !4 = inr (λ ())
  decidable1234 !2 !1 = inr (λ ())
  decidable1234 !2 !2 = inl refl
  decidable1234 !2 !3 = inr (λ ())
  decidable1234 !2 !4 = inr (λ ())
  decidable1234 !3 !1 = inr (λ ())
  decidable1234 !3 !2 = inr (λ ())
  decidable1234 !3 !3 = inl refl
  decidable1234 !3 !4 = inr (λ ())
  decidable1234 !4 !1 = inr (λ ())
  decidable1234 !4 !2 = inr (λ ())
  decidable1234 !4 !3 = inr (λ ())
  decidable1234 !4 !4 = inl refl

  f : !1234 → !1234
  f !1 = !1
  f !2 = !1
  f !3 = !4
  f !4 = !3

  exercise1'1i1 : {b : _} → equality {b = b} !1234 (mapPower f (singleton decidable1234 !1)) (fromExtension decidable1234 (!1 :: !2 :: []))
  exercise1'1i1 !1 = (λ x → record {}) ,, (λ x → record {})
  exercise1'1i1 !2 = (λ x → record {}) ,, (λ x → record {})
  exercise1'1i1 !3 = (λ ()) ,, (λ ())
  exercise1'1i1 !4 = (λ ()) ,, λ ()

  exercise1'1i2 : {b : _} → equality {b = b} !1234 (mapPower f (singleton decidable1234 !2)) (λ _ → False)
  exercise1'1i2 !1 = (λ ()) ,, λ ()
  exercise1'1i2 !2 = (λ ()) ,, (λ ())
  exercise1'1i2 !3 = (λ ()) ,, (λ ())
  exercise1'1i2 !4 = (λ ()) ,, (λ ())

  exercise1'1i3 : equality !1234 (mapPower f (fromExtension decidable1234 (!3 :: !4 :: []))) (fromExtension decidable1234 (!3 :: !4 :: []))
  exercise1'1i3 !1 = (λ x → x) ,, (λ x → x)
  exercise1'1i3 !2 = (λ x → x) ,, (λ x → x)
  exercise1'1i3 !3 = (λ x → record {}) ,, (λ x → record {})
  exercise1'1i3 !4 = (λ x → record {}) ,, (λ x → record {})

  exercise1'1ii1 : {a b c t : _} {A : Set a} {B : Set b} {T : Set t} → (f : A → B) → (sets : T → PowerSet B {c}) → equality A (mapPower f (union sets)) (union λ x → mapPower f (sets x))
  exercise1'1ii1 f sets i = (λ x → x) ,, (λ x → x)

  exercise1'1ii2 : {a b c t : _} {A : Set a} {B : Set b} {T : Set t} → (f : A → B) → (sets : T → PowerSet B {c}) → equality A (mapPower f (intersection sets)) (intersection λ x → mapPower f (sets x))
  exercise1'1ii2 f sets i = (λ x → x) ,, (λ x → x)

  exercise1'1ii3 : {a b : _} {A : Set a} {B : Set b} → (f : A → B) → equality A (mapPower f (λ i → True)) (λ i → True)
  exercise1'1ii3 f = λ z → (λ x → record {}) ,, (λ x → record {})

  exercise1'1ii4 : {a b c : _} {A : Set a} {B : Set b} → (f : A → B) → equality A (mapPower f (emptySet {b = c} B)) (emptySet A)
  exercise1'1ii4 f = λ z → (λ x → x) ,, (λ x → x)

  exercise1'1ii5 : {a b c : _} {A : Set a} {B : Set b} → (f : A → B) → (u : PowerSet B {c}) → equality A (mapPower f (complement u)) (complement (mapPower f u))
  exercise1'1ii5 f u z = (λ x → x) ,, (λ x → x)

  exercise1'1iii1 : {a b c t : _} {A : Set a} {B : Set b} {T : Set t} → (f : A → B) (sets : T → PowerSet A {c}) → equality B (mapF f (union sets)) (union λ t → mapF f (sets t))
  exercise1'1iii1 {A = A} {T = T} f sets z = x ,, y
    where
      x : mapF f (union sets) z → union (λ t → mapF f (sets t)) z
      x (a , ((t , isIn) ,, snd)) = t , (a , (isIn ,, snd))
      y : union (λ t → mapF f (sets t)) z → mapF f (union sets) z
      y (t , (r , s)) = r , ((t , _&&_.fst s) ,, _&&_.snd s)

  exercise1'1iii2 : {a b c d : _} {A : Set a} {B : Set b} → (f : A → B) → equality B (mapF f (emptySet {b = c} A)) (emptySet {b = d} B)
  exercise1'1iii2 {A = A} {B = B} f z = x ,, λ ()
    where
      x : mapF f (emptySet A) z → emptySet B z
      x (a , ())

  ex4F : !1234 → !1234
  ex4F !1 = !1
  ex4F !2 = !2
  ex4F !3 = !1
  ex4F !4 = !4

  v1 : PowerSet !1234
  v1 !1 = True
  v1 !2 = True
  v1 !3 = False
  v1 !4 = False
  v2 : PowerSet !1234
  v2 !1 = False
  v2 !2 = True
  v2 !3 = True
  v2 !4 = False

  v1AndV2 : Bool → !1234 → Set
  v1AndV2 BoolTrue = v1
  v1AndV2 BoolFalse = v2

  lhs : equality {c = lzero} !1234 (mapF ex4F (intersection v1AndV2)) (singleton decidable1234 !2)
  lhs !1 = ans ,, λ ()
    where
      ans : mapF ex4F (intersection v1AndV2) !1 → False'
      ans (!1 , (fst ,, refl)) with fst BoolFalse
      ans (!1 , (fst ,, refl)) | ()
      ans (!3 , (fst ,, refl)) with fst BoolTrue
      ans (!3 , (fst ,, refl)) | ()
  lhs !2 = (λ _ → record {}) ,, ans
    where
      u : intersection v1AndV2 !2
      u BoolTrue = record {}
      u BoolFalse = record {}
      ans : singleton decidable1234 !2 !2 → mapF ex4F (intersection v1AndV2) !2
      ans _ = !2 , (u ,, refl)
  lhs !3 = ans ,, λ ()
    where
      ans : mapF ex4F (intersection v1AndV2) !3 → False'
      ans (!3 , (fst ,, ()))
  lhs !4 = ans ,, λ ()
    where
      ans : mapF ex4F (intersection v1AndV2) !4 → False'
      ans (!4 , (fst ,, refl)) with fst BoolTrue
      ans (!4 , (fst ,, refl)) | ()

  fv1AndV2 : Bool → !1234 → Set
  fv1AndV2 BoolTrue = mapF ex4F v1
  fv1AndV2 BoolFalse = mapF ex4F v2

  rhs : equality {c = lzero} !1234 (intersection fv1AndV2) (fromExtension decidable1234 (!2 :: !1 :: []))
  rhs !1 = (λ _ → record {}) ,, λ _ → a
    where
      a : intersection fv1AndV2 !1
      a BoolTrue = !1 , (record {} ,, refl)
      a BoolFalse = !3 , (record {} ,, refl)
  rhs !2 = (λ _ → record {}) ,, λ _ → a
    where
      a : intersection fv1AndV2 !2
      a BoolTrue = !2 , (record {} ,, refl)
      a BoolFalse = !2 , (record {} ,, refl)
  rhs !3 = a ,, λ ()
    where
      a : intersection fv1AndV2 !3 → fromExtension decidable1234 (!2 :: !1 :: []) !4
      a pr with pr BoolTrue
      a pr | !1 , (fst ,, ())
      a pr | !2 , (fst ,, ())
      a pr | !3 , (fst ,, snd) = fst
      a pr | !4 , (fst ,, snd) = fst
  rhs !4 = a ,, λ ()
    where
      a : intersection fv1AndV2 !4 → fromExtension decidable1234 (!2 :: !1 :: []) !4
      a pr with pr BoolTrue
      a pr | !1 , (x ,, ())
      a pr | !2 , (x ,, ())
      a pr | !3 , (x ,, ())
      a pr | !4 , (x ,, _) = x

  exercise1'1iv1 : (equality !1234 (mapF ex4F (intersection v1AndV2)) (intersection fv1AndV2)) → False
  exercise1'1iv1 pr = ohno
    where
      bad : equality !1234 (fromExtension decidable1234 (!2 :: !1 :: [])) (singleton decidable1234 !2)
      bad = trans (symm rhs) (trans (symm pr) lhs)
      ohno : False
      ohno with bad !1
      ohno | fst ,, snd with fst record {}
      ... | ()

  exercise1'1iv2 : (equality !1234 (mapF ex4F (λ _ → True)) (λ _ → True)) → False
  exercise1'1iv2 pr with pr !3
  exercise1'1iv2 pr | fst ,, snd with snd _
  exercise1'1iv2 pr | fst ,, snd | !1 , ()
  exercise1'1iv2 pr | fst ,, snd | !2 , ()
  exercise1'1iv2 pr | fst ,, snd | !3 , ()
  exercise1'1iv2 pr | fst ,, snd | !4 , ()

  exercise1'1iv3 : equality !1234 (mapF ex4F (complement v1)) (complement v1) → False
  exercise1'1iv3 pr with pr !1
  exercise1'1iv3 pr | fst ,, snd with fst (!3 , ((λ i → i) ,, refl)) (record {})
  ... | ()

ext: agda


text:
------------------------------------------------------------------------
-- Truncated queues: any two queues representing the same sequence are
-- equal, and things are set up so that at compile-time (but not at
-- run-time) some queue operations compute in roughly the same way as
-- the corresponding list operations
------------------------------------------------------------------------

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

import Equality.Path as P

module Queue.Truncated
  {e⁺} (eq : ∀ {a p} → P.Equality-with-paths a p e⁺) where

open P.Derived-definitions-and-properties eq

open import Logical-equivalence using (_⇔_)
open import Prelude

open import Bijection equality-with-J as Bijection using (_↔_)
open import Equality.Path.Isomorphisms eq
open import Erased.Cubical eq hiding (map)
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import List equality-with-J as L hiding (map)
open import H-level equality-with-J
open import H-level.Closure equality-with-J
open import H-level.Truncation.Propositional eq as Trunc
import Queue equality-with-J as Q
open import Sum equality-with-J
open import Surjection equality-with-J using (_↠_)

private
  variable
    a b     : Level
    A B     : Type a
    p q x   : A
    f       : A → B
    xs      : List A
    s s₁ s₂ : Very-stableᴱ-≡ A

------------------------------------------------------------------------
-- Queues

-- The queue type family is parametrised.

module _
  -- The underlying queue type family.
  (Q : ∀ {ℓ} → Type ℓ → Type ℓ)

  -- Note that the predicate is required to be trivial. Perhaps the
  -- code could be made more general, but I have not found a use for
  -- such generality.
  ⦃ is-queue : ∀ {ℓ} → Q.Is-queue (λ A → Q A) (λ _ → ↑ _ ⊤) ℓ ⦄
  where

  abstract

    -- Queues indexed by corresponding lists, and truncated so that
    -- any two queues that stand for the same list are seen as equal.
    --
    -- The type is abstract to ensure that a change to a different
    -- underlying queue type family does not break code that uses this
    -- module.
    --
    -- Ulf Norell suggested to me that I could use parametrisation
    -- instead of abstract. (Because if the underlying queue type
    -- family is a parameter, then the underlying queues do not
    -- compute.) I decided to use both. (Because I want to have the
    -- flexibility that comes with parametrisation, but I do not want
    -- to force users to work in a parametrised setting.)

    Queue_⟪_⟫ : {A : Type a} → @0 List A → Type a
    Queue_⟪_⟫ {A = A} xs =
      ∥ (∃ λ (q : Q A) → Erased (Q.to-List _ q ≡ xs)) ∥

  -- Queues.

  Queue : Type a → Type a
  Queue A = ∃ λ (xs : Erased (List A)) → Queue_⟪_⟫ (erased xs)

-- The remainder of the code uses an implicit underlying queue type
-- family parameter, and an extra instance argument.

module _
  {Q : ∀ {ℓ} → Type ℓ → Type ℓ}
  ⦃ is-queue : ∀ {ℓ} → Q.Is-queue (λ A → Q A) (λ _ → ↑ _ ⊤) ℓ ⦄
  ⦃ is-queue-with-map :
      ∀ {ℓ₁ ℓ₂} → Q.Is-queue-with-map (λ A → Q A) ℓ₁ ℓ₂ ⦄
  where

  abstract

    -- Queue Q ⟪ xs ⟫ is a proposition.

    Queue-⟪⟫-propositional :
      {@0 xs : List A} →
      Is-proposition (Queue Q ⟪ xs ⟫)
    Queue-⟪⟫-propositional = truncation-is-proposition

  -- Returns the (erased) index.

  @0 ⌊_⌋ : Queue Q A → List A
  ⌊_⌋ = erased ∘ proj₁

  -- There is a bijection between equality of two values of type
  -- Queue Q A and erased equality of the corresponding list indices.

  ≡-for-indices↔≡ :
    {xs ys : Queue Q A} →
    Erased (⌊ xs ⌋ ≡ ⌊ ys ⌋) ↔ xs ≡ ys
  ≡-for-indices↔≡ {xs = xs} {ys = ys} =
    Erased (⌊ xs ⌋ ≡ ⌊ ys ⌋)  ↝⟨ Erased-≡↔[]≡[] ⟩
    proj₁ xs ≡ proj₁ ys       ↝⟨ ignore-propositional-component Queue-⟪⟫-propositional ⟩□
    xs ≡ ys                   □

  -- If a queue equality holds under the (non-dependent) assumption
  -- that equality is very stable for the carrier type, then it also
  -- holds without this assumption.
  --
  -- For an example of a lemma which has this kind of assumption, see
  -- Queue.from-List≡foldl-enqueue-empty.

  strengthen-queue-equality :
    {q₁ q₂ : Queue Q A} → (Very-stable-≡ A → q₁ ≡ q₂) → q₁ ≡ q₂
  strengthen-queue-equality {q₁ = q₁} {q₂ = q₂} eq =
    _↔_.to ≡-for-indices↔≡
      [ ⌊ q₁ ⌋  ≡⟨ cong ⌊_⌋ (eq (Very-stable→Very-stable-≡ 0 (erased Erased-Very-stable))) ⟩∎
        ⌊ q₂ ⌋  ∎
      ]

------------------------------------------------------------------------
-- Conversion functions

  mutual

    abstract

      -- The right-to-left direction of Queue-⟪⟫↔Σ-List (defined
      -- below). Note that there is no assumption of stability.

      Σ-List→Queue-⟪⟫ :
        {@0 ys : List A} →
        (∃ λ xs → Erased (xs ≡ ys)) → Queue Q ⟪ ys ⟫
      Σ-List→Queue-⟪⟫ = _  -- Agda can infer the definition.

    -- If ys : List A and equality is very stable (with erased proofs)
    -- for A, then Queue Q ⟪ ys ⟫ is isomorphic to the type of lists
    -- equal (with erased equality proofs) to ys.
    --
    -- Note that equality is very stable for A if A has decidable
    -- equality.

    Queue-⟪⟫↔Σ-List :
      {@0 ys : List A} →
      Very-stableᴱ-≡ A →
      Queue Q ⟪ ys ⟫ ↔ ∃ λ xs → Erased (xs ≡ ys)
    Queue-⟪⟫↔Σ-List {ys = ys} s = Bijection.with-other-inverse
      Queue-⟪⟫↔Σ-List′
      Σ-List→Queue-⟪⟫
      (λ _ → from-Queue-⟪⟫↔Σ-List′)
      where
      abstract

        Queue-⟪⟫↔Σ-List′ : Queue Q ⟪ ys ⟫ ↔ ∃ λ xs → Erased (xs ≡ ys)
        Queue-⟪⟫↔Σ-List′ = ↠→↔Erased-singleton
          (Q.Queue↠List _)
          (Very-stableᴱ-≡-List 0 s)

        from-Queue-⟪⟫↔Σ-List′ :
          _≡_ {A = Queue Q ⟪ ys ⟫}
              (_↔_.from Queue-⟪⟫↔Σ-List′ p)
              (Σ-List→Queue-⟪⟫ p)
        from-Queue-⟪⟫↔Σ-List′ = refl _

  -- If equality is very stable (with erased proofs) for A, then
  -- Queue Q A is isomorphic to List A.

  Queue↔List : Very-stableᴱ-≡ A → Queue Q A ↔ List A
  Queue↔List {A = A} s =
    Queue Q A                                                        ↔⟨⟩
    (∃ λ (xs : Erased (List A)) → Queue Q ⟪ erased xs ⟫)             ↝⟨ (∃-cong λ _ → Queue-⟪⟫↔Σ-List s) ⟩
    (∃ λ (xs : Erased (List A)) → ∃ λ ys → Erased (ys ≡ erased xs))  ↝⟨ Σ-Erased-Erased-singleton↔ ⟩□
    List A                                                           □

  mutual

    -- The right-to-left direction of Queue↔List. (Note that equality
    -- is not required to be very stable with erased proofs for the
    -- carrier type.)

    from-List : List A → Queue Q A
    from-List = _  -- Agda can infer the definition.

    _ : _↔_.from (Queue↔List s) ≡ from-List
    _ = refl _

  -- The forward direction of Queue↔List s.

  to-List : Very-stableᴱ-≡ A → Queue Q A → List A
  to-List s = _↔_.to (Queue↔List s)

  abstract

    -- The function to-List returns the index.

    @0 ≡⌊⌋ : to-List s q ≡ ⌊ q ⌋
    ≡⌊⌋ {s = s} {q = q} =
      to-Σ-Erased-∥-Σ-Erased-≡-∥↔≡
        (Q.Queue↠List _) (Very-stableᴱ-≡-List 0 s) q

  -- Queue Q A is isomorphic to List A in an erased context. The
  -- forward direction of this isomorphism returns the index directly.

  @0 Queue↔Listⁱ : Queue Q A ↔ List A
  Queue↔Listⁱ {A = A} =
    Queue Q A                                             ↔⟨⟩
    (∃ λ (xs : Erased (List A)) → Queue Q ⟪ erased xs ⟫)  ↝⟨ drop-⊤-right (λ _ → _⇔_.to contractible⇔↔⊤ $
                                                             propositional⇒inhabited⇒contractible Queue-⟪⟫-propositional $
                                                             _↔_.from (Queue-⟪⟫↔Σ-List (Very-stable→Very-stableᴱ 1 $
                                                                                Very-stable→Very-stable-≡ 0 $
                                                                                erased Erased-Very-stable))
                                                                      (_ , [ refl _ ])) ⟩
    Erased (List A)                                       ↝⟨ Very-stable→Stable 0 $ erased Erased-Very-stable ⟩□
    List A                                                □

  private

    @0 to-Queue↔Listⁱ-, : _↔_.to Queue↔Listⁱ q ≡ ⌊ q ⌋
    to-Queue↔Listⁱ-, = refl _

  -- The forward directions of Queue↔List and Queue↔Listⁱ match.

  @0 to-Queue↔List : _↔_.to (Queue↔List s) q ≡ _↔_.to Queue↔Listⁱ q
  to-Queue↔List = ≡⌊⌋

  -- Variants of Queue↔List and Queue↔Listⁱ.

  Maybe[×Queue]↔List :
    Very-stableᴱ-≡ A →
    Maybe (A × Queue Q A) ↔ List A
  Maybe[×Queue]↔List {A = A} s =
    Maybe (A × Queue Q A)  ↝⟨ F.id ⊎-cong F.id ×-cong Queue↔List s ⟩
    Maybe (A × List A)     ↝⟨ inverse List↔Maybe[×List] ⟩□
    List A                 □

  @0 Maybe[×Queue]↔Listⁱ :
    Maybe (A × Queue Q A) ↔ List A
  Maybe[×Queue]↔Listⁱ {A = A} =
    Maybe (A × Queue Q A)  ↝⟨ F.id ⊎-cong F.id ×-cong Queue↔Listⁱ ⟩
    Maybe (A × List A)     ↝⟨ inverse List↔Maybe[×List] ⟩□
    List A                 □

  @0 to-Maybe[×Queue]↔List :
    ∀ xs →
    _↔_.to (Maybe[×Queue]↔List s) xs ≡
    _↔_.to Maybe[×Queue]↔Listⁱ xs
  to-Maybe[×Queue]↔List {s = s} xs =
    _↔_.from List↔Maybe[×List]
      (⊎-map id (Σ-map id (_↔_.to (Queue↔List s))) xs)  ≡⟨ cong (λ f → _↔_.from List↔Maybe[×List] (⊎-map id (Σ-map id f) xs)) (⟨ext⟩ λ _ →
                                                           to-Queue↔List) ⟩∎
    _↔_.from List↔Maybe[×List]
      (⊎-map id (Σ-map id (_↔_.to Queue↔Listⁱ)) xs)     ∎

  -- A lemma that can be used to prove "to-List lemmas".

  ⌊⌋≡→to-List≡ :
    Erased (⌊ q ⌋ ≡ xs) →
    to-List s q ≡ xs
  ⌊⌋≡→to-List≡ {q = q} {xs = xs} {s = s} eq =
    to-List s q               ≡⟨ cong (to-List _) (_↔_.to ≡-for-indices↔≡ eq) ⟩
    to-List s (from-List xs)  ≡⟨ _↔_.right-inverse-of (Queue↔List _) _ ⟩∎
    xs                        ∎

------------------------------------------------------------------------
-- Some queue operations, implemented for Queue ⟪_⟫

  module Indexed where

    abstract

      private

        -- A helper function that can be used to define unary
        -- functions on queues.

        unary :
          {A : Type a} {B : Type b}
          {@0 xs : List A} {@0 f : List A → List B}
          (g : Q A → Q B) →
          @0 (∀ {q} → Q.to-List _ (g q) ≡ f (Q.to-List _ q)) →
          Queue Q ⟪ xs ⟫ → Queue Q ⟪ f xs ⟫
        unary {xs = xs} {f = f} g hyp = Trunc.rec
          truncation-is-proposition
          (uncurry λ q p →
             ∣ g q
             , [ Q.to-List _ (g q)  ≡⟨ hyp ⟩
                 f (Q.to-List _ q)  ≡⟨ cong f (erased p) ⟩∎
                 f xs               ∎
               ]
             ∣)

      -- Enqueues an element.

      enqueue :
        {@0 xs : List A}
        (x : A) → Queue Q ⟪ xs ⟫ → Queue Q ⟪ xs ++ x ∷ [] ⟫
      enqueue x = unary (Q.enqueue x) Q.to-List-enqueue

      -- A map function.

      map :
        {@0 xs : List A} →
        (f : A → B) → Queue Q ⟪ xs ⟫ → Queue Q ⟪ L.map f xs ⟫
      map f = unary (Q.map f) Q.to-List-map

    -- The result of trying to dequeue an element from an indexed
    -- queue.
    --
    -- TODO: Perhaps it makes sense to make Q an explicit argument of
    -- this definition.

    Result-⟪_⟫ : {A : Type a} → @0 List A → Type a
    Result-⟪_⟫ {A = A} xs =
      ∃ λ (q : Maybe (A × Queue Q A)) →
        Erased (_↔_.to Maybe[×Queue]↔Listⁱ q ≡ xs)

    -- If equality is very stable (with erased proofs) for A, then
    -- Result-⟪ xs ⟫ is a proposition for lists xs of type List A.

    Result-⟪⟫-propositional :
      {@0 xs : List A} →
      Very-stableᴱ-≡ A →
      Is-proposition Result-⟪ xs ⟫
    Result-⟪⟫-propositional {A = A} {xs = xs} s =
                                            $⟨ erased-singleton-with-erased-center-propositional (Very-stableᴱ-≡-List 0 s) ⟩
      Is-proposition (Erased-singleton xs)  ↝⟨ H-level-cong _ 1 (inverse lemma) ⦂ (_ → _) ⟩□
      Is-proposition Result-⟪ xs ⟫          □
      where
      lemma : _ ↔ _
      lemma =
        Result-⟪ xs ⟫                                       ↔⟨⟩

        (∃ λ (ys : Maybe (A × Queue Q A)) →
           Erased (_↔_.to Maybe[×Queue]↔Listⁱ ys ≡ xs))     ↝⟨ ∃-cong (λ ys → Erased-cong (≡⇒↝ _ $ cong (_≡ xs) $ sym $
                                                               to-Maybe[×Queue]↔List ys)) ⟩
        (∃ λ (ys : Maybe (A × Queue Q A)) →
           Erased (_↔_.to (Maybe[×Queue]↔List s) ys ≡ xs))  ↝⟨ Σ-cong (Maybe[×Queue]↔List s) (λ _ → F.id) ⟩

        (∃ λ (ys : List A) → Erased (ys ≡ xs))              ↔⟨⟩

        Erased-singleton xs                                 □

    abstract

      -- Dequeuing.

      dequeue :
        {@0 xs : List A} →
        Very-stableᴱ-≡ A →
        Queue Q ⟪ xs ⟫ →
        Result-⟪ xs ⟫
      dequeue {xs = xs} s = Trunc.rec
        (Result-⟪⟫-propositional s)
        (λ (q , [ eq ]) →

             ⊎-map id (Σ-map id λ q → _ , ∣ q , [ refl _ ] ∣)
               (Q.dequeue _ q)

           , [ _↔_.to Maybe[×Queue]↔Listⁱ
                 (⊎-map id (Σ-map id (λ q → _ , ∣ q , [ refl _ ] ∣))
                    (Q.dequeue _ q))                                     ≡⟨⟩

               _↔_.from List↔Maybe[×List]
                 (⊎-map id (Σ-map id (_↔_.to Queue↔Listⁱ))
                    (⊎-map id (Σ-map id (λ q → _ , ∣ q , [ refl _ ] ∣))
                       (Q.dequeue _ q)))                                 ≡⟨ cong (_↔_.from List↔Maybe[×List]) $ sym $ ⊎-map-∘ (Q.dequeue _ q) ⟩

               _↔_.from List↔Maybe[×List]
                 (⊎-map id (Σ-map id (Q.to-List _)) (Q.dequeue _ q))     ≡⟨ cong (_↔_.from List↔Maybe[×List]) $ Q.to-List-dequeue {q = q} ⟩

               _↔_.from List↔Maybe[×List]
                 (_↔_.to List↔Maybe[×List] (Q.to-List _ q))              ≡⟨ _↔_.left-inverse-of List↔Maybe[×List] _ ⟩

               Q.to-List _ q                                             ≡⟨ eq ⟩∎

               xs                                                        ∎
             ])

      -- The inverse of the dequeue operation. This operation does not
      -- depend on stability.

      dequeue⁻¹ :
        {@0 xs : List A} →
        Result-⟪ xs ⟫ → Queue Q ⟪ xs ⟫
      dequeue⁻¹ {xs = xs} (nothing , eq) =
        ∣ Q.empty
        , [ Q.to-List _ (Q.empty ⦂ Q _)  ≡⟨ Q.to-List-empty ⟩
            []                           ≡⟨ erased eq ⟩∎
            xs                           ∎
          ]
        ∣
      dequeue⁻¹ {xs = xs} (just (x , ys , q) , eq) =
        ∥∥-map (Σ-map (Q.cons x)
                      (λ {q′} → Erased-cong λ eq′ →
                                  Q.to-List _ (Q.cons x q′)  ≡⟨ Q.to-List-cons ⟩
                                  x ∷ Q.to-List _ q′         ≡⟨ cong (x ∷_) eq′ ⟩
                                  x ∷ erased ys              ≡⟨ erased eq ⟩∎
                                  xs                         ∎))
               q

    -- The dequeue and dequeue⁻¹ operations are inverses.

    Queue-⟪⟫↔Result-⟪⟫ :
      {@0 xs : List A} →
      Very-stableᴱ-≡ A →
      Queue Q ⟪ xs ⟫ ↔ Result-⟪ xs ⟫
    Queue-⟪⟫↔Result-⟪⟫ s = record
      { surjection = record
        { logical-equivalence = record
          { to   = dequeue s
          ; from = dequeue⁻¹
          }
        ; right-inverse-of = λ _ → Result-⟪⟫-propositional s _ _
        }
      ; left-inverse-of = λ _ → Queue-⟪⟫-propositional _ _
      }

------------------------------------------------------------------------
-- Some queue operations, implemented for Queue

  -- Note that none of these operations are abstract.

  module Non-indexed where

    -- Enqueues an element.

    enqueue : A → Queue Q A → Queue Q A
    enqueue x = Σ-map _ (Indexed.enqueue x)

    to-List-enqueue : to-List s (enqueue x q) ≡ to-List s q ++ x ∷ []
    to-List-enqueue {s = s} {x = x} {q = q} = ⌊⌋≡→to-List≡
      [ ⌊ q ⌋ ++ x ∷ []        ≡⟨ cong (_++ _) $ sym ≡⌊⌋ ⟩∎
        to-List s q ++ x ∷ []  ∎
      ]

    -- A map function.

    map : (A → B) → Queue Q A → Queue Q B
    map f = Σ-map _ (Indexed.map f)

    to-List-map : to-List s₁ (map f q) ≡ L.map f (to-List s₂ q)
    to-List-map {f = f} {q = q} {s₂ = s₂} = ⌊⌋≡→to-List≡
      [ L.map f ⌊ q ⌋           ≡⟨ cong (L.map f) $ sym ≡⌊⌋ ⟩∎
        L.map f (to-List s₂ q)  ∎
      ]

    private

      -- A variant of the result of the dequeue operation.

      Result : Type a → Type a
      Result A =
        ∃ λ (xs : Erased (List A)) → Indexed.Result-⟪ erased xs ⟫

      -- Conversion lemmas for Result.

      Result↠Maybe[×Queue] : Result A ↠ Maybe (A × Queue Q A)
      Result↠Maybe[×Queue] = record
        { logical-equivalence = record
          { to   = proj₁ ∘ proj₂
          ; from = λ q → _ , q , [ refl _ ]
          }
        ; right-inverse-of = refl
        }

      Result↔Maybe[×Queue] :
        Very-stableᴱ-≡ A →
        Result A ↔ Maybe (A × Queue Q A)
      Result↔Maybe[×Queue] s = record
        { surjection      = Result↠Maybe[×Queue]
        ; left-inverse-of = λ r →               $⟨ from∘to r ⟩
            Erased (⌊ from (to r) ⌋ʳ ≡ ⌊ r ⌋ʳ)  ↝⟨ Erased-≡↔[]≡[] ⟩
            proj₁ (from (to r)) ≡ proj₁ r       ↝⟨ ignore-propositional-component (Indexed.Result-⟪⟫-propositional s) ⟩□
            from (to r) ≡ r                     □
        }
        where
        open _↠_ Result↠Maybe[×Queue]

        @0 ⌊_⌋ʳ : Result A → List A
        ⌊_⌋ʳ = erased ∘ proj₁

        from∘to : ∀ r → Erased (⌊ from (to r) ⌋ʳ ≡ ⌊ r ⌋ʳ)
        from∘to (_ , _ , eq) = eq

    -- Queue Q A is isomorphic to Maybe (A × Queue Q A), assuming that
    -- equality is very stable (with erased proofs) for A.

    Queue↔Maybe[×Queue] :
      Very-stableᴱ-≡ A →
      Queue Q A ↔ Maybe (A × Queue Q A)
    Queue↔Maybe[×Queue] {A = A} s =
      Queue Q A              ↝⟨ ∃-cong (λ _ → Indexed.Queue-⟪⟫↔Result-⟪⟫ s) ⟩
      Result A               ↝⟨ Result↔Maybe[×Queue] s ⟩□
      Maybe (A × Queue Q A)  □

    mutual

      -- The inverse of the dequeue operation. This operation does not
      -- depend on stability.

      dequeue⁻¹ : Maybe (A × Queue Q A) → Queue Q A
      dequeue⁻¹ q = _  -- Agda can infer the definition.

      _ : _↔_.from (Queue↔Maybe[×Queue] s) ≡ dequeue⁻¹
      _ = refl _

    to-List-dequeue⁻¹ :
      to-List s (dequeue⁻¹ x) ≡
      _↔_.from List↔Maybe[×List] (⊎-map id (Σ-map id (to-List s)) x)
    to-List-dequeue⁻¹ {x = nothing} = ⌊⌋≡→to-List≡ [ refl _ ]

    to-List-dequeue⁻¹ {s = s} {x = just (x , q)} = ⌊⌋≡→to-List≡
      [ x ∷ ⌊ q ⌋        ≡⟨ cong (_ ∷_) $ sym ≡⌊⌋ ⟩∎
        x ∷ to-List s q  ∎
      ]

    -- Dequeues an element, if possible.

    dequeue : Very-stableᴱ-≡ A → Queue Q A → Maybe (A × Queue Q A)
    dequeue s = _↔_.to (Queue↔Maybe[×Queue] s)

    to-List-dequeue :
      ⊎-map id (Σ-map id (to-List s)) (dequeue s q) ≡
      _↔_.to List↔Maybe[×List] (to-List s q)
    to-List-dequeue {s = s} {q = q} =
      ⊎-map id (Σ-map id (to-List s)) (dequeue s q)                   ≡⟨ _↔_.to (from≡↔≡to (from-isomorphism List↔Maybe[×List])) $
                                                                         sym to-List-dequeue⁻¹ ⟩
      _↔_.to List↔Maybe[×List] (to-List s (dequeue⁻¹ (dequeue s q)))  ≡⟨ cong (_↔_.to List↔Maybe[×List] ∘ to-List s) $
                                                                         _↔_.left-inverse-of (Queue↔Maybe[×Queue] _) _ ⟩∎
      _↔_.to List↔Maybe[×List] (to-List s q)                          ∎

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


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

{- INDEX: Some constructions with non-recursive HITs,
   and related results.

   This formalization covers the hardest results of my
   paper titled "Constructions with non-recursive HITs".
   To be precise: I have formalized the result that all
   functions in the sequence of approximations (see Section 6)
   are weakly constant, and that the colimit is thus
   propositional. This requires a lot of lemmas. Some of
   these lemmas are trivial on paper and only tedious in Agda,
   but many lemmas are (at least for me) even on paper far
   from trivial.

   Formalized are Section 2, Section 3 (without the example
   applications), especially the first main result; all of
   Section 4 except Lemma 4.9, the definitions and principles
   of Section 5, all of Section 6 expect the last corollaries.

   The parts of the paper that are not formalized are
   (A) the examples in Section 3
   (B) the statements of remarks
   (C) Lemma 4.9, 5.4, 5.5, and 5.6
   (D) Theorem 5.7, Corollary 5.8, Theorem 6.2
   (E) the discussions and results in the concluding Section 7

   All of these are relatively easy compared with the results
   that are formalized. The items in (C) could be implemented
   easily, but are not very interesting on their own.
   The same is true for the second and third item in (D),
   which however depend on Theorem 5.7.
   Theorem 5.7 itself could be interesting to formalize.
   However, it relies on the main result of
       Capriotti, Kraus, Vezzosi,
       "Functions out of Higher Truncations".
   This result is formalized, but unfortunately in another
   library; thus, we omit Theorem 5.7 (for now) in the current
   formalization. (E) would require (D) first.

   This development type-checks with Agda 2.4.2.5 and similar
   versions (I assume with 2.4.2.x in general; same as the
   HoTT library).
-}

module nicolai.pseudotruncations.NONRECURSIVE-INDEX where

{- Some preliminary definitions/lemmas, and an explanation
   why we need to work with the spheres defined by suspension-
   iteration of the form
   Σ¹⁺ⁿ :≡ Σⁿ ∘ Σ -}
open import nicolai.pseudotruncations.Preliminary-definitions
open import nicolai.pseudotruncations.Liblemmas

{- SECTION 2
   The Sequential colimit. I am aware that there is some
   overlap with lib/types/NatColim.agda -}
open import nicolai.pseudotruncations.SeqColim

{- Here is some prepartion for Section 3 -}
open import nicolai.pseudotruncations.wconst-preparation

{- The rather lengthy argument that some heptagon commutes;
   very tedious; this is still preparation for Section 3 -}
open import nicolai.pseudotruncations.heptagon

{- SECTION 3 (without the sample applications)
   One result of the paper: If we have a sequence of weakly
   constant functions, then the colimit is propositional -}
open import nicolai.pseudotruncations.wconstSequence

{- SECTION 4
   The correspondance between loops and maps from spheres:
   a lot of tedious technical content. This was hard work for me!
   The results are in two files; first, essentially the fact that
   the 'pointed' 0-sphere [i.e. (bool, true)] is "as good as"
   the unit type if we consider pointed maps out of it.
   Second, the main lemmas. -}
open import nicolai.pseudotruncations.pointed-O-Sphere
open import nicolai.pseudotruncations.LoopsAndSpheres

{- SECTION 5 (mainly the definition and some auxiliary lemmas)
   Definition of pseudo-truncations -}
open import nicolai.pseudotruncations.PseudoTruncs

{- SECTION 6
   The sequence of approximations with increasing "connectedness-
   level", and the proof that every map is weakly constant,
   and the corollary that its colimit is propositional. -}
open import nicolai.pseudotruncations.PseudoTruncs-wconst-seq

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


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

open import Prelude hiding (A; B)
open import Categories

module Categories.Pushout {ℓ₁ ℓ₂} (C : Category ℓ₁ ℓ₂) where

open Category C

private
  variable
    A B : Ob
    h₁ h₂ j : A ⟶ B

record Pushout (f : X ⟶ Y) (g : X ⟶ Z) : Type (ℓ₁ ℓ⊔ ℓ₂) where
  field
    {Q} : Ob
    i₁ : Y ⟶ Q
    i₂ : Z ⟶ Q
    commute : i₁ · f ≡ i₂ · g
    universal : h₁ · f ≡ h₂ · g → Q ⟶ Codomain h₁
    unique : ∀ {eq : h₁ · f ≡ h₂ · g} →
             j · i₁ ≡ h₁ → j · i₂ ≡ h₂ →
             j ≡ universal eq

    universal·i₁≡h₁  : ∀ {eq : h₁ · f ≡ h₂ · g} →
                         universal eq · i₁ ≡ h₁
    universal·i₂≡h₂  : ∀ {eq : h₁ · f ≡ h₂ · g} →
                         universal eq · i₂ ≡ h₂

HasPushouts : Type (ℓ₁ ℓ⊔ ℓ₂)
HasPushouts = ∀ {X Y Z} → (f : X ⟶ Y) → (g : X ⟶ Z) → Pushout f g

max_stars_repo_name: oisdk/combinatorics-paper

max_issues_repo_name: oisdk/combinatorics-paper

max_forks_repo_name: oisdk/combinatorics-paper


text:
-- Andreas, 2016-02-02

module _ where

  data Q : Set where
    a : Q

  data Overlap : Set where
    a : Overlap

  postulate helper : ∀ {T : Set} → (T → T) → Set

  test₃ : Set
  test₃ = helper λ { a → a }

-- Does not succeed, as the type of the extended lambda is ambiguous.
-- It should fail with an error or unsolved metas instead of
-- looping the type checker.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Issue756a where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

data T : Nat → Set where
  [_] : ∀ n → T n

bad : ∀ n → T n → Nat
bad .zero                   [ zero  ] = zero
bad .(suc (let x = n in x)) [ suc n ] = zero


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

module Agda.Builtin.List where

infixr 5 _∷_
data List {a} (A : Set a) : Set a where
  []  : List A
  _∷_ : (x : A) (xs : List A) → List A

{-# BUILTIN LIST List #-}
{-# BUILTIN NIL  []   #-}
{-# BUILTIN CONS _∷_  #-}

{-# HASKELL type AgdaList a b = [b] #-}

{-# COMPILED_DATA List MAlonzo.Code.Agda.Builtin.List.AgdaList [] (:) #-}
{-# COMPILED_DATA_UHC List __LIST__ __NIL__ __CONS__ #-}
{-# COMPILED_JS List function(x,v) {
  if (x.length < 1) { return v["[]"](); } else { return v["_∷_"](x[0], x.slice(1)); }
} #-}
{-# COMPILED_JS [] Array() #-}
{-# COMPILED_JS _∷_ function (x) { return function(y) { return Array(x).concat(y); }; } #-}

max_stars_repo_name: pthariensflame/agda

max_issues_repo_name: pthariensflame/agda

max_forks_repo_name: pthariensflame/agda


text:
-- Andreas, 2015-07-07 continuation of issue 665

{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc.with.strip:60 -v tc.lhs:10 #-}

postulate
  C : Set
  anything : C

record I : Set where
  constructor c
  field
    f : C

data Wrap : (j : I) → Set where
  wrap : ∀ {j} → Wrap j

works1 : ∀ {j} → Wrap j → C
works1 {c ._} (wrap {c x}) with anything
... | z = z

works2 : ∀ {j} → Wrap j → C
works2 (wrap {_}) with anything
... | z = z

works3 : ∀ {j} → Wrap j → C
works3 wrap with anything
... | z = z

works : ∀ {j} → Wrap j → C
works {c _} (wrap {c ._}) with anything
works {c _} (wrap .{c _}) | z = z

-- The following should not pass, but issue 142 is hard to fix
-- with the current infrastructure for with-clauses.
-- Not many attempts have been made since 2009, and none succeeded.
issue142 : ∀ {j} → Wrap j → C
issue142 {c _} (wrap {c ._}) with anything
issue142 {c _} (wrap .{c anything}) | z = z

test : ∀ {j} → Wrap j → C
test {c _} (wrap {c ._}) with anything
test {c _} (wrap {c ._}) | z = z

test' : ∀ {j} → Wrap j → C
test' {c _} (wrap {c ._}) with anything
... | z = z

-- ERROR WAS::
-- Inaccessible (dotted) patterns from the parent clause must also be
-- inaccessible in the with clause, when checking the pattern {c ._},
-- when checking that the clause
-- test {c _} (wrap {c ._}) with anything
-- test {c _} (wrap {c ._}) | z = z
-- has type {j : I} → Wrap j → C

works1a : ∀ {j} → Wrap j → C
works1a {c ._} (wrap {c x}) with anything
works1a {c ._} (wrap {c x}) | z = z

works1b : ∀ {j} → Wrap j → C
works1b {c ._} (wrap {c x}) with anything
works1b .{c _} (wrap {c x}) | z = z

-- ERROR WAS:
-- With clause pattern .(c _) is not an instance of its parent pattern
-- (c .(Var 0 []) : {I})
-- when checking that the clause
-- works1b {c ._} (wrap {c _}) with anything
-- works1b {.(c _)} (wrap {c _}) | z = z
-- has type {j : I} → Wrap j → C

-- should pass


text:
open import Prelude hiding (begin_; step-≡; _∎)

module MJ.Classtable.Core (c : ℕ) where

open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×-≟_)
open import Data.List
open import Data.List.Membership.Propositional
open import Data.List.Relation.Binary.Pointwise using (decidable-≡)
open import Relation.Binary
open import Data.Vec
open import Data.Maybe
open import Data.String

open import Relation.Binary using (Decidable)

open import MJ.Types as Types

{-
To model that a class may define both field and methods in a uniform manner, we
choose to introduce two namespaces.
-}
data NS : Set where
  METHOD : NS
  FIELD  : NS

typing : NS → Set
typing METHOD = Sig c
typing FIELD = Ty c

-- decidable equality on typings
_typing-≟_ : ∀ {ns} → Decidable (_≡_ {A = typing ns})
_typing-≟_ {METHOD} = (decidable-≡ Types._≟_) ×-≟ Types._≟_
_typing-≟_ {FIELD}  = Types._≟_

{-
We choose to make parent declarations obligatory and have a distinguished class
identifier Object in which inheritance chains find their foundation.

The field constr of this record provides access to the constructor parameter types.

The field decls returns a list of named members for each namespace, where the
type of the member is namespace-dependent. The uniformity of member definitions
permits a notion of membership that works for both fields and methods:
-}
record Class : Set where
  constructor class
  field
    parent  : Cid c
    constr  : List (Ty c) -- argument types
    decls   : (ns : NS) → List (String × typing ns)

ObjectClass = class Object [] (λ _ → [])

{-
Conceptually a class table stores the types of all members of all classes.
It is modeled by a total function from class identifiers to instances of
a record Class.
-}
PreClasstable = Cid c → Class

{-
We can define inheritance as the transitive closure of a step relation
between class identifiers under a given classtable Σ:
-}
data _⊢_<:ₛ_ (Σ : PreClasstable) : Cid c → Cid c → Set where
  super : ∀ {cid} → Σ ⊢ cls cid <:ₛ (Class.parent (Σ (cls cid)))

open import Data.Star
_⊢_<:_ : (Σ : PreClasstable)(cid : Cid c) → (pid : Cid c) → Set
_⊢_<:_ Σ = Star (_⊢_<:ₛ_ Σ)

{-
We'll restrict classtables to those that satisfy three properties:

- founded: says that Object is at the base of sub-typing
- rooted: says that every class inherits from Object
- Σ-object: gives meaning to the distinguished Object class identifier
-}
record Classtable : Set where
  field
    Σ        : PreClasstable
    founded  : Class.parent (Σ Object) ≡ Object
    rooted   : ∀ C → Σ ⊢ C <: Object
    Σ-Object : Σ Object ≡ ObjectClass

  _<∶_ : ∀ (cid pid : Cid c) → Set
  a <∶ b = Σ ⊢ a <: b

  open import Relation.Binary
  open import Data.Nat.Properties

  {-
  We can show that the subtyping relation is indeed reflexive and transitive
  -}
  <:-reflexive  : Reflexive (_⊢_<:_ Σ)
  <:-reflexive  = ε

  <:-transitive : Transitive (_⊢_<:_ Σ)
  <:-transitive = _◅◅_

  {-
  From the axioms of the classtable we can derive the important properties
  that cyclic inheritance is impossible and that consequently inheritance
  proofs are unique.

  The proof is slightly involved because we have to make sure that Agda
  believes that it is total.
  -}
  private
    len : ∀ {c p} → Σ ⊢ c <: p → ℕ
    len ε = 0
    len (x ◅ px) = suc $ len px

    len-◅◅ : ∀ {c p p'}(s : Σ ⊢ c <: p)(s' : Σ ⊢ p <: p') → len (s ◅◅ s') ≡ len s + len s'
    len-◅◅ ε _ = refl
    len-◅◅ (x ◅ s) s' rewrite len-◅◅ s s' = refl

    lem-len : ∀ {c p}(px : Σ ⊢ c <: p)(qx : Σ ⊢ c <: Object) → len px ≤ len qx
    lem-len ε ε = z≤n
    lem-len ε (x ◅ qx) = z≤n
    lem-len (() ◅ px) ε
    lem-len (super ◅ px) (super ◅ qx) = s≤s (lem-len px qx)

    open ≤-Reasoning

    -- generate an inheritance proof of arbitrary length,
    -- given an inheritance proof from a parent to a child
    lem-inf : ∀ c → Σ ⊢ Class.parent (Σ (cls c)) <: (cls c) → ∀ n → ∃ λ (px : Σ ⊢ (cls c) <: (cls c)) → len px > n
    lem-inf c px n with helper px n
      where
        helper : (p : Σ ⊢ Class.parent (Σ (cls c)) <: (cls c)) → ∀ gap → ∃ λ (px : Σ ⊢ (cls c) <: (cls c)) → len px ≥ gap + len p
        helper p zero = (super ◅ p) , ≤-step ≤-refl
        helper p (suc gap) with gap ≤? len p
        ... | yes q = (super ◅ p ◅◅ (super ◅ p)) , s≤s (begin
            (gap + len p)
              ≤⟨ +-mono-≤ q (≤-step ≤-refl) ⟩
            len p + (suc (len p))
              ≡⟨ sym (len-◅◅ p (super ◅ p)) ⟩
            len (p ◅◅ super ◅ p)
          ∎)
        ... | no ¬q with helper (p ◅◅ (super ◅ p)) gap
        ... | z , q = z , (begin
            suc (gap + len p)
              ≡⟨ sym $ m+n+o≡n+m+o gap 1 (len p) ⟩
            gap + (len (super ◅ p))
              ≤⟨ +-mono-≤ { gap } ≤-refl (≤-stepsˡ (len p) ≤-refl) ⟩
            gap + (len p + len (super ◅ p))
              ≡⟨ cong (_+_ gap) (sym $ len-◅◅ p (super ◅ p)) ⟩
            gap + (len (p ◅◅ (super ◅ p)))
              ≤⟨ q ⟩
            len z ∎)
          where open import Data.Nat.Properties.Extra
    ... | py , z = super ◅ px ◅◅ py , s≤s (subst (_≤_ n) (sym $ len-◅◅ px py) (≤-stepsˡ (len px) (m+n≤o⇒m≤o n z)))

  -- Proves that a parent can't inherit from it's children,
  Σ-acyclic : ∀ c → ¬ Σ ⊢ Class.parent (Σ (cls c)) <: (cls c)
  Σ-acyclic c px with lem-inf c px (len $ rooted (cls c))
  ... | qx , impossible with lem-len qx (rooted (cls c))
  ... | z = ⊥-elim (<⇒≱ impossible z)

  -- Trivially we have that Object cannot inherit from any class
  ¬Object<:x : ∀ {cid} → ¬ Σ ⊢ Object <: cls cid
  ¬Object<:x (() ◅ p)

  -- Using acyclicity we can show that inheritance proofs are unique
  <:-unique : ∀ {c p} → (l r : Σ ⊢ c <: p) → l ≡ r
  <:-unique ε ε = refl
  <:-unique ε ch@(super ◅ r) = ⊥-elim (Σ-acyclic _ r)
  <:-unique ch@(super ◅ l) ε = ⊥-elim (Σ-acyclic _ l)
  <:-unique (super ◅ l) (super ◅ r) with <:-unique l r
  ... | refl = refl


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Homogeneously-indexed binary relations
------------------------------------------------------------------------

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

module Relation.Binary.Indexed.Homogeneous where

------------------------------------------------------------------------
-- Publicly export core definitions

open import Relation.Binary.Indexed.Homogeneous.Core public
open import Relation.Binary.Indexed.Homogeneous.Definitions public
open import Relation.Binary.Indexed.Homogeneous.Structures public
open import Relation.Binary.Indexed.Homogeneous.Bundles public

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 0.17

REL = IREL
{-# WARNING_ON_USAGE REL
"Warning: REL was deprecated in v0.17.
Please use IREL instead."
#-}
Rel = IRel
{-# WARNING_ON_USAGE Rel
"Warning: Rel was deprecated in v0.17.
Please use IRel instead."
#-}


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

open import HoTT

{- The pseudo-adjoint functors F,G : Ptd → Ptd
 - It stops at composition and ignores
 - all the higher associahedrons.
 -}

module homotopy.PtdAdjoint where

record PtdFunctor i j : Type (lsucc (lmax i j)) where
  field
    obj : Ptd i → Ptd j
    arr : {X Y : Ptd i} → fst (X ⊙→ Y) → fst (obj X ⊙→ obj Y)
    id : (X : Ptd i) → arr (⊙idf X) == ⊙idf (obj X)
    comp : {X Y Z : Ptd i} (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y))
      → arr (g ⊙∘ f) == arr g ⊙∘ arr f

{- counit-unit description of F ⊣ G -}
record CounitUnitAdjoint {i j} (F : PtdFunctor i j) (G : PtdFunctor j i)
  : Type (lsucc (lmax i j)) where

  private
    module F = PtdFunctor F
    module G = PtdFunctor G

  field
    η : (X : Ptd i) → fst (X ⊙→ G.obj (F.obj X))
    ε : (U : Ptd j) → fst (F.obj (G.obj U) ⊙→ U)

    η-natural : {X Y : Ptd i} (h : fst (X ⊙→ Y))
      → η Y ⊙∘ h == G.arr (F.arr h) ⊙∘ η X
    ε-natural : {U V : Ptd j} (k : fst (U ⊙→ V))
      → ε V ⊙∘ F.arr (G.arr k) == k ⊙∘ ε U

    εF-Fη : (X : Ptd i) → ε (F.obj X) ⊙∘ F.arr (η X) == ⊙idf (F.obj X)
    Gε-ηG : (U : Ptd j) → G.arr (ε U) ⊙∘ η (G.obj U) == ⊙idf (G.obj U)

{- hom-set isomorphism description of F ⊣ G -}
record HomAdjoint {i j} (F : PtdFunctor i j) (G : PtdFunctor j i)
  : Type (lsucc (lmax i j)) where

  private
    module F = PtdFunctor F
    module G = PtdFunctor G

  field
    eq : (X : Ptd i) (U : Ptd j) → fst (F.obj X ⊙→ U) ≃ fst (X ⊙→ G.obj U)

    nat-dom : {X Y : Ptd i} (h : fst (X ⊙→ Y)) (U : Ptd j)
      (r : fst (F.obj Y ⊙→ U))
      → –> (eq Y U) r ⊙∘ h == –> (eq X U) (r ⊙∘ F.arr h)

    nat-cod : (X : Ptd i) {U V : Ptd j} (k : fst (U ⊙→ V))
      (r : fst (F.obj X ⊙→ U))
      → G.arr k ⊙∘ –> (eq X U) r == –> (eq X V) (k ⊙∘ r)

  nat!-dom : {X Y : Ptd i} (h : fst (X ⊙→ Y)) (U : Ptd j)
    (s : fst (Y ⊙→ G.obj U))
    → <– (eq Y U) s ⊙∘ F.arr h == <– (eq X U) (s ⊙∘ h)
  nat!-dom {X} {Y} h U s =
    ! (<–-inv-l (eq X U) (<– (eq Y U) s ⊙∘ F.arr h))
    ∙ ap (<– (eq X U)) (! (nat-dom h U (<– (eq Y U) s)))
    ∙ ap (λ w → <– (eq X U) (w ⊙∘ h)) (<–-inv-r (eq Y U) s)

  nat!-cod : (X : Ptd i) {U V : Ptd j} (k : fst (U ⊙→ V))
    (s : fst (X ⊙→ G.obj U))
    → k ⊙∘ <– (eq X U) s == <– (eq X V) (G.arr k ⊙∘ s)
  nat!-cod X {U} {V} k s =
    ! (<–-inv-l (eq X V) (k ⊙∘ <– (eq X U) s))
    ∙ ap (<– (eq X V)) (! (nat-cod X k (<– (eq X U) s)))
    ∙ ap (λ w → <– (eq X V) (G.arr k ⊙∘ w)) (<–-inv-r (eq X U) s)

counit-unit-to-hom : ∀ {i j} {F : PtdFunctor i j} {G : PtdFunctor j i}
  → CounitUnitAdjoint F G → HomAdjoint F G
counit-unit-to-hom {i} {j} {F} {G} adj = record {
  eq = eq;
  nat-dom = nat-dom;
  nat-cod = nat-cod}
  where
  module F = PtdFunctor F
  module G = PtdFunctor G
  open CounitUnitAdjoint adj

  module _ (X : Ptd i) (U : Ptd j) where

    into : fst (F.obj X ⊙→ U) → fst (X ⊙→ G.obj U)
    into r = G.arr r ⊙∘ η X

    out : fst (X ⊙→ G.obj U) → fst (F.obj X ⊙→ U)
    out s = ε U ⊙∘ F.arr s

    into-out : (s : fst (X ⊙→ G.obj U)) → into (out s) == s
    into-out s =
      G.arr (ε U ⊙∘ F.arr s) ⊙∘ η X
        =⟨ G.comp (ε U) (F.arr s) |in-ctx (λ w → w ⊙∘ η X) ⟩
      (G.arr (ε U) ⊙∘ G.arr (F.arr s)) ⊙∘ η X
        =⟨ ⊙∘-assoc (G.arr (ε U)) (G.arr (F.arr s)) (η X) ⟩
      G.arr (ε U) ⊙∘ G.arr (F.arr s) ⊙∘ η X
        =⟨ ! (η-natural s) |in-ctx (λ w → G.arr (ε U) ⊙∘ w) ⟩
      G.arr (ε U) ⊙∘ η (G.obj U) ⊙∘ s
        =⟨ ! (⊙∘-assoc (G.arr (ε U)) (η (G.obj U)) s) ⟩
      (G.arr (ε U) ⊙∘ η (G.obj U)) ⊙∘ s
        =⟨ Gε-ηG U |in-ctx (λ w → w ⊙∘ s) ⟩
      ⊙idf (G.obj U) ⊙∘ s
        =⟨ ⊙∘-unit-l s ⟩
      s ∎

    out-into : (r : fst (F.obj X ⊙→ U)) → out (into r) == r
    out-into r =
      ε U ⊙∘ F.arr (G.arr r ⊙∘ η X)
        =⟨ F.comp (G.arr r) (η X) |in-ctx (λ w → ε U ⊙∘ w) ⟩
      ε U ⊙∘ F.arr (G.arr r) ⊙∘ F.arr (η X)
        =⟨ ! (⊙∘-assoc (ε U) (F.arr (G.arr r)) (F.arr (η X))) ⟩
      (ε U ⊙∘ F.arr (G.arr r)) ⊙∘ F.arr (η X)
        =⟨ ε-natural r |in-ctx (λ w → w ⊙∘ F.arr (η X)) ⟩
      (r ⊙∘ ε (F.obj X)) ⊙∘ F.arr (η X)
        =⟨ ⊙∘-assoc r (ε (F.obj X)) (F.arr (η X)) ⟩
      r ⊙∘ ε (F.obj X) ⊙∘ F.arr (η X)
        =⟨ εF-Fη X |in-ctx (λ w → r ⊙∘ w) ⟩
      r ∎

    eq : fst (F.obj X ⊙→ U) ≃ fst (X ⊙→ G.obj U)
    eq = equiv into out into-out out-into

  nat-dom : {X Y : Ptd i} (h : fst (X ⊙→ Y)) (U : Ptd j)
    (r : fst (F.obj Y ⊙→ U))
    → –> (eq Y U) r ⊙∘ h == –> (eq X U) (r ⊙∘ F.arr h)
  nat-dom {X} {Y} h U r =
    (G.arr r ⊙∘ η Y) ⊙∘ h
      =⟨ ⊙∘-assoc (G.arr r) (η Y) h ⟩
    G.arr r ⊙∘ η Y ⊙∘ h
      =⟨ η-natural h |in-ctx (λ w → G.arr r ⊙∘ w) ⟩
    G.arr r ⊙∘ G.arr (F.arr h) ⊙∘ η X
      =⟨ ! (⊙∘-assoc (G.arr r) (G.arr (F.arr h)) (η X)) ⟩
    (G.arr r ⊙∘ G.arr (F.arr h)) ⊙∘ η X
      =⟨ ! (G.comp r (F.arr h)) |in-ctx (λ w → w ⊙∘ η X) ⟩
    G.arr (r ⊙∘ F.arr h) ⊙∘ η X ∎

  nat-cod : (X : Ptd i) {U V : Ptd j} (k : fst (U ⊙→ V))
    (r : fst (F.obj X ⊙→ U))
    → G.arr k ⊙∘ –> (eq X U) r == –> (eq X V) (k ⊙∘ r)
  nat-cod X k r =
    G.arr k ⊙∘ (G.arr r ⊙∘ η X)
      =⟨ ! (⊙∘-assoc (G.arr k) (G.arr r) (η X)) ⟩
    (G.arr k ⊙∘ G.arr r) ⊙∘ η X
      =⟨ ! (G.comp k r) |in-ctx (λ w → w ⊙∘ η X) ⟩
    G.arr (k ⊙∘ r) ⊙∘ η X ∎

{- a right adjoint preserves products -}
module RightAdjoint× {i j} {F : PtdFunctor i j} {G : PtdFunctor j i}
  (adj : HomAdjoint F G) (U V : Ptd j) where

  private
    module F = PtdFunctor F
    module G = PtdFunctor G
    module A = HomAdjoint adj

  ⊙into : fst (G.obj (U ⊙× V) ⊙→ G.obj U ⊙× G.obj V)
  ⊙into = ⊙×-in (G.arr ⊙fst) (G.arr ⊙snd)

  ⊙out : fst (G.obj U ⊙× G.obj V ⊙→ G.obj (U ⊙× V))
  ⊙out = –> (A.eq _ _) (⊙×-in (<– (A.eq _ _) ⊙fst)
                              (<– (A.eq _ _) ⊙snd))

  ⊙into-out : ⊙into ⊙∘ ⊙out == ⊙idf _
  ⊙into-out =
    ⊙×-in (G.arr ⊙fst) (G.arr ⊙snd) ⊙∘ ⊙out
      =⟨ ⊙×-in-pre∘ (G.arr ⊙fst) (G.arr ⊙snd) ⊙out ⟩
    ⊙×-in (G.arr ⊙fst ⊙∘ ⊙out) (G.arr ⊙snd ⊙∘ ⊙out)
      =⟨ ap2 ⊙×-in
           (A.nat-cod _ ⊙fst (⊙×-in (<– (A.eq _ _) ⊙fst) (<– (A.eq _ _) ⊙snd))
            ∙ ap (–> (A.eq _ _))
                 (⊙fst-⊙×-in (<– (A.eq _ _) ⊙fst) (<– (A.eq _ _) ⊙snd))
            ∙ <–-inv-r (A.eq _ _) ⊙fst)
           (A.nat-cod _ ⊙snd (⊙×-in (<– (A.eq _ _) ⊙fst) (<– (A.eq _ _) ⊙snd))
            ∙ ap (–> (A.eq _ _))
                 (⊙snd-⊙×-in (<– (A.eq _ _) ⊙fst) (<– (A.eq _ _) ⊙snd))
            ∙ <–-inv-r (A.eq _ _) ⊙snd) ⟩
    ⊙×-in ⊙fst ⊙snd ∎

  ⊙out-into : ⊙out ⊙∘ ⊙into == ⊙idf _
  ⊙out-into =
    –> (A.eq _ _) (⊙×-in (<– (A.eq _ _) ⊙fst) (<– (A.eq _ _) ⊙snd))
    ⊙∘ ⊙×-in (G.arr ⊙fst) (G.arr ⊙snd)
      =⟨ A.nat-dom (⊙×-in (G.arr ⊙fst) (G.arr ⊙snd)) _
           (⊙×-in (<– (A.eq _ _) ⊙fst) (<– (A.eq _ _) ⊙snd)) ⟩
    –> (A.eq _ _) (⊙×-in (<– (A.eq _ _) ⊙fst) (<– (A.eq _ _) ⊙snd)
    ⊙∘ F.arr (⊙×-in (G.arr ⊙fst) (G.arr ⊙snd)))
      =⟨ ⊙×-in-pre∘ (<– (A.eq _ _) ⊙fst) (<– (A.eq _ _) ⊙snd)
           (F.arr (⊙×-in (G.arr ⊙fst) (G.arr ⊙snd)))
         |in-ctx –> (A.eq _ _) ⟩
    –> (A.eq _ _) (⊙×-in
            (<– (A.eq _ _) ⊙fst ⊙∘ F.arr (⊙×-in (G.arr ⊙fst) (G.arr ⊙snd)))
            (<– (A.eq _ _) ⊙snd ⊙∘ F.arr (⊙×-in (G.arr ⊙fst) (G.arr ⊙snd))))
      =⟨ ap2 (λ f g → –> (A.eq _ _) (⊙×-in f g))
           (A.nat!-dom (⊙×-in (G.arr ⊙fst) (G.arr ⊙snd)) _ ⊙fst
            ∙ ap (<– (A.eq _ _)) (⊙fst-⊙×-in (G.arr ⊙fst) (G.arr ⊙snd))
            ∙ ! (A.nat!-cod _ ⊙fst (⊙idf _)))
           (A.nat!-dom (⊙×-in (G.arr ⊙fst) (G.arr ⊙snd)) _ ⊙snd
            ∙ ap (<– (A.eq _ _)) (⊙snd-⊙×-in (G.arr ⊙fst) (G.arr ⊙snd))
            ∙ ! (A.nat!-cod _ ⊙snd (⊙idf _))) ⟩
    –> (A.eq _ _) (⊙×-in (⊙fst ⊙∘ <– (A.eq _ _) (⊙idf _))
                         (⊙snd ⊙∘ <– (A.eq _ _) (⊙idf _)))
      =⟨ ap (–> (A.eq _ _)) (! (⊙×-in-pre∘ ⊙fst ⊙snd (<– (A.eq _ _) (⊙idf _)))) ⟩
    –> (A.eq _ _) (⊙×-in ⊙fst ⊙snd ⊙∘ <– (A.eq _ _) (⊙idf _))
      =⟨ ⊙∘-unit-l _ |in-ctx –> (A.eq _ _) ⟩
    –> (A.eq _ _) (<– (A.eq _ _) (⊙idf _))
      =⟨ <–-inv-r (A.eq _ _) (⊙idf _) ⟩
    ⊙idf _ ∎

  ⊙eq : G.obj (U ⊙× V) ⊙≃ G.obj U ⊙× G.obj V
  ⊙eq = ⊙≃-in (equiv (fst ⊙into) (fst ⊙out)
                  (app= (ap fst ⊙into-out)) (app= (ap fst ⊙out-into)))
                (snd ⊙into)

  ⊙path = ⊙ua ⊙eq

{- Using the equivalence in RightAdjoint× we get a binary
 - "G.arr2" : (X × Y → Z) → (G X × G Y → G Z)
 - and there is some kind of naturality wrt the (FX→Y)≃(X→GY) equivalence
 - (use case: from ⊙ap we get ⊙ap2) -}
module RightAdjointBinary {i j} {F : PtdFunctor i j} {G : PtdFunctor j i}
  (adj : HomAdjoint F G)
  where

  private
    module F = PtdFunctor F
    module G = PtdFunctor G
    module A = HomAdjoint adj
    module A× = RightAdjoint× adj

  arr2 : {X Y Z : Ptd j}
    → fst (X ⊙× Y ⊙→ Z) → fst (G.obj X ⊙× G.obj Y ⊙→ G.obj Z)
  arr2 {X} {Y} {Z} f = G.arr f ⊙∘ A×.⊙out X Y

  nat-cod : {X : Ptd i} {Y Z W : Ptd j}
    (r₁ : fst (F.obj X ⊙→ Y)) (r₂ : fst (F.obj X ⊙→ Z))
    (o : fst (Y ⊙× Z ⊙→ W))
    → –> (A.eq X W) (o ⊙∘ ⊙×-in r₁ r₂)
      == arr2 o ⊙∘ ⊙×-in (–> (A.eq X Y) r₁) (–> (A.eq X Z) r₂)
  nat-cod {X} {Y} {Z} {W} r₁ r₂ o =
    –> (A.eq X W) (o ⊙∘ ⊙×-in r₁ r₂)
      =⟨ ! (A.nat-cod X o (⊙×-in r₁ r₂)) ⟩
    G.arr o ⊙∘ –> (A.eq X (Y ⊙× Z)) (⊙×-in r₁ r₂)
      =⟨ ! (A×.⊙out-into Y Z)
         |in-ctx (λ w → (G.arr o ⊙∘ w) ⊙∘ –> (A.eq X (Y ⊙× Z)) (⊙×-in r₁ r₂)) ⟩
    (G.arr o ⊙∘ (A×.⊙out Y Z ⊙∘ A×.⊙into Y Z))
    ⊙∘ –> (A.eq X (Y ⊙× Z)) (⊙×-in r₁ r₂)
      =⟨ ⊙∘-assoc-lemma (G.arr o) (A×.⊙out Y Z) (A×.⊙into Y Z)
           (–> (A.eq X (Y ⊙× Z)) (⊙×-in r₁ r₂)) ⟩
    arr2 o ⊙∘ A×.⊙into Y Z ⊙∘ –> (A.eq X (Y ⊙× Z)) (⊙×-in r₁ r₂)
      =⟨ ⊙×-in-pre∘ (G.arr ⊙fst) (G.arr ⊙snd) (–> (A.eq X (Y ⊙× Z)) (⊙×-in r₁ r₂))
         |in-ctx (λ w → arr2 o ⊙∘ w) ⟩
    arr2 o ⊙∘ ⊙×-in (G.arr ⊙fst ⊙∘ –> (A.eq X (Y ⊙× Z)) (⊙×-in r₁ r₂))
                    (G.arr ⊙snd ⊙∘ –> (A.eq X (Y ⊙× Z)) (⊙×-in r₁ r₂))
      =⟨ ap2 (λ w₁ w₂ → arr2 o ⊙∘ ⊙×-in w₁ w₂)
           (A.nat-cod X ⊙fst (⊙×-in r₁ r₂)
            ∙ ap (–> (A.eq X Y)) (⊙fst-⊙×-in r₁ r₂))
           (A.nat-cod X ⊙snd (⊙×-in r₁ r₂)
            ∙ ap (–> (A.eq X Z)) (⊙snd-⊙×-in r₁ r₂)) ⟩
    arr2 o ⊙∘ ⊙×-in (–> (A.eq X Y) r₁) (–> (A.eq X Z) r₂) ∎
    where
    ⊙∘-assoc-lemma : ∀ {i j k l m}
      {X : Ptd i} {Y : Ptd j} {Z : Ptd k} {U : Ptd l} {V : Ptd m}
      (k : fst (U ⊙→ V)) (h : fst (Z ⊙→ U))
      (g : fst (Y ⊙→ Z)) (f : fst (X ⊙→ Y))
      → (k ⊙∘ (h ⊙∘ g)) ⊙∘ f == (k ⊙∘ h) ⊙∘ g ⊙∘ f
    ⊙∘-assoc-lemma (k , idp) (h , idp) (g , idp) (f , idp) = idp

{- a left adjoint preserves wedges -}
module LeftAdjoint∨ {i j} {F : PtdFunctor i j} {G : PtdFunctor j i}
  (adj : HomAdjoint F G) (U V : Ptd i) where

  private
    module F = PtdFunctor F
    module G = PtdFunctor G
    module A = HomAdjoint adj

  module Into = ⊙WedgeRec (F.arr ⊙winl) (F.arr ⊙winr)

  ⊙into : fst (F.obj U ⊙∨ F.obj V ⊙→ F.obj (U ⊙∨ V))
  ⊙into = Into.⊙f

  module OutHelp = ⊙WedgeRec (–> (A.eq _ _) ⊙winl) (–> (A.eq _ _) ⊙winr)

  ⊙out : fst (F.obj (U ⊙∨ V) ⊙→ F.obj U ⊙∨ F.obj V)
  ⊙out = <– (A.eq _ _) OutHelp.⊙f

  ⊙into-out : ⊙into ⊙∘ ⊙out == ⊙idf _
  ⊙into-out =
    ⊙into ⊙∘ ⊙out
      =⟨ A.nat!-cod _ ⊙into (⊙wedge-rec (–> (A.eq _ _) ⊙winl)
                                        (–> (A.eq _ _) ⊙winr)) ⟩
    <– (A.eq _ _) (G.arr ⊙into ⊙∘ ⊙wedge-rec (–> (A.eq _ _) ⊙winl)
                                             (–> (A.eq _ _) ⊙winr))
      =⟨ ap (<– (A.eq _ _)) (⊙wedge-rec-post∘ (G.arr ⊙into)
                              (–> (A.eq _ _) ⊙winl) (–> (A.eq _ _) ⊙winr)) ⟩
    <– (A.eq _ _) (⊙wedge-rec (G.arr ⊙into ⊙∘ –> (A.eq _ _) ⊙winl)
                              (G.arr ⊙into ⊙∘ –> (A.eq _ _) ⊙winr))
      =⟨ ap2 (λ w₁ w₂ → <– (A.eq _ _) (⊙wedge-rec w₁ w₂))
             (A.nat-cod _ ⊙into ⊙winl
              ∙ ap (–> (A.eq _ _)) (Into.⊙winl-β ∙ ! (⊙∘-unit-l _))
              ∙ ! (A.nat-dom ⊙winl _ (⊙idf _)))
             (A.nat-cod _ ⊙into ⊙winr
              ∙ ap (–> (A.eq _ _)) (Into.⊙winr-β ∙ ! (⊙∘-unit-l _))
              ∙ ! (A.nat-dom ⊙winr _ (⊙idf _))) ⟩
    <– (A.eq _ _) (⊙wedge-rec (–> (A.eq _ _) (⊙idf _) ⊙∘ ⊙winl)
                              (–> (A.eq _ _) (⊙idf _) ⊙∘ ⊙winr))
      =⟨ ap (<– (A.eq _ _))
            (! (⊙wedge-rec-post∘ (–> (A.eq _ _) (⊙idf _)) ⊙winl ⊙winr)) ⟩
    <– (A.eq _ _) (–> (A.eq _ _) (⊙idf _) ⊙∘ ⊙wedge-rec ⊙winl ⊙winr)
      =⟨ ap (λ w → <– (A.eq _ _) (–> (A.eq _ _) (⊙idf _) ⊙∘ w))
            ⊙wedge-rec-η ⟩
    <– (A.eq _ _) (–> (A.eq _ _) (⊙idf _))
      =⟨ <–-inv-l (A.eq _ _) (⊙idf _) ⟩
    ⊙idf _ ∎

  ⊙out-into : ⊙out ⊙∘ ⊙into == ⊙idf _
  ⊙out-into =
    ⊙out ⊙∘ ⊙wedge-rec (F.arr ⊙winl) (F.arr ⊙winr)
      =⟨ ⊙wedge-rec-post∘ ⊙out (F.arr ⊙winl) (F.arr ⊙winr) ⟩
    ⊙wedge-rec (⊙out ⊙∘ F.arr ⊙winl) (⊙out ⊙∘ F.arr ⊙winr)
      =⟨ ap2 ⊙wedge-rec
           (A.nat!-dom ⊙winl _ (⊙wedge-rec _ _)
            ∙ ap (<– (A.eq _ _)) OutHelp.⊙winl-β
            ∙ <–-inv-l (A.eq _ _) ⊙winl)
           (A.nat!-dom ⊙winr _ (⊙wedge-rec _ _)
            ∙ ap (<– (A.eq _ _)) OutHelp.⊙winr-β
            ∙ <–-inv-l (A.eq _ _) ⊙winr) ⟩
    ⊙wedge-rec ⊙winl ⊙winr
      =⟨ ⊙wedge-rec-η ⟩
    ⊙idf _ ∎

  ⊙eq : F.obj U ⊙∨ F.obj V ⊙≃ F.obj (U ⊙∨ V)
  ⊙eq = ⊙≃-in (equiv (fst ⊙into) (fst ⊙out)
                  (app= (ap fst ⊙into-out)) (app= (ap fst ⊙out-into)))
                (snd ⊙into)

  ⊙path = ⊙ua ⊙eq

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
module test.IntegerLiteral where

open import Type
open import Declarative
open import Builtin
open import Builtin.Constant.Type
open import Builtin.Constant.Term Ctx⋆ Kind * # _⊢⋆_ con size⋆
open import Agda.Builtin.Sigma
open import Data.Integer
open import Data.Nat

-- zerepoch/zerepoch-core/test/data/integerLiteral.plc

intLit : ∀{Γ} → Γ ⊢ con integer (size⋆ 100)
intLit = con (integer 100 (ℤ.pos 102341) (-≤+ Σ., +≤+ (gen _ _ _)))

max_stars_repo_name: Quantum-One-DLT/zerepoch

max_issues_repo_name: Quantum-One-DLT/zerepoch

max_forks_repo_name: Quantum-One-DLT/zerepoch


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Relation.Binary.Base where

open import Cubical.Core.Everything

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function using (_on_)
open import Cubical.Foundations.HLevels

open import Cubical.Classes using (Cast; [_]) public

private
  variable
    a b ℓ : Level
    A : Type a
    B : Type b

RawREL : Type a → Type b → (ℓ : Level) → Type _
RawREL A B ℓ = A → B → Type ℓ

RawRel : Type a → (ℓ : Level) → Type _
RawRel A ℓ = RawREL A A ℓ

REL : Type a → Type b → (ℓ : Level) → Type _
REL A B ℓ = A → B → hProp ℓ

Rel : Type a → (ℓ : Level) → Type _
Rel A ℓ = REL A A ℓ

isPropValued : RawREL A B ℓ → Type _
isPropValued R = ∀ a b → isProp (R a b)

instance
  RelCast : Cast (REL A B ℓ) (RawREL A B ℓ)
  RelCast = record { cast = λ R a b → R a b .fst }

isProp[_] : (R : REL A B ℓ) → isPropValued [ R ]
isProp[ R ] a b = R a b .snd

fromRaw : (R : RawREL A B ℓ) → isPropValued R → REL A B ℓ
fromRaw R isPropR a b .fst = R a b
fromRaw R isPropR a b .snd = isPropR a b


text:
------------------------------------------------------------------------
-- Some results/examples related to CCS, implemented using the
-- coinductive definition of bisimilarity
------------------------------------------------------------------------

-- Unless anything else is stated the results (or statements, in the
-- case of exercises) below are taken from "Enhancements of the
-- bisimulation proof method" by Pous and Sangiorgi.

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

open import Prelude

module Bisimilarity.CCS.Examples {ℓ} {Name : Type ℓ} where

open import Equality.Propositional
open import Prelude.Size

open import Bisimilarity.CCS
import Bisimilarity.Equational-reasoning-instances
open import Equational-reasoning
open import Labelled-transition-system.CCS Name

open import Bisimilarity CCS

------------------------------------------------------------------------
-- A result mentioned in "Enhancements of the bisimulation proof
-- method"

mutual

  -- For a more general result, see 6-2-14 below.

  !∙⊕∙∼!∙∣!∙ : ∀ {i a b} → [ i ] ! (a ∙ ⊕ b ∙) ∼ ! a ∙ ∣ ! b ∙
  !∙⊕∙∼!∙∣!∙ {i} {a} {b} = ⟨ lr , rl ⟩
    where
    lemma =
      ! (a ∙ ⊕ b ∙) ∣ ∅  ∼⟨ ∣-right-identity ⟩
      ! (a ∙ ⊕ b ∙)      ∼⟨ !∙⊕∙∼′!∙∣!∙ {i = i} ⟩■
      ! a ∙ ∣ ! b ∙

    left-lemma =
      ! (a ∙ ⊕ b ∙) ∣ ∅    ∼⟨ lemma ⟩
      ! a ∙ ∣ ! b ∙        ∼⟨ symmetric ∣-right-identity ∣-cong reflexive ⟩■
      (! a ∙ ∣ ∅) ∣ ! b ∙

    right-lemma =
      ! (a ∙ ⊕ b ∙) ∣ ∅    ∼⟨ lemma ⟩
      ! a ∙ ∣  ! b ∙       ∼⟨ reflexive ∣-cong symmetric ∣-right-identity ⟩■
      ! a ∙ ∣ (! b ∙ ∣ ∅)

    τ-lemma =
      (! (a ∙ ⊕ b ∙) ∣ ∅) ∣ ∅    ∼⟨ ∣-right-identity ⟩
      ! (a ∙ ⊕ b ∙) ∣ ∅          ∼⟨ lemma ⟩
      ! a ∙ ∣ ! b ∙              ∼⟨ symmetric (∣-right-identity ∣-cong ∣-right-identity) ⟩■
      (! a ∙ ∣ ∅) ∣ (! b ∙ ∣ ∅)

    lr : ∀ {P μ} →
         ! (a ∙ ⊕ b ∙) [ μ ]⟶ P →
         ∃ λ Q → ! a ∙ ∣ ! b ∙ [ μ ]⟶ Q × [ i ] P ∼′ Q
    lr {P} tr = case 6-1-3-2 tr of λ where

      (inj₁ (.∅ , sum-left action , P∼![a⊕b]∣∅)) →
        P                    ∼⟨ P∼![a⊕b]∣∅ ⟩
        ! (a ∙ ⊕ b ∙) ∣ ∅    ∼⟨ left-lemma ⟩■
        (! a ∙ ∣ ∅) ∣ ! b ∙  [ name a ]⟵⟨ par-left (replication (par-right action)) ⟩
        ! a ∙       ∣ ! b ∙

      (inj₁ (.∅ , sum-right action , P∼![a⊕b]∣∅)) →
        P                    ∼⟨ P∼![a⊕b]∣∅ ⟩
        ! (a ∙ ⊕ b ∙) ∣ ∅    ∼⟨ right-lemma ⟩■
        ! a ∙ ∣ (! b ∙ ∣ ∅)  [ name b ]⟵⟨ par-right (replication (par-right action)) ⟩
        ! a ∙ ∣ ! b ∙

      (inj₂ (refl , P′ , P″ , c , a⊕b⟶P′ , a⊕b⟶P″ , P∼![a⊕b]∣P′∣P″)) →
        let b≡co-a , P′≡∅ , P″≡∅ = Σ-map id [ id , id ]
                                     (·⊕·-co a⊕b⟶P′ a⊕b⟶P″) in

        P                          ∼⟨ P∼![a⊕b]∣P′∣P″ ⟩
        (! (a ∙ ⊕ b ∙) ∣ P′) ∣ P″  ∼⟨ (reflexive ∣-cong ≡⇒∼ P′≡∅) ∣-cong ≡⇒∼ P″≡∅ ⟩
        (! (a ∙ ⊕ b ∙) ∣ ∅) ∣ ∅    ∼⟨ τ-lemma ⟩■
        (! a ∙ ∣ ∅) ∣ (! b ∙ ∣ ∅)  [ τ ]⟵⟨ par-τ′ b≡co-a (replication (par-right action))
                                                         (replication (par-right action)) ⟩
        ! a ∙ ∣ ! b ∙

    rl : ∀ {Q μ} →
         ! a ∙ ∣ ! b ∙ [ μ ]⟶ Q →
         ∃ λ P → ! (a ∙ ⊕ b ∙) [ μ ]⟶ P × [ i ] P ∼′ Q
    rl (par-left {P′ = P′} tr) =
      case 6-1-3-2 tr of λ where

        (inj₁ (.∅ , action , P′∼!a∣∅)) →
          ! (a ∙ ⊕ b ∙)        [ name a ]⟶⟨ replication (par-right (sum-left action)) ⟩ʳˡ
          ! (a ∙ ⊕ b ∙) ∣ ∅    ∼⟨ left-lemma ⟩
          (! a ∙ ∣ ∅) ∣ ! b ∙  ∼⟨ symmetric P′∼!a∣∅ ∣-cong reflexive ⟩■
          P′ ∣ ! b ∙

        (inj₂ (refl , .∅ , P″ , .a , action , a⟶P″ , P′∼!a∣∅∣P″)) →
          ⊥-elim (names-are-not-inverted a⟶P″)

    rl (par-right {Q′ = Q′} tr) =
      case 6-1-3-2 tr of λ where

        (inj₁ (.∅ , action , Q′∼!b∣∅)) →
          ! (a ∙ ⊕ b ∙)        [ name b ]⟶⟨ replication (par-right (sum-right action)) ⟩ʳˡ
          ! (a ∙ ⊕ b ∙) ∣ ∅    ∼⟨ right-lemma ⟩
          ! a ∙ ∣ (! b ∙ ∣ ∅)  ∼⟨ reflexive ∣-cong symmetric Q′∼!b∣∅ ⟩■
          ! a ∙ ∣ Q′

        (inj₂ (refl , .∅ , Q″ , .b , action , b⟶Q″ , Q′∼!b∣∅∣Q″)) →
          ⊥-elim (names-are-not-inverted b⟶Q″)

    rl (par-τ {P′ = P′} {Q′ = Q′} tr₁ tr₂) =
      case 6-1-3-2 tr₁ ,′ 6-1-3-2 tr₂ of λ where

        (inj₁ (.∅ , action , P′∼!a∣∅) ,
         inj₁ (.∅ , action , Q′∼!co-a∣∅)) →
          ! (a ∙ ⊕ co a ∙)              [ τ ]⟶⟨ replication (par-τ (replication (par-right (sum-left action)))
                                                                   (sum-right action)) ⟩ʳˡ
          (! (a ∙ ⊕ co a ∙) ∣ ∅) ∣ ∅    ∼⟨ τ-lemma ⟩
          (! a ∙ ∣ ∅) ∣ (! co a ∙ ∣ ∅)  ∼⟨ symmetric (P′∼!a∣∅ ∣-cong Q′∼!co-a∣∅) ⟩■
          P′ ∣ Q′

        (inj₁ _ , inj₂ (() , _))
        (inj₂ (() , _) , _)

  !∙⊕∙∼′!∙∣!∙ : ∀ {a b i} → [ i ] ! (a ∙ ⊕ b ∙) ∼′ ! a ∙ ∣ ! b ∙
  force !∙⊕∙∼′!∙∣!∙ = !∙⊕∙∼!∙∣!∙

------------------------------------------------------------------------
-- Exercise 6.2.4

mutual

  -- For a more general result, see 6-2-17-4 below.

  6-2-4 : ∀ {a i} → [ i ] ! ! a ∙ ∼ ! a ∙
  6-2-4 {a} {i} = ⟨ lr , rl ⟩
    where
    impossible : ∀ {μ P q} {Q : Type q} →
                 ! ! a ∙ [ μ ]⟶ P → μ ≡ τ → Q
    impossible {μ} !!a⟶P μ≡τ = ⊥-elim $ name≢τ
      (name a  ≡⟨ !-only (!-only ·-only) !!a⟶P ⟩
       μ       ≡⟨ μ≡τ ⟩∎
       τ       ∎)

    lemma : ∀ {P} → P ∼ ! a ∙ ∣ ∅ → _
    lemma {P} P∼!a∣∅ =
      ! ! a ∙ ∣ P            ∼⟨ reflexive ∣-cong P∼!a∣∅ ⟩
      ! ! a ∙ ∣ (! a ∙ ∣ ∅)  ∼⟨ reflexive ∣-cong ∣-right-identity ⟩
      ! ! a ∙ ∣ ! a ∙        ∼⟨ 6-1-2 ⟩
      ! ! a ∙                ∼⟨ 6-2-4′ {i = i} ⟩
      ! a ∙                  ∼⟨ symmetric ∣-right-identity ⟩■
      ! a ∙ ∣ ∅

    lr : ∀ {P μ} →
         ! ! a ∙ [ μ ]⟶ P →
         ∃ λ P′ → ! a ∙ [ μ ]⟶ P′ × [ i ] P ∼′ P′
    lr {P = P} !!a⟶P = case 6-1-3-2 !!a⟶P of λ where
      (inj₂ (μ≡τ , _))               → impossible !!a⟶P μ≡τ
      (inj₁ (P′ , !a⟶P′ , P∼!!a∣P′)) → case 6-1-3-2 !a⟶P′ of λ where
        (inj₂ (μ≡τ , _))               → impossible !!a⟶P μ≡τ
        (inj₁ (.∅ , action , P′∼!a∣∅)) →
          P             ∼⟨ P∼!!a∣P′ ⟩
          ! ! a ∙ ∣ P′  ∼⟨ lemma P′∼!a∣∅ ⟩■
          ! a ∙ ∣ ∅     [ name a ]⟵⟨ replication (par-right action) ⟩
          ! a ∙

    rl : ∀ {P μ} →
         ! a ∙ [ μ ]⟶ P →
         ∃ λ P′ → ! ! a ∙ [ μ ]⟶ P′ × [ i ] P′ ∼′ P
    rl {P = P} !a⟶P = case 6-1-3-2 !a⟶P of λ where
      (inj₂ (refl , .∅ , Q″ , .a , action , a⟶Q″ , _)) →
        ⊥-elim (names-are-not-inverted a⟶Q″)
      (inj₁ (.∅ , action , P∼!a∣∅)) →
        ! ! a ∙      [ name a ]⟶⟨ replication (par-right !a⟶P) ⟩ʳˡ
        ! ! a ∙ ∣ P  ∼⟨ lemma P∼!a∣∅ ⟩
        ! a ∙ ∣ ∅    ∼⟨ symmetric P∼!a∣∅ ⟩■
        P

  6-2-4′ : ∀ {a i} → [ i ] ! ! a ∙ ∼′ ! a ∙
  force 6-2-4′ = 6-2-4

------------------------------------------------------------------------
-- A result mentioned in "Enhancements of the bisimulation proof
-- method"

∙∣∙∼∙∙ : ∀ {a} → a ∙ ∣ a ∙ ∼ name a ∙ (a ∙)
∙∣∙∼∙∙ {a} = ⟨ lr , rl ⟩
  where
  lr : ∀ {P μ} → a ∙ ∣ a ∙ [ μ ]⟶ P →
       ∃ λ P′ → name a ∙ (a ∙) [ μ ]⟶ P′ × P ∼′ P′
  lr (par-left action) =
    ∅ ∣ a ∙         ∼⟨ ∣-left-identity ⟩■
    a ∙             [ name a ]⟵⟨ action ⟩
    name a ∙ (a ∙)

  lr (par-right action) =
    a ∙ ∣ ∅         ∼⟨ ∣-right-identity ⟩■
    a ∙             [ name a ]⟵⟨ action ⟩
    name a ∙ (a ∙)

  lr (par-τ action tr) = ⊥-elim (names-are-not-inverted tr)

  rl : ∀ {P μ} → name a ∙ (a ∙) [ μ ]⟶ P →
       ∃ λ P′ → a ∙ ∣ a ∙ [ μ ]⟶ P′ × P′ ∼′ P
  rl action =
    a ∙ ∣ a ∙  [ name a ]⟶⟨ par-right action ⟩ʳˡ
    a ∙ ∣ ∅    ∼⟨ ∣-right-identity ⟩■
    a ∙

------------------------------------------------------------------------
-- Lemma 6.2.14

mutual

  -- A more general variant of !∙⊕∙∼!∙∣!∙. For an even more general
  -- variant, see 6-2-17-2 below.

  6-2-14 :
    ∀ {i a b P Q} →
    [ i ] ! (name a ∙ P ⊕ name b ∙ Q) ∼ ! name a ∙ P ∣ ! name b ∙ Q
  6-2-14 {i} {a} {b} {P} {Q} = ⟨ lr , rl ⟩
    where
    left-lemma =
      ! (name a ∙ P ⊕ name b ∙ Q) ∣ P    ∼⟨ 6-2-14′ {i = i} ∣-cong′ reflexive ⟩
      (! name a ∙ P ∣ ! name b ∙ Q) ∣ P  ∼⟨ swap-rightmost ⟩■
      (! name a ∙ P ∣ P) ∣ ! name b ∙ Q

    right-lemma =
      ! (name a ∙ P ⊕ name b ∙ Q) ∣ Q    ∼⟨ 6-2-14′ {i = i} ∣-cong′ reflexive ⟩
      (! name a ∙ P ∣ ! name b ∙ Q) ∣ Q  ∼⟨ symmetric ∣-assoc ⟩■
      ! name a ∙ P ∣ (! name b ∙ Q ∣ Q)

    τ-lemma =
      (! (name a ∙ P ⊕ name b ∙ Q) ∣ P) ∣ Q    ∼⟨ left-lemma ∣-cong′ reflexive ⟩
      ((! name a ∙ P ∣ P) ∣ ! name b ∙ Q) ∣ Q  ∼⟨ symmetric ∣-assoc ⟩■
      (! name a ∙ P ∣ P) ∣ (! name b ∙ Q ∣ Q)

    lr : ∀ {R μ} →
         ! (name a ∙ P ⊕ name b ∙ Q) [ μ ]⟶ R →
         ∃ λ S → ! name a ∙ P ∣ ! name b ∙ Q [ μ ]⟶ S × [ i ] R ∼′ S
    lr {R} tr = case 6-1-3-2 tr of λ where

      (inj₁ (.P , sum-left action , R∼![aP⊕bQ]∣P)) →
        R                                  ∼⟨ R∼![aP⊕bQ]∣P ⟩
        ! (name a ∙ P ⊕ name b ∙ Q) ∣ P    ∼⟨ left-lemma ⟩■
        (! name a ∙ P ∣ P) ∣ ! name b ∙ Q  [ name a ]⟵⟨ par-left (replication (par-right action)) ⟩
        ! name a ∙ P       ∣ ! name b ∙ Q

      (inj₁ (.Q , sum-right action , R∼![aP⊕bQ]∣Q)) →
        R                                  ∼⟨ R∼![aP⊕bQ]∣Q ⟩
        ! (name a ∙ P ⊕ name b ∙ Q) ∣ Q    ∼⟨ right-lemma ⟩■
        ! name a ∙ P ∣ (! name b ∙ Q ∣ Q)  [ name b ]⟵⟨ par-right (replication (par-right action)) ⟩
        ! name a ∙ P ∣ ! name b ∙ Q

      (inj₂ ( refl , R′ , R″ , c , aP⊕bQ⟶R′ , aP⊕bQ⟶R″
            , R∼![aP⊕bQ]∣R′∣R″
            )) →
        let b≡co-a , R′≡,R″≡ = ·⊕·-co aP⊕bQ⟶R′ aP⊕bQ⟶R″

            lemma : _ → [ _ ] _ ∼ _
            lemma = λ where
              (inj₁ (R′≡P , R″≡Q)) →
                (! (name a ∙ P ⊕ name b ∙ Q) ∣ R′) ∣ R″  ∼⟨ (reflexive ∣-cong ≡⇒∼ R′≡P) ∣-cong ≡⇒∼ R″≡Q ⟩■
                (! (name a ∙ P ⊕ name b ∙ Q) ∣ P) ∣ Q
              (inj₂ (R′≡Q , R″≡P)) →
                (! (name a ∙ P ⊕ name b ∙ Q) ∣ R′) ∣ R″  ∼⟨ (reflexive ∣-cong ≡⇒∼ R′≡Q) ∣-cong ≡⇒∼ R″≡P ⟩
                (! (name a ∙ P ⊕ name b ∙ Q) ∣ Q) ∣ P    ∼⟨ swap-rightmost ⟩■
                (! (name a ∙ P ⊕ name b ∙ Q) ∣ P) ∣ Q
        in
        R                                        ∼⟨ R∼![aP⊕bQ]∣R′∣R″ ⟩
        (! (name a ∙ P ⊕ name b ∙ Q) ∣ R′) ∣ R″  ∼⟨ lemma R′≡,R″≡ ⟩
        (! (name a ∙ P ⊕ name b ∙ Q) ∣ P) ∣ Q    ∼⟨ τ-lemma ⟩■
        (! name a ∙ P ∣ P) ∣ (! name b ∙ Q ∣ Q)  [ τ ]⟵⟨ par-τ′ b≡co-a (replication (par-right action))
                                                                       (replication (par-right action)) ⟩
        ! name a ∙ P ∣ ! name b ∙ Q

    rl : ∀ {S μ} →
         ! name a ∙ P ∣ ! name b ∙ Q [ μ ]⟶ S →
         ∃ λ R → ! (name a ∙ P ⊕ name b ∙ Q) [ μ ]⟶ R × [ i ] R ∼′ S
    rl (par-left {P′ = S} tr) =
      case 6-1-3-2 tr of λ where
        (inj₁ (.P , action , S∼!aP∣P)) →
          ! (name a ∙ P ⊕ name b ∙ Q)        [ name a ]⟶⟨ replication (par-right (sum-left action)) ⟩ʳˡ
          ! (name a ∙ P ⊕ name b ∙ Q) ∣ P    ∼⟨ left-lemma ⟩
          (! name a ∙ P ∣ P) ∣ ! name b ∙ Q  ∼⟨ symmetric S∼!aP∣P ∣-cong reflexive ⟩■
          S ∣ ! name b ∙ Q

        (inj₂ (refl , .P , S′ , .a , action , aP⟶S′ , S∼!aP∣P∣S′)) →
          ⊥-elim (names-are-not-inverted aP⟶S′)

    rl (par-right {Q′ = S} tr) =
      case 6-1-3-2 tr of λ where
        (inj₁ (.Q , action , S∼!bQ∣Q)) →
          ! (name a ∙ P ⊕ name b ∙ Q)        [ name b ]⟶⟨ replication (par-right (sum-right action)) ⟩ʳˡ
          ! (name a ∙ P ⊕ name b ∙ Q) ∣ Q    ∼⟨ right-lemma ⟩
          ! name a ∙ P ∣ (! name b ∙ Q ∣ Q)  ∼⟨ reflexive ∣-cong symmetric S∼!bQ∣Q ⟩■
          ! name a ∙ P ∣ S

        (inj₂ (refl , .Q , S′ , .b , action , bQ⟶S′ , S∼!bQ∣Q∣S′)) →
          ⊥-elim (names-are-not-inverted bQ⟶S′)

    rl (par-τ {P′ = S} {Q′ = S′} tr₁ tr₂) =
      case 6-1-3-2 tr₁ ,′ 6-1-3-2 tr₂ of λ where
        (inj₁ (.P , action , S∼!aP∣P) ,
         inj₁ (.Q , action , S′∼!co-aQ∣Q)) →
          ! (name a ∙ P ⊕ name (co a) ∙ Q)              [ τ ]⟶⟨ replication (par-τ (replication (par-right (sum-left action)))
                                                                                (sum-right action)) ⟩ʳˡ
          (! (name a ∙ P ⊕ name (co a) ∙ Q) ∣ P) ∣ Q    ∼⟨ τ-lemma ⟩
          (! name a ∙ P ∣ P) ∣ (! name (co a) ∙ Q ∣ Q)  ∼⟨ symmetric (S∼!aP∣P ∣-cong S′∼!co-aQ∣Q) ⟩■
          S ∣ S′

        (inj₁ _ , inj₂ (() , _))
        (inj₂ (() , _) , _)

  6-2-14′ :
    ∀ {i a b P Q} →
    [ i ] ! (name a ∙ P ⊕ name b ∙ Q) ∼′ ! name a ∙ P ∣ ! name b ∙ Q
  force 6-2-14′ = 6-2-14

------------------------------------------------------------------------
-- Lemma 6.2.17

-- Some results mentioned in the proof of 6.2.17 (1) in
-- "Enhancements of the bisimulation proof method".

6-2-17-1-lemma₁ : ∀ {P Q} → (! P ∣ ! Q) ∣ (P ∣ Q) ∼ ! P ∣ ! Q
6-2-17-1-lemma₁ {P} {Q} =
  (! P ∣ ! Q) ∣ (P ∣ Q)  ∼⟨ swap-in-the-middle ⟩
  (! P ∣ P) ∣ (! Q ∣ Q)  ∼⟨ 6-1-2 ∣-cong 6-1-2 ⟩■
  ! P ∣ ! Q

abstract

  6-2-17-1-lemma₂ :
    ∀ {P Q R μ} →
    ! (P ∣ Q) [ μ ]⟶ R →
    ∃ λ S →
      R ∼ ! (P ∣ Q) ∣ S ×
      ∃ λ T →
        ! P ∣ ! Q [ μ ]⟶ T ×
        (! P ∣ ! Q) ∣ S ∼′ T
  6-2-17-1-lemma₂ {P} {Q} {R} tr = case 6-1-3-2 tr of λ where
    (inj₁ (R′ , P∣Q⟶R′ , R∼![P∣Q]∣R′)) →
      let R″ , !P∣!Q⟶R″ , !P∣!Q∣R′∼R″ =
            left-to-right
              ((! P ∣ ! Q) ∣ (P ∣ Q)  ∼⟨ 6-2-17-1-lemma₁ ⟩■
               ! P ∣ ! Q)
              ((! P ∣ ! Q) ∣ (P ∣ Q)  ⟶⟨ par-right P∣Q⟶R′ ⟩
               (! P ∣ ! Q) ∣ R′)
      in _ , R∼![P∣Q]∣R′ , _ , !P∣!Q⟶R″ , !P∣!Q∣R′∼R″

    (inj₂ (refl , R′ , R″ , a , P∣Q⟶R′ , P∣Q⟶R″ , R∼![P∣Q]∣R′∣R″)) →
      let T , !P∣!Q⟶T , !P∣!Q∣[R′∣R″]∼T =
            left-to-right
              ((! P ∣ ! Q) ∣ ((P ∣ Q) ∣ (P ∣ Q))  ∼⟨ ∣-assoc ⟩
               ((! P ∣ ! Q) ∣ (P ∣ Q)) ∣ (P ∣ Q)  ∼⟨ 6-2-17-1-lemma₁ ∣-cong reflexive ⟩
               (! P ∣ ! Q) ∣ (P ∣ Q)              ∼⟨ 6-2-17-1-lemma₁ ⟩■
               ! P ∣ ! Q)
              ((! P ∣ ! Q) ∣ ((P ∣ Q) ∣ (P ∣ Q))  ⟶⟨ par-right (par-τ P∣Q⟶R′ P∣Q⟶R″) ⟩
               (! P ∣ ! Q) ∣ (R′ ∣ R″))
      in
        _
      , (R                      ∼⟨ R∼![P∣Q]∣R′∣R″ ⟩
         (! (P ∣ Q) ∣ R′) ∣ R″  ∼⟨ symmetric ∣-assoc ⟩■
         ! (P ∣ Q) ∣ (R′ ∣ R″))
      , _
      , !P∣!Q⟶T
      , !P∣!Q∣[R′∣R″]∼T

mutual

  6-2-17-1 : ∀ {i P Q} → [ i ] ! (P ∣ Q) ∼ ! P ∣ ! Q
  6-2-17-1 {i} {P} {Q} = ⟨ lr , rl ⟩
    where
    lr : ∀ {R μ} →
         ! (P ∣ Q) [ μ ]⟶ R →
         ∃ λ S → ! P ∣ ! Q [ μ ]⟶ S × [ i ] R ∼′ S
    lr {R} tr =
      let S , R∼![P∣Q]∣S , T , !P∣!Q⟶T , !P∣!Q∣S∼T =
            6-2-17-1-lemma₂ tr in

      R                ∼⟨ R∼![P∣Q]∣S ⟩
      ! (P ∣ Q) ∣ S    ∼⟨ 6-2-17-1′ ∣-cong′ reflexive ⟩
      (! P ∣ ! Q) ∣ S  ∼⟨ !P∣!Q∣S∼T ⟩■
      T                ⟵⟨ !P∣!Q⟶T ⟩
      ! P ∣ ! Q

    lemma = λ {R S : Proc ∞} →
      ! (P ∣ Q) ∣ (R ∣ S)    ∼⟨ 6-2-17-1′ {i = i} ∣-cong′ reflexive ⟩
      (! P ∣ ! Q) ∣ (R ∣ S)  ∼⟨ swap-in-the-middle ⟩■
      (! P ∣ R) ∣ (! Q ∣ S)

    left-lemma = λ {R : Proc ∞} →
      ! (P ∣ Q) ∣ (R ∣ Q)    ∼⟨ lemma ⟩
      (! P ∣ R) ∣ (! Q ∣ Q)  ∼⟨ reflexive ∣-cong 6-1-2 ⟩■
      (! P ∣ R) ∣ ! Q

    right-lemma = λ {R : Proc ∞} →
      ! (P ∣ Q) ∣ (P ∣ R)    ∼⟨ lemma ⟩
      (! P ∣ P) ∣ (! Q ∣ R)  ∼⟨ 6-1-2 ∣-cong reflexive ⟩■
      ! P ∣ (! Q ∣ R)

    rl : ∀ {S μ} →
         ! P ∣ ! Q [ μ ]⟶ S →
         ∃ λ R → ! (P ∣ Q) [ μ ]⟶ R × [ i ] R ∼′ S
    rl (par-left {P′ = S} !P⟶S) =
      case 6-1-3-2 !P⟶S
        return (const $ ∃ λ _ → _ × [ i ] _ ∼′ _)
        of λ where
        (inj₁ (P′ , P⟶P′ , S∼!P∣P′)) →
          ! (P ∣ Q)             ⟶⟨ replication (par-right (par-left P⟶P′)) ⟩ʳˡ
          ! (P ∣ Q) ∣ (P′ ∣ Q)  ∼⟨ left-lemma ⟩
          (! P ∣ P′) ∣ ! Q      ∼⟨ symmetric S∼!P∣P′ ∣-cong reflexive ⟩■
          S ∣ ! Q

        (inj₂ (refl , P′ , P″ , a , P⟶P′ , P⟶P″ , S∼!P∣P′∣P″)) →
          ! (P ∣ Q)                          [ τ ]⟶⟨ replication (par-τ (replication (par-right (par-left P⟶P′)))
                                                                        (par-left P⟶P″)) ⟩ʳˡ
          (! (P ∣ Q) ∣ (P′ ∣ Q)) ∣ (P″ ∣ Q)  ∼⟨ left-lemma ∣-cong′ reflexive ⟩
          ((! P ∣ P′) ∣ ! Q) ∣ (P″ ∣ Q)      ∼⟨ swap-in-the-middle ⟩
          ((! P ∣ P′) ∣ P″) ∣ (! Q ∣ Q)      ∼⟨ reflexive ∣-cong 6-1-2 ⟩
          ((! P ∣ P′) ∣ P″) ∣ ! Q            ∼⟨ symmetric S∼!P∣P′∣P″ ∣-cong reflexive ⟩■
          S ∣ ! Q

    rl (par-right {Q′ = S} !Q⟶S) =
      case 6-1-3-2 !Q⟶S
        return (const $ ∃ λ _ → _ × [ i ] _ ∼′ _)
        of λ where
        (inj₁ (Q′ , Q⟶Q′ , S∼!Q∣Q′)) →
          ! (P ∣ Q)             ⟶⟨ replication (par-right (par-right Q⟶Q′)) ⟩ʳˡ
          ! (P ∣ Q) ∣ (P ∣ Q′)  ∼⟨ right-lemma ⟩
          ! P ∣ (! Q ∣ Q′)      ∼⟨ reflexive ∣-cong symmetric S∼!Q∣Q′ ⟩■
          ! P ∣ S

        (inj₂ (refl , Q′ , Q″ , a , Q⟶Q′ , Q⟶Q″ , S∼!Q∣Q′∣Q″)) →
          ! (P ∣ Q)                          [ τ ]⟶⟨ replication (par-τ (replication (par-right (par-right Q⟶Q′)))
                                                                        (par-right Q⟶Q″)) ⟩ʳˡ
          (! (P ∣ Q) ∣ (P ∣ Q′)) ∣ (P ∣ Q″)  ∼⟨ right-lemma ∣-cong′ reflexive ⟩
          (! P ∣ (! Q ∣ Q′)) ∣ (P ∣ Q″)      ∼⟨ swap-in-the-middle ⟩
          (! P ∣ P) ∣ ((! Q ∣ Q′) ∣ Q″)      ∼⟨ 6-1-2 ∣-cong reflexive ⟩
          ! P ∣ ((! Q ∣ Q′) ∣ Q″)            ∼⟨ reflexive ∣-cong symmetric S∼!Q∣Q′∣Q″ ⟩■
          ! P ∣ S

    rl (par-τ {P′ = S} {Q′ = S′} !P⟶S !Q⟶S′) =
      case 6-1-3-2 !P⟶S ,′ 6-1-3-2 !Q⟶S′ of λ where
        (inj₁ (P′ , P⟶P′ , S∼!P∣P′) ,
         inj₁ (Q′ , Q⟶Q′ , S′∼!Q∣Q′)) →
          ! (P ∣ Q)                          [ τ ]⟶⟨ replication (par-τ (replication (par-right (par-left P⟶P′)))
                                                                                (par-right Q⟶Q′)) ⟩ʳˡ
          (! (P ∣ Q) ∣ (P′ ∣ Q)) ∣ (P ∣ Q′)  ∼⟨ left-lemma ∣-cong′ reflexive ⟩
          ((! P ∣ P′) ∣ ! Q) ∣ (P ∣ Q′)      ∼⟨ swap-in-the-middle ⟩
          ((! P ∣ P′) ∣ P) ∣ (! Q ∣ Q′)      ∼⟨ swap-rightmost ∣-cong reflexive ⟩
          ((! P ∣ P) ∣ P′) ∣ (! Q ∣ Q′)      ∼⟨ (6-1-2 ∣-cong reflexive) ∣-cong reflexive ⟩
          (! P ∣ P′) ∣ (! Q ∣ Q′)            ∼⟨ symmetric (S∼!P∣P′ ∣-cong S′∼!Q∣Q′) ⟩■
          S ∣ S′

        (inj₁ _ , inj₂ (() , _))
        (inj₂ (() , _) , _)

  6-2-17-1′ : ∀ {i P Q} → [ i ] ! (P ∣ Q) ∼′ ! P ∣ ! Q
  force 6-2-17-1′ = 6-2-17-1

mutual

  6-2-17-2 : ∀ {i P Q} → [ i ] ! (P ⊕ Q) ∼ ! P ∣ ! Q
  6-2-17-2 {i} {P} {Q} = ⟨ lr , rl ⟩
    where
    left-lemma = λ {R : Proc ∞} →
      ! (P ⊕ Q) ∣ R    ∼⟨ 6-2-17-2′ {i = i} ∣-cong′ reflexive ⟩
      (! P ∣ ! Q) ∣ R  ∼⟨ swap-rightmost ⟩■
      (! P ∣ R) ∣ ! Q

    right-lemma = λ {R : Proc ∞} →
      ! (P ⊕ Q) ∣ R    ∼⟨ 6-2-17-2′ {i = i} ∣-cong′ reflexive ⟩
      (! P ∣ ! Q) ∣ R  ∼⟨ symmetric ∣-assoc ⟩■
      ! P ∣ (! Q ∣ R)

    τ-lemma₁ = λ {P′ P″ : Proc ∞} →
      (! (P ⊕ Q) ∣ P′) ∣ P″    ∼⟨ left-lemma ∣-cong′ reflexive ⟩
      ((! P ∣ P′) ∣ ! Q) ∣ P″  ∼⟨ swap-rightmost ⟩■
      ((! P ∣ P′) ∣ P″) ∣ ! Q

    τ-lemma₂ = λ {P′ Q′ : Proc ∞} →
      (! (P ⊕ Q) ∣ P′) ∣ Q′    ∼⟨ left-lemma ∣-cong′ reflexive ⟩
      ((! P ∣ P′) ∣ ! Q) ∣ Q′  ∼⟨ symmetric ∣-assoc ⟩■
      (! P ∣ P′) ∣ (! Q ∣ Q′)

    τ-lemma₃ = λ {Q′ Q″ : Proc ∞} →
      (! (P ⊕ Q) ∣ Q′) ∣ Q″    ∼⟨ right-lemma ∣-cong′ reflexive ⟩
      (! P ∣ (! Q ∣ Q′)) ∣ Q″  ∼⟨ symmetric ∣-assoc ⟩■
      ! P ∣ ((! Q ∣ Q′) ∣ Q″)

    lr : ∀ {R μ} →
         ! (P ⊕ Q) [ μ ]⟶ R →
         ∃ λ S → ! P ∣ ! Q [ μ ]⟶ S × [ i ] R ∼′ S
    lr {R} tr =
      case 6-1-3-2 tr
        return (const $ ∃ λ _ → _ × [ i ] _ ∼′ _)
        of λ where

        (inj₁ (P′ , sum-left P⟶P′ , R∼![P⊕Q]∣P′)) →
          R                 ∼⟨ R∼![P⊕Q]∣P′ ⟩
          ! (P ⊕ Q) ∣ P′    ∼⟨ left-lemma ⟩■
          (! P ∣ P′) ∣ ! Q  ⟵⟨ par-left (replication (par-right P⟶P′)) ⟩
          ! P        ∣ ! Q

        (inj₁ (Q′ , sum-right Q⟶Q′ , R∼![P⊕Q]∣Q′)) →
          R                 ∼⟨ R∼![P⊕Q]∣Q′ ⟩
          ! (P ⊕ Q) ∣ Q′    ∼⟨ right-lemma ⟩■
          ! P ∣ (! Q ∣ Q′)  ⟵⟨ par-right (replication (par-right Q⟶Q′)) ⟩
          ! P ∣  ! Q

        (inj₂ ( refl , P′ , P″ , c
              , sum-left P⟶P′ , sum-left P⟶P″
              , R∼![P⊕Q]∣P′∣P″
              )) →
          R                        ∼⟨ R∼![P⊕Q]∣P′∣P″ ⟩
          (! (P ⊕ Q) ∣ P′) ∣ P″    ∼⟨ τ-lemma₁ ⟩■
          ((! P ∣ P′) ∣ P″) ∣ ! Q  [ τ ]⟵⟨ par-left (replication (par-τ (replication (par-right P⟶P′)) P⟶P″)) ⟩
          ! P ∣ ! Q

        (inj₂ ( refl , P′ , Q′ , c
              , sum-left P⟶P′ , sum-right Q⟶Q′
              , R∼![P⊕Q]∣P′∣Q′
              )) →
          R                        ∼⟨ R∼![P⊕Q]∣P′∣Q′ ⟩
          (! (P ⊕ Q) ∣ P′) ∣ Q′    ∼⟨ τ-lemma₂ ⟩■
          (! P ∣ P′) ∣ (! Q ∣ Q′)  [ τ ]⟵⟨ par-τ (replication (par-right P⟶P′))
                                                 (replication (par-right Q⟶Q′)) ⟩
          ! P ∣ ! Q

        (inj₂ ( refl , Q′ , P′ , c
              , sum-right Q⟶Q′ , sum-left P⟶P′
              , R∼![P⊕Q]∣Q′∣P′
              )) →
          R                        ∼⟨ R∼![P⊕Q]∣Q′∣P′ ⟩
          (! (P ⊕ Q) ∣ Q′) ∣ P′    ∼⟨ right-lemma ∣-cong′ reflexive ⟩
          (! P ∣ (! Q ∣ Q′)) ∣ P′  ∼⟨ swap-rightmost ⟩■
          (! P ∣ P′) ∣ (! Q ∣ Q′)  [ τ ]⟵⟨ par-τ′ (sym $ co-involutive c)
                                                  (replication (par-right P⟶P′))
                                                  (replication (par-right Q⟶Q′)) ⟩
          ! P ∣ ! Q

        (inj₂ ( refl , Q′ , Q″ , c
              , sum-right Q⟶Q′ , sum-right Q⟶Q″
              , R∼![P⊕Q]∣Q′∣Q″
              )) →
          R                        ∼⟨ R∼![P⊕Q]∣Q′∣Q″ ⟩
          (! (P ⊕ Q) ∣ Q′) ∣ Q″    ∼⟨ τ-lemma₃ ⟩■
          ! P ∣ ((! Q ∣ Q′) ∣ Q″)  [ τ ]⟵⟨ par-right (replication (par-τ (replication (par-right Q⟶Q′)) Q⟶Q″)) ⟩
          ! P ∣ ! Q

    rl : ∀ {S μ} →
         ! P ∣ ! Q [ μ ]⟶ S →
         ∃ λ R → ! (P ⊕ Q) [ μ ]⟶ R × [ i ] R ∼′ S
    rl (par-left {P′ = S} !P⟶S) =
      case 6-1-3-2 !P⟶S
        return (const $ ∃ λ _ → _ × [ i ] _ ∼′ _)
        of λ where
        (inj₁ (P′ , P⟶P′ , S∼!P∣P′)) →
          ! (P ⊕ Q)         ⟶⟨ replication (par-right (sum-left P⟶P′)) ⟩ʳˡ
          ! (P ⊕ Q) ∣ P′    ∼⟨ left-lemma ⟩
          (! P ∣ P′) ∣ ! Q  ∼⟨ symmetric S∼!P∣P′ ∣-cong reflexive ⟩■
          S ∣ ! Q

        (inj₂ (refl , P′ , P″ , a , P⟶P′ , P⟶P″ , S∼!P∣P′∣P″)) →
          ! (P ⊕ Q)                [ τ ]⟶⟨ replication (par-τ (replication (par-right (sum-left P⟶P′)))
                                                              (sum-left P⟶P″)) ⟩ʳˡ
          (! (P ⊕ Q) ∣ P′) ∣ P″    ∼⟨ τ-lemma₁ ⟩
          ((! P ∣ P′) ∣ P″) ∣ ! Q  ∼⟨ symmetric S∼!P∣P′∣P″ ∣-cong reflexive ⟩■
          S ∣ ! Q

    rl (par-right {Q′ = S} !Q⟶S) =
      case 6-1-3-2 !Q⟶S
        return (const $ ∃ λ _ → _ × [ i ] _ ∼′ _)
        of λ where
        (inj₁ (Q′ , Q⟶Q′ , S∼!Q∣Q′)) →
          ! (P ⊕ Q)         ⟶⟨ replication (par-right (sum-right Q⟶Q′)) ⟩ʳˡ
          ! (P ⊕ Q) ∣ Q′    ∼⟨ right-lemma ⟩
          ! P ∣ (! Q ∣ Q′)  ∼⟨ reflexive ∣-cong symmetric S∼!Q∣Q′ ⟩■
          ! P ∣ S

        (inj₂ (refl , Q′ , Q″ , a , Q⟶Q′ , Q⟶Q″ , S∼!Q∣Q′∣Q″)) →
          ! (P ⊕ Q)                [ τ ]⟶⟨ replication (par-τ (replication (par-right (sum-right Q⟶Q′)))
                                                              (sum-right Q⟶Q″)) ⟩ʳˡ
          (! (P ⊕ Q) ∣ Q′) ∣ Q″    ∼⟨ τ-lemma₃ ⟩
          ! P ∣ ((! Q ∣ Q′) ∣ Q″)  ∼⟨ reflexive ∣-cong symmetric S∼!Q∣Q′∣Q″ ⟩■
          ! P ∣ S

    rl (par-τ {P′ = S} {Q′ = S′} !P⟶S !Q⟶S′) =
      case 6-1-3-2 !P⟶S ,′ 6-1-3-2 !Q⟶S′ of λ where
        (inj₁ (P′ , P⟶P′ , S∼!P∣P′) ,
         inj₁ (Q′ , Q⟶Q′ , S′∼!Q∣Q′)) →
          ! (P ⊕ Q)                [ τ ]⟶⟨ replication (par-τ (replication (par-right (sum-left P⟶P′)))
                                                                                (sum-right Q⟶Q′)) ⟩ʳˡ
          (! (P ⊕ Q) ∣ P′) ∣ Q′    ∼⟨ τ-lemma₂ ⟩
          (! P ∣ P′) ∣ (! Q ∣ Q′)  ∼⟨ symmetric (S∼!P∣P′ ∣-cong S′∼!Q∣Q′) ⟩■
          S ∣ S′

        (inj₁ _ , inj₂ (() , _))
        (inj₂ (() , _) , _)

  6-2-17-2′ : ∀ {i P Q} → [ i ] ! (P ⊕ Q) ∼′ ! P ∣ ! Q
  force 6-2-17-2′ = 6-2-17-2

6-2-17-3 : ∀ {P} → ! P ∣ ! P ∼ ! P
6-2-17-3 {P} =
  ! P ∣ ! P  ∼⟨ symmetric 6-2-17-2 ⟩
  ! (P ⊕ P)  ∼⟨ !-cong ⊕-idempotent ⟩■
  ! P

-- A result mentioned in the proof of 6.2.17 (4) in "Enhancements of
-- the bisimulation proof method".

6-2-17-4-lemma : ∀ {P Q μ} → ! P [ μ ]⟶ Q → Q ∼ ! P ∣ Q
6-2-17-4-lemma {P} {Q} !P⟶Q = case 6-1-3-2 !P⟶Q of λ where
  (inj₁ (P′ , P⟶P′ , Q∼!P∣P′)) →
    Q                 ∼⟨ Q∼!P∣P′ ⟩
    ! P ∣ P′          ∼⟨ symmetric 6-2-17-3 ∣-cong reflexive ⟩
    (! P ∣ ! P) ∣ P′  ∼⟨ symmetric ∣-assoc ⟩
    ! P ∣ (! P ∣ P′)  ∼⟨ reflexive ∣-cong symmetric Q∼!P∣P′ ⟩■
    ! P ∣ Q

  (inj₂ (_ , P′ , P″ , _ , P⟶P′ , P⟶P″ , Q∼!P∣P′∣P″)) →
    Q                        ∼⟨ Q∼!P∣P′∣P″ ⟩
    (! P ∣ P′) ∣ P″          ∼⟨ symmetric ∣-assoc ⟩
    ! P ∣ (P′ ∣ P″)          ∼⟨ symmetric 6-2-17-3 ∣-cong reflexive ⟩
    (! P ∣ ! P) ∣ (P′ ∣ P″)  ∼⟨ symmetric ∣-assoc ⟩
    ! P ∣ (! P ∣ (P′ ∣ P″))  ∼⟨ reflexive ∣-cong ∣-assoc ⟩
    ! P ∣ ((! P ∣ P′) ∣ P″)  ∼⟨ reflexive ∣-cong symmetric Q∼!P∣P′∣P″ ⟩■
    ! P ∣ Q

mutual

  6-2-17-4 : ∀ {P i} → [ i ] ! ! P ∼ ! P
  6-2-17-4 {P} {i} = ⟨ lr , rl ⟩
    where
    lemma = λ {Q μ} (!P⟶Q : ! P [ μ ]⟶ Q) →
      ! ! P ∣ Q  ∼⟨ 6-2-17-4′ {i = i} ∣-cong′ reflexive ⟩
      ! P ∣ Q    ∼⟨ symmetric (6-2-17-4-lemma !P⟶Q) ⟩■
      Q

    lr : ∀ {Q μ} →
         ! ! P [ μ ]⟶ Q →
         ∃ λ Q′ → ! P [ μ ]⟶ Q′ × [ i ] Q ∼′ Q′
    lr {Q} !!P⟶Q = case 6-1-3-2 !!P⟶Q of λ where
      (inj₁ (Q′ , !P⟶Q′ , Q∼!!P∣Q′)) →
          _
        , !P⟶Q′
        , (Q           ∼⟨ Q∼!!P∣Q′ ⟩
           ! ! P ∣ Q′  ∼⟨ lemma !P⟶Q′ ⟩■
           Q′)

      (inj₂ (refl , Q′ , Q″ , a , !P⟶Q′ , !P⟶Q″ , Q∼!!P∣Q′∣Q″)) →
        case 6-1-3-2 !P⟶Q″ of λ where
          (inj₂ (() , _))
          (inj₁ (Q‴ , P⟶Q‴ , Q″∼!P∣Q‴)) →
            let !P⟶Q′∣Q″ =
                  ! P      [ τ ]⟶⟨ replication (par-τ !P⟶Q′ P⟶Q‴) ⟩
                  Q′ ∣ Q‴
            in
            Q                          ∼⟨ Q∼!!P∣Q′∣Q″ ⟩
            (! ! P ∣ Q′) ∣ Q″          ∼⟨ reflexive ∣-cong Q″∼!P∣Q‴ ⟩
            (! ! P ∣ Q′) ∣ (! P ∣ Q‴)  ∼⟨ swap-in-the-middle ⟩
            (! ! P ∣ ! P) ∣ (Q′ ∣ Q‴)  ∼⟨ 6-1-2 ∣-cong reflexive ⟩
            ! ! P ∣ (Q′ ∣ Q‴)          ∼⟨ lemma !P⟶Q′∣Q″ ⟩■
            Q′ ∣ Q‴                    [ τ ]⟵⟨ !P⟶Q′∣Q″ ⟩
            ! P

    rl : ∀ {Q μ} →
         ! P [ μ ]⟶ Q →
         ∃ λ Q′ → ! ! P [ μ ]⟶ Q′ × [ i ] Q′ ∼′ Q
    rl {Q} !P⟶Q =
      ! ! P      ⟶⟨ replication (par-right !P⟶Q) ⟩ʳˡ
      ! ! P ∣ Q  ∼⟨ lemma !P⟶Q ⟩■
      Q

  6-2-17-4′ : ∀ {P i} → [ i ] ! ! P ∼′ ! P
  force 6-2-17-4′ = 6-2-17-4

------------------------------------------------------------------------
-- An example from "Coinduction All the Way Up" by Pous

module _ (a b : Name-with-kind) where

  A B C D : ∀ {i} → Proc i

  A = name a ∙ name b ∙ D
  B = name a ∙ name b ∙ C

  C = name (co a) · λ { .force → A ∣ C }
  D = name (co a) · λ { .force → B ∣ D }

  mutual

    A∼B : ∀ {i} → [ i ] A ∼ B
    A∼B = refl ∙-cong (refl ∙-cong symmetric C∼D)

    C∼D : ∀ {i} → [ i ] C ∼ D
    C∼D = refl ·-cong λ { .force → A∼B ∣-cong C∼D }

------------------------------------------------------------------------
-- Another example (not taken from Pous and Sangiorgi)

Restricted : Name → Proc ∞
Restricted a = ⟨ν a ⟩ (name (a , true) · λ { .force → ∅ })

Restricted∼∅ : ∀ {a} → Restricted a ∼ ∅
Restricted∼∅ =
  ⟨ (λ { (restriction x≢x action) → ⊥-elim (x≢x refl) })
  , (λ ())
  ⟩

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
{-# OPTIONS --verbose tc.constr.findInScope:15 #-}

module InstanceArguments.03-classes where

open import Algebra
open import Algebra.Structures
open import Algebra.FunctionProperties
open import Data.Nat.Properties as NatProps
open import Data.Nat
open import Data.Bool.Properties using (isCommutativeSemiring-∧-∨)
open import Data.Product using (proj₁)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary

open import Level renaming (zero to lzero; suc to lsuc)

open CommutativeSemiring NatProps.commutativeSemiring using (semiring)
open IsCommutativeSemiring isCommutativeSemiring using (isSemiring)
open IsCommutativeSemiring isCommutativeSemiring-∧-∨ using () renaming (isSemiring to Bool-isSemiring)

record S (A : Set) : Set₁ where
  field
    z : A
    o : A
    _≈_ : Rel A lzero
    _⟨+⟩_ : Op₂ A
    _⟨*⟩_ : Op₂ A
    instance isSemiring' : IsSemiring _≈_ _⟨+⟩_ _⟨*⟩_ z o

instance
  ℕ-S : S ℕ
  ℕ-S = record { z = 0; o = 1;
                 _≈_ = _≡_; _⟨+⟩_ = _+_; _⟨*⟩_ = _*_;
                 isSemiring' = isSemiring }

zero' : {A : Set} → {{aRing : S A}} → A
zero' {{ARing}} = S.z ARing

zero-nat : ℕ
zero-nat = zero'

isZero : {A : Set} {{r : S A}} (let open S r) →
         Zero _≈_ z _⟨*⟩_
isZero {{r}} = IsSemiring.zero (S.isSemiring' r)

useIsZero : 0 * 5 ≡ 0
useIsZero = proj₁ isZero 5

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Yoneda where

open import Level
open import Data.Product

open import Categories.Support.Equivalence
open import Categories.Support.EqReasoning

open import Categories.Category
import Categories.Functor as Cat
open import Categories.Functor using (Functor; module Functor)
open import Categories.Functor.Hom
import Categories.Morphisms as Mor
open import Categories.NaturalTransformation using (NaturalTransformation; module NaturalTransformation)
open import Categories.NaturalIsomorphism
open import Categories.Product
open import Categories.FunctorCategory
open import Categories.Presheaves
open import Categories.Agda

Embed : ∀ {o ℓ e} → (C : Category o ℓ e) → Functor C (Presheaves C)
Embed C = record
  { F₀ = λ x → Hom[ C ][-, x ]
  ; F₁ = λ f → record
    { η = λ X → record
      { _⟨$⟩_ = λ g → f ∘ g
      ; cong = λ x → ∘-resp-≡ʳ x
      }
    ; commute = commute′ f
    }
  ; identity = λ x≡y → trans identityˡ x≡y
  ; homomorphism = λ x≡y → trans (∘-resp-≡ʳ x≡y) assoc
  ; F-resp-≡ = λ f≡g h≡i → ∘-resp-≡ f≡g h≡i
  }
  where
  open Category C
  open Equiv

  .commute′ : {A B X Y : Obj} (f : A ⇒ B) (g : Y ⇒ X) {x y : X ⇒ A} → x ≡ y → f ∘ id ∘ x ∘ g ≡ id ∘ (f ∘ y) ∘ g
  commute′ f g {x} {y} x≡y =
    begin
      f ∘ id ∘ x ∘ g
    ↑⟨ assoc ⟩
      (f ∘ id) ∘ x ∘ g
    ≈⟨ ∘-resp-≡ˡ id-comm ⟩
      (id ∘ f) ∘ x ∘ g
    ≈⟨ ∘-resp-≡ʳ (∘-resp-≡ˡ x≡y) ⟩
      (id ∘ f) ∘ y ∘ g
    ≈⟨ assoc ⟩
      id ∘ f ∘ y ∘ g
    ↑⟨ ∘-resp-≡ʳ assoc ⟩
      id ∘ (f ∘ y) ∘ g
    ∎
    where open HomReasoning

module Embed {o ℓ e} C = Functor (Embed {o} {ℓ} {e} C)

Nat[Embed[_][c],F] : ∀ {o ℓ e} → (C : Category o ℓ e) -> Functor (Product (Presheaves C) (Category.op C)) (ISetoids _ _)
Nat[Embed[ C ][c],F] = Hom[ Presheaves C ][-,-] Cat.∘ ((Embed.op C Cat.∘ snd) ※ fst)
 where
   fst = πˡ {C = Presheaves C} {D = Category.op C}
   snd = πʳ {C = Presheaves C} {D = Category.op C}

F[c∈_] : ∀ {o ℓ e} → (C : Category o ℓ e) -> Functor (Product (Presheaves C) (Category.op C)) (ISetoids _ _)
F[c∈_] {o} {ℓ} {e} C = Lift-IS (suc e ⊔ suc ℓ ⊔ o) (o ⊔ ℓ) Cat.∘ eval {C = Category.op C} {D = ISetoids ℓ e}

yoneda : ∀ {o ℓ e} → (C : Category o ℓ e) -> NaturalIsomorphism Nat[Embed[ C ][c],F] F[c∈ C ]
yoneda C = record { F⇒G = F⇒G; F⇐G = F⇐G; iso = iso }
 where
  open NaturalTransformation
  open Categories.Functor.Functor
  open import Categories.Support.SetoidFunctions
  module C = Category C
  open C.Equiv
  module M = Mor (ISetoids _ _)
  F⇒G : NaturalTransformation Nat[Embed[ C ][c],F] F[c∈ C ]
  F⇒G = record {
   η = λ {(F , c) →
          record { _⟨$⟩_ = λ ε → lift (η ε c ⟨$⟩ C.id);
                   cong  = λ x → lift (x refl) }};
   commute = λ { {F , c₁} {G , c₂} (ε , f) {φ} {ψ} φ≡ψ → lift
     (let module s = Setoid (F₀ G c₂)
          module sr = SetoidReasoning (F₀ G c₂)
          module t = Setoid (F₀ F c₂)
          module tr = SetoidReasoning (F₀ F c₂)
       in s.sym (sr.begin
       F₁ G f ⟨$⟩ (η ε c₁ ⟨$⟩ (η ψ c₁ ⟨$⟩ C.id))
         sr.↑⟨ commute ε f (Setoid.refl (F₀ F c₁)) ⟩
       η ε c₂ ⟨$⟩ (F₁ F f ⟨$⟩ (η ψ c₁ ⟨$⟩ C.id))
         sr.↓⟨ cong (η ε c₂) (tr.begin
               F₁ F f ⟨$⟩ (η ψ c₁ ⟨$⟩ C.id)
                 tr.↑⟨ commute ψ f (refl {x = C.id}) ⟩
               η ψ c₂ ⟨$⟩ C.id C.∘ C.id C.∘ f
                 tr.↑⟨ φ≡ψ (trans C.identityʳ (trans (sym C.identityˡ) (sym C.identityˡ))) ⟩
               η φ c₂ ⟨$⟩ f C.∘ C.id
                 tr.∎) ⟩
       η ε c₂ ⟨$⟩ (η φ c₂ ⟨$⟩ f C.∘ C.id) sr.∎  )) }}

  F⇐G : NaturalTransformation F[c∈ C ] Nat[Embed[ C ][c],F]
  F⇐G = record {
   η = λ {(F , c) →
     record { _⟨$⟩_ = λ Fc →
                record { η = λ X →
                           record { _⟨$⟩_ = λ f → F₁ F f ⟨$⟩ lower Fc;
                                    cong  = λ eq → F-resp-≡ F eq (Setoid.refl (F₀ F c)) };
                         commute = λ {X} {Y} h {f} {g} f≡g →
                           let module s = Setoid (F₀ F Y)
                               module sr = SetoidReasoning (F₀ F Y)
                            in sr.begin
                               F₁ F (C.id C.∘ f C.∘ h) ⟨$⟩ lower Fc
                                 sr.↓⟨  F-resp-≡ F (trans C.identityˡ (C.∘-resp-≡ˡ f≡g)) (Setoid.refl (F₀ F c)) ⟩
                               F₁ F (g C.∘ h) ⟨$⟩ lower Fc
                                 sr.↓⟨ homomorphism F (Setoid.refl (F₀ F c)) ⟩
                               F₁ F h ⟨$⟩ (F₁ F g ⟨$⟩ lower Fc)
                                 sr.∎ };
              cong  = λ i≡j {X} {f} {g} f≡g → F-resp-≡ F f≡g (lower i≡j) }};
   commute = λ { {F , c₁} {G , c₂} (ε , e) {lift i} {lift j} i≡j {X} {f} {g} f≡g →
     let module s = Setoid (F₀ G X)
         module sr = SetoidReasoning (F₀ G X)
      in sr.begin
         F₁ G f ⟨$⟩ (F₁ G e ⟨$⟩ (η ε c₁ ⟨$⟩ i))
           sr.↑⟨ homomorphism G {f = e} {g = f} (Setoid.refl (F₀ G c₁)) ⟩
         F₁ G (e C.∘ f) ⟨$⟩ (η ε c₁ ⟨$⟩ i)
           sr.↑⟨ commute ε (e C.∘ f) (Setoid.refl (F₀ F c₁)) ⟩
         η ε X ⟨$⟩ (F₁ F (e C.∘ f) ⟨$⟩ i)
           sr.↓⟨ cong (η ε X) (F-resp-≡ F (C.∘-resp-≡ʳ f≡g) (lower i≡j)) ⟩
         η ε X ⟨$⟩ (F₁ F (e C.∘ g) ⟨$⟩ j)
           sr.∎}}

  module F⇐G = NaturalTransformation F⇐G
  module F⇒G = NaturalTransformation F⇒G

  iso : (X : Category.Obj (Product (Presheaves C) C.op)) → M.Iso (F⇒G.η X) (F⇐G.η X)
  iso (F , c) = record {
    isoˡ = λ { {ε₁} {ε₂} ε₁≡ε₂ {X} {f} {g} f≡g →
      let module s = Setoid (F₀ F X)
          open SetoidReasoning (F₀ F X)
       in begin
           F₁ F f ⟨$⟩ (η ε₁ c ⟨$⟩ C.id)
             ↑⟨ commute ε₁ f {C.id} {C.id} refl ⟩
           η ε₁ X ⟨$⟩ C.id C.∘ C.id C.∘ f
             ↓⟨ ε₁≡ε₂ (trans C.identityˡ (trans C.identityˡ f≡g)) ⟩
           η ε₂ X ⟨$⟩ g
             ∎ };
    isoʳ = λ eq → lift (identity F (lower eq)) }

yoneda-iso : ∀ {o ℓ e} → (C : Category o ℓ e) (c d : Category.Obj C) ->
               let open Mor (ISetoids _ _) in
                  Functor.F₀ Hom[ Presheaves C ][ Embed.F₀ C c ,-] (Embed.F₀ C d)
                ≅ Functor.F₀ (Lift-IS (suc e ⊔ suc ℓ ⊔ o) (o ⊔ ℓ)) (Functor.F₀ (Embed.F₀ C d) c)
yoneda-iso C c d = record { f = ⇒.η X; g = ⇐.η X;
                            iso = iso X }
  where
    open NaturalIsomorphism (yoneda C)
    module iso F,c = Mor.Iso (iso F,c)
    X = ((Embed.F₀ C d) , c)

yoneda-inj : ∀ {o ℓ e} → (C : Category o ℓ e) (c d : Category.Obj C) -> NaturalIsomorphism (Embed.F₀ C c) (Embed.F₀ C d)
              -> Mor._≅_ C c d
yoneda-inj C c d ηiso = record { f = ⇒.η c ⟨$⟩ C.id; g = ⇐.η d ⟨$⟩ C.id;
            iso = record { isoˡ = Lemma.lemma c d ηiso;
                           isoʳ = Lemma.lemma d c (IsEquivalence.sym Categories.NaturalIsomorphism.equiv ηiso)
                         } }
  where
    open import Categories.Support.SetoidFunctions
    open import Relation.Binary
    module C = Category C
    open C.HomReasoning
    module Lemma (c d : C.Obj) (ηiso : NaturalIsomorphism (Embed.F₀ C c) (Embed.F₀ C d)) where
      open NaturalIsomorphism ηiso
      module iso c = Mor.Iso (iso c)
      .lemma : (⇐.η d ⟨$⟩ C.id) C.∘ (⇒.η c ⟨$⟩ C.id) C.≡ C.id
      lemma = begin
                (⇐.η d ⟨$⟩ C.id) C.∘ (⇒.η c ⟨$⟩ C.id)
              ↑⟨ C.identityˡ ⟩
                C.id C.∘ (⇐.η d ⟨$⟩ C.id) C.∘ (⇒.η c ⟨$⟩ C.id)
              ↑⟨ ⇐.commute (⇒.η c ⟨$⟩ C.id) {C.id} C.Equiv.refl ⟩
                ⇐.η c ⟨$⟩ C.id C.∘ C.id C.∘ (⇒.η c ⟨$⟩ C.id)
              ↓⟨ cong (⇐.η c) (C.Equiv.trans C.identityˡ C.identityˡ) ⟩
                ⇐.η c ⟨$⟩ (⇒.η c ⟨$⟩ C.id)
              ↓⟨ iso.isoˡ c C.Equiv.refl ⟩
                C.id
              ∎
    open NaturalIsomorphism ηiso

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
module Common where

open import Data.String
     using (String)

-- Basic sorts -----------------------------------------------------------------

Id : Set
Id = String

max_stars_repo_name: d-plaindoux/colca

max_issues_repo_name: d-plaindoux/colca

max_forks_repo_name: d-plaindoux/colca


text:
{-# OPTIONS --cubical #-}
module Multidimensional.Data.DirNum where

open import Multidimensional.Data.DirNum.Base public

open import Multidimensional.Data.DirNum.Properties public

max_stars_repo_name: wrrnhttn/agda-cubical-multidimensional

max_issues_repo_name: wrrnhttn/agda-cubical-multidimensional

max_forks_repo_name: wrrnhttn/agda-cubical-multidimensional