Releases: pthariensflame/agda-fumulas
Releases · pthariensflame/agda-fumulas
v0.3.0
Major changes:
- tensor units of extrusions
- layerings of extrusions on their fumulas
- extrusion hierarchy is now simpler and has a few new properties available
Minor changes:
- change subscripts to superscripts for names of properties, for consistency
- generalize extrusion direct products for different universe levels
Full Changelog: v0.2.1...v0.3.0
v0.2.1
New features:
- Construction of fumulas "pointwise" over a function space
- Construction of initial and terminal extrusions, and of direct products of extrusions
Full Changelog: v0.2.0...v0.2.1
Version 0.2.0: extrusions and constructions and more, oh my
Major new features
- fumula extrusions, the fumula-world counterpart to modules over rings
- construction of initial/terminal (almost) fumulas, direct products of (almost) fumulas, and identity and composition of (almost) fumula homomorphisms
Other changes
- the tripoint bracket operator
_⤙_⤚_
is no longerinfixl
, and instead is justinfix
- conversion of reversible fumulas to and from commutative rings
- fumula property names no longer have useless
_
s ●-◆-collapse-side{,ˡ,ʳ}
have been moved out of the structures and intoProperties
, as they are derivable from the other axioms{↑-⤙⤚-●,↓-⤙⤚-■}-dup-nest{,ˡ,ʳ}
have been introduced inProperties
- the heartline of a fumula (the shadow of the integers within it) is now available, with some theorems about it, in
Properties
Full Changelog: v0.1.3...v0.2.0
Version 0.1.3
Version 0.1.2
Cleanup, better support for reversible fumulas, and support for morphism conversions.
Full Changelog: v0.1.1...v0.1.2
Version 0.1.1
Version 0.1.0
Basics are complete but bare-bones.