JasonGross

/* cilkscreen.h                  -*-C++-*-
 *
 *************************************************************************
 *                         INTEL CONFIDENTIAL
 *
 * Copyright (C) 2010-2011 Intel Corporation.  All Rights Reserved.
 *
 *  The source code contained or described herein and all documents related
 *  to the source code ("Material") are owned by Intel Corporation or its
 *  suppliers or licensors.  Title to the Material remains with Intel

JasonGross

{S0
: forall b : C_Objects_Ex22,
  path D_Edges_Ex22 U_Ex22_D (F_Functor_Ex22_ObjectOf b) ->
  match b with
  | SSN_Ex22_C => SSN
  | FirstName_Ex22_C => FirstName
  | LastName_Ex22_C => LastName
  | Salary_Ex22_C => Salary
  | T1_Ex22_C => T1_Id_Ex222
  | T2_Ex22_C => T2_Id_Ex222

JasonGross

Require Import JMeq ProofIrrelevance.

Set Implicit Arguments.
Set Asymmetric Patterns.

Local Infix "==" := JMeq (at level 70).

(* The standard library does not provide projections of [sigT2] or [sig2].
   I define coercions to [sigT] and [sig], so that [projT1], [projT2],
   [proj1_sig], and [proj2_sig] do the right thing, and I define [projT3],

JasonGross

Require Export Adjoint.
Require Import Notations Common FunctorCategoryFunctorial Duals.

Set Implicit Arguments.

Generalizable All Variables.

Section SimplifiedMorphism.
  Section single_category.
    Context `{C : SpecializedCategory objC}.

JasonGross

Require Import Notations Common SpecializedCategory Functor NaturalTransformation.

Set Implicit Arguments.

Generalizable All Variables.

Section SimplifiedMorphism.
  Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type :=
  | ReifiedIdentityMorphism : forall objC C x, @ReifiedMorphism objC C x x
  | ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'

JasonGross

diff --git a/Adjoint.v b/Adjoint.v
index 2276dc5..bac19c8 100644
--- a/Adjoint.v
+++ b/Adjoint.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+

JasonGross

(** A 0-skeletal filling of an l-simplex is (S l) vertices.
    A (S k)-skeletal filling of an l-simplex has (S l) C (S k)  (S k)-cells
    matching their boundaries in a k-skeletal filling of an l-simplex;
    where to say the (S k)-cell matches its boundary is to say that its boundary
    is the underlying k-skeletal filling of its underlying (S k)-simplex.
 *)

(** This is both the heart of the matter, and the weakest link; for some reason
    this presentation of n C k makes it very difficult to prove equations.
    Perhaps some clever person can rework the whole around a different presentation.

JasonGross

/tmp /tmp/barnowl ~/Programs/barnowl ~/Programs/barnowl-packaging/packaging ~/Programs/barnowl
Cloning into barnowl...
autoreconf2.50: Entering directory `.'
autoreconf2.50: configure.ac: not using Gettext
autoreconf2.50: running: aclocal --force -I m4
autoreconf2.50: configure.ac: tracing
autoreconf2.50: configure.ac: not using Libtool
autoreconf2.50: running: /usr/bin/autoconf --force
autoreconf2.50: running: /usr/bin/autoheader --force
autoreconf2.50: running: automake --add-missing --copy --force-missing

JasonGross

diff -r 4eb6407c6ca3 Functor.v
--- a/Functor.v	Fri May 24 20:09:37 2013 -0400
+++ b/Functor.v	Sun Jun 30 04:03:22 2013 -0400
@@ -240,6 +240,23 @@
   Variable G : SpecializedFunctor D E.
   Variable F : SpecializedFunctor C D.
 
+  Local Notation CObjectOf x := (G (F x)).
+  Local Notation CMorphismOf m := (MorphismOf G (MorphismOf F m)).
+