text:
#include "AppClass.h"
void Application::InitVariables(void)
{
	m_pCameraMngr->SetCameraMode(CAM_ORTHO_Z);

	//init the mesh
	m_pMesh = new MyMesh();
	m_pMesh->GenerateCube(1.0f, C_BLUE);

}
void Application::Update(void)
{
	//Update the system so it knows how much time has passed since the last call
	m_pSystem->Update();

	//Is the arcball active?
	ArcBall();

	//Is the first person camera active?
	CameraRotation();
}
void Application::Display(void)
{
	// Clear the screen
	ClearScreen();

	matrix4 m4View = m_pCameraMngr->GetViewMatrix();
	matrix4 m4Projection = m_pCameraMngr->GetProjectionMatrix();

	matrix4 m4Scale = glm::scale(IDENTITY_M4, vector3(2.0f,2.0f,2.0f));
	static float value = 0.0f;
	matrix4 m4Translate = glm::translate(IDENTITY_M4, vector3(value, 0.0f, 0.0f));
	value += 0.03f;

	//matrix4 m4Model = m4Translate * m4Scale;
	matrix4 m4Model = m4Scale * m4Translate;
	m_pMesh->Render(m4Projection, m4View, m4Model);

	matrix4 m4Origin = m4Model;

	//matrix4 m4Translate;

	//right of start
	for (int i = 0; i < 5; i++)
	{
		m4Translate = glm::translate(m4Model, vector3(1.0f, 0.0f, 0.0f));
		m4Model = m4Translate;
		m_pMesh->Render(m4Projection, m4View, m4Model);
	}
	for (int i = 0; i < 2; i++)
	{
		m4Translate = glm::translate(m4Model, vector3(0.0f, -1.0f, 0.0f));
		m4Model = m4Translate;
		m_pMesh->Render(m4Projection, m4View, m4Model);
	}
	//snap back to the origin
	m4Model = m4Origin;

	//left of start
	for (int i = 0; i < 5; i++)
	{
		m4Translate = glm::translate(m4Model, vector3(-1.0f, 0.0f, 0.0f));
		m4Model = m4Translate;
		m_pMesh->Render(m4Projection, m4View, m4Model);
	}
	for (int i = 0; i < 2; i++)
	{
		m4Translate = glm::translate(m4Model, vector3(0.0f, -1.0f, 0.0f));
		m4Model = m4Translate;
		m_pMesh->Render(m4Projection, m4View, m4Model);
	}
	//snap back to the origin
	m4Model = m4Origin;

	//go down a line
	m4Translate = glm::translate(m4Model, vector3(0.0f, -1.0f, 0.0f));
	m4Model = m4Translate;
	m_pMesh->Render(m4Projection, m4View, m4Model);

	//right
	for (int i = 0; i < 3; i++)
	{
		m4Translate = glm::translate(m4Model, vector3(1.0f, 0.0f, 0.0f));
		m4Model = m4Translate;
		m_pMesh->Render(m4Projection, m4View, m4Model);
	}
	for (int i = 0; i < 1; i++)
	{
		m4Translate = glm::translate(m4Model, vector3(0.0f, -1.0f, 0.0f));
		m4Model = m4Translate;
		m_pMesh->Render(m4Projection, m4View, m4Model);
	}

	//snap back to the origin
	m4Model = m4Origin;
	m4Translate = glm::translate(m4Model, vector3(0.0f, -1.0f, 0.0f));
	m4Model = m4Translate;

	//left
	for (int i = 0; i < 3; i++)
	{
		m4Translate = glm::translate(m4Model, vector3(-1.0f, 0.0f, 0.0f));
		m4Model = m4Translate;
		m_pMesh->Render(m4Projection, m4View, m4Model);
	}
	for (int i = 0; i < 1; i++)
	{
		m4Translate = glm::translate(m4Model, vector3(0.0f, -1.0f, 0.0f));
		m4Model = m4Translate;
		m_pMesh->Render(m4Projection, m4View, m4Model);
	}

	//snap back to the origin
	m4Model = m4Origin;
	m4Translate = glm::translate(m4Model, vector3(0.0f, -3.0f, 0.0f));
	m4Model = m4Translate;

	//right
	for (int i = 0; i < 2; i++)
	{
		m4Translate = glm::translate(m4Model, vector3(1.0f, 0.0f, 0.0f));
		m4Model = m4Translate;
		m_pMesh->Render(m4Projection, m4View, m4Model);
	}

	m4Translate = glm::translate(m4Model, vector3(-2.0f, 0.0f, 0.0f));
	m4Model = m4Translate;

	//left
	for (int i = 0; i < 2; i++)
	{
		m4Translate = glm::translate(m4Model, vector3(-1.0f, 0.0f, 0.0f));
		m4Model = m4Translate;
		m_pMesh->Render(m4Projection, m4View, m4Model);
	}

	//snap back to the origin
	m4Model = m4Origin;
	//go up a line
	m4Translate = glm::translate(m4Model, vector3(0.0f, 1.0f, 0.0f));
	m4Model = m4Translate;
	m_pMesh->Render(m4Projection, m4View, m4Model);

	//right
	m4Translate = glm::translate(m4Model, vector3(1.0f, 0.0f, 0.0f));
	m4Model = m4Translate;
	m_pMesh->Render(m4Projection, m4View, m4Model);

	m4Translate = glm::translate(m4Model, vector3(2.0f, 0.0f, 0.0f));
	m4Model = m4Translate;
	m_pMesh->Render(m4Projection, m4View, m4Model);

	m4Translate = glm::translate(m4Model, vector3(1.0f, 0.0f, 0.0f));
	m4Model = m4Translate;
	m_pMesh->Render(m4Projection, m4View, m4Model);

	//snap back to the origin
	m4Model = m4Origin;
	//go up a line
	m4Translate = glm::translate(m4Model, vector3(0.0f, 1.0f, 0.0f));
	m4Model = m4Translate;
	//left
	m4Translate = glm::translate(m4Model, vector3(-1.0f, 0.0f, 0.0f));
	m4Model = m4Translate;
	m_pMesh->Render(m4Projection, m4View, m4Model);

	m4Translate = glm::translate(m4Model, vector3(-2.0f, 0.0f, 0.0f));
	m4Model = m4Translate;
	m_pMesh->Render(m4Projection, m4View, m4Model);

	m4Translate = glm::translate(m4Model, vector3(-1.0f, 0.0f, 0.0f));
	m4Model = m4Translate;
	m_pMesh->Render(m4Projection, m4View, m4Model);

	//snap back to the origin
	m4Model = m4Origin;
	//go up 2 lines
	m4Translate = glm::translate(m4Model, vector3(0.0f, 2.0f, 0.0f));
	m4Model = m4Translate;
	m_pMesh->Render(m4Projection, m4View, m4Model);

	//right
	for (int i = 0; i < 3; i++)
	{
		m4Translate = glm::translate(m4Model, vector3(1.0f, 0.0f, 0.0f));
		m4Model = m4Translate;
		m_pMesh->Render(m4Projection, m4View, m4Model);
		if (i == 1)
		{
			m4Translate = glm::translate(m4Model, vector3(0.0f, 1.0f, 0.0f));
			m4Model = m4Translate;
			m_pMesh->Render(m4Projection, m4View, m4Model);
			m4Translate = glm::translate(m4Model, vector3(0.0f, -1.0f, 0.0f));
			m4Model = m4Translate;

		}
		if (i == 2)
		{
			m4Translate = glm::translate(m4Model, vector3(0.0f, 2.0f, 0.0f));
			m4Model = m4Translate;
			m_pMesh->Render(m4Projection, m4View, m4Model);
			m4Translate = glm::translate(m4Model, vector3(0.0f, -2.0f, 0.0f));
			m4Model = m4Translate;
		}
	}
	//snap back to the origin
	m4Model = m4Origin;
	//go up 2 lines
	m4Translate = glm::translate(m4Model, vector3(0.0f, 2.0f, 0.0f));
	m4Model = m4Translate;

	//left of start
	for (int i = 0; i < 3; i++)
	{
		m4Translate = glm::translate(m4Model, vector3(-1.0f, 0.0f, 0.0f));
		m4Model = m4Translate;
		m_pMesh->Render(m4Projection, m4View, m4Model);
		if (i == 1)
		{
			m4Translate = glm::translate(m4Model, vector3(0.0f, 1.0f, 0.0f));
			m4Model = m4Translate;
			m_pMesh->Render(m4Projection, m4View, m4Model);
			m4Translate = glm::translate(m4Model, vector3(0.0f, -1.0f, 0.0f));
			m4Model = m4Translate;

		}
		if (i == 2)
		{
			m4Translate = glm::translate(m4Model, vector3(0.0f, 2.0f, 0.0f));
			m4Model = m4Translate;
			m_pMesh->Render(m4Projection, m4View, m4Model);
			m4Translate = glm::translate(m4Model, vector3(0.0f, -2.0f, 0.0f));
			m4Model = m4Translate;
		}
	}

	// draw a skybox
	m_pMeshMngr->AddSkyboxToRenderList();

	// draw the grid
	m_pMeshMngr->AddGridToRenderList();

	//render list call
	m_uRenderCallCount = m_pMeshMngr->Render();

	//clear the render list
	m_pMeshMngr->ClearRenderList();

	//draw gui
	DrawGUI();

	//end the current frame (internally swaps the front and back buffers)
	m_pWindow->display();
}
void Application::Release(void)
{
	SafeDelete(m_pMesh);

	//release GUI
	ShutdownGUI();
}

extension: cpp


text:
require obexpush_${PV}.bb
inherit native

do_stage() {
	:
}

do_install() {
	:
}

SRC_URI[md5sum] = "edb66ba97fe6c84b6160c670c4bcdea8"
SRC_URI[sha256sum] = "341c6865aa392b6cf056e1bd9cda53d2f31a942460087ad22d6f6dc91bb0bd0e"

license: MIT

repository: overo/overo-oe-natty

license_type: permissive

repo_name: overo/overo-oe-natty

branch_name: HEAD

extension: bb


text:
# Copyright (c) 2021-2022 Huawei Device Co., Ltd.
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
# http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.

# 32-bits pointers optimization in Panda for objects => addresses usage low 4GB
# We need use linker scripts for section replacement above 4GB
# Note: AddressSanitizer reserves (mmap) addresses for its own needs,
#       so we have difference start addresses for asan and default buildings
function(panda_add_executable target)
    # When using rapidcheck we should use linker scripts with
    # definitions for exception handling sections
    cmake_parse_arguments(ARG "RAPIDCHECK_ON" "" "" ${ARGN})

    add_executable(${target} ${ARG_UNPARSED_ARGUMENTS})

    if(PANDA_USE_32_BIT_POINTER AND NOT (PANDA_TARGET_MOBILE OR PANDA_TARGET_WINDOWS OR PANDA_TARGET_MACOS OR PANDA_TARGET_OHOS))
        if(ARG_RAPIDCHECK_ON)
            set(LINKER_SCRIPT_ARG "-Wl,-T,${PANDA_ROOT}/ldscripts/panda_test_asan.ld")
        else()
            set(LINKER_SCRIPT_ARG "-Wl,-T,${PANDA_ROOT}/ldscripts/panda.ld")
        endif()
        if(PANDA_ENABLE_ADDRESS_SANITIZER)
            # For cross-aarch64 with ASAN with linker script we need use additional path-link
            # Here we use default addresses space (without ASAN flag). It is nuance of cross-building.
            if(PANDA_TARGET_ARM64)
                set(LINKER_SCRIPT_ARG "-Wl,-rpath-link,${PANDA_SYSROOT}/lib ${LINKER_SCRIPT_ARG}")
            else()
                set(LINKER_SCRIPT_ARG "-Wl,--defsym,LSFLAG_ASAN=1 ${LINKER_SCRIPT_ARG}")
            endif()
        endif()
        # We need use specific options for AMD64 building with Clang compiler
        # because it is necessary for placement of sections above 4GB
        if(CMAKE_CXX_COMPILER_ID STREQUAL "Clang" AND PANDA_TARGET_AMD64)
            set(LINKER_SCRIPT_ARG "${LINKER_SCRIPT_ARG} -pie")
            # -mcmodel=large with clang and asan on x64 leads to bugs in rapidcheck with high-mem mappings
            # so for rapidcheck test binaries panda_test_asan.ld is used which does not require
            # -mcmodel=large option
            if(NOT ARG_RAPIDCHECK_ON)
                target_compile_options(${target} PUBLIC "-mcmodel=large")
            endif()
        endif()
        target_link_libraries(${target} ${LINKER_SCRIPT_ARG})
    endif()
endfunction()

# This function need for non-SHARED libraries
# It is necessary for 32-bits pointers via amd64 building with Clang compiler
function(panda_set_lib_32bit_property target)
    if(PANDA_USE_32_BIT_POINTER AND PANDA_TARGET_AMD64 AND CMAKE_CXX_COMPILER_ID STREQUAL "Clang")
        set_property(TARGET ${target} PROPERTY POSITION_INDEPENDENT_CODE ON)
    endif()
endfunction()

branch_name: refs/heads/master

extension: cmake


text:
require xorg-app-common.inc
DEPENDS += " virtual/libx11 libxmu xbitmaps libxt"
PE = "1"

SRC_URI[archive.md5sum] = "98200c358e5401d648b980564d9ae39d"
SRC_URI[archive.sha256sum] = "863f673518af19f9ae35ee221b30bf8c8b695c76c543d18b3ac400a51b855c41"


text:
package internal

import (
	"bufio"
	"fmt"
	"io/ioutil"
	"log"
	"net/http"
	"net/http/cookiejar"
	"net/url"
	"os"
	"strings"

	"golang.org/x/crypto/ssh/terminal"
)

type Shopper struct {
	http.Client
}

func NewShopperWithCookies(cookies []*http.Cookie) (*Shopper, error) {
	cookieJar, err := cookiejar.New(nil)
	if err != nil {
		return nil, err
	}
	u, err := url.Parse(BaldorHost)
	if err != nil {
		return nil, err
	}
	cookieJar.SetCookies(u, cookies)
	return &Shopper{http.Client{Jar: cookieJar}}, nil
}

func NewShopperWithAuthentication(email, pass string) (*Shopper, error) {
	cookieJar, err := cookiejar.New(nil)
	if err != nil {
		return nil, err
	}
	shopper := &Shopper{http.Client{Jar: cookieJar}}

	if _, err := shopper.PostForm(URLNewLogin, url.Values{
		"EmailLoginForm[email]":      {email},
		"EmailLoginForm[password]":   {pass},
		"EmailLoginForm[rememberMe]": {"1"},
		"yt0":                        {"SIGN IN"},
	}); err != nil {
		return nil, err
	}
	if _, err := shopper.Get(URLCart); err != nil {
		return nil, err
	}
	return shopper, nil
}

func (s *Shopper) AddToCart(productKey, unit string) (int, error) {
	v := url.Values{
		"ShoppingCartModel[key]":      {productKey},
		"ShoppingCartModel[unit]":     {unit},
		"ShoppingCartModel[quantity]": {"1"},
		"qty":                         {"1"},
	}
	resp, err := s.PostForm(URLAddToCart, v)
	if err != nil {
		return resp.StatusCode, err
	}
	defer resp.Body.Close()
	b, err := ioutil.ReadAll(resp.Body)
	if err != nil {
		return http.StatusInternalServerError, err
	}
	if strings.Contains(string(b), "error") {
		// The response always returns a status 200, even when there is an
		// error.
		return http.StatusInternalServerError, fmt.Errorf("Error adding to cart: %q; values = %v", string(b), v)
	}
	log.Printf("Success! %q\n", string(b))
	return http.StatusOK, nil
}

func BaldorCookie(j http.CookieJar) (*http.Cookie, error) {
	u, err := url.Parse(BaldorHost)
	if err != nil {
		return nil, err
	}
	cookie := &http.Cookie{}
	for _, c := range j.Cookies(u) {
		if c.Name == "provided_access" || c.Name == "PHPSESSID" || c.Name == "SESSION" {
			continue
		}
		log.Printf("BALDORFOOD_COOKIE_NAME=%q\n", c.Name)
		log.Printf("BALDORFOOD_COOKIE_VALUE=%q\n", c.Value)
		cookie.Name = c.Name
		cookie.Value = c.Value
	}
	if cookie.Name == "" {
		return nil, fmt.Errorf("Authentication cookie not found")
	}
	return cookie, nil
}

func ReadEmailAndPassword() (string, string, error) {
	reader := bufio.NewReader(os.Stdin)
	fmt.Printf("Enter email: ")
	email, err := reader.ReadString('\n')
	if err != nil {
		return "", "", err
	}
	fmt.Printf("Enter password: ")
	pass, err := terminal.ReadPassword(0)
	if err != nil {
		log.Fatal(err)
	}
	return strings.TrimSuffix(email, "\n"), strings.TrimSuffix(string(pass), "\n"), nil
}

repository: stamblerre/baldorfood

repo_name: stamblerre/baldorfood

extension: go


text:
@incollection{aczel2002collection,
        Author = {Aczel, P. and Gambino, N.},
        Booktitle = {Types for proofs and programs},
        Pages = {1--23},
        Publisher = {Springer},
        Title = {Collection principles in dependent type theory},
        Year = {2002}}

@misc{aczel2001notes,
  title={Notes on constructive set theory},
  author={Aczel, P. and Rathjen, M.},
  year={2001},
  publisher={Report}
}

@book{adamek2010algebraic,
  title={Algebraic theories: a categorical introduction to general algebra},
  author={Ad{\'a}mek, Ji{\v{r}}{\'\i} and Rosick{\`y}, Ji{\v{r}}{\'\i} and Vitale, Enrico Maria},
  volume={184},
  year={2010},
  publisher={Cambridge University Press}
}

@book {Adams78,
    AUTHOR = {Adams, John Frank},
     TITLE = {Infinite loop spaces},
    SERIES = {Annals of Mathematics Studies},
    VOLUME = {90},
 PUBLISHER = {Princeton University Press, Princeton, N.J.; University of
              Tokyo Press, Tokyo},
      YEAR = {1978},
     PAGES = {x+214},
      ISBN = {0-691-08207-3; 0-691-08206-5},
   MRCLASS = {55-02 (55N20 55P47)},
  MRNUMBER = {505692},
MRREVIEWER = {Stewart B. Priddy},
}

@Article{         AdamsWalker1964,
  author	= {Adams, J. F. and Walker, G.},
  title		= {An example in homotopy theory},
  journal	= {Proc. Cambridge Philos. Soc.},
  volume	= {60},
  year		= {1964},
  pages		= {699--700},
  doi           = {10.1017/S0305004100077422}
}

@book{agda,
  title={Towards a practical programming language based on dependent type theory},
  author={Norell, U.},
  year={2007},
  publisher={Chalmers University of Technology}
}

@incollection {AhrensCapriottiSpadotti,
    AUTHOR = {Ahrens, Benedikt and Capriotti, Paolo and Spadotti, R{\'e}gis},
     TITLE = {Non-wellfounded trees in homotopy type theory},
 BOOKTITLE = {13th {I}nternational {C}onference on {T}yped {L}ambda
              {C}alculi and {A}pplications},
    SERIES = {LIPIcs. Leibniz Int. Proc. Inform.},
    VOLUME = {38},
     PAGES = {17--30},
 PUBLISHER = {Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern},
      YEAR = {2015},
   MRCLASS = {68N18 (03B35 55U35)},
  MRNUMBER = {3448094},
MRREVIEWER = {Anna Labella},
}

@article{DBLP:journals/corr/AhrensLV17,
  author    = {Benedikt Ahrens and
               Peter LeFanu Lumsdaine and
               Vladimir Voevodsky},
  title     = {Categorical structures for type theory in univalent foundations},
  journal   = {CoRR},
  volume    = {abs/1705.04310},
  year      = {2017},
  url       = {http://arxiv.org/abs/1705.04310},
  timestamp = {Wed, 07 Jun 2017 14:41:25 +0200},
  biburl    = {http://dblp.dagstuhl.de/rec/bib/journals/corr/AhrensLV17},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@article {AhrensKapulkinShulman,
    AUTHOR = {Ahrens, Benedikt and Kapulkin, Krzysztof and Shulman, Michael},
     TITLE = {Univalent categories and the {R}ezk completion},
   JOURNAL = {Math. Structures Comput. Sci.},
  FJOURNAL = {Mathematical Structures in Computer Science. A Journal in the
              Applications of Categorical, Algebraic and Geometric Methods
              in Computer Science},
    VOLUME = {25},
      YEAR = {2015},
    NUMBER = {5},
     PAGES = {1010--1039},
      ISSN = {0960-1295},
   MRCLASS = {18B99 (03B15)},
  MRNUMBER = {3340533},
MRREVIEWER = {Thomas Streicher},
       DOI = {10.1017/S0960129514000486},
       URL = {http://dx.doi.org/10.1017/S0960129514000486},
}

@InProceedings{Altenkirch1999,
  author = 	 {Altenkirch, T.},
  title = 	 {Extensional Equality in Intensional Type Theory},
  booktitle = 	 {14th Symposium on Logic in Computer Science},
  year =	 {1999},
  pages = { 412 -- 420 }
}

@unpublished{AltenkirchAmbrosi,
author={Thorsten Altenkirch and Ambrus Kaposi},
title={A syntax for cubical type theory},
url={http://www.cs.nott.ac.uk/~txa/publ/ctt.pdf},
year=2014
}

@InProceedings{AltenkirchEA2011,
  author = 	 {Altenkirch, T. and Forsberg, F. and Morris, P. and Setzer, A.},
  title = 	 {A categorical semantics for inductive-inductive definitions},
  booktitle =	 {CALCO 2011: Fourth International Conference on Algebra and Coalgebra in Computer Science},
  year =	 {2011},
  note =	 {to appear},
}

@article {AltenkirchGhaniHancock,
    AUTHOR = {Altenkirch, Thorsten and Ghani, Neil and Hancock, Peter and
              McBride, Conor and Morris, Peter},
     TITLE = {Indexed containers},
   JOURNAL = {J. Funct. Programming},
  FJOURNAL = {Journal of Functional Programming},
    VOLUME = {25},
      YEAR = {2015},
     PAGES = {e5, 41},
      ISSN = {0956-7968},
   MRCLASS = {68N18},
  MRNUMBER = {3376745},
       DOI = {10.1017/S095679681500009X},
       URL = {http://dx.doi.org/10.1017/S095679681500009X},
}

@ARTICLE{AnelBiedermanFinsterJoyal,
   author = {{Anel}, M. and {Biedermann}, G. and {Finster}, E. and {Joyal}, A.
	},
    title = "{A Generalized Blakers-Massey Theorem}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1703.09050},
 primaryClass = "math.AT",
 keywords = {Mathematics - Algebraic Topology, Mathematics - Category Theory, 55P99, 18F99},
     year = 2017,
    month = mar,
   adsurl = {http://adsabs.harvard.edu/abs/2017arXiv170309050A},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}

@InProceedings{	  chtt,
  author	= {Angiuli, Carlo and Harper, Robert and Wilson, Todd},
  title		= {Computational Higher-dimensional Type Theory},
  booktitle	= {Proceedings of the 44th ACM SIGPLAN Symposium on
		  Principles of Programming Languages (POPL 2017)},
  year		= {2017},
  pages		= {680--693},
  publisher	= {ACM},
  address	= {New York, NY, USA},
  doi		= {10.1145/3009837.3009861}
}

@ARTICLE{AngiuliHarperWilson,
   author = {{Angiuli}, C. and {Harper}, R. and {Wilson}, T.},
    title = "{Computational Higher Type Theory I: Abstract Cubical Realizability}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1604.08873},
 primaryClass = "cs.LO",
 keywords = {Computer Science - Logic in Computer Science},
     year = 2016,
    month = apr,
   adsurl = {http://adsabs.harvard.edu/abs/2016arXiv160408873A},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}

@InProceedings{dtt-parametricity,
  title = {A Relationally Parametric Model of Dependent Type Theory},
  author = {Robert Atkey and Neil Ghani and Patricia Johann},
  year = {2014},
  note = {To appear},
  booktitle = {POPL 2014},
}

@article{Avigad:limits,
author={Avigad, J. and Kapulkin, K. and Lumsdaine, P.},
title={Homotopy limits in {C}oq},
eprint={arXiv:1304.0680},
year=2013
}

@article{awodey2012type,
  title={Type theory and homotopy},
  author={Awodey, S.},
  journal={Epistemology versus Ontology},
  pages={183--201},
  year={2012},
  publisher={Springer}
}

@incollection {Awodey12,
    AUTHOR = {Awodey, Steve},
     TITLE = {Type theory and homotopy},
 BOOKTITLE = {Epistemology versus ontology},
    SERIES = {Log. Epistemol. Unity Sci.},
    VOLUME = {27},
     PAGES = {183--201},
 PUBLISHER = {Springer, Dordrecht},
      YEAR = {2012},
   MRCLASS = {03B15 (18B99 55P99)},
  MRNUMBER = {2962717},
MRREVIEWER = {Florian Rabe},
       DOI = {10.1007/978-94-007-4435-6_9},
       URL = {http://dx.doi.org/10.1007/978-94-007-4435-6_9},
}

@ARTICLE{Awodey14,
   author = {{Awodey}, S.},
    title = "{Natural models of homotopy type theory}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1406.3219},
 primaryClass = "math.CT",
 keywords = {Mathematics - Category Theory, Mathematics - Logic},
     year = 2014,
    month = jun,
   adsurl = {http://adsabs.harvard.edu/abs/2014arXiv1406.3219A},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}

@inproceedings{awodey2012inductive,
  title={Inductive types in homotopy type theory},
  author={Awodey, S. and Gambino, N. and Sojakova, K.},
  booktitle={Logic in Computer Science (LICS), 2012},
  pages={95--104},
  year={2012},
  organization={IEEE}
}

@article {AwodeyBauer2004,
    AUTHOR = {Awodey, S. and Bauer, A.},
     TITLE = {Propositions as [types]},
   JOURNAL = {J. Logic Comput.},
  FJOURNAL = {Journal of Logic and Computation},
    VOLUME = {14},
      YEAR = {2004},
    NUMBER = {4},
     PAGES = {447--471},
      ISSN = {0955-792X},
       DOI = {10.1093/logcom/14.4.447},
       URL = {http://dx.doi.org/10.1093/logcom/14.4.447},
}

@ARTICLE{AwodeyGambinoSojakova,
   author = {{Awodey}, S. and {Gambino}, N. and {Sojakova}, K.},
    title = "{Homotopy-initial algebras in type theory}",
  journal = {arXiv:1504.05531},
     year = 2015,
}

@article {AwodeyWarren2009,
    AUTHOR = {Awodey, S. and Warren, M.},
     TITLE = {Homotopy theoretic models of identity types},
   JOURNAL = {Math. Proc. Cambridge Philos. Soc.},
  FJOURNAL = {Mathematical Proceedings of the Cambridge Philosophical Society},
    VOLUME = {146},
      YEAR = {2009},
    NUMBER = {1},
     PAGES = {45--55},
      ISSN = {0305-0041},
       DOI = {10.1017/S0305004108001783},
       URL = {http://dx.doi.org/10.1017/S0305004108001783},
}

@article {AwodeyWarren,
    AUTHOR = {Awodey, Steve and Warren, Michael A.},
     TITLE = {Homotopy theoretic models of identity types},
   JOURNAL = {Math. Proc. Cambridge Philos. Soc.},
  FJOURNAL = {Mathematical Proceedings of the Cambridge Philosophical
              Society},
    VOLUME = {146},
      YEAR = {2009},
    NUMBER = {1},
     PAGES = {45--55},
      ISSN = {0305-0041},
     CODEN = {MPCPCO},
   MRCLASS = {03B15 (03B35 18G99 55U35)},
  MRNUMBER = {2461866},
MRREVIEWER = {Richard F. Blute},
       DOI = {10.1017/S0305004108001783},
       URL = {http://dx.doi.org/10.1017/S0305004108001783},
}

@InCollection{ 	  BaezDolan1998,
  author       	= {Baez, John C. and Dolan, James},
  title		= {Categorification},
  booktitle    	= {Higher category theory ({E}vanston, {IL}, 1997)},
  series       	= {Contemp. Math.},
  volume       	= {230},
  pages		= {1--36},
  publisher    	= {Amer. Math. Soc.},
  address       = {Providence, RI},
  year 		= {1998},
  doi  		= {10.1090/conm/230/03336},
}

@Article{         Baez2002,
  author	= {Baez, John C.},
  title		= {The octonions},
  journal	= {Bull. Amer. Math. Soc. (N.S.)},
  fjournal	= {American Mathematical Society. Bulletin. New Series},
  volume	= {39},
  year		= {2002},
  number	= {2},
  pages		= {145--205},
  doi		= {10.1090/S0273-0979-01-00934-X},
  eprinttype    = {arxiv},
  eprint        = {math/0105155}
}

@Article{	  BaezLauda2004,
  author	= {John C. Baez and Aaron D. Lauda},
  title		= {Higher-dimensional algebra. {V}: 2-Groups},
  fjournal	= {Theory and Applications of Categories},
  journal	= {Theory Appl. Categ.},
  volume	= {12},
  pages		= {423--491},
  year		= {2004},
  publisher	= {Mount Allison University, Department of Mathematics and
		  Computer Science, Sackville, NB},
  eprinttype    = {arxiv},
  eprint        = {math/0307200}
}

@Unpublished{bauer:loc-hasse,
  author = 	 {Tilman Bauer},
  title = 	 {Bousfield localization and the Hasse square},
  note = 	 {\url{http://math.mit.edu/conferences/talbot/2007/tmfproc/Chapter09/bauer.pdf}},
  year = 	 2011}

@Article{         Behrens2002,
  author	= {Behrens, Mark J.},
  title		= {A new proof of the {B}ott periodicity theorem},
  journal	= {Topology Appl.},
  fjournal	= {Topology and its Applications},
  volume	= {119},
  year		= {2002},
  number	= {2},
  pages		= {167--183},
  doi		= {10.1016/S0166-8641(01)00060-8},
  url		= {http://www3.nd.edu/~mbehren1/papers/bott.pdf}
}

@article{berg2016exact,
  title={Exact completion of path categories and algebraic set theory--{Part I}: Exact completion of path categories},
  author={Berg, Benno van den and Moerdijk, Ieke},
  journal={arXiv:1603.02456},
  year={2016}
}

@article {vandenBerg2012,
    AUTHOR = {Berg, B. van den},
     TITLE = {Predicative toposes},
   JOURNAL = {To appear},
eprint={arXiv:1207.0959},
      YEAR = {2012},
}

@article {VanDenBergGarner,
    AUTHOR = {van den Berg, Benno and Garner, Richard},
     TITLE = {Types are weak {$\omega$}-groupoids},
   JOURNAL = {Proc. Lond. Math. Soc. (3)},
  FJOURNAL = {Proceedings of the London Mathematical Society. Third Series},
    VOLUME = {102},
      YEAR = {2011},
    NUMBER = {2},
     PAGES = {370--394},
      ISSN = {0024-6115},
   MRCLASS = {18D05 (03B15 18D50)},
  MRNUMBER = {2769118},
MRREVIEWER = {Philippe Gaucher},
       DOI = {10.1112/plms/pdq026},
       URL = {http://dx.doi.org/10.1112/plms/pdq026},
}

@Article{      	  vdBergGarner2012,
  author       	= {van den Berg, Benno and Garner, Richard},
  title		= {Topological and simplicial models of identity types},
  journal      	= {ACM Trans. Comput. Log.},
  fjournal     	= {ACM Transactions on Computational Logic},
  volume       	= {13},
  year 		= {2012},
  number       	= {1},
  pages		= {Art. 3, 44},
  issn 		= {1529-3785},
  doi  		= {10.1145/2071368.2071371},
  eprinttype    = {arxiv},
  eprint        = {1007.4638}
}

@article{WinHoTT,
authors={Benno van den Berg and Ieke Moerdijk},
title={W-types in homotopy type theory},
year=2013}

@article{bergner2011reedy,
  title={Reedy categories and the $\Theta$-construction},
  author={Bergner, Julia E and Rezk, Charles},
  eprint={1110.1066},
  year={2011}
}

@article{bernardy2015presheaf,
  title={A presheaf model of parametric type theory},
  author={Bernardy, Jean-Philippe and Coquand, Thierry and Moulin, Guilhem},
  journal={Electronic Notes in Theoretical Computer Science},
  volume={319},
  pages={67--82},
  year={2015},
}

@incollection {BezemCoquandHuber,
    AUTHOR = {Bezem, Marc and Coquand, Thierry and Huber, Simon},
     TITLE = {A model of type theory in cubical sets},
 BOOKTITLE = {19th {I}nternational {C}onference on {T}ypes for {P}roofs and
              {P}rograms},
    SERIES = {LIPIcs. Leibniz Int. Proc. Inform.},
    VOLUME = {26},
     PAGES = {107--128},
 PUBLISHER = {Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern},
      YEAR = {2014},
   MRCLASS = {03B15},
  MRNUMBER = {3281415},
}

@book{Bishop1967,
    AUTHOR = {Bishop, E.},
     TITLE = {Foundations of constructive analysis},
 PUBLISHER = {McGraw-Hill Book Co.},
      YEAR = {1967},
     PAGES = {xiii+370},
}

@article {BoardmanVogt,
    AUTHOR = {Boardman, J. M. and Vogt, R. M.},
     TITLE = {Homotopy-everything {$H$}-spaces},
   JOURNAL = {Bull. Amer. Math. Soc.},
  FJOURNAL = {Bulletin of the American Mathematical Society},
    VOLUME = {74},
      YEAR = {1968},
     PAGES = {1117--1122},
      ISSN = {0002-9904},
   MRCLASS = {55.42},
  MRNUMBER = {0236922},
MRREVIEWER = {R. J. Milgram},
}

@Book{		  BoardmanVogt1973,
  author	= {Boardman, J. M. and Vogt, R. M.},
  title		= {Homotopy invariant algebraic structures on topological
		  spaces},
  series	= {Lecture Notes in Mathematics, Vol. 347},
  publisher	= {Springer-Verlag, Berlin-New York},
  year		= {1973},
  pages		= {x+257},
  doi           = {10.1007/BFb0068547}
}

@book {Borceux1994-2,
    AUTHOR = {Borceux, F.},
     TITLE = {Handbook of categorical algebra. 2},
    SERIES = {Encyclopedia of Mathematics and its Applications},
    VOLUME = {51},
      NOTE = {Categories and structures},
 PUBLISHER = {Cambridge University Press},
   ADDRESS = {Cambridge},
      YEAR = {1994},
     PAGES = {xviii+443},
      ISBN = {0-521-44179-X},
}

@book {BottTu,
    AUTHOR = {Bott, Raoul and Tu, Loring W.},
     TITLE = {Differential forms in algebraic topology},
    SERIES = {Graduate Texts in Mathematics},
    VOLUME = {82},
 PUBLISHER = {Springer-Verlag, New York-Berlin},
      YEAR = {1982},
     PAGES = {xiv+331},
      ISBN = {0-387-90613-4},
   MRCLASS = {57R19 (55-02 58-01 58A12)},
  MRNUMBER = {658304},
MRREVIEWER = {Hansklaus Rummler},
}

@article {Bousfield,
AUTHOR = {{Bousfield}, A.K.},
TITLE = {Localization and periodicity in unstable homotopy theory},
JOURNAL = {J. Amer. Math. Soc.},
FJOURNAL = {Journal of the American Mathematical Society},
VOLUME = 7,
YEAR = 1994,
NUMBER = 4,
PAGES = {831--873},
ISSN = {0894-0347},
MRCLASS = {55P60 (55N15 55N20 55Q05 55U10)},
MRNUMBER = 1257059,
MRREVIEWER = {N.J. Kuhn},
DOI = {10.2307/2152734},
}

@article {Brown62,
    AUTHOR = {Brown, Jr., Edgar H.},
     TITLE = {Cohomology theories},
   JOURNAL = {Ann. of Math. (2)},
  FJOURNAL = {Annals of Mathematics. Second Series},
    VOLUME = {75},
      YEAR = {1962},
     PAGES = {467--484},
      ISSN = {0003-486X},
   MRCLASS = {55.30},
  MRNUMBER = {0138104},
MRREVIEWER = {S.-T. Hu},
}

@ARTICLE{BruneriePhD,
   author = {Brunerie, Guillaume},
    title = "{On the homotopy groups of spheres in homotopy type theory}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1606.05916},
 primaryClass = "math.AT",
 keywords = {Mathematics - Algebraic Topology, Computer Science - Logic in Computer Science, Mathematics - Logic},
     year = 2016,
    month = jun,
}

@ARTICLE{Brunerie16,
   author = {{Brunerie}, G.},
    title = "{On the homotopy groups of spheres in homotopy type theory}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1606.05916},
 primaryClass = "math.AT",
 keywords = {Mathematics - Algebraic Topology, Computer Science - Logic in Computer Science, Mathematics - Logic},
     year = 2016,
    month = jun,
   adsurl = {http://adsabs.harvard.edu/abs/2016arXiv160605916B},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}

@InProceedings{	  LicataBrunerie2015,
  author	= {Licata, Daniel R. and Brunerie, Guillaume},
  title		= {A Cubical Approach to Synthetic Homotopy Theory},
  booktitle	= {Proceedings of the 2015 30th Annual ACM/IEEE Symposium on
		  Logic in Computer Science (LICS)},
  series	= {LICS '15},
  year		= {2015},
  isbn		= {978-1-4799-8875-4},
  pages		= {92--103},
  numpages	= {12},
  doi		= {10.1109/LICS.2015.19},
  acmid		= {2876525},
  publisher	= {IEEE Computer Society},
  address	= {Washington, DC, USA}
}

@Misc{ 		  MOHspaces,
  title		= {H-space structures on non-sphere suspensions?},
  author       	= {Buchholtz, Ulrik},
  howpublished 	= {MathOverflow Question},
  year          = {2016},
  url  		= {http://mathoverflow.net/q/235840}
}

@misc{BuchholtzDoornRijke,
   author = {{Buchholtz}, U. and {van Doorn}, F. and {Rijke}, E.},
    title = "{Higher Groups in Homotopy Type Theory}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1802.04315},
% primaryClass = "cs.LO",
 keywords = {Computer Science - Logic in Computer Science, Mathematics - Algebraic Topology, Mathematics - Logic, 03B15, F.4.1},
     year = 2018,
%    month = feb,
   adsurl = {http://adsabs.harvard.edu/abs/2018arXiv180204315B},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}

@InCollection{    realprojective,
  author        = {Buchholtz, Ulrik and Rijke, Egbert},
  title         = {The real projective spaces in homotopy type theory},
  booktitle	= {32nd Annual ACM/IEEE Symposium on Logic in Computer
		  Science (LICS 2017)},
  year          = {2017},
  pages         = {1--8},
  publisher     = {IEEE},
  address	= {New York, NY, USA},
  doi		= {10.1109/LICS.2017.8005146}
}

@article{DBLP:journals/entcs/BuisseD08,
  author    = {Alexandre Buisse and
               Peter Dybjer},
  title     = {Towards Formalizing Categorical Models of Type Theory in Type Theory},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {196},
  pages     = {137--151},
  year      = {2008},
  url       = {https://doi.org/10.1016/j.entcs.2007.09.023},
  doi       = {10.1016/j.entcs.2007.09.023},
  timestamp = {Sun, 28 May 2017 13:22:54 +0200},
  biburl    = {http://dblp.dagstuhl.de/rec/bib/journals/entcs/BuisseD08},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@Online{          Camarena,
  author        = {Camarena, Omar Antolín},
  title         = {The homotopy fiber of the map on classifying spaces},
  year          = {2017},
  url           = {http://www.matem.unam.mx/omar/notes/hofib-grphom.html},
  lastaccessed  = {Jan.~28, 2018}
}

@article{carboniJohnstone,
  title={Connected limits, familial representability and Artin glueing},
  author={Carboni, Aurelio and Johnstone, Peter},
  journal={Mathematical Structures in Computer Science},
  volume={5},
  number={04},
  pages={441--459},
  year={1995},
  publisher={Cambridge}
}

@ARTICLE{css:large-cardinal,
  author = {Casacuberta, Carles and Scevenels, Dirk and Smith, Jeffrey H.},
  title = {Implications of large-cardinal principles in homotopical localization},
  journal = {Adv. Math.},
  year = {2005},
  volume = {197},
  pages = {120--139},
  number = {1},
  coden = {ADMTA4},
  fjournal = {Advances in Mathematics},
  issn = {0001-8708},
  mrclass = {55P60 (03E55 18A40)},
  mrnumber = {MR2166179 (2006i:55013)},
  mrreviewer = {George Peschke}
}

@ARTICLE{chk:reflocfact,
  author = {Cassidy, C. and H{\'e}bert, M. and Kelly, G. M.},
  title = {Reflective subcategories, localizations and factorization systems},
  journal = {J. Austral. Math. Soc. Ser. A},
  year = {1985},
  volume = {38},
  pages = {287--329},
  number = {3},
  annote = {Lex-reflective subcategories = local factorization systems. See also
	Kelly, clubs and data-type constructors.},
  coden = {JAMADS},
  fjournal = {Australian Mathematical Society. Journal. Series A. Pure Mathematics
	and Statistics},
  issn = {0263-6115},
  mrclass = {18A20 (18E35)},
  mrnumber = {MR779198 (86j:18001)},
  mrreviewer = {Ji{\v{r}}{\'{\i}} Ad{\'a}mek}
}

@article{Chacholski1997,
    AUTHOR = {Chach{\'o}lski, W.},
     TITLE = {A generalization of the triad theorem of {B}lakers-{M}assey},
   JOURNAL = {Topology},
  FJOURNAL = {Topology. An International Journal of Mathematics},
    VOLUME = {36},
      YEAR = {1997},
    NUMBER = {6},
     PAGES = {1381--1400},
      ISSN = {0040-9383},
       DOI = {10.1016/S0040-9383(96)00045-6},
       URL = {http://dx.doi.org/10.1016/S0040-9383(96)00045-6},
}

@article{Chapman09,
  author    = {James Chapman},
  title     = {Type Theory Should Eat Itself},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {228},
  pages     = {21--36},
  year      = {2009},
  url       = {https://doi.org/10.1016/j.entcs.2008.12.114},
  doi       = {10.1016/j.entcs.2008.12.114},
  timestamp = {Mon, 05 Jun 2017 20:49:18 +0200},
  biburl    = {http://dblp.dagstuhl.de/rec/bib/journals/entcs/Chapman09},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@ARTICLE{ChristensenOpieRijkeScoccola,
   author = {{Christensen}, J.~D. and {Opie}, M. and {Rijke}, E. and {Scoccola}, L.
	},
    title = "{Localization in Homotopy Type Theory}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1807.04155},
 primaryClass = "math.AT",
 keywords = {Mathematics - Algebraic Topology, Mathematics - Category Theory, 55P60 (Primary), 18E35, 03B15 (Secondary)},
     year = 2018,
    month = jul,
   adsurl = {http://adsabs.harvard.edu/abs/2018arXiv180704155C},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}

@inproceedings{hcoq,
 author = {Bauer, Andrej and Gross, Jason and Lumsdaine, Peter LeFanu and Shulman, Michael and Sozeau, Matthieu and Spitters, Bas},
 title = {The HoTT Library: A Formalization of Homotopy Type Theory in Coq},
 booktitle = {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs},
 series = {CPP 2017},
 year = {2017},
 isbn = {978-1-4503-4705-1},
 location = {Paris, France},
 pages = {164--172},
 numpages = {9},
 url = {http://doi.acm.org/10.1145/3018610.3018615},
 doi = {10.1145/3018610.3018615},
 acmid = {3018615},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Coq, Higher inductive types, Homotopy type theory, Univalent foundations, Universe polymorphism},
}

@InCollection{    CCHM2016,
  author	= {Cohen, Cyril and Coquand, Thierry and
                  Huber, Simon and M{\"o}rtberg, Anders},
  title		= {Cubical Type Theory: a constructive interpretation of the univalence axiom},
  booktitle	= {21st {I}nternational {C}onference on {T}ypes for {P}roofs
		  and {P}rograms (TYPES 2015)},
  series	= {LIPIcs. Leibniz Int. Proc. Inform.},
  publisher	= {Schloss Dagstuhl. Leibniz-Zent. Inform.},
  address       = {Wadern},
  note          = {To appear},
  year		= {2016},
  eprinttype    = {arxiv},
  eprint        = {1611.02108}
}

@book{Coq,
        author = {{Coq Development Team}},
        title = {The {C}oq Proof Assistant Reference Manual},
        publisher = {INRIA-Rocquencourt},
        year = {2012}
}

@article{Stacks,
  author    = {Thierry Coquand and
               Bassel Mannaa and
               Fabian Ruch},
  title     = {Stack Semantics of Type Theory},
  journal   = {CoRR},
  volume    = {abs/1701.02571},
  year      = 2017,
  url       = {http://arxiv.org/abs/1701.02571}
}

@misc{Coquand:stack,
title={Cubical stacks},
author={Thierry Coquand},
note={\url{http://www.cse.chalmers.se/~coquand/stack.pdf}},
url={http://www.cse.chalmers.se/~coquand/stack.pdf},
year=2017
}

@techreport{Coquand:simplicial,
       author={Thierry Coquand and Simon Huber},
       title={Simplicial sets model of type theory},
       url={http://www.cse.chalmers.se/~coquand/decuniv.pdf},
       year=2013}

@Unpublished{coquand2012constructive,
  author =       {Barras, B. and Coquand, T. and Huber, S.},
  title =        {A Generalization of {T}akeuti-{G}andy Interpretation},
  note =         {\url{http://uf-ias-2012.wikispaces.com/file/view/semi.pdf}},
  year =      2013}

@misc{Danielson12Blog,
  author = {Danielson, N.},
   title = {Positive h-levels are closed under W},
     url = {https://homotopytypetheory.org/2012/09/21/positive-h-levels-are-closed-under-w/},
    year = {2012},
}

@article {Diaconescu1975,
    AUTHOR = {Diaconescu, R.},
     TITLE = {Axiom of choice and complementation},
   JOURNAL = {Proc. Amer. Math. Soc.},
  FJOURNAL = {Proceedings of the American Mathematical Society},
    VOLUME = {51},
      YEAR = {1975},
     PAGES = {176--178},
      ISSN = {0002-9939},
}

@Article{	  Dickson1919,
  author	= {Dickson, Leonard E.},
  title		= {On quaternions and their generalization and the history of
		  the eight square theorem},
  journal	= {Ann. of Math. (2)},
  fjournal	= {Annals of Mathematics. Second Series},
  volume	= {20},
  year		= {1919},
  number	= {3},
  pages		= {155--171},
  issn		= {0003-486X},
  coden		= {ANMAAH},
  doi		= {10.2307/1967865},
}

@Article{	  DoldLashof1959,
  author	= {Dold, Albrecht and Lashof, Richard},
  title		= {Principal quasi-fibrations and fibre homotopy equivalence
		  of bundles},
  journal	= {Illinois J. Math.},
  fjournal	= {Illinois Journal of Mathematics},
  volume	= {3},
  year		= {1959},
  pages		= {285--305},
  issn		= {0019-2082}
}

@InProceedings{	  vanDoorn2016,
  title		= {Constructing the propositional truncation using
		  non-recursive HITs},
  author	= {Doorn, Floris van},
  booktitle	= {Proceedings of the 5th ACM SIGPLAN Conference on Certified
		  Programs and Proofs},
  pages		= {122--129},
  year		= 2016,
  organization	= {ACM},
  eprinttype    = {arxiv},
  eprint        = {1512.02274}
}

@unpublished {DoornRijkeSojakova,
  AUTHOR = {Doorn, {F. van} and Rijke, {E.} and Sojakova, {K.}},
  TITLE  = {Identity types of sequential colimits},
  YEAR   = {2018},
  NOTE   = {In preparation},
  URL    = {https://github.com/cmu-phil/Spectral/blob/master/colimit/seq_colim.hlean}
}

@inproceedings{vDvRB2017HoTTLean,
  title={Homotopy Type Theory in {Lean}},
  author={Doorn, Floris van and von Raumer, Jakob and Buchholtz, Ulrik},
  booktitle={Interactive Theorem Proving (ITP 2017)},
  pages={479--495},
  year={2017},
  publisher={Springer},
  address={Cham},
  isbn={978-3-319-66107-0},
  doi={10.1007/978-3-319-66107-0_30}
}

@Article{	  DwyerWilkerson1994,
  author	= {William G. Dwyer and Clarence W. Wilkerson},
  title		= {Homotopy fixed-point methods for Lie groups and finite
		  loop spaces},
  fjournal	= {Annals of Mathematics. Second Series},
  journal	= {Ann. Math. (2)},
  volume	= {139},
  number	= {2},
  pages		= {395--442},
  year		= {1994},
  publisher	= {Princeton University, Mathematics Department, Princeton,
		  NJ; Mathematical Sciences Publishers (MSP), Berkeley, CA},
  doi		= {10.2307/2946585}
}

@InCollection{	  DwyerZabrodsky1987,
  author	= {Dwyer, William G. and Zabrodsky, Alexander},
  title		= {Maps between classifying spaces},
  booktitle	= {Algebraic topology, {B}arcelona, 1986},
  series	= {Lecture Notes in Math.},
  volume	= {1298},
  pages		= {106--119},
  publisher	= {Springer},
  address       = {Berlin},
  year		= {1987},
  doi		= {10.1007/BFb0083003}
}

@unpublished {Escardo2016,
  AUTHOR = {Escard\'o, Mart\'in},
   TITLE = {N/A},
   URL   = {https://www.cs.bham.ac.uk/~mhe/agda-new/UF-IdEmbedding.html},
  YEAR   = {2017},
}

@book {Farjoun,
    AUTHOR = {Farjoun, Emmanuel Dror},
     TITLE = {Cellular spaces, null spaces and homotopy localization},
    SERIES = {Lecture Notes in Mathematics},
    VOLUME = {1622},
 PUBLISHER = {Springer-Verlag, Berlin},
      YEAR = {1996},
     PAGES = {xiv+199},
      ISBN = {3-540-60604-1},
   MRCLASS = {55P60 (55-02 55P65)},
  MRNUMBER = {1392221},
MRREVIEWER = {Carles Casacuberta},
       DOI = {10.1007/BFb0094429},
       URL = {https://doi.org/10.1007/BFb0094429},
}

@InProceedings{Dybjer1996,
  AUTHOR = {Dybjer, P.},
  TITLE = {Internal type theory},
  booktitle = {Types for proofs and programs},
  YEAR = {1996},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {1158},
  PAGES = {120-134},
}

@article {DybjerSetzer2003,
    AUTHOR = {Dybjer, P. and Setzer, A.},
     TITLE = {Induction-recursion and initial algebras},
   JOURNAL = {Ann. Pure Appl. Logic},
  FJOURNAL = {Annals of Pure and Applied Logic},
    VOLUME = {124},
      YEAR = {2003},
    NUMBER = {1-3},
     PAGES = {1--47},
      ISSN = {0168-0072},
       DOI = {10.1016/S0168-0072(02)00096-9},
       URL = {http://dx.doi.org/10.1016/S0168-0072(02)00096-9},
}

@article{DybjerSetzer2006,
    AUTHOR = {Dybjer, P. and Setzer, A.},
     TITLE = {Indexed induction-recursion},
   JOURNAL = {J. Log. Algebr. Program.},
  FJOURNAL = {The Journal of Logic and Algebraic Programming},
    VOLUME = {66},
      YEAR = {2006},
    NUMBER = {1},
     PAGES = {1--49},
      ISSN = {1567-8326},
       DOI = {10.1016/j.jlap.2005.07.001},
       URL = {http://dx.doi.org/10.1016/j.jlap.2005.07.001},
}

@Article{	  Elmendorf1983,
  author	= {Anthony D. Elmendorf},
  title		= {Systems of fixed point sets.},
  fjournal	= {Transactions of the American Mathematical Society},
  journal	= {Trans. Am. Math. Soc.},
  issn		= {0002-9947; 1088-6850/e},
  volume	= {277},
  pages		= {275--284},
  year		= {1983},
  publisher	= {American Mathematical Society (AMS), Providence, RI},
  doi		= {10.2307/1999356},
}

@incollection {ElmendorfMandellMay,
    AUTHOR = {Elmendorf, A. D. and K{\v{r}}{\'{\i}}{\v{z}}, I. and Mandell,
              M. A. and May, J. P.},
     TITLE = {Modern foundations for stable homotopy theory},
 BOOKTITLE = {Handbook of algebraic topology},
     PAGES = {213--253},
 PUBLISHER = {North-Holland, Amsterdam},
      YEAR = {1995},
   MRCLASS = {55P42},
  MRNUMBER = {1361891},
MRREVIEWER = {J. M. Boardman},
       DOI = {10.1016/B978-044481779-2/50007-9},
       URL = {http://dx.doi.org/10.1016/B978-044481779-2/50007-9},
}

@InProceedings{   FavoniaHarper2016,
  author        = {Hou (Favonia), Kuen-Bang and Harper, Robert},
  title         = {Covering Spaces in Homotopy Type Theory},
  booktitle     = {22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  editor        = {Herman Geuvers and Silvia Ghilezan and Jelena Ivetic},
  series        = {Leibniz International Proceedings in Informatics (LIPIcs)},
  publisher     = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address       = {Dagstuhl, Germany}
}

@inproceedings {FinsterLicata,
    AUTHOR = {Licata, Daniel R. and Finster, Eric},
     TITLE = {Eilenberg-{M}ac{L}ane spaces in homotopy type theory},
 BOOKTITLE = {Proceedings of the {J}oint {M}eeting of the {T}wenty-{T}hird
              {EACSL} {A}nnual {C}onference on {C}omputer {S}cience {L}ogic
              ({CSL}) and the {T}wenty-{N}inth {A}nnual {ACM}/{IEEE}
              {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS})},
     PAGES = {Article No. 66, 10},
 PUBLISHER = {ACM, New York},
      YEAR = {2014},
   MRCLASS = {68N18 (03B15 03B70 55U35)},
  MRNUMBER = {3397687},
MRREVIEWER = {Dae-Woong Lee},
}

@article{fourman1979sheaf,
  title={Sheaf models for analysis},
  author={Fourman, M. and Hyland, J.},
  journal={Applications of sheaves},
  pages={280--301},
  year={1979},
  publisher={Springer}
}

@inproceedings{gambino2013polynomial,
  title={Polynomial functors and polynomial monads},
  author={Gambino, Nicola and Kock, Joachim},
  booktitle={Mathematical Proceedings of the Cambridge Philosophical Society},
  volume={154},
  number={01},
  pages={153--192},
  year={2013},
  organization={Cambridge}
}

@article{GhaniHancock2011,
  AUTHOR =       {Ghani, N. and Hancock, P.},
  TITLE =        {An Algebraic Implementation of Induction Recursion and Indexed Induction Recursion},
  NOTE =         {To appear, submitted to \emph{Mathematical Structures in Computer Science}},
  URL =          {\url{https://personal.cis.strath.ac.uk/neil.ghani/pub.html}},
  YEAR =         {2011}
}

@Misc{            Grothendieck1983,
  author        = {Grothendieck, Alexander},
  title         = {Pursuing Stacks},
  year          = {1983},
  address       = {Les Aumettes, Mormoiron},
  note          = {Manuscript},
  url           = {http://thescrivener.github.io/PursuingStacks/}
}

@Misc{		  Gurski-stable-homotopy-hypothesis,
  author	= {Gurski, Nick},
  title		= {The Stable Homotopy Hypothesis and Categorified Abelian Groups},
  year		= {2018},
  note		= {Blog post. The {$n$}-Category Caf{\'e}},
  url		= {https://golem.ph.utexas.edu/category/2018/01/the_stable_homotopy_hypothesis.html},
  lastaccessed	= {Jan.~30, 2018}
}

@Article{	  Harris1980,
  author	= {Harris, Bruno},
  title		= {Bott periodicity via simplicial spaces},
  journal	= {J. Algebra},
  fjournal	= {Journal of Algebra},
  volume	= {62},
  year		= {1980},
  number	= {2},
  pages		= {450--454},
  doi		= {10.1016/0021-8693(80)90194-5},
}

@book {HatcherAT,
    AUTHOR = {Hatcher, Allen},
     TITLE = {Algebraic topology},
 PUBLISHER = {Cambridge University Press, Cambridge},
      YEAR = {2002},
     PAGES = {xii+544},
      ISBN = {0-521-79160-X; 0-521-79540-0},
   MRCLASS = {55-01 (55-00)},
  MRNUMBER = {1867354},
MRREVIEWER = {Donald W. Kahn},
}

@unpublished{HatcherSSAT,
  AUTHOR = {Hatcher, Allen},
  TITLE = {Spectral sequences in algebraic topology},
  YEAR = {2004},
  URL = {https://www.math.cornell.edu/~hatcher/SSAT/SSATpage.html},
}

@Misc{            JakeTikZ,
  author        = {Jake},
  title         = {Moebius Strip using {TikZ}},
  howpublished  = {TeX StackExchange answer},
  year          = {2013},
  url           = {https://tex.stackexchange.com/a/118573/}
}

@incollection{hofmann:syntax-and-semantics,
        Address = {Cambridge},
        Author = {Hofmann, Martin},
        Booktitle = {Semantics and logics of computation ({C}ambridge, 1995)},
        Doi = {10.1017/CBO9780511526619.004},
        Mrclass = {03B70 (68N15 68Q55)},
        Mrnumber = {1629519},
        Pages = {79--130},
        Publisher = {Cambridge Univ. Press},
        Series = {Publ. Newton Inst.},
        Title = {Syntax and semantics of dependent types},
        Url = {http://dx.doi.org/10.1017/CBO9780511526619.004},
        Volume = {14},
        Year = {1997},
        Bdsk-Url-1 = {http://dx.doi.org/10.1017/CBO9780511526619.004}}

@article{hofmann1998groupoid,
  title={The groupoid interpretation of type theory},
  author={Hofmann, M. and Streicher, T.},
  journal={Twenty-five years of constructive type theory (Venice, 1995)},
  volume={36},
  pages={83--111},
  year={1998}
}

@phdthesis{hofmann1995extensional,
  title={Extensional concepts in intensional type theory},
  author={Hofmann, M.},
  School = {University of Edinburgh},
  year={1995},
  publisher={University of Edinburgh. College of Science and Engineering. School of Informatics.}
}

@inproceedings {Hopkins02,
    AUTHOR = {Hopkins, M. J.},
     TITLE = {Algebraic topology and modular forms},
 BOOKTITLE = {Proceedings of the {I}nternational {C}ongress of
              {M}athematicians, {V}ol. {I} ({B}eijing, 2002)},
     PAGES = {291--317},
 PUBLISHER = {Higher Ed. Press, Beijing},
      YEAR = {2002},
   MRCLASS = {11F23 (14H52 55N34 55Q45)},
  MRNUMBER = {1989190},
MRREVIEWER = {Matthew Ando},
}

@book{jacobs1999categorical,
  title={Categorical logic and type theory},
  author={Jacobs, B.},
  volume={141},
  year={1999},
  publisher={Elsevier}
}

@inproceedings{jaber2012extending,
  title={Extending type theory with forcing},
  author={Jaber, G. and Tabareau, N. and Sozeau, M.},
  booktitle={Logic in Computer Science (LICS), 2012 27th Annual IEEE Symposium on},
  pages={395--404},
  year={2012},
  organization={IEEE}
}

@Article{Janelidze1994,
author="Janelidze, George and Tholen, Walter",
title="Facets of descent, I",
journal="Applied Categorical Structures",
year="1994",
volume="2",
number="3",
pages="245--281",
doi="10.1007/BF00878100",
url="http://dx.doi.org/10.1007/BF00878100"
}

@article{JohannSojakova,
  author    = {Patricia Johann and Kristina Sojakova},
  title     = {Cubical Categories for Higher-Dimensional Parametricity},
  journal   = {CoRR},
  volume    = {abs/1701.06244},
  year      = {2017},
  url       = {http://arxiv.org/abs/1701.06244},
}

@Article{	  JohnsonOsorno,
  author	= {Niles Johnson and Ang{\'e}lica M. Osorno},
  title		= {Modeling stable one-types},
  journal	= {Theory and Applications of Categories},
  volume	= {26},
  year		= {2012},
  number	= {20},
  pages		= {520--537},
  url		= {http://www.tac.mta.ca/tac/volumes/26/20/26-20abs.html}
}

@Book{johnstone:elephant,
  author =       {Johnstone, P.},
  title =        {Sketches of an elephant: A topos theory compendium},
  publisher =    {Oxford},
  year =         2002
}

@ARTICLE{joinconstruction,
   author = {{Rijke}, E.},
    title = "{The join construction}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1701.07538},
 primaryClass = "math.CT",
 keywords = {Mathematics - Category Theory, Mathematics - Logic},
     year = 2017,
    month = jan,
   adsurl = {http://adsabs.harvard.edu/abs/2017arXiv170107538R},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}

@article{JoyalMoerdijk,
title = "A completeness theorem for open maps ",
journal = "Annals of Pure and Applied Logic ",
volume = "70",
number = "1",
pages = "51 - 86",
year = "1994",
issn = "0168-0072",
doi = "http://dx.doi.org/10.1016/0168-0072(94)90069-8",
url = "http://www.sciencedirect.com/science/article/pii/0168007294900698",
author = "A. Joyal and I. Moerdijk"
}

@book{JoyalMoerdijk1995,
    AUTHOR = {Joyal, A. and Moerdijk, I.},
     TITLE = {Algebraic set theory},
    SERIES = {London Mathematical Society Lecture Note Series},
    VOLUME = {220},
 PUBLISHER = {Cambridge University Press},
      YEAR = {1995},
     PAGES = {viii+123},
       DOI = {10.1017/CBO9780511752483},
       URL = {http://dx.doi.org/10.1017/CBO9780511752483},
}

@ARTICLE{KapulkinLeFanuLumsdaine,
   author = {{Kapulkin}, C. and {LeFanu Lumsdaine}, P.},
    title = "{The Simplicial Model of Univalent Foundations (after Voevodsky)}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1211.2851},
 primaryClass = "math.LO",
 keywords = {Mathematics - Logic, Mathematics - Algebraic Topology, Mathematics - Category Theory, 03B15, 55U10 (Primary), 18C50, 55U35 (Secondary)},
     year = 2012,
    month = nov,
   adsurl = {http://adsabs.harvard.edu/abs/2012arXiv1211.2851K},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}

@article {Kelly80,
    AUTHOR = {Kelly, G. M.},
     TITLE = {A unified treatment of transfinite constructions for free
              algebras, free monoids, colimits, associated sheaves, and so
              on},
   JOURNAL = {Bull. Austral. Math. Soc.},
  FJOURNAL = {Bulletin of the Australian Mathematical Society},
    VOLUME = {22},
      YEAR = {1980},
    NUMBER = {1},
     PAGES = {1--83},
      ISSN = {0004-9727},
     CODEN = {ALNBAB},
   MRCLASS = {18C15 (18A40)},
  MRNUMBER = {589937},
MRREVIEWER = {V{\'a}clav Koubek},
       DOI = {10.1017/S0004972700006353},
       URL = {http://dx.doi.org/10.1017/S0004972700006353},
}

@book {Kochman96,
    AUTHOR = {Kochman, S. O.},
     TITLE = {Bordism, stable homotopy and {A}dams spectral sequences},
    SERIES = {Fields Institute Monographs},
    VOLUME = {7},
 PUBLISHER = {American Mathematical Society, Providence, RI},
      YEAR = {1996},
     PAGES = {xiv+272},
      ISBN = {0-8218-0600-9},
   MRCLASS = {55P42 (55N20 55N22 55Q45 55R40 55T15)},
  MRNUMBER = {1407034},
MRREVIEWER = {J. P. C. Greenlees},
       DOI = {10.1090/fim/007},
       URL = {http://dx.doi.org/10.1090/fim/007},
}

@article{kock2012data,
  title={Data types with symmetries and polynomial functors over groupoids},
  author={Kock, Joachim},
  journal={Electronic Notes in Theoretical Computer Science},
  volume={286},
  pages={351--365},
  year={2012}
}

@InProceedings{	  Kraus2016,
  author	= {Kraus, Nicolai},
  title		= {Constructions with Non-Recursive Higher Inductive Types},
  booktitle	= {Proceedings of the 31st Annual ACM/IEEE Symposium on Logic
		  in Computer Science},
  series	= {LICS '16},
  year		= {2016},
  pages		= {595--604},
  doi		= {10.1145/2933575.2933586},
  publisher	= {ACM},
  address	= {New York, NY, USA},
}

@article{ks:u-not-ntype,
 author = {Kraus, Nicolai and Sattler, Christian},
 title = {Higher Homotopies in a Hierarchy of Univalent Universes},
 journal = {ACM Trans. Comput. Logic},
 issue_date = {March 2015},
 volume = {16},
 number = {2},
 month = apr,
 year = {2015},
 issn = {1529-3785},
 pages = {18:1--18:12},
 articleno = {18},
 numpages = {12},
 acmid = {2729979},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Homotopy type theory, loop spaces, truncation levels, univalent universes},
}

@book{lambek1988introduction,
  title={Introduction to higher-order categorical logic},
  author={Lambek, J. and Scott, P.},
  volume={7},
  year={1988},
  publisher={Cambridge University Press}
}

@book{lawvere2003sets,
  title={Sets for mathematics},
  author={Lawvere, F. and Rosebrugh, R.},
  year={2003},
  publisher={Cambridge}
}

@book{leinster2004higher,
  title={Higher operads, higher categories},
  author={Leinster, Tom},
  volume={298},
  year={2004},
  publisher={Cambridge}
}

@book {LewisMay,
    AUTHOR = {Lewis, Jr., L. G. and May, J. P. and Steinberger, M. and
              McClure, J. E.},
     TITLE = {Equivariant stable homotopy theory},
    SERIES = {Lecture Notes in Mathematics},
    VOLUME = {1213},
      NOTE = {With contributions by J. E. McClure},
 PUBLISHER = {Springer-Verlag, Berlin},
      YEAR = {1986},
     PAGES = {x+538},
      ISBN = {3-540-16820-6},
   MRCLASS = {55-02 (55Nxx 55Pxx 57S99)},
  MRNUMBER = {866482},
MRREVIEWER = {T. tom Dieck},
       DOI = {10.1007/BFb0075778},
       URL = {http://dx.doi.org/10.1007/BFb0075778},
}

@incollection {LicataShulman,
    AUTHOR = {Licata, Daniel R. and Shulman, Michael},
     TITLE = {Calculating the fundamental group of the circle in homotopy
              type theory},
 BOOKTITLE = {2013 28th {A}nnual {ACM}/{IEEE} {S}ymposium on {L}ogic in
              {C}omputer {S}cience ({LICS} 2013)},
     PAGES = {223--232},
 PUBLISHER = {IEEE Computer Soc., Los Alamitos, CA},
      YEAR = {2013},
   MRCLASS = {03B15 (55U40)},
  MRNUMBER = {3323808},
MRREVIEWER = {Thomas John Hunter},
}

@inproceedings{licata2012canonicity,
  title={Canonicity for 2-dimensional type theory},
  author={Licata, D. and Harper, R.},
  booktitle={Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  pages={337--348},
  year={2012},
  organization={ACM}
}

@book {lucas,
    AUTHOR = {Lucas, Edouard},
     TITLE = {Th\'eorie des nombres. {T}ome {I}: {L}e calcul des nombres
              entiers, le calcul des nombres rationnels, la divisibilit\'e
              arithm\'etique},
 PUBLISHER = {Nouveau tirage augment\'e dun avant-propos de Georges Bouligand.
              Librairie Scientifique et Technique Albert Blanchard, Paris},
      YEAR = {1961},
     PAGES = {xxxiv+520},
   MRCLASS = {10.01},
  MRNUMBER = {0123503},
MRREVIEWER = {W. J. LeVeque},
}

@misc {Lumsdaine11Blog,
    AUTHOR = {Lefanu Lumsdaine, Peter},
     TITLE = {Higher inductive types: a tour of the menagerie},
       URL = {https://homotopytypetheory.org/2011/04/24/higher-inductive-types-a-tour-of-the-menagerie/},
      YEAR = {2011}
}

@misc {Lumsdaine12Blog,
  AUTHOR = {Lefanu Lumsdaine, Peter},
   TITLE = {Reducing all HIT's to 1-HIT's},
     URL = {https://homotopytypetheory.org/2012/05/07/reducing-all-hits-to-1-hits/},
    YEAR = {2012}
}

@article {Lumsdaine10,
    AUTHOR = {Lefanu Lumsdaine, Peter},
     TITLE = {Weak {$\omega$}-categories from intensional type theory
              [reprint of MR2720193]},
   JOURNAL = {Log. Methods Comput. Sci.},
  FJOURNAL = {Logical Methods in Computer Science},
      YEAR = {2010},
    NUMBER = {Special issue: Selected papers of the conference ``Typed
              Lambda Calculi and Applications 2009''},
     PAGES = {3:24, 19},
      ISSN = {1860-5974},
   MRCLASS = {03B15 (18D50)},
  MRNUMBER = {2912856},
}

@article{LumsdaineShulman,
   author = {{LeFanu Lumsdaine}, P. and {Shulman}, M.},
    title = "{Semantics of higher inductive types}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1705.07088},
 primaryClass = "math.LO",
 keywords = {Mathematics - Logic, Mathematics - Category Theory, 18C50 (primary), 03B15, 18G55},
     year = 2017,
    month = may,
     }

@article{LumsdaineWarren,
  title={The local universe model of type theory},
  author={Lumsdaine, P. and Warren, M.},
  journal={In preparation},
  year=2013
}

@book {Lurie09,
    AUTHOR = {Lurie, Jacob},
     TITLE = {Higher topos theory},
    SERIES = {Annals of Mathematics Studies},
    VOLUME = {170},
 PUBLISHER = {Princeton University Press, Princeton, NJ},
      YEAR = {2009},
     PAGES = {xviii+925},
      ISBN = {978-0-691-14049-0},
   MRCLASS = {18-02 (18B25 18E35 18G30 18G55 55U40)},
  MRNUMBER = {2522659},
MRREVIEWER = {Mark Hovey},
       DOI = {10.1515/9781400830558},
       URL = {http://dx.doi.org/10.1515/9781400830558},
}

@incollection{MacLaneMoerdijk,
    AUTHOR = {Mac Lane, S. and Moerdijk, I.},
     TITLE = {Topos theory},
 BOOKTITLE = {Handbook of algebra, {V}ol.\ 1},
    SERIES = {Handb. Algebr.},
    VOLUME = {1},
     PAGES = {501--528},
 PUBLISHER = {Elsevier},
      YEAR = {1996},
       DOI = {10.1016/S1570-7954(96)80018-0},
}

@article{maietti2005toward,
        Author = {Maietti, M. and Sambin, G.},
        Journal = {From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics},
        Pages = {91--114},
        Publisher = {Oxford Logic Guides},
        Title = {Toward a minimalist foundation for constructive mathematics},
        Volume = {48},
        Year = {2005}}

@article{malatesta2012small,
  title={Small Induction Recursion, Indexed Containers and Dependent Polynomials are equivalent},
  author={Malatesta, L. and Altenkirch, T. and Ghani, N. and Hancock, P. and McBride, C.},
  journal={Submitted for Publication},
  year={2012}
}

@Book{		  MartinLof1984,
    AUTHOR = {Martin-L{\"o}f, Per},
     TITLE = {Intuitionistic type theory},
    SERIES = {Studies in Proof Theory. Lecture Notes},
    VOLUME = {1},
      NOTE = {Notes by Giovanni Sambin},
 PUBLISHER = {Bibliopolis, Naples},
      YEAR = {1984},
     PAGES = {iv+91},
      ISBN = {88-7088-105-9},
   MRCLASS = {03B15 (03F50 03F55)},
  MRNUMBER = {769301},
MRREVIEWER = {M. M. Richter},
}

@article {Massey52,
    AUTHOR = {Massey, W. S.},
     TITLE = {Exact couples in algebraic topology. {I}, {II}},
   JOURNAL = {Ann. of Math. (2)},
  FJOURNAL = {Annals of Mathematics. Second Series},
    VOLUME = {56},
      YEAR = {1952},
     PAGES = {363--396},
      ISSN = {0003-486X},
   MRCLASS = {56.0X},
  MRNUMBER = {0052770},
MRREVIEWER = {H. Cartan},
}

@book {May72,
    AUTHOR = {May, J. P.},
     TITLE = {The geometry of iterated loop spaces},
      NOTE = {Lectures Notes in Mathematics, Vol. 271},
 PUBLISHER = {Springer-Verlag, Berlin-New York},
      YEAR = {1972},
     PAGES = {viii+175},
   MRCLASS = {55D35},
  MRNUMBER = {0420610},
MRREVIEWER = {J. Stasheff},
}

@Book{mp:more-concise,
  author = 	 {J. P. May and K. Ponto},
  title = 	 {More concise algebraic topology},
  publisher = 	 {University of Chicago Press},
  year = 	 2012,
  series = 	 {Chicago lectures in mathematics}}

@book {McCleary01,
    AUTHOR = {McCleary, John},
     TITLE = {A user's guide to spectral sequences},
    SERIES = {Cambridge Studies in Advanced Mathematics},
    VOLUME = {58},
   EDITION = {Second},
 PUBLISHER = {Cambridge University Press, Cambridge},
      YEAR = {2001},
     PAGES = {xvi+561},
      ISBN = {0-521-56759-9},
   MRCLASS = {55Txx (18G40)},
  MRNUMBER = {1793722},
MRREVIEWER = {Frank Neumann},
}

@Book{Mines/R/R:1988,
  Author         = {Mines, R. and Richman, F. and Ruitenburg, W.},
  Title          = {A course in constructive algebra},
  Publisher      = {Springer},
  year           = 1988
}

@Book{		  MilnorCharacteristic,
  author	= {Milnor, John W. and Stasheff, James D.},
  title		= {Characteristic classes},
  note		= {Annals of Mathematics Studies, No. 76},
  publisher	= {Princeton University Press, Princeton, N. J.; University
		  of Tokyo Press, Tokyo},
  year		= {1974},
  pages		= {vii+331}
}

@Article{	  Milnor1956b,
  author	= {Milnor, John},
  title		= {Construction of universal bundles. {II}},
  journal	= {Ann. of Math. (2)},
  fjournal	= {Annals of Mathematics. Second Series},
  volume	= {63},
  year		= {1956},
  pages		= {430--436},
  issn		= {0003-486X},
  doi           = {10.2307/1970012}
}

@Article{	  Milnor1956,
  author	= {Milnor, John},
  title		= {On manifolds homeomorphic to the {$7$}-sphere},
  journal	= {Ann. of Math. (2)},
  fjournal	= {Annals of Mathematics. Second Series},
  volume	= {64},
  year		= {1956},
  pages		= {399--405},
  issn		= {0003-486X},
  mrclass	= {55.0X},
  mrnumber	= {0082103},
  mrreviewer	= {J. C. Moore}
}

@inproceedings {MoerdijkPalmgren2000,
    AUTHOR = {Moerdijk, I. and Palmgren, E.},
     TITLE = {Wellfounded trees in categories},
 BOOKTITLE = {Proceedings of the {W}orkshop on {P}roof {T}heory and
              {C}omplexity, {PTAC}'98 ({A}arhus)},
   JOURNAL = {Ann. Pure Appl. Logic},
    VOLUME = {104},
      YEAR = {2000},
    NUMBER = {1-3},
     PAGES = {189--218},
      ISSN = {0168-0072},
       DOI = {10.1016/S0168-0072(00)00012-9},
       URL = {http://dx.doi.org/10.1016/S0168-0072(00)00012-9},
}

@article {MoerdijkPalmgren2002,
    AUTHOR = {Moerdijk, I. and Palmgren, E.},
     TITLE = {Type theories, toposes and constructive set theory:
              predicative aspects of {AST}},
      NOTE = {Commemorative Symposium Dedicated to Anne S. Troelstra
              (Noordwijkerhout, 1999)},
   JOURNAL = {Ann. Pure Appl. Logic},
  FJOURNAL = {Annals of Pure and Applied Logic},
    VOLUME = {114},
      YEAR = {2002},
    NUMBER = {1-3},
     PAGES = {155--201},
       DOI = {10.1016/S0168-0072(01)00079-3},
       URL = {http://dx.doi.org/10.1016/S0168-0072(01)00079-3},
}

@InProceedings{	  Moura2015,
  author	= "Moura, {Leonardo de} and Kong, Soonho and Avigad, Jeremy and
		  Doorn, Floris van and von Raumer, Jakob",
  editor	= "Felty, P. Amy and Middeldorp, Aart",
  title 	= "The Lean Theorem Prover (System Description)",
  booktitle	= "Automated Deduction -- CADE-25",
  year		= "2015",
  publisher	= "Springer",
  address       = "Cham",
  pages		= "378--388",
  doi		= "10.1007/978-3-319-21401-6_26",
}

@article {Nishida73,
    AUTHOR = {Nishida, Goro},
     TITLE = {The nilpotency of elements of the stable homotopy groups of
              spheres},
   JOURNAL = {J. Math. Soc. Japan},
  FJOURNAL = {Journal of the Mathematical Society of Japan},
    VOLUME = {25},
      YEAR = {1973},
     PAGES = {707--732},
      ISSN = {0025-5645},
   MRCLASS = {55E45},
  MRNUMBER = {0341485},
MRREVIEWER = {J. F. Adams},
}

@InCollection{    Notbohm1995,
  author	= {D. Notbohm},
  title		= {Classifying spaces of compact Lie groups and finite loop
		  spaces},
  booktitle	= {Handbook of algebraic topology},
  isbn		= {0-444-81779-4/hbk},
  pages		= {1049--1094},
  year		= {1995},
  publisher	= {Amsterdam: North-Holland}
}

@article{palmgren2012constructivist,
  title={Constructivist and structuralist foundations: Bishop’s and Lawvere’s theories of sets},
  author={Palmgren, E.},
  journal={Annals of Pure and Applied Logic},
  year={2012},
  publisher={Elsevier}
}

@incollection {Palmgren1998,
    AUTHOR = {Palmgren, E.},
     TITLE = {On universes in type theory},
 BOOKTITLE = {Twenty-five years of constructive type theory ({V}enice,
              1995)},
    SERIES = {Oxford Logic Guides},
    VOLUME = {36},
     PAGES = {191--204},
 PUBLISHER = {Oxford Univ. Press},
      YEAR = {1998}
}

@article{pelayo2013preliminary,
  title={A preliminary univalent formalization of the p-adic numbers},
  author={Pelayo, {\'A}. and Voevodsky, V. and Warren, M.},
  journal={arXiv:1302.1207},
  eprint={arXiv:1302.1207},
  year={2013}
}

@article{pelayo2012homotopy,
  title={Homotopy type theory and {V}oevodsky's univalent foundations},
  author={Pelayo, {\'A}. and Warren, M.},
  journal={arXiv:1210.5658},
  eprint={1210.5658},
  year={2012}
}

@incollection {Pontryagin59,
    AUTHOR = {Pontryagin, L. S.},
     TITLE = {Smooth manifolds and their applications in homotopy theory},
 BOOKTITLE = {American {M}athematical {S}ociety {T}ranslations, {S}er. 2,
              {V}ol. 11},
     PAGES = {1--114},
 PUBLISHER = {American Mathematical Society, Providence, R.I.},
      YEAR = {1959},
   MRCLASS = {57.00},
  MRNUMBER = {0115178},
}

@book {Ravenel86,
    AUTHOR = {Ravenel, Douglas C.},
     TITLE = {Complex cobordism and stable homotopy groups of spheres},
    SERIES = {Pure and Applied Mathematics},
    VOLUME = {121},
 PUBLISHER = {Academic Press, Inc., Orlando, FL},
      YEAR = {1986},
     PAGES = {xx+413},
      ISBN = {0-12-583430-6; 0-12-583431-4},
   MRCLASS = {55-02 (55Qxx 57-02)},
  MRNUMBER = {860042},
MRREVIEWER = {Joseph Neisendorfer},
}

@Misc{            Rezk,
  author        = {Charles Rezk},
  title         = {Proof of the {B}lakers-{M}assey Theorem},
  year          = {2015},
  note          = {Note},
  url           = {http://www.math.uiuc.edu/~rezk/freudenthal-and-blakers-massey.pdf}
}

@misc{rezk2014homotopy,
  title={WHEN ARE HOMOTOPY COLIMITS COMPATIBLE WITH HOMOTOPY BASE CHANGE?},
  author={Rezk, Charles},
 url={http://www.math.uiuc.edu/~rezk/i-hate-the-pi-star-kan-condition.pdf},
 year={2014}
}

@article{rezk2010toposes,
  title={Toposes and homotopy toposes (version 0.15)},
  author={Rezk, C.},
  year={2010}
}

@ARTICLE{RijkeShulmanSpitters,
   author = {{Rijke}, E. and {Shulman}, M. and {Spitters}, B.},
    title = "{Modalities in homotopy type theory}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1706.07526},
 primaryClass = "math.CT",
 keywords = {Mathematics - Category Theory, Computer Science - Logic in Computer Science, Mathematics - Logic, 03B15, 03B35, 03B45, 03B70, 03F65, 03G30, 18A32, 18B25, 18C35, 18C50, 18D30, F.3.1, F.4.1},
     year = 2017,
    month = jun,
}

@article {RijkeSpitters,
    AUTHOR = {Rijke, Egbert and Spitters, Bas},
     TITLE = {Sets in homotopy type theory},
   JOURNAL = {Math. Structures Comput. Sci.},
  FJOURNAL = {Mathematical Structures in Computer Science. A Journal in the
              Applications of Categorical, Algebraic and Geometric Methods
              in Computer Science},
    VOLUME = {25},
      YEAR = {2015},
    NUMBER = {5},
     PAGES = {1172--1202},
      ISSN = {0960-1295},
   MRCLASS = {03B15 (03E99 18Bxx 55U35)},
  MRNUMBER = {3340540},
MRREVIEWER = {Krzysztof R. Kapulkin},
       DOI = {10.1017/S0960129514000553},
       URL = {http://dx.doi.org/10.1017/S0960129514000553},
}

@book {Rudyak98,
    AUTHOR = {Rudyak, Yuli B.},
     TITLE = {On {T}hom spectra, orientability, and cobordism},
    SERIES = {Springer Monographs in Mathematics},
      NOTE = {With a foreword by Haynes Miller},
 PUBLISHER = {Springer-Verlag, Berlin},
      YEAR = {1998},
     PAGES = {xii+587},
      ISBN = {3-540-62043-5},
   MRCLASS = {55-02 (55N22 55P42 57-02)},
  MRNUMBER = {1627486},
MRREVIEWER = {Donald M. Davis},
}

@Article{	  Serre1951,
  author	= {Serre, Jean-Pierre},
  title		= {Homologie singuli\`ere des espaces fibr\'es.
		  {A}pplications},
  journal	= {Ann. of Math. (2)},
  fjournal	= {Annals of Mathematics. Second Series},
  volume	= {54},
  year		= {1951},
  pages		= {425--505},
  issn		= {0003-486X}
}

@article {Serre53,
    AUTHOR = {Serre, Jean-Pierre},
     TITLE = {Groupes d'homotopie et classes de groupes ab\'eliens},
   JOURNAL = {Ann. of Math. (2)},
  FJOURNAL = {Annals of Mathematics. Second Series},
    VOLUME = {58},
      YEAR = {1953},
     PAGES = {258--294},
      ISSN = {0003-486X},
   MRCLASS = {56.0X},
  MRNUMBER = {0059548},
MRREVIEWER = {W. S. Massey},
}

@unpublished{SerreSpectralSequence,
    author = "Doorn, Floris van and Avigad, Jeremy and Awodey, Steve and Buchholtz, Ulrik and Rijke, Egbert and Shulman, Mike",
    title = "Spectral Sequences in Homotopy Type Theory",
    year = "2018",
    url = "https://github.com/cmu-phil/Spectral",
    note = "Paper forthcoming."
  }

@article{UrsCohesive,
  title={Differential cohomology in a cohesive infinity-topos},
  author={Schreiber, Urs},
  journal={arXiv:1310.7930},
  year={2013}
}

@InProceedings{   SchreiberShulman,
  author	= {Schreiber, Urs and Shulman, Michael},
  year		= {2014},
  title		= {Quantum Gauge Field Theory in Cohesive Homotopy Type
		  Theory},
  editor	= {Duncan, Ross and Panangaden, Prakash},
  booktitle	= {{\rm Proceedings 9th Workshop on} Quantum Physics and
		  Logic, {\rm Brussels, Belgium, 10-12 October 2012}},
  series	= {Electronic Proceedings in Theoretical Computer Science},
  volume	= {158},
  publisher	= {Open Publishing Association},
  address       = {Waterloo, NSW},
  pages		= {109-126},
  doi		= {10.4204/EPTCS.158.8}
}

@Misc{		  Shulman-classifying,
  author	= {Shulman, Michael},
  title		= {The Univalent Perspective on Classifying Spaces},
  year		= {2015},
  note		= {Blog post. The {$n$}-Category Caf{\'e}},
  url		= {https://golem.ph.utexas.edu/category/2015/01/the_univalent_perspective_on_c.html},
  lastaccessed	= {Jan.~29, 2018}
}

@unpublished{Shulman:HIT,
author={M. Shulman},
title={A tentative proposal for a general syntax of higher inductive types},
note={\url{http://uf-ias-2012.wikispaces.com/file/view/syntax.pdf/382449944/syntax.pdf}},
year=2012
}

@misc{Shulman13Cohomology,
  title = {Cohomology},
   author = {Shulman, Michael},
  howpublished = {\url{https://homotopytypetheory.org/2013/07/24/cohomology/}},
  year = {2013}
}

@misc{Shulman13Spectral,
  title = {Spectral sequences in HoTT},
  author = {Shulman, Michael},
  howpublished = {\url{https://ncatlab.org/homotopytypetheory/show/spectral+sequences}},
  year = {2013},
}

@misc{Shulman11Blog,
  title = {Homotopy Type Theory, VI},
  author = {Shulman, Michael},
  howpublished = {\url{https://golem.ph.utexas.edu/category/2011/04/homotopy_type_theory_vi.html}},
  year = {2011}
}

@article {shulman:inverseEI,
    AUTHOR = {Shulman, Michael},
     TITLE = {Univalence for inverse {EI} diagrams},
   JOURNAL = {Homology Homotopy Appl.},
  FJOURNAL = {Homology, Homotopy and Applications},
    VOLUME = {19},
      YEAR = {2017},
    NUMBER = {2},
     PAGES = {219--249},
      ISSN = {1532-0073},
   MRCLASS = {55U35 (03G30 18G55)},
  MRNUMBER = {3723769},
MRREVIEWER = {Thomas H\"uttemann},
       DOI = {10.4310/HHA.2017.v19.n2.a12},
       URL = {https://doi.org/10.4310/HHA.2017.v19.n2.a12},
}

@article{shulman2012univalence,
author = {Shulman, Michael},
title = {Univalence for inverse diagrams and homotopy canonicity},
journal = {Mathematical Structures in Computer Science},
volume = {25},
issue = {Special Issue 05},
month = {6},
year = {2015},
issn = {1469-8072},
pages = {1203--1277},
numpages = {75},
doi = {10.1017/S0960129514000565},
URL = {http://journals.cambridge.org/article_S0960129514000565},
eprint={1203.3253},
}

@article {Shulman15,
    AUTHOR = {Shulman, Michael},
     TITLE = {The univalence axiom for elegant {R}eedy presheaves},
   JOURNAL = {Homology Homotopy Appl.},
  FJOURNAL = {Homology, Homotopy and Applications},
    VOLUME = {17},
      YEAR = {2015},
    NUMBER = {2},
     PAGES = {81--106},
      ISSN = {1532-0073},
   MRCLASS = {03G30 (18G55 55U35)},
  MRNUMBER = {3421464},
MRREVIEWER = {Krzysztof R. Kapulkin},
       DOI = {10.4310/HHA.2015.v17.n2.a6},
       URL = {http://dx.doi.org/10.4310/HHA.2015.v17.n2.a6},
}

@article{shulmanlogicofspace,
author={Michael Shulman},
title={Homotopy type theory: the logic of space},
journal={arXiv:1703.03007},
year=2017
}

@article{shulman2015brouwer,
 AUTHOR = {Shulman, Michael},
     TITLE = {Brouwer's fixed-point theorem in real-cohesive homotopy type
              theory},
   JOURNAL = {Math. Structures Comput. Sci.},
  FJOURNAL = {Mathematical Structures in Computer Science. A Journal in the
              Applications of Categorical, Algebraic and Geometric Methods
              in Computer Science},
    VOLUME = {28},
      YEAR = {2018},
    NUMBER = {6},
     PAGES = {856--941},
      ISSN = {0960-1295},
   MRCLASS = {18G55 (03B40 55M20)},
  MRNUMBER = {3798599},
       DOI = {10.1017/S0960129517000147},
       URL = {https://doi.org/10.1017/S0960129517000147},
}

@unpublished{Shulman2013,
author={Shulman, M.},
title={Higher modalities},
URL={\url{http://uf-ias-2012.wikispaces.com/file/view/modalitt.pdf/376001920/modalitt.pdf}},
NOTE={\url{http://uf-ias-2012.wikispaces.com/file/view/modalitt.pdf/376001920/modalitt.pdf}}
}

@Misc{            Shulman2017,
  author	= {Michael Shulman},
  title		= {Elementary {$(\infty,1)$}-Topoi},
  year		= {2017},
  note          = {Blog post},
  url           = {https://golem.ph.utexas.edu/category/2017/04/elementary_1topoi.html}
}

@Article{	  Snaith1979,
  author	= {Snaith, Victor P.},
  title		= {Algebraic cobordism and {$K$}-theory},
  journal	= {Mem. Amer. Math. Soc.},
  fjournal	= {Memoirs of the American Mathematical Society},
  volume	= {21},
  year		= {1979},
  number	= {221},
  pages		= {vii+152},
  doi		= {10.1090/memo/0221},
}

@Article{         Snaith1981,
  author	= {Snaith, Victor P.},
  title		= {Localized stable homotopy of some classifying spaces},
  journal	= {Math. Proc. Cambridge Philos. Soc.},
  fjournal	= {Mathematical Proceedings of the Cambridge Philosophical
		  Society},
  volume	= {89},
  year		= {1981},
  number	= {2},
  pages		= {325--330},
  doi		= {10.1017/S0305004100058205},
}

@ARTICLE{HITsinitial,
   author = {Sojakova, K.},
    title = "{Higher Inductive Types as Homotopy-Initial Algebras}",
  journal = {ArXiv:1402.0761},
     year = 2014,
}

@PhDthesis {SojakovaPhD,
   AUTHOR = {Sojakova, Kristina},
   TITLE  = {Higher Inductive Types as Homotopy-Initial Algebras},
   SCHOOL = {School of Computer Science, Carnegie Mellon University},
    YEAR  = {2016},
   MONTH  = {8},
   URL    = {http://reports-archive.adm.cs.cmu.edu/anon/2016/CMU-CS-16-125.pdf}}

@phdthesis{Spiwack,
        Author = {Spiwack, A.},
        School = {{\'Ecole Polytechnique, Palaiseau, France}},
        Title = {A Journey Exploring the Power and Limits of Dependent Type Theory},
        Year = 2011}

@Article{	  Stasheff1963,
  author	= {Stasheff, James Dillon},
  title		= {Homotopy associativity of {$H$}-spaces. {I}, {II}},
  journal	= {Trans. Amer. Math. Soc. 108 (1963), 275-292; ibid.},
  fjournal	= {Transactions of the American Mathematical Society},
  volume	= {108},
  year		= {1963},
  pages		= {293--312},
  issn		= {0002-9947}
}

@book {Steenrod62,
    AUTHOR = {Steenrod, N. E.},
     TITLE = {Cohomology operations},
    SERIES = {Lectures by N. E. Steenrod written and revised by D. B. A.
              Epstein. Annals of Mathematics Studies, No. 50},
 PUBLISHER = {Princeton University Press, Princeton, N.J.},
      YEAR = {1962},
     PAGES = {vii+139},
   MRCLASS = {55.34},
  MRNUMBER = {0145525},
MRREVIEWER = {S.-T. Hu},
}

@article{Streicher:sstt,
author={Streicher, T.},
title={A Model of Type Theory in Simplicial Sets},
journal={Journal of Applied Logic},
publisher={Elsevier},
year=2013,
doi={10.1016/j.jal.2013.04.001}
}

@Article{	  Sugawara1957a,
  author	= {Sugawara, Masahiro},
  title		= {On a condition that a space is an {$H$}-space},
  journal	= {Math. J. Okayama Univ.},
  fjournal	= {Mathematical Journal of Okayama University},
  volume	= {6},
  year		= {1957},
  pages		= {109--129},
  issn		= {0030-1566}
}

@book {Switzer02,
    AUTHOR = {Switzer, Robert M.},
     TITLE = {Algebraic topology---homotopy and homology},
    SERIES = {Classics in Mathematics},
      NOTE = {Reprint of the 1975 original [Springer, New York;  MR0385836
              (52 \#6695)]},
 PUBLISHER = {Springer-Verlag, Berlin},
      YEAR = {2002},
     PAGES = {xiv+526},
      ISBN = {3-540-42750-3},
   MRCLASS = {55-02},
  MRNUMBER = {1886843},
}

@article {Thom54,
    AUTHOR = {Thom, Ren{\'e}},
     TITLE = {Quelques propri\'et\'es globales des vari\'et\'es
              diff\'erentiables},
   JOURNAL = {Comment. Math. Helv.},
  FJOURNAL = {Commentarii Mathematici Helvetici},
    VOLUME = {28},
      YEAR = {1954},
     PAGES = {17--86},
      ISSN = {0010-2571},
   MRCLASS = {56.0X},
  MRNUMBER = {0061823},
MRREVIEWER = {W. S. Massey},
}

@Book{hottbook,
  author =    {The {Univalent Foundations Program}},
  title =     {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher = {\url{https://homotopytypetheory.org/book}},
  address =   {Institute for Advanced Study},
  year =      2013
}

@Book{TheBook,
  author =       {The {Univalent Foundations Program}},
  title =        {Homotopy Type Theory: Univalent Foundations of Mathematics},
  shortauthor =  {UFP},
  publisher =    {\url{http://homotopytypetheory.org/book/}},
  edition =      {first},
  year =         2013}

@ARTICLE{Uemura,
   author = {{Uemura}, T.},
    title = "{Fibred Fibration Categories}",
  journal = {ArXiv},
   eprint = {1602.08206},
     year = 2016
}

@techreport{TTS,
author={Vladimir Voevodsky},
title={A simple type system with two identity types},
url={http://uf-ias-2012.wikispaces.com/file/view/HTS.pdf/410120566/HTS.pdf},
note={\url{http://uf-ias-2012.wikispaces.com/file/view/HTS.pdf/410120566/HTS.pdf}},
year=2013}

@unpublished{Universe-poly,
author={V. Voevodsky},
title ={A universe polymorphic type system},
url={\url{http://uf-ias-2012.wikispaces.com/file/view/Universe%20polymorphic%20type%20sytem.pdf/371099118/Universe%20polymorphic%20type%20sytem.pdf}},
year=2012
}

@article {Voevodsky15,
    AUTHOR = {Voevodsky, Vladimir},
     TITLE = {A {C}-system defined by a universe category},
   JOURNAL = {Theory Appl. Categ.},
  FJOURNAL = {Theory and Applications of Categories},
    VOLUME = {30},
      YEAR = {2015},
     PAGES = {No. 37, 1181--1215},
      ISSN = {1201-561X},
   MRCLASS = {18C99 (03G30)},
  MRNUMBER = {3402489},
MRREVIEWER = {Fabio Pasquali},
}

@unpublished {Voevodsky06,
  AUTHOR = {Voevodsky, Vladimir},
   TITLE = {A very short note on homotopy $\lambda$-calculus},
     URL = {http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf},
    YEAR = {2006}
}

@unpublished {Voevodsky10,
  AUTHOR = {Voevodsky, Vladimir},
   TITLE = {Univalent Foundations Project},
     URL = {http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/univalent_foundations_project.pdf},
    YEAR = {2010}
}

@article {UniMath2015,
    AUTHOR = {Voevodsky, Vladimir},
     TITLE = {An experimental library of formalized mathematics based on the
              univalent foundations},
   JOURNAL = {Math. Structures Comput. Sci.},
  FJOURNAL = {Mathematical Structures in Computer Science. A Journal in the
              Applications of Categorical, Algebraic and Geometric Methods
              in Computer Science},
    VOLUME = {25},
      YEAR = {2015},
    NUMBER = {5},
     PAGES = {1278--1294},
      ISSN = {0960-1295},
   MRCLASS = {68N18 (03B35)},
  MRNUMBER = {3340542},
       DOI = {10.1017/S0960129514000577},
       URL = {http://dx.doi.org/10.1017/S0960129514000577},
}

@Misc{UniMath,
   author = {Voevodsky, Vladimir and Ahrens, Benedikt and Grayson, Daniel and others},
   title = {{\em UniMath}: {Univalent} {Mathematics}},
   howpublished = {Available at \url{https://github.com/UniMath}}
}

@ARTICLE{WellenPhD,
   author = {{Wellen}, F.},
    title = "{Cartan Geometry in Modal Homotopy Type Theory}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1806.05966},
 primaryClass = "math.DG",
 keywords = {Mathematics - Differential Geometry, Mathematics - Algebraic Geometry, Mathematics - Category Theory, 58A15},
     year = 2018,
    month = jun,
   adsurl = {http://adsabs.harvard.edu/abs/2018arXiv180605966W},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}

@inproceedings{werner1997sets,
  title={Sets in types, types in sets},
  author={Werner, B.},
  booktitle={Theoretical aspects of computer software},
  pages={530--546},
  year={1997},
  organization={Springer}
}

@Article{	  Wessel1799,
  author	= {Wessel, Casper},
  title		= {Om directionens analytiske betegning, et fors{\o}g,
		  anvendt fornemmelig til plane og sphaeriske polygoners
		  opl{\o}sning},
  journal	= {Nye samling af det Kongelige Danske Videnskabernes
		  Selskabs Skrifter},
  series	= {2nd ser.},
  volume	= {5},
  pages		= {496--518},
  year		= {1799}
}

@Article{	  West1972,
  author	= {West, Robert W.},
  title		= {{$H$}-spaces which are co-{$H$}-spaces},
  journal	= {Proc. Amer. Math. Soc.},
  fjournal	= {Proceedings of the American Mathematical Society},
  volume	= {31},
  year		= {1972},
  pages		= {580--582},
  issn		= {0002-9939},
  mrclass	= {55.40},
  mrnumber	= {0285006},
  mrreviewer	= {C. R. Curjel}
}

@article {Whitehead62,
    AUTHOR = {Whitehead, George W.},
     TITLE = {Generalized homology theories},
   JOURNAL = {Trans. Amer. Math. Soc.},
  FJOURNAL = {Transactions of the American Mathematical Society},
    VOLUME = {102},
      YEAR = {1962},
     PAGES = {227--283},
      ISSN = {0002-9947},
   MRCLASS = {55.30},
  MRNUMBER = {0137117},
MRREVIEWER = {S.-T. Hu},
}

@Article{	  Whitehead1949,
  author	= {J. H. C. Whitehead},
  title		= {Combinatorial homotopy. {II}},
  fjournal	= {Bulletin of the American Mathematical Society},
  journal	= {Bull. Am. Math. Soc.},
  volume	= {55},
  pages		= {453--496},
  year		= {1949},
  publisher	= {American Mathematical Society (AMS), Providence, RI},
  doi		= {10.1090/S0002-9904-1949-09213-3},
}

@article {Wilander2010,
    AUTHOR = {Wilander, O.},
     TITLE = {Setoids and universes},
   JOURNAL = {Math. Structures Comput. Sci.},
    VOLUME = {20},
      YEAR = {2010},
    NUMBER = {4},
     PAGES = {563--576},
       DOI = {10.1017/S0960129510000071},
       URL = {http://dx.doi.org/10.1017/S0960129510000071},
}

@PhdThesis{wilson:frames,
  author = 	 {J. T. Wilson},
  title = 	 {The assembly tower and some categorical and algebraic aspects of frame theory},
  school = 	 {Carnegie Mellon University},
  year = 	 1994}

repository: EgbertRijke/dissertation

repo_name: EgbertRijke/dissertation

extension: bib


text:
require allgui-full-image.bb

export IMAGE_BASENAME = "allgui-dev-image"

IMAGE_INSTALL += " \
    packagegroup-gui-dev \
    \
    xfce4-dev-tools \
    libxfce4ui-glade \
"

repository: ZeraGmbH/meta-mortsgna

repo_name: ZeraGmbH/meta-mortsgna

gha_license_id: MIT


text:
package scanner

import (
	"fmt"
)

// UnexpectedCharacterError gives the error of an unexpected character in source
type UnexpectedCharacterError struct {
	line      int
	character string
}

func (e UnexpectedCharacterError) Error() string {
	return fmt.Sprintf("Unexpected character %s on line %d\n", e.character, e.line)
}

// UnterminatedStringError raised when a string is not closed with a double quote
type UnterminatedStringError struct {
	line int
}

func (e UnterminatedStringError) Error() string {
	return fmt.Sprintf("Unterminated string on col %d\n", e.line)
}

// UnterminatedCommentError raised when a string is not closed with a double quote
type UnterminatedCommentError struct {
	line int
}

func (e UnterminatedCommentError) Error() string {
	return fmt.Sprintf("Unterminated comment on col %d\n", e.line)
}

repository: musale/lode

repo_name: musale/lode


text:
package machine

import (
	"fmt"
	"os"
	"os/exec"
	"strconv"
	"strings"

	"koding/klient/machine/machinegroup"
	"koding/klientctl/klient"
	"koding/klientctl/ssh"

	"github.com/koding/logging"
)

// SSHOptions stores options for `machine ssh` call.
type SSHOptions struct {
	Identifier string // Machine identifier.
	Username   string // Remote machine user to log as.
	Log        logging.Logger
}

// SSH connects to remote machine using SSH protocol.
func SSH(options *SSHOptions) error {
	// Translate identifier to machine ID.
	//
	// TODO(ppknap): this is copied from klientctl old list and will be reworked.
	k, err := klient.CreateKlientWithDefaultOpts()
	if err != nil {
		fmt.Fprintln(os.Stderr, "Error creating klient:", err)
		return err
	}

	if err := k.Dial(); err != nil {
		fmt.Fprintln(os.Stderr, "Error dialing klient:", err)
		return err
	}

	idReq := machinegroup.IDRequest{
		Identifier: options.Identifier,
	}

	idRaw, err := k.Tell("machine.id", idReq)
	if err != nil {
		return err
	}

	idRes := machinegroup.IDResponse{}
	if err := idRaw.Unmarshal(&idRes); err != nil {
		return err
	}

	// Get local public key in case we need to copy it to remote machine.
	path, err := ssh.GetKeyPath(nil)
	if err != nil {
		return err
	}

	pubPath, privPath, err := ssh.KeyPaths(path)
	if err != nil {
		return err
	}

	pubkey, err := ssh.PublicKey(pubPath)
	if err != nil && err != ssh.ErrPublicKeyNotFound {
		return err
	}

	// Generate new key pair if it does not exist.
	if err == ssh.ErrPublicKeyNotFound {
		if pubkey, _, err = ssh.GenerateSaved(pubPath, privPath); err != nil {
			return err
		}
	}

	// Add created key to authorized hosts on remote machine.
	sshReq := machinegroup.SSHRequest{
		ID:        idRes.ID,
		Username:  options.Username,
		PublicKey: pubkey,
	}

	sshRaw, err := k.Tell("machine.ssh", sshReq)
	if err != nil {
		return err
	}

	sshRes := machinegroup.SSHResponse{}
	if err := sshRaw.Unmarshal(&sshRes); err != nil {
		return err
	}

	// TODO(ppknap): move this to ssh package.
	args := []string{
		"-i", privPath,
		"-o", "StrictHostKeychecking=no",
		"-o", "UserKnownHostsFile=/dev/null",
		"-o", "ServerAliveInterval=300",
		"-o", "ServerAliveCountMax=3",
		"-o", "ConnectTimeout=7",
		"-o", "ConnectionAttempts=1",
		sshRes.Username + "@" + sshRes.Host,
	}

	if sshRes.Port > 0 {
		args = append(args, "-p", strconv.Itoa(sshRes.Port))
	}

	options.Log.Info("Executing command: ssh %s", strings.Join(args, " "))
	cmd := exec.Command("ssh", args...)
	cmd.Stdin, cmd.Stdout, cmd.Stderr = os.Stdin, os.Stdout, os.Stderr
	return cmd.Run()
}

repository: dizag/koding

repo_name: dizag/koding


text:
package day2

import (
	"testing"

	"github.com/stretchr/testify/assert"

	"github.com/stephbu/aoc2019/util"
)

func TestPart1Sample1(t *testing.T) {
	memory := util.StringSplitInt("1,0,0,0,99")
	_, _ = RunProcessor(memory)
	assert.Equal(t, 2, memory[0])
}

func TestPart1Sample2(t *testing.T) {
	memory := util.StringSplitInt("2,3,0,3,99")
	_, _ = RunProcessor(memory)
	assert.Equal(t, 6, memory[3])
}

func TestPart1Sample3(t *testing.T) {
	memory := util.StringSplitInt("2,4,4,5,99,0")
	_, _ = RunProcessor(memory)
	assert.Equal(t, 9801, memory[5])
}

func TestPart1Sample4(t *testing.T) {
	memory := util.StringSplitInt("1,1,1,4,99,5,6,0,99")
	_, _ = RunProcessor(memory)
	assert.Equal(t, 30, memory[0])
}

func TestPart1PuzzleInput(t *testing.T) {
	memory := util.StringSplitInt("1,0,0,3,1,1,2,3,1,3,4,3,1,5,0,3,2,9,1,19,1,19,6,23,2,6,23,27,2,27,9,31,1,5,31,35,1,35,10,39,2,39,9,43,1,5,43,47,2,47,10,51,1,51,6,55,1,5,55,59,2,6,59,63,2,63,6,67,1,5,67,71,1,71,9,75,2,75,10,79,1,79,5,83,1,10,83,87,1,5,87,91,2,13,91,95,1,95,10,99,2,99,13,103,1,103,5,107,1,107,13,111,2,111,9,115,1,6,115,119,2,119,6,123,1,123,6,127,1,127,9,131,1,6,131,135,1,135,2,139,1,139,10,0,99,2,0,14,0")
	memory[1] = 12
	memory[2] = 2
	_, _ = RunProcessor(memory)
	t.Logf("memory[0]=%v", memory[0])
}

func TestPart2PuzzleInput(t *testing.T) {

	testMemory := util.StringSplitInt("1,0,0,3,1,1,2,3,1,3,4,3,1,5,0,3,2,9,1,19,1,19,6,23,2,6,23,27,2,27,9,31,1,5,31,35,1,35,10,39,2,39,9,43,1,5,43,47,2,47,10,51,1,51,6,55,1,5,55,59,2,6,59,63,2,63,6,67,1,5,67,71,1,71,9,75,2,75,10,79,1,79,5,83,1,10,83,87,1,5,87,91,2,13,91,95,1,95,10,99,2,99,13,103,1,103,5,107,1,107,13,111,2,111,9,115,1,6,115,119,2,119,6,123,1,123,6,127,1,127,9,131,1,6,131,135,1,135,2,139,1,139,10,0,99,2,0,14,0")
	cpy := make([]int, len(testMemory))

	for noun := 0; noun <= 99; noun++ {
		for verb := 0; verb <= 99; verb++ {

			copy(cpy, testMemory)

			cpy[1] = noun
			cpy[2] = verb

			_, err := RunProcessor(cpy)
			if err != nil {
				continue
			}

			if cpy[0] == 19690720 {
				t.Logf("Noun:%v, Verb:%v, Answer:%v", noun, verb, (noun*100)+verb)
				return
			}
		}
	}
	t.Fail()
}


text:
SUMMARY = "Ampere Computing LLC Update MAC Address from FRU Inventory Information"
DESCRIPTION = "Update MAC Address from FRU Inventory Information for Ampere systems"
PR = "r1"

LICENSE = "Apache-2.0"

LIC_FILES_CHKSUM = "file://${COMMON_LICENSE_DIR}/Apache-2.0;md5=89aea4e17d99a7cacdbeed46a0096b10"

inherit systemd
inherit obmc-phosphor-systemd

DEPENDS = "systemd"
RDEPENDS:${PN} = "bash"

FILESEXTRAPATHS:append := "${THISDIR}/${PN}:"

SYSTEMD_SERVICE:${PN} = "ampere_update_mac.service"

repository: openbmc/openbmc

repo_name: openbmc/openbmc

gha_license_id: NOASSERTION

gha_language: Python