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

module Cardinality.Finite.ManifestEnumerable.Isomorphism where

open import Prelude

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

open import Container.List.Isomorphism
open import Data.Fin
open import HITs.PropositionalTruncation.Sugar
open import Data.List using (_∷_; [])
open import HITs.PropositionalTruncation
open import Cardinality.Finite.SplitEnumerable.Isomorphism
open import Data.Sigma.Properties

π•ƒβ‡”β„’βŸ¨β„°βŸ© : 𝕃.β„° A ⇔ β„’.β„° A
π•ƒβ‡”β„’βŸ¨β„°βŸ© .fun (sup , cov) = 𝕃→ℒ sup , cov
π•ƒβ‡”β„’βŸ¨β„°βŸ© .inv (sup , cov) = ℒ→𝕃 sup , Ξ» x β†’ βˆˆβ„’β‡’βˆˆπ•ƒ x sup βˆ₯$βˆ₯ cov x
π•ƒβ‡”β„’βŸ¨β„°βŸ© .rightInv (sup , cov) = Ξ£Prop≑ (Ξ» xs x y i t β†’ squash (x t) (y t) i) (𝕃⇔ℒ .rightInv sup)
π•ƒβ‡”β„’βŸ¨β„°βŸ© .leftInv  (sup , cov) = Ξ£Prop≑ (Ξ» xs x y i t β†’ squash (x t) (y t) i) (𝕃⇔ℒ .leftInv sup)