russelllim22

<script>
	import {scaleBand, scaleLinear} from 'd3-scale';
	import {csvParse} from 'd3';
	import * as cloud from 'd3-cloud'
	import { fly} from 'svelte/transition';

	let years = [], selectedYear = 2020, textFile = "", nameData = [], letters = [], letterNames = {}, letterCounts = [];
	for(let y = 1880; y<=2020; y++){
		years.push(y);
	}

AndyShiue

I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory?

A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then?

A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

xib

-- Based on the original articel at http://www.codeproject.com/Articles/22824/A-Model-to-Represent-Directed-Acyclic-Graphs-DAG-o
-- Here is a port to MySQL

-- Edge table
DROP TABLE IF EXISTS `Edge`;
CREATE TABLE IF NOT EXISTS `Edge` (
  `id` int(11) NOT NULL,
  `entry_edge_id` int(11) DEFAULT NULL COMMENT 'The ID of the incoming edge to the start vertex that is the creation reason for this implied edge; direct edges contain the same value as the Id column',
  `direct_edge_id` int(11) DEFAULT NULL COMMENT 'The ID of the direct edge that caused the creation of this implied edge; direct edges contain the same value as the Id column',
  `exit_edge_id` int(11) DEFAULT NULL COMMENT 'The ID of the outgoing edge from the end vertex that is the creation reason for this implied edge; direct edges contain the same value as the Id column',

andrejbauer

(* How do to topology in Coq if you are secretly an HOL fan.
   We will not use type classes or canonical structures because they
   count as "advanced" technology. But we will use notations.
 *)

(* We think of subsets as propositional functions.
   Thus, if [A] is a type [x : A] and [U] is a subset of [A],
   [U x] means "[x] is an element of [U]".
*)
Definition P (A : Type) := A -> Prop.

copumpkin

module Topology where

import Level
open import Function
open import Data.Empty
open import Data.Unit
open import Data.Nat hiding (_⊔_)
open import Data.Fin
open import Data.Product
open import Relation.Nullary