text:
(* -*- coq-prog-args: ("-emacs-U" "-R" "../.." "FingerTree" "-R" "../../../../safe" "Safe" "-R" "../../../../monads" "Monad") -*- *)
Require Import FingerTree.DependentFingerTreeModule.
Require Import FingerTree.FingerTreeModule.
Require Import FingerTree.RopeModule.
Require Import Coq.Program.Program.

(* Unboxing of tuples. *)
Extract Inductive prod => "(*)"  [ "(,)" ].
Extract Inductive sigT => "(*)" [ " " ].

(* sumbools are bools *)
Require Import Sumbool.
Extract Inductive sumbool => "bool" [ "true" "false" ].
Extract Inductive bool => "bool" [ "true" "false" ].
Extraction Inline sumbool_of_bool.
Extraction Inline bool_of_sumbool.

(* Fine tune inlining *)
Extraction Inline eq_rect.
Unset Extraction AutoInline.

Recursive Extraction Library FingerTreeModule.
Recursive Extraction Library RopeModule.

author: coq-contribs

repo: finger-tree


text:
(** * Extensionality and Univalence *)

From Coq Require Import
  Logic.FunctionalExtensionality Logic.ProofIrrelevance
  Logic.PropExtensionality Logic.PropExtensionalityFacts.
From DEZ.Is Require Export
  Irrelevant Isomorphic.

(** We declare various axiom schemes as classes
    in hopes of one day turning them into theorems. *)

Theorem ac (A B : Type) (R : A -> B -> Prop)
  (g : forall x : A, {y : B | R x y}) :
  {f : A -> B | forall x : A, R x (f x)}.
Proof.
  exists (fun x : A => proj1_sig (g x)).
  intros x. set (p := g x). induction p as [y p]. cbn. apply p.
Defined.

Theorem dpb (A B : Type) (R : A -> B -> Prop)
  (s : {f : A -> B | forall x : A, R x (f x)}) (x : A) :
  {y : B | R x y}.
Proof.
  induction s as [f g]. exists (f x). apply (g x).
Defined.

(** This is lemma 2.15.6 from the book. *)

Theorem ac_eq (A : Type) (P : A -> Type) (R : forall x : A, P x -> Prop)
  (f : forall x : A, {a : P x | R x a}) :
  {g : forall x : A, P x | forall x : A, R x (g x)}.
Proof.
  exists (fun x : A => proj1_sig (f x)). intros x. set (f x) as y.
  destruct y as [a s]. apply s.
Defined.

Theorem ac_eq_ex (A : Type) (P : A -> Prop) (R : forall x : A, P x -> Prop)
  (f : forall x : A, exists a : P x, R x a) :
  exists g : forall x : A, P x, forall x : A, R x (g x).
Proof.
  exists (fun x : A => ex_proj1 (f x)). intros x. set (f x) as y.
  destruct y as [a s]. apply s.
Defined.

(** This is part of theorem 2.15.7 from the book. *)

Theorem dbp_eq (A : Type) (P : A -> Type) (R : forall x : A, P x -> Prop)
  (s : {g : forall x : A, P x | forall x : A, R x (g x)}) (x : A) :
  {a : P x | R x a}.
Proof.
  destruct s as [g f]. exists (g x). apply (f x).
Defined.

Theorem dbp_eq_ex (A : Type) (P : A -> Prop) (R : forall x : A, P x -> Prop)
  (s : exists g : forall x : A, P x, forall x : A, R x (g x)) (x : A) :
  exists a : P x, R x a.
Proof.
  destruct s as [g f]. exists (g x). apply (f x).
Defined.

(** TODO Clean up this mess. *)

Reserved Notation "x '_*'" (left associativity, at level 20).
Reserved Notation "x '~=' y" (no associativity, at level 70).

(** This is lemma 2.3.1 from the book. *)

Definition transport (A : Type) (P : A -> Type)
  (x y : A) (e : x = y) (a : P x) : P y.
Proof.
  induction e. apply a.
Defined.

Definition transport_dep
  (A : Type) (P : A -> Type) (Q : forall x : A, P x -> Type)
  {x y : A} (e : x = y) (p : P x) (q : Q x p) :
  Q y (transport P e p).
Proof.
  destruct e. apply q.
Defined.

#[local] Notation "'_*_'" := (transport _) (only parsing).
#[local] Notation "e '_*'" := (transport _ e) (only parsing).

(** This is lemma 2.2.1 from the book. *)

Lemma ap (A B : Type) (f : A -> B) (x y : A) (e : x = y) : f x = f y.
Proof.
  apply (transport (fun y : A => f x = f y) e). apply id%type.
Defined.

(** This is lemma 2.3.4 from the book. *)

Lemma apd (A : Type) (P : A -> Type)
  (f : forall x : A, P x) (x y : A) (e : x = y) :
  e _* (f x) = f y.
Proof.
  destruct e. apply id%type.
Defined.

Section Context.

Context (A B C : Type)
  (f : A -> B) (g : B -> C) (x y z : A) (e : x = y) (d : y = z).

#[local] Open Scope type_scope.

(** This is lemma 2.2.1 from the book. *)

Lemma ap_refl : ap (y := x) f id = id.
Proof. clear. apply id%type. Defined.

(** This is lemma 2.2.2 from the book. *)

Lemma ap_id : ap id%core e = e.
Proof. clear. destruct e. apply id%type. Defined.

Lemma ap_ap : ap g (ap f e) = ap (g o f)%core e.
Proof. clear. destruct e. apply id%type. Defined.

Lemma ap_sym : ap f (e ^-1) = ap f e ^-1.
Proof. clear. destruct e. apply id%type. Defined.

Lemma ap_trans : ap f (d o e) = ap f d o ap f e.
Proof. clear. destruct d. destruct e. apply id%type. Defined.

End Context.

Lemma happly_nondep (A B : Type) (f g : A -> B) (e : f = g) (x : A) : f x = g x.
Proof.
  apply (transport (fun h : A -> B => f x = h x) e). apply id%type.
Defined.

Lemma happly (A : Type) (P : A -> Type)
  (f g : forall x : A, P x) (e : f = g) (x : A) : f x = g x.
Proof.
  apply (transport (fun h : forall x : A, P x => f x = h x) e). apply id%type.
Defined.

Arguments happly {_ _} _ _ _ _.

Class HasEquivTypesEq (A B : Type) : Type :=
  equiv_types_eq_is_equiv_types :> HasEquivTypes A B _=_ _=_.

#[local] Notation "'_~=_'" := HasEquivTypesEq.
#[local] Notation "A '~=' B" := (HasEquivTypesEq A B).

Definition transport_refl (A : Type) (P : A -> Type) (x : A) (a : P x) :
  transport P id%type a = a.
Proof. apply id%type. Defined.

(** This is lemma 2.3.9 from the book. *)

Definition transport_trans (A : Type) (P : A -> Type)
  (x y z : A) (e : x = y) (f : y = z) (a : P x) :
  (* f _* (e _* a) = (f o e)%type _* a *)
  transport P f (transport P e a) = transport P (f o e)%type a.
Proof.
  destruct e, f. apply id%type.
Defined.

(** This is lemma 2.3.10 from the book. *)

Definition transport_ap (A B : Type) (P : B -> Type)
  (f : A -> B) (x y : A) (e : x = y) (a : P (f x)) :
  transport P (ap f e) a = transport (P o f) e a.
Proof.
  destruct e. apply id%type.
Defined.

(** This is lemma 2.3.11 from the book. *)

Definition transport_f (A : Type) (P Q : A -> Type)
  (f : forall x : A, P x -> Q x) (x y : A) (e : x = y) (a : P x) :
  transport Q e (f x a) = f y (transport P e a).
Proof.
  destruct e. apply id%type.
Defined.

(** This is part of theorem 2.15.7 from the book. *)

Theorem do_not_need_this (A : Type) (P : A -> Type) (R : forall x : A, P x -> Prop) :
  HasLInv _=_ _=_ (@ac_eq A P R).
Proof.
  exists (@dbp_eq A P R). split.
  - typeclasses eauto.
  - typeclasses eauto.
  - intros f. apply functional_extensionality_dep.
    intros x. destruct (f x) as [a s] eqn : e. cbn. rewrite e. reflexivity.
Defined.

Theorem do_not_need_this_ex (A : Type) (P : A -> Prop) (R : forall x : A, P x -> Prop) :
  HasLInv _=_ _=_ (@ac_eq_ex A P R).
Proof.
  exists (@dbp_eq_ex A P R). split.
  - typeclasses eauto.
  - typeclasses eauto.
  - intros f. apply functional_extensionality_dep.
    intros x. destruct (f x) as [a s] eqn : e. cbn. rewrite e. reflexivity.
Defined.

Theorem need_this (A : Type) (P : A -> Type) (R : forall x : A, P x -> Prop) :
  HasRInv _=_ _=_ (@ac_eq A P R).
Proof.
  exists (@dbp_eq A P R). split.
  - typeclasses eauto.
  - typeclasses eauto.
  - intros [g f]. reflexivity.
Defined.

Theorem need_this_ex (A : Type) (P : A -> Prop) (R : forall x : A, P x -> Prop) :
  HasRInv _=_ _=_ (@ac_eq_ex A P R).
Proof.
  exists (@dbp_eq_ex A P R). split.
  - typeclasses eauto.
  - typeclasses eauto.
  - intros [g f]. reflexivity.
Defined.

(** This is theorem 2.15.7 from the book. *)

Theorem this_is_equiv (A : Type) (P : A -> Type) (R : forall x : A, P x -> Prop) :
  HasBiInv _=_ _=_ (@ac_eq A P R).
Proof.
  split.
  - apply do_not_need_this.
  - apply need_this.
Defined.

Theorem this_is_equiv_ex (A : Type) (P : A -> Prop) (R : forall x : A, P x -> Prop) :
  HasBiInv _=_ _=_ (@ac_eq_ex A P R).
Proof.
  split.
  - apply do_not_need_this_ex.
  - apply need_this_ex.
Defined.

Theorem seriously (A : Type) (P : A -> Type) (R : forall x : A, P x -> Prop) :
  (forall x : A, {a : P x | R x a}) ~=
  {g : forall x : A, P x | forall x : A, R x (g x)}.
Proof. exists ac_eq. apply this_is_equiv. Defined.

Theorem seriously_ex (A : Type) (P : A -> Prop) (R : forall x : A, P x -> Prop) :
  (forall x : A, exists a : P x, R x a) ~=
  exists g : forall x : A, P x, forall x : A, R x (g x).
Proof. exists ac_eq_ex. apply this_is_equiv_ex. Defined.

(** We define these instances as explicitly as possible,
    because they are used in the univalence axiom. *)

(** ** Properties of Equality *)

#[export] Instance is_proper_eq_0 (B : Type) (x : B) :
  IsProper _=_ x.
Proof. apply id%type. Defined.

#[export] Instance is_proper_eq_1 (A B : Type) (f : A -> B) :
  IsProper (_=_ ==> _=_) f.
Proof. intros x y a. induction a. apply id%type. Defined.

#[export] Instance is_proper_eq_2 (A0 A1 B : Type) (k : A0 -> A1 -> B) :
  IsProper (_=_ ==> _=_ ==> _=_) k.
Proof.
  intros x0 y0 a0 x1 y1 a1. induction a0. induction a1. apply id%type.
Defined.

(** ** Properties of the Identity Function *)

Section Context.

Context (A : Type).

#[export] Instance is_retr_eq_id :
  IsRetr (A := A) _=_ id id.
Proof. intros x. apply id%type. Defined.

#[export] Instance is_sect_eq_id :
  IsSect (A := A) _=_ id id.
Proof. intros x. apply id%type. Defined.

#[export] Instance is_iso_l_eq_id :
  IsIsoL (A := A) (B := A) _=_ _=_ id id.
Proof.
  split.
  - apply is_proper_eq_1.
  - apply is_proper_eq_1.
  - apply is_retr_eq_id.
Defined.

#[export] Instance is_iso_r_eq_id :
  IsIsoR (A := A) (B := A) _=_ _=_ id id.
Proof.
  split.
  - apply is_proper_eq_1.
  - apply is_proper_eq_1.
  - apply is_sect_eq_id.
Defined.

#[export] Instance has_bi_inv_eq_id :
  HasBiInv (A := A) (B := A) _=_ _=_ id.
Proof.
  split.
  - exists id. apply is_iso_l_eq_id.
  - exists id. apply is_iso_r_eq_id.
Defined.

#[export] Instance has_equiv_types_eq : A ~= A.
Proof. exists id. apply has_bi_inv_eq_id. Defined.

End Context.

(** ** Properties of Transport *)

Section Context.

Context (A B : Type) (e : A = B).

#[export] Instance is_retr_eq_transport_id :
  IsRetr _=_ (transport id e) (transport id (e ^-1)).
Proof. intros x. destruct e. apply id%type. Defined.

#[export] Instance is_sect_eq_transport_id :
  IsSect _=_ (transport id e) (transport id (e ^-1)).
Proof. intros x. destruct e. apply id%type. Defined.

#[export] Instance is_iso_l_eq_transport_id :
  IsIsoL _=_ _=_ (transport id e) (transport id (e ^-1)).
Proof.
  split.
  - apply is_proper_eq_1.
  - apply is_proper_eq_1.
  - apply is_retr_eq_transport_id.
Defined.

#[export] Instance is_iso_r_eq_transport_id :
  IsIsoR _=_ _=_ (transport id e) (transport id (e ^-1)).
Proof.
  split.
  - apply is_proper_eq_1.
  - apply is_proper_eq_1.
  - apply is_sect_eq_transport_id.
Defined.

#[export] Instance has_bi_inv_eq_transport_id :
  HasBiInv _=_ _=_ (transport id e).
Proof.
  split.
  - exists (transport id (e ^-1)). apply is_iso_l_eq_transport_id.
  - exists (transport id (e ^-1)). apply is_iso_r_eq_transport_id.
Defined.

#[export] Instance idtoeqv : A ~= B.
Proof. exists (transport id e). apply has_bi_inv_eq_transport_id. Defined.

End Context.

#[export] Instance refl :
  forall A : Type, A ~= A.
Proof. intros A. apply has_equiv_types_eq. Defined.

#[export] Instance sym :
  forall A B : Type, A ~= B -> B ~= A.
Proof.
  intros A B [f [[g IIL] [h IIR]]].
  exists (g o f o h). split.
  - exists f. split.
    + apply is_proper_eq_1.
    + apply is_proper_eq_1.
    + intros y. unfold compose.
      pose proof retr (f := f) (g := g) (h y) as r.
      pose proof sect (f := f) (g := h) y as s.
      pose proof is_proper_eq_1 f r as p.
      apply (s o p)%type.
  - exists f. split.
    + apply is_proper_eq_1.
    + apply is_proper_eq_1.
    + intros x. unfold compose.
      pose proof sect (f := f) (g := h) (f x) as s.
      pose proof is_proper_eq_1 g s as p.
      pose proof retr (f := f) (g := g) x as r.
      apply (r o p)%type.
Defined.

#[export] Instance trans :
  forall A B C : Type, A ~= B -> B ~= C -> A ~= C.
Proof.
  intros A B C [f [[g IILf] [h IIRf]]] [i [[j IILi] [k IIRi]]].
  exists (i o f). split.
  - exists (g o j). split.
    + apply is_proper_eq_1.
    + apply is_proper_eq_1.
    + intros y. unfold compose.
      pose proof retr (f := i) (g := j) (f y) as ri.
      pose proof is_proper_eq_1 g ri as pi.
      pose proof retr (f := f) (g := g) y as rf.
      apply (rf o pi)%type.
  - exists (h o k). split.
    + apply is_proper_eq_1.
    + apply is_proper_eq_1.
    + intros y. unfold compose.
      pose proof sect (f := f) (g := h) (k y) as sf.
      pose proof is_proper_eq_1 i sf as pf.
      pose proof sect (f := i) (g := k) y as si.
      apply (si o pf)%type.
Defined.

Arguments refl _ : clear implicits.
Arguments sym _ _ _ : clear implicits.
Arguments trans _ _ _ _ _ : clear implicits.

Lemma idtoeqv_refl (A : Type) :
  idtoeqv id%type = refl A.
Proof. reflexivity. Defined.

Lemma idtoeqv_sym (A B : Type) (e : A = B) :
  idtoeqv (e ^-1) = sym A B (idtoeqv e).
Proof. destruct e. reflexivity. Defined.

Lemma idtoeqv_trans (A B C : Type) (e : A = B) (f : B = C) :
  idtoeqv (f o e)%type = trans A B C (idtoeqv e) (idtoeqv f).
Proof. destruct e. destruct f. reflexivity. Defined.

(** One of these ways is probably better. *)

Definition has_equiv_transport (A : Type) (P : A -> Type)
  (x y : A) (e : x = y) : P x ~= P y.
Proof. destruct e. apply idtoeqv. apply id%type. Defined.

Definition has_equiv_transport' (A : Type) (P : A -> Type)
  (x y : A) (e : x = y) : P x ~= P y.
Proof.
  exists (transport P e). split.
  - exists (transport P (e ^-1)). split.
    + typeclasses eauto.
    + typeclasses eauto.
    + intros a.
      pose proof transport_trans P e (e ^-1) a as f.
      pose proof eq_trans_sym_inv_r e as g.
      apply (transport (fun b : P _ => b = a) (f ^-1)).
      apply (transport (fun b : _ = _ => transport P b a = a) (g ^-1)).
      apply transport_refl.
  - exists (transport P (e ^-1)). split.
    + typeclasses eauto.
    + typeclasses eauto.
    + intros a.
      pose proof transport_trans P (e ^-1) e a as f.
      pose proof eq_trans_sym_inv_l e as g.
      apply (transport (fun b : P _ => b = a) (f ^-1)).
      apply (transport (fun b : _ = _ => transport P b a = a) (g ^-1)).
      apply transport_refl.
Defined.

(** This is equation 2.6.1 from the book. *)

Lemma prod_go (A B : Type)
  (a b : A * B) (e : a = b) : (fst a = fst b) * (snd a = snd b).
Proof.
  destruct a as [x y], b as [x' y'].
  pose proof ap fst e as f. apply (_,_).
  - apply f.
  - pose proof ap snd e as g. apply g.
Defined.

(** This is equation 2.6.3 from the book. *)

Lemma prod_come (A B : Type)
  (a b : A * B) (c : (fst a = fst b) * (snd a = snd b)) : a = b.
Proof.
  destruct c as [f g].
  destruct a as [x y], b as [x' y'].
  pose proof transport (fun x' : A => (x, y) = (x', y')) f as a. apply a.
  pose proof transport (fun y' : B => (x, y) = (x, y')) g as b. apply b.
  apply id%type.
Defined.

(** This is theorem 2.6.2 from the book. *)

#[export] Instance prod_has_bi_inv (A B : Type) (a b : A * B) :
  HasBiInv _=_ _=_ (prod_go (a := a) (b := b)).
Proof.
  split.
  - exists (prod_come a b). split.
    + apply is_proper_eq_1.
    + apply is_proper_eq_1.
    + intros e. destruct e. destruct a as [x y]. reflexivity.
  - exists (prod_come a b). split.
    + apply is_proper_eq_1.
    + apply is_proper_eq_1.
    + destruct a as [x y], b as [x' y']. intros [e f]. cbv in e, f.
      destruct e. destruct f. reflexivity.
Defined.

#[export] Instance prod_has_equiv_types (A B : Type) (a b : A * B) :
  (a = b) ~= (fst a = fst b) * (snd a = snd b).
Proof. exists prod_go. typeclasses eauto. Defined.

Equations prod_family (A : Type) (P Q : A -> Type) (x : A) : Type :=
  prod_family P Q x := P x * Q x.

(** This is theorem 2.6.4 from the book. *)

Lemma transport_prod (A : Type) (P Q : A -> Type)
  (x y : A) (e : x = y) (a : P x * Q x) :
  transport (prod_family P Q) e a =
  (transport P e (fst a), transport Q e (snd a)).
Proof.
  destruct e. destruct a as [p q]. apply id%type.
Defined.

#[local] Open Scope sig_scope.

Lemma sig_go (A : Type) (P : A -> Prop)
  (a b : {x : A | P x}) (e : a = b) :
  {f : proj1_sig a = proj1_sig b | transport P f (proj2_sig a) = proj2_sig b}.
Proof.
  destruct a as [x p], b as [x' p'].
  pose (ap proj1_sig e) as f. cbn in *.
  pose proof apd (P := P o proj1_sig) proj2_sig e as g. cbn in *.
  exists f. rewrite <- transport_ap in g. apply g.
Defined.

Lemma sig_come (A : Type) (P : A -> Prop)
  (a b : {x : A | P x}) (c : {f : proj1_sig a = proj1_sig b |
  transport P f (proj2_sig a) = proj2_sig b}) : a = b.
Proof.
  destruct c as [f g].
  destruct a as [x p], b as [x' p'].
  cbn in *. destruct f. destruct g. apply id%type.
Defined.

(** This is theorem 2.7.2 from the book. *)

#[export] Instance sig_has_bi_inv (A : Type) (P : A -> Prop)
  (a b : {x : A | P x}) :
  HasBiInv _=_ _=_ (sig_go (a := a) (b := b)).
Proof.
  split.
  - exists (sig_come a b). split.
    + apply is_proper_eq_1.
    + apply is_proper_eq_1.
    + intros e. destruct e. destruct a as [x y]. reflexivity.
  - exists (sig_come a b). split.
    + apply is_proper_eq_1.
    + apply is_proper_eq_1.
    + destruct a as [x y], b as [x' y']. intros [e f]. cbv in e, f.
      destruct e. destruct f. reflexivity.
Defined.

#[export] Instance sig_has_equiv_types (A : Type) (P : A -> Prop)
  (a b : {x : A | P x}) :
  (a = b) ~= {f : proj1_sig a = proj1_sig b |
  transport P f (proj2_sig a) = proj2_sig b}.
Proof. exists sig_go. typeclasses eauto. Defined.

Equations sig_family (A : Type) (P : A -> Prop) (Q : {x : A | P x} -> Prop)
  (x : A) : Type :=
  sig_family Q x := {a : P x | Q (x; a)}.

Arguments sig_family {_} _ _ _.

(** This is theorem 2.7.4 from the book. *)

Lemma transport_sig (A : Type) (P : A -> Prop) (Q : {x : A | P x} -> Prop)
  (x y : A) (e : x = y) (a : {a : P x | Q (x; a)}) :
  transport (sig_family P Q) e a =
  (transport P e (proj1_sig a);
  transport_dep (sig_curry Q) e (proj1_sig a) (proj2_sig a)).
Proof.
  destruct e. destruct a as [p q]. apply id%type.
Defined.

(** ** Proposition Extensionality *)

Class IsPropExt : Prop :=
  prop_ext (A B : Prop) (a : A <-> B) : A = B.

(** This lemma gets its name from [ZifyClasses.eq_iff]. *)

Lemma eq_iff (A B : Prop) (a : A = B) : A <-> B.
Proof. induction a. reflexivity. Qed.

(** ** Proposition Extensionality for Types *)

Class IsPropExtType : Prop :=
  prop_ext_type (A B : Type) `{!IsProp A} `{!IsProp B}
  (a : (A -> B) * (B -> A)) : A = B.

(** ** Proposition Extensionality Axiom for Types *)

Axiom propositional_extensionality_type :
  forall (A B : Type) (p : forall x y : A, x = y) (q : forall x y : B, x = y)
  (a : (A -> B) * (B -> A)), A = B.

Lemma eq_iff_type (A B : Type) `{!IsProp A} `{!IsProp B}
  (a : A = B) : (A -> B) * (B -> A).
Proof. induction a. split; apply id. Defined.

(** ** Predicate Extensionality *)

Class IsPredExt : Prop :=
  pred_ext (A : Type) (P Q : A -> Prop) (a : forall x : A, P x <-> Q x) : P = Q.

(** ** Predicate Extensionality Axiom *)

Axiom predicate_extensionality :
  forall (A : Type) (P Q : A -> Prop)
  (a : forall x : A, P x <-> Q x), P = Q.

(** ** Function Extensionality *)

Class IsFunExt : Prop :=
  fun_ext (A B : Type) (f g : A -> B) (a : forall x : A, f x = g x) : f = g.

(** This lemma gets its name from [FunctionalExtensionality.equal_f]. *)

Lemma equal_f (A B : Type) (f g : A -> B) (a : f = g) (x : A) : f x = g x.
Proof. induction a. reflexivity. Qed.

(** ** Dependent Function Extensionality *)

Class IsFunExtDep : Prop :=
  fun_ext_dep (A : Type) (P : A -> Type)
  (f g : forall x : A, P x) (a : forall x : A, f x = g x) : f = g.

(** Dependent function extensionality implies function extensionality. *)

#[export] Instance fun_ext_dep_is_fun_ext
  `{!IsFunExtDep} : IsFunExt.
Proof. intros A B f g a. apply fun_ext_dep. intros x. apply a. Qed.

(** ** Type Extensionality *)

Class IsTypeExt : Prop :=
  type_ext (A B : Type) (f : A -> B) (g : B -> A)
  `{!IsRetr _=_ f g} `{!IsSect _=_ f g} : A = B.

(** ** Type Extensionality Axiom *)

Axiom type_extensionality : forall (A B : Type)
 (f : A -> B) (g : B -> A)
 (r : forall x : A, g (f x) = x) (s : forall y : B, f (g y) = y),
 A = B.

(** ** Univalence *)

Class IsUniv : Type :=
  univ_has_bi_inv (A B : Type) :> HasBiInv _=_ _=_ (idtoeqv (A := A) (B := B)).

(** ** Univalence Axiom *)

Axiom univalence : forall A B : Type,
  HasBiInv _=_ _=_ (idtoeqv (A := A) (B := B)).

(** This is axiom 2.10.3 and its corollaries from the book. *)

Corollary ua_equiv `{IsUniv} (A B : Type) : (A = B) ~= (A ~= B).
Proof. exists idtoeqv. typeclasses eauto. Defined.

(*
Lemma ua `{IsUniv} (A B : Type) `{!A ~= B} : A = B.
Proof.
  pose proof equiv_types A B _=_ _=_ as IET.
  pose proof univ_has_bi_inv A B as IBI.
  pose proof l_inv as ILI.
  pose proof ex_proj1 ILI as e.
  apply e. apply IET.
Defined.
*)

Lemma ua (A B : Type) `{!A ~= B} : A = B.
Proof.
  pose proof equiv_types A B _=_ _=_ as IET.
  pose proof univalence A B as IBI.
  pose proof l_inv as ILI.
  pose proof proj1_sig ILI as e.
  apply e. apply IET.
Defined.

Arguments ua {_ _} _.

Module HomotopyTypicalDigression.

#[local] Open Scope ex_scope.
#[local] Open Scope sig_scope.

(** This is lemma 3.11.7 from the book. *)

Lemma ret (A B : Type) `{!HasRetrType A B _=_}
  `{!HasContr A _=_} : HasContr B _=_.
Proof.
  destruct HasRetrType0 as [f [g IR]]. destruct contr as [x h].
  exists (f x). intros y. rewrite <- (sect (f := f) y). f_equal. apply h.
Qed.

(** This is lemma 3.11.8 from the book. *)

Lemma sig_contr (A : Type) (a : A) : HasContr {x : A | a = x} _=_.
Proof.
  exists (a; id%type). intros [x e]. destruct e. apply id%type.
Defined.

Lemma ex_contr (A : Type) (a : A) : HasContr (exists x : A, a = x) _=_.
Proof.
  exists (a; id%type)%ex. intros [x e]. destruct e. apply id%type.
Defined.

(** This was definition 4.2.4 from the book. *)

Definition cf (A : Type) (P : A -> Prop) (x : A)
  (s : {a : {x : A | P x} | x = proj1_sig a}) : P x.
Proof. destruct s as [[y a] e]. simpl in e. induction e. apply a. Defined.

Definition cg (A : Type) (P : A -> Prop) (x : A)
  (a : P x) : {a : {x : A | P x} | x = proj1_sig a}.
Proof. exists (x; a). reflexivity. Defined.

Lemma classes (A : Type) (P : A -> Prop) (x : A) :
  IsIso _=_ _=_ cf (cg P x).
Proof.
  split.
  - split.
    + typeclasses eauto.
    + typeclasses eauto.
    + intros [[y a] e]. simpl in e. unfold cf, cg. rewrite e. reflexivity.
  - split.
    + typeclasses eauto.
    + typeclasses eauto.
    + intros a. unfold cf, cg. reflexivity.
Qed.

Lemma classify (A : Type) (P : A -> Prop) (x : A) :
  HasBiInv _=_ _=_ (cf (P := P) (x := x)).
Proof. split; exists (cg P x); apply classes. Defined.

(** This is lemma 4.8.1 from the book. *)

Lemma classifier (A : Type) (P : A -> Prop) (x : A) :
  fib _=_ (proj1_sig (P := P)) x ~= P x.
Proof. exists cf. apply classify. Defined.

Lemma ua_elim (A B : Type) (e : A = B) :
  idtoeqv e = (transport id e; has_bi_inv_eq_transport_id e)%sigT.
Proof. reflexivity. Defined.

Lemma ua_comp (A B : Type) (e : A ~= B) :
  idtoeqv (ua e) = e.
Proof.
  unfold ua.
  unfold equiv_types, l_inv.
  unfold bi_inv_has_l_inv.
  destruct (univalence A B) as [[f IIL] [g IIR]].
  unfold proj1_sig.
  pose proof retr (f := idtoeqv) (g := f) (g e) as r.
  pose proof sect (f := idtoeqv) (g := g) e as s.
  pose proof is_proper_eq_1 f s as p.
  pose proof (r o p ^-1)%type as c.
  pose proof is_proper_eq_1 idtoeqv c as q.
  apply (s o q)%type.
Defined.

Lemma ua_uniq (A B : Type) (e : A = B) :
  ua (idtoeqv e) = e.
Proof.
  unfold ua.
  unfold equiv_types, l_inv.
  unfold bi_inv_has_l_inv.
  destruct (univalence A B) as [[f IIL] [g IIR]].
  unfold proj1_sig.
  pose proof retr (f := idtoeqv) (g := f) e as r.
  apply r.
Defined.

Lemma ua_transport (A B : Type) (e : A ~= B) :
  transport id (ua e) = projT1 e.
Proof.
  pose proof ua_comp e as f.
  pose proof ua_elim (ua e) as g.
  pose proof (g o f ^-1)%type as h.
  pose proof ap projT1 h as i.
  apply (i ^-1).
Defined.

Lemma ua_transport' (A B : Type) (f : A -> B) (e : HasBiInv _=_ _=_ f) :
  transport id (ua (f; e)%sigT) = f.
Proof. apply ua_transport. Defined.

Lemma ua_refl (A : Type) :
  ua (refl A) = id%type.
Proof.
  rewrite <- ua_uniq. rewrite idtoeqv_refl. reflexivity.
Defined.

Lemma ua_sym (A B : Type) (e : A ~= B) :
  ua (sym A B e) = ua e ^-1.
Proof.
  rewrite <- ua_uniq. rewrite idtoeqv_sym. rewrite ua_comp. reflexivity.
Defined.

Lemma ua_trans (A B C : Type) (e : A ~= B) (f : B ~= C) :
  ua (trans A B C e f) = (ua f o ua e)%type.
Proof.
  rewrite <- ua_uniq. rewrite idtoeqv_trans. do 2 rewrite ua_comp. reflexivity.
Defined.

Lemma easy `{IsFunExtDep} (A B X : Type) (f : A -> B)
  (e : @HasBiInv A B _=_ _=_ f) : @HasBiInv (X -> A) (X -> B) _=_ _=_ (_o_ f).
Proof.
  destruct e as [[g ?] [h ?]].
  split.
  - exists (_o_ g). split; try typeclasses eauto.
    intros j. apply fun_ext_dep.
    intros x. unfold compose. rewrite retr. reflexivity.
  - exists (_o_ h). split; try typeclasses eauto.
    intros j. apply fun_ext_dep.
    intros x. unfold compose. rewrite sect. reflexivity.
Defined.

(** This is corollary 5.8.5 from the book. *)

Lemma equiv_ind (D : forall A B : Type, A ~= B -> Prop)
  (d : forall A : Type, D A A (refl A)) :
  forall (A B : Type) (e : A ~= B), D A B e.
Proof. intros A B e. rewrite <- (ua_comp e). destruct (ua e). apply d. Defined.

(** This is lemma 4.9.2 from the book. *)

Lemma also_easy (A B X : Type) (e : A ~= B) : (X -> A) ~= (X -> B).
Proof.
  destruct (ua e).
  apply refl.
Defined.

Definition inj1_sig (A : Type) (P : A -> Prop)
  `{!forall x : A, HasContr (P x) _=_} (x : A) : {x : A | P x} :=
  (x; proj1_sig contr).

Lemma contr_is_retr_proj1_sig_inj1_sig (A : Type) (P : A -> Prop)
  `{!forall x : A, HasContr (P x) _=_} : IsRetr _=_ proj1_sig inj1_sig.
Proof.
  intros [x a]. unfold proj1_sig, inj1_sig. f_equal.
  pose proof proj2_sig contr a as b. apply b.
Qed.

Lemma contr_is_sect_proj1_sig_inj1_sig (A : Type) (P : A -> Prop)
  `{!forall x : A, HasContr (P x) _=_} : IsSect _=_ proj1_sig inj1_sig.
Proof. intros x. unfold proj1_sig, inj1_sig. reflexivity. Qed.

#[local] Instance dubious (A B C : Type) (f : A -> B)
  `{!HasBiInv _=_ _=_ f} : HasBiInv (A := C -> A) (B := C -> B) _=_ _=_ (_o_ f).
Proof.
  remember ((f; _ : HasBiInv _=_ _=_ f)%sigT : _ ~= _) as e eqn : h; cbn in h.
  rewrite <- (ua_comp e) in h.
  destruct (ua e).
  rewrite ua_elim in h.
  (** This projection requires [sig] instead of [ex]. *)
  apply (ap projT1) in h. cbn in h. subst f.
  split.
  - exists (_o_ id).
    split; try apply is_proper_eq_1.
    intros i. reflexivity.
  - exists (_o_ id).
    split; try apply is_proper_eq_1.
    intros i. reflexivity.
Defined.

(** This is part of corollary 4.9.3 from the book. *)

Lemma alpha (A : Type) (P : A -> Prop)
  `{!forall x : A, HasContr (P x) _=_} (f : A -> {x : A | P x}) (x : A) : A.
Proof. apply (proj1_sig (f x)). Defined.

Lemma coalpha (A : Type) (P : A -> Prop)
  `{!forall x : A, HasContr (P x) _=_} (f : A -> A) (x : A) : {x : A | P x}.
Proof. apply (inj1_sig (f x)). Defined.

(** This is corollary 4.9.3 from the book. *)

#[local] Instance before_why (A : Type) (P : A -> Prop)
  `{!forall x : A, HasContr (P x) _=_} :
  HasBiInv _=_ _=_ (proj1_sig (P := P)).
Proof.
  split; exists inj1_sig; split;
  try typeclasses eauto;
  apply contr_is_retr_proj1_sig_inj1_sig ||
  apply contr_is_sect_proj1_sig_inj1_sig.
Defined.

Lemma why (A : Type) (P : A -> Prop)
  `{!forall x : A, HasContr (P x) _=_} :
  {x : A | P x} ~= A.
Proof. exists proj1_sig. apply before_why. Defined.

Lemma why_squared (A : Type) (P : A -> Prop)
  `{!forall x : A, HasContr (P x) _=_} :
  (A -> {x : A | P x}) ~= (A -> A).
Proof. apply also_easy. apply why. Defined.

Lemma after_why_squared (A : Type) (P : A -> Prop)
  `{!forall x : A, HasContr (P x) _=_} :
  HasBiInv _=_ _=_ alpha.
Proof.
  match goal with
  | x : forall _ : _, HasContr _ _=_ |- _ => rename x into IC
  end.
  unfold alpha.
  pose proof dubious A (f := proj1_sig) as d.
  unfold compose in d.
  apply d.
Defined.

(** These are parts of theorem 4.9.4 from the book. *)

Lemma phi (A : Type) (P : A -> Prop)
  `{!forall x : A, HasContr (P x) _=_} :
  (forall x : A, P x) -> (fib _=_ alpha id%core).
Proof. intros f. hnf. exists (fun x : A => (x; f x)). apply id%type. Defined.

Lemma psi (A : Type) (P : A -> Prop)
  `{!forall x : A, HasContr (P x) _=_} :
  (fib _=_ alpha id%core) -> (forall x : A, P x).
Proof.
  intros gp x.
  apply (transport P (happly _ _ (proj2_sig gp ^-1) x)
  (proj2_sig (proj1_sig gp x))).
Defined.

Lemma eq_pi_is_what (A : Type) (P : A -> Prop)
  `{!forall x : A, HasContr (P x) _=_} :
  HasRetrType (fib _=_ alpha id%core) (forall x : A, P x) _=_.
Proof.
  match goal with
  | x : forall _ : _, HasContr _ _=_ |- _ => rename x into c
  end.
  exists psi, phi. intros f. unfold phi. unfold psi. cbn. reflexivity.
Defined.

Lemma help (A B : Type) (f : A -> B) (x y : A) (e : x = y) :
  (transport (fun y : A => f x = f y) e id = ap f e o id)%type.
Proof. destruct e. reflexivity. Defined.

(** This is lemma 4.2.5 from the book. *)

Theorem fine (A B : Type) (f : A -> B) (y : B) (s t : fib _=_ f y) :
  (s = t) ~= {g : proj1_sig s = proj1_sig t |
  ap f g o proj2_sig s = proj2_sig t}%type.
Proof.
  eapply trans; try apply (sig_has_equiv_types s t).
  destruct s as [x p], t as [x' p']. cbn. subst y.
  hnf. pose (fun a : {g : x = x' | transport (fun y : A => f x = f y) g id%type = p'} =>
  (proj1_sig a; transport (fun p : _ => p = p') (help f (proj1_sig a)) (proj2_sig a)) :
  {g : x = x' | (ap f g o id)%type = p'}) as e.
  pose (fun a : {g : x = x' | (ap f g o id)%type = p'} =>
  (proj1_sig a; transport (fun p : _ => p = p') (help f (proj1_sig a) ^-1) (proj2_sig a)) :
  {g : x = x' | transport (fun y : A => f x = f y) g id%type = p'}) as e'.
  exists e. subst e. repeat (split; try typeclasses eauto).
  exists e'. subst e'. repeat (split; try typeclasses eauto).
  intros [e e']. cbn. apply ap.
  rewrite transport_trans. rewrite eq_trans_sym_inv_r.
  cbn. reflexivity.
  exists e'. subst e'. repeat (split; try typeclasses eauto).
  intros [e e']. cbn. apply ap.
  rewrite transport_trans. rewrite eq_trans_sym_inv_l.
  cbn. reflexivity.
Defined.

Lemma move_this (A : Type)
  (x y : A) (p q : x = y) (c : (id = p o (q ^-1))%type) : q = p.
Proof.
  rewrite <- (eq_trans_sym_inv_l q) in c.
  apply HLevels.eq_trans_cancel in c.
  apply c.
Defined.

Lemma move_that (A : Type)
  (x y z : A) (p : x = y) (q : y = z) (r : x = z)
  (c : (q o p = r)%type) : (q = r o (p ^-1))%type.
Proof.
  destruct r.
  rewrite <- (eq_trans_sym_inv_r p) in c.
  apply HLevels.eq_trans_cancel in c.
  rewrite eq_trans_refl_r.
  apply c.
Defined.

(** This is lemma 2.4.3 from the book. *)

Lemma commuting (A B : Type)
  (f g : A -> B) (h : forall x : A, f x = g x) (x y : A) (e : x = y) :
  (ap g e o h x = h y o ap f e)%type.
Proof.
  destruct e. do 2 rewrite ap_refl.
  rewrite eq_trans_refl_l. rewrite eq_trans_refl_r. reflexivity.
Defined.

(** This is corollary 2.4.4 from the book. *)

Lemma commuting_harder (A : Type)
  (f : A -> A) (h : forall x : A, f x = id x) (x : A) :
  h (f x) = ap f (h x).
Proof.
  epose proof commuting h _ as c.
  rewrite ap_id in c.
  rewrite eq_trans_sym_inv_r in c.
  rewrite ap_sym in c.
  apply move_this in c.
  symmetry. apply c.
Defined.

(** This is theorem 4.2.3 from the book. *)

Lemma pre_unhae (A B : Type) (f : A -> B)
  `{!IsQInv _=_ _=_ f} : IsHAE f.
Proof.
  match goal with
  | x : IsQInv _ _ _ |- _ => rename x into IQI
  end.
  destruct IQI as [g [IIL IIR]].
  eset (II := _ : IsIso _=_ _=_ f g). Unshelve. 2:
  { split.
    - split.
      + apply is_proper_eq_1.
      + apply is_proper_eq_1.
      + intros x. apply retr.
    - split.
      + apply is_proper_eq_1.
      + apply is_proper_eq_1.
      + intros x.
        pose proof fun b : B => sect (f := f) (g := g) (f (g b)) ^-1 as s.
        pose proof fun b : B => ap f (retr (f := f) (g := g) (g b)) as r.
        pose proof fun b : B => sect (f := f) (g := g) b as t.
        pose proof fun b : B => (t b o r b o s b)%type as u.
        apply u. }
  hnf. exists g. exists II. subst II. intros x.
  unfold retr, sect, iso_l_is_retr, iso_r_is_sect, iso_is_iso_l, iso_is_iso_r.
  destruct IIL as [p p' r], IIR as [q q' s].
  change @f_equal with @ap.
  pose proof commuting (g := f) (fun y : A => s (f y)) (r x) as c.
  cbv beta in c. apply move_that in c. rewrite c. clear c.
  f_equal. f_equal.
  rewrite <- ap_ap. apply (f_equal (ap f)).
  symmetry. apply (commuting_harder (f := fun y => g (f y)) r).
Defined.

Lemma unhae (A B : Type) (f : A -> B)
  `{!HasBiInv _=_ _=_ f} : IsHAE f.
Proof.
  match goal with
  | x : HasBiInv _ _ _ |- _ => rename x into IBI
  end.
  apply @pre_unhae.
  apply bi_inv_is_q_inv.
Defined.

(** This is theorem 4.2.6 from the book. *)

Theorem curses (A B : Type) (f : A -> B) (y : B)
  `{!IsHAE f} : HasContr (fib _=_ f y) _=_.
Proof.
  match goal with
  | x : IsHAE _ |- _ => rename x into IHAE
  end.
  destruct IHAE as [g [II c]].
  unfold iso_l_is_proper_f in c. unfold iso_is_iso_l in c.
  destruct II as [[] []].
  hnf.
  set (s := (g y; sect (f := f) (g := g) y ^-1) : fib _=_ f y); cbn in s.
  exists s. intros t.
  pose proof fine s t as IET.
  apply sym in IET.
  apply (projT1 IET).
  subst s; destruct t as [x p].
  pose (retr (f := f)) as r.
  pose (sect (f := f)) as s.
  set (gamma := (r x o ap g p)%type).
  exists gamma. unfold proj2_sig. subst gamma. subst r.
  assert (c' : forall x : A, ap f (retr x) = sect (f x)).
  { intros x'. change @ap with @f_equal. apply (c x'). }
  rewrite ap_trans.
  rewrite p. rewrite ap_refl. rewrite eq_trans_refl_l.
  rewrite c'. rewrite eq_trans_sym_inv_l. reflexivity.
Defined.

(** This is an approximation of theorem 4.2.6 from the book. *)

(** We inline the proof [apply curses, unhae] to get rid of [IsHAE]. *)

Theorem curses' (A B : Type) (f : A -> B) (y : B)
  `{!HasBiInv _=_ _=_ f} : HasContr (fib _=_ f y) _=_.
Proof.
  match goal with
  | x : HasBiInv _ _ _ |- _ => rename x into IBI
  end.
  pose proof bi_inv_is_q_inv : IsQInv _=_ _=_ f as IQI.
  destruct IQI as [g [IIL IIR]].
  eset (II := _ : IsIso _=_ _=_ f g). Unshelve. 2:
  { split.
    - split.
      + apply is_proper_eq_1.
      + apply is_proper_eq_1.
      + intros x. apply retr.
    - split.
      + apply is_proper_eq_1.
      + apply is_proper_eq_1.
      + intros x.
        pose proof fun b : B => sect (f := f) (g := g) (f (g b)) ^-1 as s.
        pose proof fun b : B => ap f (retr (f := f) (g := g) (g b)) as r.
        pose proof fun b : B => sect (f := f) (g := g) b as t.
        pose proof fun b : B => (t b o r b o s b)%type as u.
        apply u. }
  assert (c : forall x : A,
  @f_equal A B f (g (f x)) x
  (@retr A B _=_ f g
  (@iso_l_is_retr A B _=_ _=_ f g (@iso_is_iso_l A B _=_ _=_ f g II)) x) =
  @sect A B _=_ f g
  (@iso_r_is_sect A B _=_ _=_ f g (@iso_is_iso_r A B _=_ _=_ f g II))
  (f x)).
  intros x. subst II.
  unfold retr, sect, iso_l_is_retr, iso_r_is_sect, iso_is_iso_l, iso_is_iso_r.
  destruct IIL as [p p' r], IIR as [q q' s].
  change @f_equal with @ap.
  pose proof commuting (g := f) (fun y : A => s (f y)) (r x) as c.
  cbv beta in c. apply move_that in c. rewrite c. clear c.
  f_equal. f_equal.
  rewrite <- ap_ap. apply (f_equal (ap f)).
  symmetry. apply (commuting_harder (f := fun y => g (f y)) r).

  destruct II as [[] []].
  hnf.
  set (s := (g y; sect (f := f) (g := g) y ^-1) : fib _=_ f y); cbn in s.
  exists s. intros t.
  pose proof fine s t as IET.
  apply sym in IET.
  apply (projT1 IET).
  subst s; destruct t as [x p].
  pose (retr (f := f)) as r.
  pose (sect (f := f)) as s.
  set (gamma := (r x o ap g p)%type).
  exists gamma. unfold proj2_sig. subst gamma. subst r.
  assert (c' : forall x : A, ap f (retr x) = sect (f x)).
  { intros x'. change @ap with @f_equal. apply (c x'). }
  rewrite ap_trans.
  rewrite p. rewrite ap_refl. rewrite eq_trans_refl_l.
  rewrite c'. rewrite eq_trans_sym_inv_l. reflexivity.
Defined.

(** This is an approximation of theorem 4.4.3 from the book. *)

Theorem urgh (A B : Type) (f : A -> B)
  `{!forall y : B, HasContr (fib _=_ f y) _=_} : HasBiInv _=_ _=_ f.
Proof.
  match goal with
  | x : forall _ : _, HasContr _ _ |- _ => rename x into IC
  end.
  set (g y := proj1_sig (proj1_sig (IC y))).
  split.
  - exists g.
    split; try apply is_proper_eq_1.
    intros z. cbv. destruct (IC (f z)) as [[w e] e'].
    unfold fib in e'. pose proof e' (z; id%type) as i. inversion_sigma i; auto.
  - exists g.
    split; try apply is_proper_eq_1.
    intros z. cbv. destruct (IC z) as [[w e] e'].
    unfold fib in e'. symmetry. auto.
Defined.

(** This is definition 4.7.5 from the book. *)

Definition total (A : Type) (P Q : A -> Prop)
  (f : forall x : A, P x -> Q x) (a : {x : A | P x}) : {x : A | Q x}.
Proof. apply (proj1_sig a; f (proj1_sig a) (proj2_sig a))%sig. Defined.

Definition total_ex (A : Type) (P Q : A -> Prop)
  (f : forall x : A, P x -> Q x) (a : exists x : A, P x) : exists x : A, Q x.
Proof. destruct a as [x p]. exists x. apply f. apply p. Defined.

Lemma contrequiv (A B : Type) (f : A -> B)
  `{!HasContr A _=_} `{!HasContr B _=_} :
  HasBiInv _=_ _=_ f.
Proof.
  destruct (@contr A _=_ _) as [x ex].
  destruct (@contr B _=_ _) as [y ey].
  split.
  - exists (const x).
    split; try apply is_proper_eq_1.
    intros z. cbv. apply ex.
  - exists (const x).
    split; try apply is_proper_eq_1.
    intros z. cbv. etransitivity. symmetry. apply ey. apply ey.
Defined.

Definition fibernator (A : Type) (P Q : A -> Prop)
  (f : forall x : A, P x -> Q x) (x : A) (q : Q x) :
  {a : {x : A | P x} | (x; q) = total f a} -> {p : P x | q = f x p}.
Proof.
  intros [[y p] e]. cbv in e.
  inversion_sigma e as [e0 e1].
  destruct e0.
  cbv in e1.
  exists p. apply e1.
Defined.

Definition cofibernator (A : Type) (P Q : A -> Prop)
  (f : forall x : A, P x -> Q x) (x : A) (q : Q x) :
  {p : P x | q = f x p} -> {a : {x : A | P x} | (x; q) = total f a}.
Proof.
  intros [p e]. exists (x; p)%sig. cbv. f_equal. apply e.
Defined.

Arguments cofibernator {_ _ _} _ {_ _} _.

Lemma fibering (A : Type) (P Q : A -> Prop)
  (f : forall x : A, P x -> Q x) (x : A) (q : Q x) :
  HasBiInv _=_ _=_ (fibernator f (x := x) (q := q)).
Proof.
  split.
  - exists (cofibernator f (x := x) (q := q)).
    split; try apply is_proper_eq_1.
    intros [[y p] e]. cbv in e. inversion_sigma e as [e0 e1].
    destruct e0. cbv in e1. subst q. reflexivity.
  - exists (cofibernator f (x := x) (q := q)).
    split; try apply is_proper_eq_1.
    intros [p e]. subst q. reflexivity.
Defined.

(** This is theorem 4.7.6 from the book. *)

Lemma fiberwise (A : Type) (P Q : A -> Prop)
  (f : forall x : A, P x -> Q x) (x : A) (q : Q x) :
  fib _=_ (total f) (x; q) ~= fib _=_ (f x) q.
Proof.
  exists (fibernator f). apply fibering.
Defined.

(** This is theorem 4.7.7 from the book. *)

Lemma fiberwise_transform (A : Type) (P Q : A -> Prop)
  (f : forall x : A, P x -> Q x) :
  (forall x : A, HasBiInv _=_ _=_ (f x)) -> HasBiInv _=_ _=_ (total f).
Proof.
  intros e.
  pose proof fun (x : A) (q : Q x) => @curses' _ _ _ q (e x) as t.
  pose proof fiberwise f as b.
  pose proof fun (x : A) (q : Q x) => ua (b x q) as h.
  pose proof fun (x : A) (q : Q x) =>
  transport (fun hole : _ => HasContr hole _=_) (h x q ^-1) (t x q) as j;
  cbv beta in j.
  pose proof @urgh _ _ (total f) as k.
  apply k. intros [y q]. apply j.
Defined.

Lemma fiberwise_transform_dual (A : Type) (P Q : A -> Prop)
  (f : forall x : A, P x -> Q x) :
  HasBiInv _=_ _=_ (total f) -> forall x : A, HasBiInv _=_ _=_ (f x).
Proof.
  intros e y.
  eapply @urgh. intros q.
  eapply @curses' in e.
  epose proof fiberwise f as b.
  epose proof (ua (b _ _)) as h.
  rewrite h in e.
  eapply e.
Defined.

(** This is theorem 4.9.4 from the book. *)

Lemma eq_pi_contr (A : Type) (P : A -> Prop)
  `{!forall x : A, HasContr (P x) _=_} : HasContr (forall x : A, P x) _=_.
Proof.
  match goal with
  | h : forall _ : _, HasContr _ _=_ |- _ => rename h into c
  end.
  pose proof why_squared as w.
  pose proof eq_pi_is_what as q.
  pose proof @ret (fib _=_ alpha id%core) (forall x : A, P x) q as r.
  apply r.
  apply curses'.
  apply after_why_squared.
Defined.

(** This is theorem 4.9.5 from the book. *)

Lemma conclusion (A : Type) (P : A -> Prop) (f g : forall x : A, P x) :
  HasBiInv _=_ _=_ (happly f g).
Proof.
  (* enough (theorem_4_7_7 :
  HasBiInv _=_ _=_ (fun a : exists g : forall x : A, P x, f = g =>
  match a with
  | (x; e)%ex => (x; happly _ _ e)%ex
  end :
  exists h : forall x : A, P x, forall x : A, f x = h x)) by admit. *)
  enough (by_theorem_4_7_7 :
  HasBiInv _=_ _=_ (total (happly f))).
  { epose proof @fiberwise_transform_dual _ _ _ (happly f) _ as t.
    apply t; apply by_theorem_4_7_7. }
  enough (by_theorem_3_11_8 :
  HasContr {h : forall x : A, P x | forall x : A, f x = h x} _=_).
  { epose proof @contrequiv _ _ _ as c.
    eapply c.
    apply sig_contr.
    assumption. }
  enough (by_theorem_2_15_7 :
  HasContr (forall x : A, {a : P x | f x = a}) _=_).
  (** This uses function extensionality. *)
  (* { epose proof @seriously A P (fun (a : A) (b : P a) => f a = b) as s; cbv beta in s.
    rewrite <- (ua s). assumption. } *)
  { epose proof @ret _ _ as r.
    epose proof @need_this _ _ (fun x y => f x = y) as n.
    destruct n as [k [_ _ s]].
    eapply r.
    unfold HasRetrFn.
    eexists _. eexists _. eapply s.
    apply @eq_pi_contr.
    intros x.
    eapply sig_contr. }
  apply @eq_pi_contr.
  intros x. apply @sig_contr.
Defined.

Print Assumptions conclusion.

#[local] Unset Universe Checking.

Lemma fun_now : IsFunExt.
Proof.
  intros A B f g e.
  epose proof (conclusion f g) as two.
  destruct two as [[h IIL] IRI]. auto.
Qed.

(** This should follow. *)

Lemma more_fun_now : IsFunExtDep.
Proof.
  intros A P f g e.
  epose proof (conclusion f g) as two.
  destruct two as [[h IIL] IRI]. auto.
Qed.

End HomotopyTypicalDigression.

(** Proposition extensionality
    makes function extensionality an equality. *)

Lemma prop_fun_ext_dep `{IsPropExt} `{IsFunExtDep}
  (A : Type) (P : A -> Type) (f g : forall x : A, P x) :
  (forall x : A, f x = g x) = (f = g).
Proof.
  apply prop_ext. split.
  - intros a. apply fun_ext_dep. intros x. apply a.
  - intros a x. apply equal_f_dep. apply a.
Qed.

(** Families of propositions are propositions. *)

Lemma eq_pi_is_prop `{IsFunExtDep} (A : Type) (P : A -> Prop)
  `{!forall x : A, IsProp (P x)} : IsProp (forall x : A, P x).
Proof.
  match goal with
  | h : forall _ : _, IsProp _ |- _ => rename h into p
  end.
  intros g h. apply fun_ext_dep. intros x. apply p.
Qed.

(** Families of contractible types are contractible. *)

Lemma eq_pi_has_contr `{IsFunExtDep} (A : Type) (P : A -> Prop)
  `{!forall x : A, HasContr (P x) _=_} : HasContr (forall x : A, P x) _=_.
Proof.
  match goal with
  | h : forall _ : _, HasContr _ _=_ |- _ => rename h into c
  end.
  apply @inhabited_prop_has_contr.
  - intros x. apply c.
  - apply (@eq_pi_is_prop _). intros x. apply contr_is_prop.
Qed.

(** Families of sets are sets. *)

Lemma eq_pi_is_set `{IsPropExt} `{IsFunExtDep} (A : Type) (P : A -> Prop)
  `{!forall x : A, IsSet (P x)} : IsSet (forall x : A, P x).
Proof.
  match goal with
  | h : forall _ : _, IsSet _ |- _ => rename h into s
  end.
  intros f g.
  pose proof prop_fun_ext_dep f g as t. rewrite <- t. clear t.
  apply (@eq_pi_is_prop _).
  intros x. apply @set_is_prop_eq. apply s.
Qed.

(** Fibrations are at the same homotopy level as their fibers. *)

Lemma eq_h_level_has_h_level `{IsPropExt} `{IsFunExtDep}
  (A : Type) (P : A -> Prop) (n : nat)
  `{!forall x : A, HasHLevel n (P x)} : HasHLevel n (forall x : A, P x).
Proof.
  match goal with
  | h : forall _ : _, HasHLevel _ _ |- _ => rename h into a
  end.
  revert A P a. induction n as [| p b]; intros A P a.
  - apply @contr_has_h_level_0. apply (@eq_pi_has_contr _).
    intros x. apply @h_level_0_has_contr. apply a.
  - intros f g.
    pose proof prop_fun_ext_dep f g as t. rewrite <- t. clear t.
    apply b. intros x. apply h_level_S_has_h_level_eq. apply a.
Qed.

(** Univalence implies type extensionality. *)

#[export] Instance univ_is_type_ext `{IsUniv} : IsTypeExt.
Proof.
  intros A B f g r s. apply ua. exists f. split.
  - exists g. split.
    + typeclasses eauto.
    + typeclasses eauto.
    + intros x. apply r.
  - exists g. split.
    + typeclasses eauto.
    + typeclasses eauto.
    + intros y. apply s.
Qed.

(** Univalence implies proposition extensionality for types. *)

#[export] Instance univ_is_prop_ext_type `{IsUniv} : IsPropExtType.
Proof.
  intros A B IPA IPB [f g]. pose proof univ_has_bi_inv A B as s.
  destruct s as [ua [IPidtoeqv IPua]]. apply ua. exists f. split.
  - exists g. split; try typeclasses eauto. intros x. apply irrel.
  - exists g. split; try typeclasses eauto. intros x. apply irrel.
Qed.

(** Type extensionality implies proposition extensionality for types. *)

#[export] Instance type_ext_is_prop_ext_type `{IsTypeExt} : IsPropExtType.
Proof.
  intros A B IPA IPB [f g]. apply (@type_ext _ _ _ f g).
  - intros x. apply irrel.
  - intros y. apply irrel.
Qed.

(** We cannot prove that [IsPropExt] and [IsPropExtType] are related,
    because [Prop] and [Type] are stratified. *)

Module FromAxioms.

#[export] Instance is_prop_ext : IsPropExt.
Proof. intros A B. apply propositional_extensionality. Qed.

#[export] Instance is_prop_ext_type : IsPropExtType.
Proof. intros A B. apply propositional_extensionality_type. Qed.

#[export] Instance is_pred_ext : IsPredExt.
Proof. intros A P Q. apply predicate_extensionality. Qed.

#[export] Instance is_fun_ext : IsFunExt.
Proof. intros A B. apply functional_extensionality. Qed.

#[export] Instance is_fun_ext_dep : IsFunExtDep.
Proof. intros A P. apply functional_extensionality_dep. Qed.

#[export] Instance is_type_ext : IsTypeExt.
Proof. intros A B. apply type_extensionality. Qed.

#[export] Instance is_univ : IsUniv.
Proof. intros A B. apply univalence. Qed.

End FromAxioms.

(** Univalence breaks extraction. *)

Module ExtractionProblem.

Import Decisions.
Import HomotopyTypicalDigression.

#[local] Instance has_bi_inv_eq_negb :
  HasBiInv _=_ _=_ negb.
Proof.
  split; exists negb; split; try typeclasses eauto; intros []; reflexivity.
Defined.

#[local] Instance has_equiv_types_eq_bool :
  bool ~= bool.
Proof. exists negb; apply has_bi_inv_eq_negb. Defined.

Definition no : bool := false.
Definition yes : bool := transport id (ua has_equiv_types_eq_bool) false.

Definition contradiction : bool :=
  if dec (no = yes) then true else false.

Lemma no_contradiction : ~ contradiction.
Proof.
  unfold contradiction.
  destruct (dec (no = yes)) as [e | _].
  - unfold no, yes in e.
    unfold has_equiv_types_eq_bool in e.
    rewrite ua_transport' in e.
    unfold negb in e.
    congruence.
  - intros e.
    congruence.
Defined.

End ExtractionProblem.

From Coq Require Import ExtrOcamlBasic.

(* Extraction "/tmp/extraction_problem.ml" ExtractionProblem. *)

author: Tuplanolla

repo: dez

save_path: github-repos/coq/Tuplanolla-dez


text:
Require Import List.
Export ListNotations.

Require Import PeanoNat.

Require Import Ensembles.
Require Import Prop_Bi_Int_calcs.
Require Import Prop_Bi_Int_logics.

Lemma extens_diff_sBIC : forall (p : V),
    (sBIC_rules (Singleton _ (# p), Neg (wNeg (# p)))).
Proof.
intro p. apply DNs with (ps:=[(Singleton _ (# p), #p)]).
intros. inversion H. subst. apply Ids. apply IdRule_I. apply In_singleton.
inversion H0. apply DNsRule_I.
Qed.

Theorem sBIC_extens_wBIC : forall s,
    (wBIC_rules s) -> (sBIC_rules s).
Proof.
intros s D. induction D.
(* Id *)
- inversion H. subst. apply Ids. apply IdRule_I. auto.
(* Ax *)
- inversion H. subst. apply Axs. apply AxRule_I. auto.
(* MP *)
- inversion H1. subst. assert (J1: List.In (Γ, A → B) [(Γ, A → B); (Γ, A)]). apply in_eq.
  pose (H0 (Γ, A → B) J1). assert (J2: List.In (Γ, A) [(Γ, A → B); (Γ, A)]). apply in_cons. apply in_eq.
  pose (H0 (Γ, A) J2). apply MPs with (ps:=[(Γ, A → B); (Γ, A)]).
  intros. inversion H1. subst. auto. apply MPRule_I.
(* DN *)
- inversion H1. subst. assert (J1: List.In (Empty_set (BPropF V), A) [(Empty_set (BPropF V), A)]). apply in_eq.
  pose (H0 (Empty_set (BPropF V), A) J1). assert (Included _ (Empty_set _) Γ).
  intro. intro. inversion H2. pose (@sBIC_monot (Empty_set _, A) s Γ H2).
  apply DNs with (ps:=[(Γ, A)]). intros. inversion H3. subst.
  assumption. inversion H4. apply DNsRule_I.
Qed.

Theorem pair_sBIC_extens_wBIC : forall P,
    (wpair_derrec P) -> (spair_derrec P).
Proof.
intros P wpair.
unfold spair_derrec. unfold wpair_derrec in wpair.
destruct wpair. destruct H. destruct H0. exists x. repeat split ; auto.
apply sBIC_extens_wBIC. auto.
Qed.

Theorem sBIC_same_thms_wBIC : forall s,
    (sBIC_rules s) ->
    (forall A, ((Empty_set _, A) = s) -> (wBIC_rules s)).
Proof.
intros s D. induction D.
(* Ids *)
- intros A id. inversion H. subst. inversion H2. subst.
  apply Id. apply IdRule_I. auto.
(* Axs *)
- intros A id. inversion H. subst. inversion H2. subst.
  apply Ax. apply AxRule_I. auto.
(* MPs *)
- intros A id. inversion H1. subst. inversion H3. subst.
  assert (J1: List.In (Empty_set (BPropF V), A0 → A) [(Empty_set (BPropF V), A0 → A); (Empty_set (BPropF V), A0)]). apply in_eq.
  pose (H0 (Empty_set (BPropF V), A0 → A) J1).
  assert (J2: List.In (Empty_set (BPropF V), A0) [(Empty_set (BPropF V), A0 → A); (Empty_set (BPropF V), A0)]). apply in_cons. apply in_eq.
  pose (H0 (Empty_set (BPropF V), A0) J2).
  apply MP with (ps:=[(Empty_set _, A0 → A); (Empty_set _, A0)]).
  intros. inversion H2. subst. apply w with (A1:=A0 → A). auto.
  inversion H4. subst. apply w0 with (A:=A0). auto. inversion H5. apply MPRule_I.
(* DNs *)
- intros A id. inversion H1. subst. inversion H3. subst.
  assert (J1: List.In (Empty_set (BPropF V), A0) [(Empty_set (BPropF V), A0)]). apply in_eq.
  pose (H0 (Empty_set (BPropF V), A0) J1).
  apply DNw with (ps:=[(Empty_set _, A0)]). intros. inversion H2. subst.
  apply w with (A:=A0). auto. inversion H4. apply DNwRule_I.
Qed.

Theorem wBIC_same_thms_sBIC : forall s,
    (wBIC_rules s) ->
    (forall A, ((Empty_set _, A) = s) -> (sBIC_rules s)).
Proof.
intros. apply sBIC_extens_wBIC. assumption.
Qed.

author: ianshil


text:
Require Import ZArith.
Require Import List Bool Znumtheory Decidable.
Require Import Rbase Reals QArith micromega.Lia micromega.Lqa micromega.Lra Qreals.

From BY Require Import AppendixE AppendixF AppendixG Divstep Zpower_nat Zlemmas Rlemmas IZR Section9 Matrix Spectral Log Floor Section9 Impl.
From BY.Hierarchy Require Import Definitions BigOp.

Import Z.

Local Open Scope Z.

Local Coercion of_nat : nat >-> Z.

Section __.

  Variable f g : Z.
  Hypothesis fodd : odd f = true.
  Hypothesis gnon0 : g <> 0.

  Ltac Rpos :=
    repeat match goal with
           | [ |- (0 <= _ + _)%R] => apply add_pos
           | [ |- (0 <= _ / _)%R] => apply div_pos_pos
           | [ |- (0 <= _ * _)%R] => apply Rlemmas.mul_pos
           | [ |- (0 <= log ?n ?x)%R] => apply log_pos
           end; try lra.

  Ltac Rle_log :=
    repeat match goal with
           | [ |- (_ <= log _ _)%R] => apply log_le_lower_bound
           end; try lra.

  Ltac destruct_if :=
    repeat match goal with
           | [ |- context[if ?x then _ else _]] => destruct x
           end.

  Lemma log45 : (49 * log 4 5 <= 57)%R.
  Proof.
    apply Rle_div_r. lra. apply log_le_upper_bound. lra. lra.
    rewrite <- Rabs_pos_eq. apply le_pow with (n := 49%nat). lia.
    rewrite <- (Rpower_pow _ (Rpower _ _)).
    rewrite Rpower_mult. replace (57 / 49 * INR 49)%R with (INR 57).
    rewrite Rpower_pow. lra. lra. rewrite !INR_IZR_INZ. field. apply Rpower_pos_nonneg. apply Rpower_pos.
  Qed.

  Lemma iterations_bound d :
    floor ((49 * IZR d + 57) / 17) <= (49 * d + 80) / 17.
  Proof.
    apply le_IZR. apply floor_upper_bound.
    assert ((49 * d + 57) / 17 <= ((49 * d + 80) / 17) - 1)%R by lra.
    etransitivity. apply H.
    autorewrite with pull_izr.
    apply div_Rdiv.
  Qed.

  Theorem _11_2 d m (G4 : (log 2 (vec_norm (IZR f, IZR (2 * g)%Z)) > 21)%R) :
    let '(um, vm, qm, rm) := big_mul_rev (fun i => Tn 1 f g i) 0 m in
    f ^+ 2 + 4 * g ^+ 2 <= 5 * 4 ^+ d ->
    (if (lt_dec d 46)%nat then
       (49 * d + 80) / 17 <= m else (49 * d + 57) / 17 <= m) ->
    gn 1 f g m = 0 /\
    abs (fn 1 f g m) = gcd f g /\
    vm * g mod f = 2 ^+ m * (fn 1 f g m) mod f.
  Proof.
    pose proof _9_1_1 1 f g m 0 ltac:(lia) fodd as _911.
    destruct (big_mul_rev (fun i => Tn 1 f g i) 0 m) as [[[um vm] qm] rm] eqn:E.
    intros fgbound mbound.
    pose proof log45.
    pose proof iterations_bound d.
    assert (mbound1 : floor ((49 * d + 57) / 17) <= m).
    { destruct (lt_dec d 46)%nat. lia.
      autorewrite with pull_izr.
      rewrite floor_div. assumption. }

    set (R0 := f). change f with R0 in G4.
    set (R1 := 2 * g). change (2 * g) with R1 in G4.
    assert (gcdeq : gcd R0 g = gcd R0 R1). { unfold R1. rewrite <- gcd_rel_prime. reflexivity. apply odd_gcd. apply fodd. }
    assert (R0_odd : odd R0 = true). { apply fodd. }
    assert (R1_even : even R1 = true). { apply even_mul_2_l. }
    assert (R1_non0 : R1 <> 0). { assert (g <> 0) by (apply gnon0). lia. }
    set (b := (log 2 (vec_norm (IZR R0, IZR R1)))).
    set (n := (to_nat
                 (if Rle_dec b 21
                  then floor (19 * b / 17)
                  else if Rle_dec b 46
                       then floor ((49 * b + 23) / 17)
                       else floor (49 * b / 17)))).

    assert (bpos : (0 <= b)%R).
    { unfold b. Rpos. apply F6. apply vnonzero. right. cbn. change RbaseSymbolsImpl.R0 with (IZR Z0). apply IZR_neq. assumption. }

    assert (eq1 : (Rpower 4 b = (f ^+ 2 + 4 * g ^+ 2)%Z)%R).
    { replace 4%R with (2 * 2)%R by lra. rewrite <- Rpower_mult_distr by lra. unfold b. rewrite Rpower_log. unfold vec_norm.
      rewrite sqrt_sqrt. unfold R0, R1.
      autorewrite with push_izr. lra. nra.
      apply vec_norm_pos_nonneg. apply vnonzero. right. cbn. change RbaseSymbolsImpl.R0 with (IZR Z0). apply IZR_neq. assumption. lra. lra. }

    assert (bbound : (b <= IZR d + log 4 5)%R).
    { apply IZR_le in fgbound. rewrite <- eq1 in fgbound.
      apply log_le_lower_bound in fgbound.
      etransitivity. apply fgbound. autorewrite with push_izr. rewrite log_mult.
      rewrite log_pow. rewrite log_n_n. rewrite INR_IZR_INZ. lra. lra. lra. lra. lra. apply pow_lt. lra. lra. }

    assert (nlem : (n <= m)%nat).
    { replace m with (to_nat (of_nat m)) by lia. apply Z2Nat.inj_le.
      destruct_if; try apply floor_pos.
      Rpos. Rpos. Rpos. lia.
      destruct_if.
      { assert (H1 : floor (19 * b / 17) <= floor (49 * b / 17)).
        { apply floor_inc. nra. }
        assert (H2 : (floor (49 * b / 17)) <= floor (49 * (d + log 4 5) / 17)).
        { apply floor_inc. nra. }
        assert (H3 : floor (49 * (d + log 4 5) / 17) <= floor ((49 * d + 57) / 17)).
        { apply floor_inc. lra. }
        lia. }
      { destruct (lt_dec d 46)%nat.
        { assert (H1 : floor ((49 * b + 23) / 17) <= floor ((49 * (d + log 4 5) + 23) / 17)).
          { apply floor_inc. lra. }
          assert (H2 : floor ((49 * (d + log 4 5) + 23) / 17) <= floor ((49 * d + 80) / 17)).
          { apply floor_inc. lra. }
          rewrite <- floor_div in mbound. autorewrite with push_izr in mbound. lia. }
        { apply Nat.nlt_ge in n1. apply le_INR in n1. rewrite !INR_IZR_INZ in n1. replace (IZR 46%nat) with (IZR 46) in n1 by reflexivity.
          assert (H1 : floor ((49 * b + 23) / 17) <= floor ((49 * d + 23) / 17)).
          { apply floor_inc. lra. }
          assert (floor ((49 * d + 23) / 17) <= floor ((49 * d + 57) / 17)).
          { apply floor_inc. lra. }
          lia. } }
      { assert (floor (49 * b / 17) <= floor (49 * (d + log 4 5) / 17)).
        { apply floor_inc. lra. }
        assert (floor (49 * (d + log 4 5) / 17) <= floor ((49 * d + 57) / 17)).
        { apply floor_inc. lra. }
        lia. } }

    destruct (G6 R0 R1 R0_odd R1_even G4 (* R1_non0 *)) as [x [y eq]]. fold b in eq.
    apply divstep_iter_0' with (m:=m) in eq; [|assumption]. destruct eq as [d'' [f'' eq]].
    assert (f''eq : f'' = fn 1 R0 g m).
    { unfold fn. replace g with (R1 / 2) by (unfold R1; rewrite mul_comm, Z_div_mult_full; lia).
      rewrite eq. reflexivity. }

    - repeat split.
      + unfold gn. replace g with (R1 / 2) by (unfold R1; rewrite mul_comm, Z_div_mult_full; lia).
        rewrite eq. reflexivity.
      + rewrite gcdeq.
        rewrite <- f''eq.
        eapply (proj2 (G3 _ _ R0_odd R1_even)). apply eq.
      + assert (2 ^+ m * fn 1 R0 g m = um * R0 + vm * g).
        rewrite Nat.sub_0_r in _911. inversion_mat _911.
        assumption.
        rewrite H1.
        rewrite <- Zplus_mod_idemp_l.
        rewrite <- (Zmult_mod_idemp_r R0). rewrite mod_same.
        rewrite Z.mul_0_r, mod_0_l, Z.add_0_l.  reflexivity. apply odd_nonzero. assumption.
        apply odd_nonzero. assumption.
  Qed.
End __.

author: bshvass

repo: by-inversion

save_path: github-repos/coq/bshvass-by-inversion


text:
Set Warnings "-notation-overridden,-parsing".
From Coq Require Import Bool.Bool.
From Coq Require Import Init.Nat.
From Coq Require Import Arith.Arith.
From Coq Require Import Arith.EqNat.
From Coq Require Import Lia.
From Coq Require Import Lists.List.
From Coq Require Import Strings.String.
Import ListNotations.
From LF Require Import Maps.

Definition state := total_map nat.

Inductive aexp : Type :=
| ANum (n : nat)
| AId (x : string)
| APlus (a1 a2 : aexp)
| AMinus (a1 a2 : aexp)
| AMult (a1 a2 : aexp).

Definition X : string := "X".
Definition Y : string := "Y".
Definition Z : string := "Z".
Definition W : string := "W".

Inductive bexp : Type :=
  | BTrue
  | BFalse
  | BEq (a1 a2 : aexp)
  | BLe (a1 a2 : aexp)
  | BNot (b : bexp)
  | BAnd (b1 b2 : bexp).

Coercion AId : string >-> aexp.
Coercion ANum : nat >-> aexp.

Declare Custom Entry com.
Declare Scope com_scope.
Notation "<{ e }>" := e (at level 0, e custom com at level 99) : com_scope.
Notation "( x )" := x (in custom com, x at level 99) : com_scope.
Notation "x" := x (in custom com at level 0, x constr at level 0) : com_scope.
Notation "f x .. y" := (.. (f x) .. y)
                  (in custom com at level 0, only parsing,
                  f constr at level 0, x constr at level 9,
                  y constr at level 9) : com_scope.
Notation "x + y" := (APlus x y) (in custom com at level 50, left associativity).
Notation "x - y" := (AMinus x y) (in custom com at level 50, left associativity).
Notation "x * y" := (AMult x y) (in custom com at level 40, left associativity).
Notation "'true'"  := true (at level 1).
Notation "'true'"  := BTrue (in custom com at level 0).
Notation "'false'"  := false (at level 1).
Notation "'false'"  := BFalse (in custom com at level 0).
Notation "x <= y" := (BLe x y) (in custom com at level 70, no associativity).
Notation "x = y"  := (BEq x y) (in custom com at level 70, no associativity).
Notation "x && y" := (BAnd x y) (in custom com at level 80, left associativity).
Notation "'~' b"  := (BNot b) (in custom com at level 75, right associativity).

Open Scope com_scope.

Fixpoint aeval (st : state) (a : aexp) : nat :=
  match a with
  | ANum n => n
  | AId x => st x
  | <{a1 + a2}> => (aeval st a1) + (aeval st a2)
  | <{a1 - a2}> => (aeval st a1) - (aeval st a2)
  | <{a1 * a2}> => (aeval st a1) * (aeval st a2)
  end.

Fixpoint beval (st : state) (b : bexp) : bool :=
  match b with
  | <{true}>      => true
  | <{false}>     => false
  | <{a1 = a2}>   => (aeval st a1) =? (aeval st a2)
  | <{a1 <= a2}>  => (aeval st a1) <=? (aeval st a2)
  | <{~ b1}>      => negb (beval st b1)
  | <{b1 && b2}>  => andb (beval st b1) (beval st b2)
  end.

Definition empty_st := (_ !-> 0).
Notation "x '!->' v" := (t_update empty_st x v) (at level 100).

Inductive com : Type :=
| CSkip
| CAss (x : string) (a : aexp)
| CSeq (c1 c2 : com)
| CIf (b : bexp) (c1 c2 : com)
| CWhile (b : bexp) (c : com).

Notation "'skip'"  :=
         CSkip (in custom com at level 0) : com_scope.
Notation "x := y"  :=
         (CAss x y)
            (in custom com at level 0, x constr at level 0,
             y at level 85, no associativity) : com_scope.
Notation "x ; y" :=
         (CSeq x y)
           (in custom com at level 90, right associativity) : com_scope.
Notation "'if' x 'then' y 'else' z 'end'" :=
         (CIf x y z)
           (in custom com at level 89, x at level 99,
            y at level 99, z at level 99) : com_scope.
Notation "'while' x 'do' y 'end'" :=
         (CWhile x y)
            (in custom com at level 89, x at level 99, y at level 99) : com_scope.

Reserved Notation
         "st '=[' c ']=>' st'"
         (at level 40, c custom com at level 99,
          st constr, st' constr at next level).

Inductive ceval : com -> state -> state -> Prop :=
  | E_Skip : forall st,
      st =[ skip ]=> st
  | E_Ass  : forall st a n x,
      aeval st a = n ->
      st =[ x := a ]=> (x !-> n ; st)
  | E_Seq : forall c1 c2 st st' st'',
      st  =[ c1 ]=> st'  ->
      st' =[ c2 ]=> st'' ->
      st  =[ c1 ; c2 ]=> st''
  | E_IfTrue : forall st st' b c1 c2,
      beval st b = true ->
      st =[ c1 ]=> st' ->
      st =[ if b then c1 else c2 end]=> st'
  | E_IfFalse : forall st st' b c1 c2,
      beval st b = false ->
      st =[ c2 ]=> st' ->
      st =[ if b then c1 else c2 end]=> st'
  | E_WhileFalse : forall b st c,
      beval st b = false ->
      st =[ while b do c end ]=> st
  | E_WhileTrue : forall st st' st'' b c,
      beval st b = true ->
      st  =[ c ]=> st' ->
      st' =[ while b do c end ]=> st'' ->
      st  =[ while b do c end ]=> st''

  where "st =[ c ]=> st'" := (ceval c st st').

author: juniorxxue

repo: software-foundations


text:
Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 9593 lines to 104 lines, then from 187 lines to 103 lines, then from 113 lines to 90 lines *)
(* coqc version trunk (October 2014) compiled on Oct 1 2014 18:13:54 with OCaml 4.01.0
   coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (68846802a7be637ec805a5e374655a426b5723a5) *)
Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
Inductive trunc_index := minus_two | trunc_S (_ : trunc_index).
Axiom IsTrunc : trunc_index -> Type -> Type.
Existing Class IsTrunc.
Axiom Contr : Type -> Type.
Inductive Trunc (n : trunc_index) (A :Type) : Type := tr : A -> Trunc n A.
Module NonPrim.
  Unset Primitive Projections.
  Set Implicit Arguments.
  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
  Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
  Unset Implicit Arguments.
  Notation "( x ; y )" := (existT _ x y) : fibration_scope.
  Open Scope fibration_scope.
  Notation pr1 := projT1.
  Notation pr2 := projT2.
  Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
  Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
  Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
  Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :> Contr (Trunc n A).
  Axiom isconnected_elim : forall {n} {A} `{IsConnected n A}
                                  (C : Type) `{IsTrunc n C} (f : A -> C),
                             { c:C & forall a:A, f a = c }.
  Class IsConnMap (n : trunc_index) {A B : Type} (f : A -> B)
    := isconnected_hfiber_conn_map :> forall b:B, IsConnected n (hfiber f b).
  Definition conn_map_elim {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall b:B, P b.
  Proof.
    intros b.
    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
    intro x.
    exact (transport P x.2 (d x.1)).
  Defined.

  Definition conn_map_elim' {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall b:B, P b.
  Proof.
    intros b.
    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
    intros [a p].
    exact (transport P p (d a)).
  Defined.

  Definition conn_map_comp {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall a:A, conn_map_elim f P d (f a) = d a /\ conn_map_elim' f P d (f a) = d a.
  Proof.
    intros a.
    unfold conn_map_elim, conn_map_elim'.
    Set Printing Coercions.
    set (fibermap := fun a0p : hfiber f (f a)
                     => let (a0, p) := a0p in transport P p (d a0)).
    Set Printing Implicit.
    let G := match goal with |- ?G => constr:(G) end in
    first [ match goal with
              | [ |- (@isconnected_elim n (@hfiber A B f (f a))
                                        (@isconnected_hfiber_conn_map n A B f H (f a))
                                        (P (f a)) (HP (f a))
                                        (fun x : @hfiber A B f (f a) =>
                                           @transport B P (f x.1) (f a) x.2 (d x.1))).1 =
                     d a /\ _ ] => idtac
            end
          | fail 1 "projection names should be folded, [let] should generate unfolded projections, goal:" G ];
      first [ match goal with
                | [ |- _ /\ (@isconnected_elim n (@hfiber A B f (f a))
                                               (@isconnected_hfiber_conn_map n A B f H (f a))
                                               (P (f a)) (HP (f a)) fibermap).1 = d a ] => idtac
              end
            | fail 1 "destruct should generate unfolded projections, as should [let], goal:" G ].
    admit.
  Defined.
End NonPrim.

Module Prim.
  Set Primitive Projections.
  Set Implicit Arguments.
  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
  Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
  Unset Implicit Arguments.
  Notation "( x ; y )" := (existT _ x y) : fibration_scope.
  Open Scope fibration_scope.
  Notation pr1 := projT1.
  Notation pr2 := projT2.
  Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
  Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
  Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
  Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :> Contr (Trunc n A).
  Axiom isconnected_elim : forall {n} {A} `{IsConnected n A}
                                  (C : Type) `{IsTrunc n C} (f : A -> C),
                             { c:C & forall a:A, f a = c }.
  Class IsConnMap (n : trunc_index) {A B : Type} (f : A -> B)
    := isconnected_hfiber_conn_map :> forall b:B, IsConnected n (hfiber f b).
  Definition conn_map_elim {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall b:B, P b.
  Proof.
    intros b.
    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
    intro x.
    exact (transport P x.2 (d x.1)).
  Defined.

  Definition conn_map_elim' {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall b:B, P b.
  Proof.
    intros b.
    unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))).
    intros [a p].
    exact (transport P p (d a)).
  Defined.

  Definition conn_map_comp {n : trunc_index}
             {A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
             (P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
             (d : forall a:A, P (f a))
  : forall a:A, conn_map_elim f P d (f a) = d a /\ conn_map_elim' f P d (f a) = d a.
  Proof.
    intros a.
    unfold conn_map_elim, conn_map_elim'.
    Set Printing Coercions.
    set (fibermap := fun a0p : hfiber f (f a)
                     => let (a0, p) := a0p in transport P p (d a0)).
    Set Printing Implicit.
    let G := match goal with |- ?G => constr:(G) end in
    first [ match goal with
              | [ |- (@isconnected_elim n (@hfiber A B f (f a))
                                        (@isconnected_hfiber_conn_map n A B f H (f a))
                                        (P (f a)) (HP (f a))
                                        (fun x : @hfiber A B f (f a) =>
                                           @transport B P (f x.1) (f a) x.2 (d x.1))).1 =
                     d a /\ _ ] => idtac
            end
          | fail 1 "projection names should be folded, [let] should generate unfolded projections, goal:" G ];
      first [ match goal with
                | [ |- _ /\ (@isconnected_elim n (@hfiber A B f (f a))
                                               (@isconnected_hfiber_conn_map n A B f H (f a))
                                               (P (f a)) (HP (f a)) fibermap).1 = d a ] => idtac
              end
            | fail 1 "destruct should generate unfolded projections, as should [let], goal:" G ].
    admit.
  Defined.
End Prim.

author: princeton-vl

repo: CoqGym

save_path: github-repos/coq/princeton-vl-CoqGym


text:
Require Import Functor.

Record naturalTrans f g `{Functor f, Functor g} := mkNaturalTrans
{ runNaturalTrans : forall X, f X -> g X }.
Notation "f ~> g" := (naturalTrans f g) (at level 50, left associativity).
Arguments mkNaturalTrans [f g _ _].
Arguments runNaturalTrans [f g _ _] _ [X].

Record naturalTransDec f g `{Functor f, Functor g} (φ : f ~> g) :=
{ naturalTrans_comm :
    forall A B (fa : f A) (g : A -> B),
      runNaturalTrans φ (fmap g fa) = fmap g (runNaturalTrans φ fa)
}.

Definition composeNaturalTrans {f g h : Type -> Type}
                              `{Functor f, Functor g, Functor h}
                               (nt1 : g ~> h) (nt2 : f ~> g) : f ~> h :=
  mkNaturalTrans (fun _ fx => runNaturalTrans nt1 (runNaturalTrans nt2 fx)).
Notation "f • g" := (composeNaturalTrans f g) (at level 40, left associativity).

author: hablapps

repo: koky

save_path: github-repos/coq/hablapps-koky


text:
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.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.
Require Import UniMath.Bicategories.Core.Univalence.
Require Import UniMath.Bicategories.Core.BicategoryLaws.
Require Import UniMath.Bicategories.Core.Unitors.
Require Import UniMath.Bicategories.Limits.Products.
Import Products.Notations.
Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat.
Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor.
Import PseudoFunctor.Notations.

Section ConstProdPsfunctor.
  Context (B : bicat_with_binprod)
          (x : B).

  Definition const_prod_psfunctor_data
    : psfunctor_data B B.
  Proof.
    use make_psfunctor_data.
    - exact (λ y, y ⊗ x).
    - exact (λ y₁ y₂ f,  f ⊗₁ id₁ x).
    - exact (λ y₁ y₂ f g α, α ⊗₂ id₂ _).
    - exact (λ y, (pair_1cell_id_id_invertible B _ _)^-1).
    - exact (λ y₁ y₂ y₃ f g,
             pair_1cell_comp_invertible
               B
               f g
               (id₁ x) (id₁ x)
             • (id₂ _ ⊗₂ lunitor _)).
  Defined.

  Definition const_prod_psfunctor_laws
    : psfunctor_laws const_prod_psfunctor_data.
  Proof.
    repeat split.
    - intro ; intros ; cbn.
      apply pair_2cell_id_id.
    - intro ; intros ; cbn.
      refine (_ @ pair_2cell_comp _ _ _ _ _).
      rewrite id2_left.
      apply idpath.
    - intro ; intros ; cbn.
      refine (binprod_lunitor _ _ _ @ _).
      rewrite !vassocl.
      do 2 apply maponpaths.
      rewrite <- pair_2cell_comp.
      rewrite id2_left, id2_right.
      apply idpath.
    - intro ; intros ; cbn.
      refine (binprod_runitor _ _ _ @ _).
      rewrite !vassocl.
      do 2 apply maponpaths.
      rewrite <- pair_2cell_comp.
      rewrite id2_left, id2_right.
      rewrite runitor_lunitor_identity.
      apply idpath.
    - intro ; intros ; cbn.
      rewrite <- !lwhisker_vcomp, <- !rwhisker_vcomp.
      rewrite !vassocl.
      use binprod_ump_2cell_unique_alt.
      + apply (pr2 B).
      + rewrite <- !rwhisker_vcomp.
        use (vcomp_lcancel (lassociator _ _ _)) ; [ is_iso | ].
        etrans.
        {
          rewrite !vassocr.
          rewrite <- rwhisker_lwhisker.
          rewrite !vassocl.
          etrans.
          {
            apply maponpaths_2.
            apply maponpaths.
            apply binprod_ump_2cell_pr1.
          }
          rewrite !vassocl.
          apply maponpaths.
          rewrite !vassocr.
          rewrite <- rwhisker_lwhisker.
          rewrite !vassocl.
          etrans.
          {
            apply maponpaths_2.
            apply maponpaths.
            apply pair_2cell_pr1.
          }
          rewrite !vassocl.
          rewrite lwhisker_id2.
          rewrite id2_left.
          apply maponpaths.
          apply maponpaths.
          etrans.
          {
            apply maponpaths_2.
            apply binprod_ump_2cell_pr1.
          }
          apply maponpaths.
          etrans.
          {
            apply maponpaths_2.
            apply pair_2cell_pr1.
          }
          rewrite lwhisker_id2, id2_right.
          apply maponpaths.
          apply pair_2cell_pr1.
        }
        etrans.
        {
          rewrite !vassocr.
          rewrite lwhisker_vcomp.
          rewrite !vassocl.
          etrans.
          {
            apply maponpaths.
            rewrite !vassocr.
            rewrite lassociator_rassociator.
            rewrite id2_left.
            rewrite !vassocl.
            do 6 apply maponpaths.
            rewrite !vassocr.
            rewrite vcomp_linv.
            rewrite id2_left.
            apply idpath.
          }
          rewrite !vassocr.
          rewrite lwhisker_vcomp.
          rewrite !vassocl.
          unfold pair_1cell_pr1.
          rewrite vcomp_linv, id2_right.
          rewrite vcomp_linv, id2_right.
          do 4 apply maponpaths.
          rewrite !vassocr.
          rewrite vcomp_linv.
          rewrite id2_left.
          apply idpath.
        }
        rewrite <- lwhisker_vcomp.
        rewrite !vassocl.
        use vcomp_move_R_pM ; [ is_iso | ] ; cbn.
        refine (!_).
        etrans.
        {
          rewrite !vassocr.
          rewrite lassociator_lassociator.
          rewrite !vassocl.
          apply idpath.
        }
        etrans.
        {
          rewrite !vassocr.
          apply maponpaths.
          apply pair_2cell_pr1.
        }
        rewrite !vassocr.
        apply maponpaths_2.
        rewrite lwhisker_id2, id2_right.
        rewrite !vassocl.
        etrans.
        {
          do 4 apply maponpaths.
          apply maponpaths_2.
          apply binprod_ump_2cell_pr1.
        }
        unfold pair_1cell_pr1.
        rewrite !vassocl.
        rewrite vcomp_linv, id2_right.
        etrans.
        {
          do 3 apply maponpaths.
          rewrite !vassocr.
          rewrite rwhisker_rwhisker_alt.
          rewrite !vassocl.
          apply maponpaths.
          rewrite !vassocr.
          rewrite vcomp_whisker.
          rewrite !vassocl.
          apply maponpaths.
          rewrite !vassocr.
          rewrite <- rwhisker_rwhisker.
          rewrite !vassocl.
          apply maponpaths.
          etrans.
          {
            apply maponpaths_2.
            apply maponpaths.
            apply pair_2cell_pr1.
          }
          rewrite lwhisker_id2, id2_right.
          rewrite !vassocr.
          rewrite rwhisker_vcomp.
          rewrite !vassocl.
          rewrite vcomp_linv.
          rewrite id2_right.
          apply idpath.
        }
        etrans.
        {
          do 2 apply maponpaths.
          rewrite !vassocr.
          rewrite rwhisker_rwhisker_alt.
          rewrite !vassocl.
          apply maponpaths.
          rewrite !vassocr.
          rewrite vcomp_whisker.
          rewrite !vassocl.
          apply maponpaths.
          rewrite !vassocr.
          rewrite <- rwhisker_rwhisker.
          rewrite !vassocl.
          apply maponpaths.
          etrans.
          {
            apply maponpaths_2.
            apply maponpaths.
            apply binprod_ump_2cell_pr1.
          }
          rewrite !vassocr.
          rewrite rwhisker_vcomp.
          rewrite !vassocl.
          rewrite vcomp_linv.
          rewrite id2_right.
          apply idpath.
        }
        rewrite <- !rwhisker_vcomp.
        rewrite !vassocr.
        use vcomp_move_L_Mp ; [ is_iso | ] ; cbn.
        rewrite !vassocl.
        etrans.
        {
          do 9 apply maponpaths.
          rewrite !vassocr.
          rewrite rassociator_rassociator.
          apply idpath.
        }
        rewrite !vassocr.
        apply maponpaths_2.
        rewrite !vassocl.
        rewrite rwhisker_rwhisker_alt.
        rewrite !vassocr.
        apply maponpaths_2.
        use vcomp_move_R_Mp ; [ is_iso | ] ; cbn.
        rewrite !vassocl.
        rewrite <- lassociator_lassociator.
        rewrite !vassocr.
        apply maponpaths_2.
        rewrite lwhisker_vcomp.
        rewrite !vassocl.
        rewrite rassociator_lassociator.
        rewrite id2_right.
        rewrite !vassocr.
        use vcomp_move_L_Mp ; [ is_iso | ] ; cbn.
        rewrite !vassocl.
        rewrite <- rwhisker_lwhisker_rassociator.
        rewrite !vassocr.
        rewrite <- !lwhisker_vcomp.
        apply maponpaths_2.
        use vcomp_move_L_Mp ; [ is_iso | ] ; cbn.
        rewrite !vassocl.
        etrans.
        {
          do 5 apply maponpaths.
          rewrite !vassocr.
          rewrite rassociator_rassociator.
          apply idpath.
        }
        etrans.
        {
          do 4 apply maponpaths.
          rewrite !vassocr.
          rewrite lassociator_rassociator.
          apply id2_left.
        }
        rewrite <- lwhisker_lwhisker_rassociator.
        rewrite !vassocr.
        refine (_ @ id2_left _).
        apply maponpaths_2.
        rewrite !vassocl.
        etrans.
        {
          apply maponpaths.
          rewrite !vassocr.
          rewrite lassociator_rassociator.
          apply id2_left.
        }
        apply lassociator_rassociator.
      + rewrite <- !rwhisker_vcomp.
        etrans.
        {
          do 4 apply maponpaths.
          apply pair_2cell_pr2.
        }
        refine (!_).
        etrans.
        {
          do 4 apply maponpaths.
          apply pair_2cell_pr2.
        }
        rewrite !vassocr.
        apply maponpaths_2.
        rewrite lwhisker_id2.
        rewrite id2_right.
        rewrite !vassocl.
        etrans.
        {
          do 3 apply maponpaths.
          apply maponpaths_2.
          apply binprod_ump_2cell_pr2.
        }
        rewrite !vassocl.
        refine (!_).
        etrans.
        {
          do 3 apply maponpaths.
          apply maponpaths_2.
          apply pair_2cell_pr2.
        }
        rewrite !vassocl.
        rewrite vcomp_linv.
        rewrite id2_right.
        rewrite !vassocr.
        apply maponpaths_2.
        rewrite !vassocl.
        etrans.
        {
          do 2 apply maponpaths.
          apply maponpaths_2.
          apply binprod_ump_2cell_pr2.
        }
        rewrite !vassocl.
        etrans.
        {
          apply maponpaths.
          rewrite !vassocr.
          rewrite <- rwhisker_lwhisker_rassociator.
          rewrite !vassocl.
          apply idpath.
        }
        etrans.
        {
          rewrite !vassocr.
          rewrite <- rwhisker_lwhisker_rassociator.
          rewrite !vassocl.
          apply maponpaths.
          apply maponpaths_2.
          apply maponpaths.
          apply binprod_ump_2cell_pr2.
        }
        rewrite !vassocl.
        refine (!_).
        etrans.
        {
          do 2 apply maponpaths.
          rewrite !vassocr.
          rewrite rwhisker_rwhisker_alt.
          rewrite !vassocl.
          apply maponpaths.
          rewrite !vassocr.
          rewrite vcomp_whisker.
          rewrite !vassocl.
          apply maponpaths.
          rewrite !vassocr.
          rewrite <- rwhisker_rwhisker.
          rewrite !vassocl.
          apply maponpaths.
          apply maponpaths_2.
          apply maponpaths.
          apply pair_2cell_pr2.
        }
        etrans.
        {
          apply maponpaths.
          rewrite !vassocr.
          rewrite rwhisker_rwhisker_alt.
          rewrite !vassocl.
          apply maponpaths.
          rewrite !vassocr.
          rewrite vcomp_whisker.
          rewrite !vassocl.
          apply maponpaths.
          rewrite !vassocr.
          rewrite <- rwhisker_rwhisker.
          rewrite !vassocl.
          apply maponpaths.
          apply maponpaths_2.
          apply maponpaths.
          apply binprod_ump_2cell_pr2.
        }
        rewrite !vassocl.
        use vcomp_move_R_pM ; [ is_iso | ] ; cbn.
        refine (!_).
        rewrite <- lwhisker_vcomp.
        etrans.
        {
          rewrite !vassocr.
          rewrite rassociator_rassociator.
          rewrite !vassocl.
          apply idpath.
        }
        apply maponpaths.
        rewrite <- lwhisker_vcomp.
        etrans.
        {
          rewrite !vassocr.
          rewrite lwhisker_lwhisker_rassociator.
          rewrite !vassocl.
          apply idpath.
        }
        apply maponpaths.
        use vcomp_move_R_pM ; [ is_iso | ] ; cbn.
        rewrite !vassocr.
        rewrite <- lassociator_lassociator.
        rewrite !vassocl.
        rewrite <- lwhisker_vcomp.
        rewrite !vassocl.
        apply maponpaths.
        refine (!_).
        etrans.
        {
          apply maponpaths.
          rewrite !vassocr.
          rewrite rwhisker_vcomp.
          rewrite !vassocr.
          rewrite lassociator_rassociator.
          rewrite id2_left.
          rewrite !vassocl.
          apply idpath.
        }
        use vcomp_move_R_pM ; [ is_iso | ] ; cbn.
        refine (!_).
        etrans.
        {
          rewrite <- lwhisker_vcomp.
          rewrite !vassocr.
          rewrite rwhisker_lwhisker_rassociator.
          rewrite !vassocl.
          apply idpath.
        }
        rewrite <- !rwhisker_vcomp.
        rewrite !vassocl.
        apply maponpaths.
        use vcomp_move_L_pM ; [ is_iso | ] ; cbn.
        etrans.
        {
          rewrite <- lwhisker_vcomp.
          rewrite !vassocr.
          rewrite rassociator_rassociator.
          rewrite !vassocl.
          apply idpath.
        }
        unfold pair_1cell_pr2.
        rewrite !vcomp_linv, id2_right.
        rewrite !vassocr.
        apply maponpaths_2.
        rewrite !vassocl.
        rewrite rwhisker_vcomp.
        rewrite vcomp_linv.
        rewrite id2_rwhisker.
        rewrite id2_right.
        refine (!_).
        etrans.
        {
          do 2 apply maponpaths.
          rewrite !vassocr.
          rewrite rwhisker_vcomp.
          rewrite vcomp_linv.
          rewrite id2_rwhisker.
          apply id2_left.
        }
        refine (!_).
        etrans.
        {
          do 3 apply maponpaths.
          apply maponpaths_2.
          apply maponpaths.
          apply pair_2cell_pr2.
        }
        etrans.
        {
          do 2 apply maponpaths.
          rewrite !vassocr.
          rewrite !lwhisker_vcomp.
          rewrite !vassocr.
          rewrite vcomp_linv.
          rewrite id2_left.
          rewrite !vassocl.
          rewrite vcomp_linv.
          rewrite id2_right.
          apply idpath.
        }
        etrans.
        {
          do 2 apply maponpaths.
          rewrite !vassocr.
          rewrite lwhisker_lwhisker.
          rewrite !vassocl.
          rewrite <- vcomp_whisker.
          apply idpath.
        }
        etrans.
        {
          apply maponpaths.
          rewrite !vassocr.
          rewrite rassociator_lassociator.
          rewrite id2_left.
          apply idpath.
        }
        rewrite !vassocr.
        rewrite <- rwhisker_rwhisker_alt.
        rewrite !vassocl.
        apply maponpaths.
        rewrite lunitor_lwhisker.
        rewrite rwhisker_vcomp.
        apply maponpaths.
        rewrite lunitor_runitor_identity.
        rewrite runitor_triangle.
        apply idpath.
    - intro ; intros ; cbn.
      rewrite !vassocl.
      rewrite <- pair_2cell_comp.
      rewrite id2_left, id2_right.
      rewrite !vassocr.
      rewrite <- binprod_lwhisker.
      rewrite !vassocl.
      apply maponpaths.
      rewrite <- pair_2cell_comp.
      rewrite lwhisker_id2, id2_left, id2_right.
      apply idpath.
    - intro ; intros ; cbn.
      rewrite !vassocl.
      rewrite <- pair_2cell_comp.
      rewrite id2_left, id2_right.
      rewrite !vassocr.
      rewrite <- binprod_rwhisker.
      rewrite !vassocl.
      apply maponpaths.
      rewrite <- pair_2cell_comp.
      rewrite id2_rwhisker, id2_left, id2_right.
      apply idpath.
  Qed.

  Definition const_prod_psfunctor_invertible_cells
    : invertible_cells const_prod_psfunctor_data.
  Proof.
    split.
    - intro y.
      apply is_invertible_2cell_inv.
    - intros y₁ y₂ y₃ f g ; cbn.
      is_iso.
      + apply binprod_ump_2cell_invertible.
        * is_iso.
          ** apply property_from_invertible_2cell.
          ** apply property_from_invertible_2cell.
        * is_iso.
          ** apply property_from_invertible_2cell.
          ** apply property_from_invertible_2cell.
      + apply binprod_ump_2cell_invertible.
        * is_iso.
          apply property_from_invertible_2cell.
        * is_iso.
          apply property_from_invertible_2cell.
  Defined.

  Definition const_prod_psfunctor
    : psfunctor B B.
  Proof.
    use make_psfunctor.
    - exact const_prod_psfunctor_data.
    - exact const_prod_psfunctor_laws.
    - exact const_prod_psfunctor_invertible_cells.
  Defined.
End ConstProdPsfunctor.

author: UniMath

repo: UniMath

save_path: github-repos/coq/UniMath-UniMath


text:
Require Export FMG.

Section Free.

Definition FMG_functor_fun {X Y : Type} {T_X : IsHSet X} {T_Y : IsHSet Y}
  (h : X -> Y)
  : FMG X -> FMG Y
  := FMG_rec X (FMG Y) e (iota o h) m alpha lambda rho pentagon triangle T_FMG.

Definition FMG_functor_fun_alpha {X Y : Type} {T_X : IsHSet X} {T_Y : IsHSet Y}
  (h : X -> Y) (a b c : FMG X)
  : ap (FMG_functor_fun h) (alpha a b c) = alpha (FMG_functor_fun h a) (FMG_functor_fun h b) (FMG_functor_fun h c)
  := @FMG_rec_beta_alpha X (FMG Y) e (iota o h) m alpha lambda rho pentagon triangle T_FMG a b c.
Definition FMG_functor_fun_lambda {X Y : Type} {T_X : IsHSet X} {T_Y : IsHSet Y}
  (h : X -> Y) (b : FMG X)
  : ap (FMG_functor_fun h) (lambda b) = lambda (FMG_functor_fun h b)
  := @FMG_rec_beta_lambda X (FMG Y) e (iota o h) m alpha lambda rho pentagon triangle T_FMG b.
Definition FMG_functor_fun_rho {X Y : Type} {T_X : IsHSet X} {T_Y : IsHSet Y}
  (h : X -> Y) (a : FMG X)
  : ap (FMG_functor_fun h) (rho a) = rho (FMG_functor_fun h a)
  := @FMG_rec_beta_rho X (FMG Y) e (iota o h) m alpha lambda rho pentagon triangle T_FMG a.

Definition FMG_functor_arr
  : forall (X Y : Type) (T_X : IsHSet X) (T_Y : IsHSet Y), (X -> Y) -> MonoidalFunctor (FMG_MG X) (FMG_MG Y).
Proof.
  intros ???? h.
  srapply @Build_MonoidalFunctor.
  + exact (FMG_functor_fun h).
  + constructor.
  + constructor.
  + intros; simpl.
    refine (concat_p1 _ @ _ @ (concat_1p _)^).
    exact (FMG_functor_fun_alpha h a b c)^.
  + intros; simpl.
    refine (_ @ (concat_1p _)^).
    exact (FMG_functor_fun_lambda h b)^.
  + intros; simpl.
    refine (_ @ (concat_1p _)^).
    exact (FMG_functor_fun_rho h a)^.
Defined.

Definition FMG_functor_id
  : forall (X : Type) (T_X : IsHSet X),
    MonoidalNatIso (FMG_functor_arr X X T_X T_X idmap) (MonoidalFunctor_id (FMG_MG X)).
Proof.
  intros; srapply @Build_MonoidalNatIso; simpl.
  + unfold pointwise_paths. srefine (FMG_ind_to_paths_in_gpd _ _ _ _ _ _ _ _ _ _ T_FMG); simpl.
    - constructor.
    - constructor.
    - intros ?? IHa IHb.
      exact (mm IHa IHb).
    - intros ??? IHa IHb IHc; simpl.
      refine (whiskerL _ (ap_idmap _) @ _ @ whiskerR (FMG_functor_fun_alpha idmap a b c)^ _).
      exact (@alpha_natural (FMG_MG X) _ _ _ _ _ _ IHa IHb IHc)^.
    - intros ? IHb; simpl.
      refine (whiskerL _ (ap_idmap _) @ _ @ whiskerR (FMG_functor_fun_lambda idmap b)^ _).
      exact (@lambda_natural (FMG_MG X) _ _ IHb)^.
    - intros ? IHa; simpl.
      refine (whiskerL _ (ap_idmap _) @ _ @ whiskerR (FMG_functor_fun_rho idmap a)^ _).
      exact (@rho_natural (FMG_MG X) _ _ IHa)^.
  + constructor.
  + intros; simpl.
    refine (concat_1p _ @ (concat_p1 _)^).
Defined.

Definition FMG_functor_comp
  : forall (X Y Z : Type) (T_X : IsHSet X) (T_Y : IsHSet Y) (T_Z : IsHSet Z) (g : Y -> Z) (f : X -> Y),
    MonoidalNatIso
      (MonoidalFunctor_comp (FMG_functor_arr Y Z T_Y T_Z g) (FMG_functor_arr X Y T_X T_Y f))
      (FMG_functor_arr X Z T_X T_Z (fun x : X => g (f x))).
Proof.
  intros; srapply @Build_MonoidalNatIso; simpl.
  + unfold pointwise_paths. srefine (FMG_ind_to_paths_in_gpd _ _ _ _ _ _ _ _ _ _ T_FMG); simpl.
    - constructor.
    - constructor.
    - intros ?? IHa IHb.
      exact (mm IHa IHb).
    - abstract (intros ??? IHa IHb IHc; simpl;
      refine (_ @ whiskerR (ap_compose (FMG_functor_fun f) (FMG_functor_fun g) _)^ _);
      refine (whiskerL _ (FMG_functor_fun_alpha (g o f) a b c) @ _);
      refine ((@alpha_natural (FMG_MG Z) _ _ _ _ _ _ IHa IHb IHc)^ @ _);
      exact (whiskerR ((FMG_functor_fun_alpha g _ _ _)^ @ ap (ap (FMG_functor_fun g)) (FMG_functor_fun_alpha f a b c)^) _))
        using FMG_functor_comp_alpha.
    - abstract (intros ? IHb; simpl;
      refine (_ @ whiskerR (ap_compose (FMG_functor_fun f) (FMG_functor_fun g) _)^ _);
      refine (whiskerL _ (FMG_functor_fun_lambda (g o f) b) @ _);
      refine ((@lambda_natural (FMG_MG Z) _ _ IHb)^ @ _);
      exact (whiskerR ((FMG_functor_fun_lambda g _)^ @ ap (ap (FMG_functor_fun g)) (FMG_functor_fun_lambda f b)^) _))
        using FMG_functor_comp_lambda.
    - abstract (intros ? IHa; simpl;
      refine (_ @ whiskerR (ap_compose (FMG_functor_fun f) (FMG_functor_fun g) _)^ _);
      refine (whiskerL _ (FMG_functor_fun_rho (g o f) a) @ _);
      refine ((@rho_natural (FMG_MG Z) _ _ IHa)^ @ _);
      exact (whiskerR ((FMG_functor_fun_rho g _)^ @ ap (ap (FMG_functor_fun g)) (FMG_functor_fun_rho f a)^) _))
        using FMG_functor_comp_rho.
  + constructor.
  + intros; simpl.
    refine (concat_1p _ @ (concat_p1 _)^).
Defined.

Definition FMG_functor
  : IsFunctor (fun X T_X => FMG_MG X)
  := Build_IsFunctor (fun X T_X => FMG_MG X) FMG_functor_arr FMG_functor_id FMG_functor_comp.

Definition phi {X : Type} {T_X : IsHSet X} {M : MonoidalGroupoid}
  (F : MonoidalFunctor (FMG_MG X) M)
  : X -> M
  := @mg_f _ _ F o iota.

Lemma phi_natural_M {X : Type} {T_X : IsHSet X} {M : MonoidalGroupoid}
  (F : MonoidalFunctor (FMG_MG X) M)
  {N : MonoidalGroupoid} (H : MonoidalFunctor M N)
  : H o phi F == phi (MonoidalFunctor_comp H F).
Proof.
  constructor.
Defined.

Definition psi_fun {X : Type} {T_X : IsHSet X} {M : MonoidalGroupoid}
  (f : X -> M)
  : FMG X -> M
  := @FMG_rec X M mg_e f mg_m mg_alpha mg_lambda mg_rho mg_pentagon mg_triangle mgtrunc.

Definition psi_fun_alpha {X : Type} {T_X : IsHSet X} {M : MonoidalGroupoid}
  (f : X -> M) (a b c : FMG_MG X)
  : ap (psi_fun f) (mg_alpha a b c) = mg_alpha (psi_fun f a) (psi_fun f b) (psi_fun f c)
  := FMG_rec_beta_alpha X M mg_e f mg_m mg_alpha mg_lambda mg_rho mg_pentagon mg_triangle mgtrunc a b c.
Definition psi_fun_lambda {X : Type} {T_X : IsHSet X} {M : MonoidalGroupoid}
  (f : X -> M) (b : FMG_MG X)
  : ap (psi_fun f) (mg_lambda b) = mg_lambda (psi_fun f b)
  := FMG_rec_beta_lambda X M mg_e f mg_m mg_alpha mg_lambda mg_rho mg_pentagon mg_triangle mgtrunc b.
Definition psi_fun_rho {X : Type} {T_X : IsHSet X} {M : MonoidalGroupoid}
  (f : X -> M) (a : FMG_MG X)
  : ap (psi_fun f) (mg_rho a) = mg_rho (psi_fun f a)
  := FMG_rec_beta_rho X M mg_e f mg_m mg_alpha mg_lambda mg_rho mg_pentagon mg_triangle mgtrunc a.

Definition psi {X : Type} {T_X : IsHSet X} {M : MonoidalGroupoid}
  (f : X -> M)
  : MonoidalFunctor (FMG_MG X) M.
Proof.
  srapply @Build_MonoidalFunctor.
  + simpl. exact (psi_fun f).
  + constructor.
  + constructor.
  + intros; simpl.
    refine (concat_p1 _ @ _^ @ (concat_1p _)^).
    exact (psi_fun_alpha f a b c).
  + intros; simpl.
    refine (_^ @ (concat_1p _)^).
    exact (psi_fun_lambda f b).
  + intros; simpl.
    refine (_^ @ (concat_1p _)^).
    exact (psi_fun_rho f a).
Defined.

  Lemma psi_natural_X_homotopy {X : Type} {T_X : IsHSet X} {M : MonoidalGroupoid}
    (f : X -> M)
    {Y : Type} {T_Y : IsHSet Y} (h : Y -> X)
    : MonoidalFunctor_comp (psi f) (FMG_functor_arr Y X T_Y T_X h) == psi (f o h).
  Proof.
    simpl; unfold pointwise_paths.
    srefine (FMG_ind_to_paths_in_gpd Y M (psi f o FMG_functor_fun h) (psi (f o h)) _ _ _ _ _ _ mgtrunc).
    + constructor.
    + constructor.
    + intros a b a' b'.
      change (mg_m ((psi f o FMG_functor_fun h) a) ((psi f o FMG_functor_fun h) b) = mg_m (psi (f o h) a) (psi (f o h) b)).
      exact (ap011 mg_m a' b').
    + hnf. intros.
      refine (_ @ whiskerR (ap_compose (FMG_functor_fun h) (psi f) (alpha a b c))^ _).
      refine (whiskerL _ (psi_fun_alpha (f o h) a b c) @ _).
      refine (_ @ whiskerR (ap (ap (psi f)) (FMG_functor_fun_alpha h a b c))^ _).
      refine (_ @ whiskerR (psi_fun_alpha f (FMG_functor_fun h a) (FMG_functor_fun h b) (FMG_functor_fun h c))^ _).
      exact (alpha_natural a' b' c')^.
    + intros; hnf.
      refine (_ @ whiskerR (ap_compose (FMG_functor_fun h) (psi f) (lambda b))^ _).
      refine (whiskerL _ (psi_fun_lambda (f o h) b) @ _).
      refine (_ @ whiskerR (ap (ap (psi f)) (FMG_functor_fun_lambda h b))^ _).
      refine (_ @ whiskerR (psi_fun_lambda f (FMG_functor_fun h b))^ _).
      exact (lambda_natural b')^.
    + intros; hnf.
      refine (_ @ whiskerR (ap_compose (FMG_functor_fun h) (psi f) (rho a))^ _).
      refine (whiskerL _ (psi_fun_rho (f o h) a) @ _).
      refine (_ @ whiskerR (ap (ap (psi f)) (FMG_functor_fun_rho h a))^ _).
      refine (_ @ whiskerR (psi_fun_rho f (FMG_functor_fun h a))^ _).
      exact (rho_natural a')^.
  Defined.

Lemma psi_natural_X {X : Type} {T_X : IsHSet X} {M : MonoidalGroupoid}
  (f : X -> M)
  {Y : Type} {T_Y : IsHSet Y} (h : Y -> X)
  : MonoidalNatIso (MonoidalFunctor_comp (psi f) (FMG_functor_arr Y X T_Y T_X h)) (psi (f o h)).
Proof.
  srapply @Build_MonoidalNatIso.
  + exact (psi_natural_X_homotopy f h).
  + constructor.
  + intros; simpl.
    refine (concat_1p _ @ (concat_p1 _)^).
Defined.

Lemma theta (X : Type) (T_X : IsHSet X) (M : MonoidalGroupoid)
  : phi o psi == idmap.
Proof.
  constructor.
Defined.

  Lemma chi_homotopy_alpha (X : Type) (T_X : IsHSet X) (M : MonoidalGroupoid)
    (F : MonoidalFunctor (FMG_MG X) M)
    (a b c : FMG X)
    (a' : psi_fun (phi F) a = F a)
    (b' : psi_fun (phi F) b = F b)
    (c' : psi_fun (phi F) c = F c)
    : (ap011 mg_m (ap011 mg_m a' b' @ @mg_f2 (FMG_MG X) M F a b) c' @ @mg_f2 (FMG_MG X) M F (m a b) c) @ ap F (alpha a b c)
      = ap (psi_fun (phi F)) (alpha a b c) @ (ap011 mg_m a' (ap011 mg_m b' c' @ @mg_f2 (FMG_MG X) M F b c) @ @mg_f2 (FMG_MG X) M F a (m b c)).
  Proof.
    refine (_ @ whiskerR (psi_fun_alpha (phi F) a b c)^ _).
    refine (whiskerR (whiskerR (ap011_pqp1 mg_m (ap011 mg_m a' b') (@mg_f2 (FMG_MG X) M F a b) c')^ _ @ concat_pp_p _ _ _) _ @ concat_pp_p _ _ _ @ _).
    refine (_ @ concat_pp_p _ _ _ @ whiskerL _ (concat_p_pp _ _ _ @ whiskerR (ap011_pq1q mg_m a' (ap011 mg_m b' c') (@mg_f2 (FMG_MG X) M F b c)) _)).
    refine (_ @ whiskerR (alpha_natural a' b' c')^ _).
    refine (_ @ concat_p_pp _ _ _); apply whiskerL;
    exact (@mg_dalpha _ _ F a b c)^.
  Qed.

  Lemma chi_homotopy_lambda (X : Type) (T_X : IsHSet X) (M : MonoidalGroupoid)
    (F : MonoidalFunctor (FMG_MG X) M)
    (b : FMG X)
    (b' : psi_fun (phi F) b = F b)
    : (ap011 mg_m mg_f0 b' @ @mg_f2 (FMG_MG X) M F e b) @ ap F (lambda b) = ap (psi_fun (phi F)) (lambda b) @ b'.
  Proof.
    refine (_ @ whiskerR (psi_fun_lambda (phi F) b)^ _).
    refine (concat_pp_p _ _ _ @ whiskerR (ap011_1qp1 mg_m mg_f0 b')^ _ @ _).
    refine (concat_pp_p _ _ _ @ whiskerL _ (concat_p_pp _ _ _ @ (@mg_dlambda _ _ F b)^) @ _).
    exact (lambda_natural b')^.
  Qed.

  Lemma chi_homotopy_rho (X : Type) (T_X : IsHSet X) (M : MonoidalGroupoid)
    (F : MonoidalFunctor (FMG_MG X) M)
    (a : FMG X)
    (a' : psi_fun (phi F) a = F a)
    : (ap011 mg_m a' mg_f0 @ @mg_f2 (FMG_MG X) M F a e) @ ap F (rho a) = ap (psi_fun (phi F)) (rho a) @ a'.
  Proof.
    refine (_ @ whiskerR (psi_fun_rho (phi F) a)^ _).
    refine (concat_pp_p _ _ _ @ whiskerR (ap011_p11q mg_m a' mg_f0)^ _ @ _).
    refine (concat_pp_p _ _ _ @ whiskerL _ (concat_p_pp _ _ _ @ (@mg_drho _ _ F a)^) @ _).
    exact (rho_natural a')^.
  Qed.

  Lemma chi_homotopy (X : Type) (T_X : IsHSet X) (M : MonoidalGroupoid)
    (F : MonoidalFunctor (FMG_MG X) M)
    : psi (phi F) == F.
  Proof.
    simpl; unfold pointwise_paths.
    srefine (@FMG_ind_to_paths_in_gpd X M (psi_fun (phi F)) F _ _ _ _ _ _ mgtrunc).
    + change (mg_e = F e). exact mg_f0.
    + constructor.
    + intros a b a' b'. change (mg_m (psi_fun (phi F) a) (psi_fun (phi F) b) = F (m a b)).
      exact (ap011 mg_m a' b' @ @mg_f2 (FMG_MG X) M F a b).
    + intros; hnf.
      exact (chi_homotopy_alpha X T_X M F a b c a' b' c').
    + intros; hnf.
      exact (chi_homotopy_lambda X T_X M F b b').
    + intros; hnf.
      exact (chi_homotopy_rho X T_X M F a a').
  Defined.

Lemma chi (X : Type) (T_X : IsHSet X) (M : MonoidalGroupoid)
  (F : MonoidalFunctor (FMG_MG X) M)
  : MonoidalNatIso (psi (phi F)) F.
Proof.
  srapply @Build_MonoidalNatIso.
  + apply chi_homotopy.
  + simpl. exact (concat_1p _).
  + intros; simpl. exact (concat_1p _).
Defined.

Lemma FMG_FreeFunctor
  : IsFreeFunctor (fun X T_X => FMG_MG X).
Proof.
  exact (Build_IsFreeFunctor (fun X T_X => FMG_MG X) FMG_functor (@phi) (@phi_natural_M) (@psi) (@psi_natural_X) (@theta) (@chi)).
Defined.

End Free.

author: spiceghello

repo: FSMG

save_path: github-repos/coq/spiceghello-FSMG