Skip to content

Instantly share code, notes, and snippets.

@takanuva
Created August 1, 2018 17:01
Show Gist options
  • Save takanuva/e89aefa8d1b7bad3e494a353c8121e79 to your computer and use it in GitHub Desktop.
Save takanuva/e89aefa8d1b7bad3e494a353c8121e79 to your computer and use it in GitHub Desktop.
Admissibility of strong projections
(*
Prove that, due to the free theorem for impredicative sigma types, strong
projection is a valid extension. Based on Dan Doel's Agda version:
https://hub.darcs.net/dolio/agda-share/browse/ParamInduction.agda.
*)
Definition Rel (A: Prop) (B: Prop) :=
A -> B -> Prop.
Definition Sigma (T: Prop) (U: T -> Prop): Prop :=
forall Y: Prop, (forall t: T, U t -> Y) -> Y.
Notation "'∑' '(' a : A ')' . b" := (Sigma A (fun a => b))
(at level 200, a ident, right associativity,
format "'∑' '(' a : A ')' . b").
Definition Pair (T: Prop) (U: T -> Prop) (t: T) (u: U t): Sigma T U :=
fun _ f =>
f t u.
Notation "'(' a , b ')'" := (Pair _ _ a b).
Axiom free:
forall {A: Prop} {P: A -> Prop} (C D: Prop),
forall R1: Rel A A,
forall R2: (forall x0 x1, R1 x0 x1 -> Rel (P x0) (P x1)),
forall R3: Rel C D,
forall p: Sigma A P,
forall k0: (forall x: A, P x -> C),
forall k1: (forall x: A, P x -> D),
(forall x0 x1, forall r: R1 x0 x1,
forall w0: P x0, forall w1: P x1,
R2 x0 x1 r w0 w1 -> R3 (k0 x0 w0) (k1 x1 w1)) ->
R3 (p C k0) (p D k1).
Lemma l0:
forall {A P},
forall p: Sigma A P,
p (Sigma A P) (Pair A P) = p.
Proof.
intros.
eapply free with (R1 := eq).
exact p.
intros.
exact p.
intros.
exact p.
intros.
eapply H.
Qed.
Lemma l1:
forall {A P},
forall p: Sigma A P,
Sigma A (fun x => Sigma (P x) (fun w => p = Pair A P x w)).
Proof.
intros.
destruct (l0 p).
eapply free with (R1 := eq).
exact p.
intros.
exact p.
intros.
exact p.
intros.
eapply H.
Qed.
Lemma uncurry:
forall {A P},
forall (C: Sigma A P -> Prop),
forall f: (forall x: A, forall w: P x, C (x, w)),
forall p: Sigma A P,
C p.
Proof.
intros.
eapply (l1 p).
intros.
eapply H.
intros.
destruct (eq_sym H0).
apply f.
Qed.
Theorem pi1:
forall {A P},
Sigma A P -> A.
Proof.
intros.
eapply H.
intros.
exact t.
Defined.
Theorem pi2:
forall {A P},
forall p: Sigma A P,
P (pi1 p).
Proof.
intros.
eapply uncurry with (C := fun q => P (pi1 q)).
intros.
exact w.
Defined.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment