masaeedu

Thank you for the helpful response and pointers. I think I need to take my time to sort this out, thanks a lot and I'll come back with a better understanding, hopefully!

I did my homework. Now I'm not so certain about everything, so please take this with a grain of salt.

Typescript's generic functions seem to act like they're contravariant over the type parameter's type bound. I'm not entirely sure though.

Playground Link

// Assignment succeeds with F<unknown> -> F<string>

masaeedu

{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedLists #-}
{-# OPTIONS_GHC -Wall #-}

module Lib where

import Control.Category ((<<<))
import Data.Function (fix)
import Data.Map (Map)
import qualified Data.Map.Lazy as Map

masaeedu

  type AccessorAndId<D> =
    | {accessor: keyof D}
    | {id: string; accessor: AccessorFunction<D>}
  export type Column<D = any> = Partial<Column.Basics> &
    Partial<
      Column.CellProps & Column.FilterProps & Column.FooterProps & Column.HeaderProps
    > &
    AccessorAndId<D> & {
      /**
       * Property name as string or Accessor

masaeedu

2269291453

masaeedu

Keybase proof

I hereby claim:

• I am masaeedu on github.
• I am masaeedu (https://keybase.io/masaeedu) on keybase.
• I have a public key ASBe0DwlBA8JuW1EKQW4eiCL4MVe9K-N9w8IXcVi0PlfSgo

To claim this, I am signing this object:

masaeedu

module Categories where

open import Level

open import Function hiding (id; _∘_)

open import Data.List
open import Data.Bool
open import Data.Product

masaeedu

module multicategory where

open import Level
open import Data.List
open import Data.Product
open import Function
open import Agda.Builtin.Equality

data Pullback {ℓ} {a b c : Set ℓ} (f : a → c) (g : b → c) : Set ℓ
  where

masaeedu

{ pkgs }:
let

lib = pkgs.lib;

trace = builtins.trace;
show = builtins.toJSON;
perturb =
  let
    nix = pkgs.fetchurl {

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

╱ ╲

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