emilypi

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE GADTs #-}
module Data.Optics where


class Profunctor p where

iitalics

open import Level using (0ℓ)
open import Data.Nat as N using (ℕ; suc)
open import Data.Vec as Vc using (Vec; []; _∷_)
open import Data.Fin as Fn using (Fin; suc; zero)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Data.Fin.Substitution as Sbt using (Sub)

open import Codata.Thunk using (force)

Icelandjack

Non-standard operators I use :) linked to from my twitter profile

I use kind synonyms

type T   = Type
type TT  = T -> T
type TTT = T -> TT
type C   = Constraint
type TC  = T -> C