New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Computational M-types #1233
Merged
Merged
Computational M-types #1233
Changes from 58 commits
Commits
Show all changes
61 commits
Select commit
Hold shift + click to select a range
106800e
Start of Inductives.
LuisScoccola 5c000de
Modified travis and Makefile.
LuisScoccola 918e13c
Merged travis.
LuisScoccola 205f3c2
Added a bit on coalgebras, added polynomial functors.
LuisScoccola 77661cb
Trying to prove Lemma 5.1.8 in Felix's thesis.
LuisScoccola f6ebfab
Finished the proof of 5.1.8
LuisScoccola 73a69c2
Closer to proving that WHom'(W, C) is contractible for every C.
LuisScoccola 8d3d189
Proved that WHom'(W,C) is contractible for every C
LuisScoccola c4486e9
Proving WHom' is equivalent to WHom.
LuisScoccola 6f69d5b
Finished proof that W is an initial algebra.
LuisScoccola 7ca97ed
Fixed some typos.
LuisScoccola 7e46c64
Cleaning algebras.v a bit
LuisScoccola 5d51473
Cleaning addresses.v a bit
LuisScoccola 116c4d7
Construct M-types from nat
s9ferech eaeaa40
Make M-types indexed
s9ferech 2af232b
Extend M-types for judgmental computation rule
s9ferech 54b9d06
the base file with the project context
rmatthes 5182d39
WIP: Make W-types indexed
s9ferech 4353399
WIP: Define mu- and nu-containers
s9ferech 3f48ece
resolved conflicts
7dad77c
Merge branch 'LuisScoccola-master' into restorescoccolarech
ef9c646
most recent version of felix
d232b69
compiling version
39d8c34
epsilon
62c9fc3
my slides at the EUTYPES workshop in Nijmegen 2018 with comments on R…
rmatthes a68437a
Merge pull request #2 from unimath2019-ri/restorescoccolarech
dominik-kirst 91d228c
Merge branch 'dev' of https://github.com/unimath2019-ri/UniMath into dev
rmatthes cea58a0
Merge branch 'master' into dev
rmatthes 2417afc
independence of propositional resizing rule mentioned
rmatthes 80f406d
forgotten commenting of non-compiling code
rmatthes 26de029
Merge pull request #3 from unimath2019-ri/commentnoncompilingpart
rmatthes 8ce0ddf
Added missing statements from Felix without proof.
409da2c
Merge branch 'dev' of https://github.com/unimath2019-ri/UniMath into dev
c101d8d
Proof of Lemma 11 from Non-wellfounded trees.
2fd92b7
starting on ComputationalM.v
d0a9431
Merge branch 'dev' of https://github.com/unimath2019-ri/UniMath into dev
48f9819
minor improvements
rmatthes 3b9fbe2
Merge pull request #4 from unimath2019-ri/minorimprovementsoninductives
rmatthes e693b75
corecursive equation
dominik-kirst 27cf1ce
morphism equation and refactoring
dominik-kirst f46e0cf
carriers are equal
dominik-kirst 331188f
still working on equations
dominik-kirst 54c3deb
proved finality plus cleanup
dominik-kirst 00aa48b
inform makefile about ComputationalM.v, replace reflexivity by apply …
rmatthes 5f49e04
replaces some projections by accessors (very shallow contribution)
rmatthes e48805d
Merge branch 'master' into computationalM
rmatthes 3882ba9
shallow changes to reestablish compilation
rmatthes 78858b7
wip on establishing isprop for the crucial property P
rmatthes 242397f
fills the gaps in the development: P proven a proposition, fine-tunin…
rmatthes 94893bd
epsilon
dominik-kirst e771582
delta
dominik-kirst ade382c
Merge branch 'master' into computationalM
rmatthes b55caed
corrects a left-over from the merge process
rmatthes 5912b8a
some cleanup
rmatthes af3c4cd
erased remaining two upstream lemmas
dominik-kirst 8a00fc4
modifies list of authors after email exchange with Dominik
rmatthes 2473613
leaves out material on which project work at UniMathSchool 2019 was b…
rmatthes 6e37919
tiny changes to minimize number of modified files in PR
rmatthes 5d19115
description of PR integrated into introductory comments
rmatthes f6af06a
Defined replaces Qed everywhere, except for the lemma proved by idpath
rmatthes efb26ef
last Qed turned into Defined
rmatthes File filter
Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -7,3 +7,4 @@ W/Fibered.v | |
W/Naturals.v | ||
W/Uniqueness.v | ||
M/Chains.v | ||
M/ComputationalM.v |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,300 @@ | ||
(** ** Refinement of M-types | ||
|
||
M-types can be refined to satisfy the right definitional equalities. | ||
This idea is from Felix Rech's Bachelor's thesis, and Felix | ||
Rech also developed together with Luis Scoccola a first formalization | ||
in UniMath as project work of the UniMath 2017 school. The present | ||
formalization was obtained as project work of the UniMath 2019 school | ||
and is heavily inspired by that former formalization. | ||
|
||
Author: Dominik Kirst (@dominik-kirst) and Ralph Matthes (@rmatthes) | ||
|
||
*) | ||
|
||
Require Import UniMath.Foundations.All. | ||
Require Import UniMath.MoreFoundations.All. | ||
|
||
Require Import UniMath.CategoryTheory.Core.Categories. | ||
Require Import UniMath.CategoryTheory.Core.Functors. | ||
Require Import UniMath.CategoryTheory.FunctorCoalgebras. | ||
Require Import UniMath.CategoryTheory.categories.Type.Core. | ||
|
||
Require Import UniMath.Induction.PolynomialFunctors. | ||
Require Import UniMath.Induction.M.Core. | ||
Require Import UniMath.Induction.M.Uniqueness. | ||
|
||
Section Refinement. | ||
|
||
Context (A : UU). | ||
Context (B : A → UU). | ||
Local Notation F := (polynomial_functor A B). | ||
|
||
Variable M0 : coalgebra F. | ||
Local Notation carrierM0 := (coalgebra_ob _ M0). | ||
Local Notation destrM0 := (coalgebra_mor _ M0). | ||
|
||
Variable finalM0 : is_final M0. | ||
Local Notation corecM0 C := (pr11 (finalM0 C)). | ||
|
||
Local Open Scope cat. | ||
Local Open Scope functions. | ||
|
||
(* Refinement of the final coalgebra to computable elements *) | ||
|
||
Definition carrierM := ∑ m0 : carrierM0, ∃ C c, corecM0 C c = m0. | ||
|
||
(* Definition of the corecursor *) | ||
|
||
Definition corecM (C : coalgebra F) (c : coalgebra_ob _ C) : carrierM. | ||
Proof. | ||
exists (corecM0 C c). apply hinhpr. exists C, c. apply idpath. | ||
Defined. | ||
|
||
(* Definition of a proposition we factor the computation through *) | ||
|
||
Local Definition P (m0 : carrierM0) := | ||
∑ af : F carrierM, destrM0 m0 = # F pr1 af. | ||
|
||
(** in order to show [P] to be a proposition, a not obviously equivalent | ||
formulation is given for which it is easy to show [isaprop] *) | ||
Local Definition P' (m0 : carrierM0) := | ||
∑ ap : ∑ a : A, pr1 (destrM0 m0) = a, | ||
∏ (b : B (pr1 ap)), | ||
∑ mp : ∑ m0' : carrierM0, | ||
transportf (λ a, B a -> carrierM0) | ||
(pr2 ap) | ||
(pr2 (destrM0 m0)) b = | ||
m0', | ||
∃ C c, corecM0 C c = pr1 mp. | ||
|
||
(** the easy auxiliary lemma *) | ||
Local Lemma P'_isaprop m0 : | ||
isaprop (P' m0). | ||
Proof. | ||
apply isofhleveltotal2. | ||
- apply isofhlevelcontr. | ||
apply iscontrcoconusfromt. | ||
- intro ap; induction ap as [a p]. | ||
apply impred; intros b. | ||
apply isofhleveltotal2. | ||
+ apply isofhlevelcontr. | ||
apply iscontrcoconusfromt. | ||
+ intro mp; induction mp as [m0' q]. | ||
apply isapropishinh. | ||
Qed. | ||
|
||
(** the crucial lemma *) | ||
Local Lemma P_isaprop (m0 : carrierM0) : | ||
isaprop (P m0). | ||
Proof. | ||
use (@isofhlevelweqb _ _ (P' m0) _ (P'_isaprop m0)). | ||
simple refine (weqcomp (weqtotal2asstor _ _) _). | ||
simple refine (weqcomp _ (invweq (weqtotal2asstor _ _))). | ||
apply weqfibtototal; intro a. | ||
intermediate_weq ( | ||
∑ f : B a → carrierM, | ||
∑ p : pr1 (destrM0 m0) = a, | ||
transportf | ||
(λ a, B a -> carrierM0) | ||
p | ||
(pr2 (destrM0 m0)) = | ||
pr1 ∘ f). | ||
{ | ||
apply weqfibtototal; intro f. | ||
apply total2_paths_equiv. | ||
} | ||
intermediate_weq (∑ p : pr1 (destrM0 m0) = a, | ||
∑ f : B a → carrierM, | ||
transportf | ||
(λ a, B a → carrierM0) | ||
p | ||
(pr2 (destrM0 m0)) = | ||
pr1 ∘ f). | ||
{ apply weqtotal2comm. } | ||
apply weqfibtototal; intro p. | ||
intermediate_weq (∑ fg : ∑ f : B a -> carrierM0, | ||
∏ b, ∃ C c, corecM0 C c = f b, | ||
transportf | ||
(λ a, B a -> carrierM0) | ||
p | ||
(pr2 (destrM0 m0)) = | ||
pr1 fg). | ||
{ use weqbandf. | ||
- apply weqfuntototaltototal. | ||
- cbn. | ||
intro f. | ||
apply idweq. | ||
} | ||
intermediate_weq (∑ f : B a → carrierM0, | ||
∑ _ : ∏ b, ∃ C c, corecM0 C c = f b, | ||
transportf | ||
(λ a, B a → carrierM0) | ||
p | ||
(pr2 (destrM0 m0)) = | ||
f). | ||
{ apply weqtotal2asstor. } | ||
intermediate_weq (∑ f : B a → carrierM0, | ||
∑ _ : ∏ b, ∃ C c, corecM0 C c = f b, | ||
∏ b, transportf | ||
(λ a, B a → carrierM0) | ||
p | ||
(pr2 (destrM0 m0)) b = | ||
f b). | ||
{ apply weqfibtototal; intro f. | ||
apply weqfibtototal; intros _. | ||
apply weqtoforallpaths. | ||
} | ||
intermediate_weq (∑ f : B a → carrierM0, | ||
∏ b, ∑ _ : ∃ C c, corecM0 C c = f b, | ||
transportf | ||
(λ a, B a → carrierM0) | ||
p | ||
(pr2 (destrM0 m0)) b = | ||
f b). | ||
{ apply weqfibtototal; intro f. | ||
apply invweq. | ||
apply weqforalltototal. | ||
} | ||
intermediate_weq (∏ b, ∑ m0' : carrierM0, | ||
∑ _ : ∃ C c, corecM0 C c = m0', | ||
transportf | ||
(λ a, B a -> carrierM0) | ||
p | ||
(pr2 (destrM0 m0)) b = | ||
m0'). | ||
{ apply invweq. | ||
apply weqforalltototal. | ||
} | ||
apply weqonsecfibers; intro b. | ||
intermediate_weq (∑ m0' : carrierM0, | ||
∑ _ : transportf | ||
(λ a, B a -> carrierM0) | ||
p | ||
(pr2 (destrM0 m0)) b = | ||
m0', | ||
∃ C c, corecM0 C c = m0'). | ||
{ | ||
apply weqfibtototal; intro m0'. | ||
apply weqdirprodcomm. | ||
} | ||
intermediate_weq (∑ mp : ∑ m0', transportf (λ a, B a → carrierM0) p | ||
(pr2 (destrM0 m0)) b = m0', | ||
∃ C c, corecM0 C c = pr1 mp). | ||
{ | ||
apply invweq. | ||
apply weqtotal2asstor. | ||
} | ||
use weqbandf. | ||
- apply weqfibtototal; intro m0'. | ||
apply idweq. | ||
- cbn. intro mp. | ||
apply idweq. | ||
Qed. | ||
|
||
(* Now the destructor of M can be defined *) | ||
|
||
Local Definition destrM' (m : carrierM) : P (pr1 m). | ||
Proof. | ||
induction m as [m0 H]. apply (squash_to_prop H); try apply P_isaprop. | ||
intros [C [c H1]]. | ||
refine ((# F (corecM C) ∘ (pr2 C)) c,, _). cbn [pr1]. clear H. | ||
assert (H : is_coalgebra_homo F (corecM0 C)). | ||
{ destruct finalM0 as [[G H] H']. apply H. } | ||
apply toforallpaths in H. | ||
apply pathsinv0. | ||
intermediate_path (destrM0 (corecM0 C c)). | ||
- apply H. | ||
- apply maponpaths. assumption. | ||
Defined. | ||
|
||
Definition destrM (m : carrierM) : F carrierM := | ||
pr1 (destrM' m). | ||
|
||
Definition M : coalgebra F := | ||
(carrierM,, destrM). | ||
|
||
(* The destructor satisfies the corecursion equation definitionally *) | ||
|
||
Lemma corec_computation C c : | ||
destrM (corecM C c) = # F (corecM C) (pr2 C c). | ||
Proof. | ||
apply idpath. | ||
Qed. | ||
|
||
(* The two carriers are equal *) | ||
|
||
Lemma eq_corecM0 m0 : | ||
corecM0 M0 m0 = m0. | ||
Proof. | ||
induction finalM0 as [[G H1] H2]. cbn. | ||
specialize (H2 (coalgebra_homo_id F M0)). | ||
change (pr1 (G,, H1) m0 = pr1 (coalgebra_homo_id F M0) m0). | ||
apply (maponpaths (fun X => pr1 X m0)). | ||
apply pathsinv0. | ||
assumption. | ||
Qed. | ||
|
||
Definition injectM0 m0 : | ||
∃ C c, corecM0 C c = m0. | ||
Proof. | ||
apply hinhpr. exists M0, m0. apply eq_corecM0. | ||
Defined. | ||
|
||
Lemma carriers_weq : | ||
carrierM ≃ carrierM0. | ||
Proof. | ||
apply (weq_iso pr1 (λ m0, m0,, injectM0 m0)). | ||
- intros [m H]. cbn. apply maponpaths, ishinh_irrel. | ||
- intros x. cbn. apply idpath. | ||
Defined. | ||
|
||
Lemma carriers_eq : | ||
carrierM = carrierM0. | ||
Proof. | ||
apply weqtopaths, carriers_weq. | ||
Defined. (** needs to be transparent *) | ||
|
||
(* The two coalgebras are equal *) | ||
|
||
Local Lemma eq1 (m0 : carrierM0) : | ||
transportf (λ X, X → F X) carriers_eq destrM m0 | ||
= transportf (λ X, F X) carriers_eq (destrM (transportf (λ X, X) (!carriers_eq) m0)). | ||
Proof. | ||
destruct carriers_eq. apply idpath. | ||
Qed. | ||
|
||
Local Lemma eq2 (m0 : carrierM0) : | ||
transportf (λ X, X) (!carriers_eq) m0 = m0,, injectM0 m0. | ||
Proof. | ||
apply (transportf_pathsinv0' (idfun UU) carriers_eq). | ||
unfold carriers_eq. rewrite weqpath_transport. apply idpath. | ||
Qed. | ||
|
||
Local Lemma eq3 m0 : | ||
destrM (m0,, injectM0 m0) = pr1 (destrM0 m0),, corecM M0 ∘ pr2 (destrM0 m0). | ||
Proof. | ||
apply idpath. | ||
Qed. | ||
|
||
Lemma coalgebras_eq : | ||
M = M0. | ||
Proof. | ||
use total2_paths_f; try apply carriers_eq. | ||
apply funextfun. intro m0. | ||
rewrite eq1. rewrite eq2. rewrite eq3. | ||
cbn. unfold polynomial_functor_obj. | ||
rewrite transportf_total2_const. | ||
use total2_paths_f; try apply idpath. | ||
cbn. apply funextsec. intros b. rewrite <- helper_A. | ||
unfold carriers_eq. rewrite weqpath_transport. | ||
cbn. rewrite eq_corecM0. apply idpath. | ||
Qed. | ||
|
||
(* Thus M is final *) | ||
|
||
Lemma finalM : is_final M. | ||
Proof. | ||
rewrite coalgebras_eq. apply finalM0. | ||
Defined. | ||
|
||
End Refinement. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Would it be better to use
Defined.
here?