BartoszMilewski

module Lens

-- Concrete get/set lens
record Lens s t a b where
  constructor MkLens 
  get : s -> a
  set : s -> b -> t

unitLens : Lens a b a b 
unitLens = MkLens id (\x => id)

BartoszMilewski

module Main

data Vect : Type -> Nat -> Type where
  Nil : Vect a Z
  (::) : (x: a) -> (xs : Vect a n) -> Vect a (S n)

data Tree : Type -> Nat -> Type where
  Empty : Tree a Z
  Leaf  : a -> Tree a (S Z)
  Node  : Tree a k1 -> Tree a k2 -> Tree a (S (plus k1  k2))

BartoszMilewski

module HVect
import Data.Vect

-- Heterogeneous vector
public export
data HVect : Vect n Type -> Type where
  Nil : HVect Nil
  (::) : h -> HVect t -> HVect (h :: t)

export

BartoszMilewski

\[
 \begin{tikzcd}
 &C
 \arrow[ld, "\pi_X"']
 \arrow[rd, "\pi_Y"]
 \\
 P \langle X X \rangle
 \arrow[dr, "{P \langle id, f \rangle}"']
 &&P \langle Y, Y \rangle
 \arrow[dl, "{P \langle f, id \rangle}"]

BartoszMilewski

\begin{tikzpicture}

\def \xrightmost {2}
\def \xright     {1}
\def \xmid       {0}
\def \xleft      {-\xright}
\def \xleftmost  {-\xrightmost}

\def \ybot       {0}
\def \ymid       {1}