agda / cubical Goto Github PK
View Code? Open in Web Editor NEWAn experimental library for Cubical Agda
Home Page: https://agda.github.io/cubical/Cubical.README.html
License: Other
An experimental library for Cubical Agda
Home Page: https://agda.github.io/cubical/Cubical.README.html
License: Other
I'm hoping to add functions to get the sign of integers (from HitInt
) and rationals (for an eventual PR). So far I have this:
{-# OPTIONS --cubical --exact-split #-}
module hello-world where
open import IO
open import Cubical.HITs.HitInt renaming ( Sign to Sign'; sign to sign' )
open import Cubical.HITs.Rational
open import Cubical.Core.PropositionalTruncation
open import Cubical.Core.Everything
open import Cubical.Data.Bool
open import Cubical.Data.Nat
open import Cubical.Foundations.Function
data Sign : Set where
pos neg zero : Sign
sign-ℤ : ℤ → Sign
sign-ℤ (pos zero) = zero
sign-ℤ (pos (suc n)) = pos
sign-ℤ (neg zero) = zero
sign-ℤ (neg (suc n)) = neg
sign-ℤ (posneg i) = zero
sign-ℚ : ℚ → Sign
sign-ℚ (con u a x) = case sign-ℤ u , sign-ℤ a of λ
{ (pos , pos) → pos
; (pos , neg) → neg
; (neg , pos) → neg
; (neg , neg) → pos
; (_ , zero) → {!!}
; (zero , _) → zero
}
sign-ℚ (path u a v b x i) = {!!}
sign-ℚ (trunc q q₁ x y i i₁) = {!!}
I am however stuck on how to fill in the holes remaining. I'm still new to CTT. Any help would be appreciated.
For the following code, the type doesn't check but the color scheme makes it look like checked.
{-# OPTIONS --cubical #-}
open import Cubical.Core.Prelude
open import Cubical.Basics.Nat
Nat-test : ℕ → ℕ
Nat-test 0 = 0
Nat-test (suc n) = suc n
Nat-test-id : (Nat-test ≡ (\ x → x))
Nat-test-id i x = x
-- Nat-test-id i 0 = 0
-- Nat-test-id i (suc n) = suc n
Agda complains
Nat-test x != x of type ℕ when checking the definition of Nat-test-id
But what I got on screen was the following (so the color "checks", type doesn't):
I'm not sure if this is an issue of Agda or Cubical (or simply due to something silly for this particular color scheme, I'm using the default one). But if I do similar things in Agda without --cubical
it does complain with color:
On a side note, I wish
Nat-test-id : (Nat-test ≡ (\ x → x))
Nat-test-id i x = x
just checks. (Why doesn't it? Just because Nat-test
was defined by pattern matching?)
The following is a question/comment, rather than a bug report.
As I understand it, Agda.Builtin.Cubical.Id hardwires into
Agda-cubical Andrew Swan's trick for creating an identity type with
definitional computational rule within the cubical sets model of Type
Theory.
Why bother? There is already a perfectly good identity type with
definitional computational rule within Agda, given by
Agda.Builtin.Equality (≡). This can be proved to be path equivalent to
Agda-cubical's path type (here denoted ~ to distinguish it from
≡) -- see the proof
here.
The advantage of ≡ over Id from Agda.Builtin.Cubical.Id is that we
have access to pattern matching on refl.
I don't think they should be hand written. We can have a script for that purpose.
I asked this yesterday on SO, but I haven't gotten any bites. At this point I think that people who know Cubical Agda and the people who answer Agda questions on SO do not have much overlap so I am passing it here to see if anybody is interested.
The Cubical library is fairly advanced and I would like to see more tutorial material before I try studying it seriously.
See #110 (review)
Also @L-TChen has developed more about finite sets
https://github.com/L-TChen/FiniteSets/blob/master/FiniteSets/List/Properties.agda#L47
Right now Cubical.Data.Rational
only contains the datatype.
Arithmetic is there to be implemented!
The Book defines rationals as the set quotient Z x N / ~
where
(a, b) ~ (c, d) iff a(d + 1) = c(b + 1)
and it would be good to provide an equivalence.
Most people define the fiber of f : X -> Y
by fiber f y = Sigma(x:X), f x = y
.
Examples:
and probably all HoTT/UF libraries around, in Agda, Coq and Lean.
I suggest that, for the sake of compatibility, we adopt this definition both for the cubical path type, and for the cubical identity type. This involves not only changing the definition but also changing a few proofs/constructions. I haven't checked whether we have the definition of contractibility with the usual conventions yet.
@Saizan : There are some issues with transp
:
https://github.com/agda/cubical/blob/master/Cubical/Basics/Int.agda#L50
I was playing with Cubical Agda and got https://gist.github.com/phadej/527ad34e3bed28e5ea3e8cf9d9a2cb79 to work.
data ℤ : Set where
zero : ℤ
succ : ℤ → ℤ
pred : ℤ → ℤ
succpred : ∀ z → succ (pred z) ≡ z
predsucc : ∀ z → pred (succ z) ≡ z
trunc : isSet ℤ
...
Int≡ℤ : Int ≡ ℤ
Int≡ℤ = isoToPath (iso Int→ℤ ℤ→Int ℤ→Int→ℤ Int→ℤ→Int)
Should it be included in this library: it demonstrates the truncation problem as mentioned in http://www.cs.nott.ac.uk/~psztxa/talks/bonn18.pdf
It is rather unfortunate that Agda calls its univereses Set
. Renaming it to Type
will be much more readable.
Set
into Type
.Set
with Type
.I have no idea how these will be achieved in Agda. Some people discussed possible solutions in #77 so let's collect them here and discuss.
I wonder if we can make the proof of the 3x3 lemma for pushouts shorter in the following way:
Given the 3x3 commutative diagram, we can encode this data as 4 types (the corners), 4 type families indexed by types on the edge (the edges) and finally a type family over the total spaces of the four type families (the middle).
It is easy to show that the 4 homotopies witnessing the commutativity of the diagram can also be recovered from this "type theoretric" encoding of a 3x3 diagram. You can get the original 3x3 by looking at the total spaces of the families and the original maps become the projection maps.
Now from this consider the HIT with 4 point constructors for each of the 4 corner types. 4 path constructors making sure that coming from the middle of an edge through a corner agrees and finally a square constructor for these 4 paths.
Now the idea is that it should be simpler to show that a double pushout is equivalent to this symmetric double pushout HIT. Which you can do both ways.
I tried to formalise this in coq earlier this year, but the path algebra got a bit heavy for me. Seeing the success of the Torus, I expect this to work easily.
This was originally Mike Shulmans idea.
Here is the following coq code you can use as pseudocode:
Section Push.
Context
{A00 A10 A01 A11 : Type}
{A0x : A00 -> A01 -> Type}
{A1x : A10 -> A11 -> Type}
{Ax0 : A00 -> A10 -> Type}
{Ax1 : A01 -> A11 -> Type}
(Axx : forall a00 a01 a10 a11,
A0x a00 a01 ->
A1x a10 a11 ->
Ax0 a00 a10 ->
Ax1 a01 a11 -> Type).
Local Definition B00 := A00.
Local Definition B10 := A10.
Local Definition B01 := A01.
Local Definition B11 := A11.
Local Definition B0x := {a00 : A00 & {a01 : A01 & A0x a00 a01}}.
Local Definition B1x := {a10 : A10 & {a11 : A11 & A1x a10 a11}}.
Local Definition Bx0 := {a00 : A00 & {a10 : A10 & Ax0 a00 a10}}.
Local Definition Bx1 := {a01 : A01 & {a11 : A11 & Ax1 a01 a11}}.
Local Definition Bxx := {a00 : A00 & {a01 : A01 & {a10 : A10 & {a11 : A11 &
{a0x : A0x a00 a01 & {a1x : A1x a10 a11 &
{ax0 : Ax0 a00 a10 & {ax1 : Ax1 a01 a11 &
Axx a00 a01 a10 a11 a0x a1x ax0 ax1}}}}}}}}.
Local Definition fi0 : Bx0 -> B00 := pr1.
Local Definition fj0 : Bx0 -> B10 := fun x => pr1 (pr2 x).
Local Definition f'ix : Bxx -> B0x := fun a => (a.1; a.2.1; a.2.2.2.2.1).
Local Definition fjx : Bxx -> B1x := fun a => (a.2.2.1; a.2.2.2.1; a.2.2.2.2.2.1).
Local Definition fi1 : Bx1 -> B01 := pr1.
Local Definition fj1 : Bx1 -> B11 := fun x => pr1 (pr2 x).
Local Definition f0i : B0x -> B00 := pr1.
Local Definition f0j : B0x -> B01 := fun x => pr1 (pr2 x).
Local Definition fxi : Bxx -> Bx0 := fun a => (a.1; a.2.2.1; a.2.2.2.2.2.2.1).
Local Definition fxj : Bxx -> Bx1 := fun a => (a.2.1; a.2.2.2.1; a.2.2.2.2.2.2.2.1).
Local Definition f1i : B1x -> B10 := pr1.
Local Definition f1j : B1x -> B11 := fun x => pr1 (pr2 x).
Private Inductive SymP :=
| a : B00 -> SymP
| b : B10 -> SymP
| c : B01 -> SymP
| d : B11 -> SymP.
Axiom H1 : a o f0i == c o f0j.
Axiom H2 : a o fi0 == b o fj0.
Axiom H3 : c o fi1 == d o fj1.
Axiom H4 : b o f1i == d o f1j.
Axiom sq
: forall x,
Square (H1 (f'ix x)) (H4 (fjx x)) (H2 (fxi x)) (H3 (fxj x)).
Unlike the main Agda repository, this one doesn't have a licence file in it. It would probably be a good idea to add one, perhaps similar to the one in the main Agda repository? That one appears to be based on the MIT licence.
I wonder what's the standard practice to solve module dependency circle? Say I have two modules A.agda
and B.agda
. In A.agda
there is
import B
fooA = ...
barA = ...fooB...
while in B.agda
there is
import A
fooB = ...fooA...
barB = ...barA...
This makes a dependency circle which agda won't be happy about. The first solution is of course better modulization. But some times it just feel more "right" to split definitions like the above (and I believe there are numerous examples of these). In that case, how do we handle this?
After the commit agda/agda@13d516f, Cubical.Core.Glue
isn't working anymore. Here is the error message:
unglueIsEquiv A (~ i0 ∨ i0)
(λ { (i0 = i0) → A , idEquiv A ; (i0 = i1) → w })
!= idIsEquiv A of type isEquiv (unglue (~ i0 ∨ i0))
when checking that the expression
λ i →
let f : PartialP (~ i ∨ i) (λ x → Σ-syntax (Set ℓ) λ T → T ≃ A)
f = λ { (i = i0) → A , idEquiv A ; (i = i1) → w }
in Glue A f , unglueEquiv _ _ f
has type (A , idEquiv A) ≡ w
Currently travis didn't finish. Can someone restart?
as discussed in #134
I suppose this issue also includes defining localization and finally showing that the two definitions of truncation are the same.
I see there're definitions of 1024 in different representations of int/nats, it's good to have them. But they're exposed as a public function, it's not what we expect for a library.
Is it better to make them private?
There's a comment in Cubical.Core.Glue
that it contains a proof of univalence:
Proof of univalence using that unglue is an equivalence (
EquivContr
)
and then there is a module at the end with
EquivContr : ∀ {ℓ} (A : Set ℓ) → isContr (Σ[ T ∈ Set ℓ ] T ≃ A) module _ {ℓ : I → Level} (P : (i : I) → Set (ℓ i)) where pathToEquiv : A ≃ B
Do these prove univalence? Do they provide all the kit needed to prove it? I have absolutely no idea. As a regular user, what would be useful is if there was an explicitly spelled out univalence witness:
univalence : ∀ {ℓ} {A B : Set ℓ} → (A ≡ B) ≃ (A ≃ B)
We have quite a few stale branches in this repo at the moment. Since most of these have been merged or abandoned, can we delete them?
There will soon be some proper documentation for Cubical Agda (agda/agda#3571). Once this has been merged I plan to shrink the core a bit (some parts are just there as documentation and have now been incorporated into the proper documentation) and update the README so that it reflects what is actually in the library.
The paper states this about transport
.
transport : ∀ {A B : Set} → A ≡ B → A → B
transport p a = transp (λ i → p i) i0 a
This is defined using another primitive of Cubical Agda called transp. It is a generalization of the regular transport principle which lets us specify where the transport is the identity function. In particular, when the second argument to transp is i1 it will reduce to a, which let us prove that transp A r a is always path equal to a (cf. addp later).
So I'd expect something like the following to hold based on that description.
transport : ∀ {A B : Set} → A ≡ B → A → A
transport p a = transp (λ i → p i) i1 a
It gives me a type error. Also, I'd expect the first argument to not matter when the second is i1
since it is stated that it reduces to a
in that case, but experimenting I haven't found this to be true. The function is not symmetric in the second argument and playing around, I haven't be able to make it pass typechecking. So what is it supposed to be doing?
I can think of at least one use case for ghcomp
namely the definition of compPath
. This definition is judgmentally equal to the current one.
ghcomp : ∀ {ℓ} {A : Set ℓ} {φ : I}
(u : I → Partial φ A)
(u0 : Sub A φ (u i0)) → A
ghcomp {φ = φ} u u0 = hcomp {φ = φ ∨ ~ φ}
(λ { j (φ = i1) → u j 1=1
; j (φ = i0) → ouc u0} )
(ouc u0)
ghfill : ∀ {ℓ} {A : Set ℓ} {φ : I}
(u : I → Partial φ A)
(u0 : Sub A φ (u i0))
------------------------
(i : I) → A
ghfill {φ = φ} u u0 i = ghcomp (λ { j (φ = i1) → u (i ∧ j) 1=1
; j (i = i0) → ouc (u0)})
(inc {φ = φ ∨ ~ i} (ouc u0))
compPath : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
compPath p q i = ghcomp {φ = i} (λ j _ → q j) (inc (p i))
fillPath : {A : Set} {x y z : A} (p : x ≡ y) (q : y ≡ z)
→ I → I → A
fillPath {x = x} p q j i = ghfill {φ = i} (λ j _ → q j) (inc (p i)) j
Now, with variable
keyword, codes like
f0 : forall {i} {A : Set i} -> blabla
f1 : forall {i} {A : Set i} -> blabla
can be replaced with
variable
i : Level
A : Set i
f0 : blabla
f1 : blabla
which makes the code more readable.
For my master thesis about cubical type theory, I am proving a kind of structure invariance principle for magmas with this library.
At some point in the proof I have the following given:
f : ℕ → ℕ₀
f
: fIso : Iso ℕ ℕ₀
invIso : Iso A B → Iso B A
Now, I would like to prove that
sym (ua (isoToEquiv fIso)) ≡ ua (isoToEquiv (invIso fIso))
Is this a valid theorem in HoTT? Are there built-in functions in this library that may help in the proof?
Currently the readme talks about making an agda sandbox, but doesn't specify what to do afterwards. For those who aren't so familiar with agda, this isn't completely obvious. Could you add some clearer installation instructions?
This library seems to be getting a lot of development effort at the moment, and it looks like it's going to develop into a useful base library for those interested in using cubical Agda. I'm not sure how much thought has been put into its layout? I was wondering if you'd considered using the structure of the standard library (where applicable)?
The advantages would be:
Obviously I realise it wouldn't be possible to mimic everything!
When I run Primitives.agda, I get:
C:\Users\wand\Dropbox\Work\Research\Cubicaltt 2018\cubical-agda\Cubical\Core\Primitives.agda:86,10: Not a valid pattern: i = i0
=<ERROR>
Set
sys i (i = i1) = Set
I am running Agda version 2.5.4.1
What am I doing wrong?
I think we can make use of CIs to improve PR process and ensure this library is working under at least a specific revision of Agda (and we update this revision from time to time).
Another question: Travis or Circle?
as discussed in #134
cubical/Cubical/Foundations/HLevels.agda
Lines 28 to 34 in 27ec388
Has
B : A → Type ℓ
should it rather be
B : A → Type ℓ' -- primed
I checked out the master branch and ran make. GHC 8.0.2 and Agda 2.6.0. Error:
agda Cubical/Core/Everything.agda Checking Cubical.Core.Everything (/Users/ruben/Documents/thirdparty/cubical/Cubical/Core/Everything.agda). Checking Cubical.Core.Primitives (/Users/ruben/Documents/thirdparty/cubical/Cubical/Core/Primitives.agda). /Users/ruben/Documents/thirdparty/cubical/Cubical/Core/Primitives.agda:193,3-196,16 A (i ∧ i0) → A (i ∧ i1) !=< A i of type Set (ℓ-max (ℓ′ (i ∧ i0)) (ℓ′ (i ∧ i1))) when checking that the inferred type of an application A (i ∧ i0) → A (i ∧ i1) matches the expected type A i make: *** [check] Error 1
https://github.com/agda/cubical/blob/master/Cubical/Core/README.md mentions HoTT-UF which does not exist.
This is referred from agda/doc/user-manual/language/cubical, which is likely outdated.
There is a tool in Agda to fix the whitespace issue. The following is the explanation from the tool
Background: Agda was reported to fail to compile on Windows because a file did not end with a newline character (Agda uses -Werror).
If this is still an issue, then this check should be included in the Makefile so that Travis can check it as well.
Unfortunately, I will be unavailable for a few week, so I won't be able to make a PR on this.
Normalizing the application of +-comm
to cubical numerals fails for relatively low values such as for example in +-comm 4 6
. Is this normal expected behaviour? Normalization works for any number when the implementation of the numerals in the standard library is used.
I've read that the interval is supposed to be defined on the real line. I find this absolutely mystifying given that its purpose is to map between discrete types in various places.
It would be better if the core library does not rely on reversals so that it is compatible with the simplicial set model
I see the definitions' names are in a mess, names like binnat
, HitInt
are used together .
Should we have a convention for naming? Like following the stdlib directly?
I see there's a lot of HITs, it's good.
Can we have properties for them? Like plus/times assoc/comm?
I'll open this "issue" as a place to discuss various cubical things, like "how to prove X cubically", as suggested by @3abc .
Let me open up with two questions that came up in agda/agda#3599.
transport p ≡ transport q → p ≡ q
https://github.com/agda/agda/blob/master/src/data/lib/prim/Agda/Builtin/Cubical/Glue.agda#L104
A slick proof that transport
is an equivalence is the following:
isEquivTransport : ∀ {ℓ} {A B : Set ℓ} (p : A ≡ B) → isEquiv (transport p)
isEquivTransport {A = A} {B = B} p =
transport (λ i → isEquiv (λ x → transp (λ j → p (i ∧ j)) (~ i) x)) (idIsEquiv A)
transportEquiv : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A ≃ B
transportEquiv p = (transport p , isEquivTransport p)
What's going on in pathToEquiv
is very similar, but I can't figure out how to get an analogous proof to typecheck... Any ideas? @Saizan
The file https://github.com/agda/cubical/blob/master/Cubical/Foundations/Logic.agda should be made universe polymorphic and Ω should be removed in favour of hProp
_[_↦_] : ∀ {ℓ} (A : Set ℓ) (φ : I) (u : Partial φ A) → Setω
A [ φ ↦ u ] = Sub A φ u
There is just too little information in the documentation on how to use these or what are their purpose. Because Sub
is built in, I can't gleam anything from it.
inc : ∀ {ℓ} {A : Set ℓ} {φ : I} (u : A) → A [ φ ↦ (λ _ → u) ]
ouc : ∀ {ℓ} {A : Set ℓ} {φ : I} {u : Partial φ A} → A [ φ ↦ u ] → A
Also these two do not seem to be in the library. Are they supposed to be builtins or is it possible to define them?
One of the things I like about the HoTT-coq library is that truncations are defined as modalities, then many results about truncations come from their more general counter-parts for modalities. it will be a bit of a long project to write a modalities library for cubical agda but I think it could be done. The advantage would be that many results such as Blakers-Massey will end up holding in much greater generality, I have been trying to prove GBMT for a while in HoTT-coq now but there are many technical small lemmas that are needed. It would be very interesting to see if cubical can help.
Another thing I would be interested to see is Bruneries 3x3 lemma in cubical. Showing that pushouts commute with pushouts on a 3x3 square of span rows and columns. This has been proven in the agda library but I struggled to prove it in coq.
In the following code I was trying to define Sphere n
as a HIT depending on n
. If I do this with S²
or S³
it works fine. But it won't check Sphere n
if I uncomment cell
. In theory this should work, right?
PtType : Set₁
PtType = Σ Set (λ A → A)
Ω1 : PtType → PtType
Ω1 A = ((A .snd) ≡ (A .snd)) , refl
Ω : (n : ℕ) → PtType → PtType
Ω 0 A = A
Ω (suc n) A = Ω1 (Ω n A)
data S² : Set where
base : S²
surf : (Ω 2 (S² , base)) .fst
data S³ : Set where
base : S³
cell : (Ω 3 (S³ , base)) .fst
data Sphere : ℕ → Set where
base : (n : ℕ) → Sphere n
--cell : (n : ℕ) → (Ω n (Sphere n , base n)) .fst
PS E:\TheoremProving\CubicalAgdaStuff\cubical> make
cabal exec -- fix-agda-whitespace --check
Warning: The exec command is a part of the legacy v1 style of cabal usage.
Please switch to using either the new project style and the new-exec command
or the legacy v1-exec alias as new-style projects will become the default in
the next version of cabal-install. Please file a bug if you cannot replicate a
working v1- use case with the new-style commands.
For more information, see: https://wiki.haskell.org/Cabal/NewBuild
cabal: The program 'fix-agda-whitespace' is required but it could not be
found.
make: *** [GNUmakefile:11: check-whitespace] Error 1
I know that make
which I got through Chocolatey works as I needed to use it for Proof General + Coq. I tried cabal install fix-agda-whitespace
, but am getting nothing.
Also I get a type error when I try to typecheck the Cubical.Core.Primitives
file.
E:\TheoremProving\CubicalAgdaStuff\cubical\Cubical\Core\Primitives.agda:193,3-196,16
A (i ∧ i0) → A (i ∧ i1) !=< A i of type
Set (ℓ-max (ℓ′ (i ∧ i0)) (ℓ′ (i ∧ i1)))
when checking that the inferred type of an application
A (i ∧ i0) → A (i ∧ i1)
matches the expected type
A i
This is for ...
-- Heterogeneous filling defined using comp
fill : (A : ∀ i → Type (ℓ′ i))
{φ : I}
(u : ∀ i → Partial φ (A i))
(u0 : A i0 [ φ ↦ u i0 ])
---------------------------
(i : I) → A i
fill A {φ = φ} u u0 i =
comp (λ j → A (i ∧ j))
(λ j → λ { (φ = i1) → u (i ∧ j) 1=1
; (i = i0) → outS u0 })
(outS u0)
I do not think this error is related to the build failure which makes it that much more puzzling. I got Agda 2.6.0.1 just now. Should I try going back to 2.6.0?
It would be very nice to have cubical Agda to internally translate pattern matching on refl (with --without-K) to path induction. This would not only make proofs more readable, but also would allow existing Agda developments to migrate seamlessly to cubical Agda.
In particular, I am eager to try my own existing development with cubical Agda. I deliberately designed it so that all "univalent" features are explicit assumptions (univalence, functional extensionality, propositional truncation, and everything).
However, because my developement doesn't use J, I can't just supply such assumptions as data and test the computational behaviour of cubical Agda. Because my codebase has 30k lines, it is not an option to just manually convert all uses of pattern matching on refl to uses of J.
In principle we know the theory to convert the use of pattern matching to eliminators automatically, at least if one uses --exact-split, which I do. Moreover, I take care of making definitions in Agda so that I know that they are more or less directly translatable in an automatic way to Martin-Loef combinators.
It should be possible to translate "well behaved code" that relies on without-K-pattern-matching-on-refl to cubicaltt combinators automatically internally in Agda in a transparent way.
I realized that cong
is actually function composition on path lambdas. Is it a good idea to rename it into _∘_
, which is function composition in the stdlib?
So we can browse this project easier.
BTW I need an admin (like @UlfNorell) to enable gh-pages rendering for this repo.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.