masaeedu

{-# OPTIONS_GHC -Wno-name-shadowing #-}
{-# LANGUAGE AllowAmbiguousTypes, FunctionalDependencies #-}

module FinitaryContainers where

import Data.Proxy
import Data.Functor.Const
import Data.Functor.Identity
import Data.Profunctor

masaeedu

module Data.Record.Operations where

import Prelude

import Data.Functor.Variant (SProxy(..))
import Data.Variant.Internal (RLProxy(..))
import Prim.RowList (Cons, Nil, kind RowList)
import Type.Data.Boolean (True, False, kind Boolean)
import Type.Data.Symbol (class Equals)
import Type.Prelude (class ListToRow, class RowToList)

masaeedu

Resolving dependencies...
Build profile: -w ghc-8.6.4 -O1
In order, the following will be built (use -v for more details):
 - adtcorerep-0.0.0 (lib) (first run)
Configuring library for adtcorerep-0.0.0..
Preprocessing library for adtcorerep-0.0.0..
Building library for adtcorerep-0.0.0..
[1 of 3] Compiling Foo              ( src/Foo.hs, /mnt/data/depot/git/haskell/experiments/adtcorerep/dist-newstyle/build/x86_64-linux/ghc-8.6.4/adtcorerep-0.0.0/build/Foo.o )

==================== Tidy Core ====================

masaeedu

module ct.ct where

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

record relation (a : Set) (b : Set) : Set₁ where
  infix 4 _~_

  field
    _~_ : a → b → Set

masaeedu

{-# LANGUAGE LambdaCase, EmptyCase, AllowAmbiguousTypes #-}
module SOP.Products where

import MyPrelude

import GHC.Generics

import Data.Void
import Data.Proxy

masaeedu

{-# LANGUAGE LambdaCase, DeriveGeneric #-}
module Examples.Biparsing.JSON where

import MyPrelude hiding (exponent)

import GHC.Generics
import GHC.Natural

import Data.List.NonEmpty (NonEmpty(..))

masaeedu

zipr  = tabulate . zipf . bimap index index
huskr = tabulate . huskf

Right unit law
---
map2 huskr > zipr > map runit_fwd

= {definitions}
map2 (tabulate < huskf) > (tabulate < zipf < bimap index index) > map runit_fwd

masaeedu

module naryapplicative where

open import Agda.Primitive

module Functor
  where

  record functor { ℓ } (f : Set ℓ → Set ℓ) : Set (lsuc ℓ)
    where
    field

masaeedu

{-# LANGUAGE ImpredicativeTypes #-}
module Whatever where

import Data.Profunctor

newtype ForgetP p a b = ForgetP { runForgetP :: p a b }
  deriving Profunctor

class (forall p. Profunctor p => thing (t p)) => Free thing t
  where

masaeedu

Let's imagine how a given category is a monad in a bicategory of spans.

Consider the set of all the objects in the category C0 and the set of all the morphisms in the category C1 (they're all muddled together in this set). We have two functions domain : C1 -> C0 and codomain : C1 -> C0 which assign to each morphism its source and target object.

This pair of functions forms a "span" of sets, which is a diagram of this shape:

       C_1
      ╱   ╲
   dom     cod

╱ ╲