(* -*- mode: coq; mode: visual-line -*- *)
Require Import HoTT.Basics HoTT.Types.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Modality Accessible.

Local Open Scope path_scope.


(** * The identity modality *)

(** Everything to say here is fairly trivial. *)

Definition purely : Modality.
Modality
Proof.
Modality
  srapply (Build_Modality (fun _ => Unit) _ _ idmap).
forall T U : Type,
(fun _ : Type => Unit) T ->
forall f : T -> U,
IsEquiv f -> (fun _ : Type => Unit) U
forall T : Type, (fun _ : Type => Unit) (idmap T)
forall T : Type, T -> idmap T
forall (A : Type) (B : idmap A -> Type),
(forall oa : idmap A, (fun _ : Type => Unit) (B oa)) ->
(forall a : A, B (?to' A a)) ->
forall z : idmap A, B z
forall (A : Type) (B : idmap A -> Type)
(B_inO : forall oa : idmap A,
         (fun _ : Type => Unit) (B oa))
(f : forall a : A, B (?to' A a)) (a : A),
?O_ind' A B B_inO f (?to' A a) = f a
forall A : Type,
(fun _ : Type => Unit) A ->
forall z z' : A, (fun _ : Type => Unit) (z = z')
  1-2,6:intros; exact tt.
forall T : Type, T -> idmap T
forall (A : Type) (B : idmap A -> Type),
(forall oa : idmap A, (fun _ : Type => Unit) (B oa)) ->
(forall a : A, B (?to' A a)) ->
forall z : idmap A, B z
forall (A : Type) (B : idmap A -> Type)
(B_inO : forall oa : idmap A,
         (fun _ : Type => Unit) (B oa))
(f : forall a : A, B (?to' A a)) (a : A),
?O_ind' A B B_inO f (?to' A a) = f a
  -
forall T : Type, T -> idmap T intros; assumption.
  -
forall (A : Type) (B : idmap A -> Type),
(forall oa : idmap A, (fun _ : Type => Unit) (B oa)) ->
(forall a : A, B ((fun T : Type => idmap) A a)) ->
forall z : idmap A, B z intros ? ? ? f z; exact (f z).
  -
forall (A : Type) (B : idmap A -> Type)
(B_inO : forall oa : idmap A,
         (fun _ : Type => Unit) (B oa))
(f : forall a : A, B ((fun T : Type => idmap) A a))
(a : A),
(fun (A0 : Type) (B0 : idmap A0 -> Type)
   (_ : forall oa : idmap A0,
        (fun _ : Type => Unit) (B0 oa))
   (f0 : forall a0 : A0,
         B0 ((fun T : Type => idmap) A0 a0))
   (z : idmap A0) => f0 z) A B B_inO f
  ((fun T : Type => idmap) A a) = f a intros; reflexivity.
Defined.

Global Instance accmodality_purely : IsAccModality purely.
IsAccModality purely
Proof.
IsAccModality purely
  unshelve econstructor.
NullGenerators
forall X : Type,
In purely X <-> IsNull_Internal.IsNull ?acc_ngen X
  -
NullGenerators econstructor.
?ngen_indices -> Type
    exact (@Empty_rec Type).
  -
forall X : Type,
In purely X <->
IsNull_Internal.IsNull
  {| ngen_indices := Empty; ngen_type := Empty_rec |}
  X intros X; split.
X: Type
In purely X ->
IsNull_Internal.IsNull
  {| ngen_indices := Empty; ngen_type := Empty_rec |}
  X
X: Type
IsNull_Internal.IsNull
  {| ngen_indices := Empty; ngen_type := Empty_rec |}
  X -> In purely X
    +
X: Type
In purely X ->
IsNull_Internal.IsNull
  {| ngen_indices := Empty; ngen_type := Empty_rec |}
  X intros _ [].
    +
X: Type
IsNull_Internal.IsNull
  {| ngen_indices := Empty; ngen_type := Empty_rec |}
  X -> In purely X intros; exact tt.
Defined.