k-bx

Шановні студенти, аспіранти, викладачі!

15-17 січня 2020 року Інститут математики НАН України спільно з кафедрою математики КАУ проводить Зимову школу з математики. Програма школи – 6 цікавих вступних сюжетів сучасної математики.

Програма Зимової школи з математики

Цикли лекцій :

1. А. Дрозд. Алгебра і геометрія. Програма лекцій: Простори, точки і функції. Алгебричні многовиди й алгебричні функції. Теорема Гільберта про нулі. Словник перекладу між алгебричною й геометричною мовами.

k-bx

module Topology where

open import Data.Product public using (Σ; Σ-syntax; _×_; _,_; proj₁; proj₂; map₁; map₂)

-- Goal: encode the notion of Topology:
--
-- Let X be a non-empty set. A set τ of subsets of X
-- is said to be a topolgy on X if:
-- 
-- 1. X and the empty set, Ø, belong to τ

k-bx

module ex01 where

import prelude
import pi
import sigma
import algstruct
import category

-- Category Theory by Steve Awodey
-- Page 12. Example 12:

k-bx

module curryhoward where

-- https://queuea9.wordpress.com/2018/10/17/why-i-no-longer-believe-in-computational-classical-type-theory/

data Absurd =

data Either (A : U) (B : U) = Left (a : A)
                            | Right (b : B)

-- law of excluded middle

k-bx

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}

k-bx

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}

k-bx

cabal sandbox init
cabal install owcloud-*/
# in 3 different terminals
.cabal-sandbox/bin/owlcloud-front
.cabal-sandbox/bin/owlcloud-users
.cabal-sandbox/bin/owlcloud-albums

k-bx

Keybase proof

I hereby claim:

• I am k-bx on github.
• I am kobx (https://keybase.io/kobx) on keybase.
• I have a public key whose fingerprint is 0E1C 98EA 2448 0D24 EF5B C70C A144 9CC4 600F 1668

To claim this, I am signing this object:

k-bx

-- | This script will replace expected stdout files of failed tests
-- with actual (new) ones. This will need some careful review (see
-- turtle_review.hs)

{-# LANGUAGE OverloadedStrings #-}

import qualified Control.Foldl             as L
import           Data.List                 ((\\))
import qualified Data.Text                 as T
import           Data.Traversable          (forM)

k-bx

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}

data Req = A | B

data ReqData :: Req -> * where
    ReqDataA :: ReqData A
    ReqDataB :: ReqData B