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

   Copyright (c) 2020, 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.ImplShared.Base.Types

open import LibraBFT.Abstract.Types.EpochConfig UID NodeId
open import LibraBFT.Base.ByteString
open import LibraBFT.Base.Encode
open import LibraBFT.Base.KVMap as KVMap
open import LibraBFT.Base.PKCS
open import LibraBFT.Concrete.System
open import LibraBFT.Concrete.System.Parameters
open import LibraBFT.Hash
open import LibraBFT.Impl.Consensus.EpochManagerTypes
import      LibraBFT.Impl.Consensus.Liveness.RoundState as RoundState
import      LibraBFT.Impl.IO.OBM.GenKeyFile             as GenKeyFile
open import LibraBFT.Impl.IO.OBM.InputOutputHandlers
import      LibraBFT.Impl.IO.OBM.Start                  as Start
open import LibraBFT.Impl.OBM.Rust.RustTypes
open import LibraBFT.Impl.OBM.Time
import      LibraBFT.Impl.Types.BlockInfo               as BlockInfo
import      LibraBFT.Impl.Types.ValidatorSigner         as ValidatorSigner
open import LibraBFT.Impl.Consensus.RoundManager
open import LibraBFT.ImplShared.Consensus.Types
open import LibraBFT.ImplShared.Consensus.Types.EpochIndep
open import LibraBFT.ImplShared.Interface.Output
open import LibraBFT.ImplShared.Util.Crypto
open import LibraBFT.ImplShared.Util.Util
open import LibraBFT.Lemmas
open import LibraBFT.Prelude
open import LibraBFT.Yasm.Base
import      LibraBFT.Yasm.Types as LYT
open import Optics.All

-- This module connects implementation handlers to the interface of the SystemModel.

module LibraBFT.Impl.Handle where

open EpochConfig

------------------------------------------------------------------------------
-- This function works with any implementation of a RoundManager.

-- NOTE: The system layer only cares about this step function.
-- 0 is given as a timestamp.
peerStep : NodeId → NetworkMsg → RoundManager → RoundManager × List (LYT.Action NetworkMsg)
peerStep nid msg st = runHandler st (handle nid msg 0)
 where
  -- This invokes an implementation handler.
  runHandler : RoundManager → LBFT Unit → RoundManager × List (LYT.Action NetworkMsg)
  runHandler st handler = ×-map₂ (outputsToActions {st}) (proj₂ (LBFT-run handler st))

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

-- This connects the implementation handler to the system model so it can be initialized.

module InitHandler where
  {-
  IMPL-DIFF: In Haskell, nodes are started with a filepath of a file containing
  - number of faults allowed
  - genesis LedgerInfoWithSignatures
  - network addresses/name and secret and public keys of all nodes in the genesis epoch

  Main reads/checks that file then calls a network specific 'run' functions (e.g., ZMQ.hs)
  that setup the network handlers then eventually call 'Start.startViaConsensusProvider'.

  That functions calls 'ConsensusProvider.startConsensus' which returns
  '(EpochManager, [Output]'.

  'Start.startViaConsensusProvider' then goes on to create and wire up internal communication
  channels and starts threads.  The most relevant thread starts up
  `(EpochManager.obmStartLoop epochManager output ...)' to handle the initialization output
  and then to handle new messages from the network.

  In Agda below,
  - we assume 'BootstrapInfo' known to all peers
    - i.e., the same info that Haskell creates via 'GenKeyFile.create'
    - the assumed info is given to 'mkSysInitAndHandlers' in 'InitAndHandlers'
  - System initialization calls 'initHandler'
  - 'initHandler' eventually calls 'initialize'
  - 'initialize' calls 'State.startViaConsensusProvider'
    when then calls 'ConsensusProvider.startConsensus' which returns
    '(EpochManager, List Output)', just like Haskell.
  - Since there is no network, internal channels and threads, this is the end of this process.

  Note: although both the Haskell and Agda version support non-uniform voting, the
  above initialization process assumes one-vote per peer.
  -}

  postulate -- TODO-2: Eliminate when/if timestamps are modeled
    now : Instant

  proposalGenerator : ProposalGenerator
  proposalGenerator = ProposalGenerator∙new 0

  initialize' : Instant → GenKeyFile.NfLiwsVsVvPe → Either ErrLog (EpochManager × List Output)
  initialize' now nfLiwsVsVvPe =
    Start.startViaConsensusProvider
      now nfLiwsVsVvPe
      (TxTypeDependentStuffForNetwork∙new
        proposalGenerator
        (StateComputer∙new BlockInfo.gENESIS_VERSION))

  abstract
    initialize  : Instant → GenKeyFile.NfLiwsVsVvPe → Either ErrLog (EpochManager × List Output)
    initialize  = initialize'
    initialize≡ : initialize ≡ initialize'
    initialize≡ = refl

  mkNfLiwsVsVvPe : BootstrapInfo → ValidatorSigner → GenKeyFile.NfLiwsVsVvPe
  mkNfLiwsVsVvPe bsi vs = (bsi ^∙ bsiNumFaults , bsi ^∙ bsiLIWS , vs , bsi ^∙ bsiVV , bsi ^∙ bsiPE)

  initEMWithOutput' : BootstrapInfo → ValidatorSigner → Either  ErrLog (EpochManager × List Output)
  initEMWithOutput' bsi vs =
    initialize now (mkNfLiwsVsVvPe bsi vs)

  initEMWithOutput  : BootstrapInfo → ValidatorSigner → EitherD ErrLog (EpochManager × List Output)
  initEMWithOutput  bsi vs =
    fromEither $
    initialize now (mkNfLiwsVsVvPe bsi vs)

  getEmRm : EpochManager → Either ErrLog RoundManager
  getEmRm em =
    case em ^∙ emProcessor of λ where
      nothing  → Left fakeErr
      (just p) → case p of λ where
                   (RoundProcessorRecovery _) → Left fakeErr
                   (RoundProcessorNormal rm)  → Right rm

  initRMWithOutput' : BootstrapInfo → ValidatorSigner → Either  ErrLog (RoundManager × List Output)
  initRMWithOutput' bsi vs = do
    (em , lo) ← initEMWithOutput' bsi vs
    rm        ← getEmRm em
    Right (rm , lo)

  initRMWithOutput  : BootstrapInfo → ValidatorSigner → EitherD ErrLog (RoundManager × List Output)
  initRMWithOutput  bsi vs = do
    (em , lo) ← initEMWithOutput bsi vs
    rm        ← fromEither
              $ getEmRm em
    fromEither $ Right (rm , lo)

  -- This shows that the Either and EitherD versions are equivalent.
  -- This is a first step towards eliminating the painful VariantOf stuff,
  -- so we can have the version that looks (almost) exactly like the Haskell,
  -- and the EitherD variant, broken into explicit steps, etc. for proving.
  initEMWithOutput≡
    : ∀ {bsi : BootstrapInfo} {vs : ValidatorSigner}
    → initEMWithOutput' bsi vs ≡ EitherD-run (initEMWithOutput bsi vs)
  initEMWithOutput≡ {bsi} {vs}
    with initialize now (mkNfLiwsVsVvPe bsi vs)
  ... | Left  _ = refl
  ... | Right _ = refl

  initRMWithOutput≡
    : ∀ {bsi : BootstrapInfo} {vs : ValidatorSigner}
    → initRMWithOutput' bsi vs ≡ EitherD-run (initRMWithOutput bsi vs)
  initRMWithOutput≡ {bsi} {vs}
    with initialize now (mkNfLiwsVsVvPe bsi vs)
  ... | Left  _ = refl
  ... | Right (em , _)
    with getEmRm em
  ... | Left  _ = refl
  ... | Right _ = refl

  abstract
   initHandler : Author → BootstrapInfo → Maybe (RoundManager × List (LYT.Action NetworkMsg))
   initHandler pid bsi =
    case ValidatorSigner.obmGetValidatorSigner pid (bsi ^∙ bsiVSS) of λ where
      (Left _)   → nothing
      (Right vs) →
        case initRMWithOutput' bsi vs of λ where
          (Left _)          → nothing
          (Right (rm , lo)) → just (rm , outputsToActions {State = rm} lo)

  InitAndHandlers : SystemInitAndHandlers ℓ-RoundManager ConcSysParms
  InitAndHandlers =
    mkSysInitAndHandlers
      fakeBootstrapInfo
      fakeInitRM
      initHandler
      peerStep
   where
    postulate -- TODO-1: eliminate by constructing inhabitants
      bs : BlockStore
      pe : ProposerElection
      rs : RoundState
      sr : SafetyRules
      vv : BootstrapInfo → ValidatorVerifier
    -- For uninitialised peers, so we know nothing about their state.
    -- Construct a value of type `RoundManager` to ensure it is inhabitable.
    fakeInitRM : RoundManager
    fakeInitRM = RoundManager∙new
      ObmNeedFetch∙new
      (EpochState∙new 1 (vv fakeBootstrapInfo))
      bs rs pe proposalGenerator sr false

max_stars_repo_name: oracle/bft-consensus-agda

max_issues_repo_name: oracle/bft-consensus-agda

max_forks_repo_name: oracle/bft-consensus-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to All
------------------------------------------------------------------------

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

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

open import Axiom.Extensionality.Propositional using (Extensionality)
open import Data.Bool.Base using (Bool; T; true; false)
open import Data.Bool.Properties using (T-∧)
open import Data.Empty
open import Data.Fin.Base using (Fin) renaming (zero to fzero; suc to fsuc)
open import Data.List.Base as List using
  ( List; []; _∷_; [_]; _∷ʳ_; fromMaybe; null; _++_; concat; map; mapMaybe
  ; inits; tails; drop; take; applyUpTo; applyDownFrom; replicate; tabulate
  ; filter; zipWith; all; derun; deduplicate
  )
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
open import Data.List.Relation.Unary.All as All using
  ( All; []; _∷_; lookup; updateAt
  ; _[_]=_; here; there
  ; Null
  )
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
import Data.List.Relation.Binary.Equality.Setoid as ListEq using (_≋_; []; _∷_)
open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
open import Data.Maybe.Relation.Unary.All as MAll using (just; nothing)
open import Data.Nat.Base using (zero; suc; z≤n; s≤s; _<_)
open import Data.Nat.Properties using (≤-refl; ≤-step)
open import Data.Product as Prod using (_×_; _,_; uncurry; uncurry′)
open import Function.Base
open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence using (_⇔_; equivalence; Equivalence)
open import Function.Inverse using (_↔_; inverse)
open import Function.Surjection using (_↠_; surjection)
open import Level using (Level)
open import Relation.Binary as B using (REL; Setoid; _Respects_)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong; cong₂; _≗_)
open import Relation.Nullary.Reflects using (invert)
open import Relation.Nullary
open import Relation.Nullary.Negation using (¬?; contradiction; decidable-stable)
open import Relation.Unary
  using (Decidable; Pred; Universal) renaming (_⊆_ to _⋐_)

private
  variable
    a b c p q r ℓ : Level
    A : Set a
    B : Set b
    C : Set c

------------------------------------------------------------------------
-- Properties regarding Null

Null⇒null : ∀ {xs : List A} → Null xs → T (null xs)
Null⇒null [] = _

null⇒Null : ∀ {xs : List A} → T (null xs) → Null xs
null⇒Null {xs = []   } _ = []
null⇒Null {xs = _ ∷ _} ()

------------------------------------------------------------------------
-- Properties of the "points-to" relation _[_]=_

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

  -- Relation _[_]=_ is deterministic: each index points to a single value.

  []=-injective : ∀ {x xs} {px qx : P x} {pxs : All P xs} {i : x ∈ xs} →
                  pxs [ i ]= px →
                  pxs [ i ]= qx →
                  px ≡ qx
  []=-injective here          here          = refl
  []=-injective (there x↦px) (there x↦qx) = []=-injective x↦px x↦qx

  -- See also Data.List.Relation.Unary.All.Properties.WithK.[]=-irrelevant.

------------------------------------------------------------------------
-- Lemmas relating Any, All and negation.

module _ {P : A → Set p} where

  ¬Any⇒All¬ : ∀ xs → ¬ Any P xs → All (¬_ ∘ P) xs
  ¬Any⇒All¬ []       ¬p = []
  ¬Any⇒All¬ (x ∷ xs) ¬p = ¬p ∘ here ∷ ¬Any⇒All¬ xs (¬p ∘ there)

  All¬⇒¬Any : ∀ {xs} → All (¬_ ∘ P) xs → ¬ Any P xs
  All¬⇒¬Any (¬p ∷ _)  (here  p) = ¬p p
  All¬⇒¬Any (_  ∷ ¬p) (there p) = All¬⇒¬Any ¬p p

  ¬All⇒Any¬ : Decidable P → ∀ xs → ¬ All P xs → Any (¬_ ∘ P) xs
  ¬All⇒Any¬ dec []       ¬∀ = ⊥-elim (¬∀ [])
  ¬All⇒Any¬ dec (x ∷ xs) ¬∀ with dec x
  ... |  true because  [p] = there (¬All⇒Any¬ dec xs (¬∀ ∘ _∷_ (invert [p])))
  ... | false because [¬p] = here (invert [¬p])

  Any¬⇒¬All : ∀ {xs} → Any (¬_ ∘ P) xs → ¬ All P xs
  Any¬⇒¬All (here  ¬p) = ¬p           ∘ All.head
  Any¬⇒¬All (there ¬p) = Any¬⇒¬All ¬p ∘ All.tail

  ¬Any↠All¬ : ∀ {xs} → (¬ Any P xs) ↠ All (¬_ ∘ P) xs
  ¬Any↠All¬ = surjection (¬Any⇒All¬ _) All¬⇒¬Any to∘from
    where
    to∘from : ∀ {xs} (¬p : All (¬_ ∘ P) xs) → ¬Any⇒All¬ xs (All¬⇒¬Any ¬p) ≡ ¬p
    to∘from []         = refl
    to∘from (¬p ∷ ¬ps) = cong₂ _∷_ refl (to∘from ¬ps)

    -- If equality of functions were extensional, then the surjection
    -- could be strengthened to a bijection.

    from∘to : Extensionality _ _ →
              ∀ xs → (¬p : ¬ Any P xs) → All¬⇒¬Any (¬Any⇒All¬ xs ¬p) ≡ ¬p
    from∘to ext []       ¬p = ext λ ()
    from∘to ext (x ∷ xs) ¬p = ext λ
      { (here p)  → refl
      ; (there p) → cong (λ f → f p) $ from∘to ext xs (¬p ∘ there)
      }

  Any¬⇔¬All : ∀ {xs} → Decidable P → Any (¬_ ∘ P) xs ⇔ (¬ All P xs)
  Any¬⇔¬All dec = equivalence Any¬⇒¬All (¬All⇒Any¬ dec _)
    where
    -- If equality of functions were extensional, then the logical
    -- equivalence could be strengthened to a surjection.
    to∘from : Extensionality _ _ →
              ∀ {xs} (¬∀ : ¬ All P xs) → Any¬⇒¬All (¬All⇒Any¬ dec xs ¬∀) ≡ ¬∀
    to∘from ext ¬∀ = ext (⊥-elim ∘ ¬∀)

module _ {_~_ : REL A B ℓ} where

  All-swap : ∀ {xs ys} →
             All (λ x → All (x ~_) ys) xs →
             All (λ y → All (_~ y) xs) ys
  All-swap {ys = []}     _   = []
  All-swap {ys = y ∷ ys} []  = All.universal (λ _ → []) (y ∷ ys)
  All-swap {ys = y ∷ ys} ((x~y ∷ x~ys) ∷ pxs) =
    (x~y ∷ (All.map All.head pxs)) ∷
    All-swap (x~ys ∷ (All.map All.tail pxs))

------------------------------------------------------------------------
-- Defining properties of lookup and _[_]=_
--
-- pxs [ i ]= px  if and only if  lookup pxs i = px.

module _ {P : A → Set p} where

  -- `i` points to `lookup pxs i` in `pxs`.

  []=lookup : ∀ {x xs} (pxs : All P xs) (i : x ∈ xs) →
              pxs [ i ]= lookup pxs i
  []=lookup (px ∷ pxs) (here refl) = here
  []=lookup (px ∷ pxs) (there i)   = there ([]=lookup pxs i)

  -- If `i` points to `px` in `pxs`, then `lookup pxs i ≡ px`.

  []=⇒lookup : ∀ {x xs} {px : P x} {pxs : All P xs} {i : x ∈ xs} →
               pxs [ i ]= px →
               lookup pxs i ≡ px
  []=⇒lookup x↦px = []=-injective ([]=lookup _ _) x↦px

  -- If `lookup pxs i ≡ px`, then `i` points to `px` in `pxs`.

  lookup⇒[]= : ∀{x xs} {px : P x} (pxs : All P xs) (i : x ∈ xs) →
               lookup pxs i ≡ px →
               pxs [ i ]= px
  lookup⇒[]= pxs i refl = []=lookup pxs i

------------------------------------------------------------------------
-- Properties of operations over `All`
------------------------------------------------------------------------
-- map

module _ {P : Pred A p} {Q : Pred A q} {f : P ⋐ Q} where

  map-cong : ∀ {xs} {g : P ⋐ Q} (pxs : All P xs) →
             (∀ {x} → f {x} ≗ g) → All.map f pxs ≡ All.map g pxs
  map-cong []         _   = refl
  map-cong (px ∷ pxs) feq = cong₂ _∷_ (feq px) (map-cong pxs feq)

  map-id : ∀ {xs} (pxs : All P xs) → All.map id pxs ≡ pxs
  map-id []         = refl
  map-id (px ∷ pxs) = cong (px ∷_)  (map-id pxs)

  map-compose : ∀ {r} {R : Pred A r} {xs} {g : Q ⋐ R} (pxs : All P xs) →
                All.map g (All.map f pxs) ≡ All.map (g ∘ f) pxs
  map-compose []         = refl
  map-compose (px ∷ pxs) = cong (_ ∷_) (map-compose pxs)

  lookup-map : ∀ {xs x} (pxs : All P xs) (i : x ∈ xs) →
               lookup (All.map f pxs) i ≡ f (lookup pxs i)
  lookup-map (px ∷ pxs) (here refl) = refl
  lookup-map (px ∷ pxs) (there i)   = lookup-map pxs i

------------------------------------------------------------------------
-- _[_]%=_ / updateAt

module _ {P : Pred A p} where

  -- Defining properties of updateAt:

  -- (+) updateAt actually updates the element at the given index.

  updateAt-updates : ∀ {x xs} (i : x ∈ xs) {f : P x → P x} {px : P x} (pxs : All P xs) →
                     pxs              [ i ]= px →
                     updateAt i f pxs [ i ]= f px
  updateAt-updates (here  refl) (px ∷ pxs) here         = here
  updateAt-updates (there i)    (px ∷ pxs) (there x↦px) =
    there (updateAt-updates i pxs x↦px)

  -- (-) updateAt i does not touch the elements at other indices.

  updateAt-minimal : ∀ {x y xs} (i : x ∈ xs) (j : y ∈ xs) →
                     ∀ {f : P y → P y} {px : P x} (pxs : All P xs) →
                     i ≢∈ j →
                     pxs              [ i ]= px →
                     updateAt j f pxs [ i ]= px
  updateAt-minimal (here .refl) (here refl) (px ∷ pxs) i≢j here        =
    ⊥-elim (i≢j refl refl)
  updateAt-minimal (here .refl) (there j)   (px ∷ pxs) i≢j here        = here
  updateAt-minimal (there i)    (here refl) (px ∷ pxs) i≢j (there val) = there val
  updateAt-minimal (there i)    (there j)   (px ∷ pxs) i≢j (there val) =
    there (updateAt-minimal i j pxs (there-injective-≢∈ i≢j) val)

  -- lookup after updateAt reduces.

  -- For same index this is an easy consequence of updateAt-updates
  -- using []=↔lookup.

  lookup∘updateAt : ∀ {x xs} (pxs : All P xs) (i : x ∈ xs) {f : P x → P x} →
                    lookup (updateAt i f pxs) i ≡ f (lookup pxs i)
  lookup∘updateAt pxs i =
    []=⇒lookup (updateAt-updates i pxs (lookup⇒[]= pxs i refl))

  -- For different indices it easily follows from updateAt-minimal.

  lookup∘updateAt′ : ∀ {x y xs} (i : x ∈ xs) (j : y ∈ xs) →
                     ∀ {f : P y → P y} {px : P x} (pxs : All P xs) →
                     i ≢∈ j →
                     lookup (updateAt j f pxs) i ≡ lookup pxs i
  lookup∘updateAt′ i j pxs i≢j =
    []=⇒lookup (updateAt-minimal i j pxs i≢j (lookup⇒[]= pxs i refl))

  -- The other properties are consequences of (+) and (-).
  -- We spell the most natural properties out.
  -- Direct inductive proofs are in most cases easier than just using
  -- the defining properties.

  -- In the explanations, we make use of shorthand  f = g ↾ x
  -- meaning that f and g agree at point x, i.e.  f x ≡ g x.

  -- updateAt (i : x ∈ xs)  is a morphism
  -- from the monoid of endofunctions  P x → P x
  -- to the monoid of endofunctions  All P xs → All P xs.

  -- 1a. relative identity:  f = id ↾ (lookup pxs i)
  --                implies  updateAt i f = id ↾ pxs

  updateAt-id-relative : ∀ {x xs} (i : x ∈ xs) {f : P x → P x} (pxs : All P xs) →
                         f (lookup pxs i) ≡ lookup pxs i →
                         updateAt i f pxs ≡ pxs
  updateAt-id-relative (here refl)(px ∷ pxs) eq = cong (_∷ pxs) eq
  updateAt-id-relative (there i)  (px ∷ pxs) eq = cong (px ∷_) (updateAt-id-relative i pxs eq)

  -- 1b. identity:  updateAt i id ≗ id

  updateAt-id : ∀ {x xs} (i : x ∈ xs) (pxs : All P xs) →
                updateAt i id pxs ≡ pxs
  updateAt-id i pxs = updateAt-id-relative i pxs refl

  -- 2a. relative composition:  f ∘ g = h ↾ (lookup i pxs)
  --                   implies  updateAt i f ∘ updateAt i g = updateAt i h ↾ pxs

  updateAt-compose-relative : ∀ {x xs} (i : x ∈ xs) {f g h : P x → P x} (pxs : All P xs) →
                              f (g (lookup pxs i)) ≡ h (lookup pxs i) →
                              updateAt i f (updateAt i g pxs) ≡ updateAt i h pxs
  updateAt-compose-relative (here refl) (px ∷ pxs) fg=h = cong (_∷ pxs) fg=h
  updateAt-compose-relative (there i)   (px ∷ pxs) fg=h =
    cong (px ∷_) (updateAt-compose-relative i pxs fg=h)

  -- 2b. composition:  updateAt i f ∘ updateAt i g ≗ updateAt i (f ∘ g)

  updateAt-compose : ∀ {x xs} (i : x ∈ xs) {f g : P x → P x} →
                     updateAt {P = P} i f ∘ updateAt i g ≗ updateAt i (f ∘ g)
  updateAt-compose (here refl) (px ∷ pxs) = refl
  updateAt-compose (there i)   (px ∷ pxs) = cong (px ∷_) (updateAt-compose i pxs)

  -- 3. congruence:  updateAt i  is a congruence wrt. extensional equality.

  -- 3a.  If    f = g ↾ (lookup pxs i)
  --      then  updateAt i f = updateAt i g ↾ pxs

  updateAt-cong-relative : ∀ {x xs} (i : x ∈ xs) {f g : P x → P x} (pxs : All P xs) →
                           f (lookup pxs i) ≡ g (lookup pxs i) →
                           updateAt i f pxs ≡ updateAt i g pxs
  updateAt-cong-relative (here refl) (px ∷ pxs) f=g = cong (_∷ pxs) f=g
  updateAt-cong-relative (there i)   (px ∷ pxs) f=g = cong (px ∷_) (updateAt-cong-relative i pxs f=g)

  -- 3b. congruence:  f ≗ g → updateAt i f ≗ updateAt i g

  updateAt-cong : ∀ {x xs} (i : x ∈ xs) {f g : P x → P x} →
                  f ≗ g →
                  updateAt i f ≗ updateAt i g
  updateAt-cong i f≗g pxs = updateAt-cong-relative i pxs (f≗g (lookup pxs i))

  -- The order of updates at different indices i ≢ j does not matter.

  -- This a consequence of updateAt-updates and updateAt-minimal
  -- but easier to prove inductively.

  updateAt-commutes : ∀ {x y xs} (i : x ∈ xs) (j : y ∈ xs) →
                      ∀ {f : P x → P x} {g : P y → P y} →
                      i ≢∈ j →
                      updateAt i f ∘ updateAt j g ≗ updateAt j g ∘ updateAt i f
  updateAt-commutes (here refl) (here refl) i≢j (px ∷ pxs) =
    ⊥-elim (i≢j refl refl)
  updateAt-commutes (here refl) (there j)   i≢j (px ∷ pxs) = refl
  updateAt-commutes (there i)   (here refl) i≢j (px ∷ pxs) = refl
  updateAt-commutes (there i)   (there j)   i≢j (px ∷ pxs) =
    cong (px ∷_) (updateAt-commutes i j (there-injective-≢∈ i≢j) pxs)

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

  map-updateAt : ∀ {x xs} {f : P ⋐ Q} {g : P x → P x} {h : Q x → Q x}
                 (pxs : All P xs) (i : x ∈ xs) →
                 f (g (lookup pxs i)) ≡ h (f (lookup pxs i)) →
                 All.map f (pxs All.[ i ]%= g) ≡ (All.map f pxs) All.[ i ]%= h
  map-updateAt (px ∷ pxs) (here refl) = cong (_∷ _)
  map-updateAt (px ∷ pxs) (there i) feq = cong (_ ∷_) (map-updateAt pxs i feq)

------------------------------------------------------------------------
-- Introduction (⁺) and elimination (⁻) rules for list operations
------------------------------------------------------------------------
-- map

module _ {P : B → Set p} {f : A → B} where

  map⁺ : ∀ {xs} → All (P ∘ f) xs → All P (map f xs)
  map⁺ []       = []
  map⁺ (p ∷ ps) = p ∷ map⁺ ps

  map⁻ : ∀ {xs} → All P (map f xs) → All (P ∘ f) xs
  map⁻ {xs = []}    []       = []
  map⁻ {xs = _ ∷ _} (p ∷ ps) = p ∷ map⁻ ps

-- A variant of All.map.

module _ {P : A → Set p} {Q : B → Set q} {f : A → B} where

  gmap : P ⋐ Q ∘ f → All P ⋐ All Q ∘ map f
  gmap g = map⁺ ∘ All.map g

------------------------------------------------------------------------
-- mapMaybe

module _ (P : B → Set p) {f : A → Maybe B} where

  mapMaybe⁺ : ∀ {xs} → All (MAll.All P) (map f xs) → All P (mapMaybe f xs)
  mapMaybe⁺ {[]}     [] = []
  mapMaybe⁺ {x ∷ xs} (px ∷ pxs) with f x
  ... | nothing = mapMaybe⁺ pxs
  ... | just v with px
  ...   | just pv = pv ∷ mapMaybe⁺ pxs

------------------------------------------------------------------------
-- _++_

module _ {P : A → Set p} where

  ++⁺ : ∀ {xs ys} → All P xs → All P ys → All P (xs ++ ys)
  ++⁺ []         pys = pys
  ++⁺ (px ∷ pxs) pys = px ∷ ++⁺ pxs pys

  ++⁻ˡ : ∀ xs {ys} → All P (xs ++ ys) → All P xs
  ++⁻ˡ []       p          = []
  ++⁻ˡ (x ∷ xs) (px ∷ pxs) = px ∷ (++⁻ˡ _ pxs)

  ++⁻ʳ : ∀ xs {ys} → All P (xs ++ ys) → All P ys
  ++⁻ʳ []       p          = p
  ++⁻ʳ (x ∷ xs) (px ∷ pxs) = ++⁻ʳ xs pxs

  ++⁻ : ∀ xs {ys} → All P (xs ++ ys) → All P xs × All P ys
  ++⁻ []       p          = [] , p
  ++⁻ (x ∷ xs) (px ∷ pxs) = Prod.map (px ∷_) id (++⁻ _ pxs)

  ++↔ : ∀ {xs ys} → (All P xs × All P ys) ↔ All P (xs ++ ys)
  ++↔ {xs} = inverse (uncurry ++⁺) (++⁻ xs) ++⁻∘++⁺ (++⁺∘++⁻ xs)
    where
    ++⁺∘++⁻ : ∀ xs {ys} (p : All P (xs ++ ys)) →
              uncurry′ ++⁺ (++⁻ xs p) ≡ p
    ++⁺∘++⁻ []       p          = refl
    ++⁺∘++⁻ (x ∷ xs) (px ∷ pxs) = cong (_∷_ px) $ ++⁺∘++⁻ xs pxs

    ++⁻∘++⁺ : ∀ {xs ys} (p : All P xs × All P ys) →
              ++⁻ xs (uncurry ++⁺ p) ≡ p
    ++⁻∘++⁺ ([]       , pys) = refl
    ++⁻∘++⁺ (px ∷ pxs , pys) rewrite ++⁻∘++⁺ (pxs , pys) = refl

------------------------------------------------------------------------
-- concat

module _ {P : A → Set p} where

  concat⁺ : ∀ {xss} → All (All P) xss → All P (concat xss)
  concat⁺ []           = []
  concat⁺ (pxs ∷ pxss) = ++⁺ pxs (concat⁺ pxss)

  concat⁻ : ∀ {xss} → All P (concat xss) → All (All P) xss
  concat⁻ {[]}       []  = []
  concat⁻ {xs ∷ xss} pxs = ++⁻ˡ xs pxs ∷ concat⁻ (++⁻ʳ xs pxs)

------------------------------------------------------------------------
-- take and drop

module _ {P : A → Set p} where

  drop⁺ : ∀ {xs} n → All P xs → All P (drop n xs)
  drop⁺ zero    pxs        = pxs
  drop⁺ (suc n) []         = []
  drop⁺ (suc n) (px ∷ pxs) = drop⁺ n pxs

  take⁺ : ∀ {xs} n → All P xs → All P (take n xs)
  take⁺ zero    pxs        = []
  take⁺ (suc n) []         = []
  take⁺ (suc n) (px ∷ pxs) = px ∷ take⁺ n pxs

------------------------------------------------------------------------
-- applyUpTo

module _ {P : A → Set p} where

  applyUpTo⁺₁ : ∀ f n → (∀ {i} → i < n → P (f i)) → All P (applyUpTo f n)
  applyUpTo⁺₁ f zero    Pf = []
  applyUpTo⁺₁ f (suc n) Pf = Pf (s≤s z≤n) ∷ applyUpTo⁺₁ (f ∘ suc) n (Pf ∘ s≤s)

  applyUpTo⁺₂ : ∀ f n → (∀ i → P (f i)) → All P (applyUpTo f n)
  applyUpTo⁺₂ f n Pf = applyUpTo⁺₁ f n (λ _ → Pf _)

  applyUpTo⁻ : ∀ f n → All P (applyUpTo f n) → ∀ {i} → i < n → P (f i)
  applyUpTo⁻ f (suc n) (px ∷ _)   (s≤s z≤n)       = px
  applyUpTo⁻ f (suc n) (_  ∷ pxs) (s≤s (s≤s i<n)) =
    applyUpTo⁻ (f ∘ suc) n pxs (s≤s i<n)

------------------------------------------------------------------------
-- applyDownFrom

module _ {P : A → Set p} where

  applyDownFrom⁺₁ : ∀ f n → (∀ {i} → i < n → P (f i)) → All P (applyDownFrom f n)
  applyDownFrom⁺₁ f zero    Pf = []
  applyDownFrom⁺₁ f (suc n) Pf = Pf ≤-refl ∷ applyDownFrom⁺₁ f n (Pf ∘ ≤-step)

  applyDownFrom⁺₂ : ∀ f n → (∀ i → P (f i)) → All P (applyDownFrom f n)
  applyDownFrom⁺₂ f n Pf = applyDownFrom⁺₁ f n (λ _ → Pf _)

------------------------------------------------------------------------
-- tabulate

module _ {P : A → Set p} where

  tabulate⁺ : ∀ {n} {f : Fin n → A} →
              (∀ i → P (f i)) → All P (tabulate f)
  tabulate⁺ {zero}  Pf = []
  tabulate⁺ {suc n} Pf = Pf fzero ∷ tabulate⁺ (Pf ∘ fsuc)

  tabulate⁻ : ∀ {n} {f : Fin n → A} →
              All P (tabulate f) → (∀ i → P (f i))
  tabulate⁻ {suc n} (px ∷ _) fzero    = px
  tabulate⁻ {suc n} (_ ∷ pf) (fsuc i) = tabulate⁻ pf i

------------------------------------------------------------------------
-- remove

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

  ─⁺ : ∀ {xs} (p : Any P xs) → All Q xs → All Q (xs Any.─ p)
  ─⁺ (here px) (_ ∷ qs) = qs
  ─⁺ (there p) (q ∷ qs) = q ∷ ─⁺ p qs

  ─⁻ : ∀ {xs} (p : Any P xs) → Q (Any.lookup p) → All Q (xs Any.─ p) → All Q xs
  ─⁻ (here px) q qs        = q ∷ qs
  ─⁻ (there p) q (q′ ∷ qs) = q′ ∷ ─⁻ p q qs

------------------------------------------------------------------------
-- filter

module _ {P : A → Set p} (P? : Decidable P) where

  all-filter : ∀ xs → All P (filter P? xs)
  all-filter []       = []
  all-filter (x ∷ xs) with P? x
  ... |  true because [Px] = invert [Px] ∷ all-filter xs
  ... | false because  _   = all-filter xs

module _ {P : A → Set p} {Q : A → Set q} (P? : Decidable P) where

  filter⁺ : ∀ {xs} → All Q xs → All Q (filter P? xs)
  filter⁺ {xs = _}     [] = []
  filter⁺ {xs = x ∷ _} (Qx ∷ Qxs) with does (P? x)
  ... | false = filter⁺ Qxs
  ... | true  = Qx ∷ filter⁺ Qxs

  filter⁻ : ∀ {xs} → All Q (filter P? xs) → All Q (filter (¬? ∘ P?) xs) → All Q xs
  filter⁻ {[]}         []          []                           = []
  filter⁻ {x ∷ xs}       all⁺        all⁻ with P? x  | ¬? (P? x)
  filter⁻ {x ∷ xs}       all⁺        all⁻  | yes  Px | yes  ¬Px = contradiction Px ¬Px
  filter⁻ {x ∷ xs} (qx ∷ all⁺)       all⁻  | yes  Px | no  ¬¬Px = qx ∷ filter⁻ all⁺ all⁻
  filter⁻ {x ∷ xs}       all⁺  (qx ∷ all⁻) | no    _ | yes  ¬Px = qx ∷ filter⁻ all⁺ all⁻
  filter⁻ {x ∷ xs}       all⁺        all⁻  | no  ¬Px | no  ¬¬Px = contradiction ¬Px ¬¬Px

------------------------------------------------------------------------
-- derun and deduplicate

module _ {P : A → Set p} {R : A → A → Set q} (R? : B.Decidable R) where

  derun⁺ : ∀ {xs} → All P xs → All P (derun R? xs)
  derun⁺ {[]} [] = []
  derun⁺ {x ∷ []} (px ∷ []) = px ∷ []
  derun⁺ {x ∷ y ∷ xs} (px ∷ all[P,y∷xs]) with does (R? x y)
  ... | false = px ∷ derun⁺ all[P,y∷xs]
  ... | true  = derun⁺ all[P,y∷xs]

  deduplicate⁺ : ∀ {xs} → All P xs → All P (deduplicate R? xs)
  deduplicate⁺ [] = []
  deduplicate⁺ {x ∷ _} (px ∷ all[P,xs]) = px ∷ filter⁺ (¬? ∘ R? x) (deduplicate⁺ all[P,xs])

  derun⁻ : P B.Respects (flip R) → ∀ xs → All P (derun R? xs) → All P xs
  derun⁻ P-resp-R []       []          = []
  derun⁻ P-resp-R (x ∷ xs) all[P,x∷xs] = aux x xs all[P,x∷xs] where
    aux : ∀ x xs → All P (derun R? (x ∷ xs)) → All P (x ∷ xs)
    aux x []       (px ∷ []) = px ∷ []
    aux x (y ∷ xs) all[P,x∷y∷xs] with R? x y
    aux x (y ∷ xs) all[P,y∷xs]        | yes Rxy with aux y xs all[P,y∷xs]
    aux x (y ∷ xs) all[P,y∷xs]        | yes Rxy | r@(py ∷ _) = P-resp-R Rxy py ∷ r
    aux x (y ∷ xs) (px ∷ all[P,y∷xs]) | no _ = px ∷ aux y xs all[P,y∷xs]

  module _ (P-resp-R : P B.Respects R) where

    deduplicate⁻ : ∀ xs → All P (deduplicate R? xs) → All P xs
    deduplicate⁻ [] [] = []
    deduplicate⁻ (x ∷ xs) (px ∷ app[P,dedup[xs]]) = px ∷ deduplicate⁻ xs (filter⁻ (¬? ∘ R? x) app[P,dedup[xs]] (All.tabulate aux)) where
      aux : ∀ {z} → z ∈ filter (¬? ∘ ¬? ∘ R? x) (deduplicate R? xs) → P z
      aux {z} z∈filter = P-resp-R (decidable-stable (R? x z) (Prod.proj₂ (∈-filter⁻ (¬? ∘ ¬? ∘ R? x) {z} {deduplicate R? xs} z∈filter))) px

------------------------------------------------------------------------
-- zipWith

module _ (P : C → Set p) (f : A → B → C) where

  zipWith⁺ : ∀ {xs ys} → Pointwise (λ x y → P (f x y)) xs ys →
             All P (zipWith f xs ys)
  zipWith⁺ []              = []
  zipWith⁺ (Pfxy ∷ Pfxsys) = Pfxy ∷ zipWith⁺ Pfxsys

------------------------------------------------------------------------
-- Operations for constructing lists
------------------------------------------------------------------------
-- singleton

module _ {P : A → Set p} where

  singleton⁻ : ∀ {x} → All P [ x ] → P x
  singleton⁻ (px ∷ []) = px

------------------------------------------------------------------------
-- snoc

module _ {P : A → Set p} {x xs} where

  ∷ʳ⁺ : All P xs → P x → All P (xs ∷ʳ x)
  ∷ʳ⁺ pxs px = ++⁺ pxs (px ∷ [])

  ∷ʳ⁻ : All P (xs ∷ʳ x) → All P xs × P x
  ∷ʳ⁻ pxs = Prod.map₂ singleton⁻ $ ++⁻ xs pxs

------------------------------------------------------------------------
-- fromMaybe

module _ {P : A → Set p} where

  fromMaybe⁺ : ∀ {mx} → MAll.All P mx → All P (fromMaybe mx)
  fromMaybe⁺ (just px) = px ∷ []
  fromMaybe⁺ nothing   = []

  fromMaybe⁻ : ∀ mx → All P (fromMaybe mx) → MAll.All P mx
  fromMaybe⁻ (just x) (px ∷ []) = just px
  fromMaybe⁻ nothing  p         = nothing

------------------------------------------------------------------------
-- replicate

module _ {P : A → Set p} where

  replicate⁺ : ∀ n {x} → P x → All P (replicate n x)
  replicate⁺ zero    px = []
  replicate⁺ (suc n) px = px ∷ replicate⁺ n px

  replicate⁻ : ∀ {n x} → All P (replicate (suc n) x) → P x
  replicate⁻ (px ∷ _) = px

------------------------------------------------------------------------
-- inits

module _ {P : A → Set p} where

  inits⁺ : ∀ {xs} → All P xs → All (All P) (inits xs)
  inits⁺ []         = [] ∷ []
  inits⁺ (px ∷ pxs) = [] ∷ gmap (px ∷_) (inits⁺ pxs)

  inits⁻ : ∀ xs → All (All P) (inits xs) → All P xs
  inits⁻ []               pxs                   = []
  inits⁻ (x ∷ [])         ([] ∷ p[x] ∷ [])      = p[x]
  inits⁻ (x ∷ xs@(_ ∷ _)) ([] ∷ pxs@(p[x] ∷ _)) =
    singleton⁻ p[x] ∷ inits⁻ xs (All.map (drop⁺ 1) (map⁻ pxs))

------------------------------------------------------------------------
-- tails

module _ {P : A → Set p} where

  tails⁺ : ∀ {xs} → All P xs → All (All P) (tails xs)
  tails⁺ []             = [] ∷ []
  tails⁺ pxxs@(_ ∷ pxs) = pxxs ∷ tails⁺ pxs

  tails⁻ : ∀ xs → All (All P) (tails xs) → All P xs
  tails⁻ []       pxs        = []
  tails⁻ (x ∷ xs) (pxxs ∷ _) = pxxs

------------------------------------------------------------------------
-- all

module _ (p : A → Bool) where

  all⁺ : ∀ xs → T (all p xs) → All (T ∘ p) xs
  all⁺ []       _     = []
  all⁺ (x ∷ xs) px∷xs with Equivalence.to (T-∧ {p x}) ⟨$⟩ px∷xs
  ... | (px , pxs) = px ∷ all⁺ xs pxs

  all⁻ : ∀ {xs} → All (T ∘ p) xs → T (all p xs)
  all⁻ []         = _
  all⁻ (px ∷ pxs) = Equivalence.from T-∧ ⟨$⟩ (px , all⁻ pxs)

------------------------------------------------------------------------
-- All is anti-monotone.

anti-mono : ∀ {P : A → Set p} {xs ys} → xs ⊆ ys → All P ys → All P xs
anti-mono xs⊆ys pys = All.tabulate (lookup pys ∘ xs⊆ys)

all-anti-mono : ∀ (p : A → Bool) {xs ys} →
                xs ⊆ ys → T (all p ys) → T (all p xs)
all-anti-mono p xs⊆ys = all⁻ p ∘ anti-mono xs⊆ys ∘ all⁺ p _

------------------------------------------------------------------------
-- Interactions with pointwise equality
------------------------------------------------------------------------

module _ {c ℓ} (S : Setoid c ℓ) where

  open Setoid S
  open ListEq S

  respects : {P : Pred Carrier p} → P Respects _≈_ → (All P) Respects _≋_
  respects p≈ []            []         = []
  respects p≈ (x≈y ∷ xs≈ys) (px ∷ pxs) = p≈ x≈y px ∷ respects p≈ xs≈ys pxs

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

-- Version 0.16

All-all = all⁻
{-# WARNING_ON_USAGE All-all
"Warning: All-all was deprecated in v0.16.
Please use all⁻ instead."
#-}
all-All = all⁺
{-# WARNING_ON_USAGE all-All
"Warning: all-All was deprecated in v0.16.
Please use all⁺ instead."
#-}
All-map = map⁺
{-# WARNING_ON_USAGE All-map
"Warning: All-map was deprecated in v0.16.
Please use map⁺ instead."
#-}
map-All = map⁻
{-# WARNING_ON_USAGE map-All
"Warning: map-All was deprecated in v0.16.
Please use map⁻ instead."
#-}

-- Version 1.0

filter⁺₁ = all-filter
{-# WARNING_ON_USAGE filter⁺₁
"Warning: filter⁺₁ was deprecated in v1.0.
Please use all-filter instead."
#-}
filter⁺₂ = filter⁺
{-# WARNING_ON_USAGE filter⁺₂
"Warning: filter⁺₂ was deprecated in v1.0.
Please use filter⁺ instead."
#-}

-- Version 1.3

Any¬→¬All = Any¬⇒¬All
{-# WARNING_ON_USAGE Any¬→¬All
"Warning: Any¬→¬All was deprecated in v1.3.
Please use Any¬⇒¬All instead."
#-}

ext: agda


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

open import lib.Basics
open import lib.types.Paths
open import lib.types.Pi
open import lib.types.Unit
open import lib.types.Nat
open import lib.types.TLevel
open import lib.types.Pointed
open import lib.types.Sigma
open import lib.NType2

open import lib.types.PathSeq

open import nicolai.pseudotruncations.Liblemmas
open import nicolai.pseudotruncations.SeqColim

open import nicolai.pseudotruncations.wconst-preparation

module nicolai.pseudotruncations.heptagon
  {i} {C : Sequence {i}} (wc : wconst-chain C) (a₀ : fst C O) where

  {- î-def is defined in this module: -}
  open wconst-init {i} {C} wc a₀

  module _ (n : ℕ) (a : A n) where

    {- Let us formulate different simplification steps of the
       heptagon. -}

    full-hepta : seq-loop (ins (S n) (f n a))
    full-hepta = (î-def (S n) (f n a)) ⋯ (‼ (î-def n a) ⋯ toSeq (glue n a))

    remove-g : seq-loop (ins (S n) (f n a))
    remove-g = (î-def (S n) (f n a))
               ⋯ ‼ (ins (S n) (f n a)
                      =⟪ ap (ins (S n)) (wc n _ _) ⟫
                    ins (S n) (lift-point C a₀ (S n))
                      =⟪ ! (lift-point-= C a₀ (S n)) ⟫
                    ins O a₀
                      ∎∎)

    simplify-‼ : seq-loop (ins (S n) (f n a))
    simplify-‼ = (î-def (S n) (f n a))
               ⋯ (ins O a₀
                    =⟪ lift-point-= C a₀ (S n) ⟫
                  ins (S n) (lift-point C a₀ (S n))
                    =⟪ ! (ap (ins (S n)) (wc n _ _)) ⟫
                  ins (S n) (f n a)
                    ∎∎)

    simplify-one-g : seq-loop (ins {C = C} (S n) (f n a))
    simplify-one-g =
                  ins (S n) (f n a)
                    =⟪ glue (S n) (f n a) ⟫
                  ins (S (S n)) (f (S n) (f n a))
                    =⟪ ap (ins (S (S n))) (wc (S n) (f n a) (lift-point C a₀ (S n))) ⟫
                  ins (S (S n)) (lift-point C a₀ (S (S n)))
                    =⟪ ! (glue (S n) (lift-point C a₀ (S n))) ⟫
                  ins (S n) (lift-point C a₀ (S n))
                    =⟪ ! (lift-point-= C a₀ (S n)) ⟫
                  ins O a₀
                    =⟪ lift-point-= C a₀ (S n) ⟫
                  ins (S n) (lift-point C a₀ (S n))
                    =⟪ ! (ap (ins (S n)) (wc n a (lift-point C a₀ n))) ⟫
                  ins (S n) (f n a)
                    ∎∎

    simplify-many-g : seq-loop (ins {C = C} (S n) (f n a))
    simplify-many-g =
                  ins (S n) (f n a)
                    =⟪ glue (S n) (f n a) ⟫
                  ins (S (S n)) (f (S n) (f n a))
                    =⟪ ap (ins (S (S n))) (wc (S n) (f n a) (lift-point C a₀ (S n))) ⟫
                  ins (S (S n)) (lift-point C a₀ (S (S n)))
                    =⟪ ! (glue (S n) (lift-point C a₀ (S n))) ⟫
                  ins (S n) (lift-point C a₀ (S n))
                    =⟪ ! (ap (ins (S n)) (wc n a (lift-point C a₀ n))) ⟫
                  ins (S n) (f n a)
                    ∎∎

    replace-ap-SSn : seq-loop (ins {C = C} (S n) (f n a))
    replace-ap-SSn =
                  ins (S n) (f n a)
                    =⟪ glue (S n) (f n a) ⟫
                  ins (S (S n)) (f (S n) (f n a))
                    =⟪ ap (ins (S (S n))) (ap (f (S n)) (wc n a (lift-point C a₀ n))) ⟫
                  ins (S (S n)) (lift-point C a₀ (S (S n)))
                    =⟪ ! (glue (S n) (lift-point C a₀ (S n))) ⟫
                  ins (S n) (lift-point C a₀ (S n))
                    =⟪ ! (ap (ins (S n)) (wc n a (lift-point C a₀ n))) ⟫
                  ins (S n) (f n a)
                    ∎∎

    {-
      Now, let us generalize:
        x   for   f n a
        y   for   lift-point C a₀ (S n)
        q   for   wc n a (lift C a₀ n)
      Then, we can show that the square commutes by induction on q.
    -}
    generalize-square : (x y : A (S n)) (q : x == y)
              → (↯
                  ins {C = C} (S n) x
                    =⟪ glue (S n) x ⟫
                  ins (S (S n)) (f (S n) x)
                    =⟪ ap (ins (S (S n))) (ap (f (S n)) q) ⟫
                  ins (S (S n)) (f (S n) y)
                    =⟪ ! (glue (S n) y) ⟫
                  ins (S n) y
                    =⟪ ! (ap (ins (S n)) q) ⟫
                  ins (S n) x
                    ∎∎
               ) == idp
    generalize-square x .x idp =
                  glue (S n) x ∙ ! (glue (S n) x) ∙ idp
                    =⟨ ap (λ q → (glue (S n) x) ∙ q) (∙-unit-r _) ⟩
                  glue (S n) x ∙ ! (glue (S n) x)
                    =⟨ !-inv-r (glue (S n) x) ⟩
                  idp
                    ∎

    {- Let us use some ad-hoc lemmas; these could all be done via
       very tedious concatenations of library lemmas.
       Of course, our ad-hoc way is somewhat ugly, but it saves a
       lot of work compared to using concatenations and nestings of
       library lemmas. The strategy is to formulate the equality
       that we need and solve it by trivial path induction.

       This ad-hoc approach is surely not the best way one can
       think of.
       The best way to do it would probably be a more principled
       approach with more powerful high-level lemmas that allow the
       manipulation of paths; however, such a technology is not
       implemented so far. -}
    adhoc-!-∙ : ∀ {i} {X : Type i} {x y z u v w o : X}
                         (p : x == y) (q : y == z) (r : u == z)
                         (s : v == u) (t : v == w) (l : w == o)
                         → (↯ x =⟪ p ⟫ y =⟪ q ⟫ z =⟪ ! (s ∙ r) ⟫ v =⟪ t ⟫ w =⟪ l ⟫ o ∎∎ )
                           ==
                           (↯ x =⟪ p ⟫ y =⟪ q ⟫ z =⟪ ! r ⟫ u =⟪ ! s ⟫ v =⟪ t ⟫ w =⟪ l ⟫ o ∎∎)
    adhoc-!-∙ idp idp idp idp idp idp = idp

    adhoc-cancel-inv : ∀ {i} {X : Type i} {x y z u v w : X}
                         (p : x == y) (q : y == z) (r : z == u)
                         (s : v == u) (t : u == w)
                         → (↯ x =⟪ p ⟫ y =⟪ q ⟫ z =⟪ r ⟫ u =⟪ ! s ⟫ v =⟪ s ⟫ u =⟪ t ⟫ w ∎∎ )
                           ==
                           (↯ x =⟪ p ⟫ y =⟪ q ⟫ z =⟪ r ⟫ u =⟪ t ⟫ w ∎∎)
    adhoc-cancel-inv idp idp idp idp idp = idp

    {- Now, we are ready to show that the heptagon is trivial! -}
    ĝ-def :  (↯ full-hepta) == idp
    ĝ-def =

      (↯ full-hepta)

        =⟨ ap (λ q → (glue (S n) (f n a))
                   ∙ ap (ins (S (S n))) (wc (S n) (f n a) (snd C n (lift-point C a₀ n)))
                   ∙ ! ((lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n))
                        ∙ glue (S n) (snd C n (lift-point C a₀ n)))
                   ∙ ! (! (lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n)))
                   ∙ ! (ap (ins (S n)) (wc n a (lift-point C a₀ n)))
                   ∙ q )
              (!-inv-l (glue n a)) ⟩

      (↯ (remove-g ⋯ (toSeq idp)))

        =⟨ ap (λ q → (glue (S n) (f n a))
                    ∙ ap (ins (S (S n))) (wc (S n) (f n a) (snd C n (lift-point C a₀ n)))
                    ∙ ! ((lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n))
                    ∙ glue (S n) (snd C n (lift-point C a₀ n)))
                    ∙ ! (! (lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n)))
                    ∙ q )
              (∙-unit-r (! (ap (ins (S n)) (wc n a (lift-point C a₀ n))))) ⟩
      (↯ remove-g)

        =⟨ ap (λ q → (glue (S n) (f n a))
                    ∙ ap (ins (S (S n))) (wc (S n) (f n a) (snd C n (lift-point C a₀ n)))
                    ∙ ! ((lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n))
                    ∙ glue (S n) (snd C n (lift-point C a₀ n)))
                    ∙ q
                    ∙ ! (ap (ins (S n)) (wc n a (lift-point C a₀ n)))
               )
               (!-! (lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n))) ⟩

      (↯ simplify-‼)

        =⟨ adhoc-!-∙
              (glue (S n) (f n a))
              (ap (ins (S (S n))) (wc (S n) (f n a) (snd C n (lift-point C a₀ n))))
              (glue (S n) (snd C n (lift-point C a₀ n)))
              (lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n))
              (lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n))
              (! (ap (ins (S n)) (wc n a (lift-point C a₀ n)))) ⟩
      (↯ simplify-one-g)
        =⟨ adhoc-cancel-inv
             (glue (S n) (f n a))
             (ap (ins (S (S n))) (wc (S n) (f n a) (snd C n (lift-point C a₀ n))))
             (! (glue (S n) (snd C n (lift-point C a₀ n))))
             (lift-point-= C a₀ n ∙ glue n (lift-point C a₀ n))
             (! (ap (ins (S n)) (wc n a (lift-point C a₀ n)))) ⟩

      (↯ simplify-many-g)

        =⟨ ap (λ q → (glue (S n) (f n a))
                    ∙ q
                    ∙ ! (glue (S n) (snd C n (lift-point C a₀ n)))
                    ∙ ! (ap (ins (S n)) (wc n a (lift-point C a₀ n)))
               )
               (ap-wconst (ins (S (S n)))
                          (ins-wconst (S (S n)))
                          (wc (S n) (f n a) (snd C n (lift-point C a₀ n)))
                          (ap (f (S n)) (wc n a (lift-point C a₀ n)))
               ) ⟩

      (↯ replace-ap-SSn)

        =⟨ generalize-square (f n a) (lift-point C a₀ (S n)) (wc n a (lift-point C a₀ n)) ⟩

      idp
        ∎

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text: module FormalLanguage.ContextFreeGrammar where

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:
-- Andreas, 2015-02-13
-- Termination errors in parametrized modules

module Issue1429 (A : Set) (f : A → A) where

  test : A → A
  test a = test (f a)

-- should report problematic call
--
--     test (f a)
--
-- not
--
--     test (f₁ a)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


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

module Algebra.Construct.Sign where

open import Prelude

data Signed {a} (A : Type a) : Type a where
  ⁻_ : A → Signed A
  ±0 : Signed A
  ⁺_ : A → Signed A

unsign : (A → B) → B → (A → B) → Signed A → B
unsign f g h (⁻ x) = f x
unsign f g h ±0 = g
unsign f g h (⁺ x) = h x

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


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

open import HoTT

{-
This file contains three proofs of Ω(S¹) = ℤ and the fact that the circle is
a 1-type:
- Something closely related to Mike’s original proof
- Dan’s encode-decode proof
- Guillaume’s proof using the flattening lemma.
This file is divided in a lot of different parts so that common parts can be
factored:

1. Definition of the universal cover and the encoding map (this part is common
   to all three proofs)
2. Proof that [encode (loop^ n) == n] (this part is common to Mike’s proof and
   the encode-decode proof)
3. Dan’s encode-decode proof that [Ω S¹ ≃ ℤ]
4. Mike’s proof that [Σ S¹ Cover] is contractible
5. Proof with the flattening lemma that [Σ S¹ S¹Cover] is contractible
6. Proof of [Ω S¹ ≃ ℤ] using the fact that [Σ S¹ S¹Cover] is contractible (common
   to Mike’s proof and the flattening lemma proof)
7. Encode-decode proof of the whole equivalence
8. Proof that the circle is a 1-type (common to all three proofs)

Keep
- 1, 2, 3    for the encode-decode proof    (+ 7, 8 for S¹ is a 1-type)
- 1, 2, 4, 6 for Mike’s proof               (+ 8)
- 1, 5, 6    for the flattening lemma proof (+ 8)
-}

module homotopy.LoopSpaceCircle where

{- 1. Universal cover and encoding map (common to all three proofs) -}

module S¹Cover = S¹RecType ℤ succ-equiv

S¹Cover : S¹ → Type₀
S¹Cover = S¹Cover.f

encode : {x : S¹} (p : base == x) → S¹Cover x
encode p = transport S¹Cover p 0

{- 2. Encoding [loop^ n] (common to Mike’s proof and the encode-decode proof) -}

-- We define the element of [Ω S¹] which is supposed to correspond to an
-- integer [n], this is the loop winding around the circle [n] times.
-- This is easy by induction on [n]
loop^ : (n : ℤ) → base == base
loop^ (pos O) = idp
loop^ (pos (S n)) = loop^ (pos n) ∙ loop
loop^ (negsucc O) = ! loop
loop^ (negsucc (S n)) = loop^ (negsucc n) ∙ (! loop)

-- Compatibility of [loop^] with the successor function
-- This is again not difficult by induction on [n]
loop^succ : (n : ℤ) → loop^ n ∙ loop == loop^ (succ n)
loop^succ (pos n) = idp
loop^succ (negsucc O) = !-inv-l loop
loop^succ (negsucc (S n)) =
  (loop^ (negsucc n) ∙ ! loop) ∙ loop
        =⟨ ∙-assoc (loop^ (negsucc n)) (! loop) loop ⟩
   loop^ (negsucc n) ∙ (! loop ∙ loop)
        =⟨ !-inv-l loop |in-ctx (λ u → loop^ (negsucc n) ∙ u) ⟩
   loop^ (negsucc n) ∙ idp
        =⟨ ∙-unit-r _ ⟩
   loop^ (negsucc n) ∎

-- Now we check that encoding [loop^ n] gives indeed [n], again by induction
-- on [n]
encode-loop^ : (n : ℤ) → encode (loop^ n) == n
encode-loop^ (pos O) = idp
encode-loop^ (pos (S n)) =
  encode (loop^ (pos n) ∙ loop) =⟨ idp ⟩
  coe (ap S¹Cover (loop^ (pos n) ∙ loop)) 0
       =⟨ ap-∙ S¹Cover (loop^ (pos n)) loop |in-ctx (λ u → coe u 0) ⟩
  coe (ap S¹Cover (loop^ (pos n)) ∙ ap S¹Cover loop) 0
       =⟨ coe-∙ (ap S¹Cover (loop^ (pos n)))
                (ap S¹Cover loop) 0 ⟩
  coe (ap S¹Cover loop) (coe (ap S¹Cover (loop^ (pos n))) 0)
       =⟨ encode-loop^ (pos n) |in-ctx coe (ap S¹Cover loop) ⟩
  coe (ap S¹Cover loop) (pos n)
       =⟨ S¹Cover.coe-loop-β (pos n) ⟩
  pos (S n) ∎
encode-loop^ (negsucc O) =
  coe (ap S¹Cover (! loop)) 0 =⟨ coe-ap-! S¹Cover loop 0 ⟩
  coe! (ap S¹Cover loop) 0 =⟨ S¹Cover.coe!-loop-β 0 ⟩
  negsucc O ∎
encode-loop^ (negsucc (S n)) =
  encode (loop^ (negsucc n) ∙ ! loop) =⟨ idp ⟩
  coe (ap S¹Cover (loop^ (negsucc n) ∙ ! loop)) 0
       =⟨ ap-∙ S¹Cover (loop^ (negsucc n)) (! loop)
          |in-ctx (λ u → coe u 0) ⟩
  coe (ap S¹Cover (loop^ (negsucc n)) ∙ ap S¹Cover (! loop)) 0
       =⟨ coe-∙ (ap S¹Cover (loop^ (negsucc n)))
                (ap S¹Cover (! loop)) 0 ⟩
  coe (ap S¹Cover (! loop)) (coe (ap S¹Cover (loop^ (negsucc n))) 0)
       =⟨ encode-loop^ (negsucc n) |in-ctx coe (ap S¹Cover (! loop)) ⟩
  coe (ap S¹Cover (! loop)) (negsucc n)
       =⟨ coe-ap-! S¹Cover loop (negsucc n) ⟩
  coe! (ap S¹Cover loop) (negsucc n)
       =⟨ S¹Cover.coe!-loop-β (negsucc n) ⟩
  negsucc (S n) ∎

{- 3. Dan’s encode-decode proof -}

-- The decoding function at [base] is [loop^], but we extend it to the whole
-- of [S¹] so that [decode-encode] becomes easier (and we need [loop^succ] to
-- be able to extend it)
decode : (x : S¹) → (S¹Cover x → base == x)
decode =
  S¹-elim loop^ (↓-→-in (λ {n} q →
                 ↓-cst=idf-in
                   (loop^succ n ∙ ap loop^ (S¹Cover.↓-loop-out q))))

decode-encode : (x : S¹) (p : base == x) → decode x (encode p) == p
decode-encode _ p = J (λ x p → decode x (encode p) == p) idp p  -- Magic!

-- And we get the theorem
ΩS¹≃ℤ : (base == base) ≃ ℤ
ΩS¹≃ℤ = equiv encode (decode base) encode-loop^ (decode-encode base)

{- 4. Mike’s proof that [Σ S¹ Cover] is contractible -}

-- We want to prove that every point of [Σ S¹ S¹Cover] is equal to [(base , O)]
paths-mike : (xt : Σ S¹ S¹Cover) → (base , 0) == xt
paths-mike (x , t) = paths-mike-c x t where

  -- We do it by circle-induction on the first component. When it’s [base],
  -- we use the [↓-loop^] below (which is essentially [encode-loop^]) and
  -- for [loop] we use [loop^succ] and the fact that [ℤ] is a set.
  paths-mike-c : (x : S¹) (t : S¹Cover x) → (base , 0) == (x , t) :> Σ S¹ S¹Cover
  paths-mike-c = S¹-elim
    (λ n → pair= (loop^ n) (↓-loop^ n))
    (↓-Π-in (λ {n} {n'} q →
     ↓-cst=idf-in
       (pair= (loop^ n) (↓-loop^ n) ∙ pair= loop q
                  =⟨ Σ-∙ (↓-loop^ n) q ⟩
        pair= (loop^ n ∙ loop) (↓-loop^ n ∙ᵈ q)
                  =⟨ pair== (loop^succ n ∙ ap loop^ (S¹Cover.↓-loop-out q))
                            (set-↓-has-all-paths-↓ ℤ-is-set) ⟩
        pair= (loop^ n') (↓-loop^ n') ∎))) where

    ↓-loop^ : (n : ℤ) → 0 == n [ S¹Cover ↓ loop^ n ]
    ↓-loop^ n = from-transp _ _ (encode-loop^ n)

contr-mike : is-contr (Σ S¹ S¹Cover)
contr-mike = ((base , 0) , paths-mike)

{- 5. Flattening lemma proof that [Σ S¹ Cover] is contractible -}

--We import the flattening lemma for the universal cover of the circle
--open FlatteningS¹ ℤ succ-equiv
open S¹Cover using (module Wt; Wt; cct; ppt; flattening-S¹)

-- We prove that the flattened HIT corresponding to the universal cover of the
-- circle (the real line) is contractible
Wt-is-contr : is-contr Wt
Wt-is-contr = (cct tt 0 , Wt.elim (base* ∘ snd) (loop* ∘ snd)) where

  -- This is basically [loop^]
  base* : (n : ℤ) → cct tt 0 == cct tt n
  base* (pos O) = idp
  base* (pos (S n)) = base* (pos n) ∙ ppt tt (pos n)
  base* (negsucc O) = ! (ppt tt (negsucc O))
  base* (negsucc (S n)) = base* (negsucc n) ∙ ! (ppt tt (negsucc (S n)))

  loop* : (n : ℤ)
    → base* n == base* (succ n) [ (λ x → cct tt 0 == x) ↓ ppt tt n ]
  loop* n = ↓-cst=idf-in (aux n) where

    -- This is basically [loop^succ]
    aux : (n : ℤ) → base* n ∙ ppt tt n == base* (succ n)
    aux (pos n) = idp
    aux (negsucc O) = !-inv-l (ppt tt (negsucc O))
    aux (negsucc (S n)) =
      base* (negsucc (S n)) ∙ ppt tt (negsucc (S n))
                =⟨ idp ⟩
      (base* (negsucc n) ∙ ! (ppt tt (negsucc (S n)))) ∙ ppt tt (negsucc (S n))
                =⟨ ∙-assoc (base* (negsucc n)) _ _ ⟩
      base* (negsucc n) ∙ (! (ppt tt (negsucc (S n))) ∙ ppt tt (negsucc (S n)))
                =⟨ !-inv-l (ppt tt (negsucc (S n)))
                       |in-ctx (λ u → base* (negsucc n) ∙ u) ⟩
      base* (negsucc n) ∙ idp
                =⟨ ∙-unit-r _ ⟩
      base* (negsucc n) ∎

-- Then, using the flattening lemma we get that the total space of [Cover] is
-- contractible
contr-flattening : is-contr (Σ S¹ S¹Cover)
contr-flattening = transport! is-contr flattening-S¹ Wt-is-contr

{- 6. Proof that [Ω S¹ ≃ ℤ] using the fact that [Σ S¹ Cover] is contractible -}

tot-encode : Σ S¹ (λ x → base == x) → Σ S¹ S¹Cover
tot-encode (x , y) = (x , encode y)

-- The previous map induces an equivalence on the total spaces, because both
-- total spaces are contractible
total-is-equiv : is-equiv tot-encode
total-is-equiv = contr-to-contr-is-equiv _ (pathfrom-is-contr base) contr-flattening

-- Hence it’s an equivalence fiberwise
postulate  -- TODO, will be only one line using the fact that an equivalence on
           -- total spaces induces an equivalence fiberwise
  encode-is-equiv : (x : S¹) → is-equiv (encode {x})

-- We can then conclude that the loop space of the circle is equivalent to [ℤ]
ΩS¹≃ℤ' : (base == base) ≃ ℤ
ΩS¹≃ℤ' = (encode {base} , encode-is-equiv base)

{- 7. Encode-decode proof of the whole fiberwise equivalence -}

-- This is quite similar to [paths-mike], we’re doing it by circle-induction,
-- the base case is [encode-loop^] and the loop case is using the fact that [ℤ]
-- is a set (and [loop^succ] is already used in [decode])
encode-decode : (x : S¹) (t : S¹Cover x) → encode (decode x t) == t
encode-decode =
  S¹-elim {P = λ x → (t : S¹Cover x) → encode (decode x t) == t}
    encode-loop^ (↓-Π-in (λ q → prop-has-all-paths-↓ (ℤ-is-set _ _)))

encode-is-equiv' : (x : S¹) → is-equiv (encode {x})
encode-is-equiv' x = is-eq encode (decode x) (encode-decode x) (decode-encode x)

{- 8. Proof that the circle is a 1-type -}

S¹Cover-is-set : (y : S¹) → is-set (S¹Cover y)
S¹Cover-is-set = S¹-elim ℤ-is-set (prop-has-all-paths-↓ is-set-is-prop)

ΩS¹-is-set : (y : S¹) → is-set (base == y)
ΩS¹-is-set y = equiv-preserves-level ((encode {y} , encode-is-equiv y) ⁻¹)
                                     (S¹Cover-is-set y)

S¹-level : has-level 1 S¹
S¹-level =
  S¹-elim ΩS¹-is-set (prop-has-all-paths-↓ (Π-level (λ x → is-set-is-prop)))

max_stars_repo_name: cmknapp/HoTT-Agda

max_issues_repo_name: cmknapp/HoTT-Agda

max_forks_repo_name: cmknapp/HoTT-Agda


text:
open import FRP.JS.Bool using ( Bool ; _∨_ ; not )
open import FRP.JS.True using ( True )
open import FRP.JS.Maybe using ( Maybe )
open import FRP.JS.Float using ( ℝ ) renaming ( _/?_ to _/?r_ )
open import FRP.JS.Primitive using ( ℕ ; String )

module FRP.JS.Int where

infixr 4 _≤_ _<_ _≟_
infixl 6 _+_ _-_
infixl 7 _*_ _/_ _/?_

open import FRP.JS.Primitive public using ( ℤ )

private
 primitive
  primIntegerPlus     : ℤ -> ℤ -> ℤ
  primIntegerMinus    : ℤ -> ℤ -> ℤ
  primIntegerTimes    : ℤ -> ℤ -> ℤ
  primIntegerDiv      : ℤ -> ℤ -> ℤ
  primIntegerMod      : ℤ -> ℤ -> ℤ
  primIntegerEquality : ℤ -> ℤ -> Bool
  primIntegerLess     : ℤ -> ℤ -> Bool
  primIntegerToFloat  : ℤ -> ℝ
  primIntegerAbs      : ℤ -> ℕ
  primShowInteger     : ℤ -> String
  primNatToInteger    : ℕ → ℤ
  primFloatDiv        : ℝ → ℝ → ℝ

_+_   = primIntegerPlus
_-_   = primIntegerMinus
_*_   = primIntegerTimes
_%_   = primIntegerMod
_≟_  = primIntegerEquality
_<_   = primIntegerLess
float = primIntegerToFloat
abs   = primIntegerAbs
show  = primShowInteger

{-# COMPILED_JS _+_   function(x) { return function(y) { return x + y; }; } #-}
{-# COMPILED_JS _-_   function(x) { return function(y) { return x - y; }; } #-}
{-# COMPILED_JS _*_   function(x) { return function(y) { return x * y; }; } #-}
{-# COMPILED_JS _%_   function(x) { return function(y) { if (x < 0) { return (x % y) + x; } else { return x % y; } }; } #-}
{-# COMPILED_JS _≟_  function(x) { return function(y) { return x === y; }; } #-}
{-# COMPILED_JS _<_   function(x) { return function(y) { return x < y; }; } #-}
{-# COMPILED_JS float function(x) { return x; } #-}
{-# COMPILED_JS abs   function(x) { return Math.abs(x); } #-}
{-# COMPILED_JS show  function(x) { return x.toString(); } #-}

+0 = primNatToInteger 0
+1 = primNatToInteger 1
-1 = +0 - +1

-_ : ℤ → ℤ
- x = +0 - x

_≤_ : ℤ → ℤ → Bool
x ≤ y = (x < y) ∨ (x ≟ y)

_≠_ : ℤ → ℤ → Bool
x ≠ y = not (x ≟ y)

_/_ : (x y : ℤ) → {y≠0 : True (y ≠ +0)} → ℝ
x / y = primFloatDiv (float x) (float y)

_/?_ : ℤ → ℤ → Maybe ℝ
x /? y = (float x) /?r (float y)

{-# COMPILED_JS _/_ function(x) { return function(y) { return x / y; }; } #-}
{-# COMPILED_JS _≤_ function(x) { return function(y) { return x <= y; }; } #-}
{-# COMPILED_JS _≠_ function(x) { return function(y) { return x !== y; }; } #-}
{-# COMPILED_JS _/_  function(x) { return function(y) { return function() { return x / y; }; }; } #-}
{-# COMPILED_JS _/?_  function(x) { return function(y) { if (y === 0) { return null; } else { return x / y; } }; } #-}

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
{-
  Define finitely generated ideals of commutative rings and
  show that they are an ideal.
  Parts of this should be reusable for explicit constructions
  of free modules over a finite set.
-}
{-# OPTIONS --safe #-}
module Cubical.Algebra.CommRing.FGIdeal where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Transport
open import Cubical.Foundations.HLevels

open import Cubical.Data.Sigma
open import Cubical.Data.FinData hiding (elim ; rec)
open import Cubical.Data.Nat renaming ( zero to ℕzero ; suc to ℕsuc
                                      ; _+_ to _+ℕ_ ; _·_ to _·ℕ_
                                      ; +-assoc to +ℕ-assoc ; +-comm to +ℕ-comm
                                      ; ·-assoc to ·ℕ-assoc ; ·-comm to ·ℕ-comm)
                             hiding (elim)
open import Cubical.HITs.PropositionalTruncation

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.Ring.QuotientRing
open import Cubical.Algebra.Ring.Properties
open import Cubical.Algebra.Ring.BigOps
open import Cubical.Algebra.RingSolver.ReflectionSolving
open import Cubical.Algebra.Matrix

private
  variable
    ℓ : Level

module _ (Ring@(R , str) : CommRing ℓ) where
  infixr 5 _holds
  _holds : hProp ℓ → Type ℓ
  P holds = fst P
  open CommRingStr str
  open RingTheory (CommRing→Ring Ring)
  open Sum (CommRing→Ring Ring)

  linearCombination : {n : ℕ} → FinVec R n → FinVec R n → R
  linearCombination α V = ∑ (λ i → α i · V i)

  sumDist+ : ∀ {n : ℕ} (α β V : FinVec R n)
           → linearCombination (λ i → α i + β i) V ≡ linearCombination α V + linearCombination β V
  sumDist+ α β V = ∑Ext (λ i → ·Ldist+ (α i) (β i) (V i)) ∙ ∑Split (λ i → α i · V i) (λ i → β i · V i)

  dist- : ∀ {n : ℕ} (α V : FinVec R n)
        → linearCombination (λ i → - α i) V ≡ - linearCombination α V
  dist- α V = ∑Ext (λ i → -DistL· (α i) (V i)) ∙ ∑Dist- (λ i → α i · V i)

  dist0 : ∀ {n : ℕ} (V : FinVec R n)
        → linearCombination (replicateFinVec n 0r) V ≡ 0r
  dist0 {n = n} V = ∑Ext (λ i → 0LeftAnnihilates (V i)) ∙ ∑0r n

  isLinearCombination : {n : ℕ} → FinVec R n → R → Type ℓ
  isLinearCombination V x = ∃[ α ∈ FinVec R _ ] x ≡ linearCombination α V

  {- If x and y are linear combinations of l, then (x + y) is
     a linear combination. -}
  isLinearCombination+ : {n : ℕ} {x y : R} (V : FinVec R n)
                         → isLinearCombination V x
                         → isLinearCombination V y
                         → isLinearCombination V (x + y)
  isLinearCombination+ V = map2 λ α β → (λ i → α .fst i + β .fst i)
                                       , cong₂ (_+_) (α .snd) (β .snd) ∙ sym (sumDist+ _ _ V)

  {- If x is a linear combinations of l, then -x is
     a linear combination. -}
  isLinearCombination- : {n : ℕ} {x : R} (V : FinVec R n)
                       → isLinearCombination V x → isLinearCombination V (- x)
  isLinearCombination- V = map λ α → (λ i → - α .fst i) , cong (-_) (α .snd) ∙ sym (dist- _ V)

  {- 0r is the trivial linear Combination -}
  isLinearCombination0 : {n : ℕ} (V : FinVec R n)
                       → isLinearCombination V 0r
  isLinearCombination0 V = ∣ _ , sym (dist0 V) ∣

  {- Linear combinations are stable under left multiplication -}
  isLinearCombinationL· : {n : ℕ} (V : FinVec R n) (r : R) {x : R}
                        → isLinearCombination V x → isLinearCombination V (r · x)
  isLinearCombinationL· V r = map λ α → (λ i → r · α .fst i) , cong (r ·_) (α .snd)
                                                            ∙∙ ∑Mulrdist r (λ i → α .fst i · V i)
                                                            ∙∙ ∑Ext λ i → ·Assoc r (α .fst i) (V i)

  generatedIdeal : {n : ℕ} → FinVec R n → IdealsIn Ring
  generatedIdeal V = makeIdeal Ring
                               (λ x → isLinearCombination V x , isPropPropTrunc)
                               (isLinearCombination+ V)
                               (isLinearCombination0 V)
                               λ r → isLinearCombinationL· V r

open CommIdeal.isCommIdeal
genIdeal : {n : ℕ} (R : CommRing ℓ) → FinVec (fst R) n → CommIdeal.CommIdeal R
fst (genIdeal R V) x = isLinearCombination R V x , isPropPropTrunc
+Closed (snd (genIdeal R V)) = isLinearCombination+ R V
contains0 (snd (genIdeal R V)) = isLinearCombination0 R V
·Closed (snd (genIdeal R V)) r = isLinearCombinationL· R V r

syntax genIdeal R V = ⟨ V ⟩[ R ]

FGIdealIn : (R : CommRing ℓ) → Type (ℓ-suc ℓ)
FGIdealIn R = Σ[ I ∈ CommIdeal.CommIdeal R ]
                   ∃[ nV ∈ Σ[ n ∈ ℕ ] FinVec (fst R) n ] I ≡ ⟨ nV .snd ⟩[ R ]

-- The lattice laws
module _ (R' : CommRing ℓ) where
 open CommRingStr (snd R')
 open RingTheory (CommRing→Ring R')
 open CommIdeal R'
 open Sum (CommRing→Ring R')
 open KroneckerDelta (CommRing→Ring R')
 private
  R = fst R'
  ⟨_⟩ : {n : ℕ} → FinVec R n → CommIdeal
  ⟨ V ⟩ = ⟨ V ⟩[ R' ]

 inclOfFGIdeal : {n : ℕ} (V : FinVec R n) (I : CommIdeal)
     → (∀ i → V i ∈ I) → ⟨ V ⟩ ⊆ I
 inclOfFGIdeal V I ∀i→Vi∈I x = elim (λ _ → I .fst x .snd) inclOfFGIdealΣ
  where
  inclOfFGIdealΣ : Σ[ α ∈ FinVec R _ ] x ≡ linearCombination R' α V → x ∈ I
  inclOfFGIdealΣ (α , x≡α·V) = subst-∈ I (sym x≡α·V) (∑Closed I (λ i → α i · V i)
                             λ i → ·Closed (I .snd) _ (∀i→Vi∈I i))

 indInIdeal : ∀ {n : ℕ} (U : FinVec R n) (i : Fin n) → U i ∈ ⟨ U ⟩
 indInIdeal U i = ∣ (δ i) , sym (∑Mul1r _ U i) ∣

 sucIncl : ∀ {n : ℕ} (U : FinVec R (ℕsuc n)) → ⟨ U ∘ suc ⟩ ⊆ ⟨ U ⟩
 sucIncl U x = map λ (α , x≡∑αUsuc) → (λ { zero → 0r ; (suc i) → α i }) , x≡∑αUsuc ∙ path _ _
  where
  path : ∀ s u₀ → s ≡ 0r · u₀ + s
  path = solve R'

 emptyFGIdeal : ∀ (V : FinVec R 0) → ⟨ V ⟩ ≡ 0Ideal
 emptyFGIdeal V = CommIdeal≡Char (λ _ →  rec (is-set _ _) snd)
                                 (λ _ x≡0 → ∣ (λ ()) , x≡0 ∣)

 0FGIdealLIncl : {n : ℕ} → ⟨ replicateFinVec n 0r ⟩ ⊆ 0Ideal
 0FGIdealLIncl x = elim (λ _ → is-set _ _)
         λ (α , x≡∑α0) → subst-∈ 0Ideal (sym x≡∑α0) (∑Closed 0Ideal (λ i → α i · 0r)
         λ i → subst-∈ 0Ideal (sym (0RightAnnihilates _)) refl)

 0FGIdealRIncl : {n : ℕ} → 0Ideal ⊆ ⟨ replicateFinVec n 0r ⟩
 0FGIdealRIncl x x≡0 = subst-∈ ⟨ replicateFinVec _ 0r ⟩ (sym x≡0)
                        (⟨ replicateFinVec _ 0r ⟩ .snd .contains0)

 0FGIdeal : {n : ℕ} → ⟨ replicateFinVec n 0r ⟩ ≡ 0Ideal
 0FGIdeal = CommIdeal≡Char 0FGIdealLIncl 0FGIdealRIncl

 FGIdealAddLemmaLIncl : {n m : ℕ} (U : FinVec R n) (V : FinVec R m)
                      → ⟨ U ++Fin V ⟩ ⊆ (⟨ U ⟩ +i ⟨ V ⟩)
 FGIdealAddLemmaLIncl {n = ℕzero} U V x x∈⟨V⟩ =
                                  ∣ (0r , x) , ⟨ U ⟩ .snd .contains0 , x∈⟨V⟩ , sym (+Lid x) ∣
 FGIdealAddLemmaLIncl {n = ℕsuc n} U V x = rec isPropPropTrunc helperΣ
   where
   helperΣ : Σ[ α ∈ FinVec R _ ] (x ≡ ∑ λ i → α i · (U ++Fin V) i) → x ∈ (⟨ U ⟩ +i ⟨ V ⟩)
   helperΣ (α , p) = subst-∈ (⟨ U ⟩ +i ⟨ V ⟩) (sym p)
                              ((⟨ U ⟩ +i ⟨ V ⟩) .snd .+Closed zeroIncl sumIncl)
    where
    zeroIncl : (α zero · U zero) ∈ (⟨ U ⟩ +i ⟨ V ⟩)
    zeroIncl = +iLincl ⟨ U ⟩ ⟨ V ⟩ (α zero · U zero)
                 (⟨ U ⟩ .snd .·Closed (α zero) (indInIdeal U zero))

    sumIncl : (∑ λ i → (α ∘ suc) i · ((U ∘ suc) ++Fin V) i) ∈ (⟨ U ⟩ +i ⟨ V ⟩)
    sumIncl = let sum = ∑ λ i → (α ∘ suc) i · ((U ∘ suc) ++Fin V) i in
         +iRespLincl ⟨ U ∘ suc ⟩ ⟨ U ⟩ ⟨ V ⟩ (sucIncl U) sum
           (FGIdealAddLemmaLIncl (U ∘ suc) V _ ∣ (α ∘ suc) , refl ∣)

 FGIdealAddLemmaRIncl : {n m : ℕ} (U : FinVec R n) (V : FinVec R m)
                      → (⟨ U ⟩ +i ⟨ V ⟩) ⊆ ⟨ U ++Fin V ⟩
 FGIdealAddLemmaRIncl U V x = rec isPropPropTrunc (uncurry3 helper)
   where
   helperΣ : ((y , z) : R × R)
           → Σ[ α ∈ FinVec R _ ] (y ≡ ∑ λ i → α i · U i)
           → Σ[ β ∈ FinVec R _ ] (z ≡ ∑ λ i → β i · V i)
           → x ≡ y + z
           → x ∈ ⟨ U ++Fin V ⟩
   helperΣ (y , z) (α , y≡∑αU) (β , z≡∑βV) x≡y+z = ∣ (α ++Fin β) , path ∣
    where
    path : x ≡ ∑ λ i → (α ++Fin β) i · (U ++Fin V) i
    path = x                                               ≡⟨ x≡y+z ⟩
           y + z                                           ≡⟨ cong₂ (_+_) y≡∑αU z≡∑βV ⟩
           (∑ λ i → α i · U i) + (∑ λ i → β i · V i)       ≡⟨ sym (∑Split++ (λ i → α i · U i) _) ⟩
           (∑ ((λ i → α i · U i) ++Fin (λ i → β i · V i))) ≡⟨ ∑Ext (mul++dist α U β V) ⟩
           (∑ λ i → (α ++Fin β) i · (U ++Fin V) i)         ∎

   helper : ((y , z) : R × R)
          → ∃[ α ∈ FinVec R _ ] (y ≡ ∑ λ i → α i · U i)
          → ∃[ β ∈ FinVec R _ ] (z ≡ ∑ λ i → β i · V i)
          → x ≡ y + z
          → x ∈ ⟨ U ++Fin V ⟩
   helper _ = rec2 (isPropΠ (λ _ → isPropPropTrunc)) (helperΣ _)

 FGIdealAddLemma : {n m : ℕ} (U : FinVec R n) (V : FinVec R m)
                 → ⟨ U ++Fin V ⟩ ≡ ⟨ U ⟩ +i ⟨ V ⟩
 FGIdealAddLemma U V = CommIdeal≡Char (FGIdealAddLemmaLIncl U V) (FGIdealAddLemmaRIncl U V)

 IdealAddAssoc :  {n m k : ℕ} (U : FinVec R n) (V : FinVec R m) (W : FinVec R k)
               → ⟨ U ++Fin (V ++Fin W) ⟩ ≡  ⟨ (U ++Fin V) ++Fin W ⟩
 IdealAddAssoc {n = n} {m = m} {k = k} U V W =
   let genIdealExpl : (n : ℕ) → FinVec R n → CommIdeal
       genIdealExpl _ V = ⟨ V ⟩
   in  cong₂ genIdealExpl (+ℕ-assoc n m k) (++FinAssoc U V W)

 ++FinComm : ∀ {n m : ℕ} (V : FinVec R n) (W : FinVec R m)
           → ⟨ V ++Fin W ⟩ ≡ ⟨ W ++Fin V ⟩
 ++FinComm V W = FGIdealAddLemma V W ∙∙ +iComm ⟨ V ⟩ ⟨ W ⟩ ∙∙ sym (FGIdealAddLemma W V)

 open ProdFin R'
 prodIn··Ideal : {n m : ℕ} (U : FinVec R n) (V : FinVec R m) (x y : R)
          → (x ∈ ⟨ U ⟩) → (y ∈ ⟨ V ⟩) → (x · y) ∈ ⟨ U ··Fin V ⟩
 prodIn··Ideal {n = n} {m = m} U V x y = map2 Σhelper
  where
  Σhelper : Σ[ α ∈ FinVec R n ] x ≡ linearCombination R' α U
          → Σ[ β ∈ FinVec R m ] y ≡ linearCombination R' β V
          → Σ[ γ ∈ FinVec R (n ·ℕ m) ] (x · y) ≡ linearCombination R' γ (U ··Fin V)
  Σhelper (α , x≡∑αU) (β , y≡∑βV) = α ··Fin β , path
   where
   path : x · y ≡ ∑ λ i → (α ··Fin β) i · (U ··Fin V) i
   path = x · y ≡⟨ cong₂ (_·_) x≡∑αU y≡∑βV ⟩
          (∑ λ i → α i · U i) · (∑ λ i → β i · V i) ≡⟨ ∑Dist··Fin (λ i → α i · U i) _ ⟩
          (∑ λ j → ((λ i → α i · U i) ··Fin (λ i → β i · V i)) j) ≡⟨ ∑Ext (·Dist··Fin α U β V) ⟩
          (∑ λ i → (α ··Fin β) i · (U ··Fin V) i) ∎

 FGIdealMultLemmaLIncl : {n m : ℕ} (U : FinVec R n) (V : FinVec R m)
                       → ⟨ U ··Fin V ⟩ ⊆ (⟨ U ⟩ ·i ⟨ V ⟩)
 FGIdealMultLemmaLIncl U V x = elim (λ _ → isPropPropTrunc)
   λ (α , x≡∑αUV) → subst-∈ (⟨ U ⟩ ·i ⟨ V ⟩)  (sym x≡∑αUV) --replace x by ∑αᵢⱼUᵢVⱼ
     (∑Closed (⟨ U ⟩ ·i ⟨ V ⟩) (λ i → α i · (U ··Fin V) i) --show that each αᵢ(U··V)ᵢ is in product
       λ i → (⟨ U ⟩ ·i ⟨ V ⟩) .snd .·Closed (α i) --drop the α's
         (flattenElim {P = _∈ (⟨ U ⟩ ·i ⟨ V ⟩)} (toMatrix U V) --show theat UᵢVⱼ is in product
           (λ j k → prodInProd ⟨ U ⟩ ⟨ V ⟩ (U j) (V k) (indInIdeal U j) (indInIdeal V k)) i))

 FGIdealMultLemmaRIncl : {n m : ℕ} (U : FinVec R n) (V : FinVec R m)
                       → (⟨ U ⟩ ·i ⟨ V ⟩) ⊆ ⟨ U ··Fin V ⟩
 FGIdealMultLemmaRIncl U V x = elim (λ _ → isPropPropTrunc)
   λ (_ , (α , β) , ∀α∈⟨U⟩ , ∀β∈⟨V⟩ , x≡∑αβ) → subst-∈ ⟨ U ··Fin V ⟩ (sym x≡∑αβ)
     (∑Closed ⟨ U ··Fin V ⟩ _ (λ i → prodIn··Ideal U V (α i) (β i) (∀α∈⟨U⟩ i) (∀β∈⟨V⟩ i)))

 FGIdealMultLemma : {n m : ℕ} (U : FinVec R n) (V : FinVec R m)
                 → ⟨ U ··Fin V ⟩ ≡ ⟨ U ⟩ ·i ⟨ V ⟩
 FGIdealMultLemma U V = CommIdeal≡Char (FGIdealMultLemmaLIncl U V) (FGIdealMultLemmaRIncl U V)

max_stars_repo_name: dolio/cubical

max_issues_repo_name: dolio/cubical

max_forks_repo_name: dolio/cubical


text:
open import MJ.Types as Types
import MJ.Classtable.Core as Core

module MJ.Semantics.Objects {c}(Ct : Core.Classtable c) where

open import Prelude

open import Level renaming (suc to lsuc; zero to lzero)
open import Data.List
open import Data.List.Relation.Unary.All
open import Data.List.Prefix

open Core c
open Classtable Ct

open import MJ.Classtable.Membership Ct
open import MJ.Semantics.Values Ct
open import MJ.LexicalScope c

{-
Abstract interface for object encodings.
-}
record ObjEncoding : Set (lsuc lzero) where
  field
    Obj : World c → Cid c → Set
    weaken-obj : ∀ {W W'} cid → W' ⊒ W → Obj W cid → Obj W' cid
    getter : ∀ {W m a} c → Obj W c → IsMember c FIELD m a → Val W a
    setter : ∀ {W m a} c → Obj W c → IsMember c FIELD m a → Val W a → Obj W c
    defaultObject : ∀ {W} c → Obj W c

  data StoreVal (W : World c) : Ty⁺ c → Set where
    val : ∀ {ty} → Val W ty → StoreVal W (vty ty)
    obj : ∀ cid → Obj W cid → StoreVal W (obj cid)

  Store : World c → Set
  Store W = All (StoreVal W) W


text:
postulate
  Nat : Set
  Fin : Nat → Set
  Foo : (n : Nat) → Fin n → Set

private
 module M where

  variable
    n : Nat
    m : Fin _

  postulate
    Bar : Foo n m → Set

open M public using (Bar)

variable
  n : Nat
  m : Fin _
  l : Foo n m

before : Bar l
before {n} {m} {l} = {!C-c C-e!}

after : Bar l
after {n} {m} {l} = {!C-c C-e!}

max_stars_repo_name: hborum/agda

max_issues_repo_name: hborum/agda

max_forks_repo_name: hborum/agda


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

module Cubical.Algebra.CommRing.Instances.UnivariatePoly where

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

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.Polynomials.Univariate.Base
open import Cubical.Algebra.Polynomials.Univariate.Properties

private
  variable
    ℓ : Level

UnivariatePoly : (CommRing ℓ) → CommRing ℓ
UnivariatePoly R = (PolyMod.Poly R) , str
    where
      open CommRingStr --(snd R)
      str : CommRingStr (PolyMod.Poly R)
      0r str = PolyModTheory.0P R
      1r str = PolyModTheory.1P R
      _+_ str = PolyModTheory._Poly+_ R
      _·_ str = PolyModTheory._Poly*_ R
      - str = PolyModTheory.Poly- R
      isCommRing str = makeIsCommRing (PolyMod.isSetPoly R)
                                      (PolyModTheory.Poly+Assoc R)
                                      (PolyModTheory.Poly+Rid R)
                                      (PolyModTheory.Poly+Inverses R)
                                      (PolyModTheory.Poly+Comm  R)
                                      (PolyModTheory.Poly*Associative R)
                                      (PolyModTheory.Poly*Rid R)
                                      (PolyModTheory.Poly*LDistrPoly+ R)
                                      (PolyModTheory.Poly*Commutative R)

nUnivariatePoly : (A' : CommRing ℓ) → (n : ℕ) → CommRing ℓ
nUnivariatePoly A' zero = A'
nUnivariatePoly A' (suc n) = UnivariatePoly (nUnivariatePoly A' n)

max_stars_repo_name: guilhermehas/cubical

max_issues_repo_name: guilhermehas/cubical

max_forks_repo_name: guilhermehas/cubical


text:
module Utils.NatOrdLemmas where

open import Data.Nat.Properties.Simple
open import Data.Nat
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Function

{- Just a bunch of lemmas about the standard ordering on naturals -}

data Cmp (a b : ℕ) : Set where
  LT : a Data.Nat.< b → Cmp a b
  EQ : a ≡ b → Cmp a b
  GT : a > b → Cmp a b

cmp : ∀ a b → Cmp a b
cmp zero zero = EQ refl
cmp zero (suc b) = LT (s≤s z≤n)
cmp (suc a) zero = GT (s≤s z≤n)
cmp (suc a) (suc b) with cmp a b
cmp (suc a) (suc b) | LT x = LT (s≤s x)
cmp (suc a) (suc .a) | EQ refl = EQ refl
cmp (suc a) (suc b) | GT x = GT (s≤s x)

a≮a : ∀ a → ¬ (a < a)
a≮a zero ()
a≮a (suc a) (s≤s p) = a≮a a p

<-weakenr1 : ∀ a b → a < b → a < suc b
<-weakenr1 zero b p = s≤s z≤n
<-weakenr1 (suc a) zero ()
<-weakenr1 (suc a) (suc b) (s≤s p) = s≤s (<-weakenr1 a b p)

<-weakenr : ∀ c a b → a < b → a < c + b
<-weakenr zero a b p = p
<-weakenr (suc c) a b p = <-weakenr1 a (c + b) (<-weakenr c a b p)

<-weakenl1 : ∀ a b → suc a < b → a < b
<-weakenl1 zero ._ (s≤s p) = s≤s z≤n
<-weakenl1 (suc a) zero ()
<-weakenl1 (suc a) (suc b) (s≤s p) = s≤s (<-weakenl1 a b p)

<-weakenl : ∀ c a b → c + a < b → a < b
<-weakenl zero a b p = p
<-weakenl (suc c) a b p = <-weakenl c a b (<-weakenl1 (c + a) b p)

a≢sa : (a : ℕ) → a ≢ suc a
a≢sa a ()

a<b⟶a≢sb : ∀ a b → a < b → a ≢ suc b
a<b⟶a≢sb zero b p1 ()
a<b⟶a≢sb (suc ._) ._ (s≤s p1) refl = a<b⟶a≢sb _ _ p1 refl

a<v⟶a≢c+b : ∀ c a b → a < b → a ≢ c + b
a<v⟶a≢c+b zero a .a p1 refl = a≮a a p1
a<v⟶a≢c+b (suc c) a b p1 p2 = a<b⟶a≢sb a (c + b) (<-weakenr c a b p1) p2

a<sb+a : ∀ a b → a < suc b + a
a<sb+a zero b = s≤s z≤n
a<sb+a (suc a) b rewrite +-suc b a = s≤s (a<sb+a a b)

a<b+sa : ∀ a b → a < b + suc a
a<b+sa a b rewrite +-suc b a = a<sb+a a b

≤-strict : ∀ a b → a ≤ b → a ≢ b → a < b
≤-strict zero zero z≤n p2 = ⊥-elim (p2 refl)
≤-strict zero (suc b) z≤n p2 = s≤s z≤n
≤-strict (suc a) zero () p2
≤-strict (suc a) (suc b) (s≤s p1) p2 = s≤s (≤-strict a b p1 (p2 ∘ cong suc))

a≢sa+b : ∀ a b → a ≢ suc a + b
a≢sa+b zero b ()
a≢sa+b (suc a) b p = a≢sa+b a b $ cong pred p

a≢sb+a : ∀ a b → a ≢ suc b + a
a≢sb+a a b p rewrite +-comm b a = a≢sa+b a b p

max_stars_repo_name: AndrasKovacs/SemanticsWithApplications

max_issues_repo_name: AndrasKovacs/SemanticsWithApplications

max_forks_repo_name: AndrasKovacs/SemanticsWithApplications


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

open import HoTT
open import homotopy.PtdMapSequence
open import groups.HomSequence
open import cohomology.Theory

module cohomology.PtdMapSequence {i} (CT : CohomologyTheory i) where

  open CohomologyTheory CT

  -- FIXME maybe this should be named [ap-C-seq],
  -- but I do not know how to name [C-seq-isemap]. -favonia

  C-seq : ∀ {X Y : Ptd i} (n : ℤ)
    → PtdMapSequence X Y
    → HomSequence (C n Y) (C n X)
  C-seq n (X ⊙⊣|) = C n X ⊣|ᴳ
  C-seq n (X ⊙→⟨ f ⟩ seq) = HomSeq-snoc (C-seq n seq) (C-fmap n f)

  C-comm-square : ∀ (n : ℤ) {X₀ X₁ Y₀ Y₁ : Ptd i}
    → {f₀ : X₀ ⊙→ Y₀} {f₁ : X₁ ⊙→ Y₁} {hX : X₀ ⊙→ X₁} {hY : Y₀ ⊙→ Y₁}
    → CommSquare (fst f₀) (fst f₁) (fst hX) (fst hY)
    → CommSquareᴳ (C-fmap n f₁) (C-fmap n f₀) (C-fmap n hY) (C-fmap n hX)
  C-comm-square n {f₀ = f₀} {f₁} {hX} {hY} (comm-sqr □) = comm-sqrᴳ λ y₁ →
    ∘-CEl-fmap n hX f₁ y₁ ∙ CEl-fmap-base-indep' n (λ x → ! (□ x)) y₁ ∙ CEl-fmap-∘ n hY f₀ y₁

  C-seq-fmap : ∀ {X₀ X₁ Y₀ Y₁ : Ptd i} (n : ℤ)
    {seq₀ : PtdMapSequence X₀ Y₀} {seq₁ : PtdMapSequence X₁ Y₁}
    {hX : X₀ ⊙→ X₁} {hY : Y₀ ⊙→ Y₁}
    → PtdMapSeqMap seq₀ seq₁ hX hY
    → HomSeqMap (C-seq n seq₁) (C-seq n seq₀) (C-fmap n hY) (C-fmap n hX)
  C-seq-fmap n (hX ⊙↓|) = C-fmap n hX ↓|ᴳ
  C-seq-fmap n (hX ⊙↓⟨ □ ⟩ seq) = HomSeqMap-snoc (C-seq-fmap n seq) (C-comm-square n □)

  C-seq-isemap : ∀ {X₀ X₁ Y₀ Y₁ : Ptd i} (n : ℤ)
    {seq₀ : PtdMapSequence X₀ Y₀} {seq₁ : PtdMapSequence X₁ Y₁}
    {hX : X₀ ⊙→ X₁} {hY : Y₀ ⊙→ Y₁}
    {seq-map : PtdMapSeqMap seq₀ seq₁ hX hY}
    → is-⊙seq-equiv seq-map
    → is-seqᴳ-equiv (C-seq-fmap n seq-map)
  C-seq-isemap n {seq-map = h ⊙↓|} h-is-equiv = CEl-isemap n h h-is-equiv
  C-seq-isemap n {seq-map = h ⊙↓⟨ □ ⟩ seq} (h-is-equiv , seq-is-equiv) =
    is-seqᴳ-equiv-snoc (C-seq-isemap n seq-is-equiv) (CEl-isemap n h h-is-equiv)

  C-seq-emap : ∀ {X₀ X₁ Y₀ Y₁ : Ptd i} (n : ℤ)
    {seq₀ : PtdMapSequence X₀ Y₀} {seq₁ : PtdMapSequence X₁ Y₁}
    {hX : X₀ ⊙→ X₁} {hY : Y₀ ⊙→ Y₁}
    → PtdMapSeqEquiv seq₀ seq₁ hX hY
    → HomSeqEquiv (C-seq n seq₁) (C-seq n seq₀) (C-fmap n hY) (C-fmap n hX)
  C-seq-emap n (seq , seq-ise) = C-seq-fmap n seq , C-seq-isemap n seq-ise

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
module Structure.Category.Equiv where

import      Lvl
open import Structure.Setoid
open import Structure.Category

-- TODO: https://en.wikipedia.org/wiki/Equivalence_of_categories

module _ {ℓₒ ℓₘ : Lvl.Level} {Obj : Type{ℓₒ}} (Morphism : Obj → Obj → Type{ℓₘ}) ⦃ morphism-equiv : ∀{x y} → Equiv(Morphism x y) ⦄ where
  Category-equiv : Equiv(Category(Morphism))
  Category-equiv


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

module Definition.Conversion.FullReduction where

open import Definition.Untyped as U hiding (wk)
open import Definition.Untyped.Properties
open import Definition.Typed
open import Definition.Typed.Properties
open import Definition.Typed.Weakening
open import Definition.Conversion
open import Definition.Conversion.Whnf
open import Definition.Typed.Consequences.InverseUniv
open import Definition.Typed.Consequences.Syntactic
open import Definition.Typed.Consequences.NeTypeEq
open import Definition.Typed.Consequences.Substitution

open import Tools.Product
import Tools.PropositionalEquality as PE

mutual
  data NfNeutral : Term → Set where
    var       : ∀ n                              → NfNeutral (var n)
    ∘ₙ        : ∀ {k u}     → NfNeutral k → Nf u → NfNeutral (k ∘ u)
    fstₙ      : ∀ {p}       → NfNeutral p        → NfNeutral (fst p)
    sndₙ      : ∀ {p}       → NfNeutral p        → NfNeutral (snd p)
    natrecₙ   : ∀ {C c g k} → Nf C → Nf c → Nf g → NfNeutral k
                                                 → NfNeutral (natrec C c g k)
    Emptyrecₙ : ∀ {C k}     → Nf C → NfNeutral k → NfNeutral (Emptyrec C k)

  data Nf : Term → Set where
    Uₙ     : Nf U
    Πₙ     : ∀ {A B} → Nf A → Nf B → Nf (Π A ▹ B)
    Σₙ     : ∀ {A B} → Nf A → Nf B → Nf (Σ A ▹ B)
    ℕₙ     : Nf ℕ
    Emptyₙ : Nf Empty
    Unitₙ  : Nf Unit

    lamₙ   : ∀ {t} → Nf t → Nf (lam t)
    prodₙ  : ∀ {t u} → Nf t → Nf u → Nf (prod t u)
    zeroₙ  : Nf zero
    sucₙ   : ∀ {t} → Nf t → Nf (suc t)
    starₙ  : Nf star

    ne     : ∀ {n} → NfNeutral n → Nf n

mutual
  fullRedNe : ∀ {t A Γ} → Γ ⊢ t ~ t ↑ A → ∃ λ u → NfNeutral u × Γ ⊢ t ≡ u ∷ A
  fullRedNe (var-refl x _) = var _ , var _ , refl x
  fullRedNe (app-cong t u) =
    let t′ , nfT′ , t≡t′ = fullRedNe~↓ t
        u′ , nfU′ , u≡u′ = fullRedTerm u
    in  (t′ ∘ u′) , (∘ₙ nfT′ nfU′) , app-cong t≡t′ u≡u′
  fullRedNe (fst-cong p~p) =
    let p′ , neP′ , p≡p′ = fullRedNe~↓ p~p
        ⊢ΣFG , _ , _ = syntacticEqTerm p≡p′
        ⊢F , ⊢G = syntacticΣ ⊢ΣFG
    in  fst p′ , fstₙ neP′ , fst-cong ⊢F ⊢G p≡p′
  fullRedNe (snd-cong p~p) =
    let p′ , neP′ , p≡p′ = fullRedNe~↓ p~p
        ⊢ΣFG , _ , _ = syntacticEqTerm p≡p′
        ⊢F , ⊢G = syntacticΣ ⊢ΣFG
    in  snd p′ , sndₙ neP′ , snd-cong ⊢F ⊢G p≡p′
  fullRedNe (natrec-cong C z s n) =
    let C′ , nfC′ , C≡C′ = fullRed C
        z′ , nfZ′ , z≡z′ = fullRedTerm z
        s′ , nfS′ , s≡s′ = fullRedTerm s
        n′ , nfN′ , n≡n′ = fullRedNe~↓ n
    in  natrec C′ z′ s′ n′ , natrecₙ nfC′ nfZ′ nfS′ nfN′
     ,  natrec-cong C≡C′ z≡z′ s≡s′ n≡n′
  fullRedNe (Emptyrec-cong C n) =
    let C′ , nfC′ , C≡C′ = fullRed C
        n′ , nfN′ , n≡n′ = fullRedNe~↓ n
    in  Emptyrec C′ n′ , Emptyrecₙ nfC′ nfN′
     ,  Emptyrec-cong C≡C′ n≡n′

  fullRedNe~↓ : ∀ {t A Γ} → Γ ⊢ t ~ t ↓ A → ∃ λ u → NfNeutral u × Γ ⊢ t ≡ u ∷ A
  fullRedNe~↓ ([~] A D whnfB k~l) =
    let u , nf , t≡u = fullRedNe k~l
    in  u , nf , conv t≡u (subset* D)

  fullRed : ∀ {A Γ} → Γ ⊢ A [conv↑] A → ∃ λ B → Nf B × Γ ⊢ A ≡ B
  fullRed ([↑] A′ B′ D D′ whnfA′ whnfB′ A′<>B′)
    rewrite whrDet* (D , whnfA′) (D′ , whnfB′) =
    let B″ , nf , B′≡B″ = fullRedConv↓ A′<>B′
    in  B″ , nf , trans (subset* D′) B′≡B″

  fullRedConv↓ : ∀ {A Γ} → Γ ⊢ A [conv↓] A → ∃ λ B → Nf B × Γ ⊢ A ≡ B
  fullRedConv↓ (U-refl ⊢Γ) = U , Uₙ , refl (Uⱼ ⊢Γ)
  fullRedConv↓ (ℕ-refl ⊢Γ) = ℕ , ℕₙ , refl (ℕⱼ ⊢Γ)
  fullRedConv↓ (Empty-refl ⊢Γ) = Empty , Emptyₙ , refl (Emptyⱼ ⊢Γ)
  fullRedConv↓ (Unit-refl ⊢Γ) = Unit , Unitₙ , refl (Unitⱼ ⊢Γ)
  fullRedConv↓ (ne A) =
    let B , nf , A≡B = fullRedNe~↓ A
    in  B , ne nf , univ A≡B
  fullRedConv↓ (Π-cong ⊢F F G) =
    let F′ , nfF′ , F≡F′ = fullRed F
        G′ , nfG′ , G≡G′ = fullRed G
    in  Π F′ ▹ G′ , Πₙ nfF′ nfG′ , Π-cong ⊢F F≡F′ G≡G′
  fullRedConv↓ (Σ-cong ⊢F F G) =
    let F′ , nfF′ , F≡F′ = fullRed F
        G′ , nfG′ , G≡G′ = fullRed G
    in  Σ F′ ▹ G′ , Σₙ nfF′ nfG′ , Σ-cong ⊢F F≡F′ G≡G′

  fullRedTerm : ∀ {t A Γ} → Γ ⊢ t [conv↑] t ∷ A → ∃ λ u → Nf u × Γ ⊢ t ≡ u ∷ A
  fullRedTerm ([↑]ₜ B t′ u′ D d d′ whnfB whnft′ whnfu′ t<>u)
    rewrite whrDet*Term (d , whnft′) (d′ , whnfu′) =
    let u″ , nf , u′≡u″ = fullRedTermConv↓ t<>u
    in  u″ , nf , conv (trans (subset*Term d′) u′≡u″) (sym (subset* D))

  fullRedTermConv↓ : ∀ {t A Γ} → Γ ⊢ t [conv↓] t ∷ A → ∃ λ u → Nf u × Γ ⊢ t ≡ u ∷ A
  fullRedTermConv↓ (ℕ-ins t) =
    let u , nf , t≡u = fullRedNe~↓ t
    in  u , ne nf , t≡u
  fullRedTermConv↓ (Empty-ins t) =
    let u , nf , t≡u = fullRedNe~↓ t
    in  u , ne nf , t≡u
  fullRedTermConv↓ (Unit-ins t) =
    let u , nf , t≡u = fullRedNe~↓ t
    in  u , ne nf , t≡u
  fullRedTermConv↓ (ne-ins ⊢t _ _ t) =
    let u , nfU , t≡u = fullRedNe~↓ t
        _ , ⊢t∷M , _ = syntacticEqTerm t≡u
        _ , neT , _ = ne~↓ t
    in  u , ne nfU , conv t≡u (neTypeEq neT ⊢t∷M ⊢t)
  fullRedTermConv↓ (univ ⊢t _ t) =
    let u , nf , t≡u = fullRedConv↓ t
    in  u , nf , inverseUnivEq ⊢t t≡u
  fullRedTermConv↓ (zero-refl ⊢Γ) = zero , zeroₙ , refl (zeroⱼ ⊢Γ)
  fullRedTermConv↓ (suc-cong t) =
    let u , nf , t≡u = fullRedTerm t
    in  suc u , sucₙ nf , suc-cong t≡u
  fullRedTermConv↓ (η-eq ⊢t _ _ _ t∘0) =
    let u , nf , t∘0≡u = fullRedTerm t∘0
        _ , _ , ⊢u = syntacticEqTerm t∘0≡u
        ⊢F , _ = syntacticΠ (syntacticTerm ⊢t)
        ΓF⊢ = wf ⊢F ∙ ⊢F
        wk⊢F = wk (step id) ΓF⊢ ⊢F
        ΓFF'⊢ = ΓF⊢ ∙ wk⊢F
        wk⊢u = wkTerm (lift (step id)) ΓFF'⊢ ⊢u
        λu∘0 = lam (U.wk (lift (step id)) u) ∘ var 0
    in  lam u , lamₙ nf
     ,  η-eq ⊢F ⊢t (lamⱼ ⊢F ⊢u)
                (trans t∘0≡u (PE.subst₂ (λ x y → _ ⊢ x ≡ λu∘0 ∷ y)
                                        (wkSingleSubstId u) (wkSingleSubstId _)
                                        (sym (β-red wk⊢F wk⊢u (var ΓF⊢ here)))))
  fullRedTermConv↓ (Σ-η ⊢t _ tProd _ fstConv sndConv) =
    let fst′ , nfFst′ , fst≡fst′ = fullRedTerm fstConv
        snd′ , nfSnd′ , snd≡snd′ = fullRedTerm sndConv
        _ , _ , ⊢fst′ = syntacticEqTerm fst≡fst′
        _ , _ , ⊢snd′₁ = syntacticEqTerm snd≡snd′
        ⊢ΣFG = syntacticTerm ⊢t
        ⊢F , ⊢G = syntacticΣ ⊢ΣFG

        Gfst≡Gfst′ = substTypeEq (refl ⊢G) fst≡fst′
        ⊢snd′ = conv ⊢snd′₁ Gfst≡Gfst′
        ⊢prod = prodⱼ ⊢F ⊢G ⊢fst′ ⊢snd′

        fstprod≡fst′ = Σ-β₁ ⊢F ⊢G ⊢fst′ ⊢snd′
        fst≡fstprod = trans fst≡fst′ (sym fstprod≡fst′)
        Gfst≡Gfstprod = substTypeEq (refl ⊢G) fst≡fstprod
        sndprod≡snd′ = conv (Σ-β₂ ⊢F ⊢G ⊢fst′ ⊢snd′) (sym Gfst≡Gfstprod)
        snd≡sndprod = trans snd≡snd′ (sym sndprod≡snd′)
    in  prod fst′ snd′ , prodₙ nfFst′ nfSnd′
      , Σ-η ⊢F ⊢G ⊢t ⊢prod fst≡fstprod snd≡sndprod
  fullRedTermConv↓ (η-unit ⊢t _ tUnit _) =
    star , starₙ , η-unit ⊢t (starⱼ (wfTerm ⊢t))


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

open import LogicalFormulae
open import Setoids.Setoids
open import Rings.Definition
open import Rings.IntegralDomains.Definition

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

module Rings.Primes.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) where

open import Rings.Divisible.Definition R
open Ring R
open Setoid S
open import Rings.Units.Definition R

record Prime (x : A) : Set (a ⊔ b) where
  field
    isPrime : (r s : A) → (x ∣ (r * s)) → ((x ∣ r) → False) → (x ∣ s)
    nonzero : (x ∼ 0R) → False
    nonunit : Unit x → False


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on characters
------------------------------------------------------------------------

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

module Data.Char.Properties where

open import Data.Bool.Base using (Bool)
open import Data.Char.Base

import Data.Nat.Base as ℕ
import Data.Nat.Properties as ℕₚ

open import Function
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable using (map′; isYes)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality.Core
import Relation.Binary.Construct.On as On
import Relation.Binary.PropositionalEquality as PropEq

------------------------------------------------------------------------
-- Primitive properties

open import Agda.Builtin.Char.Properties
  renaming ( primCharToNatInjective to toℕ-injective)
  public

------------------------------------------------------------------------
-- Properties of _≈_

≈⇒≡ : _≈_ ⇒ _≡_
≈⇒≡ = toℕ-injective _ _

≈-reflexive : _≡_ ⇒ _≈_
≈-reflexive = cong toℕ

≈-refl : Reflexive _≈_
≈-refl = refl

≈-sym : Symmetric _≈_
≈-sym = sym

≈-trans : Transitive _≈_
≈-trans = trans

≈-subst : ∀ {ℓ} → Substitutive _≈_ ℓ
≈-subst P x≈y p = subst P (≈⇒≡ x≈y) p

infix 4 _≈?_
_≈?_ : Decidable _≈_
x ≈? y = toℕ x ℕₚ.≟ toℕ y

≈-isEquivalence : IsEquivalence _≈_
≈-isEquivalence = record
  { refl  = λ {i} → ≈-refl {i}
  ; sym   = λ {i j} → ≈-sym {i} {j}
  ; trans = λ {i j k} → ≈-trans {i} {j} {k}
  }

≈-setoid : Setoid _ _
≈-setoid = record
  { isEquivalence = ≈-isEquivalence
  }

≈-isDecEquivalence : IsDecEquivalence _≈_
≈-isDecEquivalence = record
  { isEquivalence = ≈-isEquivalence
  ; _≟_           = _≈?_
  }

≈-decSetoid : DecSetoid _ _
≈-decSetoid = record
  { isDecEquivalence = ≈-isDecEquivalence
  }

------------------------------------------------------------------------
-- Properties of _≡_

infix 4 _≟_
_≟_ : Decidable {A = Char} _≡_
x ≟ y = map′ ≈⇒≡ ≈-reflexive (x ≈? y)

≡-setoid : Setoid _ _
≡-setoid = PropEq.setoid Char

≡-decSetoid : DecSetoid _ _
≡-decSetoid = PropEq.decSetoid _≟_

------------------------------------------------------------------------
-- Boolean equality test.
--
-- Why is the definition _==_ = primCharEquality not used? One reason
-- is that the present definition can sometimes improve type
-- inference, at least with the version of Agda that is current at the
-- time of writing: see unit-test below.

infix 4 _==_
_==_ : Char → Char → Bool
c₁ == c₂ = isYes (c₁ ≟ c₂)

private

  -- The following unit test does not type-check (at the time of
  -- writing) if _==_ is replaced by primCharEquality.

  data P : (Char → Bool) → Set where
    p : (c : Char) → P (c ==_)

  unit-test : P ('x' ==_)
  unit-test = p _

------------------------------------------------------------------------
-- Properties of _<_

infix 4 _<?_
_<?_ : Decidable _<_
_<?_ = On.decidable toℕ ℕ._<_ ℕₚ._<?_

<-isStrictPartialOrder-≈ : IsStrictPartialOrder _≈_ _<_
<-isStrictPartialOrder-≈ = On.isStrictPartialOrder toℕ ℕₚ.<-isStrictPartialOrder

<-isStrictTotalOrder-≈ : IsStrictTotalOrder _≈_ _<_
<-isStrictTotalOrder-≈ = On.isStrictTotalOrder toℕ ℕₚ.<-isStrictTotalOrder

<-strictPartialOrder-≈ : StrictPartialOrder _ _ _
<-strictPartialOrder-≈ = On.strictPartialOrder ℕₚ.<-strictPartialOrder toℕ

<-strictTotalOrder-≈ : StrictTotalOrder _ _ _
<-strictTotalOrder-≈ = On.strictTotalOrder ℕₚ.<-strictTotalOrder toℕ

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

-- Version 1.1

toNat-injective = toℕ-injective
{-# WARNING_ON_USAGE toℕ-injective
"Warning: toNat-injective was deprecated in v1.1.
Please use toℕ-injective instead."
#-}

setoid = ≡-setoid
{-# WARNING_ON_USAGE setoid
"Warning: setoid was deprecated in v1.1.
Please use ≡-setoid instead."
#-}

decSetoid = ≡-decSetoid
{-# WARNING_ON_USAGE decSetoid
"Warning: decSetoid was deprecated in v1.1.
Please use ≡-decSetoid instead."
#-}

strictTotalOrder = <-strictTotalOrder-≈
{-# WARNING_ON_USAGE strictTotalOrder
"Warning: strictTotalOrder was deprecated in v1.1.
Please use <-strictTotalOrder-≈ instead."
#-}


text:
module Dave.Logic.Bool where

    data Bool : Set where
        false : Bool
        true : Bool

    ¬_ : Bool → Bool
    ¬ true = false
    ¬ false = true

    _∧_ : Bool → Bool → Bool
    a ∧ true = a
    a ∧ false = false

    if_then_else_ : {A : Set} → Bool → A → A → A
    if false then a else b = b
    if true then a else b = a

    identity : {A : Set} → A → A
    identity a = a


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

open import LogicalFormulae
open import Setoids.Setoids
open import Rings.Definition
open import Rings.IntegralDomains.Definition
open import Vectors
open import Numbers.Naturals.Semiring
open import Numbers.Naturals.Order
open import Numbers.Naturals.Definition

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

module Rings.UniqueFactorisationDomains.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} (intDom : IntegralDomain R) where

open import Rings.Units.Definition R
open import Rings.Irreducibles.Definition intDom
open import Rings.Associates.Definition intDom
open import Rings.Primes.Definition intDom
open Ring R
open Setoid S

private
  power : A → ℕ → A
  power x zero = 1R
  power x (succ n) = x * power x n

  allDistinct : {n : ℕ} → Vec A n → Set (a ⊔ b)
  allDistinct [] = True'
  allDistinct (x ,- xs) = (allDistinct xs) && vecAllTrue (λ n → (n ∼ x) → False) xs

record Factorisation {r : A} .(nonzero : (r ∼ 0R) → False) .(nonunit : (Unit r) → False) : Set (a ⊔ b) where
  field
    len : ℕ
    factorise : Vec (A && ℕ) len
    factoriseIsFactorisation : vecFold (λ x y → y * power (_&&_.fst x) (succ (_&&_.snd x))) 1R factorise ∼ r
    factoriseIsIrreducibles : vecAllTrue Irreducible (vecMap _&&_.fst factorise)
    distinct : allDistinct (vecMap _&&_.fst factorise)

private
  equality : {n : ℕ} (v1 v2 : Vec (A && ℕ) n) → Set (a ⊔ b)
  equality [] [] = True'
  equality {succ n} ((a ,, an) ,- v1) v2 = Sg ℕ (λ index → Sg (index <N succ n) (λ i<n → (Associates (_&&_.fst (vecIndex v2 index i<n)) a) && ((_&&_.snd (vecIndex v2 index i<n) ≡ an) && equality v1 (vecDelete index i<n v2))))

factorisationEquality : {r : A} → .{nonzero : (r ∼ 0R) → False} → .{nonunit : (Unit r) → False} → Factorisation nonzero nonunit → Factorisation nonzero nonunit → Set (a ⊔ b)
factorisationEquality record { len = lenA ; factorise = factoriseA ; factoriseIsFactorisation = factoriseIsFactorisationA ; factoriseIsIrreducibles = factoriseIsIrreduciblesA ; distinct = distinctA } record { len = lenB ; factorise = factoriseB ; factoriseIsFactorisation = factoriseIsFactorisationB ; factoriseIsIrreducibles = factoriseIsIrreduciblesB ; distinct = distinctB } with ℕDecideEquality lenA lenB
factorisationEquality record { len = a ; factorise = factoriseA } record { len = .a ; factorise = factoriseB } | inl refl = equality factoriseA factoriseB
factorisationEquality record { len = a ; factorise = factoriseA } record { len = b ; factorise = factoriseB } | inr _ = False'

record UFD : Set (a ⊔ b) where
  field
    factorisation : {r : A} → (nonzero : (r ∼ 0R) → False) → (nonunit : (Unit r) → False) → Factorisation nonzero nonunit
    uniqueFactorisation : {r : A} → (nonzero : (r ∼ 0R) → False) → (nonunit : (Unit r) → False) → (f1 f2 : Factorisation nonzero nonunit) → factorisationEquality f1 f2

record UFD' : Set (a ⊔ b) where
  field
    factorisation : {r : A} → (nonzero : (r ∼ 0R) → False) → (nonunit : (Unit r) → False) → Factorisation nonzero nonunit
    irreduciblesArePrime : {r : A} → Irreducible r → Prime r


text:
module Oscar.Function where

open import Function public using (id; _∘_; _∘′_; flip; _on_; _$_) renaming (const to const_)

infix -1 _∋_
_∋_ : ∀ {a} (A : Set a) → A → A
_ ∋ x = x

open import Prelude.Function public using (it)