myuon

theory cantor
  imports Main
begin

definition map :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" where
  "map A B = {f. \<forall>a\<in>A. f a \<in> B}"

definition surj where
  "surj A B f = (f \<in> map A B \<and> (\<forall>b\<in>B. \<exists>a\<in>A. f a = b))"

myuon

definition (in Category) Iso where
  "Iso f g ≡ (f ∘ g ≈ id (dom g)) & (g ∘ f ≈ id (dom f))"

definition Iso_on_objects ("_ [ _ ≅ _ ]" 40) where
  "𝒞 [ A ≅ B ] ≡ (∃f∈Arr 𝒞. ∃g∈Arr 𝒞. f ∈ Hom[𝒞][A,B] & g ∈ Hom[𝒞][B,A] & Category.Iso 𝒞 f g)"

record 'c setmap =
  setdom :: "'c set"
  setcod :: "'c set"
  setfunction :: "'c ⇒ 'c"

mizchi

Atomコードリーディングメモ

ビルド方法

script/build

起動したらsrc/window-bootstrap.coffeeが起動時間のログを出してるので、そいつをgrepすると/src/broweser/atom-application.coffee が引っかかる。

src/broweser/atom-application.coffee は、 src/browser/main.coffee に呼ばれている

baseinc

BASE API v1 ドキュメント (β版)

BASEのAPIの開発者向けのドキュメントです。

概要

このAPIを使うと、あなたのアプリケーションとBASEを連携させることができます。

例えば

• BASEのアカウントでログインする
• BASEのショップの商品情報を取得する