Reed Mullanix
Reed Mullanix
# Description Pulling some of my changes out of #375 in hopes of getting back to it at some point. This PR defines split surjectivity, and also proves some misc....
# Description This PR defines a notion of "Σ-basis", which is a nice encoding of an equivalence to a Σ type. It also defines some general reasoning principles for Σ-bases,...
As noted in #463, `Total-hom` is a bit of a wart, and makes any solution for displayed reasoning non-modular. Moreover, the names are pretty bad! Replacing it with a sigma...
Consider the following contrived example: ```agda module Slow {o ℓ o' ℓ'} {B : Precategory o ℓ} (E : Displayed B o' ℓ') where open Cat.Displayed.Reasoning E open Displayed E...
Currently, the definition of `is-total-order` is ```agda record is-total-order {o ℓ} (P : Poset o ℓ) : Type (o ⊔ ℓ) where open Poset P public field compare : ∀...
Inside of [InterfaceCommon.hs](https://github.com/JacquesCarette/Drasil/blob/795898c6867dfe4f6bce8db710bf9c2f59125a0d/code/drasil-gool/lib/Drasil/Shared/InterfaceCommon.hs#L111C1-L113C47) we have the following very suspicious bit of code: ```haskell class (VariableSym r) => VariableElim r where variableName :: r (Variable r) -> String variableType :: r...
Filters
# Description This PR defines filters in posets, and proves some basic facts about them. I've also added some basic supporting infrastructure for directed sets. At some point we should...
# Description Just some basic definitions about Reedy/direct categories, along with a theorem about reflective subcategories of reedy categories. ## Notes It might be worth omitting "generalized" from both of...
It might be worth considering replacing `Data.Vec` with a refinement type like ``` record Vec {ℓ} (A : Type ℓ) (n : Nat) : Type ℓ where constructor vec field...
Right now, we define `F-Algebras : Displayed C ℓ ℓ` by hand. However, we could also define it as `Change-of-base Cat⟨ Id , Id ⟩ (Comma F Id)`, which would...