Define instances for GenTambara

This commit is contained in:
Kiana Sheibani 2023-03-06 10:50:30 -05:00
parent 551f238ab7
commit ac292d092e
Signed by: toki
GPG key ID: 6CB106C25E86A9F7

View file

@ -1,5 +1,6 @@
module Data.Profunctor.Strong
import Data.Tensor
import Data.Profunctor.Functor
import Data.Profunctor.Types
@ -33,10 +34,41 @@ uncurry' = rmap (uncurry id) . first
-- Tambara
public export
record GenTambara (ten, p : Type -> Type -> Type) where
record GenTambara (ten, p : Type -> Type -> Type) a b where
constructor MkTambara
getTambara : {0 c : Type} -> p (a `ten` c) (b `ten` c)
export
Bifunctor ten => Profunctor p => Profunctor (GenTambara ten p) where
dimap f g (MkTambara p) = MkTambara $ dimap (mapFst f) (mapFst g) p
export
ProfunctorFunctor (GenTambara ten) where
promap f (MkTambara p) = MkTambara (f p)
export
Tensor ten i => ProfunctorComonad (GenTambara ten) where
proextract (MkTambara p) = dimap unitr.bwd unitr.fwd p
produplicate (MkTambara p) = MkTambara $ MkTambara $ dimap assoc.bwd assoc.fwd p
export
Associative ten => Symmetric ten => Profunctor p => GenStrong ten (GenTambara ten p) where
strongl (MkTambara p) = MkTambara $ dimap assoc.bwd assoc.fwd p
strongr = dimap swap swap . strongl {ten,p=GenTambara ten p}
export
Bifunctor ten => Profunctor p => Functor (GenTambara ten p a) where
map = rmap
export
gentambara : GenStrong ten p => p :-> q -> p :-> GenTambara ten q
gentambara @{gs} f x = MkTambara $ f $ strongl @{gs} x
export
ungentambara : Tensor ten i => Profunctor q => p :-> GenTambara ten q -> p :-> q
ungentambara f x = dimap unitr.bwd unitr.fwd $ getTambara $ f x
public export
Tambara : (p : Type -> Type -> Type) -> Type
Tambara = GenTambara Pair