{-# OPTIONS --without-K #-}
module FunUniverse.Agda where

open import Type
open import Data.Two using (proj′)
import Data.Vec.NP as V
import Function as F
import Data.Product as ×
open F using (const; _∘′_)
open V using ([]; _∷_)
open × using (_×_; _,_; proj₁; proj₂; uncurry)

open import Data.One using (𝟙)
open import Data.Two using (𝟚)
open import Data.Vec using (Vec)
open import Data.Bit using (0b; 1b)

open import FunUniverse.Data
open import FunUniverse.Category
open import FunUniverse.Rewiring.Linear
open import FunUniverse.Core

-→- :     
-→- A B = A  B

funCat : Category -→-
funCat = F.id , _∘′_

module Abstract𝟚 (some𝟚 : ) where

    private
        ★-U' : Universe ★₀
        ★-U' = mk 𝟙 some𝟚 _×_ Vec

    agdaFunU : FunUniverse 
    agdaFunU = ★-U' , -→-

    module AgdaFunUniverse = FunUniverse agdaFunU
 
    funLin : LinRewiring agdaFunU
    funLin = mk funCat
                 f  ×.map f F.id)
                ×.swap  {((x , y) , z)  x , (y , z) })  x  _ , x) proj₂
                 f g  ×.map f g)  f  ×.map F.id f)
                (F.const []) _ (uncurry _∷_) V.uncons

    funRewiring : Rewiring agdaFunU
    funRewiring = mk funLin _  x  x , x) (F.const []) ×.<_,_> proj₁ proj₂
                     V.rewire V.rewireTbl

open Abstract𝟚 𝟚 public

funFork : HasFork agdaFunU
funFork =  { (b , xy)     proj′ xy b })
        ,  { f g (b , x)  proj′ (f , g) b x })

agdaFunOps : FunOps agdaFunU
agdaFunOps = mk funRewiring funFork (F.const 0b) (F.const 1b)

module AgdaFunOps = FunOps agdaFunOps