Skip to content

Instantly share code, notes, and snippets.

View shogochiai's full-sized avatar
🚀
coding

Shogo Ochiai shogochiai

🚀
coding
View GitHub Profile

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

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

概要

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

例えば

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

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

ビルド方法

script/build

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

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

@myuon
myuon / Category3.thy
Last active March 23, 2023 11:55
Yoneda Lemma
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"
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))"