{-# OPTIONS --cubical --safe #-}

module Cardinality.Finite.ManifestBishop.Isomorphism where

open import Prelude
open import Data.Fin
open import Data.Fin.Properties

open import Container.List.Isomorphism

import Cardinality.Finite.ManifestBishop.Inductive as 𝕃
import Cardinality.Finite.ManifestBishop.Container as β„’

open import Cardinality.Finite.SplitEnumerable.Isomorphism

open import Data.Nat.Properties

∈!β„’β‡’βˆˆ!𝕃 : βˆ€ (x : A) l (xs : Fin l β†’ A) β†’ x β„’.∈! (l , xs) β†’ x 𝕃.∈! ℒ→𝕃 (l , xs)
∈!β„’β‡’βˆˆ!𝕃 x (suc l) xs ((f0   , p) , u) = (f0 , p) , lemma
  where
  lemma : (y : x 𝕃.∈ ℒ→𝕃 (suc l , xs)) β†’ (f0 , p) ≑ y
  lemma (f0   , q) = cong (βˆˆβ„’β‡’βˆˆπ•ƒ x (suc l , xs)) (u (f0 , q))
  lemma (fs m , q) =
    let o , r = subst (x β„’.∈_) (ℒ→𝕃→ℒ l (xs ∘ fs)) (m , q)
    in βŠ₯-elim (znots (cong (FinToβ„• ∘ fst) (u (fs o , r))))
∈!β„’β‡’βˆˆ!𝕃 x (suc l) xs ((fs n , p) , u) = 𝕃.push! xs0β‰’x (∈!β„’β‡’βˆˆ!𝕃 x l (xs ∘ fs) ((n , p) , uxss))
  where
  xs0β‰’x : xs f0 β‰’ x
  xs0β‰’x xs0≑x = snotz (cong (FinToβ„• ∘ fst) (u (f0 , xs0≑x)))

  uxss : (y : x β„’.∈ (l , xs ∘ fs)) β†’ (n , p) ≑ y
  uxss (m , q) = cong (Ξ» { (f0 , q) β†’ βŠ₯-elim (xs0β‰’x q) ; (fs m , q) β†’ m , q}) (u (fs m , q))

π•ƒβ‡”β„’βŸ¨β„¬βŸ© : 𝕃.ℬ A ⇔ β„’.ℬ A
π•ƒβ‡”β„’βŸ¨β„¬βŸ© .fun (sup , cov) = 𝕃→ℒ sup , cov
π•ƒβ‡”β„’βŸ¨β„¬βŸ© .inv ((l , xs) , cov) = ℒ→𝕃 (l , xs) , Ξ» x β†’ ∈!β„’β‡’βˆˆ!𝕃 x l xs (cov x)
π•ƒβ‡”β„’βŸ¨β„¬βŸ© .rightInv (sup , cov) i .fst = 𝕃⇔ℒ .rightInv sup i
π•ƒβ‡”β„’βŸ¨β„¬βŸ© .rightInv ((l , xs) , cov) i .snd x =
  J
    (Ξ» ys ys≑ β†’ (zs : x β„’.∈! ys) β†’ PathP (Ξ» i β†’ x β„’.∈! sym ys≑ i) zs (cov x))
    (Ξ» _ β†’ isPropIsContr _ _)
    (sym (ℒ→𝕃→ℒ l xs))
    (∈!β„’β‡’βˆˆ!𝕃 x l xs (cov x))
    i
π•ƒβ‡”β„’βŸ¨β„¬βŸ© .leftInv  (sup , cov) i .fst = 𝕃⇔ℒ .leftInv sup i
π•ƒβ‡”β„’βŸ¨β„¬βŸ© .leftInv  (sup , cov) i .snd x =
  J
    (Ξ» ys ys≑ β†’ (zs : x 𝕃.∈! ys) β†’ PathP (Ξ» i β†’ x 𝕃.∈! sym ys≑ i) zs (cov x))
    (Ξ» zs β†’ isPropIsContr _ _)
    (sym (𝕃→ℒ→𝕃 sup))
    (∈!β„’β‡’βˆˆ!𝕃 x (𝕃.length sup) (sup 𝕃.!_) (cov x))
    i