Kostia R k-bx

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

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

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

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

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

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:

	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 τ

	module ex01 where

	import prelude
	import pi
	import sigma
	import algstruct
	import category

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

	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

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

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

	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

 -- | 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)