A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://agda.github.io/agda-stdlib/master/Data.Product.Effectful.Left.Base.html below:

Data.Product.Effectful.Left.Base

Data.Product.Effectful.Left.Base
------------------------------------------------------------------------
-- The Agda standard library
--
-- Base definitions for the left-biased universe-sensitive functor and
-- monad instances for the Product type.
--
-- To minimize the universe level of the RawFunctor, we require that
-- elements of B are "lifted" to a copy of B at a higher universe level
-- (a ⊔ b). See the Data.Product.Effectful.Examples for how this is
-- done.
------------------------------------------------------------------------

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

open import Level

module Data.Product.Effectful.Left.Base
  {a} (A : Set a) (b : Level) where

open import Data.Product.Base using (_×_; map₂; proj₁; proj₂; <_,_>)
open import Effect.Functor using (RawFunctor)
open import Effect.Comonad using (RawComonad)

------------------------------------------------------------------------
-- Definitions

Productₗ : Set (a  b)  Set (a  b)
Productₗ B = A × B

functor : RawFunctor Productₗ
functor = record { _<$>_ = λ f  map₂ f }

comonad : RawComonad Productₗ
comonad = record
  { extract = proj₂
  ; extend  = < proj₁ ,_>
  }

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4