rzk-lang/shott issues and pull requests

#149 - RS17, Proposition 9.10.

Pull Request - State: closed - Opened by robin-carlier 4 months ago - 4 comments

#148 - Update README.md

Pull Request - State: closed - Opened by nimarasekh 5 months ago - 1 comment

#147 - Generalized proofs of [RS17, Cor. 5.6]

Pull Request - State: open - Opened by thchatzidiamantis 6 months ago - 3 comments

#146 - Orientation conventions for 3-simplices

Issue - State: open - Opened by thchatzidiamantis 6 months ago

#145 - Weak FunExt implies FunExt

Pull Request - State: closed - Opened by thchatzidiamantis 6 months ago - 2 comments

#144 - Dependent Composition

Pull Request - State: closed - Opened by thchatzidiamantis 8 months ago - 8 comments

#143 - Update 06-contractible.rzk.md

Pull Request - State: closed - Opened by thchatzidiamantis 8 months ago - 9 comments

#142 - Auto-format all files

Pull Request - State: closed - Opened by aabounegm about 1 year ago - 2 comments

#141 - Representable isos

Pull Request - State: closed - Opened by cesarbm03 about 1 year ago - 9 comments

#140 - More on orthogonal calculus

Pull Request - State: closed - Opened by TashiWalde about 1 year ago

#139 - typo in mkdocs.yaml

Pull Request - State: closed - Opened by TashiWalde about 1 year ago

#138 - Functorial isomorphism of shape inclusions

Pull Request - State: closed - Opened by TashiWalde about 1 year ago - 1 comment

#137 - Reorganize proof that discrete types are Segal

Pull Request - State: closed - Opened by TashiWalde about 1 year ago - 5 comments

#136 - discrete and contractible types are Rezk

Pull Request - State: closed - Opened by TashiWalde about 1 year ago - 4 comments

#135 - Discrete fibers Cor. 8.20 RS17

Pull Request - State: closed - Opened by StiephenPradal over 1 year ago - 5 comments

#134 - More functoriality of fibers

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#133 - Formalize strict adjoint sections, LARI families and its closure properties

Issue - State: open - Opened by TashiWalde over 1 year ago

#132 - Embeddings and propositional fibers

Pull Request - State: closed - Opened by emilyriehl over 1 year ago - 1 comment

#131 - Uniqueness of adjunction data

Pull Request - State: closed - Opened by emilyriehl over 1 year ago - 4 comments

#130 - Functoriality properties of extension types

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#129 - Total fibers are iterated fibers

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#128 - Equivalences of maps induce equivalences of fibers

Pull Request - State: closed - Opened by aergus over 1 year ago - 2 comments

#127 - typo in the readme

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#126 - Anodyne shape inclusions

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 1 comment

#125 - colimits are unique up to isomorphism

Pull Request - State: closed - Opened by cesarbm03 over 1 year ago

#124 - Clean up 08-family-of-maps

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#123 - more on left orthogonal calculus

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#122 - Fibers between Segal types are Segal

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 1 comment

#121 - clean up 03-extension-types

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#120 - Fibers of right orthogonal maps have unique extensions

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 2 comments

#119 - Section-retraction pairs

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 7 comments

#118 - Further progress on right orthogonal calculus - part 2

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#117 - Update naming in 08-families-of-maps

Issue - State: closed - Opened by TashiWalde over 1 year ago

#116 - Alternative descriptions of discrete types

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#115 - Minor utilities

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#114 - remove outdated helpers for Theorem 8.8

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#113 - begin work on some homotopy coherences

Pull Request - State: closed - Opened by jonalfcam over 1 year ago - 17 comments

#112 - Further progress on right orthogonal calculus

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 3 comments

#111 - Fiber products

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#110 - Local types terminal map

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 2 comments

#109 - Clean up naming in 06-contractible

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#108 - Revert "NaiveExtExt implies WeakExtExt"

Pull Request - State: closed - Opened by jonweinb over 1 year ago - 1 comment

#107 - NaiveExtExt implies WeakExtExt

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 3 comments

#106 - Preservation of fibers under equivalences

Pull Request - State: closed - Opened by aergus over 1 year ago

#105 - Make extension weakening dependent

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#104 - Proposition utilities

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#103 - Formalize-yoneda-embedding-2

Pull Request - State: closed - Opened by cesarbm03 over 1 year ago - 9 comments

#102 - equivalences are embeddings

Issue - State: closed - Opened by jonalfcam over 1 year ago - 3 comments

#101 - fix wrong naming

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 3 comments

#100 - Formalize yoneda embedding

Pull Request - State: closed - Opened by cesarbm03 over 1 year ago - 8 comments

#99 - Discrete fibers

Pull Request - State: closed - Opened by StiephenPradal over 1 year ago - 1 comment

#98 - definition of a representable covariant family

Pull Request - State: closed - Opened by jonalfcam over 1 year ago - 8 comments

#97 - Error instead of commit on bad format

Pull Request - State: closed - Opened by fredrik-bakke over 1 year ago - 8 comments
Labels: bug

#96 - Fix permissions for autoformat workflow

Pull Request - State: closed - Opened by fredrik-bakke over 1 year ago - 8 comments
Labels: bug

#95 - Add autoformatting to CI (for Markdown, YAML, JSON)

Pull Request - State: closed - Opened by fredrik-bakke over 1 year ago - 16 comments

#95 - Add autoformatting to CI (for Markdown, YAML, JSON)

Pull Request - State: closed - Opened by fredrik-bakke over 1 year ago - 16 comments

#94 - Finish draft of the style guide

Pull Request - State: closed - Opened by fredrik-bakke over 1 year ago - 28 comments
Labels: documentation

#93 - Fiber facts

Pull Request - State: closed - Opened by emilyriehl over 1 year ago - 2 comments

#92 - Theorem 8.8

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 4 comments

#91 - Refactor is-right-orthogonal-to-shape-×

Issue - State: closed - Opened by TashiWalde over 1 year ago

#90 - Update mkdocs.yml

Pull Request - State: closed - Opened by emilyriehl over 1 year ago - 1 comment

#89 - integrate right orthogonal file by renumbering

Pull Request - State: closed - Opened by jonweinb over 1 year ago - 3 comments

#88 - Extension types up to homotopy

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 6 comments

#87 - renumbering sHoTT files

Issue - State: closed - Opened by emilyriehl over 1 year ago - 2 comments

#86 - Limits-colimits-2

Pull Request - State: closed - Opened by cesarbm03 over 1 year ago

#85 - Isomorphism extensionality

Pull Request - State: closed - Opened by dvmcarpena over 1 year ago - 2 comments

#84 - New proof that equivalences are contractible maps using fiber induction

Pull Request - State: closed - Opened by emilyriehl over 1 year ago - 4 comments

#83 - Equivalence of weak and strict extension types

Issue - State: closed - Opened by jonweinb over 1 year ago - 1 comment

#82 - Morphisms of Product Types

Pull Request - State: closed - Opened by nimarasekh over 1 year ago - 3 comments

#81 - Formalize closure properties of left orthogonal shapes and right orthogonal maps

Issue - State: open - Opened by TashiWalde over 1 year ago - 1 comment

#80 - functorial maps/equivalences

Issue - State: open - Opened by TashiWalde over 1 year ago

#79 - functorial instance of cofibration-composition

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 1 comment

#78 - Pullback of homotopy cartesian squares

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#77 - transport along a path is an equivalence

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#77 - transport along a path is an equivalence

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#76 - Right orthogonal fibrations

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#75 - Naive extext

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#74 - FunExt implies WeakFunExt

Pull Request - State: closed - Opened by MatthiasHu over 1 year ago - 6 comments

#73 - logical equivalence between weakfunext and funext

Issue - State: open - Opened by emilyriehl over 1 year ago - 6 comments

#72 - moved homotopy pullbacks into new file

Pull Request - State: closed - Opened by emilyriehl over 1 year ago - 1 comment

#71 - Interchange law for homotopies (RS17, Proposition 5.15)

Pull Request - State: closed - Opened by kyoDralliam over 1 year ago

#70 - Weak ext ext

Pull Request - State: closed - Opened by jonalfcam over 1 year ago - 11 comments

#69 - alternative defintion of slice and coslice as extension types

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 1 comment

#68 - Equivalences are invariant under equivalence

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

#67 - Functorial shape retract

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 1 comment

#66 - Formalization of Prop 10.3 of [RS17]

Pull Request - State: closed - Opened by dvmcarpena over 1 year ago - 2 comments

#65 - strengthen definition of limits/colimits

Issue - State: open - Opened by TashiWalde over 1 year ago - 1 comment

#64 - strengthen definition of inner anodyne

Issue - State: closed - Opened by TashiWalde over 1 year ago - 4 comments

#63 - Detect *.rzk.md as markdown and ignore overrides

Pull Request - State: closed - Opened by aabounegm over 1 year ago

#62 - strict computation property for first-path-Sigma

Issue - State: closed - Opened by TashiWalde over 1 year ago - 1 comment

#61 - extract computation rule for first-path-Sigma and eq-pair

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 1 comment

#60 - add Nima Rasekh to contributors

Pull Request - State: closed - Opened by jonweinb over 1 year ago - 1 comment

#59 - Vertical calculus for homotopy cartesian squares

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 2 comments

#58 - Towards Theorem 8.8

Pull Request - State: closed - Opened by cesarbm03 over 1 year ago - 1 comment

#57 - Definition of inner anodyne map

Pull Request - State: closed - Opened by kyoDralliam over 1 year ago - 7 comments

#56 - prove various things are propositions

Issue - State: open - Opened by emilyriehl over 1 year ago - 3 comments

#55 - Triangle identities

Pull Request - State: closed - Opened by emilyriehl over 1 year ago - 3 comments

#54 - Naive left fibrations vs covariant families

Pull Request - State: closed - Opened by TashiWalde over 1 year ago - 2 comments

#53 - symmetry of inverses, reversing equivalences

Pull Request - State: closed - Opened by floverity over 1 year ago

#52 - induction principle for fibers

Pull Request - State: closed - Opened by TashiWalde over 1 year ago

GitHub / rzk-lang/shott issues and pull requests