[WIP] pi-clans - #164

Open

Jlh18 wants to merge 99 commits into

Commits on Oct 28, 2025

feat: UId
Jlh18
committed
c041a29

Commits on Oct 29, 2025

feat: StrongTrans.naturality lemmas
Jlh18
committed
c9c6337

Commits on Oct 30, 2025

.
Jlh18
committed
d44df5f

Commits on Oct 31, 2025

no errors
Jlh18
committed
d5ce49a
.
Jlh18
committed
32dd5c6

Commits on Nov 1, 2025

two sorrys left
Jlh18
committed
58b148f
Merge branch 'master' into GroupoidPi
Jlh18
committed
9a18f60
chore: tidy up pi file
Jlh18
committed
2694ddf
pi file sorry free
Jlh18
committed
1ec980c
merge Pi proofs
Jlh18
committed
6e6ca27
feat: pi.Over.equivFun
Jlh18
committed
e54b433
merge clans proofs
Jlh18
committed
de8b751
fix: build failure
Jlh18
committed
67c5759
fix: add local irreducible attr
Jlh18
committed
4a0ab48
feat: pushforward
Jlh18
committed
766ae08
chore: delete file copy
Jlh18
committed
21acc29
Merge branch 'GroupoidId1' into clans1
Jlh18
committed
6930328
need MorphismProperty.HasPullbacksAlong
Jlh18
committed
cfdc225

Commits on Nov 4, 2025

splitIsofibration
Jlh18
committed
80cd27c
feat: pushforward of split isofibrations
Jlh18
committed
681b1f0

Commits on Nov 9, 2025

trying to move clans |-> clans1

Yiming Xu
authored and
Yiming Xu
committed
9f48335
delete old SplitIso

Yiming Xu
authored and
Yiming Xu
committed
47034e1
style:
Jlh18
committed
06170cb
feat: StructuredModel
Jlh18
committed
f5f6d78

Commits on Nov 12, 2025

remove preserves pullbacks proofs
Jlh18
committed
4943f63
fix: remove unprovable lemmas
Jlh18
committed
2c168e1

Commits on Nov 13, 2025

feat: ClanOver
Jlh18
committed
889ed71
fix: OverFibration
Jlh18
committed
6543722
feat: automatic instances for ExtendedFibration
Jlh18
committed
6fe775a

Commits on Nov 14, 2025

feat: P.HasPushforwardsAlong f
Jlh18
committed
aff66f7
issue in line 62

Yiming Xu
authored and
Yiming Xu
committed
ead58b1
feat: instance : (Local R X).HasPullbacks
Jlh18
committed
d2c6a29

Commits on Nov 15, 2025

feat: pullbackMapTwoSquare_isIso
Jlh18
committed
9df666c
two attempts at pushforward BC
Jlh18
committed
f4f5ea8

Commits on Nov 17, 2025

feat: pushforwardForgetTwoSquare
Jlh18
committed
f5e3b9b
rename to pushforwardCompForget'
Jlh18
committed
66c32e2
fix: generalize to ExponentiableMorphism
Jlh18
committed
7a169c7
.
Jlh18
committed
053bc2c

Commits on Nov 19, 2025

tidy
Jlh18
committed
277962a

Commits on Nov 20, 2025

two approaches
Jlh18
committed
188f221
remove unnecessary lemmas
Jlh18
committed
1efb8b6
comment out last theorem
Jlh18
committed
dafa2f8
feat: auto sorry
Jlh18
committed
ec47b17
a bit progress

Yiming Xu
authored and
Yiming Xu
committed
2bda8f0
a bit tidying

Yiming Xu
authored and
Yiming Xu
committed
f4f113e
isCartesian_pullbackMapTwoSquare

Yiming Xu
authored and
Yiming Xu
committed
9869d80
golf: isCartesian_pullbackMapTwoSquare
Jlh18
committed
2f43eca
start making Yoneda stuff

Yiming Xu
authored and
Yiming Xu
committed
8ca5c36

Commits on Nov 21, 2025

defining equiv

Yiming Xu
authored and
Yiming Xu
committed
e49b07c
backup before starting deleting

Yiming Xu
authored and
Yiming Xu
committed
1364dda
defined yoneda equiv

Yiming Xu
authored and
Yiming Xu
committed
9126c67
defined equiv

Yiming Xu
authored and
Yiming Xu
committed
ddfc2b6
feat: NatIso.yonedaMk
Jlh18
committed
0d23668
dj.
Jlh18
committed
fc71ae3
golfs
Jlh18
committed
30158e3

Commits on Nov 22, 2025

.
Jlh18
committed
c132d86

Commits on Nov 24, 2025

feat: profunctor proof
Jlh18
committed
c4e6754
delete backup files
Jlh18
committed
a030fe5
chore: remove comments
Jlh18
committed
f9e0f76
feat: pushforwardYonedaIso, pushforwardPullbackIso
Jlh18
committed
aa8d1dd
feat: pushforwardYonedaIso, pushforwardPullbackIso
Jlh18
committed
1e3f82e

Commits on Nov 25, 2025

doc: pushforward
Jlh18
committed
30c33e2
change IdIntro.k and IdElimBase.i to just context extensions
Jlh18
committed
c5ce344

Commits on Nov 26, 2025

changing structured univ

Yiming Xu
authored and
Yiming Xu
committed
0b03d7d

Commits on Nov 27, 2025

refactoring

Yiming Xu
authored and
Yiming Xu
committed
b7f61bc
newest

Yiming Xu
authored and
Yiming Xu
committed
a61a953
feat: sorry goals
Jlh18
committed
67cac1b

Commits on Nov 28, 2025

fix the explicit var

Yiming Xu
authored and
Yiming Xu
committed
911c3c3

Commits on Dec 11, 2025

problem about motiveCtx

Yiming Xu
authored and
Yiming Xu
committed
30abe18
need context iso

Yiming Xu
authored and
Yiming Xu
committed
799fcf6
.
Jlh18
committed
93b9ef9

Commits on Dec 15, 2025

try to resolve the diverge

Yiming Xu
authored and
Yiming Xu
committed
ec9cbc4
GammaATmTm

Yiming Xu
authored and
Yiming Xu
committed
bddfd64

Commits on Dec 16, 2025

mtcxToUniversalIdPb

Yiming Xu
authored and
Yiming Xu
committed
67eef80
mtcxToTmPb

Yiming Xu
authored and
Yiming Xu
committed
3f18047
maybe toTmTm arguments wrong order...

Yiming Xu
authored and
Yiming Xu
committed
36a4982

Commits on Dec 19, 2025

problem on lime 1744

Yiming Xu
authored and
Yiming Xu
committed
7b0a9f7
constructing j

Yiming Xu
authored and
Yiming Xu
committed
3daafd3

Commits on Dec 20, 2025

snd proj eq

Yiming Xu
authored and
Yiming Xu
committed
37363a7
need another one or two proj eq

Yiming Xu
authored and
Yiming Xu
committed
e17c84a

Commits on Dec 21, 2025

toWeakpullback

Yiming Xu
authored and
Yiming Xu
committed
7a93277
HasPullbacks |-> HasPullback f g, j def

Yiming Xu
authored and
Yiming Xu
committed
1dddbd3

Commits on Dec 22, 2025

j_tp

Yiming Xu
authored and
Yiming Xu
committed
9bd374c

Commits on Jan 10, 2026

try to unify structured + unstructured motiveCtx etc API

Yiming Xu
authored and
Yiming Xu
committed
f97820a

Commits on Jan 11, 2026

feat:sec_substWk

Yiming Xu
authored and
Yiming Xu
committed
2baff38
backup before making A implicit

Yiming Xu
authored and
Yiming Xu
committed
e169bc7
backup before making A implicit

Yiming Xu
authored and
Yiming Xu
committed
15b9681
make argument A implicit

Yiming Xu
authored and
Yiming Xu
committed
cf12952
stupid long proof for structured reflSubst_comp_motiveSubst

Yiming Xu
authored and
Yiming Xu
committed
85c765d
get rid of using endpts

Yiming Xu
authored and
Yiming Xu
committed
c93a039
make things a bit shorter by using substCons

Yiming Xu
authored and
Yiming Xu
committed
d075a31
golf a bit

Yiming Xu
authored and
Yiming Xu
committed
a1ae95b

Commits on Jan 12, 2026

.
Jlh18
committed
a5d4f45
.
Jlh18
committed
5fe6b3d
.
Jlh18
committed
7b5ce38

Commits on Jan 13, 2026

feat: StructuredUniverse.Id.ofUnstructured
Jlh18
committed
581f091

Commits on Jan 14, 2026

feat: Id.ofUnstructured.j
Jlh18
committed
dca97c9
problem on line 1303

Yiming Xu
authored and
Yiming Xu
committed
425bae8

Commits on Mar 10, 2026

try to generalize the classifier to cats

Yiming Xu
authored and
Yiming Xu
committed
a829fc0