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

module sets.int.core where

open import sum
open import equality
open import function
import sets.nat as N
open N using (ℕ; suc)
open import sets.int.definition
open import sets.int.utils
open import sets.vec
open import hott.level.closure

infixl 7 _*_
infixl 6 _+_

from-nat : ℕ → ℤ
from-nat n = n [-] 0

zero : ℤ
zero = from-nat 0

one : ℤ
one = from-nat 1

private
  module _ where
    open N

    add : ℕ → ℕ → ℕ → ℕ → ℤ
    add n n' m m' = (n + m) [-] (n' + m')

    add-sound : (n n' d m m' e : ℕ)
              → add n n' m m'
              ≡ add (d + n) (d + n') (e + m) (e + m')
    add-sound n n' d m m' e
      = eq-ℤ (n + m) (n' + m') (d + e)
      · ap₂ _[-]_ (solve 4 (exp λ d e n m → d :+ e :+ (n :+ m))
                           (exp λ d e n m → d :+ n :+ (e :+ m))
                           (d ∷∷ e ∷∷ n ∷∷ m ∷∷ ⟦⟧))
                  (solve 4 (exp λ d e n m → d :+ e :+ (n :+ m))
                           (exp λ d e n m → d :+ n :+ (e :+ m))
                           (d ∷∷ e ∷∷ n' ∷∷ m' ∷∷ ⟦⟧))

    mul : ℕ → ℕ → ℕ → ℕ → ℤ
    mul n n' m m' = (n * m + n' * m') [-] (n' * m + n * m')

    mul-sound : (n n' d m m' e : ℕ)
              → mul n n' m m'
              ≡ mul (d + n) (d + n') (e + m) (e + m')
    mul-sound n n' d m m' e
      = eq-ℤ (n * m + n' * m') (n' * m + n * m')
             (d * e + d * m + n * e + d * e + d * m' + n' * e)
      · ap₂ _[-]_ lem₁ lem₂
      where
        distr₂ : ∀ a b c d
               → (a + b) * (c + d)
               ≡ a * c + a * d + b * c + b * d
        distr₂ a b c d = right-distr a b (c + d)
                       · ap₂ _+_ (left-distr a c d) (left-distr b c d)
                       · sym (+-associativity (a * c + a * d) (b * c) (b * d))

        lem₁ : d * e + d * m + n * e + d * e + d * m' + n' * e + (n * m + n' * m')
             ≡ (d + n) * (e + m) + (d + n') * (e + m')
        lem₁ = sym
             $ ap₂ _+_ (distr₂ d n e m) (distr₂ d n' e m')
             · solve 7 (exp λ a b c d e f g → a :+ b :+ c :+ d :+ (a :+ e :+ f :+ g))
                       (exp λ a b c d e f g → a :+ b :+ c :+ a :+ e :+ f :+ (d :+ g))
                       ((d * e) ∷∷ (d * m) ∷∷ (n * e) ∷∷ (n * m) ∷∷
                        (d * m') ∷∷ (n' * e) ∷∷ (n' * m') ∷∷ ⟦⟧)

        lem₂ : d * e + d * m + n * e + d * e + d * m' + n' * e + (n' * m + n * m')
             ≡ (d + n') * (e + m) + (d + n) * (e + m')
        lem₂ = sym
             $ ap₂ _+_ (distr₂ d n' e m) (distr₂ d n e m')
             · solve 7 (exp λ a b c d e f g → a :+ b :+ c :+ d :+ (a :+ e :+ f :+ g))
                         (exp λ a b c d e f g → a :+ b :+ f :+ a :+ e :+ c :+ (d :+ g))
                         ((d * e) ∷∷ (d * m) ∷∷ (n' * e) ∷∷ (n' * m) ∷∷
                          (d * m') ∷∷ (n * e) ∷∷ (n * m') ∷∷ ⟦⟧)

    neg : ℕ → ℕ → ℤ
    neg n n' = n' [-] n

    neg-sound : (n n' d : ℕ) → neg n n' ≡ neg (d + n) (d + n')
    neg-sound n n' d = eq-ℤ n' n d

_+_ : ℤ → ℤ → ℤ
_+_ = elim₂-ℤ hℤ add add-sound

negate : ℤ → ℤ
negate = elim-ℤ hℤ (neg , neg-sound)

inc : ℤ → ℤ
inc n = one + n

dec : ℤ → ℤ
dec n = negate one + n

_*_ : ℤ → ℤ → ℤ
_*_ = elim₂-ℤ hℤ mul mul-sound

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


text:
-- Note that, at the time of writing, Agda does /not/ cache interfaces
-- if an internal error is encountered (at least in some cases).

import Issue2447.Internal-error

ext: agda

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
module Error-in-imported-module where

open import Error-in-imported-module.M


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.BlockStorage.BlockStore         as BlockStore
import      LibraBFT.Impl.Consensus.ConsensusTypes.SyncInfo         as SyncInfo
import      LibraBFT.Impl.Consensus.ConsensusTypes.Vote             as Vote
import      LibraBFT.Impl.Consensus.PendingVotes                    as PendingVotes
import      LibraBFT.Impl.OBM.ECP-LBFT-OBM-Diff.ECP-LBFT-OBM-Diff-1 as ECP-LBFT-OBM-Diff-1
open import LibraBFT.Impl.OBM.Logging.Logging
open import LibraBFT.Impl.OBM.Rust.Duration                         as Duration
open import LibraBFT.Impl.OBM.Rust.RustTypes
open import LibraBFT.Impl.OBM.Time
open import LibraBFT.ImplShared.Base.Types
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Util.Crypto
open import LibraBFT.ImplShared.Util.Dijkstra.All
open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open import Optics.All
open import Util.Hash
open import Util.ByteString
open import Util.PKCS
open import Util.Prelude
------------------------------------------------------------------------------
open import Agda.Builtin.Float

module LibraBFT.Impl.Consensus.Liveness.RoundState where

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

new : RoundStateTimeInterval → Instant → RoundState
new ti i = mkRoundState
  {-_rsTimeInterval          =-} ti
  {-_rsHighestCommittedRound =-} {-Round-} 0
  {-_rsCurrentRound          =-} {-Round-} 0
  {-_rsCurrentRoundDeadline  =-} i
  {-_rsPendingVotes          =-} PendingVotes∙new
  {-_rsVoteSent              =-} nothing

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

setupTimeoutM : Instant → LBFT Duration

processLocalTimeoutM : Instant → Epoch → Round → LBFT Bool
processLocalTimeoutM now obmEpoch round = do
  currentRound ← use (lRoundState ∙ rsCurrentRound)
  ifD round /= currentRound
    then pure false
    else do
      void (setupTimeoutM now) -- setup the next timeout
      ECP-LBFT-OBM-Diff-1.e_RoundState_processLocalTimeoutM obmEpoch round

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

maybeAdvanceRound : Round → SyncInfo → Maybe (Round × NewRoundReason)

processCertificatesM : Instant → SyncInfo → LBFT (Maybe NewRoundEvent)
processCertificatesM now syncInfo = do
  -- logEE ("RoundState" ∷ "processCertificatesM" {-∷ lsSI syncInfo-} ∷ []) $ do
  rshcr <- use (lRoundState ∙ rsHighestCommittedRound)
  whenD (syncInfo ^∙ siHighestCommitRound >? rshcr) $ do
    lRoundState ∙ rsHighestCommittedRound ∙= (syncInfo ^∙ siHighestCommitRound)
    logInfo fakeInfo -- InfoUpdateHighestCommittedRound (syncInfo^.siHighestCommitRound)
  rscr ← use (lRoundState ∙ rsCurrentRound)
  maybeSD (maybeAdvanceRound rscr syncInfo) (pure nothing) $ λ (pcr' , reason) → do
    lRoundState ∙ rsCurrentRound ∙= pcr'
    lRoundState ∙ rsPendingVotes ∙= PendingVotes∙new
    lRoundState ∙ rsVoteSent     ∙= nothing
    timeout                       ← setupTimeoutM now
    pure (just (NewRoundEvent∙new pcr' reason timeout))

abstract
  processCertificatesM-abs = processCertificatesM
  processCertificatesM-abs-≡ : processCertificatesM-abs ≡ processCertificatesM
  processCertificatesM-abs-≡ = refl

maybeAdvanceRound currentRound syncInfo =
  let newRound = SyncInfo.highestRound syncInfo + 1
   in if-dec newRound >? currentRound
      then just (newRound , (if is-nothing (syncInfo ^∙ siHighestTimeoutCert) then QCReady else TOReady))
      else nothing

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

insertVoteM : Vote → ValidatorVerifier → LBFT VoteReceptionResult
insertVoteM vote verifier = do
  currentRound ← use (lRoundState ∙ rsCurrentRound)
  ifD vote ^∙ vVoteData ∙ vdProposed ∙ biRound == currentRound
    then PendingVotes.insertVoteM vote verifier
    else pure (UnexpectedRound (vote ^∙ vVoteData ∙ vdProposed ∙ biRound) currentRound)

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

recordVoteM : Vote → LBFT Unit
recordVoteM v = rsVoteSent-rm ∙= just v

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

setupDeadlineM                : Instant → LBFT Duration
roundIndexAfterCommittedRound : Round → Round → Round
getRoundDuration              : ExponentialTimeInterval → Round → Duration

setupTimeoutM now = do
  timeout ← setupDeadlineM now
  r       ← use (lRoundState ∙ rsCurrentRound)
  -- act (SetTimeout timeout r)
  pure timeout

setupDeadlineM now = do
  ti          ← use (lRoundState ∙ rsTimeInterval)
  cr          ← use (lRoundState ∙ rsCurrentRound)
  hcr         ← use (lRoundState ∙ rsHighestCommittedRound)
  let timeout = getRoundDuration ti (roundIndexAfterCommittedRound cr hcr)
  lRoundState ∙ rsCurrentRoundDeadline ∙= iPlus now timeout
  pure timeout

roundIndexAfterCommittedRound currentRound highestCommittedRound =
  grd‖ highestCommittedRound == 0                 ≔ currentRound ∸ 1
     ‖ currentRound <?ℕ highestCommittedRound + 3 ≔ 0
     ‖ otherwise≔                                   currentRound ∸ highestCommittedRound ∸ 3

postulate -- TODO-1 : _**_, ceiling (for Floats)
  _**_    : Float → Float → Float
  ceiling : Float → U64

getRoundDuration i r =
  let pow            = min r (i ^∙ etiMaxExponent) -- TODO/NOTE: cap on max timeout
                                                   -- undermines theoretical liveness properties
      baseMultiplier = (i ^∙ etiExponentBase) ** {-fromIntegral-} primNatToFloat pow
    --durationMs     = ceiling (fromIntegral (i^.etiBaseMs) * baseMultiplier)
      durationMs     = ceiling (primFloatTimes (primNatToFloat (i ^∙ etiBaseMs)) baseMultiplier)
   in Duration.fromMillis durationMs


text:
module Issue2639.DR (Z : Set) where

open import Agda.Builtin.Size

mutual

  data D (i : Size) : Set where
    a : D i
    b : R i → D i

  record R (i : Size) : Set where
    coinductive
    field
      force : {j : Size< i} → D j


text:
-- This code is based on "Parallel Parsing Processes" by Koen
-- Claessen.

-- This module is a variant of Parallel in which Parser uses mixed
-- induction/coinduction.

module Parallel2 {Tok : Set} where

open import Coinduction
open import Data.Bool
import Data.Bool.Properties as Bool
open import Algebra
open import Data.Product
open import Data.Function
import Data.List as List
open List using (List; []; _∷_)
open import Data.Vec using ([]; _∷_)
open import Data.Fin using (#_)
open import Category.Monad.State
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

------------------------------------------------------------------------
-- Boring lemma

private

  lem₁ : ∀ b₁ b₂ → b₁ ∨ b₂ ∧ b₁ ≡ b₁
  lem₁ b₁ b₂ = begin
    b₁ ∨ b₂ ∧ b₁  ≡⟨ cong (_∨_ b₁) (B.∧-comm b₂ b₁) ⟩
    b₁ ∨ b₁ ∧ b₂  ≡⟨ proj₁ B.absorptive b₁ b₂ ⟩
    b₁            ∎
    where module B = BooleanAlgebra Bool.booleanAlgebra

------------------------------------------------------------------------
-- Parser monad

P : Set → Set
P = StateT (List Tok) List

------------------------------------------------------------------------
-- Basic parsers (no CPS)

-- Note that the recursive argument of symbolBind is coinductive,
-- while that of returnPlus is inductive. An infinite choice is not
-- acceptable, but an infinite tree of potential parsers is fine.

data Parser (R : Set) : Bool → Set where
  symbolBind : {e : Tok → Bool} →
               (f : (x : Tok) → ∞ (Parser R (e x))) → Parser R false
  fail       : Parser R false
  returnPlus : ∀ {e} (x : R) (p : Parser R e) → Parser R true

parse : ∀ {R e} → Parser R e → P R
parse (symbolBind f)   []       = []
parse (symbolBind f)   (x ∷ xs) = parse (♭ (f x)) xs
parse fail             _        = []
parse (returnPlus x p) xs       = (x , xs) ∷ parse p xs

cast : ∀ {R e₁ e₂} → e₁ ≡ e₂ → Parser R e₁ → Parser R e₂
cast refl = id

return : ∀ {R} → R → Parser R true
return x = returnPlus x fail

module DirectImplementations where

  -- The definition of _∣_ is fine, but is the definition of _>>=_
  -- acceptable?

  infixl 1 _>>=_
  infixl 0 _∣_

  _∣_ : ∀ {R e₁ e₂} → Parser R e₁ → Parser R e₂ → Parser R (e₁ ∨ e₂)
  symbolBind f₁    ∣ symbolBind f₂    = symbolBind (λ x → ♯ (♭ (f₁ x) ∣ ♭ (f₂ x)))

  fail             ∣ p₂               = p₂
  symbolBind f₁    ∣ fail             = symbolBind f₁
  returnPlus x₁ p₁ ∣ fail             = returnPlus x₁ p₁

  returnPlus x₁ p₁ ∣ p₂               = returnPlus x₁ (p₁ ∣ p₂)
  symbolBind f₁    ∣ returnPlus x₂ p₂ = returnPlus x₂ (symbolBind f₁ ∣ p₂)

  _>>=_ : ∀ {R₁ R₂ e₁ e₂} →
          Parser R₁ e₁ → (R₁ → Parser R₂ e₂) → Parser R₂ (e₁ ∧ e₂)
  symbolBind f₁        >>= f₂ = symbolBind (λ x → ♯ (♭ (f₁ x) >>= f₂))
  fail                 >>= f₂ = fail
  returnPlus {e} x₁ p₁ >>= f₂ = cast (lem₁ _ e) (f₂ x₁ ∣ p₁ >>= f₂)

  -- Implementing _!>>=_ seems tricky.

  -- _!>>=_ : ∀ {R₁ R₂} {e₂ : R₁ → Bool} →
  --          Parser R₁ false → ((x : R₁) → Parser R₂ (e₂ x)) →
  --          Parser R₂ false
  -- symbolBind f !>>= p₂ = symbolBind (λ x → ♯ {!♭ (f x) !>>= p₂!})
  -- fail         !>>= p₂ = fail

module IndirectImplementations where

  -- Can _>>=_ be implemented by using the productivity trick?

  infixl 1 _>>=_
  infixl 0 _∣_

  data PProg : Set → Bool → Set1 where
    symbolBind : ∀ {R} {e : Tok → Bool} →
                 (f : (x : Tok) → ∞₁ (PProg R (e x))) → PProg R false
    fail       : ∀ {R} → PProg R false
    returnPlus : ∀ {R e} (x : R) (p : PProg R e) → PProg R true
    _∣_        : ∀ {R e₁ e₂}
                 (p₁ : PProg R e₁) (p₂ : PProg R e₂) → PProg R (e₁ ∨ e₂)
    _>>=_      : ∀ {R₁ R₂ e₁ e₂}
                 (p₁ : PProg R₁ e₁) (f₂ : R₁ → PProg R₂ e₂) →
                 PProg R₂ (e₁ ∧ e₂)

  data PWHNF (R : Set) : Bool → Set1 where
    symbolBind : {e : Tok → Bool} →
                 (f : (x : Tok) → PProg R (e x)) → PWHNF R false
    fail       : PWHNF R false
    returnPlus : ∀ {e} (x : R) (p : PWHNF R e) → PWHNF R true

  -- _∣_ is a program, so implementing whnf seems challenging.

  whnf : ∀ {R e} → PProg R e → PWHNF R e
  whnf (symbolBind f)   = symbolBind (λ x → ♭₁ (f x))
  whnf fail             = fail
  whnf (returnPlus x p) = returnPlus x (whnf p)

  whnf (p₁ ∣ p₂) with whnf p₁
  ... | fail              = whnf p₂
  ... | returnPlus x₁ p₁′ = returnPlus x₁ {!(p₁′ ∣ p₂)!} -- (p₁′ ∣ p₂)
  ... | symbolBind f₁     with whnf p₂
  ...   | symbolBind f₂     = symbolBind (λ x → f₁ x ∣ f₂ x)
  ...   | fail              = symbolBind f₁
  ...   | returnPlus x₂ p₂′ = returnPlus x₂ {!!} -- (symbolBind f₁ ∣ p₂′)

  whnf (p₁ >>= f₂) with whnf p₁
  ... | symbolBind f₁     = symbolBind (λ x → f₁ x >>= f₂)
  ... | fail              = fail
  ... | returnPlus x₁ p₁′ = {!f₂ x₁ ∣ p₁′ >>= f₂!}

  mutual

    value : ∀ {R e} → PWHNF R e → Parser R e
    value (symbolBind f)   = symbolBind (λ x → ♯ ⟦ f x ⟧)
    value fail             = fail
    value (returnPlus x p) = returnPlus x (value p)

    ⟦_⟧ : ∀ {R e} → PProg R e → Parser R e
    ⟦ p ⟧ = value (whnf p)

max_stars_repo_name: yurrriq/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
module DerivedProps where

{-
open import Relation.Binary.PropositionalEquality
open import Data.Nat hiding (_>_)
-}

open import StdLibStuff

open import Syntax
open import STT

lem3 : {n : ℕ} {Γ-t : Ctx n} (F G : Form Γ-t $o) → ⊢ ((F => (F => G)) => (F => G))
lem3 F G = inf-V (inf-V ax-4-s ax-1-s) (inf-V (inf-V ax-4-s (inf-V ax-4-s ax-2-s)) ax-3-s)

lem4 : {n : ℕ} {Γ-t : Ctx n} (F G H : Form Γ-t $o) →
       ⊢ ((F => (G => H)) => (G => (F => H)))
lem4 F G H = inf-V (inf-V ax-4-s ax-1-s) (inf-V (inf-V ax-4-s (inf-V ax-4-s (inf-V (inf-V ax-4-s (inf-V (inf-V ax-4-s ax-3-s) ax-2-s)) ax-2-s))) (inf-V (inf-V ax-4-s ax-3-s) (inf-V ax-4-s (inf-V ax-4-s (inf-V (inf-V ax-4-s ax-3-s) ax-2-s)))))

lem5 : {n : ℕ} {Γ-t : Ctx n} (F G : Form Γ-t $o) →
       ⊢ ((F => G) => (~ G => ~ F))
lem5 F G = inf-V (inf-V ax-4-s ax-3-s) (inf-V ax-4-s (inf-V ax-3-s (inf-V (inf-V ax-4-s ax-1-s) ax-2-s)))

lem6 : {n : ℕ} {Γ-t : Ctx n} (F G H : Form Γ-t $o) →
       ⊢ ((F => H) => ((F & G) => H))
lem6 F G H = inf-V (inf-V ax-4-s ax-3-s) (inf-V (inf-V ax-4-s (inf-V ax-4-s (inf-V (inf-V ax-4-s (inf-V ax-3-s (inf-V (inf-V ax-4-s ax-1-s) ax-2-s))) ax-2-s))) ax-3-s)

lem6b : {n : ℕ} {Γ-t : Ctx n} (F G H : Form Γ-t $o) →
       ⊢ ((G => H) => ((F & G) => H))
lem6b F G H = inf-V (inf-V ax-4-s ax-3-s) (inf-V (inf-V ax-4-s (inf-V ax-4-s (inf-V (inf-V ax-4-s (inf-V ax-3-s (inf-V (inf-V ax-4-s ax-1-s) ax-2-s))) (inf-V (inf-V ax-4-s ax-3-s) ax-2-s)))) ax-3-s)

lemb3 : {n : ℕ} {Γ-t : Ctx n} (F G : Form Γ-t $o) →
        ⊢ (F => ((F => G) => G))
lemb3 F G = inf-V ax-1-s (inf-V (inf-V ax-4-s ax-3-s) (inf-V (inf-V ax-4-s ax-2-s) (inf-V (inf-V ax-4-s ax-2-s) (inf-V ax-3-s (inf-V ax-4-s (inf-V (inf-V ax-4-s ax-3-s) ax-2-s))))))

lem7 : {n : ℕ} {Γ-t : Ctx n} (F G H : Form Γ-t $o) →
       ⊢ (F => ((G => H) => ((F => G) => H)))
lem7 F G H = inf-V (inf-V ax-4-s (lem4 (F => G) (G => H) H)) (inf-V (inf-V ax-4-s (inf-V ax-4-s (lemb3 G H))) (lemb3 F G))

lem8h : {n : ℕ} {Γ-t : Ctx n} (F G H : Form Γ-t $o) →
        ⊢ ((H => (F => G)) => ((H => F) => (H => G)))
lem8h F G H = inf-V (inf-V ax-4-s ax-1-s) (inf-V (inf-V ax-4-s (inf-V ax-4-s (inf-V (inf-V ax-4-s ax-3-s) (inf-V (inf-V ax-4-s ax-2-s) ax-2-s)))) (inf-V (inf-V ax-4-s ax-3-s) (inf-V ax-4-s ax-4-s)))

lem8 : {n : ℕ} {Γ-t : Ctx n} (X F G H : Form Γ-t $o) →
       ⊢ ((F => (G => H)) => ((X => F) => ((X => G) => (X => H))))
lem8 X F G H = inf-V (inf-V ax-4-s (inf-V ax-4-s (lem8h G H X))) (inf-V (inf-V ax-4-s (lem8h F (G => H) X)) (inf-V (lem4 X (F => (G => H)) (F => (G => H))) (inf-V ax-3-s (inf-V ax-2-s (inf-V (inf-V ax-4-s ax-1-s) ax-2-s)))))

lem8-3 : {n : ℕ} {Γ-t : Ctx n} (X F G H I : Form Γ-t $o) →
       ⊢ ((F => (G => (H => I))) => ((X => F) => ((X => G) => ((X => H) => (X => I)))))
lem8-3 X F G H I = inf-V (inf-V ax-4-s (inf-V ax-4-s (inf-V ax-4-s (lem8h H I X)))) (inf-V (inf-V ax-4-s (inf-V ax-4-s (lem8h G (H => I) X))) (inf-V (inf-V ax-4-s (lem8h F (G => (H => I)) X)) (inf-V (lem4 X (F => (G => (H => I))) (F => (G => (H => I)))) (inf-V ax-3-s (inf-V ax-2-s (inf-V (inf-V ax-4-s ax-1-s) ax-2-s))))))

lemb2 : {n : ℕ} {Γ-t : Ctx n} (F : Form Γ-t $o) →
        ⊢ (~ (~ F) => F)
lemb2 F = inf-V ax-3-s (inf-V (inf-V ax-4-s (inf-V ax-3-s (inf-V (inf-V ax-4-s ax-1-s) ax-2-s))) (inf-V ax-3-s (inf-V (inf-V ax-4-s ax-1-s) ax-2-s)))

lem2h2h : {n : ℕ} {Γ-t : Ctx n} (F : Form Γ-t $o) →
          ⊢ (F => ~ (~ F))
lem2h2h F = inf-V ax-3-s (inf-V (inf-V ax-4-s ax-1-s) ax-2-s)

lem2h2hb : {n : ℕ} {Γ-t : Ctx n} (F : Form Γ-t $o) →
           ⊢ (F => F)
lem2h2hb F = inf-V (inf-V ax-4-s ax-1-s) ax-2-s

lem2h2 : {n : ℕ} {Γ-t : Ctx n} (F G H : Form Γ-t $o) →
         ⊢ ((F || (G || H)) => ((F || G) || H))
lem2h2 F G H = inf-V (inf-V ax-4-s (inf-V ax-4-s (lemb2 H))) (inf-V (inf-V ax-4-s ax-3-s) (inf-V (inf-V ax-4-s (inf-V ax-4-s ax-3-s)) (inf-V (inf-V ax-4-s (inf-V ax-4-s (inf-V ax-4-s (lemb2 F)))) (inf-V (inf-V ax-4-s (inf-V ax-4-s ax-3-s)) (inf-V (inf-V ax-4-s (lem4 (~ F) (~ H) G)) (inf-V (inf-V ax-4-s ax-3-s) (inf-V (inf-V ax-4-s (inf-V ax-4-s (lem2h2h F))) (inf-V (inf-V ax-4-s ax-3-s) (inf-V (inf-V ax-4-s (inf-V ax-4-s ax-3-s)) (inf-V (inf-V ax-4-s (inf-V ax-4-s (inf-V ax-4-s (lem2h2h H)))) (lem2h2hb (F || (G || H)))))))))))))

lem2h1 : {n : ℕ} {Γ-t : Ctx n} (F G H : Form Γ-t $o) →
         ⊢ ((F => (G => H)) => ((F & G) => H))
lem2h1 F G H = inf-V (inf-V ax-4-s ax-3-s) (inf-V (inf-V ax-4-s (inf-V ax-4-s (inf-V ax-3-s (inf-V (inf-V ax-4-s ax-1-s) ax-2-s)))) (inf-V (inf-V ax-4-s ax-3-s) (inf-V (inf-V ax-4-s (lem2h2 (~ F) (~ G) H)) (inf-V (inf-V ax-4-s ax-1-s) ax-2-s))))

lemb1 : {n : ℕ} {Γ-t : Ctx n} (F G : Form Γ-t $o) →
        ⊢ (F => (G => (F & G)))
lemb1 F G = inf-V ax-1-s (inf-V (inf-V ax-4-s ax-3-s) (inf-V (inf-V ax-4-s ax-2-s) (inf-V (inf-V ax-4-s ax-3-s) (inf-V (inf-V ax-4-s ax-2-s) (inf-V ax-3-s (inf-V ax-4-s ax-2-s))))))

lem2 : {n : ℕ} {Γ-t : Ctx n} (F G H : Form Γ-t $o) → ⊢ (((F => G) & (F => H)) => (F => (G & H)))
lem2 F G H = inf-V (lem2h1 (F => G) (F => H) (F => (G & H))) (inf-V (lem8 F G H (G & H)) (lemb1 G H))

lem9 : {n : ℕ} {Γ-t : Ctx n} (F G H : Form Γ-t $o) →
       ⊢ ((F => G) => ((G => H) => (F => H)))
lem9 F G H = inf-V (inf-V ax-4-s (lem4 F (G => H) H)) (inf-V (inf-V ax-4-s (inf-V ax-4-s (lemb3 G H))) (inf-V (lem4 F (F => G) G) (lemb3 F G)))

lemb4 : {n : ℕ} {Γ-t : Ctx n} (F G : Form Γ-t $o) →
        ⊢ (F => (~ F => G))
lemb4 F G = inf-V (inf-V ax-4-s ax-2-s) (inf-V ax-3-s (inf-V (inf-V ax-4-s ax-1-s) ax-2-s))

lem5r : {n : ℕ} {Γ-t : Ctx n} (F G : Form Γ-t $o) →
       ⊢ ((~ F => ~ G) => (G => F))
lem5r F G = inf-V (inf-V ax-4-s (inf-V ax-4-s (lemb2 F))) (inf-V (inf-V ax-4-s ax-3-s) (lem2h2hb (~ F => ~ G)))

lemb5 : {n : ℕ} {Γ-t : Ctx n} (F G H : Form Γ-t $o) →
        ⊢ ((F => H) => ((G => H) => ((F || G) => H)))
lemb5 F G H = inf-V (inf-V ax-4-s (inf-V ax-4-s (lem5r H (F || G)))) (inf-V (inf-V ax-4-s ax-3-s) (inf-V (inf-V ax-4-s (inf-V ax-4-s (inf-V (lem5 (G => H) (~ H => ~ G)) (lem5 G H)))) (inf-V (inf-V ax-4-s ax-3-s) (inf-V ax-3-s (inf-V (inf-V ax-4-s (inf-V (lem5 (F => H) (~ H => ~ F)) (lem5 F H))) (inf-V ax-3-s (inf-V (lem8 (~ H) (~ F) (~ G) (~ (F || G))) (inf-V (inf-V ax-4-s (inf-V ax-4-s (inf-V (lem5 (F || G) (~ (~ F) || ~ (~ G))) (inf-V (inf-V ax-4-s (inf-V ax-4-s (lem2h2h G))) (inf-V (inf-V ax-4-s ax-3-s) (inf-V (inf-V ax-4-s (inf-V ax-4-s (lem2h2h F))) (inf-V (inf-V ax-4-s ax-3-s) (lem2h2hb (F || G))))))))) (lemb1 (~ F) (~ G))))))))))

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

lem10 : {n : ℕ} {Γ-t : Ctx n} (F : Form Γ-t $o) →
        ⊢ ((F => $false) => ~ F)
lem10 F = inf-V ax-3-s (inf-V (inf-V ax-4-s (inf-V (lem5 (F => $false) (F => ~ F)) (inf-V ax-4-s (inf-V (inf-V ax-4-s (ax-5-s ($ this {refl}) (~ F))) (lem2h2hb (![ _ ] ($ this {refl}))))))) (inf-V ax-3-s ax-1-s))

lem11 : {n : ℕ} {Γ-t : Ctx n} (F : Form Γ-t $o) →
        ⊢ ($false => F)
lem11 F = inf-V (inf-V ax-4-s (ax-5-s ($ this {refl}) F)) (lem2h2hb (![ _ ] ($ this {refl})))

lem12 : {n : ℕ} {Γ-t : Ctx n} {t : Type n} (F : Form Γ-t t) →
        ⊢ (F == F)
lem12 {n} {Γ-t} {t} F = inf-V (inf-III-samectx {n} {Γ-t} {t} {t > $o} (λ z → (z · F)) (^[ t ] (![ t > $o ] (($ this {refl} · $ (next (next this)) {refl}) => ($ this {refl} · $ (next this) {refl})))) F) (inf-V (inf-III-samectx {n} {Γ-t} {t} {$o} (λ z → (z)) (![ t > $o ] (($ this {refl} · weak (weak F)) => ($ this {refl} · $ (next this) {refl}))) F) (inf-VI-s (subst (λ z → ⊢ ((($ this {refl} · z) => ($ this {refl} · weak F)))) (sub-weak-p-1 F F) (inf-V (inf-V ax-4-s ax-1-s) ax-2-s))))

lem13 : {n : ℕ} {Γ-t : Ctx n} (F G : Form Γ-t $o) →
        ⊢ ((G == F) => (F => G))
lem13 F G =
 inf-V (inf-III-samectx (λ z → ((z · F) => (F => G))) (^[ $o ] (![ $o > $o ] (($ this {refl} · $ (next (next this)) {refl}) => ($ this {refl} · $ (next this) {refl})))) G) (
 inf-V (inf-III-samectx (λ z → (z => (F => G))) (![ $o > $o ] (($ this {refl} · weak (weak G)) => ($ this {refl} · $ (next this) {refl}))) F) (
 subst (λ z → ⊢ ((![ $o > $o ] (($ this {refl} · z) => ($ this {refl} · weak F))) => (F => G))) (sub-weak-p-1 G F) (
 inf-V ax-3-s (
 inf-V (inf-V ax-4-s (inf-V (lem5 (![ $o > $o ] (($ this {refl} · weak G) => ($ this {refl} · weak F))) (((^[ $o ] ~ ($ this {refl})) · sub (^[ $o ] ~ ($ this {refl})) (weak G)) => ((^[ $o ] ~ ($ this {refl})) · sub (^[ $o ] ~ ($ this {refl})) (weak F))))
  (ax-5-s (($ this {refl} · weak G) => ($ this {refl} · weak F)) (^[ $o ] ~ ($ this {refl}))))) (
 inf-V ax-3-s (
 subst (λ z → ⊢ ((((^[ $o ] ~ ($ this {refl})) · z) => ((^[ $o ] ~ ($ this {refl})) · sub (^[ $o ] ~ ($ this {refl})) (weak F))) => (F => G))) (sub-weak-p-1' G (^[ $o ] ~ ($ this {refl}))) (
 subst (λ z → ⊢ ((((^[ $o ] ~ ($ this {refl})) · G) => ((^[ $o ] ~ ($ this {refl})) · z)) => (F => G))) (sub-weak-p-1' F (^[ $o ] ~ ($ this {refl}))) (
 inf-V (inf-III-samectx (λ z → ((z => ((^[ $o ] ~ ($ this {refl})) · F)) => (F => G))) (~ ($ this {refl})) G) (
 inf-V (inf-III-samectx (λ z → (((~ G) => z) => (F => G))) (~ ($ this {refl})) F) (
 lem5r G F
 ))))))))))

transitivity : {n : ℕ} {Γ-t : Ctx n} {t : Type n} (F G H : Form Γ-t t) →
         ⊢ ((F == G) => ((G == H) => (F == H)))
transitivity F G H =
 inf-V (inf-III-samectx (λ z → ((z · G) => ((G == H) => (F == H)))) (^[ _ ] (![ _ > $o ] (($ this {refl} · $ (next (next this)) {refl}) => ($ this {refl} · $ (next this) {refl})))) F) (
 inf-V (inf-III-samectx (λ z → (z => ((G == H) => (F == H)))) (![ _ > $o ] (($ this {refl} · weak (weak F)) => ($ this {refl} · $ (next this) {refl}))) G) (
 subst (λ z → ⊢ ((![ _ > $o ] (($ this {refl} · z) => ($ this {refl} · weak G))) => ((G == H) => (F == H)))) (sub-weak-p-1 F G) (
 inf-V (inf-III-samectx (λ z → ((![ _ > $o ] (($ this {refl} · weak F) => ($ this {refl} · weak G))) => ((z · H) => (F == H)))) (^[ _ ] (![ _ > $o ] (($ this {refl} · $ (next (next this)) {refl}) => ($ this {refl} · $ (next this) {refl})))) G) (
 inf-V (inf-III-samectx (λ z → ((![ _ > $o ] (($ this {refl} · weak F) => ($ this {refl} · weak G))) => (z => (F == H)))) (![ _ > $o ] (($ this {refl} · weak (weak G)) => ($ this {refl} · $ (next this) {refl}))) H) (
 subst (λ z → ⊢ ((![ _ > $o ] (($ this {refl} · weak F) => ($ this {refl} · weak G))) => ((![ _ > $o ] (($ this {refl} · z) => ($ this {refl} · weak H))) => (F == H)))) (sub-weak-p-1 G H) (
 inf-V (inf-III-samectx (λ z → ((![ _ > $o ] (($ this {refl} · weak F) => ($ this {refl} · weak G))) => ((![ _ > $o ] (($ this {refl} · weak G) => ($ this {refl} · weak H))) => (z · H)))) (^[ _ ] (![ _ > $o ] (($ this {refl} · $ (next (next this)) {refl}) => ($ this {refl} · $ (next this) {refl})))) F) (
 inf-V (inf-III-samectx (λ z → ((![ _ > $o ] (($ this {refl} · weak F) => ($ this {refl} · weak G))) => ((![ _ > $o ] (($ this {refl} · weak G) => ($ this {refl} · weak H))) => z))) (![ _ > $o ] (($ this {refl} · weak (weak F)) => ($ this {refl} · $ (next this) {refl}))) H) (
 subst (λ z → ⊢ ((![ _ > $o ] (($ this {refl} · weak F) => ($ this {refl} · weak G))) => ((![ _ > $o ] (($ this {refl} · weak G) => ($ this {refl} · weak H))) => (![ _ > $o ] (($ this {refl} · z) => ($ this {refl} · weak H)))))) (sub-weak-p-1 F H) (
 inf-V (inf-V ax-4-s (ax-6-s {_} {_} {_} {~ (![ _ ] (($ this {refl} · weak G) => ($ this {refl} · weak H)))} {($ this {refl} · weak F) => ($ this {refl} · weak H)})) (
 inf-V (ax-6-s {_} {_} {_} {~ (![ _ ] (($ this {refl} · weak F) => ($ this {refl} · weak G)))} {(weak (![ _ ] (($ this {refl} · weak G) => ($ this {refl} · weak H)))) => (($ this {refl} · weak F) => ($ this {refl} · weak H))}) (
 inf-VI-s (
 inf-V ax-3-s (
 inf-V (inf-V ax-4-s (inf-V (lem5 (![ _ ] (($ this {refl} · weak-i (_ ∷ ε) _ (weak F)) => ($ this {refl} · weak-i (_ ∷ ε) _ (weak G)))) (sub ($ this {refl}) (($ this {refl} · weak-i (_ ∷ ε) _ (weak F)) => ($ this {refl} · weak-i (_ ∷ ε) _ (weak G)))))
  (ax-5-s (($ this {refl} · weak-i (_ ∷ ε) _ (weak F)) => ($ this {refl} · weak-i (_ ∷ ε) _ (weak G))) ($ this {refl})))) (
 inf-V ax-3-s (
 inf-V (inf-V ax-4-s ax-3-s) (
 inf-V (inf-V ax-4-s (inf-V ax-4-s (inf-V (lem5 (![ _ ] (($ this {refl} · weak-i (_ ∷ ε) _ (weak G)) => ($ this {refl} · weak-i (_ ∷ ε) _ (weak H)))) (sub ($ this {refl}) (($ this {refl} · weak-i (_ ∷ ε) _ (weak G)) => ($ this {refl} · weak-i (_ ∷ ε) _ (weak H)))))
  (ax-5-s (($ this {refl} · weak-i (_ ∷ ε) _ (weak G)) => ($ this {refl} · weak-i (_ ∷ ε) _ (weak H))) ($ this {refl}))))) (
 inf-V (inf-V ax-4-s ax-3-s) (
 subst (λ z → ⊢ (((($ this {refl}) · z) => (($ this {refl}) · (sub ($ this {refl}) (weak-i (_ ∷ ε) _ (weak G))))) => (((($ this {refl}) · (sub ($ this {refl}) (weak-i (_ ∷ ε) _ (weak G)))) => (($ this {refl}) · (sub ($ this {refl}) (weak-i (_ ∷ ε) _ (weak H))))) => (($ this {refl} · weak F) => ($ this {refl} · weak H))))) (sub-weak-p-23 F ($ this {refl})) (
 subst (λ z → ⊢ (((($ this {refl}) · (weak F)) => (($ this {refl}) · z)) => (((($ this {refl}) · (sub ($ this {refl}) (weak-i (_ ∷ ε) _ (weak G)))) => (($ this {refl}) · (sub ($ this {refl}) (weak-i (_ ∷ ε) _ (weak H))))) => (($ this {refl} · weak F) => ($ this {refl} · weak H))))) (sub-weak-p-23 G ($ this {refl})) (
 subst (λ z → ⊢ (((($ this {refl}) · (weak F)) => (($ this {refl}) · (weak G))) => (((($ this {refl}) · z) => (($ this {refl}) · (sub ($ this {refl}) (weak-i (_ ∷ ε) _ (weak H))))) => (($ this {refl} · weak F) => ($ this {refl} · weak H))))) (sub-weak-p-23 G ($ this {refl})) (
 subst (λ z → ⊢ (((($ this {refl}) · (weak F)) => (($ this {refl}) · (weak G))) => (((($ this {refl}) · (weak G)) => (($ this {refl}) · z)) => (($ this {refl} · weak F) => ($ this {refl} · weak H))))) (sub-weak-p-23 H ($ this {refl})) (
 lem9 ($ this {refl} · weak F) ($ this {refl} · weak G) ($ this {refl} · weak H)
 ))))))))))))))))))))))

lem14 : {n : ℕ} {Γ-t : Ctx n} {t : Type n} (F G H I : Form Γ-t t) →
        ⊢ ((F == G) => ((G == H) => ((H == I) => (F == I))))
lem14 F G H I = inf-V (inf-V ax-4-s (inf-V ax-4-s (transitivity F H I))) (transitivity F G H)

lem15 : {n : ℕ} {Γ-t : Ctx n} {t : Type n} (F G : Form Γ-t t) →
        ⊢ ((F == G) => (G == F))
lem15 F G =
 inf-V (inf-III-samectx (λ z → ((z · G) => (G == F))) (^[ _ ] (![ _ > $o ] (($ this {refl} · $ (next (next this)) {refl}) => ($ this {refl} · $ (next this) {refl})))) F) (
 inf-V (inf-III-samectx (λ z → (z => (G == F))) (![ _ > $o ] (($ this {refl} · weak (weak F)) => ($ this {refl} · $ (next this) {refl}))) G) (
 subst (λ z → ⊢ ((![ _ > $o ] (($ this {refl} · z) => ($ this {refl} · weak G))) => (G == F))) (sub-weak-p-1 F G) (
 inf-V (inf-III-samectx (λ z → ((![ _ > $o ] (($ this {refl} · weak F) => ($ this {refl} · weak G))) => (z · F))) (^[ _ ] (![ _ > $o ] (($ this {refl} · $ (next (next this)) {refl}) => ($ this {refl} · $ (next this) {refl})))) G) (
 inf-V (inf-III-samectx (λ z → ((![ _ > $o ] (($ this {refl} · weak F) => ($ this {refl} · weak G))) => z)) (![ _ > $o ] (($ this {refl} · weak (weak G)) => ($ this {refl} · $ (next this) {refl}))) F) (
 subst (λ z → ⊢ ((![ _ > $o ] (($ this {refl} · weak F) => ($ this {refl} · weak G))) => (![ _ > $o ] (($ this {refl} · z) => ($ this {refl} · weak F))))) (sub-weak-p-1 G F) (
 inf-V (ax-6-s {_} {_} {_} {~ (![ _ ] (($ this {refl} · weak F) => ($ this {refl} · weak G)))} {($ this {refl} · weak G) => ($ this {refl} · weak F)}) (
 inf-VI-s (
 inf-V ax-3-s (
 inf-V (inf-V ax-4-s (inf-V (lem5 (![ _ ] (($ this {refl} · weak-i (_ ∷ ε) _ (weak F)) => ($ this {refl} · weak-i (_ ∷ ε) _ (weak G)))) (sub (^[ _ ] ~ ($ (next this) {refl} · $ this {refl})) (($ this {refl} · weak-i (_ ∷ ε) _ (weak F)) => ($ this {refl} · weak-i (_ ∷ ε) _ (weak G)))))
  (ax-5-s (($ this {refl} · weak-i (_ ∷ ε) _ (weak F)) => ($ this {refl} · weak-i (_ ∷ ε) _ (weak G))) (^[ _ ] ~ ($ (next this) {refl} · $ this {refl}))))) (
 inf-V ax-3-s (
 subst (λ z → ⊢ ((((^[ _ ] ~ ($ (next this) {refl} · $ this {refl})) · z) => ((^[ _ ] ~ ($ (next this) {refl} · $ this {refl})) · (sub (^[ _ ] ~ ($ (next this) {refl} · $ this {refl})) (weak-i (_ ∷ ε) _ (weak G))))) => (($ this {refl} · weak G) => ($ this {refl} · weak F)))) (sub-weak-p-23 F (^[ _ ] ~ ($ (next this) {refl} · $ this {refl}))) (
 subst (λ z → ⊢ ((((^[ _ ] ~ ($ (next this) {refl} · $ this {refl})) · (weak F)) => ((^[ _ ] ~ ($ (next this) {refl} · $ this {refl})) · z)) => (($ this {refl} · weak G) => ($ this {refl} · weak F)))) (sub-weak-p-23 G (^[ _ ] ~ ($ (next this) {refl} · $ this {refl}))) (
 inf-V (inf-III-samectx (λ z → ((z => ((^[ _ ] ~ ($ (next this) {refl} · $ this {refl})) · weak G)) => (($ this {refl} · weak G) => ($ this {refl} · weak F)))) (~ ($ (next this) {refl} · $ this {refl})) (weak F)) (
 inf-V (inf-III-samectx (λ z → (((~ ($ this {refl} · weak F)) => z) => (($ this {refl} · weak G) => ($ this {refl} · weak F)))) (~ ($ (next this) {refl} · $ this {refl})) (weak G)) (
 lem5r ($ this {refl} · weak F) ($ this {refl} · weak G)
 )))))))))))))))

substitutivity : {n : ℕ} {Γ-t : Ctx n} {t u : Type n} (F G : Form Γ-t t) (H : Form Γ-t (t > u)) →
        ⊢ ((F == G) => ((H · F) == (H · G)))
substitutivity F G H =
 inf-V (inf-III-samectx (λ z → ((z · G) => ((H · F) == (H · G)))) (^[ _ ] (![ _ > _ ] (($ this {refl} · $ (next (next this)) {refl}) => ($ this {refl} · $ (next this) {refl})))) F) (
 inf-V (inf-III-samectx (λ z → (z => ((H · F) == (H · G)))) (![ _ > _ ] (($ this {refl} · weak (weak F)) => ($ this {refl} · $ (next this) {refl}))) G) (
 subst (λ z → ⊢ ((![ _ > _ ] (($ this {refl} · z) => ($ this {refl} · weak G))) => ((H · F) == (H · G)))) (sub-weak-p-1 F G) (
 inf-V (inf-III-samectx (λ z → ((![ _ > _ ] (($ this {refl} · weak F) => ($ this {refl} · weak G))) => (z · (H · G)))) (^[ _ ] (![ _ > _ ] (($ this {refl} · $ (next (next this)) {refl}) => ($ this {refl} · $ (next this) {refl})))) ((H · F))) (
 inf-V (inf-III-samectx (λ z → ((![ _ > _ ] (($ this {refl} · weak F) => ($ this {refl} · weak G))) => z)) (![ _ > _ ] (($ this {refl} · weak (weak ((H · F)))) => ($ this {refl} · $ (next this) {refl}))) ((H · G))) (
 subst (λ z → ⊢ ((![ _ > _ ] (($ this {refl} · weak F) => ($ this {refl} · weak G))) => (![ _ > _ ] (($ this {refl} · z) => ($ this {refl} · weak ((H · G))))))) (sub-weak-p-1 ((H · F)) ((H · G))) (
 inf-V (ax-6-s {_} {_} {_} {~ (![ _ ] (($ this {refl} · weak F) => ($ this {refl} · weak G)))} {($ this {refl} · weak ((H · F))) => ($ this {refl} · weak ((H · G)))}) (
 inf-VI-s (
 inf-V ax-3-s (
 inf-V (inf-V ax-4-s (inf-V (lem5 (![ _ ] (($ this {refl} · weak-i (_ ∷ ε) _ (weak F)) => ($ this {refl} · weak-i (_ ∷ ε) _ (weak G)))) (sub (^[ _ ] ($ (next this) {refl} · (weak (weak H) · $ this {refl}))) (($ this {refl} · weak-i (_ ∷ ε) _ (weak F)) => ($ this {refl} · weak-i (_ ∷ ε) _ (weak G)))))
  (ax-5-s (($ this {refl} · weak-i (_ ∷ ε) _ (weak F)) => ($ this {refl} · weak-i (_ ∷ ε) _ (weak G))) (^[ _ ] ($ (next this) {refl} · (weak (weak H) · $ this {refl})))))) (
 inf-V ax-3-s (
 subst (λ z → ⊢ ((((^[ _ ] ($ (next this) {refl} · (weak (weak H) · $ this {refl}))) · z) => ((^[ _ ] ($ (next this) {refl} · (weak (weak H) · $ this {refl}))) · (sub (^[ _ ] ($ (next this) {refl} · (weak (weak H) · $ this {refl}))) (weak-i (_ ∷ ε) _ (weak G))))) => (($ this {refl} · weak (H · F)) => ($ this {refl} · weak (H · G))))) {-{weak F} {sub (^[ _ ] ($ (next this) {refl} · (weak (weak H) · $ this {refl}))) (weak-i (_ ∷ ε) _ (weak F))}-} (sub-weak-p-23 F (^[ _ ] ($ (next this) {refl} · (weak (weak H) · $ this {refl})))) (
  subst (λ z → ⊢ ((((^[ _ ] ($ (next this) {refl} · (weak (weak H) · $ this {refl}))) · (weak F)) => ((^[ _ ] ($ (next this) {refl} · (weak (weak H) · $ this {refl}))) · z)) => (($ this {refl} · weak (H · F)) => ($ this {refl} · weak (H · G))))) {-{weak G} {sub (^[ _ ] ($ (next this) {refl} · (weak (weak H) · $ this {refl}))) (weak-i (_ ∷ ε) _ (weak G))}-} (sub-weak-p-23 G (^[ _ ] ($ (next this) {refl} · (weak (weak H) · $ this {refl})))) (
 inf-V (inf-III-samectx (λ z → ((z => ((^[ _ ] ($ (next this) {refl} · (weak (weak H) · $ this {refl}))) · weak G)) => (($ this {refl} · weak (H · F)) => ($ this {refl} · weak (H · G))))) ($ (next this) {refl} · (weak (weak H) · $ this {refl})) (weak F)) (
 subst (λ z → ⊢ ((($ this {refl} · (z · weak F)) => ((^[ _ ] ($ (next this) {refl} · (weak (weak H) · $ this {refl}))) · weak G)) => (($ this {refl} · weak (H · F)) => ($ this {refl} · weak (H · G))))) {-{weak H} {sub (weak F) (weak (weak H))}-} (sub-weak-p-1' (weak H) (weak F)) (
 inf-V (inf-III-samectx (λ z → ((($ this {refl} · weak (H · F)) => z) => (($ this {refl} · weak (H · F)) => ($ this {refl} · weak (H · G))))) ($ (next this) {refl} · (weak (weak H) · $ this {refl})) (weak G)) (
 subst (λ z → ⊢ ((($ this {refl} · (weak (H · F))) => ($ this {refl} · (z · weak G))) => (($ this {refl} · weak (H · F)) => ($ this {refl} · weak (H · G))))) {-{weak H} {sub (weak G) (weak (weak H))}-} (sub-weak-p-1' (weak H) (weak G)) (
 lem2h2hb (($ this {refl} · weak (H · F)) => ($ this {refl} · (weak H · weak G)))
 )))))))))))))))))

lem16 : {n : ℕ} {Γ-t : Ctx n} {α β : Type n} (F₁ F₂ : Form Γ-t (α > β)) (G₁ G₂ : Form Γ-t α) →
        ⊢ ((F₁ == F₂) => ((G₁ == G₂) => ((F₁ · G₁) == (F₂ · G₂))))
lem16 F₁ F₂ G₁ G₂ =
 inf-V (inf-V (inf-V (lem8 (F₁ == F₂) ((G₁ == G₂) => ((F₁ · G₁) == (F₂ · G₁))) ((G₁ == G₂) => ((F₂ · G₁) == (F₂ · G₂))) ((G₁ == G₂) => ((F₁ · G₁) == (F₂ · G₂))))
 (inf-V (lem8 (G₁ == G₂) ((F₁ · G₁) == (F₂ · G₁)) ((F₂ · G₁) == (F₂ · G₂)) ((F₁ · G₁) == (F₂ · G₂))) (
  transitivity (F₁ · G₁) (F₂ · G₁) (F₂ · G₂))))
 (inf-V (lem4 (G₁ == G₂) (F₁ == F₂) ((F₁ · G₁) == (F₂ · G₁))) (inf-V ax-3-s (inf-V ax-2-s (
  subst (λ z → ⊢ ((F₁ == F₂) => ((F₁ · G₁) == (F₂ · z)))) (sym (sub-weak-p-1' G₁ F₂)) (
  inf-V (inf-II-samectx (λ z → ((F₁ == F₂) => ((F₁ · G₁) == z))) (($ this {refl}) · weak G₁) F₂) (
  subst (λ z → ⊢ ((F₁ == F₂) => ((F₁ · z) == ((^[ _ ] (($ this {refl}) · weak G₁)) · F₂)))) (sym (sub-weak-p-1' G₁ F₁)) (
  inf-V (inf-II-samectx (λ z → ((F₁ == F₂) => (z == ((^[ _ ] (($ this {refl}) · weak G₁)) · F₂)))) (($ this {refl}) · weak G₁) F₁) (
  substitutivity F₁ F₂ (^[ _ ] (($ this {refl}) · weak G₁))
 )))))))))
 (inf-V ax-3-s (inf-V ax-2-s (
  subst (λ z → ⊢ ((G₁ == G₂) => ((F₂ · G₁) == (z · G₂)))) (sym (sub-weak-p-1' F₂ G₂)) (
  inf-V (inf-II-samectx (λ z → ((G₁ == G₂) => ((F₂ · G₁) == z))) (weak F₂ · ($ this {refl})) G₂) (
  subst (λ z → ⊢ ((G₁ == G₂) => ((z · G₁) == ((^[ _ ] (weak F₂ · ($ this {refl}))) · G₂)))) (sym (sub-weak-p-1' F₂ G₁)) (
  inf-V (inf-II-samectx (λ z → ((G₁ == G₂) => (z == ((^[ _ ] (weak F₂ · ($ this {refl}))) · G₂)))) (weak F₂ · ($ this {refl})) G₁) (
  substitutivity G₁ G₂ (^[ _ ] (weak F₂ · ($ this {refl})))
 )))))))

max_stars_repo_name: frelindb/agsyHOL

max_issues_repo_name: frelindb/agsyHOL

max_forks_repo_name: frelindb/agsyHOL


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- The Covec type and some operations
------------------------------------------------------------------------

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

module Codata.Covec where

open import Size

open import Codata.Thunk using (Thunk; force)
open import Codata.Conat as Conat
open import Codata.Conat.Bisimilarity
open import Codata.Conat.Properties
open import Codata.Cofin as Cofin using (Cofin; zero; suc)
open import Codata.Colist as Colist using (Colist ; [] ; _∷_)
open import Codata.Stream as Stream using (Stream ; _∷_)
open import Function

data Covec {ℓ} (A : Set ℓ) (i : Size) : Conat ∞ → Set ℓ where
  []  : Covec A i zero
  _∷_ : ∀ {n} → A → Thunk (λ i → Covec A i (n .force)) i → Covec A i (suc n)

module _ {ℓ} {A : Set ℓ} where

 head : ∀ {n i} → Covec A i (suc n) → A
 head (x ∷ _) = x

 tail : ∀ {n} → Covec A ∞ (suc n) → Covec A ∞ (n .force)
 tail (_ ∷ xs) = xs .force

 lookup : ∀ {n} → Cofin n → Covec A ∞ n → A
 lookup zero    = head
 lookup (suc k) = lookup k ∘′ tail

 replicate : ∀ {i} → (n : Conat ∞) → A → Covec A i n
 replicate zero    a = []
 replicate (suc n) a = a ∷ λ where .force → replicate (n .force) a

 cotake : ∀ {i} → (n : Conat ∞) → Stream A i → Covec A i n
 cotake zero    xs       = []
 cotake (suc n) (x ∷ xs) = x ∷ λ where .force → cotake (n .force) (xs .force)

 infixr 5 _++_
 _++_ : ∀ {i m n} → Covec A i m → Covec A i n → Covec A i (m + n)
 []       ++ ys = ys
 (x ∷ xs) ++ ys = x ∷ λ where .force → xs .force ++ ys

 fromColist : ∀ {i} → (xs : Colist A ∞) → Covec A i (Colist.length xs)
 fromColist []       = []
 fromColist (x ∷ xs) = x ∷ λ where .force → fromColist (xs .force)

 toColist : ∀ {i n} → Covec A i n → Colist A i
 toColist []       = []
 toColist (x ∷ xs) = x ∷ λ where .force → toColist (xs .force)

 fromStream : ∀ {i} → Stream A i → Covec A i infinity
 fromStream = cotake infinity

 cast : ∀ {i} {m n} → i ⊢ m ≈ n → Covec A i m → Covec A i n
 cast zero     []       = []
 cast (suc eq) (a ∷ as) = a ∷ λ where .force → cast (eq .force) (as .force)

module _ {a b} {A : Set a} {B : Set b} where

 map : ∀ {i n} (f : A → B) → Covec A i n → Covec B i n
 map f []       = []
 map f (a ∷ as) = f a ∷ λ where .force → map f (as .force)

 ap : ∀ {i n} → Covec (A → B) i n → Covec A i n → Covec B i n
 ap []       []       = []
 ap (f ∷ fs) (a ∷ as) = (f a) ∷ λ where .force → ap (fs .force) (as .force)

 scanl : ∀ {i n} → (B → A → B) → B → Covec A i n → Covec B i (1 ℕ+ n)
 scanl c n []       = n ∷ λ where .force → []
 scanl c n (a ∷ as) = n ∷ λ where
   .force → cast (suc λ where .force → 0ℕ+-identity)
                 (scanl c (c n a) (as .force))

module _ {a b c} {A : Set a} {B : Set b} {C : Set c} where

 zipWith : ∀ {i n} → (A → B → C) → Covec A i n → Covec B i n → Covec C i n
 zipWith f []       []       = []
 zipWith f (a ∷ as) (b ∷ bs) =
   f a b ∷ λ where .force → zipWith f (as .force) (bs .force)


text:
module Structure.Category.Functor.Proofs where

open import Data.Tuple as Tuple using (_,_)
open import Functional using (_$_)
open import Logic.Predicate
import      Lvl
open import Structure.Category
open import Structure.Categorical.Properties
open import Structure.Category.Functor
open import Structure.Category.Functor.Equiv
open import Structure.Function
open import Structure.Operator
open import Structure.Relator.Equivalence
open import Structure.Relator.Properties
open import Structure.Setoid
open import Syntax.Transitivity
open import Type

private variable ℓ ℓₗₑ ℓᵣₑ : Lvl.Level
private variable Obj Obj₁ Obj₂ Obj₃ : Type{ℓ}
private variable Morphism Morphism₁ Morphism₂ Morphism₃ : Obj → Obj → Type{ℓ}

module _
  ⦃ morphism-equiv₁ : ∀{x y} → Equiv{ℓₗₑ}(Morphism₁ x y) ⦄
  ⦃ morphism-equiv₂ : ∀{x y} → Equiv{ℓᵣₑ}(Morphism₂ x y) ⦄
  {cat₁ : Category(Morphism₁)}
  {cat₂ : Category(Morphism₂)}
  (F : Obj₁ → Obj₂)
  ⦃ functor : Functor(cat₁)(cat₂)(F) ⦄
  where

  open Category.ArrowNotation ⦃ … ⦄
  open Category ⦃ … ⦄
  open Functor(functor)
  private open module MorphismEquivₗ {x}{y} = Equiv(morphism-equiv₁{x}{y}) using () renaming (_≡_ to _≡ₗₘ_)
  private open module MorphismEquivᵣ {x}{y} = Equiv(morphism-equiv₂{x}{y}) using () renaming (_≡_ to _≡ᵣₘ_)

  private instance _ = cat₁
  private instance _ = cat₂
  private variable x y : Obj₁

  isomorphism-preserving : ∀{f : x ⟶ y} → Morphism.Isomorphism ⦃ \{x y} → morphism-equiv₁ {x}{y} ⦄ (_∘_)(id)(f) → Morphism.Isomorphism ⦃ \{x y} → morphism-equiv₂ {x}{y} ⦄ (_∘_)(id)(map f)
  ∃.witness (isomorphism-preserving ([∃]-intro g)) = map g
  ∃.proof (isomorphism-preserving {f = f} iso@([∃]-intro g)) =
    (Morphism.intro $
      map g ∘ map f 🝖-[ op-preserving ]-sym
      map(g ∘ f)    🝖-[ congruence₁(map) (inverseₗ(f)(g)) ]
      map id        🝖-[ id-preserving ]
      id            🝖-end
    ) , (Morphism.intro $
      map f ∘ map g 🝖-[ op-preserving ]-sym
      map(f ∘ g)    🝖-[ congruence₁(map) (inverseᵣ(f)(g)) ]
      map id        🝖-[ id-preserving ]
      id            🝖-end
    )
    where
      open Morphism.OperModule (\{x : Obj₁} → _∘_ {x = x})
      open Morphism.IdModule   (\{x : Obj₁} → _∘_ {x = x})(id)
      open Morphism.Isomorphism(\{x : Obj₁} → _∘_ {x = x})(id)(f)
      instance _ = iso

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
-- {-# OPTIONS -v tc.lhs:10 -v tc.lhs.split:50 #-}

postulate A : Set

record R : Set where
  field f : A

test : _ → A
test record{f = a} = a
-- This could succeed, but Agda currently does not try to guess
-- the type type of the record pattern from its field names.

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module Generic.Test.Eq where

open import Generic.Main hiding (List; []; _∷_)
open import Generic.Test.Data.Fin
open import Generic.Test.Data.List
open import Generic.Test.Data.Vec

xs : Vec (List (Fin 4)) 3
xs = (fsuc fzero ∷ fzero ∷ [])
   ∷ᵥ (fsuc (fsuc fzero) ∷ [])
   ∷ᵥ (fzero ∷ fsuc (fsuc (fsuc fzero)) ∷ [])
   ∷ᵥ []ᵥ

test : xs ≟ xs ≡ yes refl
test = refl

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


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

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Functions.Fixpoint

open import Cubical.Data.Empty as ⊥
open import Cubical.HITs.PropositionalTruncation.Base

private
  variable
    ℓ  : Level
    A  : Type ℓ

-- Negation
infix 3 ¬_

¬_ : Type ℓ → Type ℓ
¬ A = A → ⊥

-- Decidable types (inspired by standard library)
data Dec (P : Type ℓ) : Type ℓ where
  yes : ( p :   P) → Dec P
  no  : (¬p : ¬ P) → Dec P

NonEmpty : Type ℓ → Type ℓ
NonEmpty A = ¬ ¬ A

Stable : Type ℓ → Type ℓ
Stable A = NonEmpty A → A

-- reexport propositional truncation for uniformity
open Cubical.HITs.PropositionalTruncation.Base
  using (∥_∥) public

SplitSupport : Type ℓ → Type ℓ
SplitSupport A = ∥ A ∥ → A

Collapsible : Type ℓ → Type ℓ
Collapsible A = Σ[ f ∈ (A → A) ] 2-Constant f

Populated ⟪_⟫ : Type ℓ → Type ℓ
Populated A = (f : Collapsible A) → Fixpoint (f .fst)
⟪_⟫ = Populated

PStable : Type ℓ → Type ℓ
PStable A = ⟪ A ⟫ → A

onAllPaths : (Type ℓ → Type ℓ) → Type ℓ → Type ℓ
onAllPaths S A = (x y : A) → S (x ≡ y)

Separated : Type ℓ → Type ℓ
Separated = onAllPaths Stable

HSeparated : Type ℓ → Type ℓ
HSeparated = onAllPaths SplitSupport

Collapsible≡ : Type ℓ → Type ℓ
Collapsible≡ = onAllPaths Collapsible

PStable≡ : Type ℓ → Type ℓ
PStable≡ = onAllPaths PStable

Discrete : Type ℓ → Type ℓ
Discrete = onAllPaths Dec

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

module Definition.Conversion.Symmetry where

open import Definition.Untyped
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Conversion
open import Definition.Conversion.Stability
open import Definition.Conversion.Soundness
open import Definition.Conversion.Conversion
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.Equality
open import Definition.Typed.Consequences.Reduction
open import Definition.Typed.Consequences.Injectivity
open import Definition.Typed.Consequences.Substitution
open import Definition.Typed.Consequences.SucCong

open import Tools.Product
import Tools.PropositionalEquality as PE

mutual
  -- Symmetry of algorithmic equality of neutrals.
  sym~↑ : ∀ {t u A Γ Δ} → ⊢ Γ ≡ Δ
        → Γ ⊢ t ~ u ↑ A
        → ∃ λ B → Γ ⊢ A ≡ B × Δ ⊢ u ~ t ↑ B
  sym~↑ Γ≡Δ (var-refl x x≡y) =
    let ⊢A = syntacticTerm x
    in  _ , refl ⊢A
     ,  var-refl (PE.subst (λ y → _ ⊢ var y ∷ _) x≡y (stabilityTerm Γ≡Δ x))
                 (PE.sym x≡y)
  sym~↑ Γ≡Δ (app-cong t~u x) =
    let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
        B , whnfB , A≡B , u~t = sym~↓ Γ≡Δ t~u
        F′ , G′ , ΠF′G′≡B = Π≡A A≡B whnfB
        F≡F′ , G≡G′ = injectivity (PE.subst (λ x → _ ⊢ _ ≡ x) ΠF′G′≡B A≡B)
    in  _ , substTypeEq G≡G′ (soundnessConv↑Term x)
    ,   app-cong (PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) ΠF′G′≡B u~t)
                 (convConvTerm (symConv↑Term Γ≡Δ x) (stabilityEq Γ≡Δ F≡F′))
  sym~↑ Γ≡Δ (fst-cong p~r) =
    let B , whnfB , A≡B , r~p = sym~↓ Γ≡Δ p~r
        F′ , G′ , Σ≡ = Σ≡A A≡B whnfB
        F≡ , G≡ = Σ-injectivity (PE.subst (λ x → _ ⊢ _ ≡ x) Σ≡ A≡B)
    in  F′ , F≡ , fst-cong (PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) Σ≡ r~p)
  sym~↑ Γ≡Δ (snd-cong {p} {r} {F} {G} p~r) =
    let fst≡  = soundness~↑ (fst-cong p~r)
        B , whnfB , A≡B , r~p = sym~↓ Γ≡Δ p~r
        F′ , G′ , Σ≡ = Σ≡A A≡B whnfB
        r~p = PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) Σ≡ r~p
        F≡ , G≡ = Σ-injectivity (PE.subst (λ x → _ ⊢ _ ≡ x) Σ≡ A≡B)
    in  G′ [ fst r ] , substTypeEq G≡ fst≡ , snd-cong r~p
  sym~↑ Γ≡Δ (natrec-cong x x₁ x₂ t~u) =
    let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
        B , whnfB , A≡B , u~t = sym~↓ Γ≡Δ t~u
        B≡ℕ = ℕ≡A A≡B whnfB
        F≡G = stabilityEq (Γ≡Δ ∙ refl (ℕⱼ ⊢Γ)) (soundnessConv↑ x)
        F[0]≡G[0] = substTypeEq F≡G (refl (zeroⱼ ⊢Δ))
    in  _ , substTypeEq (soundnessConv↑ x) (soundness~↓ t~u)
    ,   natrec-cong (symConv↑ (Γ≡Δ ∙ (refl (ℕⱼ ⊢Γ))) x)
                    (convConvTerm (symConv↑Term Γ≡Δ x₁) F[0]≡G[0])
                    (convConvTerm (symConv↑Term Γ≡Δ x₂) (sucCong F≡G))
                    (PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) B≡ℕ u~t)
  sym~↑ Γ≡Δ (Emptyrec-cong x t~u) =
    let ⊢Γ , ⊢Δ , _ = contextConvSubst Γ≡Δ
        B , whnfB , A≡B , u~t = sym~↓ Γ≡Δ t~u
        B≡Empty = Empty≡A A≡B whnfB
        F≡G = stabilityEq Γ≡Δ (soundnessConv↑ x)
    in  _ , soundnessConv↑ x
    , Emptyrec-cong (symConv↑ Γ≡Δ x)
                    (PE.subst (λ x₁ → _ ⊢ _ ~ _ ↓ x₁) B≡Empty u~t)

  -- Symmetry of algorithmic equality of neutrals of types in WHNF.
  sym~↓ : ∀ {t u A Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ t ~ u ↓ A
         → ∃ λ B → Whnf B × Γ ⊢ A ≡ B × Δ ⊢ u ~ t ↓ B
  sym~↓ Γ≡Δ ([~] A₁ D whnfA k~l) =
    let B , A≡B , k~l′ = sym~↑ Γ≡Δ k~l
        _ , ⊢B = syntacticEq A≡B
        B′ , whnfB′ , D′ = whNorm ⊢B
        A≡B′ = trans (sym (subset* D)) (trans A≡B (subset* (red D′)))
    in  B′ , whnfB′ , A≡B′ , [~] B (stabilityRed* Γ≡Δ (red D′)) whnfB′ k~l′

  -- Symmetry of algorithmic equality of types.
  symConv↑ : ∀ {A B Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ A [conv↑] B → Δ ⊢ B [conv↑] A
  symConv↑ Γ≡Δ ([↑] A′ B′ D D′ whnfA′ whnfB′ A′<>B′) =
    [↑] B′ A′ (stabilityRed* Γ≡Δ D′) (stabilityRed* Γ≡Δ D) whnfB′ whnfA′
        (symConv↓ Γ≡Δ A′<>B′)

  -- Symmetry of algorithmic equality of types in WHNF.
  symConv↓ : ∀ {A B Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ A [conv↓] B → Δ ⊢ B [conv↓] A
  symConv↓ Γ≡Δ (U-refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  U-refl ⊢Δ
  symConv↓ Γ≡Δ (ℕ-refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  ℕ-refl ⊢Δ
  symConv↓ Γ≡Δ (Empty-refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  Empty-refl ⊢Δ
  symConv↓ Γ≡Δ (Unit-refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  Unit-refl ⊢Δ
  symConv↓ Γ≡Δ (ne A~B) =
    let B , whnfB , U≡B , B~A = sym~↓ Γ≡Δ A~B
        B≡U = U≡A U≡B
    in  ne (PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) B≡U B~A)
  symConv↓ Γ≡Δ (Π-cong x A<>B A<>B₁) =
    let F≡H = soundnessConv↑ A<>B
        _ , ⊢H = syntacticEq (stabilityEq Γ≡Δ F≡H)
    in  Π-cong ⊢H (symConv↑ Γ≡Δ A<>B)
                  (symConv↑ (Γ≡Δ ∙ F≡H) A<>B₁)
  symConv↓ Γ≡Δ (Σ-cong x A<>B A<>B₁) =
    let F≡H = soundnessConv↑ A<>B
        _ , ⊢H = syntacticEq (stabilityEq Γ≡Δ F≡H)
    in  Σ-cong ⊢H (symConv↑ Γ≡Δ A<>B)
                  (symConv↑ (Γ≡Δ ∙ F≡H) A<>B₁)

  -- Symmetry of algorithmic equality of terms.
  symConv↑Term : ∀ {t u A Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ t [conv↑] u ∷ A → Δ ⊢ u [conv↑] t ∷ A
  symConv↑Term Γ≡Δ ([↑]ₜ B t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u) =
    [↑]ₜ B u′ t′ (stabilityRed* Γ≡Δ D) (stabilityRed*Term Γ≡Δ d′)
         (stabilityRed*Term Γ≡Δ d) whnfB whnfu′ whnft′ (symConv↓Term Γ≡Δ t<>u)

  -- Symmetry of algorithmic equality of terms in WHNF.
  symConv↓Term : ∀ {t u A Γ Δ} → ⊢ Γ ≡ Δ → Γ ⊢ t [conv↓] u ∷ A → Δ ⊢ u [conv↓] t ∷ A
  symConv↓Term Γ≡Δ (ℕ-ins t~u) =
    let B , whnfB , A≡B , u~t = sym~↓ Γ≡Δ t~u
        B≡ℕ = ℕ≡A A≡B whnfB
    in  ℕ-ins (PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) B≡ℕ u~t)
  symConv↓Term Γ≡Δ (Empty-ins t~u) =
    let B , whnfB , A≡B , u~t = sym~↓ Γ≡Δ t~u
        B≡Empty = Empty≡A A≡B whnfB
    in  Empty-ins (PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) B≡Empty u~t)
  symConv↓Term Γ≡Δ (Unit-ins t~u) =
    let B , whnfB , A≡B , u~t = sym~↓ Γ≡Δ t~u
        B≡Unit = Unit≡A A≡B whnfB
    in  Unit-ins (PE.subst (λ x → _ ⊢ _ ~ _ ↓ x) B≡Unit u~t)
  symConv↓Term Γ≡Δ (ne-ins t u x t~u) =
    let B , whnfB , A≡B , u~t = sym~↓ Γ≡Δ t~u
    in  ne-ins (stabilityTerm Γ≡Δ u) (stabilityTerm Γ≡Δ t) x u~t
  symConv↓Term Γ≡Δ (univ x x₁ x₂) =
    univ (stabilityTerm Γ≡Δ x₁) (stabilityTerm Γ≡Δ x) (symConv↓ Γ≡Δ x₂)
  symConv↓Term Γ≡Δ (zero-refl x) =
    let _ , ⊢Δ , _ = contextConvSubst Γ≡Δ
    in  zero-refl ⊢Δ
  symConv↓Term Γ≡Δ (suc-cong t<>u) = suc-cong (symConv↑Term Γ≡Δ t<>u)
  symConv↓Term Γ≡Δ (η-eq x₁ x₂ y y₁ t<>u) =
    let ⊢F , _ = syntacticΠ (syntacticTerm x₁)
    in  η-eq (stabilityTerm Γ≡Δ x₂) (stabilityTerm Γ≡Δ x₁)
             y₁ y (symConv↑Term (Γ≡Δ ∙ refl ⊢F) t<>u)
  symConv↓Term Γ≡Δ (Σ-η ⊢p ⊢r pProd rProd fstConv sndConv) =
    let Δ⊢p = stabilityTerm Γ≡Δ ⊢p
        Δ⊢r = stabilityTerm Γ≡Δ ⊢r
        ⊢G = proj₂ (syntacticΣ (syntacticTerm ⊢p))
        Δfst≡ = symConv↑Term Γ≡Δ fstConv
        Δsnd≡₁ = symConv↑Term Γ≡Δ sndConv
        ΔGfstt≡Gfstu = stabilityEq Γ≡Δ (substTypeEq (refl ⊢G)
                                                    (soundnessConv↑Term fstConv))
        Δsnd≡ = convConvTerm Δsnd≡₁ ΔGfstt≡Gfstu
    in  Σ-η Δ⊢r Δ⊢p rProd pProd Δfst≡ Δsnd≡
  symConv↓Term Γ≡Δ (η-unit [t] [u] tUnit uUnit) =
    let [t] = stabilityTerm Γ≡Δ [t]
        [u] = stabilityTerm Γ≡Δ [u]
    in  (η-unit [u] [t] uUnit tUnit)

symConv↓Term′ : ∀ {t u A Γ} → Γ ⊢ t [conv↓] u ∷ A → Γ ⊢ u [conv↓] t ∷ A
symConv↓Term′ tConvU =
  symConv↓Term (reflConEq (wfEqTerm (soundnessConv↓Term tConvU))) tConvU

-- Symmetry of algorithmic equality of types with preserved context.
symConv : ∀ {A B Γ} → Γ ⊢ A [conv↑] B → Γ ⊢ B [conv↑] A
symConv A<>B =
  let ⊢Γ = wfEq (soundnessConv↑ A<>B)
  in  symConv↑ (reflConEq ⊢Γ) A<>B

-- Symmetry of algorithmic equality of terms with preserved context.
symConvTerm : ∀ {t u A Γ} → Γ ⊢ t [conv↑] u ∷ A → Γ ⊢ u [conv↑] t ∷ A
symConvTerm t<>u =
  let ⊢Γ = wfEqTerm (soundnessConv↑Term t<>u)
  in  symConv↑Term (reflConEq ⊢Γ) t<>u


text:
module Haskell.Prim.Maybe where

open import Agda.Builtin.List public

open import Haskell.Prim
open import Haskell.Prim.List

--------------------------------------------------
-- Maybe

data Maybe {ℓ} (a : Set ℓ) : Set ℓ where
  Nothing : Maybe a
  Just    : a -> Maybe a

maybe : ∀ {ℓ₁ ℓ₂} {a : Set ℓ₁} {b : Set ℓ₂} → b → (a → b) → Maybe a → b
maybe n j Nothing  = n
maybe n j (Just x) = j x

mapMaybe : (a -> Maybe b) -> List a -> List b
mapMaybe _ [] = []
mapMaybe f (x ∷ xs) =
  case f x of λ where
    Nothing -> mapMaybe f xs
    (Just v) -> v ∷ (mapMaybe f xs)


text:
module Nats where

open import Agda.Builtin.Nat public
  renaming (Nat to ℕ; _-_ to _∸_)


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- An inductive definition of the sublist relation with respect to a
-- setoid. This is a generalisation of what is commonly known as Order
-- Preserving Embeddings (OPE).
------------------------------------------------------------------------

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

open import Relation.Binary using (Setoid; Rel)

module Data.List.Relation.Binary.Sublist.Setoid
  {c ℓ} (S : Setoid c ℓ) where

open import Level using (_⊔_)

open import Data.List.Base using (List; []; _∷_)
import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
import Data.List.Relation.Binary.Sublist.Heterogeneous as Heterogeneous
import Data.List.Relation.Binary.Sublist.Heterogeneous.Core
  as HeterogeneousCore
import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
  as HeterogeneousProperties
open import Data.Product using (∃; ∃₂; _,_; proj₂)

open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary using (¬_; Dec; yes; no)

open Setoid S renaming (Carrier to A)
open SetoidEquality S

------------------------------------------------------------------------
-- Definition

infix 4 _⊆_ _⊇_ _⊈_ _⊉_

_⊆_ : Rel (List A) (c ⊔ ℓ)
_⊆_ = Heterogeneous.Sublist _≈_

_⊇_ : Rel (List A) (c ⊔ ℓ)
xs ⊇ ys = ys ⊆ xs

_⊈_ : Rel (List A) (c ⊔ ℓ)
xs ⊈ ys = ¬ (xs ⊆ ys)

_⊉_ : Rel (List A) (c ⊔ ℓ)
xs ⊉ ys = ¬ (xs ⊇ ys)

------------------------------------------------------------------------
-- Re-export definitions and operations from heterogeneous sublists

open HeterogeneousCore _≈_ using ([]; _∷_; _∷ʳ_) public
open Heterogeneous {R = _≈_} hiding (Sublist; []; _∷_; _∷ʳ_) public
  renaming
  (toAny to to∈; fromAny to from∈)

open Disjoint      public using ([])
open DisjointUnion public using ([])

------------------------------------------------------------------------
-- Relational properties holding for Setoid case

⊆-reflexive : _≋_ ⇒ _⊆_
⊆-reflexive = HeterogeneousProperties.fromPointwise

open HeterogeneousProperties.Reflexivity {R = _≈_} refl public using ()
  renaming (refl to ⊆-refl)  -- ⊆-refl : Reflexive _⊆_

open HeterogeneousProperties.Transitivity {R = _≈_} {S = _≈_} {T = _≈_} trans public using ()
  renaming (trans to ⊆-trans)  -- ⊆-trans : Transitive _⊆_

open HeterogeneousProperties.Antisymmetry {R = _≈_} {S = _≈_} (λ x≈y _ → x≈y) public using ()
  renaming (antisym to ⊆-antisym)  -- ⊆-antisym : Antisymmetric _≋_ _⊆_

⊆-isPreorder : IsPreorder _≋_ _⊆_
⊆-isPreorder = record
  { isEquivalence = ≋-isEquivalence
  ; reflexive     = ⊆-reflexive
  ; trans         = ⊆-trans
  }

⊆-isPartialOrder : IsPartialOrder _≋_ _⊆_
⊆-isPartialOrder = record
  { isPreorder = ⊆-isPreorder
  ; antisym    = ⊆-antisym
  }

⊆-preorder : Preorder c (c ⊔ ℓ) (c ⊔ ℓ)
⊆-preorder = record
  { isPreorder = ⊆-isPreorder
  }

⊆-poset : Poset c (c ⊔ ℓ) (c ⊔ ℓ)
⊆-poset = record
  { isPartialOrder = ⊆-isPartialOrder
  }

------------------------------------------------------------------------
-- Raw pushout
--
-- The category _⊆_ does not have proper pushouts.  For instance consider:
--
--   τᵤ : [] ⊆ (u ∷ [])
--   τᵥ : [] ⊆ (v ∷ [])
--
-- Then, there are two unrelated upper bounds (u ∷ v ∷ []) and (v ∷ u ∷ []),
-- since _⊆_ does not include permutations.
--
-- Even though there are no unique least upper bounds, we can merge two
-- extensions of a list, producing a minimial superlist of both.
--
-- For the example, the left-biased merge would produce the pair:
--
--   τᵤ′ : (u ∷ []) ⊆ (u ∷ v ∷ [])
--   τᵥ′ : (v ∷ []) ⊆ (u ∷ v ∷ [])
--
-- We call such a pair a raw pushout.  It is then a weak pushout if the
-- resulting square commutes, i.e.:
--
--   ⊆-trans τᵤ τᵤ′ ~ ⊆-trans τᵥ τᵥ′
--
-- This requires a notion of equality _~_ on sublist morphisms.
--
-- Further, commutation requires a similar commutation property
-- for the underlying equality _≈_, namely
--
--   trans x≈y (sym x≈y) == trans x≈z (sym x≈z)
--
-- for some notion of equality _==_ for equality proofs _≈_.
-- Such a property is given e.g. if _≈_ is proof irrelevant
-- or forms a groupoid.

record RawPushout {xs ys zs : List A} (τ : xs ⊆ ys) (σ : xs ⊆ zs) : Set (c ⊔ ℓ) where
  field
    {upperBound} : List A
    leg₁         : ys ⊆ upperBound
    leg₂         : zs ⊆ upperBound

open RawPushout

------------------------------------------------------------------------
-- Extending corners of a raw pushout square

-- Extending the right upper corner.

infixr 5 _∷ʳ₁_ _∷ʳ₂_

_∷ʳ₁_ : ∀ {xs ys zs : List A} {τ : xs ⊆ ys} {σ : xs ⊆ zs} →
        (y : A) → RawPushout τ σ → RawPushout (y ∷ʳ τ) σ
y ∷ʳ₁ rpo = record
  { leg₁ = refl ∷ leg₁ rpo
  ; leg₂ = y   ∷ʳ leg₂ rpo
  }

-- Extending the left lower corner.

_∷ʳ₂_ : ∀ {xs ys zs : List A} {τ : xs ⊆ ys} {σ : xs ⊆ zs} →
        (z : A) → RawPushout τ σ → RawPushout τ (z ∷ʳ σ)
z ∷ʳ₂ rpo = record
  { leg₁ = z   ∷ʳ leg₁ rpo
  ; leg₂ = refl ∷ leg₂ rpo
  }

-- Extending both of these corners with equal elements.

∷-rpo : ∀ {x y z : A} {xs ys zs : List A} {τ : xs ⊆ ys} {σ : xs ⊆ zs} →
        (x≈y : x ≈ y) (x≈z : x ≈ z) → RawPushout τ σ → RawPushout (x≈y ∷ τ) (x≈z ∷ σ)
∷-rpo x≈y x≈z rpo = record
  { leg₁ = sym x≈y ∷ leg₁ rpo
  ; leg₂ = sym x≈z ∷ leg₂ rpo
  }

------------------------------------------------------------------------
-- Left-biased pushout: add elements of left extension first.

⊆-pushoutˡ : ∀ {xs ys zs : List A} →
             (τ : xs ⊆ ys) (σ : xs ⊆ zs) → RawPushout τ σ
⊆-pushoutˡ []        σ         = record { leg₁ = σ ; leg₂ = ⊆-refl }
⊆-pushoutˡ (y  ∷ʳ τ) σ         = y ∷ʳ₁ ⊆-pushoutˡ τ σ
⊆-pushoutˡ τ@(_ ∷ _) (z  ∷ʳ σ) = z ∷ʳ₂ ⊆-pushoutˡ τ σ
⊆-pushoutˡ (x≈y ∷ τ) (x≈z ∷ σ) = ∷-rpo x≈y x≈z (⊆-pushoutˡ τ σ)

-- Join two extensions, returning the upper bound and the diagonal
-- of the pushout square.

⊆-joinˡ : ∀ {xs ys zs : List A} →
          (τ : xs ⊆ ys) (σ : xs ⊆ zs) → ∃ λ us → xs ⊆ us
⊆-joinˡ τ σ = upperBound rpo , ⊆-trans τ (leg₁ rpo)
  where
  rpo = ⊆-pushoutˡ τ σ

------------------------------------------------------------------------
-- Upper bound of two sublists xs,ys ⊆ zs

record UpperBound {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) : Set (c ⊔ ℓ) where
  field
    {theUpperBound} : List A
    sub  : theUpperBound ⊆ zs
    inj₁ : xs ⊆ theUpperBound
    inj₂ : ys ⊆ theUpperBound

open UpperBound

infixr 5 _∷ₗ-ub_ _∷ᵣ-ub_

∷ₙ-ub : ∀ {xs ys zs} {τ : xs ⊆ zs} {σ : ys ⊆ zs} {x} →
        UpperBound τ σ → UpperBound (x ∷ʳ τ) (x ∷ʳ σ)
∷ₙ-ub u = record
  { sub  = _ ∷ʳ u .sub
  ; inj₁ = u .inj₁
  ; inj₂ = u .inj₂
  }

_∷ₗ-ub_ : ∀ {xs ys zs} {τ : xs ⊆ zs} {σ : ys ⊆ zs} {x y} →
         (x≈y : x ≈ y) → UpperBound τ σ → UpperBound (x≈y ∷ τ) (y ∷ʳ σ)
x≈y ∷ₗ-ub u = record
  { sub = refl ∷ u .sub
  ; inj₁ = x≈y ∷ u .inj₁
  ; inj₂ = _  ∷ʳ u .inj₂
  }

_∷ᵣ-ub_ : ∀ {xs ys zs} {τ : xs ⊆ zs} {σ : ys ⊆ zs} {x y} →
         (x≈y : x ≈ y) → UpperBound τ σ → UpperBound (y ∷ʳ τ) (x≈y ∷ σ)
x≈y ∷ᵣ-ub u = record
  { sub  = refl ∷ u .sub
  ; inj₁ = _   ∷ʳ u .inj₁
  ; inj₂ = x≈y  ∷ u .inj₂
  }

------------------------------------------------------------------------
-- Disjoint union
--
-- Two non-overlapping sublists τ : xs ⊆ zs and σ : ys ⊆ zs
-- can be joined in a unique way if τ and σ are respected.
--
-- For instance, if τ : [x] ⊆ [x,y,x] and σ : [y] ⊆ [x,y,x]
-- then the union will be [x,y] or [y,x], depending on whether
-- τ picks the first x or the second one.
--
-- NB: If the content of τ and σ were ignored then the union would not
-- be unique.  Expressing uniqueness would require a notion of equality
-- of sublist proofs, which we do not (yet) have for the setoid case
-- (however, for the propositional case).

⊆-disjoint-union : ∀ {xs ys zs} {τ : xs ⊆ zs} {σ : ys ⊆ zs} →
                   Disjoint τ σ → UpperBound τ σ
⊆-disjoint-union []         = record { sub = [] ; inj₁ = [] ; inj₂ = [] }
⊆-disjoint-union (x   ∷ₙ d) = ∷ₙ-ub (⊆-disjoint-union d)
⊆-disjoint-union (x≈y ∷ₗ d) = x≈y ∷ₗ-ub (⊆-disjoint-union d)
⊆-disjoint-union (x≈y ∷ᵣ d) = x≈y ∷ᵣ-ub (⊆-disjoint-union d)


text:
module Issue2575.M where

A : Set
A = Set


text:
------------------------------------------------------------------------------
-- Testing subst using an implicit arguments for the propositional function.
------------------------------------------------------------------------------

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

module FOT.FOL.ImplicitArgumentSubst where

infix 7 _≡_

postulate
  D              : Set
  _·_            : D → D → D
  zero succ pred : D

succ₁ : D → D
succ₁ n = succ · n

pred₁ : D → D
pred₁ n = pred · n

-- The identity type on the universe of discourse.
data _≡_ (x : D) : D → Set where
  refl : x ≡ x

-- The propositional function is not an implicit argument.
subst : (A : D → Set) → ∀ {x y} → x ≡ y → A x → A y
subst A refl Ax = Ax

-- The propositional formula is an implicit argument.
subst' : {A : D → Set} → ∀ {x y} → x ≡ y → A x → A y
subst' refl Ax = Ax

sym : ∀ {x y} → x ≡ y → y ≡ x
sym refl = refl

-- Conversion rules.
postulate
  pred-0 : pred₁ zero            ≡ zero
  pred-S : ∀ n → pred₁ (succ₁ n) ≡ n

-- The FOTC natural numbers type.
data N : D → Set where
  nzero :               N zero
  nsucc : ∀ {n} → N n → N (succ₁ n)

-- Works using subst.
pred-N : ∀ {n} → N n → N (pred₁ n)
pred-N nzero          = subst N (sym pred-0) nzero
pred-N (nsucc {n} Nn) = subst N (sym (pred-S n)) Nn

-- Fails using subst'.
pred-N' : ∀ {n} → N n → N (pred₁ n)
pred-N' nzero          = subst' (sym pred-0) nzero
pred-N' (nsucc {n} Nn) = subst' (sym (pred-S n)) Nn

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- A variant of code reported by Andreas Abel.

-- Andreas, 2014-01-07 Issue reported by Dmitriy Traytel
-- Andreas, 2015-04-15 Issue resurrected with Pierre Hyvernat

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

open import Common.Size
open import Common.Prelude hiding (map)
open import Common.Product

record Stream (A : Set) : Set where
  coinductive
  field
    force : A × Stream A
open Stream

map :  ∀{A B} → (A → B) → Stream A → Stream B
force (map f s) = let  a , as = force s  in  f a , map f as

-- This type should be empty, as Stream A is isomorphic to ℕ → A.
data D : (i : Size) → Set where
  lim : ∀ i → Stream (D i) → D (↑ i)

-- Emptiness witness for D.
empty : ∀ i → D i → ⊥
empty .(↑ i) (lim i s) = empty i (proj₁ (force s))

-- BAD: But we can construct an inhabitant.
inh : Stream (D ∞)
force inh = lim ∞ inh , inh -- Should be rejected by termination checker.

absurd : ⊥
absurd = empty ∞ (lim ∞ inh)


text:
module Tactic.Reflection.Quote.Class where

open import Builtin.Reflection

record Quotable {a} (A : Set a) : Set a where
  field
    ` : A → Term

open Quotable {{...}} public

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:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some properties imply others
------------------------------------------------------------------------

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

module Relation.Binary.Consequences where

open import Relation.Binary.Core
open import Relation.Nullary using (yes; no)
open import Relation.Unary using (∁)
open import Function using (_∘_; flip)
open import Data.Maybe.Base using (just; nothing)
open import Data.Sum using (inj₁; inj₂)
open import Data.Product using (_,_)
open import Data.Empty using (⊥-elim)

------------------------------------------------------------------------
-- Substitutive properties

module _ {a ℓ p} {A : Set a} {_∼_ : Rel A ℓ} (P : Rel A p) where

  subst⟶respˡ : Substitutive _∼_ p → P Respectsˡ _∼_
  subst⟶respˡ subst {y} x'∼x Px'y = subst (flip P y) x'∼x Px'y

  subst⟶respʳ : Substitutive _∼_ p → P Respectsʳ _∼_
  subst⟶respʳ subst {x} y'∼y Pxy' = subst (P x) y'∼y Pxy'

  subst⟶resp₂ : Substitutive _∼_ p → P Respects₂ _∼_
  subst⟶resp₂ subst = subst⟶respʳ subst , subst⟶respˡ subst

module _ {a ℓ p} {A : Set a} {∼ : Rel A ℓ} {P : A → Set p} where

  P-resp⟶¬P-resp : Symmetric ∼ → P Respects ∼ → (∁ P) Respects ∼
  P-resp⟶¬P-resp sym resp x∼y ¬Px Py = ¬Px (resp (sym x∼y) Py)

------------------------------------------------------------------------
-- Proofs for non-strict orders

module _ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} where

  total⟶refl : _≤_ Respects₂ _≈_ → Symmetric _≈_ →
                 Total _≤_ → _≈_ ⇒ _≤_
  total⟶refl (respʳ , respˡ) sym total {x} {y} x≈y with total x y
  ... | inj₁ x∼y = x∼y
  ... | inj₂ y∼x = respʳ x≈y (respˡ (sym x≈y) y∼x)

  total+dec⟶dec : _≈_ ⇒ _≤_ → Antisymmetric _≈_ _≤_ →
                    Total _≤_ → Decidable _≈_ → Decidable _≤_
  total+dec⟶dec refl antisym total _≟_ x y with total x y
  ... | inj₁ x≤y = yes x≤y
  ... | inj₂ y≤x with x ≟ y
  ...   | yes x≈y = yes (refl x≈y)
  ...   | no  x≉y = no (λ x≤y → x≉y (antisym x≤y y≤x))

------------------------------------------------------------------------
-- Proofs for strict orders

module _ {a ℓ₁ ℓ₂} {A : Set a} {_≈_ : Rel A ℓ₁} {_<_ : Rel A ℓ₂} where

  trans∧irr⟶asym : Reflexive _≈_ → Transitive _<_ →
                     Irreflexive _≈_ _<_ → Asymmetric _<_
  trans∧irr⟶asym refl trans irrefl x<y y<x =
    irrefl refl (trans x<y y<x)

  irr∧antisym⟶asym : Irreflexive _≈_ _<_ → Antisymmetric _≈_ _<_ →
                       Asymmetric _<_
  irr∧antisym⟶asym irrefl antisym x<y y<x =
    irrefl (antisym x<y y<x) x<y

  asym⟶antisym : Asymmetric _<_ → Antisymmetric _≈_ _<_
  asym⟶antisym asym x<y y<x = ⊥-elim (asym x<y y<x)

  asym⟶irr : _<_ Respects₂ _≈_ → Symmetric _≈_ →
               Asymmetric _<_ → Irreflexive _≈_ _<_
  asym⟶irr (respʳ , respˡ) sym asym {x} {y} x≈y x<y =
    asym x<y (respʳ (sym x≈y) (respˡ x≈y x<y))

  tri⟶asym : Trichotomous _≈_ _<_ → Asymmetric _<_
  tri⟶asym tri {x} {y} x<y x>y with tri x y
  ... | tri< _   _ x≯y = x≯y x>y
  ... | tri≈ _   _ x≯y = x≯y x>y
  ... | tri> x≮y _ _   = x≮y x<y

  tri⟶irr : Trichotomous _≈_ _<_ → Irreflexive _≈_ _<_
  tri⟶irr compare {x} {y} x≈y x<y with compare x y
  ... | tri< _   x≉y y≮x = x≉y x≈y
  ... | tri> x≮y x≉y y<x = x≉y x≈y
  ... | tri≈ x≮y _   y≮x = x≮y x<y

  tri⟶dec≈ : Trichotomous _≈_ _<_ → Decidable _≈_
  tri⟶dec≈ compare x y with compare x y
  ... | tri< _ x≉y _ = no  x≉y
  ... | tri≈ _ x≈y _ = yes x≈y
  ... | tri> _ x≉y _ = no  x≉y

  tri⟶dec< : Trichotomous _≈_ _<_ → Decidable _<_
  tri⟶dec< compare x y with compare x y
  ... | tri< x<y _ _ = yes x<y
  ... | tri≈ x≮y _ _ = no  x≮y
  ... | tri> x≮y _ _ = no  x≮y

  trans∧tri⟶respʳ≈ : Symmetric _≈_ → Transitive _≈_ →
                       Transitive _<_ → Trichotomous _≈_ _<_ →
                       _<_ Respectsʳ _≈_
  trans∧tri⟶respʳ≈ sym ≈-tr <-tr tri {x} {y} {z} y≈z x<y with tri x z
  ... | tri< x<z _ _ = x<z
  ... | tri≈ _ x≈z _ = ⊥-elim (tri⟶irr tri (≈-tr x≈z (sym y≈z)) x<y)
  ... | tri> _ _ z<x = ⊥-elim (tri⟶irr tri (sym y≈z) (<-tr z<x x<y))

  trans∧tri⟶respˡ≈ : Transitive _≈_ →
                       Transitive _<_ → Trichotomous _≈_ _<_ →
                       _<_ Respectsˡ _≈_
  trans∧tri⟶respˡ≈ ≈-tr <-tr tri {z} {_} {y} x≈y x<z with tri y z
  ... | tri< y<z _ _ = y<z
  ... | tri≈ _ y≈z _ = ⊥-elim (tri⟶irr tri (≈-tr x≈y y≈z) x<z)
  ... | tri> _ _ z<y = ⊥-elim (tri⟶irr tri x≈y (<-tr x<z z<y))

  trans∧tri⟶resp≈ : Symmetric _≈_ → Transitive _≈_ →
                      Transitive _<_ → Trichotomous _≈_ _<_ →
                      _<_ Respects₂ _≈_
  trans∧tri⟶resp≈ sym ≈-tr <-tr tri =
    trans∧tri⟶respʳ≈ sym ≈-tr <-tr tri ,
    trans∧tri⟶respˡ≈ ≈-tr <-tr tri

------------------------------------------------------------------------
-- Without Loss of Generality

module _ {a r q} {A : Set a} {_R_ : Rel A r} {Q : Rel A q} where

  wlog : Total _R_ → Symmetric Q →
         (∀ a b → a R b → Q a b) →
         ∀ a b → Q a b
  wlog r-total q-sym prf a b with r-total a b
  ... | inj₁ aRb = prf a b aRb
  ... | inj₂ bRa = q-sym (prf b a bRa)

------------------------------------------------------------------------
-- Other proofs

module _ {a b p} {A : Set a} {B : Set b} {P : REL A B p} where

  dec⟶weaklyDec : Decidable P → WeaklyDecidable P
  dec⟶weaklyDec dec x y with dec x y
  ... | yes p = just p
  ... | no _ = nothing

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

  map-NonEmpty : P ⇒ Q → NonEmpty P → NonEmpty Q
  map-NonEmpty f x = nonEmpty (f (NonEmpty.proof x))


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

-- Backwards evaluator and the fact that with eval, forms a reversible evaluator

module BackwardsEval where

open import Data.Unit using (tt)
open import Data.Sum using (inj₁; inj₂)
open import Data.Product using (_,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans; cong; cong₂; subst)

open import Singleton
open import PiFrac

bwd : {A B : 𝕌} → (A ⟷ B) → ⟦ B ⟧ → ⟦ A ⟧
bwd-eval : {A B : 𝕌} → (c : A ⟷ B) → (v : ⟦ A ⟧) → bwd c (eval c v) ≡ v

bwd unite₊l v = inj₂ v
bwd uniti₊l (inj₂ v) = v
bwd unite₊r v = inj₁ v
bwd uniti₊r (inj₁ v) = v
bwd swap₊ (inj₁ v) = inj₂ v
bwd swap₊ (inj₂ v) = inj₁ v
bwd assocl₊ (inj₁ (inj₁ v)) = inj₁ v
bwd assocl₊ (inj₁ (inj₂ v)) = inj₂ (inj₁ v)
bwd assocl₊ (inj₂ v) = inj₂ (inj₂ v)
bwd assocr₊ (inj₁ v) = inj₁ (inj₁ v)
bwd assocr₊ (inj₂ (inj₁ v)) = inj₁ (inj₂ v)
bwd assocr₊ (inj₂ (inj₂ v)) = inj₂ v
bwd unite⋆l v = (tt , v)
bwd uniti⋆l (tt , v) = v
bwd unite⋆r v = (v , tt)
bwd uniti⋆r (v , tt) = v
bwd swap⋆ (v₁ , v₂) = (v₂ , v₁)
bwd assocl⋆ ((v₁ , v₂) , v₃) = (v₁ , (v₂ , v₃))
bwd assocr⋆ (v₁ , (v₂ , v₃)) = ((v₁ , v₂) , v₃)
bwd dist (inj₁ (v₁ , v₂)) = (inj₁ v₁ , v₂)
bwd dist (inj₂ (v₂ , v₃)) = (inj₂ v₂ , v₃)
bwd factor (inj₁ v₁ , v₃) = inj₁ (v₁ , v₃)
bwd factor (inj₂ v₂ , v₃) = inj₂ (v₂ , v₃)
bwd distl (inj₁ (v₁ , v₂)) = (v₁ , inj₁ v₂)
bwd distl (inj₂ (v₁ , v₃)) = (v₁ , inj₂ v₃)
bwd factorl (v₁ , inj₁ v₂) = inj₁ (v₁ , v₂)
bwd factorl (v₁ , inj₂ v₃) = inj₂ (v₁ , v₃)
bwd id⟷ v = v
bwd (c₁ ⊚ c₂) v = bwd c₁ (bwd c₂ v)
bwd (c₁ ⊕ c₂) (inj₁ v) = inj₁ (bwd c₁ v)
bwd (c₁ ⊕ c₂) (inj₂ v) = inj₂ (bwd c₂ v)
bwd (c₁ ⊗ c₂) (v₁ , v₂) = (bwd c₁ v₁ , bwd c₂ v₂)
bwd (lift {_} {_} {v₁} c) (●₁ , v≡●₁) = (bwd c ●₁) , (trans (sym (bwd-eval c v₁)) (cong (bwd c) v≡●₁))
bwd tensorl ((w₁ , p₁) , (w₂ , p₂)) = (w₁ ,  w₂) , (cong₂ _,_ p₁ p₂)
bwd tensorr ((v₁ , v₂) , p) = (v₁ , cong proj₁ p) , (v₂ , cong proj₂ p)
bwd plusll (w , p) = (inj₁ w) , (cong inj₁ p)
bwd pluslr (inj₁ w₁ , refl) = w₁ , refl
bwd plusrl (w , p) = (inj₂ w) , (cong inj₂ p)
bwd plusrr (inj₂ w₂ , refl) = w₂ , refl
bwd fracl (f₁ , f₂) ((w₁ , w₂) , refl) = let _ = f₁ (w₁ , refl) ; _ = f₂ (w₂ , refl) in tt
bwd (fracr {v₁ = v₁} {v₂ = v₂}) f = (λ _ → f ((v₁ , v₂) , refl)) , (λ _ → f ((v₁ , v₂) , refl))
bwd (η v) p = tt
bwd (ε v) tt = (v , refl) , λ _ → tt
bwd (ll {t} {v} {w}) (v , refl) = w , refl
bwd (== c eq) v = bwd c (subst (Singleton ⟦ _ ⟧) (sym eq) v)

bwd-eval unite₊l (inj₂ v) = refl
bwd-eval uniti₊l v = refl
bwd-eval unite₊r (inj₁ v) = refl
bwd-eval uniti₊r v = refl
bwd-eval swap₊ (inj₁ v) = refl
bwd-eval swap₊ (inj₂ v) = refl
bwd-eval assocl₊ (inj₁ v) = refl
bwd-eval assocl₊ (inj₂ (inj₁ v)) = refl
bwd-eval assocl₊ (inj₂ (inj₂ v)) = refl
bwd-eval assocr₊ (inj₁ (inj₁ v)) = refl
bwd-eval assocr₊ (inj₁ (inj₂ v)) = refl
bwd-eval assocr₊ (inj₂ v) = refl
bwd-eval unite⋆l (tt , v) = refl
bwd-eval uniti⋆l v = refl
bwd-eval unite⋆r (v , tt) = refl
bwd-eval uniti⋆r v = refl
bwd-eval swap⋆ (v₁ , v₂) = refl
bwd-eval assocl⋆ (v₁ , (v₂ , v₃)) = refl
bwd-eval assocr⋆ ((v₁ , v₂) , v₃) = refl
bwd-eval dist (inj₁ v₁ , v₃) = refl
bwd-eval dist (inj₂ v₂ , v₃) = refl
bwd-eval factor (inj₁ (v₁ , v₃)) = refl
bwd-eval factor (inj₂ (v₂ , v₃)) = refl
bwd-eval distl (v₁ , inj₁ v₂) = refl
bwd-eval distl (v₁ , inj₂ v₃) = refl
bwd-eval factorl (inj₁ (v₁ , v₂)) = refl
bwd-eval factorl (inj₂ (v₁ , v₃)) = refl
bwd-eval id⟷ v = refl
bwd-eval (c₁ ⊚ c₂) v = trans (cong (bwd c₁) (bwd-eval c₂ (eval c₁ v))) (bwd-eval c₁ v)
bwd-eval (c₁ ⊕ c₂) (inj₁ v₁) = cong inj₁ (bwd-eval c₁ v₁)
bwd-eval (c₁ ⊕ c₂) (inj₂ v₂) = cong inj₂ (bwd-eval c₂ v₂)
bwd-eval (c₁ ⊗ c₂) (v₁ , v₂) = cong₂ _,_ (bwd-eval c₁ v₁) (bwd-eval c₂ v₂)
bwd-eval (lift c) v = pointed-all-paths
bwd-eval tensorl p = pointed-all-paths
bwd-eval tensorr (p₁ , p₂) = cong₂ _,_ pointed-all-paths pointed-all-paths
bwd-eval plusll p = pointed-all-paths
bwd-eval pluslr p = pointed-all-paths
bwd-eval plusrl p = pointed-all-paths
bwd-eval plusrr p = pointed-all-paths
bwd-eval fracl f = {!!}  -- needs recip-all-paths
bwd-eval fracr (f₁ , f₂) = {!!}
bwd-eval (η v) tt = refl
bwd-eval (ε v) (p , r) = cong₂ _,_ pointed-all-paths refl
bwd-eval (ll {t} {v} {.w}) (w , refl) = refl
bwd-eval (== c eq) p = pointed-all-paths

eval-bwd : {A B : 𝕌} → (c : A ⟷ B) → (v : ⟦ B ⟧) → eval c (bwd c v) ≡ v
eval-bwd unite₊l v = refl
eval-bwd uniti₊l (inj₂ v) = refl
eval-bwd unite₊r v = refl
eval-bwd uniti₊r (inj₁ v) = refl
eval-bwd swap₊ (inj₁ v) = refl
eval-bwd swap₊ (inj₂ v) = refl
eval-bwd assocl₊ (inj₁ (inj₁ v)) = refl
eval-bwd assocl₊ (inj₁ (inj₂ v)) = refl
eval-bwd assocl₊ (inj₂ v) = refl
eval-bwd assocr₊ (inj₁ v) = refl
eval-bwd assocr₊ (inj₂ (inj₁ v)) = refl
eval-bwd assocr₊ (inj₂ (inj₂ v)) = refl
eval-bwd unite⋆l v = refl
eval-bwd uniti⋆l (tt , v) = refl
eval-bwd unite⋆r v = refl
eval-bwd uniti⋆r (v , tt) = refl
eval-bwd swap⋆ (v₂ , v₁) = refl
eval-bwd assocl⋆ ((v₁ , v₂) , v₃) = refl
eval-bwd assocr⋆ (v₁ , (v₂ , v₃)) = refl
eval-bwd dist (inj₁ (v₁ , v₂)) = refl
eval-bwd dist (inj₂ (v₂ , v₃)) = refl
eval-bwd factor (inj₁ v₁ , v₃) = refl
eval-bwd factor (inj₂ v₂ , v₃) = refl
eval-bwd distl (inj₁ (v₁ , v₂)) = refl
eval-bwd distl (inj₂ (v₁ , v₃)) = refl
eval-bwd factorl (v₁ , inj₁ v₂) = refl
eval-bwd factorl (v₁ , inj₂ v₃) = refl
eval-bwd id⟷ v = refl
eval-bwd (c₁ ⊚ c₂) v = trans (cong (eval c₂) (eval-bwd c₁ (bwd c₂ v))) (eval-bwd c₂ v)
eval-bwd (c₁ ⊕ c₂) (inj₁ v) = cong inj₁ (eval-bwd c₁ v)
eval-bwd (c₁ ⊕ c₂) (inj₂ v) = cong inj₂ (eval-bwd c₂ v)
eval-bwd (c₁ ⊗ c₂) (v₃ , v₄) = cong₂ _,_ (eval-bwd c₁ v₃) (eval-bwd c₂ v₄)
eval-bwd (lift c) x = pointed-all-paths
eval-bwd tensorl p = cong₂ _,_ pointed-all-paths pointed-all-paths
eval-bwd tensorr p = pointed-all-paths
eval-bwd plusll p = pointed-all-paths
eval-bwd pluslr p = pointed-all-paths
eval-bwd plusrl p = pointed-all-paths
eval-bwd plusrr p = pointed-all-paths
eval-bwd fracl (f₁ , f₂) = {!!} -- needs recip-all-paths
eval-bwd fracr f = {!!}
eval-bwd (η v) (p , r) = cong₂ _,_ pointed-all-paths refl
eval-bwd (ε v) tt = refl
eval-bwd (ll {t} {.v} {w}) (v , refl) = refl
eval-bwd (== c eq) p = pointed-all-paths

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Library.Data.Integer where

open import Light.Level using (Level ; Setω)
open import Light.Library.Data.Empty as Empty using (Empty)
open import Light.Library.Data.Natural as Natural using (ℕ)
open import Light.Subtyping using (DirectSubtyping ; #_)
open import Light.Library.Arithmetic using (Arithmetic)
open import Light.Package using (Package)
open import Light.Library.Relation.Binary
      using (SelfTransitive ; SelfSymmetric ; Reflexive)
open import Light.Library.Relation.Binary.Equality as ≈ using (_≈_)
open import Light.Library.Relation.Binary.Equality.Decidable using (DecidableSelfEquality)
import Light.Library.Relation.Decidable

record Dependencies : Setω where
      field ⦃ natural‐package ⦄ : Package record { Natural }

record Library (dependencies : Dependencies) : Setω where
      field
            ℓ ≈ℓ : Level
            ℤ : Set ℓ
            zero : ℤ
            successor : ℤ → ℤ
            predecessor : ℤ → ℤ
            _+_ : ℤ → ℤ → ℤ
            _∗_ : ℤ → ℤ → ℤ
            _//_ : ℤ → ℤ → ℤ
            _−_ : ℤ → ℤ → ℤ
            −_ : ℤ → ℤ
            from‐natural : ℕ → ℤ
            ⦃ equals ⦄ : DecidableSelfEquality ℤ
            ⦃ ≈‐transitive ⦄ : SelfTransitive (≈.self‐relation ℤ)
            ⦃ ≈‐symmetric ⦄ : SelfSymmetric (≈.self‐relation ℤ)
            ⦃ ≈‐reflexive ⦄ : Reflexive (≈.self‐relation ℤ)

      instance naturals‐are‐integers : DirectSubtyping ℕ ℤ
      naturals‐are‐integers = # from‐natural

      instance arithmetic : Arithmetic ℤ
      arithmetic = record { _+_ = _+_ ; _∗_ = _∗_ }

open Library ⦃ ... ⦄ public

max_stars_repo_name: zamfofex/lightlib

max_issues_repo_name: Zambonifofex/lightlib

max_forks_repo_name: Zambonifofex/lightlib


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

open import Algebra

module Quasigroup.Properties
  {a ℓ} (Q : Quasigroup a ℓ) where

open Quasigroup Q


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Magma.Construct.Empty where

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude
open import Cubical.Algebra.Magma

open import Cubical.Data.Empty

_◯_ : Op₂ ⊥
_◯_ ()

isSet⊥ : isSet ⊥
isSet⊥ = isProp→isSet isProp⊥

⊥-isMagma : IsMagma ⊥ _◯_
⊥-isMagma = record { is-set = isSet⊥ }

⊥-Magma : Magma ℓ-zero
⊥-Magma = record { isMagma = ⊥-isMagma }


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bundles of parameters for passing to the Ring Solver
------------------------------------------------------------------------

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

-- This module packages up all the stuff that's passed to the other
-- modules in a convenient form.

module Tactic.RingSolver.Core.Polynomial.Parameters where

open import Algebra.Bundles using (RawRing)
open import Data.Bool.Base using (Bool; T)
open import Function
open import Level
open import Relation.Unary
open import Tactic.RingSolver.Core.AlmostCommutativeRing

-- This record stores all the stuff we need for the coefficients:
--
--  * A raw ring
--  * A (decidable) predicate on "zeroeness"
--
-- It's used for defining the operations on the Horner normal form.
record RawCoeff ℓ₁ ℓ₂ : Set (suc (ℓ₁ ⊔ ℓ₂)) where
  field
    rawRing : RawRing ℓ₁ ℓ₂
    isZero  : RawRing.Carrier rawRing → Bool

  open RawRing rawRing public

-- This record stores the full information we need for converting
-- to the final ring.
record Homomorphism ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Set (suc (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)) where
  field
    from : RawCoeff ℓ₁ ℓ₂
    to   : AlmostCommutativeRing ℓ₃ ℓ₄

  module Raw = RawCoeff from
  open AlmostCommutativeRing to public

  field
    morphism : Raw.rawRing -Raw-AlmostCommutative⟶ to
  open _-Raw-AlmostCommutative⟶_ morphism renaming (⟦_⟧ to ⟦_⟧ᵣ) public
  field
    Zero-C⟶Zero-R : ∀ x → T (Raw.isZero x) → 0# ≈  ⟦ x ⟧ᵣ


text:
{-# OPTIONS --omega-in-omega --no-termination-check --overlapping-instances #-}

module Light.Implementation.Data.Either where

open import Light.Library.Data.Either using (Library ; Dependencies)
open import Light.Level using (_⊔_)
open import Light.Variable.Levels

instance dependencies : Dependencies
dependencies = record {}

instance library : Library dependencies
library = record { Implementation }
      where
      module Implementation where
            ℓf : _
            ℓf = _⊔_
            data Either (𝕒 : Set aℓ) (𝕓 : Set bℓ) : Set (aℓ ⊔ bℓ) where
                  left : 𝕒 → Either 𝕒 𝕓
                  right : 𝕓 → Either 𝕒 𝕓


text:
module irreflexive where

open import Data.Nat using (ℕ; zero; suc)

open import Negation using (¬_)

infix 4 _<_
data _<_ : ℕ → ℕ → Set where
  z<s : ∀ {n : ℕ}
      ------------
    → zero < suc n

  s<s : ∀ {m n : ℕ}
    → m < n
      -------------
    → suc m < suc n

-- n が非反射律 ∀ n ∈ ℕ, ¬(n < n) を満たすことの証明
<-irreflexive : ∀ (n : ℕ) → ¬ (n < n)
<-irreflexive zero ()
<-irreflexive (suc n) (s<s n<n) = <-irreflexive n n<n

max_stars_repo_name: akiomik/plfa-solutions

max_issues_repo_name: akiomik/plfa-solutions

max_forks_repo_name: akiomik/plfa-solutions


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

module Identity where

open import Basic_Types

-- ------------------------------------
-- the identity type, or path type
infix  1 _≡_

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ (a : A) → a ≡ a

{-# BUILTIN EQUALITY _≡_ #-}

-- path induction
p-ind : ∀ {A : Set} {B : ∀ (x y : A) (p : x ≡ y) → Set} →
       (∀ (z : A) → B z z (refl z)) → ∀ (x y : A) (p : x ≡ y) → B x y p
p-ind f z z (refl z) = f z
-- notice here that, in the proof system of agda, the induction principle is
-- builtin for a data type, for their constructor is given expicitly. Hence,
-- one way to prove identity type is to use p-ind, which is itself proved by
-- agda using implicit path induction, or we can use agda's induction expicitly
-- which is the case when we construct apd and ass-p

-- the groupoid structure of path type
concat : ∀ {A : Set} → ∀ (x y : A) (p : x ≡ y) → ∀ (z : A) (q : y ≡ z) → x ≡ z
concat {A} x x (refl x) x (refl x) = refl x

infix  3 _∙_
_∙_ : ∀ {A : Set} {x y z : A} → ∀ (p : x ≡ y) (q : y ≡ z) → x ≡ z
_∙_ {_} {x} {y} {z} p q = concat x y p z q

inv : ∀ {A : Set} {x y : A} → ∀ (p : x ≡ y) → y ≡ x
inv {_} {x} {x} (refl x) = refl x

-- the groupoid structure of identities, viewed as higher paths
p-ass : ∀ {A : Set} {x y z w : A} → ∀ (p : x ≡ y) (q : y ≡ z) (r : z ≡ w) →
        p ∙ (q ∙ r) ≡ (p ∙ q) ∙ r
p-ass {_} {x} {x} {x} {x} (refl x) (refl x) (refl x) =
      refl (((refl x) ∙ (refl x)) ∙ (refl x))

left_unit : ∀ {A : Set} {x y : A} → ∀ (p : x ≡ y) → (refl x) ∙ p ≡ p
left_unit {_} {x} {x} (refl x) = refl (refl x)

right_unit : ∀ {A : Set} {x y : A} → ∀ (p : x ≡ y) → p ∙ (refl y) ≡ p
right_unit {_} {x} {x} (refl x) = refl (refl x)

rinv-unit : ∀ {A : Set} {x y : A} → ∀ (p : x ≡ y) → (inv p) ∙ p ≡ refl y
rinv-unit {_} {x} {x} (refl x) = refl (refl x)

linv-unit : ∀ {A : Set} {x y : A} → ∀ (p : x ≡ y) → p ∙ (inv p) ≡ refl x
linv-unit {_} {x} {x} (refl x) = refl (refl x)

invinv : ∀ {A : Set} {x y : A} → ∀ (p : x ≡ y) → inv (inv p) ≡ p
invinv {_} {x} {x} (refl x) = refl (refl x)

-- ------------------------------------
-- loop spaces
Ω : ∀ {A : Set} (a : A) → Set
Ω {_} a = a ≡ a

-- commutativity on 2-dimensional loops
-- prove the commutativity by proving a general result in the groupoid
pwr : ∀ {A : Set} {a b c : A} {p q : a ≡ b} → ∀ (r : b ≡ c) → ∀ (α : p ≡ q) →
      p ∙ r ≡ q ∙ r
pwr {_} {_} {b} {b} {p} {p} (refl b) (refl p) = refl (p ∙ (refl b))

pwl : ∀ {A : Set} {a b c : A} {q r : b ≡ c} → ∀ (p : a ≡ b) → ∀ (β : q ≡ r) →
      p ∙ q ≡ p ∙ r
pwl {_} {_} {_} {_} {q} {q} p (refl q) = refl (p ∙ q)

_*_ : ∀ {A : Set} {a b c : A} {p q : a ≡ b} {r s : b ≡ c} →
      ∀ (α : p ≡ q) (β : r ≡ s) → p ∙ r ≡ q ∙ s
_*_ {_} {_} {_} {_} {p} {q} {r} {s} α β = α∙r ∙ q∙β
  where α∙r : p ∙ r ≡ q ∙ r
        α∙r = pwr r α
        q∙β : q ∙ r ≡ q ∙ s
        q∙β = pwl q β

_*'_ : ∀ {A : Set} {a b c : A} {p q : a ≡ b} {r s : b ≡ c} →
       ∀ (α : p ≡ q) (β : r ≡ s) → p ∙ r ≡ q ∙ s
_*'_ {_} {_} {_} {_} {p} {q} {r} {s} α β = p∙β ∙ α∙s
  where p∙β : p ∙ r ≡ p ∙ s
        p∙β = pwl p β
        α∙s : p ∙ s ≡ q ∙ s
        α∙s = pwr s α

pwr-ru : ∀ {A : Set} {a : A} (p : a ≡ a) (α : refl a ≡ p) →
         pwr (refl a) α ≡ α ∙ (inv (right_unit p))
pwr-ru {_} {_} (refl a) (refl (refl a)) = refl (refl (refl a))

pwl-lu : ∀ {A : Set} {a : A} (p : a ≡ a) (α : refl a ≡ p) →
         pwl (refl a) α ≡ α ∙ (inv (left_unit p))
pwl-lu {_} {_} (refl a) (refl (refl a)) = refl (refl (refl a))

*≡*' : ∀ {A : Set} {a b c : A} {p q : a ≡ b} {r s : b ≡ c} →
       ∀ (α : p ≡ q) (β : r ≡ s) → (α * β) ≡ (α *' β)
*≡*' {_} {a} {a} {a} {refl a} {refl a} {refl a} {refl a}
     (refl (refl a)) (refl (refl a))
     = refl ((refl ((refl a) ∙ (refl a))) ∙ (refl ((refl a) ∙ (refl a))))

∙≡* : ∀ {A : Set} {a : A} → ∀ (α β : Ω (refl a)) → α ∙ β ≡ α * β
∙≡* {_} {a} α β = inv (redua)
  where redul : α * β ≡ α ∙ (pwl (refl a) β)
        redul = (pwr (pwl (refl a) β) (pwr-ru (refl a) α)) ∙
                (pwr (pwl (refl a) β) (right_unit α))
        redua : α * β ≡ α ∙ β
        redua = (redul ∙ (pwl α (pwl-lu (refl a) β))) ∙ (pwl α (right_unit β))

*'≡∙ : ∀ {A : Set} {a : A} → ∀ (α β : Ω (refl a)) → α *' β ≡ β ∙ α
*'≡∙ {_} {a} α β = redua'
  where redul' : α *' β ≡ β ∙ (pwr (refl a) α)
        redul' = (pwr (pwr (refl a) α) (pwl-lu (refl a) β)) ∙
                 (pwr (pwr (refl a) α) (right_unit β))
        redua' : α *' β ≡ β ∙ α
        redua' = redul' ∙ ((pwl β (pwr-ru (refl a) α)) ∙ (pwl β (right_unit α)))

-- finally, we are able to prove that the higher path group is commutative
Ω²-comm : ∀ {A : Set} {a : A} → ∀ (α β : Ω (refl a)) → α ∙ β ≡ β ∙ α
Ω²-comm α β = ((∙≡* α β) ∙ (*≡*' α β)) ∙ (*'≡∙ α β)

-- ------------------------------------
-- functions behave functorially
-- the action on paths
ap : ∀ {A B : Set} {x y : A} → ∀ (f : A → B) (p : x ≡ y) → f x ≡ f y
ap {_} {_} {x} {x} f (refl x) = refl (f x)

-- ap acts like a functor
ap∙ : ∀ {A B : Set} {x y z : A} → ∀ (f : A → B) (p : x ≡ y) (q : y ≡ z) →
      ap f (p ∙ q) ≡ (ap f p) ∙ (ap f q)
ap∙ {_} {_} {x} {x} {x} f (refl x) (refl x) = inv (left_unit (refl (f x)))

apinv : ∀ {A B : Set} {x y : A} → ∀ (f : A → B) (p : x ≡ y) →
        ap f (inv p) ≡ inv (ap f p)
apinv {_} {_} {x} {x} f (refl x) = refl (refl (f x))

apcomp : ∀ {A B C : Set} {x y : A} → ∀ (f : A → B) (g : B → C) (p : x ≡ y) →
         ap g (ap f p) ≡ ap (comp g f) p
apcomp {_} {_} {_} {x} {x} f g (refl x) = refl (refl (g (f x)))

apid : ∀ {A : Set} {x y : A} → ∀ (p : x ≡ y) →
       ap id p ≡ p
apid {_} {x} {x} (refl x) = refl (refl x)

-- the transport action, which is action on dependent types
tr : ∀ {A : Set} {B : A → Set} → ∀ {x y : A} → ∀ (p : x ≡ y) → B x → B y
tr {A} {B} {x} {x} (refl x) = id

<<<<<<< HEAD
=======
trc : ∀ {A B : Set} {x y : A} (p : x ≡ y) (b : B) → tr {A} {λ x → B} p b ≡ b
trc {_} {_} {x} {x} (refl x) b = refl b
>>>>>>> a0dc66dca08059f740d9290f3d1cad1bb007d721
-- If you think about this, this is not obvious from a classical point of view.
-- The existence of the transport function tells us that the dependent type
-- B : A → Set is always going to be continuous, since whenever we have a path
-- in the base A from x to y, and whenever we're given a point in B x, we can
-- construct a value in B y, using the path in the base.

-- path lifting
lift : ∀ {A : Set} {B : A → Set} → ∀ {x y : A} → ∀ (p : x ≡ y) → ∀ (b : B x) →
       (x , b) ≡ y , (tr {A} {B} p b)
lift {A} {B} {x} {x} (refl x) b = refl (x , b)

-- the dependent mapping functor
<<<<<<< HEAD
apd : ∀ {A : Set} {B : A → Set} {x y : A} → ∀ (f : (∀ (a : A) → B a)) →
      ∀ (p : x ≡ y) → tr {A} {B} {x} {y} p (f x) ≡ f y
apd {A} {B} {x} {x} f (refl x) = refl (tr {A} {B} {x} {x} (refl x) (f x))

-- the dependent and non-dependent ap(d) is closely related
trc : ∀ {A B : Set} {x y : A} (p : x ≡ y) (b : B) → tr {A} {λ x → B} p b ≡ b
trc {_} {_} {x} {x} (refl x) b = refl b

-- and now we can prove the following:
apd≡ap : ∀ {A B : Set} {x y : A} →
         ∀ (f : A → B) (p : x ≡ y) → apd f p ≡ trc p (f x) ∙ (ap f p)
apd≡ap {_} {_} {x} {x} f (refl x) = refl (refl (f x))

-- some useful properties about transport
tr∙ : ∀ {A : Set} {B : A → Set} {x y z : A} → ∀ (p : x ≡ y) (q : y ≡ z) →
      ∀ (b : B x) → tr {A} {B} q (tr {A} {B} p b) ≡ tr {A} {B} (p ∙ q) b
tr∙ {_} {_} {x} {x} {x} (refl x) (refl x) b = refl b

trcomp : ∀ {A B : Set} {P : B → Set} {x y : A} → ∀ (f : A → B) (p : x ≡ y) →
         ∀ (b : P (f x)) → tr {A} {λ a → P (f a)} p b ≡ tr {B} {P} (ap f p) b
trcomp {_} {_} {_} {x} {x} f (refl x) b = refl b

trhi : ∀ {A : Set} {P Q : A → Set} {x y : A} → ∀ (f : ∀ (x : A) → P x → Q x) →
       ∀ (p : x ≡ y) (b : P x) → f y (tr {A} {P} p b) ≡ tr {A} {Q} p (f x b)
trhi {_} {_} {_} {x} {x} f (refl x) b = refl (f x b)
=======
apd : ∀ {A : Set} {B : A → Set} → ∀ (f : (∀ (a : A) → B a)) →
      ∀ (x y : A) (p : x ≡ y) → tr {A} {B} {x} {y} p (f x) ≡ f y
apd {A} {B} f x x (refl x) = refl (tr {A} {B} {x} {x} (refl x) (f x))

-- apd helps to construct a
>>>>>>> a0dc66dca08059f740d9290f3d1cad1bb007d721


text:
open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat

-- setup

infixl 5 _>>=_
_>>=_ = bindTC

defToTerm : Name → Definition → List (Arg Term) → Term
defToTerm _ (function cs) as = pat-lam cs as
defToTerm _ (data-cons d) as = con d as
defToTerm _ _ _ = unknown

derefImmediate : Term → TC Term
derefImmediate (def f args) = getDefinition f >>= λ f' → returnTC (defToTerm f f' args)
derefImmediate x = returnTC x

macro
  reflect : ∀ {ℓ} {t : Set ℓ} → t → Term → TC ⊤
  reflect x a = quoteTC x >>= derefImmediate >>= quoteTC >>= unify a

  unfold : Name → Term → TC ⊤
  unfold x a = getDefinition x >>= λ d → unify a (defToTerm x d [])

-- crash

data Vec (A : Set) : Nat → Set where
  [] : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)

vid vid' : ∀ n → Vec Nat n → Vec Nat n
vid n [] = []
vid n (x ∷ xs) = x ∷ xs

vid' = unfold vid

crash : Term
crash = reflect vid

len : ∀ {n} → Vec Nat n → Nat
len [] = 0
len (x ∷ xs) = suc (len xs)

-- Forces different order in clause tel and patterns
f f' : ∀ n → Vec Nat n → Vec Nat n → Nat
f n xs [] = n
f n xs (y ∷ ys) = n + y + len xs + len ys

f' = unfold f