text:
{-# OPTIONS --rewriting #-}
module Auxiliary.RewriteLemmas where

open import Data.Nat
open import Data.Fin hiding (_+_ ; _<_ ; _≤_)
open import Data.Fin.Properties

open import Relation.Binary.PropositionalEquality hiding (Extensionality)

open import Agda.Builtin.Equality.Rewrite

private
  variable
    m n : ℕ

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

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

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

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

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

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

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

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

{-# REWRITE n+sucm #-}

n=fromℕtoℕn : (toℕ (fromℕ n)) ≡ n
n=fromℕtoℕn {n} = toℕ-fromℕ n

{-# REWRITE n=fromℕtoℕn #-}

sucn∸suctoℕx≡n∸toℕx : {n : ℕ} {x : Fin n} → suc (n ∸ suc (toℕ x)) ≡ n ∸ (toℕ x)
sucn∸suctoℕx≡n∸toℕx {suc n} {zero} = refl
sucn∸suctoℕx≡n∸toℕx {suc n} {suc x} = sucn∸suctoℕx≡n∸toℕx {n}{x}

sym-sucn∸suctoℕx≡n∸toℕx : {n : ℕ} {x : Fin n} → n ∸ (toℕ x) ≡ suc (n ∸ suc (toℕ x))
sym-sucn∸suctoℕx≡n∸toℕx {suc n} {x} = sym (sucn∸suctoℕx≡n∸toℕx {suc n} {x})

----------------------------------------------------------------------
-- some more required properties on natural numbers and fin

toℕx≤n : {n : ℕ} {x : Fin n} → toℕ x ≤ n
toℕx≤n {suc n} {zero} = z≤n
toℕx≤n {suc n} {suc x} = s≤s toℕx≤n

toℕx≤n' : {n : ℕ} {x : Fin (suc n)} → toℕ x ≤ n
toℕx≤n' {zero} {zero} = z≤n
toℕx≤n' {suc n} {zero} = z≤n
toℕx≤n' {suc n} {suc x} = s≤s (toℕx≤n'{n}{x})

n∸x+x≡n : {n x : ℕ} → x ≤ n  → n ∸ x + x ≡ n
n∸x+x≡n {zero} {zero} le = refl
n∸x+x≡n {zero} {suc x} ()
n∸x+x≡n {suc n} {zero} le = refl
n∸x+x≡n {suc n} {suc x} (s≤s le) = cong suc (n∸x+x≡n le)

toℕx<n : {n : ℕ} {x : Fin n} → toℕ x < n
toℕx<n {suc n} {zero} = s≤s z≤n
toℕx<n {suc n} {suc x} = s≤s toℕx<n

n∸x≡suc[n∸sucx] : {n x : ℕ} → x < n → n ∸ x ≡ suc (n ∸ (suc x))
n∸x≡suc[n∸sucx] {suc n} {zero} le = refl
n∸x≡suc[n∸sucx] {suc n} {suc x} (s≤s le) = n∸x≡suc[n∸sucx] le

suc[n+x]≡n+sucx : {n x : ℕ} → suc (n + x) ≡ (n + suc x)
suc[n+x]≡n+sucx {zero} {x} = refl
suc[n+x]≡n+sucx {suc n} {x} = refl

suc[n∸sucx+x]≡n : {n x : ℕ} → x < n → suc (n ∸ (suc x) + x) ≡ n
suc[n∸sucx+x]≡n {suc n} {zero} le = refl
suc[n∸sucx+x]≡n {suc n} {suc x} (s≤s le) = cong suc (suc[n∸sucx+x]≡n {n} {x} le)

suc[n∸suc[toℕi]+toℕi]≡n : {n : ℕ} {i : Fin n} → suc (n ∸ (suc (toℕ i)) + toℕ i) ≡ n
suc[n∸suc[toℕi]+toℕi]≡n {suc n} {i} = suc[n∸sucx+x]≡n{suc n}{toℕ i} toℕx<n

{-# REWRITE suc[n∸suc[toℕi]+toℕi]≡n #-}

<suc : {n x : ℕ} → x < n → x < suc n
<suc {suc n} {zero} le = s≤s z≤n
<suc {suc n} {suc x} (s≤s le) = s≤s (<suc le)

max_stars_repo_name: peterthiemann/dual-session

max_issues_repo_name: peterthiemann/dual-session

max_forks_repo_name: peterthiemann/dual-session


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

open import lib.Basics
open import lib.cubical.Square
open import lib.types.CommutingSquare
open import lib.types.Paths
open import lib.types.Pushout
open import lib.types.Sigma
open import lib.types.Span

module lib.types.PushoutFmap where

module PushoutFmap {i₀ j₀ k₀ i₁ j₁ k₁} {span₀ : Span {i₀} {j₀} {k₀}}
  {span₁ : Span {i₁} {j₁} {k₁}} (span-map : SpanMap span₀ span₁)
  = PushoutRec {d = span₀} {D = Pushout span₁}
    (left ∘ SpanMap.hA span-map) (right ∘ SpanMap.hB span-map)
    -- the following concatenation arrangement works well with [Susp-fmap].
    (λ c →  ( ap left (SpanMap.f-commutes span-map □$ c)
            ∙ glue (SpanMap.hC span-map c))
         ∙' ap right (! (SpanMap.g-commutes span-map □$ c)))

Pushout-fmap = PushoutFmap.f

Pushout-fmap-∘ : ∀ {i₀ j₀ k₀ i₁ j₁ k₁ i₂ j₂ k₂} {span₀ : Span {i₀} {j₀} {k₀}}
  {span₁ : Span {i₁} {j₁} {k₁}} {span₂ : Span {i₂} {j₂} {k₂}}
  (span-map₁₂ : SpanMap span₁ span₂) (span-map₀₁ : SpanMap span₀ span₁)
  → ∀ p → Pushout-fmap (SpanMap-∘ span-map₁₂ span-map₀₁) p
       == Pushout-fmap span-map₁₂ (Pushout-fmap span-map₀₁ p)
Pushout-fmap-∘ {span₀ = span₀} {span₁} span-map₁₂ span-map₀₁
  = Pushout-elim (λ _ → idp) (λ _ → idp) lemma
  where
    module span-map₀₁ = SpanMap span-map₀₁
    module span-map₁₂ = SpanMap span-map₁₂
    ap-mega-assoc : ∀ {i} {A : Type i} {a₀ a₁ a₂ a₃ a₄ a₅ : A}
      (p₀ : a₀ == a₁) (p₁ : a₁ == a₂) (p₂ : a₂ == a₃) (p₃ : a₃ == a₄) (p₄ : a₄ == a₅)
      → (p₀ ∙ ((p₁ ∙ p₂) ∙' p₃)) ∙' p₄ == ((p₀ ∙ p₁) ∙ p₂) ∙' (p₃ ∙ p₄)
    ap-mega-assoc idp p₁ p₂ idp p₄ = idp
    abstract
      lemma : ∀ c → idp == idp
        [ (λ p → Pushout-fmap (SpanMap-∘ span-map₁₂ span-map₀₁) p
              == Pushout-fmap span-map₁₂ (Pushout-fmap span-map₀₁ p))
          ↓ glue c ]
      lemma c = ↓-='-in' $
        ap (Pushout-fmap span-map₁₂ ∘ Pushout-fmap span-map₀₁) (glue c)
          =⟨ ap-∘ (Pushout-fmap span-map₁₂) (Pushout-fmap span-map₀₁) (glue c) ⟩
        ap (Pushout-fmap span-map₁₂) (ap (Pushout-fmap span-map₀₁) (glue c))
          =⟨ PushoutFmap.glue-β span-map₀₁ c |in-ctx ap (Pushout-fmap span-map₁₂) ⟩
        ap (Pushout-fmap span-map₁₂)
          ( ( ap left (span-map₀₁.f-commutes □$ c)
              ∙ glue (span-map₀₁.hC c))
            ∙' ap right (! (span-map₀₁.g-commutes □$ c)))
          =⟨ ap-∙' (Pushout-fmap span-map₁₂)
              (ap left (span-map₀₁.f-commutes □$ c) ∙ glue (span-map₀₁.hC c))
              (ap right (! (span-map₀₁.g-commutes □$ c))) ⟩
        ap (Pushout-fmap span-map₁₂) ( ap left (span-map₀₁.f-commutes □$ c)
                                       ∙ glue (span-map₀₁.hC c))
        ∙' ap (Pushout-fmap span-map₁₂) (ap right (! (span-map₀₁.g-commutes □$ c)))
          =⟨ ap2 _∙'_ (ap-∙ (Pushout-fmap span-map₁₂)
                        (ap left (span-map₀₁.f-commutes □$ c))
                        (glue (span-map₀₁.hC c)))
                      (∘-ap (Pushout-fmap span-map₁₂) right (! (span-map₀₁.g-commutes □$ c))) ⟩
        ( ap (Pushout-fmap span-map₁₂) (ap left (span-map₀₁.f-commutes □$ c))
          ∙ ap (Pushout-fmap span-map₁₂) (glue (span-map₀₁.hC c)))
        ∙' ap (right ∘ span-map₁₂.hB) (! (span-map₀₁.g-commutes □$ c))
          =⟨ ap2 _∙'_
              -- favonia: for some reasons Agda seems to need this.
              {x = ap (Pushout-fmap span-map₁₂) (ap left (span-map₀₁.f-commutes □$ c))
                 ∙ ap (Pushout-fmap span-map₁₂) (glue (span-map₀₁.hC c))}
              (ap2 _∙_
                (∘-ap (Pushout-fmap span-map₁₂) left (span-map₀₁.f-commutes □$ c))
                (PushoutFmap.glue-β span-map₁₂ (span-map₀₁.hC c)))
              (ap-∘ right span-map₁₂.hB (! (span-map₀₁.g-commutes □$ c))) ⟩
        ( ap (left ∘ span-map₁₂.hA) (span-map₀₁.f-commutes □$ c)
          ∙ ( ( ap left (span-map₁₂.f-commutes □$ span-map₀₁.hC c)
              ∙ glue (span-map₁₂.hC (span-map₀₁.hC c)))
            ∙' ap right (! (span-map₁₂.g-commutes □$ span-map₀₁.hC c))))
        ∙' ap right (ap span-map₁₂.hB (! (span-map₀₁.g-commutes □$ c)))
          =⟨ ap-mega-assoc
              (ap (left ∘ span-map₁₂.hA) (span-map₀₁.f-commutes □$ c))
              (ap left (span-map₁₂.f-commutes □$ span-map₀₁.hC c))
              (glue (span-map₁₂.hC (span-map₀₁.hC c)))
              (ap right (! (span-map₁₂.g-commutes □$ span-map₀₁.hC c)))
              (ap right (ap span-map₁₂.hB (! (span-map₀₁.g-commutes □$ c)))) ⟩
        ( ( ap (left ∘ span-map₁₂.hA) (span-map₀₁.f-commutes □$ c)
            ∙ ap left (span-map₁₂.f-commutes □$ span-map₀₁.hC c))
          ∙ glue (span-map₁₂.hC (span-map₀₁.hC c)))
        ∙'( ap right (! (span-map₁₂.g-commutes □$ span-map₀₁.hC c))
            ∙ ap right (ap span-map₁₂.hB (! (span-map₀₁.g-commutes □$ c))))
          =⟨ ap2 _∙'_
              ( ap-∘ left span-map₁₂.hA (span-map₀₁.f-commutes □$ c)
                |in-ctx _∙ ap left (span-map₁₂.f-commutes □$ span-map₀₁.hC c)
                |in-ctx _∙ glue (span-map₁₂.hC (span-map₀₁.hC c)))
              ( ∙-ap right
                  (! (span-map₁₂.g-commutes □$ span-map₀₁.hC c))
                  (ap span-map₁₂.hB (! (span-map₀₁.g-commutes □$ c)))) ⟩
        ( ( ap left (ap span-map₁₂.hA (span-map₀₁.f-commutes □$ c))
            ∙ ap left (span-map₁₂.f-commutes □$ span-map₀₁.hC c))
          ∙ glue (span-map₁₂.hC (span-map₀₁.hC c)))
        ∙' ap right
             ( ! (span-map₁₂.g-commutes □$ span-map₀₁.hC c)
               ∙ ap span-map₁₂.hB (! (span-map₀₁.g-commutes □$ c)))
          =⟨ ap2 _∙'_
              ( ∙-ap left
                  (ap span-map₁₂.hA (span-map₀₁.f-commutes □$ c))
                  (span-map₁₂.f-commutes □$ span-map₀₁.hC c)
                |in-ctx _∙ glue (span-map₁₂.hC (span-map₀₁.hC c)))
              ( ap-! span-map₁₂.hB (span-map₀₁.g-commutes □$ c)
                |in-ctx ! (span-map₁₂.g-commutes □$ span-map₀₁.hC c) ∙_
                |in-ctx ap right) ⟩
        ( ap left (CommSquare-∘v span-map₁₂.f-commutes span-map₀₁.f-commutes □$ c)
          ∙ glue (span-map₁₂.hC (span-map₀₁.hC c)))
        ∙' ap right
             ( ! (span-map₁₂.g-commutes □$ span-map₀₁.hC c)
               ∙ ! (ap span-map₁₂.hB (span-map₀₁.g-commutes □$ c)))
          =⟨ ∙-!
               (span-map₁₂.g-commutes □$ span-map₀₁.hC c)
               (ap span-map₁₂.hB (span-map₀₁.g-commutes □$ c))
            |in-ctx ap right
            |in-ctx
              ( ap left (CommSquare-∘v span-map₁₂.f-commutes span-map₀₁.f-commutes □$ c)
                ∙ glue (span-map₁₂.hC (span-map₀₁.hC c)))
              ∙'_ ⟩
        ( ap left (CommSquare-∘v span-map₁₂.f-commutes span-map₀₁.f-commutes □$ c)
          ∙ glue (span-map₁₂.hC (span-map₀₁.hC c)))
        ∙' ap right (! (CommSquare-∘v span-map₁₂.g-commutes span-map₀₁.g-commutes □$ c))
          =⟨ ! (PushoutFmap.glue-β (SpanMap-∘ span-map₁₂ span-map₀₁) c) ⟩
        ap (Pushout-fmap (SpanMap-∘ span-map₁₂ span-map₀₁)) (glue c)
          =∎

∘-Pushout-fmap : ∀ {i₀ j₀ k₀ i₁ j₁ k₁ i₂ j₂ k₂} {span₀ : Span {i₀} {j₀} {k₀}}
  {span₁ : Span {i₁} {j₁} {k₁}} {span₂ : Span {i₂} {j₂} {k₂}}
  (span-map₁₂ : SpanMap span₁ span₂) (span-map₀₁ : SpanMap span₀ span₁)
  → ∀ p → Pushout-fmap span-map₁₂ (Pushout-fmap span-map₀₁ p)
       == Pushout-fmap (SpanMap-∘ span-map₁₂ span-map₀₁) p
∘-Pushout-fmap span-map₁₂ span-map₀₁ p = ! (Pushout-fmap-∘ span-map₁₂ span-map₀₁ p)

module _ {i₀ j₀ k₀ i₁ j₁ k₁} {span₀ : Span {i₀} {j₀} {k₀}}
  {span₁ : Span {i₁} {j₁} {k₁}} (span-equiv : SpanEquiv span₀ span₁) where

  private
    module span₀ = Span span₀
    module span₁ = Span span₁
    span-to = fst span-equiv
    span-from = fst (SpanEquiv-inverse span-equiv)
    module span-to = SpanMap span-to
    module span-from = SpanMap span-from
    module To = PushoutFmap span-to
    module From = PushoutFmap span-from
    span-ise = snd span-equiv
    hA-ise = fst span-ise
    hB-ise = fst (snd span-ise)
    hC-ise = snd (snd span-ise)
    module hA-ise = is-equiv hA-ise
    module hB-ise = is-equiv hB-ise
    module hC-ise = is-equiv hC-ise

    to = To.f
    from = From.f

    abstract
      to-from' : ∀ y → Pushout-fmap (SpanMap-∘ span-to span-from) y == y
      to-from' = Pushout-elim (ap left ∘ hA-ise.f-g) (ap right ∘ hB-ise.f-g)
        (λ c → ↓-app=idf-from-square $
                PushoutFmap.glue-β (SpanMap-∘ span-to span-from) c
            ∙v⊡ ap2 _∙'_
                  (CommSquare-inverse-inv-r span-to.f-commutes hC-ise hA-ise c
                    |in-ctx ap left |in-ctx _∙ glue (span-to.hC (span-from.hC c)))
                  (CommSquare-inverse-inv-r span-to.g-commutes hC-ise hB-ise c
                    |in-ctx ! |in-ctx ap right)
            ∙v⊡ ap2 _∙'_
                  ( ap-∙ left (hA-ise.f-g (span₁.f c)) (! (ap span₁.f (hC-ise.f-g c)))
                    |in-ctx _∙ glue (span-to.hC (span-from.hC c)))
                  ( !-∙ (hB-ise.f-g (span₁.g c)) (! (ap span₁.g (hC-ise.f-g c)))
                    |in-ctx ap right)
            ∙v⊡ ap2 _∙'_
                  ( ap-! left (ap span₁.f (hC-ise.f-g c))
                    |in-ctx ap left (hA-ise.f-g (span₁.f c)) ∙_
                    |in-ctx _∙ glue (span-to.hC (span-from.hC c)))
                  ( ap-∙ right
                    (! (! (ap span₁.g (hC-ise.f-g c))))
                    (! (hB-ise.f-g (span₁.g c))))
            ∙v⊡ ( ap2 _∙_
                    ( !-! (ap span₁.g (hC-ise.f-g c))
                      |in-ctx ap right)
                    ( ap-! right (hB-ise.f-g (span₁.g c)))
                  |in-ctx ( ( ap left (hA-ise.f-g (span₁.f c))
                              ∙ ! (ap left (ap span₁.f (hC-ise.f-g c))))
                            ∙ glue (span-to.hC (span-from.hC c)))
                          ∙'_)
            ∙v⊡ ap2 _∙'_
                  ( ∘-ap left span₁.f (hC-ise.f-g c)
                    |in-ctx !
                    |in-ctx ap left (hA-ise.f-g (span₁.f c)) ∙_
                    |in-ctx _∙ glue (span-to.hC (span-from.hC c)))
                  ( ∘-ap right span₁.g (hC-ise.f-g c)
                    |in-ctx _∙ ! (ap right (hB-ise.f-g (span₁.g c))))
            ∙v⊡ ( ( lt-square (ap left (hA-ise.f-g (span₁.f c)))
                    ⊡h rt-square (ap (left ∘ span₁.f) (hC-ise.f-g c)))
                  ⊡h square-symmetry (natural-square glue (hC-ise.f-g c)))
            ⊡h' lt-square (ap (right ∘ span₁.g) (hC-ise.f-g c))
            ⊡h rt-square (ap right (hB-ise.f-g (span₁.g c))))

    to-from : ∀ y → to (from y) == y
    to-from y = ∘-Pushout-fmap span-to span-from y ∙ to-from' y

    abstract
      from-to' : ∀ x → Pushout-fmap (SpanMap-∘ span-from span-to) x == x
      from-to' = Pushout-elim (ap left ∘ hA-ise.g-f) (ap right ∘ hB-ise.g-f)
        (λ c → ↓-app=idf-from-square $
                PushoutFmap.glue-β (SpanMap-∘ span-from span-to) c
            ∙v⊡ ap2 _∙'_
                  (CommSquare-inverse-inv-l span-to.f-commutes hC-ise hA-ise c
                    |in-ctx ap left |in-ctx _∙ glue (span-from.hC (span-to.hC c)))
                  (CommSquare-inverse-inv-l span-to.g-commutes hC-ise hB-ise c
                    |in-ctx ! |in-ctx ap right)
            ∙v⊡ ap2 _∙'_
                  ( ap-∙ left (hA-ise.g-f (span₀.f c)) (! (ap span₀.f (hC-ise.g-f c)))
                    |in-ctx _∙ glue (span-from.hC (span-to.hC c)))
                  ( !-∙ (hB-ise.g-f (span₀.g c)) (! (ap span₀.g (hC-ise.g-f c)))
                    |in-ctx ap right)
            ∙v⊡ ap2 _∙'_
                  ( ap-! left (ap span₀.f (hC-ise.g-f c))
                    |in-ctx ap left (hA-ise.g-f (span₀.f c)) ∙_
                    |in-ctx _∙ glue (span-from.hC (span-to.hC c)))
                  ( ap-∙ right
                    (! (! (ap span₀.g (hC-ise.g-f c))))
                    (! (hB-ise.g-f (span₀.g c))))
            ∙v⊡ ( ap2 _∙_
                    ( !-! (ap span₀.g (hC-ise.g-f c))
                      |in-ctx ap right)
                    ( ap-! right (hB-ise.g-f (span₀.g c)))
                  |in-ctx ( ( ap left (hA-ise.g-f (span₀.f c))
                              ∙ ! (ap left (ap span₀.f (hC-ise.g-f c))))
                            ∙ glue (span-from.hC (span-to.hC c)))
                          ∙'_)
            ∙v⊡ ap2 _∙'_
                  ( ∘-ap left span₀.f (hC-ise.g-f c)
                    |in-ctx !
                    |in-ctx ap left (hA-ise.g-f (span₀.f c)) ∙_
                    |in-ctx _∙ glue (span-from.hC (span-to.hC c)))
                  ( ∘-ap right span₀.g (hC-ise.g-f c)
                    |in-ctx _∙ ! (ap right (hB-ise.g-f (span₀.g c))))
            ∙v⊡ ( ( lt-square (ap left (hA-ise.g-f (span₀.f c)))
                    ⊡h rt-square (ap (left ∘ span₀.f) (hC-ise.g-f c)))
                  ⊡h square-symmetry (natural-square glue (hC-ise.g-f c)))
            ⊡h' lt-square (ap (right ∘ span₀.g) (hC-ise.g-f c))
            ⊡h rt-square (ap right (hB-ise.g-f (span₀.g c))))

    from-to : ∀ x → from (to x) == x
    from-to x = ∘-Pushout-fmap span-from span-to x ∙ from-to' x

  Pushout-emap : Pushout span₀ ≃ Pushout span₁
  Pushout-emap = equiv to from to-from from-to

ext: agda

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


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

module sv20.assign1.Second where

{- Code partially taken from the book "Programming Language Foundations in
 - Agda" by Philip Wadler, Wen Kokke, Jeremy Siek and many others. The book
 - can be found at https://plfa.github.io/
 -
 - Based on chapters 6 and 7 - Connectives and Negation
 -  https://plfa.github.io/Connectives/
 -  https://plfa.github.io/Negation/
 -}

open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
open import Relation.Nullary using (¬_)

-- Logic can be formalised as types [1], so the current homework solution uses
-- types and type operations to proof logic operations.
--
-- [1] “Propositions as Types”, Philip Wadler, Communications of the ACM, December 2015.

------------------------------------------------------------------------------------------
--                                   HOMEWORK SOLUTION                                  --
------------------------------------------------------------------------------------------

-- Conjuction is formalised in type systems as product

-- Prove that:   A ⇒ B ⇒ C   from    A ∧ B ⇒ C
proof₁ : ∀ {A B C : Set}
  → (A × B → C)
  -------------
  → (A → B → C)
proof₁ f a b = f ⟨ a , b ⟩

-- Prove that:   (A ⇒ ¬ E ⇒ ¬ C)    from    ((A ∨ B) ⇒ (C ∨ D) ⇒ E)

-- Preliminary proofs
modus-tollens : ∀ {A B : Set}
  → (A → B)
  -------------
  → (¬ B → ¬ A)
modus-tollens a→b = λ{¬b → λ{a → ¬b (a→b a)}}

-- Disjunction is formalised as Union
lemma₁ : ∀ {A B E : Set}
  → (A ⊎ B → E)
  -------------
  → (A → E)
lemma₁ a⊎b→e a = a⊎b→e (inj₁ a)

lemma₂ : ∀ {C D : Set}
  → ¬ (C ⊎ D)
  -------------
  → ¬ C
lemma₂ c⊎d = λ{c → c⊎d (inj₁ c)}

---- And finally the proof
proof₂ : ∀ {A B C D E : Set}
  → (A ⊎ B → C ⊎ D → E)
  ---------------------
  → (A → ¬ E → ¬ C)

proof₂ a⊎b→c⊎d→e a ¬e =
  let
     --   (A ⊎ B → C ⊎ D → E)
     -- → A
     -- ---------------------
     -- → (C ⊎ D → E)
    c⊎d→e = lemma₁ a⊎b→c⊎d→e a

     --   (C ⊎ D → E)
     -- → ¬E
     -- -------------
     -- → ¬ (C ⊎ D)
    ¬c⊎d  = modus-tollens c⊎d→e ¬e

  in
     --   ¬ (C ⊎ D)
     -- -------------
     -- → ¬ C
    lemma₂ ¬c⊎d

-------- Other stuff
stuff₁ : ∀ {C D : Set}
  → ¬ (C ⊎ D)
  -------------
  → (¬ C) × (¬ D)
stuff₁ c⊎d = ⟨ (λ c → c⊎d (inj₁ c)) , (λ d → c⊎d (inj₂ d)) ⟩


text:
open import Relation.Binary.PropositionalEquality

module Experiments.STLCRefPointfree (funext : ∀ {a b} → Extensionality a b) where

open import Level
open import Data.Nat hiding (_^_)
import Data.Unit as Unit
open import Data.List
open import Data.List.Prefix
open import Data.List.Properties.Extra
open import Data.List.All.Properties.Extra
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.Any
open import Data.List.Relation.Unary.All as All
open import Data.Product hiding (curry; swap)
open import Function as Fun using (case_of_)
import Relation.Binary.PropositionalEquality as PEq
import Relation.Binary.HeterogeneousEquality as H
open import Relation.Binary.PropositionalEquality.Extensionality funext
open PEq.≡-Reasoning

-- STLCRef typed syntax
------------------------------------------------------------------------

data Ty : Set where
  unit : Ty
  _⟶_ : (a b : Ty) → Ty
  ref  : Ty → Ty

open import Experiments.Category (⊑-preorder {A = Ty})
open Product
open Exists

Ctx     = List Ty
StoreTy = List Ty

data Expr (Γ : List Ty) : Ty → Set where
  var : ∀ {t} → t ∈ Γ → Expr Γ t
  ƛ     : ∀ {a b} → Expr (a ∷ Γ) b → Expr Γ (a ⟶ b)
  app   : ∀ {a b} → Expr Γ (a ⟶ b) → Expr Γ a → Expr Γ b
  unit  : Expr Γ unit
  ref   : ∀ {t} → Expr Γ t → Expr Γ (ref t)
  !_    : ∀ {t} → Expr Γ (ref t) → Expr Γ t
  _≔_   : ∀ {t} → Expr Γ (ref t) → Expr Γ t → Expr Γ unit

module Values where
  mutual
    Env' : (Γ : Ctx)(Σ : StoreTy) → Set
    Env' Γ Σ = All (λ t → Val' t Σ) Γ

    data Val' : Ty → List Ty → Set where
      unit   : ∀ {Σ} → Val' unit Σ
      clos   : ∀ {Σ Γ a b} → Expr (a ∷ Γ) b → Env' Γ Σ → Val' (a ⟶ b) Σ
      ref    : ∀ {Σ t} → t ∈ Σ → Val' (ref t) Σ

  mutual
    val-mono : ∀ {a Σ Σ'} → Σ ⊑ Σ' → Val' a Σ → Val' a Σ'
    val-mono ext unit = unit
    val-mono ext (clos e E) = clos e (env-mono ext E)
    val-mono ext (ref x) = ref (∈-⊒ x ext)

    val-mono-refl : ∀ {Σ a}(v : Val' a Σ) → val-mono ⊑-refl v ≡ v
    val-mono-refl unit = refl
    val-mono-refl (clos e E) = cong (clos e) (env-mono-refl E)
    val-mono-refl (ref x) = cong ref ∈-⊒-refl

    val-mono-trans : ∀ {a Σ Σ' Σ''}(v : Val' a Σ)(p : Σ' ⊒ Σ)(q : Σ'' ⊒ Σ') → val-mono (⊑-trans p q) v ≡ (val-mono q (val-mono p v))
    val-mono-trans unit p q = refl
    val-mono-trans (clos x E) p q = cong (clos x) (env-mono-trans E p q)
    val-mono-trans (ref x) p q = cong ref (∈-⊒-trans p q)

    env-mono : ∀ {Γ Σ Σ'} → Σ ⊑ Σ' → Env' Γ Σ → Env' Γ Σ'
    env-mono ext [] = []
    env-mono ext (px ∷ E) = (val-mono ext px) ∷ (env-mono ext E)

    env-mono-refl : ∀ {Γ Σ}(E : Env' Γ Σ) → env-mono ⊑-refl E ≡ E
    env-mono-refl [] = refl
    env-mono-refl (px ∷ E) = cong₂ _∷_ (val-mono-refl px) (env-mono-refl E)

    env-mono-trans : ∀ {Γ Σ Σ' Σ''}(E : Env' Γ Σ)(p : Σ' ⊒ Σ)(q : Σ'' ⊒ Σ') → env-mono (⊑-trans p q) E ≡ (env-mono q (env-mono p E))
    env-mono-trans [] p q = refl
    env-mono-trans (px ∷ E) p q = cong₂ _∷_ (val-mono-trans px p q) (env-mono-trans E p q)

    Env : Ctx → MP _
    Env Γ = mp (Env' Γ) (record {
      monotone = env-mono ;
      monotone-refl = env-mono-refl ;
      monotone-trans = env-mono-trans })

    Val : Ty → MP _
    Val a = mp (Val' a) (record {
      monotone = val-mono ;
      monotone-refl = val-mono-refl ;
      monotone-trans = val-mono-trans })

open Values
open import Experiments.StrongMonad Ty Val funext

-- Val constructors
------------------------------------------------------------------------

mkclos : ∀ {Γ a b} → Const (Expr (a ∷ Γ) b) ⊗ Env Γ ⇒ Val (a ⟶ b)
mkclos = mk⇒ (λ{ (e , E) → clos e E}) λ c~c' → refl

mkunit : ⊤ ⇒ Val unit
mkunit = mk⇒ (λ _ → Values.unit) λ c~c' → refl

-- destructors
------------------------------------------------------------------------

destructfun : ∀ {a b} → Val (a ⟶ b) ⇒ (Exists (λ Γ → Const (Expr (a ∷ Γ) b) ⊗ Env Γ))
destructfun = mk⇒ (λ{ (clos x E) → _ , x , E}) λ{ c~c' {clos x E} → refl }

-- state manipulation
------------------------------------------------------------------------

alloc : ∀ {a} → Val a ⇒ M (Val (ref a))
alloc {a} = mk⇒
  (λ v Σ₁ ext μ₁ →
    let ext' = ∷ʳ-⊒ a Σ₁ in
      (Σ₁ ∷ʳ a) ,
      ext' ,
      ((All.map (MP.monotone (Val _) ext') μ₁) all-∷ʳ MP.monotone (Val _) (⊑-trans ext ext') v) ,
      ref (∈-∷ʳ Σ₁ a))
  (λ c~c' {p} → funext³ λ q ext μ →
    mcong {P = (Val (ref a))} refl H.refl
    (H.≡-to-≅ (
      cong (λ u → All.map _ μ all-∷ʳ u)
        (trans
          (sym (MP.monotone-trans (Val a) p c~c' _))
          (cong (λ u → (MP.monotone (Val a) u p)) ⊑-trans-assoc)
        )
    )) H.refl)

load : ∀ {a} → Val (ref a) ⇒ M (Val a)
load  {a} = mk⇒
  (λ v Σ₁ ext μ₁ → case v of λ{
    (ref x) → Σ₁ , ⊑-refl , μ₁ , (∈-all (∈-⊒ x ext) μ₁)
  })
  (λ{ c~c' {ref x} →
      funext³ λ p₁ q r →
      mcong {P = Val _} refl H.refl H.refl
        ((H.cong (λ u → ∈-all u r) (H.≡-to-≅ (sym (∈-⊒-trans c~c' q)))))
  })

store : ∀ {a} → (Val (ref a) ⊗ Val a) ⇒ M ⊤
store = mk⇒
  (λ x Σ₁ ext μ₁ → case x of λ{
    (ref l , v) → Σ₁ , ⊑-refl , (μ₁ All.[ ∈-⊒ l ext ]≔ MP.monotone (Val _) ext v) , Unit.tt
  })
  (λ{ c~c' {ref x , v} →
    funext³ λ p q r →
    mcong {P = ⊤} refl H.refl
      (H.cong₂ (λ u v → r All.[ u ]≔ v)
        (H.≡-to-≅ (sym (∈-⊒-trans c~c' q)))
        (H.≡-to-≅ (sym (MP.monotone-trans (Val _) v _ _))))
      H.refl
  })

-- environment manipulation
------------------------------------------------------------------------

envlookup : ∀ {a Γ} → a ∈ Γ → Env Γ ⇒ Val a
envlookup x = mk⇒ (λ E → All.lookup E x) λ{ c~c' {E} → sym (lem c~c' E x)}
  where
    lem : ∀ {Γ Σ Σ' a} → (p : Σ ⊑ Σ') → (E : Env' Γ Σ) → (e : a ∈ Γ)
        → val-mono p (All.lookup E e) ≡ All.lookup (env-mono p E) e
    lem p (px ∷ E) (here refl) = refl
    lem p (px ∷ E) (there e) = lem p E e

envcons : ∀ {a Γ} → Val a ⊗ Env Γ ⇒ Env (a ∷ Γ)
envcons = mk⇒ (uncurry _∷_) λ c~c' → refl

-- STLCRef interpreter; pointfree style
------------------------------------------------------------------------

open Exponential (sym ⊑-trans-assoc) ⊑-trans-refl ⊑-trans-refl'
open Strong

mutual
  interpclos : ∀ {a b} → Val (a ⟶ b) ⇒ M (Val b) ^ (Val a)
  interpclos = curry (
      elim (
        uncurry₁ eval
        ∘ (xmap (id (Const _)) (envcons ∘ Product.swap (Env _)(Val _)))
        ∘ Product.comm (Const _)(Env _)(Val _)
      )
      ∘ ∃-⊗-comm (λ Γ → Const _ ⊗ Env Γ)(Val _)
      ∘ xmap destructfun (id (Val _)))

  {-# TERMINATING #-}
  eval : ∀ {Γ a} → Expr Γ a → Env Γ ⇒ M (Val a)
  eval (var x) = η (Val _) ∘ envlookup x
  eval (ƛ e) = η (Val _) ∘ mkclos ∘ ⟨ terminal e , id (Env _) ⟩
  eval (app f e) =
    μ (Val _)
    ∘ fmap (ε ∘ xmap interpclos (id (Val _)))
    ∘ μ (Val _ ⊗ Val _)
    ∘ fmap (ts (Val _) (Val _))
    ∘ ts' (Val _) (M (Val _))
    ∘ ⟨ eval f , eval e ⟩
  eval unit = η (Val _) ∘ mkunit ∘ terminal Unit.tt
  eval (ref e) = bind (Val _) alloc ∘ eval e
  eval (! e) = bind (Val _) load ∘ eval e
  eval (e₁ ≔ e₂) =
      fmap mkunit
    ∘ μ ⊤
    ∘ fmap store
    ∘ μ ((Val _) ⊗ (Val _))
    ∘ fmap (ts' (Val _)(Val _))
    ∘ ts (M (Val _))(Val _)
    ∘ ⟨ eval e₁ , eval e₂ ⟩

module Examples where

  test : Expr [] unit
  test = let id = ƛ (var (here refl)) in app (ƛ (app id (var (here refl)))) unit

  test! : apply (eval test) [] [] ⊑-refl [] ≡ ([] , [] , [] , unit)
  test! = refl


text:
module Thesis.Environments where

open import Thesis.Types

open import Base.Data.DependentList public
open import Base.Denotation.Environment Type ⟦_⟧Type public

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
module Control.Monad.State where

open import Prelude
open import Control.Monad.Zero
open import Control.Monad.Identity
open import Control.Monad.Transformer

record StateT {a} (S : Set a) (M : Set a → Set a) (A : Set a) : Set a where
  no-eta-equality
  constructor stateT
  field runStateT : S → M (A × S)

open StateT public

-- Instances --

module _ {a} {S : Set a} {M : Set a → Set a} where

  instance
    FunctorStateT : {{_ : Functor M}} → Functor {a = a} (StateT S M)
    runStateT (fmap {{FunctorStateT}} f m) s = first f <$> runStateT m s

    FunctorZeroStateT : {{_ : FunctorZero M}} → FunctorZero {a = a} (StateT S M)
    runStateT (empty {{FunctorZeroStateT}}) s = empty

    AlternativeStateT : {{_ : Alternative M}} → Alternative {a = a} (StateT S M)
    runStateT (_<|>_ {{AlternativeStateT}} x y) s = runStateT x s <|> runStateT y s

  module _ {{_ : Monad M}} where

    private
      bindStateT : ∀ {A B} → StateT S M A → (A → StateT S M B) → StateT S M B
      runStateT (bindStateT m f) s = runStateT m s >>= λ r → uncurry (runStateT ∘ f) r

    instance
      ApplicativeStateT : Applicative {a = a} (StateT S M)
      runStateT (pure  {{ApplicativeStateT}} x)     s = pure (x , s)
      _<*>_ {{ApplicativeStateT}} = monadAp bindStateT

      MonadStateT : Monad {a = a} (StateT S M)
      _>>=_  {{MonadStateT}} = bindStateT

    liftStateT : {A : Set a} → M A → StateT S M A
    runStateT (liftStateT m) s = m >>= λ x → return (x , s)

    gets : {A : Set a} → (S → A) → StateT S M A
    runStateT (gets f) s = return (f s , s)

    modify : (S → S) → StateT S M S
    runStateT (modify f) s = return (s , f s)

    get : StateT S M S
    get = gets id

    put : S → StateT S M S
    put s = modify (const s)

instance
  TransformerStateT : ∀ {a} {S : Set a} → Transformer (StateT S)
  lift {{TransformerStateT}} = liftStateT

State : ∀ {a} (S : Set a) (A : Set a) → Set a
State S = StateT S Identity

runState : ∀ {a} {S : Set a} {A : Set a} → State S A → S → A × S
runState m s = runIdentity (runStateT m s)

execState : ∀ {a} {S : Set a} {A : Set a} → State S A → S → S
execState m s = snd (runState m s)

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
{-# OPTIONS --safe #-}
module Cubical.Categories.Instances.DistLattice where

open import Cubical.Foundations.Prelude

open import Cubical.Algebra.DistLattice

open import Cubical.Categories.Category
open import Cubical.Categories.Instances.Lattice

open Category

DistLatticeCategory : ∀ {ℓ} (L : DistLattice ℓ) → Category ℓ ℓ
DistLatticeCategory L = LatticeCategory (DistLattice→Lattice L)

max_stars_repo_name: FernandoLarrain/cubical


text:
module #3 where

open import Data.Product
open import Data.Sum
open import Relation.Binary.PropositionalEquality

{-
Exercise 1.3. Derive the induction principle for products indA×B, using only the projections and
the propositional uniqueness principle uppt. Verify that the definitional equalities are valid.
Generalize uppt to Σ-types, and do the same for Σ-types. (This requires concepts from Chapter 2.)
-}

module Product { a b c }{A : Set a}{B : Set b}{C : Set c}(g : A → B → C) where

  uppt : (x : A × B) → (proj₁ x , proj₂ x) ≡ x
  uppt = λ x → refl

  indₓ : ∀{k}(P : A × B → Set k) → ((x : A)(y : B) → P (x , y)) → (x : A × B) → P x
  indₓ P f x = subst P (uppt x) (f (proj₁ x) (proj₂ x))

  indₓ-β : ∀{k}(P : A × B → Set k) → (f : (x : A)(y : B) → P (x , y)) → (x : A)(y : B) → indₓ P f (x , y) ≡ f x y
  indₓ-β P f x y = refl

module Sum { a b c }{A : Set a}{B : A → Set b}{C : Set c}(g : (x : A) → B x → C) where

  uppt : (x : Σ A B) → (proj₁ x , proj₂ x) ≡ x
  uppt = λ x → refl

  ind-Σ : ∀{k}(C : Σ A B → Set k) → ((a : A)(b : B a) → C (a , b)) → (p : Σ A B) → C p
  ind-Σ C f x = subst C (uppt x) (f (proj₁ x) (proj₂ x))

  ind-Σ-β : ∀{k}(C : Σ A B → Set k) → (f : (a : A)(b : B a) → C (a , b)) → (x : A)(y : B x) → ind-Σ C f (x , y) ≡ f x y
  ind-Σ-β C f x y = refl

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


text:
module CoinductiveBuiltinNatural where

open import Imports.Coinduction

data ℕ : Set where
  zero : ℕ
  suc  : (n : ∞ ℕ) → ℕ

{-# BUILTIN NATURAL ℕ    #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

max_stars_repo_name: asr/agda-kanso

max_issues_repo_name: np/agda-git-experiment

max_forks_repo_name: np/agda-git-experiment


text:
-- stuff I did not find in the standard library, but which
-- I might just not have noticed.

module AgdaHelperFunctions where

open import Data.String
open import Data.Sum
open import Category.Monad

infixr 0 _$_
_$_ : {A B : Set} -> (A -> B) -> A -> B
x $ y = x y

bind : {error x y : Set} -> error ⊎ x -> (x -> error ⊎ y) -> error ⊎ y
bind (inj₁ x) f = inj₁ x
bind (inj₂ y) f = f y

SumMonad : {error : Set} -> RawMonad (error ⊎_)
SumMonad  = record
  { return  = inj₂
  ; _>>=_ = bind
  }

bindT : {monadType : Set -> Set}(underlyingMonad : RawMonad monadType){error x y : Set} -> (monadType (error ⊎ x)) -> (x -> monadType (error ⊎ y)) -> monadType (error ⊎ y)
bindT underlyingMonad x f = do
    inj₂ content <- x
      where inj₁ e -> return $ inj₁ e
    f content
  where open RawMonad underlyingMonad

SumMonadT : {monadType : Set -> Set}(underlyingMonad : RawMonad monadType)(error : Set) -> RawMonad (λ x -> monadType (error ⊎ x))
SumMonadT underlyingMonad error = record
  { return = λ x -> r $ inj₂ x
  ; _>>=_ = bindT underlyingMonad
  }
  where open RawMonad underlyingMonad renaming (return to r)

import IO.Primitive as Prim

IOMonad : RawMonad (λ (x : Set) -> Prim.IO x)
IOMonad = record
  { return = Prim.return
  ; _>>=_ = Prim._>>=_
  }


text:
module Eq.Defs where

open import Prelude
open import T
open import Contexts
import SubstTheory

infix 30 _⊆_ _≃_ _≃_

-- General stuff about relations
Rel : Set → Set1
Rel A = A → A → Set

Reflexive : ∀{A} → Rel A → Set
Reflexive R = ∀{x} → R x x
Symmetric : ∀{A} → Rel A → Set
Symmetric R = ∀{x y} → R x y → R y x
Transitive : ∀{A} → Rel A → Set
Transitive R = ∀{x y z} → R x y → R y z → R x z

_⊆_ : ∀{A} → Rel A → Rel A → Set
P ⊆ Q = ∀{x y} → P x y → Q x y
Includes = _⊆_

record IsEquivalence {A : Set}
                     (R : Rel A) : Set  where
  field
    refl_  : Reflexive R
    sym_   : Symmetric R
    trans_ : Transitive R

TRel = (Γ : Ctx) (A : TTp) → Rel (TExp Γ A)
CRel = (A : TTp) → Rel (TExp [] A)

-- Specific relation stuff about T
Congruence : TRel → Set
Congruence R = ∀{Γ} {A} {e e' : TExp Γ A} →
               R Γ A e e' →
               {Γ' : Ctx} {A' : TTp} → (C : TCtx Γ A Γ' A') →
               R Γ' A' (C < e >) (C < e' >)

-- Kleene equivalence
record KleeneEq (e e' : TNat) : Set where
  constructor kleeneq
  field
    n : TNat
    val : TVal n
    E1 : e ~>* n
    E2 : e' ~>* n

_≃_ = KleeneEq

-- Definition of consistency:
-- a relation is consistent if it respects Kleene equivalence
Consistent : TRel → Set
Consistent R = ∀ {e e' : TNat} → R [] nat e e' → e ≃ e'

record IsConsistentCongruence (R : TRel) : Set where
  field
    equiv : ∀{Γ A} → IsEquivalence (R Γ A)
    cong : Congruence R
    consistent : Consistent R

-- Observational equivalence
PCtx : (Γ : Ctx) (A : TTp) → Set
PCtx Γ A = TCtx Γ A [] nat

-- This is a record in the hopes that it will be easier to read.
-- Doing it this way also has a lot of annoying drawbacks when
-- actually proving observational eqs.
record ObservEq (Γ : Ctx) (A : TTp) (e e' : TExp Γ A) : Set where
  constructor obs
  field
    observe : ∀(C : PCtx Γ A) → C < e > ≃ C < e' >

syntax ObservEq Γ A e e' = Γ ⊢ e ≅ e' :: A

---- Logical equivalence
LogicalEq : CRel
LogicalEq nat e e' = e ≃ e'
LogicalEq (A ⇒ B) e e' = (e₁ e₁' : TCExp A) →
                         LogicalEq A e₁ e₁' → LogicalEq B (e $ e₁) (e' $ e₁')

syntax LogicalEq A e e' = e ~ e' :: A

-- Need a notion of pairs of closing substitutions that respect a relation on closed terms
-- Relations on closed terms

SubstRel : (R : CRel) (Γ : Ctx) → TSubst Γ [] → TSubst Γ [] → Set
SubstRel R Γ γ γ' = ∀{A} (x : A ∈ Γ) → (R A (γ x) (γ' x))

emptySubstRel : ∀(R : CRel) {γ γ' : TSubst [] []} -> SubstRel R [] γ γ'
emptySubstRel R ()

extendSubstRel : ∀(R : CRel) {Γ A} {e e' : TCExp A} {γ γ' : TSubst Γ []} →
                   SubstRel R Γ γ γ' → (R A e e') →
                   SubstRel R (A :: Γ) (extendγ γ e) (extendγ γ' e')
extendSubstRel R η eq Z = eq
extendSubstRel R {_} {_} {e} {e'} {γ} {γ'} η eq (S n) with η n
... | xeq = ID.coe2 (R _)
            (SubstTheory.extend-nofail-s γ e n) (SubstTheory.extend-nofail-s γ' e' n) xeq

-- Specialize that stuff for logical equivalence
LogicalEqΓ = SubstRel LogicalEq
emptyLogicalEqΓ = emptySubstRel LogicalEq
extendLogicalEQΓ = extendSubstRel LogicalEq

---- Open logical equivalence
OLogicalEq : TRel
OLogicalEq Γ A e e' = ∀{γ γ' : TSubst Γ []} → LogicalEqΓ Γ γ γ' →
                      (ssubst γ e) ~ (ssubst γ' e') :: A

syntax OLogicalEq Γ A e e' = Γ ⊢ e ~ e' :: A

---- Definitional (beta) equivalence
-- Definitional equivalence is the strongest congruence closed under
-- the beta axioms. Dunno what the best way to define this is,
-- so I'm just going to define it with constructors for refl/sym/trans
-- and congruence as well as the axioms.
data _==_ : ∀{Γ} {A} → TExp Γ A → TExp Γ A → Set where
  def-refl  : ∀{Γ} {A} {e : TExp Γ A} →
              e == e
  def-sym   : ∀{Γ} {A} {e e' : TExp Γ A} →
              e == e' → e' == e
  def-trans : ∀{Γ} {A} {e e' e'' : TExp Γ A} →
              e == e' → e' == e'' → e == e''

  def-cong  : ∀{Γ} {A} {e e' : TExp Γ A} →
              e == e' →
              {Γ' : Ctx} {A' : TTp} → (C : TCtx Γ A Γ' A') →
              C < e > == C < e' >

  def-beta  : ∀{Γ} {A B} {e : TExp (A :: Γ) B} {e' : TExp Γ A} →
              ((Λ e) $ e') == ssubst (singγ e') e
  def-rec-z : ∀{Γ} {A} {e0 : TExp Γ A} {es : TExp (A :: Γ) A} →
              rec zero e0 es == e0
  def-rec-s : ∀{Γ} {A} {e : TExp Γ nat} {e0 : TExp Γ A} {es : TExp (A :: Γ) A} →
              rec (suc e) e0 es == ssubst (singγ (rec e e0 es)) es

DefEq : TRel
DefEq Γ A = _==_ {Γ} {A}

---- Denotational equivalence
CDenotationalEq : CRel
CDenotationalEq A e e' = cmeaning e ≡ cmeaning e'

max_stars_repo_name: msullivan/godels-t

max_issues_repo_name: msullivan/godels-t

max_forks_repo_name: msullivan/godels-t


text:
module Structure.Setoid.Names where

open import Data.Tuple
open import Functional
open import Function.Equals
import      Lvl
open import Logic
open import Logic.Propositional
open import Logic.Predicate
open import Structure.Setoid
open import Syntax.Function
open import Type

private variable ℓ : Lvl.Level
private variable A B : Type{ℓ}

-- TODO: Probably incorrect
-- Choice : let _ = A , B in ⦃ equiv-B : Equiv(B) ⦄ → (A → B → Stmt{ℓ}) → Stmt
-- Choice {A = A} {B = B} (_▫_) = (∀{x} → ∃(y ↦ x ▫ y)) → ∃{Obj = A → B}(f ↦ (∀{x} → (x ▫ f(x))) ∧ (∀{x y} → (x ▫ y) → (f(x) ≡ y)))

-- Choice-[∘]-inverseᵣ : let _ = A in ⦃ equiv-B : Equiv(B) ⦄ → (A → B → Stmt{ℓ}) → Stmt
-- Choice-[∘]-inverseᵣ {A = A} {B = B} (f) = ∃{Obj = B → A}(f⁻¹ ↦ f ∘ f⁻¹ ⊜ id)

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
{-

Basic properties of James construction

This file contains:

  - The type James X has h-monoid structure, namely being a monoid in "homotopy category".

  - The equivalence "James X₊ ≃ List X" for type X,
    where X₊ denotes the type formed by freely adjoining a base point to X.

-}
{-# OPTIONS --safe #-}
module Cubical.HITs.James.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Pointed

open import Cubical.Data.Maybe
open import Cubical.Data.List hiding (_++_)

open import Cubical.HITs.James.Base

private
  variable
    ℓ : Level

-- The h-monoid structure on James X

module _
  (X∙@(X , x₀) : Pointed ℓ) where

  ++lUnit : (xs : James X∙) → xs ≡ [] ++ xs
  ++lUnit _ = refl

  ++rUnit : (xs : James X∙) → xs ≡ xs ++ []
  ++rUnit [] = refl
  ++rUnit (x ∷ xs) t = x ∷ ++rUnit xs t
  ++rUnit (unit xs i) t = unit (++rUnit xs t) i

  ++Assoc :  (xs ys zs : James X∙) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
  ++Assoc [] _ _ = refl
  ++Assoc (x ∷ xs) ys zs t = x ∷ ++Assoc xs ys zs t
  ++Assoc (unit xs i) ys zs t = unit (++Assoc xs ys zs t) i

-- Freely adjoining a point

module _
  (X : Type ℓ) where

  private
    X₊ = Maybe∙ X

  J₊→List : James X₊ → List X
  J₊→List [] = []
  J₊→List (just x  ∷ xs) = x ∷ J₊→List xs
  J₊→List (nothing ∷ xs) = J₊→List xs
  J₊→List (unit xs i) = J₊→List xs

  List→J₊ : List X → James X₊
  List→J₊ [] = []
  List→J₊ (x ∷ xs) = just x ∷ List→J₊ xs

  List→J₊→List : (xs : List X) → J₊→List (List→J₊ xs) ≡ xs
  List→J₊→List [] = refl
  List→J₊→List (x ∷ xs) i = x ∷ List→J₊→List xs i

  J₊→List→J₊ : (xs : James X₊) → List→J₊ (J₊→List xs) ≡ xs
  J₊→List→J₊ [] = refl
  J₊→List→J₊ (just x  ∷ xs) i = just x ∷ J₊→List→J₊ xs i
  J₊→List→J₊ (nothing ∷ xs) = J₊→List→J₊ xs ∙ unit xs
  J₊→List→J₊ (unit xs i) j =
    hcomp (λ k → λ
      { (i = i0) → J₊→List→J₊ xs j
      ; (i = i1) → compPath-filler (J₊→List→J₊ xs) (unit xs) k j
      ; (j = i0) → List→J₊ (J₊→List xs)
      ; (j = i1) → unit xs (i ∧ k) })
    (J₊→List→J₊ xs j)

  J₊≃List : James X₊ ≃ List X
  J₊≃List = isoToEquiv (iso J₊→List List→J₊ List→J₊→List J₊→List→J₊)

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical


text:
{- constructions on ℕ, everything I could think of that seemed interesting -}
-- "interesting"=?
-- maybe some of these should be discarded. e.g. ⟦⟧ is just an instance of ⟦_⟧, namely ⟦ ⊤ ⟧
-- maybe add a record version of ≤
-- categorise
-- what about ≡?
module Oscar.Data1 where

-- Nat
data ⟦⟧ : Set where
  ∅ : ⟦⟧
  ! : ⟦⟧ → ⟦⟧

-- List
data ⟦_⟧ {a} (A : Set a) : Set a where
  ∅ : ⟦ A ⟧
  _∷_ : A → ⟦ A ⟧ → ⟦ A ⟧

-- Fin
data ⟦⟧[_] : ⟦⟧ → Set where
  ∅ : ∀ {n} → ⟦⟧[ ! n ]
  ! : ∀ {n} → ⟦⟧[ n ] → ⟦⟧[ ! n ]

-- same, with payload
data ⟦_⟧[_] {a} (A : ⟦⟧ → Set a) : ⟦⟧ → Set a where
  ∅ : ∀ {n} → ⟦ A ⟧[ ! n ]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ n ] → ⟦ A ⟧[ ! n ]

-- m ≤ n, counting down from n-1 to m
data ⟦⟧[_≤↓_] (m : ⟦⟧) : ⟦⟧ → Set where
  ∅ : ⟦⟧[ m ≤↓ m ]
  ! : ∀ {n} → ⟦⟧[ m ≤↓ n ] → ⟦⟧[ m ≤↓ ! n ]

-- same, with payload
data ⟦_⟧[_≤↓_] {a} (A : ⟦⟧ → Set a) (m : ⟦⟧) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[ m ≤↓ m ]
  _∷_ : ∀ {n} → A n → ⟦ A ⟧[ m ≤↓ n ] → ⟦ A ⟧[ m ≤↓ ! n ]

-- m ≤ n, counting up from m to n-1
data ⟦⟧[_↑≤_] (m : ⟦⟧) : ⟦⟧ → Set where
  ∅ : ⟦⟧[ m ↑≤ m ]
  ! : ∀ {n} → ⟦⟧[ ! m ↑≤ n ] → ⟦⟧[ m ↑≤ n ]

-- same, with payload
data ⟦_⟧[_↑≤_] {a} (A : ⟦⟧ → Set a) (m : ⟦⟧) : ⟦⟧ → Set a where
  ∅ : ⟦ A ⟧[ m ↑≤ m ]
  _∷_ : ∀ {n} → A m → ⟦ A ⟧[ ! m ↑≤ n ] → ⟦ A ⟧[ m ↑≤ n ]

-- Inj
data ⟦⟧[_↓≤↓_] : ⟦⟧ → ⟦⟧ → Set where
  ∅ : ∀ {n} → ⟦⟧[ ∅ ↓≤↓ n ]
  ! : ∀ {m n} → ⟦⟧[ m ↓≤↓ n ] → ⟦⟧[ ! m ↓≤↓ ! n ]

-- same, with payload
data ⟦_⟧[_↓≤↓_] {a} (A : ⟦⟧ → ⟦⟧ → Set a) : ⟦⟧ → ⟦⟧ → Set a where
  ∅ : ∀ {n} → ⟦ A ⟧[ ∅ ↓≤↓ n ]
  ! : ∀ {m n} → A m n → ⟦ A ⟧[ m ↓≤↓ n ] → ⟦ A ⟧[ ! m ↓≤↓ ! n ]


text:
{-

          Types Summer School 2007

                 Bertinoro
             Aug 19 - 31, 2007

                   Agda

                Ulf Norell

-}

module CurryHoward where

-- Propositions as types!

data True : Set where
  tt : True

data False : Set where

data _∧_ (P Q : Set) : Set where
  _,_ : P -> Q -> P ∧ Q

data _∨_ (P Q : Set) : Set where
  inl : P -> P ∨ Q
  inr : Q -> P ∨ Q

data ∃ (A : Set)(P : A -> Set) : Set where
  ex : (x : A) -> P x -> ∃ A P

¬_ : Set -> Set
¬ A = A -> False

∏ : (A : Set)(P : A -> Set) -> Set
∏ A P = (x : A) -> P x

-- Some simple examples

const : {A B : Set} -> A -> (B -> A)
const = \x y -> x

swap : {P Q : Set} -> P ∧ Q -> Q ∧ P
swap (p , q) = (q , p)

notNotEM : (P : Set) -> ¬ ¬ (P ∨ ¬ P)
notNotEM P = \f -> f (inr (\p -> f (inl p)))

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Cubical.HITs.Delooping.Two.Base where

open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude

-- Explicit construction of the delooping of the two-element group
data Bℤ₂ : Type₀ where
  base : Bℤ₂
  loop : base ≡ base
  loop² : Square loop refl refl loop
  trunc : isGroupoid Bℤ₂

private
  variable
    ℓ : Level
    A : Type ℓ

module Elim where
  rec : (x : A)
      → (p : x ≡ x)
      → (sq : Square p refl refl p)
      → isGroupoid A
      → Bℤ₂ → A
  rec x p sq Agpd = go
    where
    go : _ → _
    go base = x
    go (loop i) = p i
    go (loop² i j) = sq i j
    go (trunc x y p q r s i j k)
      = Agpd
          (go x) (go y)
          (cong go p) (cong go q)
          (cong (cong go) r) (cong (cong go) s)
          i j k

  elim : (P : Bℤ₂ → Type ℓ)
       → (x : P base)
       → (p : PathP (λ i → P (loop i)) x x)
       → (sq : SquareP (λ i j → P (loop² i j)) p (λ i → x) (λ i → x) p)
       → isOfHLevelDep 3 P
       → (z : Bℤ₂) → P z
  elim P x p sq Pgpd = go
    where
    go : (z : Bℤ₂) → P z
    go base = x
    go (loop i) = p i
    go (loop² i j) = sq i j
    go (trunc x y p q r s i j k)
      = Pgpd (go x) (go y)
             (cong go p) (cong go q)
             (cong (cong go) r) (cong (cong go) s)
             (trunc x y p q r s) i j k

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- The syntax of terms with the Nehemiah plugin.
------------------------------------------------------------------------

module Nehemiah.Syntax.Term where

open import Nehemiah.Syntax.Type

open import Data.Integer

import Parametric.Syntax.Term Base as Term

data Const : Term.Structure where
  intlit-const : (n : ℤ) → Const int
  add-const : Const (int ⇒ int ⇒ int)
  minus-const : Const (int ⇒ int)

  empty-const : Const bag
  insert-const : Const (int ⇒ bag ⇒ bag)
  union-const : Const (bag ⇒ bag ⇒ bag)
  negate-const : Const (bag ⇒ bag)

  flatmap-const : Const ((int ⇒ bag) ⇒ bag ⇒ bag)
  sum-const : Const (bag ⇒ int)

open Term.Structure Const public

-- Shorthands of constants

pattern intlit n = const (intlit-const n)
pattern add s t = app (app (const add-const) s) t
pattern minus t = app (const minus-const) t
pattern empty = const empty-const
pattern insert s t = app (app (const insert-const) s) t
pattern union s t = app (app (const union-const) s) t
pattern negate t = app (const negate-const) t
pattern flatmap s t = app (app (const flatmap-const) s) t
pattern sum t = app (const sum-const) t


text:
-- Product of functors

module Control.Functor.Product where

open import Function using (id) renaming (_∘′_ to _∘_)

open import Data.Product using (_×_; _,_; proj₁; proj₂; <_,_>)
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

open import Control.Functor

_×̂_ : Functor → Functor → Functor
FF ×̂ GG = functor (λ X → F X × G X) record
  { ops  = record { map    = map    }
  ; laws = record { map-id = map-id
                  ; map-∘  = λ {A}{B}{C}{f}{g} → map-∘ f g
                  }
  }
  where
    open Functor FF using () renaming (F to F; map to mapF; map-id to mapF-id; map-∘ to mapF-∘)
    open Functor GG using () renaming (F to G; map to mapG; map-id to mapG-id; map-∘ to mapG-∘)

    map : ∀ {A B : Set} (f : A → B) (p : F A × G A) → F B × G B
    map f = < mapF f ∘ proj₁ , mapG f ∘ proj₂ >

    map-id : ∀ {A : Set} → map {A = A} id ≡ id
    map-id = begin
      map id                                 ≡⟨⟩
      < mapF id ∘ proj₁ , mapG id ∘ proj₂ >  ≡⟨ cong (λ z → < z ∘ proj₁ , _ >) mapF-id ⟩
      < proj₁ , mapG id ∘ proj₂ >            ≡⟨ cong (λ z → < _ , z ∘ proj₂ >) mapG-id ⟩
      < proj₁ , proj₂ >                      ≡⟨⟩
      id                                     ∎

    map-∘ : ∀ {A B C : Set} (f : A → B) (g : B → C) →  map (g ∘ f) ≡ map g ∘ map f
    map-∘ f g = begin
      map (g ∘ f) ≡⟨⟩
      < mapF (g ∘ f) ∘ proj₁ , mapG (g ∘ f) ∘ proj₂ >       ≡⟨ cong (λ z → < z ∘ proj₁ , _ >) mapF-∘ ⟩
      < mapF g ∘ mapF f ∘ proj₁ , mapG (g ∘ f) ∘ proj₂ >    ≡⟨ cong (λ z → < mapF g ∘ _ , z ∘ proj₂ >) mapG-∘ ⟩
      < mapF g ∘ mapF f ∘ proj₁ , mapG g ∘ mapG f ∘ proj₂ > ≡⟨⟩
      map g ∘ map f
      ∎

max_stars_repo_name: andreasabel/cubical

max_issues_repo_name: andreasabel/cubical

max_forks_repo_name: andreasabel/cubical


text:
-- Agda program using the Iowa Agda library

open import bool

module PROOF-appendIsAssoc
  (Choice : Set)
  (choose : Choice → 𝔹)
  (lchoice : Choice → Choice)
  (rchoice : Choice → Choice)
  where

open import eq
open import bool
open import nat
open import list
open import maybe

---------------------------------------------------------------------------
-- Translated Curry operations:

data List (a : Set) : Set where
   Empty : List a
   Cons : a → List a → List a

append : {a : Set} → List a → List a → List a
append Empty x = x
append (Cons y z) u = Cons y (append z u)

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

appendIsAssoc : {a : Set} → (x : List a) → (y : List a) → (z : List a)
              → (append (append x y) z) ≡ (append x (append y z))
appendIsAssoc Empty y z = refl
appendIsAssoc (Cons x xs) y z rewrite appendIsAssoc xs y z = refl

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

max_stars_repo_name: phlummox/curry-tools

max_issues_repo_name: phlummox/curry-tools

max_forks_repo_name: phlummox/curry-tools


text:
{-# OPTIONS --without-K --safe #-}
module Categories.Category.Instance.Setoids where

-- Category of Setoids, aka (Setoid, _⟶_, Setoid ≈)
-- Note the (explicit) levels in each

open import Level
open import Relation.Binary
open import Function.Equality as SΠ renaming (id to ⟶-id)

open import Categories.Category

Setoids : ∀ c ℓ → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
Setoids c ℓ = record
  { Obj       = Setoid c ℓ
  ; _⇒_       = _⟶_
  ; _≈_       = λ {A B} → Setoid._≈_ (A ⇨ B)
  ; id        = ⟶-id
  ; _∘_       = _∘_
  ; assoc     = λ {_ _ _ D} {f g h} → cong (h ∘ g ∘ f)
  ; sym-assoc = λ {_ _ _ D} {f g h} → cong (h ∘ g ∘ f)
  ; identityˡ = λ {_ _} {f} → cong f
  ; identityʳ = λ {_ _} {f} → cong f
  ; identity² = λ eq → eq
  ; equiv     = λ {A B} → Setoid.isEquivalence (A ⇨ B)
  ; ∘-resp-≈  = λ f≡h g≡i x≡y → f≡h (g≡i x≡y)
  }

max_stars_repo_name: Trebor-Huang/agda-categories

max_issues_repo_name: Code-distancing/agda-categories

max_forks_repo_name: Code-distancing/agda-categories


text:
------------------------------------------------------------------------
-- Simplified XML documents
------------------------------------------------------------------------

-- This example is based on (but not identical to) one in Wadler's "A
-- prettier printer".

{-# OPTIONS --guardedness #-}

module Examples.XML where

open import Codata.Musical.Notation
open import Data.Bool
open import Data.Char
open import Data.List as List using (List; []; _∷_)
open import Data.List.NonEmpty as List⁺ using (_∷_)
open import Data.Product
import Data.String as String
open import Data.Unit
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

open import Examples.Identifier
open import Grammar.Infinite as Grammar
  using (Grammar) hiding (module Grammar)
open import Pretty using (Pretty-printer)
open import Renderer
open import Utilities

-- Text.

is-text-char : Char → Bool
is-text-char t =
  ('A' ≤?C t) ∧ (t ≤?C 'Z')
    ∨
  ('a' ≤?C t) ∧ (t ≤?C 'z')
    ∨
  ('0' ≤?C t) ∧ (t ≤?C '9')
    ∨
  List.any (_==_ t) (String.toList ":./ \n")

Text : Set
Text = List (∃ λ (t : Char) → T (is-text-char t))

text-g : Grammar Text
text-g = sat _ ⋆
  where open Grammar

text-printer : Pretty-printer text-g
text-printer = map⋆ (sat is-text-char)
  where open Pretty

mutual

  data XML : Set where
    elt : Identifier → List Att → List XML → XML
    txt : Text → XML

  data Att : Set where
    att : Identifier → Text → Att

module _ where

  open Grammar

  mutual

    -- The following grammar is ambiguous: a sequence of txt elements can
    -- be parsed in several different ways.

    xml : Grammar XML
    xml = (start-of-element >>= λ { (t , atts) →
           elt t atts <$> (
               [] <$ string′ "/"
             ∣     string′ ">"
                ⊛> xmls
               <⊛  symbol′ "</"
               <⊛  symbol (List.map proj₁ (List⁺.toList t)))}) <⊛
          symbol′ ">"
        ∣ txt <$> text-g <⊛ whitespace ⋆

    start-of-element : Grammar (Identifier × List Att)
    start-of-element = _,_ <$ symbol′ "<" ⊛ identifier ⊛ attrs

    xmls : Grammar (List XML)
    xmls = whitespace ⋆ ⊛> ♯ xml ⋆

    attrs : Grammar (List Att)
    attrs = [] <$ whitespace ⋆
          ∣ List⁺.toList <$> (whitespace + ⊛> attr +)

    attr : Grammar Att
    attr = att <$> identifier
               <⊛  whitespace ⋆
               <⊛  symbol′ "="
               <⊛  string′ "\""
                ⊛  text-g
               <⊛  symbol′ "\""

open Pretty

mutual

  xml-printer : Pretty-printer xml
  xml-printer (elt t atts []) =
    left ((start-of-element-printer (t , atts) ◇
           <$> left (<$ text))
          <⊛ symbol)
  xml-printer (elt t atts xs) =
    left ((start-of-element-printer (t , atts) ◇
           <$> right (text ⊛> xmls-printer xs <⊛ symbol <⊛ symbol))
          <⊛ symbol)
  xml-printer (txt t) =
    -- Wadler pretty-prints text items in a different way. (The
    -- grammar that I use does not allow me to modify the amount of
    -- whitespace in the same way as Wadler.)
    right (<$> text-printer t <⊛ nil-⋆)

  start-of-element-printer : Pretty-printer start-of-element
  start-of-element-printer (t , atts) =
    <$ symbol ⊛ identifier-printer t ⊛ attrs-printer atts

  attrs-printer : Pretty-printer attrs
  attrs-printer []       = left (<$ nil-⋆)
  attrs-printer (a ∷ as) =
    right (<$> group (nest 2 line
                        tt-⊛>
                      final-line 4
                        (nest 2 (map+-fill 2 attr-printer (a ∷ as))) 0))

  attr-printer : Pretty-printer attr
  attr-printer (att n v) =
    <$> identifier-printer n
    <⊛  nil-⋆
    <⊛  symbol
    <⊛  text
     ⊛  text-printer v
    <⊛  symbol

  -- The following definition uses "fill+ 3 (to-docs x xs)" (along
  -- with the auxiliary definition of to-docs) rather than
  -- "map+-fill 3 xml-printer (x ∷ xs)" because the latter piece of
  -- code makes the termination checker complain.

  xmls-printer : Pretty-printer xmls
  xmls-printer []       = nil-⋆ ⊛> nil-⋆
  xmls-printer (x ∷ xs) =
    group (nest 2 line⋆
             tt-⊛>
           final-line-+⋆ 5 (nest 2 (fill+ 3 (to-docs x xs))) 0)
    where
    to-docs : ∀ x xs → Docs xml (x ∷ xs)
    to-docs x []        = [ xml-printer x ]
    to-docs x (x′ ∷ xs) = xml-printer x ∷ to-docs x′ xs

example : XML
example = elt (str⁺ "p")
              (att (str⁺ "color") (str "red") ∷
               att (str⁺ "font") (str "Times") ∷
               att (str⁺ "size") (str "10") ∷ [])
              (txt (str "Here is some") ∷
               elt (str⁺ "em")
                   []
                   (txt (str "emphasized") ∷ []) ∷
               txt (str "text.") ∷
               txt (str "Here is a") ∷
               elt (str⁺ "a")
                   (att (str⁺ "href") (str "http://www.eg.com/") ∷ [])
                   (txt (str "link") ∷ []) ∷
               txt (str "elsewhere.") ∷ [])

test₁ : render 30 (xml-printer example) ≡
        "
\n  Here is some\n   emphasized  text.\n  Here is a\n   link \n  elsewhere.\n
"
test₁ = refl

test₂ : render 60 (xml-printer example) ≡
        "
\n  Here is some  emphasized  text. Here is a\n   link  elsewhere.\n
"
test₂ = refl

max_stars_repo_name: nad/pretty

max_issues_repo_name: nad/pretty

max_forks_repo_name: nad/pretty


text:
open import Prelude
open import dynamics-core

module ground-decidable where
  ground-decidable : (τ : htyp) → (τ ground) + ((τ ground) → ⊥)
  ground-decidable num = Inl GNum
  ground-decidable (⦇-⦈ ==> ⦇-⦈) = Inl GArrHole
  ground-decidable (⦇-⦈ ⊕ ⦇-⦈) = Inl GSumHole
  ground-decidable ⦇-⦈ = Inr (λ ())
  ground-decidable (num ==> τ₁) = Inr (λ ())
  ground-decidable (⦇-⦈ ==> num) = Inr (λ ())
  ground-decidable (⦇-⦈ ==> τ₁ ==> τ₂) = Inr (λ ())
  ground-decidable (⦇-⦈ ==> τ₁ ⊕ τ₂) = Inr (λ ())
  ground-decidable ((τ ==> τ₂) ==> τ₁) = Inr (λ ())
  ground-decidable ((τ ⊕ τ₂) ==> τ₁) = Inr (λ ())
  ground-decidable (num ⊕ τ₁) = Inr (λ ())
  ground-decidable (⦇-⦈ ⊕ num) = Inr (λ ())
  ground-decidable (⦇-⦈ ⊕ τ₁ ==> τ₂) = Inr (λ ())
  ground-decidable (⦇-⦈ ⊕ τ₁ ⊕ τ₂) = Inr (λ ())
  ground-decidable ((τ ==> τ₂) ⊕ τ₁) = Inr (λ ())
  ground-decidable ((τ ⊕ τ₂) ⊕ τ₁) = Inr (λ ())
  ground-decidable (⦇-⦈ ==> τ₁ ⊠ τ₂) = Inr (λ ())
  ground-decidable ((τ ⊠ τ₂) ==> τ₁) = Inr (λ ())
  ground-decidable (⦇-⦈ ⊕ τ₁ ⊠ τ₂) = Inr (λ ())
  ground-decidable ((τ ⊠ τ₂) ⊕ τ₁) = Inr (λ ())
  ground-decidable (num ⊠ num) = Inr (λ ())
  ground-decidable (num ⊠ ⦇-⦈) = Inr (λ ())
  ground-decidable (num ⊠ τ₁ ==> τ₂) = Inr (λ ())
  ground-decidable (num ⊠ τ₁ ⊕ τ₂) = Inr (λ ())
  ground-decidable (num ⊠ τ₁ ⊠ τ₂) = Inr (λ ())
  ground-decidable (⦇-⦈ ⊠ num) = Inr (λ ())
  ground-decidable (⦇-⦈ ⊠ ⦇-⦈) = Inl GProdHole
  ground-decidable (⦇-⦈ ⊠ τ₁ ==> τ₂) = Inr (λ ())
  ground-decidable (⦇-⦈ ⊠ τ₁ ⊕ τ₂) = Inr (λ ())
  ground-decidable (⦇-⦈ ⊠ τ₁ ⊠ τ₂) = Inr (λ ())
  ground-decidable ((τ ==> τ₁) ⊠ num) = Inr (λ ())
  ground-decidable ((τ ==> τ₁) ⊠ ⦇-⦈) = Inr (λ ())
  ground-decidable ((τ ==> τ₁) ⊠ τ₂ ==> τ₃) = Inr (λ ())
  ground-decidable ((τ ==> τ₁) ⊠ τ₂ ⊕ τ₃) = Inr (λ ())
  ground-decidable ((τ ==> τ₁) ⊠ τ₂ ⊠ τ₃) = Inr (λ ())
  ground-decidable ((τ ⊕ τ₁) ⊠ num) = Inr (λ ())
  ground-decidable ((τ ⊕ τ₁) ⊠ ⦇-⦈) = Inr (λ ())
  ground-decidable ((τ ⊕ τ₁) ⊠ τ₂ ==> τ₃) = Inr (λ ())
  ground-decidable ((τ ⊕ τ₁) ⊠ τ₂ ⊕ τ₃) = Inr (λ ())
  ground-decidable ((τ ⊕ τ₁) ⊠ τ₂ ⊠ τ₃) = Inr (λ ())
  ground-decidable ((τ ⊠ τ₁) ⊠ num) = Inr (λ ())
  ground-decidable ((τ ⊠ τ₁) ⊠ ⦇-⦈) = Inr (λ ())
  ground-decidable ((τ ⊠ τ₁) ⊠ τ₂ ==> τ₃) = Inr (λ ())
  ground-decidable ((τ ⊠ τ₁) ⊠ τ₂ ⊕ τ₃) = Inr (λ ())
  ground-decidable ((τ ⊠ τ₁) ⊠ τ₂ ⊠ τ₃) = Inr (λ ())

max_stars_repo_name: hazelgrove/hazelnut-agda

max_issues_repo_name: hazelgrove/hazelnut-agda

max_forks_repo_name: hazelgrove/hazelnut-agda


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

module Function.Injective.Properties where

open import Level
open import Path
open import Data.Sigma
open import Function.Injective.Base
open import Relation.Nullary.Decidable
open import Relation.Nullary.Discrete
open import Function

Discrete-pull-inj : A ↣ B → Discrete B → Discrete A
Discrete-pull-inj (f , inj) _≟_ x y =
  case (f x ≟ f y) of
    λ  { (no ¬p) → no (¬p ∘ cong f)
       ; (yes p) → yes (inj x y p) }

inject-contrapositive : (f : A → B) → Injective f → ∀ x y → x ≢ y → f x ≢ f y
inject-contrapositive f inj x y x≢y fx≡fy = x≢y (inj x y fx≡fy)

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
------------------------------------------------------------------------
-- Binomial theorem
------------------------------------------------------------------------

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

-- agda-stdlib
open import Algebra
import Algebra.Operations.Semiring as SemiringOperations
import Algebra.Properties.CommutativeMonoid as CommutativeMonoidProperties
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

module Math.BinomialTheorem.Generic {e l} (SR : Semiring e l) where

-- agda-stdlib
open import Data.Nat as ℕ using (zero; suc; _∸_)
open import Function

-- agda-combinatorics
open import Math.Combinatorics.Function
open import Math.Combinatorics.Function.Properties

-- agda-misc
open import Math.NumberTheory.Summation.Generic
open import Math.NumberTheory.Summation.Generic.Properties

open Semiring SR
open SemiringOperations SR
open CommutativeMonoidProperties +-commutativeMonoid
open SetoidReasoning setoid
open MonoidSummation +-monoid
open SemiringSummationProperties SR
{-
theorem : ∀ x y n →
  (x + y) ^ n ≈ Σ[ k ≤ n ] (C n k × (x ^ k * y ^ (n ∸ k)))
theorem x y 0       = begin
  1#
    ≈⟨ sym $ *-identityʳ 1# ⟩
  1# * 1#
    ≈⟨ sym $ +-identityʳ (1# * 1#) ⟩
  1# * 1# + 0#
    ≡⟨⟩
  C 0 0 × ((x ^ 0) * y ^ (0 ∸ 0))
    ≈⟨ sym $ Σ≤[0,f]≈f[0] (λ k → C 0 k × (x ^ k * y ^ (0 ∸ k))) ⟩
  Σ≤ 0 (λ k → C 0 k × (x ^ k * y ^ (0 ∸ k)))
    ∎
theorem x y (suc n) = begin
  (x + y) * (x + y) ^ n ≈⟨ *-congˡ $ theorem x y n ⟩
  (x + y) * Σ[ k ≤ n ] (C n k × (x ^ k * y ^ (n ∸ k))) ≈⟨ {!   !} ⟩
  Σ≤ (suc n) (λ k → C (suc n) k × (x ^ k * y ^ (suc n ∸ k))) ∎
-}


text:
module _ where

open import Imports.Issue958

-- Extra parameterised module to make sure checkpoints line up with
-- the checkpoints in the imported module.
module Dummy (X : Set) where

module M (_ fun : IsFunctor) where

  open IsFunctor

  -- Here we're in the "same" checkpoint as when the display form was
  -- created. It's not the same though, so the display form should be
  -- generalized and lifted to the appropriate context.
  test : map fun
  test = fun

  -- EXPECTED: IsFunctor !=< map fun


text:
open import Relation.Binary.Core

module InsertSort.Impl1 {A : Set}
                  (_≤_ : A → A → Set)
                  (tot≤ : Total _≤_)  where

open import Bound.Lower A
open import Bound.Lower.Order _≤_
open import Data.List
open import Data.Sum

insert : A → List A → List A
insert x [] = [ x ]
insert x (y ∷ ys)
    with tot≤ x y
... | inj₁ _ = x ∷ y ∷ ys
... | inj₂ _ = y ∷ insert x ys

insertSort : List A → List A
insertSort = foldr insert []

max_stars_repo_name: bgbianchi/sorting

max_issues_repo_name: bgbianchi/sorting

max_forks_repo_name: bgbianchi/sorting


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}
open import Axiom.Extensionality.Propositional
open import Data.Empty
open import Level
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality hiding (Extensionality)

module Util.FunctionOverride
          {ℓ₁   : Level}
          (A    : Set ℓ₁)
          (_≟A_ : (a₁ a₂ : A) → Dec (a₁ ≡ a₂))
          {ℓ₂ : Level}{B : Set ℓ₂}
  where

  override : (A → B) → A → B → (A → B)
  override f p v x
     with p ≟A x
  ...| yes refl = v
  ...| no  neq  = f x

  syntax override m p v = ⟦ m , p ← v ⟧

  postulate -- valid assumption
    -- TODO-2: Eliminate postulate using https://github.com/agda/cubical
    funext : Extensionality ℓ₁ ℓ₂

  override-target-≡ : ∀ {a : A}{b : B}{f}
                    → override f a b a ≡ b
  override-target-≡ {a}
     with a ≟A a
  ...| yes refl = refl
  ...| no  neq  = ⊥-elim (neq refl)

  override-target-≢ : ∀ {a a' : A}{b : B}{f}
                    → a' ≢ a
                    → f a' ≡ (override f a b) a'
  override-target-≢ {a} {a'} neq
     with a ≟A a'
  ...| yes refl = ⊥-elim (neq refl)
  ...| no  _    = refl

  overrideSameVal-correct : ∀ {f : A → B}
              → (p a : A)
              → override f p (f p) a ≡ f a
  overrideSameVal-correct p a
     with p ≟A a
  ...| no neq   = refl
  ...| yes refl = refl

  overrideSameVal-correct-ext : ∀ {f : A → B}{p : A} → override f p (f p) ≡ f
  overrideSameVal-correct-ext {p = p} = funext (overrideSameVal-correct p)

max_stars_repo_name: cwjnkins/bft-consensus-agda

max_issues_repo_name: cwjnkins/bft-consensus-agda

max_forks_repo_name: cwjnkins/bft-consensus-agda


text:
module MonoidTactic where

open import Prelude
open import Container.Traversable
open import Structure.Monoid.Laws
open import Tactic.Monoid
open import Tactic.Reflection

MonoidAnd : Monoid Bool
mempty {{MonoidAnd}} = true
_<>_   {{MonoidAnd}} = _&&_

MonoidLawsAnd : MonoidLaws Bool {{MonoidAnd}}
idLeft  {{MonoidLawsAnd}} x = refl
idRight {{MonoidLawsAnd}} false = refl
idRight {{MonoidLawsAnd}} true  = refl
<>assoc {{MonoidLawsAnd}} true  y z = refl
<>assoc {{MonoidLawsAnd}} false y z = refl

test₁ : (a b : Bool) → (a && (b && a && true)) ≡ ((a && b) && a)
test₁ a b = auto-monoid {{Laws = MonoidLawsAnd}}

test₂ : ∀ {a} {A : Set a} {{Mon : Monoid A}} {{Laws : MonoidLaws A}} →
          (x y : A) → x <> (y <> x <> mempty) ≡ (x <> y) <> x
test₂ x y = auto-monoid

test₃ : ∀ {a} {A : Set a} (xs ys zs : List A) → xs ++ ys ++ zs ≡ (xs ++ []) ++ (ys ++ []) ++ zs
test₃ xs ys zs = runT monoidTactic

max_stars_repo_name: lclem/agda-prelude

max_issues_repo_name: lclem/agda-prelude

max_forks_repo_name: lclem/agda-prelude


text:
-- Andreas, 2021-06-01, also test issue #5425

module ModuleArgs where

open import Common.Nat
open import Common.IO
open import Common.Unit

module X (y : Nat) where

  addTo : Nat → Nat
  addTo x = y + x

  data D : Set where
    c : D

open X 23

-- This used to crash `agda --js --js-optimize`
-- which could not cope with constructors from applied modules
-- (missing canonicalization of constructor names).
c' : D
c' = c

-- should return 35
main : IO Unit
main = printNat (addTo 12)


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import LibraBFT.Base.Types
import      LibraBFT.Impl.Consensus.ConsensusTypes.Vote as Vote
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import Optics.All
open import Util.Prelude

module LibraBFT.Impl.Consensus.ConsensusTypes.VoteMsg where

verify : VoteMsg → ValidatorVerifier → Either ErrLog Unit
verify self validator = do
  lcheck (self ^∙ vmVote ∙ vEpoch == self ^∙ vmSyncInfo ∙ siEpoch)
         -- (here $ "VoteMsg has different epoch" ∷ lsSI (self ^∙ vmSyncInfo) ∷ [])
         ("VoteMsg has different epoch" ∷ [])
  Vote.verify (self ^∙ vmVote) validator


text:
-- Jesper, 2018-10-16: When solving constraints, unsolved metas should
-- be turned into interaction holes. Metas that refer to an existing
-- interaction hole should be printed as _ instead.

postulate
  _==_ : {A : Set} (a b : A) → Set
  P : Set → Set
  f : {A : Set} {a : A} {b : A} → P (a == b)

x : P {!!}
x = f

y : P {!!}
y = f {a = {!!}} {b = {!!}}


text:
module With-flicker where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero  + n = n
suc m + n = suc (m + n)

fib : ℕ → ℕ
fib zero          = zero
fib (suc zero)    = suc zero
fib (suc (suc n)) = fib n + fib (suc n)

thirteen = suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))))))

postulate
  P : ℕ → Set
  n : ℕ

-- The interactive highlighting used to flicker a lot when the
-- following definition was checked.

Foo : P (fib (thirteen + n)) → Set₁
Foo p with zero
Foo p | _ = Set


text:
-- Andreas, 2016-10-11, AIM XXIV
-- COMPILED pragma accidentially also accepted for abstract definitions
-- Ulf, 2017-02-22: We now allow COMPILE pragmas on functions, and abstract
-- functions should not be an exception. The original problem, however, was
-- that we expected an unused argument-version of the function to be available.
-- This is not the case for COMPILE'd functions. This problem has now been
-- fixed.

open import Common.String

data Unit : Set where
  unit : Unit

{-# COMPILE GHC Unit = data () (()) #-}

postulate
  IO : Set → Set
  doNothing : IO Unit
  doSomething : String → IO Unit

{-# COMPILE GHC IO = type IO #-}
{-# BUILTIN IO IO #-}
{-# COMPILE GHC doNothing = return () #-}

{-# FOREIGN GHC import qualified Data.Text.IO #-}

abstract
  putStrLn : Unit → String → IO Unit
  putStrLn _ = doSomething

{-# COMPILE GHC putStrLn = \ _ -> Data.Text.IO.putStrLn #-}

main = putStrLn unit "Hello, world!"

-- WAS: compiler produced ill-formed Haskell-code
-- NOW: Error on COMPILE GHC pragma

max_stars_repo_name: Blaisorblade/Agda

max_issues_repo_name: Blaisorblade/Agda

max_forks_repo_name: Blaisorblade/Agda


text:
field
  Foo = Set

-- Error IS:  Parse error.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module #10 where

{-
  Exercise 1.10. Show that the Ackermann function ack : N → N → N is definable using only
  recN satisfying the following equations:
-}

open import Data.Nat
open import Relation.Binary.PropositionalEquality

recₙ : ∀{c}{C : Set c} → C → (ℕ → C → C) → ℕ → C
recₙ c₀ cₛ zero = c₀
recₙ c₀ cₛ (suc n) = cₛ n (recₙ c₀ cₛ n)

ack : ℕ → ℕ → ℕ
ack zero n = suc n
ack (suc m) zero = ack m 1
ack (suc m) (suc n) = ack m (ack (suc m) n)

ack-rec : ℕ → ℕ → ℕ
ack-rec = recₙ suc (λ m cont → recₙ (cont 1) (λ _ n → cont n))

{- The process of proving this might destroy my computer, so no.
ack-β : (n m : ℕ) → ack m n ≡ ack-rec m n
ack-β m n = {!!}
-}

max_stars_repo_name: CodaFi/HoTT-Exercises

max_issues_repo_name: CodaFi/HoTT-Exercises

max_forks_repo_name: CodaFi/HoTT-Exercises


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

open import Categories.Category.Monoidal using (SymmetricMonoidalCategory)

-- The monoidal structure of a monoidal catgeory D
-- lifted pointwise to monoidal functors F : C → D.

module Categories.Functor.Monoidal.PointwiseTensor {o o′ ℓ ℓ′ e e′}
  {C : SymmetricMonoidalCategory o ℓ e}
  {D : SymmetricMonoidalCategory o′ ℓ′ e′} where

open import Level using (_⊔_)
open import Data.Product using (_,_)

private
  module C = SymmetricMonoidalCategory C
  module D = SymmetricMonoidalCategory D

open import Categories.Category using (module Commutation)
open import Categories.Category.Product using (_⁂_)
import Categories.Category.Construction.Core as Core
import Categories.Functor as Func
open import Categories.Category.Monoidal.Properties using (module Kelly's)
open import Categories.Category.Monoidal.Braided.Properties D.braided
  as BraidedProps using (braiding-coherence)
open import Categories.Category.Monoidal.Reasoning D.monoidal
open import Categories.Category.Monoidal.Utilities D.monoidal
open import Categories.Functor.Construction.Constant using (const)
open import Categories.Functor.Monoidal.Tensor using
  (module LaxSymmetric; module StrongSymmetric)
import Categories.Functor.Monoidal.Symmetric as SF
open import Categories.Morphism.Reasoning D.U
open import Categories.NaturalTransformation
  using (NaturalTransformation; ntHelper)
open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper)
import Categories.NaturalTransformation.Monoidal.Symmetric as SMNT
import Categories.NaturalTransformation.NaturalIsomorphism as NI
import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric as SMNI

open D hiding (U) renaming (unitorˡ to λᵢ; unitorʳ to ρᵢ; associator to αᵢ)
open Commutation D.U
open Core.Shorthands D.U
open Kelly's D.monoidal
open Shorthands              -- for λ⇒, ρ⇒, α⇒, ...
open BraidedProps.Shorthands -- for σ⇒, ...

module Underlying where
  open Func hiding (id)
  open NI

  private
    infix 4 _⇛_
    _⇛_ = NaturalTransformation

  infixr 10 _⊗̇₀_ _⊗̇₁_

  -- The pointwise tensor product of two functors.
  --
  -- NOTE: the definition of _⊗̇₀_ is a manual expansion of the functor
  -- composition
  --
  --   F ⊗̇₀ G = ⊗ ∘ (F × G) ∘ Δ
  --
  -- where Δ : D → D × D is the diagonal functor.

  _⊗̇₀_ : (F G : Functor C.U D.U) → Functor C.U D.U
  F ⊗̇₀ G = record
    { F₀           = λ X → F.₀ X ⊗₀ G.₀ X
    ; F₁           = λ f → F.₁ f ⊗₁ G.₁ f
    ; identity     = (F.identity ⟩⊗⟨ G.identity) ○ ⊗.identity
    ; homomorphism = (F.homomorphism ⟩⊗⟨ G.homomorphism) ○ ⊗.homomorphism
    ; F-resp-≈     = λ eq → F.F-resp-≈ eq ⟩⊗⟨ G.F-resp-≈ eq
    }
    where
      module F = Functor F
      module G = Functor G

  _⊗̇₁_ : {F₁ F₂ G₁ G₂ : Functor C.U D.U} →
         F₁ ⇛ F₂ → G₁ ⇛ G₂ → F₁ ⊗̇₀ G₁ ⇛ F₂ ⊗̇₀ G₂
  _⊗̇₁_ {F₁} {F₂} {G₁} {G₂} β γ = ntHelper (record
    { η       = λ X → β.η X ⊗₁ γ.η X
    ; commute = λ {X Y} f → begin
        β.η Y ⊗₁ γ.η Y ∘ F₁.₁ f ⊗₁ G₁.₁ f     ≈˘⟨ ⊗.homomorphism ⟩
        (β.η Y ∘ F₁.₁ f) ⊗₁ (γ.η Y ∘ G₁.₁ f)  ≈⟨ β.commute f ⟩⊗⟨ γ.commute f ⟩
        (F₂.₁ f ∘ β.η X) ⊗₁ (G₂.₁ f ∘ γ.η X)  ≈⟨ ⊗.homomorphism ⟩
        F₂.₁ f ⊗₁ G₂.₁ f ∘ β.η X ⊗₁ γ.η X     ∎
    })
    where
      module F₁ = Functor F₁
      module F₂ = Functor F₂
      module G₁ = Functor G₁
      module G₂ = Functor G₂
      module β = NaturalTransformation β
      module γ = NaturalTransformation γ

  -- The constant functor to the unit in D.

  unitF : Functor C.U D.U
  unitF = const D.unit

  module unitF = Functor unitF

  unitF-⊗-homo : D.⊗ ∘F (unitF ⁂ unitF) ≃ unitF ∘F C.⊗
  unitF-⊗-homo = niHelper (record
    { η            = λ _ → λ⇒
    ; η⁻¹          = λ _ → λ⇐
    ; commute      = λ _ → begin
      λ⇒ ∘ id ⊗₁ id  ≈⟨ refl⟩∘⟨ ⊗.identity ⟩
      λ⇒ ∘ id        ≈⟨ id-comm ⟩
      id ∘ λ⇒        ∎
    ; iso          = λ _ → λᵢ.iso
    })

  module unitF-⊗-homo = NaturalIsomorphism unitF-⊗-homo

  -- The pointwise tensor product and the unit functor induce a
  -- symmetric monoidal structure on symmetric monoidal functors.

  ⊗̇-unitorˡ : {F : Functor C.U D.U} → unitF ⊗̇₀ F ≃ F
  ⊗̇-unitorˡ {F} = niHelper (record
    { η       = λ _ → λ⇒
    ; η⁻¹     = λ _ → λ⇐
    ; commute = λ _ → unitorˡ-commute-from
    ; iso     = λ _ → λᵢ.iso
    })

  ⊗̇-unitorʳ : {F : Functor C.U D.U} → F ⊗̇₀ unitF ≃ F
  ⊗̇-unitorʳ {F} = niHelper (record
    { η       = λ _ → ρ⇒
    ; η⁻¹     = λ _ → ρ⇐
    ; commute = λ _ → unitorʳ-commute-from
    ; iso     = λ _ → ρᵢ.iso
    })

  ⊗̇-associator : {F G H : Functor C.U D.U} → (F ⊗̇₀ G) ⊗̇₀ H ≃ F ⊗̇₀ (G ⊗̇₀ H)
  ⊗̇-associator {F} {G} {H} = niHelper (record
    { η       = λ _ → α⇒
    ; η⁻¹     = λ _ → α⇐
    ; commute = λ _ → assoc-commute-from
    ; iso     = λ _ → αᵢ.iso
    })

  ⊗̇-braiding : {F G : Functor C.U D.U} → F ⊗̇₀ G ≃ G ⊗̇₀ F
  ⊗̇-braiding {F} {G} = niHelper (record
    { η       = λ X → braiding.⇒.η (F.₀ X , G.₀ X)
    ; η⁻¹     = λ X → braiding.⇐.η (F.₀ X , G.₀ X)
    ; commute = λ f → braiding.⇒.commute (F.₁ f , G.₁ f)
    ; iso     = λ X → braiding.iso (F.₀ X , G.₀ X)
    })
    where
      module F = Functor F
      module G = Functor G

-- Shorthands for the interchange map that makes ⊗ a strong symmetric
-- monoidal functor.

open StrongSymmetric D.symmetric using ()renaming
  ( ⊗-SymmetricMonoidalFunctor to ⊗ˢ
  ; ⊗-homo-iso                 to i-iso′
  ; ⊗-homo-selfInverse         to i-selfInverse
  )
private
  module ⊗ˢ = SF.Strong.SymmetricMonoidalFunctor ⊗ˢ
  module interchange = ⊗ˢ.⊗-homo
  i  = interchange.FX≅GX
  i⇒ = λ {W X Y Z} → interchange.⇒.η ((W , X) , (Y , Z))
  i⇐ = λ {W X Y Z} → interchange.⇐.η ((W , X) , (Y , Z))

module Lax where
  open SF.Lax
  open SMNT.Lax using (SymmetricMonoidalNaturalTransformation)
  open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; _≃_)

  private
    infix 4 _⇛_
    _⇛_ = SymmetricMonoidalNaturalTransformation

  infixr 10 _⊗̇₀_ _⊗̇₁_

  -- The pointwise tensor product of lax symmetric monoidal functors.
  --
  -- NOTE: the definition of _⊗̇₀_ is a manual expansion of the
  -- (lax monoidal) functor composition
  --
  --   F ⊗̇₀ G = ⊗ ∘ (F × G) ∘ Δ
  --
  -- with Δ : D → D × D the diagonal functor.  We could define _⊗̇₀_ in
  -- this way but that would clutter the definition of ε and ⊗-homo
  -- with extra identities that then need to be dealt with elsewhere
  -- (e.g. in the definition of _⊗̇₁_ below.  In principle, _⊗̇₁_ should
  -- be similarly definable as a composition of (monoidal) natural
  -- transformations, but the Agda type checker seems to choke on
  -- definitions involving compositions of natural transformations.

  _⊗̇₀_ : (F G : SymmetricMonoidalFunctor C D) → SymmetricMonoidalFunctor C D
  F ⊗̇₀ G = record
    { F                 = F.F Underlying.⊗̇₀ G.F
    ; isBraidedMonoidal = record
      { isMonoidal      = record
        { ε             = F.ε ⊗₁ G.ε ∘ λ⇐
        ; ⊗-homo        = ntHelper (record
          { η           = λ _ → Fh ⊗₁ Gh ∘ i⇒
          ; commute     = λ{ (f , g) → commute f g }
          })
        ; associativity = associativity
        ; unitaryˡ      = unitaryˡ
        ; unitaryʳ      = unitaryʳ
        }
      ; braiding-compat = braiding-compat
      }
    }
    where
      module F = SymmetricMonoidalFunctor F
      module G = SymmetricMonoidalFunctor G
      Fh = λ {X Y} → F.⊗-homo.η (X , Y)
      Gh = λ {X Y} → G.⊗-homo.η (X , Y)
      Cλ⇒ = λ {X} → C.braided.unitorˡ.from {X}
      Cρ⇒ = λ {X} → C.braided.unitorʳ.from {X}
      Cα⇒ = λ {X Y Z} → C.braided.associator.from {X} {Y} {Z}
      Cσ⇒ = λ {X Y} → C.braided.braiding.⇒.η (X , Y)

      commute : ∀ {W X Y Z} (f : W C.⇒ X) (g : Y C.⇒ Z) →
                  (Fh ⊗₁ Gh ∘ i⇒) ∘ (F.₁ f ⊗₁ G.₁ f) ⊗₁ (F.₁ g ⊗₁ G.₁ g)
                ≈ F.₁ (f C.⊗₁ g) ⊗₁ G.₁ (f C.⊗₁ g) ∘ (Fh ⊗₁ Gh) ∘ i⇒
      commute f g = begin
          (Fh ⊗₁ Gh ∘ i⇒) ∘ (F.₁ f ⊗₁ G.₁ f) ⊗₁ (F.₁ g ⊗₁ G.₁ g)
        ≈⟨ pullʳ (interchange.⇒.commute ((F.₁ f , G.₁ f) , (F.₁ g , G.₁ g))) ⟩
          Fh ⊗₁ Gh ∘ (F.₁ f ⊗₁ F.₁ g) ⊗₁ (G.₁ f ⊗₁ G.₁ g) ∘ i⇒
        ≈˘⟨ pushˡ ⊗.homomorphism ⟩
          (Fh ∘ F.₁ f ⊗₁ F.₁ g) ⊗₁ (Gh ∘ G.₁ f ⊗₁ G.₁ g) ∘ i⇒
        ≈⟨ F.⊗-homo.commute (f , g) ⟩⊗⟨ G.⊗-homo.commute (f , g) ⟩∘⟨refl ⟩
          (F.₁ (f C.⊗₁ g) ∘ Fh) ⊗₁ (G.₁ (f C.⊗₁ g) ∘ Gh) ∘ i⇒
        ≈⟨ pushˡ ⊗.homomorphism ⟩
          F.₁ (f C.⊗₁ g) ⊗₁ G.₁ (f C.⊗₁ g) ∘ (Fh ⊗₁ Gh) ∘ i⇒
        ∎

      associativity : ∀ {X Y Z} →
                      [ ((F.₀ X ⊗₀ G.₀ X) ⊗₀ (F.₀ Y ⊗₀ G.₀ Y)) ⊗₀ (F.₀ Z ⊗₀ G.₀ Z)
                      ⇒ F.₀ (X C.⊗₀ (Y C.⊗₀ Z)) ⊗₀ G.₀ (X C.⊗₀ (Y C.⊗₀ Z)) ]⟨
                        F.₁ Cα⇒ ⊗₁ G.₁ Cα⇒ ∘
                        (Fh ⊗₁ Gh ∘ i⇒) ∘ (Fh ⊗₁ Gh ∘ i⇒) ⊗₁ id
                      ≈ (Fh ⊗₁ Gh ∘ i⇒) ∘ id ⊗₁ (Fh ⊗₁ Gh ∘ i⇒) ∘ α⇒
                      ⟩
      associativity = begin
          F.₁ Cα⇒ ⊗₁ G.₁ Cα⇒ ∘ (Fh ⊗₁ Gh ∘ i⇒) ∘ (Fh ⊗₁ Gh ∘ i⇒) ⊗₁ id
        ≈⟨ refl⟩∘⟨ pullʳ (refl⟩∘⟨ split₁ˡ) ⟩
          F.₁ Cα⇒ ⊗₁ G.₁ Cα⇒ ∘ Fh ⊗₁ Gh ∘ i⇒ ∘ (Fh ⊗₁ Gh) ⊗₁ id ∘ i⇒ ⊗₁ id
        ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ ⊗.identity ⟩∘⟨refl ⟩
          F.₁ Cα⇒ ⊗₁ G.₁ Cα⇒ ∘ Fh ⊗₁ Gh ∘
          i⇒ ∘ (Fh ⊗₁ Gh) ⊗₁ (id ⊗₁ id) ∘ i⇒ ⊗₁ id
        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (interchange.⇒.commute ((Fh , Gh) , (id , id))) ⟩
          F.₁ Cα⇒ ⊗₁ G.₁ Cα⇒ ∘ Fh ⊗₁ Gh ∘ (Fh ⊗₁ id) ⊗₁ (Gh ⊗₁ id) ∘ i⇒ ∘ i⇒ ⊗₁ id
        ≈˘⟨ refl⟩∘⟨ pushˡ ⊗.homomorphism ⟩
          F.₁ Cα⇒ ⊗₁ G.₁ Cα⇒ ∘ (Fh ∘ Fh ⊗₁ id) ⊗₁ (Gh ∘ Gh ⊗₁ id) ∘ i⇒ ∘ i⇒ ⊗₁ id
        ≈⟨ extendʳ (parallel (F.associativity ○ sym-assoc) (G.associativity ○ sym-assoc)) ⟩
          (Fh ∘ id ⊗₁ Fh) ⊗₁ (Gh ∘ id ⊗₁ Gh) ∘ α⇒ ⊗₁ α⇒ ∘ i⇒ ∘ i⇒ ⊗₁ id
        ≈⟨ ⊗.homomorphism ⟩∘⟨ ⊗ˢ.associativity ⟩
          ((Fh ⊗₁ Gh) ∘ (id ⊗₁ Fh) ⊗₁ (id ⊗₁ Gh)) ∘ i⇒ ∘ id ⊗₁ i⇒ ∘ α⇒
        ≈˘⟨ pushʳ (extendʳ (interchange.⇒.commute ((id , id) , (Fh , Gh)))) ⟩
          (Fh ⊗₁ Gh) ∘ i⇒ ∘ (id ⊗₁ id) ⊗₁ (Fh ⊗₁ Gh) ∘ id ⊗₁ i⇒ ∘ α⇒
        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩
          (Fh ⊗₁ Gh) ∘ i⇒ ∘ id ⊗₁ (Fh ⊗₁ Gh) ∘ id ⊗₁ i⇒ ∘ α⇒
        ≈˘⟨ pullʳ (refl⟩∘⟨ pushˡ split₂ˡ) ⟩
          (Fh ⊗₁ Gh ∘ i⇒) ∘ id ⊗₁ (Fh ⊗₁ Gh ∘ i⇒) ∘ α⇒
        ∎

      unitaryˡ : ∀ {X} → [ unit ⊗₀ (F.₀ X ⊗₀ G.₀ X) ⇒ F.₀ X ⊗₀ G.₀ X ]⟨
                   F.₁ Cλ⇒ ⊗₁ G.₁ Cλ⇒ ∘ (Fh ⊗₁ Gh ∘ i⇒) ∘ (F.ε ⊗₁ G.ε ∘ λ⇐) ⊗₁ id
                 ≈ λ⇒
                 ⟩
      unitaryˡ = begin
          F.₁ Cλ⇒ ⊗₁ G.₁ Cλ⇒ ∘ (Fh ⊗₁ Gh ∘ i⇒) ∘ (F.ε ⊗₁ G.ε ∘ λ⇐) ⊗₁ id
        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₁ˡ ⟩
          F.₁ Cλ⇒ ⊗₁ G.₁ Cλ⇒ ∘ (Fh ⊗₁ Gh ∘ i⇒) ∘ (F.ε ⊗₁ G.ε) ⊗₁ id ∘ λ⇐ ⊗₁ id
        ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩⊗⟨ ⊗.identity ⟩∘⟨refl ⟩
          F.₁ Cλ⇒ ⊗₁ G.₁ Cλ⇒ ∘ (Fh ⊗₁ Gh ∘ i⇒) ∘ (F.ε ⊗₁ G.ε) ⊗₁ (id ⊗₁ id) ∘ λ⇐ ⊗₁ id
        ≈⟨ refl⟩∘⟨ pullʳ (extendʳ (interchange.⇒.commute ((F.ε , G.ε) , (id , id)))) ⟩
          F.₁ Cλ⇒ ⊗₁ G.₁ Cλ⇒ ∘ Fh ⊗₁ Gh ∘ (F.ε ⊗₁ id) ⊗₁ (G.ε ⊗₁ id) ∘ i⇒ ∘ λ⇐ ⊗₁ id
        ≈˘⟨ refl⟩∘⟨ pushˡ ⊗.homomorphism ⟩
          F.₁ Cλ⇒ ⊗₁ G.₁ Cλ⇒ ∘ (Fh ∘ F.ε ⊗₁ id) ⊗₁ (Gh ∘ G.ε ⊗₁ id) ∘ i⇒ ∘ λ⇐ ⊗₁ id
        ≈˘⟨ pushˡ ⊗.homomorphism ⟩
          (F.₁ Cλ⇒ ∘ Fh ∘ F.ε ⊗₁ id) ⊗₁ (G.₁ Cλ⇒ ∘ Gh ∘ G.ε ⊗₁ id) ∘ i⇒ ∘ λ⇐ ⊗₁ id
        ≈⟨ F.unitaryˡ ⟩⊗⟨ G.unitaryˡ ⟩∘⟨refl ⟩
          λ⇒ ⊗₁ λ⇒ ∘ i⇒ ∘ λ⇐ ⊗₁ id
        ≈⟨ ⊗ˢ.unitaryˡ ⟩
          λ⇒
        ∎

      unitaryʳ : ∀ {X} → [ (F.₀ X ⊗₀ G.₀ X) ⊗₀ unit ⇒ F.₀ X ⊗₀ G.₀ X ]⟨
                   F.₁ Cρ⇒ ⊗₁ G.₁ Cρ⇒ ∘ (Fh ⊗₁ Gh ∘ i⇒) ∘ id ⊗₁ (F.ε ⊗₁ G.ε ∘ λ⇐)
                 ≈ ρ⇒
                 ⟩
      unitaryʳ = begin
          F.₁ Cρ⇒ ⊗₁ G.₁ Cρ⇒ ∘ (Fh ⊗₁ Gh ∘ i⇒) ∘ id ⊗₁ (F.ε ⊗₁ G.ε ∘ λ⇐)
        ≈⟨ refl⟩∘⟨ refl⟩∘⟨ split₂ˡ ⟩
          F.₁ Cρ⇒ ⊗₁ G.₁ Cρ⇒ ∘ (Fh ⊗₁ Gh ∘ i⇒) ∘ id ⊗₁ (F.ε ⊗₁ G.ε) ∘ id ⊗₁ λ⇐
        ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ ⊗.identity ⟩⊗⟨refl ⟩∘⟨refl ⟩
          F.₁ Cρ⇒ ⊗₁ G.₁ Cρ⇒ ∘ (Fh ⊗₁ Gh ∘ i⇒) ∘ (id ⊗₁ id) ⊗₁ (F.ε ⊗₁ G.ε) ∘ id ⊗₁ λ⇐
        ≈⟨ refl⟩∘⟨ pullʳ (extendʳ (interchange.⇒.commute ((id , id) , (F.ε , G.ε)))) ⟩
          F.₁ Cρ⇒ ⊗₁ G.₁ Cρ⇒ ∘ Fh ⊗₁ Gh ∘ (id ⊗₁ F.ε) ⊗₁ (id ⊗₁ G.ε) ∘ i⇒ ∘ id ⊗₁ λ⇐
        ≈˘⟨ refl⟩∘⟨ pushˡ ⊗.homomorphism ⟩
          F.₁ Cρ⇒ ⊗₁ G.₁ Cρ⇒ ∘ (Fh ∘ id ⊗₁ F.ε) ⊗₁ (Gh ∘ id ⊗₁ G.ε) ∘ i⇒ ∘ id ⊗₁ λ⇐
        ≈˘⟨ pushˡ ⊗.homomorphism ⟩
          (F.₁ Cρ⇒ ∘ Fh ∘ id ⊗₁ F.ε) ⊗₁ (G.₁ Cρ⇒ ∘ Gh ∘ id ⊗₁ G.ε) ∘ i⇒ ∘ id ⊗₁ λ⇐
        ≈⟨ F.unitaryʳ ⟩⊗⟨ G.unitaryʳ ⟩∘⟨refl ⟩
          ρ⇒ ⊗₁ ρ⇒ ∘ i⇒ ∘ id ⊗₁ λ⇐
        ≈⟨ ⊗ˢ.unitaryʳ ⟩
          ρ⇒
        ∎

      braiding-compat = λ {X Y} → begin
          F.₁ Cσ⇒ ⊗₁ G.₁ Cσ⇒ ∘ Fh {X} {Y} ⊗₁ Gh {X} {Y} ∘ i⇒
        ≈⟨ extendʳ (parallel F.braiding-compat G.braiding-compat) ⟩
          (Fh ⊗₁ Gh) ∘ σ⇒ ⊗₁ σ⇒ ∘ i⇒
        ≈⟨ pushʳ ⊗ˢ.braiding-compat ⟩
          (Fh ⊗₁ Gh ∘ i⇒) ∘ σ⇒
        ∎

  _⊗̇₁_ : {F₁ F₂ G₁ G₂ : SymmetricMonoidalFunctor C D} →
         F₁ ⇛ F₂ → G₁ ⇛ G₂ → F₁ ⊗̇₀ G₁ ⇛ F₂ ⊗̇₀ G₂
  _⊗̇₁_ {F₁} {F₂} {G₁} {G₂} β γ = record
    { U               = β.U Underlying.⊗̇₁ γ.U
    ; isMonoidal      = record
      { ε-compat      = ε-compat
      ; ⊗-homo-compat = ⊗-homo-compat
      }
    }
    where
      module F₁ = SymmetricMonoidalFunctor F₁
      module F₂ = SymmetricMonoidalFunctor F₂
      module G₁ = SymmetricMonoidalFunctor G₁
      module G₂ = SymmetricMonoidalFunctor G₂
      module β = SymmetricMonoidalNaturalTransformation β
      module γ = SymmetricMonoidalNaturalTransformation γ

      ε-compat = begin
          β.η C.unit ⊗₁ γ.η C.unit ∘ F₁.ε ⊗₁ G₁.ε ∘ λ⇐
        ≈˘⟨ pushˡ ⊗.homomorphism ⟩
          (β.η C.unit ∘ F₁.ε) ⊗₁ (γ.η C.unit ∘ G₁.ε) ∘ λ⇐
        ≈⟨ β.ε-compat ⟩⊗⟨ γ.ε-compat ⟩∘⟨refl ⟩
          F₂.ε ⊗₁ G₂.ε ∘ λ⇐
        ∎

      ⊗-homo-compat = λ {X Y} → begin
          β.η (X C.⊗₀ Y) ⊗₁ γ.η (X C.⊗₀ Y) ∘
          F₁.⊗-homo.η (X , Y) ⊗₁ G₁.⊗-homo.η (X , Y) ∘ i⇒
        ≈˘⟨ pushˡ ⊗.homomorphism ⟩
          (β.η (X C.⊗₀ Y) ∘ F₁.⊗-homo.η (X , Y)) ⊗₁
          (γ.η (X C.⊗₀ Y) ∘ G₁.⊗-homo.η (X , Y)) ∘ i⇒
        ≈⟨ β.⊗-homo-compat ⟩⊗⟨ γ.⊗-homo-compat ⟩∘⟨refl ⟩
          (F₂.⊗-homo.η (X , Y) ∘ β.η X ⊗₁ β.η Y) ⊗₁
          (G₂.⊗-homo.η (X , Y) ∘ γ.η X ⊗₁ γ.η Y) ∘ i⇒
        ≈⟨ pushˡ ⊗.homomorphism ⟩
          F₂.⊗-homo.η (X , Y) ⊗₁ G₂.⊗-homo.η (X , Y) ∘
          (β.η X ⊗₁ β.η Y) ⊗₁ (γ.η X ⊗₁ γ.η Y) ∘ i⇒
        ≈˘⟨ pullʳ (interchange.⇒.commute ((β.η X , γ.η X) , (β.η Y , γ.η Y))) ⟩
          (F₂.⊗-homo.η (X , Y) ⊗₁ G₂.⊗-homo.η (X , Y) ∘ i⇒) ∘
          (β.η X ⊗₁ γ.η X) ⊗₁ (β.η Y ⊗₁ γ.η Y)
        ∎

  -- The constant functor to the unit in D is (lax) monoidal.

  unitF : SymmetricMonoidalFunctor C D
  unitF = record
    { F                 = Underlying.unitF
    ; isBraidedMonoidal = record
      { isMonoidal      = record
        { ε             = id
        ; ⊗-homo        = Underlying.unitF-⊗-homo.F⇒G
        ; associativity = begin
          id ∘ λ⇒ ∘ λ⇒ ⊗₁ id  ≈⟨ identityˡ ⟩
          λ⇒ ∘ λ⇒ ⊗₁ id       ≈˘⟨ refl⟩∘⟨ coherence₁ ⟩
          λ⇒ ∘ λ⇒ ∘ α⇒        ≈˘⟨ extendʳ unitorˡ-commute-from ⟩
          λ⇒ ∘ id ⊗₁ λ⇒ ∘ α⇒  ∎
        ; unitaryˡ      = begin
          id ∘ λ⇒ ∘ id ⊗₁ id  ≈⟨ identityˡ ⟩
          λ⇒ ∘ id ⊗₁ id       ≈⟨ refl⟩∘⟨ ⊗.identity ⟩
          λ⇒ ∘ id             ≈⟨ identityʳ ⟩
          λ⇒                  ∎
        ; unitaryʳ      = begin
          id ∘ λ⇒ ∘ id ⊗₁ id  ≈⟨ identityˡ ⟩
          λ⇒ ∘ id ⊗₁ id       ≈⟨ refl⟩∘⟨ ⊗.identity ⟩
          λ⇒ ∘ id             ≈⟨ identityʳ ⟩
          λ⇒                  ≈⟨ coherence₃ ⟩
          ρ⇒                  ∎

        }
      ; braiding-compat = begin
        id ∘ λ⇒               ≈⟨ identityˡ ⟩
        λ⇒                    ≈⟨ coherence₃ ⟩
        ρ⇒                    ≈˘⟨ braiding-coherence ⟩
        λ⇒ ∘ braiding.⇒.η _   ∎
      }
    }
  module unitF = SymmetricMonoidalFunctor unitF

  -- The pointwise tensor product and the unit functor induce a
  -- symmetric monoidal structure on symmetric monoidal functors.

  ⊗̇-unitorˡ : {F : SymmetricMonoidalFunctor C D} → unitF ⊗̇₀ F ≃ F
  ⊗̇-unitorˡ {F} = record
    { U               = Underlying.⊗̇-unitorˡ
    ; F⇒G-isMonoidal  = record
      { ε-compat      = ε-compat
      ; ⊗-homo-compat = ⊗-homo-compat
      }
    }
    where
      open SymmetricMonoidalFunctor F

      ε-compat = begin
        λ⇒ ∘ id ⊗₁ ε ∘ λ⇐   ≈⟨ extendʳ unitorˡ-commute-from ⟩
        ε ∘ λ⇒ ∘ λ⇐         ≈⟨ elimʳ λᵢ.isoʳ ⟩
        ε                   ∎

      ⊗-homo-compat = λ {X Y} → let h = ⊗-homo.η (X , Y) in begin
          λ⇒ ∘ λ⇒ ⊗₁ h ∘ i⇒
        ≈⟨ pullˡ (refl⟩∘⟨ serialize₂₁) ⟩
          (λ⇒ ∘ id ⊗₁ h ∘ λ⇒ ⊗₁ id) ∘ i⇒
        ≈⟨ extendʳ unitorˡ-commute-from ⟩∘⟨ i-selfInverse ⟩
          (h ∘ λ⇒ ∘ λ⇒ ⊗₁ id) ∘ i⇐
        ≈˘⟨ pushʳ (switch-fromtoʳ i (switch-tofromʳ (λᵢ ⊗ᵢ idᵢ)
                                                    (assoc ○ ⊗ˢ.unitaryˡ))) ⟩
          h ∘ λ⇒ ⊗₁ λ⇒
        ∎

  ⊗̇-unitorʳ : {F : SymmetricMonoidalFunctor C D} → F ⊗̇₀ unitF ≃ F
  ⊗̇-unitorʳ {F} = record
    { U               = Underlying.⊗̇-unitorʳ
    ; F⇒G-isMonoidal  = record
      { ε-compat      = ε-compat
      ; ⊗-homo-compat = ⊗-homo-compat
      }
    }
    where
      open SymmetricMonoidalFunctor F

      ε-compat = begin
        ρ⇒ ∘ ε ⊗₁ id ∘ λ⇐   ≈⟨ extendʳ unitorʳ-commute-from ⟩
        ε ∘ ρ⇒ ∘ λ⇐         ≈˘⟨ refl⟩∘⟨ coherence₃ ⟩∘⟨refl ⟩
        ε ∘ λ⇒ ∘ λ⇐         ≈⟨ elimʳ λᵢ.isoʳ ⟩
        ε                   ∎

      ⊗-homo-compat = λ {X Y} → let h = ⊗-homo.η (X , Y) in begin
          ρ⇒ ∘ h ⊗₁ λ⇒ ∘ i⇒
        ≈⟨ pullˡ (refl⟩∘⟨ serialize₁₂) ⟩
          (ρ⇒ ∘ h ⊗₁ id ∘ id ⊗₁ λ⇒) ∘ i⇒
        ≈⟨ extendʳ unitorʳ-commute-from ⟩∘⟨ i-selfInverse ⟩
          (h ∘ ρ⇒ ∘ id ⊗₁ λ⇒) ∘ i⇐
        ≈˘⟨ pushʳ (switch-fromtoʳ i (switch-tofromʳ (idᵢ ⊗ᵢ λᵢ)
                                                    (assoc ○ ⊗ˢ.unitaryʳ))) ⟩
          h ∘ ρ⇒ ⊗₁ ρ⇒
        ∎

  ⊗̇-associator : {F G H : SymmetricMonoidalFunctor C D} →
                 (F ⊗̇₀ G) ⊗̇₀ H ≃ F ⊗̇₀ (G ⊗̇₀ H)
  ⊗̇-associator {F} {G} {H} = record
    { U               = Underlying.⊗̇-associator
    ; F⇒G-isMonoidal  = record
      { ε-compat      = ε-compat
      ; ⊗-homo-compat = ⊗-homo-compat
      }
    }
    where
      module F = SymmetricMonoidalFunctor F
      module G = SymmetricMonoidalFunctor G
      module H = SymmetricMonoidalFunctor H
      Fh = λ {X Y} → F.⊗-homo.η (X , Y)
      Gh = λ {X Y} → G.⊗-homo.η (X , Y)
      Hh = λ {X Y} → H.⊗-homo.η (X , Y)

      ε-compat = begin
          α⇒ ∘ (F.ε ⊗₁ G.ε ∘ λ⇐) ⊗₁ H.ε ∘ λ⇐
        ≈⟨ pullˡ (pushʳ split₁ʳ) ⟩
          ((α⇒ ∘ (F.ε ⊗₁ G.ε) ⊗₁ H.ε) ∘ λ⇐ ⊗₁ id) ∘ λ⇐
        ≈⟨ pushˡ assoc-commute-from ⟩∘⟨refl ⟩
          (F.ε ⊗₁ (G.ε ⊗₁ H.ε) ∘ α⇒ ∘ λ⇐ ⊗₁ id) ∘ λ⇐
        ≈⟨ (refl⟩∘⟨ helper) ⟩∘⟨refl ⟩
          (F.ε ⊗₁ (G.ε ⊗₁ H.ε) ∘ id ⊗₁ λ⇐) ∘ λ⇐
        ≈˘⟨ split₂ʳ ⟩∘⟨refl ⟩
          F.ε ⊗₁ (G.ε ⊗₁ H.ε ∘ λ⇐) ∘ λ⇐
        ∎
        where
          helper = begin
            α⇒ ∘ λ⇐ ⊗₁ id    ≈⟨ refl⟩∘⟨ coherence-inv₃ ⟩⊗⟨refl ⟩
            α⇒ ∘ ρ⇐ ⊗₁ id    ≈˘⟨ conjugate-from (ρᵢ ⊗ᵢ idᵢ) (idᵢ ⊗ᵢ λᵢ)
                                                (identityˡ ○ ⟺ triangle) ⟩
            id ⊗₁ λ⇐ ∘ id    ≈⟨ identityʳ ⟩
            id ⊗₁ λ⇐         ∎

      ⊗-homo-compat = λ {X Y} → begin
          α⇒ ∘ (Fh {X} {Y} ⊗₁ Gh {X} {Y} ∘ i⇒) ⊗₁ Hh {X} {Y} ∘ i⇒
        ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ i-selfInverse) ⟩⊗⟨refl ⟩∘⟨ i-selfInverse ⟩
          α⇒ ∘ (Fh ⊗₁ Gh ∘ i⇐) ⊗₁ Hh ∘ i⇐
        ≈⟨ refl⟩∘⟨ pushˡ split₁ʳ ⟩
          α⇒ ∘ (Fh ⊗₁ Gh) ⊗₁ Hh ∘ i⇐ ⊗₁ id ∘ i⇐
        ≈⟨ extendʳ assoc-commute-from ⟩
          Fh ⊗₁ (Gh  ⊗₁ Hh) ∘ α⇒ ∘ i⇐ ⊗₁ id ∘ i⇐
        ≈˘⟨ refl⟩∘⟨ conjugate-from (i ∘ᵢ i ⊗ᵢ idᵢ) (i ∘ᵢ idᵢ ⊗ᵢ i)
                                   (⊗ˢ.associativity ○ sym-assoc) ⟩
          Fh ⊗₁ (Gh  ⊗₁ Hh) ∘ (id ⊗₁ i⇐ ∘ i⇐) ∘ α⇒ ⊗₁ α⇒
        ≈˘⟨ pushˡ (pushˡ split₂ʳ) ⟩
          (Fh ⊗₁ (Gh ⊗₁ Hh ∘ i⇐) ∘ i⇐) ∘ α⇒ ⊗₁ α⇒
        ≈˘⟨ (refl⟩⊗⟨ (refl⟩∘⟨ i-selfInverse) ⟩∘⟨
                              i-selfInverse) ⟩∘⟨refl ⟩
          (Fh ⊗₁ (Gh ⊗₁ Hh ∘ i⇒) ∘ i⇒) ∘ α⇒ ⊗₁ α⇒
        ∎

  ⊗̇-braiding : {F G : SymmetricMonoidalFunctor C D } → F ⊗̇₀ G ≃ G ⊗̇₀ F
  ⊗̇-braiding {F} {G} = record
    { U               = Underlying.⊗̇-braiding
    ; F⇒G-isMonoidal  = record
      { ε-compat      = ε-compat
      ; ⊗-homo-compat = ⊗-homo-compat
      }
    }
    where
      module F = SymmetricMonoidalFunctor F
      module G = SymmetricMonoidalFunctor G
      Fh = λ {X Y} → F.⊗-homo.η (X , Y)
      Gh = λ {X Y} → G.⊗-homo.η (X , Y)

      ε-compat = begin
        σ⇒ ∘ F.ε ⊗₁ G.ε ∘ λ⇐   ≈⟨  extendʳ (braiding.⇒.commute (F.ε , G.ε)) ⟩
        G.ε ⊗₁ F.ε ∘ σ⇒ ∘ λ⇐   ≈⟨  refl⟩∘⟨ refl⟩∘⟨ coherence-inv₃ ⟩
        G.ε ⊗₁ F.ε ∘ σ⇒ ∘ ρ⇐   ≈˘⟨ refl⟩∘⟨ conjugate-from ρᵢ λᵢ
                                     (identityˡ ○ ⟺ braiding-coherence) ⟩
        G.ε ⊗₁ F.ε ∘ λ⇐ ∘ id   ≈⟨ refl⟩∘⟨ identityʳ ⟩
        G.ε ⊗₁ F.ε ∘ λ⇐        ∎

      ⊗-homo-compat : ∀ {X Y} →
                        σ⇒ ∘ Fh {X} {Y} ⊗₁ Gh {X} {Y} ∘ i⇒
                      ≈ (Gh ⊗₁ Fh ∘ i⇒) ∘ σ⇒ ⊗₁ σ⇒
      ⊗-homo-compat {X} {Y} = begin
        σ⇒ ∘ Fh ⊗₁ Gh ∘ i⇒           ≈⟨ extendʳ (braiding.⇒.commute (Fh , Gh)) ⟩
        Gh ⊗₁ Fh ∘ σ⇒ ∘ i⇒           ≈⟨ pushʳ (conjugate-to i-iso′ i-iso′
                                          (⟺ ⊗ˢ.braiding-compat)) ⟩
        (Gh ⊗₁ Fh ∘ i⇒) ∘ σ⇒ ⊗₁ σ⇒   ∎

  module ⊗̇-unitorˡ {F} = SymmetricMonoidalNaturalIsomorphism (⊗̇-unitorˡ {F})
  module ⊗̇-unitorʳ {F} = SymmetricMonoidalNaturalIsomorphism (⊗̇-unitorʳ {F})
  module ⊗̇-associator {F} {G} {H} =
    SymmetricMonoidalNaturalIsomorphism (⊗̇-associator {F} {G} {H})
  module ⊗̇-braiding {F} {G} =
    SymmetricMonoidalNaturalIsomorphism (⊗̇-braiding {F} {G})

module Strong where
  open SF.Strong
  open SMNT.Strong using (SymmetricMonoidalNaturalTransformation)
  open SMNI.Strong using (SymmetricMonoidalNaturalIsomorphism; _≃_)
  open SymmetricMonoidalFunctor using ()
    renaming (laxSymmetricMonoidalFunctor to laxSMF)

  private
    infix 4 _⇛_
    _⇛_ = SymmetricMonoidalNaturalTransformation

  infixr 10 _⊗̇₀_ _⊗̇₁_

  -- The pointwise tensor product of strong symmetric monoidal functors.

  _⊗̇₀_ : (F G : SymmetricMonoidalFunctor C D) → SymmetricMonoidalFunctor C D
  F ⊗̇₀ G = record
    { F                  = F.F Underlying.⊗̇₀ G.F
    ; isBraidedMonoidal  = record
      { isStrongMonoidal = record
        { ε              = F.ε ⊗ᵢ G.ε ∘ᵢ ⊗ˢ.ε
        ; ⊗-homo         = niHelper (record
          { η            = ⊗-homoᵢ.from
          ; η⁻¹          = ⊗-homoᵢ.to
          ; commute      = ⊗-homo.commute
          ; iso          = ⊗-homoᵢ.iso
          })
        ; associativity  = associativity
        ; unitaryˡ       = unitaryˡ
        ; unitaryʳ       = unitaryʳ
        }
      ; braiding-compat  = braiding-compat
      }
    }
    where
      module F = SymmetricMonoidalFunctor F
      module G = SymmetricMonoidalFunctor G
      ⊗-homoᵢ = λ XY → F.⊗-homo.FX≅GX {XY} ⊗ᵢ G.⊗-homo.FX≅GX {XY} ∘ᵢ i
      module ⊗-homoᵢ XY = _≅_ (⊗-homoᵢ XY)
      open SF.Lax.SymmetricMonoidalFunctor (laxSMF F Lax.⊗̇₀ laxSMF G)

  _⊗̇₁_ : {F₁ F₂ G₁ G₂ : SymmetricMonoidalFunctor C D} →
         F₁ ⇛ F₂ → G₁ ⇛ G₂ → F₁ ⊗̇₀ G₁ ⇛ F₂ ⊗̇₀ G₂
  _⊗̇₁_ β γ = record
    { U               = β.U Underlying.⊗̇₁ γ.U
    ; isMonoidal      = record
      { ε-compat      = ε-compat
      ; ⊗-homo-compat = λ {X Y} → ⊗-homo-compat
      }
    }
    where
      module β = SymmetricMonoidalNaturalTransformation β
      module γ = SymmetricMonoidalNaturalTransformation γ
      open SMNT.Lax.SymmetricMonoidalNaturalTransformation (β.laxSNT Lax.⊗̇₁ γ.laxSNT)

  -- The constant functor to the unit in D is (strong) monoidal.

  unitF : SymmetricMonoidalFunctor C D
  unitF = record
    { F                  = Underlying.unitF
    ; isBraidedMonoidal  = record
      { isStrongMonoidal = record
        { ε              = idᵢ
        ; ⊗-homo         = Underlying.unitF-⊗-homo
        ; associativity  = λ {X Y Z} → Lax.unitF.associativity {X = X} {Y} {Z}
        ; unitaryˡ       = λ {X} → Lax.unitF.unitaryˡ {X = X}
        ; unitaryʳ       = λ {X} → Lax.unitF.unitaryʳ {X = X}
        }
      ; braiding-compat  = λ {X Y} → Lax.unitF.braiding-compat {X = X} {Y}
      }
    }
  module unitF = SymmetricMonoidalFunctor unitF

  -- The pointwise tensor product and the unit functor induce a
  -- symmetric monoidal structure on symmetric monoidal functors.

  ⊗̇-unitorˡ : {F : SymmetricMonoidalFunctor C D} → unitF ⊗̇₀ F ≃ F
  ⊗̇-unitorˡ {F} = record
    { U               = U
    ; F⇒G-isMonoidal  = record
      { ε-compat      = ε-compat
      ; ⊗-homo-compat = λ {X Y} → ⊗-homo-compat {X = X} {Y}
      }
    }
    where open SMNI.Lax.SymmetricMonoidalNaturalIsomorphism (Lax.⊗̇-unitorˡ {F = laxSMF F})

  ⊗̇-unitorʳ : {F : SymmetricMonoidalFunctor C D} → F ⊗̇₀ unitF ≃ F
  ⊗̇-unitorʳ {F} = record
    { U               = U
    ; F⇒G-isMonoidal  = record
      { ε-compat      = ε-compat
      ; ⊗-homo-compat = λ {X Y} → ⊗-homo-compat {X = X} {Y}
      }
    }
    where open SMNI.Lax.SymmetricMonoidalNaturalIsomorphism (Lax.⊗̇-unitorʳ {F = laxSMF F})

  ⊗̇-associator : {F G H : SymmetricMonoidalFunctor C D} →
                 (F ⊗̇₀ G) ⊗̇₀ H ≃ F ⊗̇₀ (G ⊗̇₀ H)
  ⊗̇-associator {F} {G} {H} = record
    { U               = U
    ; F⇒G-isMonoidal  = record
      { ε-compat      = ε-compat
      ; ⊗-homo-compat = λ {X Y} → ⊗-homo-compat {X = X} {Y}
      }
    }
    where open SMNI.Lax.SymmetricMonoidalNaturalIsomorphism (Lax.⊗̇-associator {F = laxSMF F} {laxSMF G} {laxSMF H})

  ⊗̇-braiding : {F G : SymmetricMonoidalFunctor C D } → F ⊗̇₀ G ≃ G ⊗̇₀ F
  ⊗̇-braiding {F} {G} = record
    { U               = U
    ; F⇒G-isMonoidal  = record
      { ε-compat      = ε-compat
      ; ⊗-homo-compat = λ {X Y} → ⊗-homo-compat {X = X} {Y}
      }
    }
    where open SMNI.Lax.SymmetricMonoidalNaturalIsomorphism (Lax.⊗̇-braiding {F = laxSMF F} {laxSMF G})

  module ⊗̇-unitorˡ {F} = SymmetricMonoidalNaturalIsomorphism (⊗̇-unitorˡ {F})
  module ⊗̇-unitorʳ {F} = SymmetricMonoidalNaturalIsomorphism (⊗̇-unitorʳ {F})
  module ⊗̇-associator {F} {G} {H} =
    SymmetricMonoidalNaturalIsomorphism (⊗̇-associator {F} {G} {H})
  module ⊗̇-braiding {F} {G} =
    SymmetricMonoidalNaturalIsomorphism (⊗̇-braiding {F} {G})


text:
------------------------------------------------------------------------------
-- Testing the use of implicit arguments
------------------------------------------------------------------------------

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

-- The dot in the name of the implicit arguments must be removed.

module ImplicitArguments where

postulate
  D   : Set
  a b : D

-- The identity type.
data _≡_ (x : D) : D → Set where
  refl : x ≡ x

postulate a≡b : a ≡ b
{-# ATP axiom a≡b #-}

foo : {n : D} → b ≡ a
foo = prf
  where
  postulate prf : b ≡ a
  {-# ATP prove prf #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia