paper: update after mscs review

paper/depstream.v

@@ -0,0 +1,53 @@
+(** The interpretation of dependent streams as a coinductive type in Coq *)
+
+Section DepStream.
+
+Context {A} (B: A -> Type) (f: forall a, B a -> A).
+
+CoInductive DepStream (a: A): Type :=
+  { this : B a ; next : DepStream (f a this) }.
+
+Check this: forall a, DepStream a -> B a.
+Check next: forall a (x: DepStream a), DepStream (f a x.(this a)).
+
+Context (D: A -> Type) (v: forall a, D a -> B a)
+        (s: forall a d, D (f a (v a d))).
+
+CoFixpoint make a (d: D a) : DepStream a :=
+  {| this := v a d; next := make (f a (v a d)) (s a d) |}.
+
+Check fun a d => eq_refl: (make a d).(this a) = v a d.
+Check fun a d => eq_refl: (make a d).(next a) =
+  make (f a (make a d).(this a)) (s a d).
+
+End DepStream.
+
+(** Over propositions, we can also give a second-order interpretation *)
+
+Section DepStreamProp.
+
+Context {A: Prop} (B: A->Prop) (f: forall a, B a -> A).
+
+Definition DepStreamProp (a: A): Prop :=
+  exists D: A -> Prop, (D a /\ exists (v: forall a, D a -> B a),
+    (forall a d, D (f a (v a d)))).
+
+Definition this_prop a (x: DepStreamProp a): B a :=
+  let '(ex_intro _ D (conj d (ex_intro _ v s))) := x in v a d.
+
+Definition next_prop a (x: DepStreamProp a):
+  DepStreamProp (f a (this_prop a x)) :=
+  let '(ex_intro _ D (conj d (ex_intro _ v s))) := x in
+  ex_intro _ D (conj (s a d) (ex_intro _ v s)).
+
+Context (D: A -> Prop) (v: forall a, D a -> B a)
+  (s: forall a d, D (f a (v a d))).
+
+Definition make_prop a (d: D a): DepStreamProp a :=
+  ex_intro _ D (conj d (ex_intro _ v s)).
+
+Check fun a d => eq_refl: this_prop a (make_prop a d) = v a d.
+Check fun a d => eq_refl: next_prop a (make_prop a d) =
+  make_prop (f a (this_prop a (make_prop a d))) (s a d).
+
+End DepStreamProp.

paper/paper.bib

@@ -186,37 +186,6 @@ @phdthesis{moeneclaey22phd
   school = {Universit\'e Paris Cit\'e}
 }
 
-@manual{coq23,
-  author = {{The Coq Development Team}},
-  title  = {The {Coq} Reference Manual, version 8.18.0},
-  month  = {Jul},
-  year   = {2023},
-  url    = {https://coq.inria.fr/distrib/current/refman/}
-}
-
-@inproceedings{lean15,
-  author    = {Leonardo Mendon{\c{c}}a de Moura and
-               Soonho Kong and
-               Jeremy Avigad and
-               Floris van Doorn and
-               Jakob von Raumer},
-  editor    = {Amy P. Felty and
-               Aart Middeldorp},
-  title     = {The Lean Theorem Prover (System Description)},
-  booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on
-               Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
-  series    = {Lecture Notes in Computer Science},
-  volume    = {9195},
-  pages     = {378--388},
-  publisher = {Springer},
-  year      = {2015},
-  url       = {https://doi.org/10.1007/978-3-319-21401-6\_26},
-  doi       = {10.1007/978-3-319-21401-6\_26},
-  timestamp = {Tue, 14 May 2019 10:00:39 +0200},
-  biburl    = {https://dblp.org/rec/conf/cade/MouraKADR15.bib},
-  bibsource = {dblp computer science bibliography, https://dblp.org}
-}
-
 @misc{voevodsky12,
   author = {Vladimir Voevodsky},
   title  = {Semi-simplicial types},
@@ -381,14 +350,6 @@ @inproceedings{kraus21
   bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
-@manual{agda23,
-  author = {{The Agda Team}},
-  title  = {Agda User Manual, Release 2.6.4},
-  month  = {Jan},
-  year   = {2023},
-  url    = {https://readthedocs.org/projects/agda/downloads/pdf/latest}
-}
-
 @inproceedings{cohen16,
   author    = {Cyril Cohen and Thierry Coquand and Simon Huber and Anders M{\"{o}}rtberg},
   title     = {{Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom}},
@@ -464,7 +425,7 @@ @article{shulman15
   number    = {5},
   journal   = {Mathematical Structures in Computer Science},
   publisher = {Cambridge University Press},
-  author    = {SHULMAN, MICHAEL},
+  author    = {Shulman, Michael},
   year      = {2015},
   pages     = {1203–1277}
 }
@@ -531,6 +492,15 @@ @article{annenkovCK17
   bibsource    = {dblp computer science bibliography, https://dblp.org}
 }
 
+@article{AnnenkovCKS2023,
+  author={Annenkov, Danil and Capriotti, Paolo and Kraus, Nicolai and Sattler, Christian},
+  title={Two-level type theory and applications},
+  volume={33}, DOI={10.1017/S0960129523000130},
+  number={8}, journal={Mathematical Structures in Computer Science},
+  year={2023},
+  pages={688–743}
+}
+
 @article{shulman_2014,
 	doi = {10.1017/s0960129514000565},
  	url = {https://doi.org/10.1017%2Fs0960129514000565},
@@ -553,6 +523,31 @@ @PhDThesis{HofmannPhd
   year        = 1995
 }
 
+@inproceedings{HofmannStreicher94,
+  author      = {Martin Hofmann and Thomas Streicher},
+  title       = {The Groupoid Model Refutes Uniqueness of Identity Proofs},
+  booktitle   = {Proceedings of the Ninth Annual Symposium on Logic in Computer Science
+                 {(LICS} '94), Paris, France, July 4-7, 1994},
+  pages       = {208--212},
+  year        = {1994},
+  publisher   = {{IEEE} Computer Society},
+}
+
+@inproceedings{BezemCoquandHuber13,
+  author      = {Marc Bezem and Thierry Coquand and Simon Huber},
+  title       = {A Model of Type Theory in Cubical Sets},
+  booktitle   = {19th International Conference on Types for Proofs and Programs, {TYPES}
+                 2013, April 22-26, 2013, Toulouse, France},
+  pages       = {107--128},
+  year        = {2013},
+  url         = {https://doi.org/10.4230/LIPIcs.TYPES.2013.107},
+  doi         = {10.4230/LIPIcs.TYPES.2013.107},
+  editor      = {Ralph Matthes and Aleksy Schubert},
+  series      = {LIPIcs},
+  volume      = {26},
+  publisher   = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
+}
+
 @article{LoregianRiehl20,
   title       = {Categorical notions of fibration},
   journal     = {Expositiones Mathematicae},
@@ -565,3 +560,15 @@ @article{LoregianRiehl20
   author      = {Fosco Loregian and Emily Riehl},
   keywords    = {Grothendieck fibration, Two-sided fibration, Profunctor},
 }
+
+@article{nuytsdevriese24,
+  TITLE = {{Transpension: The Right Adjoint to the Pi-type}},
+  AUTHOR = {Andreas Nuyts and Dominique Devriese},
+  URL = {https://lmcs.episciences.org/13798},
+  DOI = {10.46298/lmcs-20(2:16)2024},
+  JOURNAL = {{Logical Methods in Computer Science}},
+  VOLUME = {{Volume 20, Issue 2}},
+  YEAR = {2024},
+  MONTH = Jun,
+  KEYWORDS = {Computer Science - Logic in Computer Science},
+}