module Operad.FinSet.Properties where

open import Cubical.Data.Empty renaming (rec to ⊥-rec)

open import Cubical.Data.Nat hiding (snotz; znots)

open import Cubical.Data.Unit renaming (Unit to ⊤)

open import Cubical.Foundations.Equiv

open import Cubical.Foundations.Function

open import Cubical.Foundations.HLevels

open import Cubical.Foundations.Isomorphism

open import Cubical.Foundations.Path

open import Cubical.Foundations.Prelude

open import Cubical.Foundations.Transport

open import Cubical.Foundations.Univalence

open import Cubical.HITs.PropositionalTruncation renaming (rec to p-rec)

open import Cubical.Relation.Nullary

open import Operad.Fin

open import Operad.FinSet.Base

open import Operad.Sigma

variable

ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level

X : Type ℓ₁

Y : Type ℓ₂

Z : Type ℓ₄

W : X → Type ℓ₂

open Iso

p-rec₂ : {P : Type ℓ₃} → isProp P → (X → Y → P) → ∥ X ∥ → ∥ Y ∥ → P

p-rec₂ p f x y = p-rec p (λ x → p-rec p (f x) y) x

compIso⁻ : Iso X Y → Iso X Z → Iso Y Z

compIso⁻ I₁ I₂ = compIso (invIso I₁) I₂

sameSize : ∀ m n → Iso X (Fin m) → Iso X (Fin n) → m ≡ n

sameSize m n I₁ I₂ = Fin-inj (compIso⁻ I₁ I₂)

transportInv : {A₁ A₂ : Type ℓ₁} (I : Iso A₁ A₂) → ∀ a → inv I a ≡ transport⁻ (isoToPath I) a

transportInv I a = cong (inv I) (sym (transportRefl _))

iso→substPath : {A₁ A₂ : Type ℓ₁} {B₁ : A₁ → Type ℓ₃} {B₂ : A₂ → Type ℓ₃} →

(I : Iso A₁ A₂) → ((a : A₂) → Iso (B₁ (inv I a)) (B₂ a)) →

subst (λ A → A → Type ℓ₃) (isoToPath I) B₁ ≡ B₂

iso→substPath {B₁ = B₁} {B₂ = B₂} I Is =

funExt λ a → isoToPath (subst (λ x → Iso (B₁ x) (B₂ a)) (transportInv I a) (Is a))

iso-cong-path : {A₁ A₂ : Type ℓ₁} {B₁ : A₁ → Type ℓ₂} {B₂ : A₂ → Type ℓ₂} →

(I : Iso A₁ A₂) → ((a : A₂) → Iso (B₁ (inv I a)) (B₂ a)) →

PathP (λ i → isoToPath I i → Type ℓ₂) B₁ B₂

iso-cong-path {B₁ = B₁} I Is = transport⁻ (PathP≡Path _ _ _) (iso→substPath {B₁ = B₁} I Is)

congIso₂ : (_∙_ : ∀ {ℓ₁ ℓ₂} (A : Type ℓ₁) → (A → Type ℓ₂) → Type (ℓ-max ℓ₁ ℓ₂))

{A₁ A₂ : Type ℓ₁} {B₁ : A₁ → Type ℓ₃} {B₂ : A₂ → Type ℓ₃} →

(I : Iso A₁ A₂) → ((a : A₂) → Iso (B₁ (inv I a)) (B₂ a)) →

Iso (A₁ ∙ B₁) (A₂ ∙ B₂)

congIso₂ _∙_ I Is =

pathToIso (cong₂ _∙_ (isoToPath I) (iso-cong-path I Is))

isOfHLevelRespectIso : ∀ n → Iso X Y → isOfHLevel n X → isOfHLevel n Y

isOfHLevelRespectIso n I p = isOfHLevelRetract n (inv I) (fun I) (rightInv I) p

inv≡inv→b₁≡b₂ : (I : Iso X Y) → ∀ {x₁ x₂} → inv I x₁ ≡ inv I x₂ → x₁ ≡ x₂

inv≡inv→b₁≡b₂ I {x₁} {x₂} p =

x₁ ≡⟨ sym (rightInv I x₁) ⟩

fun I (inv I x₁) ≡⟨ cong (fun I) p ⟩

fun I (inv I x₂) ≡⟨ rightInv I x₂ ⟩

x₂ ∎

discreteRespectsIso : Iso X Y → Discrete X → Discrete Y

discreteRespectsIso I Dₓ y₁ y₂ with Dₓ (inv I y₁) (inv I y₂)

discreteRespectsIso I Dₓ y₁ y₂ | yes p = yes (inv≡inv→b₁≡b₂ I p)

discreteRespectsIso I Dₓ y₁ y₂ | no ¬p = no (¬p ∘ cong (inv I))

Finite→Discrete : ∀ {n} {x y : X} → Iso X (Fin n) → Dec (x ≡ y)

Finite→Discrete I = discreteRespectsIso (invIso I) discreteFin _ _

ContrIso : isContr X → isContr Y → Iso X Y

fun (ContrIso (x , p) (y , q)) = const y

inv (ContrIso (x , p) (y , q)) = const x

rightInv (ContrIso (x , p) (y , q)) = q

leftInv (ContrIso (x , p) (y , q)) = p

Inj→¬Iso : (f : X → Y) → (∀ x y → f x ≡ f y → x ≡ y) → ∀ x y → Iso (¬ x ≡ y) (¬ f x ≡ f y)

fun (Inj→¬Iso f g x y) ¬p p = ¬p (g x y p)

inv (Inj→¬Iso f g x y) ¬p p = ¬p (cong f p)

rightInv (Inj→¬Iso f g x y) _ = isProp¬ _ _ _

leftInv (Inj→¬Iso f g x y) _ = isProp¬ _ _ _

¬Iso0 : Iso X (Fin 0) → Iso (¬ X) (Fin 1)

fun (¬Iso0 I) _ = zero

inv (¬Iso0 I) _ x = ¬Fin0 (fun I x)

rightInv (¬Iso0 I) zero = refl

leftInv (¬Iso0 I) _ = isPropΠ (λ _ → isProp⊥) _ _

¬Iso-suc : ∀ {n} → Iso X (Fin (suc n)) → Iso (¬ X) (Fin 0)

fun (¬Iso-suc I) f = ⊥-rec (f (inv I zero))

inv (¬Iso-suc I) i = ⊥-rec (¬Fin0 i)

rightInv (¬Iso-suc I) _ = isPropFin0 _ _

leftInv (¬Iso-suc I) _ = isPropΠ (λ _ → isProp⊥) _ _

isContr→≡Fin1 : isContr X → X ≡ Lift (Fin 1)

isContr→≡Fin1 p = isoToPath (ContrIso p (lift _ , λ { (lift zero) → refl }))

uniqueSize : (p q : isFinite X) → p .fst ≡ q .fst

uniqueSize (m , p) (n , q) = p-rec₂ (isSetℕ m n) (sameSize m n) p q

isPropIsFinite : isProp (isFinite X)

isPropIsFinite x y = Σ≡Prop (λ _ → squash) (uniqueSize x y)

isFinite→isSet : isFinite X → isSet X

isFinite→isSet (_ , p) = p-rec isPropIsSet (λ I → isOfHLevelRespectIso 2 (invIso I) isSetFin) p

isSetFinSet : (A : FinSet ℓ₁) → isSet ⟦ A ⟧

isSetFinSet (_ , p) = isFinite→isSet p

isFinite→Discrete : isFinite X → Discrete X

isFinite→Discrete q@(_ , p) x y = p-rec (isPropDec (isFinite→isSet q x y)) Finite→Discrete p

isDiscreteFinSet : (A : FinSet ℓ₁) → Discrete ⟦ A ⟧

isDiscreteFinSet (_ , p) = isFinite→Discrete p

isCardPropInj : (A : FinSet ℓ₁) (B : FinSet ℓ₂) → card A ≡ card B → ∥ Iso ⟦ A ⟧ ⟦ B ⟧ ∥

isCardPropInj A B p = rec A squash λ I₁ →

rec B squash λ I₂ →

∣ compIso (subst (λ n → Iso ⟦ A ⟧ (Fin n)) p I₁) (invIso I₂) ∣

¬isCardPropInj : (A : FinSet ℓ₁) (B : FinSet ℓ₂) → ¬ card A ≡ card B → ¬ ∥ Iso ⟦ A ⟧ ⟦ B ⟧ ∥

¬isCardPropInj A B p = rec A (isPropΠ λ _ ()) λ I₁ →

rec B (isPropΠ λ _ ()) λ I₂ →

p-rec (λ ()) λ I →

p (Fin-inj (compIso (invIso I₁) (compIso I I₂)))

Lift≡ : (A₁ A₂ : FinSet ℓ₁) → ⟦ A₁ ⟧ ≡ ⟦ A₂ ⟧ → A₁ ≡ A₂

Lift≡ A₁ A₂ p = Σ≡Prop (λ _ → isPropIsFinite) p

Lower≡ : (A₁ A₂ : FinSet ℓ₁) → A₁ ≡ A₂ → ⟦ A₁ ⟧ ≡ ⟦ A₂ ⟧

Lower≡ A₁ A₂ p i = fst (p i)

LiftLower≃ : (A₁ A₂ : FinSet ℓ₁) → (⟦ A₁ ⟧ ≡ ⟦ A₂ ⟧) ≃ (A₁ ≡ A₂)

LiftLower≃ A₁ A₂ = Σ≡PropEquiv λ _ → isPropIsFinite

isGroupoidFinSet : isGroupoid (FinSet ℓ₁)

isGroupoidFinSet A B = isOfHLevelRespectEquiv 2 (LiftLower≃ A B)

(isOfHLevel≡ 2 (isSetFinSet A) (isSetFinSet B))

Card1→isContr : (A : FinSet ℓ₁) → 1 ≡ card A → isContr ⟦ A ⟧

Card1→isContr A p = rec A isPropIsContr λ I →

isOfHLevelRespectIso 0 (invIso I)

(subst (isContr ∘ Fin) p isContrFin1)

Card1→≡⊤ : {A : FinSet ℓ₁} → 1 ≡ card A → A ≡ 1-FinSet ℓ₁

Card1→≡⊤ {A = A} p = Lift≡ _ _ (isContr→≡Fin1 (Card1→isContr A p))

ContrFinSet₁ : isContr (Σ[ A ∈ FinSet ℓ₁ ] 1 ≡ card A)

ContrFinSet₁ = (1-FinSet _ , refl) , λ { (_ , p) → Σ≡Prop (λ _ → isSetℕ _ _) (sym (Card1→≡⊤ p)) }

isFiniteContr : isContr X → isFinite X

isFiniteContr (x , p) = 1 , ∣ iso (const zero) (const x) (λ { zero → refl }) (λ _ → p _) ∣

isFiniteEmpty : ¬ X → isFinite X

isFiniteEmpty ¬X = 0 , ∣ iso (⊥-rec ∘ ¬X) (λ ()) (λ ()) (⊥-rec ∘ ¬X) ∣

isFiniteDecProp : isProp X → Dec X → isFinite X

isFiniteDecProp isPropX (yes x) = isFiniteContr (x , isPropX _)

isFiniteDecProp isPropX (no ¬x) = isFiniteEmpty ¬x

isFiniteRemove : isFinite X → (x : X) → isFinite (Σ[ y ∈ X ] ¬ x ≡ y)

isFiniteRemove (zero , p) x = p-rec isPropIsFinite (λ I → ⊥-rec (¬Fin0 (fun I x))) p

isFiniteRemove (suc n , p) x = n , p-rec squash (λ I →

∣ compIso (Σ-cong-iso I λ y → Inj→¬Iso (fun I) (isoFunInjective I) x y) (Fin/ n (fun I x)) ∣

) p

_/_ : (A : FinSet ℓ₁) (a : ⟦ A ⟧) → FinSet ℓ₁

(_ , p) / a = _ , isFiniteRemove p a

isFiniteFin≡ : isFinite X → (a b : X) → isFinite (a ≡ b)

isFiniteFin≡ isFiniteX a b with isFinite→Discrete isFiniteX a b

... | yes p = 1 , ∣ iso

(const zero)

(const p)

(λ { zero → refl })

(isFinite→isSet isFiniteX _ _ p)

∣

... | no ¬p = 0 , ∣ iso (⊥-rec ∘ ¬p) (⊥-rec ∘ ¬Fin0) (⊥-rec ∘ ¬Fin0) (⊥-rec ∘ ¬p) ∣

_⟨_≡_⟩ : (A : FinSet ℓ₁) → ⟦ A ⟧ → ⟦ A ⟧ → FinSet ℓ₁

(_ , isFiniteA) ⟨ a ≡ b ⟩ = _ , isFiniteFin≡ isFiniteA a b

isFinite¬ : isFinite X → isFinite (¬ X)

isFinite¬ (zero , p) = 1 , p-rec squash (∣_∣ ∘ ¬Iso0) p

isFinite¬ (suc n , p) = 0 , p-rec squash (∣_∣ ∘ ¬Iso-suc) p

_⟨_≢_⟩ : (A : FinSet ℓ₁) → ⟦ A ⟧ → ⟦ A ⟧ → FinSet ℓ₁

A ⟨ a ≢ b ⟩ = _ , isFinite¬ (isFiniteFin≡ (snd A) a b) -- (A ⟨ a ≡ b ⟩)

isFiniteClosure : (_∙_ : ∀ {ℓ₁ ℓ₂} (A : Type ℓ₁) → (A → Type ℓ₂) → Type (ℓ-max ℓ₁ ℓ₂)) →

(size : ∀ n (ns : Fin n → ℕ) → ℕ) →

(∀ m (ns : Fin m → ℕ) → Iso (Lift {j = ℓ₁} (Fin m) ∙

(Lift {j = ℓ₂} ∘ Fin ∘ ns ∘ lower))

(Fin (size m ns))) →

{X : Type ℓ₁} {Y : X → Type ℓ₂} →

isFinite X → (∀ x → isFinite (Y x)) → isFinite (X ∙ Y)

isFiniteClosure _∙_ size is (n , X↔Fin) isFiniteY =

p-rec isPropIsFinite (λ I →

size n (fst ∘ isFiniteY ∘ inv I) ,

p-rec squash (λ Is →

∣

compIso (congIso₂ _∙_ (compIso I LiftIso) (flip compIso LiftIso ∘ Is ∘ lower))

(is n (fst ∘ isFiniteY ∘ inv I))

∣

) (finiteChoice n (snd ∘ isFiniteY ∘ inv I))

) X↔Fin

isFiniteClosure′ : (_∙_ : ∀ {ℓ₁ ℓ₂} → Type ℓ₁ → Type ℓ₂ → Type (ℓ-max ℓ₁ ℓ₂)) →

(_+_ : ℕ → ℕ → ℕ) →

(∀ m n → Iso (Lift (Fin m) ∙ Lift (Fin n)) (Fin (m + n))) →

isFinite X → isFinite Y → isFinite (X ∙ Y)

isFiniteClosure′ _∙_ _+_ is (m , X↔Fin) (n , Y↔Fin) =

m + n , p-rec₂ squash (λ Ix Iy →

∣

compIso (congIso₂′ _∙_ (compIso Ix LiftIso)

(compIso Iy LiftIso))

(is m n)

∣

) X↔Fin Y↔Fin

fromClosure : (_∙_ : ∀ {ℓ₁ ℓ₂} (A : Type ℓ₁) → (A → Type ℓ₂) → Type (ℓ-max ℓ₁ ℓ₂)) →

(size : ∀ n (ns : Fin n → ℕ) → ℕ) →

(∀ m (ns : Fin m → ℕ) → Iso (Lift (Fin m) ∙ (Lift ∘ Fin ∘ ns ∘ lower))

(Fin (size m ns))) →

(A : FinSet ℓ₁) → (⟦ A ⟧ → FinSet ℓ₂) → FinSet (ℓ-max ℓ₁ ℓ₂)

fromClosure _∙_ size ps (_ , isFiniteA) B =

_ , isFiniteClosure _∙_ size ps isFiniteA (snd ∘ B)

fromClosure′ : (_∙_ : ∀ {ℓ₁ ℓ₂} → Type ℓ₁ → Type ℓ₂ → Type (ℓ-max ℓ₁ ℓ₂)) →

(_+_ : ℕ → ℕ → ℕ) →

(∀ m n → Iso (Lift (Fin m) ∙ Lift (Fin n)) (Fin (m + n))) →

FinSet ℓ₁ → FinSet ℓ₂ → FinSet (ℓ-max ℓ₁ ℓ₂)

fromClosure′ _∙_ _+_ is (_ , isFiniteA) (_ , isFiniteB) =

_ , isFiniteClosure′ _∙_ _+_ is isFiniteA isFiniteB

finiteProp : (P : FinSet ℓ₁ → Type ℓ₂) → (∀ A → isProp (P A)) →

(∀ n → P (n-FinSet n)) → ∀ A → P A

finiteProp P isPropP f A =

rec A (isPropP A) λ I →

let Fin≡A = sym (Lift≡ A (n-FinSet (card A)) (isoToPath (compIso I LiftIso)))

in subst P Fin≡A (f (card A))

finiteProp₂ : (P : (A : FinSet ℓ₁) (B : ⟦ A ⟧ → FinSet ℓ₁) → Type ℓ₂) →

(∀ A B → isProp (P A B)) →

(∀ n ns → P (n-FinSet n) (n-FinSet ∘ ns ∘ lower)) → ∀ A B → P A B

finiteProp₂ P isPropP f =

finiteProp (λ A → (∀ B → P A B)) (λ _ → isPropΠ λ _ → isPropP _ _) λ n B →

let B↔Fin = finiteChoice n (Fin↔ ∘ B ∘ lift)

in p-rec (isPropP _ _) (λ Is →

let Fin≡B : ∀ i → n-FinSet (card (B i)) ≡ B i

Fin≡B i = sym (Lift≡ _ _ (isoToPath (compIso (Is (lower i)) LiftIso)))

in subst (P (n-FinSet n)) (funExt Fin≡B) (f n (card ∘ B ∘ lift))

) B↔Fin

finiteProp₃ : (P : (A : FinSet ℓ₁) (B : ⟦ A ⟧ → FinSet ℓ₁)

(C : ∀ a → ⟦ B a ⟧ → FinSet ℓ₁) → Type ℓ₂) →

(∀ A B C → isProp (P A B C)) →

(∀ n ns (nss : ∀ i → Fin (ns i) → ℕ) →

P (n-FinSet n) (n-FinSet ∘ ns ∘ lower)

(λ i j → n-FinSet (nss (lower i) (lower j)))) →

∀ A B C → P A B C

finiteProp₃ P isPropP f =

finiteProp₂ (λ A B → ∀ C → P A B C) (λ _ _ → isPropΠ λ _ → isPropP _ _ _)

λ n ns C →

let C↔Fin = finiteChoice₂ n ns λ i j → Fin↔ (C (lift i) (lift j))

in p-rec (isPropP _ _ _) (λ Is →

let Fin≡C : ∀ i j → n-FinSet (card (C i j)) ≡ C i j

Fin≡C i j =

sym (

Lift≡ _ _ (isoToPath (compIso (Is (lower i) (lower j)) LiftIso))

)

in subst (P (n-FinSet n) (n-FinSet ∘ ns ∘ lower))

(λ i j k → Fin≡C j k i)

(f n ns λ i j → card (C (lift i) (lift j)))

) C↔Fin