kik kik

## q.nand
1 1 1
A0 0 0
F_SHIFT_PUTC
o0 1 1
o1 1 1
o2 1 1
o3 1 1
o4 0 0
o5 0 0
o6 1 1

## 2-category
5ページ 2行目、M^abc(l, h) は M^abc(l, g)
16ページ 最後の図式の一番右の id_c・λ_(g・f) は λ_{id_c・(g・f)} (消すid_cがずれてる)
17ページ 最初の図式、ところどころ id_c が id になってる
30ページ 最初の図の一番下のαはα^-1
33ページ 一番下の式の3行目()が一個よけい
43ページ 証明の真ん中あたり、φ_gpはφ_qp
52ページ ∵の最初の赤い丸のあたり、βとγが一か所typo
52ページ ω_a(u)_sが関手であることを示した後に、ω_aが関手であることも示さないといけなくない？
    ω_aの射の行先ω_a(f)を決めた後に、Δの確認のところで、θ_a(ω_a(f))=P(id_a)(f)も確かめないといけなさそう。
    (ω_a(u)_p)_g := φ_pg で定義することも書かないと54ページの定義より～がおかしくなりそう。

## gist:2782177
#include <cstdio>
#include <cstring>
#include <algorithm>

using namespace std;

typedef unsigned char  u8;
typedef unsigned short u16;
typedef unsigned int   u32;

## LucasLehmer.v
From mathcomp
Require Import all_ssreflect.
From mathcomp
Require Import ssralg ring_quotient finalg poly polydiv zmodp.
From mathcomp
Require Import all_fingroup cyclic.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

## B.v
Require Import Arith Even Bool List Omega.

Local Coercion is_true : bool >-> Sortclass.

Set Implicit Arguments.

(*
 * 問題の定義
 *)
Definition happiest (ps : list bool) : bool :=

## test
<!DOCTYPE html>
<html>
  <head>
    <title>Bootstrap 101 Template</title>
    <meta name="viewport" content="width=device-width, initial-scale=1.0">
    <!-- Bootstrap -->
    <link href="css/bootstrap.min.css" rel="stylesheet">

    <!-- HTML5 Shim and Respond.js IE8 support of HTML5 elements and media queries -->
    <!-- WARNING: Respond.js doesn't work if you view the page via file:// -->

## ToyPr.hs
{-# LANGUAGE TupleSections #-}

import Data.List
import Data.Maybe
import Data.IORef
import Control.Applicative
import Control.Exception hiding (try, assert)
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Error

## HoTT2.hs
-- {-# LANGUAGE RankNTypes #-}
--{-# LANGUAGE GADTs #-}
-- {-# LANGUAGE FlexibleInstances #-}
-- {-# LANGUAGE ImpredicativeTypes #-}

-- import Control.Monad.Reader

data Term = TmU Int
          | TmVar Int
          | TmProd Type Term

## LC.hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeSynonymInstances #-}
-- {-# LANGUAGE StandaloneDeriving #-}
-- {-# LANGUAGE FlexibleInstances #-}
-- {-# LANGUAGE ImpredicativeTypes #-}

import Control.Monad.Reader hiding (join)

data TermP v where

## HoTT.hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
-- {-# LANGUAGE StandaloneDeriving #-}
-- {-# LANGUAGE FlexibleInstances #-}
-- {-# LANGUAGE ImpredicativeTypes #-}

import Control.Monad.Reader hiding (join)

data TermP v where
  TmFamily   :: TermP v -> (v -> TermP v) -> TermP v
	1 1 1
	A0 0 0
	F_SHIFT_PUTC
	o0 1 1
	o1 1 1
	o2 1 1
	o3 1 1
	o4 0 0
	o5 0 0
	o6 1 1
	5ページ 2行目、M^abc(l, h) は M^abc(l, g)
	16ページ最後の図式の一番右の id_c・λ_(g・f) は λ_{id_c・(g・f)} (消すid_cがずれてる)
	17ページ最初の図式、ところどころ id_c が id になってる
	30ページ最初の図の一番下のαはα^-1
	33ページ一番下の式の3行目()が一個よけい
	43ページ証明の真ん中あたり、φ_gpはφ_qp
	52ページ ∵の最初の赤い丸のあたり、βとγが一か所typo
	52ページ ω_a(u)_sが関手であることを示した後に、ω_aが関手であることも示さないといけなくない？
	ω_aの射の行先ω_a(f)を決めた後に、Δの確認のところで、θ_a(ω_a(f))=P(id_a)(f)も確かめないといけなさそう。
	(ω_a(u)_p)_g := φ_pg で定義することも書かないと54ページの定義より～がおかしくなりそう。
	#include <cstdio>
	#include <cstring>
	#include <algorithm>

	using namespace std;

	typedef unsigned char u8;
	typedef unsigned short u16;
	typedef unsigned int u32;
	From mathcomp
	Require Import all_ssreflect.
	From mathcomp
	Require Import ssralg ring_quotient finalg poly polydiv zmodp.
	From mathcomp
	Require Import all_fingroup cyclic.

	Set Implicit Arguments.
	Unset Strict Implicit.
	Unset Printing Implicit Defensive.
	Require Import Arith Even Bool List Omega.

	Local Coercion is_true : bool >-> Sortclass.

	Set Implicit Arguments.

	(*
	* 問題の定義
	*)
	Definition happiest (ps : list bool) : bool :=
	<!DOCTYPE html>
	<html>
	<head>
	<title>Bootstrap 101 Template</title>
	<meta name="viewport" content="width=device-width, initial-scale=1.0">
	<!-- Bootstrap -->
	<link href="css/bootstrap.min.css" rel="stylesheet">

	<!-- HTML5 Shim and Respond.js IE8 support of HTML5 elements and media queries -->
	<!-- WARNING: Respond.js doesn't work if you view the page via file:// -->
	{-# LANGUAGE TupleSections #-}

	import Data.List
	import Data.Maybe
	import Data.IORef
	import Control.Applicative
	import Control.Exception hiding (try, assert)
	import Control.Monad.State
	import Control.Monad.Reader
	import Control.Monad.Error
	-- {-# LANGUAGE RankNTypes #-}
	--{-# LANGUAGE GADTs #-}
	-- {-# LANGUAGE FlexibleInstances #-}
	-- {-# LANGUAGE ImpredicativeTypes #-}

	-- import Control.Monad.Reader

	data Term = TmU Int
	\| TmVar Int
	\| TmProd Type Term
	{-# LANGUAGE RankNTypes #-}
	{-# LANGUAGE GADTs #-}
	{-# LANGUAGE TypeSynonymInstances #-}
	-- {-# LANGUAGE StandaloneDeriving #-}
	-- {-# LANGUAGE FlexibleInstances #-}
	-- {-# LANGUAGE ImpredicativeTypes #-}

	import Control.Monad.Reader hiding (join)

	data TermP v where