andrejbauer

(* An initial attempt at universal algebra in Coq.
   Author: Andrej Bauer <Andrej.Bauer@andrej.com>

   If someone knows of a less painful way of doing this, please let me know.

   We would like to define the notion of an algebra with given operations satisfying given
   equations. For example, a group has of three operations (unit, multiplication, inverse)
   and five equations (associativity, unit left, unit right, inverse left, inverse right).
*)

AndyShiue

I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory?

A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then?

A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

atondwal

tonymorris

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE StandaloneDeriving #-}

mpilquist

/* Example of encoding Functor/Applicative/Monad from cats with Dotty 0.15 features.
 * Derived in part from Cats -- see https://github.com/typelevel/cats/blob/master/COPYING for full license & copyright.
 */
package structures

import scala.annotation._

trait Functor[F[_]] {
  def (fa: F[A]) map[A, B](f: A => B): F[B]
  def (fa: F[A]) as[A, B](b: B): F[B] =

emilypi

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


class Profunctor p where

jdegoes

final case class ZIO[-R, +E, +A](run: R => Either[E, A]) {
  final def map[B](f: A => B): ZIO[R, E, B] = 
    ZIO(r => run(r).map(f))

  final def flatMap[R1 <: R, E1 >: E, B](f: A => ZIO[R1, E1, B]): ZIO[R1, E1, B] = 
    ZIO(r => run(r).flatMap(a => f(a).run(r)))

  final def provide(r: R): ZIO[Any, E, A] = 
    ZIO(_ => run(r))

bond15

record Monad (F : Set₀ -> Set₀) : Set₁ where
  field
    return : ∀ {A : Set} -> A -> F A
    _>>=_  : ∀ {A B : Set} -> F A -> (A -> F B) -> F B
    -- laws
    leftUnit : ∀ {A B : Set}
                 (a : A)
                 (f : A -> F B)
                    -> (return a) >>= f ≡ f a
    rightUnit : ∀ {A : Set}