forked from HoTT/HoTT-Agda
-
Notifications
You must be signed in to change notification settings - Fork 2
/
BAut.agda
30 lines (23 loc) · 1.16 KB
/
BAut.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
{-# OPTIONS --without-K --rewriting --overlapping-instances #-}
open import lib.Basics
open import lib.NType2
open import lib.NConnected
open import lib.types.Nat
open import lib.types.Subtype
open import lib.types.Truncation
-- classifying types of automorphism groups of types
module lib.types.BAut where
BAut : ∀ {i} → Type i → Type (lsucc i)
BAut {i} A = Σ (Type i) λ X → Trunc -1 (A == X)
BAut-prop : ∀ {i} (A : Type i) → SubtypeProp (Type i) (lsucc i)
BAut-prop A = ((λ X → Trunc -1 (A == X)) , (λ X → Trunc-level))
pBAut : ∀ {i} → Type i → Ptd (lsucc i)
de⊙ (pBAut A) = BAut A
pt (pBAut A) = A , [ idp ]
BAut-trunc-path : ∀ {i} (A X : Type i) → (tp : Trunc -1 (A == X))
→ Trunc -1 ((A , [ idp ]) == (X , tp) :> BAut A)
BAut-trunc-path {i} A X = Trunc-elim λ p → [ pair= p prop-has-all-paths-↓ ]
BAut-conn : ∀ {i} (A : Type i) → is-connected 0 (BAut A)
fst (has-level-apply (BAut-conn A)) = [ pt (pBAut A) ]
snd (has-level-apply (BAut-conn A)) = Trunc-elim (λ { (X , tp) → <– (=ₜ-equiv [ A , [ idp ] ] [ X , tp ])
(BAut-trunc-path A X tp) })