Lysxia

module R where

open import Agda.Builtin.FromNat
open import Data.Unit using (tt)
open import Data.Rational as ℚ
open import Data.Rational.Properties
open import Data.Rational.Literals as ℚ
open import Data.Nat as ℕ using (ℕ)
import Data.Nat.Properties as ℕ
import Data.Integer as ℤ

Lysxia

{-# OPTIONS --cubical #-}

module DPoly where

open import Cubical.Core.Everything
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Transport
open import Cubical.Foundations.HLevels

Lysxia

{-# LANGUAGE DeriveGeneric, DerivingVia #-}

import GHC.Generics (Generic)
import Generic.Data
import Generic.Data.Microsurgery

data R = R {a :: Int, b :: Int}
  deriving Generic
  deriving (Read, Show) via Surgery Derecordify R

Lysxia

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
module D where

import Control.Applicative (liftA2)
import Data.Kind (Type)

data F = VALUE | F :-> F

infixr 1 :->

Lysxia

monoid homomorphism is_odd : Z -> B

Categorically, a monoid (Z, 1, (*)) is described by a pair of morphisms (const 1 : () -> Z) and (uncurry (*) : Z x Z -> Z).
A monoid homomorphism is_odd : Z -> B is a morphism which makes the following diagrams commute:

           const 1
     () ------------> Z
     |                |
  id |                | is_odd
     |                |

Lysxia

{-# LANGUAGE
    ConstraintKinds,
    FlexibleContexts,
    FlexibleInstances,
    MultiParamTypeClasses,
    QuantifiedConstraints,
    RankNTypes,
    ScopedTypeVariables,
    TypeApplications,
    UndecidableInstances #-}

Lysxia

{-# LANGUAGE DeriveGeneric #-}
module Main where

import Generic.Functor
import GHC.Generics (Generic)

data T a b = C Int a b
  deriving (Show, Generic)

fmapT :: (b -> b') -> T a b -> T a b'

Lysxia

{-# LANGUAGE
    ConstraintKinds,
    FlexibleContexts,
    FlexibleInstances,
    MultiParamTypeClasses,
    QuantifiedConstraints,
    RankNTypes,
    ScopedTypeVariables,
    TypeApplications,
    UndecidableInstances #-}

Lysxia

-- Traversables as Graded functors
-- Graded functors as functors that commute with grading
--
-- Graded endofunctors on KleisliApp are Traversables
--
-- Laws omitted.

module T where

open import Level

Lysxia

{-# LANGUAGE
  DataKinds,
  PolyKinds,
  StandaloneKindSignatures,
  TypeFamilies #-}
module F where

import Data.Void
import Data.Functor.Const
import Data.Kind (Type)