{-# OPTIONS --safe #-}

-- See README.md for prerequisites and Agda instructions.

module README where

open import Multiset.Prelude
open import Multiset.Util using (isInjective)

open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism using (Iso ; section)
open import Cubical.Data.List as List using (List)
open import Cubical.Data.Nat as Nat using ( ; suc)
open import Cubical.Data.SumFin using (Fin)
open import Cubical.HITs.PropositionalTruncation as PT using (∥_∥₁)
open import Cubical.HITs.SetQuotients as SQ using (_/_)
open import Cubical.HITs.SetTruncation as ST using (∥_∥₂ ; ∣_∣₂)

-- 3. The Finite Bag Functor in Sets
-- ---------------------------------

-- 3.1 The free commutative monoid
-- -------------------------------

import Multiset.FCM

-- Finite multisets, defined as the free commutative monoid on a type.
-- Implemented as a HIT:
FCM :  {}  Type   Type 
FCM = Multiset.FCM.M

-- 3.2 As a Quotient of Lists
-- --------------------------

import Multiset.Ordering.Order
import Multiset.Ordering.PermEquiv

-- Inductive definition of permutations of lists:
Perm :  {A}  List A  List A  Type
Perm = Multiset.Ordering.Order.Perm

-- Finite multisets as lists modulo permutation:
List[_]/Perm : Type  Type
List[_]/Perm = Multiset.Ordering.Order.Mset

import Multiset.ListQuotient.Base

-- Relational lifting of R to a relation on lists
DRelator :  {} {X Y : Type } (R : X  Y  Type )  List X  List Y  Type 
DRelator = Multiset.ListQuotient.Base.DRelator

Relator :  {} {X : Type } (R : X  X  Type )  List X  List X  Type 
Relator = Multiset.ListQuotient.Base.Relator

import Multiset.Ordering.PermEquiv

-- The relational lifting of paths witnesses exactly the mere existence of a permutation:
∥Perm∥₁≃Relator≡ : {A : Type} {xs ys : List A}   Perm xs ys ∥₁  Relator _≡_ xs ys
∥Perm∥₁≃Relator≡ = Multiset.Ordering.PermEquiv.∥Perm∥₁≃Relator=


-- 3.3 As an Analytic Functor
-- --------------------------

import Multiset.FMSet
import Multiset.ListQuotient.FMSetEquiv

-- Finite multisets as an analytic functor:
FMSet :  {}  Type   Type 
FMSet = Multiset.FMSet.FMSet

-- The action of the symmetric group that `FMSet` is quotiented by:
SymAct :  {X}  (n : )  (v w : Fin n  X)  Type
SymAct = Multiset.FMSet.SymmetricAction

-- The non-propositionally truncated version:
SymAct∞ :  {X}  (n : )  (v w : Fin n  X)  Type
SymAct∞ = Multiset.ListQuotient.FMSetEquiv.SymmetricActionΣ

-- Abbreviation with size implict:
_∼_ = Multiset.FMSet._∼_

-- Finite choice for Fin-indexed types:
import Multiset.FiniteChoice

module FiniteChoice {n : } (Y : Fin n  Type) where
  finChoiceEquiv : ((k : Fin n)   Y k ∥₂)   ((k : Fin n)  Y k) ∥₂
  finChoiceEquiv = Multiset.FiniteChoice.setFinChoice≃ Y

  box : ((k : Fin n)   Y k ∥₂)   ((k : Fin n)  Y k) ∥₂
  box = Multiset.FiniteChoice.box

  unbox :  ((k : Fin n)  Y k) ∥₂  ((k : Fin n)   Y k ∥₂)
  unbox = Multiset.FiniteChoice.unbox

-- Dependent eliminator for Fin-indexed families:
elim-∥_∥₂-fin : {n : } (X : Type) {B : (Fin n   X ∥₂)  Type}
   ((∣v∣ : Fin n   X ∥₂)  isSet (B ∣v∣))
   ((v : Fin n  X)  B (∣_∣₂  v))
   (v : Fin n   X ∥₂)  B v
elim-∥ X ∥₂-fin = Multiset.FiniteChoice.elimₙ

-- Propositional computation rule for the eliminator:
elim-∥_∥₂-finᵝ : {n : } (X : Type) {B : (Fin n   X ∥₂)  Type}
   (setB : (∣v∣ : Fin n   X ∥₂)  isSet (B ∣v∣))
   (choice : (v : Fin n  X)  B (∣_∣₂  v))
   (v : Fin n  X)
   elim-∥ X ∥₂-fin setB choice (∣_∣₂  v)  choice v
elim-∥ X ∥₂-finᵝ = Multiset.FiniteChoice.elimₙ-comp

import Multiset.FMSet.Properties using (module STInvariance)

-- FMSet is invariant under set truncation:
FMSetTruncInvariance : {X : Type}  FMSet  X ∥₂  FMSet X
FMSetTruncInvariance = Multiset.FMSet.Properties.STInvariance.STInvarianceEquiv

-- 3.4 Equivalence of Presentations
-- --------------------------------

import Multiset.Equivalences.FCM-PList
import Multiset.Equivalences.PList-RelatorList

-- The four presentations of finite multisets above are provably equivalent:
FMSetEquivs :  X  FCM X  FMSet X
FMSetEquivs X =
  FCM X                ≃⟨ Multiset.Equivalences.FCM-PList.M≃PList 
  List X / Perm        ≃⟨ Multiset.Equivalences.PList-RelatorList.List/Perm≃List/Relator≡ 
  List X / Relator _≡_ ≃⟨ invEquiv Multiset.ListQuotient.FMSetEquiv.FMSet≃List/Relator= 
  FMSet X 

-- All equivalences above are natural:
FCM≃List/Perm-natural = Multiset.Equivalences.FCM-PList.PListToM-nat
List/Perm≃List/Relator-natural = Multiset.Equivalences.PList-RelatorList.List/Perm→List/Relator≡-nat
FMSet→List/Relator=-natural = Multiset.Equivalences.PList-RelatorList.FMSet→List/Relator=-nat


-- Variations
-- ----------

-- The following are not mentioned explicitly in the paper, but are used when convenient:
import Multiset.Util.BundledVec
import Multiset.ListQuotient.ListFinality

-- A variation of lists, as a vector bundled with its length.
List' : Type  Type
List' = Multiset.Util.BundledVec.ΣVec

-- This type is convenient when proving that List preserves ω-chain limits,
-- since that relies on access to a countable family of lists *of the same length*.
_ = Multiset.ListQuotient.ListFinality.isTerminalFix⁻

-- The relational lifting, but for lists bundled with a length:
Relator' : _
Relator' = Multiset.Util.BundledVec.Relator
  
-- The two definitions are naturally equivalent:
ΣVec-List-nat = Multiset.ListQuotient.ListFinality.ΣVec-List-EquivNat

-- Equivalences of FCM and a HIT of head-permuted lists, defined in Cubical.HITs.FiniteMultiset.
open import Cubical.HITs.FiniteMultiset.Base using () renaming (FMSet to HeadPList)
import Multiset.Equivalences.FCM-HeadPList

_ :  {X : Type}  FCM X  HeadPList X
_ = Multiset.Equivalences.FCM-HeadPList.M≃HeadPList

-- 3.5 Definable Quotients and Sorting

import Multiset.Ordering.Order

isLinOrder : {A : Type} (R : A  A  Type)  Type
isLinOrder = Multiset.Ordering.Order.isLinOrder

module LexFMSet {A : Type} (setA : isSet A) (R : A  A  Type) (linR : isLinOrder R) where
  import Multiset.Ordering.FMSetOrder
  module S = Multiset.Ordering.FMSetOrder.SortingFMSet setA R linR

  -- For linearly ordered A, `∼` induces a definable quotient:
  sort : (n : )  (Fin n  A) / _∼_  (Fin n  A)
  sort = S.sortPVect

  SymActDefinable : (n : )  section SQ.[_] (sort n)
  SymActDefinable = S.sortPVect-section

  -- For linearly ordered A, there is a canonical permutation between
  -- any two unordered finite sets of A's:
  SymActUntruncate : (n : ) (v w : Fin n  A)  SymAct n v w  SymAct∞ n v w
  SymActUntruncate = S.canonicalS

  -- The result above is powered by a (weakly constant) function computing
  -- a canonical permutation from an arbitrary permutation of lists:
  canonPerm : (xs ys : List A)  Perm xs ys  Perm xs ys
  canonPerm = Multiset.Ordering.Order.Sorting.canonPerm setA R linR

  -- In particular, we can evaluate this function for concrete linear orders:
  module BraidExample = Multiset.Ordering.Order.Example

  -- The above extends to a linear order on finite multisets:
  LexFMSet : FMSet A  FMSet A  Type
  LexFMSet = S.LexFMSet

  linLexFMSet : isLinOrder LexFMSet
  linLexFMSet = S.linLexFMSet

-- 4 The Final Coalgebra in Sets
-- -----------------------------

import Multiset.Functor
import Multiset.Coalgebra

-- The structure of a functor of types:
Functor : (F : Type  Type)  Type _
Functor = Multiset.Functor.Functor

-- Coalgebras are unbundled functions:
Coalgebra : (F : Type  Type)   Functor F   _
Coalgebra F =  {A}  A  F A

-- Coalgebra morphisms:
CoalgebraMorphism : (F : Type  Type)   Functor F    {A B}  (α : A  F A)  (β : B  F B)  Type _
CoalgebraMorphism = Multiset.Coalgebra.CoalgebraMorphism


-- 4.1 As an ω-Limit
-- -----------------

-- Definition of the terminal ω-chain of an endofunctor:
open import Multiset.Limit.TerminalChain as TerminalChain
  using
    ( ch        -- The chain 1 ← F(1) ← F²(1) ← ...
    ; _^_       -- Helper for the type Fⁿ(1)
    ; _map-!^_  -- Helper for the iterated map !ⁿ : Fⁿ⁺¹(1) → Fⁿ(1)
    ; Lim       -- The type of limits of such a chain
    ; ShLim     -- The limits of the shifted chain F(1) ← F²(1) ← F³(1) ← ...
    ; isLimitPreserving
    )

module IterLimit (F : Type  Type) {{FunctorF : Functor F}} where

  -- The limit and the shifted limit of a chain are equivalent
  shift : Lim F  ShLim F
  shift = invEquiv (TerminalChain.ShLim≃Lim F)

  -- The family of projections out of a limit.
   : (n : )  Lim F  F ^ n
   = TerminalChain.cut F
  -- NB: This is not called "ℓ" in the rest of the code because
  -- of naming conflicts with universe levels.

  -- The limit-preservation maps into the shifted limit.
  pres : F (Lim F)  ShLim F
  pres = TerminalChain.pres F

  -- If F preserves limits of this shape, it admits a fixpoint:
  fix : isLimitPreserving F  F (Lim F)  Lim F
  fix = TerminalChain.fix

  -- The inverse of the above equivalence is the structure map
  -- of the final coalgebra:
  coalg : isLimitPreserving F  Lim F  F (Lim F)
  coalg = TerminalChain.Fixpoint.fix⁻

  open import Multiset.Limit.Chain using (Chain ; ChainEquiv ; Limit)
  import Multiset.Limit.Isomorphism

  chainEquivToLimitEquiv :  {} {C C' : Chain }  ChainEquiv C C'  Limit C  Limit C'
  chainEquivToLimitEquiv = Multiset.Limit.Isomorphism.mapLimit-pres-equiv

open IterLimit using (pres)

import Multiset.FCM.Limit

-- The Lesser Limit Principle of Omniscience:
open import Multiset.Omniscience using (LLPO)

-- Injectivity of the limit-preservation map of finite multisets implies LLPO.
-- Note that this is proved for the presentation as a HIT:
InjectiveFMSetPresToLLPO : isInjective (pres FCM)  LLPO
InjectiveFMSetPresToLLPO = Multiset.FCM.Limit.pres-inj⇒llpo

-- The crucial lemma that the above proof depends on:
LimitAlternationLemma = TerminalChain.diag-islim-alternating

-- The lemma instanciated to `FCM`, as necessary (kept here in order not to break old links):
FMSetAlternationLemma = TerminalChain.diag-islim-alternating (FCM { = ℓ-zero})

-- The detailed proof that completeness of two-element multisets implies LLPO:
CompleteToLLPO : Multiset.FCM.Limit.Complete  LLPO
CompleteToLLPO = Multiset.FCM.Limit.complete⇒llpo
-- NB: The proof of `isSetoidMorphismCoalgListToLLPO` is conceptually the same,
-- but might be slightly more readable than the above proof.

import Multiset.ListQuotient.ToInjectivity

-- LLPO also implies the injectivity of the limit-preservation map.
-- This time, we use lists modulo a relational lifting for the proof:
LLPOToInjectiveFMSetPres : LLPO  isInjective (pres  X  List X / Relator _≡_))
LLPOToInjectiveFMSetPres = Multiset.ListQuotient.ToInjectivity.llpo⇒pres-inj

import Multiset.FMSet.Limit

-- Using the third preservation of finite multisets in terms of an analytic
-- functor, we can at least show that the limit-preservation map has a section,
-- i.e. the limit is weakly preserved:
LexFMSet^ : (n : )  FMSet ^ n  FMSet ^ n  Type
LexFMSet^ = Multiset.FMSet.Limit.LexFMSet^

linLexIterFMSet :  n  isLinOrder (LexFMSet^ n)
linLexIterFMSet = Multiset.FMSet.Limit.linLexFMSet^

FMSetPresSection : section (pres FMSet) Multiset.FMSet.Limit.PresSection.pres⁻¹
FMSetPresSection = Multiset.FMSet.Limit.PresSection.pres-section

-- 4.2 As a Quotient of the Final List-Coalgebra
-- ---------------------------------------------

import Multiset.ListQuotient.Bisimilarity

-- List has a final coalgebra whose carrier is the type of ordered non-wellfounded trees:
Tree = Multiset.ListQuotient.ListFinality.Tree

_ : Tree  Lim List'
_ = refl

coalgList : Tree  List' Tree
coalgList = Multiset.ListQuotient.ListFinality.fix⁻

-- Relation on finite approximation of infinite trees that relates
-- them up to the order of their subtrees:
Approx : (n : )  List' ^ n  List' ^ n  Type
Approx = Multiset.ListQuotient.Bisimilarity.Approx

!-Approx : (n : ) {s t : (List' ^ (suc n))}
   Relator' (Approx n) s t  Approx n ((List' map-!^ n) s) ((List' map-!^ n) t)
!-Approx = Multiset.ListQuotient.Bisimilarity.Approx-π

-- Bisimilarity of trees.  This is the limit of a chain defined in
-- terms of `Approx` above:
Bisim : (s t : Tree)  Type
Bisim = Multiset.ListQuotient.Bisimilarity.Bisim

open import Multiset.Axioms.Choice as AOC using (AC)
import Multiset.ListQuotient.LLPO

open import Cubical.Categories.Functor using () renaming (Functor to Functor')
import Multiset.Categories.Coalgebra as Cat
open import Cubical.Categories.Instances.Sets using (SET)

-- Under the assuming that `coalgList` is a morphism of setoids, we can deduce the following:
module Setoid (isSetoidMorCoalgList : (∀ {s} {t}  Bisim s t  Relator' Bisim (coalgList s) (coalgList t))) where

  -- 1) The anti-constructive principle LLPO:
  isSetoidMorphismCoalgListToLLPO : LLPO
  isSetoidMorphismCoalgListToLLPO = Multiset.ListQuotient.LLPO.fix⁻-preserves-≈→LLPO isSetoidMorCoalgList

  import Multiset.Setoid.Category
  open import Cubical.Categories.Category using (Category)

  -- The category of setoids: Objects are pairs of hSets and prop-valued equivalence relations;
  -- morphisms are relation-preserving functions modulo the relation in the domain
  SetoidCategory : Category (ℓ-suc ℓ-zero) ℓ-zero
  SetoidCategory = Multiset.Setoid.Category.SetoidCategory ℓ-zero ℓ-zero

  FMSetoid : Functor' SetoidCategory SetoidCategory
  FMSetoid = Multiset.Util.BundledVec.RelatorFunctor

  import Multiset.ListQuotient.Finality

  -- 2) coalgList induces a terminal coalgebra of the functor `FMSetoid : (X, R) ↦ (List' X, Relator R)`:
  finalFMSetoidCoalgebra : Cat.TerminalCoalgebra FMSetoid
  finalFMSetoidCoalgebra = Multiset.ListQuotient.Finality.finalFMSetoidCoalgebra isSetoidMorCoalgList

  import Multiset.ListQuotient.Fixpoint

  FMSet' : Type  Type
  FMSet' X = List' X / (Relator' _≡_)

  -- 3) coalgList lifts to a FMSet-coalgebra, and induces a fixpoint of trees modulo bisimilarity:
  coalgFMSet : Tree / Bisim  FMSet' (Tree / Bisim)
  coalgFMSet = Multiset.ListQuotient.Fixpoint.fixQ⁻ isSetoidMorCoalgList

  FMSetFixpointTree/Bisim : FMSet' (Tree / Bisim)  Tree / Bisim
  FMSetFixpointTree/Bisim = Multiset.ListQuotient.Fixpoint.FMSetFixpointTree/Bisim isSetoidMorCoalgList

  FMSetFunctor : Functor' (SET _) (SET _)
  FMSetFunctor = Multiset.ListQuotient.Fixpoint.FMSetFunctor

  -- 4) Assuming the axiom of choice this fixpoint is the largest, i.e. coalgFMSet is the final coalgebra:
  FinalFMSetCoalgebra : AC _ _ _  Cat.TerminalCoalgebra FMSetFunctor
  FinalFMSetCoalgebra = Multiset.ListQuotient.Fixpoint.TerminalfixQ⁻ isSetoidMorCoalgList


-- 5 The Finite Bag Functor in Groupoids
-- -------------------------------------

open import Cubical.Data.FinSet.Base using (FinSet)
import Multiset.Tote

-- The "large" type of bags, defined in terms of FinSet:
Tote : Type₀  Type₁
Tote = Multiset.Tote.Tote

isGroupoidTote :  {X : Type}  isGroupoid X  isGroupoid (Tote X)
isGroupoidTote = Multiset.Tote.isGroupoidTote

-- The set-truncation of this type is naturally equivalent to finite multisets:
FMSetToteTruncEquiv : {X : Type}  FMSet X   Tote X ∥₂
FMSetToteTruncEquiv = Multiset.Tote.FMSet≃∥Tote∥₂

FMSet→∥Tote∥₂ :  {X : Type}  FMSet X   Tote X ∥₂
FMSet→∥Tote∥₂ = equivFun FMSetToteTruncEquiv

isNatural-FMSetToteTruncEquiv :  {X Y : Type} (f : X  Y)
   FMSet→∥Tote∥₂  Multiset.FMSet.map f  ST.map (Multiset.Tote.map f)  FMSet→∥Tote∥₂
isNatural-FMSetToteTruncEquiv = Multiset.Tote.isNatural-FMSet≃∥Tote∥₂

import Multiset.Bij

-- A small type, equivalent to the large type of (Bishop-) finite types:
Bij : Type
Bij = Multiset.Bij.Bij

BinFinSetEquiv : Bij  FinSet ℓ-zero
BinFinSetEquiv = Multiset.Bij.Bij≃FinSet

import Multiset.Bag

Bag : Type  Type
Bag = Multiset.Bag.Bag

-- Both defintions, small and large, are equivalent:
BagToteEquiv :  {X : Type}  Bag X  Tote X
BagToteEquiv = Multiset.Bag.Bag≃Tote

-- The equivalence is natural:
isNaturalBagToteEquiv : {X Y : Type}  (f : X  Y)
   equivFun BagToteEquiv  Multiset.Bag.map f  Multiset.Tote.map f  equivFun BagToteEquiv
isNaturalBagToteEquiv = Multiset.Bag.isNaturalBagToteEquiv

-- 6 The Final Coalgebra in Groupoids
-- ----------------------------------

-- Bag preserves limits of ω-chains, so by [Ahrens et al. '15] it admits a final coalgebra:
isLimitPreservingBag : isEquiv (pres Bag)
isLimitPreservingBag = Multiset.Bag.isLimitPreservingBag

import Multiset.FMSet.Fixpoint

-- `FMSetToteTruncEquiv` from above also applies to `Bag`:
TruncBagFMSetEquiv : {X : Type}   Bag X ∥₂  FMSet X
TruncBagFMSetEquiv = Multiset.FMSet.Fixpoint.TruncBagFMSetEquiv

-- This applies also to the iterated types:
IterTruncBagFMSetEquiv :  n   Bag ^ n ∥₂  FMSet ^ n
IterTruncBagFMSetEquiv = Multiset.FMSet.Fixpoint.IterTruncBagFMSetEquiv

-- Truncating the type of Bag-limits yields a fixpoint for FMSet:
FMSetFixpointTruncBagLim : FMSet  Lim Bag ∥₂   Lim Bag ∥₂
FMSetFixpointTruncBagLim = Multiset.FMSet.Fixpoint.FMSetFixSetTruncTree

import Multiset.FMSet.Finality

FMSetFunctor' : Functor' (SET _) (SET _)
FMSetFunctor' = Multiset.FMSet.Finality.FMSetFunctor

module _
  -- Assume bag has a final coalgebra (follows from `isLimitPreservingBag` + [Ahrens et al. '15])
  (ana : {X : Type}  (c : X  Bag X)  X  Lim Bag)
  (anaEq : {X : Type} (c : X  Bag X)
     ana c  Multiset.Bag.fix⁺  Multiset.Bag.map (ana c)  c)
  (anaUniq : {X : Type} (c : X  Bag X)
     (h : X  Lim Bag)
     h  Multiset.Bag.fix⁺  (Multiset.Bag.map h)  c
     ana c  h)
  where
  abstract
    e : {X : Type}   Bag X ∥₂  FMSet X
    e = Multiset.FMSet.Fixpoint.TruncBagFMSetEquiv

    eNat :  {X Y : Type} (f : X  Y)  equivFun e  ST.map (Multiset.Bag.map f)  Multiset.FMSet.map f  equivFun e
    eNat = Multiset.FMSet.Fixpoint.isNaturalTruncBagFMSetEquiv
  
  -- Assuming two instance of choice, one for groupoids and one for sets, FMSet admits a final coalgebra in the category of hSets:
  FMSetFinalCoalgebra : (ac32 : AOC.AC[Gpd,Set] ℓ-zero ℓ-zero)  (ac : AOC.AC[Set,Prop] ℓ-zero ℓ-zero)  Cat.TerminalCoalgebra FMSetFunctor'
  FMSetFinalCoalgebra = Multiset.FMSet.Finality.FinalityWithChoice.FMSetFinalCoalgebra ana anaEq anaUniq e eNat

  import Multiset.FMSet.FiniteFinality

  coalgFinite : Cat.Coalgebra FMSetFunctor'
  coalgFinite = Multiset.FMSet.FiniteFinality.FinalityFinite.coalg ana anaEq anaUniq e eNat

  -- When not assuming choice, there is still a unique coalgebra morphism from a coalgebra with finite carrier and `coalg'`:
  uniqueCoalgMorphismFinCarrier :  n (c : Fin n  FMSet (Fin n))  isContr (Cat.CoalgebraHom FMSetFunctor' (Cat.coalgebra c) coalgFinite)
  uniqueCoalgMorphismFinCarrier = Multiset.FMSet.FiniteFinality.FinalityFinite.uniqueFiniteCoalg ana anaEq anaUniq e eNat